theory KHeap_DR

lemma dcorres_cancel_all_signals:
  "dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.cancel_all_ipc oid)
          (cancel_all_signals oid)" apply (clarsimp simp: cancel_all_signals_def 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 ntfn_ext y) apply (case_tac "ntfn_obj ntfn_ext") 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_notification_pick,simp) apply (simp add:valid_ntfn_abstract_def none_is_waiting_ntfn_def) apply (simp add:ntfn_waiting_set_lift ep_waiting_set_send_lift ep_waiting_set_recv_lift) apply (frule ntfn_not_waiting_ep_send[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply (drule ntfn_not_waiting_ep_recv[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply clarsimp+ apply (rule corres_guard_imp) apply (rule fast_finalise_wait_ntfn[simplified]) apply (simp add:obj_at_def)+ 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_notification_pick,simp) apply (simp add:valid_ntfn_abstract_def none_is_waiting_ntfn_def) apply (simp add:ntfn_waiting_set_lift ep_waiting_set_send_lift ep_waiting_set_recv_lift) apply (frule ntfn_not_waiting_ep_send[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply (drule ntfn_not_waiting_ep_recv[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply clarsimp+ 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) (cancel_all_signals 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 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);
ntfn <- case partial_inv kernel_object.Notification (the (kheap x oid)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj ntfn IdleNtfn;
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 | _ \<Rightarrow> return ()
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);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s' oid)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj ntfn IdleNtfn;
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 | _ \<Rightarrow> return ()
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4 y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification x4; kheap s' oid = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj x4 of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' ntfn_ext y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext y. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = IdleNtfn\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 2. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 3. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn\<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' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 3. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; 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' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 3. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s' ntfn_ext s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; 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' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s' ntfn_ext s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; 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' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn\<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' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; valid_ntfn_abstract ntfn_ext 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' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set 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' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (6 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> valid_objs s'a
 2. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 6. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (6 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> valid_objs s'a
 2. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}; ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 6. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn_ext s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = IdleNtfn; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}; ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = IdleNtfn; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext y x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ())
 5. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (2 subgoals):
 1. \<And>s' ntfn_ext x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (do _ <- set_notification oid (ntfn_set_obj ntfn_ext IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od)
 2. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (4 subgoals):
 1. \<And>s' ntfn_ext x2. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc (?Q70 s' ntfn_ext x2) (?Q'70 s' ntfn_ext x2) (PageTableUnmap_D.cancel_all_ipc oid) (do _ <- set_notification oid (ntfn_set_obj ntfn_ext IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od)
 2. \<And>s' ntfn_ext x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2; transform s' = s\<rbrakk> \<Longrightarrow> ?Q70 s' ntfn_ext x2 s
 3. \<And>s' ntfn_ext x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2; s' = s\<rbrakk> \<Longrightarrow> ?Q'70 s' ntfn_ext x2 s
 4. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' ntfn_ext x2 s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = WaitingNtfn x2; s' = s\<rbrakk> \<Longrightarrow> (valid_state and valid_idle and valid_etcbs and ko_at (kernel_object.Notification ntfn_ext) oid and (\<lambda>_. ntfn_obj ntfn_ext = WaitingNtfn x2)) s
 3. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; the (kheap s' oid) = kernel_object.Notification ntfn_ext; kheap s' oid = Some y; ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (case ntfn_obj ntfn_ext of WaitingNtfn queue \<Rightarrow> do _ <- set_notification oid $ ntfn_set_obj (THE y. kernel_object.Notification y = the (kheap s' oid)) IdleNtfn;
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 | _ \<Rightarrow> return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' ntfn_ext y x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; y = kernel_object.Notification ntfn_ext; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.cancel_all_ipc oid) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' ntfn_ext x3. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3\<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 ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' ntfn_ext x3 s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; 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 ()) proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext x3 s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; 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' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>s' ntfn_ext x3 s'a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; 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' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3\<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' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; valid_ntfn_abstract ntfn_ext 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' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set 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' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}\<rbrakk> \<Longrightarrow> valid_objs s'a
 2. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; kheap s'a oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}\<rbrakk> \<Longrightarrow> valid_objs s'a
 2. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}; ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn_ext x3 s'a. \<lbrakk>valid_state s'a; valid_idle s'a; valid_etcbs s'a; ntfn_obj ntfn_ext = ActiveNtfn x3; set_option (ntfn_bound_tcb ntfn_ext) = ntfn_bound_set oid s'a \<and> ntfn_waiting_set oid s'a = {}; ep_waiting_set_send oid s'a = {}; ep_waiting_set_recv oid s'a = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv oid s'a = {} \<and> ep_waiting_set_send oid s'a = {}
 2. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' ntfn_ext x3 s'a s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' oid = Some (kernel_object.Notification ntfn_ext); ntfn_obj ntfn_ext = ActiveNtfn x3; transform s' = transform s'a; s' = s'a; s'a = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!