theory InterruptAcc_R

lemma setIRQState_invs[wp]:
  "\<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace>
      setIRQState state irq
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def) apply (wp dmo_maskInterrupt) apply (clarsimp simp: invs'_def valid_state'_def cur_tcb'_def
                        Invariants_H.valid_queues_def valid_queues'_def
                        valid_idle'_def valid_irq_node'_def
                        valid_arch_state'_def valid_global_refs'_def
                        global_refs'_def valid_machine_state'_def
                        if_unsafe_then_cap'_def ex_cte_cap_to'_def
                        valid_irq_handlers'_def irq_issued'_def
                        cteCaps_of_def valid_irq_masks'_def
                        bitmapQ_defs valid_queues_no_bitmap_def) apply (rule conjI, clarsimp) apply (clarsimp simp: irqs_masked'_def ct_not_inQ_def) apply (rule conjI) apply fastforce apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace> setIRQState state irq \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace> do st <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state)) st));
doMachineOp (maskInterrupt (state = irqstate.IRQInactive) irq)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> (state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ) \<Longrightarrow> invs' (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := state = irqstate.IRQInactive))) (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := state)) (ksInterruptState s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; irqs_masked' s; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> (capability.IRQHandlerCap irq \<in> ran (map_option cteCap \<circ> ctes_of s) \<longrightarrow> state = irqstate.IRQSignal) \<and> irqs_masked' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) \<and> ct_not_inQ (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) \<and> ct_idle_or_in_cur_domain' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; irqs_masked' s; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> irqs_masked' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) \<and> ct_not_inQ (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) \<and> ct_idle_or_in_cur_domain' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> (maxIRQ < irq \<longrightarrow> state = irqstate.IRQInactive) \<and> ct_idle_or_in_cur_domain' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> maxIRQ < irq \<longrightarrow> state = irqstate.IRQInactive
 2. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> ct_idle_or_in_cur_domain' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<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) = []); \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []); \<forall>d i. Ex ((!!) (ksReadyQueuesL2Bitmap s (d, invertL1Index i))) \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i; \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> (\<exists>crefa. cte_wp_at' (\<lambda>c. cref \<in> cte_refs' (cteCap c) (irq_node' s)) crefa s); obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); idle_thread_ptr \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); is_aligned (irq_node' s) (size 0 + cteSizeBits); \<forall>irq. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s; \<forall>cap\<in>ran (map_option cteCap \<circ> ctes_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; \<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq; \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0; \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)); ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) 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); tcb_at' (ksCurThread s) s; state \<noteq> irqstate.IRQSignal \<longrightarrow> capability.IRQHandlerCap irq \<notin> ran (map_option cteCap \<circ> ctes_of s); state \<noteq> irqstate.IRQInactive \<longrightarrow> irq \<le> maxIRQ\<rbrakk> \<Longrightarrow> ct_idle_or_in_cur_domain' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_ a. if a = irq then state else intStateIRQTable (ksInterruptState s) a) (ksInterruptState s)\<rparr>) proof (prove)
goal:
No subgoals!