The verus! macro

Recall the sample program from the Getting Started chapters:

use vstd::prelude::*;

verus! {

spec fn min(x: int, y: int) -> int {
    if x <= y {
        x
    } else {
        y
    }
}

fn main() {
    assert(min(10, 20) == 10);
    assert(min(-10, -20) == -20);
    assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j);
    assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j);
    assert(forall|i: int, j: int| min(i, j) == min(j, i));
}

} // verus!

What is this exactly? Is it Verus? Is it Rust?

It’s both! It’s a Rust source file that uses the verus! macro to embed Verus. Specifically, the verus! macro extends Rust’s syntax with verification-related features such as preconditions, postconditions, assertions, forall, exists, etc., which we will learn more about in this tutorial.

Verus uses a macro named verus! to extend Rust’s syntax with verification-related features such as preconditions, postconditions, assertions, forall, exists, etc. Therefore, each file in a crate will typically take the following form:

use vstd::prelude::*;

verus! {
    // ...
}

The vstd::prelude exports the verus! macro along with some other Verus utilities.

The verus! macro, besides extending Rust’s syntax, also has the function of instructing Verus to verify the functions contained within. By default, Verus verifies everything inside the verus! macro and ignores anything defined outside the verus! macro. There are various attributes and directives to modify this behavior (e.g., see this chapter), but for most of the tutorial, we will consider all code to be Verus code that must be in the verus! macro.

Note for the tutorial. In the remainder of this guide, we will omit these declarations from the examples to avoid clutter. However, remember that any example code should be placed inside the verus! { ... } block, and that the file should contain use vstd::prelude::*;.