Implement Sledgehammer-inspired proof search using `broadcast` by dschoepe · Pull Request #2048 · verus-lang/verus

dschoepe · 2025-12-20T02:22:37Z

Completing proofs involving data structures such as sequences, sets, and maps often involves finding the right lemmas that exist in the standard library. Since vstd provides a large number of lemmas that is expected to grow over time, identifying which lemmas may be useful during a proof development becomes a tedious, manual task, in addition to potentially large number of project specific lemmas.

This PR adds a #[verifier::sledgehammer] feature, inspired by the eponymous tool provided by the Isabelle theorem prover.

Open Questions / Issues

Should we rename the feature since each theorem prover usually uses a different name for their Sledgehammer-style tool? Perhaps there is a fitting Rust-specific pun here.
Lemmas from other crates are only considered if they are referenced by the current crate; otherwise they are pruned prior to verification.
The implementation tracks some extra data in verify_bucket that can probably be captured more cleanly.
The call graph is currently recomputed on each proof attempt. This is inefficient, but perhaps not prohibitively so during proof attempts with Sledgehammer.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

jaybosamiya-ms

Awesome to see this! I haven't reviewed the code, but I read through the doc and have a couple of minor comments included inline, and a couple of higher level ones here:

On naming: since this is looking for broadcasts to use, it feels a bit like tuning a radio to the valid frequencies/broadcasts, so maybe a name like autoscan could work 📻

In terms of output: rustc often uses a special syntax to mark "this is how code should change for an auto-fix", it may be nice to generate the final "note" with that so that tools like verus-analyzer and verus-mode.el can pick that up and automatically insert it in. I for one would be interested in introducing a single keybinding to verus-mode.el that automatically introduces the ~~#[verifier::sledgehammer]~~ #[verifier::autoscan], runs on that one function, picks up the results, and auto-rewrites the result with that. The particular rewrite syntax output does not necessarily need to be in this PR, imho, but just documenting it here as something that might be worth doing.

jaybosamiya-ms · 2025-12-22T21:20:41Z

source/docs/guide/src/sledgehammer.md

+mode functions. After finding a proof with Sledgehammer, the
+`#[verifier::sledgehammer]` attribute should afterwards be removed from the
+function to avoid rerunning the proof search on every Verus invocation.


Minor comment: it'd be nice if the sledgehammer tool could automatically recognize that it is no longer needed and tell you to remove it. I haven't tested the branch, so if it already supports/does this, that's great! If not, would be good to document something to the note of "future versions of Verus will automatically detect such cases" or similar.

Good point, I'll add something like that.

jaybosamiya-ms · 2025-12-22T21:21:30Z

source/docs/guide/src/sledgehammer.md

+
+By default, Sledgehammer will minimize a proof; in the above example,
+Sledgehammer initially found a proof that used 5 lemmas, but then determined
+that only one lemma is actually necessary. However, in some case, minimizing a


Minor typo: "some case" -> "some cases"

parno

Thanks for putting this together. I added a bunch of mostly minor comments. For this one:

Lemmas from other crates are only considered if they are referenced by the current crate; otherwise they are pruned prior to verification.

In your experience, is this going to be a significant limitation? If so, should we consider broadening the scope (either automatically or based on another Sledgehammer option)? We could do it in a couple of ways (e.g., detecting a sledgehammer attribute and disabling pruning, or caching a copy of the pre-pruned data prior to pruning).

parno · 2026-01-20T15:21:02Z

source/docs/guide/src/sledgehammer.md

+the [Isabelle](https://isabelle.in.tum.de/) theorem prover.
+
+Sledgehammer is an *experimental* feature that attempts to automatically complete
+a proof attempt by automatically using relevant lemmas using the


Perhaps we can cut one of the two "automatically"s in this sentence?

parno · 2026-01-20T15:21:53Z

source/docs/guide/src/sledgehammer.md

+{{#include ../../../../examples/guide/sledgehammer.rs:set_example_lemma}}
+```
+
+The proof of `union_three_sets` automatically succeeds when adding `broadcast


I would rephrase as:

automatically succeeds when broadcast use union_len; is added to its body.

parno · 2026-01-20T15:22:08Z

source/docs/guide/src/sledgehammer.md

+```
+
+The proof of `union_three_sets` automatically succeeds when adding `broadcast
+use union_len;` to its body. However, this requires identifying both knowing the


Cut "identifying"

parno · 2026-01-20T15:22:20Z

source/docs/guide/src/sledgehammer.md

+use union_len;` to its body. However, this requires identifying both knowing the
+name of this lemma, and enabling it via `broadcast use`.
+
+To simplifying finding relevant lemmas, Verus provides the


"simplifying" -> "simplify"

parno · 2026-01-20T15:22:52Z

source/docs/guide/src/sledgehammer.md

+Running Verus on this example now prints the following message:
+
+```
+note: Sledgehammer found proof with 5 lemmas, minimizing..


I think we want "found proof" -> "found a proof"

parno · 2026-01-20T15:35:17Z

source/rust_verify/src/sledgehammer.rs

+) -> Result<(Option<Krate>, GlobalCtx), VirErr> {
+    let Some(mut sh) = Sledgehammer::<'a, R>::new(verifier, reporter, krate, source_map, bucket_id)
+    else {
+        // TODO: report error here


Lingering TODO here

parno · 2026-01-20T15:37:38Z

source/rust_verify/src/sledgehammer.rs

+    do_minimize: bool,
+}
+
+pub(crate) fn sledgehammer<'a, R: Diagnostics + 'a>(


Since there's already a constructor for Sledgehammer, should the style be to call that and then make this a function on the returned Sledgehammer? Or is your preference to keep the call site limited to a single call to this function?

parno · 2026-01-20T15:44:51Z

source/rust_verify/src/sledgehammer.rs

+        global_ctx: GlobalCtx,
+    ) -> Result<(Guess, GlobalCtx), SledgehammerErr> {
+        let mut min_state = MinimizeState::from(&guess);
+        self.minimize_outer(guess, 2, &mut min_state, global_ctx)


What does 2 signify here?

parno · 2026-01-20T15:54:59Z

source/rust_verify/src/sledgehammer.rs

+    ) -> Result<GlobalCtx, VirErr> {
+        let prev_errors = self.count_errors;
+        let prev_verified = self.count_verified;
+        // TODO: the following is copied from verify_bucket_outer; it would be nicer


Is it copied because the original logic in verify_bucket_outer isn't cleanly factored out of its current setting? If so, we should probably fix that, so that the code here and there doesn't get out of sync.

parno · 2026-01-20T15:59:39Z

source/rust_verify/src/sledgehammer.rs

I'm not sure how well we've stuck to this, but I think we've generally tried to sort files topologically, such that the callees precede callers.

dschoepe added 2 commits December 19, 2025 18:15

Implement Sledgehammer-style proof search

3ad86db

Add documentation for Sledgehammer

150498b

dschoepe force-pushed the sledgehammer branch from 852f5f3 to 150498b Compare December 20, 2025 02:22

dschoepe requested review from Chris-Hawblitzel and parno December 20, 2025 02:26

jaybosamiya-ms reviewed Dec 22, 2025

View reviewed changes

parno approved these changes Jan 20, 2026

View reviewed changes

Conversation

dschoepe commented Dec 20, 2025

Open Questions / Issues

Uh oh!

jaybosamiya-ms left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

parno left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants