theory Syscall_IF

lemma handle_recv_reads_respects_f:
  fixes st aag
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes mywp =
    domains_distinct
    cap_fault_on_failure_ev'
    receive_ipc_silc_inv[where st=st]
    reads_respects_f[OF receive_ipc_reads_respects, where st=st]
    delete_caller_cap_reads_respects_f[where st=st]
    delete_caller_cap_silc_inv[where st=st]
    reads_respects_f_inv[OF receive_signal_reads_respects receive_signal_silc_inv, where st=st]
    reads_respects_f[OF lookup_slot_for_thread_rev, where st=st and Q=\<top>]
    reads_respects_f_inv[OF get_cap_rev get_cap_inv, where st=st]
    get_cap_auth_wp[where aag=aag]
    reads_respects_f[OF get_simple_ko_reads_respects, where st=st and Q=\<top>]
    lookup_slot_for_thread_authorised
    get_simple_ko_wp
  shows
    "reads_respects_f aag l (silc_inv aag st and einvs and ct_active and pas_refined aag
                                             and pas_cur_domain aag and is_subject aag \<circ> cur_thread)
                      (handle_recv is_blocking)" apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) apply (wp mywp | wpc | assumption | simp | clarsimp
                 | strengthen aag_can_read_self[where x ="fst (fst y)" for y])+ apply (rule_tac Q'="\<lambda>r s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and>
                                   pas_cur_domain aag s \<and> cte_wp_at \<top> (fst r) s \<and> is_subject aag rv \<and>
                                   is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst r))"
                      in hoare_post_imp_R) apply ((wp lookup_slot_for_thread_authorised lookup_slot_cte_at_wp | simp)+)[1] apply (clarsimp simp: silc_inv_not_subject[symmetric] invs_mdb invs_valid_objs) apply (auto intro: caps_of_state_valid reads_ep
                      simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)[1] apply (wp reads_respects_f[OF handle_fault_reads_respects,where st=st]) apply (wpsimp wp: get_simple_ko_wp get_cap_wp)+ apply (rule_tac Q="\<lambda>r s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and>
                                 tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and>
                                 is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst r))"
                     and E=E and F=E for E in hoare_post_impErr) apply (wp lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault) apply ((fastforce simp add:valid_fault_def)+)[3] apply (wp reads_respects_f[OF as_user_reads_respects,where st=st and Q=\<top>]) apply simp apply (wp as_user_silc_inv[where st=st] | simp)+ by (fastforce simp: det_getRegister invs_valid_objs tcb_at_invs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (handle_recv is_blocking) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (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 <- doE p <- lookup_slot_for_thread thread ep_cptr;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva. \<lbrace>?P'304 rv rva\<rbrace> lookup_slot_for_thread rv rva \<lbrace>\<lambda>rva s. \<forall>cap. caps_of_state s (fst rva) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> pasObjectAbs aag rv \<noteq> SilcLabel \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cur_domain aag s \<and> s \<turnstile> EndpointCap x xa xb \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb) \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> aag_can_read_or_affect aag l x \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some rv \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv)))\<rbrace>, -
 2. \<And>rv rva e. reads_respects_f aag l (?E2 rv rva e) (handle_fault rv e)
 3. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>?E2 rv rva\<rbrace>
 4. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> ?P'304 rv rva s) and ?Q2 rv rva\<rbrace>
 6. reads_respects_f aag l ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva. \<lbrace>?P'304 rv rva\<rbrace> lookup_slot_for_thread rv rva \<lbrace>\<lambda>r s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> cte_wp_at (\<lambda>_. True) (fst r) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst r))\<rbrace>, -
 2. \<And>rv rva rvb s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> cte_wp_at (\<lambda>_. True) (fst rvb) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rvb)) \<Longrightarrow> \<forall>cap. caps_of_state s (fst rvb) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> pasObjectAbs aag rv \<noteq> SilcLabel \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cur_domain aag s \<and> s \<turnstile> EndpointCap x xa xb \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb) \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> aag_can_read_or_affect aag l x \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some rv \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv)))
 3. \<And>rv rva e. reads_respects_f aag l (?E2 rv rva e) (handle_fault rv e)
 4. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>?E2 rv rva\<rbrace>
 5. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 6. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> ?P'304 rv rva s) and ?Q2 rv rva\<rbrace>
 7. reads_respects_f aag l ?P' (gets cur_thread)
 8. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 9. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> cte_wp_at (\<lambda>_. True) (fst rvb) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rvb)) \<Longrightarrow> \<forall>cap. caps_of_state s (fst rvb) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> pasObjectAbs aag rv \<noteq> SilcLabel \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cur_domain aag s \<and> s \<turnstile> EndpointCap x xa xb \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb) \<and> invs s \<and> tcb_at rv s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag rv \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> aag_can_read_or_affect aag l x \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some rv \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s \<and> valid_objs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag rv)))
 2. \<And>rv rva e. reads_respects_f aag l (?E2 rv rva e) (handle_fault rv e)
 3. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>?E2 rv rva\<rbrace>
 4. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and ?Q2 rv rva\<rbrace>
 6. reads_respects_f aag l ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv a b s cap. \<lbrakk>silc_inv aag st s; invs s; valid_list s; valid_sched s; pas_refined aag s; tcb_at rv s; pas_cur_domain aag s; cte_wp_at (\<lambda>_. True) (a, b) s; is_subject aag rv; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some cap; pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> s \<turnstile> EndpointCap x xa xb \<and> pas_cap_cur_auth aag (EndpointCap x xa xb) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some rv \<longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)))
 2. \<And>rv rva e. reads_respects_f aag l (?E2 rv rva e) (handle_fault rv e)
 3. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>?E2 rv rva\<rbrace>
 4. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and ?Q2 rv rva\<rbrace>
 6. reads_respects_f aag l ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva e. reads_respects_f aag l (?E2 rv rva e) (handle_fault rv e)
 2. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>?E2 rv rva\<rbrace>
 3. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 4. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and ?Q2 rv rva\<rbrace>
 5. reads_respects_f aag l ?P' (gets cur_thread)
 6. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 7. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<lbrace>?Q2 rv rva\<rbrace> cap_fault_on_failure (of_bl rva) True (doE ep_cap <- doE p <- lookup_slot_for_thread rv rva;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap rv;
receive_ipc rv ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some rv \<or> boundTCB = None then liftE $ receive_signal rv ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) -, \<lbrace>\<lambda>e. silc_inv aag st and (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag rv \<and> valid_fault e)) and (pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault e \<and> is_subject aag rv))\<rbrace>
 2. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 3. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and ?Q2 rv rva\<rbrace>
 4. reads_respects_f aag l ?P' (gets cur_thread)
 5. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 6. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<lbrace>?P'738 rv rva\<rbrace> lookup_slot_for_thread rv rva \<lbrace>\<lambda>p s. \<forall>cap. cte_wp_at ((=) cap) (fst p) s \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some rv \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)\<rbrace>, \<lbrace>\<lambda>rvb s. valid_fault (CapFault (of_bl rva) True rvb) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True rvb) \<and> is_subject aag rv\<rbrace>
 2. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 3. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> ?P'738 rv rva s)\<rbrace>
 4. reads_respects_f aag l ?P' (gets cur_thread)
 5. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 6. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva. \<lbrace>?P'738 rv rva\<rbrace> lookup_slot_for_thread rv rva \<lbrace>\<lambda>r s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst r))\<rbrace>, \<lbrace>\<lambda>rvb s. valid_fault (CapFault (of_bl rva) True rvb) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True rvb) \<and> is_subject aag rv\<rbrace>
 2. \<And>rv rva rvb s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rvb)) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (fst rvb) s \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some rv \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)
 3. \<And>rv rva e s. valid_fault (CapFault (of_bl rva) True e) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True e) \<and> is_subject aag rv \<Longrightarrow> valid_fault (CapFault (of_bl rva) True e) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True e) \<and> is_subject aag rv
 4. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> ?P'738 rv rva s)\<rbrace>
 6. reads_respects_f aag l ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva rvb s. silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rvb)) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (fst rvb) s \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some rv \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> is_subject aag rv \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True (MissingCapability 0)) \<and> is_subject aag rv)
 2. \<And>rv rva e s. valid_fault (CapFault (of_bl rva) True e) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True e) \<and> is_subject aag rv \<Longrightarrow> valid_fault (CapFault (of_bl rva) True e) \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl rva) True e) \<and> is_subject aag rv
 3. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 4. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> invs s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s)\<rbrace>
 5. reads_respects_f aag l ?P' (gets cur_thread)
 6. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 7. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv. reads_respects_f aag l (?P'1 rv) (liftM to_bl (as_user rv (getRegister cap_register)))
 2. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> invs s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s)\<rbrace>
 3. reads_respects_f aag l ?P' (gets cur_thread)
 4. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 5. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv s. (silc_inv aag st and (\<lambda>_. True)) s \<Longrightarrow> silc_inv aag st s
 2. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> invs s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s)\<rbrace>
 3. reads_respects_f aag l ?P' (gets cur_thread)
 4. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. (silc_inv aag st and K (det (getRegister cap_register) \<and> aag_can_read_or_affect aag l rv) and (\<lambda>_. True)) s \<and> ?P''1 rv s\<rbrace>
 5. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?P''1 rv\<rbrace> liftM to_bl (as_user rv (getRegister cap_register)) \<lbrace>\<lambda>rva. (\<lambda>s. ((silc_inv aag st and (pas_refined aag and K (is_subject aag rv)) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> (pas_refined aag and K (is_subject aag rv)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag rv)) s \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> valid_objs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s) and (\<lambda>s. silc_inv aag st s \<and> (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<and> is_subject aag rv \<and> invs s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> is_subject aag rv \<and> silc_inv aag st s \<and> einvs s \<and> pas_refined aag s \<and> tcb_at rv s \<and> pas_cur_domain aag s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag rv)) s)\<rbrace>
 2. reads_respects_f aag l ?P' (gets cur_thread)
 3. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. (silc_inv aag st and K (det (getRegister cap_register) \<and> aag_can_read_or_affect aag l rv) and (\<lambda>_. True)) s \<and> ?P''1 rv s\<rbrace>
 4. \<And>s. (silc_inv aag st and einvs and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?P' s \<and> ?P'' 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> ct_active s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<Longrightarrow> silc_inv aag ?st1120 s \<and> det (getRegister cap_register) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> tcb_at (cur_thread s) s \<and> valid_objs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> tcb_at (cur_thread s) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s