Rust subset #

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

Function calls #

Syntax:

V@[fn_call_expr] ::= R@[path] ( V@[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:

V@[spec_block_expr] ::= { V@[spec_let_stmt]* V@[spec_expr] }
V@[spec_let_stmt]   ::= let R@[pattern] = V@[spec_expr];

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

if / if let / match expressions #

Syntax:

V@[if_expr]     ::= if V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
V@[if_let_expr] ::= if let R@[pattern] = V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
V@[match_expr]  ::= match R@[expr] { R@[match_arms] }

These work as normal.

&& and || #

Syntax:

V@[and_expr] ::= V@[spec_expr] && V@[spec_expr]
V@[or_expr]  ::= V@[spec_expr] || V@[spec_expr]
V@[not_expr] ::= ! V@[spec_expr]

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

Equality (==) #

Syntax:

V@[equality_expr] ::= V@[spec_expr] == V@[spec_expr]
                | V@[spec_expr] != V@[spec_expr]

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

Arithmetic #

Syntax:

V@[arith_expr] ::= V@[spec_expr] \+ V@[spec_expr]
             | V@[spec_expr] - V@[spec_expr]
             | - V@[spec_expr]
             | V@[spec_expr] \* V@[spec_expr]
             | V@[spec_expr] / V@[spec_expr]
             | V@[spec_expr] % V@[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:

V@[ref_expr]   ::= & V@[spec_expr]
V@[deref_expr] ::= \* V@[spec_expr]

Verus attempts to ignore Box and references as much as possible in spec mode. However, you still need 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:

V@[box_new_expr] ::= Box::new( V@[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.