How to use verus-find

Verus-find can find functions and lemmas in Verus files that match some user-provided pattern. Verus-find supports searching for an expression pattern in the pre- and or postcondition and searching for functions that match a specific signature pattern.

Searching in pre- and postconditions

To search in pre- or postconditions, type a Verus expression.
The results are the functions whose pre-/postcondition contains an expression that matches the queried expression.

For example, a search for _.difference(_).len() finds the following lemma:

Expression matching

General rules

• Identifiers are matched by string comparison. Wildcards are supported and often more useful.
• a + b matches a + b
• _ + _ matches a + b, a + s.len()
• a + a does not match 1 + 1
• Expressions are matched on the outer-most syntactic constructor
• _ + _ matches x + y
• _ + _ does not match (x + y) * z
• Nested matching is supported with a prefix asterisk.
• *(_ - _) % _ matches (x * (1 - d)) % d
•  (_ - _) % _ does not match (x * (1 - d)) % d
• Some syntax in the pre-/postconditions is ignored during matching.
• _ + _ matches (x + y)
• 3 matches 3 as int
• Certain functions are treated as matching corresponding operators.
• _.index(_) matches s[i]
• _[_] matches s.index(i)
• _ == _ matches equal(3, 1 + 2)
• Paths in the query must match a prefix.
• Generics are ignored
• Arguments to function calls and method calls are matched according to the rules below.

Argument matching rules

The arguments to function and method calls are matched as follows.

• A query with no arguments matches only a call with no arguments
• foo() matches foo()
• foo() does not match foo(a)
• Individual arguments match iff the expressions match.
• foo(_ + _, 7) matches foo(a + 1, 7)
• foo(_ + _) does not match foo(7)
• A wildcard _ matches 0 or more arbitrary arguments.
• foo(_) matches foo(a + 1, 7)
• foo(_) matches foo()
• foo(_, 7, _) matches foo(a, 7, b)
• foo(_, 7, 8, _) does not match foo(a, 7, b, 8, c)

Searching by function signature

To search by function signature, type a valid Verus function signature.

For example, a search for fn any(_: &mut Vec<_>, _: _) finds the following function:

Signature matching rules

• Function names match if the query is a substring. The function name any is treated as a wildcard.
• fn any() matches fn foo()
• fn foo() matches fn foobar()
• fn foo() does not match fn f()
• Arguments are matched the same as arguments to function or method calls, as explained above. _: _ is treated as a wildcard, while e.g. _: u64 matches any u64 argument.
• fn foo(_: Vec) matches method foo in impl Vec { fn foo(&self) }
• The query doesn't support self arguments but the first argument is used to match against the self argument of searched methods.
• fn foo(_: u64) matches spec fn foo()
• If the query includes a mode, only signatures with that mode match.
• spec fn foo() matches spec fn foo()
• exec fn foo() matches fn foo()
• spec fn foo() does not match proof fn foo()
• If the query includes a return type, the signature's return type must match.
• fn foo() -> u64 matches fn foo() -> u64
• fn foo() -> u64 does not match fn foo()

Can I search functions in my own project?