theory KHeap_DR

lemma fast_finalise_recv_ep:
  "dcorres dc \<top> (valid_state and valid_idle and ko_at (kernel_object.Endpoint (Structures_A.endpoint.RecvEP list)) epptr and valid_etcbs)
  (PageTableUnmap_D.cancel_all_ipc epptr)
  (do queue \<leftarrow> get_ep_queue (Structures_A.endpoint.RecvEP list);
      _ \<leftarrow> set_endpoint epptr Structures_A.endpoint.IdleEP;
      _ \<leftarrow> mapM_x (\<lambda>t. do _ \<leftarrow> set_thread_state t Structures_A.thread_state.Restart;
                         tcb_sched_action tcb_sched_enqueue t
                  od) queue;
      reschedule_required
  od)" supply if_cong[cong] apply (simp add:get_ep_queue_def cancel_all_ipc_def_alt1) apply (rule dcorres_absorb_get_l) apply clarsimp apply (rule corres_dummy_return_pl) apply (rule_tac Q="\<lambda>r. \<top>" and
                  Q'="\<lambda>r s. (s = update_kheap ((kheap s')(epptr\<mapsto> (Endpoint Structures_A.endpoint.IdleEP))) s')"
          in corres_split_forwards' [where r'="dc"]) apply (rule corres_dummy_set_sync_ep[THEN corres_guard_imp],(simp|wp)+) apply (rule set_ep_exec_wp) apply clarsimp apply (rule_tac
    Q'="\<lambda>s. (\<forall>x\<in> (set list). valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s)"
    in corres_guard_imp[where Q=\<top>]) apply (rule dcorres_rhs_noop_below_True[OF reschedule_required_dcorres]) apply (rule_tac lift_func = id in set_list_modify_corres_helper) apply (clarsimp simp:obj_at_def) apply (drule valid_objs_valid_ep_simp[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply (simp add:valid_ep_def) apply (simp add:inj_on_def) apply (frule_tac epptr=epptr in get_endpoint_pick,simp add:obj_at_def) apply (simp add:valid_ep_abstract_def none_is_sending_ep_def none_is_receiving_ep_def obj_at_def)+ apply (subst is_thread_blocked_on_sth[simplified]) apply (clarsimp simp:ntfn_waiting_set_lift ep_waiting_set_send_lift ep_waiting_set_recv_lift) apply (drule ep_not_waiting_ntfn[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply clarsimp apply (clarsimp simp:set_thread_state_def tcb_filter_modify_def bind_assoc) apply (rule dcorres_absorb_gets_the) apply (rule dcorres_rhs_noop_below_True[OF dcorres_rhs_noop_below_True[OF tcb_sched_action_dcorres _],
                                             OF set_thread_state_ext_dcorres _]) apply (clarsimp simp: set_object_def get_object_def in_monad simpler_modify_def put_def
                           return_def get_def bind_def corres_underlying_def mk_ef_def select_f_def) apply (frule ep_not_idle) apply (fastforce simp:obj_at_def is_ep_def) apply (simp add:transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp dest!: get_tcb_SomeD simp:transform_objects_update_other split:if_splits option.splits) apply (drule get_tcb_rev)+ apply (simp add:obj_at_def) apply (frule_tac epptr = epptr in get_endpoint_pick,simp,clarsimp simp:valid_ep_abstract_def) apply (clarsimp simp:ep_waiting_set_recv_def) apply (drule get_tcb_rev)+ apply  (clarsimp simp:lift_simp not_idle_thread_def) apply (drule(1) valid_etcbs_get_tcb_get_etcb)+ apply (auto simp: transform_tcb_def remove_pending_operation_def infer_tcb_pending_op_def
                       restrict_map_def tcb_slots infer_tcb_bound_notification_def
                       map_add_def get_tcb_def get_etcb_def is_etcb_at_def is_tcb
                 cong: transform_full_intent_cong split: option.splits)[1] apply (clarsimp simp:not_idle_thread_def | wp)+ apply (frule_tac pending_thread_in_recv_not_idle) apply (simp add:not_idle_thread_def)+ apply (frule ep_not_idle) apply (fastforce simp:obj_at_def is_ep_def) apply (clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def ep_not_idle not_idle_thread_def) apply (drule_tac epptr=epptr in get_endpoint_pick) apply (simp add:obj_at_def) apply (clarsimp simp:valid_ep_abstract_def) apply (clarsimp simp:ep_waiting_set_recv_def) apply (drule_tac ptr=x in valid_etcbs_tcb_etcb) apply (auto simp: is_etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and ko_at (kernel_object.Endpoint (RecvEP list)) epptr and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc epptr) (do queue <- get_ep_queue (RecvEP list);
_ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and ko_at (kernel_object.Endpoint (RecvEP list)) epptr and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc epptr) (do queue <- get_ep_queue (RecvEP list);
_ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and ko_at (kernel_object.Endpoint (RecvEP list)) epptr and valid_etcbs) (do s <- get;
tcb_filter_modify {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (\<lambda>x. case x of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))
od) (do _ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_state and valid_idle and ko_at (kernel_object.Endpoint (RecvEP list)) epptr and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (\<lambda>x. case x of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) (do _ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do return (?b5 s');
tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))
od) (do _ <- set_endpoint epptr IdleEP;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return (?b5 s')) (set_endpoint epptr IdleEP)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return (?b5 s') \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>r s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrace>
 4. \<And>s' rv rv'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') (K_bind (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) rv) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>r s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrace>
 2. \<And>s' rv rv'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') (K_bind (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) rv) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' rv rv'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') (K_bind (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) rv) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s) (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od)
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s) (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list)
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; valid_ep (RecvEP list) s'\<rbrakk> \<Longrightarrow> distinct list
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> inj_on id (set list)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 6. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 8. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; valid_ep (RecvEP list) s'\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> inj_on id (set list)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; valid_ep_abstract (RecvEP list) epptr s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; list \<noteq> [] \<and> set list = ep_waiting_set_recv epptr s' \<and> ep_waiting_set_send epptr s' = {} \<and> (\<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p')\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = ep_waiting_set_recv epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; list \<noteq> [] \<and> set list = ep_waiting_set_recv epptr s' \<and> ep_waiting_set_send epptr s' = {} \<and> (\<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p')\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads epptr (transform s') \<union> get_waiting_sync_send_threads epptr (transform s') \<union> get_waiting_ntfn_recv_threads epptr (transform s') = ep_waiting_set_recv epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; list \<noteq> []; set list = ep_waiting_set_recv epptr s'; ep_waiting_set_send epptr s' = {}; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ntfn_waiting_set epptr s' = ep_waiting_set_recv epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; list \<noteq> []; set list = ep_waiting_set_recv epptr s'; ep_waiting_set_send epptr s' = {}; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; list \<noteq> []; set list = ep_waiting_set_recv epptr s'; ep_waiting_set_send epptr s' = {}; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; ntfn_waiting_set epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ntfn_waiting_set epptr s' = ep_waiting_set_recv epptr s'
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; list \<noteq> []; set list = ep_waiting_set_recv epptr s'; ep_waiting_set_send epptr s' = {}; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; ntfn_waiting_set epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ntfn_waiting_set epptr s' = ep_waiting_set_recv epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_idle s \<and> tcb_at a s \<and> not_idle_thread a s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at a s) (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (do x <- gets_the (get_tcb a);
x <- KHeap_A.set_object a (TCB (update_tcb_state Restart x));
_ <- set_thread_state_ext a;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; valid_idle s'a \<and> tcb_at a s'a \<and> not_idle_thread a s'a \<and> idle_thread s'a = idle_thread s' \<and> is_etcb_at a s'a; get_tcb a s'a = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (do x <- KHeap_A.set_object a (TCB (update_tcb_state Restart obj'));
_ <- set_thread_state_ext a;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; valid_idle s'a \<and> tcb_at a s'a \<and> not_idle_thread a s'a \<and> idle_thread s'a = idle_thread s' \<and> is_etcb_at a s'a; get_tcb a s'a = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (KHeap_A.set_object a (TCB (update_tcb_state Restart obj')))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (5 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ep_at (?epptr72 s' a s'a obj' tcb) s'
 2. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb); not_idle_thread (?epptr72 s' a s'a obj' tcb) s'\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb); not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb); not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = (\<lambda>x. if x = a then case transform_objects s'a a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else transform_objects s'a x)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb x. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; get_tcb a s'a = Some obj'; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; kheap s'a a = Some (TCB tcb); not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) x = (if x = a then case transform_objects s'a a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else transform_objects s'a x)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; a \<in> set list; valid_idle s'a; tcb_at a s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; a \<in> set list; valid_idle s'a; \<exists>ko. kheap s'a a = Some ko \<and> is_tcb ko; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; a \<in> ep_waiting_set_recv epptr s'; valid_idle s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; get_tcb a s'a = Some tcb; list \<noteq> []; kheap s'a a = Some ko; is_tcb ko; set list = ep_waiting_set_recv epptr s'; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko t payload. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; valid_idle s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; get_tcb a s'a = Some tcb; list \<noteq> []; kheap s'a a = Some ko; is_tcb ko; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' a = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko t payload. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; valid_idle s'a; not_idle_thread a s'a; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; not_idle_thread epptr s'; get_tcb a s'a = Some tcb; list \<noteq> []; kheap s'a a = Some ko; is_tcb ko; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; tcb_state t = BlockedOnReceive epptr payload; get_tcb a s' = Some t\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb ko t payload. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; valid_idle s'a; a \<noteq> idle_thread s'; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; epptr \<noteq> idle_thread s'; get_tcb a s'a = Some tcb; list \<noteq> []; kheap s'a a = Some ko; is_tcb ko; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; tcb_state t = BlockedOnReceive epptr payload; get_tcb a s' = Some t\<rbrakk> \<Longrightarrow> Some (case ekheap s'a a of Some x \<Rightarrow> transform_tcb (machine_state s'a) a (update_tcb_state Restart tcb) x) = (case transform_object (machine_state s'a) a (ekheap s'a a) ko of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb ko t payload. \<lbrakk>valid_state s'; valid_idle s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_idle s'a; a \<noteq> idle_thread s'; idle_thread s'a = idle_thread s'; is_etcb_at a s'a; epptr \<noteq> idle_thread s'; get_tcb a s'a = Some tcb; list \<noteq> []; kheap s'a a = Some ko; is_tcb ko; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; tcb_state t = BlockedOnReceive epptr payload; get_tcb a s' = Some t; \<exists>etcb. get_etcb a s' = Some etcb\<rbrakk> \<Longrightarrow> Some (case ekheap s'a a of Some x \<Rightarrow> transform_tcb (machine_state s'a) a (update_tcb_state Restart tcb) x) = (case transform_object (machine_state s'a) a (ekheap s'a a) ko of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. valid_idle s \<and> tcb_at y s \<and> not_idle_thread y s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at y s\<rbrace>
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (3 subgoals):
 1. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; idle_thread s' \<in> set list; y \<in> set list; valid_idle s; tcb_at y s; y \<noteq> idle_thread s'; idle_thread s = idle_thread s'; is_etcb_at y s\<rbrakk> \<Longrightarrow> False
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (6 subgoals):
 1. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; idle_thread s' \<in> set list; y \<in> set list; valid_idle s; tcb_at y s; y \<noteq> idle_thread s'; idle_thread s = idle_thread s'; is_etcb_at y s\<rbrakk> \<Longrightarrow> valid_idle s'
 2. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; idle_thread s' \<in> set list; y \<in> set list; valid_idle s; tcb_at y s; y \<noteq> idle_thread s'; idle_thread s = idle_thread s'; is_etcb_at y s\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Endpoint (RecvEP (?list200 s' y s))) (?epptr200 s' y s) s'
 3. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; idle_thread s' \<in> set list; y \<in> set list; valid_idle s; tcb_at y s; y \<noteq> idle_thread s'; idle_thread s = idle_thread s'; is_etcb_at y s\<rbrakk> \<Longrightarrow> ?a200 s' y s \<in> set (?list200 s' y s)
 4. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; idle_thread s' \<in> set list; y \<in> set list; valid_idle s; tcb_at y s; y \<noteq> idle_thread s'; idle_thread s = idle_thread s'; is_etcb_at y s; not_idle_thread (?a200 s' y s) s'\<rbrakk> \<Longrightarrow> False
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle s \<and> tcb_at x s \<and> not_idle_thread x s \<and> idle_thread s = idle_thread s' \<and> is_etcb_at x s proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> x \<noteq> idle_thread s' \<and> is_etcb_at x s' proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'\<rbrakk> \<Longrightarrow> ep_at (?epptr201 s' s) s'
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'; not_idle_thread (?epptr201 s' s) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> x \<noteq> idle_thread s' \<and> is_etcb_at x s' proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; ko_at (kernel_object.Endpoint (RecvEP list)) epptr s'; valid_etcbs s'; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s'; not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Endpoint IdleEP)) s') \<and> x \<noteq> idle_thread s' \<and> is_etcb_at x s' proof (prove)
goal (1 subgoal):
 1. \<And>s' x tcb. \<lbrakk>valid_state s'; kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal (2 subgoals):
 1. \<And>s' x tcb. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> kheap s' epptr = Some (kernel_object.Endpoint (?endpoint226 s' x tcb))
 2. \<And>s' x tcb. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); valid_ep_abstract (?endpoint226 s' x tcb) epptr s'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal (1 subgoal):
 1. \<And>s' x tcb. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); valid_ep_abstract (RecvEP list) epptr s'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal (1 subgoal):
 1. \<And>s' x tcb. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; x \<in> ep_waiting_set_recv epptr s'; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); list \<noteq> []; set list = ep_waiting_set_recv epptr s'; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal (1 subgoal):
 1. \<And>s' x tcb t payload. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); valid_etcbs s'; epptr \<noteq> idle_thread_ptr; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' x = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal (2 subgoals):
 1. \<And>s' x tcb t payload. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); epptr \<noteq> idle_thread_ptr; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' x = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> kheap s' x = Some (TCB (?tcb235 s' x tcb t payload))
 2. \<And>s' x tcb t payload. \<lbrakk>kheap s' epptr = Some (kernel_object.Endpoint (RecvEP list)); epptr \<noteq> idle_thread_ptr; idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> (\<exists>payload. tcb_state t = BlockedOnReceive epptr payload)}; none_is_sending_ep epptr s'; \<forall>p'. Some (kernel_object.Endpoint (RecvEP list)) = kheap s' p' \<longrightarrow> epptr = p'; kheap s' x = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload; \<exists>etcb. ekheap s' x = Some etcb\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Endpoint IdleEP) \<and> is_etcb_at epptr s') \<and> (x \<noteq> epptr \<longrightarrow> x \<noteq> idle_thread_ptr \<and> is_etcb_at x s') proof (prove)
goal:
No subgoals!