theory IpcCancel_AI

lemma cancel_all_signals_unlive[wp]:
  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr s\<rbrace>
     cancel_all_signals ntfnptr
   \<lbrace>\<lambda> rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>" apply (simp add: cancel_all_signals_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp
        | wpc
        | simp add: unbind_maybe_notification_def)+ apply (rule_tac Q="\<lambda>_. obj_at (is_ntfn and Not \<circ> live) ntfnptr" in hoare_post_imp) apply (fastforce elim: obj_at_weakenE) apply (wp mapM_x_wp' sts_obj_at_impossible
          | simp add: is_ntfn)+ apply (simp add: set_simple_ko_def) apply (wp get_object_wp obj_set_prop_at) apply (auto simp: live_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ 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. obj_at (Not \<circ> live) ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ 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 () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ 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 () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?B27 ntfn x2 ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) x2 \<lbrace>\<lambda>x. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B27 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 4. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R19 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn x2 rv s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn x2; obj_at (is_ntfn and Not \<circ> live) ntfnptr s\<rbrakk> \<Longrightarrow> obj_at (Not \<circ> live) ntfnptr s
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?B27 ntfn x2 ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) x2 \<lbrace>\<lambda>_. obj_at (is_ntfn and Not \<circ> live) ntfnptr\<rbrace>
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B27 ntfn x2\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 5. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R19 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?B27 ntfn x2 ()\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) x2 \<lbrace>\<lambda>_. obj_at (is_ntfn and Not \<circ> live) ntfnptr\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B27 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 4. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R19 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>a. obj_at (\<lambda>a. (\<exists>ep. a = Notification ep) \<and> \<not> live a) ntfnptr\<rbrace>
 2. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 3. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R19 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> do obj <- get_object ntfnptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Notification y = obj);
set_object ntfnptr (Notification (ntfn_set_obj ntfn IdleNtfn))
od \<lbrace>\<lambda>a. obj_at (\<lambda>a. (\<exists>ep. a = Notification ep) \<and> \<not> live a) ntfnptr\<rbrace>
 2. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 3. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R19 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R20 ntfn x3\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ntfnptr\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> obj_at (Not \<circ> live) ntfnptr s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> (\<forall>ko. ko_at ko ntfnptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Notification y = ko) \<longrightarrow> (\<exists>ep. Notification (ntfn_set_obj ntfn IdleNtfn) = Notification ep) \<and> \<not> live (Notification (ntfn_set_obj ntfn IdleNtfn)))) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal:
No subgoals!