kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_pte:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (pte_C ptr \<rightharpoonup> pte_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (erule(5) pspace_no_overlap_induce_pte[unfolded size_of_def,simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_endpoint:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (endpoint_C ptr \<rightharpoonup> endpoint_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (erule(5) pspace_no_overlap_induce_endpoint[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+16} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_asid_pool:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (asid_pool_C ptr \<rightharpoonup> asid_pool_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (erule(5) pspace_no_overlap_induce_asidpool[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_cte:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (cte_C ptr \<rightharpoonup> cte_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none) apply (erule(5) pspace_no_overlap_induce_cte) apply (simp add: cte_C_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (2 subgoals):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(cte_C) \<noteq> typ_uinfo_t TYPE(8 word) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE(cte_C) \<noteq> typ_uinfo_t TYPE(8 word) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma cnodes_retype_have_size_mono:
  "cnodes_retype_have_size T bits cns \<and> S \<subseteq> T
    \<longrightarrow> cnodes_retype_have_size S bits cns" by (auto simp add: cnodes_retype_have_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnodes_retype_have_size T bits cns \<and> S \<subseteq> T \<longrightarrow> cnodes_retype_have_size S bits cns
theory Retype_C

lemma insertNewCap_sch_act_simple[wp]:
 "\<lbrace>sch_act_simple\<rbrace>insertNewCap a b c\<lbrace>\<lambda>_. sch_act_simple\<rbrace>" by (simp add:sch_act_simple_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> insertNewCap a b c \<lbrace>\<lambda>_. sch_act_simple\<rbrace>
theory Retype_C

lemma insertNewCap_pspace_no_overlap':
notes blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
      Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
shows "\<lbrace>pspace_no_overlap' ptr sz and pspace_aligned'
  and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cptr\<rbrace>
  insertNewCap srcSlot cptr x
  \<lbrace>\<lambda>rv s. pspace_no_overlap' ptr sz s\<rbrace>" apply (clarsimp simp:insertNewCap_def) apply (rule hoare_pre) apply (wp updateMDB_pspace_no_overlap'
     setCTE_pspace_no_overlap' getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cptr\<rbrace> insertNewCap srcSlot cptr x \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cptr\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE cptr;
y <- assert (nullCapPointers oldCTE);
y <- setCTE cptr (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. cptr));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. cptr));
updateNewFreeIndex cptr
od \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE cptr;
y <- assert (nullCapPointers oldCTE);
y <- setCTE cptr (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. cptr));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. cptr));
updateNewFreeIndex cptr
od \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cptr) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) cptr) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) srcSlot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) srcSlot s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) cptr s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) cptr s \<and> (nullCapPointers cte \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma createObject_sch_act_simple[wp]:
  "\<lbrace>\<lambda>s. sch_act_simple s
    \<rbrace>createObject ty ptr us dev\<lbrace>\<lambda>r s. sch_act_simple s \<rbrace>" apply (simp add:sch_act_simple_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>r. sch_act_simple\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>r s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_C

lemma createObject_capRange_helper:
assumes static: "\<lbrace>P\<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>m s. Q {ptr.. ptr + 2 ^ (APIType_capBits ty us) - 1} s\<rbrace>"
shows "\<lbrace>P\<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>m s. Q (capRange m) s\<rbrace>" apply (rule hoare_pre) apply (rule hoare_strengthen_post[OF hoare_vcg_conj_lift]) apply (rule static) apply (rule createObject_capRange) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m. Q (capRange m)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m. Q (capRange m)\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P4\<rbrace> global.createObject ty ptr us dev \<lbrace>?Q4\<rbrace>
 2. \<lbrace>?P'4\<rbrace> global.createObject ty ptr us dev \<lbrace>?Q'4\<rbrace>
 3. \<And>rv s. ?Q4 rv s \<and> ?Q'4 rv s \<Longrightarrow> Q (capRange rv) s
 4. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?P'4 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'4\<rbrace> global.createObject ty ptr us dev \<lbrace>?Q'4\<rbrace>
 2. \<And>rv s. Q {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> ?Q'4 rv s \<Longrightarrow> Q (capRange rv) s
 3. \<And>s. P s \<Longrightarrow> P s \<and> ?P'4 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Q {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> capRange rv = {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<Longrightarrow> Q (capRange rv) s
 2. \<And>s. P s \<Longrightarrow> P s \<and> ?P'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> ?P'4 s proof (prove)
goal:
No subgoals!
theory Retype_C

lemma createObject_caps_overlap_reserved':
  "\<lbrace>\<lambda>s. caps_overlap_reserved' S s \<and>
         pspace_aligned' s \<and>
         pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and>
         is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits
    \<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>rv. caps_overlap_reserved' S\<rbrace>" apply (simp add:createObject_def3) apply (wp createNewCaps_caps_overlap_reserved'[where sz = "APIType_capBits ty us"]) apply (clarsimp simp:range_cover_full) 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 (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv. caps_overlap_reserved' S\<rbrace> 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 (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved' S s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> caps_overlap_reserved' S s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma insertNewCap_untypedRange:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot s\<rbrace>
    insertNewCap srcSlot destSlot x
   \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot s\<rbrace>" apply (simp add:insertNewCap_def) apply (wp updateMDB_weak_cte_wp_at setCTE_cte_wp_at_other getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot\<rbrace> insertNewCap srcSlot destSlot x \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE destSlot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE destSlot (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. destSlot));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. destSlot));
updateNewFreeIndex destSlot
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> P untypedRange (cteCap cte)) srcSlot s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) srcSlot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) srcSlot s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) destSlot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) destSlot s \<and> (nullCapPointers cte \<longrightarrow> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<and> P untypedRange (cteCap c)) srcSlot and (\<lambda>s. destSlot \<noteq> srcSlot)) s))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma range_cover_one:
  "\<lbrakk>is_aligned (ptr :: 'a :: len word) us; us\<le> sz;sz < len_of TYPE('a)\<rbrakk>
  \<Longrightarrow> range_cover ptr sz us (Suc 0)" apply (clarsimp simp:range_cover_def) apply (rule Suc_leI) apply (rule unat_less_power) apply simp apply (rule shiftr_less_t2n) apply simp apply (rule le_less_trans[OF word_and_le1]) apply (simp add:mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> range_cover ptr sz us (Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> Suc (unat (ptr && mask sz >> us)) \<le> 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> us) < 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> sz - us < LENGTH('a)
 2. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr && mask sz >> us < 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr && mask sz >> us < 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr && mask sz < 2 ^ (us + (sz - us)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr && mask sz < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us; us \<le> sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask sz < 2 ^ sz proof (prove)
goal:
No subgoals!
theory Retype_C

lemma range_cover_bound'':
  "\<lbrakk>range_cover ptr sz us n; x < of_nat n\<rbrakk>
  \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1" apply (frule range_cover_cell_subset) apply assumption apply (drule(1) range_cover_subset_not_empty) apply (clarsimp simp: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> ?x < word_of_nat n
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; {ptr + ?x * 2 ^ us..ptr + ?x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!
theory Retype_C

lemma range_cover_head_mask:
  "\<lbrakk>range_cover (ptr :: word32) sz us (Suc n); ptr \<noteq> 0\<rbrakk>
  \<Longrightarrow> ptr + (of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz" apply (case_tac n) apply clarsimp apply (clarsimp simp:range_cover_tail_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc n); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc n); ptr \<noteq> 0; n = 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz
 2. \<And>nat. \<lbrakk>range_cover ptr sz us (Suc n); ptr \<noteq> 0; n = Suc nat\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>range_cover ptr sz us (Suc n); ptr \<noteq> 0; n = Suc nat\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal:
No subgoals!
theory Retype_C

lemma pspace_no_overlap'_strg:
  "pspace_no_overlap' ptr sz s \<and> sz' \<le> sz \<and> sz < word_bits \<longrightarrow> pspace_no_overlap' ptr sz' s" apply clarsimp apply (erule(2) pspace_no_overlap'_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' ptr sz s \<and> sz' \<le> sz \<and> sz < word_bits \<longrightarrow> pspace_no_overlap' ptr sz' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz s; sz' \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz' s proof (prove)
goal:
No subgoals!
theory Retype_C

lemma cte_wp_at_no_0:
  "\<lbrakk>invs' s; cte_wp_at' (\<lambda>_. True) ptr s\<rbrakk> \<Longrightarrow> ptr \<noteq> 0" by (clarsimp dest!:invs_mdb' simp:valid_mdb'_def valid_mdb_ctes_def no_0_def cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>_. True) ptr s\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
theory Retype_C

lemma insertNewCap_cte_wp_at_other:
  "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and K (slot \<noteq> p)\<rbrace> insertNewCap srcSlot slot x
            \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p \<rbrace>" apply (clarsimp simp:insertNewCap_def) apply (wp updateMDB_weak_cte_wp_at setCTE_cte_wp_at_other getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and K (slot \<noteq> p)\<rbrace> insertNewCap srcSlot slot x \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and (\<lambda>y. slot \<noteq> p)\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>cte. P (cteCap cte)) p and (\<lambda>y. slot \<noteq> p)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) srcSlot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) srcSlot s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (nullCapPointers cte \<longrightarrow> (cte_wp_at' (\<lambda>c. P (cteCap c)) p and (\<lambda>s. slot \<noteq> p)) s))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) proof (prove)
goal:
No subgoals!