From 3f81be5f7e1efb42ce1a01c88b5a835b7af10c04 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 27 Aug 2026 12:52:26 +0200 Subject: [PATCH] fix: correct stale prose in the cascade oracle (it claimed 3 stages were missing) + add an image provenance pin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SELF-VERIFY (overdue) came back 7/7 CONFIRMED, with claim 1 STRENGTHENED: the verifier rebuilt the fused cascade independently (0 skips, 5/5 T symbols), added a negative control jess had not run (the v0.59.0 RELEASE synth on the same input gives 3 skips, 0 T symbols), and established that THE COMMITTED IMAGE IS BIT-REPRODUCIBLE — a fresh pipeline build yields a byte-identical SHA256 from two independent builds. THE REAL INCONSISTENCY: the oracle's own header comment still described the previous 2-of-5 image — "loom 1.2.0 / synth 0.55 / 65,452 B" and, flatly false of the committed ELF, "iekf/position/attitude entry points are NOT in this image ... the single remaining upstream gate". The test cases were correct; only the prose lied. It mattered because THIS FILE IS THE EVIDENCE cited upstream for the 5/5 claim. The stale 214,696 instruction count also survived in the robot and one TEST-PIX-031 paragraph (correct: 213,439). Both corrected. STRUCTURAL GAP (the more valuable finding): CI runs the robot against the COMMITTED ELF and never rebuilds the meld->loom->synth chain — so CI gated EXECUTION but not PROVENANCE, and a hand-swapped image would have passed. Closed half of it with an IMAGE PROVENANCE PIN (SHA256 asserted in the robot, negative-controlled — a mutated digest fails). Honest scope stated in the file: the pin detects that the bytes changed, it does NOT prove the pipeline produced them. The full gate needs meld/loom/synth in the runner. Pinning is meaningful here precisely because the image was shown bit-reproducible; pinning an unreproducible blob would be theatre. Verified: oracle now 3/3 OK; provenance pin negative-controlled (mutated digest fails); rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/findings.yaml | 46 +++++++++++++++++++ artifacts/phase2-pixhawk.yaml | 3 +- .../renode/cascade-m7/falcon-cascade-m7.robot | 32 +++++++++---- 3 files changed, 72 insertions(+), 9 deletions(-) diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index bdc0510..eaa7539 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -1584,6 +1584,52 @@ artifacts: - type: traces-to target: REQ-PIX-001 + - id: AFD-041 + type: ai-found-defect + title: Clean-room verify of the 5/5 cascade claims — 7/7 CONFIRMED and one claim STRENGTHENED (bit-reproducible image), but the oracle's own prose was STALE and CI gated execution without provenance + status: resolved + description: > + 2026-08-27 SELF-VERIFY (overdue - four features since the last, and two claims had gone UPSTREAM + to synth#1069, so an overclaim would have been costly). Fresh-context subagent, no inherited framing. + ALL SEVEN CLAIMS CONFIRMED, and claim 1 came back STRONGER THAN CLAIMED: the verifier rebuilt the + fused cascade from the five .wasm inputs independently (0 skips, 5/5 T symbols), ADDED a negative + control jess had not run (the v0.59.0 RELEASE synth on the SAME fused input gives exit=1, 3 skips, + 0 T symbols), and established something jess had not: THE COMMITTED IMAGE IS BIT-REPRODUCIBLE - a + fresh pipeline build yields a byte-identical SHA256 (c692f50d..., 94,907 B) from two independent + builds. Also confirmed: the source-built synth genuinely differs from the release build (md5 + 1a3244 vs 6cdf7f despite both reporting 0.59.0) and the fixture discriminates exactly; the oracle + is NON-VACUOUS (both injected mutants fail with real read-back values); the publish-gate SIGPIPE + fix holds with 6/6 positive and the negative control still biting; rivet PASS (197 warnings); + no stranded branches this time (git ls-remote = main only, 62 PRs all merged); no CI gate bypassed. + *** THE REAL INCONSISTENCY - STALE PROSE IN THE EVIDENCE ITSELF ***: the header comment of + hardware/renode/cascade-m7/falcon-cascade-m7.robot still described the PREVIOUS 2-of-5 image - + "loom 1.2.0 / synth 0.55 / 65,452 B" and, flatly false of the committed ELF, "Three functions + remain skipped ... iekf/position/attitude entry points are NOT in this image - that is expected + and is the single remaining upstream gate". The test cases were correct and non-vacuous; only the + prose lied. It mattered because THIS FILE IS THE EVIDENCE cited upstream for the 5/5 claim: anyone + opening it to check would read a comment saying three stages were missing. Also the instruction + count 214,696 (the 2-of-5 figure) survived in both the robot and one paragraph of TEST-PIX-031 + while the updated paragraph said 213,439. Both corrected. + *** STRUCTURAL GAP FOUND (the more valuable finding) ***: CI runs the robot against the COMMITTED + ELF and never rebuilds the meld->loom->synth chain, so CI gated EXECUTION but not PROVENANCE - a + hand-swapped or drifted image would have passed. Closed HALF of it: an IMAGE PROVENANCE PIN + (SHA256 asserted in the robot, negative-controlled - a mutated digest fails). HONEST SCOPE stated + in the file: the pin detects that the committed bytes changed; it does NOT prove the pipeline + produced them. The full gate (rebuild the chain in CI) needs meld/loom/synth in the runner and is + tracked as follow-on work. Pinning is meaningful here precisely BECAUSE the image was shown + bit-reproducible - pinning an unreproducible blob would be theatre. + METHOD NOTE: the verifier also observed main's HEAD CI was QUEUED when it started (so the claim + was not yet true at that moment) and polled it to completion (5/5 jobs green) rather than + reporting the queued state as a pass - the same never-on-pending discipline, applied to jess. + tags: [self-verify, clean-room, oracle, provenance, reproducibility, falcon, cascade] + fields: + detected-by: fresh-context clean-room subagent over the 5/5 cascade claims, 2026-08-27 + severity: minor + triage-status: closed + links: + - type: traces-to + target: REQ-PIX-001 + - id: AFD-040 type: ai-found-defect title: gale-nano 0.7.0 passes the gate and holds its invariant via the SOUND path; meld now REFUSES the silent-overlap fuse; loom 1.4.1 neutral; and jess's own publish-gate had a SIGPIPE false-negative diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml index 5bb0f26..a5cb69e 100644 --- a/artifacts/phase2-pixhawk.yaml +++ b/artifacts/phase2-pixhawk.yaml @@ -568,7 +568,8 @@ artifacts: 0x20002238=0x3E800000 (0.25f), 0x2000223C=0x42480000 (50.0f) - the last two are recognisable f32 control constants. B EXECUTION PROGRESS - >100k instructions retired AND PC inside the image .text (0..0xFB29). - Observed PC 0x16C (immediately below mixer#mix at 0x178) and 0x344A8 = 214,696 instructions. + Observed PC 0x16C and 0x341BF = 213,439 instructions (the 214,696 figure was the earlier + 2-of-5 image; corrected after clean-room verification flagged the inconsistency). Discriminating: a never-started image retires ~0; a HardFault lockup pins PC at a vector. NEGATIVE-CONTROLLED: both assertions were re-run with a wrong expected word (0xDEADBEEF) and an impossible instruction threshold - BOTH FAILED, so neither is vacuous. diff --git a/hardware/renode/cascade-m7/falcon-cascade-m7.robot b/hardware/renode/cascade-m7/falcon-cascade-m7.robot index fbe3706..5c211a7 100644 --- a/hardware/renode/cascade-m7/falcon-cascade-m7.robot +++ b/hardware/renode/cascade-m7/falcon-cascade-m7.robot @@ -10,13 +10,17 @@ Test Setup Boot Falcon Cascade # # relay falcon-v1.134.1 OCI components (iekf position attitude rate mixer) # -> meld 0.52.0 fuse --memory shared --pack-rebase (5 pages 320 KB -> 1 page 64 KB) -# -> loom 1.2.0 optimize -# -> synth 0.55 compile -t cortex-m7dp --cortex-m (self-contained EXEC, 65,452 B) +# -> loom 1.4.1 optimize +# -> synth (main, increments 1+2 / PR#1073+#1075) compile -t cortex-m7dp --cortex-m +# (self-contained EXEC, 94,907 B) # -# The image exports pulseengine:falcon-cascade/{rate@0.7.0#tick, mixer@0.7.0#mix} as real -# defined symbols. Three functions remain skipped (all GI-FPU-002 VFP register exhaustion, -# synth#881) so iekf/position/attitude entry points are NOT in this image — that is expected -# and is the single remaining upstream gate. +# The image exports ALL FIVE cascade stages as real defined symbols: +# attitude@0.7.0#tick · ekf@0.7.0#estimate · mixer@0.7.0#mix · position@0.7.0#tick · rate@0.7.0#tick +# ZERO skips. synth increment 2 (PR#1075, frame-homed overflow VFP locals) removed the 13->14 +# homed-local wall that was GI-FPU-002; there is no remaining upstream gate on this path. +# (This block previously described a 2-of-5 image and said three stages were missing — stale +# after the 5/5 result landed, and caught by clean-room verification. Kept accurate here because +# THIS FILE IS THE EVIDENCE cited upstream for the 5/5 claim.) # # WHAT THIS ASSERTS, and why each assertion can actually FAIL: # A. LINEAR-MEMORY INIT — the reset handler copies 0xd061 (53,345) bytes of wasm linear @@ -28,8 +32,7 @@ Test Setup Boot Falcon Cascade # fault. Asserted as: >100k instructions retired, and PC landing inside the image .text # (0x0..0xFB29). Both are discriminating — a never-started image retires ~0 instructions, # and a HardFault lockup pins PC at a fault vector rather than in the export region. -# Observed: PC 0x16C (immediately below mixer@0.7.0#mix at 0x178), 0x344A8 = 214,696 -# instructions retired. +# Observed: PC 0x16C, 0x341BF = 213,439 instructions retired. # NOTE — what this deliberately does NOT assert, and why: the reset handler also writes # CPACR (0xE000ED88) |= 0x00F00000 to enable CP10/CP11, which is the FPU-enable that a # cortex-m7dp hard-float image depends on. That register is NOT readable through @@ -42,7 +45,16 @@ Test Setup Boot Falcon Cascade # argument marshalling; that is the next rung, and it is where relay's SIL reference # (converged 0.193 s, steady-state |err| 0.0059 rad/s) becomes the comparison baseline. +# IMAGE PROVENANCE PIN. Clean-room verification flagged that CI runs this robot against the +# COMMITTED ELF and never rebuilds the meld->loom->synth chain — so CI gated EXECUTION but not +# PROVENANCE, and a hand-swapped or drifted image would still pass. This pin makes a silent swap +# fail loudly. HONEST SCOPE: it detects that the committed bytes changed; it does NOT prove the +# pipeline produced them. The full gate (rebuild the chain in CI) needs meld/loom/synth in the +# runner and is tracked separately. The image IS bit-reproducible from the pipeline — a fresh +# build produced this exact digest — which is what makes pinning it meaningful rather than +# pinning an unreproducible blob. *** Variables *** +${IMAGE_SHA256} c692f50dc6cc1ee7994d6b072ad50b236456c04bb169da21c1c5f49ba91af193 ${ELF} ${CURDIR}/falcon-cascade-m7.elf ${PLATFORM} ${CURDIR}/../pixhawk6xrt.repl ${TEXT_END} 0xFB29 @@ -59,6 +71,10 @@ Memory Word Should Be Should Contain ${v} ${expected} *** Test Cases *** +Committed image is the one this oracle was written against + ${actual}= Run shasum -a 256 ${ELF} + Should Contain ${actual} ${IMAGE_SHA256} + Fused falcon cascade initialises linear memory on the RT1176 M7 Execute Command emulation RunFor "0.05" # non-zero probes — a vacuous zero-probe could not distinguish copied from never-ran