theory Syscall_AC

lemma handle_recv_pas_refined:
  "\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace>
     handle_recv is_blocking
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) apply (wp handle_fault_pas_refined receive_ipc_pas_refined receive_signal_pas_refined
            get_cap_auth_wp [where aag=aag] lookup_slot_for_cnode_op_authorised
            lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault
            hoare_vcg_all_lift_R get_simple_ko_wp
         | wpc | simp
         | (rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread \<and> aag_has_auth_to aag Receive thread"
                  in hoare_strengthen_post,
            wp, clarsimp simp: invs_valid_objs invs_sym_refs))+ apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s
                              \<and> cur_thread s = thread \<and> is_subject aag (cur_thread s)
                              \<and> is_subject aag thread" in hoare_post_imp_R [rotated]) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def
                             cap_rights_to_auth_def valid_fault_def) apply (wp user_getreg_inv | strengthen invs_vobjs_strgs | simp)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs 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>_. pas_refined aag\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr cap. \<lbrace>?P420 thread ep_cptr cap\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> 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> 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> is_subject aag thread \<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> invs s \<and> tcb_at thread s \<and> is_subject aag thread \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (AllowRead \<notin> xb \<longrightarrow> 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> is_subject aag thread \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> is_subject aag thread \<and> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> is_subject aag thread \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasObjectAbs aag thread, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> is_subject aag thread \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasObjectAbs aag thread, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> 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> 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> 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> 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> 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> 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> 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> 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> 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> 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. pas_refined aag s \<and> invs s \<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> (\<forall>x. ?P420 thread ep_cptr x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr cap rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag (cur_thread s) \<and> is_subject aag thread \<Longrightarrow> caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> 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> 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> is_subject aag thread \<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> invs s \<and> tcb_at thread s \<and> is_subject aag thread \<and> pas_cap_cur_auth aag (EndpointCap x xa xb)) \<and> (AllowRead \<notin> xb \<longrightarrow> 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> is_subject aag thread \<and> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> is_subject aag thread \<and> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> is_subject aag thread \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasObjectAbs aag thread, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> is_subject aag thread \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasObjectAbs aag thread, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> 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> 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> 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> 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> 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> 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> 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> 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> 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> 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 ep_cptr cap. \<lbrace>?P420 thread ep_cptr cap\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag (cur_thread s) \<and> is_subject aag thread\<rbrace>, -
 3. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. pas_refined aag s \<and> invs s \<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> (\<forall>x. ?P420 thread ep_cptr x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 5. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr cap. \<lbrace>?P420 thread ep_cptr cap\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag (cur_thread s) \<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. pas_refined aag s \<and> invs s \<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> (\<forall>x. ?P420 thread ep_cptr x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<Longrightarrow> tcb_at (cur_thread s) s proof (prove)
goal:
No subgoals!