theory DetSchedDomainTime_AI

lemma handle_event_domain_time_inv:
  "\<lbrace>\<lambda>s. P (domain_time s) \<and> e \<noteq> Interrupt \<rbrace>
   handle_event e
   \<lbrace>\<lambda>_ s. P (domain_time s) \<rbrace>" apply (cases e, simp_all) apply (rename_tac syscall) apply (case_tac syscall, simp_all add: handle_send_def) apply (wp|simp|wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s) \<and> e \<noteq> Interrupt\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> 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 \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 4. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 5. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>syscall. e = SyscallEvent syscall \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> 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 \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 4. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 5. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>syscall. \<lbrakk>e = SyscallEvent SysCall; syscall = SysCall\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> handle_call \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 2. \<And>syscall. \<lbrakk>e = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do y <- handle_reply;
handle_recv True
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 3. \<And>syscall. \<lbrakk>e = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> handle_invocation False True \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 4. \<And>syscall. \<lbrakk>e = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> handle_invocation False False \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 5. \<And>syscall. \<lbrakk>e = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (handle_recv True) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 6. \<And>syscall. \<lbrakk>e = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE handle_reply \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 7. \<And>syscall. \<lbrakk>e = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE handle_yield \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 8. \<And>syscall. \<lbrakk>e = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (handle_recv False) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 9. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
 10. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
A total of 12 subgoals... proof (prove)
goal:
No subgoals!