Macro vstd::prelude::proof_decl

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

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!