fix(verus): correct vstd lemma paths + matches!→is + lemma_div_multiples_vanish#212
Merged
fix(verus): correct vstd lemma paths + matches!→is + lemma_div_multiples_vanish#212
Conversation
📐 Rivet artifact deltaNo artifact changes in this PR. Code-only changes (renderer, CLI wiring, tests) don't touch the artifact graph. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
⚠️ Performance Alert ⚠️
Possible performance regression was detected for benchmark 'Rivet Criterion Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.
| Benchmark suite | Current: f9607e6 | Previous: 77fa2e0 | Ratio |
|---|---|---|---|
store_lookup/100 |
2209 ns/iter (± 64) |
1685 ns/iter (± 23) |
1.31 |
store_lookup/1000 |
26279 ns/iter (± 771) |
19210 ns/iter (± 128) |
1.37 |
traceability_matrix/1000 |
61804 ns/iter (± 2798) |
40182 ns/iter (± 516) |
1.54 |
diff/100 |
64084 ns/iter (± 327) |
51859 ns/iter (± 1050) |
1.24 |
diff/1000 |
711693 ns/iter (± 4114) |
567495 ns/iter (± 4051) |
1.25 |
query/100 |
779 ns/iter (± 3) |
645 ns/iter (± 1) |
1.21 |
query/1000 |
7218 ns/iter (± 35) |
5456 ns/iter (± 91) |
1.32 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…les_vanish Three concrete bugs in verus_specs.rs identified by the parallel research agent sweep (REQ-004 follow-up): 1. vstd lemma paths: mul_internals→mul, div_internals→div_mod. The internals modules are under vstd::arithmetic::internals:: and don't expose those names — rust_verify rejects with "unresolved import" before reaching SMT (matches the "FAIL in 0.1s" symptom on the previous run). 2. lemma_div_is_ordered alone proves (covered*100)/total <= (total*100)/total, but to conclude (covered*100)/total <= 100 we also need (total*100)/total == 100. Add the missing lemma_div_multiples_vanish(100, total) step. 3. matches! macro is not in Verus's spec subset. Replace matches!(x.severity, GhostSeverity::Error) with x.severity is Error (Verus's enum-discriminant operator). Validates: REQ-004 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
fix/verus-vstd-paths-and-matches
branch
from
1f48446 to
ee27b98
Compare
Verus's lemma_div_is_ordered signature requires int args: fn lemma_div_is_ordered(x: int, y: int, z: int) But `covered * 100` and `total * 100` are `nat * int` (since covered and total are nat), so the call failed with E0308: expected `int`, found `nat` at rivet-core/src/verus_specs.rs:249:13 (covered * 100, total * 100) Surfaced via the bazel test.log artifact upload (PR #209) — without it the Verus failure was just "FAIL in 0.4s" with no detail. Cast both products as int explicitly. The third argument `total as int` was already correctly cast. Verifies: REQ-004
Verus couldn't auto-infer triggers for the forward-implies-backward and
backward-implies-forward forall quantifiers in
backlink_symmetric_invariant. Without a trigger Verus rejects the
quantifier at parse-time:
error: Could not automatically infer triggers for this quantifier.
--> verus_specs.rs:155:9
156 | g.backward.contains_key(tgt)
157 | && 0 <= j < g.backward[tgt].len()
Annotate `g.forward[src][i]` and `g.backward[tgt][j]` (the let-binding
RHS in each forall body) as #[trigger] — these terms mention all
quantified variables and serve as the canonical instantiation pattern
for the SMT solver.
Verifies: REQ-004
Verus rejects the exists|i| and exists|mid, i| quantifiers in the
reachable_in spec function (rivet-core/src/verus_specs.rs:345-355)
without an explicit trigger:
error: Could not automatically infer triggers for this quantifier.
--> verus_specs.rs:350:44
Annotate `g.forward[src][i]` with #[trigger] in both quantifiers (as
the access expression that mentions all bound variables).
Verifies: REQ-004
Verus rejected the trigger #[trigger] g.forward[src][i] in the
exists|mid, i| quantifier because it doesn't cover the variable mid
("trigger does not cover variable mid").
Since mid is defined by `g.forward[src][i].target == mid`, it's
redundant — substituting g.forward[src][i].target for mid eliminates
the variable entirely and reduces the quantifier to exists|i| where
the existing trigger suffices.
Semantically equivalent; Verus-syntactically clean.
Verifies: REQ-004
Same pattern as backlink_symmetric_invariant at lines 141-166: the require-clause foralls need explicit triggers on the indexed access expressions g.forward[src][i] and g.backward[tgt][j], plus triggers on the inner exists access expressions. Verifies: REQ-004
The lemma's requires clauses are literally the two conjuncts of backlink_symmetric (compare requires lines 179-203 with backlink_symmetric's forall bodies at lines 141-166). Explicit assert(backlink_symmetric(g, s)) lets Verus connect the trigger patterns of the requires-side foralls to the spec-function-side foralls and discharge the postcondition. If Verus still rejects (e.g., because the spec function's auto-chosen triggers differ from the requires-side annotated triggers), fallback options would be: (a) annotate spec-function-side triggers to match, (b) introduce intermediate assertions for each forall conjunct, (c) use `assume()` as a documented gap. Verifies: REQ-004
After 8 iteration cycles fixing syntax errors (vstd paths, matches!→is, nat→int casts, 4 trigger annotations, mid-elimination), the spec now parses and Verus reaches actual SMT verification. The remaining gap is that lemma_build_yields_symmetric's requires clauses are logically equivalent to backlink_symmetric's body, but Verus's trigger inference picks different patterns for the requires-side foralls (with our custom #[trigger] annotations) than for the spec-function definition (with auto-chosen triggers), and cannot bridge them without manually-written instantiation lemmas in the body. Mirroring the Rocq Admitted pattern landed in proofs/rocq/Schema.v during the same sweep (PR #210): document the gap as a future REQ-004 follow-up and use assume() to keep the rest of the spec compiling. Once the actual proof body lands (trigger normalization between requires and spec-function, or explicit forall-instantiation lemmas), the assume() becomes deletable and Verus moves from "trust the lemma" to "verify the lemma". The downstream theorems that depend on this lemma already work. Verifies: REQ-004
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
Three concrete bugs in
rivet-core/src/verus_specs.rsthat preventbazel test //verus:rivet_specs_verifyfrom compiling — the previous run failed in 0.1s, far too fast for SMT, indicating Verus rejected the file at parse/typecheck before reaching the solver.Diagnosis from the parallel research agent sweep (REQ-004 follow-up):
Wrong vstd module paths (lines 244, 249).
vstd::arithmetic::mul_internals::lemma_mul_inequalityandvstd::arithmetic::div_internals::lemma_div_is_ordereddo not exist — the*_internalsmodules live undervstd::arithmetic::internals::*and don't expose those names. The public re-exports are at:vstd::arithmetic::mul::lemma_mul_inequalityvstd::arithmetic::div_mod::lemma_div_is_orderedMissing arithmetic step in
lemma_coverage_bounded.lemma_div_is_orderedonly proves(covered*100)/total <= (total*100)/total. To discharge(covered*100)/total <= 100Verus also needs(total*100)/total == 100, which islemma_div_multiples_vanish(100, total).matches!not in Verus's spec subset (lines 283, 399).Replaced
matches!(diag.severity, GhostSeverity::Error)withdiag.severity is Error(Verus's enum-discriminant operator).Test plan
cargo check -p rivet-corepasses (verus_specs is#[cfg(verus)]-gated, but the file should be valid Rust regardless).test.logartifact uploaded by the parallel CI workflow PR (PR A in this sweep).Notes
rivet-core/src/verus_specs.rsonly.cargo checkand CI.🤖 Generated with Claude Code