theory Tcb_R

lemma bindNotification_invs':
  "\<lbrace>bound_tcb_at' ((=) None) tcbptr
       and ex_nonz_cap_to' ntfnptr
       and ex_nonz_cap_to' tcbptr
       and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> WaitingNtfn q)) ntfnptr
       and invs'\<rbrace>
    bindNotification tcbptr ntfnptr
   \<lbrace>\<lambda>_. invs'\<rbrace>" including no_pre apply (simp add: bindNotification_def invs'_def valid_state'_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp set_ntfn_valid_pspace' sbn_sch_act' sbn_valid_queues valid_irq_node_lift
             setBoundNotification_ct_not_inQ valid_bound_ntfn_lift
             untyped_ranges_zero_lift
          | clarsimp dest!: global'_no_ex_cap simp: cteCaps_of_def)+ apply (clarsimp simp: valid_pspace'_def) apply (cases "tcbptr = ntfnptr") apply (clarsimp dest!: pred_tcb_at' simp: obj_at'_def projectKOs) apply (clarsimp simp: pred_tcb_at' conj_comms o_def) apply (subst delta_sym_refs, assumption) apply (fastforce simp: ntfn_q_refs_of'_def obj_at'_def projectKOs
                    dest!: symreftype_inverse'
                    split: ntfn.splits if_split_asm) apply (clarsimp split: if_split_asm) apply (fastforce simp: tcb_st_refs_of'_def
                    dest!: bound_tcb_at_state_refs_ofD'
                    split: if_split_asm thread_state.splits) apply (fastforce simp: obj_at'_def projectKOs state_refs_of'_def
                   dest!: symreftype_inverse') apply (clarsimp simp: valid_pspace'_def) apply (frule_tac P="\<lambda>k. k=ntfn" in obj_at_valid_objs', simp) apply (clarsimp simp: valid_obj'_def projectKOs valid_ntfn'_def obj_at'_def
                    dest!: pred_tcb_at'
                    split: ntfn.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' ((=) None) tcbptr and ex_nonz_cap_to' ntfnptr and ex_nonz_cap_to' tcbptr and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and invs'\<rbrace> bindNotification tcbptr ntfnptr \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' ((=) None) tcbptr and ex_nonz_cap_to' ntfnptr and ex_nonz_cap_to' tcbptr and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and invs'\<rbrace> bindNotification tcbptr ntfnptr \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at' ((=) None) tcbptr and ex_nonz_cap_to' ntfnptr and ex_nonz_cap_to' tcbptr and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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 ntfnptr;
y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn);
setBoundNotification (Some ntfnptr) tcbptr
od \<lbrace>\<lambda>_. (\<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>ntfn. \<lbrace>bound_tcb_at' ((=) None) tcbptr and ex_nonz_cap_to' ntfnptr and ex_nonz_cap_to' tcbptr and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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 ntfnptr\<rbrace> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn);
setBoundNotification (Some ntfnptr) tcbptr
od \<lbrace>\<lambda>_. (\<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>ntfn. \<lbrace>?Q4 ntfn\<rbrace> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn);
setBoundNotification (Some ntfnptr) tcbptr
od \<lbrace>\<lambda>_. (\<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>ntfn s. (bound_tcb_at' ((=) None) tcbptr and ex_nonz_cap_to' ntfnptr and ex_nonz_cap_to' tcbptr and obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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 ntfnptr) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> tcb_at' ntfnptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> ntfnptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcb_at' tcbptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of' s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcbptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> tcb_at' ntfnptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> ntfnptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcb_at' tcbptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of' s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcbptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr = ntfnptr\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> tcb_at' ntfnptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> ntfnptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcb_at' tcbptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of' s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcbptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s))
 2. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> tcb_at' ntfnptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> ntfnptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcb_at' tcbptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of' s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcbptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> tcb_at' ntfnptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some ntfnptr) ntfn) s \<and> ntfnptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcb_at' tcbptr s \<and> ntfn_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of' s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> tcbptr \<noteq> ksIdleThread s \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s a) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> (if x = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if x = ntfnptr then insert (tcbptr, NTFNBound) (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 = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s y)
 2. \<And>ntfn s x y tp. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if x = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s y)
 3. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if x = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcbptr then insert (ntfnptr, TCBBound) {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of' s tcbptr} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of' (ntfnObj ntfn)) else state_refs_of' s y)
 2. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> True proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s y. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, TCBBound) \<in> state_refs_of' s tcbptr; y \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> (y = tcbptr \<longrightarrow> (tcbptr, NTFNBound) \<notin> state_refs_of' s tcbptr) \<and> (y \<noteq> tcbptr \<longrightarrow> (tcbptr, NTFNBound) \<notin> state_refs_of' s y)
 2. \<And>ntfn s y tp. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of' s ntfnptr; y = tcbptr \<longrightarrow> tp \<noteq> NTFNBound; (y, tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = tcbptr \<longrightarrow> symreftype tp \<noteq> TCBBound \<and> (symreftype tp = TCBBound \<or> (ntfnptr, symreftype tp) \<notin> state_refs_of' s tcbptr)) \<and> (y \<noteq> tcbptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of' s y))
 3. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of' s ntfnptr; y = tcbptr \<longrightarrow> tp \<noteq> NTFNBound; (y, tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = tcbptr \<longrightarrow> symreftype tp \<noteq> TCBBound \<and> (symreftype tp = TCBBound \<or> (ntfnptr, symreftype tp) \<notin> state_refs_of' s tcbptr)) \<and> (y \<noteq> tcbptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of' s y))
 2. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>bound_tcb_at' ((=) None) tcbptr s; ex_nonz_cap_to' ntfnptr s; ex_nonz_cap_to' tcbptr s; obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None \<and> (\<forall>q. ntfnObj ntfn \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr 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_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 ntfnptr s; \<not> ex_nonz_cap_to' (ksIdleThread s) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; tcbptr \<noteq> ntfnptr; \<exists>k. k = ntfn \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ksIdleThread s \<and> ntfn_at' ntfnptr s \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. Some tcbptr) ntfn) s proof (prove)
goal:
No subgoals!