theory Ipc_DR

lemma valid_idle_cancel_all_signals:
  "\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.cancel_all_signals word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>" including no_pre apply (simp add:cancel_all_signals_def) apply (wp|wpc|simp)+ apply (rename_tac list) apply (rule_tac I = "(\<lambda>s. (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
                    and ko_at (kernel_object.Notification (ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn)) word1 and valid_idle" in mapM_x_inv_wp) apply clarsimp apply (wp KHeap_DR.tcb_at_set_thread_state_wp) apply (rule hoare_conjI) apply (rule_tac P="(\<lambda>s. (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
                and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn)) word1"
              in hoare_vcg_precond_imp) apply (rule set_thread_state_ko) apply (simp add:is_tcb_def) apply (wp valid_idle_set_thread_state)+ apply (clarsimp simp:)+ apply (rule hoare_vcg_conj_lift) apply (rule hoare_Ball_helper) apply (wp set_simple_ko_tcb| clarsimp simp : not_idle_thread_def)+ apply (wp simple_obj_set_prop_at)+ apply (rule hoare_strengthen_post[OF get_simple_ko_sp]) apply (clarsimp  | rule conjI)+ apply (clarsimp simp:obj_at_def valid_pspace_def valid_state_def) apply (drule(1) valid_objs_valid_ntfn_simp) apply (clarsimp simp:is_tcb_def valid_ntfn_def obj_at_def) apply (drule(1) pending_thread_in_wait_not_idle) apply (simp add:not_idle_thread_def obj_at_def is_ntfn_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> cancel_all_signals word1 \<lbrace>\<lambda>a. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> cancel_all_signals word1 \<lbrace>\<lambda>a. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> do ntfn <- get_notification word1;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification word1 $ 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>a. valid_idle\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?B21 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>a. valid_idle\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B21 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn list. ntfn_obj ntfn = WaitingNtfn list \<Longrightarrow> \<lbrace>?B21 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>a. valid_idle\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>?B21 ntfn x2\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P27 ntfn list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 3. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> ?P27 ntfn list s
 4. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 5. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P27 ntfn list\<rbrace> do y <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 2. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> ?P27 ntfn list s
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'40 ntfn list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>rv s. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'40 ntfn list s
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'40 ntfn list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1\<rbrace>
 2. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?P'40 ntfn list\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ?P'40 ntfn list s
 4. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 5. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>?Q47 ntfn list x\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1\<rbrace>
 2. \<And>ntfn list x s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s\<rbrakk> \<Longrightarrow> ?Q47 ntfn list x s
 3. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 4. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s
 5. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 6. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 7. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ntfn list x s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s\<rbrakk> \<Longrightarrow> (ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and K (\<not> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)))) s
 2. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s
 4. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 5. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 6. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list x. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1\<rbrace> set_thread_state x Restart \<lbrace>\<lambda>r. valid_idle\<rbrace>
 2. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list x s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; x \<in> set list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s\<rbrakk> \<Longrightarrow> (not_idle_thread x and valid_idle) s
 2. \<And>ntfn list s. \<lbrakk>ntfn_obj ntfn = WaitingNtfn list; ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. tcb_at x s \<and> not_idle_thread x s) \<and> ((\<lambda>s. \<forall>a\<in>set list. tcb_at a s \<and> not_idle_thread a s) and valid_idle and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1) s
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 $ ntfn_set_obj ntfn IdleNtfn \<lbrace>\<lambda>a. (\<lambda>s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s) and ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 and valid_idle\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?R13 ntfn x2\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>a b. (\<forall>a\<in>set x2. tcb_at a b \<and> not_idle_thread a b) \<and> ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 b \<and> valid_idle b\<rbrace>
 2. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 3. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R13 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?P56 ntfn x2\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. \<forall>a\<in>set x2. tcb_at a s \<and> not_idle_thread a s\<rbrace>
 2. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?P'56 ntfn x2\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 s \<and> valid_idle s\<rbrace>
 3. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 4. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?P56 ntfn x s \<and> ?P'56 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn x2 a. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?P59 ntfn x2 a\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. tcb_at a s \<and> not_idle_thread a s\<rbrace>
 2. \<And>ntfn x2 P. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (set x2)\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. P (set x2)\<rbrace>
 3. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?P'56 ntfn x2\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 s \<and> valid_idle s\<rbrace>
 4. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 5. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> (\<forall>xa\<in>set x. ?P59 ntfn x xa s) \<and> ?P'56 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x2. ntfn_obj ntfn = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?P'56 ntfn x2\<rbrace> set_notification word1 (ntfn_set_obj ntfn IdleNtfn) \<lbrace>\<lambda>rv s. ko_at (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) word1 s \<and> valid_idle s\<rbrace>
 2. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?R14 ntfn x3\<rbrace> return () \<lbrace>\<lambda>a. valid_idle\<rbrace>
 3. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> ?P'56 ntfn x s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R14 ntfn x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_state\<rbrace> get_notification word1 \<lbrace>\<lambda>ntfn s. (ntfn_obj ntfn = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn) = kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn) \<and> (obj_at (\<lambda>ko. partial_inv kernel_object.Notification ko \<noteq> None) word1 and valid_idle) s) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> valid_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (ko_at (kernel_object.Notification rv) word1 and (valid_idle and valid_state)) s \<Longrightarrow> (ntfn_obj rv = IdleNtfn \<longrightarrow> valid_idle s) \<and> (\<forall>x. ntfn_obj rv = WaitingNtfn x \<longrightarrow> (\<forall>x\<in>set x. tcb_at x s \<and> x \<noteq> idle_thread s) \<and> kernel_object.Notification (ntfn_set_obj rv IdleNtfn) = kernel_object.Notification (ntfn_set_obj rv IdleNtfn) \<and> (obj_at (\<lambda>ko. partial_inv kernel_object.Notification ko \<noteq> None) word1 and valid_idle) s) \<and> (\<forall>x. ntfn_obj rv = ActiveNtfn x \<longrightarrow> valid_idle s) proof (prove)
goal (3 subgoals):
 1. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> tcb_at xa s
 2. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>rv s x. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) word1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Notification rv); valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>rv s x. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) word1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s x xa. \<lbrakk>kheap s word1 = Some (kernel_object.Notification rv); valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; valid_ntfn rv s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s xa = Some ko \<and> is_tcb ko
 2. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 3. \<And>rv s x. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) word1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 2. \<And>rv s x. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) word1 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> ?a133 rv s x xa \<in> set (?list133 rv s x xa)
 2. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification (?ntfn133 rv s x xa)) (?epptr133 rv s x xa) s
 3. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn133 rv s x xa) = WaitingNtfn (?list133 rv s x xa)
 4. \<And>rv s x xa. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; ntfn_obj rv = WaitingNtfn x; xa \<in> set x; not_idle_thread (?a133 rv s x xa) s\<rbrakk> \<Longrightarrow> xa \<noteq> idle_thread s
 5. \<And>rv s x. \<lbrakk>ko_at (kernel_object.Notification rv) word1 s; valid_idle s; valid_state s; ntfn_obj rv = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) word1 s proof (prove)
goal:
No subgoals!