test(dissolve): lock cabi-arena-realloc → __cabi_arena_realloc linkability (#418) - #420
Merged
Merged
Conversation
…ility (#418) Verifies the synth-layer mechanism for the BYO-OS lean-MCU dissolve (gale#89): an `env::__cabi_arena_realloc` import (the grow-free `cabi_realloc` extern) lowers, on the `--relocatable` host-link path (#197), to a `R_ARM_THM_CALL` relocation against an UNDEFINED `__cabi_arena_realloc` symbol — which the native link binds to the TCB's arena allocator. synth references the symbol; the TCB provides it; the linker binds it (synth never implements the allocator or the realloc contract). Empirically confirmed (was a read-only triage claim before): the .o carries `*UND* __cabi_arena_realloc` + the relocation at the call site. synth sees the verbatim core field name — the kebab `cabi-arena-realloc` is component-surface, never reaching synth — so no naming transform on our side. Frozen-safe: new test (synth-cli, object .o parse) + a minimal wat fixture, zero codegen; control_step verified unchanged (113 instrs); rivet non-xref 0. The full end-to-end check on gale's real dissolved component lands when that fixture arrives (requested on #418). Trace: skip Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jul 17, 2026
…arena-realloc importers, decline matrix + CI oracle CLI: on the self-contained Cortex-M --all-exports path (ARM backend, not --relocatable, not --native-pointer-abi), a sole env::__cabi_arena_realloc import is bound via the synth-core arena-bind rewrite — the compile yields a fully self-contained ET_EXEC image (previously: ET_REL 'link me with the Kiln bridge', the embedder seam). Pinned opt-out: --no-bind-cabi-arena. Untouched seams (asserted): --relocatable keeps the #420 TCB layering (undefined symbol, host-link-bound); modules with OTHER imports keep the host seam entirely (never a half-bound hybrid); modules without the import pass through byte-identically. Gates: - scripts/repro/cabi_arena_bind_418_differential.py now GREEN (was red-first): unicorn runs the image's own startup then each export; wasmtime satisfies the import with a host arena at a DIFFERENT base — all six pointer-independent cases match, exhaustion traps on both sides. CI job arena-bind-418-oracle. - cabi_arena_bind_418.rs: ET_EXEC + no undefined arena symbol + binding log; opt-out/relocatable restore the external seam; wrong signature declines loudly; mixed imports keep ET_REL. - Harness anti-vacuity: startup must reach the first compiled function AND leave R11 = __linear_memory_base (a min()-over-symbols bug initially ran nothing and greened 4/6 cases on a zeroed machine — caught and locked). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 17, 2026
…ssolve — synthesized in-module arena allocator (#799) * test(#418): red-first execution differential — self-contained arena-import dissolve vs wasmtime host arena The fixture is the wit-bindgen cabi-realloc-extern / meld-dissolve shape (exported cabi_realloc routing to env::__cabi_arena_realloc, Rust/wasm-ld layout globals). The gate asserts the default self-contained compile yields ET_EXEC and every export matches wasmtime ground truth where the import is satisfied by a host arena implementing the #418 contract (0/0 -> align, bump, copy-on-grow, bounded + trap on exhaustion). Host arena uses a DIFFERENT base than synth will, so only pointer-independent semantics can green. RED today: the arena import degrades the compile to an ET_REL link-me object (the embedder seam) — script exits at the ET_EXEC assert. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#418): arena-bind rewrite — replace the sole env::__cabi_arena_realloc import with a synthesized in-module allocator A wasm->wasm transform in synth-core: when env::__cabi_arena_realloc is the module's ONLY import, remove it and prepend a DEFINED allocator function implementing the #418 contract ((i32x4)->i32; old_len==0&&new_len==0 -> align; bump allocation from an appended cursor global; copy-on-realloc of min(old,new) bytes; bounded [arena_base, linmem_end) — traps on exhaustion, never memory.grow). Imports-first index space + sole-import removal + prepend = every call/export/elem index PRESERVED, no remapping; untouched sections are byte-copied verbatim (count-patch only on function/global/code). arena_base mirrors the shipped used-extent rule: max(data_end, i32-const global inits <= linmem) — covering __stack_pointer / __heap_base / __data_end — floor 16, 16-aligned. Loud declines: wrong signature, no/64-bit memory, non-const data offsets, no defined functions, no arena room. Other imports present -> NotApplicable pass-through (the module keeps the host-linked seam). Result is Validator-checked before use. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#418): wire the arena binding — self-contained dissolve of cabi-arena-realloc importers, decline matrix + CI oracle CLI: on the self-contained Cortex-M --all-exports path (ARM backend, not --relocatable, not --native-pointer-abi), a sole env::__cabi_arena_realloc import is bound via the synth-core arena-bind rewrite — the compile yields a fully self-contained ET_EXEC image (previously: ET_REL 'link me with the Kiln bridge', the embedder seam). Pinned opt-out: --no-bind-cabi-arena. Untouched seams (asserted): --relocatable keeps the #420 TCB layering (undefined symbol, host-link-bound); modules with OTHER imports keep the host seam entirely (never a half-bound hybrid); modules without the import pass through byte-identically. Gates: - scripts/repro/cabi_arena_bind_418_differential.py now GREEN (was red-first): unicorn runs the image's own startup then each export; wasmtime satisfies the import with a host arena at a DIFFERENT base — all six pointer-independent cases match, exhaustion traps on both sides. CI job arena-bind-418-oracle. - cabi_arena_bind_418.rs: ET_EXEC + no undefined arena symbol + binding log; opt-out/relocatable restore the external seam; wrong signature declines loudly; mixed imports keep ET_REL. - Harness anti-vacuity: startup must reach the first compiled function AND leave R11 = __linear_memory_base (a min()-over-symbols bug initially ran nothing and greened 4/6 cases on a zeroed machine — caught and locked). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore: drop stray __pycache__ artifact + ignore it Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Fable 5 <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
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.
What
Verifies — and regression-locks — the synth-layer mechanism for #418 (the BYO-OS lean-MCU dissolve, gale#89). An
env::__cabi_arena_reallocimport lowers, on the--relocatablehost-link path (#197), to aR_ARM_THM_CALLrelocation against an UNDEFINED__cabi_arena_reallocsymbol — which the native link binds to the TCB's arena allocator.Layering: synth references the symbol; the TCB provides it; the linker binds it. synth never implements the allocator or the canonical-ABI realloc contract.
This was a read-only triage claim before; now confirmed empirically (the
.ocarries*UND* __cabi_arena_realloc+ the call-site relocation) and locked by a test. synth sees the verbatim core field name — the kebabcabi-arena-reallocis component-surface and never reaches synth, so no naming transform on our side.Frozen-safe
New test (synth-cli,
object.oparse) + a minimal wat fixture; zero codegen; control_step verified unchanged (113 instrs); rivet non-xref 0.The full end-to-end check on gale's real dissolved component lands when that fixture arrives (requested on #418).
Refs: #418, gale#89, meld#301, synth#197.
🤖 Generated with Claude Code