From 0ea19d7e0591dfb463964d3e3b5fae1f5ab69a36 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 03:25:32 +0000 Subject: [PATCH 01/27] add neg/add/mul backend interfaces --- src/backends/mod.rs | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 6bc43655f..2f5735ff5 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -9,7 +9,7 @@ use crate::{ error::{Error, ErrorKind, Result}, helpers::PrettyField, imports::FnHandle, - var::{CellVar, Value, Var}, + var::{CellVar, ConstOrCell, Value, Var}, witness::WitnessEnv, }; @@ -35,6 +35,26 @@ pub trait Backend: Clone { /// It increments the variable index for look up later. fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar; + /// basic constraint negation + fn enforce_neg_constraint( + &mut self, + var: &ConstOrCell, + ) -> ConstOrCell; + + /// basic constraint addition + fn enforce_add_constraint( + &mut self, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + ) -> ConstOrCell; + + /// basic constraint multiplication + fn enforce_mul_constraint( + &mut self, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + ) -> ConstOrCell; + /// 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( From 4d32ca7734700fd9d675d730f21c6ca03fe2a033 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 03:26:01 +0000 Subject: [PATCH 02/27] impl neg constraint --- examples/arithmetic.no | 3 +++ src/backends/kimchi/mod.rs | 42 ++++++++++++++++++++++++++++++++++++++ src/constraints/field.rs | 25 ++++++----------------- 3 files changed, 51 insertions(+), 19 deletions(-) diff --git a/examples/arithmetic.no b/examples/arithmetic.no index 29199551e..fbb3cda48 100644 --- a/examples/arithmetic.no +++ b/examples/arithmetic.no @@ -1,4 +1,7 @@ fn main(pub public_input: Field, private_input: Field) { let xx = private_input + public_input; assert_eq(xx, 2); + + let yy = private_input - public_input; + assert_eq(yy, 0); } diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index efc139075..d45886065 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -546,4 +546,46 @@ impl Backend for KimchiVesta { res } + + fn enforce_neg_constraint( + &mut self, + var: &crate::var::ConstOrCell, + ) -> crate::var::ConstOrCell { + match var { + crate::var::ConstOrCell::Const(ff) => crate::var::ConstOrCell::Const(ff.neg()), + crate::var::ConstOrCell::Cell(var) => { + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + let neg_var = self.new_internal_var( + Value::LinearCombination(vec![(one.neg(), *var)], zero), + var.span, + ); + self.add_generic_gate( + "constraint to validate a negation (`x + (-x) = 0`)", + vec![Some(*var), None, Some(neg_var)], + vec![one, zero, one], + var.span, + ); + + crate::var::ConstOrCell::Cell(neg_var) + } + } + } + + fn enforce_add_constraint( + &mut self, + lhs: &crate::var::ConstOrCell, + rhs: &crate::var::ConstOrCell, + ) -> crate::var::ConstOrCell { + todo!() + } + + fn enforce_mul_constraint( + &mut self, + lhs: &crate::var::ConstOrCell, + rhs: &crate::var::ConstOrCell, + ) -> crate::var::ConstOrCell { + todo!() + } } diff --git a/src/constraints/field.rs b/src/constraints/field.rs index d6993715b..0dbfc88f7 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -2,6 +2,7 @@ use crate::{ backends::Backend, circuit_writer::CircuitWriter, constants::Span, + constraints::field, var::{ConstOrCell, Value, Var}, }; @@ -76,14 +77,14 @@ pub fn add( /// Subtracts two variables, we only support variables that are of length 1. pub fn sub( compiler: &mut CircuitWriter, - lhs: &ConstOrCell, - rhs: &ConstOrCell, + const_cell_lhs: &ConstOrCell, + const_cell_rhs: &ConstOrCell, span: Span, ) -> Var { let zero = B::Field::zero(); let one = B::Field::one(); - match (lhs, rhs) { + match (const_cell_lhs, const_cell_rhs) { // const1 - const2 (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs - *rhs, span), @@ -136,22 +137,8 @@ pub fn sub( // 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 = compiler.backend.enforce_neg_constraint(const_cell_rhs); + field::add(compiler, const_cell_lhs, &neg_rhs, span) } } } From ec3bf052052a014416a726e179806510356ed940 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 06:09:13 +0000 Subject: [PATCH 03/27] update asm --- examples/arithmetic.asm | 8 +++++++- examples/if_else.asm | 20 ++++++++++++-------- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/examples/arithmetic.asm b/examples/arithmetic.asm index 2c926b97f..0b05313e3 100644 --- a/examples/arithmetic.asm +++ b/examples/arithmetic.asm @@ -3,5 +3,11 @@ DoubleGeneric<1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,0,0,-2> -(0,0) -> (1,1) +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1> +(0,0) -> (1,1) -> (3,0) +(1,0) -> (4,0) (1,2) -> (2,0) +(3,2) -> (4,1) +(4,2) -> (5,0) diff --git a/examples/if_else.asm b/examples/if_else.asm index 00d8d2e99..edc91994e 100644 --- a/examples/if_else.asm +++ b/examples/if_else.asm @@ -7,16 +7,20 @@ DoubleGeneric<1,-1,-1> DoubleGeneric<1,1,0,0,-1> DoubleGeneric<0,0,0,1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,-1,-1> -DoubleGeneric<1,-1,-1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> DoubleGeneric<0,0,-1,1> DoubleGeneric<1,0,0,0,-2> -(0,0) -> (1,0) -> (3,1) -> (7,1) -> (8,1) -(1,2) -> (7,0) +(0,0) -> (1,0) -> (3,1) -> (7,0) -> (9,0) +(1,2) -> (8,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) +(4,1) -> (5,0) -> (11,0) +(7,2) -> (8,1) +(8,2) -> (11,1) +(9,2) -> (10,1) +(10,0) -> (12,0) +(10,2) -> (11,2) From bb6b8181efd42cb4090daecef8623b29292c3cfb Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 06:19:09 +0000 Subject: [PATCH 04/27] add span arg to basic constraint interface --- src/backends/kimchi/mod.rs | 7 +++++-- src/backends/mod.rs | 3 +++ src/constraints/field.rs | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index d45886065..9d828189d 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -550,6 +550,7 @@ impl Backend for KimchiVesta { fn enforce_neg_constraint( &mut self, var: &crate::var::ConstOrCell, + span: Span, ) -> crate::var::ConstOrCell { match var { crate::var::ConstOrCell::Const(ff) => crate::var::ConstOrCell::Const(ff.neg()), @@ -559,13 +560,13 @@ impl Backend for KimchiVesta { let neg_var = self.new_internal_var( Value::LinearCombination(vec![(one.neg(), *var)], zero), - var.span, + span, ); self.add_generic_gate( "constraint to validate a negation (`x + (-x) = 0`)", vec![Some(*var), None, Some(neg_var)], vec![one, zero, one], - var.span, + span, ); crate::var::ConstOrCell::Cell(neg_var) @@ -577,6 +578,7 @@ impl Backend for KimchiVesta { &mut self, lhs: &crate::var::ConstOrCell, rhs: &crate::var::ConstOrCell, + span: Span, ) -> crate::var::ConstOrCell { todo!() } @@ -585,6 +587,7 @@ impl Backend for KimchiVesta { &mut self, lhs: &crate::var::ConstOrCell, rhs: &crate::var::ConstOrCell, + span: Span, ) -> crate::var::ConstOrCell { todo!() } diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 2f5735ff5..7522d3fd6 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -39,6 +39,7 @@ pub trait Backend: Clone { fn enforce_neg_constraint( &mut self, var: &ConstOrCell, + span: Span, ) -> ConstOrCell; /// basic constraint addition @@ -46,6 +47,7 @@ pub trait Backend: Clone { &mut self, lhs: &ConstOrCell, rhs: &ConstOrCell, + span: Span, ) -> ConstOrCell; /// basic constraint multiplication @@ -53,6 +55,7 @@ pub trait Backend: Clone { &mut self, lhs: &ConstOrCell, rhs: &ConstOrCell, + span: Span, ) -> ConstOrCell; /// This should be called only when you want to constrain a constant for real. diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 0dbfc88f7..55ea884f2 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -137,7 +137,7 @@ pub fn sub( // lhs - rhs (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - let neg_rhs = compiler.backend.enforce_neg_constraint(const_cell_rhs); + let neg_rhs = compiler.backend.enforce_neg_constraint(const_cell_rhs, span); field::add(compiler, const_cell_lhs, &neg_rhs, span) } } From b9797ee7901c479539e420f36b22bcd3794d72ca Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 06:33:43 +0000 Subject: [PATCH 05/27] move add of field constraint to kimchi backend --- src/backends/kimchi/mod.rs | 56 ++++++++++++++++++++++++++++++++++++-- src/constraints/field.rs | 56 +++----------------------------------- 2 files changed, 58 insertions(+), 54 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 9d828189d..f768d09d1 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -21,7 +21,7 @@ use crate::{ constants::Span, error::{Error, ErrorKind, Result}, helpers::PrettyField, - var::{CellVar, Value, Var}, + var::{CellVar, ConstOrCell, Value, Var}, witness::WitnessEnv, }; @@ -580,7 +580,59 @@ impl Backend for KimchiVesta { rhs: &crate::var::ConstOrCell, span: Span, ) -> crate::var::ConstOrCell { - todo!() + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + match (lhs, rhs) { + // 2 constants + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { + ConstOrCell::Const(*lhs + *rhs) + } + + // const and a var + (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) + | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { + // if the constant is zero, we can ignore this gate + if cst.is_zero() { + return ConstOrCell::Cell(*cvar); + } + + // create a new variable to store the result + let res = self + .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 + self.add_generic_gate( + "add a constant with a variable", + vec![Some(*cvar), None, Some(res)], + vec![one, zero, one.neg(), zero, *cst], + span, + ); + + ConstOrCell::Cell(res) + } + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { + // create a new variable to store the result + let res = self.new_internal_var( + Value::LinearCombination( + vec![(Self::Field::one(), *lhs), (Self::Field::one(), *rhs)], + Self::Field::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![Self::Field::one(), Self::Field::one(), Self::Field::one().neg()], + span, + ); + + ConstOrCell::Cell(res) + } + } } fn enforce_mul_constraint( diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 55ea884f2..4d66f1a8a 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -19,58 +19,10 @@ 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), - - // const and a var - (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) - | (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), 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, - ); - - 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, - ); - - Var::new_var(res, span) - } + let res = compiler.backend.enforce_add_constraint(lhs, rhs, span); + match res { + ConstOrCell::Const(cst) => Var::new_constant(cst, span), + ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), } } From cce2669305c2f1ab4f19d5c0b44572208e43b8e0 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 06:41:52 +0000 Subject: [PATCH 06/27] move mul constraint of field to kimchi backend --- src/backends/kimchi/mod.rs | 52 +++++++++++++++++++++++++++++++++- src/constraints/field.rs | 58 +++----------------------------------- 2 files changed, 55 insertions(+), 55 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index f768d09d1..8c9fc5b3d 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -641,6 +641,56 @@ impl Backend for KimchiVesta { rhs: &crate::var::ConstOrCell, span: Span, ) -> crate::var::ConstOrCell { - todo!() + let zero = Self::Field::zero(); + let one = Self::Field::one(); + + match (lhs, rhs) { + // 2 constants + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => ConstOrCell::Const(*lhs * *rhs), + + // const and a var + (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) + | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { + // if the constant is zero, we can ignore this gate + if cst.is_zero() { + let zero = self.add_constant( + Some("encoding zero for the result of 0 * var"), + Self::Field::zero(), + span, + ); + return ConstOrCell::Cell(zero); + } + + // create a new variable to store the result + let res = self.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 + self.add_generic_gate( + "add a constant with a variable", + vec![Some(*cvar), None, Some(res)], + vec![*cst, zero, one.neg(), zero, *cst], + span, + ); + + ConstOrCell::Cell(res) + } + + // everything is a var + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { + // 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, + ); + + ConstOrCell::Cell(res) + } + } } } diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 4d66f1a8a..ace2091d4 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -102,60 +102,10 @@ 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), - - // const and a var - (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) - | (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); - } - - // 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, - ); - - 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, - ); - - Var::new_var(res, span) - } + let res = compiler.backend.enforce_mul_constraint(lhs, rhs, span); + match res { + ConstOrCell::Const(cst) => Var::new_constant(cst, span), + ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), } } From 34728240b9abbf02791a83a064bbe07d9f432ea3 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 07:18:56 +0000 Subject: [PATCH 07/27] refactor boolean constraints using basic constraints --- examples/bool.asm | 14 ++++++---- src/constraints/boolean.rs | 57 ++++++++++---------------------------- 2 files changed, 23 insertions(+), 48 deletions(-) diff --git a/examples/bool.asm b/examples/bool.asm index 053da8cc4..33f08dfd1 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -1,11 +1,15 @@ @ noname.0.7.0 DoubleGeneric<1> -DoubleGeneric<-1,0,0,1> -DoubleGeneric<-1,0,0,1> -DoubleGeneric<0,-1,-1,0,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<-1,0,-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) +(0,0) -> (1,0) -> (2,0) -> (7,1) +(1,2) -> (2,1) +(3,0) -> (4,0) -> (5,0) (3,2) -> (4,1) +(5,2) -> (6,1) diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index 06f8fff00..d43a2093c 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -11,23 +11,22 @@ use crate::{ var::{ConstOrCell, Value, Var}, }; +use super::field; + 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 - 1) + let x_1 = field::sub(compiler, xx, &ConstOrCell::Const(one.neg()), span); + field::mul(compiler, xx, &x_1.cvars[0], span); + }, }; } @@ -52,24 +51,10 @@ 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 - Var::new_var(res, span) + (ConstOrCell::Cell(_), ConstOrCell::Cell(_)) => { + // todo: should it check if the vars are either 1 or 0? + // lhs * rhs + field::mul(compiler, lhs, rhs, span) } } } @@ -91,25 +76,11 @@ pub fn not( } // constant and a var - ConstOrCell::Cell(cvar) => { - let zero = B::Field::zero(); + ConstOrCell::Cell(_) => { 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 + field::sub(compiler, &ConstOrCell::Const(one), var, span) } } } From 7f1862d3335339efc9953315d763b6e29e80895a Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 07:37:30 +0000 Subject: [PATCH 08/27] add neg wrapper in field constraint, so as to be consistent. --- src/constraints/field.rs | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/constraints/field.rs b/src/constraints/field.rs index ace2091d4..12094bfa8 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -12,6 +12,19 @@ use ark_ff::{One, Zero}; use std::{ops::Neg, sync::Arc}; +/// Adds two field elements +pub fn neg( + compiler: &mut CircuitWriter, + cvar: &ConstOrCell, + span: Span, +) -> Var { + let res = compiler.backend.enforce_neg_constraint(cvar, span); + match res { + ConstOrCell::Const(cst) => Var::new_constant(cst, span), + ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), + } +} + /// Adds two field elements pub fn add( compiler: &mut CircuitWriter, @@ -89,8 +102,8 @@ pub fn sub( // lhs - rhs (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - let neg_rhs = compiler.backend.enforce_neg_constraint(const_cell_rhs, span); - field::add(compiler, const_cell_lhs, &neg_rhs, span) + let neg_rhs = field::neg(compiler, const_cell_rhs, span); + field::add(compiler, const_cell_lhs, &neg_rhs.cvars[0], span) } } } From 02345e8cf30bcafb663cff99e7bb5a7dbbc802f7 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 07:47:47 +0000 Subject: [PATCH 09/27] refactor sub constraint --- examples/bool.asm | 8 +++-- src/constraints/field.rs | 66 +++------------------------------------- 2 files changed, 9 insertions(+), 65 deletions(-) diff --git a/examples/bool.asm b/examples/bool.asm index 33f08dfd1..37813cc6f 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -5,11 +5,13 @@ DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<-1,0,-1,0,1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,-1,0,0,1> DoubleGeneric<0,-1,0,0,1> -(0,0) -> (1,0) -> (2,0) -> (7,1) +(0,0) -> (1,0) -> (2,0) -> (8,1) (1,2) -> (2,1) (3,0) -> (4,0) -> (5,0) (3,2) -> (4,1) -(5,2) -> (6,1) +(5,2) -> (6,0) +(6,2) -> (7,1) diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 12094bfa8..ca2eda9d0 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -42,70 +42,12 @@ pub fn add( /// Subtracts two variables, we only support variables that are of length 1. pub fn sub( compiler: &mut CircuitWriter, - const_cell_lhs: &ConstOrCell, - const_cell_rhs: &ConstOrCell, + lhs: &ConstOrCell, + rhs: &ConstOrCell, span: Span, ) -> Var { - let zero = B::Field::zero(); - let one = B::Field::one(); - - match (const_cell_lhs, const_cell_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)) => { - let neg_rhs = field::neg(compiler, const_cell_rhs, span); - field::add(compiler, const_cell_lhs, &neg_rhs.cvars[0], span) - } - } + let neg_rhs = neg(compiler, rhs, span); + add(compiler, lhs, &neg_rhs.cvars[0], span) } /// Multiplies two field elements From 654dda32ad84b47f8a4b740dc9cdef44e205a63c Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 08:10:22 +0000 Subject: [PATCH 10/27] refactor if_else constraint --- examples/if_else.asm | 8 ++++++-- src/constraints/field.rs | 23 +++++------------------ 2 files changed, 11 insertions(+), 20 deletions(-) diff --git a/examples/if_else.asm b/examples/if_else.asm index edc91994e..76976532e 100644 --- a/examples/if_else.asm +++ b/examples/if_else.asm @@ -12,6 +12,8 @@ DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,1,-1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> DoubleGeneric<1,0,0,0,-2> (0,0) -> (1,0) -> (3,1) -> (7,0) -> (9,0) (1,2) -> (8,0) @@ -22,5 +24,7 @@ DoubleGeneric<1,0,0,0,-2> (7,2) -> (8,1) (8,2) -> (11,1) (9,2) -> (10,1) -(10,0) -> (12,0) -(10,2) -> (11,2) +(10,0) -> (14,0) +(10,2) -> (12,0) +(11,2) -> (13,0) +(12,2) -> (13,1) diff --git a/src/constraints/field.rs b/src/constraints/field.rs index ca2eda9d0..5d415d73b 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -336,25 +336,12 @@ 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(); + let then_m_else = sub(compiler, then_, else_, span)[0]; + let res_m_else = sub(compiler, &ConstOrCell::::Cell(res), else_, span)[0]; - 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, - ); + // constraint for ternary operator: cond * (then - else) = res - else + let res_mul = mul(compiler, cond, &then_m_else, span)[0]; + sub(compiler, &res_mul, &res_m_else, span); Var::new_var(res, span) } From 1dd5684bf80a8058a89d4c43581b1a7b4c162b15 Mon Sep 17 00:00:00 2001 From: kata Date: Mon, 22 Apr 2024 08:33:50 +0000 Subject: [PATCH 11/27] refactor equal_cells --- examples/equals.asm | 46 +++++++++++++++++++++++++------------- examples/if_else.asm | 38 ++++++++++++++++++------------- src/constraints/field.rs | 48 +++++++--------------------------------- 3 files changed, 62 insertions(+), 70 deletions(-) diff --git a/examples/equals.asm b/examples/equals.asm index 41dd7602e..d50f23dbd 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,0,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> DoubleGeneric<0,-1,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,0,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<0,0,-1,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,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) +(0,0) -> (2,0) -> (12,0) +(1,0) -> (3,0) +(2,2) -> (3,1) +(3,2) -> (6,1) -> (7,1) +(4,0) -> (6,0) -> (10,1) +(4,2) -> (5,0) +(5,2) -> (8,0) +(7,2) -> (9,0) +(8,2) -> (9,1) +(11,0) -> (13,0) +(12,2) -> (13,1) +(13,2) -> (16,1) -> (17,1) +(14,0) -> (16,0) -> (20,1) +(14,2) -> (15,0) +(15,2) -> (18,0) +(17,2) -> (19,0) +(18,2) -> (19,1) diff --git a/examples/if_else.asm b/examples/if_else.asm index 76976532e..8afbb8870 100644 --- a/examples/if_else.asm +++ b/examples/if_else.asm @@ -3,10 +3,14 @@ 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,0,1> +DoubleGeneric<1,1,-1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1,0,1> +DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> @@ -15,16 +19,20 @@ DoubleGeneric<0,0,-1,1> DoubleGeneric<1,0,1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,0,0,-2> -(0,0) -> (1,0) -> (3,1) -> (7,0) -> (9,0) -(1,2) -> (8,0) -(2,0) -> (3,0) -(3,2) -> (5,1) -> (6,1) -(4,0) -> (6,2) -(4,1) -> (5,0) -> (11,0) -(7,2) -> (8,1) -(8,2) -> (11,1) +(0,0) -> (1,0) -> (3,0) -> (11,0) -> (13,0) +(1,2) -> (12,0) +(2,0) -> (4,0) +(3,2) -> (4,1) +(4,2) -> (7,1) -> (8,1) +(5,0) -> (7,0) -> (15,0) +(5,2) -> (6,0) +(6,2) -> (9,0) +(8,2) -> (10,0) (9,2) -> (10,1) -(10,0) -> (14,0) -(10,2) -> (12,0) -(11,2) -> (13,0) -(12,2) -> (13,1) +(11,2) -> (12,1) +(12,2) -> (15,1) +(13,2) -> (14,1) +(14,0) -> (18,0) +(14,2) -> (16,0) +(15,2) -> (17,0) +(16,2) -> (17,1) diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 5d415d73b..acfad0097 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -170,55 +170,23 @@ 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 diff = sub(compiler, &ConstOrCell::Cell(x2), &ConstOrCell::Cell(x1), span)[0]; // 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 one_minus_res = sub(compiler, &ConstOrCell::Const(one), &ConstOrCell::Cell(res), span)[0]; // 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 = mul(compiler, &ConstOrCell::Cell(res), &diff, span)[0]; + // ensure that res * diff = 0 + sub(compiler, &res_mul_diff, &ConstOrCell::Const(zero), span); // 4. diff_inv * diff = one_minus_res let diff_inv = compiler .backend - .new_internal_var(Value::Inverse(diff), span); + .new_internal_var(Value::Inverse(*diff.cvar().unwrap()), 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 = mul(compiler, &ConstOrCell::Cell(diff_inv), &diff, span)[0]; + sub(compiler, &diff_inv_mul_diff, &one_minus_res, span); Var::new_var(res, span) } From eeaf71a54de6a674bcdd7a6142b0aff1a330a986 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 03:07:07 +0000 Subject: [PATCH 12/27] add backend interfaces for assert eq constraints --- src/backends/kimchi/mod.rs | 35 +++++++++++++++++++++++++++++++++++ src/backends/mod.rs | 16 ++++++++++++++++ src/stdlib/mod.rs | 35 +++++------------------------------ 3 files changed, 56 insertions(+), 30 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 8c9fc5b3d..e095f4a67 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -693,4 +693,39 @@ impl Backend for KimchiVesta { } } } + + fn constraint_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 constraint_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, + ); + } } diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 7522d3fd6..3e55037a0 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -58,6 +58,22 @@ pub trait Backend: Clone { span: Span, ) -> ConstOrCell; + /// add a constraint to assert a var equals a constant + fn constraint_eq_const( + &mut self, + var: &CellVar, + cst: Self::Field, + span: Span, + ); + + /// add a constraint to assert a var equals another var + fn constraint_eq_var( + &mut self, + lhs: &CellVar, + rhs: &CellVar, + span: Span, + ); + /// 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( diff --git a/src/stdlib/mod.rs b/src/stdlib/mod.rs index 4f336012c..5774d31d6 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.constraint_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.constraint_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.constraint_eq_const(cvar, one, span); } } From ba9233e564523b50f3c82998f34010fd50fdf871 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 03:12:17 +0000 Subject: [PATCH 13/27] fix: under-constraint --- src/constraints/field.rs | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/constraints/field.rs b/src/constraints/field.rs index acfad0097..ef4f0ae60 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -169,6 +169,7 @@ fn equal_cells( span, ); + // todo: replace these front end constraints with backend constraints // 1. diff = x2 - x1 let diff = sub(compiler, &ConstOrCell::Cell(x2), &ConstOrCell::Cell(x1), span)[0]; @@ -178,7 +179,9 @@ fn equal_cells( // 3. res * diff = 0 let res_mul_diff = mul(compiler, &ConstOrCell::Cell(res), &diff, span)[0]; // ensure that res * diff = 0 - sub(compiler, &res_mul_diff, &ConstOrCell::Const(zero), span); + compiler + .backend + .constraint_eq_const(res_mul_diff.cvar().unwrap(), zero, span); // 4. diff_inv * diff = one_minus_res let diff_inv = compiler @@ -186,7 +189,12 @@ fn equal_cells( .new_internal_var(Value::Inverse(*diff.cvar().unwrap()), span); let diff_inv_mul_diff = mul(compiler, &ConstOrCell::Cell(diff_inv), &diff, span)[0]; - sub(compiler, &diff_inv_mul_diff, &one_minus_res, span); + // ensure that diff_inv * diff = one_minus_res + compiler.backend.constraint_eq_var( + diff_inv_mul_diff.cvar().unwrap(), + one_minus_res.cvar().unwrap(), + span, + ); Var::new_var(res, span) } From e2ad54ccb92834ea464ffdd03ca3a93794776cfe Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 03:12:50 +0000 Subject: [PATCH 14/27] test: update asm --- examples/bool.asm | 8 ++++---- examples/equals.asm | 32 ++++++++++++++++---------------- examples/if_else.asm | 12 ++++++------ 3 files changed, 26 insertions(+), 26 deletions(-) diff --git a/examples/bool.asm b/examples/bool.asm index 37813cc6f..9ffbcf8fb 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -7,11 +7,11 @@ DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> DoubleGeneric<1,0,1> DoubleGeneric<1,0,-1,0,1> -DoubleGeneric<0,-1,0,0,1> -DoubleGeneric<0,-1,0,0,1> -(0,0) -> (1,0) -> (2,0) -> (8,1) +DoubleGeneric<1,0,0,0,-1> +DoubleGeneric<1,0,0,0,-1> +(0,0) -> (1,0) -> (2,0) -> (8,0) (1,2) -> (2,1) (3,0) -> (4,0) -> (5,0) (3,2) -> (4,1) (5,2) -> (6,0) -(6,2) -> (7,1) +(6,2) -> (7,0) diff --git a/examples/equals.asm b/examples/equals.asm index d50f23dbd..9255cd994 100644 --- a/examples/equals.asm +++ b/examples/equals.asm @@ -7,34 +7,34 @@ DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,0,1> -DoubleGeneric<1,1,-1> -DoubleGeneric<0,-1,0,0,1> +DoubleGeneric<1,-1> +DoubleGeneric<1,0,0,0,-1> DoubleGeneric<1,0,0,0,-3> DoubleGeneric<1,0,1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,0,1> -DoubleGeneric<1,1,-1> -DoubleGeneric<0,-1,0,0,1> +DoubleGeneric<1,-1> +DoubleGeneric<1,0,0,0,-1> (0,0) -> (2,0) -> (12,0) (1,0) -> (3,0) (2,2) -> (3,1) -(3,2) -> (6,1) -> (7,1) -(4,0) -> (6,0) -> (10,1) +(3,2) -> (6,1) -> (8,1) +(4,0) -> (6,0) -> (10,0) (4,2) -> (5,0) -(5,2) -> (8,0) -(7,2) -> (9,0) -(8,2) -> (9,1) +(5,2) -> (9,1) +(6,2) -> (7,0) +(8,2) -> (9,0) (11,0) -> (13,0) (12,2) -> (13,1) -(13,2) -> (16,1) -> (17,1) -(14,0) -> (16,0) -> (20,1) +(13,2) -> (16,1) -> (18,1) +(14,0) -> (16,0) -> (20,0) (14,2) -> (15,0) -(15,2) -> (18,0) -(17,2) -> (19,0) -(18,2) -> (19,1) +(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 8afbb8870..b41fd2237 100644 --- a/examples/if_else.asm +++ b/examples/if_else.asm @@ -8,9 +8,9 @@ DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,0,-1,0,1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,0,1> -DoubleGeneric<1,1,-1> +DoubleGeneric<1,-1> DoubleGeneric<1,0,1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,1> @@ -23,12 +23,12 @@ DoubleGeneric<1,0,0,0,-2> (1,2) -> (12,0) (2,0) -> (4,0) (3,2) -> (4,1) -(4,2) -> (7,1) -> (8,1) +(4,2) -> (7,1) -> (9,1) (5,0) -> (7,0) -> (15,0) (5,2) -> (6,0) -(6,2) -> (9,0) -(8,2) -> (10,0) -(9,2) -> (10,1) +(6,2) -> (10,1) +(7,2) -> (8,0) +(9,2) -> (10,0) (11,2) -> (12,1) (12,2) -> (15,1) (13,2) -> (14,1) From 01b0ebf655daba50d821ecf3d9a7de902acaa9e8 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 03:34:22 +0000 Subject: [PATCH 15/27] rename constraint interface --- src/backends/kimchi/mod.rs | 6 +++--- src/backends/mod.rs | 6 +++--- src/constraints/field.rs | 6 +++--- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index e095f4a67..d1162bc67 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -547,7 +547,7 @@ impl Backend for KimchiVesta { res } - fn enforce_neg_constraint( + fn constraint_neg( &mut self, var: &crate::var::ConstOrCell, span: Span, @@ -574,7 +574,7 @@ impl Backend for KimchiVesta { } } - fn enforce_add_constraint( + fn constraint_add( &mut self, lhs: &crate::var::ConstOrCell, rhs: &crate::var::ConstOrCell, @@ -635,7 +635,7 @@ impl Backend for KimchiVesta { } } - fn enforce_mul_constraint( + fn constraint_mul( &mut self, lhs: &crate::var::ConstOrCell, rhs: &crate::var::ConstOrCell, diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 3e55037a0..7d0cf9879 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -36,14 +36,14 @@ pub trait Backend: Clone { fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar; /// basic constraint negation - fn enforce_neg_constraint( + fn constraint_neg( &mut self, var: &ConstOrCell, span: Span, ) -> ConstOrCell; /// basic constraint addition - fn enforce_add_constraint( + fn constraint_add( &mut self, lhs: &ConstOrCell, rhs: &ConstOrCell, @@ -51,7 +51,7 @@ pub trait Backend: Clone { ) -> ConstOrCell; /// basic constraint multiplication - fn enforce_mul_constraint( + fn constraint_mul( &mut self, lhs: &ConstOrCell, rhs: &ConstOrCell, diff --git a/src/constraints/field.rs b/src/constraints/field.rs index ef4f0ae60..add8704e9 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -18,7 +18,7 @@ pub fn neg( cvar: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.enforce_neg_constraint(cvar, span); + let res = compiler.backend.constraint_neg(cvar, span); match res { ConstOrCell::Const(cst) => Var::new_constant(cst, span), ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), @@ -32,7 +32,7 @@ pub fn add( rhs: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.enforce_add_constraint(lhs, rhs, span); + let res = compiler.backend.constraint_add(lhs, rhs, span); match res { ConstOrCell::Const(cst) => Var::new_constant(cst, span), ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), @@ -57,7 +57,7 @@ pub fn mul( rhs: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.enforce_mul_constraint(lhs, rhs, span); + let res = compiler.backend.constraint_mul(lhs, rhs, span); match res { ConstOrCell::Const(cst) => Var::new_constant(cst, span), ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), From 76e43c99d96a65e881b354e346e55bb55bb205e7 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 03:47:19 +0000 Subject: [PATCH 16/27] refactor args for neg interface --- src/backends/kimchi/mod.rs | 37 ++++++++++++++++--------------------- src/backends/mod.rs | 4 ++-- src/constraints/field.rs | 10 ++++++---- 3 files changed, 24 insertions(+), 27 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index d1162bc67..6009c009c 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -549,29 +549,24 @@ impl Backend for KimchiVesta { fn constraint_neg( &mut self, - var: &crate::var::ConstOrCell, + var: &CellVar, span: Span, - ) -> crate::var::ConstOrCell { - match var { - crate::var::ConstOrCell::Const(ff) => crate::var::ConstOrCell::Const(ff.neg()), - crate::var::ConstOrCell::Cell(var) => { - 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), None, Some(neg_var)], - vec![one, zero, one], - span, - ); + ) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); - crate::var::ConstOrCell::Cell(neg_var) - } - } + 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), None, Some(neg_var)], + vec![one, zero, one], + span, + ); + + neg_var } fn constraint_add( diff --git a/src/backends/mod.rs b/src/backends/mod.rs index 7d0cf9879..e5d7f0e78 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -38,9 +38,9 @@ pub trait Backend: Clone { /// basic constraint negation fn constraint_neg( &mut self, - var: &ConstOrCell, + var: &CellVar, span: Span, - ) -> ConstOrCell; + ) -> CellVar; /// basic constraint addition fn constraint_add( diff --git a/src/constraints/field.rs b/src/constraints/field.rs index add8704e9..be5b0a138 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -18,10 +18,12 @@ pub fn neg( cvar: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.constraint_neg(cvar, span); - match res { - ConstOrCell::Const(cst) => Var::new_constant(cst, span), - ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), + match cvar { + crate::var::ConstOrCell::Const(ff) => Var::new_constant(ff.neg(), span), + crate::var::ConstOrCell::Cell(var) => { + let res = compiler.backend.constraint_neg(var, span); + Var::new_var(res, span) + } } } From 70c8358e97b6ccc1ffae5e8529c36b81089441d2 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 04:04:22 +0000 Subject: [PATCH 17/27] refactor args for add interface --- src/backends/kimchi/mod.rs | 89 ++++++++++++++++++-------------------- src/backends/mod.rs | 16 +++++-- src/constraints/field.rs | 26 +++++++++-- 3 files changed, 75 insertions(+), 56 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 6009c009c..1562afe7c 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -571,63 +571,56 @@ impl Backend for KimchiVesta { fn constraint_add( &mut self, - lhs: &crate::var::ConstOrCell, - rhs: &crate::var::ConstOrCell, + lhs: &CellVar, + rhs: &CellVar, span: Span, - ) -> crate::var::ConstOrCell { + ) -> CellVar { let zero = Self::Field::zero(); let one = Self::Field::one(); - match (lhs, rhs) { - // 2 constants - (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { - ConstOrCell::Const(*lhs + *rhs) - } - - // const and a var - (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) - | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { - // if the constant is zero, we can ignore this gate - if cst.is_zero() { - return ConstOrCell::Cell(*cvar); - } + // 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 new variable to store the result - let res = self - .new_internal_var(Value::LinearCombination(vec![(one, *cvar)], *cst), 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, + ); - // 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(*cvar), None, Some(res)], - vec![one, zero, one.neg(), zero, *cst], - span, - ); + res + } - ConstOrCell::Cell(res) - } - (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = self.new_internal_var( - Value::LinearCombination( - vec![(Self::Field::one(), *lhs), (Self::Field::one(), *rhs)], - Self::Field::zero(), - ), - span, - ); + fn constraint_add_const( + &mut self, + var: &CellVar, + cst: &Self::Field, + span: Span, + ) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); - // create a gate to store the result - self.add_generic_gate( - "add two variables together", - vec![Some(*lhs), Some(*rhs), Some(res)], - vec![Self::Field::one(), Self::Field::one(), Self::Field::one().neg()], - span, - ); + // 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, + ); - ConstOrCell::Cell(res) - } - } + res } fn constraint_mul( diff --git a/src/backends/mod.rs b/src/backends/mod.rs index e5d7f0e78..b6365da4a 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -42,13 +42,21 @@ pub trait Backend: Clone { span: Span, ) -> CellVar; - /// basic constraint addition + /// add a constraint to assert two vars are added together fn constraint_add( &mut self, - lhs: &ConstOrCell, - rhs: &ConstOrCell, + lhs: &CellVar, + rhs: &CellVar, span: Span, - ) -> ConstOrCell; + ) -> CellVar; + + /// add a constraint to assert a var is added to a constant + fn constraint_add_const( + &mut self, + var: &CellVar, + cst: &Self::Field, + span: Span, + ) -> CellVar; /// basic constraint multiplication fn constraint_mul( diff --git a/src/constraints/field.rs b/src/constraints/field.rs index be5b0a138..82503af93 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -34,10 +34,28 @@ pub fn add( rhs: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.constraint_add(lhs, rhs, span); - match res { - ConstOrCell::Const(cst) => Var::new_constant(cst, span), - ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), + match (lhs, rhs) { + // 2 constants + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { + Var::new_constant(*lhs + *rhs, span) + } + + // const and a var + (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) + | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { + // if the constant is zero, we can ignore this gate + if cst.is_zero() { + return Var::new_var(*cvar, span); + } + + let res = compiler.backend.constraint_add_const(cvar, cst, span); + + Var::new_var(res, span) + } + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { + let res = compiler.backend.constraint_add(lhs, rhs, span); + Var::new_var(res, span) + } } } From 314422c429f9367a35a6b63e9dc7921fafa3d9b1 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 04:22:46 +0000 Subject: [PATCH 18/27] refactor args for mul interface --- src/backends/kimchi/mod.rs | 84 ++++++++++++++++---------------------- src/backends/mod.rs | 16 ++++++-- src/constraints/field.rs | 31 ++++++++++++-- 3 files changed, 75 insertions(+), 56 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 1562afe7c..38a7af602 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -610,7 +610,7 @@ impl Backend for KimchiVesta { // 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( @@ -625,61 +625,49 @@ impl Backend for KimchiVesta { fn constraint_mul( &mut self, - lhs: &crate::var::ConstOrCell, - rhs: &crate::var::ConstOrCell, + lhs: &CellVar, + rhs: &CellVar, span: Span, - ) -> crate::var::ConstOrCell { + ) -> CellVar { let zero = Self::Field::zero(); let one = Self::Field::one(); - match (lhs, rhs) { - // 2 constants - (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => ConstOrCell::Const(*lhs * *rhs), - - // const and a var - (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) - | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { - // if the constant is zero, we can ignore this gate - if cst.is_zero() { - let zero = self.add_constant( - Some("encoding zero for the result of 0 * var"), - Self::Field::zero(), - span, - ); - return ConstOrCell::Cell(zero); - } - - // create a new variable to store the result - let res = self.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 - self.add_generic_gate( - "add a constant with a variable", - vec![Some(*cvar), None, Some(res)], - vec![*cst, zero, one.neg(), zero, *cst], - span, - ); + // create a new variable to store the result + let res = self.new_internal_var(Value::Mul(*lhs, *rhs), span); - ConstOrCell::Cell(res) - } + // 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 + } - // everything is a var - (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { - // create a new variable to store the result - let res = self.new_internal_var(Value::Mul(*lhs, *rhs), span); + fn constraint_mul_const( + &mut self, + var: &CellVar, + cst: &Self::Field, + span: Span, + ) -> CellVar { + let zero = Self::Field::zero(); + let one = Self::Field::one(); - // 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, - ); + // create a new variable to store the result + let res = self.new_internal_var(Value::Scale(*cst, *var), span); - ConstOrCell::Cell(res) - } - } + // 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 constraint_eq_const( diff --git a/src/backends/mod.rs b/src/backends/mod.rs index b6365da4a..c1b04a63d 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -58,13 +58,21 @@ pub trait Backend: Clone { span: Span, ) -> CellVar; - /// basic constraint multiplication + /// add a constraint to assert a var is multiplied by another var fn constraint_mul( &mut self, - lhs: &ConstOrCell, - rhs: &ConstOrCell, + lhs: &CellVar, + rhs: &CellVar, span: Span, - ) -> ConstOrCell; + ) -> CellVar; + + /// add a constraint to assert a var is multiplied by a constant + fn constraint_mul_const( + &mut self, + var: &CellVar, + cst: &Self::Field, + span: Span, + ) -> CellVar; /// add a constraint to assert a var equals a constant fn constraint_eq_const( diff --git a/src/constraints/field.rs b/src/constraints/field.rs index 82503af93..56ad00469 100644 --- a/src/constraints/field.rs +++ b/src/constraints/field.rs @@ -77,10 +77,33 @@ pub fn mul( rhs: &ConstOrCell, span: Span, ) -> Var { - let res = compiler.backend.constraint_mul(lhs, rhs, span); - match res { - ConstOrCell::Const(cst) => Var::new_constant(cst, span), - ConstOrCell::Cell(cvar) => Var::new_var(cvar, span), + match (lhs, rhs) { + // 2 constants + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs * *rhs, span), + + // const and a var + (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) + | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { + // if the constant is zero, we can ignore this gate + // todo: do we really need this? + 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); + } + + let res = compiler.backend.constraint_mul_const(cvar, cst, span); + Var::new_var(res, span) + } + + // everything is a var + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { + let res = compiler.backend.constraint_mul(lhs, rhs, span); + Var::new_var(res, span) + } } } From 7efa2ab38e900d0d6b61967fd52e145cc932e30b Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 06:05:25 +0000 Subject: [PATCH 19/27] refactor check fn --- examples/bool.asm | 16 ++++++++++------ src/constraints/boolean.rs | 7 ++++--- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/examples/bool.asm b/examples/bool.asm index 9ffbcf8fb..83df0c384 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -1,17 +1,21 @@ @ noname.0.7.0 DoubleGeneric<1> -DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<1,0,-1,0,-1> DoubleGeneric<0,0,-1,1> -DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<1> +DoubleGeneric<1,0,-1,0,-1> DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<1,0,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) -> (8,0) +(0,0) -> (1,0) -> (2,0) -> (10,0) (1,2) -> (2,1) -(3,0) -> (4,0) -> (5,0) -(3,2) -> (4,1) +(2,2) -> (3,0) +(4,0) -> (5,0) -> (7,0) +(4,2) -> (5,1) (5,2) -> (6,0) -(6,2) -> (7,0) +(7,2) -> (8,0) +(8,2) -> (9,0) diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index d43a2093c..efbadcaff 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -22,10 +22,11 @@ pub fn check(compiler: &mut CircuitWriter, xx: &ConstOrCell assert!(is_valid(*ff)), - ConstOrCell::Cell(_) => { + ConstOrCell::Cell(var) => { // x * (x - 1) - let x_1 = field::sub(compiler, xx, &ConstOrCell::Const(one.neg()), span); - field::mul(compiler, xx, &x_1.cvars[0], span); + let x_1 = compiler.backend.constraint_add_const(var, &one.neg(), span); + let res = compiler.backend.constraint_mul(var, &x_1, span); + compiler.backend.constraint_eq_const(&res, B::Field::zero(), span); }, }; } From 4378fc1709e54dd2a2c76c1c373c8a372f2ad360 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 06:24:50 +0000 Subject: [PATCH 20/27] refactor: and operation --- src/constraints/boolean.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index efbadcaff..86aa1e313 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -52,10 +52,14 @@ pub fn and( } // two vars - (ConstOrCell::Cell(_), ConstOrCell::Cell(_)) => { - // todo: should it check if the vars are either 1 or 0? + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { // lhs * rhs - field::mul(compiler, lhs, rhs, span) + let res = compiler.backend.constraint_mul(lhs, rhs, span); + + // check if it is either 1 or 0 + check(compiler, &ConstOrCell::Cell(res), span); + + Var::new_var(res, span) } } } From bff163fb23bcfa85101476147ecc1c72ae0435c1 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 06:42:56 +0000 Subject: [PATCH 21/27] refactor: not operation --- examples/bool.asm | 9 +++++++-- src/constraints/boolean.rs | 16 ++++++++++------ 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/examples/bool.asm b/examples/bool.asm index 83df0c384..2e8894c83 100644 --- a/examples/bool.asm +++ b/examples/bool.asm @@ -9,13 +9,18 @@ DoubleGeneric<0,0,-1,1> DoubleGeneric<1> DoubleGeneric<1,0,1> DoubleGeneric<1,0,-1,0,1> +DoubleGeneric<1,0,-1,0,-1> +DoubleGeneric<0,0,-1,1> +DoubleGeneric<1> DoubleGeneric<1,0,0,0,-1> DoubleGeneric<1,0,0,0,-1> -(0,0) -> (1,0) -> (2,0) -> (10,0) +(0,0) -> (1,0) -> (2,0) -> (13,0) (1,2) -> (2,1) (2,2) -> (3,0) (4,0) -> (5,0) -> (7,0) (4,2) -> (5,1) (5,2) -> (6,0) (7,2) -> (8,0) -(8,2) -> (9,0) +(8,2) -> (9,0) -> (10,0) -> (12,0) +(9,2) -> (10,1) +(10,2) -> (11,0) diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index 86aa1e313..6a27801c2 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -11,7 +11,7 @@ use crate::{ var::{ConstOrCell, Value, Var}, }; -use super::field; +use super::field::{self, sub}; pub fn is_valid(f: F) -> bool { f.is_one() || f.is_zero() @@ -79,13 +79,17 @@ pub fn not( Var::new_constant(value, span) } - - // constant and a var - ConstOrCell::Cell(_) => { - let one = B::Field::one(); + ConstOrCell::Cell(var) => { + let one = ConstOrCell::Const(B::Field::one()); + let var = ConstOrCell::Cell(*var); // 1 - x - field::sub(compiler, &ConstOrCell::Const(one), var, span) + let res = field::sub(compiler, &one, &var, span)[0]; + + // ensure it is either 1 or 0 + check(compiler, &res, span); + + Var::new_cvar(res, span) } } } From f5fe05e5d80532c47d09762863f3b7ff9e360c03 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 08:12:41 +0000 Subject: [PATCH 22/27] add backend constraint for inputs and outputs --- src/backends/kimchi/mod.rs | 31 +++++++++++++++++++++++++++++++ src/backends/mod.rs | 6 ++++++ src/circuit_writer/writer.rs | 27 ++------------------------- 3 files changed, 39 insertions(+), 25 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 38a7af602..3273cb4aa 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -704,4 +704,35 @@ impl Backend for KimchiVesta { span, ); } + + fn constraint_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, + ); + + cvar + } + + fn constraint_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, + ); + + cvar + } } diff --git a/src/backends/mod.rs b/src/backends/mod.rs index c1b04a63d..de7190553 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -118,6 +118,12 @@ pub trait Backend: Clone { span: Span, ); + /// Add a constraint for a public input + fn constraint_public_input(&mut self, val: Value, span: Span) -> CellVar; + + /// Add a constraint for a public output + fn constraint_public_output(&mut self, val: Value, span: Span) -> CellVar; + /// 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. diff --git a/src/circuit_writer/writer.rs b/src/circuit_writer/writer.rs index 0045d99c7..d5f473f05 100644 --- a/src/circuit_writer/writer.rs +++ b/src/circuit_writer/writer.rs @@ -697,20 +697,8 @@ 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); + let cvar = self.backend.constraint_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; @@ -723,19 +711,8 @@ 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); + let cvar = self.backend.constraint_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; From e4cd10f5cd112a8b66488af61c61162d2c12efbb Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 08:42:59 +0000 Subject: [PATCH 23/27] revert test --- examples/arithmetic.asm | 8 +------- examples/arithmetic.no | 3 --- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/examples/arithmetic.asm b/examples/arithmetic.asm index 0b05313e3..2c926b97f 100644 --- a/examples/arithmetic.asm +++ b/examples/arithmetic.asm @@ -3,11 +3,5 @@ DoubleGeneric<1> DoubleGeneric<1,1,-1> DoubleGeneric<1,0,0,0,-2> -DoubleGeneric<1,0,1> -DoubleGeneric<1,1,-1> -DoubleGeneric<1> -(0,0) -> (1,1) -> (3,0) -(1,0) -> (4,0) +(0,0) -> (1,1) (1,2) -> (2,0) -(3,2) -> (4,1) -(4,2) -> (5,0) diff --git a/examples/arithmetic.no b/examples/arithmetic.no index fbb3cda48..29199551e 100644 --- a/examples/arithmetic.no +++ b/examples/arithmetic.no @@ -1,7 +1,4 @@ fn main(pub public_input: Field, private_input: Field) { let xx = private_input + public_input; assert_eq(xx, 2); - - let yy = private_input - public_input; - assert_eq(yy, 0); } From 4b004b2ee572aa706e66f2cf27eebede83e68308 Mon Sep 17 00:00:00 2001 From: kata Date: Tue, 23 Apr 2024 08:58:21 +0000 Subject: [PATCH 24/27] fmt --- src/backends/kimchi/mod.rs | 72 +++++++++--------------------------- src/backends/mod.rs | 48 ++++-------------------- src/circuit_writer/writer.rs | 8 +++- src/constraints/boolean.rs | 6 ++- src/constraints/field.rs | 19 +++++++--- 5 files changed, 48 insertions(+), 105 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 3273cb4aa..875968a8c 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -547,11 +547,7 @@ impl Backend for KimchiVesta { res } - fn constraint_neg( - &mut self, - var: &CellVar, - span: Span, - ) -> CellVar { + fn constraint_neg(&mut self, var: &CellVar, span: Span) -> CellVar { let zero = Self::Field::zero(); let one = Self::Field::one(); @@ -565,25 +561,17 @@ impl Backend for KimchiVesta { vec![one, zero, one], span, ); - + neg_var } - fn constraint_add( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ) -> CellVar { + fn constraint_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, - ), + Value::LinearCombination(vec![(one, *lhs), (one, *rhs)], zero), span, ); @@ -598,18 +586,12 @@ impl Backend for KimchiVesta { res } - fn constraint_add_const( - &mut self, - var: &CellVar, - cst: &Self::Field, - span: Span, - ) -> CellVar { + fn constraint_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); + 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 @@ -623,12 +605,7 @@ impl Backend for KimchiVesta { res } - fn constraint_mul( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ) -> CellVar { + fn constraint_mul(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar { let zero = Self::Field::zero(); let one = Self::Field::one(); @@ -642,16 +619,11 @@ impl Backend for KimchiVesta { vec![zero, zero, one.neg(), one], span, ); - + res } - fn constraint_mul_const( - &mut self, - var: &CellVar, - cst: &Self::Field, - span: Span, - ) -> CellVar { + fn constraint_mul_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar { let zero = Self::Field::zero(); let one = Self::Field::one(); @@ -666,16 +638,11 @@ impl Backend for KimchiVesta { vec![*cst, zero, one.neg()], span, ); - + res } - - fn constraint_eq_const( - &mut self, - cvar: &CellVar, - cst: Self::Field, - span: Span, - ) { + + fn constraint_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)], @@ -689,13 +656,8 @@ impl Backend for KimchiVesta { span, ); } - - fn constraint_eq_var( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ) { + + fn constraint_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", @@ -704,7 +666,7 @@ impl Backend for KimchiVesta { span, ); } - + fn constraint_public_input(&mut self, val: Value, span: Span) -> CellVar { // create the var let cvar = self.new_internal_var(val, span); @@ -717,10 +679,10 @@ impl Backend for KimchiVesta { vec![Self::Field::one()], span, ); - + cvar } - + fn constraint_public_output(&mut self, val: Value, span: Span) -> CellVar { // create the var let cvar = self.new_internal_var(val, span); diff --git a/src/backends/mod.rs b/src/backends/mod.rs index de7190553..a80eb44e5 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -36,59 +36,25 @@ pub trait Backend: Clone { fn new_internal_var(&mut self, val: Value, span: Span) -> CellVar; /// basic constraint negation - fn constraint_neg( - &mut self, - var: &CellVar, - span: Span, - ) -> CellVar; + fn constraint_neg(&mut self, var: &CellVar, span: Span) -> CellVar; /// add a constraint to assert two vars are added together - fn constraint_add( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ) -> CellVar; + fn constraint_add(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar; /// add a constraint to assert a var is added to a constant - fn constraint_add_const( - &mut self, - var: &CellVar, - cst: &Self::Field, - span: Span, - ) -> CellVar; + fn constraint_add_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar; /// add a constraint to assert a var is multiplied by another var - fn constraint_mul( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ) -> CellVar; + fn constraint_mul(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar; /// add a constraint to assert a var is multiplied by a constant - fn constraint_mul_const( - &mut self, - var: &CellVar, - cst: &Self::Field, - span: Span, - ) -> CellVar; + fn constraint_mul_const(&mut self, var: &CellVar, cst: &Self::Field, span: Span) -> CellVar; /// add a constraint to assert a var equals a constant - fn constraint_eq_const( - &mut self, - var: &CellVar, - cst: Self::Field, - span: Span, - ); + fn constraint_eq_const(&mut self, var: &CellVar, cst: Self::Field, span: Span); /// add a constraint to assert a var equals another var - fn constraint_eq_var( - &mut self, - lhs: &CellVar, - rhs: &CellVar, - span: Span, - ); + fn constraint_eq_var(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span); /// 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. diff --git a/src/circuit_writer/writer.rs b/src/circuit_writer/writer.rs index d5f473f05..36dc7ab29 100644 --- a/src/circuit_writer/writer.rs +++ b/src/circuit_writer/writer.rs @@ -697,7 +697,9 @@ impl CircuitWriter { let mut cvars = Vec::with_capacity(num); for idx in 0..num { - let cvar = self.backend.constraint_public_input(Value::External(name.clone(), idx), span); + let cvar = self + .backend + .constraint_public_input(Value::External(name.clone(), idx), span); cvars.push(ConstOrCell::Cell(cvar)); } @@ -711,7 +713,9 @@ impl CircuitWriter { let mut cvars = Vec::with_capacity(num); for _ in 0..num { - let cvar = self.backend.constraint_public_output(Value::PublicOutput(None), span); + let cvar = self + .backend + .constraint_public_output(Value::PublicOutput(None), span); cvars.push(ConstOrCell::Cell(cvar)); } self.public_input_size += num; diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs index 6a27801c2..9da440af3 100644 --- a/src/constraints/boolean.rs +++ b/src/constraints/boolean.rs @@ -26,8 +26,10 @@ pub fn check(compiler: &mut CircuitWriter, xx: &ConstOrCell( ) -> Var { match (lhs, rhs) { // 2 constants - (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { - Var::new_constant(*lhs + *rhs, span) - } + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs + *rhs, span), // const and a var (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) | (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); } @@ -214,10 +213,20 @@ fn equal_cells( // todo: replace these front end constraints with backend constraints // 1. diff = x2 - x1 - let diff = sub(compiler, &ConstOrCell::Cell(x2), &ConstOrCell::Cell(x1), span)[0]; + let diff = sub( + compiler, + &ConstOrCell::Cell(x2), + &ConstOrCell::Cell(x1), + span, + )[0]; // 2. one_minus_res = 1 - res - let one_minus_res = sub(compiler, &ConstOrCell::Const(one), &ConstOrCell::Cell(res), span)[0]; + let one_minus_res = sub( + compiler, + &ConstOrCell::Const(one), + &ConstOrCell::Cell(res), + span, + )[0]; // 3. res * diff = 0 let res_mul_diff = mul(compiler, &ConstOrCell::Cell(res), &diff, span)[0]; From cea6a714988cb450a6083828aa7507e635ccfd9a Mon Sep 17 00:00:00 2001 From: kata Date: Wed, 24 Apr 2024 01:52:25 +0000 Subject: [PATCH 25/27] move public_input_size to kimchi backend --- src/backends/kimchi/mod.rs | 15 +++++++++++---- src/backends/kimchi/prover.rs | 5 ++--- src/backends/mod.rs | 1 - src/circuit_writer/mod.rs | 6 +----- src/circuit_writer/writer.rs | 3 --- 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index 875968a8c..cb1504e82 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,6 +136,7 @@ impl KimchiVesta { pending_generic_gate: None, debug_info: vec![], finalized: false, + public_input_size: 0, } } } @@ -348,7 +352,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 +383,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 +427,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]); } @@ -680,6 +683,8 @@ impl Backend for KimchiVesta { span, ); + self.public_input_size += 1; + cvar } @@ -695,6 +700,8 @@ impl Backend for KimchiVesta { span, ); + self.public_input_size += 1; + cvar } } diff --git a/src/backends/kimchi/prover.rs b/src/backends/kimchi/prover.rs index bc7358afd..d70c3a7f8 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")?; @@ -131,7 +130,7 @@ impl CompiledCircuit { let (prover_index, verifier_index) = self .circuit .backend - .compile_to_indexes(self.circuit.public_input_size)?; + .compile_to_indexes()?; // wrap let prover_index = { ProverIndex { diff --git a/src/backends/mod.rs b/src/backends/mod.rs index a80eb44e5..ac46102b3 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -160,7 +160,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..7a578fc0b 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![], } @@ -244,6 +240,6 @@ impl CircuitWriter { witness_env: &mut WitnessEnv, ) -> Result { self.backend - .generate_witness(witness_env, self.public_input_size) + .generate_witness(witness_env) } } diff --git a/src/circuit_writer/writer.rs b/src/circuit_writer/writer.rs index 36dc7ab29..ddc4a64a2 100644 --- a/src/circuit_writer/writer.rs +++ b/src/circuit_writer/writer.rs @@ -703,8 +703,6 @@ impl CircuitWriter { cvars.push(ConstOrCell::Cell(cvar)); } - self.public_input_size += num; - Var::new(cvars, span) } @@ -718,7 +716,6 @@ impl CircuitWriter { .constraint_public_output(Value::PublicOutput(None), span); cvars.push(ConstOrCell::Cell(cvar)); } - self.public_input_size += num; // store it let res = Var::new(cvars, span); From a92fea91d3566febca21aad070540b4a1418082f Mon Sep 17 00:00:00 2001 From: kata Date: Wed, 24 Apr 2024 01:59:37 +0000 Subject: [PATCH 26/27] move add_gate and add_generic_gate to kimchi backend --- src/backends/kimchi/mod.rs | 100 +++++++++++++++++++------------------ src/backends/mod.rs | 19 ------- 2 files changed, 51 insertions(+), 68 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index cb1504e82..26f28e3ce 100644 --- a/src/backends/kimchi/mod.rs +++ b/src/backends/kimchi/mod.rs @@ -139,56 +139,8 @@ impl KimchiVesta { 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, @@ -242,6 +194,7 @@ impl Backend for KimchiVesta { } } + /// Add a generic double gate to the circuit fn add_generic_gate( &mut self, label: &'static str, @@ -280,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, diff --git a/src/backends/mod.rs b/src/backends/mod.rs index ac46102b3..afad70be5 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -65,25 +65,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, - ); - /// Add a constraint for a public input fn constraint_public_input(&mut self, val: Value, span: Span) -> CellVar; From 427f04eaf3209948c978663f142a6c001e7b0e21 Mon Sep 17 00:00:00 2001 From: kata Date: Wed, 24 Apr 2024 02:08:03 +0000 Subject: [PATCH 27/27] outdated note --- src/backends/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/backends/mod.rs b/src/backends/mod.rs index afad70be5..ed201e181 100644 --- a/src/backends/mod.rs +++ b/src/backends/mod.rs @@ -127,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,