feat(ssa): Implement missing brillig constraints SSA check (#6658)

Co-authored-by: Michael J Klein <michaeljklein@users.noreply.github.com>
Co-authored-by: Akosh Farkash <aakoshh@gmail.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>

.github/workflows/test-rust-workspace-msrv.yml

@@ -87,6 +87,7 @@ jobs:
           name: nextest-archive
       - name: Run tests
         run: |
+          RUST_MIN_STACK=8388608 \
           cargo nextest run --archive-file nextest-archive.tar.zst \
             --partition count:${{ matrix.partition }}/4 \
             --no-fail-fast

.github/workflows/test-rust-workspace.yml

@@ -74,6 +74,7 @@ jobs:
           name: nextest-archive
       - name: Run tests
         run: |
+          RUST_MIN_STACK=8388608 \
           cargo nextest run --archive-file nextest-archive.tar.zst \
             --partition count:${{ matrix.partition }}/4 \
             --no-fail-fast

compiler/noirc_driver/src/lib.rs

@@ -131,6 +131,12 @@ pub struct CompileOptions {
     #[arg(long)]
     pub skip_underconstrained_check: bool,
 
+    /// Flag to turn off the compiler check for missing Brillig call constrains.
+    /// Warning: This can improve compilation speed but can also lead to correctness errors.
+    /// This check should always be run on production code.
+    #[arg(long)]
+    pub skip_brillig_constraints_check: bool,
+
     /// Setting to decide on an inlining strategy for Brillig functions.
     /// A more aggressive inliner should generate larger programs but more optimized
     /// A less aggressive inliner should generate smaller programs
@@ -631,6 +637,7 @@ pub fn compile_no_check(
         },
         emit_ssa: if options.emit_ssa { Some(context.package_build_path.clone()) } else { None },
         skip_underconstrained_check: options.skip_underconstrained_check,
+        skip_brillig_constraints_check: options.skip_brillig_constraints_check,
         inliner_aggressiveness: options.inliner_aggressiveness,
         max_bytecode_increase_percent: options.max_bytecode_increase_percent,
     };

compiler/noirc_evaluator/Cargo.toml

@@ -32,6 +32,7 @@ cfg-if.workspace = true
 [dev-dependencies]
 proptest.workspace = true
 similar-asserts.workspace = true
+tracing-test = "0.2.5"
 num-traits.workspace = true
 test-case.workspace = true
 

compiler/noirc_evaluator/src/errors.rs

@@ -93,7 +93,10 @@ impl From<SsaReport> for FileDiagnostic {
                 let message = bug.to_string();
                 let (secondary_message, call_stack) = match bug {
                     InternalBug::IndependentSubgraph { call_stack } => {
-                        ("There is no path from the output of this brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability".to_string(),call_stack)
+                        ("There is no path from the output of this Brillig call to either return values or inputs of the circuit, which creates an independent subgraph. This is quite likely a soundness vulnerability".to_string(), call_stack)
+                    }
+                    InternalBug::UncheckedBrilligCall { call_stack } => {
+                        ("This Brillig call's inputs and its return values haven't been sufficiently constrained. This should be done to prevent potential soundness vulnerabilities".to_string(), call_stack)
                     }
                     InternalBug::AssertFailed { call_stack } => ("As a result, the compiled circuit is ensured to fail. Other assertions may also fail during execution".to_string(), call_stack)
                 };
@@ -117,8 +120,10 @@ pub enum InternalWarning {
 
 #[derive(Debug, PartialEq, Eq, Clone, Error, Serialize, Deserialize, Hash)]
 pub enum InternalBug {
-    #[error("Input to brillig function is in a separate subgraph to output")]
+    #[error("Input to Brillig function is in a separate subgraph to output")]
     IndependentSubgraph { call_stack: CallStack },
+    #[error("Brillig function call isn't properly covered by a manual constraint")]
+    UncheckedBrilligCall { call_stack: CallStack },
     #[error("Assertion is always false")]
     AssertFailed { call_stack: CallStack },
 }

compiler/noirc_evaluator/src/ssa.rs

@@ -72,7 +72,10 @@ pub struct SsaEvaluatorOptions {
     /// Skip the check for under constrained values
     pub skip_underconstrained_check: bool,
 
-    /// The higher the value, the more inlined brillig functions will be.
+    /// Skip the missing Brillig call constraints check
+    pub skip_brillig_constraints_check: bool,
+
+    /// The higher the value, the more inlined Brillig functions will be.
     pub inliner_aggressiveness: i64,
 
     /// Maximum accepted percentage increase in the Brillig bytecode size after unrolling loops.
@@ -104,12 +107,22 @@ pub(crate) fn optimize_into_acir(
 
     let mut ssa = optimize_all(builder, options)?;
 
-    let ssa_level_warnings = if options.skip_underconstrained_check {
-        vec![]
-    } else {
-        time("After Check for Underconstrained Values", options.print_codegen_timings, || {
-            ssa.check_for_underconstrained_values()
-        })
+    let mut ssa_level_warnings = vec![];
+
+    if !options.skip_underconstrained_check {
+        ssa_level_warnings.extend(time(
+            "After Check for Underconstrained Values",
+            options.print_codegen_timings,
+            || ssa.check_for_underconstrained_values(),
+        ));
+    }
+
+    if !options.skip_brillig_constraints_check {
+        ssa_level_warnings.extend(time(
+            "After Check for Missing Brillig Call Constraints",
+            options.print_codegen_timings,
+            || ssa.check_for_missing_brillig_constraints(),
+        ));
     };
 
     drop(ssa_gen_span_guard);