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

Merged

avrabe merged 3 commits into

main from

feat/arm64linux-1178

Sep 7, 2026

Merged

feat(aarch64): RQ-64-ARM64LINUX — the arm64-Linux host-library claim, linked by ld.lld and EXECUTED (natively, qemu-user, unicorn) vs wasmtime #1179
avrabe merged 3 commits into
main from
feat/arm64linux-1178

Conversation

@avrabe

@avrabe avrabe commented Sep 7, 2026

Copy link

ばつ 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 #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.com/claude-code) https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L " data-view-component="true"> Copy Markdown

Contributor

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:

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);
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);
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;
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

avrabe added a commit that referenced this pull request

Uh oh!

Conversation

@avrabe avrabe commented Sep 7, 2026

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

What the oracle links and executes

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

Red-first (measured)

The precondition, stated (the #1131 rule)

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

Also in this PR

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

Uh oh!

codecov Bot commented Sep 7, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

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