theory ArchDetype_AI

lemma in_user_frame_eq:
  notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                     Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
                     order_class.Icc_eq_Icc
    and [simp] = p2pm1_to_mask
  shows "p \<notin> untyped_range cap \<Longrightarrow> in_user_frame p
              (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s
               \<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>)
         = in_user_frame p s" using cap_is_valid untyped apply (cases cap; simp add: in_user_frame_def valid_untyped_def valid_cap_def obj_at_def) apply (rule iffI; erule exEI; elim conjE exE; simp) subgoal for dev ptr n f sz ko apply (elim allE; erule (1) impE) apply (drule valid_pspace_aligned[OF valid_pspace]) apply (clarsimp simp: obj_range_def) apply (erule impE) apply (erule not_emptyI[rotated]) apply (rule mask_in_range[THEN iffD1, simplified]) apply (simp add: is_aligned_neg_mask) apply (simp add: mask_lower_twice) apply (cut_tac mask_in_range[THEN iffD1, simplified, OF is_aligned_neg_mask[OF le_refl] refl]) apply fastforce done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<notin> untyped_range cap \<Longrightarrow> in_user_frame p (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>) = in_user_frame p s proof (prove)
using this:
s \<turnstile> cap
is_untyped_cap cap

goal (1 subgoal):
 1. p \<notin> untyped_range cap \<Longrightarrow> in_user_frame p (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>) = in_user_frame p s proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>p \<notin> mask_range x22 x23; cap_aligned (UntypedCap x21 x22 x23 x24) \<and> (\<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> mask_range x22 x23 \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> mask_range x22 x23 \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}) \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (\<exists>sz. p && ~~ mask (pageBitsForSize sz) \<notin> mask_range x22 x23 \<and> (p && ~~ mask (pageBitsForSize sz) \<notin> mask_range x22 x23 \<longrightarrow> (\<exists>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz)))) = (\<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x ko. \<lbrakk>p \<notin> mask_range x22 x23; cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> mask_range x22 x23 \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> mask_range x22 x23 \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; kheap s (p && ~~ mask (pageBitsForSize x)) = Some ko; a_type ko = AArch (AUserData x)\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize x) \<notin> mask_range x22 x23 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> mask_range ptr n \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko; a_type ko = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<notin> mask_range ptr n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko; a_type ko = AArch (AUserData sz); obj_range (p && ~~ mask (pageBitsForSize sz)) ko \<inter> mask_range ptr n \<noteq> {} \<longrightarrow> obj_range (p && ~~ mask (pageBitsForSize sz)) ko \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> obj_range (p && ~~ mask (pageBitsForSize sz)) ko = {}\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<notin> mask_range ptr n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; a_type ko = AArch (AUserData sz); obj_range (p && ~~ mask (pageBitsForSize sz)) ko \<inter> mask_range ptr n \<noteq> {} \<longrightarrow> obj_range (p && ~~ mask (pageBitsForSize sz)) ko \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> obj_range (p && ~~ mask (pageBitsForSize sz)) ko = {}; is_aligned (p && ~~ mask (pageBitsForSize sz)) (obj_bits ko)\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<notin> mask_range ptr n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<inter> mask_range ptr n \<noteq> {} \<longrightarrow> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n\<rbrakk> \<Longrightarrow> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<inter> mask_range ptr n \<noteq> {}
 2. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz)\<rbrakk> \<Longrightarrow> p && ~~ mask (pageBitsForSize sz) \<in> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz)
 2. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz)\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz)
 2. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz)\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)
 3. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz)\<rbrakk> \<Longrightarrow> (p && ~~ mask (pageBitsForSize sz)) && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)
 2. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> mask_range ptr n; cap = UntypedCap dev ptr n f; cap_aligned (UntypedCap dev ptr n f); untyped_min_bits \<le> n; f \<le> 2 ^ n; ptr \<noteq> 0; ko = ArchObj (DataPage False sz); p && ~~ mask (pageBitsForSize sz) \<in> mask_range ptr n; mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) \<subseteq> mask_range ptr n \<and> (if f < 2 ^ n then {ptr + word_of_nat f..ptr + 2 ^ n - 1} else {}) \<inter> mask_range (p && ~~ mask (pageBitsForSize sz)) (pageBitsForSize sz) = {}; ?ptr'26 \<in> mask_range (?ptr'26 && ~~ mask ?bits26) ?bits26\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!