kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma (in mdb_insert) n_revocable:
  "n p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then mdbRevocable node = revokable' src_cap c'
          else mdbRevocable node = mdbRevocable node' \<and> m p = Some (CTE cap node')" using src dest by (clarsimp simp: n new_src_def new_dest_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then mdbRevocable node = revokable' src_cap c' else mdbRevocable node = mdbRevocable node' \<and> m p = Some (CTE cap node') proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then mdbRevocable node = revokable' src_cap c' else mdbRevocable node = mdbRevocable node' \<and> m p = Some (CTE cap node')
theory CSpace_R

lemma not_untyped: "capAligned c' \<Longrightarrow> \<not>isUntypedCap src_cap" using no_child partial_is_derived' ut_rev src apply (clarsimp simp: ut_revocable'_def isMDBParentOf_CTE) apply (erule_tac x=src in allE) apply simp apply (clarsimp simp: is_derived'_def freeIndex_update_def isCap_simps capAligned_def
                        badge_derived'_def) apply (clarsimp simp: sameRegionAs_def3 capMasterCap_def isCap_simps interval_empty
                        is_aligned_no_overflow split:capability.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capAligned c' \<Longrightarrow> \<not> isUntypedCap src_cap proof (prove)
using this:
\<not> isMDBParentOf (CTE src_cap src_node) (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))
is_derived' m src c' src_cap
ut_revocable' m
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. capAligned c' \<Longrightarrow> \<not> isUntypedCap src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c'; global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); is_derived' m src c' src_cap; \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; m src = Some (CTE src_cap src_node); isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c'; global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); is_derived' m src c' src_cap; m src = Some (CTE src_cap src_node); isUntypedCap src_cap; \<forall>cap n. m src = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c'; global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); is_derived' m src c' src_cap; m src = Some (CTE src_cap src_node); isUntypedCap src_cap; mdbRevocable src_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f fa. \<lbrakk>\<not> global.sameRegionAs (capability.UntypedCap d v0 v1 f) (capability.UntypedCap d v0 v1 f); m src = Some (CTE (capability.UntypedCap d v0 v1 f) src_node); mdbRevocable src_node; src_cap = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; descendants_of' src m = {}; vsCapRef (capability.UntypedCap d v0 v1 f) = vsCapRef (capability.UntypedCap d v0 v1 fa); c' = capability.UntypedCap d v0 v1 fa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma trancl_prev_update:
  "modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y" apply (rule iffI) apply (erule update_prev_next_trancl2) apply (erule update_prev_next_trancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
 2. m \<turnstile> x \<leadsto>\<^sup>+ y \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma rtrancl_prev_update:
  "modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>* y = m \<turnstile> x \<leadsto>\<^sup>* y" by (simp add: trancl_prev_update rtrancl_eq_or_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>* y = m \<turnstile> x \<leadsto>\<^sup>* y
theory CSpace_R

lemma descendants_of_prev_update:
  "descendants_of' p (modify_map m x (cteMDBNode_update (mdbPrev_update f))) =
   descendants_of' p m" by (simp add: descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = descendants_of' p m
theory CSpace_R

lemma capAligned_maskedAsFull:
  "capAligned s_cap \<Longrightarrow> capAligned (maskedAsFull s_cap cap)" apply (case_tac s_cap) apply (clarsimp simp:isCap_simps capAligned_def maskedAsFull_def max_free_index_def)+ done

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

lemma maskedAsFull_usable_empty:
  "\<lbrakk>capMasterCap cap = capMasterCap s_cap;
    isUntypedCap (maskedAsFull s_cap cap)\<rbrakk>
   \<Longrightarrow> usableUntypedRange (maskedAsFull s_cap cap) = {}" apply (simp add:isCap_simps maskedAsFull_def max_free_index_def split:if_split_asm) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap cap = capMasterCap s_cap; isUntypedCap (maskedAsFull s_cap cap)\<rbrakk> \<Longrightarrow> usableUntypedRange (maskedAsFull s_cap cap) = {} proof (prove)
goal (2 subgoals):
 1. \<And>d da v0 v1 f fa. \<lbrakk>da = d; s_cap = capability.UntypedCap d v0 v1 f; cap = capability.UntypedCap d v0 v1 fa\<rbrakk> \<Longrightarrow> f < 2 ^ v1 \<longrightarrow> (\<forall>da. d = (\<not> da)) \<longrightarrow> d
 2. \<lbrakk>capMasterCap cap = capMasterCap s_cap; capPtr s_cap = capPtr cap \<longrightarrow> (\<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f) \<or> capBlockSize s_cap \<noteq> capBlockSize cap; \<exists>d v0 v1 f. s_cap = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> ((\<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f) \<and> capPtr s_cap = capPtr cap \<and> capBlockSize s_cap = capBlockSize cap \<longrightarrow> usableUntypedRange (capFreeIndex_update (\<lambda>_. 2 ^ capBlockSize cap) s_cap) = {}) \<and> usableUntypedRange s_cap = {} proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma capMaster_isUntyped:
  "capMasterCap c = capMasterCap c' \<Longrightarrow> isUntypedCap c = isUntypedCap c'" by (simp add: capMasterCap_def isCap_simps split: capability.splits)

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

lemma capMaster_capRange:
  "capMasterCap c = capMasterCap c' \<Longrightarrow> capRange c = capRange c'" by (simp add: capMasterCap_def capRange_def split: capability.splits arch_capability.splits)

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

lemma capMaster_untypedRange:
  "capMasterCap c = capMasterCap c' \<Longrightarrow> untypedRange c = untypedRange c'" by (simp add: capMasterCap_def capRange_def split: capability.splits arch_capability.splits)

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

lemma capMaster_capClass:
  "capMasterCap c = capMasterCap c' \<Longrightarrow> capClass c = capClass c'" by (simp add: capMasterCap_def split: capability.splits arch_capability.splits)

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

lemma distinct_zombies_nonCTE_modify_map:
  "\<And>m x f. \<lbrakk> \<And>cte. cteCap (f cte) = cteCap cte \<rbrakk>
     \<Longrightarrow> distinct_zombies (modify_map m x f) = distinct_zombies m" apply (simp add: distinct_zombies_def modify_map_def o_def) apply (rule_tac f=distinct_zombie_caps in arg_cong) apply (rule ext) apply simp apply (simp add: map_option.compositionality o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m x f. (\<And>cte. cteCap (f cte) = cteCap cte) \<Longrightarrow> distinct_zombies (modify_map m x f) = distinct_zombies m proof (prove)
goal (1 subgoal):
 1. \<And>m x f. (\<And>cte. cteCap (f cte) = cteCap cte) \<Longrightarrow> distinct_zombie_caps (\<lambda>xa. map_option cteCap (if xa = x then map_option f (m x) else m xa)) = distinct_zombie_caps (\<lambda>x. map_option cteCap (m x)) proof (prove)
goal (1 subgoal):
 1. \<And>m x f. (\<And>cte. cteCap (f cte) = cteCap cte) \<Longrightarrow> (\<lambda>xa. map_option cteCap (if xa = x then map_option f (m x) else m xa)) = (\<lambda>x. map_option cteCap (m x)) proof (prove)
goal (1 subgoal):
 1. \<And>m x f xa. (\<And>cte. cteCap (f cte) = cteCap cte) \<Longrightarrow> map_option cteCap (if xa = x then map_option f (m x) else m xa) = map_option cteCap (m xa) proof (prove)
goal (1 subgoal):
 1. \<And>m x f xa. (\<And>cte. cteCap (f cte) = cteCap cte) \<Longrightarrow> xa = x \<longrightarrow> map_option cteCap (map_option f (m x)) = map_option cteCap (m x) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma valid_dlist_prevD:
  "\<lbrakk>m p = Some cte;valid_dlist m;mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk>
   \<Longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and>
               mdbNext (cteMDBNode cte') = p)" by (clarsimp simp:valid_dlist_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; valid_dlist m; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
theory CSpace_R

lemma valid_dlist_nextD:
  "\<lbrakk>m p = Some cte;valid_dlist m;mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk>
   \<Longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and>
               mdbPrev (cteMDBNode cte') = p)" by (clarsimp simp:valid_dlist_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; valid_dlist m; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p
theory CSpace_R

lemma cteInsert_valid_pspace:
  "\<lbrace>valid_pspace' and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and valid_objs' and
    (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>_. valid_pspace'\<rbrace>" unfolding valid_pspace'_def apply (rule hoare_pre) apply (wp cteInsert_valid_objs) apply (fastforce elim: valid_capAligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_cap' cap and (\<lambda>s. src \<noteq> dest) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> (valid_objs' and valid_cap' cap) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateMDB_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s\<rbrace>
     updateMDB p m
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s\<rbrace>" apply (clarsimp simp: updateMDB_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (wp setCTE_iflive') apply (clarsimp elim!: cte_wp_at_weakenE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> updateMDB p m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>if_live_then_nonz_cap'\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. p \<noteq> 0 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) p and if_live_then_nonz_cap'\<rbrace> setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte) \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s. \<lbrakk>p \<noteq> 0; (cte_wp_at' (\<lambda>c. c = cte) p and if_live_then_nonz_cap') s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)). ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateCap_iflive':
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte')
                          - zobj_refs' cap.
                                ko_wp_at' (Not \<circ> live') p' s) p s
      \<and> if_live_then_nonz_cap' s\<rbrace>
     updateCap p cap
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s\<rbrace>" apply (simp add: updateCap_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (wp setCTE_iflive') apply (clarsimp elim!: cte_wp_at_weakenE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s\<rbrace> updateCap p cap \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrace>cte_wp_at' (\<lambda>c. c = cte) p and (\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s)\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) cte) \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) p and (\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s)) s \<Longrightarrow> cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap (cteCap_update (\<lambda>_. cap) cte)). ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setUntypedCapAsFull_ko_wp_not_at'[wp]:
  "\<lbrace>\<lambda>s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) cap src
   \<lbrace>\<lambda>r s. P ( ko_wp_at' (Not \<circ> live') p' s)\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def updateCap_def) apply (wp setCTE_ko_wp_at_live setCTE_ko_wp_at_not_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) cte)
od \<lbrace>\<lambda>r s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setUntypedCapAsFull_ko_wp_at'[wp]:
  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) cap src
   \<lbrace>\<lambda>r s. P ( ko_wp_at' live' p' s)\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def updateCap_def) apply (wp setCTE_ko_wp_at_live setCTE_ko_wp_at_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) cte)
od \<lbrace>\<lambda>r s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma zobj_refs'_capFreeIndex_update[simp]:
  "isUntypedCap ctecap \<Longrightarrow>
   zobj_refs' (capFreeIndex_update f (ctecap)) = zobj_refs' ctecap" by (case_tac ctecap,auto simp:isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap ctecap \<Longrightarrow> zobj_refs' (capFreeIndex_update f ctecap) = zobj_refs' ctecap
theory CSpace_R

lemma maskedAsFull_simps[simp]:
  "maskedAsFull capability.NullCap cap =  capability.NullCap" by (auto simp:maskedAsFull_def)

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

lemma ifunsafe'_def2:
  "if_unsafe_then_cap' =
    (\<lambda>s. \<forall>cref cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> NullCap
              \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte'
                                  \<and> cref \<in> cte_refs' (cteCap cte') (irq_node' s)))" by (clarsimp intro!: ext
                 simp: if_unsafe_then_cap'_def cte_wp_at_ctes_of
                       ex_cte_cap_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap' = (\<lambda>s. \<forall>cref cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') (irq_node' s)))
theory CSpace_R

lemma ifunsafe'_def3:
  "if_unsafe_then_cap' =
    (\<lambda>s. \<forall>cref cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> NullCap
              \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap'
                          \<and> cref \<in> cte_refs' cap' (irq_node' s)))" apply (simp add: cteCaps_of_def o_def ifunsafe'_def2) apply (fastforce intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap' = (\<lambda>s. \<forall>cref cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') (irq_node' s))) = (\<lambda>s. \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma tree_cte_cteCap_eq:
  "cte_wp_at' (P \<circ> cteCap) p s = (case_option False P (cteCaps_of s p))" apply (simp add: cte_wp_at_ctes_of cteCaps_of_def) apply (cases "ctes_of s p", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (P \<circ> cteCap) p s = (case cteCaps_of s p of None \<Rightarrow> False | Some x \<Rightarrow> P x) proof (prove)
goal (1 subgoal):
 1. (\<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)) = (case ctes_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P (cteCap x2)) proof (prove)
goal:
No subgoals!