const declarations
In Verus, const
declarations are treated internally as 0-argument function calls.
Thus just like functions, const
declarations can be marked spec
, proof
, exec
,
or left without an explicit mode.
By default, a const
without an explicit mode is assigned a dual spec/exec
mode.
We’ll go through what each of these modes mean.
spec
consts
A spec const
is like a spec
function with no arguments.
It is always ghost and cannot be used as an exec
value.
spec const SPEC_ONE: int = 1;
spec fn spec_add_one(x: int) -> int {
x + SPEC_ONE
}
proof
and exec
consts
Just as proof
and exec
functions can have ensures
clauses specifying a postcondition,
proof
and exec
consts can have ensures
clauses to tie the declaration to a spec
expression.
The syntax follows the syntax of a function definition.
exec const C: u64
ensures
C == 7,
{
7
}
Note here that we can also use assert
when defining the const,
and that we can define it using a call to another const
function.
spec fn f() -> int {
1
}
const fn e() -> (u: u64)
ensures
u == f(),
{
1
}
exec const E: u64
ensures
E == 2,
{
assert(f() == 1);
1 + e()
}
spec/exec
consts
A const
without an explicit mode is dual-use:
it is usable as both an exec
value and a spec
value.
const ONE: u8 = 1;
fn add_one(x: u8) -> (ret: u8)
requires
x < 0xff,
ensures
ret == x + ONE, // use "ONE" in spec code
{
x + ONE // use "ONE" in exec code
}
Therefore, the const
definition is restricted to obey the rules
for both exec
code and spec
code.
For example, as with exec
code, its type must be compilable (e.g. u8
, not int
),
and, as with spec
code, it cannot call any exec
or proof
functions.
const fn foo() -> u64 { 1 }
const C: u64 = foo(); // FAILS with error "cannot call function `foo` with mode exec"
Using an exec const
in a spec
or proof
context
Similar to functions, if you want to use an exec const
in a spec
or proof
context,
you can annotate the declaration with [verifier::when_used_as_spec(SPEC_DEF)]
,
where SPEC_DEF
is the name of a spec const
or a spec
function with no arguments.
use vstd::layout;
global layout usize is size == 8;
spec const SPEC_USIZE_BYTES: usize = layout::size_of_as_usize::<usize>();
#[verifier::when_used_as_spec(SPEC_USIZE_BYTES)]
exec const USIZE_BYTES: usize
ensures
USIZE_BYTES as nat == layout::size_of::<usize>(),
{
8
}
In this example, without the annotation, Verus will give the error “cannot read const with mode exec.”
Moreover, attempting to use the annotation
#[verifier::when_used_as_spec(layout::size_of::<usize>)]
,
without defining SPEC_USIZE_BYTES
separately,
will also result in an error:
when_used_as_spec
can only handle the case when two functions or consts have the same signature.
It doesn’t handle using something like ::<usize>
to coerce a function to a different signature.
Trouble-shooting overflow errors
Verus may have difficulty proving that a const
declaration does not overflow;
using [verifier::when_used_as_const(SPEC_DEF)]
or [verifier::non_linear]
may help.
For example, here [verifier::non_linear]
is added to prevent the error
“possible arithmetic underflow/overflow.”
This allows Verus to reason about the (seemingly)
non-linear expression BAR_PLUS_ONE * BAR
,
instead of giving up immediately.
See the chapter on non-linear reasoning for more details.
pub const FOO: u8 = 4;
pub const BAR: u8 = FOO;
pub const BAR_PLUS_ONE: u8 = BAR + 1;
#[verifier::nonlinear]
pub const G: u8 = BAR_PLUS_ONE * BAR;