fix(verus): the gate enforcing the proofs has never passed — and it was hiding 2 broken ones - #377
Merged
Merged
Conversation
…it was hiding 2 v1.135 added verus.yml to enforce the Verus track, after finding 19 proofs defined and never run. I verified the workflow FIRES. I never verified it PASSES. It has failed on every run on main since the commit that added it: 2026-08-26 10:42 b777ba9 failure <- the commit that ADDED it 2026-08-26 21:53 32528a5 failure 2026-09-01 16:01 53ef471 failure 2026-09-02 06:52 cf19c79 failure 2026-09-02 11:45 dacd91c failure 2026-09-02 20:58 34cc0fd failure 2026-09-07 05:05 9a5a912 failure Seven runs, zero successes, twelve days. Invisible because `Verus` is not one of main's seven required contexts, so its failure blocks nothing. Meanwhile the rivet gate reports `[enforced-by-verus-gate]` for 16+ artifacts' verus steps — a claim that the Verus CI check runs them. It was false the whole time. TWO SEPARATE PROBLEMS, separated by contrast rather than by guessing: aarch64-apple-darwin (local) 17/19 PASSED, 2 real failures x86_64-unknown-linux-gnu (CI) 0/19, every one aborting in <=0.1s with error[E0463]: can't find crate for `std` The linux half is upstream — the bundled Verus rust sysroot lacks the target std. Filed as pulseengine/rules_verus#25, including that their fetch-time check verifies `libcore-*.rlib` only and not `libstd-*.rlib`, so a partial sysroot passes the check and fails at first use. THIS COMMIT FIXES THE OTHER HALF — the two genuine relay defects the unrunnable gate was concealing: relay_nid bitpack.rs:22 — 3x error[E0507]: cannot move out of `msg.id_type` / `msg.ua_type` / `msg.status` behind a shared reference. The proofs were SOUND ("7 verified, 0 errors"); the crate did not COMPILE under Verus. CAUSE: dual-tree drift. The verus tree had `#[derive(PartialEq, Eq)]` where the plain tree has `#[derive(Clone, Copy, PartialEq, Eq, Debug)]`, and `enum as u8` behind `&BasicId` needs Copy. FIX: restore Clone, Copy on IdType, UaType, OperationalStatus, MessageType — parity with the plain tree. relay_mavlink heartbeat.rs:41 — error: expression has mode spec, expected mode exec, on `const FALCON_AUTOPILOT_ID: u8 = MavAutopilot::Invalid as u8`. CAUSE: Verus rejects an enum-to-integer cast in exec mode. Adding Copy did NOT fix it — recorded because the obvious fix failing is worth knowing. FIX: move the const outside the `verus!` block. It carries no proof obligation; items outside are external to Verus, and Rust item order is irrelevant so the exec code inside still resolves. MEASURED AFTER: bazel test $(bazel query 'kind("verus_test rule", //:*)') 19 tests, 19 PASSED, exit 0 (aarch64-apple-darwin) cargo test -p relay-nid -p relay-mavlink 99 passed; 0 failed (plain trees unaffected) HONEST SCOPE: verified on darwin-arm64 ONLY. CI cannot confirm these until rules_verus#25 lands, because the linux runner cannot execute any Verus target. The artifacts stay `implemented` and claim no CI enforcement. Reporting "19/19 pass" without "on one platform, off CI" would repeat the exact error this change exists to correct. VGATE-P03 records the pattern, now at its third level: P01 checks a cited proof is in the matrix (claimed -> exists); P02 checks a matrix proof is cited (runs -> recorded); P03 requires the gate cited as the enforcer to have actually passed (exists -> passes). Each layer was added after the previous turned out to be satisfiable while the property underneath was false. Two-commit rule: code change, nothing promoted past `implemented`. rivet validate exit 0; FV-RELAY-VGATE-003's 4 CI steps PASS. Refs #6 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
September 7, 2026 07:10
PR #377's gate went red on FV-RELAY-VCHAIN-001, and not because of anything in #377 — VGATE-003's own four steps all PASS. The crosswalk step fails because the runner cannot execute three of the four tracks. Its own output says so: Kani : PRESENT (7 harnesses ...) — cargo-kani not installed Verus : RUN ❌ //:relay_sc_verus_test Rocq : RUN ❌ Lean : PRESENT A track that ran FAILED — see logs above. The Verus half additionally CANNOT work on linux at all until pulseengine/rules_verus#25 — the bundled sysroot lacks the target std, which is the whole finding #377 exists to record. So the crosswalk was re-reporting a known-broken toolchain through a second, worse channel. Each track already has a dedicated workflow that is its real enforcer. This is the same arrangement as `cargo kani -p` (enforced-by-kani-gate) and `bazel test //:*_verus_test` (enforced-by-verus-gate): the gate defers, the dedicated job runs it. `verify-chain.sh` now classifies bench-only by COMMAND SHAPE like every other such decision, anchored at line start so a step merely NAMING the script is not silently skipped. WHY IT SURFACED NOW, which is the part worth keeping: this step had not been executed in recent memory, because no PR's Verify-Filter had selected FV-RELAY-VCHAIN-001. #377's narrow `(has-tag "verus")` filter selected it and it failed immediately — exactly how #375's filter revealed FV-FALCON-RELEASE-001's three never-executed `gh`/`cosign` steps. Two releases running, a narrowed filter has found evidence that had quietly never run. The default `(has-tag "falcon")` sweep is not the whole tree, and artifacts outside it are unexercised. Over-match checked, not assumed: swept every step in every artifact — exactly 1 newly classifies bench-only, and it is this one. Full unfiltered dry-run exits 0. Refs #380, rules_verus#25 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
…r ran Found while answering "how much verification do I actually have". The gate's default was the bare string `--type sw-verification`, and that single word was a scope hole nobody had looked at. MEASURED: type artifacts steps swept? sw-verification 215 554 yes sys-verification 36 59 NO unit-verification 38 38 NO TOTAL 289 651 outside every gate run: 74 artifacts / 97 steps = 15% of all verification steps Among the invisible: 32 of the 36 artifacts that cite a Verus proof. The gate had been reporting `enforced-by-verus-gate` for 4 of them while 32 more were not even enumerated. This is the same failure shape as #342 (a filter matching zero artifacts passed), #375 (three `gh`/`cosign` steps that had never executed) and #377 (a crosswalk that could not run) — on a THIRD axis. Tags, command shape, and now TYPE. Each time the gate swept a subset and reported as though it had swept the tree. FIX: `--type` takes a comma-separated list and defaults to all three. Ordering preserved, duplicates dropped, so a type listed twice cannot double-run a step. COST OF CLOSING IT, measured before changing the default rather than after: both previously-unswept types are green today — `--type unit-verification` 16 artifacts exit 0, `--type sys-verification` 36 artifacts exit 0. So this widens what runs without smuggling in a red gate. On the same `(has-tag "verus")` filter the sweep goes 6 -> 22 artifacts, 0 FAIL, exit 0. Worth stating plainly: the 16 unit-verification artifacts it now sweeps consist ENTIRELY of steps that defer to the Verus gate, and that gate has never passed (rules_verus#25). Sweeping them makes their existence visible; it does not make them enforced. That gap is SWREQ-RELAY-VGATE-P03, still open. Refs #380 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
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.
Verify-Filter: (has-tag "verus")
v1.135 added
verus.ymlto enforce the Verus track, after finding 19 proofsdefined and never run. I verified the workflow FIRES. I never verified it PASSES.
It has never once succeeded
b777ba9832528a5e53ef471acf19c79fdacd91c234cc0fd69a5a912fSeven runs, zero successes, twelve days. Invisible because
Verusis not oneof main's seven required contexts, so its failure blocks nothing.
Meanwhile the rivet gate prints
[enforced-by-verus-gate]for the verus steps in16+ artifacts — a claim that the Verus CI check runs them. False the whole time.
Two separate problems, separated by contrast rather than guessed
The linux half is upstream — the bundled Verus rust sysroot lacks the target
std. Filed as pulseengine/rules_verus#25, including the detail that their
fetch-time check verifies
libcore-*.rlibbut notlibstd-*.rlib, so a partialsysroot passes the check and then fails at first use.
This PR fixes the other half — 2 real defects the unrunnable gate was hiding
relay_nidThe proofs were sound —
verification results:: 7 verified, 0 errors. Thecrate simply did not compile under Verus.
Cause: dual-tree drift. The verus tree had
#[derive(PartialEq, Eq)]wherethe plain tree has
#[derive(Clone, Copy, PartialEq, Eq, Debug)], andenum as u8behind&BasicIdneedsCopy.relay_mavlinkVerus rejects an enum→integer cast in exec mode. Adding
Copydid not fixit — recorded because the obvious fix failing is worth knowing. The const is
now declared outside the
verus!block: it carries no proof obligation, itemsoutside are external to Verus, and Rust item order is irrelevant so the exec code
inside still resolves it.
Measured after
Honest scope — please read this bit
These fixes are verified on darwin-arm64 only, locally. CI cannot confirm
them until rules_verus#25 lands, because the linux runner cannot execute any
Verus target at all. The artifacts stay
implementedand claim no CIenforcement.
Reporting "19/19 pass" without "on one platform, off CI" would repeat the exact
error this change exists to correct.
The pattern, now at its third level
Each layer was added after the previous one turned out to be satisfiable while
the property underneath was false.
Two-commit rule: code change, nothing past
implemented.rivet validateexit 0;FV-RELAY-VGATE-003's 4 CI steps PASS.Refs #6
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG