theory Syscall_R

lemma handleEvent_corres:
  "corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
                       (\<lambda>s. scheduler_action s = resume_cur_thread))
                      (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
                       (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
                       (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
                      (handle_event event) (handleEvent event)"
  (is "?handleEvent_corres") proof - have hw:
    "\<And>isBlocking. corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread))
               (invs' and ct_running'
                      and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
               (handle_recv isBlocking) (handleRecv isBlocking)" apply (rule corres_guard_imp [OF handleRecv_isBlocking_corres]) apply (clarsimp simp: ct_in_state_def ct_in_state'_def
                     elim!: st_tcb_weakenE pred_tcb'_weakenE
                     dest!: ct_not_ksQ)+ done show ?thesis apply (case_tac event) apply (simp_all add: handleEvent_def) apply (rename_tac syscall) apply (case_tac syscall) apply (auto intro: corres_guard_imp[OF handleSend_corres]
                                     corres_guard_imp[OF hw]
                                     corres_guard_imp [OF handleReply_corres]
                                     corres_guard_imp[OF handleReply_handleRecv_corres]
                                     corres_guard_imp[OF handleCall_corres]
                                     corres_guard_imp[OF handleYield_corres]
                                     active_from_running active_from_running'
                              simp: simple_sane_strg)[8] apply (rule corres_underlying_split) apply (rule corres_guard_imp[OF getCurThread_corres], simp+) apply (rule handleFault_corres) apply simp apply (simp add: valid_fault_def) apply wp apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
                            simp: ct_in_state_def) apply wp apply (clarsimp) apply (frule(1) ct_not_ksQ) apply (auto simp: ct_in_state'_def sch_act_simple_def
                            sch_act_sane_def
                      elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1] apply (rule corres_underlying_split) apply (rule corres_guard_imp, rule getCurThread_corres, simp+) apply (rule handleFault_corres) apply (simp add: valid_fault_def) apply wp apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
                           simp: ct_in_state_def valid_fault_def) apply wp apply clarsimp apply (frule(1) ct_not_ksQ) apply (auto simp: ct_in_state'_def sch_act_simple_def
                           sch_act_sane_def
                     elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1] apply (rule corres_guard_imp) apply (rule corres_split_eqr[where R="\<lambda>rv. einvs"
                                       and R'="\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> R'' x s"
                                       for R'']) apply (rule corres_machine_op) apply (rule corres_Id, simp+) apply wp apply (case_tac rv, simp_all add: doMachineOp_return)[1] apply (rule handleInterrupt_corres) apply (wp hoare_vcg_all_lift
                     doMachineOp_getActiveIRQ_IRQ_active'
                    | simp
                    | simp add: imp_conjR | wp (once) hoare_drop_imps)+ apply force apply simp apply (simp add: invs'_def valid_state'_def) apply (rule_tac corres_underlying_split) apply (rule corres_guard_imp, rule getCurThread_corres, simp+) apply (rule corres_split_catch) apply (rule handleVMFault_corres) apply (erule handleFault_corres) apply (rule hoare_elim_pred_conjE2) apply (rule hoare_vcg_E_conj, rule valid_validE_E, wp) apply (wp handle_vm_fault_valid_fault) apply (rule hv_inv_ex') apply wp apply (clarsimp simp: simple_from_running tcb_at_invs) apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE simp: ct_in_state_def) apply wp apply (clarsimp) apply (frule(1) ct_not_ksQ) apply (fastforce simp: simple_sane_strg sch_act_simple_def ct_in_state'_def
                   elim: st_tcb_ex_cap'' pred_tcb'_weakenE) apply (rule corres_underlying_split) apply (rule corres_guard_imp[OF getCurThread_corres], simp+) apply (rule handleHypervisorFault_corres) apply (simp add: valid_fault_def) apply wp apply (fastforce elim!: st_tcb_ex_cap st_tcb_weakenE
                        simp: ct_in_state_def) apply wp apply (clarsimp) apply (frule(1) ct_not_ksQ) apply (auto simp: ct_in_state'_def sch_act_simple_def
                        sch_act_sane_def
                  elim: pred_tcb'_weakenE st_tcb_ex_cap'')[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event) proof (state)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event) proof (prove)
goal (1 subgoal):
 1. \<And>isBlocking. corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_recv isBlocking) (handleRecv isBlocking) proof (prove)
goal (2 subgoals):
 1. \<And>isBlocking s. (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and ct_active) s
 2. \<And>isBlocking s. (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> (invs' and ct_active' and sch_act_sane and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_recv ?isBlocking) (handleRecv ?isBlocking)

goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event) proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event) proof (prove)
goal (6 subgoals):
 1. \<And>x1. event = SyscallEvent x1 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)
 4. event = Interrupt \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event) proof (prove)
goal (6 subgoals):
 1. \<And>x1. event = SyscallEvent x1 \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case x1 of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case x1 of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od)
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>syscall. event = SyscallEvent syscall \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od)
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (13 subgoals):
 1. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysCall\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 2. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 3. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysSend\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 4. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBSend\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 5. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysRecv\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 6. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysReply\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 7. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 8. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False) (case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False)
 9. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od)
 10. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
A total of 13 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od)
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (8 subgoals):
 1. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> corres (?r'361 x2) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (gets cur_thread) getCurThread
 2. \<And>x2 thread threada. \<lbrakk>event = UnknownSyscall x2; ?r'361 x2 thread threada\<rbrakk> \<Longrightarrow> corres dc (?Q361 x2 thread) (?Q'361 x2 threada) (handle_fault thread (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))) (handleFault threada (Fault_H.fault.UnknownSyscallException (word_of_nat x2)))
 3. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q361 x2\<rbrace>
 4. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'361 x2\<rbrace>
 5. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 6. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 7. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 8. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>x2 thread threada. \<lbrakk>event = UnknownSyscall x2; thread = threada\<rbrakk> \<Longrightarrow> corres dc (?Q361 x2 threada) (?Q'361 x2 threada) (handle_fault threada (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2))) (handleFault threada (Fault_H.fault.UnknownSyscallException (word_of_nat x2)))
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q361 x2\<rbrace>
 3. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'361 x2\<rbrace>
 4. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 5. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>x2 thread threada. \<lbrakk>event = UnknownSyscall x2; thread = threada\<rbrakk> \<Longrightarrow> fr (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2)) (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active threada and ex_nonz_cap_to threada and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2)))\<rbrace>
 3. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 4. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 5. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active threada and ex_nonz_cap_to threada and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.UnknownSyscallException (word_of_nat x2)))\<rbrace>
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active threada and ex_nonz_cap_to threada\<rbrace>
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x2 s. \<lbrakk>event = UnknownSyscall x2; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (einvs and st_tcb_at active (cur_thread s) and ex_nonz_cap_to (cur_thread s)) s
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2 s. \<lbrakk>event = UnknownSyscall x2; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_not (ksCurThread s) and (\<lambda>sa. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues sa p)) and st_tcb_at' simple' (ksCurThread s) and ex_nonz_cap_to' (ksCurThread s)) s
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2 s. \<lbrakk>event = UnknownSyscall x2; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2 s. \<lbrakk>event = UnknownSyscall x2; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))
od) (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od)
 2. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> corres (?r'434 x31 x32) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (gets cur_thread) getCurThread
 2. \<And>x31 x32 thread threada. \<lbrakk>event = UserLevelFault x31 x32; ?r'434 x31 x32 thread threada\<rbrakk> \<Longrightarrow> corres dc (?Q434 x31 x32 thread) (?Q'434 x31 x32 threada) (handle_fault thread (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))) (handleFault threada (Fault_H.fault.UserException x31 (x32 && mask 28)))
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q434 x31 x32\<rbrace>
 4. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'434 x31 x32\<rbrace>
 5. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 thread threada. \<lbrakk>event = UserLevelFault x31 x32; thread = threada\<rbrakk> \<Longrightarrow> corres dc (?Q434 x31 x32 threada) (?Q'434 x31 x32 threada) (handle_fault threada (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28))) (handleFault threada (Fault_H.fault.UserException x31 (x32 && mask 28)))
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q434 x31 x32\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'434 x31 x32\<rbrace>
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 thread threada. \<lbrakk>event = UserLevelFault x31 x32; thread = threada\<rbrakk> \<Longrightarrow> fr (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28)) (Fault_H.fault.UserException x31 (x32 && mask 28))
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active threada and ex_nonz_cap_to threada and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28)))\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 4. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active threada and ex_nonz_cap_to threada and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28)))\<rbrace>
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 s. \<lbrakk>event = UserLevelFault x31 x32; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (einvs and st_tcb_at active (cur_thread s) and ex_nonz_cap_to (cur_thread s) and (\<lambda>_. valid_fault (ExceptionTypes_A.fault.UserException x31 (x32 && mask 28)))) s
 2. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 2. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 s. \<lbrakk>event = UserLevelFault x31 x32; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_not (ksCurThread s) and (\<lambda>sa. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues sa p)) and st_tcb_at' simple' (ksCurThread s) and ex_nonz_cap_to' (ksCurThread s)) s
 2. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 s. \<lbrakk>event = UserLevelFault x31 x32; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 s. \<lbrakk>event = UserLevelFault x31 x32; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. event = Interrupt \<Longrightarrow> corres dc (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. event = Interrupt \<Longrightarrow> corres dc ?Q509 ?Q'509 (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)
 2. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> ?Q509 s
 3. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ?Q'509 s
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (8 subgoals):
 1. event = Interrupt \<Longrightarrow> corres (=) ?P513 ?P'513 (do_machine_op (getActiveIRQ False)) (doMachineOp (getActiveIRQ False))
 2. \<And>rv. event = Interrupt \<Longrightarrow> corres dc einvs (\<lambda>s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handle_interrupt x) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x)
 3. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 4. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s\<rbrace>
 5. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (?P513 and ?Q513) s
 6. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (?P'513 and ?Q'513) s
 7. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 8. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (8 subgoals):
 1. event = Interrupt \<Longrightarrow> corres_underlying Id False True (=) ?P522 ?Q522 (getActiveIRQ False) (getActiveIRQ False)
 2. \<And>rv. event = Interrupt \<Longrightarrow> corres dc einvs (\<lambda>s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handle_interrupt x) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x)
 3. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 4. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s\<rbrace>
 5. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (?P522 \<circ> machine_state and ?Q513) s
 6. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (?Q522 \<circ> ksMachineState and ?Q'513) s
 7. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 8. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (8 subgoals):
 1. event = Interrupt \<Longrightarrow> no_fail ?Q522 (getActiveIRQ False)
 2. \<And>rv. event = Interrupt \<Longrightarrow> corres dc einvs (\<lambda>s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handle_interrupt x) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x)
 3. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 4. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s\<rbrace>
 5. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q513) s
 6. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (?Q522 \<circ> ksMachineState and ?Q'513) s
 7. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 8. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>rv. event = Interrupt \<Longrightarrow> corres dc einvs (\<lambda>s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handle_interrupt x) (case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x)
 2. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 3. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s\<rbrace>
 4. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q513) s
 5. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'513) s
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>rv a. \<lbrakk>event = Interrupt; rv = Some a\<rbrakk> \<Longrightarrow> corres dc einvs (?R''517 a) (handle_interrupt a) (handleInterrupt a)
 2. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 3. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> ?R''517 x s\<rbrace>
 4. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q513) s
 5. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'513) s
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. event = Interrupt \<Longrightarrow> \<lbrace>?Q513\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>rv. einvs\<rbrace>
 2. event = Interrupt \<Longrightarrow> \<lbrace>?Q'513\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) x \<noteq> irqstate.IRQInactive)) s\<rbrace>
 3. \<And>s. \<lbrakk>event = Interrupt; (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q513) s
 4. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'513) s
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>event = Interrupt; invs s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)
 2. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and (\<lambda>s. \<forall>x. invs' s \<and> valid_irq_states' s)) s
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>event = Interrupt; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and (\<lambda>s. \<forall>x. invs' s \<and> valid_irq_states' s)) s
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>event = Interrupt; invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> valid_irq_states' s
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od)
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> corres (?r'559 x5) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (gets cur_thread) getCurThread
 2. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; ?r'559 x5 thread threada\<rbrakk> \<Longrightarrow> corres dc (?Q559 x5 thread) (?Q'559 x5 threada) (handle_vm_fault thread x5 <catch> handle_fault thread) (handleVMFault threada x5 <catch> handleFault threada)
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q559 x5\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'559 x5\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> corres dc (?Q559 x5 threada) (?Q'559 x5 threada) (handle_vm_fault threada x5 <catch> handle_fault threada) (handleVMFault threada x5 <catch> handleFault threada)
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q559 x5\<rbrace>
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'559 x5\<rbrace>
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> corres (?f564 x5 thread threada \<oplus> dc) (?P565 x5 threada) (?P'567 x5 threada) (handle_vm_fault threada x5) (handleVMFault threada x5)
 2. \<And>x5 thread threada ft ft'. \<lbrakk>event = VMFaultEvent x5; thread = threada; ?f564 x5 thread threada ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E564 x5 thread threada ft) (?E'564 x5 thread threada ft') (handle_fault threada ft) (handleFault threada ft')
 3. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q566 x5 threada\<rbrace> handle_vm_fault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E564 x5 thread threada\<rbrace>
 4. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'564 x5 thread threada\<rbrace>
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. ?P565 x5 threada and ?Q566 x5 threada\<rbrace>
 6. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. ?P'567 x5 threada and ?Q'568 x5 threada\<rbrace>
 7. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x5 thread threada ft ft'. \<lbrakk>event = VMFaultEvent x5; thread = threada; fr ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E564 x5 thread threada ft) (?E'564 x5 thread threada ft') (handle_fault threada ft) (handleFault threada ft')
 2. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q566 x5 threada\<rbrace> handle_vm_fault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E564 x5 thread threada\<rbrace>
 3. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'564 x5 thread threada\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and ?Q566 x5 threada\<rbrace>
 5. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and ?Q'568 x5 threada\<rbrace>
 6. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q566 x5 threada\<rbrace> handle_vm_fault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft. einvs and st_tcb_at active threada and ex_nonz_cap_to threada and (\<lambda>_. valid_fault ft)\<rbrace>
 2. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and ?Q566 x5 threada\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and ?Q'568 x5 threada\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q566 x5 threada\<rbrace> handle_vm_fault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft s. (einvs and st_tcb_at active threada and ex_nonz_cap_to threada) s \<and> valid_fault ft\<rbrace>
 2. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and ?Q566 x5 threada\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and ?Q'568 x5 threada\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?P'587 x5 threada\<rbrace> handle_vm_fault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>
 2. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and (\<lambda>s. (invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at active threada s \<and> ex_nonz_cap_to threada s) \<and> ?P'587 x5 threada s)\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and ?Q'568 x5 threada\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x5 thread threada. \<lbrakk>event = VMFaultEvent x5; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'568 x5 threada\<rbrace> handleVMFault threada x5 \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace>
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and (\<lambda>s. (invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at active threada s \<and> ex_nonz_cap_to threada s) \<and> True \<and> True)\<rbrace>
 3. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and ?Q'568 x5 threada\<rbrace>
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. tcb_at threada and (\<lambda>s. (invs s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at active threada s \<and> ex_nonz_cap_to threada s) \<and> True \<and> True)\<rbrace>
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and (invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada)\<rbrace>
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>x5 s. \<lbrakk>event = VMFaultEvent x5; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (tcb_at (cur_thread s) and (\<lambda>sa. (invs sa \<and> valid_list sa \<and> valid_sched sa \<and> st_tcb_at active (cur_thread s) sa \<and> ex_nonz_cap_to (cur_thread s) sa) \<and> True \<and> True)) s
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and (invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada)\<rbrace>
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>x5 s. \<lbrakk>event = VMFaultEvent x5; invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); ct_running s; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s
 2. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and (invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada)\<rbrace>
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. tcb_at' threada and (invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada)\<rbrace>
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5 s. \<lbrakk>event = VMFaultEvent x5; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (tcb_at' (ksCurThread s) and (invs' and sch_act_not (ksCurThread s) and (\<lambda>sa. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues sa p)) and st_tcb_at' simple' (ksCurThread s) and ex_nonz_cap_to' (ksCurThread s))) s
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5 s. \<lbrakk>event = VMFaultEvent x5; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5 s. \<lbrakk>event = VMFaultEvent x5; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (1 subgoal):
 1. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres dc (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- getCurThread;
handleHypervisorFault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> corres (?r'681 x6) (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (gets cur_thread) getCurThread
 2. \<And>x6 thread threada. \<lbrakk>event = HypervisorEvent x6; ?r'681 x6 thread threada\<rbrakk> \<Longrightarrow> corres dc (?Q681 x6 thread) (?Q'681 x6 threada) (handle_hypervisor_fault thread x6) (handleHypervisorFault threada x6)
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q681 x6\<rbrace>
 4. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'681 x6\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x6 thread threada. \<lbrakk>event = HypervisorEvent x6; thread = threada\<rbrakk> \<Longrightarrow> corres dc (?Q681 x6 threada) (?Q'681 x6 threada) (handle_hypervisor_fault threada x6) (handleHypervisorFault threada x6)
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>?Q681 x6\<rbrace>
 3. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>?Q'681 x6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active (?thread696 x6 threada) and ex_nonz_cap_to (?thread696 x6 threada) and (\<lambda>_. valid_fault (?f692 x6 threada))\<rbrace>
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not (?thread696 x6 threada) and (\<lambda>s. \<forall>p. ?thread696 x6 threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' (?thread696 x6 threada) and ex_nonz_cap_to' (?thread696 x6 threada)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. einvs and st_tcb_at active (?thread696 x6 threada) and ex_nonz_cap_to (?thread696 x6 threada) and (\<lambda>_. \<forall>mw b n g. ?f692 x6 threada = ExceptionTypes_A.fault.CapFault mw b (ExceptionTypes_A.lookup_failure.GuardMismatch n g) \<longrightarrow> length g \<le> word_bits)\<rbrace>
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not (?thread696 x6 threada) and (\<lambda>s. \<forall>p. ?thread696 x6 threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' (?thread696 x6 threada) and ex_nonz_cap_to' (?thread696 x6 threada)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6 s. \<lbrakk>event = HypervisorEvent x6; (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)) s\<rbrakk> \<Longrightarrow> (einvs and st_tcb_at active (?thread696 x6 (cur_thread s)) and ex_nonz_cap_to (?thread696 x6 (cur_thread s)) and (\<lambda>_. \<forall>mw b n g. ?f692 x6 (cur_thread s) = ExceptionTypes_A.fault.CapFault mw b (ExceptionTypes_A.lookup_failure.GuardMismatch n g) \<longrightarrow> length g \<le> word_bits)) s
 2. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not (?thread696 x6 threada) and (\<lambda>s. \<forall>p. ?thread696 x6 threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' (?thread696 x6 threada) and ex_nonz_cap_to' (?thread696 x6 threada)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> getCurThread \<lbrace>\<lambda>threada. invs' and sch_act_not threada and (\<lambda>s. \<forall>p. threada \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' threada and ex_nonz_cap_to' threada\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x6 s. \<lbrakk>event = HypervisorEvent x6; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_not (ksCurThread s) and (\<lambda>sa. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues sa p)) and st_tcb_at' simple' (ksCurThread s) and ex_nonz_cap_to' (ksCurThread s)) s proof (prove)
goal (1 subgoal):
 1. \<And>x6 s. \<lbrakk>event = HypervisorEvent x6; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>x6 s. \<lbrakk>event = HypervisorEvent x6; invs' s; ct_running' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) (handle_event event) (handleEvent event)

goal:
No subgoals!