Arrays with non-constant lengths

[eponier]

I open this to get some feedback. This is still early draft, in particular no proof has been tried.

The length of an array is no longer an integer, but a simple arithmetic expression (with additions and multiplications).

This change is used to implement some kind of templating for functions (cf. tests/template) as a POC.

[eponier]

Comments:

• this should allow to get rid of (part of?) insert_copy_and_fix_length.ml, this has not been done yet
• the template feature is a POC, we should discuss if this is a reasonable feature to expose complementary to the module system we may want to have, or if we should get rid of it in favour of a module system
• the concrete syntax is horrible and has to be changed
• would it make sense to have fn f(reg u64 a[]) with unspecified length?
• there is nearly no check in the current implementation that the template arguments are used correctly; if a template arg is used at a wrong place, this will trigger an error in the middle of a pass
• maybe this is an opportunity to remove all uses of int as lengths of arrays on the OCaml side (use Z.t instead)
• the fact that lengths of arrays are positive on the Rocq side is sometimes painful, it would be good to explore whether we can use Z instead

[eponier]

Also the feature was added on top of the param/subst machinery. I don't know if we want to remove it and get rid of the polymorphism on the type of length of arrays. What is done in this PR is not as expressive, though.