theory IpcCancel_AI

lemma cancel_all_signals_valid_objs:
  "\<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace>
   cancel_all_signals ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: cancel_all_signals_def unbind_maybe_notification_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp unbind_notification_valid_objs | wpc | simp_all add:unbind_maybe_notification_def)+ apply (wp cancel_all_helper hoare_vcg_const_Ball_lift
             set_simple_ko_valid_objs unbind_notification_valid_objs
        | clarsimp simp: ntfn_queued_st_tcb_at obj_at_def
                         valid_ntfn_def valid_bound_tcb_def
        | wpc)+ apply (clarsimp split: option.splits) apply (erule (1) valid_objsE) apply (simp add: valid_obj_def valid_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> cancel_all_signals ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> do ntfn <- get_notification ptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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. valid_objs\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))) 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. valid_objs\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R19 ntfn x2\<rbrace> set_notification ptr (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. valid_objs\<rbrace>
 4. \<And>ntfn s. ko_at (Notification ntfn) ptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> (\<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 (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>kheap s ptr = Some (Notification ntfn); valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at t s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x x2. \<lbrakk>kheap s ptr = Some (Notification ntfn); valid_objs s; sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x; ntfn_bound_tcb ntfn = Some x2\<rbrakk> \<Longrightarrow> tcb_at x2 s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x x2. \<lbrakk>kheap s ptr = Some (Notification ntfn); sym_refs (state_refs_of s); ntfn_obj ntfn = WaitingNtfn x; ntfn_bound_tcb ntfn = Some x2; valid_obj ptr (Notification ntfn) s\<rbrakk> \<Longrightarrow> tcb_at x2 s proof (prove)
goal:
No subgoals!