theory Syscall_AC

lemma handle_event_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag
                       and domain_sep_inv (pasMaySendIrqs aag) st'
                       and einvs and schact_is_rct
                       and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
                       and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and ((=) st)\<rbrace>
   handle_event ev
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases ev; simp) apply (unfold handle_send_def handle_call_def) by (wpsimp wp: handle_recv_integrity handle_invocation_respects
                  handle_reply_respects handle_fault_integrity_autarch
                  handle_interrupt_integrity handle_vm_fault_integrity
                  handle_reply_pas_refined handle_vm_fault_valid_fault
                  handle_reply_valid_sched
                  hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps
            simp: domain_sep_inv_def
      | rule dmo_wp hoare_vcg_E_elim
      | fastforce
      | (rule hoare_vcg_conj_lift)?, wpsimp wp: getActiveIRQ_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st\<rbrace> handle_event ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) 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>_. integrity aag X st\<rbrace>
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. ev = Interrupt \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (=) st\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> case x1 of SysCall \<Rightarrow> handle_invocation True True | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_invocation False True | SysNBSend \<Rightarrow> handle_invocation False 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>_. integrity aag X st\<rbrace>
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. ev = Interrupt \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (=) st\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and ct_active and (=) st\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>