diff --git a/examples/bool.asm b/examples/bool.asm
index 053da8cc4..2e8894c83 100644
--- a/examples/bool.asm
+++ b/examples/bool.asm
@@ -1,11 +1,26 @@
 @ noname.0.7.0
 
 DoubleGeneric<1>
-DoubleGeneric<-1,0,0,1>
-DoubleGeneric<-1,0,0,1>
-DoubleGeneric<0,-1,-1,0,1>
-DoubleGeneric<0,-1,0,0,1>
-DoubleGeneric<0,-1,0,0,1>
-(0,0) -> (1,0) -> (1,1) -> (5,1)
-(2,0) -> (2,1) -> (3,1)
-(3,2) -> (4,1)
+DoubleGeneric<1,0,-1,0,-1>
+DoubleGeneric<0,0,-1,1>
+DoubleGeneric<1>
+DoubleGeneric<1,0,-1,0,-1>
+DoubleGeneric<0,0,-1,1>
+DoubleGeneric<1>
+DoubleGeneric<1,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) -> (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) -> (10,0) -> (12,0)
+(9,2) -> (10,1)
+(10,2) -> (11,0)
diff --git a/examples/equals.asm b/examples/equals.asm
index 41dd7602e..9255cd994 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,-1,0,0,1>
+DoubleGeneric<1>
+DoubleGeneric<0,0,-1,1>
+DoubleGeneric<1,-1>
+DoubleGeneric<1,0,0,0,-1>
 DoubleGeneric<1,0,0,0,-3>
-DoubleGeneric<1,-1,-1>
-DoubleGeneric<1,1,0,0,-1>
-DoubleGeneric<0,0,0,1>
+DoubleGeneric<1,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<0,-1,0,0,1>
-(0,0) -> (2,1) -> (8,1)
-(1,0) -> (2,0)
-(2,2) -> (4,1) -> (5,1)
-(3,0) -> (5,2)
-(3,1) -> (4,0) -> (6,1)
-(7,0) -> (8,0)
-(8,2) -> (10,1) -> (11,1)
-(9,0) -> (11,2)
-(9,1) -> (10,0) -> (12,1)
+DoubleGeneric<1,-1>
+DoubleGeneric<1,0,0,0,-1>
+(0,0) -> (2,0) -> (12,0)
+(1,0) -> (3,0)
+(2,2) -> (3,1)
+(3,2) -> (6,1) -> (8,1)
+(4,0) -> (6,0) -> (10,0)
+(4,2) -> (5,0)
+(5,2) -> (9,1)
+(6,2) -> (7,0)
+(8,2) -> (9,0)
+(11,0) -> (13,0)
+(12,2) -> (13,1)
+(13,2) -> (16,1) -> (18,1)
+(14,0) -> (16,0) -> (20,0)
+(14,2) -> (15,0)
+(15,2) -> (19,1)
+(16,2) -> (17,0)
+(18,2) -> (19,0)
diff --git a/examples/if_else.asm b/examples/if_else.asm
index 00d8d2e99..b41fd2237 100644
--- a/examples/if_else.asm
+++ b/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<1>
 DoubleGeneric<0,0,-1,1>
-DoubleGeneric<1,-1,-1>
-DoubleGeneric<1,-1,-1>
+DoubleGeneric<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) -> (9,1)
+(5,0) -> (7,0) -> (15,0)
+(5,2) -> (6,0)
+(6,2) -> (10,1)
+(7,2) -> (8,0)
+(9,2) -> (10,0)
+(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/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs
index efc139075..26f28e3ce 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,
 };
 
@@ -89,6 +89,9 @@ pub struct KimchiVesta {
     /// Once this is set, you can generate a witness (and can't modify the circuit?)
     // Note: I don't think we need this, but it acts as a nice redundant failsafe.
     pub(crate) finalized: bool,
+
+    /// Size of the public input.
+    pub(crate) public_input_size: usize,
 }
 
 impl Witness {
@@ -133,58 +136,11 @@ impl KimchiVesta {
             pending_generic_gate: None,
             debug_info: vec![],
             finalized: false,
+            public_input_size: 0,
         }
     }
-}
-
-impl Backend for KimchiVesta {
-    type Field = VestaField;
-    type GeneratedWitness = GeneratedWitness;
-
-    fn poseidon() -> crate::imports::FnHandle<Self> {
-        builtin::poseidon
-    }
-
-    fn witness_vars(&self) -> &HashMap<usize, Value<Self>> {
-        &self.witness_vars
-    }
-
-    fn new_internal_var(&mut self, val: Value<KimchiVesta>, span: Span) -> CellVar {
-        // create new var
-        let var = CellVar::new(self.next_variable, span);
-        self.next_variable += 1;
-
-        // store it in the circuit_writer
-        self.witness_vars.insert(var.index, val);
-
-        var
-    }
-
-    fn add_constant(
-        &mut self,
-        label: Option<&'static str>,
-        value: VestaField,
-        span: Span,
-    ) -> CellVar {
-        if let Some(cvar) = self.cached_constants.get(&value) {
-            return *cvar;
-        }
-
-        let var = self.new_internal_var(Value::Constant(value), span);
-        self.cached_constants.insert(value, var);
-
-        let zero = VestaField::zero();
-
-        let _ = &self.add_generic_gate(
-            label.unwrap_or("hardcode a constant"),
-            vec![Some(var)],
-            vec![VestaField::one(), zero, zero, zero, value.neg()],
-            span,
-        );
-
-        var
-    }
 
+    /// Add a gate to the circuit
     fn add_gate(
         &mut self,
         note: &'static str,
@@ -238,6 +194,7 @@ impl Backend for KimchiVesta {
         }
     }
 
+    /// Add a generic double gate to the circuit
     fn add_generic_gate(
         &mut self,
         label: &'static str,
@@ -276,6 +233,55 @@ impl Backend for KimchiVesta {
             });
         }
     }
+}
+
+impl Backend for KimchiVesta {
+    type Field = VestaField;
+    type GeneratedWitness = GeneratedWitness;
+
+    fn poseidon() -> crate::imports::FnHandle<Self> {
+        builtin::poseidon
+    }
+
+    fn witness_vars(&self) -> &HashMap<usize, Value<Self>> {
+        &self.witness_vars
+    }
+
+    fn new_internal_var(&mut self, val: Value<KimchiVesta>, span: Span) -> CellVar {
+        // create new var
+        let var = CellVar::new(self.next_variable, span);
+        self.next_variable += 1;
+
+        // store it in the circuit_writer
+        self.witness_vars.insert(var.index, val);
+
+        var
+    }
+
+    fn add_constant(
+        &mut self,
+        label: Option<&'static str>,
+        value: VestaField,
+        span: Span,
+    ) -> CellVar {
+        if let Some(cvar) = self.cached_constants.get(&value) {
+            return *cvar;
+        }
+
+        let var = self.new_internal_var(Value::Constant(value), span);
+        self.cached_constants.insert(value, var);
+
+        let zero = VestaField::zero();
+
+        let _ = &self.add_generic_gate(
+            label.unwrap_or("hardcode a constant"),
+            vec![Some(var)],
+            vec![VestaField::one(), zero, zero, zero, value.neg()],
+            span,
+        );
+
+        var
+    }
 
     fn finalize_circuit(
         &mut self,
@@ -348,7 +354,6 @@ impl Backend for KimchiVesta {
     fn generate_witness(
         &self,
         witness_env: &mut WitnessEnv<VestaField>,
-        public_input_size: usize,
     ) -> Result<GeneratedWitness> {
         if !self.finalized {
             unreachable!("the circuit must be finalized before generating a witness");
@@ -380,7 +385,7 @@ impl Backend for KimchiVesta {
             }
 
             // check if the row makes sense
-            let is_not_public_input = row >= public_input_size;
+            let is_not_public_input = row >= self.public_input_size;
             if is_not_public_input {
                 #[allow(clippy::single_match)]
                 match gate.typ {
@@ -424,9 +429,9 @@ impl Backend for KimchiVesta {
         }
 
         // extract full public input (containing the public output)
-        let mut full_public_inputs = Vec::with_capacity(public_input_size);
+        let mut full_public_inputs = Vec::with_capacity(self.public_input_size);
 
-        for witness_row in witness.iter().take(public_input_size) {
+        for witness_row in witness.iter().take(self.public_input_size) {
             full_public_inputs.push(witness_row[0]);
         }
 
@@ -546,4 +551,159 @@ impl Backend for KimchiVesta {
 
         res
     }
+
+    fn constraint_neg(&mut self, var: &CellVar, span: Span) -> CellVar {
+        let zero = Self::Field::zero();
+        let one = Self::Field::one();
+
+        let neg_var = self.new_internal_var(
+            Value::LinearCombination(vec![(one.neg(), *var)], zero),
+            span,
+        );
+        self.add_generic_gate(
+            "constraint to validate a negation (`x + (-x) = 0`)",
+            vec![Some(*var), None, Some(neg_var)],
+            vec![one, zero, one],
+            span,
+        );
+
+        neg_var
+    }
+
+    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),
+            span,
+        );
+
+        // create a gate to store the result
+        self.add_generic_gate(
+            "add two variables together",
+            vec![Some(*lhs), Some(*rhs), Some(res)],
+            vec![one, one, one.neg()],
+            span,
+        );
+
+        res
+    }
+
+    fn 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);
+
+        // create a gate to store the result
+        // TODO: we should use an add_generic function that takes advantage of the double generic gate
+        self.add_generic_gate(
+            "add a constant with a variable",
+            vec![Some(*var), None, Some(res)],
+            vec![one, zero, one.neg(), zero, *cst],
+            span,
+        );
+
+        res
+    }
+
+    fn constraint_mul(&mut self, lhs: &CellVar, rhs: &CellVar, span: Span) -> CellVar {
+        let zero = Self::Field::zero();
+        let one = Self::Field::one();
+
+        // create a new variable to store the result
+        let res = self.new_internal_var(Value::Mul(*lhs, *rhs), span);
+
+        // create a gate to store the result
+        self.add_generic_gate(
+            "add two variables together",
+            vec![Some(*lhs), Some(*rhs), Some(res)],
+            vec![zero, zero, one.neg(), one],
+            span,
+        );
+
+        res
+    }
+
+    fn 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 new variable to store the result
+        let res = self.new_internal_var(Value::Scale(*cst, *var), span);
+
+        // create a gate to store the result
+        // TODO: we should use an add_generic function that takes advantage of the double generic gate
+        self.add_generic_gate(
+            "add a constant with a variable",
+            vec![Some(*var), None, Some(res)],
+            vec![*cst, zero, one.neg()],
+            span,
+        );
+
+        res
+    }
+
+    fn 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,
+        );
+    }
+
+    fn constraint_public_input(&mut self, val: Value<Self>, span: Span) -> CellVar {
+        // create the var
+        let cvar = self.new_internal_var(val, span);
+
+        // create the associated generic gate
+        self.add_gate(
+            "add public input",
+            GateKind::DoubleGeneric,
+            vec![Some(cvar)],
+            vec![Self::Field::one()],
+            span,
+        );
+
+        self.public_input_size += 1;
+
+        cvar
+    }
+
+    fn constraint_public_output(&mut self, val: Value<Self>, span: Span) -> CellVar {
+        // create the var
+        let cvar = self.new_internal_var(val, span);
+
+        // create the associated generic gate
+        self.add_generic_gate(
+            "add public output",
+            vec![Some(cvar)],
+            vec![Self::Field::one()],
+            span,
+        );
+
+        self.public_input_size += 1;
+
+        cvar
+    }
 }
diff --git a/src/backends/kimchi/prover.rs b/src/backends/kimchi/prover.rs
index bc7358afd..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<Curve, OpeningProof<Curve>>,
         kimchi::verifier_index::VerifierIndex<Curve, OpeningProof<Curve>>,
@@ -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<KimchiVesta> {
         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 6bc43655f..ed201e181 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,27 @@ 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 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;
+
+    /// 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;
+
+    /// add a constraint to assert a var is multiplied by another var
+    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;
+
+    /// 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(
@@ -44,24 +65,11 @@ 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<Option<CellVar>>,
-        coeffs: Vec<Self::Field>,
-        span: Span,
-    );
+    /// Add a constraint for a public input
+    fn constraint_public_input(&mut self, val: Value<Self>, span: Span) -> CellVar;
 
-    /// Add a generic double gate to the circuit. Kimchi specific atm.
-    fn add_generic_gate(
-        &mut self,
-        label: &'static str,
-        vars: Vec<Option<CellVar>>,
-        coeffs: Vec<Self::Field>,
-        span: Span,
-    );
+    /// Add a constraint for a public output
+    fn constraint_public_output(&mut self, val: Value<Self>, 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.
@@ -119,7 +127,6 @@ pub trait Backend: Clone {
         }
     }
 
-    // TODO: we may need to move the finalized flag from circuit writer to backend, so the backend can freeze itself once finalized.
     /// Finalize the circuit by doing some sanitizing checks.
     fn finalize_circuit(
         &mut self,
@@ -133,7 +140,6 @@ pub trait Backend: Clone {
     fn generate_witness(
         &self,
         witness_env: &mut WitnessEnv<Self::Field>,
-        public_input_size: usize,
     ) -> Result<Self::GeneratedWitness>;
 
     /// 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<B: Backend> CircuitWriter<B> {
         Self {
             typed,
             backend,
-            public_input_size: 0,
             public_output: None,
             private_input_indices: vec![],
         }
@@ -244,6 +240,6 @@ impl<B: Backend> CircuitWriter<B> {
         witness_env: &mut WitnessEnv<B::Field>,
     ) -> Result<B::GeneratedWitness> {
         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 0045d99c7..ddc4a64a2 100644
--- a/src/circuit_writer/writer.rs
+++ b/src/circuit_writer/writer.rs
@@ -697,24 +697,12 @@ impl<B: Backend> CircuitWriter<B> {
         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);
+                .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;
-
         Var::new(cvars, span)
     }
 
@@ -723,21 +711,11 @@ impl<B: Backend> CircuitWriter<B> {
 
         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);
+                .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;
 
         // store it
         let res = Var::new(cvars, span);
diff --git a/src/constraints/boolean.rs b/src/constraints/boolean.rs
index 06f8fff00..9da440af3 100644
--- a/src/constraints/boolean.rs
+++ b/src/constraints/boolean.rs
@@ -11,23 +11,25 @@ use crate::{
     var::{ConstOrCell, Value, Var},
 };
 
+use super::field::{self, sub};
+
 pub fn is_valid<F: Field>(f: F) -> bool {
     f.is_one() || f.is_zero()
 }
 
 pub fn check<B: Backend>(compiler: &mut CircuitWriter<B>, xx: &ConstOrCell<B::Field>, 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(var) => {
+            // x * (x - 1)
+            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);
+        }
     };
 }
 
@@ -53,22 +55,12 @@ pub fn and<B: Backend>(
 
         // two vars
         (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => {
-            // create a new variable to store the result
-            let res = compiler
-                .backend
-                .new_internal_var(Value::Mul(*lhs, *rhs), span);
-
-            // create a gate to constrain the result
-            let zero = B::Field::zero();
-            let one = B::Field::one();
-            compiler.backend.add_generic_gate(
-                "constrain the AND as lhs * rhs",
-                vec![Some(*lhs), Some(*rhs), Some(res)],
-                vec![zero, zero, one.neg(), one], // mul
-                span,
-            );
-
-            // return the result
+            // lhs * rhs
+            let res = compiler.backend.constraint_mul(lhs, rhs, span);
+
+            // check if it is either 1 or 0
+            check(compiler, &ConstOrCell::Cell(res), span);
+
             Var::new_var(res, span)
         }
     }
@@ -89,27 +81,17 @@ pub fn not<B: Backend>(
 
             Var::new_constant(value, span)
         }
+        ConstOrCell::Cell(var) => {
+            let one = ConstOrCell::Const(B::Field::one());
+            let var = ConstOrCell::Cell(*var);
 
-        // constant and a var
-        ConstOrCell::Cell(cvar) => {
-            let zero = B::Field::zero();
-            let one = B::Field::one();
-
-            // create a new variable to store the result
-            let lc = Value::LinearCombination(vec![(one.neg(), *cvar)], one); // 1 - X
-            let res = compiler.backend.new_internal_var(lc, span);
-
-            // create a gate to constrain the result
-            compiler.backend.add_generic_gate(
-                "constrain the NOT as 1 - X",
-                vec![None, Some(*cvar), Some(res)],
-                // we use the constant to do 1 - X
-                vec![zero, one.neg(), one.neg(), zero, one],
-                span,
-            );
-
-            // return the result
-            Var::new_var(res, span)
+            // 1 - x
+            let res = field::sub(compiler, &one, &var, span)[0];
+
+            // ensure it is either 1 or 0
+            check(compiler, &res, span);
+
+            Var::new_cvar(res, span)
         }
     }
 }
diff --git a/src/constraints/field.rs b/src/constraints/field.rs
index d6993715b..8e9c8f790 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},
 };
 
@@ -11,6 +12,21 @@ use ark_ff::{One, Zero};
 
 use std::{ops::Neg, sync::Arc};
 
+/// Adds two field elements
+pub fn neg<B: Backend>(
+    compiler: &mut CircuitWriter<B>,
+    cvar: &ConstOrCell<B::Field>,
+    span: Span,
+) -> Var<B::Field> {
+    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)
+        }
+    }
+}
+
 /// Adds two field elements
 pub fn add<B: Backend>(
     compiler: &mut CircuitWriter<B>,
@@ -18,9 +34,6 @@ pub fn add<B: Backend>(
     rhs: &ConstOrCell<B::Field>,
     span: Span,
 ) -> Var<B::Field> {
-    let zero = B::Field::zero();
-    let one = B::Field::one();
-
     match (lhs, rhs) {
         // 2 constants
         (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs + *rhs, span),
@@ -34,40 +47,12 @@ pub fn add<B: Backend>(
                 return Var::new_var(*cvar, span);
             }
 
-            // create a new variable to store the result
-            let res = compiler
-                .backend
-                .new_internal_var(Value::LinearCombination(vec![(one, *cvar)], *cst), span);
-
-            // create a gate to store the result
-            // TODO: we should use an add_generic function that takes advantage of the double generic gate
-            compiler.backend.add_generic_gate(
-                "add a constant with a variable",
-                vec![Some(*cvar), None, Some(res)],
-                vec![one, zero, one.neg(), zero, *cst],
-                span,
-            );
+            let res = compiler.backend.constraint_add_const(cvar, cst, span);
 
             Var::new_var(res, span)
         }
         (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => {
-            // create a new variable to store the result
-            let res = compiler.backend.new_internal_var(
-                Value::LinearCombination(
-                    vec![(B::Field::one(), *lhs), (B::Field::one(), *rhs)],
-                    B::Field::zero(),
-                ),
-                span,
-            );
-
-            // create a gate to store the result
-            compiler.backend.add_generic_gate(
-                "add two variables together",
-                vec![Some(*lhs), Some(*rhs), Some(res)],
-                vec![B::Field::one(), B::Field::one(), B::Field::one().neg()],
-                span,
-            );
-
+            let res = compiler.backend.constraint_add(lhs, rhs, span);
             Var::new_var(res, span)
         }
     }
@@ -80,80 +65,8 @@ pub fn sub<B: Backend>(
     rhs: &ConstOrCell<B::Field>,
     span: Span,
 ) -> Var<B::Field> {
-    let zero = B::Field::zero();
-    let one = B::Field::one();
-
-    match (lhs, rhs) {
-        // const1 - const2
-        (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => Var::new_constant(*lhs - *rhs, span),
-
-        // const - var
-        (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) => {
-            // create a new variable to store the result
-            let res = compiler.backend.new_internal_var(
-                Value::LinearCombination(vec![(one.neg(), *cvar)], *cst),
-                span,
-            );
-
-            // create a gate to store the result
-            compiler.backend.add_generic_gate(
-                "constant - variable",
-                vec![Some(*cvar), None, Some(res)],
-                // cst - cvar - out = 0
-                vec![one.neg(), zero, one.neg(), zero, *cst],
-                span,
-            );
-
-            Var::new_var(res, span)
-        }
-
-        // var - const
-        (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => {
-            // if the constant is zero, we can ignore this gate
-            if cst.is_zero() {
-                // TODO: that span is incorrect, it should come from lhs or rhs...
-                return Var::new_var(*cvar, span);
-            }
-
-            // create a new variable to store the result
-            let res = compiler.backend.new_internal_var(
-                Value::LinearCombination(vec![(one, *cvar)], cst.neg()),
-                span,
-            );
-
-            // create a gate to store the result
-            // TODO: we should use an add_generic function that takes advantage of the double generic gate
-            compiler.backend.add_generic_gate(
-                "variable - constant",
-                vec![Some(*cvar), None, Some(res)],
-                // var - cst - out = 0
-                vec![one, zero, one.neg(), zero, cst.neg()],
-                span,
-            );
-
-            Var::new_var(res, span)
-        }
-
-        // lhs - rhs
-        (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => {
-            // create a new variable to store the result
-            let res = compiler.backend.new_internal_var(
-                Value::LinearCombination(vec![(one, *lhs), (one.neg(), *rhs)], zero),
-                span,
-            );
-
-            // create a gate to store the result
-            compiler.backend.add_generic_gate(
-                "var1 - var2",
-                vec![Some(*lhs), Some(*rhs), Some(res)],
-                // lhs - rhs - out = 0
-                vec![one, one.neg(), one.neg()],
-                span,
-            );
-
-            Var::new_var(res, span)
-        }
-    }
+    let neg_rhs = neg(compiler, rhs, span);
+    add(compiler, lhs, &neg_rhs.cvars[0], span)
 }
 
 /// Multiplies two field elements
@@ -163,9 +76,6 @@ pub fn mul<B: Backend>(
     rhs: &ConstOrCell<B::Field>,
     span: Span,
 ) -> Var<B::Field> {
-    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),
@@ -174,6 +84,7 @@ pub fn mul<B: Backend>(
         (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"),
@@ -183,38 +94,13 @@ pub fn mul<B: Backend>(
                 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,
-            );
-
+            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)) => {
-            // create a new variable to store the result
-            let res = compiler
-                .backend
-                .new_internal_var(Value::Mul(*lhs, *rhs), span);
-
-            // create a gate to store the result
-            compiler.backend.add_generic_gate(
-                "add two variables together",
-                vec![Some(*lhs), Some(*rhs), Some(res)],
-                vec![zero, zero, one.neg(), one],
-                span,
-            );
-
+            let res = compiler.backend.constraint_mul(lhs, rhs, span);
             Var::new_var(res, span)
         }
     }
@@ -325,54 +211,40 @@ fn equal_cells<B: Backend>(
                 span,
             );
 
+            // todo: replace these front end constraints with backend constraints
             // 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()],
+            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()],
+            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
+            compiler
+                .backend
+                .constraint_eq_const(res_mul_diff.cvar().unwrap(), 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],
+            let diff_inv_mul_diff = mul(compiler, &ConstOrCell::Cell(diff_inv), &diff, span)[0];
+            // 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,
             );
 
@@ -492,25 +364,12 @@ pub fn if_else_inner<B: Backend>(
                 span,
             );
 
-            let then_m_else = sub(compiler, then_, else_, span)[0]
-                .cvar()
-                .cloned()
-                .unwrap();
-            let res_m_else = sub(compiler, &ConstOrCell::<B::Field>::Cell(res), else_, span)[0]
-                .cvar()
-                .cloned()
-                .unwrap();
-
-            let zero = B::Field::zero();
-            let one = B::Field::one();
-
-            compiler.backend.add_generic_gate(
-                "constraint for ternary operator: cond * (then - else) = res - else",
-                vec![Some(cond_cell), Some(then_m_else), Some(res_m_else)],
-                // cond * (then - else) = res - else
-                vec![zero, zero, one.neg(), one],
-                span,
-            );
+            let then_m_else = sub(compiler, then_, else_, span)[0];
+            let res_m_else = sub(compiler, &ConstOrCell::<B::Field>::Cell(res), else_, span)[0];
+
+            // 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)
         }
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<B: Backend>(
         // 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<B: Backend>(
             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);
         }
     }