aarch64: call_indirect (§4.4.8 traps) + globals + param homing (#851)

.github/workflows/ci.yml

@@ -480,6 +480,37 @@ jobs:
         # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity
         # against a min=max module (growth failure is spec-forced there).
         run: SYNTH=./target/debug/synth python scripts/repro/aarch64_surface_851_differential.py
+      - name: Run #851 lane L3 GLOBALS execution oracle (emitted .data region + persistence)
+        # synth EMITS the globals region (a `.data` image carrying the decoded
+        # initializers) and reaches it `adrp`+`add :lo12:` — no base register,
+        # no precondition. The harness places `.text` and `.data` on DIFFERENT
+        # pages and resolves the relocations itself, so a wrong page delta or
+        # lo12 lands on the wrong bytes. NON-VACUITY: assert a non-zero check
+        # count (a harness that compiled nothing would otherwise pass silently)
+        # AND the summary verdict. `set -euo pipefail` (not bare `pipefail`,
+        # which leaves the step's status as the LAST command's) makes the
+        # script's own non-zero exit fail the step (#890).
+        run: |
+          set -euo pipefail
+          SYNTH=./target/debug/synth \
+            python scripts/repro/aarch64_globals_851_differential.py | tee globals851.txt
+          grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' globals851.txt
+          grep -q '^RESULT: PASS' globals851.txt
+      - name: Run #851 lane L3 CALL_INDIRECT execution oracle (§4.4.8 OOB + null + type traps)
+        # A64's `blr` is TOTAL; WASM §4.4.8 is not. All three traps must fire
+        # exactly where wasmtime traps — and the structurally-DUPLICATE type
+        # must NOT trap (the direction an "always trap" lowering would hide).
+        # NON-VACUITY: assert non-zero counts in BOTH directions, so a run that
+        # only trapped (or only returned values) fails, plus the summary
+        # verdict. `set -euo pipefail` makes the script's own non-zero exit fail
+        # the step (bare `pipefail` would leave the status as the last command's
+        # — the #890 class).
+        run: |
+          set -euo pipefail
+          SYNTH=./target/debug/synth \
+            python scripts/repro/aarch64_call_indirect_851_differential.py | tee ci851.txt
+          grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' ci851.txt
+          grep -q '^RESULT: PASS' ci851.txt
       - name: Run decline-matrix honesty oracle
         run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py
 

CHANGELOG.md

@@ -7,6 +7,65 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- **aarch64 `call_indirect` and WASM globals — the two largest remaining
+  structural declines on that backend (#851).** Both were "no substrate" gaps,
+  not missing selector arms, so the lane is mostly about *where the data lives*.
+
+  **Precondition status, stated plainly: this lane adds NONE.** synth EMITS both
+  regions into the object and reaches them with an `adrp` + `add :lo12:` pair
+  the linker resolves. Globals live in a synth-emitted `.data` section
+  (`__synth_globals`) carrying each global's decoded constant initializer; the
+  funcref table is a synth-emitted `.text`-resident array (`__synth_func_table`).
+  Neither needs a base register, a startup, a linker script or an ambient input.
+  That is deliberately *unlike* `x28` — the linear-memory base, which remains
+  the ONE aarch64 precondition the embedder must supply, exactly as v0.53
+  documented it. Using PC-relative addressing rather than a dedicated base
+  register also removes the #275/#717 collision class by construction: there is
+  no base register to collide with.
+
+  `call_indirect` emits all THREE WASM §4.4.8 trap guards inline, because A64's
+  `blr` is total and gives none of them for free (the #709
+  "more-total-than-WASM" class): an **out-of-range index** (an UNSIGNED bounds
+  compare), a **null slot**, and a **signature mismatch**. Each table slot is an
+  8-byte `[u32 structural-class-id][b func_N]` record — null slots are
+  `[0][brk #0]` — so one compare serves as both the type check and the null
+  check (id 0 matches no real class, which is ≥ 1). The compared id is
+  **structural**, so a module carrying duplicate-but-identical types keeps them
+  interchangeable; comparing raw type indices would trap where wasmtime calls.
+
+  **Param homing** landed as the prerequisite: a non-leaf function referencing a
+  parameter used to loud-decline, 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 an 8-byte stack slot and store the incoming
+  argument registers there at the prologue. Leaf functions are byte-identical.
+
+  Execution-verified against wasmtime under unicorn, CI-wired in the
+  `aarch64-oracle` job: `aarch64_globals_851_differential.py` (17 checks —
+  initial values, i32/i64 slots, stores persisting across calls) and
+  `aarch64_call_indirect_851_differential.py` (35 checks, 23 of them traps —
+  every §4.4.8 trap, plus the duplicate type that must NOT trap). The
+  `call_indirect` fixture declares TWO tables on purpose: the first version of
+  that oracle PASSED a compiler with the bounds guard removed, because
+  past-the-end bytes read as class id 0 and the type check trapped anyway. With
+  a second table, index 4 of table 0 lands on a fully valid, type-matching slot,
+  so only the bounds guard can trap there.
+
+  Rather than guess, these shapes LOUD-DECLINE with a machine reason: an
+  imported global, a global with no decoded constant initializer (float, v128 or
+  a non-const init expr), a growable imported table, an element segment that is
+  not statically verifiable, a table slot holding an imported function, a
+  non-leaf FLOAT parameter, and anything past the 12-bit guard immediates. The
+  unverifiable-element-segment decline is the load-bearing one: the existing
+  region reconstruction degrades such a table to all-null, which would trap on
+  every dispatch — conservative-*looking*, but wrong in the other direction.
+
+  The VCR-SEL-005 third-backend parity gate flips `global.get`, `global.set` and
+  `call_indirect` from `Err(reason)` to lowering in the same commit that makes
+  them lower, and two new `claims.yaml` pins hold the precondition and trap
+  claims to their evidence.
+
 ## [0.53.0] - 2026-07-30
 
 **"The last mile" — seven lanes.** falcon's VFP wall comes down, RISC-V compiles

artifacts/status.json

@@ -1,5 +1,5 @@
 {
-  "aarch64_selector_ops": 161,
+  "aarch64_selector_ops": 164,
   "arm_refinement_assumed_connection": 5,
   "arm_semantics_axioms": 72,
   "backends": [

claims.yaml

@@ -810,6 +810,48 @@ claims:
         glob: ['crates/synth-backend-aarch64/src/selector.rs']
         min: 1
 
+  # #851 lane L3 — the load-bearing HONESTY claim of this lane. v0.52's cold
+  # review caught a doc that described a shipped feature as "not yet"; v0.53
+  # made the `x28` precondition explicit so the NEXT feature could not quietly
+  # add a second one. This pin holds that line: if globals or the funcref table
+  # ever become an ambient input the embedder must supply, the sentence claiming
+  # they are EMITTED must change with it, and the gate reddens until it does.
+  - id: SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION
+    doc: scripts/templates/feature_matrix.md.tmpl
+    text: "The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents"
+    evidence:
+      # The single producer of both regions — if this file goes, the claim goes.
+      - kind: file-exists
+        path: crates/synth-backend-aarch64/src/substrate.rs
+      # The regions are placed in the object, not assumed: a `.data` blob and a
+      # `.text`-resident table, reached PC-relatively (no base register).
+      - kind: count-min
+        pattern: 'DataBlob'
+        glob: ['crates/synth-backend-aarch64/src/elf.rs']
+        min: 1
+      - kind: count-min
+        pattern: 'AArch64AdrPrelPgHi21'
+        glob: ['crates/synth-backend-aarch64/src/selector.rs']
+        min: 1
+
+  # #851 lane L3 — all THREE §4.4.8 traps are EMITTED, not inherited from `blr`
+  # (which is total). Pinned to both oracles being CI-wired, so the claim cannot
+  # outlive its evidence.
+  - id: SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS
+    doc: scripts/templates/feature_matrix.md.tmpl
+    text: "all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch"
+    evidence:
+      - kind: file-exists
+        path: scripts/repro/aarch64_call_indirect_851_differential.py
+      - kind: count-min
+        pattern: 'aarch64_call_indirect_851_differential\.py'
+        glob: ['.github/workflows/ci.yml']
+        min: 1
+      - kind: count-min
+        pattern: 'aarch64_globals_851_differential\.py'
+        glob: ['.github/workflows/ci.yml']
+        min: 1
+
   - id: SYNTH-MATRIX-AARCH64-DIVREM-POPCNT
     doc: scripts/templates/feature_matrix.md.tmpl
     # v0.53: the op list this sentence heads grew (select/CSEL, drop/nop, wrap,

crates/synth-backend-aarch64/src/backend.rs

@@ -82,7 +82,11 @@ impl AArch64Backend {
                 )));
             }
         };
-        let (words, call_sites) = selector::select_typed_cf_calls(
+        // #851 lane L3: the module-level context for globals + call_indirect.
+        // Its `substrate_emitted` flag is FAIL-SAFE — false unless the driver
+        // has actually placed `__synth_globals` / `__synth_func_table`.
+        let ctx = module_ctx(config);
+        let (words, call_sites, sym_relocs) = selector::select_typed_cf_calls(
             ops,
             num_params,
             &config.current_func_params_f32,
@@ -93,18 +97,22 @@ impl AArch64Backend {
             func_result_counts,
             func_ret_float,
             bounds,
+            &ctx,
         )
         .map_err(|e| BackendError::CompilationFailed(e.to_string()))?;
         let code: Vec<u8> = words.iter().flat_map(|w| w.to_le_bytes()).collect();
         // Each direct call site → an R_AARCH64_CALL26 against the callee's
-        // `func_N` symbol (emitted for every local function by compile_module).
+        // `func_N` symbol (emitted for every local function by compile_module);
+        // #851 lane L3 adds the `adrp`+`add :lo12:` pairs that reach the
+        // emitted globals region / funcref table.
         let relocations: Vec<CodeRelocation> = call_sites
             .iter()
             .map(|cs| CodeRelocation {
                 offset: cs.offset,
                 symbol: format!("func_{}", cs.callee),
                 kind: RelocKind::AArch64Call26,
             })
+            .chain(sym_relocs)
             .collect();
         Ok(CompiledFunction {
             name: name.to_string(),
@@ -122,6 +130,48 @@ impl AArch64Backend {
     }
 }
 
+/// #851 lane L3 — build the selector's module context from the driver-supplied
+/// [`CompileConfig`]. `substrate_emitted` is threaded verbatim: it is `false`
+/// unless the driver ran [`crate::substrate::plan`] AND placed its output, so a
+/// context built here can never authorize code that addresses a region the
+/// object lacks.
+fn module_ctx(config: &CompileConfig) -> selector::ModuleCtx {
+    let guards = &config.call_indirect_guards;
+    // Per table: (slot count, base SLOT index). `base_byte_offset` counts the
+    // 4-byte pointer slots of the ARM region contract, so /4 recovers the slot
+    // index — the aarch64 table uses the same SLOT ORDER with 8-byte records.
+    // Stop at the first table without a compile-time size/base: every later
+    // table's base is then not a constant, and an index past the end
+    // LOUD-DECLINES at the lowering (matching `funcref_region_slots`).
+    let mut tables: Vec<(u32, u32)> = Vec::new();
+    for t in &guards.tables {
+        match (t.table_size, t.base_byte_offset) {
+            (Some(size), Some(base_bytes)) => tables.push((size, base_bytes / 4)),
+            _ => break,
+        }
+    }
+    let n_types = config
+        .type_arg_counts
+        .len()
+        .max(config.type_class_ids.len())
+        .max(config.type_result_counts.len());
+    selector::ModuleCtx {
+        substrate_emitted: config.a64_substrate_emitted,
+        // #643 slot widths: 8 ⇒ an i64/f64 global (the `x` view).
+        global_is64: config.global_widths.iter().map(|w| *w == 8).collect(),
+        tables,
+        type_class_ids: config.type_class_ids.clone(),
+        type_arg_counts: config.type_arg_counts.clone(),
+        type_result_counts: config.type_result_counts.clone(),
+        type_ret_float: (0..n_types)
+            .map(|i| {
+                config.type_ret_f32.get(i).copied().unwrap_or(false)
+                    || config.type_ret_f64.get(i).copied().unwrap_or(false)
+            })
+            .collect(),
+    }
+}
+
 /// Count register parameters from the op stream (a local index read before it is
 /// written is a parameter). Mirrors the ARM/RISC-V backends' heuristic.
 fn count_params(ops: &[WasmOp]) -> u32 {
@@ -237,6 +287,28 @@ impl Backend for AArch64Backend {
             ));
         }
 
+        // #851 lane L3 — plan the MODULE-LEVEL substrate (globals `.data` image
+        // + `.text` funcref table) BEFORE compiling any body, so an
+        // unrepresentable shape declines the whole compile rather than being
+        // discovered after code that addresses it was emitted. `plan` is the
+        // single producer of both regions, so what the code addresses and what
+        // the object ships cannot disagree.
+        let uses_globals = locals.iter().any(|f| {
+            f.ops
+                .iter()
+                .any(|op| matches!(op, WasmOp::GlobalGet(_) | WasmOp::GlobalSet(_)))
+        });
+        let uses_call_indirect = locals.iter().any(|f| {
+            f.ops
+                .iter()
+                .any(|op| matches!(op, WasmOp::CallIndirect { .. }))
+        });
+        let substrate = crate::substrate::plan(
+            &crate::substrate::PlanInputs::from_module(module)
+                .with_usage(uses_globals, uses_call_indirect),
+        )
+        .map_err(|e| BackendError::CompilationFailed(format!("aarch64: {e}")))?;
+
         // #851: per-function "returns a float" mask (v0/d0 result) — a
         // float-returning callee is loud-declined by the call lowering.
         let nrf = module.func_ret_f32.len().max(module.func_ret_f64.len());
@@ -277,6 +349,17 @@ impl Backend for AArch64Backend {
                 current_func_param_count: declared_params.or(config.current_func_param_count),
                 num_imports: module.num_imported_funcs,
                 func_arg_counts: module.func_arg_counts.clone(),
+                // #851 lane L3: the substrate metadata + the fail-safe gate.
+                // `emitted` is true only when `plan` produced a region that the
+                // ELF build below actually places.
+                a64_substrate_emitted: substrate.emitted,
+                call_indirect_guards: module.call_indirect_guards(),
+                type_class_ids: module.structural_type_class_ids(),
+                type_arg_counts: module.type_arg_counts.clone(),
+                type_result_counts: module.type_result_counts.clone(),
+                type_ret_f32: module.type_ret_f32.clone(),
+                type_ret_f64: module.type_ret_f64.clone(),
+                global_widths: module.globals.iter().map(|g| g.slot_bytes).collect(),
                 ..config.clone()
             };
             let compiled = self.compile_function_with_results(
@@ -295,15 +378,20 @@ impl Backend for AArch64Backend {
             {
                 aliases.push(exp.clone());
             }
-            elf_funcs.push(ElfFunction {
-                symbols: aliases,
-                code: compiled.code.clone(),
-                relocations: compiled.relocations.clone(),
-            });
+            elf_funcs.push(ElfFunction::code(
+                aliases,
+                compiled.code.clone(),
+                compiled.relocations.clone(),
+            ));
             functions.push(compiled);
         }
 
-        let elf = elf::build_relocatable_object(&elf_funcs);
+        // #851 lane L3: the funcref table goes LAST in `.text`, so every real
+        // function keeps the offset it had before the table existed.
+        if let Some(table) = substrate.table {
+            elf_funcs.push(table);
+        }
+        let elf = elf::build_relocatable_object_with_data(&elf_funcs, &substrate.globals);
         Ok(CompilationResult {
             functions,
             elf: Some(elf),