theory DomainSepInv

lemma handle_invocation_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace>
   handle_invocation calling blocking
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: handle_invocation_def ts_Restart_case_helper
                   split_def liftE_liftM_liftME liftME_def bindE_assoc) apply (wp syscall_valid perform_invocation_domain_sep_inv set_thread_state_runnable_valid_sched
         | simp split del: if_split)+ apply (rule_tac E="\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of
                                                       and valid_mdb and (\<lambda>y. valid_fault ft)"
                    and R="Q" and Q=Q for Q in hoare_post_impErr) apply (wp | simp | clarsimp)+ apply (rule_tac E="\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and
                              valid_mdb and (\<lambda>y. valid_fault (CapFault x False ft))"
                  and R="Q" and Q=Q for Q in hoare_post_impErr) apply (wp lcs_ex_cap_to2 | clarsimp)+ apply (auto intro: st_tcb_ex_cap simp: ct_in_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
x <- liftE (as_user thread (getRegister cap_register));
syscall (doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args (to_bl x) (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (do state <- get_thread_state thread;
if state = Restart then do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od else return ()
od)
odE)
odE \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>thread info x p buffer. \<lbrace>?B72 thread info x p buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>extracaps a. domain_sep_inv irqs st a \<and> a \<turnstile> fst p \<and> invs a \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> real_cte_at (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r a) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>cap\<in>set extracaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>x\<in>set extracaps. a \<turnstile> fst x) \<and> (\<forall>x\<in>set extracaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at ((=) (fst x)) (snd x) a) \<and> (\<forall>x\<in>set extracaps. real_cte_at (snd x) a) \<and> (\<forall>x\<in>set extracaps. ex_cte_cap_wp_to is_cnode_cap (snd x) a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at (interrupt_derived (fst x)) (snd x) a) \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> domain_sep_inv irqs st a \<and> a \<turnstile> fst p \<and> invs a \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> real_cte_at (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r a) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>cap\<in>set extracaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>x\<in>set extracaps. a \<turnstile> fst x) \<and> (\<forall>x\<in>set extracaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at ((=) (fst x)) (snd x) a) \<and> (\<forall>x\<in>set extracaps. real_cte_at (snd x) a) \<and> (\<forall>x\<in>set extracaps. ex_cte_cap_wp_to is_cnode_cap (snd x) a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at (interrupt_derived (fst x)) (snd x) a) \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault ft)) else domain_sep_inv irqs st\<rbrace>
 2. \<And>thread info x p. \<lbrace>?B71 thread info x p\<rbrace> liftE (lookup_ipc_buffer False thread) \<lbrace>?B72 thread info x p\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault ft)) else domain_sep_inv irqs st\<rbrace>
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x)) \<lbrace>?B71 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault ft)) else domain_sep_inv irqs st\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>s. (domain_sep_inv irqs st and invs and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread info x p buffer. \<lbrace>?B72 thread info x p buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>extracaps a. domain_sep_inv irqs st a \<and> a \<turnstile> fst p \<and> invs a \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> real_cte_at (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r a) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>cap\<in>set extracaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>x\<in>set extracaps. a \<turnstile> fst x) \<and> (\<forall>x\<in>set extracaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at ((=) (fst x)) (snd x) a) \<and> (\<forall>x\<in>set extracaps. real_cte_at (snd x) a) \<and> (\<forall>x\<in>set extracaps. ex_cte_cap_wp_to is_cnode_cap (snd x) a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at (interrupt_derived (fst x)) (snd x) a) \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> domain_sep_inv irqs st a \<and> a \<turnstile> fst p \<and> invs a \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> real_cte_at (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r a) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>cap\<in>set extracaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node a). ex_cte_cap_wp_to (\<lambda>_. True) r a) \<and> (\<forall>x\<in>set extracaps. a \<turnstile> fst x) \<and> (\<forall>x\<in>set extracaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at ((=) (fst x)) (snd x) a) \<and> (\<forall>x\<in>set extracaps. real_cte_at (snd x) a) \<and> (\<forall>x\<in>set extracaps. ex_cte_cap_wp_to is_cnode_cap (snd x) a) \<and> (\<forall>x\<in>set extracaps. cte_wp_at (interrupt_derived (fst x)) (snd x) a) \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a\<rbrace>, \<lbrace>\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault ft)\<rbrace>
 2. \<And>thread info x p buffer rv s. domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>x\<in>set rv. s \<turnstile> fst x) \<and> (\<forall>x\<in>set rv. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s) \<and> (\<forall>x\<in>set rv. real_cte_at (snd x) s) \<and> (\<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap (snd x) s) \<and> (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s) \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>x\<in>set rv. s \<turnstile> fst x) \<and> (\<forall>x\<in>set rv. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s) \<and> (\<forall>x\<in>set rv. real_cte_at (snd x) s) \<and> (\<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap (snd x) s) \<and> (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s) \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<Longrightarrow> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>x\<in>set rv. s \<turnstile> fst x) \<and> (\<forall>x\<in>set rv. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s) \<and> (\<forall>x\<in>set rv. real_cte_at (snd x) s) \<and> (\<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap (snd x) s) \<and> (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s) \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> (\<forall>x\<in>set rv. s \<turnstile> fst x) \<and> (\<forall>x\<in>set rv. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s) \<and> (\<forall>x\<in>set rv. real_cte_at (snd x) s) \<and> (\<forall>x\<in>set rv. ex_cte_cap_wp_to is_cnode_cap (snd x) s) \<and> (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s) \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s
 3. \<And>thread info x p buffer e s. (domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault e)) s \<Longrightarrow> (if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault e)) else domain_sep_inv irqs st) s
 4. \<And>thread info x p. \<lbrace>?B71 thread info x p\<rbrace> liftE (lookup_ipc_buffer False thread) \<lbrace>?B72 thread info x p\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault ft)) else domain_sep_inv irqs st\<rbrace>
 5. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x)) \<lbrace>?B71 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault ft)) else domain_sep_inv irqs st\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 9. \<And>s. (domain_sep_inv irqs st and invs and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> lookup_cap_and_slot thread (to_bl x) \<lbrace>\<lambda>p s. domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> invs s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s\<rbrace>, \<lbrace>\<lambda>ft. if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault (CapFault x False ft))) else domain_sep_inv irqs st\<rbrace>
 2. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>s. (domain_sep_inv irqs st and invs and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> lookup_cap_and_slot thread (to_bl x) \<lbrace>\<lambda>p s. domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> invs s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst p \<and> invs s \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> real_cte_at (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> (\<forall>r\<in>zobj_refs (fst p). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst p) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s\<rbrace>, \<lbrace>\<lambda>ft. domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault (CapFault x False ft))\<rbrace>
 2. \<And>thread info x rv s. domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> invs s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst rv \<and> invs s \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> real_cte_at (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> (\<forall>r\<in>zobj_refs (fst rv). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst rv) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst rv \<and> invs s \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> real_cte_at (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> (\<forall>r\<in>zobj_refs (fst rv). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst rv) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<Longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> invs s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst rv \<and> invs s \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> real_cte_at (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> (\<forall>r\<in>zobj_refs (fst rv). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst rv) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> domain_sep_inv irqs st s \<and> s \<turnstile> fst rv \<and> invs s \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> real_cte_at (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> (\<forall>r\<in>zobj_refs (fst rv). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst rv) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s
 3. \<And>thread info x e s. (domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault (CapFault x False e))) s \<Longrightarrow> (if blocking then domain_sep_inv irqs st and (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and (\<lambda>y. valid_fault (CapFault x False e))) else domain_sep_inv irqs st) s
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>s. (domain_sep_inv irqs st and invs and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_sep_inv irqs st s; invs s; ct_active s\<rbrakk> \<Longrightarrow> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal:
No subgoals!