From 5c6cd0e921484d14e2b0f5e126f3a51c419f24f3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 26 Sep 2024 10:06:40 +0200 Subject: [PATCH] crefine arm+arm-hyp: deal with smaller irq_len Remove remaining use of direct numeral related to irq_len. The lemma happened to work for irq_len >= 8, but not for smaller irq_len. Signed-off-by: Gerwin Klein --- proof/crefine/ARM/Ctac_lemmas_C.thy | 2 +- proof/crefine/ARM/Interrupt_C.thy | 4 +++- proof/crefine/ARM/Refine_C.thy | 5 +++-- proof/crefine/ARM_HYP/Ctac_lemmas_C.thy | 2 +- proof/crefine/ARM_HYP/Interrupt_C.thy | 4 +++- proof/crefine/ARM_HYP/Refine_C.thy | 5 +++-- 6 files changed, 14 insertions(+), 8 deletions(-) diff --git a/proof/crefine/ARM/Ctac_lemmas_C.thy b/proof/crefine/ARM/Ctac_lemmas_C.thy index 2b42ab3a0c..c6e7f407ed 100644 --- a/proof/crefine/ARM/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM/Ctac_lemmas_C.thy @@ -183,7 +183,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 256 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2^LENGTH(irq_len) \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) diff --git a/proof/crefine/ARM/Interrupt_C.thy b/proof/crefine/ARM/Interrupt_C.thy index 9432a06011..58bc21d17d 100644 --- a/proof/crefine/ARM/Interrupt_C.thy +++ b/proof/crefine/ARM/Interrupt_C.thy @@ -299,7 +299,9 @@ lemma invokeIRQControl_expanded_ccorres: apply (rule conjI, fastforce)+ apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val ucast_and_mask) - apply word_eqI + (* if irq_len < 8, there may be an additional term in the goal *) + apply (rule conjI, word_eqI_solve)? + apply (word_eqI_solve dest: bit_imp_le_length) done lemma invokeIRQControl_ccorres: diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index f072174c0c..03ddfd76b4 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -36,13 +36,14 @@ lemma schedule_sch_act_wf: apply (rule schedule_invs') done -(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs +(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs by type alone. *) lemma irq_type_never_invalid_left: "ucast irq \ irqInvalid" for irq::irq unfolding irqInvalid_def using ucast_less[of irq, where 'a=machine_word_len] - by (clarsimp simp: mask_def) + apply (clarsimp simp: mask_def) + done lemmas irq_type_never_invalid = irq_type_never_invalid_left irq_type_never_invalid_left[symmetric] diff --git a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy index e099909f4e..f79b929cc6 100644 --- a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy @@ -186,7 +186,7 @@ lemmas ccorres_move_c_guard_ap = ccorres_move_c_guards [OF move_c_guard_ap] lemma array_assertion_abs_irq: "\s s'. (s, s') \ rf_sr \ True - \ (n s' \ 256 \ (x s' \ 0 \ n s' \ 0)) + \ (n s' \ 2^LENGTH(irq_len) \ (x s' \ 0 \ n s' \ 0)) \ (x s' = 0 \ array_assertion intStateIRQNode_Ptr (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) diff --git a/proof/crefine/ARM_HYP/Interrupt_C.thy b/proof/crefine/ARM_HYP/Interrupt_C.thy index 88046147c6..8c8d9e1ac2 100644 --- a/proof/crefine/ARM_HYP/Interrupt_C.thy +++ b/proof/crefine/ARM_HYP/Interrupt_C.thy @@ -309,7 +309,9 @@ lemma invokeIRQControl_expanded_ccorres: apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift cap_to_H_def c_valid_cap_def cl_valid_cap_def irq_len_val word_bw_assocs mask_twice) - apply word_eqI + (* if irq_len < 8, there may be an additional term in the goal *) + apply (rule conjI, word_eqI_solve)? + apply (word_eqI_solve dest: bit_imp_le_length) done lemma invokeIRQControl_ccorres: diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 1c73871530..67354b5bbc 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -30,13 +30,14 @@ lemma schedule_sch_act_wf: apply (rule schedule_invs') done -(* On GICv2 and GICv3, irqInvalid is picked such it is outside the range of possible IRQs +(* On Arm, irqInvalid is picked such it is outside the range of possible IRQs by type alone. *) lemma irq_type_never_invalid_left: "ucast irq \ irqInvalid" for irq::irq unfolding irqInvalid_def using ucast_less[of irq, where 'a=machine_word_len] - by (clarsimp simp: mask_def) + apply (clarsimp simp: mask_def) + done lemmas irq_type_never_invalid = irq_type_never_invalid_left irq_type_never_invalid_left[symmetric]