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:

{{#include ../../../../examples/guide/traits.rs:basic_trait}}

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.

{{#include ../../../../examples/guide/traits.rs:impl_extends}}

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:

{{#include ../../../../examples/guide/traits.rs:requires_ensures}}

{{#include ../../../../examples/guide/traits.rs:requires_ensures_impl}}

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.

{{#include ../../../../examples/guide/traits.rs:dispatch}}

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.

{{#include ../../../../examples/guide/traits.rs:spec_trait}}

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

{{#include ../../../../examples/guide/traits.rs:spec_trait_impl}}

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:

{{#include ../../../../examples/guide/traits.rs:view_impl}}

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:

{{#include ../../../../examples/guide/traits.rs:default_ensures}}

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.

{{#include ../../../../examples/guide/traits.rs:default_ensures_impls}}

{{#include ../../../../examples/guide/traits.rs:default_ensures_callers}}

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.