Modules§
- exec_
spec - This module provides runtime utilities for the compiled
executable code of [
builtin_macros::exec_spec].
Attribute Macros§
- auto_
spec - 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.