theory Untyped_R

lemma cNodeNoOverlap:
  notes Int_atLeastAtMost[simp del]
  shows
  "corres dc (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>cap. is_untyped_cap cap
                  \<and> Collect R \<subseteq> usable_untyped_range cap) cref s
              \<and> valid_objs s \<and> pspace_aligned s)
     \<top>
    (return x) (stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) R) [])" apply (simp add: stateAssert_def assert_def) apply (rule corres_symb_exec_r[OF _ get_sp]) apply (rule corres_req[rotated], subst if_P, assumption) apply simp apply (clarsimp simp: cNodeOverlap_def cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid_cap) apply (frule usable_range_subseteq[rotated], simp add: valid_cap_def) apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq
                          obj_at_def is_cap_table is_cap_simps) apply (frule(1) pspace_alignedD) apply simp apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) apply (clarsimp simp: is_aligned_no_overflow simp del: ) apply blast apply (simp add: is_aligned_no_overflow power_overflow word_bits_def
                     Int_atLeastAtMost) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) cref s \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>_. True) (return x) (stateAssert (\<lambda>s. \<not> cNodeOverlap (gsCNodes s) R) []) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. (\<exists>a b. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) (a, b) s) \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>_. True) (return x) (do s <- get;
if \<not> cNodeOverlap (gsCNodes s) R then return () else fail
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. corres dc (\<lambda>s. (\<exists>a b. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) (a, b) s) \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>sa. sa = s \<and> True) (return x) (if \<not> cNodeOverlap (gsCNodes s) R then return () else fail)
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (4 subgoals):
 1. \<And>s. \<not> cNodeOverlap (gsCNodes s) R \<Longrightarrow> corres dc (\<lambda>s. (\<exists>a b. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) (a, b) s) \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>sa. sa = s \<and> True) (return x) (return ())
 2. \<And>s sa s'. \<lbrakk>(sa, s') \<in> state_relation; (\<exists>a b. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) (a, b) sa) \<and> valid_objs sa \<and> pspace_aligned sa; s' = s \<and> True\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes s) R
 3. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa s'. \<lbrakk>(sa, s') \<in> state_relation; (\<exists>a b. cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> Collect R \<subseteq> usable_untyped_range cap) (a, b) sa) \<and> valid_objs sa \<and> pspace_aligned sa; s' = s \<and> True\<rbrakk> \<Longrightarrow> \<not> cNodeOverlap (gsCNodes s) R
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b cap. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some cap; is_untyped_cap cap; Collect R \<subseteq> usable_untyped_range cap; gsCNodes s p = Some n\<rbrakk> \<Longrightarrow> is_aligned p (cte_level_bits + n) \<and> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b cap. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some cap; is_untyped_cap cap; Collect R \<subseteq> usable_untyped_range cap; gsCNodes s p = Some n; sa \<turnstile> cap\<rbrakk> \<Longrightarrow> is_aligned p (cte_level_bits + n) \<and> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b cap. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some cap; is_untyped_cap cap; Collect R \<subseteq> usable_untyped_range cap; gsCNodes s p = Some n; sa \<turnstile> cap; usable_untyped_range cap \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> is_aligned p (cte_level_bits + n) \<and> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; cap_aligned (cap.UntypedCap dev r bits f); kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned p (cte_level_bits + n) \<and> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; cap_aligned (cap.UntypedCap dev r bits f); kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; is_aligned p (obj_bits (CNode n cs))\<rbrakk> \<Longrightarrow> is_aligned p (cte_level_bits + n) \<and> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; cap_aligned (cap.UntypedCap dev r bits f); kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; is_aligned p (cte_level_bits + n)\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; is_aligned r bits \<and> bits < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; is_aligned p (cte_level_bits + n); {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1) \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (4 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; is_aligned r bits \<and> bits < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1) \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}; is_aligned p (cte_level_bits + n); cte_level_bits + n < word_bits\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; is_aligned r bits \<and> bits < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1) \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}; p = 0; word_bits \<le> cte_level_bits + n\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 3. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (4 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1 \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}; is_aligned p (cte_level_bits + n); cte_level_bits + n < word_bits; is_aligned r bits; bits < word_bits\<rbrakk> \<Longrightarrow> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; is_aligned r bits \<and> bits < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1) \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}; p = 0; word_bits \<le> cte_level_bits + n\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 3. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (3 subgoals):
 1. \<And>s sa p n a b dev r bits f cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; caps_of_state sa (a, b) = Some (cap.UntypedCap dev r bits f); Collect R \<subseteq> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}); (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<subseteq> {r..r + 2 ^ bits - 1}; is_aligned r bits \<and> bits < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> r \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> r + 2 ^ bits - 1) \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ (cte_level_bits + n) - 1} = {}; p = 0; word_bits \<le> cte_level_bits + n\<rbrakk> \<Longrightarrow> \<not> word_bits \<le> cte_level_bits + n \<and> {p..p + 2 ^ (cte_level_bits + n) - 1} \<inter> Collect R = {}
 2. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. True \<Longrightarrow> no_fail (\<lambda>_. True) get proof (prove)
goal:
No subgoals!