assert … by

The assert ... by statement is used to encapsulate a proof.

Syntax

assert_by_stmt ::= assert ( spec_expr ) by { proof_stmt* }

Proof operation

For a boolean predicate P:

assert(P) by {
    // ... proof here
}
// ... remainder

Verus will validate the proof and then attempt to use it to prove P. The contents of the proof, however, will not be included in the context used to prove the remainder. Only P will be introduced into the context for the remainder.