kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma setCTE_cteCaps_of[wp]:
  "\<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> cteCap cte))\<rbrace>
      setCTE p cte
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp add: cteCaps_of_def) apply wp apply (clarsimp elim!: rsubst[where P=P] intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> cteCap cte))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((map_option cteCap \<circ> ctes_of s)(p \<mapsto> cteCap cte))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((map_option cteCap \<circ> ctes_of s)(p \<mapsto> cteCap cte)) \<Longrightarrow> P (map_option cteCap \<circ> (ctes_of s)(p \<mapsto> cte)) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma capMaster_eq_capBits_eq:
  "capMasterCap cap = capMasterCap cap' \<Longrightarrow> capBits cap = capBits cap'" by (metis capBits_Master)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capMasterCap cap = capMasterCap cap' \<Longrightarrow> capBits cap = capBits cap'
theory CSpace_R

lemma setCTE_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> setCTE ptr cte \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF setCTE_nosch]) apply (simp add: setCTE_def ct_not_inQ_def) apply (rule hoare_weaken_pre) apply (wps setObject_cte_ct) apply (rule setObject_cte_obj_at_tcb') apply (clarsimp simp add: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setCTE ptr cte \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setCTE ptr cte \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setObject ptr cte \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q10\<rbrace> setObject ptr cte \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q10 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P13 prev_s\<rbrace> setObject ptr cte \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P13 s s proof (prove)
goal (6 subgoals):
 1. \<And>prev_s tcb f. (Not \<circ> tcbQueued) (tcbCTable_update f tcb) = (Not \<circ> tcbQueued) tcb
 2. \<And>prev_s tcb f. (Not \<circ> tcbQueued) (tcbVTable_update f tcb) = (Not \<circ> tcbQueued) tcb
 3. \<And>prev_s tcb f. (Not \<circ> tcbQueued) (tcbReply_update f tcb) = (Not \<circ> tcbQueued) tcb
 4. \<And>prev_s tcb f. (Not \<circ> tcbQueued) (tcbCaller_update f tcb) = (Not \<circ> tcbQueued) tcb
 5. \<And>prev_s tcb f. (Not \<circ> tcbQueued) (tcbIPCBufferFrame_update f tcb) = (Not \<circ> tcbQueued) tcb
 6. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_ksCurDomain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace>
      setCTE p cte
   \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>" apply (simp add: setCTE_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject p cte \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setObject_cte_ksDomSchedule[wp]: "\<lbrace> \<lambda>s. P (ksDomSchedule s) \<rbrace> setObject ptr (v::cte) \<lbrace> \<lambda>_ s. P (ksDomSchedule s) \<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_cte_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject ptr v \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject v (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace>
      setCTE p cte
   \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" apply (simp add: setCTE_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject p cte \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_tcbDomain_inv[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace> setObject ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_tcbPriority_inv[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> setObject ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cteInsert_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> cteInsert a b c \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> cteInsert a b c \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> cteInsert a b c \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> cteInsert a b c \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> cteInsert a b c \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> cteInsert a b c \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>d aa t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> cteInsert a b c \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setObject_cte_domIdx:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject t (v::cte) \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace>" by (clarsimp simp: valid_def setCTE_def[symmetric] dest!: setCTE_pspace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace>
theory CSpace_R

lemma ran_split:
  "inj_on m (dom m)
    \<Longrightarrow> ran (\<lambda>x. if P x then m' x else m x)
        = ((ran m - (ran (restrict_map m (Collect P))))
            \<union> (ran (restrict_map m' (Collect P))))" apply (clarsimp simp: ran_def restrict_map_def set_eq_iff) apply (safe, simp_all) apply (auto dest: inj_onD[OF _ trans[OF _ sym]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on m (dom m) \<Longrightarrow> ran (\<lambda>x. if P x then m' x else m x) = ran m - ran (m |` Collect P) \<union> ran (m' |` Collect P) proof (prove)
goal (1 subgoal):
 1. \<And>x. inj_on m (dom m) \<Longrightarrow> (\<exists>a. (P a \<longrightarrow> m' a = Some x) \<and> (\<not> P a \<longrightarrow> m a = Some x)) = ((\<exists>a. m a = Some x) \<and> (\<forall>a. P a \<longrightarrow> m a \<noteq> Some x) \<or> (\<exists>a. (P a \<longrightarrow> m' a = Some x) \<and> P a)) proof (prove)
goal (8 subgoals):
 1. \<And>x a. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; \<not> P a; m a = Some x\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some x
 2. \<And>x a aa. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; \<not> P a; m a = Some x; P aa; m aa = Some x\<rbrakk> \<Longrightarrow> False
 3. \<And>x a. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; m' a = Some x; P a\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some x
 4. \<And>x a aa. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; m' a = Some x; P a; P aa; m aa = Some x\<rbrakk> \<Longrightarrow> False
 5. \<And>x a. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; m' a = Some x; m a = Some x\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some x
 6. \<And>x a aa. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<and> m' a \<noteq> Some x \<or> \<not> P a; m' a = Some x; m a = Some x; P aa; m aa = Some x\<rbrakk> \<Longrightarrow> False
 7. \<And>x a. \<lbrakk>inj_on m (dom m); \<forall>a. P a \<longrightarrow> m a \<noteq> Some x; m a = Some x\<rbrakk> \<Longrightarrow> \<exists>a. (P a \<longrightarrow> m' a = Some x) \<and> (\<not> P a \<longrightarrow> m a = Some x)
 8. \<And>x a. \<lbrakk>inj_on m (dom m); P a; m' a = Some x\<rbrakk> \<Longrightarrow> \<exists>a. (P a \<longrightarrow> m' a = Some x) \<and> (\<not> P a \<longrightarrow> m a = Some x) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma ran_split_eq:
  "inj_on m (dom m)
    \<Longrightarrow> \<forall>x. \<not> P x \<longrightarrow> m' x = m x
    \<Longrightarrow> ran m'
        = ((ran m - (ran (restrict_map m (Collect P))))
            \<union> (ran (restrict_map m' (Collect P))))" apply (rule trans[rotated], erule ran_split) apply (rule arg_cong[where f=ran]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on m (dom m); \<forall>x. \<not> P x \<longrightarrow> m' x = m x\<rbrakk> \<Longrightarrow> ran m' = ran m - ran (m |` Collect P) \<union> ran (m' |` Collect P) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on m (dom m); \<forall>x. \<not> P x \<longrightarrow> m' x = m x\<rbrakk> \<Longrightarrow> ran m' = ran (\<lambda>x. if P x then m' x else m x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on m (dom m); \<forall>x. \<not> P x \<longrightarrow> m' x = m x\<rbrakk> \<Longrightarrow> m' = (\<lambda>x. if P x then m' x else m x) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma restrict_map_is_map_comp:
  "restrict_map m S = m \<circ>\<^sub>m (\<lambda>x. if x \<in> S then Some x else None)" by (simp add: restrict_map_def map_comp_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` S = m \<circ>\<^sub>m (\<lambda>x. if x \<in> S then Some x else None)
theory CSpace_R

lemma untypedZeroRange_to_usableCapRange:
  "untypedZeroRange c = Some (x, y) \<Longrightarrow> valid_cap' c s
    \<Longrightarrow> isUntypedCap c \<and> usableUntypedRange c = {x .. y}
        \<and> x \<le> y" apply (clarsimp simp: untypedZeroRange_def split: if_split_asm) apply (frule(1) usableUntypedRange_empty) apply (clarsimp simp: isCap_simps valid_cap_simps' max_free_index_def) apply (simp add: getFreeRef_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>untypedZeroRange c = Some (x, y); valid_cap' c s\<rbrakk> \<Longrightarrow> isUntypedCap c \<and> usableUntypedRange c = {x..y} \<and> x \<le> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; isUntypedCap c; capFreeIndex c \<noteq> max_free_index (capBlockSize c); \<not> capIsDevice c; x = getFreeRef (capPtr c) (capFreeIndex c); y = capPtr c + 2 ^ capBlockSize c - 1\<rbrakk> \<Longrightarrow> usableUntypedRange c = {getFreeRef (capPtr c) (capFreeIndex c)..capPtr c + 2 ^ capBlockSize c - 1} \<and> getFreeRef (capPtr c) (capFreeIndex c) \<le> capPtr c + 2 ^ capBlockSize c - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; isUntypedCap c; capFreeIndex c \<noteq> max_free_index (capBlockSize c); \<not> capIsDevice c; x = getFreeRef (capPtr c) (capFreeIndex c); y = capPtr c + 2 ^ capBlockSize c - 1; (usableUntypedRange c = {}) = (capFreeIndex c = maxFreeIndex (capBlockSize c))\<rbrakk> \<Longrightarrow> usableUntypedRange c = {getFreeRef (capPtr c) (capFreeIndex c)..capPtr c + 2 ^ capBlockSize c - 1} \<and> getFreeRef (capPtr c) (capFreeIndex c) \<le> capPtr c + 2 ^ capBlockSize c - 1 proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>f \<noteq> 2 ^ v1; \<not> d; x = getFreeRef v0 f; y = v0 + 2 ^ v1 - 1; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; c = capability.UntypedCap False v0 v1 f; capAligned (capability.UntypedCap False v0 v1 f); valid_untyped' False v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> v0 + word_of_nat f = getFreeRef v0 f \<and> getFreeRef v0 f \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma ran_restrict_map_insert:
  "ran (restrict_map m (insert x S)) = (set_option (m x) \<union> ran (restrict_map m S))" by (auto simp add: ran_def restrict_map_Some_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (m |` insert x S) = set_option (m x) \<union> ran (m |` S)
theory CSpace_R

lemma valid_NullCap:
  "valid_cap' NullCap = \<top>" by (rule ext, simp add: valid_cap_simps' capAligned_def word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' capability.NullCap = (\<lambda>_. True)
theory CSpace_R

lemma deriveCap_valid [wp]:
  "\<lbrace>\<lambda>s. s \<turnstile>' c\<rbrace>
  deriveCap slot c
  \<lbrace>\<lambda>rv s. s \<turnstile>' rv\<rbrace>,-" apply (simp add: deriveCap_def split del: if_split) apply (rule hoare_pre) apply (wp arch_deriveCap_valid | simp add: o_def)+ apply (simp add: valid_NullCap) apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' c\<rbrace> global.deriveCap slot c \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' c\<rbrace> if isZombie c then returnOk capability.NullCap else if isIRQControlCap c then returnOk capability.NullCap else if isUntypedCap c then doE y <- ensureNoChildren slot;
returnOk c
odE else if isReplyCap c then returnOk capability.NullCap else if isArchObjectCap c then Arch.deriveCap slot (capCap c) else returnOk c \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'12\<rbrace> if isZombie c then returnOk capability.NullCap else if isIRQControlCap c then returnOk capability.NullCap else if isUntypedCap c then doE y <- ensureNoChildren slot;
returnOk c
odE else if isReplyCap c then returnOk capability.NullCap else if isArchObjectCap c then Arch.deriveCap slot (capCap c) else returnOk c \<lbrace>valid_cap'\<rbrace>, -
 2. \<And>s. valid_cap' c s \<Longrightarrow> ?P'12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' c s \<Longrightarrow> (isZombie c \<longrightarrow> valid_cap' capability.NullCap s) \<and> (\<not> isZombie c \<longrightarrow> (isIRQControlCap c \<longrightarrow> valid_cap' capability.NullCap s) \<and> (\<not> isIRQControlCap c \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> (isReplyCap c \<longrightarrow> valid_cap' capability.NullCap s) \<and> (\<not> isReplyCap c \<longrightarrow> isArchObjectCap c \<longrightarrow> valid_cap' (capability.ArchObjectCap (capCap c)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' c s \<Longrightarrow> \<not> isZombie c \<longrightarrow> \<not> isIRQControlCap c \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> isReplyCap c \<longrightarrow> isArchObjectCap c \<longrightarrow> valid_cap' (capability.ArchObjectCap (capCap c)) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma lookup_cap_valid':
  "\<lbrace>valid_objs'\<rbrace> lookupCap t c \<lbrace>valid_cap'\<rbrace>, -" apply (simp add: lookupCap_def lookupCapAndSlot_def
                   lookupSlotForThread_def split_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupCap t c \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> liftME fst (doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
p <- CSpace_H.resolveAddressBits threadRoot c (size c);
returnOk (fst p)
odE;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE) \<lbrace>valid_cap'\<rbrace>, - proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma capAligned_Null [simp]:
  "capAligned NullCap" by (simp add: capAligned_def is_aligned_def word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capAligned capability.NullCap
theory CSpace_R

lemma lookupSlotForCNodeOp_inv'[wp]:
  "\<lbrace>P\<rbrace> lookupSlotForCNodeOp src croot ptr depth \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp hoare_drop_imps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookupSlotForCNodeOp src croot ptr depth \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if isCNodeCap croot then doE y <- rangeCheck depth (Suc 0) (size ptr);
lookupErrorOnFailure src (doE result <- CSpace_H.resolveAddressBits croot ptr depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup src Fault_H.lookup_failure.InvalidRoot) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q7\<rbrace> if isCNodeCap croot then doE y <- rangeCheck depth (Suc 0) (size ptr);
lookupErrorOnFailure src (doE result <- CSpace_H.resolveAddressBits croot ptr depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup src Fault_H.lookup_failure.InvalidRoot) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q7 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (isCNodeCap croot \<longrightarrow> P s \<and> P s \<and> P s \<and> P s \<and> True) \<and> (\<not> isCNodeCap croot \<longrightarrow> P s \<and> True) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma loadWordUser_inv [wp]:
  "\<lbrace>P\<rbrace> loadWordUser p \<lbrace>\<lambda>rv. P\<rbrace>" unfolding loadWordUser_def by (wp dmo_inv' loadWord_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> loadWordUser p \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do stateAssert (pointerInUserData p) [];
doMachineOp $ loadWord p
od \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_R

lemma capTransferFromWords_inv:
  "\<lbrace>P\<rbrace> capTransferFromWords buffer \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: capTransferFromWords_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> capTransferFromWords buffer \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do w0 <- loadWordUser buffer;
w1 <- loadWordUser (buffer + word_of_nat wordSize);
w2 <- loadWordUser (buffer + 2 * word_of_nat wordSize);
return (CT w0 w1 (unat w2))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma lct_inv' [wp]:
  "\<lbrace>P\<rbrace> loadCapTransfer b \<lbrace>\<lambda>rv. P\<rbrace>" unfolding loadCapTransfer_def apply (wp capTransferFromWords_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> loadCapTransfer b \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do intSize <- return (fromIntegral wordSize);
offset <- return (msgMaxLength + msgMaxExtraCaps + 2);
capTransferFromWords (b + PPtr (offset * intSize))
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma maskCapRightsNull [simp]:
  "maskCapRights R NullCap = NullCap" by (simp add: maskCapRights_def isCap_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.maskCapRights R capability.NullCap = capability.NullCap
theory CSpace_R

lemma maskCapRightsUntyped [simp]:
  "maskCapRights R (UntypedCap d r n f) = UntypedCap d r n f" by (simp add: maskCapRights_def isCap_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.maskCapRights R (capability.UntypedCap d r n f) = capability.UntypedCap d r n f
theory CSpace_R

lemma ensureEmpty_inv[wp]:
  "\<lbrace>P\<rbrace> ensureEmptySlot p \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: ensureEmptySlot_def unlessE_whenE whenE_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensureEmptySlot p \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_R

lemma untyped_derived_eq_ArchObjectCap:
  "untyped_derived_eq (capability.ArchObjectCap cap) = \<top>" by (rule ext, simp add: untyped_derived_eq_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_derived_eq (capability.ArchObjectCap cap) = (\<lambda>_. True)