theory Untyped_DR

lemma delete_objects_dcorres:
  notes order_class.Icc_eq_Icc [simp del]
        is_aligned_neg_mask_eq[simp del]
        is_aligned_neg_mask_weaken[simp del]
  assumes S: "S = {ptr..ptr + 2 ^ bits - 1}"
  shows "dcorres dc \<top>
      (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>cref dev idx.
        cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) cref s
         \<and> descendants_range (cap.UntypedCap dev ptr bits idx) cref s) \<and> valid_etcbs s)
      (modify (Untyped_D.detype S))
      (delete_objects ptr bits)" apply (clarsimp simp: S) apply (unfold delete_objects_def2 K_bind_def) apply (rule corres_bind_return) apply (rule_tac F="is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits"
                  in corres_req) apply clarsimp apply (drule cte_wp_valid_cap, clarsimp) apply (simp add: valid_cap_def cap_aligned_def untyped_min_bits_def) apply (rule corres_name_pre, clarify) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule detype_dcorres; simp) apply (rule freeMemory_dcorres, simp+) apply wp apply clarsimp apply (rule TrueI)? apply clarsimp apply (rule conjI) apply fastforce apply (frule cte_wp_valid_cap, clarsimp) apply (intro conjI) apply (erule pspace_no_overlap_detype) apply clarsimp+ apply (frule invs_untyped_children) apply (drule_tac detype_invariants, simp_all) apply (clarsimp simp: empty_descendants_range_in descendants_range_def2 invs_def valid_state_def
                         valid_pspace_def detype_clear_um_independent valid_etcbs_def) apply (simp add: invs_def valid_state_def valid_pspace_def detype_clear_um_independent valid_etcbs_def
                   is_etcb_at_def detype_def detype_ext_def st_tcb_at_kh_def obj_at_kh_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>cref dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) cref s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) cref s) \<and> valid_etcbs s) (modify (Untyped_D.detype S)) (delete_objects ptr bits) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1})) (delete_objects ptr bits) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1})) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; invs s' \<and> ct_active s' \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s' \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s') \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits
 2. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b dev idx. \<lbrakk>invs s'; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits
 2. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' a b dev idx. \<lbrakk>invs s'; ct_active s'; valid_etcbs s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits
 2. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>a b dev idx. cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s \<and> descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s) \<and> valid_etcbs s) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 s s' a b dev idx) (?Q'34 s s' a b dev idx) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) >>= return) (do y <- modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od)
 2. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q34 s s' a b dev idx sa
 3. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'34 s s' a b dev idx sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres (?r'38 s s' a b dev idx) (?P38 s s' a b dev idx) (?P'38 s s' a b dev idx) (modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1})) (modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1}))
 2. \<And>s s' a b dev idx rv y. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; ?r'38 s s' a b dev idx rv y\<rbrakk> \<Longrightarrow> dcorres dc (?R38 s s' a b dev idx rv) (?R'38 s s' a b dev idx y) (return rv) (do_machine_op (freeMemory ptr bits))
 3. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s s' a b dev idx\<rbrace> modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>?R38 s s' a b dev idx\<rbrace>
 4. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'38 s s' a b dev idx\<rbrace> modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>?R'38 s s' a b dev idx\<rbrace>
 5. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s = sa\<rbrakk> \<Longrightarrow> (?P38 s s' a b dev idx and ?Q38 s s' a b dev idx) sa
 6. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'38 s s' a b dev idx and ?Q'38 s s' a b dev idx) sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b dev idx rv y. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; dc rv y\<rbrakk> \<Longrightarrow> dcorres dc (?R38 s s' a b dev idx rv) (?R'38 s s' a b dev idx y) (return rv) (do_machine_op (freeMemory ptr bits))
 2. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s s' a b dev idx\<rbrace> modify (Untyped_D.detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>?R38 s s' a b dev idx\<rbrace>
 3. \<And>s s' a b dev idx. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'38 s s' a b dev idx\<rbrace> modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>?R'38 s s' a b dev idx\<rbrace>
 4. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q38 s s' a b dev idx) sa
 5. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. invs sa \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap (?dev44 s s' a b dev idx) ptr bits (?idx44 s s' a b dev idx))) cref sa) \<and> valid_etcbs sa) and ?Q'38 s s' a b dev idx) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' a b dev idx. \<lbrakk>transform s' = s; is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'38 s s' a b dev idx\<rbrace> modify (Retype_A.detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>\<lambda>y. pspace_no_overlap (up_aligned_area ptr bits) and valid_objs and valid_etcbs\<rbrace>
 2. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q38 s s' a b dev idx) sa
 3. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. invs sa \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap (?dev44 s s' a b dev idx) ptr bits (?idx44 s s' a b dev idx))) cref sa) \<and> valid_etcbs sa) and ?Q'38 s s' a b dev idx) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q38 s s' a b dev idx) sa
 2. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. invs sa \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap (?dev44 s s' a b dev idx) ptr bits (?idx44 s s' a b dev idx))) cref sa) \<and> valid_etcbs sa) and (\<lambda>s. (pspace_no_overlap (up_aligned_area ptr bits) and valid_objs and valid_etcbs) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} s))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s' a b dev idx. \<lbrakk>is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'\<rbrakk> \<Longrightarrow> ?Q38 (transform s') s' a b dev idx (transform s')
 2. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. invs sa \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap (?dev44 s s' a b dev idx) ptr bits (?idx44 s s' a b dev idx))) cref sa) \<and> valid_etcbs sa) and (\<lambda>s. (pspace_no_overlap (up_aligned_area ptr bits) and valid_objs and valid_etcbs) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} s))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' a b dev idx sa. \<lbrakk>True; transform (snd (s, s')) = fst (s, s'); is_aligned ptr bits; invs s'; 2 \<le> bits; bits < word_bits; ct_active s'; valid_etcbs s'; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) s'; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) s'; s' = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. invs sa \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap (?dev44 s s' a b dev idx) ptr bits (?idx44 s s' a b dev idx))) cref sa) \<and> valid_etcbs sa) and (\<lambda>s. (pspace_no_overlap (up_aligned_area ptr bits) and valid_objs and valid_etcbs) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} s))) sa proof (prove)
goal (1 subgoal):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> (\<exists>aa ba. cte_wp_at ((=) (cap.UntypedCap (?dev44 (transform sa) sa a b dev idx) ptr bits (?idx44 (transform sa) sa a b dev idx))) (aa, ba) sa) \<and> pspace_no_overlap (up_aligned_area ptr bits) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (2 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at ((=) (cap.UntypedCap (?dev44 (transform sa) sa a b dev idx) ptr bits (?idx44 (transform sa) sa a b dev idx))) (aa, ba) sa
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (1 subgoal):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (1 subgoal):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) \<and> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (3 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 3. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (4 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> pspace_aligned sa
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa\<rbrakk> \<Longrightarrow> valid_objs sa
 3. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 4. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (2 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (2 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx; untyped_children_in_mdb sa\<rbrakk> \<Longrightarrow> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (2 subgoals):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx; untyped_children_in_mdb sa; invs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} sa)) \<and> untyped_children_in_mdb (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} (clear_um {ptr..ptr + 2 ^ bits - 1} sa))\<rbrakk> \<Longrightarrow> valid_objs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa)
 2. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal (1 subgoal):
 1. \<And>a b dev idx sa. \<lbrakk>is_aligned ptr bits; invs sa; 2 \<le> bits; bits < word_bits; ct_active sa; valid_etcbs sa; cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) (a, b) sa; descendants_range (cap.UntypedCap dev ptr bits idx) (a, b) sa; sa \<turnstile> cap.UntypedCap dev ptr bits idx\<rbrakk> \<Longrightarrow> valid_etcbs (Retype_A.detype {ptr..ptr + 2 ^ bits - 1} sa) proof (prove)
goal:
No subgoals!