theory Ipc_R

lemma sendFaultIPC_corres:
  "valid_fault f \<Longrightarrow> fr f f' \<Longrightarrow>
  corres (fr \<oplus> dc)
         (einvs and st_tcb_at active thread and ex_nonz_cap_to thread)
         (invs' and sch_act_not thread and tcb_at' thread)
         (send_fault_ipc thread f) (sendFaultIPC thread f')" apply (simp add: send_fault_ipc_def sendFaultIPC_def
                   liftE_bindE Let_def) apply (rule corres_guard_imp) apply (rule corres_split [where r'="\<lambda>fh fh'. fh = to_bl fh'"]) apply (rule threadGet_corres) apply (simp add: tcb_relation_def) apply simp apply (rule corres_splitEE) apply (rule corres_cap_fault) apply (rule lookup_cap_corres, rule refl) apply (rule_tac P="einvs and st_tcb_at active thread
                                and valid_cap handler_cap and ex_nonz_cap_to thread"
                    and P'="invs' and tcb_at' thread and sch_act_not thread
                                  and valid_cap' handlerCap"
                    in corres_inst) apply (case_tac handler_cap,
               simp_all add: isCap_defs lookup_failure_map_def
                             case_bool_If If_rearrage
                  split del: if_split cong: if_cong)[1] apply (rule corres_guard_imp) apply (rule corres_if2 [OF refl]) apply (simp add: dc_def[symmetric]) apply (rule corres_split[OF threadset_corres sendIPC_corres], simp_all)[1] apply (simp add: tcb_relation_def fault_rel_optionation_def exst_same_def)+ apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state
                       thread_set_typ_at ep_at_typ_at ex_nonz_cap_to_pres
                       thread_set_cte_wp_at_trivial thread_set_not_state_valid_sched
                  | simp add: tcb_cap_cases_def)+ apply ((wp threadSet_invs_trivial threadSet_tcb'
                  | simp add: tcb_cte_cases_def
                  | wp (once) sch_act_sane_lift)+)[1] apply (rule corres_trivial, simp add: lookup_failure_map_def) apply (clarsimp simp: st_tcb_at_tcb_at split: if_split) apply (simp add: valid_cap_def) apply (clarsimp simp: valid_cap'_def inQ_def) apply auto[1] apply (clarsimp simp: lookup_failure_map_def) apply wp+ apply (fastforce elim: st_tcb_at_tcb_at) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_fault f; fr f f'\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) (invs' and sch_act_not thread and tcb_at' thread) (send_fault_ipc thread f) (sendFaultIPC thread f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) (invs' and sch_act_not thread and tcb_at' thread) (do handler_cptr <- thread_get tcb_fault_handler thread;
doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE
od) (do handlerCPtr <- threadGet tcbFaultHandler thread;
doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) ?Q1 ?Q'1 (do handler_cptr <- thread_get tcb_fault_handler thread;
doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE
od) (do handlerCPtr <- threadGet tcbFaultHandler thread;
doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE
od)
 2. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> corres (\<lambda>fh fh'. fh = to_bl fh') ?P5 ?P'5 (thread_get tcb_fault_handler thread) (threadGet tcbFaultHandler thread)
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R5 handler_cptr) (?R'5 handlerCPtr) (doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE) (doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE)
 3. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>?R5\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcb'. \<lbrakk>valid_fault f; f' = fault_map f; tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> tcb_fault_handler tcb = to_bl (tcbFaultHandler tcb')
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R5 handler_cptr) (?R'5 handlerCPtr) (doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE) (doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE)
 3. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>?R5\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R5 handler_cptr) (?R'5 handlerCPtr) (doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr);
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE) (doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE)
 2. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>?R5\<rbrace>
 3. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R5 (to_bl handlerCPtr)) (?R'5 handlerCPtr) (doE handler_cap <- cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr));
case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))
odE) (doE handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE)
 2. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>?R5\<rbrace>
 3. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 5. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (fr \<oplus> ?r'13 handler_cptr handlerCPtr) (?P26 (to_bl handlerCPtr)) (?P'23 handlerCPtr) (cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr))) (capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr))
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; ?r'13 handler_cptr handlerCPtr handler_cap handlerCap\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R13 handler_cptr handlerCPtr handler_cap) (?R'13 handler_cptr handlerCPtr handlerCap) (case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>?R13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>?R'13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. ?P26 a and ?Q24 a\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. ?P'23 a and ?Q'21 a\<rbrace>
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> ?r'13 handler_cptr handlerCPtr) (?P26 (to_bl handlerCPtr)) (?P'23 handlerCPtr) (lookup_cap thread (to_bl handlerCPtr)) (lookupCap thread handlerCPtr)
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; ?r'13 handler_cptr handlerCPtr handler_cap handlerCap\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R13 handler_cptr handlerCPtr handler_cap) (?R'13 handler_cptr handlerCPtr handlerCap) (case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>?R13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>?R'13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. ?P26 a and ?Q24 a\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. ?P'23 a and ?Q'21 a\<rbrace>
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; cap_relation handler_cap handlerCap\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (?R13 handler_cptr handlerCPtr handler_cap) (?R'13 handler_cptr handlerCPtr handlerCap) (case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>?R13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>?R'13 handler_cptr handlerCPtr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; cap_relation handler_cap handlerCap\<rbrakk> \<Longrightarrow> corres (fr \<oplus> dc) (einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (case handler_cap of cap.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 f)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0)) | _ \<Rightarrow> throwError (ExceptionTypes_A.fault.CapFault (of_bl handler_cptr) False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then liftE (do y <- thread_set (tcb_fault_update (\<lambda>_. Some f)) thread;
send_ipc True True x32 (AllowGrant \<in> x33) True thread x31
od) else throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then liftE (do y <- threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread;
sendIPC True True x32 (AllowGrant \<in> x33) True thread x31
od) else throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (10 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q43 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'43 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then liftE (do y <- thread_set (tcb_fault_update (\<lambda>_. Some f)) thread;
send_ipc True True x32 (AllowGrant \<in> x33) True thread x31
od) else throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then liftE (do y <- threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread;
sendIPC True True x32 (AllowGrant \<in> x33) True thread x31
od) else throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> ?Q43 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> ?Q'43 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 5. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 8. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 9. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 10. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (11 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?P47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?P'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (liftE (do y <- thread_set (tcb_fault_update (\<lambda>_. Some f)) thread;
send_ipc True True x32 (AllowGrant \<in> x33) True thread x31
od)) (liftE (do y <- threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread;
sendIPC True True x32 (AllowGrant \<in> x33) True thread x31
od))
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then ?P47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then ?P'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 5. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 6. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 9. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 10. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> corres dc (?P47 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33) (?P'47 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some f)) thread;
send_ipc True True x32 (AllowGrant \<in> x33) True thread x31
od) (do y <- threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread;
sendIPC True True x32 (AllowGrant \<in> x33) True thread x31
od)
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then ?P47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then ?P'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 5. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 6. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 9. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 10. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 tcb tcb'. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33); tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_fault := Some f\<rparr>) (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb')
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 tcb'. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> exst_same tcb' (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb')
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?Q79 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some f)) thread \<lbrace>\<lambda>y. einvs and st_tcb_at active thread and ep_at x31 and ex_nonz_cap_to thread\<rbrace>
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33\<rbrace> threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread \<lbrace>\<lambda>y. invs' and sch_act_not thread and tcb_at' thread and ep_at' x31\<rbrace>
 5. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 6. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at thread and ?Q79 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 7. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and ?Q'77 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 8. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 9. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?Q79 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some f)) thread \<lbrace>\<lambda>y. einvs and st_tcb_at active thread and ep_at x31 and ex_nonz_cap_to thread\<rbrace>
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33\<rbrace> threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread \<lbrace>\<lambda>y. invs' and sch_act_not thread and tcb_at' thread and ep_at' x31\<rbrace>
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at thread and ?Q79 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 5. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and ?Q'77 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 6. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 7. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 10. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 (to_bl handlerCPtr) handlerCPtr (cap.EndpointCap x31 x32 x33) (capability.EndpointCap x31 x32 True (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)) x31 x32 x33\<rbrace> threadSet (tcbFault_update (\<lambda>_. Some (fault_map f))) thread \<lbrace>\<lambda>y s. invs' s \<and> sch_act_not thread s \<and> tcb_at' thread s \<and> ep_at' x31 s\<rbrace>
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at thread and (\<lambda>a. invs a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at active thread a \<and> ep_at x31 a \<and> ex_nonz_cap_to thread a) else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and ?Q'77 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 5. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 6. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 9. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 10. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; \<not> (AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33))\<rbrakk> \<Longrightarrow> corres ((\<lambda>a b. b = fault_map a) \<oplus> (\<lambda>a b. True)) (?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (throwError (Fault_H.fault.CapFault handlerCPtr False (Fault_H.lookup_failure.MissingCapability 0)))
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at thread and (\<lambda>a. invs a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at active thread a \<and> ep_at x31 a \<and> ex_nonz_cap_to thread a) else ?Q47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and (\<lambda>a. (invs' a \<and> tcb_at' thread a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> thread \<notin> set (ksReadyQueues a (d, p))) \<and> (\<forall>ko d p. ko_at' ko thread a \<and> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) ko) \<and> \<not> inQ d p ko \<longrightarrow> thread \<in> set (ksReadyQueues a (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> ex_nonz_cap_to' thread a \<and> thread \<noteq> ksCurThread a) \<and> (\<forall>tcb. tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb) \<and> ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> thread \<noteq> ksCurThread a)) \<and> sch_act_not thread a \<and> tcb_at' thread a \<and> ep_at' x31 a) else ?Q'47 handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33) s
 4. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 5. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 8. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 9. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 10. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (einvs and st_tcb_at active thread and valid_cap (cap.EndpointCap x31 x32 x33) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at thread and (\<lambda>a. invs a \<and> valid_list a \<and> valid_sched a \<and> st_tcb_at active thread a \<and> ep_at x31 a \<and> ex_nonz_cap_to thread a) else (\<lambda>_. True)) s
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and (\<lambda>a. (invs' a \<and> tcb_at' thread a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> thread \<notin> set (ksReadyQueues a (d, p))) \<and> (\<forall>ko d p. ko_at' ko thread a \<and> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) ko) \<and> \<not> inQ d p ko \<longrightarrow> thread \<in> set (ksReadyQueues a (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> ex_nonz_cap_to' thread a \<and> thread \<noteq> ksCurThread a) \<and> (\<forall>tcb. tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb) \<and> ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> thread \<noteq> ksCurThread a)) \<and> sch_act_not thread a \<and> tcb_at' thread a \<and> ep_at' x31 a) else (\<lambda>_. True)) s
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 7. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 9. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; invs s; valid_list s; valid_sched s; st_tcb_at active thread s; s \<turnstile> cap.EndpointCap x31 x32 x33; ex_nonz_cap_to thread s; AllowWrite \<in> x33; AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33\<rbrakk> \<Longrightarrow> ep_at x31 s
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and (\<lambda>a. (invs' a \<and> tcb_at' thread a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> thread \<notin> set (ksReadyQueues a (d, p))) \<and> (\<forall>ko d p. ko_at' ko thread a \<and> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) ko) \<and> \<not> inQ d p ko \<longrightarrow> thread \<in> set (ksReadyQueues a (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> ex_nonz_cap_to' thread a \<and> thread \<noteq> ksCurThread a) \<and> (\<forall>tcb. tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb) \<and> ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> thread \<noteq> ksCurThread a)) \<and> sch_act_not thread a \<and> tcb_at' thread a \<and> ep_at' x31 a) else (\<lambda>_. True)) s
 3. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 7. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 9. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x31 x32 x33 s. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; handlerCap = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); handler_cap = cap.EndpointCap x31 x32 x33; (invs' and tcb_at' thread and sch_act_not thread and valid_cap' (capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33))) s\<rbrakk> \<Longrightarrow> (if AllowWrite \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then tcb_at' thread and (\<lambda>a. (invs' a \<and> tcb_at' thread a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> thread \<notin> set (ksReadyQueues a (d, p))) \<and> (\<forall>ko d p. ko_at' ko thread a \<and> inQ d p (tcbFault_update (\<lambda>_. Some (fault_map f)) ko) \<and> \<not> inQ d p ko \<longrightarrow> thread \<in> set (ksReadyQueues a (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb)) \<longrightarrow> ex_nonz_cap_to' thread a \<and> thread \<noteq> ksCurThread a) \<and> (\<forall>tcb. tcbQueued (tcbFault_update (\<lambda>_. Some (fault_map f)) tcb) \<and> ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> thread \<noteq> ksCurThread a)) \<and> sch_act_not thread a \<and> tcb_at' thread a \<and> ep_at' x31 a) else (\<lambda>_. True)) s
 2. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 6. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 8. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>handler_cptr handlerCPtr handler_cap handlerCap x12. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr; \<exists>a'. acap_relation x12 a' \<and> handlerCap = capability.ArchObjectCap a'; handler_cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = fault_map a) \<oplus> (\<lambda>a b. True)) (einvs and st_tcb_at active thread and valid_cap (cap.ArchObjectCap x12) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap) (throwError (ExceptionTypes_A.fault.CapFault handlerCPtr False (ExceptionTypes_A.lookup_failure.MissingCapability 0))) (case handlerCap of capability.EndpointCap epptr x bool1 xa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just (fault_map f))) thread;
sendIPC True True (capEPBadge handlerCap) canGrant True thread (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0)
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>x12 a' s s'. \<lbrakk>valid_fault f; f' = fault_map f; acap_relation x12 a'; invs s; valid_list s; valid_sched s; st_tcb_at active thread s; s \<turnstile> cap.ArchObjectCap x12; ex_nonz_cap_to thread s; invs' s'; tcb_at' thread s'; sch_act_not thread s'; valid_cap' (capability.ArchObjectCap a') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> Fault_H.lookup_failure.MissingCapability 0 = lookup_failure_map (ExceptionTypes_A.lookup_failure.MissingCapability 0)
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 5. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 7. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 (to_bl handlerCPtr)\<rbrace> cap_fault_on_failure handlerCPtr False (lookup_cap thread (to_bl handlerCPtr)) \<lbrace>\<lambda>handler_cap. einvs and st_tcb_at active thread and valid_cap handler_cap and ex_nonz_cap_to thread\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>handler_cptr handlerCPtr. \<lbrakk>valid_fault f; f' = fault_map f; handler_cptr = to_bl handlerCPtr\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 handlerCPtr\<rbrace> capFaultOnFailure handlerCPtr False (lookupCap thread handlerCPtr) \<lbrace>\<lambda>handlerCap. invs' and tcb_at' thread and sch_act_not thread and valid_cap' handlerCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> thread_get tcb_fault_handler thread \<lbrace>\<lambda>a. valid_objs and pspace_aligned and tcb_at thread and ?Q24 a\<rbrace>
 4. \<lbrakk>valid_fault f; f' = fault_map f\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> threadGet tcbFaultHandler thread \<lbrace>\<lambda>a. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and ?Q'21 a\<rbrace>
 5. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q5) s
 6. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (tcb_at thread and (valid_objs and pspace_aligned and tcb_at thread and (\<lambda>a. True \<and> (einvs and st_tcb_at active thread) a \<and> valid_objs a \<and> ex_nonz_cap_to thread a))) s
 2. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (\<lambda>a. True \<and> (invs' and tcb_at' thread and sch_act_not thread) a \<and> valid_objs' a))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_fault f; f' = fault_map f; (invs' and sch_act_not thread and tcb_at' thread) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread and (\<lambda>a. True \<and> (invs' and tcb_at' thread and sch_act_not thread) a \<and> valid_objs' a))) s proof (prove)
goal:
No subgoals!