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

Commit

Permalink
feat(acvm)!: Simplification pass for ACIR (#151)
Browse files Browse the repository at this point in the history
* Simplification pass for ACIR

* update comments

* Apply simplification during fallback

* Add unit test

* Move simplifier to optimiser module

* Fix unit tests

* make simplify public
  • Loading branch information
guipublic authored May 8, 2023
1 parent 10edd64 commit 7bc42c6
Show file tree
Hide file tree
Showing 9 changed files with 554 additions and 47 deletions.
31 changes: 17 additions & 14 deletions acir/src/circuit/directives.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,15 @@ use crate::{
};
use serde::{Deserialize, Serialize};

#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct QuotientDirective {
pub a: Expression,
pub b: Expression,
pub q: Witness,
pub r: Witness,
pub predicate: Option<Expression>,
}

#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
/// Directives do not apply any constraints.
/// You can think of them as opcodes that allow one to use non-determinism
Expand All @@ -18,13 +27,7 @@ pub enum Directive {
},

//Performs euclidian division of a / b (as integers) and stores the quotient in q and the rest in r
Quotient {
a: Expression,
b: Expression,
q: Witness,
r: Witness,
predicate: Option<Expression>,
},
Quotient(QuotientDirective),

//decomposition of a: a=\sum b[i]*radix^i where b is an array of witnesses < radix in little endian form
ToLeRadix {
Expand All @@ -48,7 +51,7 @@ impl Directive {
pub fn name(&self) -> &str {
match self {
Directive::Invert { .. } => "invert",
Directive::Quotient { .. } => "quotient",
Directive::Quotient(_) => "quotient",
Directive::ToLeRadix { .. } => "to_le_radix",
Directive::PermutationSort { .. } => "permutation_sort",
Directive::Log { .. } => "log",
Expand All @@ -71,7 +74,7 @@ impl Directive {
write_u32(&mut writer, x.witness_index())?;
write_u32(&mut writer, result.witness_index())?;
}
Directive::Quotient { a, b, q, r, predicate } => {
Directive::Quotient(QuotientDirective { a, b, q, r, predicate }) => {
a.write(&mut writer)?;
b.write(&mut writer)?;
write_u32(&mut writer, q.witness_index())?;
Expand Down Expand Up @@ -151,7 +154,7 @@ impl Directive {
false => None,
};

Ok(Directive::Quotient { a, b, q, r, predicate })
Ok(Directive::Quotient(QuotientDirective { a, b, q, r, predicate }))
}
2 => {
let a = Expression::read(&mut reader)?;
Expand Down Expand Up @@ -249,20 +252,20 @@ fn serialization_roundtrip() {
// TODO: Find a way to ensure that we include all of the variants
let invert = Directive::Invert { x: Witness(10), result: Witness(10) };

let quotient_none = Directive::Quotient {
let quotient_none = Directive::Quotient(QuotientDirective {
a: Expression::default(),
b: Expression::default(),
q: Witness(1u32),
r: Witness(2u32),
predicate: None,
};
let quotient_predicate = Directive::Quotient {
});
let quotient_predicate = Directive::Quotient(QuotientDirective {
a: Expression::default(),
b: Expression::default(),
q: Witness(1u32),
r: Witness(2u32),
predicate: Some(Expression::default()),
};
});

let to_le_radix = Directive::ToLeRadix {
a: Expression::default(),
Expand Down
4 changes: 2 additions & 2 deletions acir/src/circuit/opcodes.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use std::io::{Read, Write};

use super::directives::{Directive, LogInfo};
use super::directives::{Directive, LogInfo, QuotientDirective};
use crate::native_types::Expression;
use crate::serialization::{read_n, write_bytes};

Expand Down Expand Up @@ -149,7 +149,7 @@ impl std::fmt::Display for Opcode {
write!(f, "DIR::INVERT ")?;
write!(f, "(_{}, out: _{}) ", x.witness_index(), r.witness_index())
}
Opcode::Directive(Directive::Quotient { a, b, q, r, predicate }) => {
Opcode::Directive(Directive::Quotient(QuotientDirective { a, b, q, r, predicate })) => {
write!(f, "DIR::QUOTIENT ")?;
if let Some(pred) = predicate {
writeln!(f, "PREDICATE = {pred}")?;
Expand Down
4 changes: 4 additions & 0 deletions acir/src/native_types/expression/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,10 @@ impl Expression {
self.is_linear() && self.linear_combinations.len() == 1
}

pub fn is_zero(&self) -> bool {
*self == Self::zero()
}

/// Returns a `FieldElement` if the expression represents a constant polynomial.
/// Otherwise returns `None`.
///
Expand Down
4 changes: 3 additions & 1 deletion acvm/src/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ use thiserror::Error;
use transformers::{CSatTransformer, FallbackTransformer, IsOpcodeSupported, R1CSTransformer};

use self::optimizers::RangeOptimizer;
use self::optimizers::Simplifier;

#[derive(PartialEq, Eq, Debug, Error)]
pub enum CompileError {
Expand All @@ -25,13 +26,14 @@ pub fn compile(
acir: Circuit,
np_language: Language,
is_opcode_supported: IsOpcodeSupported,
simplifier: &Simplifier,
) -> Result<Circuit, CompileError> {
// Instantiate the optimizer.
// Currently the optimizer and reducer are one in the same
// for CSAT

// Fallback transformer pass
let acir = FallbackTransformer::transform(acir, is_opcode_supported)?;
let acir = FallbackTransformer::transform(acir, is_opcode_supported, simplifier)?;

// General optimizer pass
let mut opcodes: Vec<Opcode> = Vec::new();
Expand Down
2 changes: 2 additions & 0 deletions acvm/src/compiler/optimizers/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
mod general;
mod redundant_range;
pub mod simplify;

pub(crate) use general::GeneralOpt as GeneralOptimizer;
pub(crate) use redundant_range::RangeOptimizer;
pub(crate) use simplify::CircuitSimplifier as Simplifier;
Loading

0 comments on commit 7bc42c6

Please sign in to comment.