Refactor for basic constraints

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)

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);
 }

examples/bool.asm

@@ -1,11 +1,17 @@
 @ 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>
+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) -> (8,1)
+(1,2) -> (2,1)
+(3,0) -> (4,0) -> (5,0)
 (3,2) -> (4,1)
+(5,2) -> (6,0)
+(6,2) -> (7,1)

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)

examples/if_else.asm

@@ -3,20 +3,36 @@
 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,-1,-1>
-DoubleGeneric<1,-1,-1>
+DoubleGeneric<1,0,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,1>
+DoubleGeneric<1,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) -> (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)
+(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)

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,
 };
 
@@ -546,4 +546,151 @@ impl Backend for KimchiVesta {
 
         res
     }
+
+    fn enforce_neg_constraint(
+        &mut self,
+        var: &crate::var::ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> crate::var::ConstOrCell<Self::Field> {
+        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,
+                );
+
+                crate::var::ConstOrCell::Cell(neg_var)
+            }
+        }
+    }
+
+    fn enforce_add_constraint(
+        &mut self,
+        lhs: &crate::var::ConstOrCell<Self::Field>,
+        rhs: &crate::var::ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> crate::var::ConstOrCell<Self::Field> {
+        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(
+        &mut self,
+        lhs: &crate::var::ConstOrCell<Self::Field>,
+        rhs: &crate::var::ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> crate::var::ConstOrCell<Self::Field> {
+        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)
+            }
+        }
+    }
 }

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,29 @@ pub trait Backend: Clone {
     /// It increments the variable index for look up later.
     fn new_internal_var(&mut self, val: Value<Self>, span: Span) -> CellVar;
 
+    /// basic constraint negation
+    fn enforce_neg_constraint(
+        &mut self,
+        var: &ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> ConstOrCell<Self::Field>;
+
+    /// basic constraint addition
+    fn enforce_add_constraint(
+        &mut self,
+        lhs: &ConstOrCell<Self::Field>,
+        rhs: &ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> ConstOrCell<Self::Field>;
+
+    /// basic constraint multiplication
+    fn enforce_mul_constraint(
+        &mut self,
+        lhs: &ConstOrCell<Self::Field>,
+        rhs: &ConstOrCell<Self::Field>,
+        span: Span,
+    ) -> ConstOrCell<Self::Field>;
+
     /// 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(