theory Syscall_AI

lemma hw_invs[wp]: "\<lbrace>invs and ct_active\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>r. invs\<rbrace>" apply (simp add: handle_recv_def Let_def ep_ntfn_cap_case_helper
    cong: if_cong) apply (wp get_simple_ko_wp | clarsimp)+ apply (wp delete_caller_cap_nonz_cap get_simple_ko_wp hoare_vcg_ball_lift | simp)+ apply (rule hoare_vcg_E_elim) apply (simp add: lookup_cap_def lookup_slot_for_thread_def) apply wp apply (simp add: split_def) apply (wp resolve_address_bits_valid_fault2)+ apply (simp add: valid_fault_def) apply ((wp hoare_vcg_all_lift_R lookup_cap_ex_cap
          | simp add: obj_at_def
          | simp add: conj_disj_distribL ball_conj_distrib
          | wp (once) hoare_drop_imps)+) apply (simp add: ct_in_state_def) apply (fold obj_at_def) apply (fastforce elim!: invs_valid_tcb_ctable st_tcb_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
if is_ep_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then liftE (do y <- delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od) else throwError (MissingCapability 0) else if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap is_blocking) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>thread ep_cptr ep_cap. \<lbrakk>is_ep_cap ep_cap; AllowRecv \<in> cap_rights ep_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'33 thread ep_cptr ep_cap\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv s. ex_nonz_cap_to thread s \<and> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s)\<rbrace>
 2. \<And>thread ep_cptr ep_cap. \<lbrakk>is_ep_cap ep_cap; AllowRecv \<notin> cap_rights ep_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R23 thread ep_cptr ep_cap\<rbrace> throwError (MissingCapability 0) \<lbrace>\<lambda>r. invs\<rbrace>, \<lbrace>\<lambda>ft s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True ft)\<rbrace>
 3. \<And>thread ep_cptr ep_cap. \<not> is_ep_cap ep_cap \<Longrightarrow> \<lbrace>?R22 thread ep_cptr ep_cap\<rbrace> if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap is_blocking) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0) \<lbrace>\<lambda>r. invs\<rbrace>, \<lbrace>\<lambda>ft s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True ft)\<rbrace>
 4. \<And>thread ep_cptr. \<lbrace>?B14 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (invs and tcb_at thread) s \<and> st_tcb_at active thread s \<and> ?P'33 thread ep_cptr ep_cap s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> ?R23 thread ep_cptr ep_cap s)) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> ?R22 thread ep_cptr ep_cap s)\<rbrace>, \<lbrace>\<lambda>ft s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True ft)\<rbrace>
 5. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>?B14 thread\<rbrace>
 6. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 7. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'100 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> ?P'100 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 3. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> ?P112 thread ep_cptr s \<and> ?P'112 thread ep_cptr s\<rbrace>
 4. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 5. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P112 thread ep_cptr\<rbrace> doE (ref', uu_) <- doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, ep_cptr)
odE;
liftE (get_cap ref')
odE -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 3. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> ?P112 thread ep_cptr s \<and> ?P'112 thread ep_cptr s\<rbrace>
 4. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 5. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (6 subgoals):
 1. \<And>thread ep_cptr x. \<lbrace>?B116 thread ep_cptr x\<rbrace> case x of (ref', uu_) \<Rightarrow> liftE (get_cap ref') -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P112 thread ep_cptr\<rbrace> doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, ep_cptr)
odE \<lbrace>?B116 thread ep_cptr\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 3. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 4. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> ?P112 thread ep_cptr s \<and> ?P'112 thread ep_cptr s\<rbrace>
 5. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 6. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (6 subgoals):
 1. \<And>thread ep_cptr x. \<lbrace>?B116 thread ep_cptr x\<rbrace> liftE (get_cap (fst x)) -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P112 thread ep_cptr\<rbrace> doE tcb <- liftE (gets_the (get_tcb thread));
resolve_address_bits (tcb_ctable tcb, ep_cptr)
odE \<lbrace>?B116 thread ep_cptr\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 3. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 4. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> ?P112 thread ep_cptr s \<and> ?P'112 thread ep_cptr s\<rbrace>
 5. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 6. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb thread s)), ep_cptr))) s \<and> True) \<and> ?P'112 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'112 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> invs s \<and> tcb_at thread s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> tcb_at thread s \<and> valid_objs s \<and> (\<forall>x\<in>zobj_refs ep_cap. ex_nonz_cap_to x s \<and> tcb_at thread s \<and> valid_objs s)) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s)) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (\<forall>r\<in>zobj_refs ep_cap. ex_nonz_cap_to r s) \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some thread)) (cap_ep_ptr ep_cap) s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s)) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s))\<rbrace>, -
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. invs s \<and> st_tcb_at active thread s \<and> ex_nonz_cap_to thread s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb thread s)), ep_cptr))) s \<and> True) \<and> ?P'112 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (invs and ct_active) s \<Longrightarrow> ?Q12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> ct_active s \<Longrightarrow> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>y. get_tcb (cur_thread s) s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb (cur_thread s) s))) \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<and> valid_objs s \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<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 active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>x. ntfn_bound_tcb x \<noteq> Some (cur_thread s) \<and> (\<exists>y. ntfn_bound_tcb x = Some y)) \<longrightarrow> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s) \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> st_tcb_at active (cur_thread s) s \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>y. get_tcb (cur_thread s) s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb (cur_thread s) s))) \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<and> ex_nonz_cap_to (cur_thread s) s \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<and> valid_objs s \<and> (\<exists>ko. kheap s (cur_thread s) = Some ko \<and> is_tcb ko) \<and> valid_objs s \<and> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>x. ntfn_bound_tcb x \<noteq> Some (cur_thread s) \<and> (\<exists>y. ntfn_bound_tcb x = Some y)) \<longrightarrow> ex_nonz_cap_to (cur_thread s) s) \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> st_tcb_at active (cur_thread s) s \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>y. get_tcb (cur_thread s) s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb (cur_thread s) s))) \<and> tcb_at (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> tcb_at (cur_thread s) s \<and> valid_objs s \<and> tcb_at (cur_thread s) s \<and> valid_objs s \<and> ex_nonz_cap_to (cur_thread s) s \<and> ((\<exists>x. ntfn_bound_tcb x \<noteq> Some (cur_thread s) \<and> (\<exists>y. ntfn_bound_tcb x = Some y)) \<longrightarrow> ex_nonz_cap_to (cur_thread s) s) \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal:
No subgoals!