theory Ipc_DR

lemma send_fault_ipc_corres:
  "did = thread \<Longrightarrow>
   dcorres (dc\<oplus>dc) \<top>
     (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and
      invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap  s thread = Some etcb) and
      (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs)
     (Endpoint_D.send_fault_ipc did) (Ipc_A.send_fault_ipc thread ft')" apply (simp add:Endpoint_D.send_fault_ipc_def Ipc_A.send_fault_ipc_def) apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) apply (rule_tac P'="(=) s'" in thread_get_corresE[where tcb' = tcb and etcb'=etcb]) apply simp_all prefer 2 apply (rule conjI) apply (simp add:transform_tcb_def) apply (simp add: get_etcb_def) apply (rule corres_guard_imp) apply (rule_tac R' ="\<lambda>rv s. (\<forall>ref badge rights.
                       rv = cap.EndpointCap ref badge rights \<longrightarrow> (ep_at ref s))
      \<and> not_idle_thread (cur_thread s) s
      \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s
      \<and> not_idle_thread thread s" and R= "\<lambda>r. \<top>"
      in corres_splitEE[where r'="\<lambda>x y. x = transform_cap y"]) apply (clarsimp simp: cap_fault_injection) apply (rule dcorres_injection_handler_rhs) apply (rule lookup_cap_corres) apply simp apply (simp add: tcb_fault_handler_length[OF invs_valid_stateI]) apply (simp add: Let_def cap_fault_injection) apply (rule dcorres_expand_pfx) apply (clarsimp split:cap.splits arch_cap.splits simp:transform_cap_def) apply (clarsimp | rule conjI)+ apply (rule corres_guard_imp) apply (rule corres_split[where r'="dc"]) apply (rule thread_set_fault_corres,simp) apply clarsimp apply (rule send_sync_ipc_corres) apply simp+ apply (simp add:not_idle_thread_def) apply wp apply (wps) apply (strengthen invs_valid_stateI) apply (wp abs_typ_at_lifts[OF thread_set_typ_at]
                    thread_set_fault_obj_at thread_set_fault_st_tcb_at thread_set_valid_etcbs_2
                    thread_set_tcb_fault_set_invs)+ apply ((simp add: ko_at_tcb_at not_idle_thread_def)+) apply (clarsimp simp add: st_tcb_at_def invs_def) apply clarsimp apply wp+ apply (rule validE_validE_R) apply (rule hoare_validE_conj) prefer 2 apply wp+ apply (rule hoare_post_imp_R, rule lookup_cap_valid) apply (clarsimp simp: valid_cap_simps) apply clarsimp+ apply (intro conjI; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. did = thread \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) (Endpoint_D.send_fault_ipc did) (Ipc_A.send_fault_ipc thread ft') proof (prove)
goal (1 subgoal):
 1. did = thread \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) (doE tcb <- liftE (get_thread thread);
CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint tcb) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE) (doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (CSpace_A.lookup_cap thread handler_cptr);
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) s) ((=) s') (doE tcb <- liftE (get_thread thread);
CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint tcb) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE) (doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (CSpace_A.lookup_cap thread handler_cptr);
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q3 s s') (?Q'3 s s') (doE tcb <- liftE (get_thread thread);
CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint tcb) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE) (doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (CSpace_A.lookup_cap thread handler_cptr);
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s s' sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'3 s s' sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'\<rbrakk> \<Longrightarrow> thread = thread
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint (?tcb7 s s')) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> True
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; True; (not_idle_thread thread and st_tcb_at active thread and valid_irq_node and invs and ko_at (TCB tcb) thread and (\<lambda>s. ekheap s thread = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ((=) s' and not_idle_thread thread and valid_irq_node and (\<lambda>sa. transform_tcb (machine_state sa) thread tcb etcb = Tcb (?tcb7 s s')) and ko_at (TCB tcb) thread and (\<lambda>s. get_etcb thread s = Some etcb)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint (?tcb7 (transform s') s')) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform sa; not_idle_thread thread sa \<and> st_tcb_at active thread sa \<and> valid_irq_node sa \<and> invs sa \<and> ko_at (TCB tcb) thread sa \<and> ekheap sa thread = Some etcb \<and> not_idle_thread (cur_thread sa) sa \<and> valid_fault ft' \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> transform_tcb (machine_state sa) thread tcb etcb = Tcb (?tcb7 (transform sa) sa) \<and> get_etcb thread sa = Some etcb proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>did = thread; s = transform sa; not_idle_thread thread sa \<and> st_tcb_at active thread sa \<and> valid_irq_node sa \<and> invs sa \<and> ko_at (TCB tcb) thread sa \<and> ekheap sa thread = Some etcb \<and> not_idle_thread (cur_thread sa) sa \<and> valid_fault ft' \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> transform_tcb (machine_state sa) thread tcb etcb = Tcb (?tcb7 (transform sa) sa) \<and> get_etcb thread sa = Some etcb
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint (?tcb7 (transform s') s')) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>did = thread; s = transform sa; not_idle_thread thread sa \<and> st_tcb_at active thread sa \<and> valid_irq_node sa \<and> invs sa \<and> ko_at (TCB tcb) thread sa \<and> ekheap sa thread = Some etcb \<and> not_idle_thread (cur_thread sa) sa \<and> valid_fault ft' \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> transform_tcb (machine_state sa) thread tcb etcb = Tcb (?tcb7 (transform sa) sa)
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform sa; not_idle_thread thread sa \<and> st_tcb_at active thread sa \<and> valid_irq_node sa \<and> invs sa \<and> ko_at (TCB tcb) thread sa \<and> ekheap sa thread = Some etcb \<and> not_idle_thread (cur_thread sa) sa \<and> valid_fault ft' \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> get_etcb thread sa = Some etcb
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint (?tcb7 (transform s') s')) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>did = thread; s = transform sa; not_idle_thread thread sa \<and> st_tcb_at active thread sa \<and> valid_irq_node sa \<and> invs sa \<and> ko_at (TCB tcb) thread sa \<and> ekheap sa thread = Some etcb \<and> not_idle_thread (cur_thread sa) sa \<and> valid_fault ft' \<and> valid_etcbs sa; s' = sa\<rbrakk> \<Longrightarrow> get_etcb thread sa = Some etcb
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((=) s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q12 s s') (?Q'12 s s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>ref badge rights. if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (doE handler_cap <- cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb));
let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ?Q12 s s' sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'12 s s' sa proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?P16 s s') (?P'16 s s') (CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)))
 2. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> (?P16 s s' and ?Q16 s s') sa
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'16 s s' and ?Q'16 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>did = thread; not_idle_thread thread s'; st_tcb_at active thread s'; valid_irq_node s'; invs s'; ko_at (TCB tcb) thread s'; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?P16 (transform s') s') (?P'16 (transform s') s') (CSpace_D.lookup_cap thread (of_bl (tcb_fault_handler tcb))) (injection_handler (CapFault (of_bl (tcb_fault_handler tcb)) False) (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)))
 2. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> (?P16 s s' and ?Q16 s s') sa
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'16 s s' and ?Q'16 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>did = thread; not_idle_thread thread s'; st_tcb_at active thread s'; valid_irq_node s'; invs s'; ko_at (TCB tcb) thread s'; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>a b. a = transform_cap b)) (?P16 (transform s') s') (?P'16 (transform s') s') (CSpace_D.lookup_cap thread (of_bl (tcb_fault_handler tcb))) (CSpace_A.lookup_cap thread (tcb_fault_handler tcb))
 2. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> (?P16 s s' and ?Q16 s s') sa
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'16 s s' and ?Q'16 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>did = thread; not_idle_thread thread s'; st_tcb_at active thread s'; valid_irq_node s'; invs s'; ko_at (TCB tcb) thread s'; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> of_bl (tcb_fault_handler tcb) = of_bl (tcb_fault_handler tcb)
 2. \<And>s'. \<lbrakk>did = thread; not_idle_thread thread s'; st_tcb_at active thread s'; valid_irq_node s'; invs s'; ko_at (TCB tcb) thread s'; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits
 3. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 7. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>did = thread; not_idle_thread thread s'; st_tcb_at active thread s'; valid_irq_node s'; invs s'; ko_at (TCB tcb) thread s'; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits
 2. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref badge rights. rv' = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case rv of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (let f = CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0) in case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError f | _ \<Rightarrow> throwError f)
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' rv rv'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>s. (\<forall>ref. (\<exists>badge rights. rv' = cap.EndpointCap ref badge rights) \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> st_tcb_at active thread s \<and> invs s \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s) (case transform_cap rv' of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' rv rv' sa s'a. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; rv = transform_cap rv'; sa = transform s'a; True; (\<forall>ref. (\<exists>badge rights. rv' = cap.EndpointCap ref badge rights) \<longrightarrow> ep_at ref s'a) \<and> not_idle_thread (cur_thread s'a) s'a \<and> st_tcb_at active thread s'a \<and> invs s'a \<and> ko_at (TCB tcb) thread s'a \<and> valid_etcbs s'a \<and> not_idle_thread thread s'a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) sa) ((=) s'a) (case transform_cap rv' of cdl_cap.EndpointCap ref badge rights \<Rightarrow> if AllowWrite \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True badge (AllowGrant \<in> rights) True thread ref
od else throw | _ \<Rightarrow> throw) (case rv' 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 ft')) thread;
Ipc_A.send_ipc True True (cap_ep_badge rv') (AllowGrant \<in> rights) True thread (cap_ep_ptr rv')
od else throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> (x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od)) \<and> (AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0))))) \<and> ((AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od))
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od)
 2. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 3. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 7. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> dcorres dc (?Q348 s' s'a x31a x32a x33a) (?Q'348 s' s'a x31a x32a x33a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a
od)
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q348 s' s'a x31a x32a x33a s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> ?Q'348 s' s'a x31a x32a x33a s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (12 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> dcorres dc (?P352 s' s'a x31a x32a x33a) (?P'352 s' s'a x31a x32a x33a) (update_thread_fault thread (\<lambda>_. True)) (thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread)
 2. \<And>s' s'a x31a x32a x33a y ya. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R352 s' s'a x31a x32a x33a y) (?R'352 s' s'a x31a x32a x33a ya) (Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a) (Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a)
 3. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q352 s' s'a x31a x32a x33a\<rbrace> update_thread_fault thread (\<lambda>_. True) \<lbrace>?R352 s' s'a x31a x32a x33a\<rbrace>
 4. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>?R'352 s' s'a x31a x32a x33a\<rbrace>
 5. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> (?P352 s' s'a x31a x32a x33a and ?Q352 s' s'a x31a x32a x33a) s
 6. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (?P'352 s' s'a x31a x32a x33a and ?Q'352 s' s'a x31a x32a x33a) s
 7. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 8. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 9. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s' s'a x31a x32a x33a y ya. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R352 s' s'a x31a x32a x33a y) (?R'352 s' s'a x31a x32a x33a ya) (Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a) (Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a)
 2. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q352 s' s'a x31a x32a x33a\<rbrace> update_thread_fault thread (\<lambda>_. True) \<lbrace>?R352 s' s'a x31a x32a x33a\<rbrace>
 3. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>?R'352 s' s'a x31a x32a x33a\<rbrace>
 4. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 5. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'352 s' s'a x31a x32a x33a) s
 6. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 7. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 8. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> dcorres dc (?R352 s' s'a x31a x32a x33a ()) (?R'352 s' s'a x31a x32a x33a ()) (Endpoint_D.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a) (Ipc_A.send_ipc True True x32a (AllowGrant \<in> x33a) True thread x31a)
 2. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q352 s' s'a x31a x32a x33a\<rbrace> update_thread_fault thread (\<lambda>_. True) \<lbrace>?R352 s' s'a x31a x32a x33a\<rbrace>
 3. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>?R'352 s' s'a x31a x32a x33a\<rbrace>
 4. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 5. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'352 s' s'a x31a x32a x33a) s
 6. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 7. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 8. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> x31a = x31a
 2. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> thread = thread
 3. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q352 s' s'a x31a x32a x33a\<rbrace> update_thread_fault thread (\<lambda>_. True) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>a. not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs\<rbrace>
 5. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 6. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'352 s' s'a x31a x32a x33a) s
 7. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 8. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 9. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>a b. not_idle_thread thread b \<and> not_idle_thread (cur_thread b) b \<and> st_tcb_at active thread b \<and> valid_state b \<and> valid_etcbs b\<rbrace>
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'352 s' s'a x31a x32a x33a) s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; thread \<noteq> idle_thread s'; cur_thread s'a \<noteq> idle_thread s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; thread \<noteq> idle_thread s'a; ekheap s' thread = Some etcb; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'352 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>a b. thread \<noteq> idle_thread b \<and> cur_thread b \<noteq> idle_thread b \<and> st_tcb_at active thread b \<and> valid_state b \<and> valid_etcbs b\<rbrace>
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and ?Q'352 s' s'a x31a x32a x33a) s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a. \<lbrakk>did = thread; ep_at x31a s'a; thread \<noteq> idle_thread s'; cur_thread s'a \<noteq> idle_thread s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; thread \<noteq> idle_thread s'a; ekheap s' thread = Some etcb; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?P'365 s' s'a x31a x32a x33a\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>rv s. cur_thread s \<noteq> idle_thread s \<and> st_tcb_at active thread s \<and> valid_state s \<and> valid_etcbs s\<rbrace>
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. thread \<noteq> idle_thread s \<and> ?P'365 s' s'a x31a x32a x33a s)) s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a prev_s. \<lbrakk>did = thread; ep_at x31a s'a; thread \<noteq> idle_thread s'; cur_thread s'a \<noteq> idle_thread s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; thread \<noteq> idle_thread s'a; ekheap s' thread = Some etcb; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?P368 s' s'a x31a x32a x33a prev_s\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>rv s'b. cur_thread prev_s \<noteq> idle_thread prev_s \<and> st_tcb_at active thread s'b \<and> valid_state s'b \<and> valid_etcbs_2 (ekheap prev_s) (kheap s'b)\<rbrace>
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. thread \<noteq> idle_thread s \<and> ?P368 s' s'a x31a x32a x33a s s)) s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s' s'a x31a x32a x33a prev_s. \<lbrakk>did = thread; ep_at x31a s'a; thread \<noteq> idle_thread s'; cur_thread s'a \<noteq> idle_thread s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; thread \<noteq> idle_thread s'a; ekheap s' thread = Some etcb; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> \<lbrace>?P368 s' s'a x31a x32a x33a prev_s\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>r s. cur_thread prev_s \<noteq> idle_thread prev_s \<and> st_tcb_at active thread s \<and> invs s \<and> valid_etcbs_2 (ekheap prev_s) (kheap s)\<rbrace>
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 3. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. thread \<noteq> idle_thread s \<and> ?P368 s' s'a x31a x32a x33a s s)) s
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 5. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 9. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; transform s'a = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q352 s' s'a x31a x32a x33a) s
 2. \<And>s' s'a x31a x32a x33a s. \<lbrakk>did = thread; ep_at x31a s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a; s'a = s\<rbrakk> \<Longrightarrow> (tcb_at thread and not_idle_thread thread and valid_etcbs and (\<lambda>s. thread \<noteq> idle_thread s \<and> cur_thread s \<noteq> idle_thread s \<and> st_tcb_at active thread s \<and> invs s \<and> valid_etcbs s)) s
 3. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 4. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 5. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 8. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; thread \<noteq> idle_thread s'; cur_thread s'a \<noteq> idle_thread s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; thread \<noteq> idle_thread s'a; ekheap s' thread = Some etcb; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; valid_etcbs s'; AllowWrite \<in> x33a; AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a\<rbrakk> \<Longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s'a)) ((=) s'a) (liftE (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od)) (throwError (CapFault (of_bl (tcb_fault_handler tcb)) False (MissingCapability 0)))
 2. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 6. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a x31 x32 x33 x31a x32a x33a. \<lbrakk>did = thread; ep_at x31 s'a; not_idle_thread thread s'; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'; st_tcb_at active thread s'a; valid_irq_node s'; invs s'a; invs s'; ko_at (TCB tcb) thread s'a; ko_at (TCB tcb) thread s'; valid_etcbs s'a; not_idle_thread thread s'a; ekheap s' thread = Some etcb; not_idle_thread (cur_thread s') s'; valid_fault ft'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33a \<longrightarrow> AllowGrant \<notin> x33a \<and> AllowGrantReply \<notin> x33a) \<longrightarrow> AllowWrite \<in> x33a \<and> (AllowGrant \<in> x33a \<or> AllowGrantReply \<in> x33a) \<longrightarrow> x31 = x31a \<and> x32 = x32a \<and> x33 = x33a \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- update_thread_fault thread (\<lambda>_. True);
Endpoint_D.send_ipc True True x32a False True thread x31a
od) (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread;
Ipc_A.send_ipc True True x32a False True thread x31a
od)
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 5. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s s'\<rbrace> CSpace_D.lookup_cap thread (cdl_tcb_fault_endpoint \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op thread (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s s'\<rbrace> cap_fault_on_failure (of_bl (tcb_fault_handler tcb)) False (CSpace_A.lookup_cap thread (tcb_fault_handler tcb)) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?Q16 s s') sa
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and ?Q'16 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, -
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>sa. True \<and> ?P'435 s s' sa)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s) \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>sa. True \<and> ?P'435 s s' sa)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. \<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>sa. True \<and> ?P'435 s s' sa)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'435 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. \<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>sa. True \<and> ?P'435 s s' sa)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'459 s s'\<rbrace> CSpace_A.lookup_cap thread (tcb_fault_handler tcb) \<lbrace>\<lambda>rv s. \<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref s\<rbrace>, -
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True \<and> not_idle_thread (cur_thread sa) sa \<and> (st_tcb_at active thread sa \<and> invs sa) \<and> ko_at (TCB tcb) thread sa \<and> valid_etcbs sa \<and> not_idle_thread thread sa\<rbrakk> \<Longrightarrow> True \<and> ?P'459 s s' sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>s. True \<and> True \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s' rv sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; sa \<turnstile> rv\<rbrakk> \<Longrightarrow> \<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> ep_at ref sa
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True \<and> not_idle_thread (cur_thread sa) sa \<and> (st_tcb_at active thread sa \<and> invs sa) \<and> ko_at (TCB tcb) thread sa \<and> valid_etcbs sa \<and> not_idle_thread thread sa\<rbrakk> \<Longrightarrow> True \<and> valid_objs sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 4. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>s. True \<and> True \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True \<and> not_idle_thread (cur_thread sa) sa \<and> (st_tcb_at active thread sa \<and> invs sa) \<and> ko_at (TCB tcb) thread sa \<and> valid_etcbs sa \<and> not_idle_thread thread sa\<rbrakk> \<Longrightarrow> True \<and> valid_objs sa
 2. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>s. True \<and> True)) sa
 3. \<And>s s' sa. \<lbrakk>did = thread; s = transform s'; not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_irq_node s' \<and> invs s' \<and> ko_at (TCB tcb) thread s' \<and> ekheap s' thread = Some etcb \<and> not_idle_thread (cur_thread s') s' \<and> valid_fault ft' \<and> valid_etcbs s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs and (\<lambda>s. True \<and> True \<and> not_idle_thread (cur_thread s) s \<and> (st_tcb_at active thread s \<and> invs s) \<and> ko_at (TCB tcb) thread s \<and> valid_etcbs s \<and> not_idle_thread thread s)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>did = thread; not_idle_thread thread sa; st_tcb_at active thread sa; valid_irq_node sa; invs sa; ko_at (TCB tcb) thread sa; ekheap sa thread = Some etcb; not_idle_thread (cur_thread sa) sa; valid_fault ft'; valid_etcbs sa\<rbrakk> \<Longrightarrow> valid_global_refs sa \<and> valid_objs sa \<and> valid_idle sa proof (prove)
goal:
No subgoals!