Skip to content
Merged
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
152 changes: 152 additions & 0 deletions acvm-repo/acvm/src/pwg/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,98 @@
// Re-usable methods that backends can use to implement their PWG

//! This module contains methods to implement the partial witness generation (PWG) of an ACIR program.
//! The goal of ACIR execution is to compute the values of all the ACIR witnesses, or an error if it could not compute them all.
//! A proving system will then be able to use the ACIR circuit and the values of the ACIR witnesses to generate a proof of this execution.
//! The ACIR opcodes are not modified by the execution.
//! Witness generation means getting valid values for the witnesses used by the ACIR opcodes of the program.
//! They are called *partial* witness because a proving system may create additional witnesses on its own for
//! generating the proof (and a corresponding low-level circuit). The PWG generates values for all the witnesses
//! of the ACIR program, or returns an error if it cannot do it.
//!
//! Implementation details & examples:
//! It starts by instantiating an ACVM (ACIR Virtual Machine), which executes the given ACIR opcodes in the `solve()` function.
//!
//! Parameters: When instantiating the ACVM, it needs to be provided with:
//! - a `backend` implementing the `BlackBoxFunctionSolver` trait. Different implementation can be used depending on the EC used by the underlying proving system.
//! - `opcodes`: the ACIR opcodes of the program to solve.
//! - `initial_witness`: a mapping of initial witness values representing the inputs of the program. The ACVM will update this map as it solves the opcodes.
//! - `unconstrained_functions`: the Brillig bytecode of the unconstrained functions used by the program.
//! - `assertion_payloads`: additional information used to provide feedback to the user when an assertion fails.
//!
//! Returns: ACVM Status
//! - `Solved`: all witness have been sucessfully computed, execution is complete.

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

View workflow job for this annotation

GitHub Actions / Code

Misspelled word (sucessfully) Suggestions: (successfully*)
//! - `InProgress`: The ACVM is processing the circuit, i.e solving the opcodes. This status is used to resume execution after it has been paused.
//! - `Failure(OpcodeResolutionError<F>)`: Error, execution is stopped.
//! - `RequiresForeignCall(ForeignCallWaitInfo<F>)`: Execution is paused until the result of a foreign call is provided
//! - `RequiresAcirCall(AcirCallWaitInfo<F>)`: Execution is paused until the result of an ACIR call is provided
//!
//! Each opcode is solved independently. In general we require its inputs to be already known, i.e previoulsy solved,

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

View workflow job for this annotation

GitHub Actions / Code

Misspelled word (previoulsy) Suggestions: (previously*)
//! and the output is simply computed from the inputs, and then the output becomes 'known' for the subsequent opcodes.
//!
//! - AssertZero opcode: The arithmetic expression of the opcode is solved for one unknwon witness.

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

View workflow job for this annotation

GitHub Actions / Code

Misspelled word (unknwon) Suggestions: (unknown*)
//! It will fail if there is more than one unkwnown witness in the expression.

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

View workflow job for this annotation

GitHub Actions / Code

Unknown word (unkwnown)
//!
//! - BlackBoxFuncCall opcode: The blackbox module knows how to compute the result of the function when all its input are known.
//!
//! - MemoryInit opcode: Instantiate a MemoryOpSolver for the opcode's array, using the given initial values.
//! Initial witness values must be known. The memory values will be updated later by MemoryOp opcodes.
//!
//! - MemoryOp opcode: Update the memory values of the opcode's array from the opcode witness values:
//! A read operation will solve the corresponding witness value, reading the memory value tracked by the MemoryOpSolver at the (known value) of the opcode index.
//! A write operation will update the memory value tracked by the MemoryOpSolver using the known values of the opcode index/value witnesses.
//!
//! - BrilligCall opcode: Calls an unconstrained Brillig function by instantiating a BrilligSolver (i.e a Brillig VM).
//! If the function is a foreign call, the `solve()` will halt and wait for the caller to resolve the foreign call.
//!
//! - Call opcode: Execute the ACIR call in a separate ACVM instance. The result of the ACIR call will be passed back to the ACVM using a
//! mechanism similar to the one for foreign calls.
//!
//!
//!
//! Example:
// Compiled ACIR for main (non-transformed):
// func 0
// current witness: w9
// private parameters: [w0, w1, w2, w3, w4]
// public parameters: []
// return values: [w9]
// BLACKBOX::RANGE [w0]:32 bits []
// BLACKBOX::RANGE [w1]:32 bits []
// BLACKBOX::RANGE [w2]:32 bits []
// BLACKBOX::RANGE [w3]:32 bits []
// BLACKBOX::RANGE [w4]:32 bits []
// EXPR [ (1, w0) (-1, w1) (-1, w6) 0 ]
// BRILLIG CALL func 0: inputs: [EXPR [ (1, w6) 0 ]], outputs: [w7]
// EXPR [ (1, w6, w7) (1, w8) -1 ]
// EXPR [ (1, w6, w8) 0 ]
// EXPR [ (1, w1, w8) 0 ]
// EXPR [ (1, w0) (-1, w2) (-1, w9) 0 ]
//!
//! This ACIR program defines the 'main' function and indicates it is 'non-transformed'.
//! Indeed, some ACIR pass can transform the ACIR program in order to apply optimisations,

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

View workflow job for this annotation

GitHub Actions / Code

Unknown word (optimisations)
//! or to make it compatible with a specific proving system.
//! However, ACIR execution is expected to work on any ACIR program (transformed or not).
//! Then the program indicates the 'current witness', which is the lasted witness used in the program.
//! Any transformation that needs to add more witness will use it in order to not overlap with
//! existing witnesses. This is not relevant for execution.
//! Then we see the parameters of the program as public and private inputs.
//! The `initial_witness` needs to contain values for these parameters before execution, else
//! the execution will fail.
//! The first ACIR opcodes are RANGE opcodes which ensure the inputs have the expected range (as specified in the Noir source code).
//! Solving this black-box simply means to validate that the values (from `initial_witness`) are indeed 32 bits for w0, w1, w2, w3, w4
//! If `initial_witness` does not have values for w0, w1, w2, w3, w4, or if the values are over 32 bits, the execution will fail.
//! The next opcode is an AssertZero opcode: EXPR [ (1, w0) (-1, w1) (-1, w6) 0 ], which indicates that `w0 - w1 - w6` should be equal to 0.
//! Since we know the values of `w0, w1` from `initial_witness`, we can compute `w6 = w0 + w1` so that the AssertZero is satified.

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

View workflow job for this annotation

GitHub Actions / Code

Misspelled word (satified) Suggestions: (satisfied*)
//! Solving AssertZero means computing the unknown witness and adding the result to `initial_witness`, which now contains the value for `w6`.
//! The next opcode is a Brillig Call where input is `w6` and output is `w7`. From the function id of the opcode, the solver will retrieve the
//! corresponding Brillig bytecode and instantiate a Brillig VM with the value of the input. This value was just computed before.
//! Executing the Brillig VM on this input will give us the output which is the value for `w7`, that we add to `initial_witness`.
//! The next opcode is again an AssertZero: `w6 * w7 + w8 - 1 = 0`, which computes the value of `w8`.
//! The two next opcode are AssertZero without any unkwown witness: `w6 * w8 = 0` and `w1 * w8 = 0`

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

View workflow job for this annotation

GitHub Actions / Code

Misspelled word (unkwown) Suggestions: (unknown*)
//! Solving such opcodes means that we compute `w6 * w8 ` and `w1 * w8` using the known values, and check that it is 0.
//! If not, we would return an error.
//! Finally, the last AssertZero computes `w9` which is the last witness. All the witness have now been computed; execution is complete.

use std::collections::HashMap;

use acir::{
Expand Down Expand Up @@ -866,3 +959,62 @@
/// Initial witness for the given circuit to be called
pub initial_witness: WitnessMap<F>,
}

#[cfg(test)]
mod tests {
use std::collections::BTreeMap;

use acir::{
FieldElement,
circuit::{
Opcode,
opcodes::{BlackBoxFuncCall, FunctionInput},
},
native_types::{Witness, WitnessMap},
};

use crate::pwg::{ACVM, ACVMStatus};

#[test]
fn solve_simple_circuit() {
let initial_witness = WitnessMap::from(BTreeMap::from_iter([
(Witness(1), FieldElement::from(1u128)),
(Witness(2), FieldElement::from(1u128)),
(Witness(3), FieldElement::from(2u128)),
]));
let backend = acvm_blackbox_solver::StubbedBlackBoxSolver(false);
let opcodes = vec![
Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
input: FunctionInput::Witness(Witness(1)),
num_bits: 32,
}),
Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
input: FunctionInput::Witness(Witness(2)),
num_bits: 32,
}),
Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
input: FunctionInput::Witness(Witness(3)),
num_bits: 32,
}),
Opcode::AssertZero(acir::native_types::Expression {
mul_terms: vec![],
linear_combinations: vec![
(FieldElement::from(2u128), Witness(1)),
(FieldElement::from(-1_i128), Witness(2)),
(FieldElement::from(-1_i128), Witness(4)),
],
q_c: FieldElement::from(0u128),
}),
Opcode::AssertZero(acir::native_types::Expression {
mul_terms: vec![(FieldElement::from(1u128), Witness(2), Witness(4))],
linear_combinations: vec![(FieldElement::from(1u128), Witness(5))],
q_c: FieldElement::from(-1_i128),
}),
];
let empty1 = Vec::new();
let empty2 = Vec::new();
let mut acvm = ACVM::new(&backend, &opcodes, initial_witness, &empty1, &empty2);
assert_eq!(acvm.solve(), ACVMStatus::Solved);
assert_eq!(acvm.witness_map()[&Witness(5)], FieldElement::from(0u128));
}
}
Loading