Prevent module-object substitution timeouts

[ebmoon]

Summary

Large module parameters containing many substitutive objects no longer spend
minutes rebuilding delta-resolver maps before their bodies are elaborated.
Sequential substitutions are now retained as a bounded, serializable
composition and normalized in balanced rounds, preserving the existing
Mod_subst.join law while removing eager work from the repeated
Libobject.Ref path.

The compiled-object checker understands the new representation, and the
regressions cover module paths, canonical kernel names, constants, inductives,
constructors, projections, inline bodies, resolver domain/codomain transforms,
functor parameters, includes, with Module, rollback/replay, Marshal round
trips, and skewed long chains.

Performance

Measurements used an isolated switch where Rocq, ELPI, Lean import,
QuickChick, and the snapshot dependencies were rebuilt against one OCaml ABI.

Workload	Before	After
Exact 230-component empty-body parameter probe	>305 s, ~11.2 GiB RSS	1.22 s, 597,432 KiB RSS
Full QuickChick runATest interface	300 s timeout, ~18 GiB RSS in the preserved snapshot	10.73 s, 938,184 KiB RSS
Representative ztauto interface	300 s timeout family	8.60 s, 552,204 KiB RSS

On the synthetic parameter-load profile, the same 69 join calls went from 68
resolver substitutions and 185 delta folds to zero of each. This is measured
hot-path evidence, not a claim of a specific asymptotic bound.

Validation

• dune build rocq-runtime.install rocq-core.install
• 16/16 Mod_subst unit characterizations pass, including 10,000 left-associated joins and bounded right-associated joins
• ModuleObjectSubstitutionChain.v, IncludeSelfChain.v, and Tescik.v compile and pass rocqchk
• Complete module suite: 57/57 pass, including compiled-object checks
• Exact ProbeBaseline.v: 2.13 s, 595,004 KiB RSS
• Exact ProbeNoImport.v: 1.22 s, 597,432 KiB RSS
• Full QuickChick runATest: 10.73 s, 938,184 KiB RSS
• Representative ztauto: 8.60 s, 552,204 KiB RSS

dune build @check could not complete in the local switch because the optional
lablgtk3-sourceview3 and camlzip packages are absent; both affected Rocq
install targets above build cleanly.

Known limitation

The representative genChecker target no longer times out and reaches its
generated body in 29.42 s (586,392 KiB RSS), where it encounters an existing
generated-relation type mismatch (A_R has type A1 -> A2 -> Type but
PRUnivalent A1 A2 is expected). That downstream generator error is separate
from module-parameter loading and is not changed here.

Post-Deploy Monitoring & Validation

This is compiler-internal rather than a live service change. Healthy signals
are green module/rocqchk CI, downstream interface builds completing without
gen_subst_delta_resolver dominating parameter loading, and no time/RSS
regressions on large module signatures. Revert this PR if CI finds substitution
semantic differences, compiled-object validation failures, or material
small-workload regressions; validate through this PR's CI and the next
downstream QuickChick rebuild, owned by the Rocq maintainers and downstream
package maintainers respectively.

• Added / updated test-suite.

---

[ebmoon]

@JasonGross

[JasonGross]

This seems good at a glance, please also submit upstream to rocq (or I can submit upstream if you prefer)