theory InterruptAcc_R

lemma invs'_irq_state_independent [simp, intro!]:
  "invs' (s\<lparr>ksMachineState := ksMachineState s
                 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
   invs' s" apply (clarsimp simp: irq_state_independent_H_def invs'_def valid_state'_def
          valid_pspace'_def sch_act_wf_def
          valid_queues_def sym_refs_def state_refs_of'_def
          if_live_then_nonz_cap'_def if_unsafe_then_cap'_def
          valid_idle'_def valid_global_refs'_def
          valid_arch_state'_def valid_irq_node'_def
          valid_irq_handlers'_def valid_irq_states'_def
          irqs_masked'_def bitmapQ_defs valid_queues_no_bitmap_def
          valid_queues'_def valid_pde_mappings'_def
          pspace_domain_valid_def cur_tcb'_def
          valid_machine_state'_def tcb_in_cur_domain'_def
          ct_not_inQ_def ct_idle_or_in_cur_domain'_def
          cong: if_cong option.case_cong) apply (rule iffI[rotated]) apply (clarsimp) apply (case_tac "ksSchedulerAction s", simp_all) apply clarsimp apply (case_tac "ksSchedulerAction s", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = invs' s proof (prove)
goal (1 subgoal):
 1. (valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) \<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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 (2 subgoals):
 1. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) \<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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) \<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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 (2 subgoals):
 1. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (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; \<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {}); \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); global_refs' s \<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 (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; \<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; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = idle_thread_ptr \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s; \<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; 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' s; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>)
 2. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) \<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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 \<Longrightarrow> valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 (1 subgoal):
 1. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) \<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> (\<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {})) \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> (\<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s) \<and> obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s \<and> valid_refs' kernel_data_refs (ctes_of s) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s) \<and> valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState 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> irq_issued' irq s) \<and> (\<forall>irq. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive \<longrightarrow> irq_masks (ksMachineState s) irq) \<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> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> (\<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}) \<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 \<Longrightarrow> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) s \<and> obj_at' idle_tcb' idle_thread_ptr s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = idle_thread_ptr \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>); \<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; \<forall>x. \<forall>xa\<in>case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s then refs_of' ko else {}. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> (case ksPSpace s y of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned y (objBitsKO ko) \<and> ps_clear y (objBitsKO ko) s then refs_of' ko else {}); \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_refs' kernel_data_refs (ctes_of s); global_refs' s \<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 (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; \<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; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = idle_thread_ptr \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s; \<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; 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' s; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> Structures_H.scheduler_action.rec_scheduler_action (ct_in_state' activatable') (\<lambda>_. True) (\<lambda>t s. st_tcb_at' runnable' t s \<and> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!