assume_specification

Caution

Since the assume_specification statement is unchecked, it can easily be used to subvert Verus’s guarantees.

Be sure to read our advice on interacting with unverified code.

The assume_specification directive tells Verus to use the given specification for the given function. Verus assumes that this specification holds without proof.

It can be used with any exec-mode function that Verus would otherwise be unaware of; for example, any function marked external or which is imported from an external crate.

It is similar to having a function which is external_body; the difference is that when assume_specification is used, the specification is separate from the function declaration and body.

The assume_specification declaration does NOT have to be in the same module or crate as its corresponding function. However:

• The function must be visible to its assume_specification declaration
• The assume_specification declaration must be visible wherever the function is visible.

The general form of this directive is:

assume_specification_item ::=
    visibility? assume_specification generics? [ function_path ] (args...) ( -> exec_return_type )?
        where_clause?
        requires_clause?
        ensures_clause?
        returns_clause?
        invariants_clause?
        unwind_clause?
        ;

It is intended to look like an ordinary Rust function signature with a Verus specification, except instead of having a name, it refers to a different function by path.

For associated functions and methods, the function_path should have the form Type::method_name, using “turbofish syntax” for the type (e.g., Vec::<T>). For trait methods, the function_path should use the “qualified self” form, <Type as Trait>::method_name.

The signature must be the same as the function in question, including arguments, return type, generics, and trait bounds. All arguments should be named and should not use self.

Examples

To apply to an ordinary function:

pub assume_specification<T> [core::mem::swap::<T>] (a: &mut T, b: &mut T)
    ensures
        *a == *old(b),
        *b == *old(a),
    opens_invariants none
    no_unwind;

To apply to an associated function of Vec:

pub assume_specification<T>[Vec::<T>::new]() -> (v: Vec<T>)
    ensures
        v@ == Seq::<T>::empty();

To apply to an method of Vec:

pub assume_specification<T, A: Allocator>[Vec::<T, A>::clear](vec: &mut Vec<T, A>)
    ensures
        vec@ == Seq::<T>::empty();

To apply to clone for a specific type:

pub assume_specification [<bool as Clone>::clone](b: &bool) -> (res: bool)
    ensures res == b;

Type signature matching

Verus requires the type signature and trait bounds to match exactly. If these do not line up, you will get an error message displaying the mismatched signature or mismatched trait bounds. It can sometimes be nontrivial to get these to line up due to differences in the source form and the internal form.

Tips:

1. It usually helps to make all lifetime variables (e.g., 'a) explicit.

2. The Sized trait is somewhat complex, as the source form of Sized-bounds doesn’t always look like Rust’s internal representation of the trait bound. This is also complicated by unstable Sized features. As of Rust 1.95.0, these are related as follows: