ADR-0203 stage 4: elided artifacts serialize + load soundly — closes D-515(1) - #140
Merged
Conversation
…ly (closes D-515(1))
Elided-bounds codegen is now AOT-serializable end-to-end:
- format v0.5 gains `flag_bounds_elided` (header flags bit 2; in the
header round-trip test).
- produce: the ElidedBoundsNotAotSerializable refusal is GONE — the
loader upholds the ADR-0202 "elided ⇒ guarded binding" invariant: the
re-link re-registers per-func oob-stub trap entries against the LOADED
block (linkWithThunks does this unconditionally; oob_stub_off rides
func_extras since stage 2), setup's allocBacking binds the guarded
reservation with NO plain-heap fallback for a qualifying memory, and
the loader explicitly REJECTS an elided artifact on a non-guarded host
(ElidedArtifactNeedsGuardedHost — ADR-0202 D5's "non-D1-host reject";
vacuous today, enforced rather than left to set-inclusion coincidence).
- compileWasmForAot no longer forces `.explicit` — the default
`zwasm compile` output is now ELIDED on qualifying memories (verified:
header flags 0x05), the same codegen the fresh JIT runs.
- deserializer restores `bounds_elided` from the header flag.
- Unit (produce.zig): an elided module serializes, deserializes, and its
page-straddling load GUARD-FAULTS to a clean Error.Trap through the
re-registered entries; `expect(bounds_elided)` pre-serialize proves the
code has no inline check, so Trap can only arrive via the registry.
- test/aot/corpus gains oob_guard_boundary ({wat,wasm}) so the
cross-process differential pins artifact-OOB → clean trap on every run
(63/63 MATCH).
- D-515 row: item (1) struck ((2) spec-assert corpus remains); ADR-0202
status note updated (all five D5 clauses realized, host-reject named).
DA-critique check #8 (17/20) findings folded in: the missing non-D1-host
reject implemented; artifact-OOB coverage added to the aot corpus (the
prior evidence claim misattributed the fuzz-corpus fixture); format
round-trip test extended with the new flag; ADR wording corrected;
stale runner_test comment re-pointed. The critique independently proved
the soundness chain cross-process (elided .cwasm → fresh process →
trap kind=oob_memory).
Verified: zig build test green · test-aot-diff 63/63 MATCH with elided
artifacts as the default output · fuzz-diff 0 mismatch · Rosetta
x86_64-macos suite green.
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
1 participant
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.
Summary
AOT-full-fidelity campaign, Phase IV stage 4 (ADR-0203 D4 / ADR-0202 D5). Guard-page-elided codegen — the default
.automode — is now AOT-serializable end-to-end, closing D-515(1).zwasm compile's default output is now the SAME elided machine code the fresh JIT runs.The soundness chain (each link verified + critique-proven cross-process)
flag_bounds_elided(v0.5 header bit 2) iff the compile elided; theElidedBoundsNotAotSerializablerefusal andcompileWasmForAot's forced.explicitare gone.linkWithThunksdoes this unconditionally, andoob_stub_offhas riddenfunc_extrassince stage 2.allocBackingfails loudly), andqualifies()is a pure function of the module declaration — identical verdicts at compile- and load-time.ElidedArtifactNeedsGuardedHost— the ADR-0202 D5 "non-D1-host reject" clause; vacuous today since every jit_mem platform is guarded-capable, but enforced rather than left to set-inclusion coincidence).Verification
Error.Trapthrough the re-registered entries (expect(bounds_elided)pre-serialize proves no inline check exists, so a Trap can only arrive via the registry redirect).test/aot/corpusgainsoob_guard_boundary— the cross-process differential now pins artifact-OOB → clean trap on every CI run: 63/63 MATCH with elided artifacts as the default output.zig build testgreen ·fuzz-diff0 mismatch · Rosetta x86_64-macos suite green..cwasm→ fresh process →trap kind=oob_memory.Bookkeeping
D-515 row: item (1) struck — item (2) (spec-assert corpus under elision) remains. ADR-0202 status note: AOT elision ENABLED, all five D5 clauses realized.
Next
Stage 5 =
--cachetransparent compilation cache (D-508, ADR-0203 D5) → stage V retrospective → v2.2.0 release (user-directed).