theory FinalCaps

lemma handle_recv_silc_inv:
  "\<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace>
   handle_recv is_blocking
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) apply (wp hoare_vcg_all_lift get_simple_ko_wp delete_caller_cap_silc_inv
            receive_ipc_silc_inv lookup_slot_for_thread_authorised
            lookup_slot_for_thread_cap_fault get_cap_auth_wp[where aag=aag]
         | wpc | simp
         | rule_tac Q="\<lambda>rv s. invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and>
                              (pasSubject aag, Receive, pasObjectAbs aag x31) \<in> pasPolicy aag"
                 in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+ apply (rule_tac Q'="\<lambda>r s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and>
                              is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread"
                 in hoare_post_imp_R) apply wp apply ((clarsimp simp add: invs_valid_objs invs_sym_refs
            | intro impI allI conjI
            | rule cte_wp_valid_cap caps_of_state_cteD
            | fastforce simp: aag_cap_auth_def cap_auth_conferred_def
                              cap_rights_to_auth_def valid_fault_def
                        dest: silc_inv_not_subject)+)[1] apply (wp delete_caller_cap_silc_inv | simp add: split_def cong: conj_cong)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<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 <- 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 \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'283 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag thread \<noteq> SilcLabel \<and> invs s \<and> tcb_at thread 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 thread \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<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 = Some thread \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread))) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)\<rbrace>, -
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. silc_inv aag st s \<and> (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<and> invs s \<and> is_subject aag thread \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> ?P'283 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'283 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>r s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread\<rbrace>, -
 2. \<And>thread ep_cptr rv s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread \<Longrightarrow> \<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag thread \<noteq> SilcLabel \<and> invs s \<and> tcb_at thread 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 thread \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<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 = Some thread \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread))) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)
 3. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. silc_inv aag st s \<and> (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<and> invs s \<and> is_subject aag thread \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> ?P'283 thread ep_cptr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 5. \<And>s. (silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr rv s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread \<Longrightarrow> \<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRead \<in> xb \<longrightarrow> silc_inv aag st s \<and> pasObjectAbs aag thread \<noteq> SilcLabel \<and> invs s \<and> tcb_at thread 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 thread \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<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 = Some thread \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> silc_inv aag st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread))) \<and> (AllowRead \<notin> xb \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s \<and> pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. silc_inv aag st s \<and> (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<and> invs s \<and> is_subject aag thread \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. silc_inv aag st s \<and> (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<and> invs s \<and> is_subject aag thread \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag thread \<and> tcb_at thread s \<and> cur_thread s = thread\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> tcb_at (cur_thread s) s proof (prove)
goal:
No subgoals!