theory Invariants_H

lemma cte_wp_at_cases':
  shows "cte_wp_at' P p s =
  ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits
             \<and> P cte \<and> ps_clear p cteSizeBits s) \<or>
   (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits
             \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))"
  (is "?LHS = ?RHS") apply (rule iffI) apply (clarsimp simp: cte_wp_at'_def split_def
                         getObject_def bind_def simpler_gets_def
                         assert_opt_def return_def fail_def
                  split: option.splits
                    del: disjCI) apply (clarsimp simp: loadObject_cte typeError_def alignError_def
                         fail_def return_def objBits_simps'
                         is_aligned_mask[symmetric] alignCheck_def
                         tcbVTableSlot_def field_simps tcbCTableSlot_def
                         tcbReplySlot_def tcbCallerSlot_def
                         tcbIPCBufferSlot_def
                         lookupAround2_char1
                         cte_level_bits_def Ball_def
                         unless_def when_def bind_def
                  split: kernel_object.splits if_split_asm option.splits
                    del: disjCI) apply (subst(asm) in_magnitude_check3, simp+,
               simp split: if_split_asm, (rule disjI2)?, intro exI, rule conjI,
               erule rsubst[where P="\<lambda>x. ksPSpace s x = v" for s v],
               fastforce simp add: field_simps, simp)+ apply (subst(asm) in_magnitude_check3, simp+) apply (simp split: if_split_asm) apply (simp add: cte_wp_at'_def getObject_def split_def
                   bind_def simpler_gets_def return_def
                   assert_opt_def fail_def objBits_simps'
            split: option.splits) apply (elim disjE conjE exE) apply (erule(1) ps_clear_lookupAround2) apply simp apply (simp add: field_simps) apply (erule is_aligned_no_wrap') apply (simp add: cte_level_bits_def word_bits_conv) apply (simp add: cte_level_bits_def) apply (simp add: loadObject_cte unless_def alignCheck_def
                    is_aligned_mask[symmetric] objBits_simps'
                    cte_level_bits_def magnitudeCheck_def
                    return_def fail_def) apply (clarsimp simp: bind_def return_def when_def fail_def
                  split: option.splits) apply simp apply (erule(1) ps_clear_lookupAround2) prefer 3 apply (simp add: loadObject_cte unless_def alignCheck_def
                    is_aligned_mask[symmetric] objBits_simps'
                    cte_level_bits_def magnitudeCheck_def
                    return_def fail_def tcbCTableSlot_def tcbVTableSlot_def
                    tcbIPCBufferSlot_def tcbReplySlot_def tcbCallerSlot_def
                split: option.split_asm) apply (clarsimp simp: bind_def tcb_cte_cases_def split: if_split_asm) apply (clarsimp simp: bind_def tcb_cte_cases_def iffD2[OF linorder_not_less]
                          return_def
                   split: if_split_asm) apply (subgoal_tac "p - n \<le> (p - n) + n", simp) apply (erule is_aligned_no_wrap') apply (simp add: word_bits_conv) apply (simp add: tcb_cte_cases_def split: if_split_asm) apply (subgoal_tac "(p - n) + n \<le> (p - n) + 511") apply (simp add: field_simps) apply (rule word_plus_mono_right) apply (simp add: tcb_cte_cases_def split: if_split_asm) apply (erule is_aligned_no_wrap') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p s = ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (2 subgoals):
 1. cte_wp_at' P p s \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)
 2. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>a b cte. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, b); fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)}; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))
 2. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (7 subgoals):
 1. \<And>a cte x6. \<lbrakk>P cte; a \<le> a + 0x10; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> a + 0x10 \<longrightarrow> ksPSpace s z = None; is_aligned a 9; p = a + 0x10; (\<Union>x\<in>fst (magnitudeCheck a (snd (lookupAround2 (a + 0x10) (ksPSpace s))) 9 s). fst (case x of (y, s) \<Rightarrow> ({(tcbVTable x6, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s (a + 0x10) = Some (KOCTE cte) \<and> is_aligned (a + 0x10) 4 \<and> P cte \<and> ps_clear (a + 0x10) 4 s) \<or> (\<exists>n tcb. ksPSpace s (a + 0x10 - n) = Some (KOTCB tcb) \<and> is_aligned (a + 0x10 - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (a + 0x10 - n) 9 s))
 2. \<And>cte x6. \<lbrakk>P cte; ksPSpace s p = Some (KOTCB x6); \<forall>z. p < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p 9; (\<Union>x\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) 9 s). fst (case x of (y, s) \<Rightarrow> ({(tcbCTable x6, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)
 3. \<And>a cte x6. \<lbrakk>P cte; a \<le> a + 0x20; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> a + 0x20 \<longrightarrow> ksPSpace s z = None; is_aligned a 9; p = a + 0x20; (\<Union>x\<in>fst (magnitudeCheck a (snd (lookupAround2 (a + 0x20) (ksPSpace s))) 9 s). fst (case x of (y, s) \<Rightarrow> ({(tcbReply x6, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (a + 0x20 - n) = Some (KOTCB tcb) \<and> is_aligned (a + 0x20 - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (a + 0x20 - n) 9 s)
 4. \<And>a cte x6. \<lbrakk>P cte; a \<le> a + 0x30; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> a + 0x30 \<longrightarrow> ksPSpace s z = None; is_aligned a 9; p = a + 0x30; (\<Union>x\<in>fst (magnitudeCheck a (snd (lookupAround2 (a + 0x30) (ksPSpace s))) 9 s). fst (case x of (y, s) \<Rightarrow> ({(tcbCaller x6, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (a + 0x30 - n) = Some (KOTCB tcb) \<and> is_aligned (a + 0x30 - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (a + 0x30 - n) 9 s)
 5. \<And>a cte x6. \<lbrakk>P cte; a \<le> a + 0x40; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> a + 0x40 \<longrightarrow> ksPSpace s z = None; is_aligned a 9; p = a + 0x40; (\<Union>x\<in>fst (magnitudeCheck a (snd (lookupAround2 (a + 0x40) (ksPSpace s))) 9 s). fst (case x of (y, s) \<Rightarrow> ({(tcbIPCBufferFrame x6, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (a + 0x40 - n) = Some (KOTCB tcb) \<and> is_aligned (a + 0x40 - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (a + 0x40 - n) 9 s)
 6. \<And>cte x7. \<lbrakk>P cte; ksPSpace s p = Some (KOCTE x7); \<forall>z. p < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p 4; (\<Union>x\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) 4 s). fst (case x of (y, s) \<Rightarrow> ({(x7, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> P x7 \<and> ps_clear p 4 s \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))
 7. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>cte x7. \<lbrakk>P cte; ksPSpace s p = Some (KOCTE x7); \<forall>z. p < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p 4; (\<Union>x\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) 4 s). fst (case x of (y, s) \<Rightarrow> ({(x7, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> P x7 \<and> ps_clear p 4 s \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))
 2. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>cte x7. \<lbrakk>P cte; ksPSpace s p = Some (KOCTE x7); \<forall>z. p < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p 4; (\<Union>x\<in>if ps_clear p 4 s then {((), s)} else {}. fst (case x of (y, s) \<Rightarrow> ({(x7, s)}, False))) = {(cte, s)}\<rbrakk> \<Longrightarrow> P x7 \<and> ps_clear p 4 s \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))
 2. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (1 subgoal):
 1. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s) \<Longrightarrow> cte_wp_at' P p s proof (prove)
goal (1 subgoal):
 1. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; ps_clear p 4 s\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (4 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte\<rbrakk> \<Longrightarrow> p \<le> p
 2. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ 4 - 1
 3. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 4. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ 4 - 1
 2. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte\<rbrakk> \<Longrightarrow> p \<le> p + 0xF
 2. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); P cte\<rbrakk> \<Longrightarrow> 0xF < 2 ^ cte_level_bits
 2. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p 4; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> \<exists>ctea. fst (loadObject p p (snd (lookupAround2 p (ksPSpace s))) (KOCTE cte) s) = {(ctea, s)} \<and> P ctea
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p 4; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - p\<rbrakk> \<Longrightarrow> \<exists>ctea. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
y <- case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - p < 1 << 4) fail;
\<lambda>s. ({(cte, s)}, False)
od) s) = {(ctea, s)} \<and> P ctea
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (2 subgoals):
 1. \<And>cte x2a. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p 4; P cte; fst (lookupAround2 p (ksPSpace s)) = Some (p, KOCTE cte); snd (lookupAround2 p (ksPSpace s)) = Some x2a; 0x10 \<le> x2a - p; x2a - p < 0x10\<rbrakk> \<Longrightarrow> False
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); ps_clear (p - n) 9 s; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); fst (lookupAround2 p (ksPSpace s)) = Some (p - n, KOTCB tcb); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - (p - n)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte)) proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); fst (lookupAround2 p (ksPSpace s)) = Some (p - n, KOTCB tcb); case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - (p - n)\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b)) \<and> (\<forall>a b. fst (lookupAround2 p (ksPSpace s)) = Some (a, b) \<longrightarrow> (\<exists>cte. fst (loadObject p a (snd (lookupAround2 p (ksPSpace s))) b s) = {(cte, s)} \<and> P cte))
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (4 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); fst (lookupAround2 p (ksPSpace s)) = Some (p - n, KOTCB tcb); snd (lookupAround2 p (ksPSpace s)) = None\<rbrakk> \<Longrightarrow> (n = 0x40 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x40 \<longrightarrow> (n = 0x30 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({(tcbCaller tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x30 \<longrightarrow> (n = 0x20 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({(tcbReply tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x20 \<longrightarrow> (n = 0 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({(tcbCTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0 \<longrightarrow> (n = 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({(tcbVTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- \<lambda>s. ({((), s)}, False);
\<lambda>s. ({}, True)
od) s) = {(cte, s)} \<and> P cte))))))
 2. \<And>n tcb getF setF x2. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); fst (lookupAround2 p (ksPSpace s)) = Some (p - n, KOTCB tcb); snd (lookupAround2 p (ksPSpace s)) = Some x2; 0x200 \<le> x2 - (p - n)\<rbrakk> \<Longrightarrow> (n = 0x40 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x40) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x40 \<longrightarrow> (n = 0x30 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x30) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbCaller tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x30 \<longrightarrow> (n = 0x20 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x20) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbReply tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x20 \<longrightarrow> (n = 0 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - p < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbCTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0 \<longrightarrow> (n = 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x10) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbVTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - n) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({}, True)
od) s) = {(cte, s)} \<and> P cte))))))
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p
 4. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF x2. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); fst (lookupAround2 p (ksPSpace s)) = Some (p - n, KOTCB tcb); snd (lookupAround2 p (ksPSpace s)) = Some x2; 0x200 \<le> x2 - (p - n)\<rbrakk> \<Longrightarrow> (n = 0x40 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x40) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x40 \<longrightarrow> (n = 0x30 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x30) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbCaller tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x30 \<longrightarrow> (n = 0x20 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x20) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbReply tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x20 \<longrightarrow> (n = 0 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - p < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbCTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0 \<longrightarrow> (n = 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - 0x10) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({(tcbVTable tcb, s)}, False)
od) s) = {(cte, s)} \<and> P cte)) \<and> (n \<noteq> 0x10 \<longrightarrow> (\<exists>cte. fst ((do y <- \<lambda>s. ({((), s)}, False);
y <- when (x2 - (p - n) < 0x200) (\<lambda>s. ({}, True));
\<lambda>s. ({}, True)
od) s) = {(cte, s)} \<and> P cte))))))
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p - n + n
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> n < 2 ^ 9
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> n < 0x200
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF); p - n + n \<le> p - n + 0x1FF\<rbrakk> \<Longrightarrow> p \<le> p - n + 2 ^ 9 - 1
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n + n \<le> p - n + 0x1FF proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n + n \<le> p - n + 0x1FF proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> n \<le> 0x1FF
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p - n + 0x1FF proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p - n \<le> p - n + 0x1FF proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); P (getF tcb); tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> 0x1FF < 2 ^ 9 proof (prove)
goal:
No subgoals!