theory CSpace1_R

lemma cte_map_inj:
  assumes neq: "p \<noteq> p'"
  assumes c1: "cte_at p s"
  assumes c2: "cte_at p' s"
  assumes vo: "valid_objs s"
  assumes al: "pspace_aligned s"
  assumes pd: "pspace_distinct s"
  shows "cte_map p \<noteq> cte_map p'" using cte_at_cte_map_in_obj_bits [OF c1 al vo]
        cte_at_cte_map_in_obj_bits [OF c2 al vo]
        pd apply (clarsimp simp: pspace_distinct_def
              simp del: atLeastAtMost_iff Int_atLeastAtMost) apply (elim allE, drule mp) apply (erule conjI)+ defer apply (simp add: field_simps
               del: atLeastAtMost_iff Int_atLeastAtMost) apply blast apply (clarsimp simp: cte_map_def split_def) apply (thin_tac "b \<le> a" for b a)+ apply (rule notE[OF neq]) apply (insert cte_at_length_limit [OF c1 vo]) apply (simp add: shiftl_t2n[where n=4, simplified, simplified mult.commute, symmetric]
                   word_bits_def cte_level_bits_def prod_eq_iff) apply (insert cte_at_cref_len[where p="fst p" and c="snd p" and c'="snd p'", simplified, OF c1]) apply (simp add: c2 prod_eqI) apply (subst rev_is_rev_conv[symmetric]) apply (rule nth_equalityI) apply simp apply clarsimp apply (drule_tac x="i + 4" in word_eqD) apply (simp add: nth_shiftl test_bit_of_bl nth_rev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map p \<noteq> cte_map p' proof (prove)
using this:
cte_map p \<in> {fst p..fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1} \<and> kheap s (fst p) \<noteq> None
cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits (the (kheap s (fst p'))) - 1} \<and> kheap s (fst p') \<noteq> None
pspace_distinct s

goal (1 subgoal):
 1. cte_map p \<noteq> cte_map p' proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>\<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}; cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> kheap s (?x10 y ya) = Some (?ko12 y ya) \<and> kheap s (?y11 y ya) = Some (?ko'13 y ya) \<and> ?x10 y ya \<noteq> ?y11 y ya
 2. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'; {?x10 y ya..?x10 y ya + (2 ^ obj_bits (?ko12 y ya) - 1)} \<inter> {?y11 y ya..?y11 y ya + (2 ^ obj_bits (?ko'13 y ya) - 1)} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> fst p \<noteq> fst p'
 2. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'; {fst p..fst p + (2 ^ obj_bits y - 1)} \<inter> {fst p'..fst p' + (2 ^ obj_bits ya - 1)} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'; {fst p..fst p + (2 ^ obj_bits y - 1)} \<inter> {fst p'..fst p' + (2 ^ obj_bits ya - 1)} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> fst p \<noteq> fst p' proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; kheap s (fst p) = Some y; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; kheap s (fst p') = Some ya; cte_map p = cte_map p'; {fst p..fst p + 2 ^ obj_bits y - 1} \<inter> {fst p'..fst p' + 2 ^ obj_bits ya - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> fst p \<noteq> fst p' proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>cte_map p' \<in> {fst p..fst p + 2 ^ obj_bits y - 1}; cte_map p' \<in> {fst p'..fst p' + 2 ^ obj_bits ya - 1}; cte_map p = cte_map p'\<rbrakk> \<Longrightarrow> fst p \<noteq> fst p' proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>of_bl (snd p) * 2 ^ cte_level_bits = of_bl (snd p') * 2 ^ cte_level_bits; fst p' + of_bl (snd p') * 2 ^ cte_level_bits \<le> fst p' + 2 ^ obj_bits y - 1; fst p' \<le> fst p' + of_bl (snd p') * 2 ^ cte_level_bits; fst p' + of_bl (snd p') * 2 ^ cte_level_bits \<le> fst p' + 2 ^ obj_bits ya - 1; fst p = fst p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>of_bl (snd p) * 2 ^ cte_level_bits = of_bl (snd p') * 2 ^ cte_level_bits; fst p = fst p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>of_bl (snd p) * 2 ^ cte_level_bits = of_bl (snd p') * 2 ^ cte_level_bits; fst p = fst p'\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>of_bl (snd p) * 2 ^ cte_level_bits = of_bl (snd p') * 2 ^ cte_level_bits; fst p = fst p'; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p) < 28\<rbrakk> \<Longrightarrow> snd p = snd p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p) < 28; cte_wp_at (\<lambda>_. True) (fst p, snd p') s \<Longrightarrow> length (snd p) = length (snd p')\<rbrakk> \<Longrightarrow> snd p = snd p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p')\<rbrakk> \<Longrightarrow> snd p = snd p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p')\<rbrakk> \<Longrightarrow> rev (snd p) = rev (snd p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p')\<rbrakk> \<Longrightarrow> length (rev (snd p)) = length (rev (snd p'))
 2. \<And>i. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p'); i < length (rev (snd p))\<rbrakk> \<Longrightarrow> rev (snd p) ! i = rev (snd p') ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p'); i < length (rev (snd p))\<rbrakk> \<Longrightarrow> rev (snd p) ! i = rev (snd p') ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>of_bl (snd p) << 4 = of_bl (snd p') << 4; fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p'); i < length (snd p')\<rbrakk> \<Longrightarrow> rev (snd p) ! i = rev (snd p') ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>fst p = fst p'; length (snd p') < 28; length (snd p) = length (snd p'); i < length (snd p'); (of_bl (snd p) << 4) !! (i + 4) = (of_bl (snd p') << 4) !! (i + 4)\<rbrakk> \<Longrightarrow> rev (snd p) ! i = rev (snd p') ! i proof (prove)
goal:
No subgoals!