theory Syscall_S

lemma send_fault_ipc_bisim:
  "bisim (=) \<top> (tcb_at tcb and valid_objs and separate_state)
   (set_thread_state tcb Inactive) (send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt')" unfolding send_fault_ipc_def apply (rule bisim_guard_imp) apply (rule bisim_catch_faults_r [where S = "separate_state and valid_objs"]) apply (clarsimp simp: handle_double_fault_def) apply (rule bisim_refl') apply (simp add: Let_def) apply (rule hoare_vcg_seqE) apply (rule hoare_vcg_seqE) apply (wpc; wp) apply wp apply simp apply (rule hoare_post_imp_R [OF lc_sep]) apply (clarsimp simp: separate_cap_def) apply (wp | simp add: Let_def)+ apply (rule_tac P = "separate_cap handler_cap" in hoare_gen_asmE') apply (erule separate_capE, simp_all)[1] apply (wp | simp)+ apply (wp not_empty_lc) apply (rule_tac P = "separate_cap xa" in not_empty_gen_asm) apply (erule separate_capE, simp_all)[1] apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (tcb_at tcb and valid_objs and separate_state) (set_thread_state tcb Inactive) (send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt') proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (tcb_at tcb and valid_objs and separate_state) (set_thread_state tcb Inactive) (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE <catch> handle_double_fault tcb flt') proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?Q' (set_thread_state tcb Inactive) (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE <catch> handle_double_fault tcb flt')
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>x. bisim (=) ?Q (?P'4 x) (set_thread_state tcb Inactive) (handle_double_fault tcb flt' x)
 2. \<lbrace>separate_state and valid_objs\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>?P'4\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>x. bisim (=) ?Q (?P'4 x) (set_thread_state tcb Inactive) (set_thread_state tcb Inactive)
 2. \<lbrace>separate_state and valid_objs\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>?P'4\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler tcb);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap tcb handler_cptr);
case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr. \<lbrace>?B13 handler_cptr\<rbrace> doE handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap tcb handler_cptr);
case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (7 subgoals):
 1. \<And>handler_cptr handler_cap. \<lbrace>?B16 handler_cptr handler_cap\<rbrace> case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>handler_cptr. \<lbrace>?B13 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap tcb handler_cptr) \<lbrace>?B16 handler_cptr\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 5. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 6. \<And>s. True \<Longrightarrow> True
 7. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr. \<lbrace>?B13 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap tcb handler_cptr) \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb xc. handler_cap = UntypedCap x xa xb xc \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = EndpointCap x xa xb \<longrightarrow> True \<and> False) \<and> (\<forall>x xa xb. handler_cap = NotificationCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = ReplyCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = CNodeCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = ThreadCap x \<longrightarrow> True \<and> True) \<and> (handler_cap = DomainCap \<longrightarrow> True \<and> True) \<and> (handler_cap = IRQControlCap \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = IRQHandlerCap x \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = Zombie x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = ArchObjectCap x \<longrightarrow> True \<and> True)\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr. \<lbrace>?P'168 handler_cptr\<rbrace> lookup_cap tcb handler_cptr \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb xc. handler_cap = UntypedCap x xa xb xc \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = EndpointCap x xa xb \<longrightarrow> True \<and> False) \<and> (\<forall>x xa xb. handler_cap = NotificationCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = ReplyCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = CNodeCap x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = ThreadCap x \<longrightarrow> True \<and> True) \<and> (handler_cap = DomainCap \<longrightarrow> True \<and> True) \<and> (handler_cap = IRQControlCap \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = IRQHandlerCap x \<longrightarrow> True \<and> True) \<and> (\<forall>x xa xb. handler_cap = Zombie x xa xb \<longrightarrow> True \<and> True) \<and> (\<forall>x. handler_cap = ArchObjectCap x \<longrightarrow> True \<and> True)\<rbrace>, -
 2. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>\<lambda>handler_cptr s. True \<and> ?P'168 handler_cptr s\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr. \<lbrace>?P'168 handler_cptr\<rbrace> lookup_cap tcb handler_cptr \<lbrace>\<lambda>handler_cap s. \<forall>x xa xb. handler_cap \<noteq> EndpointCap x xa xb\<rbrace>, -
 2. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>\<lambda>handler_cptr s. True \<and> ?P'168 handler_cptr s\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>handler_cptr rv s. separate_cap rv \<Longrightarrow> \<forall>x xa xb. rv \<noteq> EndpointCap x xa xb
 2. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>\<lambda>handler_cptr s. True \<and> (separate_state and valid_objs) s\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>separate_state and valid_objs\<rbrace> liftE (thread_get tcb_fault_handler tcb) \<lbrace>\<lambda>handler_cptr s. True \<and> (separate_state and valid_objs) s\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s. \<lbrace>?S'4 and (=) s\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (7 subgoals):
 1. \<And>s handler_cptr handler_cap. \<lbrace>?B196 s handler_cptr handler_cap\<rbrace> case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. (=) s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<And>s handler_cptr. \<lbrace>?B195 s handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr \<lbrace>?B196 s handler_cptr\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. \<And>s. \<lbrace>?Q193 s\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>?B195 s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. \<And>s sa. (?S'4 and (=) s) sa \<Longrightarrow> ?Q193 s sa
 5. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 6. \<And>s. True \<Longrightarrow> True
 7. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (7 subgoals):
 1. \<And>s handler_cptr handler_cap. separate_cap handler_cap \<Longrightarrow> \<lbrace>?P'198 s handler_cptr handler_cap\<rbrace> case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. (=) s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<And>s handler_cptr. \<lbrace>?B195 s handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr \<lbrace>\<lambda>handler_cap. ?P'198 s handler_cptr handler_cap and K (separate_cap handler_cap)\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. \<And>s. \<lbrace>?Q193 s\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>?B195 s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. \<And>s sa. (?S'4 and (=) s) sa \<Longrightarrow> ?Q193 s sa
 5. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 6. \<And>s. True \<Longrightarrow> True
 7. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (8 subgoals):
 1. \<And>s handler_cptr. \<lbrace>?P'198 s handler_cptr NullCap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. (=) s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<And>s handler_cptr handler_cap ptr badge rights. handler_cap = NotificationCap ptr badge rights \<Longrightarrow> \<lbrace>?P'198 s handler_cptr (NotificationCap ptr badge rights)\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>_. (=) s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 3. \<And>s handler_cptr. \<lbrace>?B195 s handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr \<lbrace>\<lambda>handler_cap. ?P'198 s handler_cptr handler_cap and K (separate_cap handler_cap)\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 4. \<And>s. \<lbrace>?Q193 s\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>?B195 s\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>
 5. \<And>s sa. (?S'4 and (=) s) sa \<Longrightarrow> ?Q193 s sa
 6. not_empty ?Pd4 (doE handler_cptr <- liftE $ thread_get tcb_fault_handler tcb;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tcb handler_cptr;
let f = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tcb (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE)
 7. \<And>s. True \<Longrightarrow> True
 8. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and ?S'4 and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>x. not_empty (?Pa257 x) (lookup_cap tcb x)
 2. \<And>x xa. not_empty (?Pb257 x xa) (let f = CapFault (of_bl x) False (MissingCapability 0) in case xa of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge xa) (AllowGrant \<in> rights) True tcb (cap_ep_ptr xa)
od else throwError f | _ \<Rightarrow> throwError f)
 3. \<And>x. \<lbrace>?Pb'257 x\<rbrace> cap_fault_on_failure (of_bl x) False $ lookup_cap tcb x \<lbrace>?Pb257 x\<rbrace>, -
 4. \<lbrace>?Pb'250\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>\<lambda>x. ?Pa257 x and ?Pb'257 x\<rbrace>, -
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and (\<lambda>s. separate_state s \<and> valid_objs s) and (tcb_at tcb and ?Pb'250)) s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. not_empty (?Pb257 x xa) (let f = CapFault (of_bl x) False (MissingCapability 0) in case xa of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge xa) (AllowGrant \<in> rights) True tcb (cap_ep_ptr xa)
od else throwError f | _ \<Rightarrow> throwError f)
 2. \<And>x. \<lbrace>?Pb'257 x\<rbrace> cap_fault_on_failure (of_bl x) False $ lookup_cap tcb x \<lbrace>?Pb257 x\<rbrace>, -
 3. \<lbrace>?Pb'250\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>\<lambda>x. tcb_at tcb and valid_objs and separate_state and ?Pb'257 x\<rbrace>, -
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and (\<lambda>s. separate_state s \<and> valid_objs s) and (tcb_at tcb and ?Pb'250)) s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. separate_cap xa \<Longrightarrow> not_empty (?R265 x xa) (let f = CapFault (of_bl x) False (MissingCapability 0) in case xa of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some flt')) tcb;
send_ipc True True (cap_ep_badge xa) (AllowGrant \<in> rights) True tcb (cap_ep_ptr xa)
od else throwError f | _ \<Rightarrow> throwError f)
 2. \<And>x. \<lbrace>?Pb'257 x\<rbrace> cap_fault_on_failure (of_bl x) False $ lookup_cap tcb x \<lbrace>\<lambda>xa. ?R265 x xa and (\<lambda>_. separate_cap xa)\<rbrace>, -
 3. \<lbrace>?Pb'250\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>\<lambda>x. tcb_at tcb and valid_objs and separate_state and ?Pb'257 x\<rbrace>, -
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and (\<lambda>s. separate_state s \<and> valid_objs s) and (tcb_at tcb and ?Pb'250)) s proof (prove)
goal (6 subgoals):
 1. \<And>x. not_empty (?R265 x NullCap) (throwError (CapFault (of_bl x) False (MissingCapability 0)))
 2. \<And>x xa ptr badge rights. xa = NotificationCap ptr badge rights \<Longrightarrow> not_empty (?R265 x (NotificationCap ptr badge rights)) (throwError (CapFault (of_bl x) False (MissingCapability 0)))
 3. \<And>x. \<lbrace>?Pb'257 x\<rbrace> cap_fault_on_failure (of_bl x) False $ lookup_cap tcb x \<lbrace>\<lambda>xa. ?R265 x xa and (\<lambda>_. separate_cap xa)\<rbrace>, -
 4. \<lbrace>?Pb'250\<rbrace> liftE $ thread_get tcb_fault_handler tcb \<lbrace>\<lambda>x. tcb_at tcb and valid_objs and separate_state and ?Pb'257 x\<rbrace>, -
 5. \<And>s. True \<Longrightarrow> True
 6. \<And>s. (tcb_at tcb and valid_objs and separate_state) s \<Longrightarrow> (separate_state and valid_objs and (\<lambda>s. separate_state s \<and> valid_objs s) and (tcb_at tcb and ?Pb'250)) s proof (prove)
goal:
No subgoals!