Verus Tutorial and Reference

Enum

In Verus, just as in Rust, you can use enum to define a datatype that is any one of the defined variants:

enum Beverage {
    Coffee { creamers: nat, sugar: bool },
    Soda { flavor: Syrup },
    Water { ice: bool },
}

An enum is often used just for its tags, without member fields:

enum Syrup {
    Cola,
    RootBeer,
    Orange,
    LemonLime,
}

Identifying a variant with the is operator

In spec contexts, the is operator lets you query which variant of an enum a variable contains.

fn make_float(bev: Beverage) -> Dessert
    requires bev is Soda
{
    Dessert::new(/*...*/)
}

Accessing fields with the arrow operator

If all the fields have distinct names, as in the Beverage example, you can refer to fields with the arrow -> operator:

proof fn sufficiently_creamy(bev: Beverage) -> bool
    requires bev is Coffee
{
   bev->creamers >= 2
}

If an enum field reuses a name, you can qualify the field access:

enum Life {
    Mammal { legs: int, has_pocket: bool },
    Arthropod { legs: int, wings: int },
    Plant { leaves: int },
}

spec fn is_insect(l: Life) -> bool
{
    l is Arthropod && l->Arthropod_legs == 6
}

match works as in Rust.

enum Shape {
    Circle(int),
    Rect(int, int),
}

spec fn area_2(s: Shape) -> int {
    match s {
        Shape::Circle(radius) => { radius * radius * 3 },
        Shape::Rect(width, height) => { width * height }
    }
}

For variants like Shape declared with round parentheses (), you can use Verus’ `->’ tuple-like syntax to access a single field without a match destruction:

spec fn rect_height(s: Shape) -> int
    recommends s is Rect
{
    s->1
}

matches with &&, ==>, and &&&

match is natural for examining every variant of an enum. If you’d like to bind the fields while only considering one or two of the variants, you can use Verus’ matches syntax:

use Life::*;
spec fn cuddly(l: Life) -> bool {
    ||| l matches Mammal { legs, .. } && legs == 4
    ||| l matches Arthropod { legs, wings } && legs == 8 && wings == 0
}

Because the matches syntax binds names in patterns, it has no trouble with field names reused across variants, so it may be preferable to the (qualified) arrow syntax.

Notice that l matches Mammal{legs} && legs == 4 is a boolean expression, with the special property that legs is bound in the remainder of the expression after &&. That helpful binding also works with ==> and &&&:

spec fn is_kangaroo(l: Life) -> bool {
    &&& l matches Life::Mammal { legs, has_pocket }
    &&& legs == 2
    &&& has_pocket
}

spec fn walks_upright(l: Life) -> bool {
    l matches Life::Mammal { legs, .. } ==> legs == 2
}