diff --git a/.vscode/launch.json b/.vscode/launch.json new file mode 100644 index 00000000000..5c7247b40ad --- /dev/null +++ b/.vscode/launch.json @@ -0,0 +1,7 @@ +{ + // Use IntelliSense to learn about possible attributes. + // Hover to view descriptions of existing attributes. + // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 + "version": "0.2.0", + "configurations": [] +} \ No newline at end of file diff --git a/acvm-repo/acvm/src/compiler/simulator.rs b/acvm-repo/acvm/src/compiler/simulator.rs index 96134926f5e..c5c76dd1193 100644 --- a/acvm-repo/acvm/src/compiler/simulator.rs +++ b/acvm-repo/acvm/src/compiler/simulator.rs @@ -8,6 +8,7 @@ use acir::{ native_types::{Expression, Witness}, }; use std::collections::{BTreeSet, HashMap, HashSet}; +use tracing::field::Field; #[derive(PartialEq)] enum BlockStatus { @@ -20,7 +21,10 @@ enum BlockStatus { pub struct CircuitSimulator { /// Track the witnesses that can be solved solvable_witness: HashSet, - + /// Track the witnesses that require a hard inversion + hard_to_invert: HashSet, + /// Track the witnesses that are only require inverting a 1 or -1 + easy_to_invert: HashSet, /// Tells whether a Memory Block is: /// - Not initialized if not in the map /// - Initialized if its status is Initialized in the Map @@ -48,24 +52,37 @@ impl CircuitSimulator { let mut unresolved = HashSet::new(); match opcode { Opcode::AssertZero(expr) => { - for (_, w1, w2) in &expr.mul_terms { + for (c, w1, w2) in &expr.mul_terms { if !self.solvable_witness.contains(w1) { + // this means that w1 is not known at the time if !self.solvable_witness.contains(w2) { return false; + } else { + // now we can compute the term that's getting multiplied by w1 + if *c == F::one() || *c == -F::one() { + self.easy_to_invert.insert(*w1); + } else { + self.hard_to_invert.insert(*w1); + } } - unresolved.insert(*w1); } if !self.solvable_witness.contains(w2) && w1 != w2 { unresolved.insert(*w2); } } - for (_, w) in &expr.linear_combinations { + for (c, w) in &expr.linear_combinations { if !self.solvable_witness.contains(w) { unresolved.insert(*w); } } if unresolved.len() == 1 { self.mark_solvable(*unresolved.iter().next().unwrap()); + // we should be assigning the witness in this opcode now + if *c == F::one() || *c == -F::one() { + self.easy_to_invert.insert(*w); + } else { + self.hard_to_invert.insert(*w); + } return true; } unresolved.is_empty() diff --git a/acvm-repo/acvm/src/pwg/arithmetic.rs b/acvm-repo/acvm/src/pwg/arithmetic.rs index 0708dfb2dc5..995738bd06c 100644 --- a/acvm-repo/acvm/src/pwg/arithmetic.rs +++ b/acvm-repo/acvm/src/pwg/arithmetic.rs @@ -1,14 +1,101 @@ +use super::{ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, insert_value}; use acir::{ AcirField, native_types::{Expression, Witness, WitnessMap}, }; - -use super::{ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, insert_value}; - /// An Expression solver will take a Circuit's assert-zero opcodes with witness assignments /// and create the other witness variables pub(crate) struct ExpressionSolver; +#[derive(Clone, Debug)] +pub(crate) struct PendingArithmeticOpcodes { + pending_witness_write: Vec>, + failures: u32, +} + +impl PendingArithmeticOpcodes { + pub(crate) fn new() -> Self { + Self { pending_witness_write: vec![], failures: 0 } + } + + pub(crate) fn add_pending_op( + &mut self, + neumerator: F, + denominator: F, + witness: Witness, + ) -> Result<(), OpcodeResolutionError> { + // note that there might be multiple witness assignments in this list + // however when pending_ops is called, this would cause an error + self.pending_witness_write.push(PendingOp { neumerator, denominator, witness }); + Ok(()) + } + + pub(crate) fn write_pending_ops( + &mut self, + initial_witness: &mut WitnessMap, + ) -> Result<(), OpcodeResolutionError> { + // get the list of denominator + let mut denominator_list: Vec = self + .pending_witness_write + .clone() + .into_iter() + .map(|pending_op| pending_op.denominator) + .collect(); + batch_invert::(&mut denominator_list); + for (idx, pending_op) in self.pending_witness_write.iter().enumerate() { + let assignment = pending_op.neumerator * denominator_list[idx]; + let res = insert_value(&pending_op.witness, assignment, initial_witness); + if res.is_err() { + return Err(OpcodeResolutionError::UnsatisfiedConstrain { + opcode_location: ErrorLocation::Unresolved, + payload: None, + }); + } + } + self.pending_witness_write.clear(); + self.failures = 0; + Ok(()) + } +} + +// this is the same function as in arkworks +pub(crate) fn batch_invert(v: &mut [F]) { + // First pass: compute [a, ab, abc, ...] + // we're never adding elements that are zero to this list + let mut prod = Vec::with_capacity(v.len()); + let mut tmp = F::one(); + for f in v.iter() { + tmp = tmp * *f; + prod.push(tmp); + } + + // Invert `tmp`. + tmp = tmp.inverse(); // Guaranteed to be nonzero. + + // Second pass: iterate backwards to compute inverses + for (f, s) in v + .iter_mut() + // Backwards + .rev() + // Ignore normalized elements + .filter(|f| !f.is_zero()) + // Backwards, skip last element, fill in one for last term. + .zip(prod.into_iter().rev().skip(1).chain(Some(F::one()))) + { + // tmp := tmp * f; f := tmp * s = 1/f + let new_tmp = tmp * *f; + *f = tmp * s; + tmp = new_tmp; + } +} + +#[derive(Clone, Debug)] +pub(crate) struct PendingOp { + neumerator: F, + denominator: F, + witness: Witness, +} + #[allow(clippy::enum_variant_names)] pub(super) enum OpcodeStatus { OpcodeSatisfied(F), @@ -23,6 +110,162 @@ pub(crate) enum MulTerm { } impl ExpressionSolver { + /// the solver method along side the the optimization with the pending arithmetic opcodes + /// Derives the rest of the witness based on the initial low level variables + pub(crate) fn solve_optimized( + initial_witness: &mut WitnessMap, + opcode: &Expression, + pending_arithmetic_opcodes: &mut PendingArithmeticOpcodes, + ) -> Result<(), OpcodeResolutionError> { + let opcode = &ExpressionSolver::evaluate(opcode, initial_witness); + // Evaluate multiplication term + let mul_result = + ExpressionSolver::solve_mul_term(opcode, initial_witness).map_err(|_| { + OpcodeResolutionError::OpcodeNotSolvable( + OpcodeNotSolvable::ExpressionHasTooManyUnknowns(opcode.clone()), + ) + })?; + // Evaluate the fan-in terms + let opcode_status = ExpressionSolver::solve_fan_in_term(opcode, initial_witness); + + match (mul_result, opcode_status) { + (MulTerm::TooManyUnknowns, _) | (_, OpcodeStatus::OpcodeUnsolvable) => { + // if we have too many unknowns, and there are no pending ops, then we can return an error + if pending_arithmetic_opcodes.pending_witness_write.is_empty() { + return Err(OpcodeResolutionError::OpcodeNotSolvable( + OpcodeNotSolvable::ExpressionHasTooManyUnknowns(opcode.clone()), + )); + } + // there might be too many unknowns that are in the pending witness list that is not written down yet. + // so we write down the pending witness lists and solve again + // pending_arithmetic_opcodes.failures += 1; + let write_output = pending_arithmetic_opcodes.write_pending_ops(initial_witness); + write_output.map_err(|_| { + OpcodeResolutionError::OpcodeNotSolvable( + OpcodeNotSolvable::ExpressionHasTooManyUnknowns(opcode.clone()), + ) + })?; + // no we have to solve again to see if the opcode is solvable + ExpressionSolver::solve_optimized( + initial_witness, + opcode, + pending_arithmetic_opcodes, + ) + } + + (MulTerm::OneUnknown(q, w1), OpcodeStatus::OpcodeSolvable(a, (b, w2))) => { + if w1 == w2 { + // We have one unknown so we can solve the equation + let total_sum = a + opcode.q_c; + match q + b { + x if x.is_zero() => { + if !total_sum.is_zero() { + Err(OpcodeResolutionError::UnsatisfiedConstrain { + opcode_location: ErrorLocation::Unresolved, + payload: None, + }) + } else { + Ok(()) + } + } + x if x == F::one() => insert_value(&w1, total_sum, initial_witness), + x if x == -F::one() => insert_value(&w1, -total_sum, initial_witness), + x => { + // normally we would do + // let assignment = -total_sum / (q + b); + // insert_value(&w1, assignment, initial_witness) + // but we want to add this to pending_arithmetic_opcodes + pending_arithmetic_opcodes.add_pending_op(-total_sum, x, w1) + } + } + } else { + // TODO: can we be more specific with this error? + Err(OpcodeResolutionError::OpcodeNotSolvable( + OpcodeNotSolvable::ExpressionHasTooManyUnknowns(opcode.clone()), + )) + } + } + ( + MulTerm::OneUnknown(partial_prod, unknown_var), + OpcodeStatus::OpcodeSatisfied(sum), + ) => { + // We have one unknown in the mul term and the fan-in terms are solved. + // Hence the equation is solvable, since there is a single unknown + // The equation is: partial_prod * unknown_var + sum + qC = 0 + + let total_sum = sum + opcode.q_c; + + match partial_prod { + x if x.is_zero() => { + if !total_sum.is_zero() { + Err(OpcodeResolutionError::UnsatisfiedConstrain { + opcode_location: ErrorLocation::Unresolved, + payload: None, + }) + } else { + Ok(()) + } + } + x if x == F::one() => insert_value(&unknown_var, -total_sum, initial_witness), + x if x == -F::one() => insert_value(&unknown_var, total_sum, initial_witness), + _ => { + // normally we would do + // let assignment = -(total_sum / partial_prod); + // insert_value(&unknown_var, assignment, initial_witness) + // but we want to add this to pending_arithmetic_opcodes + pending_arithmetic_opcodes.add_pending_op( + -total_sum, + partial_prod, + unknown_var, + ) + } + } + } + (MulTerm::Solved(a), OpcodeStatus::OpcodeSatisfied(b)) => { + // All the variables in the MulTerm are solved and the Fan-in is also solved + // There is nothing to solve + if !(a + b + opcode.q_c).is_zero() { + Err(OpcodeResolutionError::UnsatisfiedConstrain { + opcode_location: ErrorLocation::Unresolved, + payload: None, + }) + } else { + Ok(()) + } + } + ( + MulTerm::Solved(total_prod), + OpcodeStatus::OpcodeSolvable(partial_sum, (coeff, unknown_var)), + ) => { + // The variables in the MulTerm are solved and there is one unknown in the Fan-in + // Hence the equation is solvable, since we have one unknown + // The equation is total_prod + partial_sum + coeff * unknown_var + q_C = 0 + let total_sum = total_prod + partial_sum + opcode.q_c; + match coeff { + x if x.is_zero() => { + if !total_sum.is_zero() { + Err(OpcodeResolutionError::UnsatisfiedConstrain { + opcode_location: ErrorLocation::Unresolved, + payload: None, + }) + } else { + Ok(()) + } + } + x if x == F::one() => insert_value(&unknown_var, -total_sum, initial_witness), + x if x == -F::one() => insert_value(&unknown_var, total_sum, initial_witness), + _ => { + // normally we would do + // let assignment = -(total_sum / coeff); + // insert_value(&unknown_var, assignment, initial_witness) + // but we want to add this to pending_arithmetic_opcodes + pending_arithmetic_opcodes.add_pending_op(-total_sum, coeff, unknown_var) + } + } + } + } + } + /// Derives the rest of the witness based on the initial low level variables pub(crate) fn solve( initial_witness: &mut WitnessMap, @@ -321,6 +564,25 @@ mod tests { assert_eq!(values.get(&a).unwrap(), &FieldElement::from(2_i128)); } + #[test] + fn test_batch_invert() { + let mut v = vec![ + FieldElement::from(1_i128), + FieldElement::from(2_i128), + FieldElement::from(3_i128), + ]; + batch_invert::(&mut v); + // assert_eq!(v, vec![FieldElement::from(1_i128), FieldElement::from(2_i128), FieldElement::from(3_i128)]); + assert_eq!( + [ + v[0] * FieldElement::from(1_i128), + v[1] * FieldElement::from(2_i128), + v[2] * FieldElement::from(3_i128) + ], + [FieldElement::from(1_i128), FieldElement::from(1_i128), FieldElement::from(1_i128)] + ); + } + #[test] fn solves_unknown_in_linear_term() { let a = Witness(0); @@ -361,4 +623,171 @@ mod tests { assert_eq!(values.get(&a).unwrap(), &FieldElement::from(4_i128)); } + + #[test] + fn test_pending_ops() { + let mut pending_ops: PendingArithmeticOpcodes = + PendingArithmeticOpcodes::new(); + let a = Witness(0); + let opcode_a = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one() + FieldElement::one(), a)], + q_c: -FieldElement::one(), + }; + let mut initial_witness: WitnessMap = WitnessMap::new(); + let _ = + ExpressionSolver::solve_optimized(&mut initial_witness, &opcode_a, &mut pending_ops); + println!("pending_ops: {:?}", pending_ops); + } + #[test] + fn test_pending_ops_2() { + let mut pending_ops: PendingArithmeticOpcodes = + PendingArithmeticOpcodes::new(); + let a = Witness(0); + let opcode_a = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one() + FieldElement::one(), a)], + q_c: -FieldElement::one(), + }; + let b: Witness = Witness(1); + let opcode_b = Expression { + mul_terms: vec![], + linear_combinations: vec![ + (FieldElement::one() + FieldElement::one(), a), + (FieldElement::one(), b), + ], + q_c: -FieldElement::one(), + }; + let mut initial_witness: WitnessMap = WitnessMap::new(); + let _ = + ExpressionSolver::solve_optimized(&mut initial_witness, &opcode_a, &mut pending_ops); + println!("pending_ops: {:?}", pending_ops); + println!("initial_witness: {:?}", initial_witness); + let _ = + ExpressionSolver::solve_optimized(&mut initial_witness, &opcode_b, &mut pending_ops); + println!("pending_ops: {:?}", pending_ops); + println!("initial_witness: {:?}", initial_witness); + } + + #[test] + fn test_pending_ops_batching_linear_combinations() { + // we want the following scenario + // w0 = 2 + // 9w1 = 3 + w0 + // w1 1/9 should be added to pending_ops, + // 5w2 = 3 * w0 + // w2 1/5 should be added to the pending ops + // w3 = 4 + w1 + // a failure should happen so w1 and w2 should be written + // w4 = 5 * w2 + // there's no unknowns here so the pending ops should be empty + let mut pending_ops: PendingArithmeticOpcodes = + PendingArithmeticOpcodes::new(); + let w0 = Witness(0); + let w1 = Witness(1); + let w2 = Witness(2); + let w3 = Witness(3); + let w4 = Witness(4); + // opcode0 : w0 - 15 = 0 + // w0 = 15 + let opcode0 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one(), w0)], + q_c: -FieldElement::from(15_i128), + }; + // opcode1 : 9w1 - 3 - w0 = 0 + // w1 = 2 + let opcode1 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::from(9_i128), w1), (-FieldElement::one(), w0)], + q_c: -FieldElement::from(3_i128), + }; + // opcode2 : 5w2 - 3 * w0 = 0 + // w2 = 9 + let opcode2 = Expression { + mul_terms: vec![], + linear_combinations: vec![ + (FieldElement::from(5_i128), w2), + (-FieldElement::from(3_i128), w0), + ], + q_c: FieldElement::zero(), + }; + // opcode3 : w3 - 4 - w1 = 0 + // w3 = 6 + let opcode3 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one(), w3), (-FieldElement::one(), w1)], + q_c: -FieldElement::from(4_i128), + }; + // opcode4: w4 - 5 * w2 = 0 + // w4 = 45 + let opcode4 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one(), w4), (-FieldElement::from(5_i128), w2)], + q_c: FieldElement::zero(), + }; + let mut initial_witness: WitnessMap = WitnessMap::new(); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode0, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode1, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode2, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode3, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode4, &mut pending_ops); + + assert_eq!(initial_witness.get(&w0).unwrap(), &FieldElement::from(15_i128)); + assert_eq!(initial_witness.get(&w1).unwrap(), &FieldElement::from(2_i128)); + assert_eq!(initial_witness.get(&w2).unwrap(), &FieldElement::from(9_i128)); + assert_eq!(initial_witness.get(&w3).unwrap(), &FieldElement::from(6_i128)); + assert_eq!(initial_witness.get(&w4).unwrap(), &FieldElement::from(45_i128)); + } + #[test] + fn test_pending_ops_batching_multiplication_terms() { + // 5 * w0 = 15 => w0 = 3 // opcode0 = 5 * w0 - 15 = 0 + // 3 * w1 = 12 => w1 = 4 // opcode1 = 3 * w1 - 12 = 0 + // w2 * w0 = 15 => w2 = 5 // opcode2 = w2 * w0 - 15 = 0 + // w3 + 2 = w2 => true // opcode3 = w3 + 2 - w2 = 0 + // + let mut pending_ops: PendingArithmeticOpcodes = + PendingArithmeticOpcodes::new(); + let w0 = Witness(0); + let w1 = Witness(1); + let w2 = Witness(2); + + // opcode0 : 5 * w0 - 15 = 0 + let opcode0 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::from(5_i128), w0)], + q_c: -FieldElement::from(15_i128), + }; + // opcode1 = 3 * w1 - 12 = 0 + let opcode1 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::from(3_i128), w1)], + q_c: -FieldElement::from(12_i128), + }; + // opcode2 = w2 * w0 - 15 = 0 + let opcode2 = Expression { + mul_terms: vec![(FieldElement::one(), w0, w2)], + linear_combinations: vec![], + q_c: -FieldElement::from(15_i128), + }; + // opcode3 = w0 + 2 - w2 = 0 + let opcode3 = Expression { + mul_terms: vec![], + linear_combinations: vec![(FieldElement::one(), w0), (-FieldElement::one(), w2)], + q_c: FieldElement::from(2_i128), + }; + // set up an empty witness map + let mut initial_witness: WitnessMap = WitnessMap::new(); + // now we run the opcodes + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode0, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode1, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode2, &mut pending_ops); + let _ = ExpressionSolver::solve_optimized(&mut initial_witness, &opcode3, &mut pending_ops); + + // empty the pending writes + let _ = pending_ops.write_pending_ops(&mut initial_witness); + assert_eq!(initial_witness.get(&w0).unwrap(), &FieldElement::from(3_i128)); + assert_eq!(initial_witness.get(&w1).unwrap(), &FieldElement::from(4_i128)); + assert_eq!(initial_witness.get(&w2).unwrap(), &FieldElement::from(5_i128)); + } } diff --git a/acvm-repo/acvm/src/pwg/mod.rs b/acvm-repo/acvm/src/pwg/mod.rs index 7d462ad6244..673e448e112 100644 --- a/acvm-repo/acvm/src/pwg/mod.rs +++ b/acvm-repo/acvm/src/pwg/mod.rs @@ -18,10 +18,11 @@ use acvm_blackbox_solver::BlackBoxResolutionError; use brillig_vm::BranchToFeatureMap; use self::{ - arithmetic::ExpressionSolver, blackbox::bigint::AcvmBigIntSolver, memory_op::MemoryOpSolver, + arithmetic::{ExpressionSolver, PendingArithmeticOpcodes}, + blackbox::bigint::AcvmBigIntSolver, + memory_op::MemoryOpSolver, }; use crate::BlackBoxFunctionSolver; - use thiserror::Error; // arithmetic @@ -402,12 +403,63 @@ impl<'a, F: AcirField, B: BlackBoxFunctionSolver> ACVM<'a, F, B> { /// 2. The circuit has been found to be unsatisfiable. /// 2. A Brillig [foreign call][`ForeignCallWaitInfo`] has been encountered and must be resolved. pub fn solve(&mut self) -> ACVMStatus { + let mut pending_arithmetic_opcodes: PendingArithmeticOpcodes = + PendingArithmeticOpcodes::new(); + while self.status == ACVMStatus::InProgress { - self.solve_opcode(); + self.solve_opcode_optimized(&mut pending_arithmetic_opcodes); + } + // write the pending opcodes that are not written down yet + let final_write_result = + pending_arithmetic_opcodes.write_pending_ops(&mut self.witness_map); + if self.status == ACVMStatus::Solved && final_write_result.is_err() { + self.status(ACVMStatus::Failure(final_write_result.err().unwrap())); } self.status.clone() } + pub(crate) fn solve_opcode_optimized( + &mut self, + pending_arithmetic_opcodes: &mut PendingArithmeticOpcodes, + ) -> ACVMStatus { + let opcode = &self.opcodes[self.instruction_pointer]; + let resolution = match opcode { + Opcode::AssertZero(expr) => ExpressionSolver::solve_optimized( + &mut self.witness_map, + expr, + pending_arithmetic_opcodes, + ), + Opcode::BlackBoxFuncCall(bb_func) => blackbox::solve( + self.backend, + &mut self.witness_map, + bb_func, + &mut self.bigint_solver, + ), + Opcode::MemoryInit { block_id, init, .. } => { + let solver = self.block_solvers.entry(*block_id).or_default(); + solver.init(init, &self.witness_map) + } + Opcode::MemoryOp { block_id, op, predicate } => { + let solver = self.block_solvers.entry(*block_id).or_default(); + solver.solve_memory_op( + op, + &mut self.witness_map, + predicate, + self.backend.pedantic_solving(), + ) + } + Opcode::BrilligCall { .. } => match self.solve_brillig_call_opcode() { + Ok(Some(foreign_call)) => return self.wait_for_foreign_call(foreign_call), + res => res.map(|_| ()), + }, + Opcode::Call { .. } => match self.solve_call_opcode() { + Ok(Some(input_values)) => return self.wait_for_acir_call(input_values), + res => res.map(|_| ()), + }, + }; + self.handle_opcode_resolution(resolution) + } + pub fn solve_opcode(&mut self) -> ACVMStatus { let opcode = &self.opcodes[self.instruction_pointer]; let resolution = match opcode { @@ -618,7 +670,7 @@ impl<'a, F: AcirField, B: BlackBoxFunctionSolver> ACVM<'a, F, B> { }; let opcode_location = - ErrorLocation::Resolved(OpcodeLocation::Acir(self.instruction_pointer())); + ErrorLocation::Resolved(OpcodeLocation::Acir(self.instruction_pointer)); let witness = &mut self.witness_map; let should_skip = match is_predicate_false( witness, diff --git a/acvm-repo/acvm/tests/solver.rs b/acvm-repo/acvm/tests/solver.rs index ce75a7d2001..dcda9601e59 100644 --- a/acvm-repo/acvm/tests/solver.rs +++ b/acvm-repo/acvm/tests/solver.rs @@ -50,11 +50,12 @@ fn bls12_381_circuit() { let mut acvm = ACVM::new(&solver, &opcodes, witness_assignments, &[], &[]); // use the partial witness generation solver with our acir program let solver_status = acvm.solve(); + println!("solver_status: {:?}", solver_status); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); // ACVM should be able to be finalized in `Solved` state. let witness_stack = acvm.finalize(); - + println!("witness_stack: {:?}", witness_stack); assert_eq!(witness_stack.get(&Witness(3)).unwrap(), &Bls12FieldElement::from(5u128)); } diff --git a/tooling/nargo_cli/tests/comptime_correctness.proptest-regressions b/tooling/nargo_cli/tests/comptime_correctness.proptest-regressions new file mode 100644 index 00000000000..7f85b7029e5 --- /dev/null +++ b/tooling/nargo_cli/tests/comptime_correctness.proptest-regressions @@ -0,0 +1,10 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 6a5cd355acc9373871792fc3df09bae47993ca04f5f454984e367f815876eec6 # shrinks to (comptime_expr, runtime_expr, a, b) = ("135498780 - 3261502582", "a - b", 135498780, 3261502582) +cc a08277a802c111eae18b6dd790863276ef5beee388af841c77b82d8983a93ca5 # shrinks to (comptime_expr, runtime_expr, a, b) = ("219873777 * 3665822852", "a * b", 219873777, 3665822852) +cc 3a95092b2ef83275163af01b6d7872871b9c3509ab36c84b4f15a6c4f8deeaa5 # shrinks to (comptime_expr, runtime_expr, a, b) = ("168250881 / 1518081420", "a / b", 168250881, 1518081420) +cc 2255f39f8b52de7d71b7f0c64868e2bb295295c3fc16c4e73adec37f4cf6d09e # shrinks to (comptime_expr, runtime_expr, a, b) = ("9338499 + 814394354", "a + b", 9338499, 814394354)