diff --git a/src/backends/kimchi.rs b/src/backends/kimchi.rs new file mode 100644 index 000000000..bad26aaac --- /dev/null +++ b/src/backends/kimchi.rs @@ -0,0 +1,756 @@ +use std::collections::HashMap; + +use ark_ff::Field; +use kimchi::circuits::polynomials::generic::{GENERIC_COEFFS, GENERIC_REGISTERS}; + +use crate::{ + circuit_writer::{ + writer::{AnnotatedCell, Cell, PendingGate}, + DebugInfo, Gate, GateKind, Wiring, + }, + constants::{Span, NUM_REGISTERS}, + constraints::{BooleanConstraints, FieldConstraints}, + helpers::PrettyField, + var::{CellVar, ConstOrCell, Value, Var}, +}; + +#[derive(Debug)] +pub struct KimchiBackend +where + F: Field, +{ + /// The gates created by the circuit generation. + pub gates: Vec>, + + /// The wiring of the circuit. + /// It is created during circuit generation. + pub(crate) wiring: HashMap, + + /// 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>, + + /// 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>>, + + /// A vector of debug information that maps to each row of the created circuit. + pub(crate) debug_info: Vec, +} + +impl KimchiBackend { + /// 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>, + coeffs: Vec, + 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>, + mut coeffs: Vec, + 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, + }); + } + } +} + +impl BooleanConstraints for KimchiBackend { + fn check( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + xx: &crate::var::ConstOrCell, + span: Span, + ) { + let zero = F::zero(); + let one = F::one(); + + match xx { + ConstOrCell::Const(ff) => assert!(self.is_valid(*ff)), + ConstOrCell::Cell(var) => self.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, + ), + }; + } + + fn and( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &crate::var::ConstOrCell, + rhs: &crate::var::ConstOrCell, + span: Span, + ) -> crate::var::Var { + match (lhs, rhs) { + // two constants + (ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { + Var::new_constant(*lhs * *rhs, span) + } + + // constant and a var + (ConstOrCell::Const(cst), ConstOrCell::Cell(cvar)) + | (ConstOrCell::Cell(cvar), ConstOrCell::Const(cst)) => { + if cst.is_one() { + Var::new_var(*cvar, span) + } else { + Var::new_constant(*cst, span) + } + } + + // two vars + (ConstOrCell::Cell(lhs), ConstOrCell::Cell(rhs)) => { + // create a new variable to store the result + let res = compiler.new_internal_var(Value::Mul(*lhs, *rhs), span); + + // create a gate to constrain the result + let zero = F::zero(); + let one = F::one(); + self.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) + } + } + } + + fn not( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + var: &crate::var::ConstOrCell, + span: Span, + ) -> crate::var::Var { + match var { + ConstOrCell::Const(cst) => { + let value = if cst.is_one() { F::zero() } else { F::one() }; + + Var::new_constant(value, span) + } + + // constant and a var + ConstOrCell::Cell(cvar) => { + let zero = F::zero(); + let one = F::one(); + + // create a new variable to store the result + let lc = Value::LinearCombination(vec![(one.neg(), *cvar)], one); // 1 - X + let res = compiler.new_internal_var(lc, span); + + // create a gate to constrain the result + self.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) + } + } + } + + fn or( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &crate::var::ConstOrCell, + rhs: &crate::var::ConstOrCell, + span: Span, + ) -> crate::var::Var { + let not_lhs = self.not(compiler, lhs, span); + let not_rhs = self.not(compiler, rhs, span); + let both_false = self.and(compiler, ¬_lhs[0], ¬_rhs[0], span); + self.not(compiler, &both_false[0], span) + } +} + +impl FieldConstraints for KimchiBackend { + fn add( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var { + let zero = F::zero(); + let one = F::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 + .new_internal_var(Value::LinearCombination(vec![(one, *cvar)], *cst), span); + + self.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.new_internal_var( + Value::LinearCombination(vec![(F::one(), *lhs), (F::one(), *rhs)], F::zero()), + span, + ); + + self.add_generic_gate( + "add two variables together", + vec![Some(*lhs), Some(*rhs), Some(res)], + vec![F::one(), F::one(), F::one().neg()], + span, + ); + + Var::new_var(res, span) + } + } + } + + fn sub( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var { + let zero = F::zero(); + let one = F::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.new_internal_var( + Value::LinearCombination(vec![(one.neg(), *cvar)], *cst), + span, + ); + + // create a gate to store the result + self.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.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 + self.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.new_internal_var( + Value::LinearCombination(vec![(one, *lhs), (one.neg(), *rhs)], zero), + span, + ); + + // create a gate to store the result + self.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) + } + } + } + + fn mul( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var { + let zero = F::zero(); + let one = F::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.add_constant( + Some("encoding zero for the result of 0 * var"), + F::zero(), + span, + ); + return Var::new_var(zero, span); + } + + // create a new variable to store the result + let res = compiler.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, + ); + + 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.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, + ); + + Var::new_var(res, span) + } + } + } + + fn equal( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + lhs: &Var, + rhs: &Var, + span: Span, + ) -> Var { + // sanity check + assert_eq!(lhs.len(), rhs.len()); + + if lhs.len() == 1 { + return self.equal_cells(compiler, &lhs[0], &rhs[0], span); + } + + // create an accumulator + let one = F::one(); + + let acc = compiler.add_constant( + Some("start accumulator at 1 for the equality check"), + one, + span, + ); + let mut acc = Var::new_var(acc, span); + + for (l, r) in lhs.cvars.iter().zip(&rhs.cvars) { + let res = self.equal_cells(compiler, l, r, span); + acc = self.and(compiler, &res[0], &acc[0], span); + } + + acc + } + + fn equal_cells( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + x1: &ConstOrCell, + x2: &ConstOrCell, + span: Span, + ) -> Var { + // These four constraints are enough: + // + // 1. `diff = x2 - x1` + // 2. `one_minus_res + res = 1` + // 3. `res * diff = 0` + // 4. `diff_inv * diff = one_minus_res` + // + // To prove this, it suffices to prove that: + // + // a. `diff = 0 => res = 1`. + // b. `diff != 0 => res = 0`. + // + // Proof: + // + // a. if `diff = 0`, + // then using (4) `one_minus_res = 0`, + // then using (2) `res = 1` + // + // b. if `diff != 0` + // then using (3) `res = 0` + // + + let zero = F::zero(); + let one = F::one(); + + match (x1, x2) { + // two constants + (ConstOrCell::Const(x1), ConstOrCell::Const(x2)) => { + let res = if x1 == x2 { one } else { F::zero() }; + Var::new_constant(res, span) + } + + (x1, x2) => { + let x1 = match x1 { + ConstOrCell::Const(cst) => compiler.add_constant( + Some("encode the lhs constant of the equality check in the circuit"), + *cst, + span, + ), + ConstOrCell::Cell(cvar) => *cvar, + }; + + let x2 = match x2 { + ConstOrCell::Const(cst) => compiler.add_constant( + Some("encode the rhs constant of the equality check in the circuit"), + *cst, + span, + ), + ConstOrCell::Cell(cvar) => *cvar, + }; + + // compute the result + let res = compiler.new_internal_var( + Value::Hint(Box::new(move |compiler, env| { + let x1 = compiler.compute_var(env, x1)?; + let x2 = compiler.compute_var(env, x2)?; + if x1 == x2 { + Ok(F::one()) + } else { + Ok(F::zero()) + } + })), + span, + ); + + // 1. diff = x2 - x1 + let diff = compiler.new_internal_var( + Value::LinearCombination(vec![(one, x2), (one.neg(), x1)], zero), + span, + ); + + self.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, + ); + + // 2. one_minus_res = 1 - res + let one_minus_res = compiler + .new_internal_var(Value::LinearCombination(vec![(one.neg(), res)], one), span); + + self.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, + ); + + // 3. res * diff = 0 + self.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, + ); + + // 4. diff_inv * diff = one_minus_res + let diff_inv = compiler.new_internal_var(Value::Inverse(diff), span); + + self.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, + ); + + Var::new_var(res, span) + } + } + } + + fn if_else( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + cond: &Var, + then_: &Var, + else_: &Var, + span: Span, + ) -> Var { + assert_eq!(cond.len(), 1); + assert_eq!(then_.len(), else_.len()); + + let cond = cond[0]; + + let mut vars = vec![]; + + for (then_, else_) in then_.cvars.iter().zip(&else_.cvars) { + let var = self.if_else_inner(compiler, &cond, then_, else_, span); + vars.push(var[0]); + } + + Var::new(vars, span) + } + + fn if_else_inner( + &self, + compiler: &mut crate::circuit_writer::CircuitWriter, + cond: &ConstOrCell, + then_: &ConstOrCell, + else_: &ConstOrCell, + span: Span, + ) -> Var { + // we need to constrain: + // + // * res = (1 - cond) * else + cond * then + // + + // if cond is constant, easy + let cond_cell = match cond { + ConstOrCell::Const(cond) => { + if cond.is_one() { + return Var::new_cvar(*then_, span); + } else { + return Var::new_cvar(*else_, span); + } + } + ConstOrCell::Cell(cond) => *cond, + }; + + match (&then_, &else_) { + // if the branches are constant, + // we can create the following constraints: + // + // res = (1 - cond) * else + cond * then + // + // translates to + // + // cond_then = cond * then + // temp = (1 - cond) * else => + // - either + // - one_minus_cond = 1 - cond + // - one_minus_cond * else + // - or + // - cond_else = cond * else + // - else - cond_else + // res - temp + cond_then = 0 + // res - X = 0 + // + (ConstOrCell::Const(_), ConstOrCell::Const(_)) => { + let cond_then = self.mul(compiler, then_, cond, span); + let one = ConstOrCell::Const(F::one()); + let one_minus_cond = self.sub(compiler, &one, cond, span); + let temp = self.mul(compiler, &one_minus_cond[0], else_, span); + self.add(compiler, &cond_then[0], &temp[0], span) + } + + // if one of them is a var + // + // res = (1 - cond) * else + cond * then + // + // translates to + // + // cond_then = cond * then + // temp = (1 - cond) * else => + // - either + // - one_minus_cond = 1 - cond + // - one_minus_cond * else + // - or + // - cond_else = cond * else + // - else - cond_else + // res - temp + cond_then = 0 + // res - X = 0 + // + _ => { + // let cond_inner = cond.clone(); + let then_clone = *then_; + let else_clone = *else_; + + let res = compiler.new_internal_var( + Value::Hint(Box::new(move |compiler, env| { + let cond = compiler.compute_var(env, cond_cell)?; + let res_var = if cond.is_one() { + &then_clone + } else { + &else_clone + }; + match res_var { + ConstOrCell::Const(cst) => Ok(*cst), + ConstOrCell::Cell(var) => compiler.compute_var(env, *var), + } + })), + span, + ); + + let then_m_else = self.sub(compiler, then_, else_, span)[0] + .cvar() + .cloned() + .unwrap(); + let res_m_else = self.sub(compiler, &ConstOrCell::Cell(res), else_, span)[0] + .cvar() + .cloned() + .unwrap(); + + let zero = F::zero(); + let one = F::one(); + + self.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, + ); + + Var::new_var(res, span) + } + } + } +} diff --git a/src/backends/mod.rs b/src/backends/mod.rs new file mode 100644 index 000000000..74eaba6c2 --- /dev/null +++ b/src/backends/mod.rs @@ -0,0 +1,2 @@ +pub mod kimchi; +pub mod r1cs; \ No newline at end of file diff --git a/src/backends/r1cs.rs b/src/backends/r1cs.rs new file mode 100644 index 000000000..f4e040d4f --- /dev/null +++ b/src/backends/r1cs.rs @@ -0,0 +1,5 @@ + +#[derive(Debug)] +pub struct R1CSBackend { + +} diff --git a/src/circuit_writer/mod.rs b/src/circuit_writer/mod.rs index 9bd8791f4..9189c54d7 100644 --- a/src/circuit_writer/mod.rs +++ b/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 where F: Field { - /// The gates created by the circuit generation. - pub gates: Vec>, - - /// The wiring of the circuit. - /// It is created during circuit generation. - pub(crate) wiring: HashMap, - - /// 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>, - - /// 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>>, - - /// A vector of debug information that maps to each row of the created circuit. - pub(crate) debug_info: Vec, -} - -#[derive(Debug)] -pub struct R1CSBackend { - -} // enums for proving backends @@ -59,102 +29,6 @@ pub enum ProvingBackend { R1CS(R1CSBackend), } -impl KimchiBackend { - /// 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>, - coeffs: Vec, - 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>, - mut coeffs: Vec, - 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)] diff --git a/src/cli/cmd_build_and_check.rs b/src/cli/cmd_build_and_check.rs index 0b7f89a8e..f25b2741d 100644 --- a/src/cli/cmd_build_and_check.rs +++ b/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(path: &PathBuf) -> miette::Result<(Sources, TypeChecker)> { +fn produce_all_asts( + path: &PathBuf, +) -> miette::Result<(Sources, TypeChecker)> { // find manifest let manifest = validate_package_and_get_manifest(&path, false)?; diff --git a/src/constraints/mod.rs b/src/constraints/mod.rs index 63dd53b7f..d3d3307c5 100644 --- a/src/constraints/mod.rs +++ b/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 { + fn is_valid(&self, f: F) -> bool { + f.is_one() || f.is_zero() + } + + fn check( + &self, + compiler: &mut CircuitWriter, + xx: &ConstOrCell, + span: Span, + ); + + fn and( + &self, + compiler: &mut CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var; + + fn not( + &self, + compiler: &mut CircuitWriter, + var: &ConstOrCell, + span: Span, + ) -> Var; + + fn or( + &self, + compiler: &mut CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var; +} + +pub trait FieldConstraints { + fn add( + &self, + compiler: &mut CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var; + + fn sub( + &self, + compiler: &mut CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var; + + fn mul( + &self, + compiler: &mut CircuitWriter, + lhs: &ConstOrCell, + rhs: &ConstOrCell, + span: Span, + ) -> Var; + + fn equal( + &self, + compiler: &mut CircuitWriter, + lhs: &Var, + rhs: &Var, + span: Span, + ) -> Var; + + fn equal_cells( + &self, + compiler: &mut CircuitWriter, + x1: &ConstOrCell, + x2: &ConstOrCell, + span: Span, + ) -> Var; + + fn if_else( + &self, + compiler: &mut CircuitWriter, + cond: &Var, + then_: &Var, + else_: &Var, + span: Span, + ) -> Var; + + fn if_else_inner( + &self, + compiler: &mut CircuitWriter, + cond: &ConstOrCell, + then_: &ConstOrCell, + else_: &ConstOrCell, + span: Span, + ) -> Var; +} diff --git a/src/lib.rs b/src/lib.rs index 1cdad976a..3375b9c0c 100644 --- a/src/lib.rs +++ b/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; diff --git a/src/prover.rs b/src/prover.rs index 8cfe5694d..58c3b7270 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -194,9 +194,9 @@ impl ProverIndex { // impl VerifierIndex { - pub fn verify( + pub fn verify( &self, - full_public_inputs: Vec, + full_public_inputs: Vec, proof: ProverProof>, ) -> miette::Result<()> { // verify the proof