theory Syscall_AC

lemma handle_recv_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread
                       and K (valid_mdb st \<and> valid_objs st)\<rbrace>
   handle_recv is_blocking
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) apply (wp handle_fault_integrity_autarch receive_ipc_integrity_autarch
            receive_signal_integrity_autarch lookup_slot_for_thread_authorised
            lookup_slot_for_thread_cap_fault get_cap_auth_wp [where aag=aag] 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> einvs s \<and> is_subject aag (cur_thread s)
                              \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag thread
                              \<and> integrity aag X st s" 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 wpsimp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread and K (valid_mdb st \<and> valid_objs st)\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs 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>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?P'473 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> pas_refined aag s \<and> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag thread) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> is_subject aag thread \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag thread) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> pas_refined aag s \<and> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)\<rbrace>, -
 2. \<And>thread. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?B3 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. pas_refined aag s \<and> integrity aag X st s \<and> (is_subject aag \<circ> cur_thread) s \<and> invs 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'473 thread ep_cptr s\<rbrace>
 3. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>valid_mdb st \<and> valid_objs st; (integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr rv s. \<lbrakk>valid_mdb st \<and> valid_objs st; pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s) \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag thread \<and> integrity aag X st s\<rbrakk> \<Longrightarrow> \<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (cap = NullCap \<longrightarrow> pas_refined aag s \<and> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag thread) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> is_subject aag thread \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> is_subject aag thread) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> pas_refined aag s \<and> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs 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> integrity aag X st s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)) \<and> is_subject aag thread)
 2. \<And>thread ep_cptr. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?P'473 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s) \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag thread \<and> integrity aag X st s\<rbrace>, -
 3. \<And>thread. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?B3 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. pas_refined aag s \<and> integrity aag X st s \<and> (is_subject aag \<circ> cur_thread) s \<and> invs 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'473 thread ep_cptr s\<rbrace>
 4. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 5. \<And>s. \<lbrakk>valid_mdb st \<and> valid_objs st; (integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?P'473 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s) \<and> tcb_at thread s \<and> cur_thread s = thread \<and> is_subject aag thread \<and> integrity aag X st s\<rbrace>, -
 2. \<And>thread. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?B3 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. pas_refined aag s \<and> integrity aag X st s \<and> (is_subject aag \<circ> cur_thread) s \<and> invs 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'473 thread ep_cptr s\<rbrace>
 3. valid_mdb st \<and> valid_objs st \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets cur_thread \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>valid_mdb st \<and> valid_objs st; (integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_mdb st; valid_objs st; integrity aag X st s; pas_refined aag s; invs s; valid_list s; valid_sched s; is_subject aag (cur_thread s)\<rbrakk> \<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!