fix(clone): compare oracle-call restrictions when overriding a module type

[Yiping106283]

Summary

clone ... with module type X <- Y (likewise = and <=) accepted Y whenever its parameters and procedure names/types matched those of X; the allowed-oracle-call sets (proc f() : t {O.g}) were never compared. Lemmas proved for A <: X are replayed verbatim for A <: Y, so with a looser Y they can be instantiated with adversaries the original proof never accounted for, which yields false (see the MRE in the issue).

Fixes #1123

Root cause

src/ecTheoryReplay.ml, replay_modtype, decides the override with EcReduction.EqTest.for_msig. Its implementation, for_module_sig in src/ecReduction.ml, compares mis_params and mis_body only and ignores mis_oinfos, in both Alias and Inline modes. The typing-side check EcTyping.check_item_compatible (mode `Eq) does compare the sets, but the clone path bypasses it.

Fix

for_module_sig now additionally requires, per procedure, equality of the allowed-call sets: the parameter renaming already applied to the body is applied to the oracle infos, the paths are normalised with NormMp.norm_xfun when ~norm is set, and the lists are compared as Sx sets, so the order in which the oracles are written is irrelevant.

Since for_module_type falls back to for_module_sig for parameters whose type names differ, the signatures of functor parameters are covered as well. for_msig has no other caller; for_mexpr (module overrides in clone) inherits the stricter comparison of its parameters, where it is equally required.

Exact equality is required in both directions, as in check_item_compatible. A looser Y is unsound as explained above. A tighter Y is unsound too: module-type binders also occur negatively, in lemma hypotheses (forall (A <: X), ...) => ..., and the replayed proofs (which are not re-checked) may instantiate an X-lemma or axiom at a module such as Wrap(B) that inhabits X but not Y.

Impact

Only clone overrides of module types (and, through the parameter comparison, of modules) whose oracle-call sets differ are affected; they are now rejected with the existing module type X is incompatible error. No clone in theories/ or examples/ overrides a module type or a module at all (the only such override is in tests/clone-module-stateless.ec, with equal oracle sets), so no existing development relied on the lax check; make unit and make stdlib pass, and make examples shows only the pre-existing ChaChaPoly/chacha_poly.ec prover-timeout failure that occurs identically on unpatched main.

Test

tests/clone-modtype-oinfos.ec: overrides that loosen or tighten the oracle set (via <-, = and <=) must fail, a mismatch inside a functor parameter's signature must fail, and the same set written in a different order must be accepted. The file fails on unpatched main (every fail clone is accepted there) and passes with this patch. The issue's MRE is now rejected at the clone line.