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);
}
} 
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, likecargo verifythat 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: