Macro 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 other than statement macros are treated similar to those in proof! Statement macros are not supported; invoke declaration macros in the surrounding scope or use proof! for proof statements.