Requested feature: Create an attribute that allow users to mark their proof harness functions.
Use case: The same way users can tag their test functions using the #[test] attribute, users should be able to tag their proof harness with an attribute such as #[proof]. We can then create a cargo subcommand, like cargo verify that will execute all proofs in a crate.

Link to relevant documentation (Rust reference, Nomicon, RFC): N/A
Is this a breaking change? No

Test case:

We could modify the test in src/test/expected/enum/main.rs to be something like:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

/* other stuff */

#[cfg(rmc)]
mod rmc_tests {
    use super::*;
    #[proof]
    fn test_one_plus_two() {
        let p = Pair::new(1, 2);
        assert!(p.sum() == 3);
    }
}