theory Ipc_DR

lemma valid_idle_cancel_all_ipc:
  "\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.cancel_all_ipc word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>" including no_pre apply (simp add:cancel_all_ipc_def) apply (wp|wpc|simp)+ apply (rename_tac queue list) apply (rule_tac I = "(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
             and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1  and valid_idle" in mapM_x_inv_wp) apply clarsimp apply (wp KHeap_DR.tcb_at_set_thread_state_wp) apply (rule hoare_conjI) apply (rule_tac P="(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
                  and valid_idle and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1"
               in hoare_vcg_precond_imp) apply (wp | clarsimp)+ apply (rule set_thread_state_ko) apply (simp add:is_tcb_def) apply (wp valid_idle_set_thread_state) apply (clarsimp simp:)+ apply wp apply (rule hoare_vcg_conj_lift) apply (rule hoare_Ball_helper) apply (wp simple_obj_set_prop_at | clarsimp simp :get_ep_queue_def not_idle_thread_def)+ apply (rename_tac queue list) apply (rule_tac I = "(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
            and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1  and valid_idle" in mapM_x_inv_wp) apply clarsimp apply (wp KHeap_DR.tcb_at_set_thread_state_wp) apply (rule hoare_conjI) apply (rule_tac P="(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
                       and valid_idle and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1"
              in hoare_vcg_precond_imp) apply (rule set_thread_state_ko) apply (simp add:is_tcb_def) apply (wp valid_idle_set_thread_state) apply (clarsimp simp:)+ apply wp apply (rule hoare_vcg_conj_lift) apply (rule hoare_Ball_helper) apply (wp simple_obj_set_prop_at | clarsimp simp :get_ep_queue_def not_idle_thread_def)+ apply (rule hoare_strengthen_post[OF get_simple_ko_sp]) apply (clarsimp  | rule conjI)+ apply (clarsimp simp:obj_at_def valid_pspace_def valid_state_def) apply (drule(1) valid_objs_valid_ep_simp) apply (clarsimp simp:is_tcb_def valid_ep_def obj_at_def) apply (drule(1) pending_thread_in_send_not_idle) apply (simp add:not_idle_thread_def obj_at_def is_ep_def)+ apply (clarsimp | rule conjI)+ apply (clarsimp simp:obj_at_def valid_pspace_def valid_state_def) apply (drule(1) valid_objs_valid_ep_simp) apply (clarsimp simp:is_tcb_def valid_ep_def obj_at_def) apply (drule(1) pending_thread_in_recv_not_idle) apply (simp add:not_idle_thread_def obj_at_def is_ep_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> IpcCancel_A.cancel_all_ipc word1 \<lbrace>\<lambda>a. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> IpcCancel_A.cancel_all_ipc word1 \<lbrace>\<lambda>a. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> do ep <- get_endpoint word1;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od
od \<lbrace>\<lambda>a. valid_idle\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B22 (SendEP x2) x2 queue ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue \<lbrace>\<lambda>a. valid_idle\<rbrace>
 2. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>?B22 ep x2 queue\<rbrace>
 3. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ep queue list. ep = SendEP queue \<Longrightarrow> \<lbrace>?B22 (SendEP queue) queue list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>a. valid_idle\<rbrace>
 2. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>?B22 ep x2 queue\<rbrace>
 3. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P32 ep queue list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 3. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> ?P32 ep queue list s
 4. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 6. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 7. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P32 ep queue list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 2. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> ?P32 ep queue list s
 3. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'52 ep queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'52 ep queue list s
 3. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'52 ep queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace>
 2. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'52 ep queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'52 ep queue list s
 4. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 6. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 7. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 ep queue list x\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace>
 2. \<And>ep queue list x s. \<lbrakk>ep = SendEP queue; x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> ?Q59 ep queue list x s
 3. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 4. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 5. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 6. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 7. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 8. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?Q59 (SendEP queue) queue list x\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace>
 2. \<And>ep queue list x s. \<lbrakk>ep = SendEP queue; x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> ?Q59 ep queue list x s
 3. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 4. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 5. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 6. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 7. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 8. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ep queue list x s. \<lbrakk>ep = SendEP queue; x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> (ko_at (kernel_object.Endpoint IdleEP) word1 and K (\<not> is_tcb (kernel_object.Endpoint IdleEP))) s
 2. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 4. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 6. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 7. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep queue list x. \<lbrakk>ep = SendEP queue; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 2. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 3. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep queue list x s. \<lbrakk>ep = SendEP queue; x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> (not_idle_thread x and valid_idle) s
 2. \<And>ep queue list s. \<lbrakk>ep = SendEP queue; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 3. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B21 ep x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2 queue. \<lbrace>?B21 (SendEP x2) x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a b. x2 = queue \<and> (\<forall>a\<in>set queue. tcb_at a b \<and> not_idle_thread a b) \<and> ko_at (kernel_object.Endpoint IdleEP) word1 b \<and> valid_idle b\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B21 ep x2\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2 queue. \<lbrace>?P'74 (SendEP x2) x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s) \<and> ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x2 = a \<and> ?P'74 ep x2 a b\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x2 queue. \<lbrace>?P80 (SendEP x2) x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. \<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s\<rbrace>
 2. \<And>x2 queue. \<lbrace>?P'79 (SendEP x2) x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 3. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x2 = a \<and> ?P80 ep x2 a b \<and> ?P'79 ep x2 a b\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x2 queue a. \<lbrace>\<lambda>b. ?P84 (SendEP x2) x2 queue b a\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>b c. tcb_at a c \<and> not_idle_thread a c\<rbrace>
 2. \<And>x2 queue P. \<lbrace>\<lambda>s. P (set queue)\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. P (set queue)\<rbrace>
 3. \<And>x2 queue. \<lbrace>?P'79 (SendEP x2) x2 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 4. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R13 ep x2\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x2 = a \<and> (\<forall>x\<in>set a. ?P84 ep x2 a b x) \<and> ?P'79 ep x2 a b\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint word1 IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R13 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x3 queue. \<lbrace>?B121 (RecvEP x3) x3 queue ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue \<lbrace>\<lambda>a. valid_idle\<rbrace>
 2. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>?B121 ep x3 queue\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queue list. \<lbrace>?B121 (RecvEP queue) queue list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>a. valid_idle\<rbrace>
 2. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>?B121 ep x3 queue\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> valid_idle s
 2. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?P137 queue list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 3. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> ?P137 queue list s
 4. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?P137 queue list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 2. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> ?P137 queue list s
 3. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?P'157 queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'157 queue list s
 3. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?P'157 queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace>
 2. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?P'157 queue list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'157 queue list s
 4. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>?Q164 queue list x\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace>
 2. \<And>queue list x s. \<lbrakk>x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> ?Q164 queue list x s
 3. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 4. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 5. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 6. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 7. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>queue list x s. \<lbrakk>x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> (ko_at (kernel_object.Endpoint IdleEP) word1 and K (\<not> is_tcb (kernel_object.Endpoint IdleEP))) s
 2. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 4. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 5. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queue list x. x \<in> set list \<Longrightarrow> \<lbrace>(\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 2. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 3. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queue list x s. \<lbrakk>x \<in> set list; ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s\<rbrakk> \<Longrightarrow> (not_idle_thread x and valid_idle) s
 2. \<And>queue list s. ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle) s \<Longrightarrow> queue = list \<and> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. queue = list \<and> (\<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s)) and valid_idle and ko_at (kernel_object.Endpoint IdleEP) word1) s
 3. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B120 ep x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a. (\<lambda>s. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s)) and ko_at (kernel_object.Endpoint IdleEP) word1 and valid_idle\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3 queue. \<lbrace>?B120 (RecvEP x3) x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>a b. x3 = queue \<and> (\<forall>a\<in>set queue. tcb_at a b \<and> not_idle_thread a b) \<and> ko_at (kernel_object.Endpoint IdleEP) word1 b \<and> valid_idle b\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B120 ep x3\<rbrace>
 3. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3 queue. \<lbrace>?P'176 (RecvEP x3) x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. (\<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s) \<and> ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x3 = a \<and> ?P'176 ep x3 a b\<rbrace>
 3. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x3 queue. \<lbrace>?P182 (RecvEP x3) x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. \<forall>a\<in>set queue. tcb_at a s \<and> not_idle_thread a s\<rbrace>
 2. \<And>x3 queue. \<lbrace>?P'181 (RecvEP x3) x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x3 = a \<and> ?P182 ep x3 a b \<and> ?P'181 ep x3 a b\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3 queue a. \<lbrace>\<lambda>b. ?P186 (RecvEP x3) x3 queue b a\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>b c. tcb_at a c \<and> not_idle_thread a c\<rbrace>
 2. \<And>x3 queue P. \<lbrace>\<lambda>s. P (set queue)\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. P (set queue)\<rbrace>
 3. \<And>x3 queue. \<lbrace>?P'181 (RecvEP x3) x3 queue\<rbrace> set_endpoint word1 IdleEP \<lbrace>\<lambda>rv s. ko_at (kernel_object.Endpoint IdleEP) word1 s \<and> valid_idle s\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R14 ep x3\<rbrace> get_ep_queue ep \<lbrace>\<lambda>a b. x3 = a \<and> (\<forall>x\<in>set a. ?P186 ep x3 a b x) \<and> ?P'181 ep x3 a b\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> x = x \<and> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R14 ep x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> get_endpoint word1 \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (ko_at (kernel_object.Endpoint rv) word1 and (valid_idle and valid_state)) s \<Longrightarrow> (rv = IdleEP \<longrightarrow> valid_idle s) \<and> (\<forall>x. rv = SendEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) \<and> (\<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s \<and> valid_idle s) proof (prove)
goal (4 subgoals):
 1. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> tcb_at xa s
 2. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>s x. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s
 4. \<And>rv s. \<lbrakk>ko_at (kernel_object.Endpoint rv) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s proof (prove)
goal (4 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (SendEP x)); valid_idle s; xa \<in> set x; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>s x. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s
 4. \<And>rv s. \<lbrakk>ko_at (kernel_object.Endpoint rv) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s proof (prove)
goal (4 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (SendEP x)); valid_idle s; xa \<in> set x; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; valid_ep (SendEP x) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>s x. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s
 4. \<And>rv s. \<lbrakk>ko_at (kernel_object.Endpoint rv) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s proof (prove)
goal (3 subgoals):
 1. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 2. \<And>s x. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s
 3. \<And>rv s. \<lbrakk>ko_at (kernel_object.Endpoint rv) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s proof (prove)
goal (5 subgoals):
 1. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; xa \<in> set x\<rbrakk> \<Longrightarrow> ?a277 s x xa \<in> set (?list277 s x xa)
 2. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; xa \<in> set x\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Endpoint (SendEP (?list277 s x xa))) (?epptr277 s x xa) s
 3. \<And>s x xa. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; xa \<in> set x; not_idle_thread (?a277 s x xa) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 4. \<And>s x. \<lbrakk>ko_at (kernel_object.Endpoint (SendEP x)) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s
 5. \<And>rv s. \<lbrakk>ko_at (kernel_object.Endpoint rv) word1 s; valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) word1 s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint rv); valid_idle s; valid_state s\<rbrakk> \<Longrightarrow> \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>x\<in>set x. (\<exists>ko. kheap s x = Some ko \<and> is_tcb ko) \<and> x \<noteq> idle_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; xa \<in> set x; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; xa \<in> set x; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; valid_ep (RecvEP x) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; valid_state s; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s proof (prove)
goal (3 subgoals):
 1. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; xa \<in> set x\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Endpoint (RecvEP (?list323 s x xa))) (?epptr323 s x xa) s
 2. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; xa \<in> set x\<rbrakk> \<Longrightarrow> ?a323 s x xa \<in> set (?list323 s x xa)
 3. \<And>s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Endpoint (RecvEP x)); valid_idle s; xa \<in> set x; not_idle_thread (?a323 s x xa) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s proof (prove)
goal:
No subgoals!