theory Syscall_S

lemma handle_event_bisim:
  "bisim (dc \<oplus> (=)) \<top> (separate_state and cur_tcb and valid_objs) (handle_event ev) (Syscall_A.handle_event ev)" apply (cases ev; simp add: handle_send_def Syscall_A.handle_send_def
                             handle_call_def Syscall_A.handle_call_def
                             handle_reply_def
                        cong: syscall.case_cong) apply (rename_tac syscall) apply (case_tac syscall, simp_all)[1] apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) apply (rule bisim_guard_imp_both) apply (rule bisim_symb_exec_r_bs) apply (rule handle_reply_bisim) apply (rule handle_recv_bisim) apply simp apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp) apply (rule bisim_guard_imp_both, rule handle_reply_bisim, simp) apply (simp add: handle_yield_def Syscall_A.handle_yield_def) apply (rule bisim_guard_imp_both, rule bisim_refl', simp) apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp) apply (rule bisim_split_refl) apply (rule handle_fault_bisim) apply wp+ apply (simp add: cur_tcb_def) apply (rule bisim_split_refl) apply (rule handle_fault_bisim) apply wp+ apply (simp add: cur_tcb_def) apply (rule bisim_refl) apply simp apply (rename_tac vmfault_type) apply (rule bisim_guard_imp_both) apply (rule bisim_split_refl) apply (rule bisim_split_catch_req) apply (rule bisim_reflE) apply (rule handle_fault_bisim) apply (wpsimp wp: hv_inv_ex) apply wpsimp+ apply (simp add: cur_tcb_def) apply (rule bisim_refl, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_event ev) (Syscall_A.handle_event ev) proof (prove)
goal (6 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (case x1 of SysCall \<Rightarrow> Syscall_SA.handle_invocation True True | SysSend \<Rightarrow> Syscall_SA.handle_invocation False True | SysNBSend \<Rightarrow> Syscall_SA.handle_invocation False False | SysReply \<Rightarrow> liftE (return ()) | SysYield \<Rightarrow> liftE Syscall_SA.handle_yield | SysNBRecv \<Rightarrow> liftE (Syscall_SA.handle_recv False) | _ \<Rightarrow> liftE (Syscall_SA.handle_recv True)) (case x1 of SysCall \<Rightarrow> Syscall_A.handle_invocation True True | SysReplyRecv \<Rightarrow> liftE (do y <- Syscall_A.handle_reply;
Syscall_A.handle_recv True
od) | SysSend \<Rightarrow> Syscall_A.handle_invocation False True | SysNBSend \<Rightarrow> Syscall_A.handle_invocation False False | SysRecv \<Rightarrow> liftE (Syscall_A.handle_recv True) | SysReply \<Rightarrow> liftE Syscall_A.handle_reply | SysYield \<Rightarrow> liftE Syscall_A.handle_yield | SysNBRecv \<Rightarrow> liftE (Syscall_A.handle_recv False))
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 4. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>syscall. ev = SyscallEvent syscall \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (case syscall of SysCall \<Rightarrow> Syscall_SA.handle_invocation True True | SysSend \<Rightarrow> Syscall_SA.handle_invocation False True | SysNBSend \<Rightarrow> Syscall_SA.handle_invocation False False | SysReply \<Rightarrow> liftE (return ()) | SysYield \<Rightarrow> liftE Syscall_SA.handle_yield | SysNBRecv \<Rightarrow> liftE (Syscall_SA.handle_recv False) | _ \<Rightarrow> liftE (Syscall_SA.handle_recv True)) (case syscall of SysCall \<Rightarrow> Syscall_A.handle_invocation True True | SysReplyRecv \<Rightarrow> liftE (do y <- Syscall_A.handle_reply;
Syscall_A.handle_recv True
od) | SysSend \<Rightarrow> Syscall_A.handle_invocation False True | SysNBSend \<Rightarrow> Syscall_A.handle_invocation False False | SysRecv \<Rightarrow> liftE (Syscall_A.handle_recv True) | SysReply \<Rightarrow> liftE Syscall_A.handle_reply | SysYield \<Rightarrow> liftE Syscall_A.handle_yield | SysNBRecv \<Rightarrow> liftE (Syscall_A.handle_recv False))
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 4. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (13 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysCall; syscall = SysCall\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation True True) (Syscall_A.handle_invocation True True)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (do y <- Syscall_A.handle_reply;
Syscall_A.handle_recv True
od)
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 8. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 9. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 10. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (do y <- Syscall_A.handle_reply;
Syscall_A.handle_recv True
od)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 8. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 9. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 10. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (?P22 syscall) (?P'22 syscall) (Syscall_SA.handle_recv True) (do y <- Syscall_A.handle_reply;
Syscall_A.handle_recv True
od)
 2. \<And>syscall s. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P22 syscall s \<and> ?P'22 syscall s
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 8. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 9. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 10. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (?R25 syscall) (?P'22 syscall) (return ()) Syscall_A.handle_reply
 2. \<And>syscall y. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (?P25 syscall) (?P'25 syscall) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 3. \<And>syscall s. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> (?P25 syscall and ?R25 syscall and ?P'25 syscall) s \<and> ?P'22 syscall s
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 8. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 9. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 10. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>syscall y. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> bisim (=) (?P25 syscall) (?P'25 syscall) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 2. \<And>syscall s. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> (?P25 syscall and (\<lambda>_. True) and ?P'25 syscall) s \<and> (separate_state and cur_tcb) s
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 8. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 9. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 10. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>syscall s. \<lbrakk>ev = SyscallEvent SysReplyRecv; syscall = SysReplyRecv; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and (separate_state and cur_tcb and valid_objs)) s \<and> (separate_state and cur_tcb) s
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 7. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 8. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 9. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 10. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False True) (Syscall_A.handle_invocation False True)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 6. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 7. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 8. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 9. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 10. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_invocation False False) (Syscall_A.handle_invocation False False)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 5. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 6. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 7. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 8. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 9. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 10. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (9 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv True) (Syscall_A.handle_recv True)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 4. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 5. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 6. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 7. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 8. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 9. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (8 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (return ()) Syscall_A.handle_reply
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 3. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 4. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 5. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 6. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 7. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 8. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) Syscall_SA.handle_yield Syscall_A.handle_yield
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 3. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 4. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 5. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 6. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 7. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue thread);
y <- do_extended_op (tcb_sched_action tcb_sched_append thread);
do_extended_op reschedule_required
od) (do thread <- gets cur_thread;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue thread);
y <- do_extended_op (tcb_sched_action tcb_sched_append thread);
do_extended_op reschedule_required
od)
 2. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 3. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 4. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 5. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 6. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 7. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>syscall. \<lbrakk>ev = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv False) (Syscall_A.handle_recv False)
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 4. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UnknownSyscallException (word_of_nat x2))
od)
 2. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 3. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 4. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 5. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>x2 r. ev = UnknownSyscall x2 \<Longrightarrow> bisim (=) (?Q54 x2 r) (?Q'54 x2 r) (Ipc_SA.handle_fault r (UnknownSyscallException (word_of_nat x2))) (Ipc_A.handle_fault r (UnknownSyscallException (word_of_nat x2)))
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cur_thread \<lbrace>?Q54 x2\<rbrace>
 3. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> gets cur_thread \<lbrace>?Q'54 x2\<rbrace>
 4. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 5. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 6. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 7. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> gets cur_thread \<lbrace>\<lambda>r. separate_state and tcb_at r and valid_objs\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 4. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x2 s. \<lbrakk>ev = UnknownSyscall x2; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> (separate_state and tcb_at (cur_thread s) and valid_objs) s
 2. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 3. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 4. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 5. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
Ipc_SA.handle_fault thread (UserException x31 (x32 && mask 28))
od) (do thread <- gets cur_thread;
Ipc_A.handle_fault thread (UserException x31 (x32 && mask 28))
od)
 2. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 3. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 4. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 r. ev = UserLevelFault x31 x32 \<Longrightarrow> bisim (=) (?Q67 x31 x32 r) (?Q'67 x31 x32 r) (Ipc_SA.handle_fault r (UserException x31 (x32 && mask 28))) (Ipc_A.handle_fault r (UserException x31 (x32 && mask 28)))
 2. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cur_thread \<lbrace>?Q67 x31 x32\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> gets cur_thread \<lbrace>?Q'67 x31 x32\<rbrace>
 4. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> gets cur_thread \<lbrace>\<lambda>r. separate_state and tcb_at r and valid_objs\<rbrace>
 3. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 4. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 5. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 s. \<lbrakk>ev = UserLevelFault x31 x32; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> (separate_state and tcb_at (cur_thread s) and valid_objs) s
 2. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 3. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 4. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (3 subgoals):
 1. ev = Interrupt \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt)
 2. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 3. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>r. ev = Interrupt \<Longrightarrow> r = r
 2. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 3. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> Ipc_A.handle_fault thread
od)
 2. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_vm_fault thread vmfault_type <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread vmfault_type <catch> Ipc_A.handle_fault thread
od)
 2. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (3 subgoals):
 1. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim (=) (?P82 vmfault_type) (?P'82 vmfault_type) (do thread <- gets cur_thread;
handle_vm_fault thread vmfault_type <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
handle_vm_fault thread vmfault_type <catch> Ipc_A.handle_fault thread
od)
 2. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 3. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>vmfault_type r. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim (=) (?Q85 vmfault_type r) (?Q'85 vmfault_type r) (handle_vm_fault r vmfault_type <catch> Ipc_SA.handle_fault r) (handle_vm_fault r vmfault_type <catch> Ipc_A.handle_fault r)
 2. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P82 vmfault_type\<rbrace> gets cur_thread \<lbrace>?Q85 vmfault_type\<rbrace>
 3. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P'82 vmfault_type\<rbrace> gets cur_thread \<lbrace>?Q'85 vmfault_type\<rbrace>
 4. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 5. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (7 subgoals):
 1. \<And>vmfault_type r. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pn89 vmfault_type r) (?Q'85 vmfault_type r) (handle_vm_fault r vmfault_type) (handle_vm_fault r vmfault_type)
 2. \<And>vmfault_type r x. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim (=) (?Pf89 vmfault_type r x) (?Pf'89 vmfault_type r x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 3. \<And>vmfault_type r. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P89 vmfault_type r\<rbrace> handle_vm_fault r vmfault_type \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ra. ?Pf89 vmfault_type r ra and ?Pf'89 vmfault_type r ra\<rbrace>
 4. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r. ?Pn89 vmfault_type r and ?P89 vmfault_type r\<rbrace>
 5. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P'82 vmfault_type\<rbrace> gets cur_thread \<lbrace>?Q'85 vmfault_type\<rbrace>
 6. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 7. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (6 subgoals):
 1. \<And>vmfault_type r x. ev = VMFaultEvent vmfault_type \<Longrightarrow> bisim (=) (?Pf89 vmfault_type r x) (?Pf'89 vmfault_type r x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 2. \<And>vmfault_type r. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P89 vmfault_type r\<rbrace> handle_vm_fault r vmfault_type \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ra. ?Pf89 vmfault_type r ra and ?Pf'89 vmfault_type r ra\<rbrace>
 3. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (\<lambda>_. True) and ?P89 vmfault_type r\<rbrace>
 4. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P'82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 5. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (5 subgoals):
 1. \<And>vmfault_type r. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P89 vmfault_type r\<rbrace> handle_vm_fault r vmfault_type \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ra. (\<lambda>_. True) and (separate_state and tcb_at r and valid_objs)\<rbrace>
 2. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (\<lambda>_. True) and ?P89 vmfault_type r\<rbrace>
 3. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P'82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 5. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (4 subgoals):
 1. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (\<lambda>_. True) and ((\<lambda>_. True) and (separate_state and tcb_at r and valid_objs))\<rbrace>
 2. \<And>vmfault_type. ev = VMFaultEvent vmfault_type \<Longrightarrow> \<lbrace>?P'82 vmfault_type\<rbrace> gets cur_thread \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; (separate_state and cur_tcb and valid_objs) s\<rbrakk> \<Longrightarrow> ?P82 vmfault_type s \<and> ?P'82 vmfault_type s
 4. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (2 subgoals):
 1. \<And>vmfault_type s. \<lbrakk>ev = VMFaultEvent vmfault_type; separate_state s; cur_tcb s; valid_objs s\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s
 2. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal (1 subgoal):
 1. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) proof (prove)
goal:
No subgoals!