theory Interrupt_C

lemma isIRQActive_ccorres:
  "ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
        (\<lambda>s. irq \<le> scast Kernel_C.maxIRQ) (UNIV \<inter> {s. irq_' s = ucast irq}) []
        (isIRQActive irq) (Call isIRQActive_'proc)" apply (cinit lift: irq_') apply (simp add: getIRQState_def getInterruptState_def) apply (rule_tac P="irq \<le> ucast Kernel_C.maxIRQ \<and> unat irq < (160::nat)" in ccorres_gen_asm) apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def
                         word_less_nat_alt) apply (clarsimp simp: order_le_less_trans unat_less_helper Kernel_C.IRQInactive_def
                         Kernel_C.maxIRQ_def word_0_sle_from_less[OF order_less_le_trans, OF ucast_less]) apply (clarsimp simp: rf_sr_def cstate_relation_def Kernel_C.maxIRQ_def
                         Let_def cinterrupt_relation_def) apply (drule spec, drule(1) mp) apply (case_tac "intStateIRQTable (ksInterruptState \<sigma>) irq") apply (simp add: irq_state_defs Kernel_C.maxIRQ_def word_le_nat_alt)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (\<lambda>s. irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (isIRQActive irq) (Call isIRQActive_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irqa = UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> ccorres ((\<lambda>rv rv'. rv' = from_bool rv) \<circ> (\<lambda>x. x \<noteq> irqstate.IRQInactive)) ret__unsigned_long_' (?Q37 irqa) (?Q'37 irqa) [SKIP] (getIRQState irq) (Guard ArrayBounds \<lbrace>irqa < 0xA0\<rbrace> (return_C ret__unsigned_long_'_update (\<lambda>s. if intStateIRQTable_' (globals s).[unat irqa] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q37 irqa s \<and> s' \<in> ?Q'37 irqa proof (prove)
goal (2 subgoals):
 1. ccorres ((\<lambda>rv rv'. rv' = from_bool rv) \<circ> (\<lambda>x. x \<noteq> irqstate.IRQInactive) \<circ> (swp id irq \<circ> intStateIRQTable)) ret__unsigned_long_' (?Q37 (UCAST(10 \<rightarrow> 32) irq)) (?Q'37 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (gets ksInterruptState) (Guard ArrayBounds (if UCAST(10 \<rightarrow> 32) irq < 0xA0 then UNIV else {}) (return_C ret__unsigned_long_'_update (\<lambda>s. if intStateIRQTable_' (globals s).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q37 irqa s \<and> s' \<in> ?Q'37 irqa proof (prove)
goal (2 subgoals):
 1. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160 \<Longrightarrow> ccorres ((\<lambda>rv rv'. rv' = from_bool rv) \<circ> (\<lambda>x. x \<noteq> irqstate.IRQInactive) \<circ> (swp id irq \<circ> intStateIRQTable)) ret__unsigned_long_' (?G56 (UCAST(10 \<rightarrow> 32) irq)) (?Q'37 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (gets ksInterruptState) (Guard ArrayBounds (if UCAST(10 \<rightarrow> 32) irq < 0xA0 then UNIV else {}) (return_C ret__unsigned_long_'_update (\<lambda>s. if intStateIRQTable_' (globals s).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?G56 irqa and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> ?Q'37 irqa proof (prove)
goal (2 subgoals):
 1. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160 \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} Guard ArrayBounds (if UCAST(10 \<rightarrow> 32) irq < 0xA0 then UNIV else {}) (return_C ret__unsigned_long_'_update (\<lambda>s. if intStateIRQTable_' (globals s).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) {},{s. \<exists>(rv, \<sigma>')\<in>fst (gets ksInterruptState \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((\<lambda>rv rv'. rv' = from_bool rv) \<circ> (\<lambda>x. x \<noteq> irqstate.IRQInactive) \<circ> (swp id irq \<circ> intStateIRQTable)) rv (ret__unsigned_long_' s)}
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160 \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> (if UCAST(10 \<rightarrow> 32) irq < 0xA0 then UNIV else {}) \<inter> {s. \<exists>(rv, \<sigma>')\<in>fst (gets ksInterruptState \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := if intStateIRQTable_' (globals s).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (if intStateIRQTable_' (globals s).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (swp id irq (intStateIRQTable rv) \<noteq> irqstate.IRQInactive)}
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>(\<sigma>, x) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; unat irq < 160\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>(\<sigma>, x) \<in> rf_sr; irq \<le> 0x9F\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; \<forall>irq\<le>0x9F. irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]; intStateIRQTable (ksInterruptState \<sigma>) irq = irqstate.IRQInactive\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 2. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]; intStateIRQTable (ksInterruptState \<sigma>) irq = irqstate.IRQSignal\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 3. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]; intStateIRQTable (ksInterruptState \<sigma>) irq = irqstate.IRQTimer\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 4. \<And>\<sigma> x. \<lbrakk>irq \<le> 0x9F; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); symbol_table ''intStateIRQNode'' = irq_node' \<sigma>; cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' \<sigma>); {irq_node' \<sigma>..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; irqstate_to_C (intStateIRQTable (ksInterruptState \<sigma>) irq) = intStateIRQTable_' (globals x).[unat irq]; intStateIRQTable (ksInterruptState \<sigma>) irq = irqstate.IRQReserved\<rbrakk> \<Longrightarrow> (if intStateIRQTable_' (globals x).[unat irq] \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (intStateIRQTable (ksInterruptState \<sigma>) irq \<noteq> irqstate.IRQInactive)
 5. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; irq \<le> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>_. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> unat irq < 160)) s \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!