theory KHeap_DR

lemma dcorres_cancel_all_ipc:
  "dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc oid)
          (IpcCancel_A.cancel_all_ipc oid)" apply (simp add:IpcCancel_A.cancel_all_ipc_def IpcCancel_A.cancel_all_signals_def
                  PageTableUnmap_D.fast_finalise_def partial_inv_def) apply (clarsimp simp:get_simple_ko_def get_object_def bind_assoc gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:assert_def corres_free_fail partial_inv_def a_type_def
          split:Structures_A.kernel_object.splits, safe) apply (rename_tac endpoint y) apply (case_tac endpoint) apply (clarsimp simp:cancel_all_ipc_def_alt1) apply (rule dcorres_absorb_get_l) apply (rule filter_modify_empty_corres[THEN corres_guard_imp]) apply (subst is_thread_blocked_on_sth[simplified]) apply clarsimp apply (frule_tac epptr = oid in get_endpoint_pick,simp) apply (simp add:valid_ep_abstract_def none_is_sending_ep_def none_is_receiving_ep_def) apply (simp add: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 simp apply clarsimp+ apply (rule corres_guard_imp) apply (rule fast_finalise_send_ep) apply (simp add:obj_at_def)+ apply (rule corres_guard_imp) apply (rule fast_finalise_recv_ep) apply (simp add:obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc oid) (IpcCancel_A.cancel_all_ipc oid) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc oid) (do ep <- get_endpoint oid;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint oid 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) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc oid) (do x <- get;
xa <- assert (\<exists>y. kheap x oid = Some y);
xa <- assert (a_type (the (kheap x oid)) = AEndpoint \<or> a_type (the (kheap x oid)) = ANTFN);
ep <- case partial_inv kernel_object.Endpoint (the (kheap x oid)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint oid 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) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_state and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (do x <- assert (\<exists>y. kheap s' oid = Some y);
x <- assert (a_type (the (kheap s' oid)) = AEndpoint \<or> a_type (the (kheap s' oid)) = ANTFN);
ep <- case partial_inv kernel_object.Endpoint (the (kheap s' oid)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint oid 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) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3 y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint x3; kheap s' oid = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case x3 of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (1 subgoal):
 1. \<And>s' endpoint y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (3 subgoals):
 1. \<And>s' endpoint y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = IdleEP\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 2. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 3. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
tcb_filter_modify {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb oid} (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) (return ())
 2. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 3. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (3 subgoals):
 1. \<And>s' s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s'a) x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb oid} (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)))) (return ())
 2. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 3. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s'a) x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb oid} = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s' s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads oid (transform s'a) \<union> get_waiting_sync_send_threads oid (transform s'a) \<union> get_waiting_ntfn_recv_threads oid (transform s'a) = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Endpoint IdleEP)\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads oid (transform s'a) = {} \<and> get_waiting_sync_send_threads oid (transform s'a) = {} \<and> get_waiting_ntfn_recv_threads oid (transform s'a) = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Endpoint IdleEP); valid_ep_abstract IdleEP oid s'a\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads oid (transform s'a) = {} \<and> get_waiting_sync_send_threads oid (transform s'a) = {} \<and> get_waiting_ntfn_recv_threads oid (transform s'a) = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Endpoint IdleEP); ep_waiting_set_send oid s'a = {} \<and> ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads oid (transform s'a) = {} \<and> get_waiting_sync_send_threads oid (transform s'a) = {} \<and> get_waiting_ntfn_recv_threads oid (transform s'a) = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Endpoint IdleEP); ep_waiting_set_send oid s'a = {} \<and> ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> ntfn_waiting_set oid s'a = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (6 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ep_waiting_set_send oid s'a = {} \<and> ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> valid_objs s'a
 2. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ep_waiting_set_send oid s'a = {} \<and> ep_waiting_set_recv oid s'a = {}; ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> ntfn_waiting_set oid s'a = {}
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 6. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ep_waiting_set_send oid s'a = {} \<and> ep_waiting_set_recv oid s'a = {}; ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> ntfn_waiting_set oid s'a = {}
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 5. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (4 subgoals):
 1. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint IdleEP); transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' endpoint y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = SendEP x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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)
 4. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (2 subgoals):
 1. \<And>s' x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (do queue <- get_ep_queue (SendEP x2);
y <- set_endpoint oid IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od)
 2. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (4 subgoals):
 1. \<And>s' x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2))\<rbrakk> \<Longrightarrow> dcorres dc (?Q70 s' x2) (?Q'70 s' x2) (PageTableUnmap_D.cancel_all_ipc oid) (do queue <- get_ep_queue (SendEP x2);
y <- set_endpoint oid IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od)
 2. \<And>s' x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q70 s' x2 s
 3. \<And>s' x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2)); s' = s\<rbrakk> \<Longrightarrow> ?Q'70 s' x2 s
 4. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (3 subgoals):
 1. \<And>s' x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2)); transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Endpoint (SendEP x2)); s' = s\<rbrakk> \<Longrightarrow> (valid_state and valid_idle and ko_at (kernel_object.Endpoint (SendEP x2)) oid and valid_etcbs) s
 3. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Endpoint endpoint; kheap s' oid = Some y; endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case endpoint of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue (THE y. kernel_object.Endpoint y = the (kheap s' oid));
set_endpoint oid 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) proof (prove)
goal (1 subgoal):
 1. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (do queue <- get_ep_queue (RecvEP x3);
y <- set_endpoint oid IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' endpoint y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3\<rbrakk> \<Longrightarrow> dcorres dc (?Q75 s' endpoint y x3) (?Q'75 s' endpoint y x3) (PageTableUnmap_D.cancel_all_ipc oid) (do queue <- get_ep_queue (RecvEP x3);
y <- set_endpoint oid IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) queue;
reschedule_required
od)
 2. \<And>s' endpoint y x3 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3; transform s' = s\<rbrakk> \<Longrightarrow> ?Q75 s' endpoint y x3 s
 3. \<And>s' endpoint y x3 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3; s' = s\<rbrakk> \<Longrightarrow> ?Q'75 s' endpoint y x3 s proof (prove)
goal (2 subgoals):
 1. \<And>s' endpoint y x3 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' endpoint y x3 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Endpoint (RecvEP x3); kheap s' oid = Some (kernel_object.Endpoint (RecvEP x3)); endpoint = RecvEP x3; s' = s\<rbrakk> \<Longrightarrow> (valid_state and valid_idle and ko_at (kernel_object.Endpoint (RecvEP x3)) oid and valid_etcbs) s proof (prove)
goal:
No subgoals!