Skip to content

fix(verus): the gate enforcing the proofs has never passed — and it was hiding 2 broken ones - #377

Merged
avrabe merged 6 commits into
mainfrom
fix/verus-proofs-that-never-ran
Sep 10, 2026
Merged

fix(verus): the gate enforcing the proofs has never passed — and it was hiding 2 broken ones#377
avrabe merged 6 commits into
mainfrom
fix/verus-proofs-that-never-ran

Conversation

@avrabe

@avrabe avrabe commented Sep 7, 2026

Copy link
Copy Markdown
Contributor

Verify-Filter: (has-tag "verus")

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 never once succeeded

run commit
2026-08-26 10:42 b777ba98 failure ← the commit that added it
2026-08-26 21:53 32528a5e failure
2026-09-01 16:01 53ef471a failure
2026-09-02 06:52 cf19c79f failure
2026-09-02 11:45 dacd91c2 failure
2026-09-02 20:58 34cc0fd6 failure
2026-09-07 05:05 9a5a912f 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 prints [enforced-by-verus-gate] for the verus steps in
16+ artifacts — a claim that the Verus CI check runs them. False the whole time.

Two separate problems, separated by contrast rather than guessed

aarch64-apple-darwin (local)   17/19 PASSED, 2 real failures
x86_64-unknown-linux-gnu (CI)  0/19, every one aborting in <=0.1s
                               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 the detail that their
fetch-time check verifies libcore-*.rlib but not libstd-*.rlib, so a partial
sysroot passes the check and then fails at first use.

This PR fixes the other half — 2 real defects the unrunnable gate was hiding

relay_nid

error[E0507]: cannot move out of `msg.id_type` which is behind a shared reference
  --> crates/relay-nid/src/bitpack.rs:22:16

The proofs were soundverification results:: 7 verified, 0 errors. The
crate simply 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.

relay_mavlink

error: expression has mode spec, expected mode exec
  --> crates/relay-mavlink/src/heartbeat.rs:41:37
41 | pub const FALCON_AUTOPILOT_ID: u8 = MavAutopilot::Invalid as u8;

Verus rejects an enum→integer cast in exec mode. Adding Copy did not fix
it
— recorded because the obvious fix failing is worth knowing. The const is
now declared 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 it.

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 — 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 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.

The pattern, now at its third level

check shape
VGATE-P01 a cited proof is in the matrix claimed → exists
VGATE-P02 a matrix proof is cited runs → recorded
VGATE-P03 the gate cited as enforcer actually passed exists → passes

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 validate exit 0;
FV-RELAY-VGATE-003's 4 CI steps PASS.

Refs #6

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

…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
avrabe enabled auto-merge (squash) September 7, 2026 07:10
avrabe and others added 5 commits September 10, 2026 18:42
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
@avrabe
avrabe merged commit 0bd85c2 into main Sep 10, 2026
58 checks passed
@avrabe
avrabe deleted the fix/verus-proofs-that-never-ran branch September 10, 2026 21:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant