theory Refine_C

lemma callKernel_withFastpath_corres_C:
  "corres_underlying rf_sr False True dc
           (all_invs' e)
           \<top>
           (callKernel e) (callKernel_withFastpath_C e)" using no_fail_callKernel [of e] callKernel_corres_C [of e] supply if_split[split del] apply (cases "e = SyscallEvent syscall.SysCall \<or>
            e = SyscallEvent syscall.SysReplyRecv") apply (simp_all add: callKernel_withFastpath_C_def
                  del: Collect_const cong: call_ignore_cong) apply (erule ccorres_corres_u[rotated]) apply (rule ccorres_guard_imp2) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_symb_exec_r)+ apply (rule ccorres_Cond_rhs) apply simp apply (ctac add: ccorres_get_registers[OF fastpath_call_ccorres_callKernel]) apply simp apply (ctac add: ccorres_get_registers[OF fastpath_reply_recv_ccorres_callKernel]) apply vcg apply (rule conseqPre, vcg, clarsimp) apply vcg apply (rule conseqPre, vcg, clarsimp) apply (clarsimp simp: all_invs'_def rf_sr_ksCurThread) apply (frule(1) obj_at_cslift_tcb[OF tcb_at_invs']) apply (clarsimp simp: typ_heap_simps' ct_in_state'_def
                        "StrictC'_register_defs" word_sle_def word_sless_def
                        st_tcb_at'_opeq_simp) apply (rule conjI, fastforce simp: st_tcb_at'_def) apply (auto elim!: pred_tcb'_weakenE cnode_caps_gsCNodes_from_sr[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_withFastpath_C e) proof (prove)
using this:
no_fail (all_invs' e) (callKernel e)
corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e)

goal (1 subgoal):
 1. corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_withFastpath_C e) proof (prove)
using this:
no_fail (all_invs' e) (callKernel e)
corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e)

goal (1 subgoal):
 1. corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_withFastpath_C e) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_fail (all_invs' e) (callKernel e); corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_withFastpath_C e)
 2. \<lbrakk>no_fail (all_invs' e) (callKernel e); corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); \<not> (e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv)\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_withFastpath_C e) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail (all_invs' e) (callKernel e); corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (exec_C \<Gamma> (\<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister);;
\<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
IF e = SyscallEvent syscall.SysCall THEN
  CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo)
ELSE
  CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo)
FI)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (all_invs' e) \<lbrace>True\<rbrace> [] (callKernel e) (\<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister);;
\<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
IF e = SyscallEvent syscall.SysCall THEN
  CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo)
ELSE
  CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo)
FI) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q6 ?Q'6 [] (callKernel e) (\<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister);;
\<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
IF e = SyscallEvent syscall.SysCall THEN
  CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo)
ELSE
  CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo)
FI)
 2. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q6 ?Q'6 [] (callKernel e) (\<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister);;
(\<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
IF e = SyscallEvent syscall.SysCall THEN
  CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo)
ELSE
  CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo)
FI))
 2. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q6 ?Q'15 [] (callKernel e) (IF e = SyscallEvent syscall.SysCall THEN
  CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo)
ELSE
  CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo)
FI)
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) ?Q'15
 3. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; ?Q6 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 4. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 5. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; ?Q6 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 6. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; e = SyscallEvent syscall.SysCall\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q19 ?S19 [] (callKernel e) (CALL fastpath_call_'proc(\<acute>cptr,\<acute>msgInfo))
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; e \<noteq> SyscallEvent syscall.SysCall\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?R19 ?T19 [] (callKernel e) (CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo))
 3. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. (e = SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?S19) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?T19)}
 4. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 5. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 6. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 7. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' (SyscallEvent syscall.SysCall)) (\<lambda>_. True) (callKernel (SyscallEvent syscall.SysCall)) (callKernel_C (SyscallEvent syscall.SysCall)); e = SyscallEvent syscall.SysCall\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q19 ?S19 [] (callKernel (SyscallEvent syscall.SysCall)) (CALL fastpath_call_'proc())
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; e \<noteq> SyscallEvent syscall.SysCall\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?R19 ?T19 [] (callKernel e) (CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo))
 3. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. (e = SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?S19) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?T19)}
 4. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 5. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 6. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 7. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> ?Q19 s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; e \<noteq> SyscallEvent syscall.SysCall\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?R19 ?T19 [] (callKernel e) (CALL fastpath_reply_recv_'proc(\<acute>cptr,\<acute>msgInfo))
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. (e = SyscallEvent syscall.SysCall \<longrightarrow> s \<in> {s. s \<in> {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]}}) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?T19)}
 3. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 4. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 5. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 6. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' (SyscallEvent syscall.SysReplyRecv)) (\<lambda>_. True) (callKernel (SyscallEvent syscall.SysReplyRecv)) (callKernel_C (SyscallEvent syscall.SysReplyRecv)); e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?R19 ?T19 [] (callKernel (SyscallEvent syscall.SysReplyRecv)) (CALL fastpath_reply_recv_'proc())
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. (e = SyscallEvent syscall.SysCall \<longrightarrow> s \<in> {s. s \<in> {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]}}) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> s \<in> ?T19)}
 3. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 4. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 5. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 6. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ?R19 s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'11 \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. (e = SyscallEvent syscall.SysCall \<longrightarrow> s \<in> {s. s \<in> {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]}}) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> s \<in> {s. s \<in> {s. \<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> msgInfo_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]}})}
 2. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'11 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 3. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) ?Q'11
 4. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 5. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>msgInfo :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s'. (s, s') \<in> rf_sr}
 2. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))}
 3. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 4. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q'6 \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> cptr_' s = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))}
 2. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'6 \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 3. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)) \<and> s' \<in> ?Q'6 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cptr :== CALL getRegister_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister) {s'. (s, s') \<in> rf_sr}
 2. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)) \<and> s' \<in> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>corres_underlying rf_sr False True dc (all_invs' e) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; all_invs' e s; s' \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> ((e = SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksDomainTime s \<noteq> 0))) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and ct_in_state' (\<lambda>_. True) and (invs' and ct_in_state' ((=) Structures_H.thread_state.Running) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)))) s)) \<and> s' \<in> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<and> (e = SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister])) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> (\<exists>v. cslift s (ksCurThread_' (globals s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]))} proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (e = SyscallEvent syscall.SysCall \<longrightarrow> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> ct_in_state' (\<lambda>_. True) s \<and> ct_in_state' ((=) Structures_H.thread_state.Running) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> ct_in_state' (\<lambda>_. True) s \<and> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister < 0x14 \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < 0x14 \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<exists>v. cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s') \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> True \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (e = SyscallEvent syscall.SysCall \<longrightarrow> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> ct_in_state' (\<lambda>_. True) s \<and> ct_in_state' ((=) Structures_H.thread_state.Running) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> ct_in_state' (\<lambda>_. True) s \<and> ct_in_state' ((=) Structures_H.thread_state.Running) s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister < 0x14 \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister < 0x14 \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<exists>v. cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some v \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.capRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.capRegister] \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister)] = registers_C (tcbContext_C (tcbArch_C v)).[unat Kernel_C.msgInfoRegister]) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa ko ko'. \<lbrakk>corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s') s') \<and> (st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s') s' \<or> st_tcb_at' idle' (ksCurThread s') s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<or> st_tcb_at' idle' (ksCurThread s) s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread; ko_at' ko (ksCurThread s) s; cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (e = SyscallEvent syscall.SysCall \<longrightarrow> st_tcb_at' (\<lambda>_. True) (ksCurThread s) s) \<and> (e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<and> st_tcb_at' (\<lambda>_. True) (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa ko ko'. \<lbrakk>corres_underlying rf_sr False True dc (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<and> 0 < domain_time s \<and> valid_domain_list s \<and> invs' s' \<and> vs_valid_duplicates' (ksPSpace s') \<and> (e \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s') s') \<and> (st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s') s' \<or> st_tcb_at' idle' (ksCurThread s') s') \<and> ksDomainTime s' \<noteq> 0 \<and> ksSchedulerAction s' = ResumeCurrentThread) (\<lambda>_. True) (callKernel e) (callKernel_C e); e = SyscallEvent syscall.SysCall \<or> e = SyscallEvent syscall.SysReplyRecv; (s, s') \<in> rf_sr; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched_2 (ready_queues sa) (ekheap sa) resume_cur_thread (cur_domain sa) (kheap sa) (cur_thread sa) (idle_thread sa); e \<noteq> Interrupt \<longrightarrow> ct_running sa; ct_running sa \<or> ct_idle sa; scheduler_action sa = resume_cur_thread; 0 < domain_time sa; valid_domain_list sa; invs' s; vs_valid_duplicates' (ksPSpace s); e \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<or> st_tcb_at' idle' (ksCurThread s) s; ksDomainTime s \<noteq> 0; ksSchedulerAction s = ResumeCurrentThread; ko_at' ko (ksCurThread s) s; cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> e \<noteq> SyscallEvent syscall.SysCall \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<and> st_tcb_at' (\<lambda>_. True) (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s \<and> cnode_caps_gsCNodes (only_cnode_caps (ctes_of s)) (gsCNodes s) proof (prove)
goal:
No subgoals!