theory Syscall_R

lemma he_invs'[wp]:
  "\<lbrace>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)\<rbrace>
   handleEvent event
   \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have nidle: "\<And>s. invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s" by (clarsimp) show ?thesis apply (case_tac event, simp_all add: handleEvent_def) apply (rename_tac syscall) apply (case_tac syscall,
               (wp handleReply_sane handleReply_nonz_cap_to_ct handleReply_ksCurThread
                   handleReply_ct_not_ksQ
                | clarsimp simp: active_from_running' simple_from_running' simple_sane_strg simp del: split_paired_All
                | rule conjI active_ex_cap'
                | drule ct_not_ksQ[rotated]
                | strengthen nidle)+) apply (rule hoare_strengthen_post,
               rule hoare_weaken_pre,
               rule hy_invs') apply (simp add: active_from_running') apply simp apply (wp hv_inv' hh_inv'
                 | rule conjI
                 | erule pred_tcb'_weakenE st_tcb_ex_cap''
                 | clarsimp simp: tcb_at_invs ct_in_state'_def simple_sane_strg sch_act_simple_def
                 | drule st_tcb_at_idle_thread'
                 | drule ct_not_ksQ[rotated]
                 | wpc | wp (once) hoare_drop_imps)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>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)\<rbrace> handleEvent event \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>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)\<rbrace> handleEvent event \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s proof (state)
this:
invs' ?s \<and> ct_active' ?s \<longrightarrow> ksCurThread ?s \<noteq> ksIdleThread ?s

goal (1 subgoal):
 1. \<lbrace>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)\<rbrace> handleEvent event \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>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)\<rbrace> handleEvent event \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. event = SyscallEvent x1 \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>syscall. event = SyscallEvent syscall \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. event = SyscallEvent SysYield \<Longrightarrow> \<lbrace>?Q144 SysYield\<rbrace> handleYield \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>syscall s. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ?Q144 syscall s
 3. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>event = SyscallEvent SysYield; ?Q144 SysYield s\<rbrakk> \<Longrightarrow> (invs' and ct_active') s
 2. \<And>rv s. \<lbrakk>event = SyscallEvent SysYield; (invs' and ct_active') s\<rbrakk> \<Longrightarrow> invs' s
 3. \<And>syscall s. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> ?Q144 syscall s
 4. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv s. \<lbrakk>event = SyscallEvent SysYield; (invs' and ct_active') s\<rbrakk> \<Longrightarrow> invs' s
 2. \<And>syscall s. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> invs' s \<and> ct_active' s
 3. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>syscall s. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield; (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s\<rbrakk> \<Longrightarrow> invs' s \<and> ct_active' s
 2. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 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 \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. event = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv. invs'\<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> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<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> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>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)\<rbrace> handleEvent event \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!