diff --git a/acvm-repo/acvm/src/pwg/mod.rs b/acvm-repo/acvm/src/pwg/mod.rs index d492e638946..e9a29fc42f9 100644 --- a/acvm-repo/acvm/src/pwg/mod.rs +++ b/acvm-repo/acvm/src/pwg/mod.rs @@ -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. +//! - `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)`: Error, execution is stopped. +//! - `RequiresForeignCall(ForeignCallWaitInfo)`: Execution is paused until the result of a foreign call is provided +//! - `RequiresAcirCall(AcirCallWaitInfo)`: 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, +//! 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. +//! It will fail if there is more than one unkwnown witness in the expression. +//! +//! - 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, +//! 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. +//! 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` +//! 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::{ @@ -866,3 +959,62 @@ pub struct AcirCallWaitInfo { /// Initial witness for the given circuit to be called pub initial_witness: WitnessMap, } + +#[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)); + } +}