From cfbf1e7b64bcd6d59f99129c9f7bea5bd45175d7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 05:01:54 +0200 Subject: [PATCH] =?UTF-8?q?fix:=20clean-room=20verification=20found=20a=20?= =?UTF-8?q?VACUOUS=20NEGATIVE=20CONTROL=20in=20a=20merged=20safety=20artif?= =?UTF-8?q?act=20=E2=80=94=20and=20five=20more=20(AFD-048)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A fresh-context verifier was run over the three PRs merged today, per the standing every-~2-features rule. It found six real defects. The headline is the worst kind: the campaign's own anti-vacuity discipline failed inside the artifact that most loudly advertised it. F1 CRITICAL — AFD-044's negative control (i) was VACUOUS. It perturbed wx by +0.05, re-ticked, and reported the changed fold (1348 -> 2000) as proof "the fold tracks its input". The second tick ran ON THE SAME INSTANCE. The rate loop carries an integrator, so the second call differs REGARDLESS of input — ticking the IDENTICAL input twice also gives 1348 -> 2000. Independently reproduced. And on a FRESH instance the documented perturbation moves the fold by ZERO, because this operating point is mixer-SATURATED (m1=m2=0, m4=1). A build that ignored its input entirely would have passed. FIXED: fresh instance, and perturb wy, which demonstrably moves the fold. MEASURED SCOPE, now printed rather than assumed: only 4 of 18 input scalars move the fold on a single tick. The whole quaternion, position and velocity — 10 scalars — are INERT even at ±5.0. F3 — the "COMPLETELY DIFFERENT ROUTE" claim was FALSE. Both legs execute the same compiled falcon code; the rate#tick bodies are instruction-identical apart from a uniform data rebase. The oracle catches composition/lowering/ABI faults and CANNOT catch a falcon arithmetic bug. The header claimed exactly the property it lacked. F4 — the oracle's window was 0.07%. int(sum*1000) meant composed=1348 accepted any reference in [1.348,1.349); the verifier falsified the thrust setpoint to 0.75 and it still passed. FIXED: the fold is now raw f32 BITS. Both escapes now FAIL — the thrust falsification differs by a SINGLE LSB (…774 vs …773), which the old fold rounded away. F5 — build-and-verify.sh EXITED 1 as shipped: it preflighted four tools and four artifacts but not the wasmtime PYTHON module its oracle imports, failing at step 5 with a bare ModuleNotFoundError AFTER composition succeeded — so it read as an oracle mismatch, not a missing dependency. FIXED: preflight + requirements.txt. F6 — check-drift.sh had two vacuities of its own, in the tool written to prevent this: all-absent printed "no drift" and exited 0 (green on a toolchain never inspected; now exit 2), and a single-source tool scored "ok" (now "single-source (not compared)"). Both negative-controlled, and the ok path proven still REACHABLE. Third issue RECORDED NOT FIXED: tools lacking --version (spar, ordeal) read as absent though the binary IS on PATH — they drop silently out of the comparison. F10 — documentation overclaims, one of them mine THIS SESSION: - AFD-042's "ABSENT on every loop tick … has never found it" is FALSE. The board WAS attached 2026-08-25 and jess captured 77,034 bytes of live telemetry (AFD-037, 4ee2a5f), re-parsed independently at 1,021 CRC-valid frames. I repeated that false absolute verbally today while correcting a different error. The defensible claim is scoped: no falcon code has EXECUTED on the RT1176. - hardware/silicon/README.md said "this is the actual chip" while everything under it ran on Renode. - README.md labelled the Renode node "HIL emulation". No hardware is in that loop. - AFD-037's TITLE still carried "ZERO CRC failures", withdrawn as vacuous in the same PR's second commit; the withdrawal never reached the title. Also: AFD-046 said func_4, it is func_3; and "DISCHARGED" now says plainly that the discharge is a successful LINK, not an execution. WHAT THE VERIFIER CONFIRMED: m4-matrix reproduced BYTE-IDENTICALLY, its "0 undefined" is not vacuous, its zero-skips claim is substantiated, and the CI gate is genuinely non-empty. The composition, the run and the agreement are all real — the CONTROL around them was weak. FOR THE USER (F2, not fixable here): main has NO required status checks. deletion, non_fast_forward, pull_request and required_signatures are set; required_status_checks is not, and required_approving_review_count is 0. The five green checks are ADVISORY. All three oracles re-run green after the fixes. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- README.md | 2 +- app/flight-app/src/lib.rs | 10 +- artifacts/findings.yaml | 118 ++++++++++++++++++-- hardware/silicon/README.md | 5 +- tools/appcompose/build-and-verify.sh | 23 +++- tools/cascade-differential/cascade_ref.py | 56 +++++++--- tools/cascade-differential/requirements.txt | 4 + tools/varve/check-drift.sh | 32 +++++- 8 files changed, 212 insertions(+), 38 deletions(-) create mode 100644 tools/cascade-differential/requirements.txt diff --git a/README.md b/README.md index 5a98847..182f293 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ flowchart LR fw["falcon firmware
(Cortex-M ELF)"] gale["gale
verified RTOS primitives"] kiln["kiln
QM validation runtime"] - renode["Renode
HIL emulation"] + renode["Renode
emulation (no hardware in this loop)"] rwc["rules_wasm_component
hermetic Bazel chain"] subgraph gov["evidence & architecture"] diff --git a/app/flight-app/src/lib.rs b/app/flight-app/src/lib.rs index bd6fd0e..6b85186 100644 --- a/app/flight-app/src/lib.rs +++ b/app/flight-app/src/lib.rs @@ -43,14 +43,20 @@ impl bindings::Guest for App { // Fold the motor outputs to a single observable word. Bit 31 carries the // clock leg so a stalled `time` import is distinguishable from a bad mix. - let acc = (pwm.m1 + pwm.m2 + pwm.m3 + pwm.m4) * 1000.0; + // BIT-EXACT, not scaled-and-truncated. The original folded `sum * 1000.0` to an + // integer, which accepts any reference sum in [1.348, 1.349) — a 0.07% window. + // Clean-room verification falsified the reference's thrust setpoint to 0.75 and + // the oracle still reported PASS. Comparing the raw f32 bits closes that window + // to a single value; the sign bit is dropped (the sum is positive) so bit 31 + // stays available for the clock leg. + let acc_bits = (pwm.m1 + pwm.m2 + pwm.m3 + pwm.m4).to_bits() & 0x7fff_ffff; // Bit 31 must DISCRIMINATE, not merely be present. `elapsed(...) == false` // was the first choice and it is vacuous: an inert clock returns false too. // `deadline(t0, 1) != t0` cannot be produced by a stub that returns zeros — // it is true only if gale actually did the tick arithmetic on our argument. let clock_live = (deadline != t0) as u32; - (acc as u32 & 0x7fff_ffff) | (clock_live << 31) + acc_bits | (clock_live << 31) } } diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index 9edcb10..3627355 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -1696,15 +1696,26 @@ artifacts: set bit 31 from `elapsed(now, deadline) == false`, which an inert clock returns too — the same trap that voided the CRC claim in AFD-037. It now tests `deadline(t0,1) != t0`, which no zero-returning stub can produce. - DIFFERENTIAL, not a golden number. tools/cascade-differential/cascade_ref.py recomputes the - same fold by a COMPLETELY DIFFERENT ROUTE — fused core module, raw canonical-ABI pointers, no - component model, no wac, no gust:os. Both routes give 1348. A golden value would be satisfied - by both sides sharing one bug; agreement across two routes would not be. + DIFFERENTIAL, and THE CLAIM ABOUT WHAT THAT BUYS IS CORRECTED (2026-08-28, AFD-048). The two + legs differ in COMPOSITION AND ABI PATH - component model + wac + gust:os on one side, fused + core module + raw canonical-ABI pointers on the other. They do NOT differ in ARITHMETIC: + disassembly shows the rate#tick bodies INSTRUCTION-IDENTICAL apart from a uniform data rebase. + So the oracle catches composition, lowering and ABI-marshalling faults and CANNOT catch a bug + inside falcon - both sides would share it. The original wording claimed the exact opposite and + was wrong. The fold is now BIT-EXACT (raw f32 bits) rather than int(sum*1000), which accepted + a 0.07% window and let a falsified thrust setpoint pass undetected. torque tx=1 ty=0.472507507 tz=-0.147003502 thrust=0.5 <- reproduces the SIL reference exactly pwm m1=0 m2=0 m3=0.348992109 m4=1 sum=1.34899211 NEGATIVE CONTROLS, all three run: - (i) reference perturbed (wx 0.30 -> 0.35) -> 2000, DISTINCT: the fold tracks its input, so - 1348 is not a constant a miscompile that drops the state would also produce. + (i) *** THIS CONTROL WAS VACUOUS AND IS WITHDRAWN (corrected 2026-08-28 by clean-room + verification, AFD-048) ***. It perturbed wx by +0.05 and re-ticked ON THE SAME + INSTANCE, reporting the changed fold as proof the output tracks its input. It proved + only that the module is STATEFUL: the rate loop carries an integrator, so a second + call differs REGARDLESS of input - ticking the IDENTICAL input twice also gives + 1348 -> 2000. Worse, the documented perturbation moves the fold by ZERO on a fresh + instance, because this operating point is mixer-SATURATED (m1=m2=0, m4=1). A build + ignoring its input entirely would have passed. Replaced with a FRESH-INSTANCE control + perturbing wy, which demonstrably moves the fold. (ii) reference deliberately falsified (x1000 -> x1001) -> oracle EXITS 1 with "DIFFERENTIAL MISMATCH: composed=1348 reference=1350"; restored -> PASS. The gate can fail. (iii) publish gate on jess's OWN components: FAILED C4+C5 before the link flags, PASSED after. @@ -1737,6 +1748,86 @@ artifacts: - type: traces-to target: REQ-PIX-007 + - id: AFD-048 + type: ai-found-defect + severity: critical + triage-status: closed + detected-by: clean-room verification with a fresh-context subagent over PRs #191/#192/#193, 2026-08-28 + title: CLEAN-ROOM VERIFICATION FOUND A VACUOUS NEGATIVE CONTROL INSIDE A MERGED SAFETY ARTIFACT — AFD-044's control measured STATEFULNESS, not input sensitivity; plus an overstated independence claim, a 0.07% oracle window, an unpinned dependency, and documentation overclaims + status: resolved + description: > + 2026-08-28. A fresh-context verifier was run over the three PRs merged that day, per the + standing every-~2-features rule. It found six real defects. THE HEADLINE: the campaign's own + anti-vacuity discipline failed inside the artifact that most loudly advertised it. + *** F1, CRITICAL - AFD-044's NEGATIVE CONTROL (i) WAS VACUOUS ***. It perturbed wx by +0.05, + re-ticked, and reported the changed fold (1348 -> 2000) as proof "the fold tracks its input". + The second tick ran ON THE SAME INSTANCE. The rate loop carries an integrator, so the second + call differs REGARDLESS of input: ticking the IDENTICAL input twice ALSO gives 1348 -> 2000. + Independently reproduced here. And on a FRESH instance the documented perturbation moves the + fold by ZERO, because the operating point is mixer-SATURATED (m1=m2=0, m4=1) and absorbs small + moves. A build that ignored its input entirely would have passed this control. + FIXED: the control now uses a FRESH INSTANCE and perturbs wy, which demonstrably moves the fold. + MEASURED SCOPE, now printed by the oracle rather than assumed: only 4 of 18 input scalars + (wx, wy, wz, sp.ry, sp.rz) move the fold at all on a single tick. The entire quaternion, + position and velocity - 10 scalars - are INERT even at +-5.0. So the differential cannot detect + a miscompile confined to attitude/position/velocity handling, and now says so. + *** F3 - THE "COMPLETELY DIFFERENT ROUTE" CLAIM WAS FALSE ***. Both legs execute the SAME + compiled falcon code; disassembly shows the rate#tick bodies instruction-identical apart from a + uniform data rebase. The oracle tests composition, lowering and ABI marshalling - NOT falcon + arithmetic, which both sides would get wrong together. The header claimed precisely the + property it lacked. + *** F4 - THE ORACLE'S WINDOW WAS 0.07% ***. It compared int(sum * 1000.0), so composed=1348 + accepted any reference in [1.348, 1.349). The verifier falsified the reference's THRUST + SETPOINT to 0.75 and the gate still passed. FIXED: the fold is now the raw f32 BITS (sign + dropped, bit 31 still the clock leg). Both escapes now FAIL - and the thrust falsification + differs by a SINGLE LSB (1068280774 vs 1068280773), which the old fold rounded away. + *** F5 - build-and-verify.sh EXITED 1 AS SHIPPED ***: it preflighted cargo/wasm-tools/wac/the + wasmtime CLI and four supplier artifacts, but not the wasmtime PYTHON MODULE its oracle + imports. On a clean machine it failed at step 5 with a bare ModuleNotFoundError - AFTER the + composition succeeded, so it read as an oracle mismatch rather than a missing dependency. + FIXED: preflight + tools/cascade-differential/requirements.txt. + *** F6 - check-drift.sh HAD TWO RESIDUAL VACUITIES OF ITS OWN ***, in the tool written to + prevent exactly this: (a) if EVERY tool was absent it printed "no drift" and exited 0 - a green + verdict on a toolchain never inspected; now exits 2. (b) a tool found in exactly ONE source + scored "ok"; one value compared against nothing is not agreement; now "single-source (not + compared)". Both negative-controlled, and the ok path proven still reachable. A third issue is + RECORDED BUT NOT FIXED: `ver` reads versions via `--version`, so tools lacking that flag (spar, + ordeal) read as absent even though the binary IS on PATH - they drop silently OUT of the + comparison, the inverse and more dangerous direction. varve verify reports 7 shadowed tools. + *** F10 - DOCUMENTATION OVERCLAIMS, one of them MINE THIS SESSION ***: + - AFD-042 said the Pixhawk "has been ABSENT on every loop tick ... and has never found it". + FALSE. The board WAS attached 2026-08-25 and jess captured 77,034 bytes of live telemetry + (AFD-037, 4ee2a5f), independently re-parsed by the verifier at 1,021 CRC-valid MAVLink v1 + frames, single sysid, ATTITUDE/HIGHRES_IMU-dominated. jess REPEATED that false absolute + this session while correcting a different error. The defensible claim is the SCOPED one: + no falcon code has ever EXECUTED on the RT1176. + - hardware/silicon/README.md asserted "this is the actual chip" while everything under it ran + on Renode 1.16.1 and the board is marked "(ordered)". + - README.md labelled the Renode node "HIL emulation". There is no hardware in that loop. + - AFD-037's TITLE still carried "ZERO CRC failures" - a claim the same PR's second commit had + explicitly withdrawn as vacuous. The withdrawal never propagated to the title. + ALSO CORRECTED: AFD-046 named the m4f-declined function func_4; it is func_3. And AFD-046's + "the obligation was DISCHARGED" now states plainly that the discharge is a successful LINK, not + an execution - the object has been run nowhere. + *** WHAT THE VERIFIER CONFIRMED, so this is not only bad news ***: the m4-matrix result + (AFD-046) reproduced BYTE-IDENTICALLY from the recorded input, its "0 undefined" is NOT vacuous + (an empty object fails the post-link 5/5 recount), and its zero-skips claim is substantiated by + the self-contained path visibly producing skips. The composition, the run and the agreement are + all real - it is the CONTROL around them that was weak. The CI gate is genuinely non-empty: + 5 substantive checks ran SUCCESS on every merge commit. + *** F2, SEPARATE AND FOR THE USER: main has NO required status checks ***. The ruleset carries + deletion, non_fast_forward, pull_request and required_signatures, but no required_status_checks, + and required_approving_review_count is 0. The five green checks are ADVISORY - a red board would + not block a merge. jess has been asserting "CONFIRM CI SUCCESS before merging" as a process rule + and honouring it by hand, while the repo would not have enforced it. Also: none of the three new + oracles is wired into CI, and check-drift.sh currently exits 1 where it lives. + tags: [clean-room, vacuous-metric, self-correction, oracle, negative-control, campaign-machinery] + links: + - type: traces-to + target: DD-026 + - type: traces-to + target: REQ-PIX-007 + - id: AFD-046 type: ai-found-defect severity: major @@ -1750,7 +1841,7 @@ artifacts: needs is jess keeping two promises. THE SELF-CONTAINED PATH STILL DECLINES 3 FUNCTIONS ON m4f, AND THAT IS CORRECT BEHAVIOUR, not a defect: synth refuses to emit f64 on a single-precision FPU (#369). The declined functions are - func_4, position#tick and rate#tick, and synth's own message names the remedy - route the + func_3, position#tick and rate#tick, and synth's own message names the remedy - route the i64<->f32 conversions through the AEABI builtins with --relocatable (#1069). FOLLOWING SYNTH'S DOCUMENTED REMEDY WALKS A CHAIN OF THREE HONEST-REFUSAL GATES, each of which hands jess an obligation rather than failing silently: @@ -1767,6 +1858,9 @@ artifacts: are defined in the stock arm-none-eabi libgcc (thumb/v7e-m+fp/hard multilib), `arm-none-eabi-ld -r` against it returns 0 with ZERO undefined symbols remaining, and all 5 cascade stages are still present as T in the linked object. + PRECISION ON "DISCHARGED" (clean-room, AFD-048): the discharge is a successful LINK, not an + execution. The object has not been RUN anywhere - not on silicon, not in Renode. "It links" is + weaker than "it works" in exactly the way "it lowers" is, and is meant as such. NEGATIVE CONTROL: linking WITHOUT libgcc leaves exactly those 3 symbols undefined. Without this the "0 undefined" result would be vacuous - an empty nm is also what a broken object prints. The oracle asserts the negative control and FAILS if it comes back empty. @@ -1891,8 +1985,12 @@ artifacts: *** THE CORRECTION - jess's own claim, mis-stated upstream, attached to a status flip ***: synth's closing note says the flip to `verified` happened "because JESS EXECUTED IT ON HARDWARE". That is FALSE and jess corrected it immediately. Every run in that thread was on an RT1176 RENODE MODEL. - The physical Pixhawk 6X-RT has been ABSENT on every loop tick - the hardware probe runs first each - cycle and has never found it. What the evidence actually supports: (a) 5/5 cascade stages reach + The physical Pixhawk 6X-RT was absent on every loop tick OF THIS LOWERING TRACK. + *** THE ORIGINAL ABSOLUTE HERE - "has been ABSENT on every loop tick ... and has never found + it" - IS FALSE, corrected 2026-08-28 (AFD-048) ***: the board WAS attached on 2026-08-25 and + jess captured 77,034 bytes of live telemetry from it (AFD-037, commit 4ee2a5f), independently + re-parsed at 1,021 CRC-valid MAVLink v1 frames from a single sysid. The defensible claim is the + SCOPED one - no falcon code has ever EXECUTED on the RT1176 - not the absolute. What the evidence actually supports: (a) 5/5 cascade stages reach nm->T on m7dp - synth's own stated DoD, independently reproduced by jess; (b) the fused image builds, loads, initialises linear memory byte-exact and retires 213,439 instructions on an EMULATED RT1176 M7. What it does NOT support: execution on silicon, and numerical correctness of @@ -2129,7 +2227,7 @@ artifacts: - id: AFD-037 type: ai-found-defect - title: FIRST LIVE-HARDWARE VALIDATION - jess's MAVLink decoder (REQ-PIX-010) run against the real Pixhawk 6X-RT, read-only; live and committed samples decode identically with ZERO CRC failures + title: FIRST LIVE-HARDWARE VALIDATION - jess's MAVLink decoder (REQ-PIX-010) run against the real Pixhawk 6X-RT, read-only; live and committed samples decode identically (the "ZERO CRC failures" phrase once in this title was VACUOUS and is withdrawn - see the body) status: resolved description: > 2026-08-25: the physical Holybro Pixhawk 6X-RT came online (USB "PX4 FMU v6XRT_x", diff --git a/hardware/silicon/README.md b/hardware/silicon/README.md index 223f092..9a82988 100644 --- a/hardware/silicon/README.md +++ b/hardware/silicon/README.md @@ -3,7 +3,10 @@ The literal-silicon rung for **REQ-PIX-009 / TEST-PIX-016** — closing the "physical F100 reflash pending hardware" caveat on the synth#383 8 KB shrink. qemu (lm3s) gave the functional result; Renode (Cortex-M3 + 8 KB) gives the real -M3-ISA model; **this is the actual chip.** Grounded in gale `benches/gust/REFLASH.md`. +M3-ISA model of that chip. **NOTE (corrected 2026-08-28): the phrase "this is the +actual chip" stood here while everything below ran under Renode 1.16.1. Renode models +the real M3 ISA and 8 KB SRAM, which is the point — but it is not silicon, and the +physical rung below is still pending.** Grounded in gale `benches/gust/REFLASH.md`. ## Board (ordered — standalone eval, NOT the Pixhawk) **STM32VLDISCOVERY** — STM32F100RBT6B: Cortex-M3, 128 KB flash @ `0x08000000`, diff --git a/tools/appcompose/build-and-verify.sh b/tools/appcompose/build-and-verify.sh index 9b77429..7f46e96 100755 --- a/tools/appcompose/build-and-verify.sh +++ b/tools/appcompose/build-and-verify.sh @@ -3,11 +3,14 @@ # the result against an independently-computed reference. # # This is the oracle for AFD-043 (the missing application seam). It is written as a -# DIFFERENTIAL rather than a golden value on purpose: the composed component and the -# reference reach the same number by completely different routes — component model + -# wac composition + gale's gust:os on one side, fused core module + raw canonical-ABI -# pointers on the other. A single golden number would be satisfied by both sides -# sharing one bug; agreement across the two routes would not. +# DIFFERENTIAL rather than a golden value, but WITH A CORRECTED CLAIM about what that +# buys. The two legs differ in their COMPOSITION AND ABI PATH — component model + wac + +# gale's gust:os on one side, fused core module + raw canonical-ABI pointers on the +# other. They do NOT differ in their ARITHMETIC: clean-room verification disassembled +# both and found the rate#tick bodies instruction-identical apart from a uniform data +# rebase. So this oracle catches composition, lowering and ABI-marshalling faults, and +# CANNOT catch a bug inside falcon itself — both sides would share it. The earlier +# header claimed the opposite; that claim was wrong. set -euo pipefail ROOT="$(cd "$(dirname "$0")/../.." && pwd -P)" OUT="${OUT:-$ROOT/.scratch/appcompose}" @@ -42,6 +45,16 @@ for t in cargo wasm-tools wac wasmtime; do command -v "$t" >/dev/null || fail "required tool not on PATH: $t" done +# The reference driver needs the wasmtime PYTHON module, which is a separate thing from +# the wasmtime CLI checked above. Omitting this check made the script exit 1 on a clean +# machine with a bare ModuleNotFoundError from inside step 5 — after the composition had +# already succeeded, so the failure looked like an oracle mismatch rather than a missing +# dependency. See tools/cascade-differential/requirements.txt. +"$PY" -c 'import wasmtime' 2>/dev/null || fail \ + "the Python module 'wasmtime' is missing for interpreter: $PY + install it: $PY -m pip install -r $ROOT/tools/cascade-differential/requirements.txt + or point PY= at an interpreter that has it" + say "== 1. build the two jess components ==" for c in flight-app gust-hal-stub; do ( cd "$ROOT/app/$c" && cargo build --release --target wasm32-unknown-unknown ) diff --git a/tools/cascade-differential/cascade_ref.py b/tools/cascade-differential/cascade_ref.py index a6d6d5b..f36849c 100644 --- a/tools/cascade-differential/cascade_ref.py +++ b/tools/cascade-differential/cascade_ref.py @@ -39,7 +39,9 @@ def main(): # The SAME fold the component performs, in f32 to match wasm arithmetic exactly. acc32 = struct.unpack(" 0.35 - mem.write(store, struct.pack("<14f", *pert) + struct.pack("<4f", *RATE_SETPOINT), argp) - tp2 = ex["pulseengine:falcon-cascade/rate@0.7.0#tick"](store, argp) - t2 = struct.unpack("<4f", mem.read(store, tp2, tp2 + 16)) - p2 = ex["pulseengine:falcon-cascade/mixer@0.7.0#mix"](store, *t2) - pwm2 = struct.unpack("<4f", mem.read(store, p2, p2 + 16)) + # NEGATIVE CONTROL — REWRITTEN 2026-08-28 after clean-room verification found the + # original was VACUOUS. Recorded here because the mistake is instructive. + # + # The original perturbed wx by +0.05 and re-ticked ON THE SAME INSTANCE, then + # reported the changed fold as proof that "the fold tracks its input". It proved + # nothing of the sort: the rate loop carries integrator state, so a SECOND call + # differs from the first REGARDLESS of input. Ticking the IDENTICAL input twice + # also gives 1348 -> 2000. A build that ignored its input entirely would have + # passed that control. + # + # Two things were wrong and both are fixed: + # (1) the control now uses a FRESH INSTANCE, so state cannot masquerade as + # input sensitivity; + # (2) the perturbation is one that DEMONSTRABLY moves the fold on a fresh + # instance. wx +0.05 does NOT — this operating point is mixer-SATURATED + # (m1=m2=0, m4=1), which absorbs small moves. wy +0.05 does (1348 -> 1663). + store2 = Store() + inst2 = Instance(store2, Module.from_file(store2.engine, MODULE), []) + ex2 = inst2.exports(store2) + mem2 = ex2["memory"] + argp2 = (ex2["__heap_base"].value(store2) + 0xF) & ~0xF + pert = list(VEHICLE_STATE) + pert[11] += 0.05 # wy, an axis the fold responds to + mem2.write(store2, struct.pack("<14f", *pert) + struct.pack("<4f", *RATE_SETPOINT), argp2) + tp2 = ex2["pulseengine:falcon-cascade/rate@0.7.0#tick"](store2, argp2) + t2 = struct.unpack("<4f", mem2.read(store2, tp2, tp2 + 16)) + p2 = ex2["pulseengine:falcon-cascade/mixer@0.7.0#mix"](store2, *t2) + pwm2 = struct.unpack("<4f", mem2.read(store2, p2, p2 + 16)) a2 = struct.unpack(" 0.35): {f2}" - f" {'DISTINCT — the fold tracks the input' if f2 != folded else 'IDENTICAL — VACUOUS, fold ignores state'}") + f2 = struct.unpack("mixer path and the composition plumbing, and nothing else. + print(" oracle scope: 4 of 18 input scalars move the fold (wx, wy, wz, sp.ry/rz);") + print(" the quaternion, position and velocity fields are INERT here.") return 0 if f2 != folded else 1 diff --git a/tools/cascade-differential/requirements.txt b/tools/cascade-differential/requirements.txt new file mode 100644 index 0000000..91f3360 --- /dev/null +++ b/tools/cascade-differential/requirements.txt @@ -0,0 +1,4 @@ +# The reference driver runs the fused core module under wasmtime's Python bindings. +# Unpinned, build-and-verify.sh exited 1 on a clean machine with ModuleNotFoundError — +# it preflighted cargo/wasm-tools/wac/wasmtime and the supplier artifacts, but not this. +wasmtime>=42,<49 diff --git a/tools/varve/check-drift.sh b/tools/varve/check-drift.sh index 6108845..9fa1470 100755 --- a/tools/varve/check-drift.sh +++ b/tools/varve/check-drift.sh @@ -23,21 +23,35 @@ 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 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")" v="$(varve run "$t" --version 2>/dev/null | head -1 | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1)" c="$(ci_pin "$t")" - # Compare only the sources that actually exist. A tool absent from a source is not - # drift — spar is legitimately not on this machine's PATH, and not every tool is - # pinned in ci.yml. Treating absence as disagreement would make this cry wolf. + # Compare only the sources that actually exist; not every tool is pinned in ci.yml, + # and treating absence as disagreement would make this cry wolf. + # + # CAVEAT, found by clean-room verification and NOT yet fixed: `ver` reads a version by + # running ` --version`. Tools that do not support that flag (spar, ordeal) read as + # absent even though the binary IS on PATH — so a PATH binary at a wildly divergent + # version silently drops OUT of the comparison. That is the inverse of crying wolf and + # is the more dangerous direction. `varve verify` currently reports 7 shadowed tools. seen=(); [ -n "$p" ] && seen+=("$p"); [ -n "$v" ] && seen+=("$v"); [ -n "$c" ] && seen+=("$c") uniq_n=$(printf '%s\n' "${seen[@]:-}" | sort -u | grep -c . || true) # A tool present in NO source is "absent", not "ok". Scoring it ok would be a vacuous # pass — it reports agreement where nothing was compared, which is how a checker ends # up green on a toolchain it never looked at. + # + # Clean-room verification found this stopped one step short in two ways, both fixed: + # - a tool found in exactly ONE source also scored "ok" — one value compared against + # nothing is not agreement either. It is now "single-source (not compared)". + # - if EVERY tool was absent the script still exited 0 with "no drift", i.e. a green + # verdict on a toolchain it never inspected. Tracked below and now an error. + n_sources=${#seen[@]} if [ "${uniq_n:-0}" -eq 0 ]; then st="absent (not checked)" - elif [ "${uniq_n:-0}" -eq 1 ]; then st="ok" + 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)) else st="DRIFT"; drift=1; fi printf '%-8s %-12s %-12s %-12s %s\n' "$t" "${p:--}" "${v:--}" "${c:--}" "$st" done @@ -53,5 +67,11 @@ a wrong citation costs a supplier's attention (AFD-045, meld#390). MSG exit 1 fi -echo "no drift: every tool agrees across the sources that define it." -echo "(rows marked 'absent (not checked)' were compared against nothing — they are not evidence.)" +if [ "$compared" -eq 0 ]; then + echo "NOTHING WAS ACTUALLY COMPARED: no tool was found in two or more sources." >&2 + echo "A 'no drift' verdict here would be green on a toolchain never inspected." >&2 + exit 2 +fi +echo "no drift: all $compared tool(s) found in 2+ sources agree." +[ "$single" -gt 0 ] && echo "($single row(s) 'single-source' and any 'absent' rows were compared against nothing — not evidence.)" +exit 0