Attribute Macro auto_spec

#[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.