theory FinalCaps

lemma handle_invocation_silc_inv:
  "\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag
                    and is_subject aag \<circ> cur_thread and ct_active
                    and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
   handle_invocation calling blocking
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (simp add: handle_invocation_def ts_Restart_case_helper split_def
                   liftE_liftM_liftME liftME_def bindE_assoc
              split del: if_split) apply (wp syscall_valid perform_invocation_silc_inv set_thread_state_runnable_valid_sched
            set_thread_state_pas_refined decode_invocation_authorised
         | simp split del: if_split)+ apply (rule_tac E="\<lambda>ft. silc_inv aag st and pas_refined aag and
                               is_subject aag \<circ> cur_thread and invs and
                               (\<lambda>_. valid_fault ft \<and> is_subject aag thread)"
                   and R="Q" and Q=Q for Q in hoare_post_impErr) apply (wp lookup_extra_caps_authorised lookup_extra_caps_auth | simp)+ apply (rule_tac E="\<lambda>ft. silc_inv aag st and pas_refined aag and
                             is_subject aag \<circ> cur_thread and invs and
                             (\<lambda>_. valid_fault (CapFault x False ft) \<and> is_subject aag thread)"
                 and R="Q" and Q=Q for Q in hoare_post_impErr) apply (wp lookup_cap_and_slot_authorised lookup_cap_and_slot_cur_auth | simp)+ apply (auto intro: st_tcb_ex_cap simp: ct_in_state_def runnable_eq_active) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st'\<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 when calling $ reply_from_kernel thread (0, reply);
set_thread_state thread Running
od else return ()
od)
odE)
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>thread info x p buffer. \<lbrace>?B138 thread info x p buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>extracaps a. silc_inv aag 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> pas_refined aag a \<and> a \<turnstile> fst p \<and> invs a \<and> ct_active a \<and> is_subject aag (cur_thread a) \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'133 thread info x (snd p, fst p, extracaps, buffer)) a \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set extracaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set extracaps. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread a \<and> valid_objs a \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at runnable thread a \<and> simple_sched_action a \<and> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> is_subject aag (cur_thread a) \<and> silc_inv aag 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> pas_refined aag a \<and> a \<turnstile> fst p \<and> invs a \<and> ct_active a \<and> is_subject aag (cur_thread a) \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'134 thread info x (snd p, fst p, extracaps, buffer)) a \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set extracaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set extracaps. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread a \<and> valid_objs a \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at runnable thread a \<and> simple_sched_action a \<and> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> is_subject aag (cur_thread a)\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault ft \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 2. \<And>thread info x p. \<lbrace>?B137 thread info x p\<rbrace> liftE (lookup_ipc_buffer False thread) \<lbrace>?B138 thread info x p\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault ft \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 3. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x)) \<lbrace>?B137 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault ft \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 4. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>s. (silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>thread info x p buffer. \<lbrace>?B138 thread info x p buffer\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>extracaps a. silc_inv aag 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> pas_refined aag a \<and> a \<turnstile> fst p \<and> invs a \<and> ct_active a \<and> is_subject aag (cur_thread a) \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'133 thread info x (snd p, fst p, extracaps, buffer)) a \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set extracaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set extracaps. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread a \<and> valid_objs a \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at runnable thread a \<and> simple_sched_action a \<and> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> is_subject aag (cur_thread a) \<and> silc_inv aag 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> pas_refined aag a \<and> a \<turnstile> fst p \<and> invs a \<and> ct_active a \<and> is_subject aag (cur_thread a) \<and> cte_wp_at ((=) (fst p)) (snd p) a \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) a \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'134 thread info x (snd p, fst p, extracaps, buffer)) a \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set extracaps. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set extracaps. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread a \<and> valid_objs a \<and> st_tcb_at active thread a \<and> invs a \<and> ex_nonz_cap_to thread a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at runnable thread a \<and> simple_sched_action a \<and> pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a \<and> is_subject aag (cur_thread a)\<rbrace>, \<lbrace>\<lambda>ft. silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and invs and (\<lambda>_. valid_fault ft \<and> is_subject aag thread)\<rbrace>
 2. \<And>thread info x p buffer rv s. silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'133 thread info x (snd p, fst p, rv, buffer)) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set rv. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set rv. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'134 thread info x (snd p, fst p, rv, buffer)) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set rv. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set rv. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<Longrightarrow> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'133 thread info x (snd p, fst p, rv, buffer)) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set rv. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set rv. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'134 thread info x (snd p, fst p, rv, buffer)) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> (\<forall>slot\<in>set rv. is_subject aag (fst (snd slot))) \<and> (\<forall>slot\<in>set rv. pas_cap_cur_auth aag (fst slot)) \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s)
 3. \<And>thread info x p buffer e s. (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and invs and (\<lambda>_. valid_fault e \<and> is_subject aag thread)) s \<Longrightarrow> (if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault e \<and> is_subject aag thread)) else silc_inv aag st) s
 4. \<And>thread info x p. \<lbrace>?B137 thread info x p\<rbrace> liftE (lookup_ipc_buffer False thread) \<lbrace>?B138 thread info x p\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault ft \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 5. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x)) \<lbrace>?B137 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault ft \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 6. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. \<And>s. (silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> lookup_cap_and_slot thread (to_bl x) \<lbrace>\<lambda>p s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag thread \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'511 (snd p) (fst p) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'509 (snd p) (fst p) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s)\<rbrace>, \<lbrace>\<lambda>ft. if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault (CapFault x False ft) \<and> is_subject aag thread)) else silc_inv aag st\<rbrace>
 2. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>s. (silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> lookup_cap_and_slot thread (to_bl x) \<lbrace>\<lambda>p s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag thread \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'511 (snd p) (fst p) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst p \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst p)) (snd p) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd p) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'509 (snd p) (fst p) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd p)) \<and> pas_cap_cur_auth aag (fst p) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s)\<rbrace>, \<lbrace>\<lambda>ft. silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and invs and (\<lambda>_. valid_fault (CapFault x False ft) \<and> is_subject aag thread)\<rbrace>
 2. \<And>thread info x rv s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag thread \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst rv \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'511 (snd rv) (fst rv) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd rv)) \<and> pas_cap_cur_auth aag (fst rv) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst rv \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'509 (snd rv) (fst rv) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd rv)) \<and> pas_cap_cur_auth aag (fst rv) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<Longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag thread \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst rv \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'511 (snd rv) (fst rv) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd rv)) \<and> pas_cap_cur_auth aag (fst rv) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> silc_inv aag 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> pas_refined aag s \<and> s \<turnstile> fst rv \<and> invs s \<and> ct_active s \<and> is_subject aag (cur_thread s) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd rv) s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'509 (snd rv) (fst rv) thread info x) s \<and> real_cte_at (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> is_subject aag (fst (snd rv)) \<and> pas_cap_cur_auth aag (fst rv) \<and> pas_refined aag s \<and> is_subject aag thread \<and> pas_refined aag s \<and> is_subject aag thread \<and> thread = cur_thread s \<and> valid_objs s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> valid_list s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s)
 3. \<And>thread info x e s. (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and invs and (\<lambda>_. valid_fault (CapFault x False e) \<and> is_subject aag thread)) s \<Longrightarrow> (if blocking then silc_inv aag st and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault (CapFault x False e) \<and> is_subject aag thread)) else silc_inv aag st) s
 4. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>s. (silc_inv aag st and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> ct_active s \<and> domain_sep_inv (pasMaySendIrqs aag) st' s \<Longrightarrow> valid_objs s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'858 (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 \<and> st_tcb_at runnable (cur_thread s) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'859 (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 \<and> st_tcb_at runnable (cur_thread s) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!