theory Tcb_R

lemma invokeTCB_ReadRegisters_corres:
  "corres (dc \<oplus> (=))
        (einvs  and tcb_at src and ex_nonz_cap_to src)
        (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src)
        (invoke_tcb (tcb_invocation.ReadRegisters src susp n arch))
        (invokeTCB (tcbinvocation.ReadRegisters src susp n arch'))" apply (simp add: invokeTCB_def performTransfer_def genericTake_def
                   frame_registers_def gp_registers_def
                   frameRegisters_def gpRegisters_def) apply (rule corres_guard_imp) apply (rule corres_split_nor) apply (rule corres_when[OF refl]) apply (rule suspend_corres) apply (rule corres_split[OF getCurThread_corres]) apply (simp add: liftM_def[symmetric]) apply (rule asUser_corres) apply (rule corres_Id) apply simp apply simp apply (rule no_fail_mapM) apply (simp add: no_fail_getRegister) apply wp+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
                  dest!: idle_no_ex_cap) apply (clarsimp simp: invs'_def valid_state'_def dest!: global'_no_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> (=)) (einvs and tcb_at src and ex_nonz_cap_to src) (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) (invoke_tcb (tcb_invocation.ReadRegisters src susp n arch)) (invokeTCB (tcbinvocation.ReadRegisters src susp n arch')) proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and tcb_at src and ex_nonz_cap_to src) (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) (do y <- when susp (IpcCancel_A.suspend src);
self <- gets cur_thread;
as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) (do y <- when susp (ThreadDecls_H.suspend src);
self <- getCurThread;
asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do y <- when susp (IpcCancel_A.suspend src);
self <- gets cur_thread;
as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) (do y <- when susp (ThreadDecls_H.suspend src);
self <- getCurThread;
asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od)
 2. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres dc ?P4 ?P'4 (when susp (IpcCancel_A.suspend src)) (when susp (ThreadDecls_H.suspend src))
 2. corres (=) ?R4 ?R'4 (do self <- gets cur_thread;
as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) (do self <- getCurThread;
asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od)
 3. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. ?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. ?R'4\<rbrace>
 5. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. corres dc ?P9 ?P'9 (IpcCancel_A.suspend src) (ThreadDecls_H.suspend src)
 2. corres (=) ?R4 ?R'4 (do self <- gets cur_thread;
as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) (do self <- getCurThread;
asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od)
 3. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. ?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. ?R'4\<rbrace>
 5. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> ?P9 x) and ?Q4) s
 6. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> ?P'9 x) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. corres (=) ?R4 ?R'4 (do self <- gets cur_thread;
as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od) (do self <- getCurThread;
asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
od)
 2. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. ?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. ?R'4\<rbrace>
 4. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 5. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R13 self) (?R'13 selfa) (as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))) (asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters)))
 2. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>?R13\<rbrace>
 3. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>?R'13\<rbrace>
 4. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 6. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>self. corres (=) (?R13 self) (?R'13 self) (as_user src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))) (asUser src (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters)))
 2. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>?R13\<rbrace>
 3. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>?R'13\<rbrace>
 4. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 6. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>self. corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters)) (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
 2. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 3. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 6. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>self. mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters) = mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters)
 2. \<And>self rv. rv = rv
 3. \<And>self. True \<Longrightarrow> no_fail (\<lambda>_. True) (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
 4. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 5. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 8. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 9. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>self rv. rv = rv
 2. \<And>self. True \<Longrightarrow> no_fail (\<lambda>_. True) (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
 3. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 4. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 7. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>self. True \<Longrightarrow> no_fail (\<lambda>_. True) (mapM getRegister (take (unat n) MachineExports.frameRegisters @ take (unat n - length MachineExports.frameRegisters) MachineExports.gpRegisters))
 2. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 3. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 6. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>self. True \<Longrightarrow> \<forall>x. no_fail (\<lambda>_. True) (getRegister x)
 2. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 3. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 6. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q13\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at src and invs\<rbrace>
 2. \<lbrace>?Q'13\<rbrace> getCurThread \<lbrace>\<lambda>self. tcb_at' src and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> when susp (IpcCancel_A.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q13\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> when susp (ThreadDecls_H.suspend src) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'13\<rbrace>
 5. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and ?Q4) s
 6. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and tcb_at src and ex_nonz_cap_to src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (einvs and tcb_at src) x) and (\<lambda>s. True \<and> (if susp then \<lambda>s. tcb_at src s \<and> (invs and tcb_at src and (\<lambda>s. src \<noteq> idle_thread s)) s else (\<lambda>s. tcb_at src s \<and> invs s)) s)) s
 2. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and (\<lambda>s. True \<and> (if susp then \<lambda>s. tcb_at' src s \<and> (invs' and sch_act_simple and tcb_at' src and (\<lambda>s. src \<noteq> ksIdleThread s)) s else (\<lambda>s. tcb_at' src s \<and> invs' s)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src) s \<Longrightarrow> ((\<lambda>x. susp \<longrightarrow> (invs' and tcb_at' src) x) and (\<lambda>s. True \<and> (if susp then \<lambda>s. tcb_at' src s \<and> (invs' and sch_act_simple and tcb_at' src and (\<lambda>s. src \<noteq> ksIdleThread s)) s else (\<lambda>s. tcb_at' src s \<and> invs' s)) s)) s proof (prove)
goal:
No subgoals!