assume_specification

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 generics? [ function_path ] (args...) -> return_type_and_name?
    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;