theory IsolatedThreadAction

lemma setCTE_assert_modify:
  "setCTE p v = do c \<leftarrow> gets (real_cte_at' p);
                   t \<leftarrow> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits)
                                 and K ((p && mask tcbBlockSizeBits) \<in> dom tcb_cte_cases));
                   if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v)))
                   else if t then
                     modify (ksPSpace_update
                               (\<lambda>ps. ps (p && ~~ mask tcbBlockSizeBits \<mapsto>
                                           KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (K v)
                                                (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits)))))))))
                   else fail od" apply (clarsimp simp: setCTE_def setObject_def split_def
                        fun_eq_iff exec_gets) apply (case_tac "real_cte_at' p x") apply (clarsimp simp: obj_at'_def projectKOs lookupAround2_known1
                         assert_opt_def alignCheck_assert objBits_simps'
                         magnitudeCheck_assert2 updateObject_cte) apply (simp add: simpler_modify_def) apply (simp split: if_split, intro conjI impI) apply (clarsimp simp: obj_at'_def projectKOs) apply (subgoal_tac "p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1") apply (subgoal_tac "fst (lookupAround2 p (ksPSpace x))
                          = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)") apply (simp add: assert_opt_def) apply (subst updateObject_cte_tcb) apply (fastforce simp add: subtract_mask) apply (simp add: assert_opt_def alignCheck_assert bind_assoc
                      magnitudeCheck_assert
                      is_aligned_neg_mask2 objBits_def) apply (rule ps_clear_lookupAround2, assumption+) apply (rule word_and_le2) apply (simp add: objBits_simps mask_def field_simps) apply (simp add: simpler_modify_def cong: option.case_cong if_cong) apply (rule kernel_state.fold_congs[OF refl refl]) apply (clarsimp simp: projectKO_opt_tcb cong: if_cong) apply (clarsimp simp: lookupAround2_char1 word_and_le2) apply (rule ccontr, clarsimp) apply (erule(2) ps_clearD) apply (simp add: objBits_simps mask_def field_simps) apply (rule tcb_cte_cases_in_range2) apply (simp add: subtract_mask) apply simp apply (clarsimp simp: assert_opt_def split: option.split) apply (rule trans [OF bind_apply_cong[OF _ refl] fun_cong[OF fail_bind]]) apply (simp add: fail_def prod_eq_iff) apply (rule context_conjI) apply (rule ccontr, clarsimp elim!: nonemptyE) apply (frule(1) updateObject_cte_is_tcb_or_cte[OF _ refl]) apply (erule disjE) apply clarsimp apply (frule(1) tcb_cte_cases_aligned_helpers) apply (clarsimp simp: field_simps) apply (clarsimp simp: lookupAround2_char1 obj_at'_def projectKOs
                          objBits_simps) apply (clarsimp simp: obj_at'_def lookupAround2_char1
                         objBits_simps' projectKOs cte_level_bits_def) apply (erule empty_failD[OF empty_fail_updateObject_cte]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setCTE p v = do c <- gets (real_cte_at' p);
t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and K (p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases));
if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if t then modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (K v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. real_cte_at' p x \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x))
 2. \<And>x. \<not> real_cte_at' p x \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x)) proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>ksPSpace x p = Some (KOCTE obj); is_aligned p 4; ps_clear p 4 x\<rbrakk> \<Longrightarrow> ((\<exists>ko. ksPSpace x (p && ~~ mask 9) = Some ko \<and> is_aligned (p && ~~ mask 9) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ps_clear (p && ~~ mask 9) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) x) \<and> p && mask 9 \<in> dom tcb_cte_cases \<longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> KOCTE v))) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (((\<exists>ko. ksPSpace x (p && ~~ mask 9) = Some ko \<and> is_aligned (p && ~~ mask 9) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ps_clear (p && ~~ mask 9) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) x) \<longrightarrow> p && mask 9 \<notin> dom tcb_cte_cases) \<longrightarrow> modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p \<mapsto> KOCTE v))) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x)
 2. \<And>x. \<not> real_cte_at' p x \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> real_cte_at' p x \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> (real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) x) \<and> (\<not> real_cte_at' p x \<longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (2 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> (do obj' <- updateObject v (KOTCB obj) p (p && ~~ mask tcbBlockSizeBits) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (5 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> tcb_cte_cases (p - (p && ~~ mask tcbBlockSizeBits)) = Some (?accF51 x a b obj, ?updF51 x a b obj)
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> (do obj' <- do alignCheck (p && ~~ mask tcbBlockSizeBits) (objBits obj);
magnitudeCheck (p && ~~ mask tcbBlockSizeBits) (snd (lookupAround2 p (ksPSpace x))) (objBits obj);
return (KOTCB (?updF51 x a b obj (\<lambda>_. v) obj))
od;
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 4. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 5. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> (do obj' <- do alignCheck (p && ~~ mask tcbBlockSizeBits) (objBits obj);
magnitudeCheck (p && ~~ mask tcbBlockSizeBits) (snd (lookupAround2 p (ksPSpace x))) (objBits obj);
return (KOTCB (b (\<lambda>_. v) obj))
od;
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> obj')))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> (do y <- assert (case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> z - (p && ~~ mask tcbBlockSizeBits));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>_. v) obj))))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (6 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> p
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO (KOTCB obj) - 1
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - (p && ~~ mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> (do y <- assert (case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> z - (p && ~~ mask tcbBlockSizeBits));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) obj))))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 4. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 5. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 6. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (5 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO (KOTCB obj) - 1
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - (p && ~~ mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> (do y <- assert (case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> z - (p && ~~ mask tcbBlockSizeBits));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) obj))))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 4. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 5. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - (p && ~~ mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> (do y <- assert (case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> z - (p && ~~ mask tcbBlockSizeBits));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) obj))))
od) x = modify (ksPSpace_update (\<lambda>ps. ps(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - (p && ~~ mask tcbBlockSizeBits)\<rbrakk> \<Longrightarrow> x\<lparr>ksPSpace := \<lambda>a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (b (\<lambda>a. v) obj)) else ksPSpace x a\<rparr> = ksPSpace_update (\<lambda>ps a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))) else ps a) x
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (4 subgoals):
 1. \<And>x a b obj va. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj); case snd (lookupAround2 p (ksPSpace x)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - (p && ~~ mask tcbBlockSizeBits); ksPSpace x = va\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (b (\<lambda>a. v) obj)) else ksPSpace x a) = (\<lambda>a. if a = p && ~~ mask tcbBlockSizeBits then Some (KOTCB (b (\<lambda>a. v) (the (projectKO_opt (the (va (p && ~~ mask tcbBlockSizeBits))))))) else va a)
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 3. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj z. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; p && ~~ mask tcbBlockSizeBits < z; z \<le> p\<rbrakk> \<Longrightarrow> ksPSpace x z = None
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj z y. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x; p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; p && ~~ mask tcbBlockSizeBits < z; z \<le> p; ksPSpace x z = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj z y. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1; p && ~~ mask tcbBlockSizeBits < z; z \<le> p; ksPSpace x z = Some y\<rbrakk> \<Longrightarrow> z \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO (KOTCB obj) - 1
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (2 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 2. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (3 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> tcb_cte_cases (p - (p && ~~ mask tcbBlockSizeBits)) = Some (?v91 x a b obj)
 2. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits
 3. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (2 subgoals):
 1. \<And>x a b obj. \<lbrakk>\<forall>ko. is_aligned p (objBitsKO ko) \<longrightarrow> ksPSpace x p = Some ko \<longrightarrow> (\<forall>obj. ko \<noteq> KOCTE obj) \<or> \<not> ps_clear p (objBitsKO ko) x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace x (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); is_aligned (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)); ps_clear (p && ~~ mask tcbBlockSizeBits) (objBitsKO (KOTCB obj)) x\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits
 2. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (do pa <- assert_opt (fst (lookupAround2 p (ksPSpace x)));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(fst pa \<mapsto> obj')))
od) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> (do obj' <- updateObject v b p a (snd (lookupAround2 p (ksPSpace x)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(a \<mapsto> obj')))
od) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x = fail x proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {} \<and> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b)\<rbrakk> \<Longrightarrow> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}
 2. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); (\<exists>tcb getF setF. b = KOTCB tcb \<and> ba = x \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> aa = KOTCB (setF (\<lambda>x. v) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits x) \<or> (\<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>tcb getF setF. b = KOTCB tcb \<and> ba = x \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> aa = KOTCB (setF (\<lambda>x. v) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits x\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a tcb getF setF. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, KOTCB tcb); (KOTCB (setF (\<lambda>x. v) tcb), x) \<in> fst (updateObject v (KOTCB tcb) p a (snd (lookupAround2 p (ksPSpace x))) x); tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits x\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a tcb getF setF. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, KOTCB tcb); (KOTCB (setF (\<lambda>x. v) tcb), x) \<in> fst (updateObject v (KOTCB tcb) p a (snd (lookupAround2 p (ksPSpace x))) x); tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits x; a + (p - a) && mask tcbBlockSizeBits = p - a \<and> a + (p - a) && ~~ mask tcbBlockSizeBits = a\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (3 subgoals):
 1. \<And>x tcb getF setF. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (p && ~~ mask tcbBlockSizeBits, KOTCB tcb); (KOTCB (setF (\<lambda>x. v) tcb), x) \<in> fst (updateObject v (KOTCB tcb) p (p && ~~ mask tcbBlockSizeBits) (snd (lookupAround2 p (ksPSpace x))) x); tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (getF, setF); ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits x; (p && mask tcbBlockSizeBits) + (p && ~~ mask tcbBlockSizeBits) = p\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (2 subgoals):
 1. \<And>x a b aa ba. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); (aa, ba) \<in> fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x); \<exists>cte'. b = KOCTE cte' \<and> aa = KOCTE v \<and> ba = x \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits x\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>\<not> real_cte_at' p x; tcb_at' (p && ~~ mask tcbBlockSizeBits) x \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; fst (lookupAround2 p (ksPSpace x)) = Some (a, b); fst (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) = {}\<rbrakk> \<Longrightarrow> snd (updateObject v b p a (snd (lookupAround2 p (ksPSpace x))) x) proof (prove)
goal:
No subgoals!