theory Ipc_IF

lemma send_fault_ipc_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label) (invs and pas_refined aag and pas_cur_domain aag
         and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault))
     (send_fault_ipc thread fault)" apply (rule gen_asm_ev) apply (simp add: send_fault_ipc_def Let_def lookup_cap_def split_def) apply (wp send_ipc_reads_respects thread_set_reads_respects
            thread_set_refs_trivial thread_set_obj_at_impossible
            thread_set_valid_objs''
            hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift
            thread_set_pas_refined cap_fault_on_failure_rev
            lookup_slot_for_thread_rev
            lookup_slot_for_thread_authorised hoare_vcg_all_lift_R
            thread_get_reads_respects get_cap_auth_wp[where aag=aag] get_cap_rev
            thread_set_tcb_fault_set_invs
       | wpc
       | simp add: split_def add: tcb_cap_cases_def
       | strengthen aag_can_read_self)+ 
  (* clagged from Ipc_AC *)
   apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s
                          \<and> is_subject aag (cur_thread s)
                          \<and> invs s
                          \<and> pas_cur_domain aag s
                          \<and> valid_fault fault
                          \<and> is_subject aag (fst (fst rv))"
               in hoare_post_imp_R[rotated]) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
                thread_get_reads_respects
            | simp add: add: lookup_cap_def split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (send_fault_ipc thread fault) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (doE p <- lookup_slot_for_thread thread handler_cptr;
liftE (get_cap (fst p))
odE);
case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE) proof (prove)
goal (5 subgoals):
 1. \<And>rv x xa xb cap. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P277 rv x xa xb cap\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> (AllowGrant \<in> xb \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>rv. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P'269 rv\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = NotificationCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ReplyCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = CNodeCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ThreadCap x \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = DomainCap \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQControlCap \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQHandlerCap x \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = Zombie x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ArchObjectCap x \<longrightarrow> True))\<rbrace>, -
 3. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l ?P'2 (liftE (thread_get tcb_fault_handler thread))
 4. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P''2\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>rv s. ((pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and K (is_subject aag thread)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>x. ?P250 rv x s) \<and> (\<forall>x xa xb xc. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xd. ?P264 rv x xa xb xc xd s)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xc. ?P277 rv x xa xb xc s)) \<and> ?P'269 rv s\<rbrace>, -
 5. \<And>s. \<lbrakk>is_subject aag thread \<and> valid_fault fault; (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv x xa xb cap. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P277 rv x xa xb cap\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> (AllowGrant \<in> xb \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>rv. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P'269 rv\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = NotificationCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ReplyCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = CNodeCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ThreadCap x \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = DomainCap \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQControlCap \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQHandlerCap x \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = Zombie x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ArchObjectCap x \<longrightarrow> True))\<rbrace>, -
 3. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l ?P'2 (liftE (thread_get tcb_fault_handler thread))
 4. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P''2\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>rv s. ((pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and K (is_subject aag thread)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>x. ?P250 rv x s) \<and> (\<forall>x xa xb xc. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xd. ?P264 rv x xa xb xc xd s)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xc. ?P277 rv x xa xb xc s)) \<and> ?P'269 rv s\<rbrace>, -
 5. \<And>s. \<lbrakk>is_subject aag thread \<and> valid_fault fault; (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv x xa xb cap rva s. \<lbrakk>is_subject aag thread \<and> valid_fault fault; pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> pas_cur_domain aag s \<and> valid_fault fault \<and> is_subject aag (fst (fst rva))\<rbrakk> \<Longrightarrow> caps_of_state s (fst rva) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> (AllowGrant \<in> xb \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>rv x xa xb cap. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P277 rv x xa xb cap\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> pas_cur_domain aag s \<and> valid_fault fault \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<And>rv. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P'269 rv\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = NotificationCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ReplyCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = CNodeCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ThreadCap x \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = DomainCap \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQControlCap \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQHandlerCap x \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = Zombie x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ArchObjectCap x \<longrightarrow> True))\<rbrace>, -
 4. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l ?P'2 (liftE (thread_get tcb_fault_handler thread))
 5. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P''2\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>rv s. ((pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and K (is_subject aag thread)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>x. ?P250 rv x s) \<and> (\<forall>x xa xb xc. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xd. ?P264 rv x xa xb xc xd s)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xc. ?P277 rv x xa xb xc s)) \<and> ?P'269 rv s\<rbrace>, -
 6. \<And>s. \<lbrakk>is_subject aag thread \<and> valid_fault fault; (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv x xa xb cap. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P277 rv x xa xb cap\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> pas_cur_domain aag s \<and> valid_fault fault \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 2. \<And>rv. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P'269 rv\<rbrace> lookup_slot_for_thread thread rv \<lbrace>\<lambda>rv s. (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = NotificationCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ReplyCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = CNodeCap x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ThreadCap x \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = DomainCap \<longrightarrow> True)) \<and> (pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQControlCap \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = IRQHandlerCap x \<longrightarrow> True)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = Zombie x xa xb \<longrightarrow> True)) \<and> (\<forall>x. pas_refined aag s \<and> is_subject aag (fst (fst rv)) \<and> (\<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> cap = ArchObjectCap x \<longrightarrow> True))\<rbrace>, -
 3. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> reads_respects aag l ?P'2 (liftE (thread_get tcb_fault_handler thread))
 4. is_subject aag thread \<and> valid_fault fault \<Longrightarrow> \<lbrace>?P''2\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>rv s. ((pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and K (is_subject aag thread)) s) \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>x. ?P250 rv x s) \<and> (\<forall>x xa xb xc. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xd. ?P264 rv x xa xb xc xd s)) \<and> (\<forall>x xa xb. pas_refined aag s \<and> (pas_refined aag and K (is_subject aag thread)) s \<and> (\<forall>xc. ?P277 rv x xa xb xc s)) \<and> ?P'269 rv s\<rbrace>, -
 5. \<And>s. \<lbrakk>is_subject aag thread \<and> valid_fault fault; (invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal:
No subgoals!