SR-31 'multiply-instantiated detection' is marked verified but the reject is dead code — multiply-instantiated modules fuse successfully on the live path (#362 wired it against its own commit message)

[avrabe]

Summary

Safety requirement SR-31 "Multiply-instantiated module detection" is marked verified in docs/verification-matrix.md (and safety/requirements/traceability.yaml, sw-verifications.yaml), evidenced by the unit test merger::tests::ls_m_5_multiply_instantiated_module_rejected. But the shipped behavior is the opposite: on the live fuse path a component that instantiates one core module 2×/3× is accepted (fused rc=0), not rejected. The DuplicateModuleInstantiation reject the test verifies is dead code on real input, so SR-31's "verified" status is vacuous vs the actual behavior — the classic "verification that doesn't cover the shipped path" gap.

Root cause

feat(adr7): multiply-instantiated module support (#362, commit cf3c55d) wired expand_multiply_instantiated_modules unconditionally into fuse_with_stats:

meld-core/src/lib.rs:419-425
  for component in &mut self.components {
      duplicated_modules += crate::core_instance_topology::expand_multiply_instantiated_modules(component);
  }

Its own inline comment states this makes the reject "an unreachable backstop". Because the expansion runs before resolve/merge, the DuplicateModuleInstantiation returns at merger.rs:686 and resolver.rs:2432 never fire for the ordinary (instantiate $m) shape. The verifying test ls_m_5_multiply_instantiated_module_rejected calls the merger reject in isolation, bypassing fuse_with_stats, so it still passes while the live path does the opposite.

The commit's own message even contradicts the code: "Deliberately NOT wired … Until that oracle + a Tier-5 Mythos pass on the wiring land, meld still rejects multiply-instantiated modules; this module is exercised only by its own 6 structural unit tests." The code wires it on all input.

Reproduction (meld 0.41.3, fresh release)

meld fuse dup.wasm  -o out.wasm   # component instantiating one core module 2× → rc=0 "Fusion complete!"
meld fuse tri.wasm  -o out.wasm   # 3× → rc=0

Both should be rejected per SR-31. The output is a multi-memory module with N independent memories (func0→mem0, func1→mem1, func2→mem2) — for this simple shape it is correct (no aliasing, verified by execution). So this is not a miscompile; it is a safety-claim / traceability defect: SR-31 is certified verified while its property does not hold on the shipped path.

Why it matters

A functional-safety consumer reading the verification matrix believes multiply-instantiation is rejected pending the execution-oracle + Mythos gate the commit describes. That gate is bypassed on all user input. The corners the commit itself flags as un-execution-verified — per-instance import wiring and shared-memory duplicate instantiation — are now reachable by users with no guard, while SR-31 asserts they cannot occur. (Shared+--address-rebase is separately blocked by the #352 missing-reloc hard-fail — verified.)

Suggested action

Either (a) restore the DuplicateModuleInstantiation reject on the live fuse_with_stats path until the execution oracle + Mythos gate land (matching the commit message + SR-31), or (b) if the feature is intended to ship, update SR-31's status and verifying evidence to a test that exercises the live fuse path (not the isolated merger reject), and add execution verification for the per-instance import wiring + shared-memory duplicate-instantiation corners.

[avrabe]

Confirmed — this is valid on all three counts, thanks for the sharp catch. Grounded:

1. SR-31 verified-via-dead-code. Correct: expand_multiply_instantiated_modules is wired unconditionally in fuse_with_stats (lib.rs) before resolve/merge, so DuplicateModuleInstantiation (merger.rs:686 / resolver.rs:2432) is unreachable on the live (instantiate $m) path, while ls_m_5_multiply_instantiated_module_rejected verifies it in isolation. So SR-31's verified in the matrix/traceability asserts a property the shipped path contradicts.

2. Commit-message/code contradiction. Correct and my error: PR feat(adr7): multiply-instantiated module support — RFC-46 Q1 (path-H inc 3) #362 grew from a "mechanism only, not wired" first commit into the full wired feature, but the squashed commit retained the first commit's "deliberately NOT wired … meld still rejects" language. The code wires it. Apologies for the misleading merged message.

3. Reachable unverified corner — confirmed reproduced. My inc-3 execution oracle covered MultiMemory only (independent memories per instance: bump/bump$0 → independent counters). Under SharedMemory the same fixture fuses but exports only a single bump (the second instance is collapsed, not independently exported) — i.e. the shared-memory duplicate-instantiation semantics are unverified and murky, exactly as you flag. (Shared+--address-rebase is separately hard-failed by fix(351): hard-fail on stale reloc.CODE offsets instead of silent miscompile #352, agreed.)

Fix (your option b, honestly): the feature ships for the verified case and is guarded for the unverified one:

• Restore the DuplicateModuleInstantiation reject on the live path under SharedMemory (independence unverified there) — only run the normalization for the MultiMemory/multi case that the execution oracle actually proves.
• Repoint SR-31/SR-55 evidence to the live-path execution oracle (multiply_instantiated_runtime), not the isolated merger reject, and split the claim: MultiMemory support (verified) vs SharedMemory reject (verified) — updating docs/verification-matrix.md + traceability.yaml + sw-verifications.yaml, not just safety-requirements.yaml.
• Per-instance import wiring stays noted as un-execution-tested (import-free fixtures).

Fix incoming.