Add a `#[proof]` attribute that allow us to mark proof harnesses

[celinval]

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);
    }
}

[camshaft]

Is there a reason not to use the existing #[test] attribute? It has an advantage of potentially being able to use existing tests as proof harnesses.

[celinval]

Is there a reason not to use the existing #[test] attribute? It has an advantage of potentially being able to use existing tests as proof harnesses.

That's a good question and a great suggestion. It would definitely be nice to be able to use tests as proof harnesses.

I'm not quite sure the opposite applies though, harnesses not necessarily should run as tests. There are constructs such as non-deterministic assignments that don't make sense in tests.

[camshaft]

I'm not quite sure the opposite applies though, harnesses not necessarily should run as tests.

Ah that's a good point. In that case you would need to have the #[proof] attribute, or at the very least #[cfg(rmc)].