Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion acvm-repo/acvm/src/compiler/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ pub struct AcirTransformationMap {

impl AcirTransformationMap {
/// Builds a map from a vector of pointers to the old acir opcodes.
/// The index of the vector is the new opcode index.
/// The index in the vector is the new opcode index.
/// The value of the vector is the old opcode index pointed.
fn new(acir_opcode_positions: &[usize]) -> Self {
let mut old_indices_to_new_indices = HashMap::with_capacity(acir_opcode_positions.len());
Expand All @@ -36,6 +36,7 @@ impl AcirTransformationMap {
AcirTransformationMap { old_indices_to_new_indices }
}

/// Returns the new opcode location(s) corresponding to the old opcode.
pub fn new_locations(
&self,
old_location: OpcodeLocation,
Expand All @@ -58,6 +59,7 @@ impl AcirTransformationMap {
}
}

/// Update the assert messages to point to the new opcode locations.
fn transform_assert_messages<F: Clone>(
assert_messages: Vec<(OpcodeLocation, AssertionPayload<F>)>,
map: &AcirTransformationMap,
Expand Down
25 changes: 23 additions & 2 deletions acvm-repo/acvm/src/compiler/optimizers/merge_expressions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,26 @@ impl<F: AcirField> MergeExpressionsOptimizer<F> {
}
}
/// This pass analyzes the circuit and identifies intermediate variables that are
/// only used in two gates. It then merges the gate that produces the
/// only used in two arithmetic opcodes. It then merges the opcode which produces the
/// intermediate variable into the second one that uses it
/// Note: This pass is only relevant for backends that can handle unlimited width
///
/// The first pass maps witnesses to the index of the opcodes using them.
/// Public inputs are not considered because they cannot be simplified.
/// Witnesses used by MemoryInit opcodes are put in a separate map and marked as used by a Brillig call
/// if the memory block is an input to the call.
///
/// The second pass looks for arithmetic opcodes having a witness which is only used by another arithmetic opcode.
/// In that case, the opcode with the smallest index is merged into the other one via Gaussian elimination.
/// For instance, if we have '_1' used only by these two opcodes,
/// where `_{value}` refers to a witness and `{value}` refers to a constant:
/// [(1, _2,_3), (2, _2), (2, _1), (1, _3)]
/// [(2, _3, _4), (2,_1), (1, _4)]
/// We will remove the first one and modify the second one like this:
/// [(2, _3, _4), (1, _4), (-1, _2), (-1/2, _3), (-1/2, _2, _3)]
///
/// This transformation is relevant for Plonk-ish backends although they have a limited width because
/// they can potentially handle expressions with large linear combinations using 'big-add' gates.
pub(crate) fn eliminate_intermediate_variable(
&mut self,
circuit: &Circuit<F>,
Expand Down Expand Up @@ -183,7 +200,7 @@ impl<F: AcirField> MergeExpressionsOptimizer<F> {
witnesses
}
Opcode::MemoryOp { block_id: _, op, predicate } => {
//index et value, et predicate
//index, value, and predicate
let mut witnesses = CircuitSimulator::expr_wit(&op.index);
witnesses.extend(CircuitSimulator::expr_wit(&op.value));
if let Some(p) = predicate {
Expand Down Expand Up @@ -248,6 +265,10 @@ impl<F: AcirField> MergeExpressionsOptimizer<F> {
None
}

/// Returns the 'updated' opcode at index 'g' in the circuit
/// The modifications to the circuits are stored with 'deleted_gates' and 'modified_gates'
/// These structures are used to give the 'updated' opcode.
/// For instance, if the opcode has been deleted inside 'deleted_gates', then it returns None.
fn get_opcode(&self, g: usize, circuit: &Circuit<F>) -> Option<Opcode<F>> {
if self.deleted_gates.contains(&g) {
return None;
Expand Down
3 changes: 3 additions & 0 deletions acvm-repo/acvm/src/compiler/optimizers/unused_memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@ use acir::{
use std::collections::HashSet;

/// `UnusedMemoryOptimizer` will remove initializations of memory blocks which are unused.
/// A first pass collects all memory blocks which are initialized but discards the ones
/// which are used in a MemoryOp or as input to a BrilligCall.
/// The second pass removes the opcodes tagged as unused by the first pass.
pub(crate) struct UnusedMemoryOptimizer<F: AcirField> {
unused_memory_initializations: HashSet<BlockId>,
circuit: Circuit<F>,
Expand Down
8 changes: 5 additions & 3 deletions acvm-repo/acvm/src/compiler/transformers/csat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,9 +66,11 @@
self.solvable_witness.insert(witness);
}

// Still missing dead witness optimization.
// To do this, we will need the whole set of assert-zero opcodes
// I think it can also be done before the local optimization seen here, as dead variables will come from the user
/// Transform the input arithmetic expression into a new one having the correct 'width'
/// by creating intermediate variables as needed.
/// Having the correct width means:
/// - it has at most one multiplicative term
/// - it uses at most 'width-1' witness linear combination terms, to account for the new intermediate variable
pub(crate) fn transform<F: AcirField>(
&mut self,
opcode: Expression<F>,
Expand All @@ -92,7 +94,7 @@
// This optimization will search for combinations of terms which can be represented in a single assert-zero opcode
// Case 1 : qM * wL * wR + qL * wL + qR * wR + qO * wO + qC
// This polynomial does not require any further optimizations, it can be safely represented in one opcode
// ie a polynomial with 1 mul(bi-variate) term and 3 (univariate) terms where 2 of those terms match the bivariate term

Check warning on line 97 in acvm-repo/acvm/src/compiler/transformers/csat.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (bivariate)
// wL and wR, we can represent it in one opcode
// GENERALIZED for WIDTH: instead of the number 3, we use `WIDTH`
//
Expand Down
20 changes: 16 additions & 4 deletions acvm-repo/acvm/src/compiler/transformers/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,15 @@ pub(super) fn transform_internal<F: AcirField>(
///
/// Accepts an injected `acir_opcode_positions` to allow transformations to be applied directly after optimizations.
///
/// Does a single optimization pass.
/// If the width is unbounded, it does nothing.
/// If it is bounded, it first performs the 'CSAT transformation' in one pass, by creating intermediate variables when necessary.
/// This results in arithmetic opcodes having the required width.
/// Then the 'eliminate intermediate variables' pass will remove any intermediate variables (for instance created by the previous transformation)
/// that are used in exactly two arithmetic opcodes.
/// This results in arithmetic opcodes having linear combinations of potentially large width.
/// Finally, the 'range optimization' pass will remove any redundant range opcodes.
/// The backend is expected to handle linear combinations of 'unbounded width' in a more efficient way
/// than the 'CSAT transformation'.
#[tracing::instrument(
level = "trace",
name = "transform_acir_once",
Expand All @@ -102,6 +110,7 @@ fn transform_internal_once<F: AcirField>(
expression_width: ExpressionWidth,
acir_opcode_positions: Vec<usize>,
) -> (Circuit<F>, Vec<usize>) {
// If the expression width is unbounded, we don't need to do anything.
let mut transformer = match &expression_width {
ExpressionWidth::Unbounded => {
return (acir, acir_opcode_positions);
Expand All @@ -115,9 +124,10 @@ fn transform_internal_once<F: AcirField>(
}
};

// TODO: the code below is only for CSAT transformer
// TODO it may be possible to refactor it in a way that we do not need to return early from the r1cs
// TODO or at the very least, we could put all of it inside of CSatOptimizer pass
// 1. CSAT transformation
// Process each opcode in the circuit by marking the solvable witnesses and transforming the AssertZero opcodes
// to the required width by creating intermediate variables.
// Knowing if a witness is solvable avoids creating un-solvable intermediate variables.

let mut new_acir_opcode_positions: Vec<usize> = Vec::with_capacity(acir_opcode_positions.len());
// Optimize the assert-zero gates by reducing them into the correct width and
Expand Down Expand Up @@ -216,6 +226,7 @@ fn transform_internal_once<F: AcirField>(
..acir
};

// 2. Eliminate intermediate variables, when they are used in exactly two arithmetic opcodes.
let mut merge_optimizer = MergeExpressionsOptimizer::new();

let (opcodes, new_acir_opcode_positions) =
Expand All @@ -228,6 +239,7 @@ fn transform_internal_once<F: AcirField>(
..acir
};

// 3. Remove redundant range constraints.
// The `MergeOptimizer` can merge two witnesses which have range opcodes applied to them
// so we run the `RangeOptimizer` afterwards to clear these up.
let range_optimizer = RangeOptimizer::new(acir);
Expand Down
34 changes: 29 additions & 5 deletions acvm-repo/acvm/src/pwg/arithmetic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,17 @@ pub(crate) enum MulTerm<F> {
}

impl ExpressionSolver {
/// Derives the rest of the witness based on the initial low level variables
/// Derives the rest of the witness in the provided expression based on the known witness values
/// 1. Fist we simplify the expression based on the known values and try to reduce the multiplication and linear terms
/// 2. If we end up with only the constant term;
/// - if it is 0 then the opcode is solved, if not,
/// - the assert_zero opcode is not satisfied and we return an error
/// 3. If we end up with only linear terms on the same witness 'w',
/// we can regroup them and solve 'a*w+c = 0':
/// If 'a' is zero in the above expression;
/// - if c is also 0 then the opcode is solved
/// - if not that means the assert_zero opcode is not satisfied and we return an error
/// If 'a' is not zero, we can solve it by setting the value of w: 'w = -c/a'
pub(crate) fn solve<F: AcirField>(
initial_witness: &mut WitnessMap<F>,
opcode: &Expression<F>,
Expand Down Expand Up @@ -129,10 +139,11 @@ impl ExpressionSolver {
}
}

/// Returns the evaluation of the multiplication term in the expression
/// If the witness values are not known, then the function returns a None
/// XXX: Do we need to account for the case where 5xy + 6x = 0 ? We do not know y, but it can be solved given x . But I believe x can be solved with another opcode
/// XXX: What about making a mul opcode = a constant 5xy + 7 = 0 ? This is the same as the above.
/// Try to reduce the multiplication terms of the given expression to a known value or to a linear term,
/// using the provided witness mapping.
/// If there are 2 or more multiplication terms it returns the OpcodeUnsolvable error.
/// If no witnesses value is in the provided 'witness_assignments' map,
/// it returns MulTerm::TooManyUnknowns
fn solve_mul_term<F: AcirField>(
arith_opcode: &Expression<F>,
witness_assignments: &WitnessMap<F>,
Expand All @@ -149,6 +160,11 @@ impl ExpressionSolver {
}
}

/// Try to solve a multiplication term of the form q*a*b, where
/// q is a constant and a,b are witnesses
/// If both a and b have known values (in the provided map), it returns the value q*a*b
/// If only one of a or b has a known value, it returns the linear term c*w where c is a constant and w is the unknown witness
/// If both a and b are unknown, it returns MulTerm::TooManyUnknowns
fn solve_mul_term_helper<F: AcirField>(
term: &(F, Witness, Witness),
witness_assignments: &WitnessMap<F>,
Expand All @@ -166,6 +182,8 @@ impl ExpressionSolver {
}
}

/// Reduce a linear term to its value if the witness assignment is known
/// If the witness value is not known in the provided map, it returns None.
fn solve_fan_in_term_helper<F: AcirField>(
term: &(F, Witness),
witness_assignments: &WitnessMap<F>,
Expand Down Expand Up @@ -215,6 +233,12 @@ impl ExpressionSolver {
}

// Partially evaluate the opcode using the known witnesses
// For instance if values of witness 'a' and 'b' are known, then
// the multiplication 'a*b' is removed and their multiplied values are added to the constant term
// If only witness 'a' is known, then the multiplication 'a*b' is replaced by the linear term '(value of b)*a'
// etc ...
// If all values are known, the partial evaluation gives a constant expression
// If no value is known, the partial evaluation returns the original expression
pub(crate) fn evaluate<F: AcirField>(
expr: &Expression<F>,
initial_witness: &WitnessMap<F>,
Expand Down
13 changes: 13 additions & 0 deletions acvm-repo/acvm/src/pwg/blackbox/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
use hash::{solve_generic_256_hash_opcode, solve_sha_256_permutation_opcode};
use logic::{and, xor};
pub(crate) use range::solve_range_opcode;
use signature::ecdsa::{secp256k1_prehashed, secp256r1_prehashed};

Check warning on line 30 in acvm-repo/acvm/src/pwg/blackbox/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (prehashed)

Check warning on line 30 in acvm-repo/acvm/src/pwg/blackbox/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (prehashed)

/// Check if all of the inputs to the function have assignments
///
Expand All @@ -53,6 +53,19 @@
first_missing_assignment(witness_assignments, inputs).is_none()
}

/// Solve a black box function call
/// 1. Returns an error if not all the inputs are already resolved to a value
/// 2. Compute the output from the inputs, using the dedicated solvers
///
/// A blackbox is a fully specified function (e.g sha256, ecdsa signature,...)
/// which the backend can prove execution in a more efficient way than using a generic
/// arithmetic circuit.
/// Solving a black box function simply means to compute the output from the inputs for
/// the specific function.
/// Our black box solver uses the standard rust implementation for the function if it is available.
/// However, some functions depend on the backend, such as embedded curve operations, which depend on the
/// elliptic curve used by the proving system. This is why the 'solve' functions takes a blackbox solver trait.
/// The 'AcvmBigIntSolver' is also a blackbox solver, but dedicated to the BigInteger blackbox functions.
pub(crate) fn solve<F: AcirField>(
backend: &impl BlackBoxFunctionSolver<F>,
initial_witness: &mut WitnessMap<F>,
Expand Down Expand Up @@ -108,7 +121,7 @@
signature,
hashed_message: message,
output,
} => secp256k1_prehashed(

Check warning on line 124 in acvm-repo/acvm/src/pwg/blackbox/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (prehashed)
initial_witness,
public_key_x,
public_key_y,
Expand All @@ -122,7 +135,7 @@
signature,
hashed_message: message,
output,
} => secp256r1_prehashed(

Check warning on line 138 in acvm-repo/acvm/src/pwg/blackbox/mod.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (prehashed)
initial_witness,
public_key_x,
public_key_y,
Expand Down
17 changes: 12 additions & 5 deletions acvm-repo/acvm/src/pwg/brillig.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ pub enum BrilligSolverStatus<F> {
ForeignCallWait(ForeignCallWaitInfo<F>),
}

/// Specific solver for Brillig opcodes
/// It maintains a Brillig VM that can execute the bytecode of the called brillig function
pub struct BrilligSolver<'b, F, B: BlackBoxFunctionSolver<F>> {
vm: VM<'b, F, B>,
acir_index: usize,
Expand Down Expand Up @@ -86,6 +88,9 @@ impl<'b, B: BlackBoxFunctionSolver<F>, F: AcirField> BrilligSolver<'b, F, B> {
Ok(Self { vm, acir_index, function_id: brillig_function_id })
}

/// Get a BrilligVM for executing the provided bytecode
/// 1. Reduce the input expressions into a known value, or error if they do not reduce to a value.
/// 2. Instantiate the Brillig VM with the bytecode and the reduced inputs.
fn setup_brillig_vm(
initial_witness: &WitnessMap<F>,
memory: &HashMap<BlockId, MemoryOpSolver<F>>,
Expand Down Expand Up @@ -181,14 +186,14 @@ impl<'b, B: BlackBoxFunctionSolver<F>, F: AcirField> BrilligSolver<'b, F, B> {
self.vm.program_counter()
}

/// Returns the status of the Brillig VM as a 'BrilligSolverStatus' resolution.
/// It may be finished, in-progress, failed, or may be waiting for results of a foreign call.
/// Return the "resolution" to the caller who may choose to make subsequent calls
/// (when it gets foreign call results for example).
fn handle_vm_status(
&self,
vm_status: VMStatus<F>,
) -> Result<BrilligSolverStatus<F>, OpcodeResolutionError<F>> {
// Check the status of the Brillig VM and return a resolution.
// It may be finished, in-progress, failed, or may be waiting for results of a foreign call.
// Return the "resolution" to the caller who may choose to make subsequent calls
// (when it gets foreign call results for example).
match vm_status {
VMStatus::Finished { .. } => Ok(BrilligSolverStatus::Finished),
VMStatus::InProgress => Ok(BrilligSolverStatus::InProgress),
Expand Down Expand Up @@ -234,6 +239,7 @@ impl<'b, B: BlackBoxFunctionSolver<F>, F: AcirField> BrilligSolver<'b, F, B> {
self.finalize_inner(witness, outputs)
}

/// Finalize the VM and return the profiling samples.
pub(crate) fn finalize_with_profiling(
mut self,
witness: &mut WitnessMap<F>,
Expand All @@ -244,6 +250,7 @@ impl<'b, B: BlackBoxFunctionSolver<F>, F: AcirField> BrilligSolver<'b, F, B> {
Ok(self.vm.take_profiling_samples())
}

/// Finalize the VM execution and write the outputs to the provided witness map.
fn finalize_inner(
&self,
witness: &mut WitnessMap<F>,
Expand All @@ -260,14 +267,14 @@ impl<'b, B: BlackBoxFunctionSolver<F>, F: AcirField> BrilligSolver<'b, F, B> {
}
}

/// Write VM execution results into the witness map
fn write_brillig_outputs(
&self,
witness_map: &mut WitnessMap<F>,
return_data_offset: usize,
return_data_size: usize,
outputs: &[BrilligOutputs],
) -> Result<(), OpcodeResolutionError<F>> {
// Write VM execution results into the witness map
let memory = self.vm.get_memory();
let mut current_ret_data_idx = return_data_offset;
for output in outputs.iter() {
Expand Down
27 changes: 27 additions & 0 deletions acvm-repo/acvm/src/pwg/memory_op.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,16 @@ type MemoryIndex = u32;
/// Maintains the state for solving [`MemoryInit`][`acir::circuit::Opcode::MemoryInit`] and [`MemoryOp`][`acir::circuit::Opcode::MemoryOp`] opcodes.
#[derive(Default)]
pub(crate) struct MemoryOpSolver<F> {
/// Known values of the memory block, based on the index
/// This map evolves as we process the opcodes
pub(super) block_value: HashMap<MemoryIndex, F>,
/// Length of the block, i.e the number of elements stored into the memory block.
pub(super) block_len: u32,
}

impl<F: AcirField> MemoryOpSolver<F> {
/// Convert a field element into a memory index
/// Only 32 bits values are valid memory indices
fn index_from_field(&self, index: F) -> Result<MemoryIndex, OpcodeResolutionError<F>> {
if index.num_bits() <= 32 {
let memory_index = index.try_to_u64().unwrap() as MemoryIndex;
Expand All @@ -34,6 +39,8 @@ impl<F: AcirField> MemoryOpSolver<F> {
}
}

/// Update the 'block_value' map with the provided index/value
/// Returns an 'IndexOutOfBounds' error if the index is outside the block range.
fn write_memory_index(
&mut self,
index: MemoryIndex,
Expand All @@ -50,6 +57,8 @@ impl<F: AcirField> MemoryOpSolver<F> {
Ok(())
}

/// Returns the value stored in the 'block_value' map for the provided index
/// Returns an 'IndexOutOfBounds' error if the index is not in the map.
fn read_memory_index(&self, index: MemoryIndex) -> Result<F, OpcodeResolutionError<F>> {
self.block_value.get(&index).copied().ok_or(OpcodeResolutionError::IndexOutOfBounds {
opcode_location: ErrorLocation::Unresolved,
Expand All @@ -74,6 +83,24 @@ impl<F: AcirField> MemoryOpSolver<F> {
Ok(())
}

/// Update the 'block_values' by processing the provided Memory opcode
/// The opcode 'op' contains the index and value of the operation and the type
/// of the operation.
/// They are all stored as an [Expression]
/// The type of 'operation' is '0' for a read and '1' for a write. It must be a constant
/// expression.
/// Index is not required to be constant but it must reduce to a known value
/// for processing the opcode. This is done by doing the (partial) evaluation of its expression,
/// using the provided witness map.
///
/// READ: read the block at index op.index and update op.value with the read value
/// - 'op.value' must reduce to a witness (after the evaluation of its expression)
/// - the value is updated in the provided witness map, for the 'op.value' witness
///
/// WRITE: update the block at index 'op.index' with 'op.value'
/// - 'op.value' must reduce to a known value
///
/// If a requirement is not met, it returns an error.
pub(crate) fn solve_memory_op(
&mut self,
op: &MemOp<F>,
Expand Down
Loading
Loading