Skip to content
This repository has been archived by the owner on Apr 9, 2024. It is now read-only.

fix: solvable intermediate gates for csat #433

Merged
merged 36 commits into from
Jul 25, 2023
Merged
Show file tree
Hide file tree
Changes from 23 commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
d2e9c10
feat(acvm)!: replace `PartialWitnessGeneratorStatus` with `ACVMStatus`
TomAFrench Jul 5, 2023
85c3943
chore: add test that ACVM can be finalized when solved
TomAFrench Jul 5, 2023
cf084d6
chore: make cspell happy
TomAFrench Jul 5, 2023
c452d9d
chore: fix doc comment
TomAFrench Jul 5, 2023
925e84e
feat(acvm)!: Support stepwise execution of ACIR
TomAFrench Jun 21, 2023
5b0b3c8
chore: replace pattern match with equality check
TomAFrench Jul 5, 2023
0003221
Merge branch 'master' into linear-acvm
TomAFrench Jul 6, 2023
7811490
Merge branch 'acvm-status' into linear-acvm
TomAFrench Jul 6, 2023
835a49b
Merge branch 'master' into linear-acvm
TomAFrench Jul 9, 2023
66b2643
chore!: remove unnecessary brillig hashing
TomAFrench Jul 10, 2023
8b0c7b3
chore!: remove explicit tracking of `OpcodeLabel`s
TomAFrench Jul 10, 2023
d03818b
fix: set ACVM status to `Solved` if passed an empty circuit
TomAFrench Jul 10, 2023
9810b46
chore: remove sorting of opcodes in `acvm::compiler::compile`
TomAFrench Jul 10, 2023
e579fc2
Merge branch 'master' into linear-acvm
TomAFrench Jul 11, 2023
1dda0c5
csat generates solvable intermediate gates
guipublic Jul 12, 2023
84cc8c7
intermediate vars are solvable by construction
guipublic Jul 13, 2023
0c9eca2
add test case for setpwise reduction
guipublic Jul 13, 2023
ab71112
add new intermediate var to solvable
guipublic Jul 13, 2023
05a34c7
Code review: add input witnesses to the circuit
guipublic Jul 14, 2023
c6f3771
chore: replace `inputs` field to be more granular
TomAFrench Jul 17, 2023
bef0857
chore: reserve capacity in vectors
TomAFrench Jul 17, 2023
359c39b
chore: remove debug statement
TomAFrench Jul 17, 2023
b9d5c39
chore: `solvable` -> `mark_solvable`
TomAFrench Jul 17, 2023
6b07ec8
chore: standardise naming
TomAFrench Jul 17, 2023
f793fa9
chore: reserve capacity in `remaining_mul_terms`
TomAFrench Jul 17, 2023
b44fa78
chore: more naming standardisation
TomAFrench Jul 17, 2023
9863103
chore: more standardisation
TomAFrench Jul 17, 2023
4d8d62f
chore: spelling
TomAFrench Jul 17, 2023
81c95b3
Merge branch 'linear-acvm' into gd/linear-acvm
TomAFrench Jul 17, 2023
cf9597e
Apply suggestions from code review
TomAFrench Jul 17, 2023
2d784f5
Merge branch 'linear-acvm' into gd/linear-acvm
TomAFrench Jul 17, 2023
cb57394
Code review
guipublic Jul 19, 2023
e271989
Merge branch 'gd/linear-acvm' of https://github.com/noir-lang/acvm in…
guipublic Jul 19, 2023
bb4ad63
Merge branch 'linear-acvm' into gd/linear-acvm
TomAFrench Jul 25, 2023
58d3971
chore: clippy
TomAFrench Jul 25, 2023
bd7cd3a
chore: `value` -> `index`
TomAFrench Jul 25, 2023
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
1 change: 0 additions & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion acir/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
4 changes: 2 additions & 2 deletions acir/src/circuit/brillig.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@ 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<Expression>),
}

/// 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<Witness>),
Expand Down
9 changes: 9 additions & 0 deletions acir/src/circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ pub struct Circuit {
pub current_witness_index: u32,
pub opcodes: Vec<Opcode>,

/// The set of private inputs to the circuit.
pub private_parameters: BTreeSet<Witness>,
// 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.
Expand All @@ -41,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<Witness> {
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 {
Expand Down Expand Up @@ -156,6 +163,7 @@ 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)])),
};
Expand Down Expand Up @@ -184,6 +192,7 @@ 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)])),
};
Expand Down
1 change: 0 additions & 1 deletion acvm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
100 changes: 93 additions & 7 deletions acvm/src/compiler/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use acir::{
circuit::{Circuit, Opcode, OpcodeLabel},
circuit::{brillig::BrilligOutputs, directives::Directive, Circuit, Opcode, OpcodeLabel},
native_types::{Expression, Witness},
BlackBoxFunc, FieldElement,
};
Expand Down Expand Up @@ -58,12 +58,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 acir.circuit_arguments() {
csat.mark_solvable(value);
}
csat
}
};

// TODO: the code below is only for CSAT transformer
Expand Down Expand Up @@ -102,26 +108,106 @@ 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));
}
}
other_gate => {
Opcode::BlackBoxFuncCall(func) => {
match func {
acir::circuit::opcodes::BlackBoxFuncCall::AND { output, .. }
| acir::circuit::opcodes::BlackBoxFuncCall::XOR { output, .. } => {
transformer.mark_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.mark_solvable(*witness);
}
}
acir::circuit::opcodes::BlackBoxFuncCall::FixedBaseScalarMul {
outputs,
..
}
| acir::circuit::opcodes::BlackBoxFuncCall::Pedersen { outputs, .. } => {
transformer.mark_solvable(outputs.0);
transformer.mark_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.mark_solvable(*output)
}
}

new_opcode_labels.push(opcode_label[index]);
transformed_gates.push(other_gate.clone())
transformed_gates.push(opcode.clone());
}
Opcode::Directive(directive) => {
match directive {
Directive::Invert { result, .. } => {
transformer.mark_solvable(*result);
}
Directive::Quotient(quotient_directive) => {
transformer.mark_solvable(quotient_directive.q);
transformer.mark_solvable(quotient_directive.r);
}
Directive::ToLeRadix { b, .. } => {
for w in b {
transformer.mark_solvable(*w);
}
}
Directive::PermutationSort { bits, .. } => {
for w in bits {
transformer.mark_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!(),
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
Opcode::Brillig(brillig) => {
for output in &brillig.outputs {
match output {
BrilligOutputs::Simple(w) => transformer.mark_solvable(*w),
BrilligOutputs::Array(v) => {
for w in v {
transformer.mark_solvable(*w);
}
}
}
}
new_opcode_labels.push(opcode_label[index]);
transformed_gates.push(opcode.clone());
}
}
}

let current_witness_index = next_witness_index - 1;

Ok((
Circuit {
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,
},
Expand Down
4 changes: 4 additions & 0 deletions acvm/src/compiler/optimizers/redundant_range.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ 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,
},
Expand Down Expand Up @@ -139,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::{
Expand All @@ -163,6 +166,7 @@ mod tests {
Circuit {
current_witness_index: 1,
opcodes,
private_parameters: BTreeSet::new(),
public_parameters: PublicInputs::default(),
return_values: PublicInputs::default(),
}
Expand Down
Loading