From ececc2b60be66a2d907c1d113a3f33ee78380a03 Mon Sep 17 00:00:00 2001 From: Sean Bowe Date: Sun, 24 Jan 2016 01:42:29 -0700 Subject: [PATCH] Implement raw constraints for Bit --- src/bit.rs | 78 +++++++++++++++++++++++++++++++++++++++++++------ src/variable.rs | 36 +++++------------------ 2 files changed, 77 insertions(+), 37 deletions(-) diff --git a/src/bit.rs b/src/bit.rs index 02f6381..108cf09 100644 --- a/src/bit.rs +++ b/src/bit.rs @@ -214,14 +214,68 @@ fn resolve(a: &Var, b: &Var, op: Op) -> Var { vals.set_output(0, op.val(a, b)); }, |i, o, cs| { cs.push(match op { - And => Constraint::And(i[0].index(), i[1].index(), o[0].index()), - Nand => Constraint::Nand(i[0].index(), i[1].index(), o[0].index()), - Xor => Constraint::Xor(i[0].index(), i[1].index(), o[0].index()), - Xnor => Constraint::Xnor(i[0].index(), i[1].index(), o[0].index()), - Nor => Constraint::Nor(i[0].index(), i[1].index(), o[0].index()), - Or => Constraint::Or(i[0].index(), i[1].index(), o[0].index()), - MaterialNonimplication => Constraint::MaterialNonimplication(i[0].index(), i[1].index(), o[0].index()), - MaterialImplication => Constraint::MaterialImplication(i[0].index(), i[1].index(), o[0].index()) + // a * b = c + And => Constraint(vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![(FieldT::one(), o[0].clone())] + ), + // a * b = 1 - c + Nand => Constraint(vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![(FieldT::one(), Var::one()), + (-FieldT::one(), o[0].clone()) + ] + ), + // 2a * b = a + b - c + Xor => Constraint(vec![(FieldT::from(2), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![(FieldT::one(), i[0].clone()), + (FieldT::one(), i[1].clone()), + (-FieldT::one(), o[0].clone()) + ] + ), + // 2a * b = a + b + c - 1 + Xnor => Constraint(vec![(FieldT::from(2), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![ + (FieldT::one(), i[0].clone()), + (FieldT::one(), i[1].clone()), + (FieldT::one(), o[0].clone()), + (-FieldT::one(), Var::one()) + ] + ), + // a * (1 - b) = c + MaterialNonimplication => Constraint(vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::one(), Var::one()), + (-FieldT::one(), i[1].clone()) + ], + vec![(FieldT::one(), o[0].clone())] + ), + // a * b = a + c - 1 + MaterialImplication => Constraint(vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![(FieldT::one(), i[0].clone()), + (FieldT::one(), o[0].clone()), + (-FieldT::one(), Var::one()) + ] + ), + // (1 - a) * (1 - b) = c + Nor => Constraint(vec![(FieldT::one(), Var::one()), + (-FieldT::one(), i[0].clone()) + ], + vec![(FieldT::one(), Var::one()), + (-FieldT::one(), i[1].clone()) + ], + vec![(FieldT::one(), o[0].clone())] + ), + // a * b = a + b - c + Or => Constraint(vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::one(), i[1].clone())], + vec![(FieldT::one(), i[0].clone()), + (FieldT::one(), i[1].clone()), + (-FieldT::one(), o[0].clone()) + ] + ), }); vec![o[0]] @@ -263,7 +317,13 @@ impl Bit { pub fn new(v: &Var) -> Bit { Is(gadget(&[v], 0, |_| {}, |i, o, cs| { - cs.push(Constraint::Bitness(i[0].index())); + // boolean constraint: + // (1 - a) * a = 0 + cs.push(Constraint(vec![(FieldT::one(), Var::one()), + (-FieldT::one(), i[0].clone())], + vec![(FieldT::one(), i[0].clone())], + vec![(FieldT::zero(), Var::one())] + )); vec![i[0]] }).remove(0)) diff --git a/src/variable.rs b/src/variable.rs index 4dd29ed..5aab58f 100644 --- a/src/variable.rs +++ b/src/variable.rs @@ -1,7 +1,6 @@ use tinysnark::FieldT; use std::cell::Cell; use std::rc::Rc; -use std::fmt; use std::collections::BTreeMap; pub type WitnessMap = BTreeMap, Vec, Rc)>>; @@ -41,33 +40,7 @@ pub fn witness_field_elements(vars: &mut [FieldT], witness_map: &WitnessMap) { } #[derive(Clone)] -pub enum Constraint { - Bitness(Rc>), - And(Rc>, Rc>, Rc>), - Nand(Rc>, Rc>, Rc>), - Xor(Rc>, Rc>, Rc>), - Xnor(Rc>, Rc>, Rc>), - MaterialNonimplication(Rc>, Rc>, Rc>), - MaterialImplication(Rc>, Rc>, Rc>), - Nor(Rc>, Rc>, Rc>), - Or(Rc>, Rc>, Rc>) -} - -impl fmt::Debug for Constraint { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", match *self { - Constraint::Bitness(ref b) => format!("bitness: {}", b.get()), - Constraint::And(ref a, ref b, ref c) => format!("{} = {} AND {}", c.get(), a.get(), b.get()), - Constraint::Nand(ref a, ref b, ref c) => format!("{} = {} NAND {}", c.get(), a.get(), b.get()), - Constraint::Xor(ref a, ref b, ref c) => format!("{} = {} XOR {}", c.get(), a.get(), b.get()), - Constraint::Xnor(ref a, ref b, ref c) => format!("{} = {} XNOR {}", c.get(), a.get(), b.get()), - Constraint::MaterialNonimplication(ref a, ref b, ref c) => format!("{} = {} ↛ {}", c.get(), a.get(), b.get()), - Constraint::MaterialImplication(ref a, ref b, ref c) => format!("{} = {} <-> {}", c.get(), a.get(), b.get()), - Constraint::Nor(ref a, ref b, ref c) => format!("{} = {} NOR {}", c.get(), a.get(), b.get()), - Constraint::Or(ref a, ref b, ref c) => format!("{} = {} OR {}", c.get(), a.get(), b.get()) - }) - } -} +pub struct Constraint(pub Vec<(FieldT, Var)>, pub Vec<(FieldT, Var)>, pub Vec<(FieldT, Var)>); struct Gadget { inputs: Vec, @@ -122,6 +95,13 @@ impl Var { } } + pub fn one() -> Var { + Var { + index: Rc::new(Cell::new(0)), + gadget: None + } + } + // make this not public or unsafe too pub fn index(&self) -> Rc> { self.index.clone()