theory Detype_R

lemma cte_wp_at_delete':
  "\<lbrakk> s \<turnstile>' UntypedCap d base magnitude idx; pspace_distinct' s \<rbrakk> \<Longrightarrow>
   cte_wp_at' P p (s \<lparr> ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x \<rparr>)
    = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> cte_wp_at' P p s)" apply (simp add: cte_wp_at_obj_cases' obj_at_delete') apply (subgoal_tac "\<forall>Q n. obj_at' Q (p - n) s \<and> tcb_cte_cases n \<noteq> None \<longrightarrow>
                             ((p - n) \<in> {base .. base + (2 ^ magnitude - 1)})
                              = (p \<in> {base .. base + (2 ^ magnitude - 1)})") apply auto[1] apply (clarsimp simp: obj_at'_real_def projectKOs valid_cap'_def
                        valid_untyped'_def
              simp del: atLeastAtMost_iff) apply (drule_tac x="p - n" in spec) apply (clarsimp simp: ko_wp_at'_def capAligned_def
              simp del: atLeastAtMost_iff) apply (thin_tac "is_aligned x minUntypedSizeBits" for x) apply (drule(1) aligned_ranges_subset_or_disjoint) apply (subgoal_tac "{p, p - n} \<subseteq> obj_range' (p - n) (KOTCB obj)") apply (clarsimp simp del: atLeastAtMost_iff
                       simp: field_simps objBits_simps obj_range'_def) apply fastforce apply (simp add: obj_range'_def mask_in_range[symmetric]
              del: atLeastAtMost_iff) apply (simp add: objBits_simps) apply (frule(1) tcb_cte_cases_aligned_helpers) apply (simp add: is_aligned_neg_mask_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d base magnitude idx) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>) = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> cte_wp_at' P p s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d base magnitude idx) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. (base \<le> p - n \<longrightarrow> \<not> p - n \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s)) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> (obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d base magnitude idx) s; pspace_distinct' s; \<forall>Q n. obj_at' Q (p - n) s \<and> tcb_cte_cases n \<noteq> None \<longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)})\<rbrakk> \<Longrightarrow> ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. (base \<le> p - n \<longrightarrow> \<not> p - n \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s)) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> (obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s)))
 2. \<lbrakk>valid_cap' (capability.UntypedCap d base magnitude idx) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> \<forall>Q n. obj_at' Q (p - n) s \<and> tcb_cte_cases n \<noteq> None \<longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d base magnitude idx) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> \<forall>Q n. obj_at' Q (p - n) s \<and> tcb_cte_cases n \<noteq> None \<longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b. \<lbrakk>pspace_distinct' s; capAligned (capability.UntypedCap d base magnitude idx); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {base..base + 2 ^ magnitude - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<noteq> {}) ptr' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; is_aligned (word_of_nat idx) minUntypedSizeBits; ko_wp_at' (\<lambda>ko. \<exists>obj. ko = KOTCB obj \<and> Q obj) (p - n) s; tcb_cte_cases n = Some (a, b)\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b. \<lbrakk>pspace_distinct' s; capAligned (capability.UntypedCap d base magnitude idx); base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; is_aligned (word_of_nat idx) minUntypedSizeBits; ko_wp_at' (\<lambda>ko. \<exists>obj. ko = KOTCB obj \<and> Q obj) (p - n) s; tcb_cte_cases n = Some (a, b); \<not> ko_wp_at' (\<lambda>ko. {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) ko \<or> obj_range' (p - n) ko \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<noteq> {}) (p - n) s\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; is_aligned (word_of_nat idx) minUntypedSizeBits; tcb_cte_cases n = Some (a, b); is_aligned base magnitude; magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); is_aligned base magnitude; magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; {base..base + 2 ^ magnitude - 1} \<inter> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} = {} \<or> {base..base + 2 ^ magnitude - 1} \<subseteq> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<or> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<subseteq> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)}) proof (prove)
goal (2 subgoals):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; {base..base + 2 ^ magnitude - 1} \<inter> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} = {} \<or> {base..base + 2 ^ magnitude - 1} \<subseteq> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<or> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<subseteq> {base..base + 2 ^ magnitude - 1}; {p, p - n} \<subseteq> obj_range' (p - n) (KOTCB obj)\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + (2 ^ magnitude - 1)}) = (p \<in> {base..base + (2 ^ magnitude - 1)})
 2. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; {base..base + 2 ^ magnitude - 1} \<inter> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} = {} \<or> {base..base + 2 ^ magnitude - 1} \<subseteq> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<or> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<subseteq> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> {p, p - n} \<subseteq> obj_range' (p - n) (KOTCB obj) proof (prove)
goal (2 subgoals):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) tcbBlockSizeBits; ps_clear (p - n) tcbBlockSizeBits s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> {p - n..p + 2 ^ tcbBlockSizeBits - (n + 1)}; {p - n..p + 2 ^ tcbBlockSizeBits - (n + 1)} \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; p - n \<le> p + 2 ^ tcbBlockSizeBits - (n + 1) \<longrightarrow> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p + 2 ^ tcbBlockSizeBits - (n + 1) \<longrightarrow> p - n \<le> base + 2 ^ magnitude - 1 \<longrightarrow> p - n \<le> base \<and> base + 2 ^ magnitude - 1 \<le> p + 2 ^ tcbBlockSizeBits - (n + 1) \<or> base \<le> p - n \<and> p + 2 ^ tcbBlockSizeBits - (n + 1) \<le> base + 2 ^ magnitude - 1; p \<in> {p - n..p + 2 ^ tcbBlockSizeBits - (n + 1)}; p - n \<in> {p - n..p + 2 ^ tcbBlockSizeBits - (n + 1)}\<rbrakk> \<Longrightarrow> (p - n \<in> {base..base + 2 ^ magnitude - 1}) = (p \<in> {base..base + 2 ^ magnitude - 1})
 2. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; {base..base + 2 ^ magnitude - 1} \<inter> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} = {} \<or> {base..base + 2 ^ magnitude - 1} \<subseteq> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<or> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<subseteq> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> {p, p - n} \<subseteq> obj_range' (p - n) (KOTCB obj) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> obj_range' (p - n) (KOTCB obj); obj_range' (p - n) (KOTCB obj) \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; {base..base + 2 ^ magnitude - 1} \<inter> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} = {} \<or> {base..base + 2 ^ magnitude - 1} \<subseteq> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<or> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<subseteq> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> {p, p - n} \<subseteq> obj_range' (p - n) (KOTCB obj) proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) (objBitsKO (KOTCB obj)); ps_clear (p - n) (objBitsKO (KOTCB obj)) s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1}; {p - n..p - n + 2 ^ objBitsKO (KOTCB obj) - 1} \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; p - n \<le> p - n + 2 ^ objBitsKO (KOTCB obj) - 1 \<longrightarrow> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p - n + 2 ^ objBitsKO (KOTCB obj) - 1 \<longrightarrow> p - n \<le> base + 2 ^ magnitude - 1 \<longrightarrow> p - n \<le> base \<and> base + 2 ^ magnitude - 1 \<le> p - n + 2 ^ objBitsKO (KOTCB obj) - 1 \<or> base \<le> p - n \<and> p - n + 2 ^ objBitsKO (KOTCB obj) - 1 \<le> base + 2 ^ magnitude - 1\<rbrakk> \<Longrightarrow> p && ~~ mask (objBitsKO (KOTCB obj)) = p - n proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) tcbBlockSizeBits; ps_clear (p - n) tcbBlockSizeBits s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}; {p - n..p - n + 2 ^ tcbBlockSizeBits - 1} \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; p - n \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<longrightarrow> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<longrightarrow> p - n \<le> base + 2 ^ magnitude - 1 \<longrightarrow> p - n \<le> base \<and> base + 2 ^ magnitude - 1 \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<or> base \<le> p - n \<and> p - n + 2 ^ tcbBlockSizeBits - 1 \<le> base + 2 ^ magnitude - 1\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits = p - n proof (prove)
goal (1 subgoal):
 1. \<And>Q n a b obj. \<lbrakk>pspace_distinct' s; base \<noteq> 0; minUntypedSizeBits \<le> magnitude; magnitude \<le> maxUntypedSizeBits; idx \<le> 2 ^ magnitude; tcb_cte_cases n = Some (a, b); magnitude < word_bits; ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) tcbBlockSizeBits; ps_clear (p - n) tcbBlockSizeBits s; Q obj; \<not> {base..base + 2 ^ magnitude - 1} \<subset> {p - n..p - n + 2 ^ tcbBlockSizeBits - 1}; {p - n..p - n + 2 ^ tcbBlockSizeBits - 1} \<inter> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) = {}; p - n \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<longrightarrow> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<longrightarrow> p - n \<le> base + 2 ^ magnitude - 1 \<longrightarrow> p - n \<le> base \<and> base + 2 ^ magnitude - 1 \<le> p - n + 2 ^ tcbBlockSizeBits - 1 \<or> base \<le> p - n \<and> p - n + 2 ^ tcbBlockSizeBits - 1 \<le> base + 2 ^ magnitude - 1; p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits = p - n proof (prove)
goal:
No subgoals!