theory Retype_IF

lemma delete_objects_caps_no_overlap:
  "\<lbrace>invs and ct_active and (\<lambda>s. \<exists>slot idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s \<and>
                                           descendants_range_in {ptr..ptr + 2 ^ sz - 1} slot s)\<rbrace>
   delete_objects ptr sz
   \<lbrace>\<lambda>_ s :: det_ext state. caps_no_overlap ptr sz s\<rbrace>" apply (clarsimp simp: valid_def) apply (rule descendants_range_caps_no_overlapI) apply (erule use_valid | wp | simp add: descendants_range_def2 | blast)+ apply (frule untyped_cap_aligned,
         (simp add: invs_valid_objs)+) apply (rule conjI, assumption) apply (drule (2) untyped_slots_not_in_untyped_range, simp+, rule subset_refl) apply simp apply (erule use_valid | wp delete_objects_descendants_range_in | simp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and (\<lambda>s. \<exists>slot idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s \<and> descendants_range_in {ptr..ptr + 2 ^ sz - 1} slot s)\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. caps_no_overlap ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> invs b
 2. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev15 s b a ba idx) (ptr && ~~ mask sz) sz (?idx15 s b a ba idx))) (?cref15 s b a ba idx) b
 3. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (?cref15 s b a ba idx) b proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba idx. \<lbrakk>invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev50 s b a ba idx (interrupt_irq_node s)) (ptr && ~~ mask sz) sz (?idx48 s b a ba idx (interrupt_irq_node s)))) (?cref47 s b a ba idx) s \<and> (ptr \<le> fst (?cref47 s b a ba idx) \<longrightarrow> \<not> fst (?cref47 s b a ba idx) \<le> ptr + 2 ^ sz - 1)
 2. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (?cref47 s b a ba idx) b proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba idx. \<lbrakk>invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s; is_aligned ptr sz\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev50 s b a ba idx (interrupt_irq_node s)) ptr sz (?idx48 s b a ba idx (interrupt_irq_node s)))) (?cref47 s b a ba idx) s \<and> (ptr \<le> fst (?cref47 s b a ba idx) \<longrightarrow> \<not> fst (?cref47 s b a ba idx) \<le> ptr + 2 ^ sz - 1)
 2. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (?cref47 s b a ba idx) b proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba idx. \<lbrakk>invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s; is_aligned ptr sz\<rbrakk> \<Longrightarrow> ptr \<le> fst (a, ba) \<longrightarrow> \<not> fst (a, ba) \<le> ptr + 2 ^ sz - 1
 2. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (a, ba) b proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba idx. \<lbrakk>ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s; is_aligned ptr sz; fst (a, ba) \<notin> {ptr..ptr + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr \<le> fst (a, ba) \<longrightarrow> \<not> fst (a, ba) \<le> ptr + 2 ^ sz - 1
 2. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (a, ba) b proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba idx. \<lbrakk>((), b) \<in> fst (delete_objects ptr sz s); invs s; ct_active s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} (a, ba) s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) (a, ba) s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (a, ba) b proof (prove)
goal:
No subgoals!