theory Ipc_IF

lemma send_ipc_globals_equiv:
  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                     and pspace_distinct and pspace_aligned and valid_global_objs
                     and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace>
   send_ipc block call badge can_grant can_grant_reply thread epptr
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding send_ipc_def apply (wp set_simple_ko_globals_equiv set_thread_state_globals_equiv
            setup_caller_cap_globals_equiv | wpc)+ apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
                     in hoare_strengthen_post[rotated]) apply (fastforce) apply (wp set_thread_state_globals_equiv dxo_wp_weak | simp)+ apply wpc apply (wp do_ipc_transfer_globals_equiv)+ apply (clarsimp) apply (rule hoare_drop_imps) apply (wp set_simple_ko_globals_equiv)+ apply (rule_tac Q="\<lambda>ep. ko_at (Endpoint ep) epptr and globals_equiv st and valid_objs and
                           valid_arch_state and valid_global_refs and pspace_distinct and
                           pspace_aligned and valid_global_objs and
                           (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle"
                in hoare_strengthen_post) apply (wp get_simple_ko_sp) apply (clarsimp)+ apply (rule context_conjI) apply (rule valid_ep_recv_dequeue') apply (simp)+ apply (frule_tac x=xa in receive_endpoint_threads_blocked,simp+) by (clarsimp simp add: valid_idle_def pred_tcb_at_def obj_at_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> do ep <- get_endpoint epptr;
case (ep, block) of (IdleEP, 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 | (IdleEP, False) \<Rightarrow> return () | (SendEP queue, 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 | (SendEP queue, False) \<Rightarrow> return () | (RecvEP [], x) \<Rightarrow> fail | (RecvEP (dest # queue), x) \<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>_. globals_equiv st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B81 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> (globals_equiv st and valid_arch_state and valid_global_objs) s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> (globals_equiv st and valid_arch_state) s) else globals_equiv st\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B80 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B81 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B79 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>?B80 ep x3 x21 x22 x recv_state\<rbrace>
 4. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B79 ep x3 x21 x22 x\<rbrace>
 5. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 7. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa rv s. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22; (globals_equiv st and valid_arch_state and valid_global_objs) s\<rbrakk> \<Longrightarrow> (if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> (globals_equiv st and valid_arch_state and valid_global_objs) s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> (globals_equiv st and valid_arch_state) s) else globals_equiv st) s
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B81 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B80 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B81 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B79 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>?B80 ep x3 x21 x22 x recv_state\<rbrace>
 5. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B79 ep x3 x21 x22 x\<rbrace>
 6. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 7. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 8. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B81 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B80 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B81 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B79 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>?B80 ep x3 x21 x22 x recv_state\<rbrace>
 4. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B79 ep x3 x21 x22 x\<rbrace>
 5. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 7. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B79 (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. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 2. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B79 ep x3 x21 x22 x\<rbrace>
 3. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 5. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (12 subgoals):
 1. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; recv_state = Running\<rbrakk> \<Longrightarrow> \<lbrace>?R150 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 2. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; inactive recv_state\<rbrakk> \<Longrightarrow> \<lbrace>?R149 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 3. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; recv_state = Restart\<rbrakk> \<Longrightarrow> \<lbrace>?R148 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 4. \<And>ep x3 x21 x22 recv_state x41 x42. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; recv_state = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?R169 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state x41 x42\<rbrace> do do_ipc_transfer thread (Some epptr) badge can_grant x21;
return (receiver_can_grant x42)
od \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 5. \<And>ep x3 x21 x22 recv_state x51 x52. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; recv_state = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?R166 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state x51 x52\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 6. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; awaiting_reply recv_state\<rbrakk> \<Longrightarrow> \<lbrace>?R145 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 7. \<And>ep x3 x21 x22 recv_state x7. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; recv_state = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> \<lbrace>?R161 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state x7\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 8. \<And>ep x3 x21 x22 recv_state. \<lbrakk>ep = RecvEP (x21 # x22); x3 = x21 # x22; idle recv_state\<rbrakk> \<Longrightarrow> \<lbrace>?R143 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state\<rbrace> fail \<lbrace>\<lambda>reply_can_grant s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 9. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> ?R150 ep x3 x21 x22 x a b) \<and> (inactive a \<longrightarrow> ?R149 ep x3 x21 x22 x a b) \<and> (a = Restart \<longrightarrow> ?R148 ep x3 x21 x22 x a b) \<and> (\<forall>xa xb. a = BlockedOnReceive xa xb \<longrightarrow> ?R169 ep x3 x21 x22 x a xa xb b) \<and> (\<forall>xa xb. a = BlockedOnSend xa xb \<longrightarrow> ?R166 ep x3 x21 x22 x a xa xb b) \<and> (awaiting_reply a \<longrightarrow> ?R145 ep x3 x21 x22 x a b) \<and> (\<forall>xa. a = BlockedOnNotification xa \<longrightarrow> ?R161 ep x3 x21 x22 x a xa b) \<and> (idle a \<longrightarrow> ?R143 ep x3 x21 x22 x a b)\<rbrace>
 10. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x21 x22 x. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 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> (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. x21 \<noteq> idle_thread s)) b \<and> valid_arch_state b \<and> valid_global_objs b) \<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>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22. \<lbrace>?B77 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 ()\<rbrace> get_thread_state x21 \<lbrace>\<lambda>a b. (\<exists>x xa. a = BlockedOnReceive x xa) \<longrightarrow> globals_equiv st b \<and> valid_arch_state b \<and> valid_objs b \<and> valid_arch_state b \<and> valid_global_refs b \<and> pspace_distinct b \<and> pspace_aligned b \<and> valid_global_objs b \<and> x21 \<noteq> idle_thread b \<and> valid_arch_state b \<and> valid_global_objs b\<rbrace>
 2. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22. \<lbrace>?B77 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 ()\<rbrace> get_thread_state x21 \<lbrace>\<lambda>rv s. globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> x21 \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s\<rbrace>
 2. \<And>ep x3 x21 x22. \<lbrakk>ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R71 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B77 ep x3 x21 x22\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R71 ep x xa xb s))\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> (valid_objs and valid_simple_obj (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) and K (is_simple_type (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)))) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> xa \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s))\<rbrace>
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep. ko_at (Endpoint ep) epptr and globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle\<rbrace>
 2. \<And>rv s. (ko_at (Endpoint rv) epptr and globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle) s \<Longrightarrow> (rv = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. rv = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> (valid_objs and valid_simple_obj (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) and K (is_simple_type (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)))) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> xa \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s))
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (ko_at (Endpoint rv) epptr and globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle) s \<Longrightarrow> (rv = IdleEP \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> (block = True \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s) \<and> (block = False \<longrightarrow> globals_equiv st s)) \<and> (\<forall>x. rv = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> (valid_objs and valid_simple_obj (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)) and K (is_simple_type (Endpoint (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb)))) s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> xa \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s))
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s proof (prove)
goal (2 subgoals):
 1. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s\<rbrakk> \<Longrightarrow> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s \<and> xa \<noteq> idle_thread s
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s proof (prove)
goal (3 subgoals):
 1. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s\<rbrakk> \<Longrightarrow> valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s
 2. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s; valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s\<rbrakk> \<Longrightarrow> ko_at (Endpoint (RecvEP (?t288 s xa xb # xb))) (?epptr288 s xa xb) s
 2. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s; valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s proof (prove)
goal (2 subgoals):
 1. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s; valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s proof (prove)
goal (2 subgoals):
 1. \<And>s xa xb. \<lbrakk>ko_at (Endpoint (RecvEP (xa # xb))) epptr s; globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; sym_refs (state_refs_of s); valid_idle s; valid_ep (case xb of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP xb) s; st_tcb_at (receive_blocked_on epptr) xa s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 2. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> sym_refs (state_refs_of s) \<and> valid_idle s