theory IsolatedThreadAction

lemma copy_register_isolate:
  "\<lbrakk> inj idx; idx x = src; idx y = dest \<rbrakk> \<Longrightarrow>
  monadic_rewrite False True
      (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
           (do v \<leftarrow> asUser src (getRegister r);
                   asUser dest (setRegister r' (rf v)) od)
           (isolate_thread_actions idx (return ())
                 (copy_register_tsrs x y r r' rf) id)" supply if_split[split del] apply (simp add: asUser_def split_def bind_assoc
                   getRegister_def setRegister_def
                   select_f_returns isolate_thread_actions_def
                   getSchedulerAction_def) apply (simp add: threadGet_def liftM_def getObject_get_assert
                   bind_assoc threadSet_def
                   setObject_modify_assert) apply (clarsimp simp: monadic_rewrite_def exec_gets
                        exec_modify tcb_at_KOTCB_upd) apply (clarsimp simp: simpler_modify_def
                intro!: kernel_state.fold_congs[OF refl refl]) apply (clarsimp simp: copy_register_tsrs_def o_def
                        partial_overwrite_fun_upd
                        partial_overwrite_get_tcb_state_regs) apply (frule_tac x=x in spec, drule_tac x=y in spec) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
                  cong: if_cong) apply (case_tac obj, case_tac obja) apply (simp add: projectKO_opt_tcb put_tcb_state_regs_def
                   put_tcb_state_regs_tcb_def get_tcb_state_regs_def
             cong: if_cong) apply (auto simp: fun_eq_iff split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx x = src; idx y = dest\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do v <- asUser src (getRegister r);
asUser dest (setRegister r' (rf v))
od) (isolate_thread_actions idx (return ()) (copy_register_tsrs x y r r' rf) id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx x = src; idx y = dest\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do v <- asUser src (getRegister r);
asUser dest (setRegister r' (rf v))
od) (isolate_thread_actions idx (return ()) (copy_register_tsrs x y r r' rf) id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx x = src; idx y = dest\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do uc <- threadGet (atcbContextGet \<circ> tcbArch) src;
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb) src;
uca <- threadGet (atcbContextGet \<circ> tcbArch) dest;
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (uca(r' := rf (uc r))) (tcbArch tcb)) tcb) dest
od) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- gets ksSchedulerAction;
modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (copy_register_tsrs x y r r' rf tcbs)) (s\<lparr>ksSchedulerAction := sa\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx x = src; idx y = dest\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do v <- gets (tcb_at' src);
y <- assert v;
x <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) src \<circ> ksPSpace);
v <- gets (tcb_at' src);
y <- assert v;
tcb <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) src \<circ> ksPSpace);
f <- gets (tcb_at' src);
y <- assert f;
y <- modify (ksPSpace_update (\<lambda>ps. ps(src \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch x)) (tcbArch tcb)) tcb))));
v <- gets (tcb_at' dest);
y <- assert v;
xa <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) dest \<circ> ksPSpace);
v <- gets (tcb_at' dest);
y <- assert v;
tcb <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) dest \<circ> ksPSpace);
f <- gets (tcb_at' dest);
y <- assert f;
modify (ksPSpace_update (\<lambda>ps. ps(dest \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch xa))(r' := rf (atcbContextGet (tcbArch x) r))) (tcbArch tcb)) tcb))))
od) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- gets ksSchedulerAction;
modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (copy_register_tsrs x y r r' rf tcbs)) (s\<lparr>ksSchedulerAction := sa\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; src = idx x; dest = idx y; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))))) (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x)))))))) s) = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (copy_register_tsrs x y r r' rf (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; src = idx x; dest = idx y; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x)))))), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) = partial_overwrite idx (copy_register_tsrs x y r r' rf (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (ksPSpace s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; src = idx x; dest = idx y; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x)))))), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) = (ksPSpace s)(idx y := put_tcb_state_regs (TCBStateRegs (tsrState (get_tcb_state_regs (ksPSpace s (idx y)))) ((tsrContext (get_tcb_state_regs (ksPSpace s (idx y))))(r' := rf (tsrContext (get_tcb_state_regs (ksPSpace s (idx x))) r)))) (ksPSpace s (idx y))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; src = idx x; dest = idx y; tcb_at' (idx x) s; tcb_at' (idx y) s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x)))))), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (the (ksPSpace s (idx x)))))) (the (projectKO_opt (the (ksPSpace s (idx x))))))) else ksPSpace s (idx y))))))) = (ksPSpace s)(idx y := put_tcb_state_regs (TCBStateRegs (tsrState (get_tcb_state_regs (ksPSpace s (idx y)))) ((tsrContext (get_tcb_state_regs (ksPSpace s (idx y))))(r' := rf (tsrContext (get_tcb_state_regs (ksPSpace s (idx x))) r)))) (ksPSpace s (idx y))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj obja. \<lbrakk>inj idx; src = idx x; dest = idx y; ksPSpace s (idx x) = Some (KOTCB obj); ksPSpace s (idx y) = Some (KOTCB obja); is_aligned (idx x) tcbBlockSizeBits; is_aligned (idx y) tcbBlockSizeBits; ps_clear (idx x) tcbBlockSizeBits s; ps_clear (idx y) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj)))), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (KOTCB obj)))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja))))))) = (ksPSpace s)(idx y := put_tcb_state_regs (TCBStateRegs (tsrState (get_tcb_state_regs (Some (KOTCB obja)))) ((tsrContext (get_tcb_state_regs (Some (KOTCB obja))))(r' := rf (tsrContext (get_tcb_state_regs (Some (KOTCB obj))) r)))) (Some (KOTCB obja))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj obja x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a. \<lbrakk>inj idx; src = idx x; dest = idx y; ksPSpace s (idx x) = Some (KOTCB obj); ksPSpace s (idx y) = Some (KOTCB obja); is_aligned (idx x) tcbBlockSizeBits; is_aligned (idx y) tcbBlockSizeBits; ps_clear (idx x) tcbBlockSizeBits s; ps_clear (idx y) tcbBlockSizeBits s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; obja = Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj)))), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja)))))))(r' := rf (atcbContextGet (tcbArch (the (projectKO_opt (KOTCB obj)))) r))) (tcbArch (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja))))))) (the (projectKO_opt (the (if idx y = idx x then Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch (the (projectKO_opt (KOTCB obj)))) (the (projectKO_opt (KOTCB obj))))) else Some (KOTCB obja))))))) = (ksPSpace s)(idx y := put_tcb_state_regs (TCBStateRegs (tsrState (get_tcb_state_regs (Some (KOTCB obja)))) ((tsrContext (get_tcb_state_regs (Some (KOTCB obja))))(r' := rf (tsrContext (get_tcb_state_regs (Some (KOTCB obj))) r)))) (Some (KOTCB obja))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj obja x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a. \<lbrakk>inj idx; src = idx x; dest = idx y; ksPSpace s (idx x) = Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)); ksPSpace s (idx y) = Some (KOTCB (Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a)); is_aligned (idx x) tcbBlockSizeBits; is_aligned (idx y) tcbBlockSizeBits; ps_clear (idx x) tcbBlockSizeBits s; ps_clear (idx y) tcbBlockSizeBits s; obj = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16; obja = Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx x \<mapsto> KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16), idx y \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch (the (case the (if idx y = idx x then Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) else Some (KOTCB (Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a))) of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None))))(r' := rf (atcbContextGet x16 r))) (tcbArch (the (case the (if idx y = idx x then Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) else Some (KOTCB (Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a))) of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None)))) (the (case the (if idx y = idx x then Some (KOTCB (Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)) else Some (KOTCB (Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a x16a))) of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None)))) = (ksPSpace s)(idx y \<mapsto> KOTCB (Thread x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a (atcbContextSet ((atcbContextGet x16a)(r' := rf (atcbContextGet x16 r))) x16a))) proof (prove)
goal:
No subgoals!