Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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:

use vstd::contrib::exec_spec::*;
use vstd::prelude::*;

verus! {

exec_spec_verified! {

struct Point {
    x: i64,
    y: i64,
}

spec fn on_line(points: Seq<Point>) -> bool {
    forall |i: usize| #![auto] 0 <= i < points.len()
        ==> points[i as int].y == points[i as int].x
}

}

} // verus!

In the example, we define a simple spec function on_line to check if the given sequence of Points 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:

verus! {

fn main() {
    let p1 = ExecPoint { x: 1, y: 1 };
    let p2 = ExecPoint { x: 2, y: 2 };
    let points = vec![p1, p2];
    assert(on_line(points.deep_view()));
    let b = exec_on_line(points.as_slice());
    assert(b);
}

} // verus!

Currently, exec_spec_verified! supports these basic features:

  • Basic arithmetic operations
  • Logical operators (&&, ||, &&&, |||, not, ==>)
  • 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!.

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:

use vstd::contrib::exec_spec::*;
use vstd::prelude::*;

verus! {

exec_spec_unverified! {

struct Point {
    x: i64,
    y: i64,
}

spec fn on_line(points: Seq<Point>) -> bool {
    forall |i: usize| #![auto] 0 <= i < points.len()
        ==> points[i as int].y == points[i as int].x
}

}

} // verus!

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:

fn main() {
    let p1 = ExecPoint { x: 1, y: 1 };
    let p2 = ExecPoint { x: 2, y: 2 };
    let points = vec![p1, p2];
    let b = exec_on_line(points.as_slice());
    assert_eq!(b, true);
}

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, 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 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.

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 throw a runtime error if a precondition is violated (e.g. unwrapping a None) or if overflow occurs.

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, or use the when_used_as_spec attribute.