theory Syscall_AI

lemma hinv_invs':
  fixes Q :: "'state_ext state \<Rightarrow> bool" and calling blocking
  assumes perform_invocation_Q[wp]:
    "\<And>block class i.
      \<lbrace>invs and Q and ct_active and valid_invocation i\<rbrace>
        perform_invocation block class i
      \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes handle_fault_Q[wp]:
    "\<And>t f.
      \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>_. valid_fault f)\<rbrace>
        handle_fault t f
      \<lbrace>\<lambda>r. Q\<rbrace>"
  assumes reply_from_kernel_Q[wp]:
    "\<And>a b. \<lbrace>invs and Q\<rbrace> reply_from_kernel a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes sts_Q[wp]:
    "\<And>a b. \<lbrace>invs and Q\<rbrace> set_thread_state a b \<lbrace>\<lambda>_.Q\<rbrace>"
  shows
    "\<lbrace>invs and Q and ct_active\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>" apply (simp add: handle_invocation_def ts_Restart_case_helper split_def
                   liftE_liftM_liftME liftME_def bindE_assoc) apply (wp syscall_valid sts_invs_minor2 rfk_invs
            hoare_vcg_all_lift hoare_vcg_disj_lift | simp split del: if_split)+ apply (rule_tac Q = "\<lambda>st. st_tcb_at ((=) st) thread and (invs and Q)" in
         hoare_post_imp) apply (auto elim!: pred_tcb_weakenE st_tcb_ex_cap
              dest: st_tcb_at_idle_thread
              simp: st_tcb_at_tcb_at)[1] apply (rule gts_sp) apply wp apply (simp add: ct_in_state_def conj_commute conj_left_commute) apply wp apply (rule_tac Q = "\<lambda>rv s. st_tcb_at active thread s \<and> cur_thread s = thread" in
         hoare_post_imp) apply simp apply (wp sts_st_tcb_at') apply (simp only: simp_thms K_def if_apply_def2) apply (rule hoare_vcg_E_elim) apply (wp | simp add: if_apply_def2)+ apply (auto simp: ct_in_state_def elim: st_tcb_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and Q and ct_active\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and Q and ct_active\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
x <- liftE (as_user thread (getRegister cap_register));
syscall (doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
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 blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args (to_bl x) (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (do state <- get_thread_state thread;
if state = Restart then do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od else return ()
od)
odE)
odE \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>thread info x rv reply. \<lbrace>?B19 thread info x rv () reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>state s. (state = Restart \<longrightarrow> (if calling then \<lambda>s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {} \<and> st' \<noteq> BlockedOnReply) thread s \<and> invs s \<and> tcb_at thread s \<and> ex_nonz_cap_to thread s \<and> thread \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) \<and> invs s \<and> tcb_at thread s \<and> invs s \<and> Q s else (\<lambda>s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {} \<and> st' \<noteq> BlockedOnReply) thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> thread \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) \<and> invs s \<and> Q s)) s) \<and> (state \<noteq> Restart \<longrightarrow> invs s \<and> Q s)\<rbrace>
 2. \<And>thread info x rv y. \<lbrace>?B18 thread info x rv y\<rbrace> perform_invocation blocking calling rv \<lbrace>?B19 thread info x rv y\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 3. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B18 thread info x rv\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 4. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 5. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 9. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>thread info x rv reply rva s. (st_tcb_at ((=) rva) thread and (invs and Q)) s \<Longrightarrow> (rva = Restart \<longrightarrow> (if calling then \<lambda>s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {} \<and> st' \<noteq> BlockedOnReply) thread s \<and> invs s \<and> tcb_at thread s \<and> ex_nonz_cap_to thread s \<and> thread \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) \<and> invs s \<and> tcb_at thread s \<and> invs s \<and> Q s else (\<lambda>s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {} \<and> st' \<noteq> BlockedOnReply) thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> thread \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) \<and> invs s \<and> Q s)) s) \<and> (rva \<noteq> Restart \<longrightarrow> invs s \<and> Q s)
 2. \<And>thread info x rv reply. \<lbrace>?B19 thread info x rv () reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>st. st_tcb_at ((=) st) thread and (invs and Q)\<rbrace>
 3. \<And>thread info x rv y. \<lbrace>?B18 thread info x rv y\<rbrace> perform_invocation blocking calling rv \<lbrace>?B19 thread info x rv y\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 4. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B18 thread info x rv\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 6. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 7. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 8. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 9. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 10. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread info x rv reply. \<lbrace>?B19 thread info x rv () reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>st. st_tcb_at ((=) st) thread and (invs and Q)\<rbrace>
 2. \<And>thread info x rv y. \<lbrace>?B18 thread info x rv y\<rbrace> perform_invocation blocking calling rv \<lbrace>?B19 thread info x rv y\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 3. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B18 thread info x rv\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 4. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 5. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 9. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>thread info x rv y. \<lbrace>?B18 thread info x rv y\<rbrace> perform_invocation blocking calling rv \<lbrace>\<lambda>a. invs and Q\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B18 thread info x rv\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 3. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 8. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>\<lambda>y s. (invs and ct_active and valid_invocation rv) s \<and> (invs and Q and ct_active and valid_invocation rv) s \<and> (invs and ct_active and valid_invocation rv) s \<and> (invs and Q and ct_active and valid_invocation rv) s\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P_no_err9 thread info x rv\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>y s. invs s \<and> Q s \<and> valid_invocation rv s \<and> st_tcb_at active (cur_thread s) s\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P'171 thread info x rv\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>rv s. st_tcb_at active (cur_thread s) s\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> ?P'171 thread info x rv s\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>thread info x rv rva s. st_tcb_at active thread s \<and> cur_thread s = thread \<Longrightarrow> st_tcb_at active (cur_thread s) s
 2. \<And>thread info x rv. \<lbrace>?P'171 thread info x rv\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>rv s. st_tcb_at active thread s \<and> cur_thread s = thread\<rbrace>
 3. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> ?P'171 thread info x rv s\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 8. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P'171 thread info x rv\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>rv s. st_tcb_at active thread s \<and> cur_thread s = thread\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> ?P'171 thread info x rv s\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> K (active Restart) s \<and> cur_thread s = thread\<rbrace>, \<lbrace>\<lambda>err. if calling then \<lambda>s. (invs and tcb_at thread) s \<and> (invs and Q) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 2. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 4. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P_no_flt9 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> cur_thread s = thread\<rbrace>, \<lbrace>\<lambda>err x. (calling \<longrightarrow> (invs and tcb_at thread) x \<and> (invs and Q) x) \<and> (\<not> calling \<longrightarrow> invs x \<and> Q x)\<rbrace>
 2. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 3. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 4. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info x rv. \<lbrace>?P181 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE -, \<lbrace>\<lambda>err x. (calling \<longrightarrow> (invs and tcb_at thread) x \<and> (invs and Q) x) \<and> (\<not> calling \<longrightarrow> invs x \<and> Q x)\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P'181 thread info x rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args (to_bl x) (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>\<lambda>rv s. (st_tcb_at active thread and invs and ex_nonz_cap_to thread) s \<and> (invs and Q) s \<and> valid_invocation rv s \<and> cur_thread s = thread\<rbrace>, -
 3. \<And>thread info x. \<lbrace>?B8 thread info x\<rbrace> doE p <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rv s. ?P181 thread info x rv s \<and> ?P'181 thread info x rv s\<rbrace>, \<lbrace>\<lambda>ft. if blocking then \<lambda>s. (invs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s \<and> (invs and Q and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault ft)) s else (\<lambda>s. invs s \<and> Q s)\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE (gets cur_thread) \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 7. \<And>s. (invs and Q and ct_active) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> Q s \<and> ct_active s \<Longrightarrow> (blocking \<longrightarrow> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s) \<and> (calling \<longrightarrow> tcb_at (cur_thread s) s) \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s proof (prove)
goal:
No subgoals!