theory Detype_R

lemma cNodeNoPartialOverlap:
  "corres dc (\<lambda>s. \<exists>cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s
                     \<and> valid_objs s \<and> pspace_aligned s)
     \<top>
    (return x) (stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s)
       (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1)) [])" 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: cNodePartialOverlap_def) apply (drule(1) cte_wp_valid_cap) apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq
                          obj_at_def is_cap_table) 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) apply (blast intro: order_trans) apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. \<exists>cref. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) cref s \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>_. True) (return x) (stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1)) []) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. (\<exists>a b. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) (a, b) s) \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>_. True) (return x) (do s <- get;
if \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1) then return () else fail
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. corres dc (\<lambda>s. (\<exists>a b. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) (a, b) s) \<and> valid_objs s \<and> pspace_aligned s) (\<lambda>sa. sa = s \<and> True) (return x) (if \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1) 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> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1) \<Longrightarrow> corres dc (\<lambda>s. (\<exists>a b. cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) (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 ((=) (cap.UntypedCap d base magnitude idx)) (a, b) sa) \<and> valid_objs sa \<and> pspace_aligned sa; s' = s \<and> True\<rbrakk> \<Longrightarrow> \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1)
 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 ((=) (cap.UntypedCap d base magnitude idx)) (a, b) sa) \<and> valid_objs sa \<and> pspace_aligned sa; s' = s \<and> True\<rbrakk> \<Longrightarrow> \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1)
 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. \<lbrakk>(sa, s) \<in> state_relation; cte_wp_at ((=) (cap.UntypedCap d base magnitude idx)) (a, b) sa; valid_objs sa; pspace_aligned sa; 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; gsCNodes s p = Some n; sa \<turnstile> cap.UntypedCap d base magnitude idx\<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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; cap_aligned (cap.UntypedCap d base magnitude idx); kheap sa p = Some (CNode n cs); \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range p obj = {}; well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; cap_aligned (cap.UntypedCap d base magnitude idx); kheap sa p = Some (CNode n cs); \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range p obj = {}; well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; cap_aligned (cap.UntypedCap d base magnitude idx); kheap sa p = Some (CNode n cs); \<forall>p obj. kheap sa p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range p obj = {}; well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; is_aligned base magnitude \<and> magnitude < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; is_aligned p (cte_level_bits + n); p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; is_aligned base magnitude \<and> magnitude < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 2. \<And>s sa p n cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; is_aligned base magnitude \<and> magnitude < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs x xa. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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 base magnitude; magnitude < word_bits; base \<le> xa \<longrightarrow> \<not> xa \<le> base + 2 ^ magnitude - 1; base \<le> x; x \<le> base + 2 ^ magnitude - 1; p \<le> x; x \<le> p + 2 ^ (cte_level_bits + n) - 1; p \<le> xa; xa \<le> p + 2 ^ (cte_level_bits + n) - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s sa p n cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; is_aligned base magnitude \<and> magnitude < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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 cs. \<lbrakk>(sa, s) \<in> state_relation; valid_objs sa; pspace_aligned sa; is_aligned base magnitude \<and> magnitude < word_bits; kheap sa p = Some (CNode n cs); well_formed_cnode_n n cs; untyped_min_bits \<le> magnitude; idx \<le> 2 ^ magnitude; base \<noteq> 0; p \<le> base + 2 ^ magnitude - 1 \<and> base \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> p \<le> p + 2 ^ (cte_level_bits + n) - 1 \<and> base \<le> base + 2 ^ magnitude - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ (cte_level_bits + n) - 1 \<le> base + 2 ^ magnitude - 1 \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 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} \<subseteq> {x. base \<le> x \<and> x \<le> base + 2 ^ magnitude - 1} \<or> {p..p + 2 ^ (cte_level_bits + n) - 1} \<subseteq> {p. base \<le> p \<longrightarrow> \<not> p \<le> base + 2 ^ magnitude - 1})
 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!