theory Recycle_C

lemma clearMemory_PT_setObject_PTE_ccorres:
  "ccorres dc xfdc (page_table_at' ptr
                and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)
                and (\<lambda>_. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr))
            (UNIV \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat ptBits}) []
       (do x \<leftarrow> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE)
                       [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
           doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) pstart)
        od)
       (Call clearMemory_PT_'proc)" apply (rule ccorres_gen_asm)+ apply (cinit' lift: ptr___ptr_to_unsigned_long_' bits_') apply (rule ccorres_Guard_Seq) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule_tac P="page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)"
               in ccorres_from_vcg_nofail[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (subst ghost_assertion_size_logic[unfolded o_def]) apply (simp add: ptBits_def pageBits_def pteBits_def) apply simp apply (clarsimp simp: replicateHider_def[symmetric]) apply (frule is_aligned_no_overflow') apply (intro conjI) apply (clarsimp simp add: ptBits_def pageBits_def pteBits_def
                          cong: StateSpace.state.fold_congs globals.fold_congs) apply (erule is_aligned_weaken, simp add: ptBits_def pageBits_def) apply (clarsimp simp: is_aligned_def ptBits_def pageBits_def pteBits_def) apply (simp add: unat_of_nat32 order_less_le_trans[OF pt_bits_stuff(2)]
                        word_bits_def page_table_at_rf_sr_dom_s) apply (clarsimp simp add: ptBits_def pageBits_def pteBits_def
                      cong: StateSpace.state.fold_congs globals.fold_congs) apply (simp only: field_simps) apply (simp add: upto_enum_step_def objBits_simps ptBits_def pageBits_def
                       linorder_not_less[symmetric] archObjSize_def
                       upto_enum_word split_def pteBits_def) apply (erule mapM_x_store_memset_ccorres_assist
                      [unfolded split_def, OF _ _ _ _ _ _ subset_refl],
             simp_all add: shiftl_t2n hd_map objBits_simps archObjSize_def pteBits_def)[1] apply (rule cmap_relationE1, erule rf_sr_cpte_relation, erule ko_at_projectKO_opt) apply (subst coerce_memset_to_heap_update_pte) apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps) apply (rule conjI) apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos
                        update_pte_map_to_ptes carray_map_relation_upd_triv) apply (rule cmap_relation_updI, simp_all)[1] apply (simp add: cpte_relation_def Let_def pte_lift_def
                        pte_get_tag_def pte_tag_defs) apply (simp add: carch_state_relation_def cmachine_state_relation_def
                        typ_heap_simps update_pte_map_tos) apply csymbr apply (rule ccorres_Guard) apply (ctac add: cleanCacheRange_PoU_ccorres) apply (wp mapM_x_wp' setObject_ksPSpace_only updateObject_default_inv | simp)+ apply (clarsimp simp: guard_is_UNIV_def ptBits_def pageBits_def pteBits_def) apply (clarsimp simp: ptBits_def pageBits_def pteBits_def) apply (frule is_aligned_addrFromPPtr_n, simp) apply (clarsimp simp: is_aligned_no_overflow'[where n=10, simplified] pageBits_def
                        field_simps is_aligned_mask[symmetric] mask_AND_less_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and (\<lambda>_. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr)) (UNIV \<inter> \<lbrace>\<acute>ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrace> \<inter> \<lbrace>\<acute>bits = word_of_nat ptBits\<rbrace>) [] (do x <- mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) pstart)
od) (Call clearMemory_PT_'proc) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr \<Longrightarrow> ccorres dc xfdc (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) (UNIV \<inter> \<lbrace>\<acute>ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrace> \<inter> \<lbrace>\<acute>bits = word_of_nat ptBits\<rbrace>) [] (do x <- mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) pstart)
od) (Call clearMemory_PT_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q194 bits ptr___ptr_to_unsigned_long) (?Q'194 bits ptr___ptr_to_unsigned_long) [SKIP] (do x <- mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))
od) (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_PoU_'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>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q194 bits ptr___ptr_to_unsigned_long s \<and> s' \<in> ?Q'194 bits ptr___ptr_to_unsigned_long proof (prove)
goal (2 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q194 bits ptr___ptr_to_unsigned_long) (?C'200 bits ptr___ptr_to_unsigned_long) [SKIP] (do x <- mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))
od) (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_PoU_'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>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q194 bits ptr___ptr_to_unsigned_long s \<and> s' \<in> ?C'200 bits ptr___ptr_to_unsigned_long \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P202 bits ptr___ptr_to_unsigned_long) (?C'200 bits ptr___ptr_to_unsigned_long) [] (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1]) (CALL memzero_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long,1 << unat bits))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P202 bits ptr___ptr_to_unsigned_long and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> ?C'200 bits ptr___ptr_to_unsigned_long \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL memzero_'proc(PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long,1 << unat bits) {s. \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s))}
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long \<sigma>. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> {s. (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) \<noteq> 0 \<and> ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) \<le> ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) + ((1 << unat bits) - 1) \<and> is_aligned (ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long)) 2 \<and> is_aligned (1 << unat bits) 2 \<and> {ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long)..+unat (1 << unat bits)} \<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 {1 << unat bits..} \<and> (\<forall>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list (ptr_val (PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long)) (replicate (unat (1 << unat bits)) (UCAST(?'a230 \<rightarrow> 8) 0))) (t_hrs_' (globals s)) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 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>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<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 ptBits) \<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 ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 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 ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> unat (2 ^ unat (word_of_nat ptBits)) \<le> gsMaxObjectSize (?s255 \<sigma> x)
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (?s255 \<sigma> x, x) \<in> rf_sr
 3. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 4. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 6. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 7. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>, x) \<in> rf_sr
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 3. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 6. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> True \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1) \<and> is_aligned ptr 2 \<and> is_aligned (2 ^ unat (word_of_nat ptBits)) 2 \<and> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x))) \<and> ((\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ unat (word_of_nat ptBits) - 1)
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 3. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat (word_of_nat ptBits)) 2
 4. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 5. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> (\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr)
 6. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 7. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 8. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 9. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat (word_of_nat ptBits)) 2
 3. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 4. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> (\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr)
 5. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 6. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 7. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 8. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> is_aligned (2 ^ unat (word_of_nat ptBits)) 2
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 3. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> (\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr)
 4. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 6. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 7. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> {ptr..+unat (2 ^ unat (word_of_nat ptBits))} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals x)))
 2. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> (\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr)
 3. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 6. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>is_aligned ptr ptBits; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 2 ^ ptBits \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + (2 ^ ptBits - 1)\<rbrakk> \<Longrightarrow> (\<exists>t. t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))) \<longrightarrow> \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>) \<longrightarrow> (\<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicateHider (unat (2 ^ unat (word_of_nat ptBits))) 0)) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr)
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 1024 \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + 0x3FF; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 4 .e. 0x3FF + ptr] \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 4 .e. 0x3FF + ptr] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)))) x) \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; 1024 \<le> gsMaxObjectSize \<sigma>; (\<sigma>, x) \<in> rf_sr; ptr \<le> ptr + 0x3FF; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 4 .e. ptr + 0x3FF] \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 4 .e. ptr + 0x3FF] \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)))) x) \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; (\<sigma>, x) \<in> rf_sr; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); \<not> snd (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) (map ((\<lambda>x. ptr + x * 4) \<circ> word_of_nat) [0..<256]) \<sigma>)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) (map ((\<lambda>x. ptr + x * 4) \<circ> word_of_nat) [0..<256]) \<sigma>). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)))) x) \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t ptra s s' ko. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; (\<sigma>, x) \<in> rf_sr; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); (s, s') \<in> rf_sr; ko_at' ko ptra s; ptra \<in> (\<lambda>x. ptr + word_of_nat x * 4) ` {0..<256}\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(ptra \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptra (replicateHider 4 0)))) s') \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t ptra s s' ko y'. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; (\<sigma>, x) \<in> rf_sr; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); (s, s') \<in> rf_sr; ko_at' ko ptra s; ptra \<in> (\<lambda>x. ptr + word_of_nat x * 4) ` {0..<256}; map_to_ptes (ksPSpace s) ptra = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr ptra) = Some y'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(ptra \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptra (replicateHider 4 0)))) s') \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t ptra s s' ko y'. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; (\<sigma>, x) \<in> rf_sr; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); (s, s') \<in> rf_sr; ko_at' ko ptra s; ptra \<in> (\<lambda>x. ptr + word_of_nat x * 4) ` {0..<256}; map_to_ptes (ksPSpace s) ptra = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr ptra) = Some y'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(ptra \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr ptra) (pte_C.pte_C (ARRAY x. 0))))) s') \<in> rf_sr
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpspace_relation ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE))) (underlying_memory (ksMachineState s)) (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0))) (t_hrs_' (globals s'))) \<and> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s')))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpspace_relation ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE))) (underlying_memory (ksMachineState s)) (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0))) (t_hrs_' (globals s')))
 2. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s')))
 3. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 6. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')) \<and> cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')) \<and> cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ptes (ksPSpace s))(ptr + word_of_nat xa * 4 \<mapsto> ARM_H.InvalidPTE)) ((cslift s')(pte_Ptr (ptr + word_of_nat xa * 4) \<mapsto> pte_C.pte_C (ARRAY x. 0))) pte_Ptr cpte_relation
 2. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s')))
 3. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 6. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')) \<and> cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')) \<and> cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpte_relation ARM_H.InvalidPTE (pte_C.pte_C (ARRAY x. 0))
 2. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s')))
 3. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 5. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 6. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x t s s' ko y' xa. \<lbrakk>is_aligned ptr 10; page_table_at' ptr \<sigma>; ptr \<noteq> 0; pstart = addrFromPPtr ptr; \<not> gsMaxObjectSize \<sigma> < 1024; \<not> ptr + 0x3FF < ptr; t_hrs_' (globals t) = hrs_mem_update (heap_update_list ptr (replicateHider 1024 0)) (t_hrs_' (globals x)); ko_at' ko (ptr + word_of_nat xa * 4) s; map_to_ptes (ksPSpace s) (ptr + word_of_nat xa * 4) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (ptr + word_of_nat xa * 4)) = Some y'; xa < 256; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState \<sigma>) (globals x); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation \<sigma> (globals x); cte_array_relation s (globals s'); tcb_cte_array_relation \<sigma> (globals x); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; htd_safe domain (hrs_htd (t_hrs_' (globals x))); ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); - domain \<subseteq> kernel_data_refs; ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr (ptr + word_of_nat xa * 4)) (pte_C.pte_C (ARRAY x. 0)))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(ptr + word_of_nat xa * 4 \<mapsto> KOArch (KOPTE ARM_H.InvalidPTE)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s')))
 2. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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)))
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 4. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 5. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long x rv'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?Q'202 bits ptr___ptr_to_unsigned_long x rv') [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (\<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_PoU_'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>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'202 bits ptr___ptr_to_unsigned_long)
 4. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long x rv' ret__unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'; ret__unsigned_long = addrFromPPtr (ptr_val ptr___ptr_to_unsigned_long)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?G'385 bits ptr___ptr_to_unsigned_long x rv' ret__unsigned_long) [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (Guard ShiftError \<lbrace>bits < 0x20\<rbrace> (CALL cleanCacheRange_PoU_'proc(ptr_val ptr___ptr_to_unsigned_long,ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1,ret__unsigned_long)))
 2. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> ?G'385 bits ptr___ptr_to_unsigned_long x rv' v})
 4. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long x rv' ret__unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; dc x rv'; ret__unsigned_long = addrFromPPtr (ptr_val ptr___ptr_to_unsigned_long)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q202 bits ptr___ptr_to_unsigned_long x) (?C'429 bits ptr___ptr_to_unsigned_long x rv' ret__unsigned_long) [SKIP] (doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) (addrFromPPtr ptr))) (CALL cleanCacheRange_PoU_'proc(ptr_val ptr___ptr_to_unsigned_long,ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1,ret__unsigned_long))
 2. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>?Q202 bits ptr___ptr_to_unsigned_long\<rbrace>
 3. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> ?C'429 bits ptr___ptr_to_unsigned_long x rv' v \<inter> \<lbrace>bits < 0x20\<rbrace>})
 4. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> \<lbrace>?R202 bits ptr___ptr_to_unsigned_long\<rbrace> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE) [ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1] \<lbrace>\<lambda>x. (\<lambda>s. unat (ptr + 2 ^ ptBits - 1 - ptr) \<le> gsMaxObjectSize s) and (\<lambda>_. ptr \<le> ptr + 2 ^ ptBits - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ ptBits - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5)\<rbrace>
 2. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. {s. \<forall>v. v = addrFromPPtr (ptr_val (pptr_' (pptr_'_update (\<lambda>_. PTR_COERCE(32 word \<rightarrow> unit) ptr___ptr_to_unsigned_long) s))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := v\<rparr> \<in> {s. pstart_'_update (\<lambda>_. v) (end_'_update (\<lambda>_. ptr_val ptr___ptr_to_unsigned_long + (1 << unat bits) - SCAST(32 signed \<rightarrow> 32) 1) (start_'_update (\<lambda>_. ptr_val ptr___ptr_to_unsigned_long) s)) \<in> \<lbrace>\<acute>start = ptr\<rbrace> \<inter> \<lbrace>\<acute>end = ptr + 2 ^ ptBits - 1\<rbrace> \<inter> \<lbrace>\<acute>pstart = addrFromPPtr ptr\<rbrace>} \<inter> \<lbrace>bits < 0x20\<rbrace>})
 3. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ?R202 bits ptr___ptr_to_unsigned_long) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>bits ptr___ptr_to_unsigned_long. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. if 2 ^ unat (word_of_nat ptBits) = 2 ^ ptBits \<and> word_of_nat ptBits < 0x20 then UNIV else {})
 2. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ((\<lambda>s. unat (ptr + 2 ^ ptBits - 1 - ptr) \<le> gsMaxObjectSize s) and (\<lambda>_. ptr \<le> ptr + 2 ^ ptBits - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ ptBits - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5))) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>bits ptr___ptr_to_unsigned_long s s'. \<lbrakk>is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr; bits = word_of_nat ptBits; ptr___ptr_to_unsigned_long = PTR(32 word) ptr; (s, s') \<in> rf_sr; (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (page_table_at' ptr and (\<lambda>s. 2 ^ ptBits \<le> gsMaxObjectSize s) and ((\<lambda>s. unat (ptr + 2 ^ ptBits - 1 - ptr) \<le> gsMaxObjectSize s) and (\<lambda>_. ptr \<le> ptr + 2 ^ ptBits - 1 \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + (ptr + 2 ^ ptBits - 1 - ptr) \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5))) s \<and> s' \<in> UNIV \<inter> \<lbrace>bits < 0x20\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 10; page_table_at' ptr s; 1024 \<le> gsMaxObjectSize s; ptr \<noteq> 0; pstart = addrFromPPtr ptr\<rbrakk> \<Longrightarrow> ptr \<le> 0x3FF + ptr \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + 0x3FF \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; is_aligned ptr 10; page_table_at' ptr s; 1024 \<le> gsMaxObjectSize s; ptr \<noteq> 0; pstart = addrFromPPtr ptr; is_aligned (addrFromPPtr ptr) 10\<rbrakk> \<Longrightarrow> ptr \<le> 0x3FF + ptr \<and> addrFromPPtr ptr \<le> addrFromPPtr ptr + 0x3FF \<and> ptr && mask 5 = addrFromPPtr ptr && mask 5 proof (prove)
goal:
No subgoals!