theory DetSchedSchedule_AI

lemma cancel_all_signals_not_queued:
  "\<lbrace>st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t
         and sym_refs \<circ> state_refs_of\<rbrace>
    cancel_all_signals epptr
   \<lbrace>\<lambda>rv. not_queued t\<rbrace>" apply (simp add: cancel_all_signals_def) apply (wp reschedule_required_not_queued | wpc | simp)+ apply (rename_tac list) apply (rule_tac P="(t \<notin> set list)" in hoare_gen_asm) apply (rule_tac S="set list - {t}" in mapM_x_wp) apply (wp tcb_sched_action_enqueue_not_queued | clarsimp)+ apply (wp hoare_vcg_imp_lift
         | simp add: get_simple_ko_def get_object_def a_type_def split: kernel_object.splits
         | wpc | wp (once) hoare_vcg_all_lift)+ apply safe apply (rename_tac ep x y) apply (drule_tac P="\<lambda>ts. \<not> active ts" and ep=ep in
         ntfn_queued_st_tcb_at[rotated, rotated]) apply (simp_all only: st_tcb_at_not) apply (fastforce simp: obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of\<rbrace> cancel_all_signals epptr \<lbrace>\<lambda>rv. not_queued t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of\<rbrace> do ntfn <- get_notification epptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification epptr $ 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 \<lbrace>\<lambda>rv. not_queued t\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?B22 ntfn x2 ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2 \<lbrace>\<lambda>rv s. not_queued t s \<and> scheduler_act_not t s\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> set_notification epptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B22 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. not_queued t\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_notification epptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> not_queued t 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>
 5. \<And>s. (st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list. ntfn_obj ntfn = WaitingNtfn list \<Longrightarrow> \<lbrace>?B22 ntfn list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>rv s. not_queued t s \<and> scheduler_act_not t s\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> set_notification epptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B22 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. not_queued t\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_notification epptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> not_queued t 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>
 5. \<And>s. (st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; t \<notin> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'34 ntfn list ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list \<lbrace>\<lambda>rv s. not_queued t s \<and> scheduler_act_not t s\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> set_notification epptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. ?P'34 ntfn x2 a and K (t \<notin> set x2)\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. not_queued t\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_notification epptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> not_queued t 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>
 5. \<And>s. (st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; t \<notin> set list; x \<in> set list - {t}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. not_queued t a \<and> scheduler_act_not t a\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv a. not_queued t a \<and> scheduler_act_not t a\<rbrace>
 2. \<And>ntfn list. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; t \<notin> set list\<rbrakk> \<Longrightarrow> set list \<subseteq> set list - {t}
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R14 ntfn x2\<rbrace> set_notification epptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>a. not_queued t a \<and> scheduler_act_not t a) and K (t \<notin> set x2)\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. not_queued t\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_notification epptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> not_queued t 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>
 6. \<And>s. (st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_notification epptr \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> not_queued t s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> not_queued t s \<and> scheduler_act_not t s \<and> t \<notin> set x) \<and> ((\<exists>x. ntfn_obj ntfn = ActiveNtfn x) \<longrightarrow> not_queued t s)\<rbrace>
 2. \<And>s. (st_tcb_at active t and valid_objs and not_queued t and scheduler_act_not t and sym_refs \<circ> state_refs_of) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at active t s \<and> valid_objs s \<and> not_queued t s \<and> scheduler_act_not t s \<and> sym_refs (state_refs_of s) \<Longrightarrow> \<forall>x4. the (kheap s epptr) = Notification x4 \<longrightarrow> kheap s epptr = None \<or> (\<forall>x. ntfn_obj x4 = WaitingNtfn x \<longrightarrow> t \<notin> set x) proof (prove)
goal (1 subgoal):
 1. \<And>s x4 x y. \<lbrakk>st_tcb_at active t s; valid_objs s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification x4; kheap s epptr = Some y; ntfn_obj x4 = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; valid_objs s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<And>s ep x y ref. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> \<not> active (BlockedOnNotification ref)
 3. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> ko_at (Notification ep) (?ptr182 s ep x y) s
 4. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> (?t182 s ep x y, ?rt182 s ep x y) \<in> ntfn_q_refs_of (ntfn_obj ep)
 5. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (kheap s epptr) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x; st_tcb_at (\<lambda>ts. \<not> active ts) (?t182 s ep x y) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s ep x y ref. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (Some y) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> \<not> active (BlockedOnNotification ref)
 2. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (Some y) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> ko_at (Notification ep) (?ptr182 s ep x y) s
 3. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (Some y) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x\<rbrakk> \<Longrightarrow> (?t182 s ep x y, ?rt182 s ep x y) \<in> ntfn_q_refs_of (WaitingNtfn x)
 4. \<And>s ep x y. \<lbrakk>st_tcb_at active t s; not_queued t s; scheduler_act_not t s; sym_refs (state_refs_of s); the (Some y) = Notification ep; kheap s epptr = Some y; ntfn_obj ep = WaitingNtfn x; t \<in> set x; \<not> st_tcb_at active (?t182 s ep x y) s \<and> tcb_at (?t182 s ep x y) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!