# Producing executable code from spec functions with the `exec_spec_verified!` and `exec_spec_unverified!` macros

When writing proofs in Verus, we occasionally need to
implement some simple function or data structure in both exec
and spec modes, and then establish their equivalence.
This process can be tedious for simple functions.

The `exec_spec_verified!` macro simplifies this process: you only need
to write the desired functions/structs/enums in spec mode within
the supported fragment of `exec_spec_verified!`, and then the macro can
automatically generate exec counterparts of these spec items,
as well as proofs of equivalence. These proofs also ensure termination,
the absence of arithmetic overflow, and the absence of precondition violations.

The `exec_spec_unverified!` macro also automatically compiles spec code to exec code,
but without proofs of equivalence. That is, all executable code with specifications 
generated by `exec_spec_unverified!` is annotated with `#[verifier::external_body]`, so
the equivalence between the spec and the exec code is not proven by Verus.
The `exec_spec_unverified!` macro currently supports a larger fragment of Verus, 
and is ideal for scenarios where the compiled code is not invoked in a verified project 
(e.g., testing specifications on example inputs).
Skipping the proof generation sidesteps potential proof debugging in the
compiled exec code.

## Unverified translations of `vstd` functions within the `exec_spec_verified!` and `exec_spec_unverified!` macros

To enable greater expressivity, the `exec_spec_verified!` and `exec_spec_unverified!` macros support the use of
several spec functions on types in `vstd` (such as `Seq`) within the macros. This means that exec 
translations of supported spec functions are already provided by the macro. These translations 
are used for compiling spec code which invokes such functions to exec code. The full list of 
functions supported by each macro can be found below.

For many `vstd` functions, however, the translation from spec code to the exec equivalent is unverified. 
Each case is marked clearly with a \* below. We hope to reduce the number of unverified translations as Verus expands
its support for Rust language features.

## The `exec_spec_verified!` macro

Here is an example:
```rust
{{#include ../../../../examples/guide/exec_spec_verified.rs:example}}
```
In the example, we define a simple spec function `on_line` to check if
the given sequence of `Point`s have the same coordinates.

The `exec_spec_verified!` macro call in this example takes all spec items in
its scope, and then derives executable counterparts along the lines of
the following definitions:
```
struct ExecPoint {
    x: i64,
    y: i64,
}

impl DeepView for ExecPoint {
    type V = Point;
    ...
}

fn exec_on_line(points: &[ExecPoint]) -> (res: bool)
    ensures res == on_line(points.deep_view())
{ ... }
```

After the macro invocation, we have the original spec items
as before (`Point` and `on_line`), but also new items `ExecPoint` and
`exec_on_line` with a suitable equivalence verified.
We can test the equivalence using the following sanity check:
```rust
{{#include ../../../../examples/guide/exec_spec_verified.rs:check}}
```

Currently, `exec_spec_verified!` supports these basic features:
  - Basic arithmetic operations
  - Logical operators (`&&`, `||`, `&&&`, `|||`, `!`, `==>`)
  - If, match and "matches"
  - Field expressions
  - Spec function calls and recursion
  - Bounded quantifiers of the form `forall |i: <type>| <lower> <op> i <op> <upper> ==> <expr>` and `exists |i: <type>| <lower> <op> i <op> <upper> && <expr>`, where:
    - `<op>` is either `<=` or `<`
    - `<type>` is a Rust primitive integer (`i<N>`, `isize`, `u<N>`, `usize`)
  - `SpecString` (an alias to `Seq<char>` to syntactically indicate that we want `String`/`&str`), equality\*, indexing, len, string literals
  - `Option<T>` with these functions:
    - equality, `unwrap`
  - `Seq<T>` (compiled to `Vec<T>` or `&[T]` depending on the context), `seq!` literals, and these `Seq` functions:
    - equality\*, `len`, indexing, `subrange`\*, `add`\*, `push`\*, `update`\*, `empty`, `to_multiset`\*, `drop_first`\*, `drop_last`\*, `take`\*, `skip`\*, `first`, `last`, `is_suffix_of`\*, `is_prefix_of`\*, `contains`\*, `index_of`\*, `index_of_first`\*, `index_of_last`\*
  - `Map<K, V>` (compiled to `HashMap<K, V>`), and these `Map` functions:
    - equality\*, `len`\*, indexing\*, `empty`, `dom`\*, `insert`\*, `remove`\*, `get`\*
    - Note: indexing is only supported on `Map<K, V>` where `K` is a primitive type (e.g. `usize`); for other types `K`, use `get` instead.
  - `Set<T>` (compiled to `HashSet<T>`), and these `Set` functions:
    - equality\*, `len`\*, `empty`, `contains`\*, `insert`\*, `remove`\*, `union`\*, `intersect`\*, `difference`\*
  - `Multiset<T>` (compiled to `ExecMultiset<T>`, a type implemented in `vstd::contrib::exec_spec` whose internal representation is a `HashMap`), and these `Multiset` functions: 
    - equality\*, `len`\*, `count`\*, `empty`\*, `singleton`\*, `add`\*, `sub`\*
  - User-defined structs and enums. These types should be defined within the macro using spec-compatible types for the fields (e.g. `Seq`). Such types are then compiled to their `Exec-` versions, which use the exec versions of each field's type (e.g. `Vec`/slice).
  - Primitive integer/boolean types (`i<N>`, `isize`, `u<N>`, `usize`, `char`, etc.). Note that `int` and `nat` cannot be used in `exec_spec_verified!` or `exec_spec_unverified!`.
  - `is` and `isnt` expressions, both on `Option`/`Result` and on user-defined enums.
  - Dereference expressions (`*x`).
  - `impl` blocks with spec methods on user-defined structs and enums. 
    - Only `&self` methods are supported. 
    - Each spec method `T::method` is compiled to an exec method `ExecT::exec_method`, and method calls like `x.method(...)` inside the macro are compiled to `x.exec_method(...)`. 
    - Generic and trait implementations are not supported.

Functions marked with \* have unverified translations from spec to exec code.

## The `exec_spec_unverified!` macro

Here is the same example as above, but with the `exec_spec_unverified!` macro:
```rust
{{#include ../../../../examples/guide/exec_spec_unverified.rs:example}}
```

The same exec items are generated as with the `exec_spec_verified!` macro, 
except the specs on executable functions are not proven by Verus:
```
#[verifier::external_body]
fn exec_on_line(points: &[ExecPoint]) -> (res: bool)
    ensures res == on_line(points.deep_view())
{ ... }
```

We can run the executable function `exec_on_line` to sanity check the output of
the compiled `on_line` spec on a specific input using the following:
```rust
{{#include ../../../../examples/guide/exec_spec_unverified.rs:check}}
```

The `exec_spec_unverified!` macro supports all of the same Verus features as `exec_spec_verified!`, as well as these additional features:
  - More general bounded quantifiers. Quantifier expressions must match this form: `forall |x1: <type1>, x2: <type2>, ..., xN: <typeN>| <guard1> && <guard2> && ... && <guardN> ==> <body>` or `exists |x1: <type1>, x2: <type2>, ..., xN: <typeN>| <guard1> && <guard2> && ... && <guardN> && <body>`, where:
    - `<guardI>` is of the form: `<lowerI> <op> xI <op> <upperI>`, where:
        - `<op>` is either `<=` or `<`
        - `<lowerI>` and `<upperI>` can mention `xJ` for all `J < I`
    - `<typeI>` is a Rust primitive integer (`i<N>`, `isize`, `u<N>`, `usize`) or `char`. Note that `char` is not supported by quantifiers in `exec_spec_verified!`.

## Common errors

### Indexing on `Seq`

When indexing on a `Seq`, the compilation process expects a `usize` which is cast to an `int` in the spec code. 
The `int` cast will be removed by the compilation process, but it is necessary for the spec code to be accepted by Verus, 
because `Seq::index` expects an `int`.

Here is a correct example:
```
pub open spec fn my_index(s: Seq<u8>, i: usize) -> u8 
    recommends 0 <= i < s.len()
{
    s[i as int]
}
```
The following is incorrect because `i` is `u64` instead of `usize`. This will result in a type error.
```
pub open spec fn my_index_err1(s: Seq<u8>, i: u64) -> u8 
    recommends 0 <= i < s.len()
{
    s[i as int]
}
```
The following is incorrect because the compilation process expects that the index is cast to an `int` in the spec code.
This will also result in a type error.
```
pub open spec fn my_index_err2(s: Seq<u8>, i: usize) -> u8 
    recommends 0 <= i < s.len()
{
    s[i]
}
```

### Indexing on `Map`

To do indexing on a `Map<K, V>`, the key type `K` must be a primitive type. 
Using a non-primitive for `K` will result in a type error when indexing is used.

As a workaround, use `Map::get` if a non-primitive type must be used for `K`.

The following is not supported by the macros:
```
pub struct Data {
    x: usize
}

pub open spec fn my_index_err(m: Map<Data, u8>, i: Data) -> u8 
    recommends m.dom().contains(i)
{
    m[i]
}
```

Use this instead:
```
pub struct Data {
    x: usize
}

pub open spec fn my_index_map(m: Map<Data, u8>, i: Data) -> u8
    recommends m.dom().contains(i)
{
    m.get(i).unwrap()
}
```

### Arithmetic operators

Due to the [widening that Verus performs on arithmetic in spec code](spec-arithmetic.md), an arithmetic expression (like `a + b`) may have a different type than its operands. This means that sometimes the type of an arithmetic expression is unsupported by the `exec_spec_verified!` and `exec_spec_unverified!` macros (i.e., `int` or `nat`), even if the types of both of the operands are supported (e.g., `u64`).

For example, the following will result in a type error, because for `x: u64` and `y: u64`, Verus types `x + y` in spec code as an `int`.
```
pub open spec fn my_arith_err(x: u64, y: u64) -> u64 
{
    x + y
}
```

To fix this, you must cast the result to `u64`:
```
pub open spec fn my_arith(x: u64, y: u64) -> u64 
{
    (x + y) as u64
}
```

### Fully qualified paths

The `exec_spec_verified!` and `exec_spec_unverified!` macros do not currently support fully qualified paths, such as `vstd::multiset::Multiset`. To use types from another module, you should import the module at the top of the file and use the unqualified path (in this previous case, this would be `Multiset`). Using the fully qualified path will result in a type error.

### `impl` block limitations

The `impl` blocks supported by the macros have several restrictions:

- Only `&self` is supported as the receiver. Using `self` by value or
  `&mut self` will result in an error.
- Generic and trait implementations are not supported.

For example, the following are all rejected:
```
impl W {
    pub open spec fn get(self) -> u32 { self.v }       // self by value
}

impl W {
    pub open spec fn get(&mut self) -> u32 { self.v }  // &mut self
}

impl<T> W { ... }                                      // generics

impl MyTrait for S { ... }                             // trait impl
```

## Running code generated by `exec_spec_unverified!`

The `exec_spec_unverified!` macro does not generate Verus proofs for termination, the absence of arithmetic overflow, or the satisfaction of function preconditions within the compiled executable code. This differs from `exec_spec_verified!`. Instead, the code generated by `exec_spec_unverified!` will panic at runtime if a precondition is violated (e.g. unwrapping a `None`) or if overflow occurs.

## Related

`exec_spec_verified!` and `exec_spec_unverified!` compile spec items to exec items, which might not cover your use case.
For example, you may want to go from [exec to spec](exec_to_spec.html), 
or use the [`when_used_as_spec` attribute](reference-attributes.html).