Rust subset

Much of the spec language looks like a subset of the Rust language, though there are some subtle differences.

Function calls

Syntax:

fn_call_expr ::= path ( spec_expr,* )

Only pure function calls are allowed (i.e., calls to other spec functions or functions marked with the when_used_as_spec directive).

Let-assignment

Syntax:

spec_block_expr ::= { spec_let_stmt* spec_expr }
spec_let_stmt   ::= let pattern = spec_expr;

Spec expressions support let-bindings, but not let mut-bindings.

if / if let / match statements

Syntax:

if_expr     ::= if spec_expr { spec_expr } else { spec_expr }
if_let_expr ::= if let pattern = spec_expr { spec_expr } else { spec_expr }
match_expr  ::= match expr { match_arms }

These work as normal.

&& and ||

Syntax:

and_expr ::= spec_expr && spec_expr
or_expr  ::= spec_expr || spec_expr
not_expr ::= ! spec_expr

These work as normal, though as all spec expressions are pure and effectless, there is no notion of “short-circuiting”.

Equality (==)

Syntax:

equality_expr ::= spec_expr == spec_expr
                | spec_expr != spec_expr

This is not the same thing as == in exec-mode; see more on ==.

Arithmetic

Syntax:

arith_expr ::= spec_expr + spec_expr
             | spec_expr - spec_expr
             | - spec_expr
             | spec_expr * spec_expr
             | spec_expr / spec_expr
             | spec_expr % spec_expr

Arithmetic works a little differently in order to operate with Verus’s int and nat types. See more on arithmetic.

References (&T)

Syntax:

ref_expr   ::= & spec_expr
deref_expr ::= * spec_expr

Verus attempts to ignore Box and references as much as possible in spec mode. However, you still needs to satisfy the Rust type-checker, so you may need to insert references (&) or dereferences (*) to satisfy the checker. Verus will ignore these operations however.

Box

Syntax:

box_new_expr ::= Box::new( spec_expr )

Verus special-cases Box<T> along with box operations like Box::new(x) or *box so they may be used in spec mode. Like with references, these operations are ignored, however they are often useful. For example, to create a recursive type you need to satisfy Rust’s sanity checks, which often involves using a Box.