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..d7c1260 --- /dev/null +++ b/tools/lowering/joinalias/check.sh @@ -0,0 +1,52 @@ +#!/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"; } + +# 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' \ + || 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