theory DetSchedSchedule_AI

lemma send_signal_valid_sched[wp]:
  "\<lbrace> valid_sched and invs \<rbrace> send_signal ntfnptr badge \<lbrace> \<lambda>_. valid_sched \<rbrace>" apply (simp add: send_signal_def) apply (wp get_simple_ko_wp possible_switch_to_valid_sched_except
            set_thread_state_runnable_valid_queues set_thread_state_runnable_valid_sched_action
            set_thread_state_valid_blocked_except sts_st_tcb_at' gts_wp  | wpc | clarsimp)+ apply (rename_tac ntfn a st) apply (rule_tac Q="\<lambda>rv s. valid_sched s \<and> a \<noteq> idle_thread s \<and> not_cur_thread a s" in hoare_strengthen_post) apply (wp gts_wp get_simple_ko_wp | simp add: valid_sched_def)+ apply (clarsimp) apply (rule conjI, clarsimp, rule conjI) apply (frule invs_valid_idle) apply (clarsimp simp: receive_blocked_def split: thread_state.splits) apply (drule (1) st_tcb_at_idle_thread, clarsimp) apply (clarsimp simp: receive_blocked_def split: thread_state.splits) apply ((auto simp: pred_tcb_at_def obj_at_def valid_sched_action_def
            is_activatable_def not_cur_thread_def | drule sym)+)[1] apply (clarsimp) apply (frule invs_valid_idle) apply (drule_tac ptr=ntfnptr and rt=NTFNSignal and queue="set x" in idle_not_queued'') apply (clarsimp simp: invs_sym_refs) apply (simp add: state_refs_of_def obj_at_def) apply (frule invs_valid_objs) apply (simp add: valid_objs_def obj_at_def) apply (drule_tac x = ntfnptr in bspec) apply (simp add: dom_def) apply (clarsimp simp: valid_obj_def valid_ntfn_def) apply (drule hd_in_set) apply (rule conjI, clarsimp) apply (clarsimp) apply (cut_tac t="hd x" and P="\<lambda>st. \<not>activatable st" in ntfn_queued_st_tcb_at) apply ((simp add: obj_at_def ntfn_q_refs_of_def invs_def valid_state_def valid_pspace_def)+)[4] apply simp apply (clarsimp simp add: valid_sched_def valid_sched_action_def is_activatable_def st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | Some tcb \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ntfn x2 st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?P'104 ntfn x2 st\<rbrace> cancel_ipc x2 \<lbrace>\<lambda>rv s. valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> not_cur_thread x2 s \<and> x2 \<noteq> idle_thread s\<rbrace>
 2. \<And>ntfn x2 st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R35 ntfn x2 st\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ntfn x2. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R27 ntfn x2\<rbrace> get_thread_state x2 \<lbrace>\<lambda>st s. (receive_blocked st \<longrightarrow> valid_etcbs s \<and> ?P'104 ntfn x2 st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R35 ntfn x2 st s)\<rbrace>
 4. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> update_waiting_ntfn ntfnptr x2 (ntfn_bound_tcb ntfn) badge \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge x3) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> ?R27 ntfn x s)) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R14 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 7. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?P'104 ntfn a st\<rbrace> cancel_ipc a \<lbrace>\<lambda>rv s. valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> not_cur_thread a s \<and> a \<noteq> idle_thread s\<rbrace>
 2. \<And>ntfn x2 st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R35 ntfn x2 st\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>ntfn x2. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R27 ntfn x2\<rbrace> get_thread_state x2 \<lbrace>\<lambda>st s. (receive_blocked st \<longrightarrow> valid_etcbs s \<and> ?P'104 ntfn x2 st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R35 ntfn x2 st s)\<rbrace>
 4. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> update_waiting_ntfn ntfnptr x2 (ntfn_bound_tcb ntfn) badge \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge x3) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> ?R27 ntfn x s)) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R14 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 7. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?P'104 ntfn a st\<rbrace> cancel_ipc a \<lbrace>\<lambda>rv s. valid_sched s \<and> a \<noteq> idle_thread s \<and> not_cur_thread a s\<rbrace>
 2. \<And>ntfn a st rv s. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st; valid_sched s \<and> a \<noteq> idle_thread s \<and> not_cur_thread a s\<rbrakk> \<Longrightarrow> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> valid_blocked s \<and> not_cur_thread a s \<and> a \<noteq> idle_thread s
 3. \<And>ntfn x2 st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R35 ntfn x2 st\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>ntfn x2. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R27 ntfn x2\<rbrace> get_thread_state x2 \<lbrace>\<lambda>st s. (receive_blocked st \<longrightarrow> valid_etcbs s \<and> ?P'104 ntfn x2 st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R35 ntfn x2 st s)\<rbrace>
 5. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> update_waiting_ntfn ntfnptr x2 (ntfn_bound_tcb ntfn) badge \<lbrace>\<lambda>_. valid_sched\<rbrace>
 6. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge x3) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 7. \<lbrace>?Q\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> ?R27 ntfn x s)) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R14 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 8. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> invs s \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> x \<noteq> idle_thread s \<and> not_cur_thread x s))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> x \<noteq> idle_thread s \<and> not_cur_thread x s))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s)) proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s
 2. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> not_cur_thread x s
 3. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; valid_idle s\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s
 2. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> not_cur_thread x s
 3. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x41 x42. \<lbrakk>valid_idle s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some (idle_thread s); st_tcb_at ((=) (BlockedOnReceive x41 x42)) (idle_thread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> not_cur_thread x s
 3. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> not_cur_thread x s
 2. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x x41 x42. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) (BlockedOnReceive x41 x42)) x s\<rbrakk> \<Longrightarrow> not_cur_thread x s
 2. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x; valid_idle s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> set x \<times> {NTFNSignal} \<subseteq> state_refs_of s ntfnptr
 3. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> set x \<times> {NTFNSignal} \<subseteq> state_refs_of s ntfnptr
 2. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; valid_objs s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x\<rbrakk> \<Longrightarrow> ntfnptr \<in> dom (kheap s)
 2. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<exists>obj. kheap s ntfnptr = Some obj \<and> valid_obj ntfnptr obj s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<exists>obj. kheap s ntfnptr = Some obj \<and> valid_obj ntfnptr obj s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; x \<noteq> []; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; hd x \<in> set x\<rbrakk> \<Longrightarrow> hd x \<noteq> idle_thread s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; hd x \<in> set x\<rbrakk> \<Longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> hd x \<noteq> cur_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> ko_at (Notification (?ep294 s ntfn x)) (?ptr294 s ntfn x) (?s294 s ntfn x)
 2. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> (hd x, ?rt294 s ntfn x) \<in> ntfn_q_refs_of (ntfn_obj (?ep294 s ntfn x))
 3. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> valid_objs (?s294 s ntfn x)
 4. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of (?s294 s ntfn x))
 5. \<And>s ntfn x ref. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> \<not> activatable (BlockedOnNotification ref)
 6. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s; st_tcb_at (\<lambda>st. \<not> activatable st) (hd x) (?s294 s ntfn x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x ref. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s\<rbrakk> \<Longrightarrow> \<not> activatable (BlockedOnNotification ref)
 2. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s; st_tcb_at (\<lambda>st. \<not> activatable st) (hd x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_sched_action_2 resume_cur_thread (ekheap s) (kheap s) (cur_thread s) (cur_domain s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; invs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = WaitingNtfn x; idle_thread s \<notin> set x; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; cur_thread s \<in> set x; scheduler_action s = resume_cur_thread; hd x = cur_thread s; st_tcb_at (\<lambda>st. \<not> activatable st) (hd x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!