Repository navigation
Conversation
…fail closed
Prompted by jess#292, which found an absence-assertion in jess's CI that
passed on an EMPTY log ("a gate that asserted the absence of a skip, read no
evidence, and said 0"). A read-only audit of relay's workflows and the scripts
they call found the same class twice here. Each is now proven both ways with
negative controls run against the old and the new gate.
1. spar.yml "Analyze system roots" — VACUOUS on missing input (not required).
`out=$(spar analyze ...) || true` then decided on `grep -qE ERROR` alone.
Measured with spar itself: an unreadable/missing .aadl makes spar EXIT 1 and
print "Cannot read <path>: No such file or directory" — no ERROR line — so
the gate passed having analysed nothing. Same for a `spar/*.aadl` glob that
stops matching, or a missing binary. Now the exit code is the verdict and the
grep a second opinion. `|| rc=$?` (not a bare call) because `shell: bash`
runs with -e and every root should still report.
case old new
real models (spar/*.aadl) pass pass
missing input file PASS fail
glob matching nothing PASS fail
No false-failure risk, measured: all five real roots exit 0 while printing
10-22 WARNINGs each.
2. scripts/check-float-discipline.sh — LATENT in the REQUIRED Clippy check.
`[ -d "$src" ] || continue` dropped a listed flight crate silently when it
had no source, and nothing counted what was scanned; run in an empty tree
the script printed "float discipline: OK" and exited 0. Every listed crate
must now contribute a scanned file (else CANNOT DETERMINE, fail), and OK
reports its denominator.
case old new
real tree pass pass — "scanned 22/22 flight crates, 52 .rs files"
empty tree PASS fail (22 crates flagged)
a listed crate renamed away skipped fail
f64 injected in flight code fail fail (detection preserved)
The f64 control was itself wrong the first time — appended at end-of-file,
it landed inside the gate's deliberate cfg(test)-to-EOF exemption and read
as "0 hits" for BOTH versions. Placed in real code (line 40, before the
first cfg(test) at 354) both catch it. Recorded because a control that
cannot fail looks exactly like a gate that cannot fail.
This script's own comment already records one earlier vacuous incident (BSD
awk has no \y); this is the second, of a different mechanism.
NAMED, NOT FIXED (assessed as guarded or out of scope for this change):
- verification-gate.yml:349 detects "verified nothing" by grepping for the
literal "# 0 artifact(s) matched". Guarded in practice (pipefail + the
runner fails on 0 tests), but wording-coupled: renaming the print silences
it. A positive-count assertion would be sturdier.
- check-verification-independence.sh prints OK on an unresolvable base ref
(git diff errors to stderr, `|| true`). The workflow's merge-base fallback
makes that need two bad sources, so mostly guarded.
- gazebo.yml's BIT-IDENTICAL check only fires if a DIFFERENTIAL line exists;
a run with the differential off passes it (the LOOP CLOSES/^PASS checks
still bound the empty-log case).
Refs pulseengine/jess#292
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
October 21, 2026 10:48
Contributor
Author
|
Superseded by #588 — this exact commit is cherry-picked there ( |
auto-merge was automatically disabled
October 21, 2026 15:05
Pull request was closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Prompted by jess#292 (an absence-assertion that passed on an empty log). A read-only audit of relay's workflows + called scripts found the class twice; both fixed and proven both ways against old and new.
1.
spar.ymlAnalyze system roots (not required) —|| true+grep ERRORonly. Measured: a missing.aadlmakes spar exit 1 printingCannot read …with no ERROR line → gate passed having analysed nothing.No false-failure risk: all 5 roots exit 0 with 10–22 WARNINGs each.
2.
check-float-discipline.sh(inside required Clippy) — a listed crate with no source was skipped silently; an empty tree printed OK.f64in flight code(The
f64control was wrong the first time — it landed in the gate's owncfg(test)exemption and read 0 hits for both; placed in real code, both catch it.)Named, not fixed: verification-gate's "0 artifacts" detector is wording-coupled; the independence script prints OK on a bad base ref (mostly guarded upstream); gazebo's BIT-IDENTICAL check is skipped when the differential is off. Details in the commit.
Refs pulseengine/jess#292
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG