External trait specifications

When writing verified code that interacts with external Rust libraries, you may need to add specifications to traits defined in those libraries. Verus provides two attributes for this purpose:

#[verifier::external_trait_specification] — adds requires/ensures to trait methods
#[verifier::external_trait_extension] — additionally defines spec helper functions on the trait

Soundness warning

Be cautious when adding specifications to external traits. All implementations of the trait — including those in unverified code, even code that hasn’t been written yet — are assumed to uphold the specification. For example, if you verify a crate with pub fn test<A: Formatter>(...), Verus assumes that whatever type instantiates A will satisfy the Formatter specification, even if that type comes from an unverified crate. This is a contract on both current and future unverified code.

See below for a useful pattern (employed by vstd) for mitigating this soundness risk.

Basic external trait specification

Suppose we have an external trait:

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

We can add specifications to it with #[verifier::external_trait_specification]:

#[verifier::external_trait_specification]
trait ExEncoder {
    // This associated type names the trait being specified:
    type ExternalTraitSpecificationFor: Encoder;

    fn encode_value(&self, x: u64) -> (result: u64)
        ensures
            result >= x;
}

Key points about this syntax:

The specification trait (here ExEncoder) must contain a specially named associated type ExternalTraitSpecificationFor whose bound names the external trait being specified.
The trait name ExEncoder is arbitrary and is not used elsewhere.
Method signatures must match the external trait, but you can add requires and ensures clauses, and you can give a name to the return value (e.g., (result: u64)) for use in ensures.
The specification trait is not required to include all members of the external trait. Members that are not included are not accessible to verified code.

With the specification in place, verified code can use the trait:

fn use_encoder<E: Encoder>(f: &E, val: u64) -> (result: u64)
    ensures
        result >= val,
{
    f.encode_value(val)
}

External trait extension (spec helper functions)

Sometimes, a trait specification needs additional spec-mode functions that don’t exist in the original trait. For example, you may want a spec function that describes the abstract behavior of a method. The #[verifier::external_trait_extension] attribute supports this.

The attribute takes the form:

#[verifier::external_trait_extension(SpecTrait via SpecImplTrait)]

SpecTrait is the name of a spec-mode trait that becomes available in verification. It is automatically implemented for any type implementing the external trait.
SpecImplTrait is the name of a trait that concrete types implement to define the spec helper functions.

Here is an example, using a fictitious external trait named Summarizer:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(SummarizerSpec via SummarizerSpecImpl)]
trait ExSummarizer {
    type ExternalTraitSpecificationFor: Summarizer;

    // A spec helper function (not part of the original trait):
    spec fn spec_summary(&self) -> u64;

    fn summary(&self) -> (result: u64)
        ensures
            result == self.spec_summary();
}

Concrete types implement SpecImplTrait (here SummarizerSpecImpl) to define the spec helpers, and can then use the specifications in verified code:

struct MyCustomStruct { value: u64 }

// Implement the concrete external Summarizer trait
impl Summarizer for MyCustomStruct {
    fn summary(&self) -> u64 {
        // Prove that our overly complicated implementation satisfies the spec_summary
        let v = self.value;
        assert(v & 0xffff_ffff_ffff_ffff == v) by (bit_vector);
        v & 0xffff_ffff_ffff_ffff
    }
}

// Implement the additional spec functions
impl SummarizerSpecImpl for MyCustomStruct {
    spec fn spec_summary(&self) -> u64 {
        self.value
    }
}

fn test_hasher(h: &MyCustomStruct) {
    let v = h.summary();
    assert(v == h.value);
}

The `obeys_*` pattern in `vstd`

vstd uses external_trait_extension extensively for standard library traits like PartialEq, Ord, Add, From, etc. These specifications follow a common pattern using an obeys_* spec function that indicates whether a given type implementation actually follows the specification.

For example, vstd’s specification for PartialEq looks roughly like this:

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(PartialEqSpec via PartialEqSpecImpl)]
pub trait ExPartialEq<Rhs = Self> {
    type ExternalTraitSpecificationFor: PartialEq<Rhs>;

    spec fn obeys_eq_spec() -> bool;
    spec fn eq_spec(&self, other: &Rhs) -> bool;

    fn eq(&self, other: &Rhs) -> (r: bool)
        ensures
            Self::obeys_eq_spec() ==> r == self.eq_spec(other);
}

The ensures clause says: if the type obeys the Verus spec for Eq (obeys_eq_spec() is true), then the result matches eq_spec. For integer types and bool, vstd defines obeys_eq_spec() to be true, and proves that these types satisfy the eq_spec. For other types, Verus doesn’t know whether obeys_eq_spec() is true or false, so it won’t assume that the postcondition holds. This pattern lets vstd provide useful specifications for well-behaved types without making unsound assumptions about all types. If you want to use a trait like Eq for an external type, you can use an assume_specification to say that obeys_eq_spec() is true.

Rules and restrictions

The ExternalTraitSpecificationFor associated type is required and must name the external trait.
The specification trait should not have a body for any method.
Generic parameters and associated types must match the external trait exactly.
When using external_trait_extension, the two names (SpecTrait and SpecImplTrait) become real trait names; SpecTrait can be used in bounds and SpecImplTrait can be used in impl blocks.

Keyboard shortcuts