theory Tcb_DR

lemma invoke_tcb_corres_write_regs:
  "\<lbrakk> t' = tcb_invocation.WriteRegisters obj_id resume data flags;
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def arch_get_sanitise_register_info_def
                        arch_post_modify_registers_def) apply (rule corres_symb_exec_r) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule corrupt_tcb_intent_as_user_corres) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'=dc]) apply (clarsimp simp: when_def) apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def]) apply (rule corres_split_noop_rhs[OF corres_trivial]) apply (clarsimp simp: when_def) apply (rule reschedule_required_dcorres[THEN corres_trivial]) apply simp apply wp apply (clarsimp simp: when_def) apply (wpsimp wp: when_wp)+ apply (wp wp_post_taut | simp add:invs_def valid_state_def | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (do y <- corrupt_tcb_intent obj_id;
when resume (Tcb_D.restart obj_id)
od) (do self <- gets cur_thread;
y <- as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od);
y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od) proof (prove)
goal (4 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'1 self) (do y <- corrupt_tcb_intent obj_id;
when resume (Tcb_D.restart obj_id)
od) (do y <- as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od);
y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od)
 2. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> dcorres dc (?Q6 self) (?Q'6 self) (do y <- corrupt_tcb_intent obj_id;
when resume (Tcb_D.restart obj_id)
od) (do y <- as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od);
y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od)
 2. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ?Q6 self s
 3. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> ?Q'6 self s
 4. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (9 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> dcorres dc (?P10 self) (?P'10 self) (corrupt_tcb_intent obj_id) (as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od))
 2. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R10 self y) (?R'10 self ya) (when resume (Tcb_D.restart obj_id)) (do y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od)
 3. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>?R10 self\<rbrace>
 4. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>?R'10 self\<rbrace>
 5. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> (?P10 self and ?Q10 self) s
 6. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (?P'10 self and ?Q'10 self) s
 7. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (8 subgoals):
 1. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R10 self y) (?R'10 self ya) (when resume (Tcb_D.restart obj_id)) (do y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od)
 2. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>?R10 self\<rbrace>
 3. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>?R'10 self\<rbrace>
 4. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 5. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 6. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (8 subgoals):
 1. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R10 self y) (?R'10 self ya) (when resume (Tcb_D.restart obj_id) >>= return) (do y <- when resume (Tcb_A.restart obj_id);
y <- when (obj_id = self) reschedule_required;
return []
od)
 2. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>?R10 self\<rbrace>
 3. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>?R'10 self\<rbrace>
 4. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 5. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 6. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (11 subgoals):
 1. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?P19 self y) (?P'21 self ya) (when resume (Tcb_D.restart obj_id)) (when resume (Tcb_A.restart obj_id))
 2. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R18 self y ya x) (?R'18 self y ya yb) (return x) (do y <- when (obj_id = self) reschedule_required;
return []
od)
 3. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>?R18 self y ya\<rbrace>
 4. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>?R'18 self y ya\<rbrace>
 5. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. ?P19 self y and ?Q20 self y\<rbrace>
 6. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. ?P'21 self ya and ?Q'22 self ya\<rbrace>
 7. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 8. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id True data flags; t = cdl_tcb_invocation.WriteRegisters obj_id True [0] 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (?P19 self ()) (?P'21 self ()) (Tcb_D.restart obj_id) (Tcb_A.restart obj_id)
 2. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R18 self y ya x) (?R'18 self y ya yb) (return x) (do y <- when (obj_id = self) reschedule_required;
return []
od)
 3. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>?R18 self y ya\<rbrace>
 4. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>?R'18 self y ya\<rbrace>
 5. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. ?P19 self y and ?Q20 self y\<rbrace>
 6. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. ?P'21 self ya and ?Q'22 self ya\<rbrace>
 7. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 8. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R18 self y ya x) (?R'18 self y ya yb) (return x) (do y <- when (obj_id = self) reschedule_required;
return []
od)
 2. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>?R18 self y ya\<rbrace>
 3. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>?R'18 self y ya\<rbrace>
 4. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 5. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 6. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 7. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 8. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (12 subgoals):
 1. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when (obj_id = self) reschedule_required)
 2. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R39 self y ya x) (?R'37 self y ya x yb) (return x) (return [])
 3. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 self y ya yb\<rbrace> when (obj_id = self) reschedule_required \<lbrace>\<lambda>xa. ?R'37 self y ya x yb\<rbrace>
 4. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R39 self y ya x\<rbrace>
 5. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q'40 self y ya yb\<rbrace>
 6. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 7. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 8. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 9. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 10. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) reschedule_required
 2. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R39 self y ya x) (?R'37 self y ya x yb) (return x) (return [])
 3. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 self y ya yb\<rbrace> when (obj_id = self) reschedule_required \<lbrace>\<lambda>xa. ?R'37 self y ya x yb\<rbrace>
 4. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R39 self y ya x\<rbrace>
 5. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q'40 self y ya yb\<rbrace>
 6. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 7. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 8. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 9. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 10. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> dcorres dc (?R39 self y ya x) (?R'37 self y ya x yb) (return x) (return [])
 2. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 self y ya yb\<rbrace> when (obj_id = self) reschedule_required \<lbrace>\<lambda>xa. ?R'37 self y ya x yb\<rbrace>
 3. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R39 self y ya x\<rbrace>
 4. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q'40 self y ya yb\<rbrace>
 5. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 6. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 7. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 8. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>self y ya x yb. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya; dc x yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'40 self y ya yb\<rbrace> when (obj_id = self) reschedule_required \<lbrace>\<lambda>xa. ?R'37 self y ya x yb\<rbrace>
 2. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R39 self y ya x\<rbrace>
 3. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q'40 self y ya yb\<rbrace>
 4. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 5. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 6. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 7. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 8. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (9 subgoals):
 1. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 self y\<rbrace> when resume (Tcb_D.restart obj_id) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R39 self y ya x\<rbrace>
 2. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 4. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 5. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 6. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 7. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (9 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> (resume \<longrightarrow> \<lbrace>?Q20 self ()\<rbrace> Tcb_D.restart obj_id \<lbrace>?R39 self () ()\<rbrace>) \<and> (\<not> resume \<longrightarrow> \<lbrace>?Q20 self ()\<rbrace> return () \<lbrace>?R39 self () ()\<rbrace>)
 2. \<And>self y ya. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 self ya\<rbrace> when resume (Tcb_A.restart obj_id) \<lbrace>\<lambda>yb. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 self\<rbrace> corrupt_tcb_intent obj_id \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q20 self y\<rbrace>
 4. \<And>self. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 self\<rbrace> as_user obj_id (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register False r v)) (frameRegisters @ gpRegisters) data;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>ya. invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs and ?Q'22 self ya\<rbrace>
 5. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 self) s
 6. \<And>self s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 self s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id and valid_etcbs and ?Q'10 self) s
 7. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; ?Q'1 x xa\<rbrakk> \<Longrightarrow> valid_idle xa \<and> not_idle_thread obj_id xa \<and> valid_etcbs xa \<and> invs xa \<and> tcb_at obj_id xa \<and> not_idle_thread obj_id xa \<and> valid_etcbs xa
 2. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0\<rbrakk> \<Longrightarrow> \<lbrace>invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'1\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.WriteRegisters obj_id resume data flags; t = cdl_tcb_invocation.WriteRegisters obj_id resume [0] 0; False\<rbrakk> \<Longrightarrow> no_fail (invs and not_idle_thread obj_id and tcb_at obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal:
No subgoals!