theory Syscall_AC

lemma handle_event_pas_refined:
  "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
                    and einvs and schact_is_rct
                    and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s))
                    and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<rbrace>
   handle_event ev
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (case_tac ev; simp) apply (rename_tac syscall) apply (case_tac syscall; simp add: handle_send_def handle_call_def) apply ((wp handle_invocation_pas_refined handle_recv_pas_refined
                       handle_fault_pas_refined
                    | simp | clarsimp)+) apply (fastforce simp: valid_fault_def) apply (wp handle_fault_pas_refined | simp)+ apply (fastforce simp: valid_fault_def) apply (wp handle_interrupt_pas_refined handle_fault_pas_refined
             hoare_vcg_conj_lift hoare_vcg_all_lift
          | wpc
          | rule hoare_drop_imps
          | strengthen invs_vobjs_strgs invs_psp_aligned invs_vspace_objs invs_arch_state
          | simp)+ done

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