theory Syscall_AI

lemma he_invs[wp]:
  "\<And>e.
    \<lbrace>\<lambda>s. invs s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
      handle_event e
    \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (case_tac e, simp_all) apply (rename_tac syscall) apply (case_tac syscall, simp_all) apply (((rule hoare_pre, wp hvmf_active hr_invs hy_inv ) |
                 wpc | wp hoare_drop_imps hoare_vcg_all_lift |
                 simp add: if_apply_def2 |
                 fastforce simp: tcb_at_invs ct_in_state_def valid_fault_def
                         elim!: st_tcb_ex_cap)+) done

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