fix: correct stale prose in the cascade oracle (it claimed 3 stages were missing) + add an image provenance pin

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

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.

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