Traits

Verus supports writing specifications for trait functions, including requires and ensures clauses. Specifications on a trait function serve as a contract that all implementations must satisfy, and that callers can rely on when they call the function through a trait bound.

For traits defined in external crates (e.g., from the Rust standard library), see External trait specifications.

Trait function specifications

Trait functions can have requires and ensures clauses just like ordinary functions:

trait Compressor {
    fn compress(&self, input: u64) -> (output: u64)
        ensures output <= input;
}

Any type implementing Compressor must provide a compress function whose body satisfies output <= input.

Extending specifications in implementations

An implementation automatically inherits all requires and ensures clauses from the trait declaration. Additionally:

• An impl can add stronger ensures clauses.
• An impl cannot add new requires clauses — that would be unsound, because a caller using the trait bound C: Compressor has no obligation to satisfy requirements that the trait doesn’t mention.

struct HalfCompressor;

impl Compressor for HalfCompressor {
    // The trait's `ensures output <= input` is automatically inherited.
    // We additionally specify the exact return value.
    fn compress(&self, input: u64) -> (output: u64)
        ensures output == input / 2,
    {
        input / 2
    }
}

HalfCompressor::compress inherits ensures output <= input from the trait. Verus verifies that the function’s body satisfies both the inherited postcondition and the additional postcondition added by the implementation (ensures output == input / 2).

A trait function can also include both requires and ensures:

trait Bounded {
    fn clamp(&self, val: u64, lo: u64, hi: u64) -> (result: u64)
        requires lo <= hi,
        ensures lo <= result <= hi;
}

struct Saturate;

impl Bounded for Saturate {
    // Inherits: requires lo <= hi, ensures lo <= result <= hi
    // Adds: the exact formula for result
    fn clamp(&self, val: u64, lo: u64, hi: u64) -> (result: u64)
        ensures result == if val < lo { lo } else if val > hi { hi } else { val },
    {
        if val < lo { lo } else if val > hi { hi } else { val }
    }
}

Generic vs. concrete dispatch

When Verus can statically determine the concrete type of a trait function call, it uses the possibly-stronger specification from the impl. When the call is through a generic type parameter, Verus only knows the trait-level specification.

fn compress_generic<C: Compressor>(c: &C, x: u64) {
    let r = c.compress(x);
    assert(r <= x); // OK: trait-level ensures holds for every C
}

fn compress_concrete(c: &HalfCompressor, x: u64) {
    let r = c.compress(x);
    assert(r <= x);      // From the trait ensures
    assert(r == x / 2);  // From HalfCompressor's stronger ensures (statically resolved)
}

Spec and proof functions

A trait may also contain spec and proof function declarations. For example, the trait below requires implementations to provide a distance metric (dist) as a specification function and then to prove that their distance function actually computes that metric. Moreover, the implementation must also prove (in its body for valid_distance_metric) that dist is a reasonable metric.

trait Distance {
    spec fn dist(&self, other: &Self) -> nat;

    fn distance(&self, other: &Self) -> (d: u64)
        ensures
            d as nat == self.dist(other),
    ;

    proof fn valid_distance_metric()
        ensures
            forall |x: &Self, y| x.dist(y) == y.dist(x),
            forall |x: &Self, y| x.dist(y) == 0 <==> x == y,
            forall |x: &Self, y, z| x.dist(y) <= x.dist(z) + z.dist(y),
        ;
}

Here’s an example of an implementation of our Distance trait:

struct P {
    u: u64
}

impl Distance for P {
    spec fn dist(&self, other: &Self) -> nat {
        vstd::math::abs(self.u - other.u)
    }

    fn distance(&self, other: &Self) -> u64 {
        if self.u > other.u {
            self.u - other.u
        } else {
            other.u - self.u
        }
    }

    proof fn valid_distance_metric() 
    {
    }
}

In this case, Verus can automatically prove all of the postconditions for valid_distance_metric, but a more complex distance metric might need additional proof annotations.

Note that it’s not necessary to repeat the requires/ensures that the implementation inherits from the trait definition.

The View trait

The most commonly used trait in vstd is View. It allows users to give executable types a mathematical abstraction (type V) accessed via the view function. Since this is such a commonly invoked function, Verus provides the @ operator as a shortcut, so that you can write x@ instead of x.view().

pub trait View {
    type V;
    spec fn view(&self) -> Self::V;
}

vstd provides View implementations for common types:

• Vec<T> → Seq<T>
• HashMap<K, V> → Map<K, V>
• HashSet<K> → Set<K>
• Primitive types (u64, bool, etc.) → themselves

To implement View for a custom type, choose an appropriate abstraction and then define type V and spec fn view:

struct Stack {
    data: Vec<u64>,
}

impl View for Stack {
    type V = Seq<u64>;

    closed spec fn view(&self) -> Seq<u64> {
        self.data@
    }
}

impl Stack {
    fn push(&mut self, val: u64)
        ensures final(self)@ == old(self)@.push(val),
    {
        self.data.push(val);
    }

    fn is_empty(&self) -> (result: bool)
        ensures result <==> self@.len() == 0,
    {
        self.data.len() == 0
    }
}

Because Stack’s data is a private field, view is closed — callers cannot see its definition, but they can still reason about the effect each function has on that view, as illustrated by the postconditions on push and is_empty. If you want callers to unfold @ to its definition (e.g., for a pub type with a pub field), use open spec fn view instead.

vstd also provides DeepView, which recursively applies the view abstraction to nested elements. Most code only needs View.

default_ensures: specifications for default function implementations

In Rust, a trait function can provide a default implementation — a body that implementations inherit if they do not override the function. This creates a subtle specification problem: the trait-level ensures clause must be weak enough to allow any valid override, but the default body may satisfy a stronger postcondition.

default_ensures solves this by separating these two concerns:

trait Reducer {
    // Every implementation must satisfy: output <= input.
    // The default implementation additionally satisfies: output == input / 2.
    fn halve(&self, input: u64) -> (output: u64)
        ensures output <= input,
        default_ensures output == input / 2,
    {
        input / 2
    }
}

Here the trait-level ensures (output <= input) is what any implementation must satisfy. The default_ensures (output == input / 2) is an additional guarantee that holds only when a type uses the default implementation without overriding it.

The rules:

• default_ensures is only allowed on a trait function that has a default body in the trait declaration.
• default_ensures is checked against the default body just like a normal ensures.
• Callers that statically know the type inherits the default learn both ensures and default_ensures; callers using a generic bound T: Trait learn only the ensures.

struct DefaultReducer;

impl Reducer for DefaultReducer {
    // No override: inherits the default implementation and its default_ensures.
}

struct ThirdReducer;

impl Reducer for ThirdReducer {
    // Overrides with a different strategy.  Only the trait `ensures` (output <= input)
    // applies to callers who don't statically know the type.
    fn halve(&self, input: u64) -> (output: u64)
        ensures output == input / 3,
    {
        input / 3
    }
}

fn call_generic<H: Reducer>(h: &H, x: u64) {
    let r = h.halve(x);
    assert(r <= x);        // From trait ensures — always available
    // assert(r == x / 2); // Would FAIL: not known for arbitrary H
}

fn call_default(h: &DefaultReducer, x: u64) {
    let r = h.halve(x);
    assert(r <= x);     // From trait ensures
    assert(r == x / 2); // From default_ensures (DefaultReducer uses the default impl)
}

fn call_override(h: &ThirdReducer, x: u64) {
    let r = h.halve(x);
    assert(r <= x);        // From trait ensures
    assert(r == x / 3);    // From ThirdReducer's own ensures
    // assert(r == x / 2); // Would FAIL: ThirdReducer overrides, no default_ensures
}

When writing your own trait, consider using default_ensures on functions where a sensible default makes a stronger promise that custom implementations are not required to match.

Common vstd trait specifications

vstd provides specifications for many standard library traits. A few worth knowing:

• PartialEq / Eq — vstd wraps these with an obeys_eq_spec() guard so that only types that opt in are assumed to satisfy the functional equality contract. See External trait specifications for the obeys_* pattern.
• Iterator — vstd provides IteratorSpecImpl (not Iterator directly) for writing specs on custom iterators. See Iterator Specifications.
• PartialOrd / Ord — similar to PartialEq, with obeys_ord_spec() guards.

External trait specifications

For adding specifications to traits from external crates (including std), see External trait specifications.