The compute mode #

Methods of invocation #

By assertion. The compute and compute_only modes can be invoked via an assert-by statement:

assert(Q) by(compute_only);

Proves Q by simplifying it via the interpreter and checking if the result is the boolean value true.

assert(Q) by(compute);

Proves Q by simplifying it via the interpreter to an expression Q' and replacing the statement with assert(Q');.

Interpreter operation #

The interpreter unfolds function definitions and evaluates arithmetic expressions. It is capable of some symbolic manipulation, but it does not handle algebraic laws like a + b == b + a, and it works best when evaluating constant expressions.

Note that it will not substitute local variables, instead treating them as symbolic values.

This statement:

assert(P) by(compute);

Will first run the interpreter as above, but if it doesn't succeed, it will then attempt to finish the problem through the normal solver. So for example, if after expansion P results in a trivial expression like a+b == b+a, then it should be solved with by(compute).

Configuring the evaluation strategy #

The #[verifier::memoize] attribute can be used to mark certain functions for memoizing. This will direct Verus's internal interpreter to only evaluate the function once for any given combination of arguments. This is useful for functions that would be impractical to evaluate naively, as in this example:

{{#include ../../../../examples/guide/assert_by_compute.rs:fibonacci_memoize}}