theory Retype_C

lemma ctes_of_ko_at_strong:
  "\<lbrakk>ctes_of s p = Some a; is_aligned p cteSizeBits\<rbrakk> \<Longrightarrow>
  (\<exists>ptr ko. (ksPSpace s ptr = Some ko \<and> {p ..+ 2^cteSizeBits} \<subseteq> obj_range' ptr ko))" apply (clarsimp simp: map_to_ctes_def Let_def split: if_split_asm) apply (intro exI conjI, assumption) apply (simp add: obj_range'_def objBits_simps is_aligned_no_wrap' field_simps) apply (subst intvl_range_conv[where bits=cteSizeBits]) apply simp apply (simp add: word_bits_def objBits_defs) apply (simp add: field_simps) apply (intro exI conjI, assumption) apply (clarsimp simp: objBits_simps obj_range'_def word_and_le2) apply (cut_tac intvl_range_conv[where bits=cteSizeBits and ptr=p, simplified]) defer apply simp apply (simp add: word_bits_conv objBits_defs) apply (intro conjI) apply (rule order_trans[OF word_and_le2]) apply clarsimp apply clarsimp apply (thin_tac "P \<or> Q" for P Q) apply (erule order_trans) apply (subst word_plus_and_or_coroll2[where x=p and w="mask tcbBlockSizeBits",symmetric]) apply (clarsimp simp: tcb_cte_cases_def field_simps split: if_split_asm;
         simp only: p_assoc_help;
         rule word_plus_mono_right[OF _ is_aligned_no_wrap', OF _ Aligned.is_aligned_neg_mask[OF le_refl]];
         simp add: objBits_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some a; is_aligned p cteSizeBits\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)); {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko
 2. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)); {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' p (KOCTE a)
 2. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> {p..+2 ^ cteSizeBits} \<subseteq> {p..p + 2 ^ cteSizeBits - 1}
 2. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> is_aligned p cteSizeBits
 2. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> cteSizeBits < LENGTH(32)
 3. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> {p..p + 2 ^ cteSizeBits - 1} \<subseteq> {p..p + 2 ^ cteSizeBits - 1}
 4. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> cteSizeBits < LENGTH(32)
 2. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> {p..p + 2 ^ cteSizeBits - 1} \<subseteq> {p..p + 2 ^ cteSizeBits - 1}
 3. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p cteSizeBits; {1 + p..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> {p..p + 2 ^ cteSizeBits - 1} \<subseteq> {p..p + 2 ^ cteSizeBits - 1}
 2. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' ptr ko proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b. \<lbrakk>is_aligned p cteSizeBits; is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> {p..+2 ^ cteSizeBits} \<subseteq> obj_range' (p && ~~ mask (objBitsKO (KOTCB undefined))) (KOTCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x \<and> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (3 subgoals):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x \<and> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 2. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> is_aligned p cteSizeBits
 3. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> cteSizeBits < 32 proof (prove)
goal (3 subgoals):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> is_aligned p cteSizeBits
 2. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> cteSizeBits < 32
 3. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x \<and> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}\<rbrakk> \<Longrightarrow> cteSizeBits < 32
 2. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x \<and> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x \<and> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> x
 2. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> p \<le> x
 2. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); x \<in> {p..+2 ^ cteSizeBits}; {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ cteSizeBits - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}; p \<le> x; x \<le> p + 2 ^ cteSizeBits - 1\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}; p \<le> x; x \<le> p + 2 ^ cteSizeBits - 1\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}; p \<le> x\<rbrakk> \<Longrightarrow> p + 2 ^ cteSizeBits - 1 \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b x. \<lbrakk>is_aligned p cteSizeBits; {(p && ~~ mask tcbBlockSizeBits) + 1..(p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (aa, b); {p..+2 ^ cteSizeBits} = {p..p + 2 ^ cteSizeBits - 1}; p \<le> x\<rbrakk> \<Longrightarrow> (p && mask tcbBlockSizeBits) + (p && ~~ mask tcbBlockSizeBits) + 2 ^ cteSizeBits - 1 \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal:
No subgoals!