theory DetSchedSchedule_AI

lemma do_reply_transfer_valid_sched[wp]:
  "\<lbrace>valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot
       and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: do_reply_transfer_def) apply (wp set_thread_state_not_runnable_valid_sched sts_st_tcb_at'
            cap_delete_one_reply_st_tcb_at do_ipc_transfer_non_null_cte_wp_at2
            thread_set_not_state_valid_sched thread_set_no_change_tcb_state
            possible_switch_to_valid_sched_except
         | wpc | clarsimp split del: if_split)+ apply (wp set_thread_state_runnable_valid_queues
                  set_thread_state_runnable_valid_sched_action
                  set_thread_state_valid_blocked_except sts_st_tcb_at')[1] apply (rule_tac Q="\<lambda>_. valid_sched and not_cur_thread receiver
                               and (\<lambda>s. receiver \<noteq> idle_thread s)"
              in hoare_strengthen_post) apply wp apply (simp add: valid_sched_def) apply (wp possible_switch_to_valid_sched_except)+ apply simp apply (rule conjI) apply clarsimp apply (rule_tac P="valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver
                               and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)" in hoare_weaken_pre) apply (wp set_thread_state_runnable_valid_queues
                       set_thread_state_runnable_valid_sched_action
                       set_thread_state_valid_blocked_except sts_st_tcb_at')[1] apply (fastforce simp: valid_sched_def ct_in_state_def st_tcb_at_def not_cur_thread_def
                                  obj_at_def) apply clarsimp apply (wp set_thread_state_not_runnable_valid_sched) apply simp apply (wp thread_set_not_state_valid_sched thread_set_no_change_tcb_state
                    cap_delete_one_reply_st_tcb_at thread_set_ct_active_wp | simp add: ct_in_state_def | wps)+ apply (wp hoare_drop_imps hoare_vcg_all_lift)[1] apply (simp add: get_thread_state_def thread_get_def | wp)+ apply (clarsimp simp: ct_in_state_def cte_wp_at_caps_of_state not_cur_thread_def) apply (fastforce simp: st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do state <- get_thread_state receiver;
y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state. \<lbrace>?P'29 state () None () ()\<rbrace> set_thread_state receiver Running \<lbrace>\<lambda>rv s. valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked_except receiver s \<and> st_tcb_at runnable receiver s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<And>state y x ya. x = None \<Longrightarrow> \<lbrace>?B20 state y x ya\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yb s. valid_etcbs s \<and> ?P'29 state y x ya yb s\<rbrace>
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>?B20 state y x\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 8. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya. x = None \<Longrightarrow> \<lbrace>?B20 state y x ya\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yb s. valid_etcbs s \<and> (valid_queues and K (runnable Running)) s \<and> ct_not_in_q s \<and> (valid_sched_action and (\<lambda>s. runnable Running)) s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> K (runnable Running) s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>?B20 state y x\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 7. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>state y x ya. x = None \<Longrightarrow> \<lbrace>?B20 state y x ya\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. valid_sched and not_cur_thread receiver and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 2. \<And>state y x ya rv s. \<lbrakk>x = None; (valid_sched and not_cur_thread receiver and (\<lambda>s. receiver \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (valid_queues and K (runnable Running)) s \<and> ct_not_in_q s \<and> (valid_sched_action and (\<lambda>s. runnable Running)) s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> K (runnable Running) s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s
 3. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>?B20 state y x\<rbrace>
 4. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 6. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 8. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya rv s. \<lbrakk>x = None; (valid_sched and not_cur_thread receiver and (\<lambda>s. receiver \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (valid_queues and K (runnable Running)) s \<and> ct_not_in_q s \<and> (valid_sched_action and (\<lambda>s. runnable Running)) s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> K (runnable Running) s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s
 2. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>\<lambda>ya s. valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s\<rbrace>
 3. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 5. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 7. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<And>state y x. x = None \<Longrightarrow> \<lbrace>?R16 state y x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>\<lambda>ya s. valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (possible_switch_to receiver)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R16 state y x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 4. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 6. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (11 subgoals):
 1. \<And>state y x x2 ya mi buf mrs restart yb. x = Some x2 \<Longrightarrow> \<lbrace>?B95 state y x x2 ya mi buf mrs restart yb\<rbrace> set_thread_state receiver (if restart then Restart else Inactive) \<lbrace>\<lambda>yc. if restart then valid_sched_except_blocked and valid_blocked_except receiver and st_tcb_at runnable receiver and not_cur_thread receiver and (\<lambda>s. receiver \<noteq> idle_thread s) else valid_sched\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B95 state y x x2 ya mi buf mrs restart\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> (restart \<longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs True ()\<rbrace> set_thread_state receiver Restart \<lbrace>\<lambda>yc a. valid_etcbs a \<and> valid_queues a \<and> ct_not_in_q a \<and> valid_sched_action a \<and> ct_in_cur_domain a \<and> valid_idle_etcb a \<and> valid_blocked_except receiver a \<and> st_tcb_at runnable receiver a \<and> not_cur_thread receiver a \<and> receiver \<noteq> idle_thread a\<rbrace>) \<and> (\<not> restart \<longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs False ()\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>)
 2. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B95 state y x x2 ya mi buf mrs restart\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> restart \<longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs True ()\<rbrace> set_thread_state receiver Restart \<lbrace>\<lambda>yc a. valid_etcbs a \<and> valid_queues a \<and> ct_not_in_q a \<and> valid_sched_action a \<and> ct_in_cur_domain a \<and> valid_idle_etcb a \<and> valid_blocked_except receiver a \<and> st_tcb_at runnable receiver a \<and> not_cur_thread receiver a \<and> receiver \<noteq> idle_thread a\<rbrace>
 2. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<not> restart \<longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs False ()\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B95 state y x x2 ya mi buf mrs restart\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs True ()\<rbrace> set_thread_state receiver Restart \<lbrace>\<lambda>yc a. valid_etcbs a \<and> valid_queues a \<and> ct_not_in_q a \<and> valid_sched_action a \<and> ct_in_cur_domain a \<and> valid_idle_etcb a \<and> valid_blocked_except receiver a \<and> st_tcb_at runnable receiver a \<and> not_cur_thread receiver a \<and> receiver \<noteq> idle_thread a\<rbrace>
 2. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<not> restart \<longrightarrow> \<lbrace>?B95 state () (Some x2) x2 () mi buf mrs False ()\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B95 state y x x2 ya mi buf mrs restart\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>state x2 mi buf mrs restart. restart \<Longrightarrow> \<lbrace>?Q111 state x2 mi buf mrs restart\<rbrace> set_thread_state receiver Restart \<lbrace>\<lambda>yc a. valid_etcbs a \<and> valid_queues a \<and> ct_not_in_q a \<and> valid_sched_action a \<and> ct_in_cur_domain a \<and> valid_idle_etcb a \<and> valid_blocked_except receiver a \<and> st_tcb_at runnable receiver a \<and> not_cur_thread receiver a \<and> receiver \<noteq> idle_thread a\<rbrace>
 2. \<And>state x2 mi buf mrs restart s. \<lbrakk>restart; (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ?Q111 state x2 mi buf mrs restart s
 3. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<not> restart \<longrightarrow> \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 5. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 6. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 7. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 8. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 9. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 10. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x2 mi buf mrs restart s. \<lbrakk>restart; (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (valid_queues and K (runnable Restart)) s \<and> ct_not_in_q s \<and> (valid_sched_action and (\<lambda>s. runnable Restart)) s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> K (runnable Restart) s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s
 2. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<not> restart \<longrightarrow> \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 4. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 5. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 6. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 7. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 8. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 9. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 10. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x x2 mi buf mrs restart. x = Some x2 \<Longrightarrow> \<not> restart \<longrightarrow> \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>restart. \<not> restart \<Longrightarrow> \<lbrace>\<lambda>a. valid_sched a \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver a \<and> ct_active a \<and> receiver \<noteq> idle_thread a\<rbrace> set_thread_state receiver Inactive \<lbrace>\<lambda>yc. valid_sched\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>restart s. \<lbrakk>\<not> restart; valid_sched s \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver s \<and> ct_active s \<and> receiver \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and K (\<not> runnable Inactive)) s
 2. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 3. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 4. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 5. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 6. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 7. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 8. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 9. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 10. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state y x x2 ya mi buf mrs restart. x = Some x2 \<Longrightarrow> \<lbrace>?B94 state y x x2 ya mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>\<lambda>a. valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
 2. \<And>state y x x2 ya mi buf mrs. x = Some x2 \<Longrightarrow> \<lbrace>?B93 state y x x2 ya mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B94 state y x x2 ya mi buf mrs\<rbrace>
 3. \<And>state y x x2 ya mi buf. x = Some x2 \<Longrightarrow> \<lbrace>?B92 state y x x2 ya mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B93 state y x x2 ya mi buf\<rbrace>
 4. \<And>state y x x2 ya mi. x = Some x2 \<Longrightarrow> \<lbrace>?B91 state y x x2 ya mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B92 state y x x2 ya mi\<rbrace>
 5. \<And>state y x x2 ya. x = Some x2 \<Longrightarrow> \<lbrace>?B90 state y x x2 ya\<rbrace> get_message_info sender \<lbrace>?B91 state y x x2 ya\<rbrace>
 6. \<And>state y x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R17 state y x x2\<rbrace> cap_delete_one slot \<lbrace>?B90 state y x x2\<rbrace>
 7. \<And>state y. \<lbrace>?B6 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_sched s \<and> not_cur_thread receiver s \<and> receiver \<noteq> idle_thread s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R17 state y x xa s)\<rbrace>
 8. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 10. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>state prev_s. \<lbrace>?P258 state prev_s\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>rv s'. (rv = None \<longrightarrow> valid_sched prev_s \<and> not_cur_thread receiver prev_s \<and> receiver \<noteq> idle_thread prev_s) \<and> (\<forall>x. rv = Some x \<longrightarrow> valid_sched prev_s \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver prev_s \<and> cte_wp_at (is_reply_cap_to (?t'a262 state () (Some x) x)) slot prev_s \<and> st_tcb_at active (cur_thread prev_s) prev_s \<and> cte_wp_at (is_reply_cap_to (?t'b263 state () (Some x) prev_s x)) slot prev_s \<and> receiver \<noteq> idle_thread prev_s)\<rbrace>
 2. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B6 state\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 4. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>:000 :003 x. ?t'264 :000 () (Some x) :003 x \<equiv>\<^sup>? \<lambda>:000 :003 x. ?t'b263 :000 () (Some x) :003 x
\<lambda>:000 x. ?t'a262 :000 () (Some x) x \<equiv>\<^sup>? \<lambda>:000 x. ?t'232 :000 () (Some x) x
\<lambda>state s. ?P258 state s s \<equiv>\<^sup>? \<lambda>state. ?B6 state () proof (prove)
goal (3 subgoals):
 1. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>\<lambda>a b. (valid_sched b \<and> not_cur_thread receiver b \<and> receiver \<noteq> idle_thread b) \<and> (\<forall>x. valid_sched b \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver b \<and> cte_wp_at (is_reply_cap_to (?t'a289 state a x)) slot b \<and> st_tcb_at active (cur_thread b) b \<and> cte_wp_at (is_reply_cap_to (?t'b288 state a b x)) slot b \<and> receiver \<noteq> idle_thread b)\<rbrace>
 2. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>?B5\<rbrace>
 3. \<And>s. (valid_sched and valid_objs and ct_active and cte_wp_at (is_reply_cap_to t') slot and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q4 s
flex-flex pairs:
\<lambda>state. ?t'a289 state () \<equiv>\<^sup>? \<lambda>state x. ?t'a262 state () (Some x) x
\<lambda>state. ?t'b288 state () \<equiv>\<^sup>? \<lambda>state s x. ?t'b263 state () (Some x) s x
\<lambda>:000 :003 x. ?t'264 :000 () (Some x) :003 x \<equiv>\<^sup>? \<lambda>:000 :003 x. ?t'b263 :000 () (Some x) :003 x
\<lambda>:000 x. ?t'a262 :000 () (Some x) x \<equiv>\<^sup>? \<lambda>:000 x. ?t'232 :000 () (Some x) x proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<and> valid_objs s \<and> ct_active s \<and> cte_wp_at (is_reply_cap_to t') slot s \<and> receiver \<noteq> idle_thread s \<Longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> awaiting_reply (tcb_state (the (get_tcb receiver s))) \<longrightarrow> not_cur_thread receiver s \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver s \<and> (\<forall>x. cte_wp_at (is_reply_cap_to (?t'a289 (ds_id BlockedOnReply) () x)) slot s \<and> st_tcb_at active (cur_thread s) s \<and> cte_wp_at (is_reply_cap_to (?t'b288 (ds_id BlockedOnReply) () s x)) slot s)
flex-flex pairs:
\<lambda>state. ?t'a289 state () \<equiv>\<^sup>? \<lambda>state x. ?t'a262 state () (Some x) x
\<lambda>state. ?t'b288 state () \<equiv>\<^sup>? \<lambda>state s x. ?t'b263 state () (Some x) s x
\<lambda>:000 :003 x. ?t'264 :000 () (Some x) :003 x \<equiv>\<^sup>? \<lambda>:000 :003 x. ?t'b263 :000 () (Some x) :003 x
\<lambda>:000 x. ?t'a262 :000 () (Some x) x \<equiv>\<^sup>? \<lambda>:000 x. ?t'232 :000 () (Some x) x proof (prove)
goal (1 subgoal):
 1. \<And>s cap y. \<lbrakk>valid_sched s; valid_objs s; st_tcb_at active (cur_thread s) s; receiver \<noteq> idle_thread s; caps_of_state s slot = Some cap; is_reply_cap_to t' cap; get_tcb receiver s = Some y; awaiting_reply (tcb_state y)\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> receiver \<noteq> cur_thread s) \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver s \<and> (\<forall>x. is_reply_cap_to (?t'a289 (ds_id BlockedOnReply) () x) cap \<and> is_reply_cap_to (?t'b288 (ds_id BlockedOnReply) () s x) cap)
flex-flex pairs:
\<lambda>state. ?t'a289 state () \<equiv>\<^sup>? \<lambda>state x. ?t'a262 state () (Some x) x
\<lambda>state. ?t'b288 state () \<equiv>\<^sup>? \<lambda>state s x. ?t'b263 state () (Some x) s x
\<lambda>:000 :003 x. ?t'264 :000 () (Some x) :003 x \<equiv>\<^sup>? \<lambda>:000 :003 x. ?t'b263 :000 () (Some x) :003 x
\<lambda>:000 x. ?t'a262 :000 () (Some x) x \<equiv>\<^sup>? \<lambda>:000 x. ?t'232 :000 () (Some x) x proof (prove)
goal:
No subgoals!