feat(clone): reintroduce module overriding for stateless modules

[strub]

Module overriding in clones (clone T with module X <- Y, also <=, =, and theory S <- S' for theories containing modules) was removed by #458 as a fix for the unsoundness reported in #380: a clone transfers the statements of a theory without replaying their proofs, and proofs freely use the disjointness of program variables owned by distinct modules; identifying two modules that own state can therefore turn a proved statement into a false one.

That argument does not apply to modules owning no program variable. The only facts the logic has about a concrete module are judgments on its procedures, its glob, the disjointness of its own variables, and memory restrictions (normalised to variable sets). With an empty own-glob and AST-equal components, the source and target modules are indiscernible, so substituting one for the other is a renaming.

This restores the override for exactly that fragment. An override is accepted iff:

• the source and the target own no program variable, transitively through their sub-modules (EcCoreModules.module_own_state; calling external stateful modules and taking module parameters is allowed);
• the target is a concrete top-level module;
• the components are AST-equal after the clone substitution (EqTest.for_mexpr ~body:false, so an alias target is accepted).

Otherwise the clone fails at the override clause, naming the offending module: "declares state and cannot be overridden", "is not a concrete top-level module", or "is incompatible". theory S <- S' is likewise accepted when every module of S is stateless, and rejected naming the first stateful one (this replaces the former blanket rejection of any theory containing a module). Stateful modules keep failing as before.

Mode semantics follow the pre-#458 code: <- rewrites references to the target and drops the item, <= additionally keeps an alias, = keeps an alias only. The alias mode now honours rename [module].

Both #380 counter-examples are kept as failing regression tests (tests/clone-module-stateless.ec).

Also fix a pre-existing defect in EqTest.for_module_expr reached by the new check: the two functor parameter lists were bound with add_modules (a List.fold_left2) without being compared, unlike for_module_sig. An arity mismatch raised Invalid_argument, and parameters of different module types were treated as equal whenever the body did not use them. Add the same for_module_type guard.

Related: #380 (left open — the stateful case is not addressed), #458 (the removal this partially reverts).