theory IsolatedThreadAction

lemma setCTE_isolatable:
  "thread_actions_isolatable idx (setCTE p v)" supply if_split[split del] apply (simp add: setCTE_assert_modify) apply (clarsimp simp: thread_actions_isolatable_def
                        monadic_rewrite_def fun_eq_iff
                        liftM_def exec_gets
                        isolate_thread_actions_def
                        bind_assoc exec_gets getSchedulerAction_def
                        bind_select_f_bind[symmetric]
                        obj_at_partial_overwrite_If
                        obj_at_partial_overwrite_id2
                  cong: if_cong) apply (case_tac "p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases") apply clarsimp apply (frule_tac x=x in spec, erule obj_atE') apply (subgoal_tac "\<not> real_cte_at' p s") apply (clarsimp simp: select_f_returns select_f_asserts split: if_split) apply (clarsimp simp: o_def simpler_modify_def partial_overwrite_fun_upd2) apply (rule kernel_state.fold_congs[OF refl refl]) apply (rule ext) apply (clarsimp simp: partial_overwrite_get_tcb_state_regs
                   split: if_split) apply (clarsimp simp: projectKOs get_tcb_state_regs_def
                          put_tcb_state_regs_def put_tcb_state_regs_tcb_def
                          partial_overwrite_def
                   split: tcb_state_regs.split) apply (case_tac obj, simp add: projectKO_opt_tcb) apply (simp add: tcb_cte_cases_def split: if_split_asm) apply (drule_tac x=x in spec) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps subtract_mask(2) [symmetric]) apply (erule notE[rotated], erule (3) tcb_ctes_clear[rotated]) apply (simp add: select_f_returns select_f_asserts split: if_split) apply (intro conjI impI) apply (clarsimp simp: simpler_modify_def fun_eq_iff partial_overwrite_fun_upd2
                  intro!: kernel_state.fold_congs[OF refl refl]) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (erule notE[rotated], rule tcb_ctes_clear[rotated 2], assumption+) apply (fastforce simp add: subtract_mask) apply simp apply (clarsimp simp: simpler_modify_def
                         partial_overwrite_fun_upd2 o_def
                         partial_overwrite_get_tcb_state_regs
                 intro!: kernel_state.fold_congs[OF refl refl]
                  split: if_split) apply (simp add: partial_overwrite_def) apply (subgoal_tac "p \<notin> range idx") apply (clarsimp simp: simpler_modify_def
                         partial_overwrite_fun_upd2 o_def
                         partial_overwrite_get_tcb_state_regs
                 intro!: kernel_state.fold_congs[OF refl refl]) apply clarsimp apply (drule_tac x=x in spec) apply (clarsimp simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setCTE p v) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setCTE p v) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do c <- gets (real_cte_at' p);
t <- gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) and (\<lambda>y. 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))) (\<lambda>y. v) (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) else fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))))) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ps (idx x)))))))) s = ksPSpace_update (\<lambda>xa. (partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) xa)(idx x := put_tcb_state_regs (get_tcb_state_regs (Some ko)) (Some (KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) xa (idx x)))))))))) s
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj va. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s; ksPSpace s = va\<rbrakk> \<Longrightarrow> va(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (va (idx x))))))) = (partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) va)(idx x := put_tcb_state_regs (get_tcb_state_regs (Some ko)) (Some (KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) va (idx x)))))))))
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj va xa. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s; ksPSpace s = va\<rbrakk> \<Longrightarrow> (va(idx x \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (va (idx x)))))))) xa = ((partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) va)(idx x := put_tcb_state_regs (get_tcb_state_regs (Some ko)) (Some (KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) va (idx x)))))))))) xa
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; ps_clear (idx x) (objBitsKO ko) s; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> Some (KOTCB (b (\<lambda>y. v) (the (projectKO_opt ko)))) = put_tcb_state_regs (get_tcb_state_regs (Some ko)) (Some (KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) (idx x))))))))
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b obj x1 x2. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some (KOTCB obj); is_aligned (idx x) (objBitsKO (KOTCB obj)); ps_clear (idx x) (objBitsKO (KOTCB obj)) s; \<not> real_cte_at' p s; undefined = TCBStateRegs x1 x2\<rbrakk> \<Longrightarrow> b (\<lambda>y. v) (the (projectKO_opt (KOTCB obj))) = tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch obj)) (tcbArch (b (\<lambda>y. v) (the (projectKO_opt (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch obj)) (tcbState_update (\<lambda>_. x1) obj)))))))) (tcbState_update (\<lambda>_. tcbState obj) (b (\<lambda>y. v) (the (projectKO_opt (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch obj)) (tcbState_update (\<lambda>_. x1) obj)))))))
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s x a b obj x1 x2 x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some (KOTCB (Thread x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); is_aligned (idx x) (objBitsKO (KOTCB (Thread x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))); ps_clear (idx x) (objBitsKO (KOTCB (Thread x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16))) s; \<not> real_cte_at' p s; undefined = TCBStateRegs x1 x2; obj = Thread x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> b (\<lambda>y. v) (Thread x1a x2a x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) = tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet x16) (tcbArch (b (\<lambda>y. v) (Thread x1a x2a x3 x4 x5 x6 x1 x8 x9 x10 x11 x12 x13 x14 x15 (atcbContextSet x2 x16))))) (tcbState_update (\<lambda>_. x7) (b (\<lambda>y. v) (Thread x1a x2a x3 x4 x5 x6 x1 x8 x9 x10 x11 x12 x13 x14 x15 (atcbContextSet x2 x16))))
 2. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b ko obj. \<lbrakk>inj idx; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (idx x) = Some ko; is_aligned (idx x) (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear (idx x) (objBitsKO ko) s; tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> \<not> real_cte_at' p s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b obj obja. \<lbrakk>inj idx; p && ~~ mask tcbBlockSizeBits = idx x; tcb_cte_cases (p - idx x) = Some (a, b); ksPSpace s (idx x) = Some (KOTCB obj); ps_clear (idx x) tcbBlockSizeBits s; is_aligned (idx x) tcbBlockSizeBits; is_aligned p cteSizeBits; ksPSpace s p = Some (KOCTE obja); ps_clear p cteSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; \<not> (p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)\<rbrakk> \<Longrightarrow> (if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) s = (do (rv, s') <- select_f ((if real_cte_at' p s then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) else if tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then 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))))))))) else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> (tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<longrightarrow> (real_cte_at' p s \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s) \<and> (\<not> real_cte_at' p s \<longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s)) \<and> ((tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases) \<longrightarrow> real_cte_at' p s \<longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; real_cte_at' p s; tcb_at' (p && ~~ mask tcbBlockSizeBits) s; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> (if x = p then Some (KOCTE v) else ksPSpace s x) = (if x = p then if p \<in> range idx then put_tcb_state_regs (get_tcb_state_regs (ksPSpace s (idx (inv idx p)))) (Some (KOCTE v)) else Some (KOCTE v) else partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) (ksPSpace s) x)
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b x obj obja. \<lbrakk>inj idx; \<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (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 (idx x) (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) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s p = Some (KOCTE obj); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obja); is_aligned p cteSizeBits; ps_clear p cteSizeBits s; ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (if x = p then Some (KOCTE v) else ksPSpace s x) = (if x = p then if p \<in> range idx then put_tcb_state_regs (get_tcb_state_regs (ksPSpace s (idx (inv idx p)))) (Some (KOCTE v)) else Some (KOCTE v) else partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) (ksPSpace s) x)
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (4 subgoals):
 1. \<And>s a b x obj obja. \<lbrakk>inj idx; \<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (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 (idx x) (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) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obja); is_aligned p cteSizeBits; ps_clear p cteSizeBits s; ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (p - (p && ~~ mask tcbBlockSizeBits)) = Some (?getF192 s a b x obj obja, ?setF192 s a b x obj obja)
 2. \<And>s a b x obj obja. \<lbrakk>inj idx; \<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (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 (idx x) (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) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obja); is_aligned p cteSizeBits; ps_clear p cteSizeBits s; ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 4. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b x obj obja. \<lbrakk>inj idx; \<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (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 (idx x) (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) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obja); is_aligned p cteSizeBits; ps_clear p cteSizeBits s; ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> is_aligned (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases; \<not> real_cte_at' p s\<rbrakk> \<Longrightarrow> 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))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<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)))))))) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<notin> range idx; \<not> real_cte_at' p s; tcb_at' (p && ~~ mask tcbBlockSizeBits) s; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)\<rbrakk> \<Longrightarrow> (ksPSpace s)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (ksPSpace s (p && ~~ mask tcbBlockSizeBits))))))) = (ksPSpace s)(p && ~~ mask tcbBlockSizeBits \<mapsto> KOTCB (b (\<lambda>y. v) (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) (p && ~~ mask tcbBlockSizeBits)))))))
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s; p \<notin> range idx\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> ((\<lambda>ps. ps(p \<mapsto> KOCTE v)) \<circ> partial_overwrite idx (\<lambda>y. undefined))) s) s
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> p \<notin> range idx proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; p && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (p && ~~ mask tcbBlockSizeBits) s \<longrightarrow> p && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' p s\<rbrakk> \<Longrightarrow> p \<notin> range idx proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; idx x && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> idx x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (idx x && ~~ mask tcbBlockSizeBits) s \<longrightarrow> idx x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' (idx x) s; p = idx x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>inj idx; idx x && ~~ mask tcbBlockSizeBits \<in> range idx \<longrightarrow> idx x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; tcb_at' (idx x && ~~ mask tcbBlockSizeBits) s \<longrightarrow> idx x && mask tcbBlockSizeBits \<notin> dom tcb_cte_cases; real_cte_at' (idx x) s; p = idx x; tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!