theory Tcb_DR

lemma invoke_tcb_corres_read_regs:
  "\<lbrakk> t' = tcb_invocation.ReadRegisters obj_id resume data flags;
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and tcb_at obj_id and not_idle_thread 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) apply (case_tac "resume") apply (rule corres_alternate1) apply clarsimp apply (subst bind_return [symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule suspend_corres, simp) apply (rule corres_symb_exec_r) apply (rule dcorres_idempotent_as_user) apply (rule hoare_mapM_idempotent) apply wpsimp+ apply (rule corres_alternate2) apply (rule corres_symb_exec_r) apply (rule dcorres_idempotent_as_user) apply (rule hoare_mapM_idempotent) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread 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.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id) (do y <- IpcCancel_A.suspend obj_id;
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id >>= return) (do y <- IpcCancel_A.suspend obj_id;
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc ?Q8 ?Q'8 (Tcb_D.suspend obj_id >>= return) (do y <- IpcCancel_A.suspend obj_id;
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> ?Q8 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'8 s
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc ?P12 ?P'12 (Tcb_D.suspend obj_id) (IpcCancel_A.suspend obj_id)
 2. \<And>rv y. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; dc rv y\<rbrakk> \<Longrightarrow> dcorres dc (?R12 rv) (?R'12 y) (return rv) (do self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 3. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> Tcb_D.suspend obj_id \<lbrace>?R12\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12\<rbrace> IpcCancel_A.suspend obj_id \<lbrace>?R'12\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> (?P12 and ?Q12) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'12 and ?Q'12) s
 7. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (?R12 ()) (?R'12 ()) (return ()) (do self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od)
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> Tcb_D.suspend obj_id \<lbrace>?R12\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12\<rbrace> IpcCancel_A.suspend obj_id \<lbrace>?R'12\<rbrace>
 4. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 5. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at obj_id and invs and valid_etcbs and ?Q'12) s
 6. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (9 subgoals):
 1. \<And>self. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> dcorres dc (?R12 ()) (?Q'18 self) (return ()) (as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers)))
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?R'12 ()\<rbrace> gets cur_thread \<lbrace>?Q'18\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; ?R'12 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; False\<rbrakk> \<Longrightarrow> no_fail (?R'12 ()) (gets cur_thread)
 5. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> Tcb_D.suspend obj_id \<lbrace>?R12\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12\<rbrace> IpcCancel_A.suspend obj_id \<lbrace>?R'12\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at obj_id and invs and valid_etcbs and ?Q'12) s
 9. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (9 subgoals):
 1. \<And>self a. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = a\<rbrace> mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers) \<lbrace>\<lambda>_ s. s = a\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?R'12 ()\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at obj_id\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; ?R'12 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; False\<rbrakk> \<Longrightarrow> no_fail (?R'12 ()) (gets cur_thread)
 5. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> Tcb_D.suspend obj_id \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12\<rbrace> IpcCancel_A.suspend obj_id \<lbrace>?R'12\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at obj_id and invs and valid_etcbs and ?Q'12) s
 9. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (9 subgoals):
 1. \<And>self a aa R. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> getRegister aa \<lbrace>\<lambda>_. R\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?R'12 ()\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at obj_id\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; ?R'12 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; False\<rbrakk> \<Longrightarrow> no_fail (?R'12 ()) (gets cur_thread)
 5. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q12\<rbrace> Tcb_D.suspend obj_id \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume\<rbrakk> \<Longrightarrow> \<lbrace>?Q'12\<rbrace> IpcCancel_A.suspend obj_id \<lbrace>?R'12\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id True data flags; t = cdl_tcb_invocation.ReadRegisters obj_id True 0 0; resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at obj_id and invs and valid_etcbs and ?Q'12) s
 9. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id resume data flags; t = cdl_tcb_invocation.ReadRegisters obj_id resume 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do y <- when resume (IpcCancel_A.suspend obj_id);
self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (Tcb_D.suspend obj_id \<sqinter> return ()) (do self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (return ()) (do self <- gets cur_thread;
as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers))
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'58 rv) (return ()) (as_user obj_id (mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers)))
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> \<lbrace>invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'58\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; False\<rbrakk> \<Longrightarrow> no_fail (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (4 subgoals):
 1. \<And>rv a. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = a\<rbrace> mapM getRegister (take (unat data) frame_registers @ take (unat data - length frame_registers) gp_registers) \<lbrace>\<lambda>_ s. s = a\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> \<lbrace>invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>\<lambda>rv. tcb_at obj_id\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; False\<rbrakk> \<Longrightarrow> no_fail (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal (4 subgoals):
 1. \<And>rv a aa R. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> getRegister aa \<lbrace>\<lambda>_. R\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume\<rbrakk> \<Longrightarrow> \<lbrace>invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs\<rbrace> gets cur_thread \<lbrace>\<lambda>rv. tcb_at obj_id\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.ReadRegisters obj_id False data flags; t = cdl_tcb_invocation.ReadRegisters obj_id False 0 0; \<not> resume; False\<rbrakk> \<Longrightarrow> no_fail (invs and tcb_at obj_id and not_idle_thread obj_id and valid_etcbs) (gets cur_thread) proof (prove)
goal:
No subgoals!