assert … by(…)

The assert ... by statement is used to invoke a specialized prover mode for proving the given assertion.

Syntax

We divide the prover modes into “solver modes” (which invoke a solver) and “interpreter modes” (which invoke the interpreter).

assert_by_prover_stmt ::=
    assert ( spec_expr ) by ( assert_by_solver_mode ) assert_by_prover_requires? ;
  | assert ( spec_expr ) by ( assert_by_interpreter_mode );

assert_by_solver_mode ::= nonlinear_arith | bit_vector;
assert_by_interpreter_mode ::= compute | compute_only;

assert_by_prover_requires ::=
    requires (spec_expr,)+

Note

At present, the integer_ring prover mode may only be used in a proof function declaration, not in an assert-by.

Proof operation

Solver modes. For nonlinear_arith and bit_vector modes, Verus attempts to prove the given predicate via the specified solver (the nonlinear_arith solver or the bit_vector solver). The predicate is proved in isolation, absent any surrounding context.

Specifically, for a statement assert ( Q ) by ( assert_by_solver_mode ), Verus tries to prove Q using the solver, and then assumes Q for the subsequent code.

If a requires P clause is additionally provides, then Verus:

• Proves P using the default solver (with full context available)
• Proves P ==> Q using the specified solver (in isolation)
• And finally assumes Q for subsequent code.

Interpreter modes. For compute and compute_only modes, Verus uses its specification interpreter to simplify the expression Q as much as possible, yielding an expression Q'.

• For compute_only, Verus will check that Q' is the boolean value true, and then assumes the given predicate for all subsequent code.
• For compute, Verus will replace the assert-by statement with assert(Q'), which then behaves like an ordinary assert.