feat: --pedantic-solving flag (#6716)

Co-authored-by: Akosh Farkash <aakoshh@gmail.com> Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
noir-lang · Jan 7, 2025 · 5b9a113 · 5b9a113
1 parent dcdccfc
commit 5b9a113
Show file tree

Hide file tree

Showing 47 changed files with 879 additions and 300 deletions.
diff --git a/.github/workflows/test-js-packages.yml b/.github/workflows/test-js-packages.yml
@@ -597,7 +597,7 @@ jobs:
       - name: Run nargo test
         working-directory: ./test-repo/${{ matrix.project.path }}
         run: |
-          nargo test --silence-warnings --skip-brillig-constraints-check --format json ${{ matrix.project.nargo_args }} | tee ${{ github.workspace }}/noir-repo/.github/critical_libraries_status/${{ matrix.project.repo }}/${{ matrix.project.path }}.actual.jsonl
+          nargo test --silence-warnings --pedantic-solving --skip-brillig-constraints-check --format json ${{ matrix.project.nargo_args }} | tee ${{ github.workspace }}/noir-repo/.github/critical_libraries_status/${{ matrix.project.repo }}/${{ matrix.project.path }}.actual.jsonl
         env:
           NARGO_IGNORE_TEST_FAILURES_FROM_FOREIGN_CALLS: true
 

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/acvm-repo/acvm/src/pwg/blackbox/bigint.rs b/acvm-repo/acvm/src/pwg/blackbox/bigint.rs
@@ -12,12 +12,16 @@ use crate::pwg::OpcodeResolutionError;
 /// - When it encounters a bigint operation opcode, it performs the operation on the stored values
 ///   and store the result using the provided ID.
 /// - When it gets a to_bytes opcode, it simply looks up the value and resolves the output witness accordingly.
-#[derive(Default)]
 pub(crate) struct AcvmBigIntSolver {
     bigint_solver: BigIntSolver,
 }
 
 impl AcvmBigIntSolver {
+    pub(crate) fn with_pedantic_solving(pedantic_solving: bool) -> AcvmBigIntSolver {
+        let bigint_solver = BigIntSolver::with_pedantic_solving(pedantic_solving);
+        AcvmBigIntSolver { bigint_solver }
+    }
+
     pub(crate) fn bigint_from_bytes<F: AcirField>(
         &mut self,
         inputs: &[FunctionInput<F>],
@@ -39,6 +43,9 @@ impl AcvmBigIntSolver {
         outputs: &[Witness],
         initial_witness: &mut WitnessMap<F>,
     ) -> Result<(), OpcodeResolutionError<F>> {
+        if self.bigint_solver.pedantic_solving() && outputs.len() != 32 {
+            panic!("--pedantic-solving: bigint_to_bytes: outputs.len() != 32: {}", outputs.len());
+        }
         let mut bytes = self.bigint_solver.bigint_to_bytes(input)?;
         while bytes.len() < outputs.len() {
             bytes.push(0);

diff --git a/acvm-repo/acvm/src/pwg/blackbox/logic.rs b/acvm-repo/acvm/src/pwg/blackbox/logic.rs
@@ -14,13 +14,14 @@ pub(super) fn and<F: AcirField>(
     lhs: &FunctionInput<F>,
     rhs: &FunctionInput<F>,
     output: &Witness,
+    pedantic_solving: bool,
 ) -> Result<(), OpcodeResolutionError<F>> {
     assert_eq!(
         lhs.num_bits(),
         rhs.num_bits(),
         "number of bits specified for each input must be the same"
     );
-    solve_logic_opcode(initial_witness, lhs, rhs, *output, |left, right| {
+    solve_logic_opcode(initial_witness, lhs, rhs, *output, pedantic_solving, |left, right| {
         bit_and(left, right, lhs.num_bits())
     })
 }
@@ -32,13 +33,14 @@ pub(super) fn xor<F: AcirField>(
     lhs: &FunctionInput<F>,
     rhs: &FunctionInput<F>,
     output: &Witness,
+    pedantic_solving: bool,
 ) -> Result<(), OpcodeResolutionError<F>> {
     assert_eq!(
         lhs.num_bits(),
         rhs.num_bits(),
         "number of bits specified for each input must be the same"
     );
-    solve_logic_opcode(initial_witness, lhs, rhs, *output, |left, right| {
+    solve_logic_opcode(initial_witness, lhs, rhs, *output, pedantic_solving, |left, right| {
         bit_xor(left, right, lhs.num_bits())
     })
 }
@@ -49,11 +51,13 @@ fn solve_logic_opcode<F: AcirField>(
     a: &FunctionInput<F>,
     b: &FunctionInput<F>,
     result: Witness,
+    pedantic_solving: bool,
     logic_op: impl Fn(F, F) -> F,
 ) -> Result<(), OpcodeResolutionError<F>> {
-    // TODO(https://github.com/noir-lang/noir/issues/5985): re-enable these once we figure out how to combine these with existing
+    // TODO(https://github.com/noir-lang/noir/issues/5985): re-enable these by
+    // default once we figure out how to combine these with existing
     // noirc_frontend/noirc_evaluator overflow error messages
-    let skip_bitsize_checks = true;
+    let skip_bitsize_checks = !pedantic_solving;
     let w_l_value = input_to_value(initial_witness, *a, skip_bitsize_checks)?;
     let w_r_value = input_to_value(initial_witness, *b, skip_bitsize_checks)?;
     let assignment = logic_op(w_l_value, w_r_value);

diff --git a/acvm-repo/acvm/src/pwg/blackbox/mod.rs b/acvm-repo/acvm/src/pwg/blackbox/mod.rs
@@ -76,9 +76,15 @@ pub(crate) fn solve<F: AcirField>(
         BlackBoxFuncCall::AES128Encrypt { inputs, iv, key, outputs } => {
             solve_aes128_encryption_opcode(initial_witness, inputs, iv, key, outputs)
         }
-        BlackBoxFuncCall::AND { lhs, rhs, output } => and(initial_witness, lhs, rhs, output),
-        BlackBoxFuncCall::XOR { lhs, rhs, output } => xor(initial_witness, lhs, rhs, output),
-        BlackBoxFuncCall::RANGE { input } => solve_range_opcode(initial_witness, input),
+        BlackBoxFuncCall::AND { lhs, rhs, output } => {
+            and(initial_witness, lhs, rhs, output, backend.pedantic_solving())
+        }
+        BlackBoxFuncCall::XOR { lhs, rhs, output } => {
+            xor(initial_witness, lhs, rhs, output, backend.pedantic_solving())
+        }
+        BlackBoxFuncCall::RANGE { input } => {
+            solve_range_opcode(initial_witness, input, backend.pedantic_solving())
+        }
         BlackBoxFuncCall::Blake2s { inputs, outputs } => {
             solve_generic_256_hash_opcode(initial_witness, inputs, None, outputs, blake2s)
         }

diff --git a/acvm-repo/acvm/src/pwg/blackbox/range.rs b/acvm-repo/acvm/src/pwg/blackbox/range.rs
@@ -7,10 +7,11 @@ use acir::{circuit::opcodes::FunctionInput, native_types::WitnessMap, AcirField}
 pub(crate) fn solve_range_opcode<F: AcirField>(
     initial_witness: &WitnessMap<F>,
     input: &FunctionInput<F>,
+    pedantic_solving: bool,
 ) -> Result<(), OpcodeResolutionError<F>> {
     // TODO(https://github.com/noir-lang/noir/issues/5985):
-    // re-enable bitsize checks
-    let skip_bitsize_checks = true;
+    // re-enable bitsize checks by default
+    let skip_bitsize_checks = !pedantic_solving;
     let w_value = input_to_value(initial_witness, *input, skip_bitsize_checks)?;
     if w_value.num_bits() > input.num_bits() {
         return Err(OpcodeResolutionError::UnsatisfiedConstrain {

diff --git a/acvm-repo/acvm/src/pwg/memory_op.rs b/acvm-repo/acvm/src/pwg/memory_op.rs
@@ -66,6 +66,7 @@ impl<F: AcirField> MemoryOpSolver<F> {
         op: &MemOp<F>,
         initial_witness: &mut WitnessMap<F>,
         predicate: &Option<Expression<F>>,
+        pedantic_solving: bool,
     ) -> Result<(), OpcodeResolutionError<F>> {
         let operation = get_value(&op.operation, initial_witness)?;
 
@@ -83,7 +84,9 @@ impl<F: AcirField> MemoryOpSolver<F> {
         let is_read_operation = operation.is_zero();
 
         // Fetch whether or not the predicate is false (e.g. equal to zero)
-        let skip_operation = is_predicate_false(initial_witness, predicate)?;
+        let opcode_location = ErrorLocation::Unresolved;
+        let skip_operation =
+            is_predicate_false(initial_witness, predicate, pedantic_solving, &opcode_location)?;
 
         if is_read_operation {
             // `value_read = arr[memory_index]`
@@ -131,6 +134,9 @@ mod tests {
 
     use super::MemoryOpSolver;
 
+    // use pedantic_solving for tests
+    const PEDANTIC_SOLVING: bool = true;
+
     #[test]
     fn test_solver() {
         let mut initial_witness = WitnessMap::from(BTreeMap::from_iter([
@@ -150,7 +156,9 @@ mod tests {
         block_solver.init(&init, &initial_witness).unwrap();
 
         for op in trace {
-            block_solver.solve_memory_op(&op, &mut initial_witness, &None).unwrap();
+            block_solver
+                .solve_memory_op(&op, &mut initial_witness, &None, PEDANTIC_SOLVING)
+                .unwrap();
         }
 
         assert_eq!(initial_witness[&Witness(4)], FieldElement::from(2u128));
@@ -175,7 +183,9 @@ mod tests {
         let mut err = None;
         for op in invalid_trace {
             if err.is_none() {
-                err = block_solver.solve_memory_op(&op, &mut initial_witness, &None).err();
+                err = block_solver
+                    .solve_memory_op(&op, &mut initial_witness, &None, PEDANTIC_SOLVING)
+                    .err();
             }
         }
 
@@ -209,7 +219,12 @@ mod tests {
         for op in invalid_trace {
             if err.is_none() {
                 err = block_solver
-                    .solve_memory_op(&op, &mut initial_witness, &Some(Expression::zero()))
+                    .solve_memory_op(
+                        &op,
+                        &mut initial_witness,
+                        &Some(Expression::zero()),
+                        PEDANTIC_SOLVING,
+                    )
                     .err();
             }
         }
@@ -241,7 +256,12 @@ mod tests {
         for op in invalid_trace {
             if err.is_none() {
                 err = block_solver
-                    .solve_memory_op(&op, &mut initial_witness, &Some(Expression::zero()))
+                    .solve_memory_op(
+                        &op,
+                        &mut initial_witness,
+                        &Some(Expression::zero()),
+                        PEDANTIC_SOLVING,
+                    )
                     .err();
             }
         }