This macro takes an expresion of the form:
set_build!{ elem_expr: optional_typ | x1: typ1 in ..., ..., xn: typn in ..., cond1, ..., condm }
or just:
set_build!{ x: typ in ..., cond1, ..., condm }
where each xk: typk in ... has one of the following forms:
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.