From 096b2a43d470c5e6c53caf8730bf3632b4d6c109 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 8 Sep 2026 20:59:34 +0200 Subject: [PATCH 1/2] fix: the off-pin detector judged a PATH STRING, so the pinned binary was declared a candidate differential (AFD-115) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Clean-room verification of AFD-113/AFD-114. Every substantive claim in both CONFIRMED — six artifacts byte-identical across the pin bump, the #1189 signature, the silicon result, gale-nano's import/export asymmetry — and neither finding overstated scope. What the audit found was in the MACHINERY, again. 1. THE OFF-PIN DETECTOR JUDGED A PATH STRING, CONTRADICTING ITS OWN COMMENT. cascade-invoke/build.sh used `[ "$SYNTH" = "$SCRATCH/synthpin/synth" ]`, an absolute-path compare. Invoking the GENUINELY PINNED binary by a relative path — what a local run types, and what AFD-114's own verification used — took the off-pin branch, announced a CANDIDATE differential for an on-pin build, and made REQUIRE_ON_PIN=1 FAIL on the correct binary. Six lines above, the meld/loom comment already says why: "judge by DIGEST ... otherwise every CI run would announce itself as a candidate differential and the banner would stop meaning anything." announce_tool does it right; the synth branch bypassed it. CI escaped by accident (ci.yml omits SYNTH, so the default absolute path string-matched). Now a digest comparison; verified both ways. 2. A VACUOUS AGREEMENT CLAIM I INTRODUCED YESTERDAY. AFD-114 removed ci.yml's SYNTH_VERSION as accretion; check-drift greps for that literal, so synth and loom now read `-` in the CI column — while the summary still said "ci.yml and the varve pin agree" and "every tool compared (5)". No such comparison happened for those two. Now counts only where BOTH are declared and NAMES the uncompared tools. Blocking class re-verified potent. 3. THE #1189 EVIDENCE COULD NOT BE RE-RUN. The load-bearing "the control fires" half existed only as prose. tools/lowering/joinalias/ commits the module and asserts the property directly on the pinned synth. Potent both ways: PASS on 0.64.0 (adds r4, r2, r0), FAIL on 0.60.0 (adds r3, r0, r0). Wired into CI. 4. THREE FIXES IN THE GALE-NANO HARNESS. (a) the seam check asserted membership, not exclusivity. Writing the exact-set assertion surfaced a real subtlety: nm lists all SIX as undefined even after aliasing, because --redefine-sym renames the DEFINITION to the imported name so the object carries both T and U. The raw U list is NOT the obligation. Now compares UNRESOLVED = undefined MINUS defined; breaking an alias is refused. (b) the gale-nano digest was hardcoded — a second copy of a value that also lives in artifacts.pins with nothing enforcing agreement, the drifted-mirror shape AFD-104 deleted a registry for. Now read from the pins file. (c) run-on-silicon.sh printed handle and exec_state but never asserted them, so the exec_state==1 that localises the fault to poll-round was eyeballed. Both asserted now; re-run on silicon, result unchanged. Also corrected in AFD-113/114 themselves: "8/8 assertions" (the oracle emits no such count), citing jess's OWN WIT comment as the record for handle 0 (circular — the fact is measured, the citation was not evidence), and "16 references" where the count is 20. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 9 ++ artifacts/findings.yaml | 103 +++++++++++++++++- hardware/renode/cascade-invoke/build.sh | 23 +++- hardware/silicon/f100-gale-nano/build.sh | 33 +++++- .../silicon/f100-gale-nano/run-on-silicon.sh | 13 ++- hardware/silicon/f100-gust-hal/README.md | 5 +- hardware/silicon/f100-init/README.md | 4 +- tools/lowering/joinalias/check.sh | 43 ++++++++ tools/lowering/joinalias/joinalias.wat | 20 ++++ tools/lowering/m4-matrix.sh | 2 +- tools/varve/check-drift.sh | 25 ++++- 11 files changed, 254 insertions(+), 26 deletions(-) create mode 100755 tools/lowering/joinalias/check.sh create mode 100644 tools/lowering/joinalias/joinalias.wat diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0a6fb13..c394507 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -513,6 +513,15 @@ jobs: echo "a NO-OP apply loop PASSED the check — it can no longer detect non-consumption"; exit 1 fi echo "negative control OK: a gutted apply loop is refused" + # synth#1189 (AFD-114). The pin was bumped on the strength of a two-binary differential + # whose evidence lived only as prose in a findings file — nothing could re-run it. + # This asserts the property directly on the pinned synth: the if/else join must not + # alias a param's home register. Potency verified both ways (passes on 0.64.0, fails + # on 0.60.0 with `adds r3, r0, r0`). + - name: lowering — synth#1189 join-alias signature is absent from the pinned synth + run: tools/lowering/joinalias/check.sh + env: + SYNTH: .scratch/synthpin/synth # H3 first half (AFD-109). gust:hal read32/write32 as REAL MMIO. CI builds and gates # the image and asserts the SEAM exists; the silicon leg needs an ST-Link and is # hand-run against the bench (see hardware/silicon/f100-gust-hal/README.md). diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index dd4d73f..899e742 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -6347,13 +6347,19 @@ artifacts: no admit (negative control) 00000000 deadbeef deadbeef c0ffee00 GALE'S CODE RUNS ON THE PART, and exec_admit WORKS: gale's OWN view, exec_state(handle), returns 1 — exactly what TEST-PIX-035 asserts ("admitted task starts in state 1"). - handle == 0 is CORRECT, not a failure: jess already recorded that gale-nano hands out - handle 0 (app/gust-dispatch-probe's WIT says so, which is why its never-called sentinel is - 0xFFFFFFFF). + handle == 0 is CORRECT, not a failure — MEASURED, not cited: the wasmtime reference's own + `admitted-handle()` returns 0 in the same run. + CORRECTION (clean-room): this first said "jess already recorded that gale-nano hands out + handle 0 (app/gust-dispatch-probe's WIT says so)". That WIT comment is jess's OWN authored + prose, so citing it as the record was circular — it is a restatement of the belief, not + evidence for it. The fact is independently measured; only the citation was wrong. + CORRECTION (clean-room): the "8/8 assertions" figure above was removed. tools/dispatch/run.sh + emits no assertion count at all — it prints a Result: PASS line and its measurement rows. + "exit 0" and "green" were true; "8/8" was a precision the cited oracle does not produce. *** THE DIVERGENCE *** exec_poll_round reaches poll-task ZERO times on silicon. The wasmtime reference was re-run - GREEN the same day against the same pinned artifact (exit 0, 8/8 assertions) and reaches it + GREEN the same day against the same pinned artifact (exit 0) and reaches it ONCE: `with-admit() 1`, `without-admit() 0`, `state-before-round() 1`. Both sides use the SAME constants (PRIO=1, DEADLINE_LO=1000, NOW_LO=2000) taken from app/dispatch-driver. This is the on-target differential doing its job — the thing jess's lane exists for. @@ -6453,7 +6459,10 @@ artifacts: *** TWO PIECES OF ACCRETION REMOVED IN THE SAME CHANGE *** (a) The pin directory was named `fg60`, encoding 0.60.0 in a path — the version-in-a-filename hazard AFD-106 flagged and did not fix. Renamed to `synthpin` (version-neutral) across - all 16 references in 6 files, so the next bump cannot produce a lying filename. + 6 files, so the next bump cannot produce a lying filename. + CORRECTION (clean-room): this said "all 16 references"; the count outside findings.yaml + is 20. The file count was right and the rename is complete (grep over .github/, tools/, + hardware/, scripts/ returns nothing); only the reference count was wrong. (b) CI fetched synth 0.62.0 SEPARATELY, purely because the old pin predated verify-embedder. The pin now carries it, so that download was a stale version left behind by an earlier bump — the exact drift-by-accretion this repo keeps finding. Removed; build and check now @@ -6470,3 +6479,87 @@ artifacts: detected-by: per-piece release-watch of synth v0.64.0 against every jess-lowered artifact, 2026-09-07 severity: critical triage-status: confirmed + + - id: AFD-115 + type: ai-found-defect + title: "the cascade build judged synth ON-PIN by PATH STRING, so the genuinely pinned binary reached by a relative path was declared a CANDIDATE differential and REQUIRE_ON_PIN failed on it — plus check-drift claimed ci-vs-pin agreement for two tools it never compared" + status: open + description: |- + 2026-09-08. Clean-room verification of AFD-113/AFD-114. Every substantive claim in both + CONFIRMED — all six artifacts byte-identical across the pin bump, the #1189 defect signature, + the silicon result, and gale-nano's component import/export asymmetry. Neither finding was + found to overstate scope (nothing implies gale-nano dispatched; nothing implies the RT1176). + What the audit found was in the MACHINERY, again. + + *** (1) THE OFF-PIN DETECTOR JUDGED A PATH STRING, AND CONTRADICTED ITS OWN COMMENT *** + hardware/renode/cascade-invoke/build.sh decided on-pin-ness with + `[ "$SYNTH" = "$SCRATCH/synthpin/synth" ]` — an ABSOLUTE path comparison. Invoking the + GENUINELY PINNED binary by a RELATIVE path (`SYNTH=.scratch/synthpin/synth`, exactly what a + local run types, and what AFD-114's own verification command used) took the off-pin branch: + !! OFF-PIN TOOLCHAIN — release-watch mode + !! synth in use : synth 0.64.0 !! pinned synth : v0.64.0 + announcing a CANDIDATE differential for an on-pin build, and `REQUIRE_ON_PIN=1` FAILED on the + correct binary. Six lines above it, the meld/loom comment already says why this is wrong: + "judge by DIGEST, not by 'was an override used' — otherwise every CI run would announce + itself as a candidate differential and the banner would stop meaning anything." announce_tool + does it right, with three traps recorded from earlier clean-room passes; the synth branch + bypassed all of it. CI escaped only by accident — ci.yml omits SYNTH, so the default absolute + path happened to string-match. + Fixed to a digest comparison against artifacts.pins. Verified both directions: the relative + path is now ON-PIN and REQUIRE_ON_PIN=1 succeeds; synth 0.60.0 still trips the banner and + still fails under REQUIRE_ON_PIN=1. + + *** (2) A VACUOUS AGREEMENT CLAIM I INTRODUCED THE DAY BEFORE *** + AFD-111 split check-drift.sh into BLOCKING (ci.yml != varve pin) and ADVISORY (PATH only). + AFD-114 then removed ci.yml's SYNTH_VERSION as accretion. `ci_pin()` greps for that literal, + so synth and loom now read `-` in the CI-YML column — yet the summary still printed + "ADVISORY: 4 tool(s) differ ONLY on PATH — ci.yml and the varve pin agree" and "agree for + every tool compared (5)". For synth and loom NO ci-vs-pin comparison happened. The script + already had vocabulary for this ("single-source (not compared)") and the two-source + PATH+varve rows slipped past it. + Now counts ci-vs-pin comparisons only where BOTH are declared, and NAMES the tools it did not + compare. Reads: "agree for the 3 tool(s) where BOTH are declared / NOT COMPARED against + ci.yml (no *_VERSION there): synth loom". Blocking class re-verified potent by reintroducing + the rivet disagreement. + + *** (3) THE #1189 EVIDENCE COULD NOT BE RE-RUN *** + AFD-114's load-bearing "the differential is NOT vacuous" half — the positive control that + makes byte-identity meaningful — existed only as prose. No .wat, no script; the verifier + could reproduce the assembly signature but not the quoted byte counts. + tools/lowering/joinalias/ now commits the module and a check that asserts the property + DIRECTLY on the pinned synth: in the buggy lowering the join writes the param's home so the + final add takes it as BOTH operands (`adds rN, r0, r0`); in the fixed one it reads two + different registers. Guarded against vacuity (refuses if the disassembly contains no `adds` + at all). Potency verified: PASS on 0.64.0 (`adds r4, r2, r0`), FAIL on 0.60.0 + (`adds r3, r0, r0`). Wired into CI. + + *** (4) THREE FIXES IN THE GALE-NANO HARNESS *** + (a) The seam check asserted the three symbols ARE undefined but never that they are the ONLY + ones, while printing "the 3 jess genuinely owes". Writing the exact-set assertion is what + surfaced a real subtlety: `nm` lists all SIX as undefined even after aliasing, because + --redefine-sym renames the DEFINITION to the imported name and the object then carries + both a T and a U entry. So the raw U list is NOT the embedder's obligation. The check now + compares UNRESOLVED = undefined MINUS defined. Negative control: breaking one alias is + refused. + (b) The gale-nano digest was HARDCODED in build.sh, a second copy of a value that also lives + in artifacts.pins with nothing enforcing agreement — the drifted-mirror shape AFD-104 + deleted a registry for. Now read from the pins file, refusing if it cannot be read. + (c) run-on-silicon.sh PRINTED handle and exec_state but never asserted them — so the + exec_state==1 that localises the fault to poll-round rather than admit was eyeballed, and + a regression breaking exec_admit would still have printed OK on the control leg. Both are + now asserted per leg. Re-run on silicon: result unchanged, new assertions pass silently, + only the count still fails — the honest recorded state. + + *** ALSO CORRECTED IN AFD-113/114 THEMSELVES *** + "8/8 assertions" (tools/dispatch/run.sh emits no such count — a precision the cited oracle + does not produce); citing jess's OWN authored WIT comment as the record that gale-nano hands + out handle 0 (circular — the fact is measured, the citation was not evidence); and "16 + references" where the count is 20. All three recorded as corrections in place. + + NOT FOUND: any overstatement of scope in either finding. The verifier specifically checked + for claims that gale-nano dispatched or that anything ran on the RT1176, and found none. + tags: [clean-room, machinery, vacuous-gate, drift, afd-113, afd-114, afd-111, synth-1189] + fields: + detected-by: clean-room verification of AFD-113 and AFD-114 with a fresh-context subagent, 2026-09-08 + severity: major + triage-status: confirmed diff --git a/hardware/renode/cascade-invoke/build.sh b/hardware/renode/cascade-invoke/build.sh index 5e9490e..4ac85aa 100755 --- a/hardware/renode/cascade-invoke/build.sh +++ b/hardware/renode/cascade-invoke/build.sh @@ -52,8 +52,25 @@ command -v arm-none-eabi-gcc >/dev/null || fail "arm-none-eabi-gcc not on PATH" # release), that one pin is set aside EXPLICITLY and the version actually used is printed. # The input pins — the falcon stages and gale-nano — are still enforced, because a # toolchain differential is only meaningful if the inputs are identical. -PINNED_SYNTH="$SCRATCH/synthpin/synth" -if [ "$SYNTH" = "$PINNED_SYNTH" ]; then +# Judge synth by DIGEST, not by the path string. +# +# This was `[ "$SYNTH" = "$SCRATCH/synthpin/synth" ]`, an ABSOLUTE-path comparison. So +# invoking the GENUINELY PINNED binary by a RELATIVE path — `SYNTH=.scratch/synthpin/synth`, +# exactly what a local run types — took the off-pin branch: the banner announced a CANDIDATE +# differential for an on-pin build, and `REQUIRE_ON_PIN=1` FAILED on the correct binary. +# The adjacent comment for meld/loom already said to judge by digest "otherwise every CI run +# would announce itself as a candidate differential and the banner would stop meaning +# anything"; the synth branch did not follow it. Found by clean-room verification. +synth_on_pin() { + local d + [ -x "$SYNTH" ] || return 1 + if command -v shasum >/dev/null 2>&1; then d="$(shasum -a 256 "$SYNTH" 2>/dev/null | cut -d" " -f1)" + elif command -v sha256sum >/dev/null 2>&1; then d="$(sha256sum "$SYNTH" 2>/dev/null | cut -d" " -f1)" + else fail "cannot verify synth against its pin: neither shasum nor sha256sum is available"; fi + [ "${#d}" -eq 64 ] || return 1 + grep -qE "^synthpin/synth[[:space:]]+$d([[:space:]]|\$)" "$ROOT/tools/deps/artifacts.pins" +} +if synth_on_pin; then SCRATCH="$SCRATCH" "$ROOT/tools/deps/check.sh" >/dev/null 2>&1 \ || fail "external artifacts do not match tools/deps/artifacts.pins" else @@ -62,7 +79,7 @@ else export DEPS_EXCLUDE="synthpin/synth" # threaded to the sub-oracles' own preflights echo "!! OFF-PIN TOOLCHAIN — release-watch mode" echo "!! synth in use : $("$SYNTH" --version 2>&1 | head -1) ($SYNTH)" - echo "!! pinned synth : $(grep '^synthpin/synth' "$ROOT/tools/deps/artifacts.pins" | awk '{print $3}' | sed 's/.*@//;s/!.*//')" + echo "!! pinned synth : $(grep '^synthpin/synth' "$ROOT/tools/deps/artifacts.pins" | awk '{print $3}' | sed 's/.*@//;s/!.*//' | head -1)" echo "!! inputs ARE pin-verified; results from this build are a CANDIDATE differential," echo "!! not a campaign result, until the pin is updated." [ "$REQUIRE_ON_PIN" = "1" ] && fail "REQUIRE_ON_PIN is set and synth is off-pin" diff --git a/hardware/silicon/f100-gale-nano/build.sh b/hardware/silicon/f100-gale-nano/build.sh index 9388218..94fad15 100755 --- a/hardware/silicon/f100-gale-nano/build.sh +++ b/hardware/silicon/f100-gale-nano/build.sh @@ -19,7 +19,12 @@ command -v arm-none-eabi-gcc >/dev/null || fail "arm-none-eabi-gcc not on PATH" # The artifact must be the PINNED one. A differential against an unpinned gale-nano is a # result about whatever happened to be in .scratch. -want=546531952a5cf0edb05ea804bb77dea9ec2786530cef8310bd718559eeede86f +# READ the expected digest from artifacts.pins rather than carrying a second copy here. +# Two hardcoded hashes that agree today, with nothing enforcing that they keep agreeing, is +# the drifted-mirror shape AFD-104 deleted a registry for. Found by clean-room verification. +want=$(awk '$1=="galenano7/gale-nano-0.7.0.wasm"{print $2; exit}' "$ROOT/tools/deps/artifacts.pins") +[ ${#want} -eq 64 ] || fail "could not read the gale-nano digest from tools/deps/artifacts.pins + (got '${want}') — refusing to verify against a digest this script invented" got=$(shasum -a 256 "$GALE" 2>/dev/null | awk '{print $1}') [ -z "$got" ] && got=$(sha256sum "$GALE" | awk '{print $1}') [ "$got" = "$want" ] || fail "gale-nano is not the pinned artifact @@ -50,11 +55,27 @@ n=$(grep -ci 'skip' "$OUT/lower.log" || true) # The gust:os seam must BE a seam. If these stopped being undefined, gale-nano would be # calling something other than jess's harness and the differential would measure nothing. -for s in poll-task deadline read32; do - arm-none-eabi-nm "$OUT/gale.o" | grep -qE "^ +U $s\$" \ - || fail "'$s' is not undefined in the lowered object — the embedder seam is absent" -done -echo "embedder seam present: poll-task, deadline, read32 (the 3 jess genuinely owes)" +# EXACT set, not membership. The previous check asserted these three ARE undefined and +# said "the 3 jess genuinely owes", but never that they are the ONLY ones — so a lowering +# that grew a seventh obligation would have passed while the message kept claiming three. +# UNRESOLVED = undefined MINUS defined, within this one object. +# +# `nm` lists all SIX as undefined even after the aliasing, because --redefine-sym renames the +# definition to the imported name and the object then carries BOTH a T and a U entry for it; +# the linker resolves them internally. So the raw U list is NOT "what the embedder owes", and +# a check written against it either expects six (and silently tolerates the aliasing breaking) +# or expects three (and fails on a correct build). Writing this assertion is what surfaced +# that — the earlier membership check could not have. +und="$(arm-none-eabi-nm "$OUT/gale.o" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u)" +def_="$(arm-none-eabi-nm "$OUT/gale.o" | awk '$2=="T"||$2=="t"||$2=="W"{print $3}' | sort -u)" +got="$(comm -23 <(printf '%s\n' "$und") <(printf '%s\n' "$def_") | tr '\n' ' ')" +[ "$got" = "deadline poll-task read32 " ] \ + || fail "the embedder seam is not the expected set. + expected (unresolved): deadline poll-task read32 + got: $got + (3 of gale-nano's 6 lowered imports are its OWN exports, aliased above and resolved inside + the object; a change here means synth's lowering moved or the aliasing stopped resolving.)" +echo "embedder seam is EXACTLY: poll-task, deadline, read32 (the 3 jess genuinely owes)" "$PY" "$ROOT/tools/embedder-init/extract_init.py" "$GALE" \ --out-c "$OUT/init_tables.c" --out-manifest "$OUT/init.json" >"$OUT/einit.log" 2>&1 \ diff --git a/hardware/silicon/f100-gale-nano/run-on-silicon.sh b/hardware/silicon/f100-gale-nano/run-on-silicon.sh index d41b1d0..cdd4963 100755 --- a/hardware/silicon/f100-gale-nano/run-on-silicon.sh +++ b/hardware/silicon/f100-gale-nano/run-on-silicon.sh @@ -44,8 +44,15 @@ run_leg() { echo printf "%-42s %-11s %-9s %-9s %s\n" "LEG (only the ADMIT word differs)" "poll-task#" "handle" "state" "completion" rc=0 -for leg in "1|task admitted (baseline)|ge1" "0|no admit (negative control)|eq0"; do - IFS='|' read -r flag label want <}" "$h" "${st:-}" "$d" "$ok" done echo diff --git a/hardware/silicon/f100-gust-hal/README.md b/hardware/silicon/f100-gust-hal/README.md index 3953bab..6fa5620 100644 --- a/hardware/silicon/f100-gust-hal/README.md +++ b/hardware/silicon/f100-gust-hal/README.md @@ -57,8 +57,9 @@ produce it. ## H3's second half: what gale-nano still needs -Measured against the **pinned** artifact (`gale-nano 0.7.0`, sha256 `546531952a5c…`), with -synth 0.60.0: +Measured against the **pinned** artifact (`gale-nano 0.7.0`, sha256 `546531952a5c…`). First +measured under synth 0.60.0 and re-verified byte-identical under the current pin, 0.64.0 +(AFD-114) — the numbers below hold for both: ``` cortex-m3 exit 0, 0 skips, 4775 B diff --git a/hardware/silicon/f100-init/README.md b/hardware/silicon/f100-init/README.md index a84dce2..130e890 100644 --- a/hardware/silicon/f100-init/README.md +++ b/hardware/silicon/f100-init/README.md @@ -93,8 +93,8 @@ linkability, not consumption. Hence the executed check above. ## Reproducibility and recovery -The flashed image is **byte-identical whether built with the campaign pin (synth 0.60.0) -or 0.63.0** (`md5 44cbc79c49735d1a616eec6b34a6cdd3`), so the silicon result is not an +The flashed image is **byte-identical across every synth the campaign has pinned (0.60.0, 0.63.0 and the current +pin 0.64.0)** (`md5 44cbc79c49735d1a616eec6b34a6cdd3`), so the silicon result is not an artifact of an off-pin toolchain. The board's resident firmware is restored from diff --git a/tools/lowering/joinalias/check.sh b/tools/lowering/joinalias/check.sh new file mode 100755 index 0000000..345536e --- /dev/null +++ b/tools/lowering/joinalias/check.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# Assert the pinned synth does NOT exhibit synth#1189 (the if/else join aliasing a local's +# home register on the ARM direct selector). +# +# WHY THIS EXISTS AS A GATE. AFD-114 bumped the pin to 0.64.0 on the strength of a +# two-binary differential, and clean-room verification pointed out that the evidence — +# including the "the control fires" half that makes the byte-identical result non-vacuous — +# lived ONLY as prose in a findings file. Nothing could re-run it. This can. +# +# The signature is specific rather than a version check: in the BUGGY lowering the join +# writes the param's home register, so the final add has that register as BOTH operands +# (`adds rN, r0, r0`). In the fixed lowering the then-arm copies the home into a temp first +# and the add reads two DIFFERENT registers. This module never legitimately doubles param 0 +# — the correct answer is 5 + a — so a same-register add of r0 is the defect and nothing else. +set -uo pipefail +D="$(cd "$(dirname "$0")" && pwd)" +ROOT="$(cd "$D/../../.." && pwd -P)" +SYNTH="${SYNTH:-$ROOT/.scratch/synthpin/synth}" +OUT="${OUT:-$(mktemp -d)}" +fail() { printf 'FAIL: %s\n' "$*" >&2; exit 1; } +[ -x "$SYNTH" ] || fail "synth not executable at $SYNTH" +command -v wasm-tools >/dev/null || fail "wasm-tools not on PATH" + +"${WASM_TOOLS:-wasm-tools}" parse "$D/joinalias.wat" -o "$OUT/j.wasm" || fail "wasm-tools parse" +"$SYNTH" compile "$OUT/j.wasm" -t cortex-m3 --cortex-m --relocatable --all-exports \ + -o "$OUT/j.o" >"$OUT/lower.log" 2>&1 || { cat "$OUT/lower.log"; fail "control did not lower"; } + +dis="$("$SYNTH" disasm "$OUT/j.o" 2>/dev/null)" +# The disassembly must be non-empty AND contain the add, or the grep below would pass +# vacuously on an empty string — the failure this repo keeps finding in checkers. +echo "$dis" | grep -qE '\badds\b' \ + || fail "no 'adds' in the disassembly — the check would be vacuous +$dis" + +bad="$(echo "$dis" | grep -E '\badds\s+r[0-9]+,\s*r0,\s*r0\b' || true)" +if [ -n "$bad" ]; then + echo "$bad" + fail "synth#1189 SIGNATURE PRESENT: the join wrote param 0's home register, so the add + takes it as both operands. This lowering computes a + a instead of 5 + a — exit 0, + wrong answer. $("$SYNTH" --version 2>&1 | head -1)" +fi +echo "synth#1189 absent: the join does not alias param 0's home ($("$SYNTH" --version 2>&1 | head -1))" +echo "$dis" | grep -E '\badds\b' | sed 's/^/ /' diff --git a/tools/lowering/joinalias/joinalias.wat b/tools/lowering/joinalias/joinalias.wat new file mode 100644 index 0000000..280b2d7 --- /dev/null +++ b/tools/lowering/joinalias/joinalias.wat @@ -0,0 +1,20 @@ +;; synth#1189 / RQ-64-JOINALIAS control module. +;; +;; The defect class: on the ARM DIRECT SELECTOR (every --relocatable compile), `local.get` +;; of a register-homed local pushes the HOME REGISTER uncopied. When that is the then-arm +;; result of a value-carrying if/else, the join `mov R_then, R_else` on the else path WRITES +;; THE LOCAL — so a later `local.get` of it reads the join's value instead. Exit 0, no +;; decline, wrong answer. +;; +;; This module is the minimal shape that exhibits it: param 0 is homed in a register, it is +;; the then-arm result, and it is RE-READ after the join. +;; f(a=7, b=0) -> else taken -> if-result = 5, so the correct answer is 5 + 7 = 12. +;; Under synth 0.60.0 the join clobbers r0 and the code computes r0 + r0 = 14. +(module + (func (export "joinalias") (param $a i32) (param $b i32) (result i32) + (i32.add + (if (result i32) (local.get $b) + (then (local.get $a)) + (else (i32.const 5))) + (local.get $a))) +) diff --git a/tools/lowering/m4-matrix.sh b/tools/lowering/m4-matrix.sh index 4831ccd..8df4293 100755 --- a/tools/lowering/m4-matrix.sh +++ b/tools/lowering/m4-matrix.sh @@ -4,7 +4,7 @@ # externals is not a shippable image. # # WHAT THIS ESTABLISHES (AFD-046): the M4-portability half of GI-FPU-002 is resolved in -# synth v0.60 via the relocatable + embedder-contract path, and jess's obligation as the +# the campaign-pinned synth via the relocatable + embedder-contract path, and jess's obligation as the # embedder is exactly THREE AEABI symbols, all present in the stock ARM toolchain. # # The plain self-contained path still declines 3 functions on m4f — that is NOT a defect, diff --git a/tools/varve/check-drift.sh b/tools/varve/check-drift.sh index 8e9ae2f..64aae04 100755 --- a/tools/varve/check-drift.sh +++ b/tools/varve/check-drift.sh @@ -23,7 +23,7 @@ ci_pin() { # tool -> the version ci.yml downloads, or empty } ver() { "$@" --version 2>/dev/null | head -1 | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1; } -compared=0; single=0; advisory=0 +compared=0; single=0; advisory=0; cipin=0; nocipin="" printf '%-8s %-12s %-12s %-12s %s\n' TOOL PATH VARVE-PIN CI-YML STATUS for t in rivet spar meld synth loom sigil; do p="$(ver "$t")" @@ -65,18 +65,28 @@ for t in rivet spar meld synth loom sigil; do n_sources=${#seen[@]} if [ "${uniq_n:-0}" -eq 0 ]; then st="absent (not checked)" elif [ "$n_sources" -eq 1 ]; then st="single-source (not compared)"; single=$((single+1)) - elif [ "${uniq_n:-0}" -eq 1 ]; then st="ok"; compared=$((compared+1)) + elif [ "${uniq_n:-0}" -eq 1 ]; then + st="ok"; compared=$((compared+1)) + # An all-agree row is still a ci-vs-pin comparison when both are declared — count it, + # or the summary under-reports what it actually checked. + if [ -n "$v" ] && [ -n "$c" ]; then cipin=$((cipin+1)); else nocipin="$nocipin $t"; fi elif [ -n "$v" ] && [ -n "$c" ] && [ "$v" != "$c" ]; then - st="DRIFT-BLOCKING (ci.yml != pin)"; drift=1; compared=$((compared+1)) + st="DRIFT-BLOCKING (ci.yml != pin)"; drift=1; compared=$((compared+1)); cipin=$((cipin+1)) else st="drift-advisory (PATH only)"; advisory=$((advisory+1)); compared=$((compared+1)) + # Count the ci-vs-pin comparison ONLY when BOTH sources exist. A row with just PATH and + # the varve pin is a two-source row, but it says NOTHING about ci.yml — and the summary + # used to claim "ci.yml and the varve pin agree" for exactly those rows. That went + # unnoticed until removing ci.yml's SYNTH_VERSION made synth and loom read `-` here while + # the prose still asserted agreement for them. Found by clean-room verification. + if [ -n "$v" ] && [ -n "$c" ]; then cipin=$((cipin+1)); else nocipin="$nocipin $t"; fi fi printf '%-8s %-12s %-12s %-12s %s\n' "$t" "${p:--}" "${v:--}" "${c:--}" "$st" done echo if [ "$advisory" -gt 0 ]; then - echo "ADVISORY: $advisory tool(s) differ ONLY on PATH — ci.yml and the varve pin agree." + echo "ADVISORY: $advisory tool(s) differ on PATH from the pin." echo " Harmless for the BUILD (scripts resolve explicitly or via varve), but it is exactly" echo " what produced meld#390: a defect filed against the PATH binary's version." echo " Before citing ANY version upstream, quote \`varve run --version\`, not PATH." @@ -101,6 +111,11 @@ if [ "$compared" -eq 0 ]; then echo "A 'no drift' verdict here would be green on a toolchain never inspected." >&2 exit 2 fi -echo "no blocking drift: ci.yml and the varve pin agree for every tool compared ($compared)." +echo "no blocking drift: ci.yml and the varve pin agree for the $cipin tool(s) where BOTH are declared." +if [ -n "$nocipin" ]; then + echo "NOT COMPARED against ci.yml (no *_VERSION there):$nocipin" + echo " These rows say nothing about CI. Claiming agreement for them would be a verdict" + echo " about a comparison that never happened." +fi [ "$single" -gt 0 ] && echo "($single row(s) 'single-source' and any 'absent' rows were compared against nothing — not evidence.)" exit 0 From 2cd8d1246deb1f08aff7f84d2ba2c6d19ee3a49c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 8 Sep 2026 21:05:10 +0200 Subject: [PATCH 2/2] =?UTF-8?q?fix:=20the=20join-alias=20gate=20used=20syn?= =?UTF-8?q?th=20disasm=20and=20captured=20stdout=20only=20=E2=80=94=20CI?= =?UTF-8?q?=20proved=20it=20empty?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The gate passed locally and failed in CI with 'no adds in the disassembly'. synth writes its disassembly and INFO log across both streams and the split differs on the Linux build, so a stdout-only capture came back without the instruction. The vacuity guard caught it rather than letting an empty capture report a pass, which is the one thing that had to work — a gate whose evidence silently vanishes is exactly what this check exists to prevent. Switched to arm-none-eabi-objdump: deterministic, already a preflight dependency of the job that runs this, and format-stable across hosts. Potency re-verified all three ways — PASS on 0.64.0, FAIL on 0.60.0, and the vacuity guard still refuses an empty disassembly. Co-Authored-By: Claude Opus 4.8 --- tools/lowering/joinalias/check.sh | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/tools/lowering/joinalias/check.sh b/tools/lowering/joinalias/check.sh index 345536e..d7c1260 100755 --- a/tools/lowering/joinalias/check.sh +++ b/tools/lowering/joinalias/check.sh @@ -25,7 +25,16 @@ command -v wasm-tools >/dev/null || fail "wasm-tools not on PATH" "$SYNTH" compile "$OUT/j.wasm" -t cortex-m3 --cortex-m --relocatable --all-exports \ -o "$OUT/j.o" >"$OUT/lower.log" 2>&1 || { cat "$OUT/lower.log"; fail "control did not lower"; } -dis="$("$SYNTH" disasm "$OUT/j.o" 2>/dev/null)" +# Disassemble with arm-none-eabi-objdump, NOT `synth disasm`. +# +# The first version used `synth disasm` and captured stdout only. That passed locally and +# FAILED IN CI with "no 'adds' in the disassembly" — synth writes its disassembly and its INFO +# log across both streams, and the split is not the same on the Linux build. The vacuity guard +# below caught it rather than letting an empty capture report a pass, which is the one thing +# that had to work. objdump is deterministic, is already a preflight dependency of the job that +# runs this, and does not change format between hosts. +command -v arm-none-eabi-objdump >/dev/null || fail "arm-none-eabi-objdump not on PATH" +dis="$(arm-none-eabi-objdump -d "$OUT/j.o" 2>/dev/null)" # The disassembly must be non-empty AND contain the add, or the grep below would pass # vacuously on an empty string — the failure this repo keeps finding in checkers. echo "$dis" | grep -qE '\badds\b' \