theory Ipc_AC

lemma send_fault_ipc_integrity_autarch:
  "\<lbrace>pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread
                    and K (valid_fault fault) and K (is_subject aag thread)\<rbrace>
   send_fault_ipc thread fault
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp add: send_fault_ipc_def Let_def) apply (wp send_ipc_integrity_autarch thread_set_integrity_autarch thread_set_fault_pas_refined
            thread_set_valid_objs'' thread_set_refs_trivial thread_set_tcb_fault_update_valid_mdb
            thread_set_tcb_fault_set_invs
         | wpc | simp add: is_obj_defs)+ 
  (* 14 subgoals *)
   apply (rename_tac word1 word2 set) apply (rule_tac R="\<lambda>rv s. ep_at word1 s" in hoare_post_add) apply (simp only: obj_at_conj_distrib[symmetric] flip: conj_assoc) apply (wp thread_set_obj_at_impossible thread_set_tcb_fault_set_invs
            get_cap_auth_wp[where aag=aag]
         | simp add: lookup_cap_def is_obj_defs split_def)+ 
    (* down to 3 : normal indentation *)
     apply (rule_tac Q'="\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s
                          \<and> invs s
                          \<and> valid_fault fault
                          \<and> is_subject aag (cur_thread s)
                          \<and> is_subject aag (fst (fst rv))"
               in hoare_post_imp_R[rotated]) apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state obj_at_def) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_def  is_ep aag_cap_auth_def cap_auth_conferred_def
                           cap_rights_to_auth_def AllowSend_def
                    elim!: obj_atE) apply (intro conjI; fastforce ?) apply (clarsimp simp: ep_q_refs_of_def split: endpoint.splits) apply (frule(1) pas_refined_ep_recv, simp add: obj_at_def,assumption) apply (frule(1) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed,rotated],
            blast) apply (simp add: aag_has_Control_iff_owns) apply (wp lookup_slot_for_thread_authorised)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread and K (valid_fault fault) and K (is_subject aag thread)\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?P'124 handler_cptr (EndpointCap x31 x32 x33) x31 x32 x33\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>rv s. obj_at (\<lambda>ep. AllowGrant \<in> x33 \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) x31 s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag\<rbrace>
 2. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; \<not> (AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> \<lbrace>?R93 handler_cptr handler_cap x31 x32 x33\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>handler_cptr handler_cap x41 x42 x43. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>handler_cptr handler_cap x51 x52 x53. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>handler_cptr handler_cap x61 x62 x63. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>handler_cptr handler_cap x7. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>handler_cptr handler_cap x10. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 10. \<And>handler_cptr handler_cap x111 x112 x113. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap x111 x112 x113\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?P'124 handler_cptr (EndpointCap x31 x32 x33) x31 x32 x33\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>rv s. obj_at (\<lambda>ep. AllowGrant \<in> x33 \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) x31 s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x31) \<in> pasPolicy aag\<rbrace>
 2. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; \<not> (AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> \<lbrace>?R93 handler_cptr handler_cap x31 x32 x33\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>handler_cptr handler_cap x41 x42 x43. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>handler_cptr handler_cap x51 x52 x53. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>handler_cptr handler_cap x61 x62 x63. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>handler_cptr handler_cap x7. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>handler_cptr handler_cap x10. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 10. \<And>handler_cptr handler_cap x111 x112 x113. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap x111 x112 x113\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handler_cap word1 word2 set. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap word1 word2 set; AllowSend \<in> set \<and> (AllowGrant \<in> set \<or> AllowGrantReply \<in> set)\<rbrakk> \<Longrightarrow> \<lbrace>?P'124 handler_cptr (EndpointCap word1 word2 set) word1 word2 set\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>rv s. obj_at (\<lambda>ep. AllowGrant \<in> set \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) word1 s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag word1) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag word1) \<in> pasPolicy aag\<rbrace>
 2. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; \<not> (AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> \<lbrace>?R93 handler_cptr handler_cap x31 x32 x33\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>handler_cptr handler_cap x41 x42 x43. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>handler_cptr handler_cap x51 x52 x53. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>handler_cptr handler_cap x61 x62 x63. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>handler_cptr handler_cap x7. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>handler_cptr handler_cap x10. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 10. \<And>handler_cptr handler_cap x111 x112 x113. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap x111 x112 x113\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handler_cap word1 word2 set. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap word1 word2 set; AllowSend \<in> set \<and> (AllowGrant \<in> set \<or> AllowGrantReply \<in> set)\<rbrakk> \<Longrightarrow> \<lbrace>?P'124 handler_cptr (EndpointCap word1 word2 set) word1 word2 set\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>r s. ep_at word1 s \<and> obj_at (\<lambda>ep. AllowGrant \<in> set \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) word1 s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag word1) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag word1) \<in> pasPolicy aag\<rbrace>
 2. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; \<not> (AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> \<lbrace>?R93 handler_cptr handler_cap x31 x32 x33\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>handler_cptr handler_cap x41 x42 x43. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>handler_cptr handler_cap x51 x52 x53. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>handler_cptr handler_cap x61 x62 x63. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>handler_cptr handler_cap x7. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>handler_cptr handler_cap x10. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 10. \<And>handler_cptr handler_cap x111 x112 x113. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap x111 x112 x113\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handler_cap word1 word2 set. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap word1 word2 set; AllowSend \<in> set \<and> (AllowGrant \<in> set \<or> AllowGrantReply \<in> set)\<rbrakk> \<Longrightarrow> \<lbrace>?P'124 handler_cptr (EndpointCap word1 word2 set) word1 word2 set\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread \<lbrace>\<lambda>r s. (obj_at (\<lambda>ep. is_ep ep \<and> (AllowGrant \<in> set \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) word1 s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag word1) \<in> pasPolicy aag) \<and> (pasSubject aag, Call, pasObjectAbs aag word1) \<in> pasPolicy aag\<rbrace>
 2. \<And>handler_cptr handler_cap x31 x32 x33. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = EndpointCap x31 x32 x33; \<not> (AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> \<lbrace>?R93 handler_cptr handler_cap x31 x32 x33\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>handler_cptr handler_cap x41 x42 x43. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>handler_cptr handler_cap x51 x52 x53. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>handler_cptr handler_cap x61 x62 x63. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>handler_cptr handler_cap x7. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>handler_cptr handler_cap. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>handler_cptr handler_cap x10. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 10. \<And>handler_cptr handler_cap x111 x112 x113. \<lbrakk>is_subject aag thread; valid_fault fault; handler_cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap x111 x112 x113\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
A total of 14 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. 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 = NullCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> integrity aag X st s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>a. (\<exists>ep. a = Endpoint ep) \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>refs_of a. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) x s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> integrity aag X st s)) \<and> ((\<exists>x xa xb. cap = NotificationCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> integrity aag X st s) \<and> (cap = DomainCap \<longrightarrow> integrity aag X st s) \<and> (cap = IRQControlCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> integrity aag X st s))\<rbrace>, -
 2. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. 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 = NullCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> integrity aag X st s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>a. (\<exists>ep. a = Endpoint ep) \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>refs_of a. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) x s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> integrity aag X st s)) \<and> ((\<exists>x xa xb. cap = NotificationCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> integrity aag X st s) \<and> (cap = DomainCap \<longrightarrow> integrity aag X st s) \<and> (cap = IRQControlCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> integrity aag X st s))\<rbrace>, -
 2. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr rv s. \<lbrakk>is_subject aag thread; valid_fault fault; integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrakk> \<Longrightarrow> 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 = NullCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> integrity aag X st s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> obj_at (\<lambda>a. (\<exists>ep. a = Endpoint ep) \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>refs_of a. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) x s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> integrity aag X st s)) \<and> ((\<exists>x xa xb. cap = NotificationCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> integrity aag X st s) \<and> (cap = DomainCap \<longrightarrow> integrity aag X st s) \<and> (cap = IRQControlCap \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> integrity aag X st s) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> integrity aag X st s))
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); pas_cap_cur_auth aag (EndpointCap x xa xb); AllowSend \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<exists>ko. kheap s x = Some ko \<and> (\<exists>ep. ko = Endpoint ep) \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>refs_of ko. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); pas_cap_cur_auth aag (EndpointCap x xa xb); AllowSend \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; s \<turnstile> EndpointCap x xa xb\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<exists>ko. kheap s x = Some ko \<and> (\<exists>ep. ko = Endpoint ep) \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>refs_of ko. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)))) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb ep. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); AllowWrite \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag; cap_aligned (EndpointCap x xa xb); kheap s x = Some (Endpoint ep); (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>auth\<in>(if AllowRead \<in> xb then {Receive} else {}) \<union> (if AllowGrant \<in> xb then UNIV else {}) \<union> (if AllowGrantReply \<in> xb then {Call} else {}). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x xa xb); cap_links_irq aag (pasSubject aag) (EndpointCap x xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb ep. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); AllowWrite \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag; cap_aligned (EndpointCap x xa xb); kheap s x = Some (Endpoint ep); (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>auth\<in>(if AllowRead \<in> xb then {Receive} else {}) \<union> (if AllowGrant \<in> xb then UNIV else {}) \<union> (if AllowGrantReply \<in> xb then {Call} else {}). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x xa xb); cap_links_irq aag (pasSubject aag) (EndpointCap x xa xb)\<rbrakk> \<Longrightarrow> AllowGrant \<in> xb \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb x3 xc. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); AllowWrite \<in> xb; cap_aligned (EndpointCap x xa xb); kheap s x = Some (Endpoint (RecvEP x3)); \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x xa xb); cap_links_irq aag (pasSubject aag) (EndpointCap x xa xb); AllowGrant \<in> xb; xc \<in> set x3\<rbrakk> \<Longrightarrow> is_subject aag xc
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb x3 xc. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); AllowWrite \<in> xb; cap_aligned (EndpointCap x xa xb); kheap s x = Some (Endpoint (RecvEP x3)); \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x xa xb); cap_links_irq aag (pasSubject aag) (EndpointCap x xa xb); AllowGrant \<in> xb; xc \<in> set x3; (pasObjectAbs aag xc, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag xc
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>a b s x xa xb x3 xc. \<lbrakk>is_subject aag thread; integrity aag X st s; pas_refined aag s; invs s; valid_fault fault; is_subject aag (cur_thread s); is_subject aag a; caps_of_state s (a, b) = Some (EndpointCap x xa xb); AllowWrite \<in> xb; cap_aligned (EndpointCap x xa xb); kheap s x = Some (Endpoint (RecvEP x3)); \<forall>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (EndpointCap x xa xb); cap_links_irq aag (pasSubject aag) (EndpointCap x xa xb); AllowGrant \<in> xb; xc \<in> set x3; (pasObjectAbs aag xc, Receive, pasObjectAbs aag x) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag xc) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag xc
 2. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?P'227 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 2. \<lbrakk>is_subject aag thread; valid_fault fault\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>\<lambda>handler_cptr s. integrity aag X st s \<and> True \<and> pas_refined aag s \<and> ?P'227 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag thread; valid_fault fault; (pas_refined aag and invs and integrity aag X st and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> integrity aag X st s \<and> True \<and> pas_refined aag s \<and> integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> valid_fault fault \<and> is_subject aag (cur_thread s) \<and> (pas_refined aag and K (is_subject aag thread)) s proof (prove)
goal:
No subgoals!