theory DetSchedSchedule_AI

lemma send_ipc_valid_sched:
  "\<lbrace>valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread
      and (ct_active or ct_idle) and invs\<rbrace>
   send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: send_ipc_def) apply (wp set_thread_state_sched_act_not_valid_sched | wpc)+ apply ((wp set_thread_state_sched_act_not_valid_sched
                       setup_caller_cap_sched_act_not_valid_sched
                       possible_switch_to_valid_sched_except
                       hoare_vcg_if_lift2 hoare_drop_imps | simp)+)[5] 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') apply (clarsimp simp: conj.commute eq_commute) apply (rename_tac recvr q recv_state) apply (rule_tac Q="\<lambda>_. valid_sched and scheduler_act_not thread and not_queued thread
                              and (\<lambda>s. recvr \<noteq> cur_thread s)
                              and (\<lambda>s. recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread)"
               in hoare_strengthen_post) apply ((wp thread_set_ct_active_wp|wpc)+)[1] apply (clarsimp simp: valid_sched_def) apply (clarsimp simp: ct_in_state_def cte_wp_at_caps_of_state not_cur_thread_def) apply (simp | wp gts_wp hoare_vcg_all_lift)+ apply (rename_tac recvr q recv_state) apply (wp hoare_vcg_imp_lift) apply ((simp add: set_simple_ko_def set_object_def | wp hoare_drop_imps | wpc)+)[1] apply (wpsimp wp: hoare_vcg_imp_lift get_object_wp
          | simp add: get_simple_ko_def
          | wpc |
           wp (once) hoare_vcg_all_lift)+ apply (subst st_tcb_at_kh_simp[symmetric]) apply (clarsimp simp: st_tcb_at_kh_if_split pred_tcb_at_def2 obj_at_def a_type_def
                        valid_sched_def valid_sched_action_def
                        weak_valid_sched_action_def scheduler_act_not_def
                  split: kernel_object.splits)+ apply (rename_tac tcb recvr q rtcb ep recv_pl) apply (case_tac "recvr = idle_thread s") subgoal by (fastforce dest: invs_valid_idle simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (case_tac "recvr = cur_thread s") subgoal by (fastforce simp: ct_in_state_def st_tcb_at_def2 obj_at_def) apply (clarsimp simp: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [thread]
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case block of True \<Rightarrow> do set_thread_state thread (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [thread])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap thread dest reply_can_grant else set_thread_state thread Inactive
od
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> \<lbrace>?Q80 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> setup_caller_cap thread x21 reply_can_grant \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R80 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state thread Inactive \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B74 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> ?Q80 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R80 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else valid_sched\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B73 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B74 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B72 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B73 ep x3 x21 x22 x recv_state\<rbrace>
 6. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 7. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 8. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 9. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ep x3 x21 x22 recv_state reply_can_grant. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?P'148 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant\<rbrace> set_thread_state x21 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 x21 s \<and> st_tcb_at runnable x21 s \<and> not_cur_thread x21 s \<and> x21 \<noteq> idle_thread s \<and> thread \<noteq> x21 \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> valid_etcbs s \<and> 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 x21 s \<and> st_tcb_at runnable x21 s \<and> not_cur_thread x21 s \<and> x21 \<noteq> idle_thread s \<and> thread \<noteq> x21 \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> valid_etcbs s \<and> 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 x21 s \<and> st_tcb_at runnable x21 s \<and> not_cur_thread x21 s \<and> x21 \<noteq> idle_thread s\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B72 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>\<lambda>reply_can_grant s. valid_etcbs s \<and> ?P'148 ep x3 x21 x22 x recv_state reply_can_grant s\<rbrace>
 3. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 4. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 6. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B72 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>\<lambda>reply_can_grant 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 x21 s \<and> x21 \<noteq> idle_thread s \<and> thread \<noteq> x21 \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> 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 x21 s \<and> x21 \<noteq> idle_thread s \<and> thread \<noteq> x21 \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> 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 x21 s \<and> x21 \<noteq> idle_thread s\<rbrace>
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 5. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 recv_state. \<lbrace>?B72 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>\<lambda>reply_can_grant s. valid_etcbs s \<and> 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 s \<and> not_cur_thread x21 s \<and> x21 \<noteq> idle_thread s \<and> x21 \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> not_cur_thread x21 s \<and> x21 \<noteq> idle_thread s \<and> x21 \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> x21 \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> x21 \<noteq> idle_thread s \<and> not_cur_thread x21 s\<rbrace>
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 5. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>recvr q recv_state. \<lbrace>?B72 (RecvEP (recvr # q)) (recvr # q) recvr q () recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant recvr;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>\<lambda>reply_can_grant s. valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> recvr \<noteq> idle_thread s \<and> not_cur_thread recvr s\<rbrace>
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 5. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>recvr q recv_state. \<lbrace>?B72 (RecvEP (recvr # q)) (recvr # q) recvr q () recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer thread (Some epptr) badge can_grant recvr;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. valid_sched and scheduler_act_not thread and not_queued thread and (\<lambda>s. recvr \<noteq> cur_thread s) and (\<lambda>s. recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread)\<rbrace>
 2. \<And>recvr q recv_state rv s. (valid_sched and scheduler_act_not thread and not_queued thread and (\<lambda>s. recvr \<noteq> cur_thread s) and (\<lambda>s. recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread)) s \<Longrightarrow> valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> recvr \<noteq> idle_thread s \<and> not_cur_thread recvr s
 3. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B72 ep x3 x21 x22 x\<rbrace>
 4. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 6. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>recvr q recv_state rv s. (valid_sched and scheduler_act_not thread and not_queued thread and (\<lambda>s. recvr \<noteq> cur_thread s) and (\<lambda>s. recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread)) s \<Longrightarrow> valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> not_cur_thread recvr s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> scheduler_act_not thread s \<and> recvr \<noteq> thread \<and> valid_etcbs s \<and> 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 s \<and> recvr \<noteq> idle_thread s \<and> not_cur_thread recvr s
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> True) \<and> (inactive a \<longrightarrow> True) \<and> (a = Restart \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnReceive x xa \<longrightarrow> valid_sched b \<and> scheduler_act_not thread b \<and> not_queued thread b \<and> x21 \<noteq> cur_thread b \<and> x21 \<noteq> idle_thread b \<and> x21 \<noteq> thread) \<and> (\<forall>x xa. a = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply a \<longrightarrow> True) \<and> (\<forall>x. a = BlockedOnNotification x \<longrightarrow> True) \<and> (idle a \<longrightarrow> True)\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 5. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>recvr s. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; scheduler_act_not thread s; not_queued thread s; recvr \<noteq> cur_thread s; recvr \<noteq> idle_thread s; recvr \<noteq> thread\<rbrakk> \<Longrightarrow> not_cur_thread recvr s
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> True) \<and> (inactive a \<longrightarrow> True) \<and> (a = Restart \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnReceive x xa \<longrightarrow> valid_sched b \<and> scheduler_act_not thread b \<and> not_queued thread b \<and> x21 \<noteq> cur_thread b \<and> x21 \<noteq> idle_thread b \<and> x21 \<noteq> thread) \<and> (\<forall>x xa. a = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply a \<longrightarrow> True) \<and> (\<forall>x. a = BlockedOnNotification x \<longrightarrow> True) \<and> (idle a \<longrightarrow> True)\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 5. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B70 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> True) \<and> (inactive a \<longrightarrow> True) \<and> (a = Restart \<longrightarrow> True) \<and> (\<forall>x xa. a = BlockedOnReceive x xa \<longrightarrow> valid_sched b \<and> scheduler_act_not thread b \<and> not_queued thread b \<and> x21 \<noteq> cur_thread b \<and> x21 \<noteq> idle_thread b \<and> x21 \<noteq> thread) \<and> (\<forall>x xa. a = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply a \<longrightarrow> True) \<and> (\<forall>x. a = BlockedOnNotification x \<longrightarrow> True) \<and> (idle a \<longrightarrow> True)\<rbrace>
 2. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R64 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B70 ep x3 x21 x22\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R64 ep x xa xb s))\<rbrace>
 4. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3 x21 x22 st. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. ?P512 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 a st\<rbrace> set_endpoint epptr (case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22) \<lbrace>\<lambda>a b. st_tcb_at ((=) st) x21 b \<longrightarrow> (\<exists>x xa. st = BlockedOnReceive x xa) \<longrightarrow> valid_sched b \<and> scheduler_act_not thread b \<and> not_queued thread b \<and> x21 \<noteq> cur_thread b \<and> x21 \<noteq> idle_thread b \<and> x21 \<noteq> thread\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>xc. ?P512 ep x xa xb s xc)))\<rbrace>
 3. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3 recvr q recv_state. \<lbrakk>ep = RecvEP (recvr # q); x3 = recvr # q\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. ?P512 (RecvEP (recvr # q)) (recvr # q) recvr q a recv_state\<rbrace> set_endpoint epptr (case q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP q) \<lbrace>\<lambda>a b. st_tcb_at ((=) recv_state) recvr b \<longrightarrow> (\<exists>x xa. recv_state = BlockedOnReceive x xa) \<longrightarrow> valid_sched b \<and> scheduler_act_not thread b \<and> not_queued thread b \<and> recvr \<noteq> cur_thread b \<and> recvr \<noteq> idle_thread b \<and> recvr \<noteq> thread\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>xc. ?P512 ep x xa xb s xc)))\<rbrace>
 3. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 recvr q recv_state. \<lbrakk>ep = RecvEP (recvr # q); x3 = recvr # q\<rbrakk> \<Longrightarrow> \<lbrace>?P'521 (RecvEP (recvr # q)) (recvr # q) recvr q recv_state\<rbrace> set_endpoint epptr (case q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP q) \<lbrace>\<lambda>rv s. \<not> st_tcb_at ((=) recv_state) recvr s\<rbrace>
 2. \<And>ep x3 recvr q recv_state. \<lbrakk>ep = RecvEP (recvr # q); x3 = recvr # q\<rbrakk> \<Longrightarrow> \<lbrace>?Q'519 (RecvEP (recvr # q)) (recvr # q) recvr q recv_state\<rbrace> set_endpoint epptr (case q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP q) \<lbrace>\<lambda>rv s. (\<exists>x xa. recv_state = BlockedOnReceive x xa) \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> recvr \<noteq> cur_thread s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>xc. ?P'521 ep x xa xb xc s \<or> ?Q'519 ep x xa xb xc s)))\<rbrace>
 4. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3 recvr q recv_state. \<lbrakk>ep = RecvEP (recvr # q); x3 = recvr # q\<rbrakk> \<Longrightarrow> \<lbrace>?Q'519 (RecvEP (recvr # q)) (recvr # q) recvr q recv_state\<rbrace> set_endpoint epptr (case q of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP q) \<lbrace>\<lambda>rv s. (\<exists>x xa. recv_state = BlockedOnReceive x xa) \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s \<and> recvr \<noteq> cur_thread s \<and> recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (valid_sched and scheduler_act_not thread and not_queued thread and K (\<not> runnable (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>))) s) \<and> (block = False \<longrightarrow> valid_sched s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (\<forall>xc. \<not> st_tcb_at ((=) xc) xa (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb))\<rparr>) \<or> ?Q'519 ep x xa xb xc s)))\<rbrace>
 3. \<And>s. (valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and (ct_active or ct_idle) and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_sched s; st_tcb_at active thread s; scheduler_act_not thread s; not_queued thread s; ct_active s \<or> ct_idle s; invs s; ko_at ko epptr s\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<forall>x. Endpoint x = ko \<longrightarrow> (\<forall>xa. x = RecvEP xa \<longrightarrow> (\<forall>x xb. xa = x # xb \<longrightarrow> (\<forall>xa. st_tcb_at ((=) xa) x (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) else kheap s a\<rparr>) \<longrightarrow> (\<forall>x xb. xa \<noteq> BlockedOnReceive x xb) \<or> x \<noteq> cur_thread s \<and> x \<noteq> idle_thread s \<and> x \<noteq> thread))))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<forall>x. Endpoint x = ko \<longrightarrow> (\<forall>xa. x = RecvEP xa \<longrightarrow> (\<forall>x xb. xa = x # xb \<longrightarrow> (\<forall>xa. st_tcb_at ((=) xa) x (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) else kheap s a\<rparr>) \<longrightarrow> (\<forall>x xb. xa \<noteq> BlockedOnReceive x xb) \<or> x \<noteq> cur_thread s \<and> x \<noteq> idle_thread s \<and> x \<noteq> thread))))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_sched s; st_tcb_at active thread s; scheduler_act_not thread s; not_queued thread s; ct_active s \<or> ct_idle s; invs s; ko_at ko epptr s\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<forall>x. Endpoint x = ko \<longrightarrow> (\<forall>xa. x = RecvEP xa \<longrightarrow> (\<forall>x xb. xa = x # xb \<longrightarrow> (\<forall>xa. st_tcb_at_kh ((=) xa) x (kheap (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) else kheap s a\<rparr>)) \<longrightarrow> (\<forall>x xb. xa \<noteq> BlockedOnReceive x xb) \<or> x \<noteq> cur_thread s \<and> x \<noteq> idle_thread s \<and> x \<noteq> thread))))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<forall>x. Endpoint x = ko \<longrightarrow> (\<forall>xa. x = RecvEP xa \<longrightarrow> (\<forall>x xb. xa = x # xb \<longrightarrow> (\<forall>xa. st_tcb_at ((=) xa) x (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) else kheap s a\<rparr>) \<longrightarrow> (\<forall>x xb. xa \<noteq> BlockedOnReceive x xb) \<or> x \<noteq> cur_thread s \<and> x \<noteq> idle_thread s \<and> x \<noteq> thread))))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb xa xb tcba xd xe. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (xa # xb))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; xa \<noteq> epptr; kheap s xa = Some (TCB tcba); xa = cur_thread s \<or> xa = idle_thread s \<or> xa = thread; tcb_state tcba = BlockedOnReceive xd xe\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr = idle_thread s\<rbrakk> \<Longrightarrow> False
 2. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_action s_ \<noteq> switch_thread thread; not_queued thread s_; ct_active s_ \<or> ct_idle s_; invs s_; kheap s_ epptr = Some (Endpoint (RecvEP (recvr_ # q_))); valid_etcbs s_; kheap s_ thread = Some (TCB tcb_); active (tcb_state tcb_); valid_queues s_; ct_not_in_q s_; is_activatable (cur_thread s_) s_; \<forall>t. scheduler_action s_ = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s_ t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s_; ct_in_cur_domain s_; valid_blocked s_; valid_idle_etcb s_; recvr_ \<noteq> epptr; kheap s_ recvr_ = Some (TCB rtcb_); recvr_ = cur_thread s_ \<or> recvr_ = idle_thread s_ \<or> recvr_ = thread; tcb_state rtcb_ = BlockedOnReceive ep_ recv_pl_; recvr_ = idle_thread s_\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr \<noteq> idle_thread s; recvr = cur_thread s\<rbrakk> \<Longrightarrow> False
 2. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr \<noteq> idle_thread s; recvr \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_action s_ \<noteq> switch_thread thread; not_queued thread s_; ct_active s_ \<or> ct_idle s_; invs s_; kheap s_ epptr = Some (Endpoint (RecvEP (recvr_ # q_))); valid_etcbs s_; kheap s_ thread = Some (TCB tcb_); active (tcb_state tcb_); valid_queues s_; ct_not_in_q s_; is_activatable (cur_thread s_) s_; \<forall>t. scheduler_action s_ = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s_ t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s_; ct_in_cur_domain s_; valid_blocked s_; valid_idle_etcb s_; recvr_ \<noteq> epptr; kheap s_ recvr_ = Some (TCB rtcb_); recvr_ = cur_thread s_ \<or> recvr_ = idle_thread s_ \<or> recvr_ = thread; tcb_state rtcb_ = BlockedOnReceive ep_ recv_pl_; recvr_ \<noteq> idle_thread s_; recvr_ = cur_thread s_\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s tcb recvr q rtcb ep recv_pl. \<lbrakk>scheduler_action s \<noteq> switch_thread thread; not_queued thread s; ct_active s \<or> ct_idle s; invs s; kheap s epptr = Some (Endpoint (RecvEP (recvr # q))); valid_etcbs s; kheap s thread = Some (TCB tcb); active (tcb_state tcb); valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>tcb. kheap s t = Some (TCB tcb) \<and> runnable (tcb_state tcb)); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; recvr \<noteq> epptr; kheap s recvr = Some (TCB rtcb); recvr = cur_thread s \<or> recvr = idle_thread s \<or> recvr = thread; tcb_state rtcb = BlockedOnReceive ep recv_pl; recvr \<noteq> idle_thread s; recvr \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!