returns #

The returns clause is syntactic sugar for an ensures clause of a certain form. The returns clause can be provided instead of or in addition to an ensures clause.

The following:

fn example() -> return_type
    returns $expr
{
  ...
}

is equivalent to:

fn example() -> (return_name: return_type)
    ensures return_name == $expr
{
  ...
}

With the #[verifier::allow_in_spec] attribute #

The #[verifier::allow_in_spec] attribute can be applied to an executable function with a returns clause. This allows the function to be used in spec mode, where it is interpreted as equivalent to the specified return-value.