theory IpcCancel_AI

lemma unbind_notification_invs:
  shows "\<lbrace>invs\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: unbind_notification_def invs_def valid_state_def valid_pspace_def) apply (rule hoare_seq_ext [OF _ gbn_sp]) apply (case_tac ntfnptr, clarsimp, wp, simp) apply clarsimp apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (wp valid_irq_node_typ set_simple_ko_valid_objs valid_ioports_lift
         | 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: live_def valid_ntfn_set_bound_None is_ntfn valid_obj_def
    )?) apply (clarsimp simp: if_split) apply (rule delta_sym_refs, assumption) apply (fastforce simp: obj_at_def is_tcb
                   dest!: pred_tcb_at_tcb_at ko_at_state_refs_ofD
                   split: if_split_asm) apply (clarsimp split: if_split_asm) apply (frule pred_tcb_at_tcb_at) apply (frule_tac p=t 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>invs\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. invs\<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_ioports 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 and cur_tcb\<rbrace> do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od
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_ioports 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 and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr. \<lbrace>bound_tcb_at ((=) ntfnptr) t 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_ioports 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 and cur_tcb)\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' 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_ioports 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 and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr a. ntfnptr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t 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_ioports 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 and cur_tcb)\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' 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_ioports 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 and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrace>bound_tcb_at ((=) (Some a)) t 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_ioports 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 and cur_tcb)\<rbrace> do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t 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_ioports 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 and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn. \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) t 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_ioports 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 and cur_tcb))\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t 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_ioports 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 and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s \<and> (live (Notification (ntfn_set_bound_tcb ntfn None)) \<longrightarrow> ex_nonz_cap_to a s) \<and> sym_refs (\<lambda>b. if b = t then {r \<in> if t = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s t. 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. Notification y = ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = t then {r \<in> if t = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s t. 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>a ntfn s. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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>a ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> (if x = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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 = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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>a ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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 = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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>a ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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 = t then {r. (t = a \<longrightarrow> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (t \<noteq> a \<longrightarrow> r \<in> state_refs_of s t) \<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>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s t; t = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = t \<longrightarrow> (t, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = t \<longrightarrow> t = a \<and> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> t \<noteq> a \<and> (t, symreftype tp) \<notin> state_refs_of s t \<or> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s a; a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s t; t = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; tcb_at t s\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = t \<longrightarrow> (t, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = t \<longrightarrow> t = a \<and> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> t \<noteq> a \<and> (t, symreftype tp) \<notin> state_refs_of s t \<or> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s a; a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn s y tp ko. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s t; t = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; tcb_at t s; ko_at ko t s; is_tcb ko\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = t \<longrightarrow> (t, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = t \<longrightarrow> t = a \<and> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> t \<noteq> a \<and> (t, symreftype tp) \<notin> state_refs_of s t \<or> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s a; a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn s y tp ko. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> refs_of ko; t = a \<and> (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> tp = TCBBound; tcb_at t s; ko_at ko t s; is_tcb ko\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = t \<longrightarrow> (t, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (a \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn))) \<and> (y \<noteq> a \<longrightarrow> (y = t \<longrightarrow> t = a \<and> (t, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn) \<or> t \<noteq> a \<and> (t, symreftype tp) \<notin> state_refs_of s t \<or> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s a; a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> state_refs_of s a; a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) t 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_ioports 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; cur_tcb s; (y, tp) \<in> refs_of (Notification ntfn); a \<noteq> t; (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 = t \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s t \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> t \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal:
No subgoals!