theory Syscall_S

lemma handle_recv_bisim:
  "bisim (=) \<top> (separate_state and cur_tcb and valid_objs) (handle_recv is_blocking) (Syscall_A.handle_recv is_blocking)" unfolding handle_recv_def Syscall_A.handle_recv_def apply (simp add: Let_def) apply (rule bisim_guard_imp_both) apply (rule bisim_split_refl) apply (rule bisim_split_refl) apply (rule bisim_split_catch_req) apply (simp add: cap_fault_injection) apply (rule bisim_injection [OF refl refl, where f' = "(=)"]) apply simp apply (rule bisim_split_reflE) apply (rule_tac cap = rb in bisim_separate_cap_cases) apply (simp, rule bisim_throwError, rule refl)+ apply (simp split del: if_split) apply (rule bisim_refl [where P = \<top> and P' = \<top>]) apply (case_tac rc, simp_all)[1] apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del:  hoare_True_E_R)+ apply (rule handle_fault_bisim) apply (wp get_simple_ko_wp | wpc | simp)+ apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_post_imp_R) prefer 2 apply simp apply (wp | simp add: cur_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.handle_recv is_blocking) (Syscall_A.handle_recv is_blocking) proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
ep_cptr <- liftM data_to_cptr $ as_user thread $ getRegister cap_register;
(cap_fault_on_failure (of_bl ep_cptr) True $ doE ep_cap <- lookup_cap thread ep_cptr;
let flt = throwError $ MissingCapability 0 in case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else flt
odE else flt | _ \<Rightarrow> flt
odE) <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
ep_cptr <- liftM data_to_cptr $ as_user thread $ getRegister cap_register;
(cap_fault_on_failure (of_bl ep_cptr) True $ doE ep_cap <- lookup_cap thread ep_cptr;
let flt = throwError $ MissingCapability 0 in case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od else flt | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else flt
odE else flt | _ \<Rightarrow> flt
odE) <catch> Ipc_A.handle_fault thread
od) proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_A.handle_fault thread
od) proof (prove)
goal (2 subgoals):
 1. bisim (=) ?P ?P' (do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_SA.handle_fault thread
od) (do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_A.handle_fault thread
od)
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>r. bisim (=) (?Q3 r) (?Q'3 r) (do ep_cptr <- liftM to_bl (as_user r (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap r ep_cptr;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_SA.handle_fault r
od) (do ep_cptr <- liftM to_bl (as_user r (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap r ep_cptr;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_A.handle_fault r
od)
 2. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 4. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>r ra. bisim (=) (?Q7 r ra) (?Q'7 r ra) (cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_SA.handle_fault r) (cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> Ipc_A.handle_fault r)
 2. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q7 r\<rbrace>
 3. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 4. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 5. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 6. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>r ra. bisim ((=) \<oplus> (=)) (?Pn11 r ra) (?Q'7 r ra) (cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE)) (cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE))
 2. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 3. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 4. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 5. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 6. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 7. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 8. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>r ra. bisim ((=) \<oplus> (=)) (?Pn11 r ra) (?Q'7 r ra) (injection_handler (CapFault (of_bl ra) True) (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE)) (injection_handler (CapFault (of_bl ra) True) (doE ep_cap <- lookup_cap r ra;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE))
 2. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 3. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 4. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 5. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 6. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 7. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 8. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>r ra ft ft'. ft = ft' \<Longrightarrow> CapFault (of_bl ra) True ft = CapFault (of_bl ra) True ft'
 2. \<And>r ra. bisim ((=) \<oplus> (=)) (?Pn11 r ra) (?Q'7 r ra) (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) (doE ep_cap <- lookup_cap r ra;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE)
 3. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 4. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 5. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 6. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 7. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 8. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 9. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>r ra. bisim ((=) \<oplus> (=)) (?Pn11 r ra) (?Q'7 r ra) (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) (doE ep_cap <- lookup_cap r ra;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE)
 2. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 3. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 4. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 5. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 6. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 7. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 8. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (12 subgoals):
 1. \<And>r ra rb. bisim ((=) \<oplus> (=)) (?Q18 r ra rb) (?Q'18 r ra rb) (case rb of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)) (case rb of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r rb is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0))
 2. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>?Q18 r ra\<rbrace>, -
 3. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>?Q'18 r ra\<rbrace>, -
 4. \<And>r ra e. e = e
 5. \<And>r ra rb. rb = rb
 6. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 7. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 8. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 9. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 10. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>r ra rb. rb = NullCap \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pn24 r ra rb) (?Pn'24 r ra rb) (case rb of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)) (case rb of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r rb is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0))
 2. \<And>r ra rb ptr badge rights. rb = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa24 r ra rb ptr badge rights) (?Pa'24 r ra rb ptr badge rights) (case rb of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)) (case rb of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r rb is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0))
 3. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb s. (rb = NullCap \<longrightarrow> ?Pn24 r ra rb s) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa24 r ra rb ptr badge rights s)\<rbrace>, -
 4. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb. (\<lambda>s. (rb = NullCap \<longrightarrow> ?Pn'24 r ra rb s) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa'24 r ra rb ptr badge rights s)) and K (separate_cap rb)\<rbrace>, -
 5. \<And>r ra e. e = e
 6. \<And>r ra rb. rb = rb
 7. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 8. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 9. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 10. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>r ra rb ptr badge rights. rb = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa24 r ra rb ptr badge rights) (?Pa'24 r ra rb ptr badge rights) (case rb of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)) (case rb of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap r;
receive_ipc r rb is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0))
 2. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa24 r ra rb ptr badge rights s)\<rbrace>, -
 3. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb. (\<lambda>s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa'24 r ra rb ptr badge rights s)) and K (separate_cap rb)\<rbrace>, -
 4. \<And>r ra e. e = e
 5. \<And>r ra rb. rb = rb
 6. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 7. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 8. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 9. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 10. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>r ra rb ptr badge rights. rb = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa24 r ra (NotificationCap ptr badge rights) ptr badge rights) (?Pa'24 r ra (NotificationCap ptr badge rights) ptr badge rights) (if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ptr;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0)) (if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ptr;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r rb is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0))
 2. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa24 r ra rb ptr badge rights s)\<rbrace>, -
 3. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb. (\<lambda>s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> ?Pa'24 r ra rb ptr badge rights s)) and K (separate_cap rb)\<rbrace>, -
 4. \<And>r ra e. e = e
 5. \<And>r ra rb. rb = rb
 6. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 7. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 8. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 9. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 10. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>r ra rb ptr badge rights rc. rb = NotificationCap ptr badge rights \<Longrightarrow> ((=) \<oplus> (=)) rc rc
 2. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> True)\<rbrace>, -
 3. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb. (\<lambda>s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> True)) and K (separate_cap rb)\<rbrace>, -
 4. \<And>r ra e. e = e
 5. \<And>r ra rb. rb = rb
 6. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 7. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 8. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 9. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 10. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>r ra. \<lbrace>?Pn11 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> True)\<rbrace>, -
 2. \<And>r ra. \<lbrace>?Q'7 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>rb. (\<lambda>s. (rb = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. rb = NotificationCap ptr badge rights \<longrightarrow> True)) and K (separate_cap rb)\<rbrace>, -
 3. \<And>r ra e. e = e
 4. \<And>r ra rb. rb = rb
 5. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 6. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 7. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. ?Pn11 r ra and ?P11 r ra\<rbrace>
 8. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>?Q'7 r\<rbrace>
 9. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 10. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
A total of 11 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>r ra x. bisim (=) (?Pf11 r ra x) (?Pf'11 r ra x) (Ipc_SA.handle_fault r x) (Ipc_A.handle_fault r x)
 2. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rb. ?Pf11 r ra rb and ?Pf'11 r ra rb\<rbrace>
 3. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and ?P11 r ra\<rbrace>
 4. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 5. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 6. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 7. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>r ra. \<lbrace>?P11 r ra\<rbrace> cap_fault_on_failure (of_bl ra) True (doE ep_cap <- lookup_cap r ra;
case ep_cap of NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some r \<or> boundTCB = None then liftE $ receive_signal r ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ra. (\<lambda>_. True) and (separate_state and tcb_at r and valid_objs)\<rbrace>
 2. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and ?P11 r ra\<rbrace>
 3. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 4. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 5. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 6. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>r ra. \<lbrace>?P'323 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>ep_cap s. (ep_cap = NullCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb xc. ep_cap = UntypedCap x xa xb xc) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. ep_cap = EndpointCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (\<forall>x xa xb. ep_cap = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some r \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> (AllowRecv \<notin> xb \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> ((\<exists>x xa xb. ep_cap = ReplyCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. ep_cap = CNodeCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. ep_cap = ThreadCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (ep_cap = DomainCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (ep_cap = IRQControlCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. ep_cap = IRQHandlerCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. ep_cap = Zombie x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. ep_cap = ArchObjectCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)\<rbrace>, -
 2. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and (\<lambda>s. True \<and> separate_state s \<and> tcb_at r s \<and> valid_objs s \<and> ?P'323 r ra s)\<rbrace>
 3. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 4. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 5. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 6. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>r ra. \<lbrace>?P'323 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>_. separate_state and valid_objs and tcb_at r\<rbrace>, -
 2. \<And>r ra rv s. (separate_state and valid_objs and tcb_at r) s \<Longrightarrow> (rv = NullCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some r \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> (AllowRecv \<notin> xb \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (rv = DomainCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (rv = IRQControlCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = ArchObjectCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)
 3. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and (\<lambda>s. True \<and> separate_state s \<and> tcb_at r s \<and> valid_objs s \<and> ?P'323 r ra s)\<rbrace>
 4. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 5. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 6. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 7. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>r ra rv s. (separate_state and valid_objs and tcb_at r) s \<Longrightarrow> (rv = NullCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> ntfn_bound_tcb ntfn \<noteq> Some r \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> (AllowRecv \<notin> xb \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (rv = DomainCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> (rv = IRQControlCap \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s) \<and> ((\<exists>x. rv = ArchObjectCap x) \<longrightarrow> separate_state s \<and> tcb_at r s \<and> valid_objs s)
 2. \<And>r ra. \<lbrace>?P'323 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>_. separate_state and valid_objs and tcb_at r\<rbrace>, -
 3. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and (\<lambda>s. True \<and> separate_state s \<and> tcb_at r s \<and> valid_objs s \<and> ?P'323 r ra s)\<rbrace>
 4. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 5. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 6. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 7. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (6 subgoals):
 1. \<And>r ra. \<lbrace>?P'323 r ra\<rbrace> lookup_cap r ra \<lbrace>\<lambda>_. separate_state and valid_objs and tcb_at r\<rbrace>, -
 2. \<And>r. \<lbrace>?Q3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra. (\<lambda>_. True) and (\<lambda>s. True \<and> separate_state s \<and> tcb_at r s \<and> valid_objs s \<and> ?P'323 r ra s)\<rbrace>
 3. \<And>r. \<lbrace>?Q'3 r\<rbrace> liftM to_bl (as_user r (getRegister cap_register)) \<lbrace>\<lambda>ra s. True \<and> (separate_state and valid_objs) s\<rbrace>
 4. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?Q3\<rbrace>
 5. \<lbrace>?P'\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 6. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal:
No subgoals!