theory Invoke_C

lemma clearMemory_untyped_ccorres:
  "ccorres dc xfdc ((\<lambda>s. invs' s
              \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s
                  \<and> isUntypedCap cap
                  \<and> {ptr ..+ 2 ^ sz} \<subseteq> untypedRange cap
                  \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s)
              \<and> 2 ^ sz \<le> gsMaxObjectSize s)
          and (\<lambda>_. is_aligned ptr sz \<and> sz \<ge> 2 \<and> sz \<le> resetChunkBits))
      ({s. region_actually_is_bytes ptr (2 ^ sz) s}
            \<inter> {s. bits_' s = of_nat sz}
            \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr})
      []
     (doMachineOp (clearMemory ptr (2 ^ sz))) (Call clearMemory_'proc)"
  (is "ccorres dc xfdc ?P ?P' [] ?m ?c") apply (rule ccorres_gen_asm) apply (cinit' lift: bits_' ptr___ptr_to_unsigned_long_') apply (rule_tac P="ptr \<noteq> 0 \<and> sz < word_bits"
                in ccorres_gen_asm) apply (rule ccorres_Guard_Seq) apply (simp add: clearMemory_def) apply (simp add: doMachineOp_bind ef_storeWord) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule_tac P="?P" and P'="{s. region_actually_is_bytes ptr (2 ^ sz) s}"
         in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
                            is_aligned_no_wrap'[OF _ word32_power_less_1]
                            unat_of_nat_eq word_bits_def) apply (simp add: is_aligned_weaken is_aligned_triv[THEN is_aligned_weaken]) apply (clarsimp simp: ghost_assertion_size_logic[unfolded o_def]
                            region_actually_is_bytes_dom_s) apply (clarsimp simp: field_simps word_size_def mapM_x_storeWord_step
                            word_bits_def cte_wp_at_ctes_of) apply (frule ctes_of_valid', clarify+) apply (simp add: doMachineOp_def split_def exec_gets) apply (simp add: select_f_def simpler_modify_def bind_def
                       valid_cap_simps' capAligned_def) apply (subst pspace_no_overlap_underlying_zero_update, simp+) apply (case_tac sz, simp_all)[1] apply (case_tac nat, simp_all)[1] apply (clarsimp dest!: region_actually_is_bytes) apply (drule(1) rf_sr_rep0) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                            carch_state_relation_def cmachine_state_relation_def) apply csymbr apply (ctac add: cleanCacheRange_RAM_ccorres) apply wp apply (simp add: guard_is_UNIV_def unat_of_nat
                    word_bits_def capAligned_def word_of_nat_less) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule ctes_of_valid', clarify+) apply (clarsimp simp: isCap_simps valid_cap_simps' capAligned_def
                        word_of_nat_less Kernel_Config.resetChunkBits_def
                        word_bits_def unat_2p_sub_1) apply (strengthen is_aligned_no_wrap'[where sz=sz] is_aligned_addrFromPPtr_n)+ apply (simp add: addrFromPPtr_mask) apply (cases "ptr = 0") apply (drule subsetD, rule intvl_self, simp) apply (simp split: if_split_asm) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits)) ({s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>\<acute>bits = word_of_nat sz\<rbrace> \<inter> \<lbrace>\<acute>ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrace>) [] (doMachineOp (clearMemory ptr (2 ^ sz))) (Call clearMemory_'proc) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits \<Longrightarrow> ccorres dc xfdc (\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) ({s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>\<acute>bits = word_of_nat sz\<rbrace> \<inter> \<lbrace>\<acute>ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrace>) [] (doMachineOp (clearMemory ptr (2 ^ sz))) (Call clearMemory_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q193 ptr___ptr_to_unsigned_long bits) (?Q'193 ptr___ptr_to_unsigned_long bits) [SKIP] (doMachineOp (clearMemory ptr (2 ^ sz))) (Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL memzero_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long,1 << unat bits));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long);;
Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL cleanCacheRange_RAM_'proc(ptr_val ptr___ptr_to_unsigned_long,ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1,\<acute>ret__unsigned_long))))
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ?Q193 ptr___ptr_to_unsigned_long bits s \<and> s' \<in> ?Q'193 ptr___ptr_to_unsigned_long bits proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G199 ptr___ptr_to_unsigned_long bits) (?Q'193 ptr___ptr_to_unsigned_long bits) [SKIP] (doMachineOp (clearMemory ptr (2 ^ sz))) (Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL memzero_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long,1 << unat bits));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long);;
Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL cleanCacheRange_RAM_'proc(ptr_val ptr___ptr_to_unsigned_long,ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1,\<acute>ret__unsigned_long))))
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> (?G199 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> ?Q'193 ptr___ptr_to_unsigned_long bits proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G199 ptr___ptr_to_unsigned_long bits) (?C'200 ptr___ptr_to_unsigned_long bits) [SKIP] (doMachineOp (clearMemory ptr (2 ^ sz))) (CALL memzero_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long,1 << unat bits);;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long);;
Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL cleanCacheRange_RAM_'proc(ptr_val ptr___ptr_to_unsigned_long,ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1,\<acute>ret__unsigned_long))))
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> (?G199 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> ?C'200 ptr___ptr_to_unsigned_long bits \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G199 (PTR(32 word) ptr) (word_of_nat sz)) (?C'200 (PTR(32 word) ptr) (word_of_nat sz)) [SKIP] (doMachineOp (do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr)
od)) (CALL memzero_'proc(PTR(unit) ptr,2 ^ unat (word_of_nat sz));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long))))
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> (?G199 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> ?C'200 ptr___ptr_to_unsigned_long bits \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G199 (PTR(32 word) ptr) (word_of_nat sz)) (?C'200 (PTR(32 word) ptr) (word_of_nat sz)) [SKIP] (do rv <- doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]);
doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))
od) (CALL memzero_'proc(PTR(unit) ptr,2 ^ unat (word_of_nat sz));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long))))
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> (?G199 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> ?C'200 ptr___ptr_to_unsigned_long bits \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P213 (PTR(32 word) ptr) (word_of_nat sz)) (?C'200 (PTR(32 word) ptr) (word_of_nat sz)) [] (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1])) (CALL memzero_'proc(PTR(unit) ptr,2 ^ unat (word_of_nat sz)))
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> (?P213 ptr___ptr_to_unsigned_long bits and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> ?C'200 ptr___ptr_to_unsigned_long bits \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits)) \<sigma> \<and> s \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<and> (\<sigma>, s) \<in> rf_sr} CALL memzero_'proc(PTR(unit) ptr,2 ^ unat (word_of_nat sz)) {s. \<exists>(rv, \<sigma>')\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits \<sigma>. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> {s. ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits)) \<sigma> \<and> s \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. ptr_val (PTR(unit) ptr) \<noteq> 0 \<and> ptr_val (PTR(unit) ptr) \<le> ptr_val (PTR(unit) ptr) + (2 ^ unat (word_of_nat sz) - 1) \<and> is_aligned (ptr_val (PTR(unit) ptr)) 2 \<and> is_aligned (2 ^ unat (word_of_nat sz)) 2 \<and> {ptr_val (PTR(unit) ptr)..+unat (2 ^ unat (word_of_nat sz))} \<times> insert SIndexVal {x. SIndexTyp 0 = x} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s))) \<and> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals s)) \<in> insert 0 {2 ^ unat (word_of_nat sz)..} \<and> (\<forall>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list (ptr_val (PTR(unit) ptr)) (replicate (unat (2 ^ unat (word_of_nat sz))) (UCAST(?'a245 \<rightarrow> 8) 0))) (t_hrs_' (globals s)) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). (\<sigma>', s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>))))}
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x cap. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < word_bits; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; isUntypedCap cap; {ptr..+2 ^ sz} \<subseteq> untypedRange cap; pspace_no_overlap' (capPtr cap) (capBlockSize cap) \<sigma>\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat sz) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat sz)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat sz))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x)) = 0 \<or> 2 ^ unat (word_of_nat sz) \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat sz))) 0)) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat sz))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) ut_slot \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>\<rbrakk> \<Longrightarrow> is_aligned ptr 2 \<and> is_aligned (2 ^ sz) 2 \<and> {ptr..+2 ^ sz} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x)) = 0 \<or> 2 ^ sz \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) ut_slot \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>\<rbrakk> \<Longrightarrow> {ptr..+2 ^ sz} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x)) = 0 \<or> 2 ^ sz \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (ghost'state_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) ut_slot \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (doMachineOp (modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; valid_cap' (cteCap cte) \<sigma>\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (doMachineOp (modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; valid_cap' (capability.UntypedCap d v0 v1 f) \<sigma>\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do p <- select_f (modify (underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x)) (ksMachineState \<sigma>));
modify (ksMachineState_update (\<lambda>_. snd p))
od) \<sigma>). (snd xa, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m x. if x \<in> {ptr..+4 * 2 ^ (sz - 2)} then 0 else m x) (ksMachineState \<sigma>)\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> {ptr..+4 * 2 ^ (sz - 2)} \<subseteq> {v0..v0 + 2 ^ v1 - 1}
 2. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (\<sigma>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 5. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 6. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte nat. \<lbrakk>is_aligned ptr (Suc nat); ptr \<noteq> 0; nat < 31; invs' \<sigma>; Suc 0 \<le> nat; Suc nat \<le> resetChunkBits; 2 * 2 ^ nat \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 * 2 ^ nat) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 * 2 ^ nat} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 * 2 ^ nat) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits; sz = Suc nat\<rbrakk> \<Longrightarrow> {ptr..+4 * 2 ^ (nat - Suc 0)} \<subseteq> {v0..v0 + 2 ^ v1 - 1}
 2. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (\<sigma>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 5. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 6. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; region_actually_is_bytes ptr (2 ^ sz) x; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1 \<and> v1 < word_bits \<and> valid_untyped' d v0 v1 f \<sigma> \<and> v0 \<noteq> 0 \<and> minUntypedSizeBits \<le> v1 \<and> v1 \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ v1 \<and> is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (\<sigma>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; region_is_bytes ptr (2 ^ sz) x; is_aligned v0 v1; v1 < word_bits; 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> (\<sigma>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x d v0 v1 f t cte. \<lbrakk>is_aligned ptr sz; ptr \<noteq> 0; sz < 32; invs' \<sigma>; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize \<sigma>; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 \<sigma>; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x)); ctes_of \<sigma> ut_slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; region_is_bytes ptr (2 ^ sz) x; is_aligned v0 v1; v1 < word_bits; 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; (\<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)))) x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (2 ^ sz) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 4. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 5. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits rv rv'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?Q'207 ptr___ptr_to_unsigned_long bits rv rv') [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR(unit) ptr);;
Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,\<acute>ret__unsigned_long)))
 2. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'207 ptr___ptr_to_unsigned_long bits)
 4. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits rv rv' ret__unsigned_long. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits; dc rv rv'; ret__unsigned_long = addrFromPPtr ptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q207 ptr___ptr_to_unsigned_long bits rv) (?G'320 ptr___ptr_to_unsigned_long bits rv rv' ret__unsigned_long) [SKIP] (doMachineOp (cleanCacheRange_RAM ptr (ptr + 2 ^ sz - 1) (addrFromPPtr ptr))) (Guard ShiftError (if word_of_nat sz < 0x20 then UNIV else {}) (CALL cleanCacheRange_RAM_'proc(ptr,ptr + 2 ^ unat (word_of_nat sz) - 1,ret__unsigned_long)))
 2. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>?Q207 ptr___ptr_to_unsigned_long bits\<rbrace>
 3. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR(unit) ptr) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> ?G'320 ptr___ptr_to_unsigned_long bits rv rv' v})
 4. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?R211 (PTR(32 word) ptr) (word_of_nat sz)\<rbrace> doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) \<lbrace>\<lambda>rv s. ptr \<le> ptr + 2 ^ sz - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ sz - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> unat (ptr + 2 ^ sz - 1 - ptr) \<le> gsMaxObjectSize s\<rbrace>
 2. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR(unit) ptr) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. pstart_'_update (\<lambda>_. v) (end_'_update (\<lambda>_. ptr + 2 ^ unat (word_of_nat sz) - 1) (start_'_update (\<lambda>_. ptr) s)) \<in> \<lbrace>\<acute>start = ptr\<rbrace> \<inter> \<lbrace>\<acute>end = ptr + 2 ^ sz - 1\<rbrace> \<inter> \<lbrace>\<acute>pstart = addrFromPPtr ptr\<rbrace>} \<inter> (if word_of_nat sz < 0x20 then UNIV else {})})
 3. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and ?R211 ptr___ptr_to_unsigned_long bits and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr___ptr_to_unsigned_long bits. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; ptr \<noteq> 0 \<and> sz < word_bits\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR(unit) ptr) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. pstart_'_update (\<lambda>_. v) (end_'_update (\<lambda>_. ptr + 2 ^ unat (word_of_nat sz) - 1) (start_'_update (\<lambda>_. ptr) s)) \<in> \<lbrace>\<acute>start = ptr\<rbrace> \<inter> \<lbrace>\<acute>end = ptr + 2 ^ sz - 1\<rbrace> \<inter> \<lbrace>\<acute>pstart = addrFromPPtr ptr\<rbrace>} \<inter> (if word_of_nat sz < 0x20 then UNIV else {})})
 2. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and (\<lambda>a. ptr \<le> ptr + 2 ^ sz - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ sz - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> unat (ptr + 2 ^ sz - 1 - ptr) \<le> gsMaxObjectSize a) and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr___ptr_to_unsigned_long bits s s'. \<lbrakk>is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; bits = word_of_nat sz; (s, s') \<in> rf_sr; invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s; s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s}\<rbrakk> \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>cap. cte_wp_at' (\<lambda>cte. cteCap cte = cap) ut_slot s \<and> isUntypedCap cap \<and> {ptr..+2 ^ sz} \<subseteq> untypedRange cap \<and> pspace_no_overlap' (capPtr cap) (capBlockSize cap) s) \<and> 2 ^ sz \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr sz \<and> 2 \<le> sz \<and> sz \<le> resetChunkBits) and (\<lambda>a. ptr \<le> ptr + 2 ^ sz - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ sz - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> unat (ptr + 2 ^ sz - 1 - ptr) \<le> gsMaxObjectSize a) and (\<lambda>_. ptr \<noteq> 0 \<and> sz < word_bits)) s \<and> s' \<in> {s. region_actually_is_bytes ptr (2 ^ sz) s} \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize s; isUntypedCap (cteCap cte); ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> untypedRange (cteCap cte); pspace_no_overlap' (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) s\<rbrakk> \<Longrightarrow> addrFromPPtr ptr \<le> addrFromPPtr ptr + (2 ^ sz - 1) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> unat (2 ^ sz - 1) \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 \<and> sz < word_bits \<and> word_of_nat sz < 0x20 proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> resetChunkBits; 2 ^ sz \<le> gsMaxObjectSize s; isUntypedCap (cteCap cte); ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> untypedRange (cteCap cte); pspace_no_overlap' (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> addrFromPPtr ptr \<le> addrFromPPtr ptr + (2 ^ sz - 1) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> unat (2 ^ sz - 1) \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 \<and> sz < word_bits \<and> word_of_nat sz < 0x20 proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> addrFromPPtr ptr \<le> addrFromPPtr ptr + (2 ^ sz - 1) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> ((is_aligned ptr sz \<and> sz \<le> 24) \<and> 2 ^ sz - 1 < 2 ^ sz) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 \<and> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; ptr = 0\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0
 2. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; ptr = 0; ptr \<in> {v0..v0 + 2 ^ v1 - 1}\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0
 2. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte d v0 v1 f. \<lbrakk>(s, s') \<in> rf_sr; region_actually_is_bytes ptr (2 ^ sz) s'; is_aligned ptr sz; invs' s; 2 \<le> sz; sz \<le> 8; 2 ^ sz \<le> gsMaxObjectSize s; ctes_of s ut_slot = Some cte; {ptr..+2 ^ sz} \<subseteq> {v0..v0 + 2 ^ v1 - 1}; pspace_no_overlap' v0 v1 s; cteCap cte = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < 32; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; f \<le> 2 ^ v1; is_aligned (word_of_nat f) minUntypedSizeBits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz - Suc 0 \<le> gsMaxObjectSize s \<and> ptr \<noteq> 0 proof (prove)
goal:
No subgoals!