Skip to content

fix(#275): self-contained --cortex-m call_indirect — loud-decline the R11/linmem silent miscompile - #717

Merged
avrabe merged 1 commit into
mainfrom
fix/275-selfcontained-call-indirect
Jul 11, 2026
Merged

avrabe merged 1 commit into
mainfrom
fix/275-selfcontained-call-indirect

Conversation

@avrabe

@avrabe avrabe commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

Outcome: B (loud decline) — and what the gate is

Read this first (silent-miscompile fix): the gate here is a decline oracle, NOT an execution differential. Outcome B removes the wrong dispatch, so there is nothing left to execute on the self-contained path — a generic "compile → assert linmem[0]==100" check will now find entry absent (loud-skipped), which is the fix, not a regression. An execution differential asserting linmem[0]==100/200/300 is what outcome A (the dedicated func-table) would need, and A is silicon-gated (see below).

To verify:

SYNTH=/path/to/target/debug/synth \
  python scripts/repro/call_indirect_275_selfcontained_differential.py   # ORACLE: PASS
# or, by hand:
synth compile scripts/repro/call_indirect_275_selfcontained.wat --cortex-m -t cortex-m3 -o /tmp/ci.elf
#   → warning: skipping function 'entry': ... — #275   +   "1 of 4 functions were skipped"
#   → `entry` absent from the ELF (no silent dispatch)

(The oracle defaults SYNTH to ./target/debug/synth — set it to your real target dir to avoid the stale-binary trap.)

Root cause (residual of #275, after the v0.11.33 reachability closure)

On the self-contained image path (build_multi_func_cortex_m_elf, i.e. no --relocatable — falcon's actual firmware path), call_indirect emits its guarded dispatch, but the function-pointer load is:

lsl.w  r12, idx, #2
ldr.w  r12, [r11, r12]   ; R11 = LINEAR-MEMORY base
blx    r12

The contiguous R11 funcref-table region is only ever populated by an external runtime/harness (the --relocatable layout contract). A self-contained image has no such runtime, so ldr [r11, idx*4] reads "function pointers" from linear-memory DATA — a silent miscompile (exit 0, 0 skips, garbage dispatched; the repro stored the selector to linmem[0] instead of 100/200/300).

The fix (B, the sound interim — AFD-008)

The self-contained path now declines call_indirect LOUDLY: the function is skipped with a #275 diagnostic naming the linmem collision, surfaced in the skip count, and absent from the output — never a silent colliding dispatch. "An unlowerable op must Err, never silently continue."

  • Selector gains reject_self_contained_call_indirect, set by the backend from !config.relocatable, and checked at the top of resolve_call_indirect_guards (covers both the direct select_with_stack path and the optimized→direct fallback — the optimizer already declines call_indirect).
  • !config.relocatable is the right discriminator: every non-relocatable ARM path (optimized abs-base, native-pointer ABI, build_cortex_m_elf) has R11=linmem with no external table provider.

Untouched: the relocatable / host-linked path

Scoped by !config.relocatable, so the --relocatable path — where a runtime places the table region at R11 — is byte-for-byte untouched:

Non-goals / upgrade path

  • B does not foreclose A. When the silicon-gated dedicated-table fix lands (a Thumb-bit-set func-pointer table in a dedicated region + a non-R11 table base), the flag simply stops declining. Even a unicorn-green A would be "held for silicon" per the maintainer's own comment on this issue, so B closes the actual soundness bug now and A stays a clean follow-up.
  • RISC-V has its own selector — out of scope for a --cortex-m issue (not a regression).

Gate / evidence

  • crates/synth-cli/tests/call_indirect_275_selfcontained.rs — self-contained declines loudly (#275 + skip count + entry absent + func_1/2/3 still compile) and --relocatable still emits entry (both ISAs). 2/2 pass.
  • scripts/repro/call_indirect_275_selfcontained{.wat,_differential.py} — decline oracle, ORACLE: PASS.
  • cargo test -p synth-backend -p synth-synthesis -p synth-cli green; cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings clean.
  • Frozen anchors 10/10.

Part of VCR (#242); the on-target Cortex-M long pole for jess (falcon's fused core has 61 call_indirect sites).

Refs #275, #242. DO NOT MERGE — maintainer gates (will re-run the decline oracle).

🤖 Generated with Claude Code

… R11/linmem silent miscompile

On the self-contained image path (build_multi_func_cortex_m_elf, no
--relocatable) the call_indirect dispatch loads the function pointer from the
contiguous R11 funcref-table region — but R11 is the linear-memory base and a
self-contained image has NO runtime to populate that region. So
`ldr ip,[r11,idx*4]` reads function pointers from linear-memory DATA: a silent
miscompile (exit 0, 0 skips, wrong dispatch), the residual half of #275 after
the v0.11.33 reachability-closure fix.

Outcome B (the sound interim, AFD-008): the self-contained path now DECLINES
call_indirect LOUDLY (the function is skipped with a #275 diagnostic naming the
linmem collision, and counted) instead of emitting the colliding dispatch. The
full fix — a dedicated Thumb-bit-set func-pointer table + a non-R11 table base —
is silicon-gated (#275) and lands as a separate increment.

Scoped by !config.relocatable: the host-linked (--relocatable) path, where a
runtime places the table region at R11, is UNTOUCHED — the #642/#650/#664/#676
dispatch bytes and differentials are unchanged. The selector's own unit tests
construct the selector directly (flag defaults false) and are unaffected.

Gate: crates/synth-cli/tests/call_indirect_275_selfcontained.rs (self-contained
declines loudly + entry absent + relocatable still emits entry, both ISAs) and
scripts/repro/call_indirect_275_selfcontained{.wat,_differential.py}.

VCR (#242) / on-target Cortex-M long pole for jess (falcon 61 call_indirect
sites). Frozen anchors 10/10; #642/#650/#664/#676 oracles PASS.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@avrabe
avrabe merged commit 99f67d1 into main Jul 11, 2026
36 checks passed
@avrabe
avrabe deleted the fix/275-selfcontained-call-indirect branch July 11, 2026 04:53
@codecov

codecov Bot commented Jul 11, 2026

Copy link
Copy Markdown

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 16, 2026
- NEW call_indirect_275_selfcontained_execution_differential.py (falcon
  shape, heterogeneous 5-slot table): the DEFAULT self-contained image
  runs under unicorn (its own Reset_Handler; nothing fabricated) vs the
  wasmtime oracle — 14/14 green incl. a linear-memory-reading dispatch
  target (the #717 non-collision proof) and all §4.4.8 traps (OOB /
  type-mismatch / null all stop AT a UDF). RED on origin/main (verified
  against a main-built binary: dispatchers loud-skip, exit 1).
- call_indirect_275_selfcontained_differential.py: converted from the
  #717 loud-decline gate to emission + RESIDUAL-decline gate (cortex-m
  emits the flash table; A32/Cortex-R5 self-contained still #275
  loud-declines; --relocatable untouched on both ISAs).
- call_indirect_275_selfcontained.rs: same three-way split.
- CI: call-indirect-275-selfcontained-oracle job (both scripts).

Frozen: all 110 repro differentials swept — 21 failures are
pre-existing host-dep (identical on a main-built binary), 0 regressions;
self-contained + relocatable outputs byte-identical old-vs-new for
modules without call_indirect, and for the relocatable call_indirect
fixtures (650/664/676).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 17, 2026
…f table

The v0.42 #717 loud-decline is converted into a real lowering on the
Thumb-2 --cortex-m image path: the funcref table ships in FLASH
(appended after the function code, the #758 ROM-image pattern) and the
dispatch reaches it PC-relative through an LdrSym literal-pool pointer
(Abs32 reloc against __synth_func_table, patched post-layout) — never
via R11 (linear-memory base, the #717 collision), R9/R10, or R12.

Same WASM Core §4.4.8 trap semantics as the relocatable R11 expansion:
MOVW size; CMP; BLO+1; UDF (OOB), the #676 sidecar type check (CMP id;
BEQ+1; UDF), and the #664 null-slot check (CMP #0; BNE+1; UDF), all on
two callee-saved scratches from free_callee_saved (loud Err on
exhaustion). Enabled only when the image builder that emits and patches
the table will run (cortex-m, not --relocatable, no imports); every
other self-contained configuration keeps the loud #275 decline
(A32/Cortex-R5, simple-ELF builder, select_default).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 17, 2026
- NEW call_indirect_275_selfcontained_execution_differential.py (falcon
  shape, heterogeneous 5-slot table): the DEFAULT self-contained image
  runs under unicorn (its own Reset_Handler; nothing fabricated) vs the
  wasmtime oracle — 14/14 green incl. a linear-memory-reading dispatch
  target (the #717 non-collision proof) and all §4.4.8 traps (OOB /
  type-mismatch / null all stop AT a UDF). RED on origin/main (verified
  against a main-built binary: dispatchers loud-skip, exit 1).
- call_indirect_275_selfcontained_differential.py: converted from the
  #717 loud-decline gate to emission + RESIDUAL-decline gate (cortex-m
  emits the flash table; A32/Cortex-R5 self-contained still #275
  loud-declines; --relocatable untouched on both ISAs).
- call_indirect_275_selfcontained.rs: same three-way split.
- CI: call-indirect-275-selfcontained-oracle job (both scripts).

Frozen: all 110 repro differentials swept — 21 failures are
pre-existing host-dep (identical on a main-built binary), 0 regressions;
self-contained + relocatable outputs byte-identical old-vs-new for
modules without call_indirect, and for the relocatable call_indirect
fixtures (650/664/676).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 17, 2026
…f table

The v0.42 #717 loud-decline is converted into a real lowering on the
Thumb-2 --cortex-m image path: the funcref table ships in FLASH
(appended after the function code, the #758 ROM-image pattern) and the
dispatch reaches it PC-relative through an LdrSym literal-pool pointer
(Abs32 reloc against __synth_func_table, patched post-layout) — never
via R11 (linear-memory base, the #717 collision), R9/R10, or R12.

Same WASM Core §4.4.8 trap semantics as the relocatable R11 expansion:
MOVW size; CMP; BLO+1; UDF (OOB), the #676 sidecar type check (CMP id;
BEQ+1; UDF), and the #664 null-slot check (CMP #0; BNE+1; UDF), all on
two callee-saved scratches from free_callee_saved (loud Err on
exhaustion). Enabled only when the image builder that emits and patches
the table will run (cortex-m, not --relocatable, no imports); every
other self-contained configuration keeps the loud #275 decline
(A32/Cortex-R5, simple-ELF builder, select_default).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 17, 2026
- NEW call_indirect_275_selfcontained_execution_differential.py (falcon
  shape, heterogeneous 5-slot table): the DEFAULT self-contained image
  runs under unicorn (its own Reset_Handler; nothing fabricated) vs the
  wasmtime oracle — 14/14 green incl. a linear-memory-reading dispatch
  target (the #717 non-collision proof) and all §4.4.8 traps (OOB /
  type-mismatch / null all stop AT a UDF). RED on origin/main (verified
  against a main-built binary: dispatchers loud-skip, exit 1).
- call_indirect_275_selfcontained_differential.py: converted from the
  #717 loud-decline gate to emission + RESIDUAL-decline gate (cortex-m
  emits the flash table; A32/Cortex-R5 self-contained still #275
  loud-declines; --relocatable untouched on both ISAs).
- call_indirect_275_selfcontained.rs: same three-way split.
- CI: call-indirect-275-selfcontained-oracle job (both scripts).

Frozen: all 110 repro differentials swept — 21 failures are
pre-existing host-dep (identical on a main-built binary), 0 regressions;
self-contained + relocatable outputs byte-identical old-vs-new for
modules without call_indirect, and for the relocatable call_indirect
fixtures (650/664/676).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 17, 2026
…ive flash funcref table (converts the #717 loud-decline) (#792)

* feat(#275): self-contained call_indirect via PC-relative flash funcref table

The v0.42 #717 loud-decline is converted into a real lowering on the
Thumb-2 --cortex-m image path: the funcref table ships in FLASH
(appended after the function code, the #758 ROM-image pattern) and the
dispatch reaches it PC-relative through an LdrSym literal-pool pointer
(Abs32 reloc against __synth_func_table, patched post-layout) — never
via R11 (linear-memory base, the #717 collision), R9/R10, or R12.

Same WASM Core §4.4.8 trap semantics as the relocatable R11 expansion:
MOVW size; CMP; BLO+1; UDF (OOB), the #676 sidecar type check (CMP id;
BEQ+1; UDF), and the #664 null-slot check (CMP #0; BNE+1; UDF), all on
two callee-saved scratches from free_callee_saved (loud Err on
exhaustion). Enabled only when the image builder that emits and patches
the table will run (cortex-m, not --relocatable, no imports); every
other self-contained configuration keeps the loud #275 decline
(A32/Cortex-R5, simple-ELF builder, select_default).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* test(#275): red-first execution differential + gates moved to residuals

- NEW call_indirect_275_selfcontained_execution_differential.py (falcon
  shape, heterogeneous 5-slot table): the DEFAULT self-contained image
  runs under unicorn (its own Reset_Handler; nothing fabricated) vs the
  wasmtime oracle — 14/14 green incl. a linear-memory-reading dispatch
  target (the #717 non-collision proof) and all §4.4.8 traps (OOB /
  type-mismatch / null all stop AT a UDF). RED on origin/main (verified
  against a main-built binary: dispatchers loud-skip, exit 1).
- call_indirect_275_selfcontained_differential.py: converted from the
  #717 loud-decline gate to emission + RESIDUAL-decline gate (cortex-m
  emits the flash table; A32/Cortex-R5 self-contained still #275
  loud-declines; --relocatable untouched on both ISAs).
- call_indirect_275_selfcontained.rs: same three-way split.
- CI: call-indirect-275-selfcontained-oracle job (both scripts).

Frozen: all 110 repro differentials swept — 21 failures are
pre-existing host-dep (identical on a main-built binary), 0 regressions;
self-contained + relocatable outputs byte-identical old-vs-new for
modules without call_indirect, and for the relocatable call_indirect
fixtures (650/664/676).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* docs(#275): CHANGELOG — self-contained call_indirect finale + #791 finding

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* test(#275): pin the imports-decline and skipped-target loud-bail residual gates

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Jul 30, 2026
…851)

`substrate::plan` materializes the globals `.data` image and the `.text`
funcref table from decoded module state, and is called by BOTH aarch64 ELF
drivers, so the regions the code addresses and the regions the object ships
cannot disagree.

PRECONDITION STATUS, stated plainly: neither region is one. Both are EMITTED
BY SYNTH and reached with `adrp` + `add :lo12:` against a symbol the same
object defines. That is deliberately unlike `x28` (the linear-memory base),
which IS an embedder precondition — v0.53 made that explicit so the next
feature would not quietly add a second, and this one does not. Using
PC-relative addressing instead of a dedicated base register also sidesteps the
#275/#717 collision class outright: there is no base register to collide with.

Layouts. Globals: ONE 8-BYTE SLOT PER GLOBAL at `k*8` (NOT the ARM/#643 dense
width-summed layout) — uniform slots stay naturally aligned for `ldr x`, where
a dense layout puts an i64 at offset 4, and the offset stays a foldable
constant. Funcref table: 8 bytes per slot, `[u32 structural class id][b
func_N]`, null slots `[0][brk #0]`.

Every unrepresentable shape LOUD-DECLINES with a machine reason rather than
guessing (9 unit tests, decline text asserted): imported globals (value
arrives at instantiation), a global with no decoded const initializer
(float/v128/non-const expr), >2048 globals or a v128 slot, an unsized
(growable imported) table, >4095 slots or class ids past the 12-bit guard
immediates, and a table slot holding an imported function.

The load-bearing one: an UNVERIFIABLE element segment declines instead of
shipping a table. `funcref_region_slots` degrades such a table to all-null,
which traps on every dispatch — that LOOKS conservative but is wrong in the
other direction, trapping where wasmtime calls successfully.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 30, 2026
Three parity-gate entries flip Err(reason) -> lowering in this commit, so no
gap claim outlives its gap: `global.get`, `global.set` (ledger entries deleted)
and `call_indirect` (`a64_extended_surface` -> `Ok(())`).

GLOBALS. `global k` lives at `__synth_globals + k*8` in the `.data` image synth
EMITS; the address is formed `adrp`+`add :lo12:`. i32/f32 use the low word of
the slot, i64/f64 the whole slot, and the size-scaled load/store immediate
folds the offset. PRECONDITION STATUS: none. Unlike `x28` (the linear-memory
base, which IS an embedder precondition), synth ships the region and its
initial values; the linker places it. No base register, so nothing can collide
with the linear-memory base the way #275/#717 did on ARM.

CALL_INDIRECT. All three §4.4.8 traps are emitted, none inherited from `blr`:

  cmp w_idx,#size / b.lo +2 / brk      out-of-range index
  adrp+add / add x16,x16,w_idx,uxtw#3  slot address (no base register)
  ldr w17,[x16] / cmp w17,#expected    signature mismatch — and, because a
  b.eq +2 / brk                        null slot's class id is 0 and every
                                       real class is >=1, the null check too
  add x16,x16,#4 / blr x16             the slot's tail-branch trampoline

The compared id is STRUCTURAL, so duplicate-but-identical types stay
interchangeable; comparing raw type indices would trap where wasmtime calls.
x16/x17 are the AAPCS64 IP0/IP1 scratch registers — outside both the value-
stack temp pool (x9..x15) and the argument registers, so no guard can alias a
live value.

PARAM HOMING was the blocker: a non-leaf function referencing a parameter
loud-declined, and a table index almost always IS a parameter, so
`call_indirect` would only have dispatched on constants. Non-leaf functions now
give EVERY local (params included) an 8-byte stack slot and store the incoming
argument registers there at the prologue, reusing the non-param-local machinery
verbatim. That restores both properties the decline protected: a post-call read
hits the slot (which the call cannot clobber), and every value-stack entry is a
temp again, so argument marshalling stays hazard-free. LEAF functions are
untouched and byte-identical, so writing a param still declines there and that
ledger entry stays valid; a non-leaf FLOAT param also still declines (homing a
v-register needs an FP store this encoder lacks).

Verified end-to-end, not just in unit tests: both features compile, LINK with
a real `ld.lld`, and disassemble correctly — the linker relaxes `adrp`+`add`
to `adr`, resolves `__synth_globals` to the emitted `.data` (0x29 = 41,
0x11f71fb04cb = 1234567890123), and the table lays out as
`[1][b func_0] [1][b func_1] [2][b func_2] [0][brk #0]`.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Aug 5, 2026
…#899)

* aarch64: encoder primitives for call_indirect + globals (#851)

Adds the five A64 primitives lane L3 needs, each pinned to
`clang -c -target aarch64-linux-gnu` ground truth in a unit test:

  blr xn              — the indirect-call branch (call_indirect dispatch)
  adrp xd, <sym>      — PC-relative page address (the data-region reach)
  cmp wn/xn, #imm12   — flags-only immediate compare (no scratch register)
  add xd,xn,wm,uxtw#s — scaled zero-extended index add (table slot address)

`adrp`'s 21-bit page delta splits across TWO disjoint fields (immlo[30:29] +
immhi[23:5]); a contiguous placement is silently wrong for every delta >= 1,
so the split is pinned by a second test against capstone decodes of the
literal words (0xF0000000 = adrp x0,#0x3000; 0x90000020 = #0x4000;
0xF0FFFFE0 = #-0x1000).

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64 ELF: .data section + the four AArch64 relocation kinds (#851)

The substrate both lane-L3 features need, with NO new precondition.

`DataBlob` — a synth-EMITTED `.data` (PROGBITS, ALLOC|WRITE, align 8) plus
`STT_OBJECT` symbols into it. This is the honest answer to "where do WASM
globals live on a backend that emits no startup and no linker script": the
bytes ARE the initial values, shipped in the object; the linker places the
section; code reaches it with `adrp`+`add :lo12:`. Contrast `x28` (the
linear-memory base), which IS an embedder precondition — globals add no
second one.

RelocKind gains the three AArch64 kinds beyond CALL26: JUMP26 (282, the
funcref-table `b func_N` trampolines), ADR_PREL_PG_HI21 (275) and
ADD_ABS_LO12_NC (277) (the symbol-address pair). The builder's kind→type
mapping has NO wildcard, and an unplaceable symbol now PANICS instead of
silently dropping the relocation — an unrelocated `adrp #0` would address the
wrong page (silent miscompile), where the old `continue` merely assumed it
could not happen.

`ElfFunction::is_object` types the `.text`-resident funcref table as OBJECT,
not FUNC: it is branched INTO at slot+4, never called at slot+0.

Byte-identity: an empty `DataBlob` reproduces the previous 5-section layout
exactly (asserted by `empty_data_blob_is_byte_identical_to_the_data_free_builder`),
so every globals-free module is unchanged.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* core: structural type-class ids + per-type result counts for aarch64 dispatch (#851)

Three additions the aarch64 `call_indirect` + globals lowerings consume:

* `DecodedModule::structural_type_class_ids()` — factored out of
  `call_indirect_guards`, which exposed the ids ONLY when its heterogeneous-
  table sidecar existed. The aarch64 dispatch type-checks UNCONDITIONALLY, so
  it needs them always. These are STRUCTURAL classes, not raw type indices:
  WASM type equality is structural, so `call_indirect (type 1)` must reach a
  function declared with a duplicate `type 0` (SS4.4.8) — comparing indices
  would trap where wasmtime calls.
* `DecodedModule::funcref_region_class_ids()` — per-slot class id in the same
  contiguous order as `funcref_region_slots()`, 0 for null/unclassifiable.
  Storing this beside each slot makes ONE compare serve as both the SS4.4.8
  type check and the null check (0 never equals a real class, which is >= 1).
* `type_result_counts` on `DecodedModule` + `CompileConfig` — an indirect
  callee is known only by its static type, and `type_ret_i64/f32/f64` conflate
  void with i32, so the 0-vs-1 "is a value pushed back" distinction needs its
  own table.

Plus `CompileConfig::a64_substrate_emitted`, FAIL-SAFE at `false`: the aarch64
selector will loud-decline globals and `call_indirect` unless the driver has
actually emitted the `.data` globals image and the `.text` funcref table, so a
driver that compiles bodies without emitting the regions cannot ship code
addressing a symbol that is not there.

Behavior unchanged: `call_indirect_guards` output is identical (pure
refactor), and no consumer reads the new fields yet.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64: substrate planner — the one source of both emitted regions (#851)

`substrate::plan` materializes the globals `.data` image and the `.text`
funcref table from decoded module state, and is called by BOTH aarch64 ELF
drivers, so the regions the code addresses and the regions the object ships
cannot disagree.

PRECONDITION STATUS, stated plainly: neither region is one. Both are EMITTED
BY SYNTH and reached with `adrp` + `add :lo12:` against a symbol the same
object defines. That is deliberately unlike `x28` (the linear-memory base),
which IS an embedder precondition — v0.53 made that explicit so the next
feature would not quietly add a second, and this one does not. Using
PC-relative addressing instead of a dedicated base register also sidesteps the
#275/#717 collision class outright: there is no base register to collide with.

Layouts. Globals: ONE 8-BYTE SLOT PER GLOBAL at `k*8` (NOT the ARM/#643 dense
width-summed layout) — uniform slots stay naturally aligned for `ldr x`, where
a dense layout puts an i64 at offset 4, and the offset stays a foldable
constant. Funcref table: 8 bytes per slot, `[u32 structural class id][b
func_N]`, null slots `[0][brk #0]`.

Every unrepresentable shape LOUD-DECLINES with a machine reason rather than
guessing (9 unit tests, decline text asserted): imported globals (value
arrives at instantiation), a global with no decoded const initializer
(float/v128/non-const expr), >2048 globals or a v128 slot, an unsized
(growable imported) table, >4095 slots or class ids past the 12-bit guard
immediates, and a table slot holding an imported function.

The load-bearing one: an UNVERIFIABLE element segment declines instead of
shipping a table. `funcref_region_slots` degrades such a table to all-null,
which traps on every dispatch — that LOOKS conservative but is wrong in the
other direction, trapping where wasmtime calls successfully.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64: globals + call_indirect LOWER, with param homing (#851)

Three parity-gate entries flip Err(reason) -> lowering in this commit, so no
gap claim outlives its gap: `global.get`, `global.set` (ledger entries deleted)
and `call_indirect` (`a64_extended_surface` -> `Ok(())`).

GLOBALS. `global k` lives at `__synth_globals + k*8` in the `.data` image synth
EMITS; the address is formed `adrp`+`add :lo12:`. i32/f32 use the low word of
the slot, i64/f64 the whole slot, and the size-scaled load/store immediate
folds the offset. PRECONDITION STATUS: none. Unlike `x28` (the linear-memory
base, which IS an embedder precondition), synth ships the region and its
initial values; the linker places it. No base register, so nothing can collide
with the linear-memory base the way #275/#717 did on ARM.

CALL_INDIRECT. All three §4.4.8 traps are emitted, none inherited from `blr`:

  cmp w_idx,#size / b.lo +2 / brk      out-of-range index
  adrp+add / add x16,x16,w_idx,uxtw#3  slot address (no base register)
  ldr w17,[x16] / cmp w17,#expected    signature mismatch — and, because a
  b.eq +2 / brk                        null slot's class id is 0 and every
                                       real class is >=1, the null check too
  add x16,x16,#4 / blr x16             the slot's tail-branch trampoline

The compared id is STRUCTURAL, so duplicate-but-identical types stay
interchangeable; comparing raw type indices would trap where wasmtime calls.
x16/x17 are the AAPCS64 IP0/IP1 scratch registers — outside both the value-
stack temp pool (x9..x15) and the argument registers, so no guard can alias a
live value.

PARAM HOMING was the blocker: a non-leaf function referencing a parameter
loud-declined, and a table index almost always IS a parameter, so
`call_indirect` would only have dispatched on constants. Non-leaf functions now
give EVERY local (params included) an 8-byte stack slot and store the incoming
argument registers there at the prologue, reusing the non-param-local machinery
verbatim. That restores both properties the decline protected: a post-call read
hits the slot (which the call cannot clobber), and every value-stack entry is a
temp again, so argument marshalling stays hazard-free. LEAF functions are
untouched and byte-identical, so writing a param still declines there and that
ledger entry stays valid; a non-leaf FLOAT param also still declines (homing a
v-register needs an FP store this encoder lacks).

Verified end-to-end, not just in unit tests: both features compile, LINK with
a real `ld.lld`, and disassemble correctly — the linker relaxes `adrp`+`add`
to `adr`, resolves `__synth_globals` to the emitted `.data` (0x29 = 41,
0x11f71fb04cb = 1234567890123), and the table lays out as
`[1][b func_0] [1][b func_1] [2][b func_2] [0][brk #0]`.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64: CI-wired execution oracles for globals + call_indirect (#851)

Two unicorn-vs-wasmtime differentials, both wired into the `aarch64-oracle`
job in this commit with `set -o pipefail` and a non-zero-count grep (the #890
"oracle exists and runs nowhere" class).

`aarch64_globals_851_differential.py` — 17 checks, 6 exports. Reads the INITIAL
values before anything is written (a region shipping zeros fails), then runs
the cases IN SEQUENCE against ONE region so a dropped or misdirected
`global.set` shows up in the next `global.get`. i32 and i64 globals are
interleaved, so a wrong slot stride shifts every later global.

`aarch64_call_indirect_851_differential.py` — 35 checks (23 trap, 12 value),
6 exports. All three §4.4.8 traps, plus the direction an "always trap" lowering
would hide: a structurally-DUPLICATE type must NOT trap.

Both harnesses act as the LINKER — they place `.text` and `.data` on different
pages and resolve ADRP page / ADD lo12 / JUMP26 themselves — so a wrong page
delta, lo12, or trampoline displacement diverges rather than passing.

RED-FIRST, and it earned its keep: the first version of the call_indirect
oracle PASSED a compiler with the bounds guard removed. Past-the-end bytes
read as class id 0, so the TYPE check trapped anyway and masked it. The fixture
now declares TWO tables, making index 4 of table 0 land on table 1's fully
valid, type-matching `$mul` slot — so only the bounds guard can trap there, and
the same fixture makes a dropped per-table base offset return 30-vs-13 instead
of agreeing by coincidence. Five injected miscompiles are now caught:

  weakened bounds guard    -> differential red (4 BUG lines)
  dropped base offset      -> differential red (2 BUG lines)
  removed type check       -> differential red (6 BUG lines)
  null slot made callable  -> differential red (2 BUG lines)
  dense globals layout     -> differential red (4 BUG lines)

One injection is NOT decidable by execution: a SIGNED bounds compare (`b.lt`
for `b.lo`). Under emulation a negative index passes the signed guard and then
faults on the unmapped scaled address, so it traps either way — but on real
silicon that address can be mapped and the dispatch would branch into it. It is
pinned instead by `call_indirect_guard_sequence_uses_an_unsigned_bounds_compare`,
which asserts the whole guard sequence word-for-word (verified red: exit 101
when only the shipped code, not the expectation, is mutated).

Plus fail-safe and scaling unit tests: both features decline under a default
`ModuleCtx`, the slot offset is size-scaled per access width, and a global
index past the region declines.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* docs: aarch64 globals + call_indirect — precondition status pinned (#851)

The FEATURE_MATRIX template row now says plainly what v0.52's cold review
caught the last version of this doc getting wrong: the globals region and the
funcref table are EMITTED BY SYNTH, not preconditions. `x28` (the linear-memory
base) remains the ONE aarch64 precondition, and the row says so in those words,
so a reader cannot come away thinking lane L3 added a second ambient input.

The row also enumerates the new LOUD DECLINES by name rather than implying full
coverage: imported globals, a global with no decoded const initializer, a
non-leaf float param, a growable imported table, an unverifiable element
segment, and a table slot holding an imported function.

Two new `claims.yaml` pins hold those claims to evidence, both verified
RED-FIRST:

  SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION — flipping the sentence to
    "are ALSO preconditions" reddens the gate; pinned to substrate.rs, the
    `.data` DataBlob, and the ADRP relocation kind actually being emitted.
  SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS — unwiring either oracle from
    ci.yml reddens the gate, so the §4.4.8 trap claim cannot outlive its
    execution evidence.

`aarch64_selector_ops` 161 -> 164 (global.get, global.set, call_indirect).
Generated status files regenerated with the script (NOT hand-edited); the
coordinator should re-run `--emit-status` once after the lane fan-in, since
every aarch64 lane moves this counter.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64: the lane's DECLINES are gated by machine reason, not just by failing (#851)

Extends the CI-wired decline-matrix honesty oracle with the seven shapes lane
L3 deliberately refuses, and upgrades the oracle itself: an entry may now pin
the machine REASON its diagnostic must contain, because "it failed somehow" is
not evidence that it failed for the right cause — a decline with the wrong
reason is a different bug than a decline.

  imported global                      -> "imports 1 global"
  float global (no decoded const init) -> "no decoded constant initializer"
  v128 global                          -> (declines upstream at decode)
  growable imported table              -> "no compile-time size"
  passive element segment              -> "not statically verifiable"
  table slot holding an import         -> "imported function"
  non-leaf FLOAT param                 -> "FLOAT parameter"

10/10 loud-decline, 6 with their reason asserted; the oracle also fails if NO
entry carries a reason, so the new check cannot rot into a no-op.

Also verified across the whole aarch64 gate set: all 14 unicorn oracles exit 0,
`aarch64_calls_851.py` is 5/5 bit-identical, the `--relocatable` path emits the
funcref table too, and gale's native acceptance matrix now reports 45 ops
accepted / 119 native checks with an EMPTY declined frontier (baseline 32).

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* aarch64 oracles: ci-status headers + `set -euo pipefail` CI steps (#890, #851)

Two corrections from lane L1's oracle-wiring gate, applied to this lane's
harnesses.

1. Both new oracles carry `# ci-status: wired`. VERIFIED non-inert: pointing
   the workflow step at a different filename makes the gate report
   "declares `wired` but NO workflow STEP runs it — the gate is INERT",
   so the declaration is checked against the parsed executable surface rather
   than taken on trust.

2. The CI steps now use `set -euo pipefail`, not bare `set -o pipefail`.
   `pipefail` alone leaves the step's exit status as its LAST command's, so a
   harness that printed FAIL and exited 1 could still green the step — the
   precise #890 class. The verdict is now taken three ways: the script's own
   exit status (via `-e`), a non-zero check-count grep, and the summary
   `RESULT: PASS` line.

MUTATION-PROVEN, not assumed: perturbing the comparison inside the
call_indirect harness (`exp` -> `exp + 1`, so a CORRECT compiler mismatches)
makes the exact CI step body exit 1, and restoring it returns exit 0. That is
the check L1 found `sret_decide_differential.py` failing — a gate that printed
`MISMATCH <-- BUG` and exited 0.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant