kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_I

lemma setCTE_valid_objs'[wp]:
  "\<lbrace>valid_objs' and (valid_cap' (cteCap cte)) \<rbrace>
    setCTE p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" unfolding setCTE_def apply (rule setObject_valid_objs') apply (clarsimp simp: prod_eq_iff lookupAround2_char1 updateObject_cte objBits_simps) apply (clarsimp simp: prod_eq_iff lookupAround2_char1
                         updateObject_cte in_monad typeError_def
                         valid_obj'_def valid_tcb'_def valid_cte'_def
                         tcb_cte_cases_def
                  split: kernel_object.split_asm if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' (cteCap cte)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' (cteCap cte)\<rbrace> setObject p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject cte ko p x n s); valid_cap' (cteCap cte) s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal (1 subgoal):
 1. \<And>x ko s ko' s'. \<lbrakk>(ko', s') \<in> fst ((case ko of KOTCB tcb \<Rightarrow> do alignCheck x (objBits tcb);
magnitudeCheck x (snd (lookupAround2 p (ksPSpace s))) (objBits tcb);
if p - x = tcbVTableSlot << cteSizeBits then return (KOTCB (tcbVTable_update (\<lambda>_. cte) tcb)) else if p - x = tcbCTableSlot << cteSizeBits then return (KOTCB (tcbCTable_update (\<lambda>_. cte) tcb)) else if p - x = tcbReplySlot << cteSizeBits then return (KOTCB (tcbReply_update (\<lambda>_. cte) tcb)) else if p - x = tcbCallerSlot << cteSizeBits then return (KOTCB (tcbCaller_update (\<lambda>_. cte) tcb)) else if p - x = tcbIPCBufferSlot << cteSizeBits then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (p = x) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits cte);
return (KOCTE cte)
od | _ \<Rightarrow> typeError [] ko) s); valid_cap' (cteCap cte) s; valid_obj' ko s; x \<le> p; ksPSpace s x = Some ko; \<forall>z. x < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma getCTE_cte_wp_at:
  "\<lbrace>\<top>\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p\<rbrace>" apply (clarsimp simp: valid_def cte_wp_at'_def getCTE_def) apply (frule state_unchanged [OF getObject_cte_inv]) apply simp apply (drule getObject_cte_det, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p b) = {(a, b)} proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (getObject p s); s = b\<rbrakk> \<Longrightarrow> fst (getObject p b) = {(a, b)} proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (getObject p b); s = b\<rbrakk> \<Longrightarrow> fst (getObject p b) = {(a, b)} proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma getCTE_sp:
  "\<lbrace>P\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p and P\<rbrace>" apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule getCTE_cte_wp_at) apply (rule getCTE_inv) apply (rule conjI, rule TrueI, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p and P\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> getCTE p \<lbrace>?Q\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = rv) p and P) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P4\<rbrace> getCTE p \<lbrace>?Q4\<rbrace>
 2. \<lbrace>?P'4\<rbrace> getCTE p \<lbrace>?Q'4\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?P'4 s
 4. \<And>rv s. ?Q4 rv s \<and> ?Q'4 rv s \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = rv) p and P) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'4\<rbrace> getCTE p \<lbrace>?Q'4\<rbrace>
 2. \<And>s. P s \<Longrightarrow> True \<and> ?P'4 s
 3. \<And>rv s. cte_wp_at' (\<lambda>c. c = rv) p s \<and> ?Q'4 rv s \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = rv) p and P) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> True \<and> ?P'4 s
 2. \<And>rv s. cte_wp_at' (\<lambda>c. c = rv) p s \<and> ?P'4 s \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = rv) p and P) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cte_wp_at' (\<lambda>c. c = rv) p s \<and> P s \<Longrightarrow> (cte_wp_at' (\<lambda>c. c = rv) p and P) s proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma getCTE_ctes_wp:
  "\<lbrace>\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s\<rbrace> getCTE ptr \<lbrace>P\<rbrace>" apply (rule hoare_strengthen_post, rule getCTE_sp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s\<rbrace> getCTE ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (cte_wp_at' (\<lambda>c. c = rv) ptr and (\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s)) s \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma updateMDB_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace> updateMDB m p \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (clarsimp simp add: updateMDB_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> updateMDB m p \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> \<lbrace>valid_objs'\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. p (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma cte_overwrite:
  "cteMDBNode_update (\<lambda>x. m) (cteCap_update (\<lambda>x. c) v) = CTE c m" by (cases v, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteMDBNode_update (\<lambda>x. m) (cteCap_update (\<lambda>x. c) v) = CTE c m
theory CSpace_I

lemma setCTE_no_0_obj' [wp]:
  "\<lbrace>no_0_obj'\<rbrace> setCTE p c \<lbrace>\<lambda>_. no_0_obj'\<rbrace>" by (simp add: setCTE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_0_obj'\<rbrace> setCTE p c \<lbrace>\<lambda>_. no_0_obj'\<rbrace>
theory CSpace1_R

lemma isMDBParentOf_CTE1:
  "isMDBParentOf (CTE cap node) cte =
   (\<exists>cap' node'. cte = CTE cap' node' \<and> sameRegionAs cap cap'
      \<and> mdbRevocable node
      \<and> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow>
           capEPBadge cap = capEPBadge cap' \<and> \<not> mdbFirstBadged node')
      \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> 0 \<longrightarrow>
           capNtfnBadge cap = capNtfnBadge cap' \<and> \<not> mdbFirstBadged node'))" apply (simp add: isMDBParentOf_def Let_def split: cte.splits split del: if_split) apply (clarsimp simp: Let_def) apply (fastforce simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap node) cte = (\<exists>cap' node'. cte = CTE cap' node' \<and> global.sameRegionAs cap cap' \<and> mdbRevocable node \<and> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow> capEPBadge cap = capEPBadge cap' \<and> \<not> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> 0 \<longrightarrow> capNtfnBadge cap = capNtfnBadge cap' \<and> \<not> mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<forall>x1 x2. cte = CTE x1 x2 \<longrightarrow> (if \<not> mdbRevocable node then False else if \<not> global.sameRegionAs cap x1 then False else if isEndpointCap cap \<and> capEPBadge cap \<noteq> 0 then capEPBadge cap = capEPBadge x1 \<and> \<not> mdbFirstBadged x2 else if isNotificationCap cap \<and> capNtfnBadge cap \<noteq> 0 then capNtfnBadge cap = capNtfnBadge x1 \<and> \<not> mdbFirstBadged x2 else True) = (global.sameRegionAs cap x1 \<and> mdbRevocable node \<and> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow> capEPBadge cap = capEPBadge x1 \<and> \<not> mdbFirstBadged x2) \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> 0 \<longrightarrow> capNtfnBadge cap = capNtfnBadge x1 \<and> \<not> mdbFirstBadged x2)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbRevocable node; global.sameRegionAs cap x1; isNotificationCap cap; capNtfnBadge cap \<noteq> 0; isEndpointCap cap; capEPBadge cap \<noteq> 0; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> (capEPBadge cap = capEPBadge x1 \<and> \<not> mdbFirstBadged x2) = (capEPBadge cap = capEPBadge x1 \<and> \<not> mdbFirstBadged x2 \<and> capNtfnBadge cap = capNtfnBadge x1 \<and> \<not> mdbFirstBadged x2) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_CTE:
  "isMDBParentOf (CTE cap node) cte =
   (\<exists>cap' node'. cte = CTE cap' node' \<and> sameRegionAs cap cap'
      \<and> mdbRevocable node
      \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'))" apply (simp add: isMDBParentOf_CTE1) apply (intro arg_cong[where f=Ex] ext conj_cong refl) apply (cases cap, simp_all add: isCap_simps) apply (auto elim!: sameRegionAsE simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap node) cte = (\<exists>cap' node'. cte = CTE cap' node' \<and> global.sameRegionAs cap cap' \<and> mdbRevocable node \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. (\<exists>cap' node'. cte = CTE cap' node' \<and> global.sameRegionAs cap cap' \<and> mdbRevocable node \<and> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow> capEPBadge cap = capEPBadge cap' \<and> \<not> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> 0 \<longrightarrow> capNtfnBadge cap = capNtfnBadge cap' \<and> \<not> mdbFirstBadged node')) = (\<exists>cap' node'. cte = CTE cap' node' \<and> global.sameRegionAs cap cap' \<and> mdbRevocable node \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<And>cap' node'. \<lbrakk>cte = CTE cap' node'; global.sameRegionAs cap cap'; mdbRevocable node\<rbrakk> \<Longrightarrow> ((isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> 0 \<longrightarrow> capEPBadge cap = capEPBadge cap' \<and> \<not> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> 0 \<longrightarrow> capNtfnBadge cap = capNtfnBadge cap' \<and> \<not> mdbFirstBadged node')) = ((capBadge cap, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node')) proof (prove)
goal (2 subgoals):
 1. \<And>cap' node' x31 x32 x33 x34. \<lbrakk>cte = CTE cap' node'; global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) cap'; mdbRevocable node; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (x32 \<noteq> 0 \<longrightarrow> x32 = capNtfnBadge cap' \<and> \<not> mdbFirstBadged node') = ((Some x32, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node'))
 2. \<And>cap' node' x51 x52 x53 x54 x55 x56. \<lbrakk>cte = CTE cap' node'; global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap'; mdbRevocable node; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (x52 \<noteq> 0 \<longrightarrow> x52 = capEPBadge cap' \<and> \<not> mdbFirstBadged node') = ((Some x52, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged node')) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma parentOf_trans:
  "\<lbrakk> s \<turnstile> a parentOf b; s \<turnstile> b parentOf c \<rbrakk> \<Longrightarrow> s \<turnstile> a parentOf c" by (auto simp: parentOf_def elim: isMDBParentOf_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> a parentOf b; s \<turnstile> b parentOf c\<rbrakk> \<Longrightarrow> s \<turnstile> a parentOf c
theory CSpace1_R

lemma subtree_parent:
  "s \<turnstile> a \<rightarrow> b \<Longrightarrow> s \<turnstile> a parentOf b" by (erule subtree.induct) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> a \<rightarrow> b \<Longrightarrow> s \<turnstile> a parentOf b
theory CSpace1_R

lemma leadsto_is_prev:
  "\<lbrakk> m \<turnstile> p \<leadsto> c; m c = Some (CTE cap node);
    valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow>
  p = mdbPrev node" by (fastforce simp add: next_unfold' valid_dlist_def Let_def no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto> c; m c = Some (CTE cap node); valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> p = mdbPrev node
theory CSpace1_R

lemma subtree_target_Some:
  "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m b \<noteq> None" by (erule subtree.cases) (auto simp: parentOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> a \<rightarrow> b \<Longrightarrow> m b \<noteq> None
theory CSpace1_R

lemma subtree_prev_loop:
  "\<lbrakk> m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow>
  m \<turnstile> p \<rightarrow> mdbPrev node = False" apply clarsimp apply (frule subtree_target_Some) apply (drule subtree_mdb_next) apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ p") apply (simp add: no_loops_def) apply (erule trancl_into_trancl) apply (clarsimp simp: mdb_next_unfold) apply (fastforce simp: next_unfold' valid_dlist_def no_0_def Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> mdbPrev node = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m \<turnstile> p \<rightarrow> mdbPrev node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m \<turnstile> p \<rightarrow> mdbPrev node; m (mdbPrev node) \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) \<noteq> None; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) \<noteq> None; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev node; m \<turnstile> p \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) \<noteq> None; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) \<noteq> None; m \<turnstile> p \<leadsto>\<^sup>+ mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) \<noteq> None\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m p = Some (CTE cap node); no_loops m; valid_dlist m; no_0 m; m (mdbPrev node) = Some y\<rbrakk> \<Longrightarrow> p = mdbNext (cteMDBNode y) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma subtree_trans: "\<lbrakk> s \<turnstile> a \<rightarrow> b; s \<turnstile> b \<rightarrow> c \<rbrakk> \<Longrightarrow> s \<turnstile> a \<rightarrow> c" by (rule subtree_trans_lemma)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> a \<rightarrow> b; s \<turnstile> b \<rightarrow> c\<rbrakk> \<Longrightarrow> s \<turnstile> a \<rightarrow> c
theory CSpace1_R

lemma same_arch_region_as_relation:
  "\<lbrakk>acap_relation c d; acap_relation c' d'\<rbrakk> \<Longrightarrow>
  arch_same_region_as c c' =
  sameRegionAs (ArchObjectCap d) (ArchObjectCap d')" apply (cases c) apply ((cases c', auto simp: ARM_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acap_relation c d; acap_relation c' d'\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d') proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>acap_relation c d; acap_relation c' d'; c = arch_cap.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d')
 2. \<lbrakk>acap_relation c d; acap_relation c' d'; c = arch_cap.ASIDControlCap\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d')
 3. \<And>x31 x32 x33 x34 x35. \<lbrakk>acap_relation c d; acap_relation c' d'; c = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d')
 4. \<And>x41 x42. \<lbrakk>acap_relation c d; acap_relation c' d'; c = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d')
 5. \<And>x51 x52. \<lbrakk>acap_relation c d; acap_relation c' d'; c = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> arch_same_region_as c c' = global.sameRegionAs (capability.ArchObjectCap d) (capability.ArchObjectCap d') proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma is_phyiscal_relation:
  "cap_relation c c' \<Longrightarrow> is_physical c = isPhysicalCap c'" by (auto simp: is_physical_def arch_is_physical_def
           split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> is_physical c = global.isPhysicalCap c'
theory CSpace1_R

lemma obj_ref_of_relation:
  "\<lbrakk> cap_relation c c'; capClass c' = PhysicalClass \<rbrakk> \<Longrightarrow>
  obj_ref_of c = capUntypedPtr c'" by (cases c; simp) (rename_tac arch_cap, case_tac arch_cap, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; capClass c' = PhysicalClass\<rbrakk> \<Longrightarrow> obj_ref_of c = global.capUntypedPtr c'
theory CSpace1_R

lemma obj_size_relation:
  "\<lbrakk> cap_relation c c'; capClass c' = PhysicalClass \<rbrakk> \<Longrightarrow>
  obj_size c = capUntypedSize c'" apply (cases c, simp_all add: objBits_simps' zbits_map_def
                                cte_level_bits_def
                         split: option.splits sum.splits) apply (rename_tac arch_cap) apply (case_tac arch_cap,
    simp_all add: objBits_def ARM_H.capUntypedSize_def asid_low_bits_def
                  pageBits_def ptBits_def pteBits_def pdBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; capClass c' = PhysicalClass\<rbrakk> \<Longrightarrow> obj_size c = global.capUntypedSize c' proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; capClass c' = PhysicalClass; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> 2 ^ arch_obj_size x12 = global.capUntypedSize c' proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>\<exists>a'. acap_relation arch_cap a' \<and> c' = capability.ArchObjectCap a'; capClass c' = PhysicalClass; c = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> 2 ^ arch_obj_size arch_cap = global.capUntypedSize c' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma tcb_cases_related:
  "tcb_cap_cases ref = Some (getF, setF, restr) \<Longrightarrow>
    \<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF'))
               \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')))" by (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1
                cte_map_def' tcb_relation_def
         split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_cases ref = Some (getF, setF, restr) \<Longrightarrow> \<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF')) \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')))
theory CSpace1_R

lemma pspace_relation_ctes_ofI:
  "\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
    cte_wp_at ((=) c) slot s; pspace_aligned' s';
     pspace_distinct' s' \<rbrakk>
  \<Longrightarrow> \<exists>cte. ctes_of s' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)" apply (cases slot, clarsimp) apply (drule(3) pspace_relation_cte_wp_at) apply (simp add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cte_wp_at ((=) c) (a, b) s; pspace_aligned' s'; pspace_distinct' s'; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cap_relation c (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) c) (a, b) s; pspace_aligned' s'; pspace_distinct' s'; slot = (a, b); cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s' (cte_map (a, b)) = Some cte \<and> cap_relation c (cteCap cte) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma getCTE_wp:
  "\<lbrace>\<lambda>s. cte_at' p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> Q cte s)\<rbrace> getCTE p \<lbrace>Q\<rbrace>" apply (clarsimp simp add: getCTE_def valid_def cte_wp_at'_def) apply (drule getObject_cte_det) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> Q cte s)\<rbrace> getCTE p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(\<exists>cte. fst (getObject p s) = {(cte, s)}) \<longrightarrow> (\<exists>cte. fst (getObject p s) = {(cte, s)} \<and> Q cte s); (a, b) \<in> fst (getObject p s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(\<exists>cte. fst (getObject p s) = {(cte, s)}) \<longrightarrow> (\<exists>cte. fst (getObject p s) = {(cte, s)} \<and> Q cte s); fst (getObject p s) = {(a, s)} \<and> b = s\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!