Macro vstd::prelude::proof_with

proof_with!() { /* proc-macro */ }

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.