Track D: Verus deductive proofs for the wohl-alert dedup invariant#12
Merged
Conversation
Adds the first formal-verification wedge to Wohl: Verus proofs for the AlertDispatcher's dedup and rate-limit invariants, modelled as a ghost state machine in `proofs/verus/alert_dedup.rs`. Why a separate file instead of inline annotations? - Plain `cargo build` / `cargo test` / `cargo clippy` / Kani are unaffected. Verus's macro syntax (`requires`, `ensures`, `forall`) doesn't parse under stock rustc, so inline annotations would require a `verus-strip` preprocessing step we don't have in CI today. - A reviewer can read the proof file in isolation. What is proved: - `theorem_dedup_invariant`: same `(zone_id, alert_type)` within `DEDUP_COOLDOWN_SEC` after a Send returns Deduplicated, for all nat timestamps. This is the primary obligation from #7 — Kani only checks bounded values. - `theorem_rate_limit_invariant`: saturated minute_count inside the 60-second window forces RateLimited (when not deduplicated). - `lemma_first_alert_sends`: empty dispatcher always Sends, used as base case for composition. - `lemma_send_records_entry`: a Send transition appends the new entry. Verification status: - Verus 0.2026.05.17.e479cce: `8 verified, 0 errors` (run locally). - cargo test / fmt / clippy / kani still PASS on wohl-alert. Follow-up (orchestrator decision, not in this PR): - Wire Verus into CI behind a `verus` job (needs the 1.95.0 toolchain and the release binary; see rules_verus pattern in rivet). - Track in a new follow-up issue. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a `# Verification` block to the engine.rs module docs pointing at `proofs/verus/alert_dedup.rs` so a future reader of the executable code can find the deductive proofs. Doc-only change: zero impact on the compiled artifact. cargo test, fmt, clippy, and kani still PASS. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The Track D Verus proofs (proofs/verus/alert_dedup.rs) were hand-run with a downloaded Verus release. Switch to the PulseEngine-standard rules_verus Bazel ruleset so verification is hermetic and reproducible, matching how pulseengine/rivet runs its Verus proofs. - MODULE.bazel: add rules_verus (git_override to commit fc7b636, the same pin rivet uses) + the verus toolchain extension (0.2026.02.15) - proofs/verus/BUILD.bazel: verus_library + verus_test targets for alert_dedup.rs Verified locally: bazel test //proofs/verus:alert_dedup_verify -> PASSED A future CI job runs `bazel test //proofs/verus/...` — no manual Verus install needed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reviewer flagged a version mismatch: the proof file + README cited Verus 0.2026.05.17 / rust 1.95.0 (the hand-installed release the agent used), but the real gate — `bazel test //proofs/verus:alert_dedup_verify` — uses the toolchain pinned in MODULE.bazel via rules_verus. - README: rewritten so `bazel test` is the documented way; dropped the hardcoded version numbers (they drift — the pin lives in MODULE.bazel). - alert_dedup.rs: doc comment points at the bazel target, not a manual `verus` invocation. Docs-only; no proof or behaviour change. Co-Authored-By: Claude Opus 4.7 (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
Phase 2 Track D. The first Verus deductive verification in the repo — proving the AlertDispatcher's dedup + rate-limit invariants beyond what Kani's bounded model reaches. Refs #7.
What's in it
proofs/verus/alert_dedup.rs— a separate Verus proof module (approach B: standalone file, not inlineverus!annotations inengine.rs).Why separate, not inline: there is no
verus-stripstep in the build today, so inline annotations would either break stock-rustccompilation or force a new build step. A separate file keepscargo build/test/clippyand the Kani harnesses completely untouched, and lets a reviewer read the proof in isolation. The model/code-drift trade-off is mitigated byspec consts mirroringengine.rs+ the existing Kani harnesses cross-checking the executable code. Documented inproofs/verus/README.md.What's proven
8 Verus obligations, 0 errors:
theorem_dedup_invariant— same (zone, type) withinDEDUP_COOLDOWN_SECafter aSendreturnsDeduplicatedtheorem_rate_limit_invariant— no more thanMAX_ALERTS_PER_MINUTEdistinct alerts in a 60s windowBazel integration (rules_verus)
Wired into the PulseEngine-standard
rules_verusruleset (same pinfc7b636that pulseengine/rivet uses):MODULE.bazel:rules_verusdep + verus toolchain extensionproofs/verus/BUILD.bazel:verus_library+verus_testtargetsVerified locally:
bazel test //proofs/verus:alert_dedup_verify→ PASSED. Verification is hermetic — no manual Verus install.Verification
bazel test //proofs/verus:alert_dedup_verify— PASSEDcargo test -p wohl-alert— unchanged, still passes (engine.rs only gained a doc-comment)cargo kani -p wohl-alert— still PASScargo +1.85.0 clippy/fmt— cleanRemaining for #7
A CI job (
bazel test //proofs/verus/...) is not in this PR —ci.ymlwas left untouched per track scope. That last step keeps #7 open; tracked alongside the other CI follow-ups in #8.🤖 Generated with Claude Code