Verus Tutorial and Reference

Struct

In Verus, just as in Rust, you can use struct to define a datatype that collects a set of fields together:

struct Point {
    x: int,
    y: int,
}

Spec and exec code can refer to struct fields:

impl Point {
    spec fn len2(&self) -> int {
        self.x * self.x + self.y * self.y
    }
}

fn rotate_90(p: Point) -> (o: Point)
    ensures o.len2() == p.len2()
{
    let o = Point { x: -p.y, y: p.x };
    assert((-p.y) * (-p.y) == p.y * p.y) by(nonlinear_arith);
    o
}