theory DomainSepInv

lemma handle_event_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
   handle_event ev
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (case_tac ev, simp_all) apply (rule hoare_pre) apply (wpsimp wp: handle_send_domain_sep_inv handle_call_domain_sep_inv
                         handle_recv_domain_sep_inv handle_reply_domain_sep_inv hy_inv
              | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def)+ apply (rule_tac E="\<lambda>rv s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state) \<and>
                               invs s \<and> valid_fault rv" and R="Q" and Q=Q for Q in hoare_post_impErr) apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def | auto)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> handle_event ev \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs 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>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. ev = Interrupt \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. ev = SyscallEvent x1 \<Longrightarrow> \<lbrace>?Q4 x1\<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>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x1 s. \<lbrakk>ev = SyscallEvent x1; (domain_sep_inv irqs st and invs and ct_active) s\<rbrakk> \<Longrightarrow> ?Q4 x1 s
 3. \<And>x2. ev = UnknownSyscall x2 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x31 x32. ev = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. ev = Interrupt \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x5 thread. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>?P'190 x5 thread\<rbrace> handle_vm_fault thread x5 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>rv s. valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> (\<forall>mw b n g. rv = CapFault mw b (GuardMismatch n g) \<longrightarrow> length g \<le> word_bits)\<rbrace>
 2. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>?Q183 x5\<rbrace> gets cur_thread \<lbrace>\<lambda>thread s. domain_sep_inv irqs st s \<and> ?P'190 x5 thread s\<rbrace>
 3. \<And>x5 s. \<lbrakk>ev = VMFaultEvent x5; (domain_sep_inv irqs st and invs and ct_active) s\<rbrakk> \<Longrightarrow> ?Q183 x5 s
 4. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x5 thread. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>?P'190 x5 thread\<rbrace> handle_vm_fault thread x5 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>, \<lbrace>\<lambda>rv s. domain_sep_inv irqs st s \<and> invs s \<and> valid_fault rv\<rbrace>
 2. \<And>x5 thread rv s. \<lbrakk>ev = VMFaultEvent x5; domain_sep_inv irqs st s\<rbrakk> \<Longrightarrow> domain_sep_inv irqs st s
 3. \<And>x5 thread e s. \<lbrakk>ev = VMFaultEvent x5; domain_sep_inv irqs st s \<and> invs s \<and> valid_fault e\<rbrakk> \<Longrightarrow> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> (\<forall>mw b n g. e = CapFault mw b (GuardMismatch n g) \<longrightarrow> length g \<le> word_bits)
 4. \<And>x5. ev = VMFaultEvent x5 \<Longrightarrow> \<lbrace>?Q183 x5\<rbrace> gets cur_thread \<lbrace>\<lambda>thread s. domain_sep_inv irqs st s \<and> ?P'190 x5 thread s\<rbrace>
 5. \<And>x5 s. \<lbrakk>ev = VMFaultEvent x5; (domain_sep_inv irqs st and invs and ct_active) s\<rbrakk> \<Longrightarrow> ?Q183 x5 s
 6. \<And>x6. ev = HypervisorEvent x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!