theory CSpace_C

lemma updateTrackedFreeIndex_noop_ccorres:
  "ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
              \<and> idx \<le> 2 ^ capBlockSize cap
              \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) o cteCap) slot
          and valid_objs' and untyped_ranges_zero')
      {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
      (updateTrackedFreeIndex slot idx) Skip"
  (is "ccorres dc xfdc ?P ?P' _ _ _") apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) apply (rule ccorres_guard_imp) apply (rule ccorres_pre_getCTE[where P="\<lambda>rv.
        cte_wp_at' ((=) rv) slot and ?P" and P'="K ?P'"]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule(1) ctes_of_valid') apply (frule(2) ctes_of_untyped_zero_rf_sr_case) apply (clarsimp simp: simpler_modify_def bind_def cte_wp_at_ctes_of) apply (erule gsUntypedZeroRanges_update_helper) apply (clarsimp simp: zero_ranges_are_zero_def
                   split: if_split) apply (case_tac "(a, b) \<in> gsUntypedZeroRanges \<sigma>") apply (drule(1) bspec, simp) apply (erule disjE_L) apply (frule(3) untypedZeroRange_idx_forward_helper) apply (clarsimp simp: isCap_simps valid_cap_simps') apply (case_tac "untypedZeroRange (cteCap cte)") apply (clarsimp simp: untypedZeroRange_def
                       valid_cap_simps'
                       max_free_index_def Let_def
                     split: if_split_asm) apply clarsimp apply (thin_tac "\<not> capIsDevice cap' \<longrightarrow> P" for P) apply (clarsimp split: option.split_asm) apply (subst region_actually_is_bytes_subset, simp+) apply (subst heap_list_is_zero_mono2, simp+) apply (frule untypedZeroRange_idx_backward_helper[where idx=idx],
      simp+) apply (clarsimp simp: isCap_simps valid_cap_simps') apply (clarsimp split: option.split_asm) apply (clarsimp dest!: untypedZeroRange_not_device) apply (subst region_actually_is_bytes_subset, simp+) apply (subst heap_list_is_zero_mono2, simp+) apply (simp add: region_actually_is_bytes'_def heap_list_zero_Ball_intvl) apply (clarsimp dest!: untypedZeroRange_not_device) apply blast apply (clarsimp simp: cte_wp_at_ctes_of) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} hs (updateTrackedFreeIndex slot idx) SKIP proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} hs (do cte <- getCTE slot;
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>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP proof (prove)
goal (3 subgoals):
 1. ccorres dc xfdc ?Q6 ?Q'6 hs (do cte <- getCTE slot;
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>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> ?Q6 s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> ?Q'6 proof (prove)
goal (3 subgoals):
 1. \<And>cte. ccorres dc xfdc (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) (K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} cte) hs (do 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>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) SKIP
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) \<sigma> \<and> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} cte \<and> (\<sigma>, s) \<in> rf_sr} SKIP {s. \<exists>(rv, \<sigma>')\<in>fst ((do 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>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma>. {s. (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) \<sigma> \<and> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} cte \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - \<lbrace>\<acute>((=) r)\<rbrace>\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; (\<sigma>, x) \<in> rf_sr; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - Collect ((=) r)\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; (\<sigma>, x) \<in> rf_sr; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - Collect ((=) r)\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; (\<sigma>, x) \<in> rf_sr; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - Collect ((=) r)\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; (\<sigma>, x) \<in> rf_sr; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))\<rparr>, x) \<in> rf_sr
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)) \<longrightarrow> zero_ranges_are_zero (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))) (t_hrs_' (globals x))
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>)))\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<in> gsUntypedZeroRanges \<sigma>\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); capFreeIndex (cteCap cte) \<le> idx \<or> cap' = cteCap cte; valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; capFreeIndex (cteCap cte) \<le> idx\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; capFreeIndex (cteCap cte) \<le> idx; case (untypedZeroRange (cteCap cte), untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))) of (None, ba) \<Rightarrow> True | (Some (a, b), None) \<Rightarrow> True | (Some (a, b), Some (a', b')) \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ v1; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (5 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ v1; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (cteCap cte) = None\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b d v0 v1 f aa. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ v1; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (cteCap cte) = Some aa\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 4. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 5. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f aa. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ v1; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (cteCap cte) = Some aa\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f aa ba. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ v1; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f aa ba. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; idx \<le> 2 ^ v1; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; {ab..+unat (bb + 1 - ab)} \<subseteq> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; idx \<le> 2 ^ v1; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb)\<rbrakk> \<Longrightarrow> region_actually_is_bytes ab (unat (bb + 1 - ab)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; f \<le> idx; {ab..+unat (bb + 1 - ab)} \<subseteq> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; idx \<le> 2 ^ v1; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb)\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 2. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice (cteCap cte) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap cte) + word_of_nat idx) (capFreeIndex (cteCap cte) - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex (cteCap cte) - idx) (capPtr (cteCap cte) + word_of_nat idx) = replicate (capFreeIndex (cteCap cte) - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x a b. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; isUntypedCap (cteCap cte); \<not> capIsDevice (cteCap cte) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap cte) + word_of_nat idx) (capFreeIndex (cteCap cte) - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (capFreeIndex (cteCap cte) - idx) (capPtr (cteCap cte) + word_of_nat idx) = replicate (capFreeIndex (cteCap cte) - idx) 0; idx \<le> 2 ^ capBlockSize (cteCap cte); valid_cap' (cteCap cte) \<sigma>; case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> capFreeIndex (cteCap cte) \<le> idx; cap' = cteCap cte; case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {capPtr (cteCap cte) + word_of_nat idx..+capFreeIndex (cteCap cte) - idx} \<union> (case untypedZeroRange (cteCap cte) of None \<Rightarrow> {} | Some (a, b) \<Rightarrow> {a..+unat (b + 1 - a)})\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x a b d v0 v1 f. \<lbrakk>valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (\<sigma>\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges \<sigma> | Some r \<Rightarrow> gsUntypedZeroRanges \<sigma> - Collect ((=) r)\<rparr>))); (a, b) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> True | Some (a', b') \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {capPtr (cteCap cte) + word_of_nat idx..+capFreeIndex (cteCap cte) - idx} \<union> (case untypedZeroRange (cteCap cte) of None \<Rightarrow> {} | Some (a, b) \<Rightarrow> {a..+unat (b + 1 - a)}); cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba. \<lbrakk>(aa, ba) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {aa..+unat (ba + 1 - aa)} \<subseteq> {v0 + word_of_nat idx..+f - idx}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; untypedZeroRange (capability.UntypedCap d v0 v1 f) = None; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (aa, ba)\<rbrakk> \<Longrightarrow> region_actually_is_bytes aa (unat (ba + 1 - aa)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0
 2. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ab (unat (bb + 1 - ab)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba. \<lbrakk>(aa, ba) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap False v0 v1 f; {aa..+unat (ba + 1 - aa)} \<subseteq> {v0 + word_of_nat idx..+f - idx}; cteCap cte = capability.UntypedCap False v0 v1 f; capAligned (capability.UntypedCap False v0 v1 f); valid_untyped' False v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; untypedZeroRange (capability.UntypedCap False v0 v1 f) = None; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<not> d; region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x; heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes aa (unat (ba + 1 - aa)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0
 2. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ab (unat (bb + 1 - ab)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba. \<lbrakk>(aa, ba) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap False v0 v1 f; {aa..+unat (ba + 1 - aa)} \<subseteq> {v0 + word_of_nat idx..+f - idx}; cteCap cte = capability.UntypedCap False v0 v1 f; capAligned (capability.UntypedCap False v0 v1 f); valid_untyped' False v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; untypedZeroRange (capability.UntypedCap False v0 v1 f) = None; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; \<not> d; region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x; heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0
 2. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ab (unat (bb + 1 - ab)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 3. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 4. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> region_actually_is_bytes (v0 + word_of_nat idx) (f - idx) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (f - idx) (v0 + word_of_nat idx) = replicate (f - idx) 0; untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb); region_actually_is_bytes aa (unat (ba + 1 - aa)) x; heap_list (hrs_mem (t_hrs_' (globals x))) (unat (ba + 1 - aa)) aa = replicate (unat (ba + 1 - aa)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ab (unat (bb + 1 - ab)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (bb + 1 - ab)) ab = replicate (unat (bb + 1 - ab)) 0
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap d v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<not> d \<longrightarrow> (\<forall>xa\<in>{v0 + word_of_nat idx..+f - idx}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])) \<and> (\<forall>xa\<in>{v0 + word_of_nat idx..+f - idx}. hrs_mem (t_hrs_' (globals x)) xa = 0); untypedZeroRange (capability.UntypedCap d v0 v1 f) = Some (aa, ba); \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> (\<forall>xa\<in>{start..+unat (end + 1 - start)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])) \<and> (\<forall>xa\<in>{start..+unat (end + 1 - start)}. hrs_mem (t_hrs_' (globals x)) xa = 0); untypedZeroRange (capability.UntypedCap d v0 v1 idx) = Some (ab, bb); \<forall>xa\<in>{aa..+unat (ba + 1 - aa)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); \<forall>xa\<in>{aa..+unat (ba + 1 - aa)}. hrs_mem (t_hrs_' (globals x)) xa = 0\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>{ab..+unat (bb + 1 - ab)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])) \<and> (\<forall>xa\<in>{ab..+unat (bb + 1 - ab)}. hrs_mem (t_hrs_' (globals x)) xa = 0)
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte \<sigma> x d v0 v1 f aa ba ab bb. \<lbrakk>(ab, bb) \<notin> gsUntypedZeroRanges \<sigma>; \<not> f \<le> idx; cap' = capability.UntypedCap False v0 v1 f; {ab..+unat (bb + 1 - ab)} \<subseteq> {v0 + word_of_nat idx..+f - idx} \<union> {aa..+unat (ba + 1 - aa)}; cteCap cte = capability.UntypedCap False v0 v1 f; capAligned (capability.UntypedCap False v0 v1 f); valid_untyped' False v0 v1 f \<sigma>; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; valid_objs' \<sigma>; ctes_of \<sigma> slot = Some cte; untyped_ranges_zero' \<sigma>; \<forall>xa\<in>gsUntypedZeroRanges \<sigma>. case xa of (start, end) \<Rightarrow> (\<forall>xa\<in>{start..+unat (end + 1 - start)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])) \<and> (\<forall>xa\<in>{start..+unat (end + 1 - start)}. hrs_mem (t_hrs_' (globals x)) xa = 0); \<forall>xa\<in>{aa..+unat (ba + 1 - aa)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); \<forall>xa\<in>{aa..+unat (ba + 1 - aa)}. hrs_mem (t_hrs_' (globals x)) xa = 0; \<not> d; \<forall>xa\<in>{v0 + word_of_nat idx..+f - idx}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); \<forall>xa\<in>{v0 + word_of_nat idx..+f - idx}. hrs_mem (t_hrs_' (globals x)) xa = 0\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>{ab..+unat (bb + 1 - ab)}. hrs_htd (t_hrs_' (globals x)) xa = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])) \<and> (\<forall>xa\<in>{ab..+unat (bb + 1 - ab)}. hrs_mem (t_hrs_' (globals x)) xa = 0)
 2. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 3. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) slot and (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero')) s
 2. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_bytes (capPtr cap' + word_of_nat idx) (capFreeIndex cap' - idx) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (capFreeIndex cap' - idx) (capPtr cap' + word_of_nat idx) = replicate (capFreeIndex cap' - idx) 0} (cte_to_H cte')} proof (prove)
goal:
No subgoals!