theory Untyped_DR

lemma init_arch_objects_corres_noop:
  notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff
  shows
  "\<lbrakk> \<forall>x \<in> set refs. is_aligned x (obj_bits_api ty obj_sz);
       range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n \<rbrakk>
   \<Longrightarrow> dcorres dc \<top>
        (\<lambda>s. (ty \<noteq> Structures_A.Untyped \<longrightarrow>
                (\<forall>x\<in>set (retype_addrs ptr ty n obj_sz).
                    obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev obj_sz) x s))
            \<and> (\<forall>cap \<in> ran (null_filter (caps_of_state s)).
                     obj_refs cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {})
               \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s)
        (return ())
        (init_arch_objects ty ptr n obj_sz refs)" apply (simp add: init_arch_objects_def
            split: Structures_A.apiobject_type.split aobject_type.split) apply (simp add: dcorres_machine_op_noop[THEN corres_guard_imp]
                   cleanCacheRange_PoU_def machine_op_lift) apply safe apply (simp add:mapM_x_mapM) apply (rule corres_guard_imp) apply (rule corres_split_noop_rhs) apply (rule corres_noop[where P=\<top> and P'=valid_idle]) apply simp apply (rule hoare_strengthen_post, rule mapM_wp') apply (subst eq_commute, wp copy_global_mappings_dwp) apply (simp add: obj_bits_api_def arch_kobj_size_def
                           default_arch_object_def pd_bits_def pageBits_def) apply (wp mapM_wp' dmo_dwp | simp)+ apply (rule corres_noop[where P=\<top> and P'=valid_idle]) apply (simp add: clearMemory_def do_machine_op_bind
                   cleanCacheRange_PoU_def ef_storeWord
                   mapM_x_mapM dom_mapM) apply (wp mapM_wp' dmo_dwp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api ty obj_sz); range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (ty \<noteq> apiobject_type.Untyped \<longrightarrow> (\<forall>x\<in>set (retype_addrs ptr ty n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev obj_sz) x s)) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (init_arch_objects ty ptr n obj_sz refs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api ty obj_sz); range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n\<rbrakk> \<Longrightarrow> ty = ArchObject PageDirectoryObj \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api ty obj_sz); range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n\<rbrakk> \<Longrightarrow> ty = ArchObject PageDirectoryObj \<longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do y <- mapM_x copy_global_mappings refs;
do_machine_op (mapM_x (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) (return ()) (do x <- mapM copy_global_mappings refs;
do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od)
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?Q13 ?Q'13 (return ()) (do x <- mapM copy_global_mappings refs;
do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od)
od)
 2. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ?Q13 s
 3. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ?Q'13 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?P17 ?P'17 (return ()) (mapM copy_global_mappings refs)
 2. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 4. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> (?P17 and ?R17) s
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (?P'17 and ?Q'17) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s'\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>rv s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> dc () rv\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (mapM copy_global_mappings refs)
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 4. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 6. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. transform s' = s \<and> valid_idle s'\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>rv s'. transform s' = s\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (mapM copy_global_mappings refs)
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 4. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 6. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (7 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. transform s' = s \<and> valid_idle s'\<rbrace> copy_global_mappings x \<lbrace>\<lambda>rv s'. transform s' = s \<and> valid_idle s'\<rbrace>
 2. \<And>s rv sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; transform sa = s \<and> valid_idle sa\<rbrakk> \<Longrightarrow> transform sa = s
 3. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (mapM copy_global_mappings refs)
 4. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 5. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 6. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 7. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (9 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 2. \<And>s x. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 s x\<rbrace> copy_global_mappings x \<lbrace>\<lambda>rv. valid_idle\<rbrace>
 3. \<And>s x sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs; s = transform sa \<and> valid_idle sa\<rbrakk> \<Longrightarrow> (valid_idle sa \<and> transform sa = s) \<and> ?P'35 s x sa
 4. \<And>s rv sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; transform sa = s \<and> valid_idle sa\<rbrakk> \<Longrightarrow> transform sa = s
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (mapM copy_global_mappings refs)
 6. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 7. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 8. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 9. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (8 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 s x\<rbrace> copy_global_mappings x \<lbrace>\<lambda>rv. valid_idle\<rbrace>
 2. \<And>s x sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; x \<in> set refs; s = transform sa \<and> valid_idle sa\<rbrakk> \<Longrightarrow> (valid_idle sa \<and> transform sa = s) \<and> ?P'35 s x sa
 3. \<And>s rv sa. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; transform sa = s \<and> valid_idle sa\<rbrakk> \<Longrightarrow> transform sa = s
 4. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (mapM copy_global_mappings refs)
 5. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 6. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 7. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 8. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> dcorres dc ?R17 ?R'17 (return ()) (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 2. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. ?R'17\<rbrace>
 3. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17) s
 4. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s'\<rbrace> do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od) \<lbrace>\<lambda>rv s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> dc () rv\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. valid_idle\<rbrace>
 4. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. transform s' = s \<and> valid_idle s'\<rbrace> do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od) \<lbrace>\<lambda>rv s'. transform s' = s\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> valid_idle s') (do_machine_op (do x <- mapM (\<lambda>x. cacheRangeOp cleanByVA_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) refs;
return ()
od))
 3. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17\<rbrace> mapM copy_global_mappings refs \<lbrace>\<lambda>x. valid_idle\<rbrace>
 4. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 5. \<And>s. \<lbrakk>\<forall>x\<in>set refs. is_aligned x (obj_bits_api (ArchObject PageDirectoryObj) obj_sz); range_cover ptr sz (obj_bits_api (ArchObject PageDirectoryObj) obj_sz) n; 0 < n; ty = ArchObject PageDirectoryObj; (\<forall>x\<in>set (retype_addrs ptr (ArchObject PageDirectoryObj) n obj_sz). obj_at (\<lambda>ko. ko = Retype_A.default_object (ArchObject PageDirectoryObj) dev obj_sz) x s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). obj_refs cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'17) s proof (prove)
goal:
No subgoals!