theory Syscall_S

lemma handle_invocation_bisim:
  "bisim (dc \<oplus> (=)) \<top> (separate_state and valid_objs and cur_tcb) (handle_invocation c b) (Syscall_A.handle_invocation c b)" unfolding handle_invocation_def Syscall_A.handle_invocation_def apply (simp add: split_def) apply (rule bisim_guard_imp) apply (rule bisim_split_reflE_dc)+ apply (rule syscall_bisim) apply (rule bisim_split_reflE_dc [where Q = "\<lambda>_. \<top>" and Q' = "\<lambda>_. \<top>"])+ apply (rule bisim_reflE_dc) apply wp+ apply (rule bisim_when [OF _ refl]) apply (rule handle_fault_bisim) apply simp apply (rule bisim_split_reflE_eq) apply (rule decode_invocation_bisim) apply wp+ apply (simp, rule bisim_refl') apply simp apply (rule bisim_split_reflE_dc) apply (rule bisim_splitE_req) apply (rule perform_invocation_bisim) apply simp apply (rule bisim_refl') apply (wp | simp)+ apply (rule decode_separate_inv) apply (wp lec_separate_caps | simp add: cur_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and valid_objs and cur_tcb) (Syscall_SA.handle_invocation c b) (Syscall_A.handle_invocation c b) proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and valid_objs and cur_tcb) (doE thread <- liftE $ gets cur_thread;
info <- without_preemption $ get_message_info thread;
ptr <- without_preemption $ liftM data_to_cptr $ as_user thread $ getRegister cap_register;
syscall (doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False $ lookup_cap_and_slot thread ptr;
buffer <- liftE $ lookup_ipc_buffer False thread;
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when b $ Ipc_SA.handle_fault thread fault) (\<lambda>(slot, cap, extracaps, buffer). doE args <- liftE $ get_mrs thread buffer info;
Decode_SA.decode_invocation (mi_label info) args ptr slot cap extracaps
odE) (\<lambda>err. when c $ reply_from_kernel thread $ msg_from_syscall_error err) (\<lambda>oper. doE without_preemption $ set_thread_state thread Restart;
reply <- Syscall_SA.perform_invocation b c oper;
without_preemption $ do state <- get_thread_state thread;
case state of Restart \<Rightarrow> do when c $ reply_from_kernel thread (0, reply);
set_thread_state thread Running
od | _ \<Rightarrow> return ()
od
odE)
odE) (doE thread <- liftE $ gets cur_thread;
info <- without_preemption $ get_message_info thread;
ptr <- without_preemption $ liftM data_to_cptr $ as_user thread $ getRegister cap_register;
syscall (doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False $ lookup_cap_and_slot thread ptr;
buffer <- liftE $ lookup_ipc_buffer False thread;
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when b $ Ipc_A.handle_fault thread fault) (\<lambda>(slot, cap, extracaps, buffer). doE args <- liftE $ get_mrs thread buffer info;
Decode_A.decode_invocation (mi_label info) args ptr slot cap extracaps
odE) (\<lambda>err. when c $ reply_from_kernel thread $ msg_from_syscall_error err) (\<lambda>oper. doE without_preemption $ set_thread_state thread Restart;
reply <- Syscall_A.perform_invocation b c oper;
without_preemption $ do state <- get_thread_state thread;
case state of Restart \<Rightarrow> do when c $ reply_from_kernel thread (0, reply);
set_thread_state thread Running
od | _ \<Rightarrow> return ()
od
odE)
odE) proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (separate_state and valid_objs and cur_tcb) (doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_SA.handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
Decode_SA.decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- Syscall_SA.perform_invocation b c oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE) (doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_A.handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
Decode_A.decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- Syscall_A.perform_invocation b c oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE) proof (prove)
goal (3 subgoals):
 1. bisim (dc \<oplus> (=)) ?Q ?Q' (doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_SA.handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
Decode_SA.decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- Syscall_SA.perform_invocation b c oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE) (doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_A.handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
Decode_A.decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- Syscall_A.perform_invocation b c oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (separate_state and valid_objs and cur_tcb) s \<Longrightarrow> ?Q' s proof (prove)
goal (9 subgoals):
 1. \<And>r ra rb. bisim (dc \<oplus> (=)) (?Q12 r ra rb) (?Q'12 r ra rb) (syscall (doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_SA.handle_fault r fault)) (\<lambda>p. doE args <- liftE (get_mrs r (snd (snd (snd p))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel r (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c oper;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)) (syscall (doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when b (Ipc_A.handle_fault r fault)) (\<lambda>p. doE args <- liftE (get_mrs r (snd (snd (snd p))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when c (reply_from_kernel r (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c oper;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE))
 2. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>?Q12 r ra\<rbrace>, -
 3. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>?Q'12 r ra\<rbrace>, -
 4. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 5. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
 6. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?Q4\<rbrace>, -
 7. \<lbrace>?Q'\<rbrace> liftE (gets cur_thread) \<lbrace>?Q'4\<rbrace>, -
 8. \<And>s. True \<Longrightarrow> ?Q s
 9. \<And>s. (separate_state and valid_objs and cur_tcb) s \<Longrightarrow> ?Q' s proof (prove)
goal (17 subgoals):
 1. \<And>r ra rb. bisim (?fr16 r ra rb \<oplus> ?r_flt_rel16 r ra rb) (?P16 r ra rb) (?P'16 r ra rb) (doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE) (doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE)
 2. \<And>r ra rb flt flt'. ?fr16 r ra rb flt flt' \<Longrightarrow> bisim (=) (?P_flt16 r ra rb flt) (?P'_flt16 r ra rb flt') (when b (Ipc_SA.handle_fault r flt)) (when b (Ipc_A.handle_fault r flt'))
 3. \<And>r ra rb rv rv'. ?r_flt_rel16 r ra rb rv rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 4. \<And>r ra rb rv rv' err err'. \<lbrakk>?r_flt_rel16 r ra rb rv rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 5. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>?r_flt_rel16 r ra rb rvf rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 6. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 7. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>?P_flt16 r ra rb\<rbrace>
 9. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>?P'_flt16 r ra rb\<rbrace>
 10. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. ?P16 r ra rb and ?Q16 r ra rb\<rbrace>, -
A total of 17 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>r ra rb rc rd re. bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) (returnOk (snd rc, fst rc, re, rd)) (returnOk (snd rc, fst rc, re, rd))
 2. \<And>r ra rb rc rd. \<lbrace>\<lambda>_. True\<rbrace> lookup_extra_caps r rd ra \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. \<And>r ra rb rc rd. \<lbrace>\<lambda>_. True\<rbrace> lookup_extra_caps r rd ra \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. \<And>r ra rb rc. \<lbrace>\<lambda>_. True\<rbrace> liftE (lookup_ipc_buffer False r) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 5. \<And>r ra rb rc. \<lbrace>\<lambda>_. True\<rbrace> liftE (lookup_ipc_buffer False r) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 6. \<And>r ra rb. \<lbrace>?P16 r ra rb\<rbrace> cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 7. \<And>r ra rb. \<lbrace>?P'16 r ra rb\<rbrace> cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 8. \<And>r ra rb flt flt'. dc flt flt' \<Longrightarrow> bisim (=) (?P_flt16 r ra rb flt) (?P'_flt16 r ra rb flt') (when b (Ipc_SA.handle_fault r flt)) (when b (Ipc_A.handle_fault r flt'))
 9. \<And>r ra rb rv rv'. rv = rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 10. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
A total of 23 subgoals... proof (prove)
goal (22 subgoals):
 1. \<And>r ra rb rc rd. \<lbrace>\<lambda>_. True\<rbrace> lookup_extra_caps r rd ra \<lbrace>\<lambda>_ _. True\<rbrace>, -
 2. \<And>r ra rb rc rd. \<lbrace>\<lambda>_. True\<rbrace> lookup_extra_caps r rd ra \<lbrace>\<lambda>_ _. True\<rbrace>, -
 3. \<And>r ra rb rc. \<lbrace>\<lambda>_. True\<rbrace> liftE (lookup_ipc_buffer False r) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 4. \<And>r ra rb rc. \<lbrace>\<lambda>_. True\<rbrace> liftE (lookup_ipc_buffer False r) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 5. \<And>r ra rb. \<lbrace>?P16 r ra rb\<rbrace> cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 6. \<And>r ra rb. \<lbrace>?P'16 r ra rb\<rbrace> cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb) \<lbrace>\<lambda>_ _. True\<rbrace>, -
 7. \<And>r ra rb flt flt'. dc flt flt' \<Longrightarrow> bisim (=) (?P_flt16 r ra rb flt) (?P'_flt16 r ra rb flt') (when b (Ipc_SA.handle_fault r flt)) (when b (Ipc_A.handle_fault r flt'))
 8. \<And>r ra rb rv rv'. rv = rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 9. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 10. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
A total of 22 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r ra rb flt flt'. dc flt flt' \<Longrightarrow> bisim (=) (?P_flt16 r ra rb flt) (?P'_flt16 r ra rb flt') (when b (Ipc_SA.handle_fault r flt)) (when b (Ipc_A.handle_fault r flt'))
 2. \<And>r ra rb rv rv'. rv = rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 3. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 5. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 6. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>?P_flt16 r ra rb\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>?P'_flt16 r ra rb\<rbrace>
 9. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 10. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r ra rb flt flt'. \<lbrakk>dc flt flt'; b\<rbrakk> \<Longrightarrow> bisim (=) (?P77 r ra rb flt) (?P'79 r ra rb flt') (Ipc_SA.handle_fault r flt) (Ipc_A.handle_fault r flt')
 2. \<And>r ra rb rv rv'. rv = rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 3. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 5. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 6. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> ?P77 r ra rb flt s\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> ?P'79 r ra rb flt' s\<rbrace>
 9. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 10. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r ra rb rv rv'. rv = rv' \<Longrightarrow> bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv') (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv') (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE)
 2. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 4. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 5. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 6. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 8. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 9. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 10. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r ra rb rv. bisim (?ser16 r ra rb \<oplus> ?r_err_rel16 r ra rb rv rv) (?P_no_flt16 r ra rb rv) (?P'_no_flt16 r ra rb rv) (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE) (doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE)
 2. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; ?ser16 r ra rb err err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; ?r_err_rel16 r ra rb rvf rvf' rve rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 4. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 5. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 6. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 8. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 9. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 10. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>r ra rb rv rc. bisim ((=) \<oplus> (=)) (?Q83 r ra rb rv rc) (?Q'83 r ra rb rv rc) (Decode_SA.decode_invocation (mi_label ra) rc rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))) (Decode_A.decode_invocation (mi_label ra) rc rb (fst rv) (fst (snd rv)) (fst (snd (snd rv))))
 2. \<And>r ra rb rv. \<lbrace>?P_no_flt16 r ra rb rv\<rbrace> liftE (get_mrs r (snd (snd (snd rv))) ra) \<lbrace>?Q83 r ra rb rv\<rbrace>, -
 3. \<And>r ra rb rv. \<lbrace>?P'_no_flt16 r ra rb rv\<rbrace> liftE (get_mrs r (snd (snd (snd rv))) ra) \<lbrace>?Q'83 r ra rb rv\<rbrace>, -
 4. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; err = err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 5. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 6. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 7. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 9. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 10. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r ra rb rv. \<lbrace>?P_no_flt16 r ra rb rv\<rbrace> liftE (get_mrs r (snd (snd (snd rv))) ra) \<lbrace>\<lambda>rc _. True\<rbrace>, -
 2. \<And>r ra rb rv. \<lbrace>?P'_no_flt16 r ra rb rv\<rbrace> liftE (get_mrs r (snd (snd (snd rv))) ra) \<lbrace>\<lambda>rc. K (separate_cap (fst (snd rv)))\<rbrace>, -
 3. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; err = err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 5. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 6. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P_no_flt16 r ra rb rv and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. ?P'_no_flt16 r ra rb rv and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 9. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 10. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
A total of 16 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>r ra rb rv rv' err err'. \<lbrakk>rv = rv'; err = err'\<rbrakk> \<Longrightarrow> bisim (=) (?P_err16 r ra rb rv err) (?P'_err16 r ra rb rv' err') (when c (reply_from_kernel r (msg_from_syscall_error err))) (when c (reply_from_kernel r (msg_from_syscall_error err')))
 2. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 3. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>?P_err16 r ra rb rv\<rbrace>
 4. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>?P'_err16 r ra rb rv'\<rbrace>
 5. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 6. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 7. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 8. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 9. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 10. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf rve) (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve;
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 2. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 3. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 4. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 5. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 6. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 7. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 8. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 9. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
 10. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?Q4\<rbrace>, -
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P_no_err16 r ra rb rvf' rve') (?P'_no_err16 r ra rb rvf' rve') (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_SA.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE y <- liftE (set_thread_state r Restart);
reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 2. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 3. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 4. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 5. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 6. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 7. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 8. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 9. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
 10. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?Q4\<rbrace>, -
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?Q98 r ra rb rvf rvf' rve rve' rc) (?Q'98 r ra rb rvf rvf' rve rve' rc) (doE reply <- Syscall_SA.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE) (doE reply <- Syscall_A.perform_invocation b c rve';
liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, reply));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
 2. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>?Q98 r ra rb rvf rvf' rve rve'\<rbrace>, -
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P'_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>?Q'98 r ra rb rvf rvf' rve rve'\<rbrace>, -
 4. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 5. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 6. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 8. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 9. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 10. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
A total of 15 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?P102 r ra rb rvf rvf' rve rve' rc) (?Q'98 r ra rb rvf rvf' rve rve' rc) (Syscall_SA.perform_invocation b c rve') (Syscall_A.perform_invocation b c rve')
 2. \<And>r ra rb rvf rvf' rve rve' rc rd. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?Q102 r ra rb rvf rvf' rve rve' rc rd) (?Q'102 r ra rb rvf rvf' rve rve' rc rd) (liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))) (liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())))
 3. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?S102 r ra rb rvf rvf' rve rve' rc\<rbrace> Syscall_SA.perform_invocation b c rve' \<lbrace>\<lambda>rd. ?Q102 r ra rb rvf rvf' rve rve' rc rd and ?Q'102 r ra rb rvf rvf' rve rve' rc rd\<rbrace>, -
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. ?P102 r ra rb rvf rvf' rve rve' rc and ?S102 r ra rb rvf rvf' rve rve' rc\<rbrace>, -
 5. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P'_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>?Q'98 r ra rb rvf rvf' rve rve'\<rbrace>, -
 6. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 7. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 9. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 10. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve' rc rd. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (dc \<oplus> (=)) (?Q102 r ra rb rvf rvf' rve rve' rc rd) (?Q'102 r ra rb rvf rvf' rve rve' rc rd) (liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))) (liftE (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())))
 2. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?S102 r ra rb rvf rvf' rve rve' rc\<rbrace> Syscall_SA.perform_invocation b c rve' \<lbrace>\<lambda>rd. ?Q102 r ra rb rvf rvf' rve rve' rc rd and ?Q'102 r ra rb rvf rvf' rve rve' rc rd\<rbrace>, -
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and ?S102 r ra rb rvf rvf' rve rve' rc\<rbrace>, -
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P'_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and K (separate_inv rve')\<rbrace>, -
 5. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 6. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 9. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 10. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve' rd. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> bisim (=) (?Q102 r ra rb rvf' rvf' rve' rve' () rd) (?Q'102 r ra rb rvf' rvf' rve' rve' () rd) (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ())) (get_thread_state r >>= case_thread_state (return ()) (return ()) (do y <- when c (reply_from_kernel r (0, rd));
set_thread_state r Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
 2. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?S102 r ra rb rvf rvf' rve rve' rc\<rbrace> Syscall_SA.perform_invocation b c rve' \<lbrace>\<lambda>rd. ?Q102 r ra rb rvf rvf' rve rve' rc rd and ?Q'102 r ra rb rvf rvf' rve rve' rc rd\<rbrace>, -
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and ?S102 r ra rb rvf rvf' rve rve' rc\<rbrace>, -
 4. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P'_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and K (separate_inv rve')\<rbrace>, -
 5. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 6. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 8. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 9. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 10. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>r ra rb rvf rvf' rve rve' rc. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?S102 r ra rb rvf rvf' rve rve' rc\<rbrace> Syscall_SA.perform_invocation b c rve' \<lbrace>\<lambda>r. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>, -
 2. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and ?S102 r ra rb rvf rvf' rve rve' rc\<rbrace>, -
 3. \<And>r ra rb rvf rvf' rve rve'. \<lbrakk>rvf = rvf'; rve = rve'\<rbrakk> \<Longrightarrow> \<lbrace>?P'_no_err16 r ra rb rvf' rve'\<rbrace> liftE (set_thread_state r Restart) \<lbrace>\<lambda>rc. (\<lambda>_. True) and K (separate_inv rve')\<rbrace>, -
 4. \<And>r ra rb rv. \<lbrace>?Q_no_flt16 r ra rb rv\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv))) ra);
Decode_SA.decode_invocation (mi_label ra) args rb (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 5. \<And>r ra rb rv'. \<lbrace>?Q'_no_flt16 r ra rb rv'\<rbrace> doE args <- liftE (get_mrs r (snd (snd (snd rv'))) ra);
Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv')))
odE \<lbrace>?P'_no_err16 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>err' _. True\<rbrace>
 6. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 7. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and ?Q'_no_flt16 r ra rb rv\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 8. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 9. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 10. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
A total of 15 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>r ra rb rv' args. \<lbrace>?B147 r ra rb rv' args\<rbrace> Decode_A.decode_invocation (mi_label ra) args rb (fst rv') (fst (snd rv')) (fst (snd (snd rv'))) \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, -
 2. \<And>r ra rb rv'. \<lbrace>?P'145 r ra rb rv'\<rbrace> liftE (get_mrs r (snd (snd (snd rv'))) ra) \<lbrace>?B147 r ra rb rv'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 4. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and (\<lambda>s. True \<and> True \<and> ?P'145 r ra rb rv s)\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 5. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 6. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 7. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 8. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
 9. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?Q4\<rbrace>, -
 10. \<lbrace>?Q'\<rbrace> liftE (gets cur_thread) \<lbrace>?Q'4\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>r ra rb rv'. \<lbrace>?P'145 r ra rb rv'\<rbrace> liftE (get_mrs r (snd (snd (snd rv'))) ra) \<lbrace>\<lambda>args. (\<lambda>_. True) and K ((\<forall>c\<in>set (fst (snd (snd rv'))). separate_cap (fst c)) \<and> separate_cap (fst (snd rv')))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>r ra rb. \<lbrace>?Q16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> True)\<rbrace>, \<lbrace>\<lambda>flt s. b \<longrightarrow> True\<rbrace>
 3. \<And>r ra rb. \<lbrace>?Q'16 r ra rb\<rbrace> doE p <- cap_fault_on_failure (of_bl rb) False (lookup_cap_and_slot r rb);
buffer <- liftE (lookup_ipc_buffer False r);
extracaps <- lookup_extra_caps r buffer ra;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv. K (separate_cap (fst (snd rv))) and (\<lambda>s. True \<and> True \<and> ?P'145 r ra rb rv s)\<rbrace>, \<lbrace>\<lambda>flt' s. b \<longrightarrow> (separate_state and tcb_at r and valid_objs) s\<rbrace>
 4. \<And>r ra. \<lbrace>?Q8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q16 r ra rb\<rbrace>, -
 5. \<And>r ra. \<lbrace>?Q'8 r ra\<rbrace> liftE (liftM to_bl (as_user r (getRegister cap_register))) \<lbrace>\<lambda>rb. (\<lambda>_. True) and ?Q'16 r ra rb\<rbrace>, -
 6. \<And>r. \<lbrace>?Q4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q8 r\<rbrace>, -
 7. \<And>r. \<lbrace>?Q'4 r\<rbrace> liftE (get_message_info r) \<lbrace>?Q'8 r\<rbrace>, -
 8. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?Q4\<rbrace>, -
 9. \<lbrace>?Q'\<rbrace> liftE (gets cur_thread) \<lbrace>?Q'4\<rbrace>, -
 10. \<And>s. True \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal:
No subgoals!