feat(fv): disable fv in non fv nargo commands

Formal verification attributes are now ignored in all other (non fv)
nargo cli commands and won't produce any errors related to semantic
analysis.

Also expanded the testing logic. Now there are two directories for
testing formal verification functionality. Them being
`formal_verify_failure` and `formal_verify_success`.

Moved the tests from PR #88 in their matching directories.

compiler/noirc_frontend/src/elaborator/comptime.rs

@@ -97,6 +97,7 @@ impl<'context> Elaborator<'context> {
             self.crate_id,
             self.debug_comptime_in_file,
             self.interpreter_call_stack.clone(),
+            self.formal_verification,
         );
 
         elaborator.function_context.push(FunctionContext::default());

compiler/noirc_frontend/src/elaborator/mod.rs

@@ -174,6 +174,9 @@ pub struct Elaborator<'context> {
     unresolved_globals: BTreeMap<GlobalId, UnresolvedGlobal>,
 
     pub(crate) interpreter_call_stack: im::Vector<Location>,
+
+    /// Indicates if we have to elaborate or ignore formal verification attributes.
+    formal_verification: bool,
 }
 
 #[derive(Default)]
@@ -197,6 +200,7 @@ impl<'context> Elaborator<'context> {
         crate_id: CrateId,
         debug_comptime_in_file: Option<FileId>,
         interpreter_call_stack: im::Vector<Location>,
+        formal_verification: bool,
     ) -> Self {
         Self {
             scopes: ScopeForest::default(),
@@ -221,6 +225,7 @@ impl<'context> Elaborator<'context> {
             current_trait: None,
             interpreter_call_stack,
             in_comptime_context: false,
+            formal_verification,
         }
     }
 
@@ -235,6 +240,7 @@ impl<'context> Elaborator<'context> {
             crate_id,
             debug_comptime_in_file,
             im::Vector::new(),
+            context.formal_verification,
         )
     }
 
@@ -436,7 +442,7 @@ impl<'context> Elaborator<'context> {
         }
 
         if let Some(attr) = attributes {
-            if !attr.fv_attributes.is_empty() {
+            if !attr.fv_attributes.is_empty() && self.formal_verification {
                 self.elaborate_fv_attributes(
                     attr.fv_attributes.clone(),
                     &id,

tooling/nargo_cli/build.rs

@@ -47,6 +47,8 @@ fn main() {
     generate_plonky2_verify_failure_tests(&mut test_file, &test_dir);
     generate_plonky2_trace_tests(&mut test_file, &test_dir);
     generate_plonky2_show_plonky2_regression_tests(&mut test_file, &test_dir);
+    generate_formal_verify_success_tests(&mut test_file, &test_dir);
+    generate_formal_verify_failure_tests(&mut test_file, &test_dir);
 }
 
 /// Some tests are explicitly ignored in brillig due to them failing.
@@ -701,3 +703,77 @@ fn plonky2_show_plonky2_regression_{test_name}() {{
         .expect("Could not write templated test file.");
     }
 }
+
+/// Tests which must succeed after undergoing formal verification.
+fn generate_formal_verify_success_tests(test_file: &mut File, test_data_dir: &Path) {
+    let test_type = "formal_verify_success";
+    let test_cases = read_test_cases(test_data_dir, test_type);
+    for (test_name, test_dir) in test_cases {
+        write!(
+            test_file,
+            r#"
+#[test]
+fn formal_verify_success_{test_name}() {{
+    let test_program_dir = PathBuf::from("{test_dir}");
+
+    let mut cmd = Command::cargo_bin("nargo").unwrap();
+    cmd.arg("--program-dir").arg(test_program_dir);
+    cmd.arg("formal-verify");
+
+    cmd.assert().success();
+}}
+            "#,
+            test_dir = test_dir.display(),
+        )
+        .expect("Could not write templated test file.");
+    }
+}
+
+/// Tests which must fail during formal verification.
+fn generate_formal_verify_failure_tests(test_file: &mut File, test_data_dir: &Path) {
+    let test_type = "formal_verify_failure";
+    let test_cases = read_test_cases(test_data_dir, test_type);
+
+    let expected_messages = HashMap::from([("simple_add", vec!["Cannot satisfy constraint"])]);
+
+    for (test_name, test_dir) in test_cases {
+        write!(
+            test_file,
+            r#"
+#[test]
+fn formal_verify_failure_{test_name}() {{
+    let test_program_dir = PathBuf::from("{test_dir}");
+
+    let mut cmd = Command::cargo_bin("nargo").unwrap();
+    cmd.arg("--program-dir").arg(test_program_dir);
+    cmd.arg("formal-verify");
+
+    cmd.assert().failure().stderr(predicate::str::contains("The application panicked (crashed).").not());"#,
+            test_dir = test_dir.display(),
+        )
+        .expect("Could not write templated test file.");
+
+        // Not all tests have expected messages, so match.
+        match expected_messages.get(test_name.as_str()) {
+            Some(messages) => {
+                for message in messages.iter() {
+                    write!(
+                        test_file,
+                        r#"
+    cmd.assert().failure().stderr(predicate::str::contains("{message}"));"#
+                    )
+                    .expect("Could not write templated test file.");
+                }
+            }
+            None => {}
+        }
+
+        write!(
+            test_file,
+            r#"
+}}
+"#
+        )
+        .expect("Could not write templated test file.");
+    }
+}