theory ADT_IF

lemma handle_event_irq_state_inv:
  "event \<noteq> Interrupt
   \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False (sta :: det_state)
                                  and K (irq_is_recurring irq st)\<rbrace>
       handle_event event
       \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (case_tac event; simp) apply (rename_tac syscall) apply (case_tac syscall) by (simp add: handle_send_def handle_call_def
      | wp handle_invocation_irq_state_inv[where sta=sta and irq=irq]
           irq_state_inv_triv[OF handle_recv_irq_state_of_state] irq_state_inv_triv
           irq_state_inv_triv[OF handle_reply_irq_state_of_state] hy_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. event \<noteq> Interrupt \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> handle_event event \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. event = SyscallEvent x1 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>syscall. event = SyscallEvent syscall \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 3. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 4. \<And>x5. event = VMFaultEvent x5 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 5. \<And>x6. event = HypervisorEvent x6 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysCall\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysSend\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBSend\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysRecv\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 6. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 7. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 8. \<And>syscall. \<lbrakk>event = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<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>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 9. \<And>x2. event = UnknownSyscall x2 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
 10. \<And>x31 x32. event = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>irq_state_inv st and invs and domain_sep_inv False sta and (\<lambda>y. irq_is_recurring irq st)\<rbrace> do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
A total of 12 subgoals...