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 <[email protected]>

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:
   "\<forall>s s'. (s, s') \<in> rf_sr \<and> True
-        \<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
+        \<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
     \<longrightarrow> (x s' = 0 \<or> 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)

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:

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 \<noteq> 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]
 

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:
   "\<forall>s s'. (s, s') \<in> rf_sr \<and> True
-        \<and> (n s' \<le> 256 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
+        \<and> (n s' \<le> 2^LENGTH(irq_len) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
     \<longrightarrow> (x s' = 0 \<or> 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)

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:

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 \<noteq> 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]