Repository navigation
fix(verus): paren-wrap struct literal in ring_buf ensures (CI red 8+ runs) - #31
Merged
Merged
Conversation
Verus's parser treats unparenthesized struct literals in ensures
clauses as statement-level constructs and rejects them. Without the
parens, `bazel test //:verus_test` fails to even parse src/ring_buf.rs,
which then poisons every per-module standalone run (`--verify-module
foo` parses the whole crate from src/lib.rs first).
CI's formal-verification.yml verus job has been failing on main for
8+ consecutive runs (2026-04-24 onward) with this exact parse error.
This 1-line fix restores the green-CI claim "805 verified, 0 errors"
and unblocks anyone trying to run the proofs standalone.
Sweep for the same pattern (==> ... === StructName{ ...) across
src/ and proofs/ found only this one site.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
3 tasks
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
After fix(ring_buf) unblocked the parse, Verus actually ran and the
empty proof body of `lemma_trailer_reserve_fits_u32` failed:
error: postcondition not satisfied
--> src/heap.rs:856
856 | (CHUNK_TRAILER_BYTES as u64) * (chunks as u64) <= u32::MAX as u64,
Verus's SMT layer doesn't multiply variables by constants on its
own. Same idiom as systick::ticks_to_cycles_checked uses: invoke
`vstd::arithmetic::mul::lemma_mul_inequality` to lift the
precondition `chunks ≤ MAX_CHUNKS` over multiplication by
CHUNK_TRAILER_BYTES, then constant-fold the upper bound.
chunks ≤ MAX_CHUNKS = 65535
⇒ chunks * CHUNK_TRAILER_BYTES ≤ 65535 * 8 = 524280 ≤ u32::MAX
Discovered when CI on PR #31 made it past the parse error and into
real verification for the first time in 8+ runs.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 3, 2026
…kstart (#32) Punch-list items from the second-pass "Shan reviewer" audit. Lands the in-progress quickstart doc together with the surrounding doc hygiene needed for it to be honest: 1. AGENTS.md L107-121 — drop `nix develop --command` prefix from the four bazel test invocations. There is no flake.nix in the repo; the prefix was misleading. Replaced with plain `bazel test ...` plus a one-paragraph note that nix-build must be on PATH (and how to put it there) because rules_rocq_rust pulls Nix for toolchain resolution. 2. .bazelversion — new file pinning Bazel 9.1.0 (matches what bazelisk currently resolves to on Linux runners and locally on macOS). Without the pin, Bazelisk's default would silently drift the day a new release lands. 3. docs/safety/verification-honesty.md — append a "Trusted code: external_body, assume_specification, --no-cheating" section. Closes the only real correctness gap in the honesty story: the doc was silent on Verus's trusted-base annotations. New table enumerates 133 external_body instances + 2 assume_specification calls per file (net_buf 36, pm 22, ipc 22, mmu 20, usage 18, thread_lifecycle 5, sched 4, poll 3, mpu 3). Notes that today's CI does NOT pass --no-cheating, intentionally, and that a --no-cheating run would correctly fail until those trust units are discharged. 4. README.md L21 — anchor the headline "805 verified, 0 errors" claim with a footnote linking to verification-honesty.md and stating that the number is gated by the formal-verification.yml CI job (i.e., when that job is red, the number is stale until it goes green again). No change to the number itself; PR #31 is the companion fix that gets the Verus job back green. 5. docs/research/verus-quickstart-for-shan.md — new file. The hand-off doc for arsene1995 (Shan) following microsoft/verus-proof-synthesis#45. Includes the two table-cell patches from the punch list: - --verify-module: caveat that Verus parses the whole crate from src/lib.rs before isolating to the named module, so a parse error elsewhere poisons even targeted runs. - --no-cheating: now lists assume_specification alongside assume / admit / external_body, and points at the trusted- base inventory in verification-honesty.md. Companion to PR #31 (which fixes the parse error in src/ring_buf.rs that has had formal-verification.yml red on main since Apr 24). This PR is doc/process hygiene only — no Rust source touched. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 10, 2026
…69×→1.50× (#159) synth 0.38.0 ships the mask-elision lever gale filed (synth#686/#692, `SYNTH_SHIFT_MASK_ELIDE`, flag-off): it elides #682's mod-32 `AND rm,#31` shift mask where the amount is provably <32 — exactly gale's gust_mix (Q8 constant shifts). Re-dissolved cm3+cm4 with the flag: fn-only 0.675 → 0.600 ticks/call (−11%), .text 82 → 68 B (−17%), ratio vs native LLVM 1.69× → 1.50× — best measured on the shipped path. Correctness-gated: gust_floor_bench soundness `mix_proven ≡ mix_native ≡ gust_mix` over [524,1524] PASSES; proof-carrying floor still 0.45×; in-range dissolved 1.55× → 1.40×. silicon_bench links cleanly for thumbv7em. NOTE: the relocatable .o grew 432 → 496 B despite the smaller .text — that's 0.38.0's new ELF metadata (#656 STB_LOCAL internal symbols + #637 .ARM.attributes), dropped/merged at link time, so flash footprint tracks the 68 B .text. 0.38.0 DEFAULT (flag-off) is perf-neutral (1.69×, .text 82) — the release adopt is safe; the win needs the flag. build.rs recipe updated. Ladder: 1.81× (stale) → 1.69× (0.37.1, #157) → 1.50× (0.38.0 elide) → 0.45× (clamp-elision floor, synth#494 phase-2). Reporting the measured 1.50× to synth#686 as the arc toward default-on. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
1 participant
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.
Summary
CI's `formal-verification.yml` Verus job has been red on main for 8+ consecutive runs since 2026-04-24, with the same parse error every time:
```
src/ring_buf.rs:598
buf_size == 0 ==> result === ClaimDecision { claim_size: 0, buffer_offset: 0 },
^^^^^^^^^^^^^^^^...
error: unparenthesized struct literal in spec position
```
The README's headline claim "39/39 modules, 805 verified, 0 errors" has been technically false on main for the same window. This 1-line fix restores it.
Root cause
Verus's parser treats unparenthesized struct literals in `ensures` clauses as statement-level constructs and rejects them. The fix is to wrap the literal in parens:
```diff
```
Same rule that requires `return (Foo {})` instead of `return Foo {}` in some Rust contexts — Verus is stricter on the spec side.
Why it's a wider blocker than CI
`verus --verify-module foo` still parses the whole crate from `src/lib.rs` before isolating to module `foo`. So the ring_buf parse error currently poisons every per-module standalone run, not just the ring_buf one. Anyone trying to run the proofs from a fresh checkout to bench / experiment / measure (Shan's VeruSAGE-Bench follow-up scenario, for one) hits this wall on the first invocation.
Sweep
`grep -nE '==> .* === [A-Z][a-zA-Z_]+ {' src/.rs proofs/*` returned only this one site. Other near-matches in the repo are control-flow predicates (`if X == K_FOREVER_TICKS`), not struct literals.
Test plan
🤖 Generated with Claude Code