kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma revokable_plus_orderD:
  "\<lbrakk> revokable' old new; (capBadge old, capBadge new) \<in> capBadge_ordering P;
       capMasterCap old = capMasterCap new \<rbrakk>
      \<Longrightarrow> (isUntypedCap new \<or> (\<exists>x. capBadge old = Some 0 \<and> capBadge new = Some x \<and> x \<noteq> 0))" by (clarsimp simp: revokable'_def isCap_simps split: if_split_asm capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>revokable' old new; (capBadge old, capBadge new) \<in> capBadge_ordering P; capMasterCap old = capMasterCap new\<rbrakk> \<Longrightarrow> isUntypedCap new \<or> (\<exists>x. capBadge old = Some 0 \<and> capBadge new = Some x \<and> x \<noteq> 0)
theory CSpace1_R

lemma sameRegionAs_update_untyped:
  "RetypeDecls_H.sameRegionAs (capability.UntypedCap d a b c) =
   RetypeDecls_H.sameRegionAs (capability.UntypedCap d a b c')" apply (rule ext) apply (case_tac x) apply (clarsimp simp:sameRegionAs_def isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs (capability.UntypedCap d a b c) = global.sameRegionAs (capability.UntypedCap d a b c') proof (prove)
goal (1 subgoal):
 1. \<And>x. global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x proof (prove)
goal (12 subgoals):
 1. \<And>x x1. x = capability.ThreadCap x1 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 2. \<And>x. x = capability.NullCap \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 3. \<And>x x31 x32 x33 x34. x = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 4. \<And>x x4. x = capability.IRQHandlerCap x4 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 5. \<And>x x51 x52 x53 x54 x55 x56. x = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 6. \<And>x. x = capability.DomainCap \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 7. \<And>x x71 x72 x73. x = capability.Zombie x71 x72 x73 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 8. \<And>x x8. x = capability.ArchObjectCap x8 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 9. \<And>x x91 x92 x93. x = capability.ReplyCap x91 x92 x93 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
 10. \<And>x x101 x102 x103 x104. x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d a b c) x = global.sameRegionAs (capability.UntypedCap d a b c') x
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma sameRegionAs_update_untyped':
  "RetypeDecls_H.sameRegionAs cap (capability.UntypedCap d a b f) =
   RetypeDecls_H.sameRegionAs cap (capability.UntypedCap d a b f')" apply (case_tac cap) apply (clarsimp simp:sameRegionAs_def isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f') proof (prove)
goal (12 subgoals):
 1. \<And>x1. cap = capability.ThreadCap x1 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 2. cap = capability.NullCap \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 3. \<And>x31 x32 x33 x34. cap = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 4. \<And>x4. cap = capability.IRQHandlerCap x4 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 5. \<And>x51 x52 x53 x54 x55 x56. cap = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 6. cap = capability.DomainCap \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 7. \<And>x71 x72 x73. cap = capability.Zombie x71 x72 x73 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 8. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 9. \<And>x91 x92 x93. cap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
 10. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> global.sameRegionAs cap (capability.UntypedCap d a b f) = global.sameRegionAs cap (capability.UntypedCap d a b f')
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma n_dest_child:
  "n \<turnstile> src \<rightarrow> dest" apply (rule subtree.direct_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def src dest n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> dest proof (prove)
goal (3 subgoals):
 1. n \<turnstile> src \<leadsto> dest
 2. dest \<noteq> 0
 3. n \<turnstile> src parentOf dest proof (prove)
goal (2 subgoals):
 1. dest \<noteq> 0
 2. n \<turnstile> src parentOf dest proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src parentOf dest proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma n_to_dest [simp]:
  "n \<turnstile> p \<leadsto> dest = (p = src)" by (simp add: n_direct_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> dest = (p = src)
theory CSpace1_R

lemma descendants:
  "descendants_of' p n =
   (if src \<in> descendants_of' p m \<or> p = src
   then descendants_of' p m \<union> {dest} else descendants_of' p m)" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (fastforce dest!: parent_n_m dest: parent_m_n simp: n_dest_child split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = (if src \<in> descendants_of' p m \<or> p = src then descendants_of' p m \<union> {dest} else descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p n) = (x \<in> (if src \<in> descendants_of' p m \<or> p = src then descendants_of' p m \<union> {dest} else descendants_of' p m)) proof (prove)
goal (1 subgoal):
 1. \<And>x. (m \<turnstile> p \<rightarrow> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = (x = dest \<or> m \<turnstile> p \<rightarrow> x)) \<and> (p = src \<longrightarrow> n \<turnstile> src \<rightarrow> x = (x = dest \<or> m \<turnstile> src \<rightarrow> x)) \<and> (\<not> m \<turnstile> p \<rightarrow> src \<and> p \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma src_no_parent:
  "m \<turnstile> src \<rightarrow> p = False" by (clarsimp dest!: subtree_parent simp: src_no_mdb_parent parentOf_def src)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<rightarrow> p = False
theory CSpace1_R

lemma src_no_parent_n [simp]:
  "n \<turnstile> src \<rightarrow> p = False" apply clarsimp apply (erule subtree.induct) apply (simp add: n_direct_eq) apply (clarsimp simp: parentOf_def n src dest new_src_def
                         new_dest_def no_child) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> p = False proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> src \<leadsto> c'; c' \<noteq> 0; n \<turnstile> src parentOf c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>n \<turnstile> src \<rightarrow> c'; False; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. n \<turnstile> src parentOf dest \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>n \<turnstile> src \<rightarrow> c'; False; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> src \<rightarrow> c'; False; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> src parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma parent_n_eq:
  "n \<turnstile> p \<rightarrow> p' = (if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p')" apply (rule iffI) apply (erule parent_n) apply (simp split: if_split_asm) apply (drule parent_m, simp) apply (drule parent_m, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<rightarrow> p' = (if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p') proof (prove)
goal (2 subgoals):
 1. n \<turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p'
 2. if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. if p' = dest then m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' = dest; m \<turnstile> p \<rightarrow> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<lbrakk>p' \<noteq> dest; m \<turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> dest; m \<turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> p' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma descendants:
  "descendants_of' p n =
   descendants_of' p m \<union> (if src \<in> descendants_of' p m then {dest} else {})" by (rule set_eqI) (simp add: descendants_of'_def parent_n_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = descendants_of' p m \<union> (if src \<in> descendants_of' p m then {dest} else {})
theory CSpace1_R

lemma mdb_None:
  assumes F: "\<And>p'. cte_map p \<in> descendants_of' p' m' \<Longrightarrow> False"
  assumes R: "cdt_relation (swp cte_at s) (cdt s) m'"
  assumes "valid_mdb s"
  shows "cdt s p = None" apply (simp add: descendants_of_None [symmetric]) apply clarsimp apply (frule descendants_of_cte_at2, rule assms) apply (insert R) apply (simp add: cdt_relation_def) apply (erule allE, erule allE, erule (1) impE) apply (rule_tac p'="cte_map (a,b)" in F) apply (drule sym) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<forall>a b. p \<notin> descendants_of (a, b) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. p \<in> descendants_of (a, b) (cdt s) \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; \<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> cte_map ` descendants_of (a, b) (cdt s) = descendants_of' (cte_map (a, b)) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; cte_map ` descendants_of (a, b) (cdt s) = descendants_of' (cte_map (a, b)) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; cte_map ` descendants_of (a, b) (cdt s) = descendants_of' (cte_map (a, b)) m'\<rbrakk> \<Longrightarrow> cte_map p \<in> descendants_of' (cte_map (a, b)) m' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<in> descendants_of (a, b) (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; descendants_of' (cte_map (a, b)) m' = cte_map ` descendants_of (a, b) (cdt s)\<rbrakk> \<Longrightarrow> cte_map p \<in> descendants_of' (cte_map (a, b)) m' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma no_fail_updateMDB [wp]:
  "no_fail (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_at' p s) (updateMDB p f)" apply (simp add: updateMDB_def) apply (rule no_fail_pre, wp) apply (simp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s) (updateMDB p f) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s) (if p = 0 then return () else do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> (if p = 0 then \<lambda>_. True else cte_wp_at' (\<lambda>_. True) p and cte_wp_at' (\<lambda>_. True) p) s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateMDB_cte_at' [wp]:
 "\<lbrace>cte_at' p\<rbrace>
  updateMDB x y
  \<lbrace>\<lambda>uu. cte_at' p\<rbrace>" by (wpsimp wp: updateMDB_weak_cte_wp_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) p\<rbrace> updateMDB x y \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>_. True) p\<rbrace>
theory CSpace1_R

lemma updateCap_cte_at' [wp]:
 "\<lbrace>cte_at' p\<rbrace> updateCap c p' \<lbrace>\<lambda>_. cte_at' p\<rbrace>" unfolding updateCap_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) p\<rbrace> updateCap c p' \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) p\<rbrace> do cte <- getCTE c;
setCTE c (cteCap_update (\<lambda>_. p') cte)
od \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>_. True) p\<rbrace>
theory CSpace1_R

lemma nullMDBNode_pointers[simp]:
  "mdbPrev nullMDBNode = nullPointer"
  "mdbNext nullMDBNode = nullPointer" by (simp add: nullMDBNode_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev nullMDBNode = nullPointer &&& mdbNext nullMDBNode = nullPointer
theory CSpace1_R

lemma maxFreeIndex_eq[simp]: "maxFreeIndex nat1 = max_free_index nat1" by (clarsimp simp:maxFreeIndex_def max_free_index_def shiftL_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxFreeIndex nat1 = max_free_index nat1
theory CSpace1_R

lemma getCTE_get:
  "\<lbrace>cte_wp_at' P src\<rbrace> getCTE src \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P src\<rbrace> getCTE src \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' P src s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> P cte) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isUntypedCap_simps[simp]:
  "isUntypedCap (capability.UntypedCap uu uv uw ux) = True"
  "isUntypedCap (capability.NullCap) = False"
  "isUntypedCap (capability.EndpointCap v va vb vc vd ve) = False"
  "isUntypedCap (capability.NotificationCap v va vb vc) = False"
  "isUntypedCap (capability.ReplyCap v1 v2 v3) = False"
  "isUntypedCap (capability.CNodeCap x1 x2 x3 x4) = False"
  "isUntypedCap (capability.ThreadCap v) = False"
  "isUntypedCap (capability.DomainCap) = False"
  "isUntypedCap (capability.IRQControlCap) = False"
  "isUntypedCap (capability.IRQHandlerCap y1) = False"
  "isUntypedCap (capability.Zombie v va1 vb1) = False"
  "isUntypedCap (capability.ArchObjectCap z) = False" by (simp_all add: isUntypedCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((isUntypedCap (capability.UntypedCap uu uv uw ux) = True &&& isUntypedCap capability.NullCap = False &&& isUntypedCap (capability.EndpointCap v va vb vc vd ve) = False) &&& isUntypedCap (capability.NotificationCap v va vb vc) = False &&& isUntypedCap (capability.ReplyCap v1 v2 v3) = False &&& isUntypedCap (capability.CNodeCap x1 x2 x3 x4) = False) &&& (isUntypedCap (capability.ThreadCap v) = False &&& isUntypedCap capability.DomainCap = False &&& isUntypedCap capability.IRQControlCap = False) &&& isUntypedCap (capability.IRQHandlerCap y1) = False &&& isUntypedCap (capability.Zombie v va1 vb1) = False &&& isUntypedCap (capability.ArchObjectCap z) = False
theory CSpace1_R

lemma cap_relation_masked_as_full:
  "\<lbrakk>cap_relation src_cap src_cap';cap_relation c c'\<rbrakk> \<Longrightarrow>
    cap_relation (masked_as_full src_cap c) (maskedAsFull src_cap' c')" apply (clarsimp simp: masked_as_full_def maskedAsFull_def
                 split: if_splits) apply (case_tac src_cap; clarsimp) by (case_tac c; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation src_cap src_cap'; cap_relation c c'\<rbrakk> \<Longrightarrow> cap_relation (masked_as_full src_cap c) (maskedAsFull src_cap' c') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation src_cap src_cap'; cap_relation c c'\<rbrakk> \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<longrightarrow> (isUntypedCap src_cap' \<and> isUntypedCap c' \<and> capPtr src_cap' = capPtr c' \<and> capBlockSize src_cap' = capBlockSize c' \<longrightarrow> cap_relation (max_free_index_update src_cap) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) src_cap')) \<and> ((capPtr src_cap' = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap src_cap' \<longrightarrow> capBlockSize src_cap' \<noteq> capBlockSize c') \<longrightarrow> cap_relation (max_free_index_update src_cap) src_cap')) \<and> ((obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c) \<longrightarrow> isUntypedCap src_cap' \<and> isUntypedCap c' \<and> capPtr src_cap' = capPtr c' \<and> capBlockSize src_cap' = capBlockSize c' \<longrightarrow> cap_relation src_cap (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) src_cap')) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>src_cap' = capability.UntypedCap x21 x22 x23 x24; cap_relation c c'; src_cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (is_untyped_cap c \<and> x22 = obj_ref_of c \<and> x23 = cap_bits_untyped c \<longrightarrow> (obj_ref_of c = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> cap_bits_untyped c \<noteq> capBlockSize c') \<longrightarrow> x24 = max_free_index (cap_bits_untyped c)) \<and> ((x22 = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> x23 \<noteq> cap_bits_untyped c) \<longrightarrow> isUntypedCap c' \<and> x22 = capPtr c' \<and> x23 = capBlockSize c' \<longrightarrow> max_free_index (capBlockSize c') = x24)
theory CSpace1_R

lemma setUntypedCapAsFull_ctes_of_no_0:
  "\<lbrace>\<lambda>s. no_0 ((ctes_of s)(a:=b)) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) cap src
   \<lbrace>\<lambda>r s. no_0 ((ctes_of s)(a:=b)) \<rbrace>" apply (clarsimp simp:no_0_def split:if_splits) apply (wp hoare_vcg_imp_lift setUntypedCapAsFull_ctes_of[where dest = 0]) apply (auto simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_0 ((ctes_of s)(a := b)) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. no_0 ((ctes_of s)(a := b))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (a = 0 \<longrightarrow> b = None \<and> cte_wp_at' ((=) srcCTE) src s) \<and> (a \<noteq> 0 \<longrightarrow> ctes_of s 0 = None \<and> cte_wp_at' ((=) srcCTE) src s)\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. (a = 0 \<longrightarrow> b = None) \<and> (a \<noteq> 0 \<longrightarrow> ctes_of s 0 = None)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (a = 0 \<longrightarrow> b = None \<and> cte_wp_at' ((=) srcCTE) src s) \<and> (a \<noteq> 0 \<longrightarrow> ctes_of s 0 = None \<and> cte_wp_at' ((=) srcCTE) src s) \<Longrightarrow> ((src \<noteq> 0 \<and> a \<noteq> 0 \<or> src = 0 \<and> a \<noteq> 0 \<and> cte_wp_at' ((=) srcCTE) src s) \<or> src \<noteq> 0 \<and> b = None \<or> src = 0 \<and> b = None \<and> cte_wp_at' ((=) srcCTE) src s) \<and> ((src \<noteq> 0 \<and> \<not> a \<noteq> 0 \<or> src = 0 \<and> \<not> a \<noteq> 0 \<and> cte_wp_at' ((=) srcCTE) src s) \<or> src \<noteq> 0 \<and> ctes_of s 0 = None \<or> src = 0 \<and> Some (CTE (maskedAsFull (cteCap srcCTE) cap) (cteMDBNode srcCTE)) = None \<and> cte_wp_at' ((=) srcCTE) src s) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma valid_dlist_preserve:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'"
  shows  "valid_dlist m = valid_dlist m'" apply (rule iffI) apply (rule valid_dlist_preserve_oneway[OF dom misc]) apply simp+ apply (rule valid_dlist_preserve_oneway) apply (simp add:dom misc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist m = valid_dlist m' proof (prove)
goal (2 subgoals):
 1. valid_dlist m \<Longrightarrow> valid_dlist m'
 2. valid_dlist m' \<Longrightarrow> valid_dlist m proof (prove)
goal (4 subgoals):
 1. \<And>x cte cte'. \<lbrakk>valid_dlist m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m (?x4 x cte cte') = Some cte
 2. \<And>x cte cte'. \<lbrakk>valid_dlist m; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> m' (?x4 x cte cte') = Some cte'
 3. valid_dlist m \<Longrightarrow> valid_dlist m
 4. valid_dlist m' \<Longrightarrow> valid_dlist m proof (prove)
goal (1 subgoal):
 1. valid_dlist m' \<Longrightarrow> valid_dlist m proof (prove)
goal (3 subgoals):
 1. \<And>x. valid_dlist m' \<Longrightarrow> (x \<in> dom ?m9) = (x \<in> dom m)
 2. \<And>x cte cte'. \<lbrakk>valid_dlist m'; ?m9 x = Some cte; m x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'
 3. valid_dlist m' \<Longrightarrow> valid_dlist ?m9 proof (prove)
goal:
No subgoals!