kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_R

lemma caps_overlap_reserved'_D:
  "\<lbrakk>caps_overlap_reserved' S s; ctes_of s p = Some cte;isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}" apply (simp add:caps_overlap_reserved'_def) apply (erule ballE) apply (erule(2) impE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_overlap_reserved' S s; ctes_of s p = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; ctes_of s p = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); isUntypedCap (cteCap ?cte) \<longrightarrow> usableUntypedRange (cteCap ?cte) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 2. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); ?cte \<notin> ran (ctes_of s)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; isUntypedCap (cteCap cte); cte \<notin> ran (ctes_of s)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma no_default_zombie:
  "cap_relation (default_cap tp p sz d) cap \<Longrightarrow> \<not>isZombie cap" by (cases tp, auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation (default_cap tp p sz d) cap \<Longrightarrow> \<not> isZombie cap
theory Untyped_R

lemma updateNewFreeIndex_valid_objs[wp]:
  "\<lbrace>valid_objs'\<rbrace> updateNewFreeIndex slot \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (simp add: updateNewFreeIndex_def getSlotCap_def) apply (wp getCTE_wp' | wpc | simp add: updateTrackedFreeIndex_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> updateNewFreeIndex slot \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma insertNewCap_valid_objs [wp]:
  "\<lbrace> valid_objs' and valid_cap' cap and pspace_aligned' and pspace_distinct'\<rbrace>
  insertNewCap parent slot cap
  \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (simp add: insertNewCap_def) apply (wp setCTE_valid_objs getCTE_wp') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap and pspace_aligned' and pspace_distinct'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap and pspace_aligned' and pspace_distinct'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs' and valid_cap' cap and pspace_aligned' and pspace_distinct') s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) parent s \<longrightarrow> ((\<lambda>next s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> (valid_objs' and valid_cap' (cteCap (CTE cap (MDB next parent True True)))) s) \<circ> (mdbNext \<circ> cteMDBNode)) cte s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma createNewCaps_descendants_range':
  "\<lbrace>\<lambda>s. descendants_range' p q (ctes_of s) \<and>
        range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and>
        pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
   createNewCaps ty ptr n us d
   \<lbrace> \<lambda>rv s. descendants_range' p q (ctes_of s)\<rbrace>" apply (clarsimp simp:descendants_range'_def2 descendants_range_in'_def2) apply (wp createNewCaps_null_filter') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range' p q (ctes_of s) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. descendants_range' p q (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange p = {}) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange p = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange p = {}) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ((\<lambda>s. \<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange p = {}) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz9 and K (range_cover ptr ?sz9 (APIType_capBits ty us) n \<and> n \<noteq> 0)) s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma createNewCaps_caps_overlap_reserved':
  "\<lbrace>\<lambda>s. caps_overlap_reserved' S s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and> 0 < n \<and>
        range_cover ptr sz (APIType_capBits ty us) n\<rbrace>
   createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. caps_overlap_reserved' S s\<rbrace>" apply (clarsimp simp: caps_overlap_reserved'_def2) apply (wp createNewCaps_null_filter') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_overlap_reserved' S s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n \<Longrightarrow> ((\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz1 and K (range_cover ptr ?sz1 (APIType_capBits ty us) n \<and> n \<noteq> 0)) s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma dmo_ctes_of[wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> doMachineOp mop \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" by (simp add: doMachineOp_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> doMachineOp mop \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>
theory Untyped_R

lemma createNewCaps_ranges':
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace>
  createNewCaps ty ptr n us d
  \<lbrace>\<lambda>rv s. distinct_sets (map capRange (map snd (zip xs rv)))\<rbrace>" apply (rule hoare_strengthen_post) apply (rule createNewCaps_ranges) apply (simp add: distinct_sets_prop del: map_map) apply (erule distinct_prop_prefixE) apply (rule Sublist.map_mono_prefix) apply (rule map_snd_zip_prefix [unfolded less_eq_list_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. distinct_sets (map capRange (map snd (zip xs rv)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace> createNewCaps ty ptr n us d \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> distinct_sets (map capRange (map snd (zip xs rv))) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. distinct_sets (map capRange rv) \<Longrightarrow> distinct_sets (map capRange (map snd (zip xs rv))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. distinct_prop (\<lambda>x y. x \<inter> y = {}) (map capRange rv) \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (map capRange (map snd (zip xs rv))) proof (prove)
goal (1 subgoal):
 1. \<And>rv. prefix (map capRange (map snd (zip xs rv))) (map capRange rv) proof (prove)
goal (1 subgoal):
 1. \<And>rv. prefix (map snd (zip xs rv)) rv proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma updateFreeIndex_pspace_no_overlap':
  "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and>
        valid_pspace' s \<and> cte_wp_at' (isUntypedCap o cteCap) src s\<rbrace>
   updateFreeIndex src index
   \<lbrace>\<lambda>r s. pspace_no_overlap' ptr sz s\<rbrace>" apply (simp add: updateFreeIndex_def getSlotCap_def updateTrackedFreeIndex_def) apply (rule hoare_pre) apply (wp getCTE_wp' | wp (once) pspace_no_overlap'_lift
     | simp)+ apply (clarsimp simp:valid_pspace'_def pspace_no_overlap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) src s\<rbrace> updateFreeIndex src index \<lbrace>\<lambda>r. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) src s\<rbrace> do y <- do cte <- getCTE src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE src;
updateCap src (capFreeIndex_update (\<lambda>_. index) (cteCap cte))
od \<lbrace>\<lambda>r. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- do cte <- getCTE src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE src;
updateCap src (capFreeIndex_update (\<lambda>_. index) (cteCap cte))
od \<lbrace>\<lambda>r. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) src s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) src s \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s) \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma descendants_range_in_subseteq':
  "\<lbrakk>descendants_range_in' A p ms ;B\<subseteq> A\<rbrakk> \<Longrightarrow> descendants_range_in' B p ms" by (auto simp:descendants_range_in'_def cte_wp_at_ctes_of dest!:bspec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' A p ms; B \<subseteq> A\<rbrakk> \<Longrightarrow> descendants_range_in' B p ms
theory Untyped_R

lemma setCTE_tcbDomain_inv[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbState tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbState 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 (tcbState tcb)) t\<rbrace> setCTE ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbState tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbState tcb)) t\<rbrace> setObject ptr v \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbState tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma cte_wp_at': "cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap
      dev (ptr && ~~ mask sz) sz idx) cref s"
  and cover: "range_cover ptr sz (APIType_capBits tp us) (length (slots::word32 list))"
  and misc2: "distinct slots"
     "slots \<noteq> []"
      "\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s"
      "\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s" using vui by (auto simp: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s &&& range_cover ptr sz (APIType_capBits tp us) (length slots) &&& (distinct slots &&& slots \<noteq> []) &&& \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s &&& \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s proof (prove)
using this:
valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype cref reset ptr_base ptr tp us slots dev) (Some (capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s &&& range_cover ptr sz (APIType_capBits tp us) (length slots) &&& (distinct slots &&& slots \<noteq> []) &&& \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s &&& \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s
theory Untyped_R

lemma idx_cases:
  "((\<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))) \<or> reset \<and> ptr = ptr && ~~ mask sz)" using vui by (clarsimp simp: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz proof (prove)
using this:
valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype cref reset ptr_base ptr tp us slots dev) (Some (capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
theory Untyped_R

lemma desc_range:
  "reset
    \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} (cref) (ctes_of s)" using vui by (clarsimp simp: empty_descendants_range_in')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
using this:
valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype cref reset ptr_base ptr tp us slots dev) (Some (capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s)
theory Untyped_R

lemma not_0_ptr[simp]: "ptr\<noteq> 0" using misc cte_wp_at' apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte) apply clarsimp apply (drule(1) ctes_of_valid_cap'[OF _ invs_valid_objs']) apply (simp add: valid_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
using this:
ct_active' s
invs' s
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s

goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev 0 sz idx; ptr = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev 0 sz idx; ptr = 0; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some (CTE (capability.UntypedCap dev 0 sz idx) x2); ptr = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>ct_active' s; invs' s; ptr = 0; valid_cap' (capability.UntypedCap dev 0 sz idx) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma subset_stuff[simp]:
      "retype_range \<subseteq> usable_range" apply (rule range_cover_subset'[OF cover]) apply (simp add:misc2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. length slots \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma idx_compare'[simp]:"unat ((ptr && mask sz) + (of_nat (length slots)<< (APIType_capBits tp us))) \<le> 2 ^ sz" apply (rule le_trans[OF unat_plus_gt]) apply (simp add: range_cover.unat_of_nat_n_shift[OF cover] range_cover_unat) apply (insert range_cover.range_cover_compare_bound[OF cover]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + (word_of_nat (length slots) << APIType_capBits tp us)) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat (length slots) << APIType_capBits tp us) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + length slots * 2 ^ APIType_capBits tp us \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. length slots * 2 ^ APIType_capBits tp us + unat (ptr && mask sz) \<le> 2 ^ sz \<Longrightarrow> unat (ptr && mask sz) + length slots * 2 ^ APIType_capBits tp us \<le> 2 ^ sz proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma ex_cte_no_overlap': "\<And>P p. ex_cte_cap_wp_to' P p s \<Longrightarrow> p \<notin> usable_range" using cte_wp_at' misc apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule_tac cte = cte in descendants_range_ex_cte'[OF descendants_range(1)]) apply (clarsimp simp: word_and_le2 isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. ex_cte_cap_wp_to' P p s \<Longrightarrow> p \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
using this:
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
ct_active' s
invs' s

goal (1 subgoal):
 1. \<And>P p. ex_cte_cap_wp_to' P p s \<Longrightarrow> p \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>P p cte. \<lbrakk>ex_cte_cap_wp_to' P p s; ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>P p cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> capRange (cteCap cte)
 2. \<And>P p cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>P p cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ctes_of s cref = Some cte
 4. \<And>P p cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 5. \<And>P p cte. \<lbrakk>ct_active' s; invs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; ptr \<le> p; p \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; p \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma cref_inv: "cref \<notin> usable_range" apply (insert misc cte_wp_at') apply (drule if_unsafe_then_capD') apply (simp add: invs'_def valid_state'_def) apply simp apply (erule ex_cte_no_overlap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s\<rbrakk> \<Longrightarrow> cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ct_active' s; invs' s\<rbrakk> \<Longrightarrow> if_unsafe_then_cap' s
 2. \<And>cte. \<lbrakk>ct_active' s; invs' s; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 3. \<lbrakk>ct_active' s; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) cref s\<rbrakk> \<Longrightarrow> cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ct_active' s; invs' s; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 2. \<lbrakk>ct_active' s; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) cref s\<rbrakk> \<Longrightarrow> cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) cref s\<rbrakk> \<Longrightarrow> cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!