theory KHeap_DR

lemma unbind_maybe_notification_valid_state[wp]:
  "\<lbrace>valid_state\<rbrace> IpcCancel_A.unbind_maybe_notification a \<lbrace>\<lambda>rv. valid_state\<rbrace>" supply if_cong[cong] apply (simp add: unbind_maybe_notification_def valid_state_def valid_pspace_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac "ntfn_bound_tcb ntfn", clarsimp, wp, simp+) apply (wp valid_irq_node_typ set_simple_ko_valid_objs
       | clarsimp split del: if_split)+ apply (intro conjI impI;
    (match conclusion in "sym_refs r" for r \<Rightarrow> \<open>-\<close>
      | auto elim!: obj_at_weakenE obj_at_valid_objsE if_live_then_nonz_capD2
                       simp: valid_ntfn_set_bound_None is_ntfn valid_obj_def
                             live_def hyp_live_def a_type_def)) apply (clarsimp simp: if_split) apply (rule delta_sym_refs, assumption) apply (fastforce simp: obj_at_def
                   dest!: pred_tcb_at_tcb_at ko_at_state_refs_ofD
                   split: if_split_asm) apply (clarsimp split: if_split_asm) apply (clarsimp simp: obj_at_def) apply (frule_tac P="(=) (Some a)" in ntfn_bound_tcb_at, simp+) apply (frule pred_tcb_at_tcb_at) apply (frule_tac p=aa in obj_at_ko_at, clarsimp) apply (subst (asm) ko_at_state_refs_ofD, assumption) apply (fastforce simp: obj_at_def is_tcb ntfn_q_refs_no_NTFNBound tcb_at_no_ntfn_bound refs_of_rev
                          tcb_ntfn_is_bound_def
                   dest!: pred_tcb_at_tcb_at bound_tcb_at_state_refs_ofD) apply (subst (asm) ko_at_state_refs_ofD, assumption) apply (fastforce simp: ntfn_bound_refs_def obj_at_def ntfn_q_refs_no_TCBBound
                  elim!: pred_tcb_weakenE
                  dest!: bound_tcb_bound_notification_at refs_in_ntfn_bound_refs symreftype_inverse'
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_state\<rbrace> IpcCancel_A.unbind_maybe_notification a \<lbrace>\<lambda>rv. valid_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_state\<rbrace> IpcCancel_A.unbind_maybe_notification a \<lbrace>\<lambda>rv. valid_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification a ntfn t
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (kernel_object.Notification ntfn) a and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region)\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> IpcCancel_A.do_unbind_notification a ntfn t \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa. ntfn_bound_tcb ntfn = Some aa \<Longrightarrow> \<lbrace>ko_at (kernel_object.Notification ntfn) a and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region)\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification aa None
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s \<and> (live (kernel_object.Notification (ntfn_set_bound_tcb ntfn None)) \<longrightarrow> ex_nonz_cap_to a s) \<and> sym_refs (\<lambda>b. if b = aa then {r \<in> if aa = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s aa. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) \<and> obj_at (\<lambda>ko. \<exists>y. kernel_object.Notification y = ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = aa then {r \<in> if aa = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s aa. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s x y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> (if x = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if x = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x); (y, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if y = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y)
 2. \<And>ntfn aa s x y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if x = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if y = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s x y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if x = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = aa then {r. (aa = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (aa \<noteq> a \<longrightarrow> r \<in> state_refs_of s aa) \<and> snd r \<noteq> TCBBound} else if y = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s aa; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; kheap s a = Some (kernel_object.Notification ntfn); 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; (y, tp) \<in> state_refs_of s aa; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; kheap s a = Some (kernel_object.Notification ntfn); 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; (y, tp) \<in> state_refs_of s aa; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; bound_tcb_at ((=) (Some a)) aa s\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; kheap s a = Some (kernel_object.Notification ntfn); 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; (y, tp) \<in> state_refs_of s aa; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; bound_tcb_at ((=) (Some a)) aa s; tcb_at aa s\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp ko. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; kheap s a = Some (kernel_object.Notification ntfn); 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; (y, tp) \<in> state_refs_of s aa; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; bound_tcb_at ((=) (Some a)) aa s; tcb_at aa s; ko_at ko aa s; is_tcb ko\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn aa s y tp ko. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; kheap s a = Some (kernel_object.Notification ntfn); 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; (y, tp) \<in> refs_of ko; aa = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; bound_tcb_at ((=) (Some a)) aa s; tcb_at aa s; ko_at ko aa s; is_tcb ko\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = aa \<longrightarrow> (aa, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> aa = a \<and> (aa, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> aa \<noteq> a \<and> (aa, symreftype tp) \<notin> state_refs_of s aa \<or> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (aa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> state_refs_of s a; a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn aa s y tp. \<lbrakk>ntfn_bound_tcb ntfn = Some aa; ko_at (kernel_object.Notification ntfn) a 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; (y, tp) \<in> refs_of (kernel_object.Notification ntfn); a \<noteq> aa; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = aa \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s aa \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> aa \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal:
No subgoals!