theory KHeap_DR

lemma dcorres_unbind_maybe_notification:
  "dcorres dc \<top> (valid_etcbs and valid_idle and valid_state)
   (PageTableUnmap_D.unbind_maybe_notification ntfn)
   (unbind_maybe_notification ntfn)" apply (simp add: PageTableUnmap_D.unbind_maybe_notification_def IpcCancel_A.unbind_maybe_notification_def) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_ntfn_bound_tcb, unfolded  fun_app_def, simplified]) apply (simp add: option_set_option_select) apply (rule_tac P'="case (ntfn_bound_tcb ntfna) of None \<Rightarrow> R' | Some x \<Rightarrow> R''" for R' R'' in corres_inst) apply (rule_tac P="case (set_to_option (set_option (ntfn_bound_tcb ntfna))) of None \<Rightarrow> R | Some x \<Rightarrow> R'''" for R R''' in corres_inst) 
      (* apply (rule_tac P'="?R' (ntfn_bound_tcb ntfn_obj)" and P="?R (ntfn_bound_tcb ntfn_obj)" in corres_inst) *)
       apply (simp add: set_to_option_Option_set) apply (rule_tac v="ntfn_bound_tcb ntfna" and v'="ntfn_bound_tcb ntfna" in corres_option_split) apply simp apply (rule corres_trivial) apply simp apply (rule_tac P'="R' (the (ntfn_bound_tcb ntfna)) ntfna" for R' in corres_inst) apply simp apply (rule dcorres_do_unbind_notification[unfolded dc_def, simplified]) apply (wp get_simple_ko_wp)+ apply (clarsimp split: option.splits) apply (clarsimp simp: valid_state_def valid_pspace_def split: option.splits) apply (simp add: obj_at_def) apply (frule (3) ntfn_bound_tcb_at[where P="\<lambda>a. a = Some ntfn"], simp) apply (clarsimp simp: valid_idle_def pred_tcb_at_def not_idle_thread_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and valid_idle and valid_state) (PageTableUnmap_D.unbind_maybe_notification ntfn) (IpcCancel_A.unbind_maybe_notification ntfn) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and valid_idle and valid_state) (do bound_tcbs <- gets (get_bound_notification_threads ntfn);
t <- option_select bound_tcbs;
case t of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb
od) (do ntfna <- get_notification ntfn;
case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do bound_tcbs <- gets (get_bound_notification_threads ntfn);
t <- option_select bound_tcbs;
case t of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb
od) (do ntfna <- get_notification ntfn;
case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres dc (?R4 (set_option (ntfn_bound_tcb ntfna))) (?R'4 ntfna) (do t <- option_select (set_option (ntfn_bound_tcb ntfna));
case t of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb
od) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres dc (?R4 (set_option (ntfn_bound_tcb ntfna))) (?R'4 ntfna) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres dc (?R4 (set_option (ntfn_bound_tcb ntfna))) (case ntfn_bound_tcb ntfna of None \<Rightarrow> ?R'20 ntfna | Some x \<Rightarrow> ?R''18 ntfna) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres dc (case set_to_option (set_option (ntfn_bound_tcb ntfna)) of None \<Rightarrow> ?R30 (set_option (ntfn_bound_tcb ntfna)) | Some x \<Rightarrow> ?R'''28 (set_option (ntfn_bound_tcb ntfna))) (case ntfn_bound_tcb ntfna of None \<Rightarrow> ?R'20 ntfna | Some x \<Rightarrow> ?R''18 ntfna) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> ?R30 a | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres dc (case set_to_option (set_option (ntfn_bound_tcb ntfna)) of None \<Rightarrow> ?R30 (set_option (ntfn_bound_tcb ntfna)) | Some x \<Rightarrow> ?R'''28 (set_option (ntfn_bound_tcb ntfna))) (case ntfn_bound_tcb ntfna of None \<Rightarrow> ?R'20 ntfna | Some x \<Rightarrow> ?R''18 ntfna) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> ?R30 a | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna. bound_tcbs = set_option (ntfn_bound_tcb ntfna) \<Longrightarrow> dcorres (\<lambda>a b. True) (case ntfn_bound_tcb ntfna of None \<Rightarrow> ?R30 (set_option (ntfn_bound_tcb ntfna)) | Some x \<Rightarrow> ?R'''28 (set_option (ntfn_bound_tcb ntfna))) (case ntfn_bound_tcb ntfna of None \<Rightarrow> ?R'20 ntfna | Some x \<Rightarrow> ?R''18 ntfna) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some tcb \<Rightarrow> PageTableUnmap_D.do_unbind_notification tcb) (case ntfn_bound_tcb ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification ntfn ntfna t)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> ?R30 a | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>bound_tcbs ntfn. bound_tcbs = set_option (ntfn_bound_tcb ntfn) \<Longrightarrow> ntfn_bound_tcb ntfn = ntfn_bound_tcb ntfn
 2. \<And>bound_tcbs ntfn. bound_tcbs = set_option (ntfn_bound_tcb ntfn) \<Longrightarrow> dcorres (\<lambda>a b. True) (?R30 (set_option (ntfn_bound_tcb ntfn))) (?R'20 ntfn) (return ()) (return ())
 3. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = set_option (ntfn_bound_tcb ntfna); ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 (set_option (ntfn_bound_tcb ntfna))) (?R''18 ntfna) (PageTableUnmap_D.do_unbind_notification x) (IpcCancel_A.do_unbind_notification ntfn ntfna x)
 4. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> ?R30 a | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?Q s
 7. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>bound_tcbs ntfn. bound_tcbs = set_option (ntfn_bound_tcb ntfn) \<Longrightarrow> dcorres (\<lambda>a b. True) (?R30 (set_option (ntfn_bound_tcb ntfn))) (?R'20 ntfn) (return ()) (return ())
 2. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = set_option (ntfn_bound_tcb ntfna); ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 (set_option (ntfn_bound_tcb ntfna))) (?R''18 ntfna) (PageTableUnmap_D.do_unbind_notification x) (IpcCancel_A.do_unbind_notification ntfn ntfna x)
 3. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> ?R30 a | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> ?R'20 a | Some x \<Rightarrow> ?R''18 a\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>bound_tcbs ntfn. bound_tcbs = set_option (ntfn_bound_tcb ntfn) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 2. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = set_option (ntfn_bound_tcb ntfna); ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 (set_option (ntfn_bound_tcb ntfna))) (?R''18 ntfna) (PageTableUnmap_D.do_unbind_notification x) (IpcCancel_A.do_unbind_notification ntfn ntfna x)
 3. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R''18 a\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = set_option (ntfn_bound_tcb ntfna); ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 (set_option (ntfn_bound_tcb ntfna))) (?R''18 ntfna) (PageTableUnmap_D.do_unbind_notification x) (IpcCancel_A.do_unbind_notification ntfn ntfna x)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R''18 a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = set_option (ntfn_bound_tcb ntfna); ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 (set_option (ntfn_bound_tcb ntfna))) (?R'46 ntfna (the (ntfn_bound_tcb ntfna)) ntfna) (PageTableUnmap_D.do_unbind_notification x) (IpcCancel_A.do_unbind_notification ntfn ntfna x)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'46 a (the (ntfn_bound_tcb a)) a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs ntfna x. \<lbrakk>bound_tcbs = {x}; ntfn_bound_tcb ntfna = Some x\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R'''28 {x}) (?R'46 ntfna x ntfna) (PageTableUnmap_D.do_unbind_notification x) (do a <- set_notification ntfn (ntfn_set_bound_tcb ntfna None);
set_bound_notification x None
od)
 2. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'''28 a\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> ?R'46 a (the (ntfn_bound_tcb a)) a\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> gets (get_bound_notification_threads ntfn) \<lbrace>\<lambda>a. case set_to_option a of None \<Rightarrow> \<lambda>a. True | _ \<Rightarrow> \<lambda>a. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> get_notification ntfn \<lbrace>\<lambda>a. case ntfn_bound_tcb a of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> valid_etcbs and valid_state and not_idle_thread (the (ntfn_bound_tcb a))\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s
 4. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> (case set_to_option (get_bound_notification_threads ntfn s) of None \<Rightarrow> \<lambda>a. True | _ \<Rightarrow> \<lambda>a. True) s
 2. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and (\<lambda>s. \<forall>ntfna. ko_at (kernel_object.Notification ntfna) ntfn s \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> valid_etcbs and valid_state and not_idle_thread (the (ntfn_bound_tcb ntfna))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_etcbs and valid_idle and valid_state) s \<Longrightarrow> (valid_state and valid_etcbs and (\<lambda>s. \<forall>ntfna. ko_at (kernel_object.Notification ntfna) ntfn s \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> \<lambda>a. True | Some x \<Rightarrow> valid_etcbs and valid_state and not_idle_thread (the (ntfn_bound_tcb ntfna))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfna x2. \<lbrakk>valid_etcbs s; 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; valid_idle 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; ntfn_bound_tcb ntfna = Some x2; ko_at (kernel_object.Notification ntfna) ntfn s\<rbrakk> \<Longrightarrow> not_idle_thread x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfna x2. \<lbrakk>valid_etcbs s; 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; valid_idle 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; ntfn_bound_tcb ntfna = Some x2; kheap s ntfn = Some (kernel_object.Notification ntfna)\<rbrakk> \<Longrightarrow> not_idle_thread x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfna x2. \<lbrakk>valid_etcbs s; 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; valid_idle 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; ntfn_bound_tcb ntfna = Some x2; kheap s ntfn = Some (kernel_object.Notification ntfna); bound_tcb_at (\<lambda>a. a = Some ntfn) x2 s\<rbrakk> \<Longrightarrow> not_idle_thread x2 s proof (prove)
goal:
No subgoals!