theory Untyped_DR

lemma clearMemory_unused_corres_noop:
  "\<lbrakk> ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj};
       range_cover ptr sz (obj_bits_api ty us) n;
       p \<in> set (retype_addrs ptr ty n us)\<rbrakk>
   \<Longrightarrow> dcorres dc \<top>
     (\<lambda>s. (\<forall>x \<in> set (retype_addrs ptr ty n us).
      obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s
      \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> (obj_refs cap)))
      \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s)
     (return ())
     (do_machine_op (clearMemory p (2 ^ (obj_bits_api ty us))))"
  (is "\<lbrakk> ?def; ?szv; ?in \<rbrakk> \<Longrightarrow> dcorres dc \<top> ?P ?f ?g") supply empty_fail_cond[simp] apply (drule page_objects_default_object[where us=us and dev = dev], clarsimp) apply (rename_tac pgsz) apply (simp add: clearMemory_def do_machine_op_bind cleanCacheRange_PoC_def
                   cleanCacheRange_RAM_def cleanL2Range_def dsb_def mapM_x_mapM) apply (subst do_machine_op_bind) apply (clarsimp simp:  ef_storeWord) apply (clarsimp simp: cacheRangeOp_def cleanByVA_def split_def) apply (simp add: dom_mapM ef_storeWord) apply (rule corres_guard_imp, rule corres_split_noop_rhs) apply (rule corres_mapM_to_mapM_x) apply (rule_tac P=\<top> and P'="?P"
                   and S="Id \<inter> ({p .. p + 2 ^ (obj_bits_api ty us) - 1} \<times> UNIV)"
                 in corres_mapM_x[where f="\<lambda>_. return ()", OF _ _ _ refl,
                                   simplified mapM_x_return]) apply clarsimp apply (rule stronger_corres_guard_imp,
                rule_tac sz=pgsz in dcorres_store_word_safe[where dev = dev]) apply (simp add: within_page_def) apply simp apply (clarsimp simp: obj_at_def) apply (subgoal_tac "x && ~~ mask (obj_bits_api ty us) = p") apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter
                         split: cap.split_asm arch_cap.split_asm) apply (cut_tac t="(t, tcb_cnode_index 4)" and P="(=) cap" for t cap
                     in cte_wp_at_tcbI, simp, fastforce, simp) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule(1) bspec) apply clarsimp apply (drule(1) bspec[OF _ ranI]) apply simp apply (drule(2) retype_addrs_aligned
           [OF _ range_cover.aligned range_cover_sz'
             [where 'a=32, folded word_bits_def] le_refl]) apply (simp add:mask_in_range) apply wp apply (simp | wp hoare_vcg_ball_lift)+ apply (simp add:zip_same_conv_map) apply (rule conjI) apply clarsimp apply (clarsimp simp: word_size_def) apply (drule subsetD[OF upto_enum_step_subset]) apply simp apply (rule dcorres_machine_op_noop, wp) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}; range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (clearMemory p (2 ^ obj_bits_api ty us))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}; range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (clearMemory p (2 ^ obj_bits_api ty us))) proof (prove)
goal (1 subgoal):
 1. \<And>vmsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev vmsz); pageBitsForSize vmsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev vmsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (clearMemory p (2 ^ obj_bits_api ty us))) proof (prove)
goal (1 subgoal):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (clearMemory p (2 ^ obj_bits_api ty us))) proof (prove)
goal (1 subgoal):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (do x <- mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1];
y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)) proof (prove)
goal (3 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> empty_fail (mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1])
 2. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> empty_fail (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]);
do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
od) proof (prove)
goal (2 subgoals):
 1. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> empty_fail (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]);
do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do rv <- do_machine_op (mapM (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]);
do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do rv <- mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1];
do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od)
od) proof (prove)
goal (5 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?P11 pgsz) (?P'11 pgsz) (return ()) (mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1])
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> (?P11 pgsz and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (?P'11 pgsz and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?P11 pgsz) (?P'11 pgsz) (return ()) (mapM_x (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1])
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> (?P11 pgsz and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (?P'11 pgsz and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) ((do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y)
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do_machine_op (storeWord x 0))
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (10 subgoals):
 1. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> within_page (?obuf26 pgsz x) x pgsz
 2. \<And>pgsz x s s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; True; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s' \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap)) \<and> valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> valid_idle s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True
 3. \<And>pgsz x s s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; True; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s' \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap)) \<and> valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> valid_idle s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (ako_at (DataPage dev pgsz) (?obuf26 pgsz x) and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> ?obuf26 pgsz x) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) s'
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 8. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 10. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; True; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s' \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap)) \<and> valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> valid_idle s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True
 2. \<And>pgsz x s s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; True; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s' \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap)) \<and> valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> valid_idle s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (ako_at (DataPage dev pgsz) (x && ~~ mask (obj_bits_api ty us)) and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> x && ~~ mask (obj_bits_api ty us)) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) s'
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x s s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; True; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s' \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap)) \<and> valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> valid_idle s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (ako_at (DataPage dev pgsz) (x && ~~ mask (obj_bits_api ty us)) and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> x && ~~ mask (obj_bits_api ty us)) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) s'
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> kheap s' (x && ~~ mask (obj_bits_api ty us)) = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> x && ~~ mask (obj_bits_api ty us))
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; x && ~~ mask (obj_bits_api ty us) = p\<rbrakk> \<Longrightarrow> kheap s' (x && ~~ mask (obj_bits_api ty us)) = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> x && ~~ mask (obj_bits_api ty us))
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us)\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us); cte_wp_at ((=) (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35))) (thread, tcb_cnode_index 4) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us); caps_of_state s' (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35))\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us); caps_of_state s' (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35)); kheap s' (x && ~~ mask (obj_bits_api ty us)) = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x && ~~ mask (obj_bits_api ty us) \<notin> obj_refs cap)\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us); caps_of_state s' (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35)); kheap s' (x && ~~ mask (obj_bits_api ty us)) = Some (ArchObj (DataPage dev pgsz)); \<forall>cap\<in>ran (caps_of_state s'). x && ~~ mask (obj_bits_api ty us) \<notin> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (9 subgoals):
 1. \<And>pgsz x s' thread tcb x31 x33 x34 x35. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x && ~~ mask (obj_bits_api ty us) \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x && ~~ mask (obj_bits_api ty us) \<le> x; x \<le> (x && ~~ mask (obj_bits_api ty us)) + 2 ^ obj_bits_api ty us - 1; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35); p = x && ~~ mask (obj_bits_api ty us); caps_of_state s' (thread, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35)); kheap s' (x && ~~ mask (obj_bits_api ty us)) = Some (ArchObj (DataPage dev pgsz)); x && ~~ mask (obj_bits_api ty us) \<notin> obj_refs (ArchObjectCap (PageCap x31 (x && ~~ mask (obj_bits_api ty us)) x33 x34 x35))\<rbrakk> \<Longrightarrow> False
 2. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 7. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 9. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (8 subgoals):
 1. \<And>pgsz x s'. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; p \<le> x; x \<le> p + 2 ^ obj_bits_api ty us - 1; \<forall>x\<in>set (retype_addrs ptr ty n us). kheap s' x = Some (ArchObj (DataPage dev pgsz)) \<and> (\<forall>cap\<in>ran (caps_of_state s'). x \<notin> obj_refs cap); valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_idle s'; valid_etcbs s'; is_aligned p (obj_bits_api ty us)\<rbrakk> \<Longrightarrow> x && ~~ mask (obj_bits_api ty us) = p
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 6. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 8. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (7 subgoals):
 1. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 5. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 6. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 7. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (6 subgoals):
 1. \<And>pgsz x y. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (x, y) \<in> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) y \<lbrace>\<lambda>rv s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrace>
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<inter> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 6. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> Id \<and> set (zip [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1]) \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> (\<lambda>x. (x, x)) ` set [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<subseteq> Id \<and> (\<lambda>x. (x, x)) ` set [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (6 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> (\<lambda>x. (x, x)) ` set [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<subseteq> Id
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> (\<lambda>x. (x, x)) ` set [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 4. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 6. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> (\<lambda>x. (x, x)) ` set [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<subseteq> {p..p + 2 ^ obj_bits_api ty us - 1} \<times> UNIV
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x \<in> set [p , p + 4 .e. p + 2 ^ obj_bits_api ty us - 1]\<rbrakk> \<Longrightarrow> p \<le> x \<and> x \<le> p + 2 ^ obj_bits_api ty us - 1
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (5 subgoals):
 1. \<And>pgsz x. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; x \<in> {p..p + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> p \<le> x \<and> x \<le> p + 2 ^ obj_bits_api ty us - 1
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 3. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 5. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (4 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> dcorres dc (?R11 pgsz) (?R'11 pgsz) (return ()) (do_machine_op (do y <- cacheRangeOp cleanByVA p (p + 2 ^ obj_bits_api ty us - 1) (addrFromPPtr p);
y <- machine_op_lift dsb_impl;
machine_op_lift (cleanL2Range_impl (addrFromPPtr p) (addrFromPPtr p + (2 ^ obj_bits_api ty us - 1)))
od))
 2. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x. ?R'11 pgsz\<rbrace>
 3. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11 pgsz) s
 4. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal (3 subgoals):
 1. \<And>pgsz. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'11 pgsz\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) [p , p + word_size .e. p + 2 ^ obj_bits_api ty us - 1] \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 3. \<And>pgsz s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p \<in> set (retype_addrs ptr ty n us); Retype_A.default_object ty dev us = ArchObj (DataPage dev pgsz); pageBitsForSize pgsz = obj_bits_api ty us; (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = ArchObj (DataPage dev pgsz)) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ((\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr ty n us). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> obj_refs cap)) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) and ?Q'11 pgsz) s proof (prove)
goal:
No subgoals!