feat(aarch64): RQ-64-ARM64LINUX — the arm64-Linux host-library claim, linked by ld.lld and EXECUTED (natively, qemu-user, unicorn) vs wasmtime

[avrabe]

RQ-64-ARM64LINUX — the arm64-Linux host-library claim, linked by a real host linker and EXECUTED

synth compile -b aarch64 --target cortex-a53 --relocatable has emitted a SysV ELF64 ET_REL for EM_AARCH64 that links into an arm64-Linux program since v0.51 — true by accident: no document claimed it, no oracle handed it to a host linker for that target, nothing executed the result. file and nm were the whole evidence base. This PR makes it a claim backed by execution, states the embedder precondition to the emitting file:line, and records the one thing the link found that does NOT work.

Refs #242 (VCR epic). Artifact artifacts/release-v0.64/RQ-64-ARM64LINUX.yaml → implemented.

What the oracle links and executes

scripts/repro/arm64_linux_host_link_rq64_differential.py (# ci-checks: emulations >= 2), fixture arm64_linux_host_link_rq64.wat:

1. compile the fixture exactly as a consumer would (-b aarch64 --target cortex-a53 --relocatable --all-exports) → synth.o, 28 defined symbols, exactly one undefined (host_add, the import);
2. generate a freestanding C harness FROM THE ORACLE'S OWN CASE TABLE (one source for the C sequence and the wasmtime sequence — globals persist across calls, so order matters), compiled clang -target aarch64-unknown-linux-gnu -ffreestanding -nostdlib -ffixed-x28, plus an asm _start that sets x28 once; the harness's only kernel surface is write(2) + exit_group(2);
3. link all three with ld.lld -m aarch64linux -static — the linker resolves every R_AARCH64_CALL26/JUMP26/ADR_PREL_PG_HI21/ADD_ABS_LO12_NC synth emits, places synth's .data (__synth_globals), binds the SHN_UNDEF import to the C definition — and the image is checked with pyelftools: ET_EXEC, EM_AARCH64, ELFOSABI_SYSV, 0 undefined symbols, 0 .rela sections left, all 28 synth symbols present;
4. execute the image and compare every printed value against a wasmtime instance that ran the same sequence with the same host import — 17 compares crossing every boundary: host→synth in w/x/d registers, synth→host through the import, synth→synth bl to a non-exported local, linear memory through x28 checked from both sides (synth stores, C reads base+16; C writes, synth loads), globals in synth's own .data persisting across calls, call_indirect through the emitted funcref table, a value below an import call's args (RQ-63-A64STACK), memory.size.

Three execution legs, because the host is arm64-Darwin and honesty about the substrate matters:

leg	where	what it is
unicorn	every run, every host	the Linux ELF-loader contract reproduced in ~30 lines (PT_LOAD at vaddr, bss zeroed, fresh stack, e_entry) + the two syscalls serviced
qemu-user	aarch64-oracle job (x86-64), REQUIRE_QEMU=1	an INDEPENDENT ELF loader + syscall implementation — not the oracle's own
native	NEW job arm64-linux-native on ubuntu-24.04-arm, REQUIRE_NATIVE=1	the thing itself: the linked image simply runs; no emulator anywhere; a non-arm64/non-Linux host is RED, never a skip

Each leg's stdout must be byte-identical to the unicorn leg's and match wasmtime. The native job is deliberately NOT a required check (a new runner pool must not be able to deadlock merges).

What it does NOT verify (written into the oracle, the doc, and the matrix row)

• Traps — every case is non-trapping on purpose: a WASM trap is brk #0 = SIGTRAP on Linux, which kills an unprepared process. Trap PLACEMENT stays gated by the sibling unicorn oracles; what the embedder does with SIGTRAP is its contract.
• Dynamic linking / PIE / libc — -static, freestanding. Every relocation synth emits is PC-relative so -pie is plausible; it is not claimed.

Red-first (measured)

Built into the oracle, run every time — each must be REFUSED by the linker with the linker's own words, exit != 0:

== host-linker refusals (red-first: broken inputs must be REFUSED by name) ==
  ok   EM_ARM (Thumb-2) object into -m aarch64linux: refused (exit 1), needle 'is incompatible with aarch64linux' present
  ok   aarch64 object into -m elf_x86_64: refused (exit 1), needle 'is incompatible with elf_x86_64' present
  ok   harness without a host_add definition: refused (exit 1), needle 'undefined symbol: host_add' present
== mutation control (can the differential fail?) ==
  FAIL [mutated] add -> 0xffffffff (wasmtime add: 0x7) — host -> synth, w-register args and result (AAPCS64)
  FAIL [mutated] add_wrap -> 0xfffffffe (wasmtime add_wrap: 0x0) — i32 wraps in the w view
  ok   flipped bit 30 of `add`'s first instruction (0x0b010009 -> 0x4b010009): mismatch reported

The mutation control flips one bit in the LINKED image (ADD-shifted-reg → SUB) and requires a reported mismatch — a check that cannot fail is not a check (#1113). Externally: pointing the oracle at a wrapper "synth" that ignores -b aarch64 and emits the EM_ARM object reddens it at its first gate (RED: synth compile failed/declined — the ARM path declines the fixture's f64 export and skips it; the oracle treats a skipping compiler as red before it ever links).

Green transcript (arm64-Darwin host, rebuilt binary):

executions: 17
host-linker refusals: 3
native-abi runs: 0            <- Darwin: native/qemu legs skipped here; CI requires them
co-link workaround runs: 1
mutation: detected
RESULT: PASS
ORACLE-EVIDENCE … mode=emulations floor=2 measured=3 emulations=3 wasmtime_calls=15 compiles=3 exit=0

The precondition, stated (the #1131 rule)

docs/embedder-abi-relocatable-aarch64.md — every fact cited to the emitting file:line, split fixed / chosen / incidental, pinned by SYNTH-EMBEDDER-ABI-RELOCATABLE-AARCH64-RQ64 (16 evidence items binding the doc's sentences to selector.rs/backend.rs/elf.rs/substrate.rs/main.rs/ci.yml):

• x28 = linear-memory (memory 0) base, set once before the first export; emitted code never writes it (LINMEM_BASE, selector.rs:181; the temp universe is x9..x15/v16..v23); anything called out to preserves it by AAPCS64. Two measured ways to keep it: -ffixed-x28 + set in startup (what the oracle runs), or a per-call asm trampoline. NOT from inline asm inside ordinary C.
• No size register, no globals register. The bounds limit is a baked immediate (MemBounds::Software { limit_bytes: config.linear_memory_bytes }, backend.rs:77-79) → the region at x28 must be ≥ initial_pages × 65536 bytes and nothing can say otherwise; memory.size is the declared constant, memory.grow is −1.
• Globals (__synth_globals, .data, initializers in the bytes) and the funcref table (__synth_func_table, .text) are EMITTED — not preconditions. Active data segments are REFUSED at compile time (backend.rs:259-275), so there is no --embedder-data-init promise on this path.
• Traps are brk #0 = SIGTRAP; --safety-bounds none removes the OOB trap entirely (compliance envelope).
• --target cortex-a53 is the only target; the object carries nothing OS-specific (EI_OSABI 0, no notes/PLT/GOT/TLS) — its "Linux-ness" is the SysV ELF64 container + AAPCS64, which is what ld.lld -m aarch64linux consumes. Only arm64-Linux is claimed, because that is what executes.

NEGATIVE FINDING (measured, pinned, documented — not fixed here)

Two independently compiled synth aarch64 objects cannot be linked into one program. aarch64 emits func_N GLOBAL (elf.rs:193, 0x12); ARM emits it LOCAL since #656 for exactly this reason.

ld.lld: error: duplicate symbol: func_1
>>> defined at synth.o:(func_1)
>>> defined at second.o:(g)

Not fixed in this lane: it changes symbol-table ordering (sh_info) in the ELF writer, and every aarch64 oracle's expectations should move with it under review. The workaround is executed by the oracle every run — llvm-objcopy --regex --localize-symbol='func_[0-9]+' on all but one object; co-link succeeds and all 17 values still match (the object's own intra-object relocations bind to the now-local symbols). The pin is bidirectional: the day the writer emits func_N LOCAL, count-eq on the 0x12 line and the oracle's pinned refusal both go red until the doc's collision section is removed.

Also in this PR

• The CLI's post-compile hint printed Link with: arm-none-eabi-ld … kiln_bridge.o for aarch64 objects too; it now names ld.lld -m aarch64linux and the x28 precondition (main.rs).
• FEATURE_MATRIX template row (aarch64) and README crate row carry the claim, the precondition and the limitation.
• .github/workflows/ci.yml: aarch64-oracle installs lld clang llvm qemu-user-static and runs the oracle with REQUIRE_QEMU=1 (--min-oracles 16 → 17); NEW arm64-linux-native job on ubuntu-24.04-arm (asserts uname -m = aarch64 first, REQUIRE_NATIVE=1, grep on the native leg's own ok line).
• --exact-emulation-floor 324845 → 324847 — RE-DERIVED by python3 scripts/oracle_wiring_check.py on the rebased tree (not added); SYNTH-ORACLE-CHECK-FLOORS-910-CI in lockstep.

Gates run locally (rebased onto 8862ee2f, the merged v0.64 plan)

• claim_check.py claims.yaml --emit-status → 60/60 claims hold
• oracle_wiring_check.py --exact-emulation-floor 324847 → exit 0 (189 scripts, 181 wired, 0 unwired)
• status_evidence_check.py → 0 failures (R7-SKIP on the uncommitted artifact only)
• rivet validate → 40 errors (main's baseline; the +24 warnings are plan(v0.64): scope the release — "The number you plan from" (9 artifacts, 4 carried) #1177's nine new artifacts)
• cargo fmt --check clean; cargo clippy --workspace --all-targets -- -D warnings exit 0; cargo test -p synth-cli green

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!