theory CSpace1_R

lemma cte_at_cte_map_in_obj_bits:
  "\<lbrakk> cte_at p s; pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> cte_map p \<in> {fst p .. fst p + 2 ^ (obj_bits (the (kheap s (fst p)))) - 1}
           \<and> kheap s (fst p) \<noteq> None" apply (simp add: cte_at_cases) apply (elim disjE conjE exE) apply (clarsimp simp: well_formed_cnode_n_def) apply (drule(1) pspace_alignedD[rotated]) apply (erule(1) valid_objsE) apply (frule arg_cong[where f="\<lambda>S. snd p \<in> S"]) apply (simp(no_asm_use) add: domIff) apply (clarsimp simp: cte_map_def split_def
                         well_formed_cnode_n_def length_set_helper ex_with_length
                         valid_obj_def valid_cs_size_def valid_cs_def) apply (subgoal_tac "of_bl (snd p) * 2^cte_level_bits < 2 ^ (cte_level_bits + length (snd p))") apply (rule conjI) apply (erule is_aligned_no_wrap') apply assumption apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (erule word_le_minus_one_leq) apply (erule is_aligned_no_wrap') apply (rule word_power_less_1) apply (simp add: cte_level_bits_def word_bits_def) apply (simp add: power_add) apply (subst mult.commute, rule word_mult_less_mono1) apply (rule of_bl_length) apply (simp add: word_bits_def) apply (simp add: cte_level_bits_def) apply (simp add: word_bits_def) apply (drule power_strict_increasing [where a="2 :: nat"]) apply simp apply (simp add: cte_level_bits_def) apply (clarsimp simp: cte_map_def split_def field_simps) apply (subgoal_tac "of_bl (snd p) * 2^cte_level_bits < (2^tcb_bits :: word32)") apply (drule(1) pspace_alignedD[rotated]) apply (rule conjI) apply (erule is_aligned_no_wrap') apply (simp add: word_bits_conv) apply (rule word_plus_mono_right) apply (drule word_le_minus_one_leq) apply simp apply (erule is_aligned_no_wrap') apply simp apply (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1 cte_level_bits_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> cte_map p \<in> {fst p..fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1} \<and> kheap s (fst p) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; snd p \<in> dom fun\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y)
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun. \<lbrakk>valid_objs s; kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (obj_bits (CNode (length (snd p)) fun))\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (obj_bits (CNode (length (snd p)) fun)); valid_obj (fst p) (CNode (length (snd p)) fun) s\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (obj_bits (CNode (length (snd p)) fun)); valid_obj (fst p) (CNode (length (snd p)) fun) s; (snd p \<in> dom fun) = (snd p \<in> {x. length x = length (snd p)})\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); valid_obj (fst p) (CNode (length (snd p)) fun) s; \<exists>y. fun (snd p) = Some y\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<and> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<and> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (4 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 3. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 4. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (4 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 3. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 4. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + (2 ^ (cte_level_bits + length (snd p)) - 1)
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (4 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits \<le> 2 ^ (cte_level_bits + length (snd p)) - 1
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + (2 ^ (cte_level_bits + length (snd p)) - 1)
 3. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 4. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + (2 ^ (cte_level_bits + length (snd p)) - 1)
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> 2 ^ (cte_level_bits + length (snd p)) - 1 < 2 ^ (cte_level_bits + length (snd p))
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits; of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))\<rbrakk> \<Longrightarrow> cte_level_bits + length (snd p) < LENGTH(32)
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ (cte_level_bits + length (snd p))
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ cte_level_bits * 2 ^ length (snd p)
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (4 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) < 2 ^ length (snd p)
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ cte_level_bits
 3. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> unat (2 ^ length (snd p)) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 4. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (4 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> length (snd p) < LENGTH(32)
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ cte_level_bits
 3. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> unat (2 ^ length (snd p)) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 4. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ cte_level_bits
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> unat (2 ^ length (snd p)) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> unat (2 ^ length (snd p)) * unat (2 ^ cte_level_bits) < 2 ^ LENGTH(32)
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; length (snd p) < 32 - cte_level_bits\<rbrakk> \<Longrightarrow> 2 ^ length (snd p) * 2 ^ cte_level_bits < 4294967296
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; 2 ^ length (snd p) < 2 ^ (32 - cte_level_bits)\<rbrakk> \<Longrightarrow> 2 ^ length (snd p) * 2 ^ cte_level_bits < 4294967296
 3. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>fun y. \<lbrakk>kheap s (fst p) = Some (CNode (length (snd p)) fun); dom fun = {x. length x = length (snd p)}; is_aligned (fst p) (cte_level_bits + length (snd p)); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; 2 ^ length (snd p) < 2 ^ (32 - cte_level_bits)\<rbrakk> \<Longrightarrow> 2 ^ length (snd p) * 2 ^ cte_level_bits < 4294967296
 2. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>pspace_aligned s; valid_objs s; snd p \<in> dom tcb_cap_cases; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> fst p \<le> cte_map p \<and> cte_map p \<le> fst p + 2 ^ obj_bits (the (kheap s (fst p))) - 1 \<and> (\<exists>y. kheap s (fst p) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<and> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<and> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<and> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (3 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + of_bl (snd p) * 2 ^ cte_level_bits
 2. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF
 3. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (3 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ obj_bits (TCB tcb)
 2. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF
 3. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p + of_bl (snd p) * 2 ^ cte_level_bits \<le> fst p + 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (3 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits \<le> 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + 0x1FF
 3. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (3 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); is_aligned (fst p) (obj_bits (TCB tcb)); of_bl (snd p) * 2 ^ cte_level_bits \<le> 2 ^ tcb_bits - 1\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits \<le> 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + 0x1FF
 3. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits; is_aligned (fst p) (obj_bits (TCB tcb))\<rbrakk> \<Longrightarrow> fst p \<le> fst p + 0x1FF
 2. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b); of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits\<rbrakk> \<Longrightarrow> 0x1FF < 2 ^ obj_bits (TCB tcb)
 2. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal (1 subgoal):
 1. \<And>tcb a aa b. \<lbrakk>pspace_aligned s; valid_objs s; kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> of_bl (snd p) * 2 ^ cte_level_bits < 2 ^ tcb_bits proof (prove)
goal:
No subgoals!