diff --git a/examples/bool.asm b/examples/bool.asm index 053da8cc4..ea1366e0a 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -1,11 +1,21 @@ @ noname.0.7.0 DoubleGeneric<1> -DoubleGeneric<-1,0,0,1> -DoubleGeneric<-1,0,0,1> -DoubleGeneric<0,-1,-1,0,1> -DoubleGeneric<0,-1,0,0,1> -DoubleGeneric<0,-1,0,0,1> -(0,0) -> (1,0) -> (1,1) -> (5,1) -(2,0) -> (2,1) -> (3,1) -(3,2) -> (4,1) +DoubleGeneric<1,0,-1,0,-1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> +DoubleGeneric<1,0,-1,0,-1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> +DoubleGeneric<1,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<1,0,0,0,-1> +DoubleGeneric<1,0,0,0,-1> +(0,0) -> (1,0) -> (2,0) -> (10,0) +(1,2) -> (2,1) +(2,2) -> (3,0) +(4,0) -> (5,0) -> (7,0) +(4,2) -> (5,1) +(5,2) -> (6,0) +(7,1) -> (8,0) +(8,2) -> (9,0) diff --git a/examples/equals.asm b/examples/equals.asm index 41dd7602e..2ffa2e4e2 100644 --- a/examples/equals.asm +++ b/examples/equals.asm @@ -2,23 +2,39 @@ DoubleGeneric<1> DoubleGeneric<1> -DoubleGeneric<1,-1,-1> -DoubleGeneric<1,1,0,0,-1> -DoubleGeneric<0,0,0,1> +DoubleGeneric<1,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,1> +DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<0,-1,0,0,1> +DoubleGeneric<1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,-1> +DoubleGeneric<1,0,0,0,-1> DoubleGeneric<1,0,0,0,-3> -DoubleGeneric<1,-1,-1> -DoubleGeneric<1,1,0,0,-1> -DoubleGeneric<0,0,0,1> +DoubleGeneric<1,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<0,-1,0,0,1> -(0,0) -> (2,1) -> (8,1) -(1,0) -> (2,0) -(2,2) -> (4,1) -> (5,1) -(3,0) -> (5,2) -(3,1) -> (4,0) -> (6,1) -(7,0) -> (8,0) -(8,2) -> (10,1) -> (11,1) -(9,0) -> (11,2) -(9,1) -> (10,0) -> (12,1) +DoubleGeneric<1,-1> +DoubleGeneric<1,0,0,0,-1> +(0,0) -> (2,0) -> (12,0) +(1,0) -> (3,0) +(2,1) -> (3,1) +(3,2) -> (6,1) -> (8,1) +(4,0) -> (6,0) -> (10,0) +(4,1) -> (5,0) +(5,2) -> (9,1) +(6,2) -> (7,0) +(8,2) -> (9,0) +(11,0) -> (13,0) +(12,1) -> (13,1) +(13,2) -> (16,1) -> (18,1) +(14,0) -> (16,0) -> (20,0) +(14,1) -> (15,0) +(15,2) -> (19,1) +(16,2) -> (17,0) +(18,2) -> (19,0) diff --git a/examples/if_else.asm b/examples/if_else.asm index 00d8d2e99..d526cf3d7 100644 --- a/examples/if_else.asm +++ b/examples/if_else.asm @@ -3,20 +3,32 @@ DoubleGeneric<1> DoubleGeneric<1,0,-1,0,1> DoubleGeneric<1,0,0,0,-1> -DoubleGeneric<1,-1,-1> -DoubleGeneric<1,1,0,0,-1> -DoubleGeneric<0,0,0,1> +DoubleGeneric<1,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,-1,-1> -DoubleGeneric<1,-1,-1> +DoubleGeneric<1,-1> +DoubleGeneric<1,1> +DoubleGeneric<1,1,-1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,-1> DoubleGeneric<1,0,0,0,-2> -(0,0) -> (1,0) -> (3,1) -> (7,1) -> (8,1) -(1,2) -> (7,0) -(2,0) -> (3,0) -(3,2) -> (5,1) -> (6,1) -(4,0) -> (6,2) -(4,1) -> (5,0) -> (9,0) -(7,2) -> (9,1) -(8,0) -> (10,0) -(8,2) -> (9,2) +(0,0) -> (1,0) -> (3,0) -> (11,0) -> (14,1) +(1,2) -> (12,0) +(2,0) -> (4,0) +(3,1) -> (4,1) +(4,2) -> (7,1) -> (9,1) +(5,0) -> (7,0) -> (13,0) +(5,1) -> (6,0) +(6,2) -> (10,1) +(7,2) -> (8,0) +(9,2) -> (10,0) +(11,1) -> (12,1) +(12,2) -> (13,1) +(13,2) -> (14,0) +(14,2) -> (15,1) +(15,0) -> (16,0) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index efc139075..94e1d6438 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -89,6 +89,9 @@ pub struct KimchiVesta { /// Once this is set, you can generate a witness (and can't modify the circuit?) // Note: I don't think we need this, but it acts as a nice redundant failsafe. pub(crate) finalized: bool, + + /// Size of the public input. + pub(crate) public_input_size: usize, } impl Witness { @@ -133,58 +136,11 @@ impl KimchiVesta { pending_generic_gate: None, debug_info: vec![], finalized: false, + public_input_size: 0, } } -} - -impl Backend for KimchiVesta { - type Field = VestaField; - type GeneratedWitness = GeneratedWitness; - - fn poseidon() -> crate::imports::FnHandle { - builtin::poseidon - } - - fn witness_vars(&self) -> &HashMap> { - &self.witness_vars - } - - fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar { - // create new var - let var = CellVar::new(self.next_variable, span); - self.next_variable += 1; - - // store it in the circuit_writer - self.witness_vars.insert(var.index, val); - - var - } - - fn add_constant( - &mut self, - label: Option<&'static str>, - value: VestaField, - span: Span, - ) -> CellVar { - if let Some(cvar) = self.cached_constants.get(&value) { - return *cvar; - } - - let var = self.new_internal_var(Value::Constant(value), span); - self.cached_constants.insert(value, var); - - let zero = VestaField::zero(); - - let _ = &self.add_generic_gate( - label.unwrap_or("hardcode a constant"), - vec![Some(var)], - vec![VestaField::one(), zero, zero, zero, value.neg()], - span, - ); - - var - } + /// Add a gate to the circuit fn add_gate( &mut self, note: &'static str, @@ -238,6 +194,7 @@ impl Backend for KimchiVesta { } } + /// Add a generic double gate to the circuit fn add_generic_gate( &mut self, label: &'static str, @@ -276,6 +233,55 @@ impl Backend for KimchiVesta { }); } } +} + +impl Backend for KimchiVesta { + type Field = VestaField; + type GeneratedWitness = GeneratedWitness; + + fn poseidon() -> crate::imports::FnHandle { + builtin::poseidon + } + + fn witness_vars(&self) -> &HashMap> { + &self.witness_vars + } + + fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar { + // create new var + let var = CellVar::new(self.next_variable, span); + self.next_variable += 1; + + // store it in the circuit_writer + self.witness_vars.insert(var.index, val); + + var + } + + fn add_constant( + &mut self, + label: Option<&'static str>, + value: VestaField, + span: Span, + ) -> CellVar { + if let Some(cvar) = self.cached_constants.get(&value) { + return *cvar; + } + + let var = self.new_internal_var(Value::Constant(value), span); + self.cached_constants.insert(value, var); + + let zero = VestaField::zero(); + + let _ = &self.add_generic_gate( + label.unwrap_or("hardcode a constant"), + vec![Some(var)], + vec![VestaField::one(), zero, zero, zero, value.neg()], + span, + ); + + var + } fn finalize_circuit( &mut self, @@ -348,7 +354,6 @@ impl Backend for KimchiVesta { fn generate_witness( &self, witness_env: &mut WitnessEnv, - public_input_size: usize, ) -> Result { if !self.finalized { unreachable!("the circuit must be finalized before generating a witness"); @@ -380,7 +385,7 @@ impl Backend for KimchiVesta { } // check if the row makes sense - let is_not_public_input = row >= public_input_size; + let is_not_public_input = row >= self.public_input_size; if is_not_public_input { #[allow(clippy::single_match)] match gate.typ { @@ -424,9 +429,9 @@ impl Backend for KimchiVesta { } // extract full public input (containing the public output) - let mut full_public_inputs = Vec::with_capacity(public_input_size); + let mut full_public_inputs = Vec::with_capacity(self.public_input_size); - for witness_row in witness.iter().take(public_input_size) { + for witness_row in witness.iter().take(self.public_input_size) { full_public_inputs.push(witness_row[0]); } @@ -546,4 +551,159 @@ impl Backend for KimchiVesta { res } + + fn neg(&mut self, var: &CellVar, span: Span) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + let neg_var = self.new_internal_var( + Value::LinearCombination(vec![(one.neg(), *var)], zero), + span, + ); + self.add_generic_gate( + "constraint to validate a negation (`x + (-x) = 0`)", + vec![Some(*var), Some(neg_var)], + vec![one, one], + span, + ); + + neg_var + } + + fn add(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + // create a new variable to store the result + let res = self.new_internal_var( + Value::LinearCombination(vec![(one, *lhs), (one, *rhs)], zero), + span, + ); + + // create a gate to store the result + self.add_generic_gate( + "add two variables together", + vec![Some(*lhs), Some(*rhs), Some(res)], + vec![one, one, one.neg()], + span, + ); + + res + } + + fn add_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + // create a new variable to store the result + let res = self.new_internal_var(Value::LinearCombination(vec![(one, *var)], *cst), span); + + // create a gate to store the result + // TODO: we should use an add_generic function that takes advantage of the double generic gate + self.add_generic_gate( + "add a constant with a variable", + vec![Some(*var), None, Some(res)], + vec![one, zero, one.neg(), zero, *cst], + span, + ); + + res + } + + fn mul(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + // create a new variable to store the result + let res = self.new_internal_var(Value::Mul(*lhs, *rhs), span); + + // create a gate to store the result + self.add_generic_gate( + "add two variables together", + vec![Some(*lhs), Some(*rhs), Some(res)], + vec![zero, zero, one.neg(), one], + span, + ); + + res + } + + fn mul_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + // create a new variable to store the result + let res = self.new_internal_var(Value::Scale(*cst, *var), span); + + // create a gate to store the result + // TODO: we should use an add_generic function that takes advantage of the double generic gate + self.add_generic_gate( + "add a constant with a variable", + vec![Some(*var), None, Some(res)], + vec![*cst, zero, one.neg()], + span, + ); + + res + } + + fn assert_eq_const(&mut self, cvar: &CellVar, cst: Self::Field, span: Span) { + self.add_generic_gate( + "constrain var - cst = 0 to check equality", + vec![Some(*cvar)], + vec![ + Self::Field::one(), + Self::Field::zero(), + Self::Field::zero(), + Self::Field::zero(), + cst.neg(), + ], + span, + ); + } + + fn assert_eq_var(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) { + // TODO: use permutation to check that + self.add_generic_gate( + "constrain lhs - rhs = 0 to assert that they are equal", + vec![Some(*lhs), Some(*rhs)], + vec![Self::Field::one(), Self::Field::one().neg()], + span, + ); + } + + fn add_public_input(&mut self, val: Value, span: Span) -> CellVar { + // create the var + let cvar = self.new_internal_var(val, span); + + // create the associated generic gate + self.add_gate( + "add public input", + GateKind::DoubleGeneric, + vec![Some(cvar)], + vec![Self::Field::one()], + span, + ); + + self.public_input_size += 1; + + cvar + } + + fn add_public_output(&mut self, val: Value, span: Span) -> CellVar { + // create the var + let cvar = self.new_internal_var(val, span); + + // create the associated generic gate + self.add_generic_gate( + "add public output", + vec![Some(cvar)], + vec![Self::Field::one()], + span, + ); + + self.public_input_size += 1; + + cvar + } } diff --git a/src/backends/kimchi/prover.rs b/src/backends/kimchi/prover.rs index bc7358afd..3ab1a672d 100644 --- a/src/backends/kimchi/prover.rs +++ b/src/backends/kimchi/prover.rs @@ -65,7 +65,6 @@ pub struct VerifierIndex { impl KimchiVesta { pub fn compile_to_indexes( &self, - public_input_size: usize, ) -> miette::Result<( kimchi::prover_index::ProverIndex>, kimchi::verifier_index::VerifierIndex>, @@ -102,7 +101,7 @@ impl KimchiVesta { // create constraint system let cs = ConstraintSystem::create(gates) - .public(public_input_size) + .public(self.public_input_size) .build() .into_diagnostic() .wrap_err("kimchi: could not create a constraint system with the given circuit and public input size")?; @@ -128,10 +127,7 @@ impl KimchiVesta { impl CompiledCircuit { pub fn compile_to_indexes(self) -> miette::Result<(ProverIndex, VerifierIndex)> { - let (prover_index, verifier_index) = self - .circuit - .backend - .compile_to_indexes(self.circuit.public_input_size)?; + let (prover_index, verifier_index) = self.circuit.backend.compile_to_indexes()?; // wrap let prover_index = { ProverIndex { diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 6bc43655f..bb96de44e 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -35,6 +35,33 @@ pub trait Backend: Clone { /// It increments the variable index for look up later. fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar; + /// negate a var + fn neg(&mut self, var: &CellVar, span: Span) -> CellVar; + + /// add two vars + fn add(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar; + + /// add a var with a constant + fn add_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar; + + /// multiply a var with another var + fn mul(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar; + + /// multiply a var with a constant + fn mul_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar; + + /// add a constraint to assert a var equals a constant + fn assert_eq_const(&mut self, var: &CellVar, cst: Self::Field, span: Span); + + /// add a constraint to assert a var equals another var + fn assert_eq_var(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span); + + /// Process a public input + fn add_public_input(&mut self, val: Value, span: Span) -> CellVar; + + /// Process a public output + fn add_public_output(&mut self, val: Value, span: Span) -> CellVar; + /// This should be called only when you want to constrain a constant for real. /// Gates that handle constants should always make sure to call this function when they want them constrained. fn add_constant( @@ -44,25 +71,6 @@ pub trait Backend: Clone { span: Span, ) -> CellVar; - /// Add a gate to the circuit. Kimchi specific atm. - fn add_gate( - &mut self, - note: &'static str, - typ: GateKind, - vars: Vec>, - coeffs: Vec, - span: Span, - ); - - /// Add a generic double gate to the circuit. Kimchi specific atm. - fn add_generic_gate( - &mut self, - label: &'static str, - vars: Vec>, - coeffs: Vec, - span: Span, - ); - /// Compute the value of the symbolic cell variables. /// It recursively does the computation down the stream until it is not a symbolic variable. /// - The symbolic variables are stored in the witness_vars. @@ -119,7 +127,6 @@ pub trait Backend: Clone { } } - // TODO: we may need to move the finalized flag from circuit writer to backend, so the backend can freeze itself once finalized. /// Finalize the circuit by doing some sanitizing checks. fn finalize_circuit( &mut self, @@ -133,7 +140,6 @@ pub trait Backend: Clone { fn generate_witness( &self, witness_env: &mut WitnessEnv, - public_input_size: usize, ) -> Result; /// Generate the asm for a backend. diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index 31a26eb8c..28d60bcd4 100644 --- a/src/circuit_writer/mod.rs +++ b/src/circuit_writer/mod.rs @@ -36,9 +36,6 @@ where /// So we might make this private if the prover facilities can be deprecated. pub backend: B, - /// Size of the public input. - pub(crate) public_input_size: usize, - /// If a public output is set, this will be used to store its [Var]. /// The public output generation works as follows: /// 1. This cvar is created and inserted in the circuit (gates) during compilation of the public input @@ -141,7 +138,6 @@ impl CircuitWriter { Self { typed, backend, - public_input_size: 0, public_output: None, private_input_indices: vec![], } @@ -243,7 +239,6 @@ impl CircuitWriter { &self, witness_env: &mut WitnessEnv, ) -> Result { - self.backend - .generate_witness(witness_env, self.public_input_size) + self.backend.generate_witness(witness_env) } } diff --git a/src/circuit_writer/writer.rs b/src/circuit_writer/writer.rs index 0045d99c7..5e2619870 100644 --- a/src/circuit_writer/writer.rs +++ b/src/circuit_writer/writer.rs @@ -697,24 +697,12 @@ impl CircuitWriter { let mut cvars = Vec::with_capacity(num); for idx in 0..num { - // create the var let cvar = self .backend - .new_internal_var(Value::External(name.clone(), idx), span); + .add_public_input(Value::External(name.clone(), idx), span); cvars.push(ConstOrCell::Cell(cvar)); - - // create the associated generic gate - self.backend.add_gate( - "add public input", - GateKind::DoubleGeneric, - vec![Some(cvar)], - vec![B::Field::one()], - span, - ); } - self.public_input_size += num; - Var::new(cvars, span) } @@ -723,21 +711,11 @@ impl CircuitWriter { let mut cvars = Vec::with_capacity(num); for _ in 0..num { - // create the var let cvar = self .backend - .new_internal_var(Value::PublicOutput(None), span); + .add_public_output(Value::PublicOutput(None), span); cvars.push(ConstOrCell::Cell(cvar)); - - // create the associated generic gate - self.backend.add_generic_gate( - "add public output", - vec![Some(cvar)], - vec![B::Field::one()], - span, - ); } - self.public_input_size += num; // store it let res = Var::new(cvars, span); diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index 06f8fff00..99bc68e91 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -11,23 +11,25 @@ use crate::{ var::{ConstOrCell, Value, Var}, }; +use super::field::sub; + pub fn is_valid(f: F) -> bool { f.is_one() || f.is_zero() } pub fn check(compiler: &mut CircuitWriter, xx: &ConstOrCell, span: Span) { - let zero = B::Field::zero(); let one = B::Field::one(); match xx { ConstOrCell::Const(ff) => assert!(is_valid(*ff)), - ConstOrCell::Cell(var) => compiler.backend.add_generic_gate( - "constraint to validate a boolean (`x(x-1) = 0`)", - // x^2 - x = 0 - vec![Some(*var), Some(*var), None], - vec![one.neg(), zero, zero, one], - span, - ), + ConstOrCell::Cell(x) => { + // x * (x - 1) + let x_1 = compiler.backend.add_const(x, &one.neg(), span); + let res = compiler.backend.mul(x, &x_1, span); + compiler + .backend + .assert_eq_const(&res, B::Field::zero(), span); + } }; } @@ -53,22 +55,9 @@ pub fn and( // two vars (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = compiler - .backend - .new_internal_var(Value::Mul(*lhs, *rhs), span); - - // create a gate to constrain the result - let zero = B::Field::zero(); - let one = B::Field::one(); - compiler.backend.add_generic_gate( - "constrain the AND as lhs * rhs", - vec![Some(*lhs), Some(*rhs), Some(res)], - vec![zero, zero, one.neg(), one], // mul - span, - ); - - // return the result + // lhs * rhs + let res = compiler.backend.mul(lhs, rhs, span); + Var::new_var(res, span) } } @@ -89,27 +78,14 @@ pub fn not( Var::new_constant(value, span) } + ConstOrCell::Cell(var) => { + let one = ConstOrCell::Const(B::Field::one()); + let var = ConstOrCell::Cell(*var); - // constant and a var - ConstOrCell::Cell(cvar) => { - let zero = B::Field::zero(); - let one = B::Field::one(); - - // create a new variable to store the result - let lc = Value::LinearCombination(vec![(one.neg(), *cvar)], one); // 1 - X - let res = compiler.backend.new_internal_var(lc, span); - - // create a gate to constrain the result - compiler.backend.add_generic_gate( - "constrain the NOT as 1 - X", - vec![None, Some(*cvar), Some(res)], - // we use the constant to do 1 - X - vec![zero, one.neg(), one.neg(), zero, one], - span, - ); - - // return the result - Var::new_var(res, span) + // 1 - x + let res = sub(compiler, &one, &var, span)[0]; + + Var::new_cvar(res, span) } } } diff --git a/src/constraints/field.rs b/src/constraints/field.rs index d6993715b..6a235375d 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -11,6 +11,21 @@ use ark_ff::{One, Zero}; use std::{ops::Neg, sync::Arc}; +/// Negates a field element +pub fn neg( + compiler: &mut CircuitWriter, + cvar: &ConstOrCell, + span: Span, +) -> Var { + match cvar { + crate::var::ConstOrCell::Const(ff) => Var::new_constant(ff.neg(), span), + crate::var::ConstOrCell::Cell(var) => { + let res = compiler.backend.neg(var, span); + Var::new_var(res, span) + } + } +} + /// Adds two field elements pub fn add( compiler: &mut CircuitWriter, @@ -18,9 +33,6 @@ pub fn add( rhs: &ConstOrCell, span: Span, ) -> Var { - let zero = B::Field::zero(); - let one = B::Field::one(); - match (lhs, rhs) { // 2 constants (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs + *rhs, span), @@ -34,40 +46,12 @@ pub fn add( return Var::new_var(*cvar, span); } - // create a new variable to store the result - let res = compiler - .backend - .new_internal_var(Value::LinearCombination(vec![(one, *cvar)], *cst), span); - - // create a gate to store the result - // TODO: we should use an add_generic function that takes advantage of the double generic gate - compiler.backend.add_generic_gate( - "add a constant with a variable", - vec![Some(*cvar), None, Some(res)], - vec![one, zero, one.neg(), zero, *cst], - span, - ); + let res = compiler.backend.add_const(cvar, cst, span); Var::new_var(res, span) } (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = compiler.backend.new_internal_var( - Value::LinearCombination( - vec![(B::Field::one(), *lhs), (B::Field::one(), *rhs)], - B::Field::zero(), - ), - span, - ); - - // create a gate to store the result - compiler.backend.add_generic_gate( - "add two variables together", - vec![Some(*lhs), Some(*rhs), Some(res)], - vec![B::Field::one(), B::Field::one(), B::Field::one().neg()], - span, - ); - + let res = compiler.backend.add(lhs, rhs, span); Var::new_var(res, span) } } @@ -80,80 +64,8 @@ pub fn sub( rhs: &ConstOrCell, span: Span, ) -> Var { - let zero = B::Field::zero(); - let one = B::Field::one(); - - match (lhs, rhs) { - // const1 - const2 - (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs - *rhs, span), - - // const - var - (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) => { - // create a new variable to store the result - let res = compiler.backend.new_internal_var( - Value::LinearCombination(vec![(one.neg(), *cvar)], *cst), - span, - ); - - // create a gate to store the result - compiler.backend.add_generic_gate( - "constant - variable", - vec![Some(*cvar), None, Some(res)], - // cst - cvar - out = 0 - vec![one.neg(), zero, one.neg(), zero, *cst], - span, - ); - - Var::new_var(res, span) - } - - // var - const - (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { - // if the constant is zero, we can ignore this gate - if cst.is_zero() { - // TODO: that span is incorrect, it should come from lhs or rhs... - return Var::new_var(*cvar, span); - } - - // create a new variable to store the result - let res = compiler.backend.new_internal_var( - Value::LinearCombination(vec![(one, *cvar)], cst.neg()), - span, - ); - - // create a gate to store the result - // TODO: we should use an add_generic function that takes advantage of the double generic gate - compiler.backend.add_generic_gate( - "variable - constant", - vec![Some(*cvar), None, Some(res)], - // var - cst - out = 0 - vec![one, zero, one.neg(), zero, cst.neg()], - span, - ); - - Var::new_var(res, span) - } - - // lhs - rhs - (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = compiler.backend.new_internal_var( - Value::LinearCombination(vec![(one, *lhs), (one.neg(), *rhs)], zero), - span, - ); - - // create a gate to store the result - compiler.backend.add_generic_gate( - "var1 - var2", - vec![Some(*lhs), Some(*rhs), Some(res)], - // lhs - rhs - out = 0 - vec![one, one.neg(), one.neg()], - span, - ); - - Var::new_var(res, span) - } - } + let neg_rhs = neg(compiler, rhs, span); + add(compiler, lhs, &neg_rhs.cvars[0], span) } /// Multiplies two field elements @@ -163,9 +75,6 @@ pub fn mul( rhs: &ConstOrCell, span: Span, ) -> Var { - let zero = B::Field::zero(); - let one = B::Field::one(); - match (lhs, rhs) { // 2 constants (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs * *rhs, span), @@ -175,46 +84,16 @@ pub fn mul( | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { // if the constant is zero, we can ignore this gate if cst.is_zero() { - let zero = compiler.backend.add_constant( - Some("encoding zero for the result of 0 * var"), - B::Field::zero(), - span, - ); - return Var::new_var(zero, span); + return Var::new_constant(*cst, span); } - // create a new variable to store the result - let res = compiler - .backend - .new_internal_var(Value::Scale(*cst, *cvar), span); - - // create a gate to store the result - // TODO: we should use an add_generic function that takes advantage of the double generic gate - compiler.backend.add_generic_gate( - "add a constant with a variable", - vec![Some(*cvar), None, Some(res)], - vec![*cst, zero, one.neg(), zero, *cst], - span, - ); - + let res = compiler.backend.mul_const(cvar, cst, span); Var::new_var(res, span) } // everything is a var (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = compiler - .backend - .new_internal_var(Value::Mul(*lhs, *rhs), span); - - // create a gate to store the result - compiler.backend.add_generic_gate( - "add two variables together", - vec![Some(*lhs), Some(*rhs), Some(res)], - vec![zero, zero, one.neg(), one], - span, - ); - + let res = compiler.backend.mul(lhs, rhs, span); Var::new_var(res, span) } } @@ -326,55 +205,28 @@ fn equal_cells( ); // 1. diff = x2 - x1 - let diff = compiler.backend.new_internal_var( - Value::LinearCombination(vec![(one, x2), (one.neg(), x1)], zero), - span, - ); - - compiler.backend.add_generic_gate( - "constraint #1 for the equals gadget (x2 - x1 - diff = 0)", - vec![Some(x2), Some(x1), Some(diff)], - // x2 - x1 - diff = 0 - vec![one, one.neg(), one.neg()], - span, - ); + let neg_x1 = compiler.backend.neg(&x1, span); + let diff = compiler.backend.add(&x2, &neg_x1, span); // 2. one_minus_res = 1 - res - let one_minus_res = compiler - .backend - .new_internal_var(Value::LinearCombination(vec![(one.neg(), res)], one), span); - - compiler.backend.add_generic_gate( - "constraint #2 for the equals gadget (one_minus_res + res - 1 = 0)", - vec![Some(one_minus_res), Some(res)], - // we constrain one_minus_res + res - 1 = 0 - // so that we can encode res and wire it elsewhere - // (and not -res) - vec![one, one, zero, zero, one.neg()], - span, - ); + let neg_res = compiler.backend.neg(&res, span); + let one_minus_res = compiler.backend.add_const(&neg_res, &one, span); // 3. res * diff = 0 - compiler.backend.add_generic_gate( - "constraint #3 for the equals gadget (res * diff = 0)", - vec![Some(res), Some(diff)], - // res * diff = 0 - vec![zero, zero, zero, one], - span, - ); + let res_mul_diff = compiler.backend.mul(&res, &diff, span); + + compiler.backend.assert_eq_const(&res_mul_diff, zero, span); // 4. diff_inv * diff = one_minus_res let diff_inv = compiler .backend .new_internal_var(Value::Inverse(diff), span); - compiler.backend.add_generic_gate( - "constraint #4 for the equals gadget (diff_inv * diff = one_minus_res)", - vec![Some(diff_inv), Some(diff), Some(one_minus_res)], - // diff_inv * diff - one_minus_res = 0 - vec![zero, zero, one.neg(), one], - span, - ); + let diff_inv_mul_diff = compiler.backend.mul(&diff_inv, &diff, span); + + compiler + .backend + .assert_eq_var(&diff_inv_mul_diff, &one_minus_res, span); Var::new_var(res, span) } @@ -492,25 +344,14 @@ pub fn if_else_inner( span, ); - let then_m_else = sub(compiler, then_, else_, span)[0] - .cvar() - .cloned() - .unwrap(); - let res_m_else = sub(compiler, &ConstOrCell::::Cell(res), else_, span)[0] - .cvar() - .cloned() - .unwrap(); - - let zero = B::Field::zero(); - let one = B::Field::one(); - - compiler.backend.add_generic_gate( - "constraint for ternary operator: cond * (then - else) = res - else", - vec![Some(cond_cell), Some(then_m_else), Some(res_m_else)], - // cond * (then - else) = res - else - vec![zero, zero, one.neg(), one], - span, - ); + let then_m_else = sub(compiler, then_, else_, span)[0]; + + // constraint for ternary operator: cond * (then - else) = res - else + let cond_mul_then_m_else = mul(compiler, cond, &then_m_else, span)[0]; + let res_to_check = add(compiler, &cond_mul_then_m_else, else_, span)[0]; + compiler + .backend + .assert_eq_var(&res, res_to_check.cvar().unwrap(), span); Var::new_var(res, span) } diff --git a/src/stdlib/mod.rs b/src/stdlib/mod.rs index 4f336012c..572299926 100644 --- a/src/stdlib/mod.rs +++ b/src/stdlib/mod.rs @@ -1,6 +1,6 @@ -use std::{collections::HashSet, ops::Neg as _}; +use std::collections::HashSet; -use ark_ff::{One as _, Zero}; +use ark_ff::One; use once_cell::sync::Lazy; use crate::{ @@ -121,27 +121,10 @@ fn assert_eq( // a const and a var (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { - compiler.backend.add_generic_gate( - "constrain var - cst = 0 to check equality", - vec![Some(*cvar)], - vec![ - B::Field::one(), - B::Field::zero(), - B::Field::zero(), - B::Field::zero(), - cst.neg(), - ], - span, - ); + compiler.backend.assert_eq_const(cvar, *cst, span) } (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // TODO: use permutation to check that - compiler.backend.add_generic_gate( - "constrain lhs - rhs = 0 to assert that they are equal", - vec![Some(*lhs), Some(*rhs)], - vec![B::Field::one(), B::Field::one().neg()], - span, - ); + compiler.backend.assert_eq_var(lhs, rhs, span) } } @@ -171,16 +154,8 @@ fn assert( assert!(cst.is_one()); } ConstOrCell::Cell(cvar) => { - // TODO: use permutation to check that - let zero = B::Field::zero(); let one = B::Field::one(); - compiler.backend.add_generic_gate( - "constrain 1 - X = 0 to assert that X is true", - vec![None, Some(*cvar)], - // use the constant to constrain 1 - X = 0 - vec![zero, one.neg(), zero, zero, one], - span, - ); + compiler.backend.assert_eq_const(cvar, one, span); } }