Automatically compiles spec items to exec items, but without proofs of functional correctness.
This means that,iIn contrast to exec_spec_verified!, all specifications on compiled executable code generated by exec_spec_unverified! are trusted.
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 “=>”.
This copies the body of an exec function into a “returns” clause,
so that the exec function will be also usable as a spec function.
For example,
#[vstd::contrib::auto_spec] fn f(u: u8) -> u8 { u / 2 }
becomes:
#[verifier::allow_in_spec] fn f(u: u8) -> u8 returns (u / 2) { u / 2 }
The macro performs some limited fixups, such as removing proof blocks
and turning +, -, and * into add, sub, mul.
However, only a few such fixups are currently implemented and not all exec bodies
will be usable as return clauses, so this macro will not work on all exec functions.