theory Invariants_H

lemma invs'_gsCNodes_update[simp]:
  "invs' (gsCNodes_update f s') = invs' s'" apply (clarsimp simp: invs'_def valid_state'_def valid_queues_def valid_queues_no_bitmap_def
             bitmapQ_defs
             valid_queues'_def valid_irq_node'_def valid_irq_handlers'_def
             irq_issued'_def irqs_masked'_def valid_machine_state'_def
             cur_tcb'_def) apply (cases "ksSchedulerAction s'") apply (simp_all add: ct_in_state'_def tcb_in_cur_domain'_def  ct_idle_or_in_cur_domain'_def ct_not_inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' (gsCNodes_update f s') = invs' s' proof (prove)
goal (1 subgoal):
 1. (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') (gsCNodes_update f s') \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<and> ct_not_inQ (gsCNodes_update f s') \<and> ct_idle_or_in_cur_domain' (gsCNodes_update f 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> tcb_at' (ksCurThread s') s') = (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') s' \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<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> tcb_at' (ksCurThread s') s') proof (prove)
goal (3 subgoals):
 1. ksSchedulerAction s' = ResumeCurrentThread \<Longrightarrow> (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') (gsCNodes_update f s') \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<and> ct_not_inQ (gsCNodes_update f s') \<and> ct_idle_or_in_cur_domain' (gsCNodes_update f 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> tcb_at' (ksCurThread s') s') = (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') s' \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<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> tcb_at' (ksCurThread s') s')
 2. ksSchedulerAction s' = ChooseNewThread \<Longrightarrow> (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') (gsCNodes_update f s') \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<and> ct_not_inQ (gsCNodes_update f s') \<and> ct_idle_or_in_cur_domain' (gsCNodes_update f 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> tcb_at' (ksCurThread s') s') = (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') s' \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<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> tcb_at' (ksCurThread s') s')
 3. \<And>x3. ksSchedulerAction s' = SwitchToThread x3 \<Longrightarrow> (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') (gsCNodes_update f s') \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<and> ct_not_inQ (gsCNodes_update f s') \<and> ct_idle_or_in_cur_domain' (gsCNodes_update f 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> tcb_at' (ksCurThread s') s') = (valid_pspace' s' \<and> sch_act_wf (ksSchedulerAction s') s' \<and> (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s' (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s') \<and> distinct (ksReadyQueues s' (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s' (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s' (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s' d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s' (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s' (d, p) \<noteq> [])) \<and> (\<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s' (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s' d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s' d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s' (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) \<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> is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s') \<and> (\<forall>cap\<in>ran (cteCaps_of s'). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s') irq = irqstate.IRQSignal) \<and> valid_irq_states' s' \<and> (\<forall>p. pointerInUserData p s' \<or> pointerInDeviceData p s' \<or> underlying_memory (ksMachineState s') p = 0) \<and> (\<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) \<and> (\<forall>d p t. obj_at' (inQ d p) t s' \<longrightarrow> t \<in> set (ksReadyQueues s' (d, p))) \<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> tcb_at' (ksCurThread s') s') proof (prove)
goal:
No subgoals!