theory Finalise_R

lemma unbindNotification_invs[wp]:
  "\<lbrace>invs'\<rbrace> unbindNotification tcb \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: unbindNotification_def invs'_def valid_state'_def) apply (rule hoare_seq_ext[OF _ gbn_sp']) apply (case_tac ntfnPtr, clarsimp, wp, clarsimp) apply clarsimp apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift
            irqs_masked_lift setBoundNotification_ct_not_inQ
            untyped_ranges_zero_lift | clarsimp simp: cteCaps_of_def o_def)+ apply (rule conjI) apply (clarsimp elim!: obj_atE'
                    simp: projectKOs
                   dest!: pred_tcb_at') apply (clarsimp simp: pred_tcb_at' conj_comms) apply (frule bound_tcb_ex_cap'', clarsimp+) apply (frule(1) sym_refs_bound_tcb_atD') apply (frule(1) sym_refs_obj_atD') apply (clarsimp simp: refs_of_rev') apply normalise_obj_at' apply (subst delta_sym_refs, assumption) apply (auto split: if_split_asm)[1] apply (auto simp: tcb_st_not_Bound ntfn_q_refs_of'_mult split: if_split_asm)[1] apply (frule obj_at_valid_objs', clarsimp+) apply (simp add: valid_ntfn'_def valid_obj'_def projectKOs
            split: ntfn.splits) apply (erule if_live_then_nonz_capE') apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> unbindNotification tcb \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> do ntfnPtr <- getBoundNotification tcb;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr. \<lbrace>bound_tcb_at' (\<lambda>st. st = ntfnPtr) tcb and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr a. ntfnPtr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at' (\<lambda>st. st = ntfnPtr) tcb and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrace>bound_tcb_at' (\<lambda>st. st = Some a) tcb and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> do ntfn <- getNotification a;
y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn. \<lbrace>bound_tcb_at' (\<lambda>st. st = Some a) tcb and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb') and ko_at' ntfn a\<rbrace> do y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn. \<lbrace>?Q64 a ntfn\<rbrace> do y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace>
 2. \<And>a ntfn s. (bound_tcb_at' (\<lambda>st. st = Some a) tcb and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb') and ko_at' ntfn a) s \<Longrightarrow> ?Q64 a ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s\<rbrakk> \<Longrightarrow> (tcb = a \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' a s \<and> sym_refs (\<lambda>b. if b = a then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s b) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) \<and> (tcb \<noteq> a \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' tcb s \<and> sym_refs (\<lambda>b. if b = tcb then {r \<in> state_refs_of' s tcb. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s\<rbrakk> \<Longrightarrow> tcb = a \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' a s \<and> sym_refs (\<lambda>b. if b = a then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s b) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 2. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s\<rbrakk> \<Longrightarrow> tcb \<noteq> a \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' tcb s \<and> sym_refs (\<lambda>b. if b = tcb then {r \<in> state_refs_of' s tcb. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s\<rbrakk> \<Longrightarrow> tcb \<noteq> a \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' tcb s \<and> sym_refs (\<lambda>b. if b = tcb then {r \<in> state_refs_of' s tcb. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s; tcb \<noteq> a\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcb} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s; tcb \<noteq> a; ex_nonz_cap_to' tcb s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcb} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; \<exists>ts ntfnptr. ntfnptr = Some a \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) tcb s \<and> state_refs_of' s tcb = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcb} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; \<exists>ts ntfnptr. ntfnptr = Some a \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) tcb s \<and> state_refs_of' s tcb = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s); \<exists>obj. obj = ntfn \<and> state_refs_of' s a = refs_of' (injectKOS obj) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS obj). ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcb} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts. \<lbrakk>bound_tcb_at' (\<lambda>st. st = Some a) tcb s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn a s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; obj_at' (tcb_ntfn_is_bound' (Some a)) tcb s; state_refs_of' s a = ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ko_wp_at' (\<lambda>ko. \<exists>ntfn. ko = KONotification ntfn \<and> ntfnBoundTCB ntfn = Some tcb) a s; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> sym_refs (\<lambda>b. if b = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if b = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s b) proof (prove)
goal (3 subgoals):
 1. \<And>a ntfn s ts ko x y tp. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; (y, tp) \<in> (if x = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if x = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s x); (y, tp) \<notin> state_refs_of' s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if y = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y)
 2. \<And>a ntfn s ts ko x y tp. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if x = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if y = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y)
 3. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>a ntfn s ts ko x y tp. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if x = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcb then {r. snd r \<noteq> TCBBound \<and> (r = (a, TCBBound) \<or> r \<in> tcb_st_refs_of' ts)} else if y = a then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y)
 2. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = insert (tcb, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)); state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; \<forall>x\<in>ntfn_q_refs_of' (ntfnObj ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (a, symreftype tp) \<in> refs_of' ko) x s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; (\<forall>ko. projectKO_opt ko = Some ntfn \<longrightarrow> KONotification ntfn = ko) \<longrightarrow> valid_obj' (KONotification ntfn) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' a s) proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = {(tcb, NTFNBound), (tcb, NTFNSignal)}; state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; ko_wp_at' (\<lambda>ko. (a, TCBSignal) \<in> refs_of' ko) tcb s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn [tcb]; tcb_at' tcb s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn s ts ko. \<lbrakk>tcbBoundNotification ko = Some a; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb \<noteq> a; ex_nonz_cap_to' tcb s; state_refs_of' s a = {(tcb, NTFNBound), (tcb, NTFNSignal)}; state_refs_of' s tcb = insert (a, TCBBound) (tcb_st_refs_of' ts); ntfnBoundTCB ntfn = Some tcb; \<forall>x\<in>tcb_st_refs_of' ts. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (tcb, symreftype tp) \<in> refs_of' ko) x s; ko_at' ntfn a s; ko_wp_at' (\<lambda>ko. (a, TCBSignal) \<in> refs_of' ko) tcb s; ko_at' ko tcb s; tcb_ntfn_is_bound' (Some a) ko; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn [tcb]; tcb_at' tcb s\<rbrakk> \<Longrightarrow> ko_wp_at' live' a s proof (prove)
goal:
No subgoals!