move and implement constraints as traits for backends

src/backends/mod.rs

@@ -0,0 +1,2 @@
+pub mod kimchi;
+pub mod r1cs;

src/backends/r1cs.rs

@@ -0,0 +1,5 @@
+
+#[derive(Debug)]
+pub struct R1CSBackend {
+
+}

src/circuit_writer/mod.rs

@@ -1,7 +1,7 @@
 use std::collections::{HashMap, HashSet};
 
 use crate::{
-    circuit_writer::writer::{AnnotatedCell, Cell}, constants::{Field, Span, NUM_REGISTERS}, error::{Error, ErrorKind, Result}, helpers::PrettyField, parser::{
+    backends::{kimchi::KimchiBackend, r1cs::R1CSBackend}, circuit_writer::writer::{AnnotatedCell, Cell}, constants::{Field, Span, NUM_REGISTERS}, error::{Error, ErrorKind, Result}, helpers::PrettyField, parser::{
         types::{AttributeKind, FnArg, TyKind},
         Expr,
     }, type_checker::{ConstInfo, FnInfo, FullyQualified, StructInfo, TypeChecker}, var::{CellVar, Value, Var}, witness::CompiledCircuit
@@ -20,36 +20,6 @@ pub mod writer;
 
 use num_traits::Zero;
 
-#[derive(Debug)]
-pub struct KimchiBackend<F> where F: Field {
-    /// The gates created by the circuit generation.
-    pub gates: Vec<Gate<F>>,
-
-    /// The wiring of the circuit.
-    /// It is created during circuit generation.
-    pub(crate) wiring: HashMap<usize, Wiring>,
-
-    /// If set to false, a single generic gate will be used per double generic gate.
-    /// This can be useful for debugging.
-    pub(crate) double_generic_gate_optimization: bool,
-
-    /// This is used to implement the double generic gate,
-    /// which encodes two generic gates.
-    pub(crate) pending_generic_gate: Option<PendingGate<F>>,
-
-    /// The execution trace table with vars as placeholders.
-    /// It is created during circuit generation,
-    /// and used by the witness generator.
-    pub(crate) rows_of_vars: Vec<Vec<Option<CellVar>>>,
-
-    /// A vector of debug information that maps to each row of the created circuit.
-    pub(crate) debug_info: Vec<DebugInfo>,
-}
-
-#[derive(Debug)]
-pub struct R1CSBackend {
-
-}
 
 
 // enums for proving backends
@@ -59,102 +29,6 @@ pub enum ProvingBackend<F: Field> {
     R1CS(R1CSBackend),
 }
 
-impl<F: Field> KimchiBackend<F> {
-    /// creates a new gate, and the associated row in the witness/execution trace.
-    // TODO: add_gate instead of gates?
-    pub fn add_gate(
-        &mut self,
-        note: &'static str,
-        typ: GateKind,
-        vars: Vec<Option<CellVar>>,
-        coeffs: Vec<F>,
-        span: Span,
-    ) {
-        // sanitize
-        assert!(coeffs.len() <= NUM_REGISTERS);
-        assert!(vars.len() <= NUM_REGISTERS);
-
-        // construct the execution trace with vars, for the witness generation
-        self.rows_of_vars.push(vars.clone());
-
-        // get current row
-        // important: do that before adding the gate below
-        let row = self.gates.len();
-
-        // add gate
-        self.gates.push(Gate { typ, coeffs });
-
-        // add debug info related to that gate
-        let debug_info = DebugInfo {
-            span,
-            note: note.to_string(),
-        };
-        self.debug_info.push(debug_info.clone());
-
-        // wiring (based on vars)
-        for (col, var) in vars.iter().enumerate() {
-            if let Some(var) = var {
-                let curr_cell = Cell { row, col };
-                let annotated_cell = AnnotatedCell {
-                    cell: curr_cell,
-                    debug: debug_info.clone(),
-                };
-
-                self.wiring
-                    .entry(var.index)
-                    .and_modify(|w| match w {
-                        Wiring::NotWired(old_cell) => {
-                            *w = Wiring::Wired(vec![old_cell.clone(), annotated_cell.clone()])
-                        }
-                        Wiring::Wired(ref mut cells) => {
-                            cells.push(annotated_cell.clone());
-                        }
-                    })
-                    .or_insert(Wiring::NotWired(annotated_cell));
-            }
-        }
-    }
-
-    pub fn add_generic_gate(
-        &mut self,
-        label: &'static str,
-        mut vars: Vec<Option<CellVar>>,
-        mut coeffs: Vec<F>,
-        span: Span,
-    ) {
-        // padding
-        let coeffs_padding = GENERIC_COEFFS.checked_sub(coeffs.len()).unwrap();
-        coeffs.extend(std::iter::repeat(F::zero()).take(coeffs_padding));
-
-        let vars_padding = GENERIC_REGISTERS.checked_sub(vars.len()).unwrap();
-        vars.extend(std::iter::repeat(None).take(vars_padding));
-
-        // if the double gate optimization is not set, just add the gate
-        if !self.double_generic_gate_optimization {
-            self.add_gate(label, GateKind::DoubleGeneric, vars, coeffs, span);
-            return;
-        }
-
-        // only add a double generic gate if we have two of them
-        if let Some(generic_gate) = self.pending_generic_gate.take() {
-            coeffs.extend(generic_gate.coeffs);
-            vars.extend(generic_gate.vars);
-
-            // TODO: what to do with the label and span?
-
-            self.add_gate(label, GateKind::DoubleGeneric, vars, coeffs, span);
-        } else {
-            // otherwise queue it
-            self.pending_generic_gate = Some(PendingGate {
-                label,
-                coeffs,
-                vars,
-                span,
-            });
-        }
-    }
-}
-
 
 //#[derive(Debug, Serialize, Deserialize)]
 #[derive(Debug)]

src/cli/cmd_build_and_check.rs

@@ -5,7 +5,15 @@ use kimchi::mina_curves::pasta::Fp;
 use miette::{Context, IntoDiagnostic};
 
 use crate::{
-    circuit_writer::{KimchiBackend, ProvingBackend}, cli::packages::path_to_package, compiler::{compile, typecheck_next_file, Sources}, constants::Field, helpers::PrettyField, inputs::{parse_inputs, JsonInputs}, prover::{compile_to_indexes, ProverIndex, VerifierIndex}, type_checker::TypeChecker
+    backends::kimchi::KimchiBackend,
+    circuit_writer::ProvingBackend,
+    cli::packages::path_to_package,
+    compiler::{compile, typecheck_next_file, Sources},
+    constants::Field,
+    helpers::PrettyField,
+    inputs::{parse_inputs, JsonInputs},
+    prover::{compile_to_indexes, ProverIndex, VerifierIndex},
+    type_checker::TypeChecker,
 };
 
 use super::packages::{
@@ -111,7 +119,9 @@ pub fn cmd_check(args: CmdCheck) -> miette::Result<()> {
     Ok(())
 }
 
-fn produce_all_asts<F: Field + PrettyField>(path: &PathBuf) -> miette::Result<(Sources, TypeChecker<F>)> {
+fn produce_all_asts<F: Field + PrettyField>(
+    path: &PathBuf,
+) -> miette::Result<(Sources, TypeChecker<F>)> {
     // find manifest
     let manifest = validate_package_and_get_manifest(&path, false)?;
 

src/constraints/mod.rs

@@ -1,2 +1,107 @@
+use ark_ff::Field;
+
+use crate::{
+    circuit_writer::CircuitWriter,
+    constants::Span,
+    helpers::PrettyField,
+    var::{ConstOrCell, Var},
+};
+
 pub mod boolean;
 pub mod field;
+
+pub trait BooleanConstraints<F: Field + PrettyField> {
+    fn is_valid(&self, f: F) -> bool {
+        f.is_one() || f.is_zero()
+    }
+
+    fn check(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        xx: &ConstOrCell<F>,
+        span: Span,
+    );
+
+    fn and(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &ConstOrCell<F>,
+        rhs: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn not(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        var: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn or(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &ConstOrCell<F>,
+        rhs: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+}
+
+pub trait FieldConstraints<F: Field + PrettyField> {
+    fn add(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &ConstOrCell<F>,
+        rhs: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn sub(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &ConstOrCell<F>,
+        rhs: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn mul(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &ConstOrCell<F>,
+        rhs: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn equal(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        lhs: &Var<F>,
+        rhs: &Var<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn equal_cells(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        x1: &ConstOrCell<F>,
+        x2: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn if_else(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        cond: &Var<F>,
+        then_: &Var<F>,
+        else_: &Var<F>,
+        span: Span,
+    ) -> Var<F>;
+
+    fn if_else_inner(
+        &self,
+        compiler: &mut CircuitWriter<F>,
+        cond: &ConstOrCell<F>,
+        then_: &ConstOrCell<F>,
+        else_: &ConstOrCell<F>,
+        span: Span,
+    ) -> Var<F>;
+}

src/lib.rs

@@ -4,6 +4,7 @@
 
 pub mod asm;
 pub mod circuit_writer;
+pub mod backends;
 pub mod cli;
 pub mod compiler;
 pub mod constants;

src/prover.rs

@@ -194,9 +194,9 @@ impl ProverIndex {
 //
 
 impl VerifierIndex {
-    pub fn verify<F: Field>(
+    pub fn verify(
         &self,
-        full_public_inputs: Vec<F>,
+        full_public_inputs: Vec<KimchiField>,
         proof: ProverProof<Curve, OpeningProof<Curve>>,
     ) -> miette::Result<()> {
         // verify the proof