RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed by avrabe · Pull Request #959 · pulseengine/synth

avrabe · 2026-08-13T15:40:12Z

What this is

The RQ-57-SENTINEL deliverable from artifacts/release-v0.57.yaml: an audit of every size/count/address path where a NUMERIC SENTINEL stands in for absence — the mechanism behind #932 (v0.56.0) and #953 (v0.56.1), two security bugs one release apart with the same root cause in opposite directions.

The number (non-vacuity)

54 sites examined / 4 converted / 41 argued-(a) / 9 listed-(c) residuals.
Full per-site table with arguments: scripts/repro/sentinel_sweep_rq57.md.

Three latent defects found and fixed (the real prize — instances three, four, five of the mechanism)

1. SECURITY — ARM --safety-bounds mask + (memory 0) = unbounded OOB read/write.
arm_backend.rs exempted bytes == 0 from the mask power-of-two gate ("0 means unknown"). A (memory 0) module bakes startup R10 = 0, so the emitted guard SUB R12, R10, #1; AND addr, R12 computes 0 − 1 = 0xFFFFFFFF — an IDENTITY mask. Every access executed unmasked at [R11 + addr] for any 32-bit address, in the mode whose purpose is bounding. Verified pre-fix on v0.56.1 (exit 0, movw r10, #0x0 baked, AND-masked bodies). Zero-byte memory now REFUSES loudly — the same contract #953 gave rv32. This is #953's disease in a third backend-mode, and worse than the 64 KiB invention: no bound at all.

2. The single-function CLI path regressed under #953.
main.rs forced linear_memory_bytes: 0 for every backend except aarch64, on a comment (from #865) claiming the field was "never consumed" by ARM/RV32 — false for RV32, whose compile_function has always read it. When #953 deleted the rv32 64 KiB fallback, --func-index + --safety-bounds software on a (memory 1) module started compiling EVERY access to the zero-size ebreak fold (pre-fix: 00050293 00100073 at entry — a live availability miscompile in v0.56.1). The declared size now threads to ALL backends; byte-invisible where unconsumed (frozen anchors are --all-exports).

3. The #932 fix's own "unreachable by construction" comment was false.
The sweep's interim .expect() on the attestation's unwrap_or(0) panicked in one test run: attestations are ALSO emitted for REFUSED ingests (#901's refusal-is-attested rule), and the imported-memory refusal — #932's exact shape — reaches the flattened 0. Shipped v0.56.x refusal attestations recorded an invented "memory_min_bytes": 0. ElisionAttestation.memory_min_bytes is now Option<u32>; absence serializes as an explicit null (accepted-case JSON unchanged).

Also converted: NativeGlobalsLayout.sp_init (0-for-absent → Option<i32>; extent folds map None → 0 as the explicit max-identity, and --shadow-stack-size on a module with no SP global now refuses loudly instead of shrinking a phantom reservation).

The 9 (c)-residuals, listed not silent

Highest blast radius first (details + guardians in the sweep doc): imported-memory modules get linear_memory_bytes = 0 → silent always-trap compiles on rv32/aarch64 (fail-closed, but the "tell the caller" class — ties to the #932 decoder follow-up); the cortex-m image's initial_pages.unwrap_or(1); the emit_wasm_data && linear_memory_bytes > 0 region-skip; decoder type-table .get().unwrap_or(0) (guarded by wasmparser validation); validator_pattern arity; arm_backend param-table defaults (#518's mechanism, guarded by the CLI always populating); provenance/ELF-name diagnostic flatteners.

Red-first evidence

All three defects demonstrated on the pre-fix tree before conversion (transcripts in the sweep doc). New tests:

arm_safety_bounds_mask_zero_size_refused_rq57 (unit) + arm_mask_zero_memory_refused (CLI, end-to-end reachability)
rv32_single_func_software_uses_declared_bound + non-vacuity control rv32_single_func_zero_memory_stays_fail_closed (proves the fix threads the declared size rather than resurrecting a fallback — (memory 0) keeps the [SECURITY] rv32: (memory 0) gets a 65532-byte bounds guard — --safety-bounds software is a 64KB no-op for reads AND writes (aarch64 folds to brk) #953 ebreak fold)
no_floor_attests_null_not_zero_rq57 (attestation null, invented-0 unrepresentable)

Gates

cargo fmt --check clean; cargo clippy --workspace --all-targets -- -D warnings exit 0 (real exit code)
cargo test --workspace exit 0 (136 suites, 0 failures)
frozen_codegen_bytes 10/10 — the Option refactors moved no shipping bytes
Two pre-existing mask tests updated to STATE their size (linear_memory_bytes: 64 * 1024) — exactly what the [SECURITY] rv32: (memory 0) gets a 65532-byte bounds guard — --safety-bounds software is a 64KB no-op for reads AND writes (aarch64 folds to brk) #953 fix required of the rv32 driver test

Refs #953, #932

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… defects found and fixed Audit of every size/count/address path where a numeric sentinel stands in for absence (the #932/#953 disease), across synth-core, synth-backend, synth-backend-riscv, synth-backend-aarch64, synth-cli, synth-verify. 54 sites examined / 4 converted / 41 argued-(a) / 9 listed-(c) residuals. Full table: scripts/repro/sentinel_sweep_rq57.md TWO LATENT DEFECTS found by the sweep (the third and fourth instances of the mechanism, one release after #953): 1. SECURITY — ARM `--safety-bounds mask` exempted `bytes == 0` from the power-of-two gate ("0 means unknown"). A `(memory 0)` module compiled with startup R10 = 0, so the emitted guard `SUB R12, R10, #1; AND` computed an IDENTITY mask (0xFFFFFFFF): every access executed unmasked at [R11 + addr] — unbounded OOB read/write in the mode whose purpose is bounding. Verified pre-fix (exit 0, movw r10 #0 baked). Zero-byte memory now REFUSES loudly, same contract as #953 gave rv32. 2. The single-function CLI path forced `linear_memory_bytes: 0` for every backend but aarch64, on a comment claiming the field was never consumed there — FALSE for RV32, whose compile_function reads it for the bound. After #953 removed the rv32 fallback, `--func-index` + software bounds on a `(memory 1)` module compiled every access to the zero-size ebreak fold (verified pre-fix: 00050293 00100073 at entry). The declared size now threads to ALL backends; `(memory 0)` keeps the fail-closed fold (pinned by a control test). Also converted: the #932 attestation `unwrap_or(0)` (documented-unreachable → expect, so acceptance-rule drift panics instead of attesting an invented 0 B floor) and `NativeGlobalsLayout.sp_init` (0-for-absent → Option<i32>; the shadow-stack shrink now refuses "no SP global" loudly). Red-first: both defects demonstrated on the pre-fix tree (transcripts in the sweep doc); new tests arm_safety_bounds_mask_zero_size_refused_rq57 + sentinel_sweep_rq57.rs (3 CLI tests incl. the non-vacuity control). Refs #953, #932 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…— type the absence The sweep's interim `.expect()` disproved the #932-era "unreachable by construction" comment in one test run: attestations are also emitted for REFUSED ingests (#901's refusal-is-attested rule), and the imported-memory refusal — #932's exact shape — reached the flattened 0. Shipped v0.56.x refusal attestations therefore recorded an invented `"memory_min_bytes": 0`. `ElisionAttestation.memory_min_bytes` is now `Option<u32>`; absence serializes as an explicit `null` (pinned by no_floor_attests_null_not_zero_rq57; the accepted-case JSON shape is unchanged — Some(x) is the bare number, proven_safe_bounds_901 still asserts 65536). Third latent defect found by this sweep. Refs #953, #932 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…lure) CI red on `Test`; the lane's local run was green. Both new assertions failed with `words: []` — an EMPTY word list, not a wrong one. Cause: the helper parsed `synth disasm` OUTPUT. The disassembler decodes with whatever target it defaults to and its rendering is host-dependent, so the parser matched on macOS and matched nothing on the ubuntu runner. This is #850, already recorded in this repo — and it is the SECOND time this exact trap has landed in a test I am responsible for: v0.56's #932 fixture counted `udf` mnemonics from `synth disasm`, passed on macOS, and returned 0 on ubuntu. Same mechanism, same month. Now reads the ELF `.text` SECTION BYTES via `object::{Object, ObjectSection}` (already a dev-dependency) and formats 4-byte little-endian words. That is host-independent BY CONSTRUCTION rather than by luck: synth is a cross-compiler and `.text` is a pure function of (wasm, flags) — the same property `frozen_codegen_bytes` relies on, which is why THAT test passes in CI while this one did not. The assertions are unchanged and still match the same encodings (`00010337` = lui t1,0x10 and `ffc30313` = addi t1,t1,-4), so the lane's red-first evidence still stands; only the reading mechanism moved. cargo test -p synth-cli --test sentinel_sweep_rq57 -> 3 passed, 0 failed Refs #953, #850

codecov · 2026-08-13T16:08:33Z

Codecov Report

❌ Patch coverage is 98.90110% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	96.96%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

Pulls four merged commits forward into a patch release because the first is a live vulnerability in a shipped version: #959 ARM --safety-bounds mask emitted an IDENTITY mask on (memory 0) #961 thumb-2 branch target could land mid-instruction (#930) #962 I64Const/I64Ldr/I64Str unpriced in the WCET model (#936) #958 synth verify covers i32.const + reports the decline denominator The ARM mask bug is the headline. The mask path exempted `bytes == 0` from its power-of-two gate, so `(memory 0)` compiled with exit 0 and `movw r10, #0x0`. The guard computes `R10 - 1`, and `0 - 1` is `0xFFFFFFFF` — a mask that masks nothing, in the mode whose whole purpose is to bound accesses. Unbounded OOB read AND write. It is the same sentinel/value collision as #953 one release earlier, running the other way: there `0` meant "unset" and INVENTED a 64 KiB bound, here `0` meant "no bound needed" and ERASED the real one. That is why the fix landed as a sweep of the collision class (54 sites, 4 converted, 3 latent defects) and not another point patch — the v0.53 finding was that we keep fixing instances rather than mechanisms. Release surfaces, all four swept to 0.56.2 and checker-confirmed: Cargo.toml [workspace.package] + 10 path-dep version= pins MODULE.bazel, npm/package.json, Cargo.lock (cargo metadata) scripts/check_version_pins.py: OK on all four Derived artifacts regenerated (--emit-status): artifacts/status.json, docs/status/FEATURE_MATRIX.md. Claim gate: 43/43. SCOPE MOVE, logged not silent: RQ-57-SENTINEL, RQ-57-BRTARGET, RQ-57-WCET2OPS, RQ-57-I32CONST and RQ-57-RULEINV were planned for v0.57 and are re-tagged release: v0.56.2 / status: implemented. SENTINEL carried the security fix and the other four were already merged on main, so a tag excluding them did not exist. rivet error/warning counts are unchanged by the move (50/164 before and after — pre-existing, unrelated to these artifacts). Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

… (RQ-57-MCDC) (#978) * feat(#912): MC/DC structural coverage over synth's own decision logic RQ-57-MCDC. #912 sat N/A for six releases on a surface argument: `witness` measures MC/DC on a Wasm artifact and synth emits ARM/RV32/A64 machine code, so "run witness on synth's output" is a category error. That is true about synth's OUTPUT and irrelevant — the decisions that ship a miscompile are in synth's own Rust, and those compile to Wasm fine. SURFACE, chosen on evidence (scripts/repro/mcdc_912_gate.md): * REJECTED native LLVM MC/DC — not a preference, the capability was REMOVED from rustc (rust-lang/rust#144999, merged 2025-08-08, Rust 1.91). Probed on three nightlies: `mcdc` is rejected, only `block|branch|condition` accepted. `condition` is the trap in the family — it builds, and it emits ZERO `llvm.instrprof.mcdc.*` intrinsics and zero mcdc_records. * REJECTED witness-over-the-fixtures-synth-compiles — it measures the fixture. gale's run named `pad_integral`, `do_count_chars`, `<u64 as Display>::fmt`, `write_prefix`, `cabi_realloc` and ZERO synth functions. A surface whose gap rows cannot name a synth decision cannot notice a missing condition in one. * CHOSEN witness over a wasm32-wasip1 build of synth's OWN crates. `synth-mcdc-harness` is a thin row driver — it calls the REAL pub fns with inputs arriving through Wasm params; it re-implements no predicate. THE RIGHT PARTS — scored where a missed condition HAS shipped a bug here: static_data_addr (VCR-VER-003 #777/#757/#798), alloc_validator (VCR-RA-003 #815; #871's fix WAS a condition added to the save-set predicate), and the RV32 bounds gate (#953/#959 — `mem_size == 0` was exempt from the power-of-two check, so `(memory 0)` emitted an identity mask and every access ran unmasked). EXCLUDED and named: instruction_selector (225 operator lines, its own lane); the aarch64 bounds closures (#865 — residual); wcet declines (match-dispatch, 1 operator line in 1061, so MC/DC has nothing to say there). MEASURED 20 decisions / 144 conditions / 63 proved / 31 gap / 50 dead, 3 at full MC/DC. Identical under witness 0.28.0 and 0.42.0. Gap rows are PRINTED with the closing vector — `is_ret` went 3-gap to 0-gap by adding exactly the three vectors witness named. THE GATE SCORES BY FUNCTION AND FLOORS COUNTS, for three reasons: the module-wide figure is 3/770 because wasip1 links wasi-libc + std; witness's `source_file` is an inlined-DWARF BASENAME and misattributes (resolve_owner's decision reports as static_data_addr.rs:355, it is at :274 — witness#179); and a ratio cannot notice a DELETED condition, which makes the percentage improve. RED-FIRST, two mutations, two distinct failure paths, both restored byte-identical: (a) delete `|| rs2 == Reg::RA` (the #871 fix) -> 19/142/54/2, all four floors trip; the condition-COUNT drop is what a ratio cannot produce. (b) drop one truth-table row (ra_validate:14) -> conditions stay 144, proved 63->62 and fully-proved 3->2. Wired as the `mcdc-structural-coverage` CI job, witness pinned to v0.42.0, with a non-vacuity assert so an empty scored table cannot print PASS. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#912): CI mode-126 on mcdc_run.sh, pin the toolchain, ceiling the dead count Three fixes from the first CI run and the cold read of it: 1. exit 126. `scripts/` is mode 644 in this repo (cf. scripts/oracle_run.py), so `./scripts/mcdc_run.sh` cannot exec on a fresh checkout even though it runs locally after a chmod. Invoke through `bash`, matching how every other script in this workflow is called. 2. PIN the toolchain to 1.96.1. The floors are counts of decisions and conditions RECONSTRUCTED FROM LOWERED WASM, so they are sensitive to how `std` inlines. `@stable` is a moving target and a Rust release could red this gate with no code change. Bumping the pin is allowed and obliges a RE-MEASURE, not a lowering. (Witness-version invariance — 0.28 = 0.42 — is evidence about witness, not about rustc; it does not transfer.) 3. CEILING the dead count at the measured 50. 50 of 144 scored conditions are never evaluated (40 in `is_straight_line`, whose match arms cover RV32 opcodes the row set does not construct). That residual was the one number in the table nothing guarded: a change that stopped reaching the segment barriers would raise `dead`, lower nothing else, and PASS. It is also a third potency surface — mutation (a) moves dead 50 -> 52, so the mutated run now trips five floors instead of four. Also trims the `sd_resolve_owner` doc comment, which claimed vectors the measurement does not show: its 2 gap conditions are now stated as a measured residual rather than implied closed. Baseline re-verified unchanged: 20 / 3 / 144 / 63 / 31 / 50, PASS. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * TEMPORARY red-first probe (#912) — DO NOT MERGE THIS COMMIT Reverted by the very next commit. Two things in one CI run: 1. RE-MEASURE the floors on the platform the gate actually runs on. The first CI run proved what could only be argued locally: these counts are PLATFORM-dependent, not just toolchain-version dependent. ubuntu x86_64, rustc 1.96.1, witness 0.42.0: 22 / 130 / 57 / 23 gap / 50 dead, 4 full macOS aarch64, rustc 1.96.1, witness 0.42.0: 20 / 144 / 63 / 31 gap / 50 dead, 3 full Same toolchain version, same witness, same 56 rows, different host. `validate_final_allocation_rv32` presents as 9 decisions / 44 conditions on Linux and 4 / 43 on macOS; `ensure_supported_target` vanishes on Linux. Floors move to the CI numbers — RE-MEASURED, not lowered to fit. Both baselines are recorded in the script so the macOS delta is a stated fact rather than a surprise. 2. RE-PROVE POTENCY ON THAT PLATFORM. The local mutation evidence does NOT obviously transfer when the same function presents as 9 decisions instead of 4 — and "it obviously still works" is the reasoning this whole lane exists to distrust. So this commit ALSO deletes the #871 condition `|| rs2 == Reg::RA` from the RV32 allocation validator's save-set predicate. The MC/DC job must go RED on the condition-COUNT floor, and the VCR-RA-003 RV32 job should go red independently. If this commit is green, the gate is vacuous and the lane is wrong. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * TEMPORARY red-first probe 2/2 (#912) — DO NOT MERGE, reverted next commit Probe 1 (25a9195) went RED on CI as required, but at the WRONG STEP for the evidence I wanted: the row-driver sanity gate (step 7) asserts `ra_validate(4) == 1` (#871: unsaved ra must be a violation), so deleting `|| rs2 == Reg::RA` fails there and the MC/DC measurement never runs. Two independent gates catching one mutation is good engineering and useless as proof that the MC/DC FLOORS bite. This probe isolates them. It restores the source byte-identical (verified: empty `git diff` vs the pre-mutation tree) and instead drops ONE truth-table row — `ra_validate:14`, the non-sp `Lw` that gives `sp_slot_load` its unique-cause pair. That touches no compiler behaviour, so: step 7 (row-driver sanity) must PASS step 8 (witness run) must PASS step 9 (MC/DC floors) must FAIL on and Conditions must stay at 130 — coverage lost, nothing deleted. That is the second of the two potency paths, and the one that proves the SCORING floor itself is what goes red, on the platform it actually runs on. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#912): restore the probes, record the CI-platform potency evidence Both red-first probes reverted; the tree is byte-identical to 712f658 for crates/synth-backend-riscv/src/alloc_validator.rs and scripts/mcdc_run.sh (verified with an empty \$(git diff 712f658 -- <path>) on each). What the two CI probes established, which the local run could not: PROBE 1 (delete the #871 condition) went RED — at the WRONG STEP. The job's own row-driver sanity gate asserts ra_validate(4) == 1 and fails there, so the MC/DC measurement never ran; the VCR-RA-003 RV32 job went red independently too. Three gates catching one mutation is good engineering and NO evidence that the MC/DC floors bite. Recording it because 'a red gate is not evidence that the gate you were testing works' generalises well past this lane — read WHICH STEP failed. PROBE 2 (drop one truth-table row, no compiler behaviour touched) isolated them. Run 31821746035: sanity gate PASS, witness run PASS, SCORING STEP FAIL. baseline 22 4 130 57 23 50 probe 2 22 3 130 56 24 50 FAIL: proved conditions 56 < floor 57 FAIL: fully-proved decisions 3 < floor 4 Decisions unchanged, CONDITIONS UNCHANGED at 130 — nothing deleted — while proved fell and a decision dropped out of full MC/DC. That is the signature of coverage lost with structure intact, produced by the MC/DC scoring step itself, on the platform the gate blocks on. Refs #912 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…place; sweep the class, not the instance The previous commit fixed `"$(brew --prefix llvm)/bin/ld.lld"` in the job's ASSERTION step and left the identical expression in the step that actually runs the oracle: SYNTH=./target/debug/synth REQUIRE_NATIVE=1 LLD="$(brew --prefix llvm)/bin/ld.lld" So the assertion went green and the oracle then failed one step later — `LLD` pointed at a binary that does not exist, the ld.lld reverse-refusal probe did not run, `host-linker refusals` came back 2 instead of 3, and the step's grep failed. Fixing the instance instead of the class is the v0.56 lesson (#932/#953/#959, where the same sentinel bug was patched three releases running before anyone swept all 54 sites). SWEPT, and the sweep found one more use that is CORRECT and is deliberately left alone: `OBJCOPY="$(brew --prefix llvm)/bin/llvm-objcopy"` in `aarch64-native-matrix`. Measured on an arm64 Darwin host with llvm 22.1.8 installed — the llvm formula ships `llvm-objcopy` and `clang` but NOT `ld.lld`, which lives in the separate `lld` formula. So the pattern is not uniformly wrong and a blanket replace would have been its own defect. Fix: drop the LLD override entirely. `brew install lld` (previous commit) puts `ld.lld` on PATH, which is where the differential's `find_tool` looks by default. VERIFIED by reproducing the CI invocation locally on arm64 Darwin, with no LLD override, exactly as CI will now run it: byte-identical modules: 141 acceptance disagreements: 0 identity mutation: detected executions: 17 host-linker refusals: 3 native-abi runs: 1 mutation: detected RESULT: PASS The run also answers a question #1180 left open: two synth Mach-O objects DO collide on `_func_1` exactly as the ELF pair does, so the `func_N` STB_GLOBAL shape is shared across containers rather than ELF-specific. The oracle pins that as a limitation rather than asserting the opposite. ci.yml parses at 59 jobs. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…lan, linked by Apple ld and EXECUTED on macOS (#1184) * test(aarch64): RQ-64-MACHO oracle lands RED-FIRST — ELF/Mach-O byte-identity sweep + macOS host-link execution differential, before any writer exists The oracle, then the writer — the gating rule this artifact was deferred from v0.63 to honour. `scripts/repro/macho_host_link_rq64_differential.py` follows #1179's shape (one case table generating both the C harness and the wasmtime sequence, wasmtime-first, red-first controls built in) and adds the increment this artifact is actually about: * BYTE IDENTITY on every host: `.text` == `__TEXT,__text`, `.data` == `__DATA,__data`, symbols map 1:1 under the Darwin `_` prefix, and the relocation SET maps 1:1 under CALL26/JUMP26 -> BRANCH26, PG_HI21 -> PAGE21, LO12 -> PAGEOFF12 — for the fixture AND every repo `.wat` the backend accepts (139 today), with acceptance required to AGREE across containers. The Mach-O is read by the file's own ~60-line parser so the leg runs on the Linux runner too. * an identity MUTATION control (bit 30 of `add`'s first word flipped in `__text` must be reported); * on arm64-Darwin (REQUIRE_NATIVE=1 makes any other host RED, never a skip): clang -arch arm64 -ffixed-x28 + an x28 shim, linked by Apple ld through the clang driver, checked by Apple nm, EXECUTED natively vs wasmtime; the ELF twin handed to Apple ld must be refused `unknown file type` (measured), a missing `_host_add` refused by name, ld.lld must refuse the Mach-O when present, the mutated object linked and run must mismatch, and the #1180 `_func_1` co-link collision is pinned. Measured RED against the flagless binary: exit 1, `unexpected argument '--object-format'`, driver floor `compiles >= 100` unmet (measured 2). The fixture is byte-for-byte #1179's module below its header (verified by diff), so the same bytes' values on arm64-Linux and macOS read side by side. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * refactor(aarch64): RQ-64-MACHO — one ObjectPlan behind the ELF writer, so a second container cannot disagree with it (140/140 objects byte-identical) `plan_object` now computes everything a relocatable object SAYS — the concatenated `.text`, the `.data` image, the symbol list in emission order (function aliases, `.data` symbols, the #1017 referenced externals; first occurrence wins on a duplicated name), and the resolved relocations with the #1013 unplaced-symbol refusal, message verbatim — and `build_relocatable_object_full` only lays ELF around it. The Mach-O writer that follows consumes the SAME plan, which is what makes `.text` identity between the two containers a property of one function rather than of two writers happening to agree (the North Star's "derive what you check against from the artifact you ship"; a hand-copied symbol-ordering rule in a second writer would be the mirror it forbids). Gated as a pure refactor: every one of the 140 repo `.wat` modules the aarch64 backend accepts (`scripts/repro/*.wat` + `tests/**/*.wat`) compiles to bytes IDENTICAL to the pre-refactor binary (corpus captured before, compared after: accepted=140 identical=140 differ=0), and the crate's 156 unit tests — including the layout-pinning ELF tests — pass unchanged. The `let info = if f.is_object { 0x11 } else { 0x12 };` line #1179's claim pin counts is kept verbatim. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(aarch64): RQ-64-MACHO — `--object-format macho` emits a CPU_TYPE_ARM64 MH_OBJECT over the ELF plan; Apple ld links it and macOS EXECUTES it 17/17 vs wasmtime The container was the blocker, not the ISA — now measured rather than argued. `crates/synth-backend-aarch64/src/macho.rs` lays Mach-O around the SAME `ObjectPlan` the ELF writer consumes (the previous commit): one unnamed LC_SEGMENT_64 with `__TEXT,__text` (+ `__DATA,__data` when the module has globals, file offsets congruent with addresses), LC_BUILD_VERSION (macOS, minos 11.0 — the one macOS-specific fact), LC_SYMTAB + LC_DYSYMTAB with every symbol N_EXT under Darwin's `_` prefix, and one `__text` relocation per planned relocation, all r_extern/r_length 2: CALL26/JUMP26 -> ARM64_RELOC_BRANCH26, ADR_PREL_PG_HI21 -> PAGE21, ADD_ABS_LO12_NC -> PAGEOFF12 (addends are zero in both containers, so no ADDEND entry is ever needed; any other kind fails loudly, the ELF rule). MH_SUBSECTIONS_VIA_SYMBOLS is deliberately NOT set so `__text` stays one atom with exactly the ELF layout. The flag is EXPLICIT and narrow: `--object-format {elf,macho}`, default `elf` (every pre-v0.64 compile byte-identical — the ELF path was corpus-diffed 140/140 in the previous commit), and `macho` is REFUSED on any backend but `-b aarch64` rather than silently emitting ELF under a flag that says otherwise. `build_aarch64_object` in synth-cli is the one place the container is chosen; both the single-function and `--all-exports` paths route through it. The post-compile hint names the toolchain the oracle actually exercised. MEASURED, by the red-first oracle from two commits ago, now green (`SYNTH=… python scripts/oracle_run.py scripts/repro/macho_host_link_rq64_differential.py`, arm64 macOS 26.6, Apple ld-1267, clang 21): * byte identity: `.text == __text` (580 B), `.data == __data`, 29 symbols and 20 relocations map 1:1 for the fixture; 139/139 corpus modules byte-identical, 0 acceptance disagreements (140 in all); * identity mutation control: a flipped bit in `__text` is reported; * Apple ld links the object with NO warnings; nm sees all 32 wanted symbols, `_host_add` bound to the C definition; * EXECUTED natively: 17/17 values match wasmtime (w/x/d registers, x28 memory from both sides, globals persisting in __DATA, call_indirect via BRANCH26 trampolines, import call, RQ-63-A64STACK shape); * refusals by name: the ELF twin into Apple ld (`unknown file type`), a missing `_host_add`, the Mach-O into ld.lld (`unknown file type`); * execution mutation control: the mutated object linked and run mismatches (add -> 0xffffffff vs 0x7); * #1180 pinned: two Mach-O objects collide `duplicate symbol '_func_1'` exactly as ELF does — noted, not fixed here; * driver floor compiles >= 100, measured 387. Six unit tests in macho.rs pin the header/sections/build-version, the symbol prefix + defined-then-undefined partition, the kind-for-kind reloc packing, `.text`/`.data` identity with the ELF writer, the no-globals single-section shape, and the shared #1013 refusal. Refs #242, #1180 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(aarch64): RQ-64-MACHO — clippy -D warnings clean (needless borrow, is_multiple_of, test type alias); ELF corpus still 140/140 identical Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(ci): RQ-64-MACHO (#242) — wire the byte-identity sweep and the native arm64-macOS host-link oracle, so the container claim is GATED Re-applied against main's ci.yml after #1179 landed. The first attempt was dropped in the rebase: git's conflict boundary fell THROUGH a cache step rather than between jobs, so a mechanical "keep both sides" produced invalid YAML with an orphaned `key:` line. Re-applied surgically instead — the new step, the ledger bump and the new job placed individually, then the file parsed (59 jobs) rather than assumed correct. - byte-identity sweep, as a step in `aarch64-oracle`: for the fixture and every `.wat` the aarch64 backend accepts, BOTH containers are emitted and `.text`/`.data`, the symbols (under Darwin's `_`) and the relocation SET must be identical, with the acceptance decision agreeing. This is the host-independent half of the artifact's thesis — that the container, not the ISA, is what blocks shipping synth output as a host library — and it needs no linker and no execution to prove it. - `macho-host-link-native` on `macos-latest`: asserts the runner really is arm64 macOS, links with Apple ld and EXECUTES against wasmtime-first values. REQUIRE_NATIVE=1, so a wrong host is RED, never a silent skip. Not a required check, per the #1179 precedent: a new runner pool that GitHub cannot schedule would deadlock every merge. CUMULATIVE COUNTERS RE-DERIVED ON THE MERGED TREE, never carried textually: `--min-oracles` in aarch64-oracle is 17 on main because #1179 already bumped 16->17, so this makes it 18 — copying the pre-rebase value would have silently un-gated one oracle. The emulation floor is UNCHANGED at 324847 and that is correct, not an oversight: the Mach-O differential declares `compiles >= 100`, so the compiles bucket moves 9 scripts/43 to 10/143 while emulations does not. oracle_wiring reports 190 scripts, 182 wired, 0 unwired debt. SYNTH-SUBTRACTION-MIRRORS: 59 -> 60 with a waiver, NOT a loosened gate. Both new files say "mirror" only to state that they are not one — elf.rs explains that a second hand-written copy of the symbol-ordering rules "would be exactly the mirror the North Star forbids" (the reason ObjectPlan exists), and the differential explains that "a hand-mirrored pair would drift" (why it generates the C harness and the wasmtime sequence from one case table). Rewording to dodge the word count would delete the explanation and leave the metric happy. Verified: claim_check 60/60, oracle_wiring exit 0 at the pinned floor, status_evidence exit 0, ci.yml parses, rivet at main's 40-error baseline. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(release): RQ-64-MACHO (#242) — flip to implemented, with provenance split between lane and coordinator The lane was terminated mid-step by an API session limit; the coordinator finished the rebase and the CI wiring. The verified-by says which claims come from which, and marks the macOS 17/17 execution as the lane's measurement for CI to confirm rather than restating it as though re-run here. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(release): RQ-64-MACHO (#242) — record PR #1184 in the artifact's landed: (R10 attribution) Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(ci): RQ-64-MACHO (#242) — the macOS oracle's own precondition named a path that never exists The `Mach-O host-link oracle, NATIVE arm64-macOS` job went RED at its FIRST assertion, before running the oracle at all. The defect is in the wiring I added in this PR, not in the lane's differential. "$(brew --prefix llvm)/bin/ld.lld" --version Two things wrong at once, and each hides the other: - `brew --prefix llvm` prints a path whether or not the formula is installed, so the expression always LOOKS resolvable. - brew's `llvm` formula does not ship `ld.lld` at all. The separate `lld` formula does. Measured on an arm64 Darwin host with llvm 22.1.8 and lld 22.1.8 both installed: `/opt/homebrew/opt/llvm/bin/ld.lld` is ABSENT, `/opt/homebrew/opt/lld/bin/ld.lld` is present and symlinked onto PATH. So the step installed the wrong formula and then checked a path that formula would not have created either way. Fixed: install `lld`, and assert via `command -v ld.lld` + `ld.lld --version` rather than a reconstructed prefix. The assertion still REQUIRES the tool rather than probing for it — the differential itself skips its ld.lld reverse-refusal control when the tool is missing, and a skipped red-first control is exactly the silent-skip class this repo keeps finding. We control this runner, so absence is an error and the control stays non-vacuous. Verified: the corrected assertion runs green on an arm64 Darwin host (`uname -m` arm64, `uname -s` Darwin, `command -v ld.lld` resolves, `ld.lld --version` prints LLD 21.0.0); ci.yml parses at 59 jobs. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(ci): RQ-64-MACHO (#242) — the SAME bad brew path was in a second place; sweep the class, not the instance The previous commit fixed `"$(brew --prefix llvm)/bin/ld.lld"` in the job's ASSERTION step and left the identical expression in the step that actually runs the oracle: SYNTH=./target/debug/synth REQUIRE_NATIVE=1 LLD="$(brew --prefix llvm)/bin/ld.lld" So the assertion went green and the oracle then failed one step later — `LLD` pointed at a binary that does not exist, the ld.lld reverse-refusal probe did not run, `host-linker refusals` came back 2 instead of 3, and the step's grep failed. Fixing the instance instead of the class is the v0.56 lesson (#932/#953/#959, where the same sentinel bug was patched three releases running before anyone swept all 54 sites). SWEPT, and the sweep found one more use that is CORRECT and is deliberately left alone: `OBJCOPY="$(brew --prefix llvm)/bin/llvm-objcopy"` in `aarch64-native-matrix`. Measured on an arm64 Darwin host with llvm 22.1.8 installed — the llvm formula ships `llvm-objcopy` and `clang` but NOT `ld.lld`, which lives in the separate `lld` formula. So the pattern is not uniformly wrong and a blanket replace would have been its own defect. Fix: drop the LLD override entirely. `brew install lld` (previous commit) puts `ld.lld` on PATH, which is where the differential's `find_tool` looks by default. VERIFIED by reproducing the CI invocation locally on arm64 Darwin, with no LLD override, exactly as CI will now run it: byte-identical modules: 141 acceptance disagreements: 0 identity mutation: detected executions: 17 host-linker refusals: 3 native-abi runs: 1 mutation: detected RESULT: PASS The run also answers a question #1180 left open: two synth Mach-O objects DO collide on `_func_1` exactly as the ELF pair does, so the `func_N` STB_GLOBAL shape is shared across containers rather than ELF-specific. The oracle pins that as a limitation rather than asserting the opposite. ci.yml parses at 59 jobs. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(repro): RQ-64-MACHO (#242) — list the Mach-O host-link fixture on the ARM sweep's EXPECTED_DECLINES Same shape and same cause as its arm64-Linux sibling in #1179. The ARM corpus sweep compiles EVERY `.wat` under scripts/repro for ARM Thumb-2, and this PR adds an aarch64 fixture carrying an `f64_scale` export. On the ARM default target that hits GI-FPU-002 phase 2 (scalar f64 requires a double-precision FPU), so `--all-exports` would ship a partial object and synth correctly REFUSES under #952. Not a regression — the gate noticing a new fixture with no expectation. Measured against the branch binary at `--target cortex-m4`, not inferred: warning: skipping function 'f64_scale': ... GI-FPU-002 phase 2: scalar f64 requires a double-precision FPU Error: #952: 1 of 12 requested export(s) were skipped ... f64_scale The sweep's RATCHET arm reddens if an EXPECTED_DECLINES entry ever starts compiling, so the entry cannot rot silently — which is why this is the right mechanism rather than excluding the file from the sweep. Verified on the rebased tree: `#973 ARM CORPUS SWEEP: PASS` (compiled 158/177, executed 2526/2526, mismatches 0), oracle_wiring exit 0 at the pinned floor 324847 with 190 scripts / 183 wired / 0 unwired debt, claim_check 60/60, status_evidence exit 0, ci.yml parses at 59 jobs, rivet at main's 40-error baseline. Refs #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

avrabe and others added 3 commits August 13, 2026 17:29

avrabe merged commit 8b4808b into main Aug 13, 2026
58 checks passed

avrabe deleted the feat/sentinel-sweep-953 branch August 13, 2026 16:57

avrabe mentioned this pull request Aug 13, 2026

chore(release): v0.56.2 — security + soundness patch #964

Merged

avrabe mentioned this pull request Aug 21, 2026

plan(v0.59): add RQ-59-POPCNT (#1021) and RQ-59-TIERCENSUS — a proof sitting above a defective expansion #1030

Merged

Navigation Menu

Repository navigation

RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed - #959

RQ-57-SENTINEL: sentinel/value-collision sweep — 54 sites, 4 converted, 3 latent defects fixed#959
avrabe merged 3 commits into
mainfrom
feat/sentinel-sweep-953

avrabe commented Aug 13, 2026

Uh oh!

codecov Bot commented Aug 13, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

avrabe commented Aug 13, 2026

What this is

The number (non-vacuity)

Three latent defects found and fixed (the real prize — instances three, four, five of the mechanism)

The 9 (c)-residuals, listed not silent

Red-first evidence

Gates

Uh oh!

codecov Bot commented Aug 13, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant