Verus

https://verus-lang.github.io/verus/guide
Admin
Verus is a verification tool that uses computer-aided theorem proving to statically verify the full...
Tokens:237,872
Snippets:2,960
Trust Score:8.3
Update:5 months ago
Show doc for...
Tokens:
Raw
### Client Example: Using TreeMap Operations

Source: https://verus-lang.github.io/verus/guide/container_bst_first_draft.html

Demonstrates the usage of `insert`, `delete`, and `get` operations on a `TreeMap`. Verifies the map's state after modifications and checks for the presence of elements.

```rust
fn test() {
    let mut tree_map = TreeMap::<bool>::new();
    tree_map.insert(17, false);
    tree_map.insert(18, false);
    tree_map.insert(17, true);

    assert(tree_map@ == map![17u64 => true, 18u64 => false]);

    tree_map.delete(17);

    assert(tree_map@ == map![18u64 => false]);

    let elem17 = tree_map.get(17);
    let elem18 = tree_map.get(18);
    assert(elem17.is_none());
    assert(elem18 == Some(&false));
}
```

--------------------------------

### Hoisted Quantifiers - Forall Example

Source: https://verus-lang.github.io/verus/guide/print.html

This example demonstrates how a `forall` statement can be conceptually understood by hoisting the quantified variables into function parameters.

```rust
proof fn hoisted_forall(i: int, j: int)
    ensures
        is_distinct(i, j) ==> is_distinct(j, i),
{
}
```

--------------------------------

### Verus Axiom Usage Info Example

Source: https://verus-lang.github.io/verus/guide/broadcast_proof.html

Example output from the `-V axiom-usage-info` flag, showing which broadcasted lemmas and groups were used in verifying a function.

```text
note: checking this function used these broadcasted lemmas and broadcast groups:
        - (group) broadcast_proof::multiple_broadcast_proof::Multiple::group_properties,
        - broadcast_proof::multiple_broadcast_proof::Multiple::lemma_add_aligned
   --> ../examples/broadcast_proof.rs:161:11
    |
161 |       proof fn increase_twice(
    |  ___________^
162 | |         p1: Multiple, v: Multiple, p2: Multiple)
    | |________________________________________________^

```

--------------------------------

### Install Singular on Debian-based Linux

Source: https://verus-lang.github.io/verus/guide/install-singular.html

Use apt-get to install Singular on Debian-based Linux distributions. Ensure the VERUS_SINGULAR_PATH environment variable is set when running Verus.

```bash
apt-get install singular
```

--------------------------------

### Verus Profiler Output Example

Source: https://verus-lang.github.io/verus/guide/print.html

An example of the output generated by the Verus profiler when run with the `--profile` option on a function that times out. It shows total quantifier instantiations and cost analysis for each quantifier.

```text
error: function body check: Resource limit (rlimit) exceeded
  --> ../examples/trigger_loops.rs:66:7
   |
66 | proof fn trigger_forever2()
   |       ^^^^^^^^^^^^^^^^^^^^^

note: Analyzing prover log for (profile rerun) trigger_loops::trigger_forever2 ...

Z3 4.12.5
note: Log analysis complete for (profile rerun) trigger_loops::trigger_forever2

note: Profile statistics for trigger_loops::trigger_forever2

note: Observed 17,963 total instantiations of user-level quantifiers

note: Cost * Instantiations: 2269911826 (Instantiated 8,981 times - 49% of the total, cost 252746) top 1 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:70:93
   |
70 | ...   forall|x: nat, y: nat| f(x + 1, 2 * y) && f(2 * x, y + x) || f(y, x) ==> #[trigger] f(x, y),
   |       ------------------------------------------------------------------------------------^^^^^^^
   |       |
   |       Triggers selected for this quantifier

note: Cost * Instantiations: 397732566 (Instantiated 8,981 times - 49% of the total, cost 44286) top 2 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:69:32
   |
69 |         forall|x: nat, y: nat| h(x, y) == f(x, y),
   |         -----------------------^^^^^^^----^^^^^^^
   |         |
   |         Triggers selected for this quantifier

note: Cost * Instantiations: 3 (Instantiated 1 times - 0% of the total, cost 3) top 3 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:68:24
   |
68 |         forall|x: nat| g(x),
   |         ---------------^^^^
   |         |
   |         Triggers selected for this quantifier

verification results:: 0 verified, 1 errors
error: aborting due to 1 previous error
```

--------------------------------

### Hoisted Quantifiers - Exists Example

Source: https://verus-lang.github.io/verus/guide/print.html

This example shows how an `exists` statement can be understood by hoisting the quantified variables into function parameters, simplifying the assertion.

```rust
proof fn hoisted_exists(x: int, i: int)
    requires
        x == i + 1 && is_distinct(i, 5),
{
    assert(x != 6);
}
```

--------------------------------

### Client-side TreeMap Usage Example

Source: https://verus-lang.github.io/verus/guide/container_bst_type_invariant.html

This test function demonstrates the usage of `TreeMap`'s `new`, `insert`, `delete`, and `get` methods, verifying its behavior as a `Map`.

```rust
fn test() {
    let mut tree_map = TreeMap::<bool>::new();
    tree_map.insert(17, false);
    tree_map.insert(18, false);
    tree_map.insert(17, true);

    assert(tree_map@ == map![17u64 => true, 18u64 => false]);

    tree_map.delete(17);

    assert(tree_map@ == map![18u64 => false]);

    let elem17 = tree_map.get(17);
    let elem18 = tree_map.get(18);
    assert(elem17.is_none());
    assert(elem18 == Some(&false));

    test2(tree_map);
}

fn test2(tree_map: TreeMap<bool>) {
    let mut tree_map = tree_map;
    tree_map.insert(25, true);
    tree_map.insert(100, true);
}
```

--------------------------------

### Verus: Matching Loop Example - s[2] <= s[3]

Source: https://verus-lang.github.io/verus/guide/multitriggers.html

Illustrates how a trigger on `s[i] <= s[i + 1]` can lead to a chain of instantiations, starting with `i = 2` and generating `s[3]`, which can then be used for further matching.

```text
0 <= 2 < s.len() - 1 ==> s[2] <= s[3]
```

--------------------------------

### Complete Verus Program Example

Source: https://verus-lang.github.io/verus/guide/requires_ensures.html

A complete Verus program demonstrating function specifications with requires and ensures, an external body function, and runtime assertions. This example shows how to combine different Verus features.

```rust
use vstd::prelude::*;

verus! {

#[verifier::external_body]
fn print_two_digit_number(i: i8)
    requires
        -99 <= i < 100,
{
    println!("The answer is {}", i);
}

fn octuple(x1: i8) -> (x8: i8)
    requires
        -16 <= x1 < 16,
    ensures
        x8 == 8 * x1,
{
    let x2 = x1 + x1;
    let x4 = x2 + x2;
    x4 + x4
}

fn main() {
    let n = octuple(10);
    assert(n == 80);
    print_two_digit_number(n);
}

} // verus!
```

--------------------------------

### Running Rustdoc with Verus Tooling

Source: https://verus-lang.github.io/verus/guide/print.html

Example shell script to run rustdoc with Verus-specific configurations and environment variables, including the VERUSDOC flag.

```Shell
VERUS=/path/to/verus/source

if [ `uname` == "Darwin" ]; then
    DYN_LIB_EXT=dylib
elif [ `uname` == "Linux" ]; then
    DYN_LIB_EXT=so
fi

# Run rustdoc.
# Note the VERUSDOC environment variable.

RUSTC_BOOTSTRAP=1 VERUSDOC=1 rustdoc \
  --extern builtin=$VERUS/target-verus/debug/libbuiltin.rlib \
  --extern builtin_macros=$VERUS/target-verus/debug/libbuiltin_macros.$DYN_LIB_EXT \
  --extern state_machines_macros=$VERUS/target-verus/debug/libstate_machines_macros.$DYN_LIB_EXT \
  --extern vstd=$VERUS/target-verus/debug/libvstd.rlib \
  --edition=2021 \
  --cfg verus_keep_ghost \
  --cfg verus_keep_ghost_body \
  --cfg 'feature="std"' \
  --cfg 'feature="alloc"' \
  '-Zcrate-attr=feature(register_tool)' \
  '-Zcrate-attr=register_tool(verus)' \
  '-Zcrate-attr=register_tool(verifier)' \
  '-Zcrate-attr=register_tool(verusfmt)' \
  --crate-type=lib \
  ./lib.rs

```

--------------------------------

### Example: Asserting usize bit size in Verus

Source: https://verus-lang.github.io/verus/guide/reference-global.html

This example demonstrates how a `global layout usize is size == 4;` directive influences Verus's assumptions about `usize`, allowing assertions like `usize::BITS == 32` to pass.

```rust
global layout usize is size == 4;

fn test(x: usize) {
    // This passes because Verus assumes x is a 32-bit integer:
    assert(x <= 0xffffffff);
    assert(usize::BITS == 32);
}
```

--------------------------------

### Uninterpreted Functions for Profiling Example

Source: https://verus-lang.github.io/verus/guide/profiling.html

These uninterpreted functions are used in the example to demonstrate quantifier profiling. They serve as placeholders for complex logic that the SMT solver needs to reason about.

```rust
uninterp spec fn f(x: nat, y: nat) -> bool;

uninterp spec fn g(x: nat) -> bool;

uninterp spec fn h(x: nat, y: nat) -> bool;
```

--------------------------------

### Verus Code Example

Source: https://verus-lang.github.io/verus/guide/getting_started_vscode.html

A basic Verus program demonstrating function definition, assertions, and universal quantifiers. Save the file to trigger verus-analyzer.

```rust
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));
    assert(forall|i: int, j: int| min(i, j) == min(i, i));
}

} // verus!
```

--------------------------------

### Verifying Constants with `#[verus_verify]`

Source: https://verus-lang.github.io/verus/guide/exec_attr.html

Demonstrates the use of `#[verus_verify]` for defining and verifying constants. Includes examples of external bodies and specification clauses.

```rust
test_verify_one_file! {
    #[test] test_verus_verify_on_const code! {
        #[verus_verify]
        const MY_CONST1: u64 = 1u64;

        #[verus_verify(external_body)]
        #[verus_spec(
            ensures MY_CONST2 == 1
        )]
        const MY_CONST2: u64 = 0;

        #[verus_verify]
        #[verus_spec]
        const MY_CONST3: u64 = 0;

        #[verus_verify]
        #[cfg_attr(not(customized_cfg), verus_spec(
            ensures MY_CONST4 == 0
        ))]
        const MY_CONST4: u64 = 0;

        #[verus_spec]
        fn test_use_const() {
            let x = MY_CONST1;
            let y = MY_CONST2;
            let z = MY_CONST3;
            let w = MY_CONST4;
            proof{
                assert(x == 1);
                assert(y == 1);
                assert(z == 0);
                assert(w == 0);
            }
        }
    } => Ok(())
}
```

--------------------------------

### Sanity Checking with exec_on_line

Source: https://verus-lang.github.io/verus/guide/print.html

Example of how to run the executable function `exec_on_line` to sanity check the output of the compiled `on_line` spec on a specific input.

```rust
__
fn main() {
    let p1 = ExecPoint { x: 1, y: 1 };
    let p2 = ExecPoint { x: 2, y: 2 };
    let points = vec![p1, p2];
    let b = exec_on_line(points.as_slice());
    assert_eq!(b, true);
}

```

--------------------------------

### Singular Query for `integer_ring` Example

Source: https://verus-lang.github.io/verus/guide/nonlinear.html

This is the Singular query generated by Verus for the `foo` function example. It shows how Verus translates the Verus code, particularly the modulus operator, into Singular's internal representation. Understanding this translation is key to debugging `integer_ring` proofs, as it highlights why certain properties might not be provable due to Singular's handling of modular arithmetic.

```singular
ring ring_R=integer, (a, b, c, d, x, y, tmp_0, tmp_1, tmp_2), dp;
    ideal ideal_I = 
      a - c,
      b - d,
      (a - (b * tmp_0)) - x,
      (c - (d * tmp_1)) - y;
    ideal ideal_G = groebner(ideal_I);
    reduce(x - y, ideal_G);
    quit;
```

--------------------------------

### Verus: Multiple Triggers Example

Source: https://verus-lang.github.io/verus/guide/multitriggers.html

Demonstrates specifying multiple triggers for a quantifier using `#![trigger ...]` syntax. The SMT solver instantiates the quantifier if any of the triggers match.

```rust
proof fn test_multitriggers(a: Seq<int>, b: Seq<int>, c: Seq<int>)
    requires
        5 <= a.len(),
        a.len() == b.len(),
        a.len() == c.len(),
        forall|i: int, j: int|
            #![trigger a[i], b[j]]
            #![trigger a[i], c[j]]
            0 <= i < j < a.len() ==> a[i] != b[j] && a[i] != c[j],
{
    assert(a[2] != c[4]);  // succeeds, matches a[i], c[j]
}
```

--------------------------------

### TreeMap Get Operation

Source: https://verus-lang.github.io/verus/guide/container_bst_all_source.html

Public interface for retrieving a value from the TreeMap by key. It initiates the get operation starting from the root node.

```rust
pub fn get(&self, key: u64) -> Option<&V>
        returns
            (if self@.dom().contains(key) { Some(&self@[key]) } else { None }),
    {
        proof { use_type_invariant(&*self); }
        Node::<V>::get_from_optional(&self.root, key)
    }
```

--------------------------------

### Struct Initialization with Follow Output

Source: https://verus-lang.github.io/verus/guide/print.html

Demonstrates initializing a struct and simultaneously handling a follow output using `proof_with!` and `proof_decl!`. This is used when a function needs to return a struct and also provide a ghost value. Requires `vstd::prelude::*`.

```rust
use vstd::prelude::*;

#[verus_verify]
pub struct TestStruct {
    pub x: u32,
    #[cfg(verus_keep_ghost_body)]
    pub y: Ghost<int>,
}

// Test combined struct fields and |= follow output in a single proof_with!
#[verus_spec(s =>
    with
        -> g: Ghost<int>
    requires
        x < u32::MAX,
    ensures
        s.x == x + 1,
        s.y == 2 * s.x,
        g == 3 * x,
)]
fn make_struct_with_follows(x: u32) -> TestStruct
{
    proof_decl! {
        let ghost g = 3 * x;
    }
    proof_with! {
        y: Ghost(2 * (x + 1)),
        |= Ghost(g)
    }
    TestStruct{
        x: x + 1,
    }
```

--------------------------------

### Verus Profiler Output Example

Source: https://verus-lang.github.io/verus/guide/profiling.html

This output demonstrates the information provided by the Verus profiler when run with the `--profile` option. It highlights the number of instantiations and estimated costs for each user-level quantifier, helping to identify performance bottlenecks.

```text
error: function body check: Resource limit (rlimit) exceeded
  --> ../examples/trigger_loops.rs:66:7
   | 
66 | proof fn trigger_forever2()
   |       ^^^^^^^^^^^^^^^^^^^^^ 

note: Analyzing prover log for (profile rerun) trigger_loops::trigger_forever2 ...

Z3 4.12.5
note: Log analysis complete for (profile rerun) trigger_loops::trigger_forever2

note: Profile statistics for trigger_loops::trigger_forever2

note: Observed 17,963 total instantiations of user-level quantifiers

note: Cost * Instantiations: 2269911826 (Instantiated 8,981 times - 49% of the total, cost 252746) top 1 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:70:93
   | 
70 | ...   forall|x: nat, y: nat| f(x + 1, 2 * y) && f(2 * x, y + x) || f(y, x) ==> #[trigger] f(x, y),
   |       ------------------------------------------------------------------------------------^^^^^^^
   |       | 
   |       Triggers selected for this quantifier

note: Cost * Instantiations: 397732566 (Instantiated 8,981 times - 49% of the total, cost 44286) top 2 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:69:32
   | 
69 |         forall|x: nat, y: nat| h(x, y) == f(x, y),
   |         -----------------------^^^^^^^----^^^^^^^
   |         | 
   |         Triggers selected for this quantifier

note: Cost * Instantiations: 3 (Instantiated 1 times - 0% of the total, cost 3) top 3 of 3 user-level quantifiers.
  --> ../examples/trigger_loops.rs:68:24
   | 
68 |         forall|x: nat| g(x),
   |         ---------------^^^^
   |         | 
   |         Triggers selected for this quantifier

verification results:: 0 verified, 1 errors
error: aborting due to 1 previous error

```

--------------------------------

### Combined Struct Fields and Follow Output with Let Binding

Source: https://verus-lang.github.io/verus/guide/exec_attr.html

Shows how to combine struct field initialization and follow output (`|=`) using `proof_with!` and a `let` binding. This allows for sequential updates to ghost state.

```rust
use vstd::prelude::*;

#[verus_verify]
pub struct TestStruct {
    pub x: u32,
    #[cfg(verus_keep_ghost_body)]
    pub y: Ghost<int>,
}

// Test combined struct fields and |= follow output with let binding
#[verus_spec(s =>
    with
        -> g: Ghost<int>
    requires
        x < u32::MAX,
    ensures
        s.x == x + 1,
        s.y == 2 * s.x,
        g == 3 * x,
)]
fn make_struct_with_follows_let(x: u32) -> TestStruct
{
    proof_decl! {
        let ghost g = 3 * x;
    }
    proof_with! { y: Ghost(2 * (x + 1))}
    let s = TestStruct{
        x: x + 1,
    };
    proof_with! { |= Ghost(g) }
    s
```

--------------------------------

### Symbolic Computation with Sequences

Source: https://verus-lang.github.io/verus/guide/assert_by_compute.html

Provides an example of using `compute_only` for symbolic computations involving sequences, demonstrating the interpreter's capability beyond concrete values.

```rust
proof fn seq_example(a: Seq<int>, b: Seq<int>, c: Seq<int>, d: Seq<int>) {
    assert(seq![a, b, c, d] =~= seq![a, b].add(seq![c, d])) by (compute_only);
}
```

--------------------------------

### Initialize Verus Project

Source: https://verus-lang.github.io/verus/guide/getting_started_vscode.html

Use this command to create a new Verus project structure.

```bash
cargo init verus_test
```

--------------------------------

### Combined Struct Fields and Follow Output with `proof_with!`

Source: https://verus-lang.github.io/verus/guide/exec_attr.html

Demonstrates using `proof_with!` to initialize both struct fields and a follow output (`|=`) simultaneously. Requires `vstd::prelude::*` and uses `proof_decl!` for ghost variables.

```rust
use vstd::prelude::*;

#[verus_verify]
pub struct TestStruct {
    pub x: u32,
    #[cfg(verus_keep_ghost_body)]
    pub y: Ghost<int>,
}

// Test combined struct fields and |= follow output in a single proof_with!
#[verus_spec(s =>
    with
        -> g: Ghost<int>
    requires
        x < u32::MAX,
    ensures
        s.x == x + 1,
        s.y == 2 * s.x,
        g == 3 * x,
)]
fn make_struct_with_follows(x: u32) -> TestStruct
{
    proof_decl! {
        let ghost g = 3 * x;
    }
    proof_with! {
        y: Ghost(2 * (x + 1)),
        |= Ghost(g)
    }
    TestStruct{
        x: x + 1,
    }
}
```

--------------------------------

### Verus Compiler Diagnostic Example

Source: https://verus-lang.github.io/verus/guide/getting_started_vscode.html

Example of a compiler error message from Verus, indicating a failed assertion.

```text
error: assertion failed
  --> verus_test/src/main.rs:19:12
   |
19 |     assert(forall|i: int, j: int| min(i, j) == min(i, i));
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

```

--------------------------------

### Node Internal Get Operation

Source: https://verus-lang.github.io/verus/guide/print.html

Details the internal `get` operation within the `Node` struct, used for recursive lookups in the TreeMap.

```APIDOC
## Node::get(&self, key: u64) -> Option<&V>

### Description
Recursively searches for a key within a `Node` and its children.

### Method
`get`

### Parameters
- **key** (u64) - The key to search for.

### Returns
- **Option<&V>** - `Some(&V)` if the key is found, `None` otherwise.

### Specification
- **Requires**: `self.well_formed()`
- **Returns**: `(if self.as_map().dom().contains(key) { Some(&self.as_map()[key]) } else { None })`

### Internal Helper: `get_from_optional`

- **Signature**: `fn get_from_optional(node: &Option<Box<Node<V>>>, key: u64) -> Option<&V>`
- **Requires**: `node.is_some() ==> node.unwrap().well_formed()`
- **Returns**: `(match node { Some(node) => (if node.as_map().dom().contains(key) { Some(&node.as_map()[key]) } else { None }), None => None, })`
```

--------------------------------

### Struct Initialization with Let Binding

Source: https://verus-lang.github.io/verus/guide/exec_attr.html

Illustrates initializing a struct using a `let` binding within a function, combined with `proof_with!` for managing ghost state. This pattern is useful for more complex initialization sequences.

```rust
use vstd::prelude::*;
use vstd::raw_ptr::PointsToRaw;

#[verus_verify]
pub struct STest {
    pub u: u32,
    #[cfg(verus_keep_ghost_body)]
    pub p: Tracked<PointsToRaw>,
}

// Test with let binding
#[verus_spec(result =>
    with
        Tracked(p): Tracked<PointsToRaw>,
    ensures
        result.u == u,
)]
pub fn make_s_test_let(u: u32) -> STest
{
    proof_with!{ p: Tracked(p) }
    let s = STest { u };
    s
```

--------------------------------

### Install Singular on macOS

Source: https://verus-lang.github.io/verus/guide/install-singular.html

Use Homebrew to install Singular on macOS. Remember to set the VERUS_SINGULAR_PATH environment variable when running Verus.

```bash
brew install Singular
```

--------------------------------

### calc! Macro Example with Trivial Proofs

Source: https://verus-lang.github.io/verus/guide/print.html

Demonstrates a simple use case of the `calc!` macro with the `<=` relation, where intermediate proof blocks are empty due to trivial steps. This proves `a <= 5` by showing `a <= a + 3 <= 5`.

```rust
let a: int = 2;
calc! {
    (<=)
    a; {}
    a + 3; {}
    5;
}
```

--------------------------------

### Get Key from TreeMap

Source: https://verus-lang.github.io/verus/guide/container_bst_all_source.html

Public method to get a value associated with a key from the TreeMap. It uses the Node's get_from_optional method to perform the lookup.

```rust
pub fn get(&self, key: u64) -> Option<&V>
    requires
        self.well_formed(),
    returns
        (if self@.dom().contains(key) { Some(&self@[key]) } else { None }),
{
    Node::<V>::get_from_optional(&self.root, key)
}
```

--------------------------------

### Basic calc! usage

Source: https://verus-lang.github.io/verus/guide/calc.html

Demonstrates the basic syntax of the `calc!` macro for proving a relation between two expressions through intermediate steps. Proofs for intermediate steps can be empty if trivial.

```rust
    let a: int = 2;
    calc! {
        (<=)
        a; {}
        a + 3; {}
        5;
    }
```

--------------------------------

### Verus: Sequence Update Example

Source: https://verus-lang.github.io/verus/guide/multitriggers.html

Example demonstrating a common scenario where Verus automatically selects a single, safer trigger to avoid excessive quantifier instantiations.

```rust
proof fn seq_update_different<A>(s: Seq<A>, i: int, j: int, a: A) {
    assert(forall|i: int, j: int|
        0 <= i < s.len() && 0 <= j < s.len() && i != j ==> s.update(j, a)[i] == s[i]);
}
```

--------------------------------

### Verus: Proving Forall with Assert By

Source: https://verus-lang.github.io/verus/guide/quantproofs.html

Shows how to prove forall expressions in Verus when automatic verification fails, using the `assert ... by` construct to provide a proof body where quantified variables are in scope.

```rust
spec fn f(i: int) -> bool { ... }

proof fn lemma_even_f(i: int)
    requires
        is_even(i),
    ensures
        f(i),
{ ... }

proof fn test_even_f() 
    ensures
        forall|i: int| is_even(i) ==> f(i),
{
    assert forall|i: int| is_even(i) implies f(i) by {
        // First, i is in scope here
        // Second, we assume is_even(i) here
        lemma_even_f(i);
        // Finally, we have to prove f(i) here
    }
}
```

--------------------------------

### Follow Output Only Before Struct Constructor

Source: https://verus-lang.github.io/verus/guide/exec_attr.html

Tests the scenario where `proof_with!` is used solely for a follow output (`|=`) before a struct constructor. This ensures the parser correctly distinguishes follow syntax from struct field initialization.

```rust
// Regression test for https://github.com/verus-lang/verus/issues/2283
// proof_with! with only |= follow output before a struct constructor
// should not attempt to parse the follow as struct fields.
#[test] test_proof_with_follows_only_before_struct code!{
    use vstd::prelude::*;

    #[verus_verify]
    pub struct S {}

    #[verus_spec(
        with
            -> res: Ghost<int>
        ensures
            res == 0,
    )]
    pub fn f() -> S {
        proof_with!(|= Ghost(0int));
        S {}
    }
}
```

--------------------------------

### Basic calc! Macro Structure

Source: https://verus-lang.github.io/verus/guide/print.html

Illustrates the fundamental syntax for the `calc!` macro, showing how to declare a transitive relation and a sequence of terms with proof blocks for each step.

```rust
calc! {
  (R)
  a_1; { /* proof that a_1 R a_2 */ }
  a_2; { /* proof that a_2 R a_3 */ }
   ...
  a_n;
}
```

--------------------------------

### Invalid Trigger Example: 0 <= i

Source: https://verus-lang.github.io/verus/guide/print.html

This example demonstrates an invalid trigger `0 <= i` which violates the rule against using basic integer arithmetic operators in triggers. The resulting error message is shown.

```rust
proof fn test_use_forall_bad1(s: Seq<int>)
    requires
        5 <= s.len(),
        forall|i: int| (#[trigger](0 <= i)) && i < s.len() ==> is_even(s[i]),
{
    assert(s[3] % 2 == 0);
}
```

```text
error: trigger must be a function call, a field access, or a bitwise operator
    |
    |         forall|i: int| (#[trigger](0 <= i)) && i < s.len() ==> is_even(s[i]),
    |                        ^^^^^^^^^


```

--------------------------------

### Verus Quantifier and Chained Operators Example

Source: https://verus-lang.github.io/verus/guide/operators.html

Illustrates the 'forall' quantifier, chained comparison operators, and implication operators in Verus specifications. Requires understanding of quantifiers for full context.

```verus
forall|i: int, j: int| 0 <= i <= j < len ==> f(i, j)
```

--------------------------------

### Run rustdoc with Verusdoc

Source: https://verus-lang.github.io/verus/guide/verusdoc.html

This script sets up environment variables and runs rustdoc with specific Verus dependencies and configurations. It then executes the verusdoc post-processor.

```shell
VERUS=/path/to/verus/source

if [ `uname` == "Darwin" ]; then
    DYN_LIB_EXT=dylib
elif [ `uname` == "Linux" ]; then
    DYN_LIB_EXT=so
fi

# Run rustdoc.
# Note the VERUSDOC environment variable.

RUSTC_BOOTSTRAP=1 VERUSDOC=1 rustdoc \
  --extern builtin=$VERUS/target-verus/debug/libbuiltin.rlib \
  --extern builtin_macros=$VERUS/target-verus/debug/libbuiltin_macros.$DYN_LIB_EXT \
  --extern state_machines_macros=$VERUS/target-verus/debug/libstate_machines_macros.$DYN_LIB_EXT \
  --extern vstd=$VERUS/target-verus/debug/libvstd.rlib \
  --edition=2021 \
  --cfg verus_keep_ghost \
  --cfg verus_keep_ghost_body \
  --cfg 'feature="std"' \
  --cfg 'feature="alloc"' \
  '-Zcrate-attr=feature(register_tool)' \
  '-Zcrate-attr=register_tool(verus)' \
  '-Zcrate-attr=register_tool(verifier)' \
  '-Zcrate-attr=register_tool(verusfmt)' \
  --crate-type=lib \
  ./lib.rs

# Run the post-processor.

$VERUS/target/debug/verusdoc

```

--------------------------------

### Verus `integer_ring` Proof Example

Source: https://verus-lang.github.io/verus/guide/nonlinear.html

This Verus proof function demonstrates the usage of the `integer_ring` strategy. It requires specific preconditions related to integer equality and modular arithmetic. Note that `integer_ring` has limitations and may not solve seemingly trivial problems if they don't strictly adhere to its supported congruence patterns.

```rust
proof fn foo(a: int, b: int, c: int, d: int, x: int, y: int) by(integer_ring)
    requires
        a == c,
        b == d,
        a % b == x,
        c % d == y
    ensures
        x == y,
{
}
```

--------------------------------

### Example Usage Requiring well_formed

Source: https://verus-lang.github.io/verus/guide/container_bst_type_invariant.html

This example demonstrates how a client must explicitly manage the `well_formed()` predicate in `requires` clauses when interacting with a `TreeMap` that does not use type invariants. The `test_callee` function requires `tree_map.well_formed()` to be true.

```rust
fn test2() {
    let mut tree_map = TreeMap::<bool>::new();
    test_callee(tree_map);
}

fn test_callee(tree_map: TreeMap<bool>)
    requires
        tree_map.well_formed(),
{
    let mut tree_map = tree_map;
    tree_map.insert(25, true);
    tree_map.insert(100, true);
}
```

--------------------------------

### Initial Proof Outline

Source: https://verus-lang.github.io/verus/guide/assert_assume.html

This is the initial outline of a proof for `lemma_len_intersect`. It requires `s1` to be finite and ensures that the length of the intersection of `s1` and `s2` is less than or equal to the length of `s1`.

```rust
__
pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases
        s1.len(),
{
    if s1.is_empty() {

    } else {
        let a = s1.choose();

        lemma_len_intersect(s1.remove(a), s2);
    }
}

```

--------------------------------

### Call Proof Functions from Exec Function using Proof Block

Source: https://verus-lang.github.io/verus/guide/proof_functions.html

Shows how to call a `proof` function (`lemma_min`) from an `exec` function (`test`) using a `proof` block. This allows subsequent assertions within the `exec` function to succeed by leveraging the properties proven by the `proof` function.

```rust
mod M1 {
    use verus_builtin::*

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

    pub proof fn lemma_min(x: int, y: int)
        ensures
            min(x, y) <= x,
            min(x, y) <= y,
            min(x, y) == x || min(x, y) == y,
    {
    }

}

mod M2 {
    use verus_builtin::*
    use crate::M1::*

    fn test() {
        proof {
            lemma_min(10, 20);
            lemma_min(100, 200);
        }
        assert(min(10, 20) == 10);  // succeeds
        assert(min(100, 200) == 100);  // succeeds
    }

}
```

--------------------------------

### Verus BST Node Get Implementation

Source: https://verus-lang.github.io/verus/guide/container_bst_generic.html

Implements the `get` method for a BST node, requiring `TotalOrdered` for key comparisons. Includes proof code to assert invariants and properties related to key presence in subtrees.

```rust
impl<K: TotalOrdered, V> Node<K, V> {
    fn get_from_optional(node: &Option<Box<Node<K, V>>>, key: K)
        requires
            node.is_some() ==> node.unwrap().well_formed(),
        returns
            (match node {
                Some(node) => (if node.as_map().dom().contains(key) { Some(&node.as_map()[key]) } else { None }),
                None => None,
            }),
        decreases node,
    {
        match node {
            None => None,
            Some(node) => {
                node.get(key)
            }
        }
    }

    fn get(&self, key: K) -> Option<&V>
        requires
            self.well_formed(),
        returns
            (if self.as_map().dom().contains(key) { Some(&self.as_map()[key]) } else { None }),
        decreases self,
    {
        match key.compare(&self.key) {
            Cmp::Equal => {
                Some(&self.value)
            }
            Cmp::Less => {
                proof {
                    if Node::<K, V>::optional_as_map(self.right).dom().contains(key) {
                        TotalOrdered::antisymmetric(self.key, key);
                        assert(false);
                    }
                    assert(key != self.key);
                    assert((match self.left {
                            Some(node) => (if node.as_map().dom().contains(key) { Some(&node.as_map()[key]) } else { None }),
                            None => None,
                        }) == (if self.as_map().dom().contains(key) { Some(&self.as_map()[key]) } else { None }));
                }
                Self::get_from_optional(&self.left, key)
            }
            Cmp::Greater => {
                proof {
                    if Node::<K, V>::optional_as_map(self.left).dom().contains(key) {
                        TotalOrdered::antisymmetric(self.key, key);
                        assert(false);
                    }
                    assert(key != self.key);
                    assert((match self.right {
                            Some(node) => (if node.as_map().dom().contains(key) { Some(&node.as_map()[key]) } else { None }),
                            None => None,
                        }) == (if self.as_map().dom().contains(key) { Some(&self.as_map()[key]) } else { None }));
                }
                Self::get_from_optional(&self.right, key)
            }
        }
    }
}
```

--------------------------------

### Example of Type Invariant Enforcement

Source: https://verus-lang.github.io/verus/guide/reference-type-invariants.html

Demonstrates a struct `X` with a type invariant `self.i <= self.j`. The `example` function asserts this invariant. `example_caller` succeeds by creating a valid `X`, while `example_caller2` fails due to an invalid `X`.

```rust
struct X {
    i: u8,
    j: u8,
}

impl X {
    #[verifier::type_invariant]
    spec fn type_inv(self) -> bool {
        self.i <= self.j
    }
}

fn example(x: X) {
    proof {
        use_type_invariant(&x);
    }

    assert(x.i <= x.j); // succeeds
}

fn example_caller() {
    let x = X { i: 20, j: 30 }; // succeeds
    example(x);
}

fn example_caller2() {
    let x = X { i: 30, j: 20 }; // fails
    example(x);
}
```

--------------------------------

### Invalid Trigger Example: 0 <= i

Source: https://verus-lang.github.io/verus/guide/forall.html

This example demonstrates an invalid trigger `0 <= i` which violates Verus's rules by using a basic comparison operator. The error message indicates that triggers must be function calls, field accesses, or bitwise operators.

```rust
proof fn test_use_forall_bad1(s: Seq<int>)
    requires
        5 <= s.len(),
        forall|i: int| (#[trigger](0 <= i)) && i < s.len() ==> is_even(s[i]),
{
    assert(s[3] % 2 == 0);
}
```

```text
error: trigger must be a function call, a field access, or a bitwise operator
    |
    |         forall|i: int| (#[trigger](0 <= i)) && i < s.len() ==> is_even(s[i]),
    |                        ^^^^^^^^^^^^^^^^
```

--------------------------------

### Verus: Matching Loop Example - s[6] <= s[7]

Source: https://verus-lang.github.io/verus/guide/multitriggers.html

Shows the ongoing nature of matching loops. The instantiation `s[6] <= s[7]` is generated from `s[6]`, highlighting how these loops can consume significant SMT solver resources if not avoided.

```text
0 <= 6 < s.len() - 1 ==> s[6] <= s[7]
```

--------------------------------

### Define External Trait

Source: https://verus-lang.github.io/verus/guide/external_trait_specifications.html

This is an example of an external trait that Verus will not verify.

```rust
#[verifier::external]
trait Encoder {
    fn encode_value(&self, x: u64) -> u64;
}
```

--------------------------------

### Choose multiple witnesses using a tuple

Source: https://verus-lang.github.io/verus/guide/exists.html

This example shows how to use 'choose' to extract multiple witnesses simultaneously by collecting them into a tuple. This relies on an 'exists' expression with multiple quantified variables.

```rust
spec fn less_than(x: int, y: int) -> bool {
    x < y
}

proof fn test_choose_succeeds2() {
    assert(less_than(3, 7));  // promote i = 3, i = 7 as a witness
    let (x, y) = choose|i: int, j: int| less_than(i, j);
    assert(x < y);
}
```

--------------------------------

### Node::get_from_optional

Source: https://verus-lang.github.io/verus/guide/container_bst_all_source.html

Helper function to safely get a value from an optional node in the tree.

```APIDOC
## Node::get_from_optional

### Description
Safely retrieves a value from an optional node based on a key.

### Method
`fn get_from_optional(node: &Option<Box<Node<K, V>>>, key: K) -> Option<&V>`

### Requires
`node.is_some() ==> node.unwrap().well_formed()`

### Returns
`Some(&V)` if the key is found in the node, `None` otherwise.
```

--------------------------------

### Verus: Proving Forall and Using Exists

Source: https://verus-lang.github.io/verus/guide/quantproofs.html

Demonstrates how Verus automatically proves forall expressions and uses exists expressions without relying on explicit triggers. Triggers are shown to be irrelevant in these cases.

```rust
spec fn is_distinct(x: int, y: int) -> bool {
    x != y
}

spec fn dummy(i: int) -> bool;

proof fn prove_forall()
    ensures
        forall|i: int, j: int|
            #![trigger dummy(i), dummy(j)]
            is_distinct(i, j) ==> is_distinct(j, i),
{
    // proving the forall just works; the trigger is irrelevant
}

proof fn use_exists(x: int)
    requires
        exists|i: int| #![trigger dummy(i)] x == i + 1 && is_distinct(i, 5),
{
    // using the exists just works; the trigger is irrelevant
    assert(x != 6);
}
```

--------------------------------

### Postcondition Not Satisfied Error

Source: https://verus-lang.github.io/verus/guide/invariants.html

Example of a postcondition failure error reported by Verus when loop invariants are missing.

```rust
error: postcondition not satisfied
   |
   |           result == fib(n as nat),
   |           ----------------------- failed this postcondition
```

--------------------------------

### Assert Forall with Proof Block

Source: https://verus-lang.github.io/verus/guide/syntax.html

Prove universally quantified statements using 'assert forall by'. For implications P ==> Q, use 'assert forall|...| P implies Q by {...}'.

```rust
fn test_assert_forall_by() {
    assert forall|x: int, y: int| f1(x) + f1(y) == x + y + 2 by {
        reveal(f1);
    }
    assert(f1(1) + f1(2) == 5);
    assert(f1(3) + f1(4) == 9);
    // to prove forall|...| P ==> Q, write assert forall|...| P implies Q by {...}
    assert forall|x: int| x < 10 implies f1(x) < 11 by {
        assert(x < 10);
        reveal(f1);
        assert(f1(x) < 11);
    }
    assert(f1(3) < 11);
}
```

--------------------------------

### Node::get

Source: https://verus-lang.github.io/verus/guide/container_bst_first_draft.html

Internal method for Node to get a value by key. This is a helper for the public TreeMap::get.

```APIDOC
## Node::get

### Description
Internal method for a `Node` to retrieve a value by key. This is a recursive helper function used by `TreeMap::get`.

### Method
GET (conceptual, as this is an SDK method)

### Signature
`fn get(&self, key: u64) -> Option<&V>`

### Parameters
#### Path Parameters
None

#### Query Parameters
- **key** (u64) - Required - The key to look up within this node and its children.

### Request Body
None

### Response
#### Success Response (Option<&V>)
- **Some(&V)**: If the key is found in this node or its children.
- **None**: If the key is not found.

### Response Example
```json
{
  "example": "Some(&value)" 
}
```

```json
{
  "example": "None"
}
```
```

--------------------------------

### Basic Verus File Structure

Source: https://verus-lang.github.io/verus/guide/verus_macro_intro.html

This shows the minimal structure for a Verus file, highlighting the `use vstd::prelude::*;` import and the `verus! { ... }` block.

```rust
use vstd::prelude::*;

verus! {
    // ...
}
```

--------------------------------

### Arithmetic Underflow/Overflow Error

Source: https://verus-lang.github.io/verus/guide/invariants.html

Example of an arithmetic underflow/overflow error reported by Verus, often due to missing invariants.

```rust
error: possible arithmetic underflow/overflow
   |
   |         let new_cur = cur + prev;
   |                       ^^^^^^^^^^
```

--------------------------------

### Verus Verification Success Output

Source: https://verus-lang.github.io/verus/guide/getting_started_cmd_line.html

Example output indicating that Verus has successfully verified the functions in the specified file.

```text
note: verifying root module

verification results:: 1 verified, 0 errors
```

--------------------------------

### Verus: `test_vec_map` Example Usage

Source: https://verus-lang.github.io/verus/guide/print.html

Demonstrates how to use the `vec_map` function with the `double` helper function and asserts the correctness of the result.

```rust
fn test_vec_map() {
    let mut v = Vec::new();
    v.push(0);
    v.push(10);
    v.push(20);
    let w = vec_map(&v, double);
    assert(w[2] == 40);
}

```

--------------------------------

### floor_log2 with Inline Proof for Termination

Source: https://verus-lang.github.io/verus/guide/print.html

Demonstrates how to provide an inline proof within a 'proof' block to help Verus verify the decreases measure for termination. This proof uses Verus's bit-vector reasoning.

```rust
__
spec fn floor_log2(n: u64) -> int 
    decreases n
{
    if n <= 1 { 
        0   
    } else { 
        proof {
          assert(n > 1 ==> (n >> 1) < n) by(bit_vector);
        }
        floor_log2(n >> 1) + 1 
    }   
}
```

--------------------------------

### Verus Verification Failure Output

Source: https://verus-lang.github.io/verus/guide/getting_started_cmd_line.html

Example output showing a verification error due to a failed assertion in the Verus code.

```text
note: verifying root module

error: assertion failed
  --> getting_started.rs:19:12
   |
19 |     assert(forall|i: int, j: int| min(i, j) == min(i, i));
   |            ^^^^^^ assertion failed

error: aborting due to previous error

verification results:: 0 verified, 1 errors
```

--------------------------------

### Implementation Method Specification

Source: https://verus-lang.github.io/verus/guide/print.html

This Verus example demonstrates specifying an implementation method (`test`) within a struct (`Foo`). It includes requirements, ensures clauses, and the use of tracked references in the specification.

```rust
test_verify_one_file! {
    #[test] test_impl_method code!{
        use vstd::prelude::*;

        pub struct Foo;

        #[verus_verify]
        impl Foo {
            #[verus_spec(ret =>
                with
                    Tracked(c): Tracked<&mut ()>
                requires
                    true,
                ensures
                    ret == 1,
            )]
            fn test(a: u64, b: u64) -> u64 {
                1
            }
        }
    } => Ok(())
}
```

--------------------------------

### Calling Proof Function with Ghost Return Value

Source: https://verus-lang.github.io/verus/guide/reference-var-modes.html

Shows how to call a proof function that returns a `ghost` value, both from proof code and exec code.

```rust
proof fn example() -> (ret: Y)

```

```rust
proof fn test() {
    let y = example();
}

```

```rust
fn test() {
    let ghost y = example();
}

```
Tokens:
Raw