feat(adr7): multiply-instantiated module support — RFC-46 Q1 (path-H inc 3) - #362
Merged
Conversation
…m (path-H inc 3, slice 1) RFC-46 Q1 (multiply-instantiated modules) "duplicate" resolution: meld currently REJECTS a component that instantiates the same core module more than once (SR-31, DuplicateModuleInstantiation). This lands the MECHANISM to support it instead — as a bounded, structurally-verified first slice. `core_instance_topology::expand_multiply_instantiated_modules` deep-clones a module per 2nd..Nth instantiation and rewrites that instantiation to the clone, so after the pass no module is instantiated more than once. Each instance then gets its OWN functions/memory/tables/globals via the merger's per-module machinery (already proven correct for N distinct modules) — no shared mutable state (STPA H-1), and every (component, module)-keyed merge map gets a distinct key per instance (no silent overwrite). The whole class of duplication-corruption bugs is dissolved by reusing the existing proof. Deliberately NOT wired: activating this (dropping the reject) flips a verified safety requirement and must be gated on a differential EXECUTION oracle proving two instances keep independent mutable state end-to-end (identical-content module duplication can stress export-name / segment handling a structural test can't see). 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. - core_instance_topology.rs: the pass + 6 unit tests (single/distinct unchanged; double/triple/interleaved → N distinct module identities; FromExports ignored). - lib.rs: register the module. - safety-requirements.yaml: SR-55 (draft) — the duplicate-support capability, refines SR-31, mitigates LS-M-5; verification-description records the execution-oracle gate. rivet validate PASS. Full meld-core lib suite green (487, unaffected — pass is unwired); fmt + clippy clean. Refs #354 (ADR-7 path-H inc 3), RFC-46 Q1 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
LS-N verification gate✅ 59/59 approved LS entries verified
Approved Failed LS entries(none) Missing regression tests(none) Updated automatically by |
…C-46 Q1, inc 3) Completes RFC-46 Q1 "duplicate": meld now SUPPORTS a component that instantiates the same core module more than once, instead of rejecting it. The `core_instance_topology` normalization pass is wired into `Fuser::fuse_with_stats` before resolve/merge. It gives each instantiation a distinct module identity, so the merger's per-module machinery (proven correct for N distinct modules) allocates each instance independent functions / memory / tables / globals — no shared mutable state (STPA H-1), no (component, module)- keyed map overwrites. After the pass no module is instantiated more than once, so the DuplicateModuleInstantiation reject becomes an unreachable backstop (retained; its ls_m_5 unit test still passes). The pass is a no-op for single-instantiation components and idempotent for a repeated fuse. Differential EXECUTION oracle (the gate for flipping this safety behavior): tests/multiply_instantiated_runtime.rs — a component instantiating one core module (a mutable counter) TWICE is fused (MultiMemory, CoreModule), VALIDATED, and executed on wasmtime. The two instances' counters advance independently (inc→1,2; inc$0→1; inc→3; inc$0→2); a shared-state H-1 corruption would fail the load-bearing `inc$0` first-call == 1 assertion. - lib.rs: wire the normalization pass (with an info log of how many modules were duplicated). - multiply_instantiated_runtime.rs: the differential execution oracle. - safety-requirements.yaml: SR-55 draft→implemented (mechanism + wiring + oracle green locally; verified pending CI/merge); SR-31 noted as superseded for handleable cases, reject retained as backstop. Full meld-core suite green (0 failures, no regression); fmt + clippy clean; rivet validate PASS. Refs #354 (ADR-7 path-H inc 3), RFC-46 Q1 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 21, 2026
… verified (#363) Strengthens the RFC-46 Q1 (multiply-instantiated modules) verification: the merged inc-3 oracle proved only GLOBAL-state independence. This adds the other critical mutable-state axis — independent LINEAR MEMORY and DATA SEGMENTS. `two_instances_keep_independent_memory_and_data_segments`: a core module keeps its counter in linear memory, seeded to 5 by a DATA segment, instantiated twice. Fused + validated + executed on wasmtime: bump→6,7; bump$0→6 (its own data-seeded 5, independent); bump→8; bump$0→7. A shared memory / mis-based segment (the segment-duplication risk an index-space audit flagged) would make bump$0's first call observe the other instance's writes. With globals + memory + data-segments all execution-proven, the H-1 hazard is comprehensively covered → SR-55 status implemented→verified. One axis remains un-execution-tested and is noted in SR-55: per-instance IMPORT wiring (distinct args per instance); the fixtures are import-free. Not a mutable-state hazard. Test + requirement only (no src change). Both oracles green; fmt clean; rivet validate PASS. Refs #362, #354 (ADR-7 path-H inc 3), RFC-46 Q1 Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jul 22, 2026
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
… fix SR-31 traceability (#366) avrabe (#364) correctly caught that SR-31 "multiply-instantiated detection" is marked verified via an ISOLATED reject test (ls_m_5) while #362 wired the normalization unconditionally into fuse_with_stats — so the reject is dead code on the live path and the shipped behavior (accept) is the OPPOSITE of the certified property. The inc-3 execution oracle only covered MultiMemory; under SharedMemory the instances share one linear memory and independence is unverified (my probe: the 2nd instance collapses to a single `bump` export). Fix (avrabe's option b, honestly): - lib.rs: gate `expand_multiply_instantiated_modules` to explicit MultiMemory — the only strategy the execution oracle proves keeps per-instance state independent. Under SharedMemory (unverified) and Auto (implicit, ADR-4) the normalization is skipped and the DuplicateModuleInstantiation reject fires. So shipped behavior == verified behavior. - multiply_instantiated_runtime.rs: `shared_memory_and_auto_reject_multiply_ instantiated` proves the reject fires on the LIVE fuse path under both. - Traceability repointed to the live-path evidence (not the isolated reject): docs/verification-matrix.md SR-31 row, sw-verifications.yaml SWV-31, safety-requirements.yaml SR-31 verification-description + SR-55 scope note. The MultiMemory support (SR-55) is unchanged and still execution-verified (independent globals + memory + data segments). Per-instance import wiring stays noted as un-execution-tested (import-free fixtures). Full meld-core suite green (0 failures); fmt + clippy clean; rivet validate PASS. Refs #364, #362, SR-31, SR-55 Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
…s + static-PIC + same-memory transcoding (#369) Ships the full ADR-7 path-H arc (address-strategy seam #359, call-lowering seam #360, multiply-instantiated modules #362/#363, static-PIC fold #365, ADR record #354) plus the extended-const fold completion (#368), the #364 safety fix (#366), and same-memory string transcoding (#367). New capabilities: multiply-instantiated module support (RFC-46 Q1, MultiMemory, SR-55), static-PIC data/element offset folding (#353), same-memory string transcoding (#361). Safety: multiply-instantiated gated to the execution- verified MultiMemory case (#364); the sync same-memory cross-encoding miscompile closed (#360/#361). Falsification statements in CHANGELOG. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Executes ADR-7 path-H, increment 3 — RFC-46 Q1 multiply-instantiated
modules, the "duplicate" resolution, execution-verified end-to-end. The
user's stated RFC-46 priority.
What changed
meld previously rejected a component that instantiates the same core module
more than once (SR-31 →
DuplicateModuleInstantiation). It now supports it.core_instance_topology::expand_multiply_instantiated_modules— apre-resolve normalization that, for each 2nd..Nth instantiation of a core
module, appends a deep clone (a fresh
module_idx) and rewrites theinstantiation to the clone. After the pass no module is instantiated more
than once.
lib.rs— the pass is wired intoFuser::fuse_with_statsbeforeresolve/merge (with an info log of how many modules were duplicated).
Why it's correct — it reuses a proof
The merger's index-remapping is already proven correct for N distinct
modules. Turning "module M instantiated N times" into "N distinct modules"
means each instance gets independent functions/memory/tables/globals — no
shared mutable state (H-1) — and every
(component, module)-keyed merge mapgets a distinct key per instance, so the whole class of duplication-overwrite
bugs (segment_bases, realloc_map, resource maps, mutable globals) an index-space
audit enumerated simply cannot arise.
Differential execution oracle (the gate)
tests/multiply_instantiated_runtime.rs::two_instances_keep_independent_counter_state— a component instantiating one core module (a mutable counter) twice is
fused (MultiMemory, CoreModule), validated, and executed on wasmtime. The two
instances' counters advance independently:
A shared-state (H-1) corruption would make
inc$0's first call return 3 — theload-bearing assertion is that it returns 1.
Verification
core_instance_topology::tests).meld-coresuite green — 0 failures, no regression (the pass is ano-op for single-instantiation components; the SR-31 reject is retained as an
unreachable backstop,
ls_m_5still passes).rivet validatePASS.refinesSR-31,mitigatesLS-M-5; SR-31 noted as superseded for handleable cases.Notes
inc; meld disambiguates thesecond with a
$0suffix (existing identical-name dedup).Refs #354 (ADR-7 path-H inc 3), RFC-46 Q1