assume

Caution

Since the assume statement is unchecked, it can easily be used to subvert Verus’s guarantees. In particular, successful “verification” by Verus provides no guarantees on the program if it includes any assume statements, unless those assume statements could in principle be replaced by a successful assert statement.

The assume statement is most useful during intermediate stages of development, e.g., within an assert/assume-driven proof-development process.

Tip

The --no-cheating flag can be used to disallow assume statements.

Syntax

assume ::= assume (spec_expr) ;

Proof operation

Assume the given predicate without proof.