theory Untyped_AI

lemma pspace_no_overlap_detype':
  "\<lbrakk> s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> pspace_no_overlap {ptr .. ptr + 2 ^ bits - 1} (detype {ptr .. ptr + 2 ^ bits - 1} s)" apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff
        simp: obj_range_def add_diff_eq[symmetric] pspace_no_overlap_def) apply (frule(2) valid_untypedD) apply (rule ccontr) apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                            Int_atLeastAtMost atLeastatMost_empty_iff is_aligned_neg_mask_eq
                      simp: valid_cap_def cap_aligned_def obj_range_def cap_range_def is_aligned_neg_mask_eq p_assoc_help) apply (drule_tac c= x in set_mp) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> pspace_no_overlap {ptr..ptr + 2 ^ bits - 1} (detype {ptr..ptr + 2 ^ bits - 1} s) proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}; obj_range x ko \<inter> cap_range (UntypedCap dev ptr bits idx) \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> cap_range (UntypedCap dev ptr bits idx) \<and> obj_range x ko \<inter> usable_untyped_range (UntypedCap dev ptr bits idx) = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}; obj_range x ko \<inter> cap_range (UntypedCap dev ptr bits idx) \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> cap_range (UntypedCap dev ptr bits idx) \<and> obj_range x ko \<inter> usable_untyped_range (UntypedCap dev ptr bits idx) = {}; {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}; {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} \<noteq> {}; is_aligned ptr bits; {x..x + (2 ^ obj_bits ko - 1)} \<subseteq> {ptr..ptr + (2 ^ bits - 1)}; {x..x + (2 ^ obj_bits ko - 1)} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; bits < word_bits; valid_untyped (UntypedCap dev ptr bits idx) s; untyped_min_bits \<le> bits; idx \<le> 2 ^ bits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}; {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} \<noteq> {}; is_aligned ptr bits; {x..x + (2 ^ obj_bits ko - 1)} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; bits < word_bits; valid_untyped (UntypedCap dev ptr bits idx) s; untyped_min_bits \<le> bits; idx \<le> 2 ^ bits; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> {x..x + (2 ^ obj_bits ko - 1)}
 2. \<And>x ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s x = Some ko; x \<notin> {ptr..ptr + (2 ^ bits - 1)}; {x..x + (2 ^ obj_bits ko - 1)} \<inter> {ptr..ptr + (2 ^ bits - 1)} \<noteq> {}; is_aligned ptr bits; {x..x + (2 ^ obj_bits ko - 1)} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; bits < word_bits; valid_untyped (UntypedCap dev ptr bits idx) s; untyped_min_bits \<le> bits; idx \<le> 2 ^ bits; ptr \<noteq> 0; x \<in> {ptr..ptr + (2 ^ bits - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!