docs(adr): ADR-7 — ABI & linking-strategy architecture (canonical mix-and-match vs symmetric/PIC fast lane)#354
Merged
Merged
Conversation
LS-N verification gate✅ 59/59 approved LS entries verified
Approved Failed LS entries(none) Missing regression tests(none) Updated automatically by |
avrabe
added a commit
that referenced
this pull request
Jul 16, 2026
…erified stack Human decision (2026-07-16): status open → resolved. - Identity: balanced/dual — meld is BOTH the RFC-46 canonical reference AND the sealed-safety (symmetric+PIC) product; both first-class. - Ownership: own + formally verify the FULL lowering stack (canonical FACT + symmetric + PIC), no external lowering dependency — a safety tool must own a frozen verifiable trusted base (overrides the review's track-upstream default). - Reconciliation: own the IMPLEMENTATION; ABIs/conventions stay open standards (symmetric→BA, PIC→tool-conventions); path-H canonical fallback keeps mix-and-match, so this is not fragmentation. - Accepted risks named (scope/budget, parity treadmill, proof surface); the heterogeneous-composition theorem is now mandatory. - Next increments: extract address strategy; formalize call-lowering seam; RFC-46 Q1 multiply-instantiated; #353 Path-A PIC flatten. Refs #353, #354, RFC-46 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…uestion) Frames how meld should support the shared-address-space fast lane (PIC #353 + symmetric ABI) WITHOUT sacrificing RFC-46 canonical mix-and-match. Recommends path-H: an ABI-agnostic verified core + pluggable per-boundary call-lowering (canonical-FACT default / symmetric-direct opt-in, canonical as universal fallback) + pluggable address strategy (multi / shared-rebase / static-base-PIC). Grounds the 'split not rewrite' verdict in current coupling (adapter already separable; reloc interleaved) and ties in the RFC-46 multiply-instantiated- modules gap. Status: open — for human decision. Refs #353, RFC-46 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…identity choice Adds the decision-independent consensus from a 10-persona strategic review as requirements on ADR-7 (status stays open): - give away the ABIs, keep the proofs/attestation (the moat is verification) - silent downgrade = hard error (per-boundary strategy declared/attested/observable) - symmetric ABI must be standardized (BA/wit-bindgen) before a safety product; gated experimental/non-portable until then - concrete shape = one binary, two attested profiles (open/ecosystem + sealed-safety) - new heterogeneous-composition theorem as the key proof obligation - frames the one open decision: meld's identity + the load-bearing track-upstream-FACT-vs-own-the-fork sub-choice Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…erified stack Human decision (2026-07-16): status open → resolved. - Identity: balanced/dual — meld is BOTH the RFC-46 canonical reference AND the sealed-safety (symmetric+PIC) product; both first-class. - Ownership: own + formally verify the FULL lowering stack (canonical FACT + symmetric + PIC), no external lowering dependency — a safety tool must own a frozen verifiable trusted base (overrides the review's track-upstream default). - Reconciliation: own the IMPLEMENTATION; ABIs/conventions stay open standards (symmetric→BA, PIC→tool-conventions); path-H canonical fallback keeps mix-and-match, so this is not fragmentation. - Accepted risks named (scope/budget, parity treadmill, proof surface); the heterogeneous-composition theorem is now mandatory. - Next increments: extract address strategy; formalize call-lowering seam; RFC-46 Q1 multiply-instantiated; #353 Path-A PIC flatten. Refs #353, #354, RFC-46 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
docs/adr7-abi-linking-strategy
branch
from
July 16, 2026 21:46
1209467 to
adcca29
Compare
avrabe
added a commit
that referenced
this pull request
Jul 17, 2026
…th-H inc 1) (#359) * refactor(adr7): extract the address strategy seam from the merger (path-H inc 1) Executes ADR-7 path-H, increment 1: extract the per-module address/memory strategy resolution out of Merger::merge into a dedicated address_strategy module, behavior-preservingly. This is the pluggable seam the decided architecture hangs off — the shared-rebase strategy lives here now; multi-memory resolves to an empty plan; static-base PIC (#353) and the per-boundary call-lowering seam come in later increments. - address_strategy.rs: AddressPlan + resolve_address_plan — the full decision + validation (path-F MissingRelocMetadata, memory64 reject, #351 MisalignedReloc backstop). has_direct_memory_access passed as a closure to keep the original lazy short-circuit exactly. - merger.rs: the ~50-line reloc-consumption block replaced with one call. - 4 unit tests (rebasing-off/base-0/no-reloc-direct-fail/bulk-only + laziness). No behavior change: canonical gating fixtures (test_326_reloc_const_rebasing, test_address_rebasing) + drop_realloc + full meld-core suite all green; fmt/clippy clean. Refs #354 (ADR-7) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * docs(adr7): clarify address-plan scope — empty plan is not fusion disabled A colleague reading #359 read "multi-memory resolves to an empty plan" as "multi-memory + FACT fusion is stopped". It is not: an AddressPlan carries only which reloc sites to shift for a shared-memory base. An empty plan means no address rebasing is needed (multi-memory keeps each component's memory at its own base) — it does not touch cross-component adapter (FACT) generation, which runs identically. Spell that out in the module doc so the seam can't be misread. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- 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.
What
ADR-7 (open design question): how should meld support the shared-address-space
fast lane (PIC #353 + Christof's symmetric ABI) without sacrificing RFC-46
canonical mix-and-match? Drafted per the "be careful / stay true / think if we
need a rework to split" steer.
Not a code change — a decision artifact for review (@cpetig too). Status open;
humans promote.
The core argument
"staying true" and must not be traded away.
ABI turns cross-component calls into ordinary linking of mangled symbols
(zero-copy, no dynamic alloc — the ASIL-D property), retiring most of the
~16.4k-line FACT/adapter subsystem for that input class.
does not mix with stock canonical components.
strategy with canonical as the universal fallback — direct wiring only
where both sides opt in, FACT adapter everywhere else. Composability is never
lost; zero-copy is only gained.
has 0 merger refs (separable); reloc/rebasing has ~26 (extract it); the
Rocq-proven core is untouched.
Error::DuplicateModuleInstantiationrejects them) is the same core-instancetopology work Evaluate PIC / shared-everything dynamic linking as an input ABI (dissolves the #351 reloc-drift class) — revisit ADR-6 #353 needs; path-H does it once and shares it.
Paths
G bolt-on (rejected) · H clean strategy-split (recommended) · I separate tool
(rejected) · J do-nothing/canonical-only (baseline).
Does not block
#352 (canonical
--emit-relocsbackstop) ships regardless — it serves themix-and-match path today.
Refs #353, RFC-46, ADR-4, ADR-6.