From d2e9c1075691a3140a6a6622f219ace3b98ac45a Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 5 Jul 2023 09:03:38 +0000 Subject: [PATCH 01/28] feat(acvm)!: replace `PartialWitnessGeneratorStatus` with `ACVMStatus` --- acvm/src/pwg/mod.rs | 46 ++++++++++++++++++++++++++++++++---------- acvm/tests/solver.rs | 48 ++++++++++++++++++++++---------------------- 2 files changed, 59 insertions(+), 35 deletions(-) diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 33a05f761..f07f9846a 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -29,11 +29,18 @@ mod block; pub use brillig::ForeignCallWaitInfo; -#[derive(Debug, PartialEq)] -pub enum PartialWitnessGeneratorStatus { +#[derive(Debug, Clone, PartialEq)] +pub enum ACVMStatus { /// All opcodes have been solved. Solved, + /// The ACVM is in the process of executing the circuit. + InProgress, + + /// The ACVM has encountered an irrecoverable error while executing the circuit and can not progress. + /// Most commonly this will be due to an unsatisfied constraint due to invalid inputs to the circuit. + Failure(OpcodeResolutionError), + /// The ACVM has encountered a request for a Brillig [foreign call][acir::brillig_vm::Opcode::ForeignCall] /// to retrieve information from outside of the ACVM. The result of the foreign call must be passed back /// to the ACVM using [`ACVM::resolve_pending_foreign_call`]. @@ -62,7 +69,7 @@ pub enum OpcodeResolution { // TODO: ExpressionHasTooManyUnknowns is specific for arithmetic expressions // TODO: we could have a error enum for arithmetic failure cases in that module // TODO that can be converted into an OpcodeNotSolvable or OpcodeResolutionError enum -#[derive(PartialEq, Eq, Debug, Error)] +#[derive(Clone, PartialEq, Eq, Debug, Error)] pub enum OpcodeNotSolvable { #[error("missing assignment for witness index {0}")] MissingAssignment(u32), @@ -70,7 +77,7 @@ pub enum OpcodeNotSolvable { ExpressionHasTooManyUnknowns(Expression), } -#[derive(PartialEq, Eq, Debug, Error)] +#[derive(Clone, PartialEq, Eq, Debug, Error)] pub enum OpcodeResolutionError { #[error("cannot solve opcode: {0}")] OpcodeNotSolvable(#[from] OpcodeNotSolvable), @@ -85,6 +92,8 @@ pub enum OpcodeResolutionError { } pub struct ACVM { + status: ACVMStatus, + backend: B, /// Stores the solver for each [block][`Opcode::Block`] opcode. This persists their internal state to prevent recomputation. block_solvers: HashMap, @@ -102,6 +111,7 @@ pub struct ACVM { impl ACVM { pub fn new(backend: B, opcodes: Vec, initial_witness: WitnessMap) -> Self { ACVM { + status: ACVMStatus::InProgress, backend, block_solvers: HashMap::default(), opcodes, @@ -124,9 +134,22 @@ impl ACVM { &self.opcodes } + /// Updates the current status of the VM. + /// Returns the given status. + fn status(&mut self, status: ACVMStatus) -> ACVMStatus { + self.status = status.clone(); + status + } + + /// Sets the VM status to [ACVMStatus::Failure] using the provided error`. + /// Returns the new status. + fn fail(&mut self, error: OpcodeResolutionError) -> ACVMStatus { + self.status(ACVMStatus::Failure(error)) + } + /// Finalize the ACVM execution, returning the resulting [`WitnessMap`]. pub fn finalize(self) -> WitnessMap { - if self.opcodes.is_empty() || self.get_pending_foreign_call().is_some() { + if !matches!(self.status, ACVMStatus::Solved) { panic!("ACVM is not ready to be finalized"); } self.witness_map @@ -153,7 +176,7 @@ impl ACVM { /// 1. All opcodes have been executed successfully. /// 2. The circuit has been found to be unsatisfiable. /// 2. A Brillig [foreign call][`UnresolvedBrilligCall`] has been encountered and must be resolved. - pub fn solve(&mut self) -> Result { + pub fn solve(&mut self) -> ACVMStatus { // TODO: Prevent execution with outstanding foreign calls? let mut unresolved_opcodes: Vec = Vec::new(); while !self.opcodes.is_empty() { @@ -212,7 +235,7 @@ impl ACVM { Err(OpcodeResolutionError::OpcodeNotSolvable(_)) => { unreachable!("ICE - Result should have been converted to GateResolution") } - Err(err) => return Err(err), + Err(error) => return self.fail(error), } } @@ -221,18 +244,19 @@ impl ACVM { // We have oracles that must be externally resolved if self.get_pending_foreign_call().is_some() { - return Ok(PartialWitnessGeneratorStatus::RequiresForeignCall); + return self.status(ACVMStatus::RequiresForeignCall); } // We are stalled because of an opcode being bad if stalled && !self.opcodes.is_empty() { - return Err(OpcodeResolutionError::OpcodeNotSolvable( + let error = OpcodeResolutionError::OpcodeNotSolvable( opcode_not_solvable .expect("infallible: cannot be stalled and None at the same time"), - )); + ); + return self.fail(error); } } - Ok(PartialWitnessGeneratorStatus::Solved) + self.status(ACVMStatus::Solved) } } diff --git a/acvm/tests/solver.rs b/acvm/tests/solver.rs index 7202f14cb..a35424863 100644 --- a/acvm/tests/solver.rs +++ b/acvm/tests/solver.rs @@ -12,7 +12,7 @@ use acir::{ }; use acvm::{ - pwg::{ForeignCallWaitInfo, OpcodeResolutionError, PartialWitnessGeneratorStatus, ACVM}, + pwg::{ACVMStatus, ForeignCallWaitInfo, OpcodeResolutionError, ACVM}, BlackBoxFunctionSolver, }; @@ -127,12 +127,12 @@ fn inversion_brillig_oracle_equivalence() { let mut acvm = ACVM::new(StubbedBackend, opcodes, witness_assignments); // use the partial witness generation solver with our acir program - let solver_status = acvm.solve().expect("should stall on brillig call"); + let solver_status = acvm.solve(); assert_eq!( solver_status, - PartialWitnessGeneratorStatus::RequiresForeignCall, - "Should require oracle data" + ACVMStatus::RequiresForeignCall, + "should require foreign call response" ); assert!(acvm.unresolved_opcodes().is_empty(), "brillig should have been removed"); @@ -146,8 +146,8 @@ fn inversion_brillig_oracle_equivalence() { acvm.resolve_pending_foreign_call(foreign_call_result.into()); // After filling data request, continue solving - let solver_status = acvm.solve().expect("should not stall on brillig call"); - assert_eq!(solver_status, PartialWitnessGeneratorStatus::Solved, "should be fully solved"); + let solver_status = acvm.solve(); + assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); } #[test] @@ -255,11 +255,11 @@ fn double_inversion_brillig_oracle() { let mut acvm = ACVM::new(StubbedBackend, opcodes, witness_assignments); // use the partial witness generation solver with our acir program - let solver_status = acvm.solve().expect("should stall on oracle"); + let solver_status = acvm.solve(); assert_eq!( solver_status, - PartialWitnessGeneratorStatus::RequiresForeignCall, - "Should require oracle data" + ACVMStatus::RequiresForeignCall, + "should require foreign call response" ); assert!(acvm.unresolved_opcodes().is_empty(), "brillig should have been removed"); @@ -273,11 +273,11 @@ fn double_inversion_brillig_oracle() { acvm.resolve_pending_foreign_call(x_plus_y_inverse.into()); // After filling data request, continue solving - let solver_status = acvm.solve().expect("should stall on brillig call"); + let solver_status = acvm.solve(); assert_eq!( solver_status, - PartialWitnessGeneratorStatus::RequiresForeignCall, - "Should require oracle data" + ACVMStatus::RequiresForeignCall, + "should require foreign call response" ); assert!(acvm.unresolved_opcodes().is_empty(), "should be fully solved"); @@ -292,8 +292,8 @@ fn double_inversion_brillig_oracle() { acvm.resolve_pending_foreign_call(i_plus_j_inverse.into()); // After filling data request, continue solving - let solver_status = acvm.solve().expect("should not stall on brillig call"); - assert_eq!(solver_status, PartialWitnessGeneratorStatus::Solved, "should be fully solved"); + let solver_status = acvm.solve(); + assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); } #[test] @@ -375,11 +375,11 @@ fn oracle_dependent_execution() { let mut acvm = ACVM::new(StubbedBackend, opcodes, witness_assignments); // use the partial witness generation solver with our acir program - let solver_status = acvm.solve().expect("should stall on oracle"); + let solver_status = acvm.solve(); assert_eq!( solver_status, - PartialWitnessGeneratorStatus::RequiresForeignCall, - "Should require oracle data" + ACVMStatus::RequiresForeignCall, + "should require foreign call response" ); assert_eq!(acvm.unresolved_opcodes().len(), 1, "brillig should have been removed"); assert_eq!( @@ -397,11 +397,11 @@ fn oracle_dependent_execution() { acvm.resolve_pending_foreign_call(x_inverse.into()); // After filling data request, continue solving - let solver_status = acvm.solve().expect("should stall on oracle"); + let solver_status = acvm.solve(); assert_eq!( solver_status, - PartialWitnessGeneratorStatus::RequiresForeignCall, - "Should require oracle data" + ACVMStatus::RequiresForeignCall, + "should require foreign call response" ); assert_eq!(acvm.unresolved_opcodes().len(), 1, "brillig should have been removed"); assert_eq!( @@ -421,8 +421,8 @@ fn oracle_dependent_execution() { // We've resolved all the brillig foreign calls so we should be able to complete execution now. // After filling data request, continue solving - let solver_status = acvm.solve().expect("should not stall on brillig call"); - assert_eq!(solver_status, PartialWitnessGeneratorStatus::Solved, "should be fully solved"); + let solver_status = acvm.solve(); + assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); } #[test] @@ -504,6 +504,6 @@ fn brillig_oracle_predicate() { .into(); let mut acvm = ACVM::new(StubbedBackend, opcodes, witness_assignments); - let solver_status = acvm.solve().expect("should not stall on brillig call"); - assert_eq!(solver_status, PartialWitnessGeneratorStatus::Solved, "should be fully solved"); + let solver_status = acvm.solve(); + assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); } From 85c3943b11c02f15a967d92e437700a879840401 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 5 Jul 2023 09:12:47 +0000 Subject: [PATCH 02/28] chore: add test that ACVM can be finalized when solved --- acvm/tests/solver.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/acvm/tests/solver.rs b/acvm/tests/solver.rs index a35424863..47a08b5ac 100644 --- a/acvm/tests/solver.rs +++ b/acvm/tests/solver.rs @@ -148,6 +148,9 @@ fn inversion_brillig_oracle_equivalence() { // After filling data request, continue solving let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); + + // ACVM should be finalizable in `Solved` state. + acvm.finalize(); } #[test] @@ -294,6 +297,9 @@ fn double_inversion_brillig_oracle() { // After filling data request, continue solving let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); + + // ACVM should be finalizable in `Solved` state. + acvm.finalize(); } #[test] @@ -423,6 +429,9 @@ fn oracle_dependent_execution() { // After filling data request, continue solving let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); + + // ACVM should be finalizable in `Solved` state. + acvm.finalize(); } #[test] @@ -506,4 +515,7 @@ fn brillig_oracle_predicate() { let mut acvm = ACVM::new(StubbedBackend, opcodes, witness_assignments); let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); + + // ACVM should be finalizable in `Solved` state. + acvm.finalize(); } From cf084d6b2d9bb81813ff1fa43b6b2927843af549 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 5 Jul 2023 09:16:29 +0000 Subject: [PATCH 03/28] chore: make cspell happy --- acvm/tests/solver.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/acvm/tests/solver.rs b/acvm/tests/solver.rs index 47a08b5ac..50a544b6e 100644 --- a/acvm/tests/solver.rs +++ b/acvm/tests/solver.rs @@ -149,7 +149,7 @@ fn inversion_brillig_oracle_equivalence() { let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); - // ACVM should be finalizable in `Solved` state. + // ACVM should be able to be finalized in `Solved` state. acvm.finalize(); } @@ -298,7 +298,7 @@ fn double_inversion_brillig_oracle() { let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); - // ACVM should be finalizable in `Solved` state. + // ACVM should be able to be finalized in `Solved` state. acvm.finalize(); } @@ -430,7 +430,7 @@ fn oracle_dependent_execution() { let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); - // ACVM should be finalizable in `Solved` state. + // ACVM should be able to be finalized in `Solved` state. acvm.finalize(); } @@ -516,6 +516,6 @@ fn brillig_oracle_predicate() { let solver_status = acvm.solve(); assert_eq!(solver_status, ACVMStatus::Solved, "should be fully solved"); - // ACVM should be finalizable in `Solved` state. + // ACVM should be able to be finalized in `Solved` state. acvm.finalize(); } From c452d9d07c6ae0a153117dfcf9beff12aa5ebc77 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 5 Jul 2023 10:05:27 +0000 Subject: [PATCH 04/28] chore: fix doc comment --- acvm/src/pwg/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index f07f9846a..617028b1a 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -141,7 +141,7 @@ impl ACVM { status } - /// Sets the VM status to [ACVMStatus::Failure] using the provided error`. + /// Sets the VM status to [ACVMStatus::Failure] using the provided `error`. /// Returns the new status. fn fail(&mut self, error: OpcodeResolutionError) -> ACVMStatus { self.status(ACVMStatus::Failure(error)) From 925e84eb6e42f99e4b898fac5a06c597ae0934ea Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 21 Jun 2023 15:14:35 +0000 Subject: [PATCH 05/28] feat(acvm)!: Support stepwise execution of ACIR --- acvm/src/pwg/block.rs | 36 +++----- acvm/src/pwg/mod.rs | 193 ++++++++++++++++++++---------------------- acvm/tests/solver.rs | 45 ++++------ 3 files changed, 118 insertions(+), 156 deletions(-) diff --git a/acvm/src/pwg/block.rs b/acvm/src/pwg/block.rs index 05ef57ef4..463b8e589 100644 --- a/acvm/src/pwg/block.rs +++ b/acvm/src/pwg/block.rs @@ -16,20 +16,9 @@ use super::{OpcodeNotSolvable, OpcodeResolution, OpcodeResolutionError}; /// block_value is the value of the Block at the solved_operations step /// solved_operations is the number of solved elements in the block #[derive(Default)] -pub(super) struct BlockSolver { - block_value: HashMap, - solved_operations: usize, -} +pub(super) struct BlockSolver; impl BlockSolver { - fn insert_value(&mut self, index: u32, value: FieldElement) { - self.block_value.insert(index, value); - } - - fn get_value(&self, index: u32) -> Option { - self.block_value.get(&index).copied() - } - // Helper function which tries to solve a Block opcode // As long as operations are resolved, we update/read from the block_value // We stop when an operation cannot be resolved @@ -44,7 +33,9 @@ impl BlockSolver { )) }; - for block_op in trace.iter().skip(self.solved_operations) { + let mut block_value: HashMap = HashMap::new(); + + for block_op in trace.iter() { let op_expr = ArithmeticSolver::evaluate(&block_op.operation, initial_witness); let operation = op_expr.to_const().ok_or_else(|| { missing_assignment(ArithmeticSolver::any_witness_from_expression(&op_expr)) @@ -57,23 +48,24 @@ impl BlockSolver { let value = ArithmeticSolver::evaluate(&block_op.value, initial_witness); let value_witness = ArithmeticSolver::any_witness_from_expression(&value); if value.is_const() { - self.insert_value(index, value.q_c); + block_value.insert(index, value.q_c); } else if operation.is_zero() && value.is_linear() { match ArithmeticSolver::solve_fan_in_term(&value, initial_witness) { GateStatus::GateUnsolvable => return Err(missing_assignment(value_witness)), GateStatus::GateSolvable(sum, (coef, w)) => { - let map_value = - self.get_value(index).ok_or_else(|| missing_assignment(Some(w)))?; + let map_value = block_value + .get(&index) + .copied() + .ok_or_else(|| missing_assignment(Some(w)))?; insert_value(&w, (map_value - sum - value.q_c) / coef, initial_witness)?; } GateStatus::GateSatisfied(sum) => { - self.insert_value(index, sum + value.q_c); + block_value.insert(index, sum + value.q_c); } } } else { return Err(missing_assignment(value_witness)); } - self.solved_operations += 1; } Ok(()) } @@ -86,16 +78,10 @@ impl BlockSolver { initial_witness: &mut WitnessMap, trace: &[MemOp], ) -> Result { - let initial_solved_operations = self.solved_operations; - match self.solve_helper(initial_witness, trace) { Ok(()) => Ok(OpcodeResolution::Solved), Err(OpcodeResolutionError::OpcodeNotSolvable(err)) => { - if self.solved_operations > initial_solved_operations { - Ok(OpcodeResolution::InProgress) - } else { - Ok(OpcodeResolution::Stalled(err)) - } + Ok(OpcodeResolution::Stalled(err)) } Err(err) => Err(err), } diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 617028b1a..161e0e6a1 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -1,10 +1,8 @@ // Re-usable methods that backends can use to implement their PWG -use std::collections::HashMap; - use acir::{ brillig_vm::ForeignCallResult, - circuit::{brillig::Brillig, opcodes::BlockId, Opcode}, + circuit::{brillig::Brillig, Opcode}, native_types::{Expression, Witness, WitnessMap}, BlackBoxFunc, FieldElement, }; @@ -46,7 +44,7 @@ pub enum ACVMStatus { /// to the ACVM using [`ACVM::resolve_pending_foreign_call`]. /// /// Once this is done, the ACVM can be restarted to solve the remaining opcodes. - RequiresForeignCall, + RequiresForeignCall(UnresolvedBrilligCall), } #[derive(Debug, PartialEq)] @@ -95,17 +93,13 @@ pub struct ACVM { status: ACVMStatus, backend: B, - /// Stores the solver for each [block][`Opcode::Block`] opcode. This persists their internal state to prevent recomputation. - block_solvers: HashMap, + /// A list of opcodes which are to be executed by the ACVM. - /// - /// Note that this doesn't include any opcodes which are waiting on a pending foreign call. opcodes: Vec, + /// Index of the next opcode to be executed. + instruction_pointer: usize, witness_map: WitnessMap, - - /// A list of foreign calls which must be resolved before the ACVM can resume execution. - pending_foreign_calls: Vec, } impl ACVM { @@ -113,10 +107,9 @@ impl ACVM { ACVM { status: ACVMStatus::InProgress, backend, - block_solvers: HashMap::default(), opcodes, + instruction_pointer: 0, witness_map: initial_witness, - pending_foreign_calls: Vec::new(), } } @@ -127,13 +120,24 @@ impl ACVM { &self.witness_map } - /// Returns a slice containing the opcodes which remain to be solved. - /// - /// Note: this doesn't include any opcodes which are waiting on a pending foreign call. - pub fn unresolved_opcodes(&self) -> &[Opcode] { + /// Returns a slice containing the opcodes of the circuit being executed. + pub fn opcodes(&self) -> &[Opcode] { &self.opcodes } + /// Returns the index of the current opcode to be executed. + pub fn instruction_pointer(&self) -> usize { + self.instruction_pointer + } + + /// Finalize the ACVM execution, returning the resulting [`WitnessMap`]. + pub fn finalize(self) -> WitnessMap { + if self.status != ACVMStatus::Solved { + panic!("ACVM is not ready to be finalized"); + } + self.witness_map + } + /// Updates the current status of the VM. /// Returns the given status. fn status(&mut self, status: ACVMStatus) -> ACVMStatus { @@ -147,27 +151,45 @@ impl ACVM { self.status(ACVMStatus::Failure(error)) } - /// Finalize the ACVM execution, returning the resulting [`WitnessMap`]. - pub fn finalize(self) -> WitnessMap { - if !matches!(self.status, ACVMStatus::Solved) { - panic!("ACVM is not ready to be finalized"); - } - self.witness_map + /// Sets the status of the VM to `RequiresForeignCall`. + /// Indicating that the VM is now waiting for a foreign call to be resolved. + fn wait_for_foreign_call( + &mut self, + opcode: Opcode, + foreign_call_wait_info: ForeignCallWaitInfo, + ) -> ACVMStatus { + let brillig = match opcode { + Opcode::Brillig(brillig) => brillig, + _ => unreachable!("Brillig resolution for non brillig opcode"), + }; + let foreign_call = UnresolvedBrilligCall { brillig, foreign_call_wait_info }; + self.status(ACVMStatus::RequiresForeignCall(foreign_call)) } /// Return a reference to the arguments for the next pending foreign call, if one exists. pub fn get_pending_foreign_call(&self) -> Option<&ForeignCallWaitInfo> { - self.pending_foreign_calls.first().map(|foreign_call| &foreign_call.foreign_call_wait_info) + if let ACVMStatus::RequiresForeignCall(foreign_call) = &self.status { + Some(&foreign_call.foreign_call_wait_info) + } else { + None + } } /// Resolves a pending foreign call using a result calculated outside of the ACVM. pub fn resolve_pending_foreign_call(&mut self, foreign_call_result: ForeignCallResult) { - // Remove the first foreign call and inject the result to create a new opcode. - let foreign_call = self.pending_foreign_calls.remove(0); + let foreign_call = if let ACVMStatus::RequiresForeignCall(foreign_call) = &self.status { + // TODO: We can avoid this clone + foreign_call.clone() + } else { + panic!("no foreign call") + }; let resolved_brillig = foreign_call.resolve(foreign_call_result); - // Mark this opcode to be executed next. - self.opcodes.insert(0, Opcode::Brillig(resolved_brillig)); + // Overwrite the brillig opcode with a new one with the foreign call response. + self.opcodes[self.instruction_pointer] = Opcode::Brillig(resolved_brillig); + + // Now that the foreign call has been resolved then we can resume execution. + self.status(ACVMStatus::InProgress); } /// Executes the ACVM's circuit until execution halts. @@ -177,86 +199,55 @@ impl ACVM { /// 2. The circuit has been found to be unsatisfiable. /// 2. A Brillig [foreign call][`UnresolvedBrilligCall`] has been encountered and must be resolved. pub fn solve(&mut self) -> ACVMStatus { - // TODO: Prevent execution with outstanding foreign calls? - let mut unresolved_opcodes: Vec = Vec::new(); - while !self.opcodes.is_empty() { - unresolved_opcodes.clear(); - let mut stalled = true; - let mut opcode_not_solvable = None; - for opcode in &self.opcodes { - let resolution = match opcode { - Opcode::Arithmetic(expr) => { - ArithmeticSolver::solve(&mut self.witness_map, expr) - } - Opcode::BlackBoxFuncCall(bb_func) => { - blackbox::solve(&self.backend, &mut self.witness_map, bb_func) - } - Opcode::Directive(directive) => { - solve_directives(&mut self.witness_map, directive) - } - Opcode::Block(block) | Opcode::ROM(block) | Opcode::RAM(block) => { - let solver = self.block_solvers.entry(block.id).or_default(); - solver.solve(&mut self.witness_map, &block.trace) - } - Opcode::Brillig(brillig) => { - BrilligSolver::solve(&mut self.witness_map, brillig) - } - }; + while self.status == ACVMStatus::InProgress { + self.solve_opcode(); + } + self.status.clone() + } + + pub fn solve_opcode(&mut self) -> ACVMStatus { + let opcode = &self.opcodes[self.instruction_pointer]; + + let resolution = match opcode { + Opcode::Arithmetic(expr) => ArithmeticSolver::solve(&mut self.witness_map, expr), + Opcode::BlackBoxFuncCall(bb_func) => { + blackbox::solve(&self.backend, &mut self.witness_map, bb_func) + } + Opcode::Directive(directive) => solve_directives(&mut self.witness_map, directive), + Opcode::Block(block) | Opcode::ROM(block) | Opcode::RAM(block) => { + BlockSolver.solve(&mut self.witness_map, &block.trace) + } + Opcode::Brillig(brillig) => { + let resolution = BrilligSolver::solve(&mut self.witness_map, brillig); + match resolution { - Ok(OpcodeResolution::Solved) => { - stalled = false; - } - Ok(OpcodeResolution::InProgress) => { - stalled = false; - unresolved_opcodes.push(opcode.clone()); - } - Ok(OpcodeResolution::InProgressBrillig(oracle_wait_info)) => { - stalled = false; - // InProgressBrillig Oracles must be externally re-solved - let brillig = match opcode { - Opcode::Brillig(brillig) => brillig.clone(), - _ => unreachable!("Brillig resolution for non brillig opcode"), - }; - self.pending_foreign_calls.push(UnresolvedBrilligCall { - brillig, - foreign_call_wait_info: oracle_wait_info, - }) - } - Ok(OpcodeResolution::Stalled(not_solvable)) => { - if opcode_not_solvable.is_none() { - // we keep track of the first unsolvable opcode - opcode_not_solvable = Some(not_solvable); - } - // We push those opcodes not solvable to the back as - // it could be because the opcodes are out of order, i.e. this assignment - // relies on a later opcodes' results - unresolved_opcodes.push(opcode.clone()); - } - Err(OpcodeResolutionError::OpcodeNotSolvable(_)) => { - unreachable!("ICE - Result should have been converted to GateResolution") + Ok(OpcodeResolution::InProgressBrillig(foreign_call_wait_info)) => { + return self.wait_for_foreign_call(opcode.clone(), foreign_call_wait_info) } - Err(error) => return self.fail(error), + res => res, } } - - // Before potentially ending execution, we must save the list of opcodes which remain to be solved. - std::mem::swap(&mut self.opcodes, &mut unresolved_opcodes); - - // We have oracles that must be externally resolved - if self.get_pending_foreign_call().is_some() { - return self.status(ACVMStatus::RequiresForeignCall); + }; + match resolution { + Ok(OpcodeResolution::Solved) => { + self.instruction_pointer += 1; + if self.instruction_pointer == self.opcodes.len() { + self.status(ACVMStatus::Solved) + } else { + self.status(ACVMStatus::InProgress) + } } - - // We are stalled because of an opcode being bad - if stalled && !self.opcodes.is_empty() { - let error = OpcodeResolutionError::OpcodeNotSolvable( - opcode_not_solvable - .expect("infallible: cannot be stalled and None at the same time"), - ); - return self.fail(error); + Ok(OpcodeResolution::InProgress) => { + unreachable!("Opcodes should be immediately solvable"); + } + Ok(OpcodeResolution::InProgressBrillig(_)) => { + unreachable!("Handled above") } + Ok(OpcodeResolution::Stalled(not_solvable)) => self.status(ACVMStatus::Failure( + OpcodeResolutionError::OpcodeNotSolvable(not_solvable), + )), + Err(error) => self.fail(error), } - self.status(ACVMStatus::Solved) } } diff --git a/acvm/tests/solver.rs b/acvm/tests/solver.rs index 50a544b6e..cab984c2a 100644 --- a/acvm/tests/solver.rs +++ b/acvm/tests/solver.rs @@ -129,12 +129,11 @@ fn inversion_brillig_oracle_equivalence() { // use the partial witness generation solver with our acir program let solver_status = acvm.solve(); - assert_eq!( - solver_status, - ACVMStatus::RequiresForeignCall, + assert!( + matches!(solver_status, ACVMStatus::RequiresForeignCall(_)), "should require foreign call response" ); - assert!(acvm.unresolved_opcodes().is_empty(), "brillig should have been removed"); + assert_eq!(acvm.instruction_pointer(), 0, "brillig should have been removed"); let foreign_call_wait_info: &ForeignCallWaitInfo = acvm.get_pending_foreign_call().expect("should have a brillig foreign call request"); @@ -259,12 +258,11 @@ fn double_inversion_brillig_oracle() { // use the partial witness generation solver with our acir program let solver_status = acvm.solve(); - assert_eq!( - solver_status, - ACVMStatus::RequiresForeignCall, + assert!( + matches!(solver_status, ACVMStatus::RequiresForeignCall(_)), "should require foreign call response" ); - assert!(acvm.unresolved_opcodes().is_empty(), "brillig should have been removed"); + assert_eq!(acvm.instruction_pointer(), 0, "should stall on brillig"); let foreign_call_wait_info: &ForeignCallWaitInfo = acvm.get_pending_foreign_call().expect("should have a brillig foreign call request"); @@ -277,12 +275,11 @@ fn double_inversion_brillig_oracle() { // After filling data request, continue solving let solver_status = acvm.solve(); - assert_eq!( - solver_status, - ACVMStatus::RequiresForeignCall, + assert!( + matches!(solver_status, ACVMStatus::RequiresForeignCall(_)), "should require foreign call response" ); - assert!(acvm.unresolved_opcodes().is_empty(), "should be fully solved"); + assert_eq!(acvm.instruction_pointer(), 0, "should stall on brillig"); let foreign_call_wait_info = acvm.get_pending_foreign_call().expect("should have a brillig foreign call request"); @@ -382,17 +379,11 @@ fn oracle_dependent_execution() { // use the partial witness generation solver with our acir program let solver_status = acvm.solve(); - assert_eq!( - solver_status, - ACVMStatus::RequiresForeignCall, + assert!( + matches!(solver_status, ACVMStatus::RequiresForeignCall(_)), "should require foreign call response" ); - assert_eq!(acvm.unresolved_opcodes().len(), 1, "brillig should have been removed"); - assert_eq!( - acvm.unresolved_opcodes()[0], - Opcode::Arithmetic(inverse_equality_check.clone()), - "Equality check of inverses should still be waiting to be resolved" - ); + assert_eq!(acvm.instruction_pointer(), 1, "should stall on brillig"); let foreign_call_wait_info: &ForeignCallWaitInfo = acvm.get_pending_foreign_call().expect("should have a brillig foreign call request"); @@ -404,17 +395,11 @@ fn oracle_dependent_execution() { // After filling data request, continue solving let solver_status = acvm.solve(); - assert_eq!( - solver_status, - ACVMStatus::RequiresForeignCall, + assert!( + matches!(solver_status, ACVMStatus::RequiresForeignCall(_)), "should require foreign call response" ); - assert_eq!(acvm.unresolved_opcodes().len(), 1, "brillig should have been removed"); - assert_eq!( - acvm.unresolved_opcodes()[0], - Opcode::Arithmetic(inverse_equality_check), - "Equality check of inverses should still be waiting to be resolved" - ); + assert_eq!(acvm.instruction_pointer(), 1, "should stall on brillig"); let foreign_call_wait_info: &ForeignCallWaitInfo = acvm.get_pending_foreign_call().expect("should have a brillig foreign call request"); From 5b0b3c89b4e067693b8d61c8b0550499805e6f4b Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Wed, 5 Jul 2023 10:19:08 +0000 Subject: [PATCH 06/28] chore: replace pattern match with equality check --- acvm/src/pwg/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 617028b1a..9be192ff9 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -149,7 +149,7 @@ impl ACVM { /// Finalize the ACVM execution, returning the resulting [`WitnessMap`]. pub fn finalize(self) -> WitnessMap { - if !matches!(self.status, ACVMStatus::Solved) { + if self.status != ACVMStatus::Solved { panic!("ACVM is not ready to be finalized"); } self.witness_map From 66b26436582e6e51ff06f731b2b16e2324148fe4 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 10 Jul 2023 09:25:19 +0000 Subject: [PATCH 07/28] chore!: remove unnecessary brillig hashing --- Cargo.toml | 1 - acir/Cargo.toml | 2 +- acir/src/circuit/brillig.rs | 4 ++-- acvm/Cargo.toml | 1 - acvm/src/pwg/mod.rs | 25 ------------------------- 5 files changed, 3 insertions(+), 30 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f871bac25..69e49789d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,7 +13,6 @@ repository = "https://github.com/noir-lang/acvm/" acir = { version = "0.17.0", path = "acir", default-features = false } acir_field = { version = "0.17.0", path = "acir_field", default-features = false } stdlib = { package = "acvm_stdlib", version = "0.17.0", path = "stdlib", default-features = false } -rmp-serde = "1.1.0" num-bigint = "0.4" num-traits = "0.2" diff --git a/acir/Cargo.toml b/acir/Cargo.toml index ee1570dc3..9e121b472 100644 --- a/acir/Cargo.toml +++ b/acir/Cargo.toml @@ -15,7 +15,7 @@ acir_field.workspace = true serde.workspace = true brillig_vm = { version = "0.17.0", path = "../brillig_vm", default-features = false } thiserror.workspace = true -rmp-serde.workspace = true +rmp-serde = "1.1.0" flate2 = "1.0.24" [dev-dependencies] diff --git a/acir/src/circuit/brillig.rs b/acir/src/circuit/brillig.rs index 02732c7d6..efc381675 100644 --- a/acir/src/circuit/brillig.rs +++ b/acir/src/circuit/brillig.rs @@ -4,7 +4,7 @@ use serde::{Deserialize, Serialize}; /// Inputs for the Brillig VM. These are the initial inputs /// that the Brillig VM will use to start. -#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug, Hash)] +#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug)] pub enum BrilligInputs { Single(Expression), Array(Vec), @@ -12,7 +12,7 @@ pub enum BrilligInputs { /// Outputs for the Brillig VM. Once the VM has completed /// execution, this will be the object that is returned. -#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug, Hash)] +#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug)] pub enum BrilligOutputs { Simple(Witness), Array(Vec), diff --git a/acvm/Cargo.toml b/acvm/Cargo.toml index 97f7829fc..9f91cd105 100644 --- a/acvm/Cargo.toml +++ b/acvm/Cargo.toml @@ -14,7 +14,6 @@ repository.workspace = true num-bigint.workspace = true num-traits.workspace = true thiserror.workspace = true -rmp-serde.workspace = true acir.workspace = true stdlib.workspace = true diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 4866a7233..731174913 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -383,28 +383,3 @@ pub fn default_is_opcode_supported(language: Language) -> fn(&Opcode) -> bool { Language::PLONKCSat { .. } => plonk_is_supported, } } - -/// Canonically hashes the Brillig struct. -/// -/// Some Brillig instances may or may not be resolved, so we do -/// not hash the `foreign_call_results`. -/// -/// This gives us a consistent hash that will be used to track `Brillig` -/// even when it is put back into the list of opcodes out of order. -/// This happens when we resolve a Brillig opcode call. -pub fn canonical_brillig_hash(brillig: &Brillig) -> UnresolvedBrilligCallHash { - let mut serialized_vector = rmp_serde::to_vec(&brillig.inputs).unwrap(); - serialized_vector.extend(rmp_serde::to_vec(&brillig.outputs).unwrap()); - serialized_vector.extend(rmp_serde::to_vec(&brillig.bytecode).unwrap()); - serialized_vector.extend(rmp_serde::to_vec(&brillig.predicate).unwrap()); - - use std::collections::hash_map::DefaultHasher; - use std::hash::Hasher; - - let mut hasher = DefaultHasher::new(); - hasher.write(&serialized_vector); - hasher.finish() -} - -/// Hash of an unresolved brillig call instance -pub(crate) type UnresolvedBrilligCallHash = u64; From 8b0c7b3d2cff82b130d82eb3bcaf549497866a18 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 10 Jul 2023 09:33:10 +0000 Subject: [PATCH 08/28] chore!: remove explicit tracking of `OpcodeLabel`s --- acvm/src/pwg/mod.rs | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 731174913..0bdcac907 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -94,8 +94,8 @@ pub struct ACVM { backend: B, - /// A list of opcodes which are to be executed by the ACVM, along with their label - opcodes_and_labels: Vec<(Opcode, OpcodeLabel)>, + /// A list of opcodes which are to be executed by the ACVM. + opcodes: Vec, /// Index of the next opcode to be executed. instruction_pointer: usize, @@ -104,17 +104,10 @@ pub struct ACVM { impl ACVM { pub fn new(backend: B, opcodes: Vec, initial_witness: WitnessMap) -> Self { - let opcodes_and_labels = opcodes - .iter() - .enumerate() - .map(|(opcode_index, opcode)| { - (opcode.clone(), OpcodeLabel::Resolved(opcode_index as u64)) - }) - .collect(); ACVM { status: ACVMStatus::InProgress, backend, - opcodes_and_labels, + opcodes, instruction_pointer: 0, witness_map: initial_witness, } @@ -128,8 +121,8 @@ impl ACVM { } /// Returns a slice containing the opcodes of the circuit being executed. - pub fn opcodes(&self) -> &[(Opcode, OpcodeLabel)] { - &self.opcodes_and_labels + pub fn opcodes(&self) -> &[Opcode] { + &self.opcodes } /// Returns the index of the current opcode to be executed. @@ -193,7 +186,7 @@ impl ACVM { let resolved_brillig = foreign_call.resolve(foreign_call_result); // Overwrite the brillig opcode with a new one with the foreign call response. - self.opcodes_and_labels[self.instruction_pointer].0 = Opcode::Brillig(resolved_brillig); + self.opcodes[self.instruction_pointer] = Opcode::Brillig(resolved_brillig); // Now that the foreign call has been resolved then we can resume execution. self.status(ACVMStatus::InProgress); @@ -213,7 +206,7 @@ impl ACVM { } pub fn solve_opcode(&mut self) -> ACVMStatus { - let (opcode, opcode_label) = &self.opcodes_and_labels[self.instruction_pointer]; + let opcode = &self.opcodes[self.instruction_pointer]; let resolution = match opcode { Opcode::Arithmetic(expr) => ArithmeticSolver::solve(&mut self.witness_map, expr), @@ -238,7 +231,7 @@ impl ACVM { match resolution { Ok(OpcodeResolution::Solved) => { self.instruction_pointer += 1; - if self.instruction_pointer == self.opcodes_and_labels.len() { + if self.instruction_pointer == self.opcodes.len() { self.status(ACVMStatus::Solved) } else { self.status(ACVMStatus::InProgress) @@ -254,20 +247,20 @@ impl ACVM { self.fail(OpcodeResolutionError::OpcodeNotSolvable(not_solvable)) } Err(mut error) => { + let opcode_label = + OpcodeLabel::Resolved(self.instruction_pointer.try_into().unwrap()); match &mut error { // If we have an unsatisfied constraint, the opcode label will be unresolved // because the solvers do not have knowledge of this information. // We resolve, by setting this to the corresponding opcode that we just attempted to solve. OpcodeResolutionError::UnsatisfiedConstrain { opcode_label: opcode_index } => { - *opcode_index = *opcode_label; + *opcode_index = opcode_label; } // If a brillig function has failed, we return an unsatisfied constraint error // We intentionally ignore the brillig failure message, as there is no way to // propagate this to the caller. OpcodeResolutionError::BrilligFunctionFailed(_) => { - error = OpcodeResolutionError::UnsatisfiedConstrain { - opcode_label: *opcode_label, - } + error = OpcodeResolutionError::UnsatisfiedConstrain { opcode_label } } // All other errors are thrown normally. _ => (), From d03818bd5d7f267bcb2fd24594c3f5f7b72e0668 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 10 Jul 2023 14:13:37 +0000 Subject: [PATCH 09/28] fix: set ACVM status to `Solved` if passed an empty circuit --- acvm/src/pwg/mod.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/acvm/src/pwg/mod.rs b/acvm/src/pwg/mod.rs index 0bdcac907..695b2b191 100644 --- a/acvm/src/pwg/mod.rs +++ b/acvm/src/pwg/mod.rs @@ -104,13 +104,8 @@ pub struct ACVM { impl ACVM { pub fn new(backend: B, opcodes: Vec, initial_witness: WitnessMap) -> Self { - ACVM { - status: ACVMStatus::InProgress, - backend, - opcodes, - instruction_pointer: 0, - witness_map: initial_witness, - } + let status = if opcodes.is_empty() { ACVMStatus::Solved } else { ACVMStatus::InProgress }; + ACVM { status, backend, opcodes, instruction_pointer: 0, witness_map: initial_witness } } /// Returns a reference to the current state of the ACVM's [`WitnessMap`]. From 9810b460dba878204e2ed3d4795b940883c2031b Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 10 Jul 2023 14:41:46 +0000 Subject: [PATCH 10/28] chore: remove sorting of opcodes in `acvm::compiler::compile` --- acvm/src/compiler/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index 4ca7ecd68..ecaa981b8 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -102,7 +102,6 @@ pub fn compile( new_gates.push(intermediate_gate); } new_gates.push(arith_expr); - new_gates.sort(); for gate in new_gates { new_opcode_labels.push(opcode_label[index]); transformed_gates.push(Opcode::Arithmetic(gate)); From 1dda0c5eb0748fb5aec7401ae9834c54b2cc2b61 Mon Sep 17 00:00:00 2001 From: guipublic Date: Wed, 12 Jul 2023 17:05:39 +0000 Subject: [PATCH 11/28] csat generates solvable intermediate gates --- acvm/src/compiler/mod.rs | 99 ++++++++++++++- acvm/src/compiler/transformers/csat.rs | 161 +++++++++++++++++-------- 2 files changed, 206 insertions(+), 54 deletions(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index ecaa981b8..506b44e97 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -1,5 +1,5 @@ use acir::{ - circuit::{Circuit, Opcode, OpcodeLabel}, + circuit::{brillig::BrilligOutputs, directives::Directive, Circuit, Opcode, OpcodeLabel}, native_types::{Expression, Witness}, BlackBoxFunc, FieldElement, }; @@ -26,6 +26,7 @@ pub enum CompileError { /// Applies [`ProofSystemCompiler`][crate::ProofSystemCompiler] specific optimizations to a [`Circuit`]. pub fn compile( acir: Circuit, + inputs: Vec, np_language: Language, is_opcode_supported: impl Fn(&Opcode) -> bool, simplifier: &CircuitSimplifier, @@ -58,12 +59,18 @@ pub fn compile( let range_optimizer = RangeOptimizer::new(acir); let (acir, opcode_label) = range_optimizer.replace_redundant_ranges(opcode_label); - let transformer = match &np_language { + let mut transformer = match &np_language { crate::Language::R1CS => { let transformer = R1CSTransformer::new(acir); return Ok((transformer.transform(), opcode_label)); } - crate::Language::PLONKCSat { width } => CSatTransformer::new(*width), + crate::Language::PLONKCSat { width } => { + let mut csat = CSatTransformer::new(*width); + for value in inputs { + csat.solvable(value); + } + csat + } }; // TODO: the code below is only for CSAT transformer @@ -107,9 +114,91 @@ pub fn compile( transformed_gates.push(Opcode::Arithmetic(gate)); } } - other_gate => { + Opcode::BlackBoxFuncCall(func) => { + match func { + acir::circuit::opcodes::BlackBoxFuncCall::AND { output, .. } + | acir::circuit::opcodes::BlackBoxFuncCall::XOR { output, .. } => { + transformer.solvable(*output) + } + acir::circuit::opcodes::BlackBoxFuncCall::RANGE { .. } => (), + acir::circuit::opcodes::BlackBoxFuncCall::SHA256 { outputs, .. } + | acir::circuit::opcodes::BlackBoxFuncCall::Keccak256 { outputs, .. } + | acir::circuit::opcodes::BlackBoxFuncCall::Keccak256VariableLength { + outputs, + .. + } + | acir::circuit::opcodes::BlackBoxFuncCall::RecursiveAggregation { + output_aggregation_object: outputs, + .. + } + | acir::circuit::opcodes::BlackBoxFuncCall::Blake2s { outputs, .. } => { + for witness in outputs { + transformer.solvable(*witness); + } + } + acir::circuit::opcodes::BlackBoxFuncCall::FixedBaseScalarMul { + outputs, + .. + } + | acir::circuit::opcodes::BlackBoxFuncCall::Pedersen { outputs, .. } => { + transformer.solvable(outputs.0); + transformer.solvable(outputs.1) + } + acir::circuit::opcodes::BlackBoxFuncCall::HashToField128Security { + output, + .. + } + | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256k1 { output, .. } + | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256r1 { output, .. } + | acir::circuit::opcodes::BlackBoxFuncCall::SchnorrVerify { output, .. } => { + transformer.solvable(*output) + } + } + + new_opcode_labels.push(opcode_label[index]); + transformed_gates.push(opcode.clone()); + } + Opcode::Directive(directive) => { + dbg!(&directive); + match directive { + Directive::Invert { result, .. } => { + transformer.solvable(*result); + } + Directive::Quotient(quotient_directive) => { + transformer.solvable(quotient_directive.q); + transformer.solvable(quotient_directive.r); + } + Directive::ToLeRadix { b, .. } => { + for w in b { + transformer.solvable(*w); + } + } + Directive::PermutationSort { bits, .. } => { + for w in bits { + transformer.solvable(*w); + } + } + Directive::Log(_) => (), + } + new_opcode_labels.push(opcode_label[index]); + transformed_gates.push(opcode.clone()); + } + Opcode::Block(_) => todo!(), + Opcode::ROM(_) => todo!(), + Opcode::RAM(_) => todo!(), + Opcode::Brillig(brillig) => { + for output in &brillig.outputs { + match output { + BrilligOutputs::Simple(w) => transformer.solvable(*w), + BrilligOutputs::Array(v) => { + for w in v { + transformer.solvable(*w); + } + } + } + } new_opcode_labels.push(opcode_label[index]); - transformed_gates.push(other_gate.clone()) + transformed_gates.push(opcode.clone()); } } } diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 3fd4d037c..0bfb317b7 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -1,4 +1,4 @@ -use std::cmp::Ordering; +use std::{cmp::Ordering, collections::HashSet}; use acir::{ native_types::{Expression, Witness}, @@ -17,6 +17,8 @@ use indexmap::IndexMap; // Have a single transformer that you instantiate with a width, then pass many gates through pub(crate) struct CSatTransformer { width: usize, + /// Track the witness that can be solved + solvable_witness: HashSet, } impl CSatTransformer { @@ -24,14 +26,47 @@ impl CSatTransformer { pub(crate) fn new(width: usize) -> CSatTransformer { assert!(width > 2); - CSatTransformer { width } + CSatTransformer { width, solvable_witness: HashSet::new() } + } + + /// Returns true if the equation 'expression=0' can be solved, and add the solved witness to set of solvable witness + fn solvable_expression(&mut self, gate: &Expression) -> bool { + let mut unresolved = Vec::new(); + for (_, w1, w2) in &gate.mul_terms { + if !self.solvable_witness.contains(w1) { + unresolved.push(w1); + if !self.solvable_witness.contains(w2) { + return false; + } + } + if !self.solvable_witness.contains(w2) { + unresolved.push(w2); + if !self.solvable_witness.contains(w1) { + return false; + } + } + } + for (_, w) in &gate.linear_combinations { + if !self.solvable_witness.contains(w) { + unresolved.push(w); + } + } + if unresolved.len() == 1 { + self.solvable(*unresolved[0]); + } + unresolved.len() <= 1 + } + + /// Adds the witness to set of solvable witness + pub(crate) fn solvable(&mut self, witness: Witness) { + self.solvable_witness.insert(witness); } // Still missing dead witness optimization. // To do this, we will need the whole set of arithmetic gates // I think it can also be done before the local optimization seen here, as dead variables will come from the user pub(crate) fn transform( - &self, + &mut self, gate: Expression, intermediate_variables: &mut IndexMap, num_witness: &mut u32, @@ -45,6 +80,7 @@ impl CSatTransformer { let mut gate = self.partial_gate_scan_optimization(gate, intermediate_variables, num_witness); gate.sort(); + self.solvable_expression(&gate); gate } @@ -72,7 +108,7 @@ impl CSatTransformer { // We can no longer extract another full gate, hence the algorithm terminates. Creating two intermediate variables t and t2. // This stage of preprocessing does not guarantee that all polynomials can fit into a gate. It only guarantees that all full gates have been extracted from each polynomial fn full_gate_scan_optimization( - &self, + &mut self, mut gate: Expression, intermediate_variables: &mut IndexMap, num_witness: &mut u32, @@ -98,9 +134,15 @@ impl CSatTransformer { // This will be our new gate which will be equal to `self` except we will have intermediate variables that will be constrained to any // subset of the terms that can be represented as full gates let mut new_gate = Expression::default(); - - while !gate.mul_terms.is_empty() { - let pair = gate.mul_terms[0]; + let mut mul_term_remains = Vec::new(); + for pair in gate.mul_terms { + // We want to layout solvable intermediate variable, if we cannot solve one of the witness + // that means the intermediate gate will not be immediatly solvable + if !self.solvable_witness.contains(&pair.1) || !self.solvable_witness.contains(&pair.2) + { + mul_term_remains.push(pair); + continue; + } // Check if this pair is present in the simplified fan-in // We are assuming that the fan-in/fan-out has been simplified. @@ -153,17 +195,22 @@ impl CSatTransformer { } // Now we have used up 2 spaces in our arithmetic gate. The width now dictates, how many more we can add - let remaining_space = self.width - 2 - 1; // We minus 1 because we need an extra space to contain the intermediate variable - // Keep adding terms until we have no more left, or we reach the width - for _ in 0..remaining_space { + let mut remaining_space = self.width - 2 - 1; // We minus 1 because we need an extra space to contain the intermediate variable + // Keep adding terms until we have no more left, or we reach the width + let mut remaining_linear_terms = Vec::new(); + while remaining_space > 0 { if let Some(wire_term) = gate.linear_combinations.pop() { // Add this element into the new gate - intermediate_gate.linear_combinations.push(wire_term); + if self.solvable_witness.contains(&wire_term.1) { + intermediate_gate.linear_combinations.push(wire_term); + remaining_space -= 1; + } else { + remaining_linear_terms.push(wire_term); + } } else { - // No more elements left in the old gate, we could stop the whole function - // We could alternative let it keep going, as it will never reach this branch again since there are no more elements left - // XXX: Future optimization - // no_more_left = true + // No more usable elements left in the old gate + gate.linear_combinations = remaining_linear_terms; + break; } } // Constraint this intermediate_gate to be equal to the temp variable by adding it into the IndexMap @@ -179,12 +226,12 @@ impl CSatTransformer { ); // Add intermediate variable to the new gate instead of the full gate + self.solvable_witness.insert(inter_var.1); new_gate.linear_combinations.push(inter_var); } }; - // Remove this term as we are finished processing it - gate.mul_terms.remove(0); } + gate.mul_terms = mul_term_remains; // Add the rest of the elements back into the new_gate new_gate.mul_terms.extend(gate.mul_terms.clone()); @@ -283,24 +330,31 @@ impl CSatTransformer { } // 2. Create Intermediate variables for the multiplication gates + let mut mult_terms_remains = Vec::new(); for mul_term in gate.mul_terms.clone().into_iter() { - let mut intermediate_gate = Expression::default(); - - // Push mul term into the gate - intermediate_gate.mul_terms.push(mul_term); - // Get an intermediate variable which squashes the multiplication term - let inter_var = Self::get_or_create_intermediate_vars( - intermediate_variables, - intermediate_gate, - num_witness, - ); - - // Add intermediate variable as a part of the fan-in for the original gate - gate.linear_combinations.push(inter_var); + if self.solvable_witness.contains(&mul_term.1) + && self.solvable_witness.contains(&mul_term.2) + { + let mut intermediate_gate = Expression::default(); + + // Push mul term into the gate + intermediate_gate.mul_terms.push(mul_term); + // Get an intermediate variable which squashes the multiplication term + let inter_var = Self::get_or_create_intermediate_vars( + intermediate_variables, + intermediate_gate, + num_witness, + ); + + // Add intermediate variable as a part of the fan-in for the original gate + gate.linear_combinations.push(inter_var); + } else { + mult_terms_remains.push(mul_term); + } } // Remove all of the mul terms as we have intermediate variables to represent them now - gate.mul_terms.clear(); + gate.mul_terms = mult_terms_remains; // We now only have a polynomial with only fan-in/fan-out terms i.e. terms of the form Ax + By + Cd + ... // Lets create intermediate variables if all of them cannot fit into the width @@ -318,29 +372,38 @@ impl CSatTransformer { // Collect as many terms up to the given width-1 and constrain them to an intermediate variable let mut intermediate_gate = Expression::default(); - for _ in 0..(self.width - 1) { - match gate.linear_combinations.pop() { - Some(term) => { - intermediate_gate.linear_combinations.push(term); - } - None => { - break; // We can also do nothing here - } - }; - } - let inter_var = Self::get_or_create_intermediate_vars( - intermediate_variables, - intermediate_gate, - num_witness, - ); + let mut linear_term_remains = Vec::new(); - added.push(inter_var); + for term in gate.linear_combinations { + if self.solvable_witness.contains(&term.1) + && intermediate_gate.linear_combinations.len() < self.width - 1 + { + intermediate_gate.linear_combinations.push(term); + } else { + linear_term_remains.push(term); + } + } + gate.linear_combinations = linear_term_remains; + let not_full = intermediate_gate.linear_combinations.len() < self.width - 1; + if intermediate_gate.linear_combinations.len() > 1 { + let inter_var = Self::get_or_create_intermediate_vars( + intermediate_variables, + intermediate_gate, + num_witness, + ); + added.push(inter_var); + } + //intermediate gate is not full, but the gate still has too many terms + if not_full && gate.linear_combinations.len() > self.width { + dbg!(&gate.linear_combinations); + unreachable!("ICE - could not reduce the expresion"); + } } // Add back the intermediate variables to // keep consistency with the original equation. gate.linear_combinations.extend(added); - + dbg!("should stpr"); self.partial_gate_scan_optimization(gate, intermediate_variables, num_witness) } } @@ -368,7 +431,7 @@ fn simple_reduction_smoke_test() { let mut num_witness = 4; - let optimizer = CSatTransformer::new(3); + let mut optimizer = CSatTransformer::new(3); let got_optimized_gate_a = optimizer.transform(gate_a, &mut intermediate_variables, &mut num_witness); From 84cc8c72cae7b96e89c5495fc8b2b3a7daabc17e Mon Sep 17 00:00:00 2001 From: guipublic Date: Thu, 13 Jul 2023 08:54:21 +0000 Subject: [PATCH 12/28] intermediate vars are solvable by construction --- acvm/src/compiler/transformers/csat.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 0bfb317b7..a820d713e 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -315,7 +315,7 @@ impl CSatTransformer { // // Cases, a lot of mul terms, a lot of fan-in terms, 50/50 fn partial_gate_scan_optimization( - &self, + &mut self, mut gate: Expression, intermediate_variables: &mut IndexMap, num_witness: &mut u32, @@ -391,19 +391,18 @@ impl CSatTransformer { intermediate_gate, num_witness, ); + self.solvable(inter_var.1); added.push(inter_var); } //intermediate gate is not full, but the gate still has too many terms if not_full && gate.linear_combinations.len() > self.width { - dbg!(&gate.linear_combinations); - unreachable!("ICE - could not reduce the expresion"); + unreachable!("Could not reduce the expresion"); } } // Add back the intermediate variables to // keep consistency with the original equation. gate.linear_combinations.extend(added); - dbg!("should stpr"); self.partial_gate_scan_optimization(gate, intermediate_variables, num_witness) } } @@ -432,13 +431,16 @@ fn simple_reduction_smoke_test() { let mut num_witness = 4; let mut optimizer = CSatTransformer::new(3); + optimizer.solvable(b); + optimizer.solvable(c); + optimizer.solvable(d); let got_optimized_gate_a = optimizer.transform(gate_a, &mut intermediate_variables, &mut num_witness); // a = b + c + d => a - b - c - d = 0 // For width3, the result becomes: - // a - b + e = 0 - // - c - d - e = 0 + // a - d + e = 0 + // - c - b - e = 0 // // a - b + e = 0 let e = Witness(4); @@ -446,7 +448,7 @@ fn simple_reduction_smoke_test() { mul_terms: vec![], linear_combinations: vec![ (FieldElement::one(), a), - (-FieldElement::one(), b), + (-FieldElement::one(), d), (FieldElement::one(), e), ], q_c: FieldElement::zero(), @@ -455,10 +457,10 @@ fn simple_reduction_smoke_test() { assert_eq!(intermediate_variables.len(), 1); - // e = - c - d + // e = - c - b let expected_intermediate_gate = Expression { mul_terms: vec![], - linear_combinations: vec![(-FieldElement::one(), d), (-FieldElement::one(), c)], + linear_combinations: vec![(-FieldElement::one(), c), (-FieldElement::one(), b)], q_c: FieldElement::zero(), }; let (_, normalized_gate) = CSatTransformer::normalize(expected_intermediate_gate); From 0c9eca2552f6cd02c98a734b2b88d190d248c140 Mon Sep 17 00:00:00 2001 From: guipublic Date: Thu, 13 Jul 2023 12:55:40 +0000 Subject: [PATCH 13/28] add test case for setpwise reduction --- acvm/src/compiler/transformers/csat.rs | 39 ++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index a820d713e..da4c47226 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -467,3 +467,42 @@ fn simple_reduction_smoke_test() { assert!(intermediate_variables.contains_key(&normalized_gate)); assert_eq!(intermediate_variables[&normalized_gate].1, e); } + +#[test] +fn stepwise_reduction_test() { + let a = Witness(0); + let b = Witness(1); + let c = Witness(2); + let d = Witness(3); + let e = Witness(4); + + // a = b + c + d + e; + let gate_a = Expression { + mul_terms: vec![], + linear_combinations: vec![ + (-FieldElement::one(), a), + (FieldElement::one(), b), + (FieldElement::one(), c), + (FieldElement::one(), d), + (FieldElement::one(), e), + ], + q_c: FieldElement::zero(), + }; + + let mut intermediate_variables: IndexMap = IndexMap::new(); + + let mut num_witness = 4; + + let mut optimizer = CSatTransformer::new(3); + optimizer.solvable(a); + optimizer.solvable(c); + optimizer.solvable(d); + optimizer.solvable(e); + let got_optimized_gate_a = + optimizer.transform(gate_a, &mut intermediate_variables, &mut num_witness); + + let witnesses: Vec = + got_optimized_gate_a.linear_combinations.iter().map(|(_, w)| *w).collect(); + // Since b is not known, it cannot be put inside intermediate gates, so it must belong to the transformed gate. + assert!(witnesses.contains(&b)); +} From ab71112d0293f042a738d93583c308cb5618ce52 Mon Sep 17 00:00:00 2001 From: guipublic Date: Thu, 13 Jul 2023 17:07:02 +0000 Subject: [PATCH 14/28] add new intermediate var to solvable --- acvm/src/compiler/transformers/csat.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index da4c47226..014c5441e 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -226,7 +226,7 @@ impl CSatTransformer { ); // Add intermediate variable to the new gate instead of the full gate - self.solvable_witness.insert(inter_var.1); + self.solvable(inter_var.1); new_gate.linear_combinations.push(inter_var); } }; @@ -348,6 +348,7 @@ impl CSatTransformer { // Add intermediate variable as a part of the fan-in for the original gate gate.linear_combinations.push(inter_var); + self.solvable(inter_var.1); } else { mult_terms_remains.push(mul_term); } From 05a34c78cc94e59968905b000104491cba9c868c Mon Sep 17 00:00:00 2001 From: guipublic Date: Fri, 14 Jul 2023 08:44:40 +0000 Subject: [PATCH 15/28] Code review: add input witnesses to the circuit --- acir/src/circuit/mod.rs | 4 ++++ acvm/src/compiler/mod.rs | 7 +++---- acvm/src/compiler/optimizers/redundant_range.rs | 2 ++ acvm/src/compiler/transformers/fallback.rs | 1 + 4 files changed, 10 insertions(+), 4 deletions(-) diff --git a/acir/src/circuit/mod.rs b/acir/src/circuit/mod.rs index 22f140999..97087b3ba 100644 --- a/acir/src/circuit/mod.rs +++ b/acir/src/circuit/mod.rs @@ -25,6 +25,8 @@ pub struct Circuit { pub public_parameters: PublicInputs, /// The set of public inputs calculated within the circuit. pub return_values: PublicInputs, + /// Input witnesses (both private and public) to the circuit + pub inputs: Vec, } #[derive(Debug, Copy, Clone, PartialEq, Eq, Default)] @@ -158,6 +160,7 @@ mod tests { opcodes: vec![and_opcode(), range_opcode(), directive_opcode()], public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2), Witness(12)])), return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(4), Witness(12)])), + inputs: vec![Witness(4), Witness(12)], }; fn read_write(circuit: Circuit) -> (Circuit, Circuit) { @@ -186,6 +189,7 @@ mod tests { ], public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])), return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])), + inputs: vec![Witness(4), Witness(2)], }; let json = serde_json::to_string_pretty(&circuit).unwrap(); diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index 506b44e97..32a7fcb2a 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -26,7 +26,6 @@ pub enum CompileError { /// Applies [`ProofSystemCompiler`][crate::ProofSystemCompiler] specific optimizations to a [`Circuit`]. pub fn compile( acir: Circuit, - inputs: Vec, np_language: Language, is_opcode_supported: impl Fn(&Opcode) -> bool, simplifier: &CircuitSimplifier, @@ -66,8 +65,8 @@ pub fn compile( } crate::Language::PLONKCSat { width } => { let mut csat = CSatTransformer::new(*width); - for value in inputs { - csat.solvable(value); + for value in &acir.inputs { + csat.solvable(*value); } csat } @@ -204,7 +203,6 @@ pub fn compile( } let current_witness_index = next_witness_index - 1; - Ok(( Circuit { current_witness_index, @@ -212,6 +210,7 @@ pub fn compile( // The optimizer does not add new public inputs public_parameters: acir.public_parameters, return_values: acir.return_values, + inputs: acir.inputs, }, new_opcode_labels, )) diff --git a/acvm/src/compiler/optimizers/redundant_range.rs b/acvm/src/compiler/optimizers/redundant_range.rs index 62f149990..3d984d75a 100644 --- a/acvm/src/compiler/optimizers/redundant_range.rs +++ b/acvm/src/compiler/optimizers/redundant_range.rs @@ -114,6 +114,7 @@ impl RangeOptimizer { opcodes: optimized_opcodes, public_parameters: self.circuit.public_parameters, return_values: self.circuit.return_values, + inputs: self.circuit.inputs, }, new_order_list, ) @@ -165,6 +166,7 @@ mod tests { opcodes, public_parameters: PublicInputs::default(), return_values: PublicInputs::default(), + inputs: Vec::new(), } } diff --git a/acvm/src/compiler/transformers/fallback.rs b/acvm/src/compiler/transformers/fallback.rs index cebfa2119..da76648f6 100644 --- a/acvm/src/compiler/transformers/fallback.rs +++ b/acvm/src/compiler/transformers/fallback.rs @@ -69,6 +69,7 @@ impl FallbackTransformer { opcodes: acir_supported_opcodes, public_parameters: acir.public_parameters, return_values: acir.return_values, + inputs: acir.inputs, }, new_opcode_labels, )) From c6f37716a6f5d767951a0f1243f4b8400b929987 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 07:28:44 +0000 Subject: [PATCH 16/28] chore: replace `inputs` field to be more granular --- acir/src/circuit/mod.rs | 13 +++++++++---- acvm/src/compiler/mod.rs | 6 +++--- acvm/src/compiler/optimizers/redundant_range.rs | 6 ++++-- acvm/src/compiler/transformers/fallback.rs | 2 +- 4 files changed, 17 insertions(+), 10 deletions(-) diff --git a/acir/src/circuit/mod.rs b/acir/src/circuit/mod.rs index 97087b3ba..a33c32ad4 100644 --- a/acir/src/circuit/mod.rs +++ b/acir/src/circuit/mod.rs @@ -18,6 +18,8 @@ pub struct Circuit { pub current_witness_index: u32, pub opcodes: Vec, + /// The set of private inputs to the circuit. + pub private_parameters: BTreeSet, // ACIR distinguishes between the public inputs which are provided externally or calculated within the circuit and returned. // The elements of these sets may not be mutually exclusive, i.e. a parameter may be returned from the circuit. // All public inputs (parameters and return values) must be provided to the verifier at verification time. @@ -25,8 +27,6 @@ pub struct Circuit { pub public_parameters: PublicInputs, /// The set of public inputs calculated within the circuit. pub return_values: PublicInputs, - /// Input witnesses (both private and public) to the circuit - pub inputs: Vec, } #[derive(Debug, Copy, Clone, PartialEq, Eq, Default)] @@ -43,6 +43,11 @@ impl Circuit { self.current_witness_index + 1 } + /// Returns all witnesses which are required to execute the circuit successfully. + pub fn circuit_arguments(&self) -> BTreeSet { + self.private_parameters.union(&self.public_parameters.0).cloned().collect() + } + /// Returns all public inputs. This includes those provided as parameters to the circuit and those /// computed as return values. pub fn public_inputs(&self) -> PublicInputs { @@ -158,9 +163,9 @@ mod tests { let circuit = Circuit { current_witness_index: 5, opcodes: vec![and_opcode(), range_opcode(), directive_opcode()], + private_parameters: BTreeSet::new(), public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2), Witness(12)])), return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(4), Witness(12)])), - inputs: vec![Witness(4), Witness(12)], }; fn read_write(circuit: Circuit) -> (Circuit, Circuit) { @@ -187,9 +192,9 @@ mod tests { range_opcode(), and_opcode(), ], + private_parameters: BTreeSet::new(), public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])), return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])), - inputs: vec![Witness(4), Witness(2)], }; let json = serde_json::to_string_pretty(&circuit).unwrap(); diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index 32a7fcb2a..ab121a11d 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -65,8 +65,8 @@ pub fn compile( } crate::Language::PLONKCSat { width } => { let mut csat = CSatTransformer::new(*width); - for value in &acir.inputs { - csat.solvable(*value); + for value in acir.circuit_arguments() { + csat.solvable(value); } csat } @@ -208,9 +208,9 @@ pub fn compile( current_witness_index, opcodes: transformed_gates, // The optimizer does not add new public inputs + private_parameters: acir.private_parameters, public_parameters: acir.public_parameters, return_values: acir.return_values, - inputs: acir.inputs, }, new_opcode_labels, )) diff --git a/acvm/src/compiler/optimizers/redundant_range.rs b/acvm/src/compiler/optimizers/redundant_range.rs index 3d984d75a..c4feb8dac 100644 --- a/acvm/src/compiler/optimizers/redundant_range.rs +++ b/acvm/src/compiler/optimizers/redundant_range.rs @@ -112,9 +112,9 @@ impl RangeOptimizer { Circuit { current_witness_index: self.circuit.current_witness_index, opcodes: optimized_opcodes, + private_parameters: self.circuit.private_parameters, public_parameters: self.circuit.public_parameters, return_values: self.circuit.return_values, - inputs: self.circuit.inputs, }, new_order_list, ) @@ -140,6 +140,8 @@ fn extract_range_opcode(opcode: &Opcode) -> Option<(Witness, u32)> { #[cfg(test)] mod tests { + use std::collections::BTreeSet; + use crate::compiler::optimizers::redundant_range::{extract_range_opcode, RangeOptimizer}; use acir::{ circuit::{ @@ -164,9 +166,9 @@ mod tests { Circuit { current_witness_index: 1, opcodes, + private_parameters: BTreeSet::new(), public_parameters: PublicInputs::default(), return_values: PublicInputs::default(), - inputs: Vec::new(), } } diff --git a/acvm/src/compiler/transformers/fallback.rs b/acvm/src/compiler/transformers/fallback.rs index da76648f6..b471b75bd 100644 --- a/acvm/src/compiler/transformers/fallback.rs +++ b/acvm/src/compiler/transformers/fallback.rs @@ -67,9 +67,9 @@ impl FallbackTransformer { Circuit { current_witness_index: witness_idx, opcodes: acir_supported_opcodes, + private_parameters: acir.private_parameters, public_parameters: acir.public_parameters, return_values: acir.return_values, - inputs: acir.inputs, }, new_opcode_labels, )) From bef085744afd615bd648cb3c8a77d83d28ef6da8 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:16:38 +0000 Subject: [PATCH 17/28] chore: reserve capacity in vectors --- acvm/src/compiler/transformers/csat.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 014c5441e..7c6b532ee 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -134,7 +134,7 @@ impl CSatTransformer { // This will be our new gate which will be equal to `self` except we will have intermediate variables that will be constrained to any // subset of the terms that can be represented as full gates let mut new_gate = Expression::default(); - let mut mul_term_remains = Vec::new(); + let mut mul_term_remains = Vec::with_capacity(gate.mul_terms.len()); for pair in gate.mul_terms { // We want to layout solvable intermediate variable, if we cannot solve one of the witness // that means the intermediate gate will not be immediatly solvable @@ -197,7 +197,8 @@ impl CSatTransformer { // Now we have used up 2 spaces in our arithmetic gate. The width now dictates, how many more we can add let mut remaining_space = self.width - 2 - 1; // We minus 1 because we need an extra space to contain the intermediate variable // Keep adding terms until we have no more left, or we reach the width - let mut remaining_linear_terms = Vec::new(); + let mut remaining_linear_terms = + Vec::with_capacity(gate.linear_combinations.len()); while remaining_space > 0 { if let Some(wire_term) = gate.linear_combinations.pop() { // Add this element into the new gate From 359c39bc64d4382f3a0a76efd64666d09f0ba8cd Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:17:49 +0000 Subject: [PATCH 18/28] chore: remove debug statement --- acvm/src/compiler/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index ab121a11d..21f1fb2a3 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -158,7 +158,6 @@ pub fn compile( transformed_gates.push(opcode.clone()); } Opcode::Directive(directive) => { - dbg!(&directive); match directive { Directive::Invert { result, .. } => { transformer.solvable(*result); From b9d5c394f92bd88a4f13dc21bd1efa49feba7753 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:20:05 +0000 Subject: [PATCH 19/28] chore: `solvable` -> `mark_solvable` --- acvm/src/compiler/mod.rs | 26 +++++++++++++------------- acvm/src/compiler/transformers/csat.rs | 24 ++++++++++++------------ 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index 21f1fb2a3..53afe492e 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -66,7 +66,7 @@ pub fn compile( crate::Language::PLONKCSat { width } => { let mut csat = CSatTransformer::new(*width); for value in acir.circuit_arguments() { - csat.solvable(value); + csat.mark_solvable(value); } csat } @@ -117,7 +117,7 @@ pub fn compile( match func { acir::circuit::opcodes::BlackBoxFuncCall::AND { output, .. } | acir::circuit::opcodes::BlackBoxFuncCall::XOR { output, .. } => { - transformer.solvable(*output) + transformer.mark_solvable(*output) } acir::circuit::opcodes::BlackBoxFuncCall::RANGE { .. } => (), acir::circuit::opcodes::BlackBoxFuncCall::SHA256 { outputs, .. } @@ -132,7 +132,7 @@ pub fn compile( } | acir::circuit::opcodes::BlackBoxFuncCall::Blake2s { outputs, .. } => { for witness in outputs { - transformer.solvable(*witness); + transformer.mark_solvable(*witness); } } acir::circuit::opcodes::BlackBoxFuncCall::FixedBaseScalarMul { @@ -140,8 +140,8 @@ pub fn compile( .. } | acir::circuit::opcodes::BlackBoxFuncCall::Pedersen { outputs, .. } => { - transformer.solvable(outputs.0); - transformer.solvable(outputs.1) + transformer.mark_solvable(outputs.0); + transformer.mark_solvable(outputs.1) } acir::circuit::opcodes::BlackBoxFuncCall::HashToField128Security { output, @@ -150,7 +150,7 @@ pub fn compile( | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256k1 { output, .. } | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256r1 { output, .. } | acir::circuit::opcodes::BlackBoxFuncCall::SchnorrVerify { output, .. } => { - transformer.solvable(*output) + transformer.mark_solvable(*output) } } @@ -160,20 +160,20 @@ pub fn compile( Opcode::Directive(directive) => { match directive { Directive::Invert { result, .. } => { - transformer.solvable(*result); + transformer.mark_solvable(*result); } Directive::Quotient(quotient_directive) => { - transformer.solvable(quotient_directive.q); - transformer.solvable(quotient_directive.r); + transformer.mark_solvable(quotient_directive.q); + transformer.mark_solvable(quotient_directive.r); } Directive::ToLeRadix { b, .. } => { for w in b { - transformer.solvable(*w); + transformer.mark_solvable(*w); } } Directive::PermutationSort { bits, .. } => { for w in bits { - transformer.solvable(*w); + transformer.mark_solvable(*w); } } Directive::Log(_) => (), @@ -187,10 +187,10 @@ pub fn compile( Opcode::Brillig(brillig) => { for output in &brillig.outputs { match output { - BrilligOutputs::Simple(w) => transformer.solvable(*w), + BrilligOutputs::Simple(w) => transformer.mark_solvable(*w), BrilligOutputs::Array(v) => { for w in v { - transformer.solvable(*w); + transformer.mark_solvable(*w); } } } diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 7c6b532ee..64efd55c2 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -52,13 +52,13 @@ impl CSatTransformer { } } if unresolved.len() == 1 { - self.solvable(*unresolved[0]); + self.mark_solvable(*unresolved[0]); } unresolved.len() <= 1 } /// Adds the witness to set of solvable witness - pub(crate) fn solvable(&mut self, witness: Witness) { + pub(crate) fn mark_solvable(&mut self, witness: Witness) { self.solvable_witness.insert(witness); } @@ -227,7 +227,7 @@ impl CSatTransformer { ); // Add intermediate variable to the new gate instead of the full gate - self.solvable(inter_var.1); + self.mark_solvable(inter_var.1); new_gate.linear_combinations.push(inter_var); } }; @@ -349,7 +349,7 @@ impl CSatTransformer { // Add intermediate variable as a part of the fan-in for the original gate gate.linear_combinations.push(inter_var); - self.solvable(inter_var.1); + self.mark_solvable(inter_var.1); } else { mult_terms_remains.push(mul_term); } @@ -393,7 +393,7 @@ impl CSatTransformer { intermediate_gate, num_witness, ); - self.solvable(inter_var.1); + self.mark_solvable(inter_var.1); added.push(inter_var); } //intermediate gate is not full, but the gate still has too many terms @@ -433,9 +433,9 @@ fn simple_reduction_smoke_test() { let mut num_witness = 4; let mut optimizer = CSatTransformer::new(3); - optimizer.solvable(b); - optimizer.solvable(c); - optimizer.solvable(d); + optimizer.mark_solvable(b); + optimizer.mark_solvable(c); + optimizer.mark_solvable(d); let got_optimized_gate_a = optimizer.transform(gate_a, &mut intermediate_variables, &mut num_witness); @@ -496,10 +496,10 @@ fn stepwise_reduction_test() { let mut num_witness = 4; let mut optimizer = CSatTransformer::new(3); - optimizer.solvable(a); - optimizer.solvable(c); - optimizer.solvable(d); - optimizer.solvable(e); + optimizer.mark_solvable(a); + optimizer.mark_solvable(c); + optimizer.mark_solvable(d); + optimizer.mark_solvable(e); let got_optimized_gate_a = optimizer.transform(gate_a, &mut intermediate_variables, &mut num_witness); From 6b07ec817da565572ea2659b029e2ed3694957bc Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:28:58 +0000 Subject: [PATCH 20/28] chore: standardise naming --- acvm/src/compiler/transformers/csat.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 64efd55c2..371a6ba55 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -331,7 +331,7 @@ impl CSatTransformer { } // 2. Create Intermediate variables for the multiplication gates - let mut mult_terms_remains = Vec::new(); + let mut remaining_mul_terms = Vec::new(); for mul_term in gate.mul_terms.clone().into_iter() { if self.solvable_witness.contains(&mul_term.1) && self.solvable_witness.contains(&mul_term.2) @@ -351,12 +351,12 @@ impl CSatTransformer { gate.linear_combinations.push(inter_var); self.mark_solvable(inter_var.1); } else { - mult_terms_remains.push(mul_term); + remaining_mul_terms.push(mul_term); } } // Remove all of the mul terms as we have intermediate variables to represent them now - gate.mul_terms = mult_terms_remains; + gate.mul_terms = remaining_mul_terms; // We now only have a polynomial with only fan-in/fan-out terms i.e. terms of the form Ax + By + Cd + ... // Lets create intermediate variables if all of them cannot fit into the width From f793fa9f2eb69dfdd1c6f0af7670532723e6081d Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:29:49 +0000 Subject: [PATCH 21/28] chore: reserve capacity in `remaining_mul_terms` --- acvm/src/compiler/transformers/csat.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 371a6ba55..66c5dd047 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -331,7 +331,7 @@ impl CSatTransformer { } // 2. Create Intermediate variables for the multiplication gates - let mut remaining_mul_terms = Vec::new(); + let mut remaining_mul_terms = Vec::with_capacity(gate.mul_terms.len()); for mul_term in gate.mul_terms.clone().into_iter() { if self.solvable_witness.contains(&mul_term.1) && self.solvable_witness.contains(&mul_term.2) From b44fa78d6917a0ba4ac877d72193c231fb1f1b62 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:30:56 +0000 Subject: [PATCH 22/28] chore: more naming standardisation --- acvm/src/compiler/transformers/csat.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 66c5dd047..e44eeac96 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -134,13 +134,13 @@ impl CSatTransformer { // This will be our new gate which will be equal to `self` except we will have intermediate variables that will be constrained to any // subset of the terms that can be represented as full gates let mut new_gate = Expression::default(); - let mut mul_term_remains = Vec::with_capacity(gate.mul_terms.len()); + let mut remaining_mul_terms = Vec::with_capacity(gate.mul_terms.len()); for pair in gate.mul_terms { // We want to layout solvable intermediate variable, if we cannot solve one of the witness // that means the intermediate gate will not be immediatly solvable if !self.solvable_witness.contains(&pair.1) || !self.solvable_witness.contains(&pair.2) { - mul_term_remains.push(pair); + remaining_mul_terms.push(pair); continue; } @@ -232,7 +232,7 @@ impl CSatTransformer { } }; } - gate.mul_terms = mul_term_remains; + gate.mul_terms = remaining_mul_terms; // Add the rest of the elements back into the new_gate new_gate.mul_terms.extend(gate.mul_terms.clone()); From 9863103e300e513d1f5acc1c86e2788ee29d6f80 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:32:30 +0000 Subject: [PATCH 23/28] chore: more standardisation --- acvm/src/compiler/transformers/csat.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index e44eeac96..3d7987e01 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -374,7 +374,7 @@ impl CSatTransformer { // Collect as many terms up to the given width-1 and constrain them to an intermediate variable let mut intermediate_gate = Expression::default(); - let mut linear_term_remains = Vec::new(); + let mut remaining_linear_terms = Vec::with_capacity(gate.linear_combinations.len()); for term in gate.linear_combinations { if self.solvable_witness.contains(&term.1) @@ -382,10 +382,10 @@ impl CSatTransformer { { intermediate_gate.linear_combinations.push(term); } else { - linear_term_remains.push(term); + remaining_linear_terms.push(term); } } - gate.linear_combinations = linear_term_remains; + gate.linear_combinations = remaining_linear_terms; let not_full = intermediate_gate.linear_combinations.len() < self.width - 1; if intermediate_gate.linear_combinations.len() > 1 { let inter_var = Self::get_or_create_intermediate_vars( From 4d8d62f90de46f7b34fe09103dd938762f619392 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Mon, 17 Jul 2023 08:33:23 +0000 Subject: [PATCH 24/28] chore: spelling --- acvm/src/compiler/transformers/csat.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 3d7987e01..0ff2452fb 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -137,7 +137,7 @@ impl CSatTransformer { let mut remaining_mul_terms = Vec::with_capacity(gate.mul_terms.len()); for pair in gate.mul_terms { // We want to layout solvable intermediate variable, if we cannot solve one of the witness - // that means the intermediate gate will not be immediatly solvable + // that means the intermediate gate will not be immediately solvable if !self.solvable_witness.contains(&pair.1) || !self.solvable_witness.contains(&pair.2) { remaining_mul_terms.push(pair); From cf9597e6469e065dd45872ea122051c2a68bc554 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Mon, 17 Jul 2023 12:19:57 +0100 Subject: [PATCH 25/28] Apply suggestions from code review --- acvm/src/compiler/transformers/csat.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 0ff2452fb..8d4dd0851 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -396,9 +396,9 @@ impl CSatTransformer { self.mark_solvable(inter_var.1); added.push(inter_var); } - //intermediate gate is not full, but the gate still has too many terms + // The intermediate gate is not full, but the gate still has too many terms if not_full && gate.linear_combinations.len() > self.width { - unreachable!("Could not reduce the expresion"); + unreachable!("Could not reduce the expression"); } } From cb57394a0bf52365acce4693d4fccb5cba2f90c4 Mon Sep 17 00:00:00 2001 From: guipublic Date: Wed, 19 Jul 2023 12:39:57 +0000 Subject: [PATCH 26/28] Code review --- acvm/src/compiler/mod.rs | 6 +++--- acvm/src/compiler/transformers/csat.rs | 13 ++++++------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index 32a7fcb2a..b8e568d41 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -182,9 +182,9 @@ pub fn compile( new_opcode_labels.push(opcode_label[index]); transformed_gates.push(opcode.clone()); } - Opcode::Block(_) => todo!(), - Opcode::ROM(_) => todo!(), - Opcode::RAM(_) => todo!(), + Opcode::Block(_) | Opcode::ROM(_) | Opcode::RAM(_) => { + unimplemented!("Stepwise execution is not compatible with {}", opcode.name()) + } Opcode::Brillig(brillig) => { for output in &brillig.outputs { match output { diff --git a/acvm/src/compiler/transformers/csat.rs b/acvm/src/compiler/transformers/csat.rs index 014c5441e..54499aa8a 100644 --- a/acvm/src/compiler/transformers/csat.rs +++ b/acvm/src/compiler/transformers/csat.rs @@ -29,20 +29,20 @@ impl CSatTransformer { CSatTransformer { width, solvable_witness: HashSet::new() } } - /// Returns true if the equation 'expression=0' can be solved, and add the solved witness to set of solvable witness - fn solvable_expression(&mut self, gate: &Expression) -> bool { + /// Check if the equation 'expression=0' can be solved, and if yes, add the solved witness to set of solvable witness + fn try_solve(&mut self, gate: &Expression) { let mut unresolved = Vec::new(); for (_, w1, w2) in &gate.mul_terms { if !self.solvable_witness.contains(w1) { unresolved.push(w1); if !self.solvable_witness.contains(w2) { - return false; + return; } } if !self.solvable_witness.contains(w2) { unresolved.push(w2); if !self.solvable_witness.contains(w1) { - return false; + return; } } } @@ -54,7 +54,6 @@ impl CSatTransformer { if unresolved.len() == 1 { self.solvable(*unresolved[0]); } - unresolved.len() <= 1 } /// Adds the witness to set of solvable witness @@ -80,7 +79,7 @@ impl CSatTransformer { let mut gate = self.partial_gate_scan_optimization(gate, intermediate_variables, num_witness); gate.sort(); - self.solvable_expression(&gate); + self.try_solve(&gate); gate } @@ -354,7 +353,7 @@ impl CSatTransformer { } } - // Remove all of the mul terms as we have intermediate variables to represent them now + // Remove the mul terms which are represented by intermediate variables gate.mul_terms = mult_terms_remains; // We now only have a polynomial with only fan-in/fan-out terms i.e. terms of the form Ax + By + Cd + ... From 58d39718427058562e6be53284cc72daff48f679 Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Tue, 25 Jul 2023 05:22:20 +0000 Subject: [PATCH 27/28] chore: clippy --- acvm/src/compiler/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index c8b6abdad..c68b0cd91 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -185,7 +185,6 @@ pub fn compile( } Opcode::MemoryInit { .. } => { // `MemoryInit` does not write values to the `WitnessMap` - () } Opcode::MemoryOp { op, .. } => { for (_, w1, w2) in &op.value.mul_terms { From bd7cd3a7da50fc78a3a89345354478c75709f54a Mon Sep 17 00:00:00 2001 From: TomAFrench Date: Tue, 25 Jul 2023 05:50:33 +0000 Subject: [PATCH 28/28] chore: `value` -> `index` --- acvm/src/compiler/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/acvm/src/compiler/mod.rs b/acvm/src/compiler/mod.rs index c68b0cd91..b8111479a 100644 --- a/acvm/src/compiler/mod.rs +++ b/acvm/src/compiler/mod.rs @@ -187,11 +187,11 @@ pub fn compile( // `MemoryInit` does not write values to the `WitnessMap` } Opcode::MemoryOp { op, .. } => { - for (_, w1, w2) in &op.value.mul_terms { + for (_, w1, w2) in &op.index.mul_terms { transformer.mark_solvable(*w1); transformer.mark_solvable(*w2); } - for (_, w) in &op.value.linear_combinations { + for (_, w) in &op.index.linear_combinations { transformer.mark_solvable(*w); } }