decreases_to!(b => a) means that height(a) < height(b), so that b can decrease to a
in decreases clauses.
decreases_to!(b1, …, bn => a1, …, am) can compare lexicographically ordered values,
which can be useful when making assertions about decreases clauses.
Notes:
proof_decl add extra stmts that are used only
for verification.
For example, declare a ghost/tracked variable.
To avoid confusion, let stmts without ghost/tracked is not supported.
Non-local stmts inside proof_decl! are treated similar to those in proof!
proof_with add ghost input/output to the next function call.
In stable rust, we cannot add attribute-based macro to expr/statement.
Using proof_with! to tell #[verus_spec] to add ghost input/output.
Using proof_with outside of #[verus_spec] does not have any side effects.
verus_proof_macro_explicit_exprs!(f!(tts)) applies verus syntax to transform tts into
tts', then returns f!(tts'), only applying the transform to any of the exprs within it that
are explicitly prefixed with @@, leaving the rest as-is. Contrast this to
[verus_proof_macro_exprs] which is likely what you want to try first to see if it satisfies
your needs.
verus_proof_macro_exprs!(f!(exprs)) applies verus syntax to transform exprs into exprs’,
then returns f!(exprs’),
where exprs is a sequence of expressions separated by “,”, “;”, and/or “=>”.
derive(Structural) means that exec-mode == and ghost == always yield the same result.
derive(Structural) is only allowed when all the fields of a type are also Structural.
derive(StructuralEq) means derive(Structural) and also implement PartialEqSpec,
setting eq_spec to == and obeys_eq_spec to true.