From 69abd0391f7faa8f1d95afdc292d2584decc192b Mon Sep 17 00:00:00 2001 From: Sean Bowe Date: Fri, 23 Feb 2018 11:15:14 -0700 Subject: [PATCH] Optimize into_bits_strict. --- src/circuit/boolean.rs | 38 +++++++++++ src/circuit/mod.rs | 4 +- src/circuit/num.rs | 148 ++++++++++++++++++++++++++++++++++++----- 3 files changed, 170 insertions(+), 20 deletions(-) diff --git a/src/circuit/boolean.rs b/src/circuit/boolean.rs index 23ec447..48d243d 100644 --- a/src/circuit/boolean.rs +++ b/src/circuit/boolean.rs @@ -34,6 +34,44 @@ impl AllocatedBit { self.variable } + /// Allocate a variable in the constraint system which can only be a + /// boolean value. Further, constrain that the boolean is false + /// unless the condition is false. + pub fn alloc_conditionally( + mut cs: CS, + value: Option, + must_be_false: &AllocatedBit + ) -> Result + where E: Engine, + CS: ConstraintSystem + { + let var = cs.alloc(|| "boolean", || { + if *value.get()? { + Ok(E::Fr::one()) + } else { + Ok(E::Fr::zero()) + } + })?; + + // Constrain: (1 - must_be_false - a) * a = 0 + // if must_be_false is true, the equation + // reduces to -a * a = 0, which implies a = 0. + // if must_be_false is false, the equation + // reduces to (1 - a) * a = 0, which is a + // traditional boolean constraint. + cs.enforce( + || "boolean constraint", + |lc| lc + CS::one() - must_be_false.variable - var, + |lc| lc + var, + |lc| lc + ); + + Ok(AllocatedBit { + variable: var, + value: value + }) + } + /// Allocate a variable in the constraint system which can only be a /// boolean value. pub fn alloc( diff --git a/src/circuit/mod.rs b/src/circuit/mod.rs index 96a9c08..84d768b 100644 --- a/src/circuit/mod.rs +++ b/src/circuit/mod.rs @@ -392,7 +392,7 @@ fn test_input_circuit_with_bls12_381() { assert!(cs.is_satisfied()); - assert_eq!(cs.num_constraints(), 99816); + assert_eq!(cs.num_constraints(), 97376); } // use bellman::groth16::*; @@ -737,7 +737,7 @@ fn test_output_circuit_with_bls12_381() { assert!(cs.is_satisfied()); - assert_eq!(cs.num_constraints(), 8315); + assert_eq!(cs.num_constraints(), 7827); } // use bellman::groth16::*; diff --git a/src/circuit/num.rs b/src/circuit/num.rs index c24fb09..92e25c7 100644 --- a/src/circuit/num.rs +++ b/src/circuit/num.rs @@ -2,6 +2,8 @@ use pairing::{ Engine, Field, PrimeField, + PrimeFieldRepr, + BitIterator }; use bellman::{ @@ -18,6 +20,7 @@ use super::{ use super::boolean::{ self, Boolean, + AllocatedBit }; pub struct AllocatedNum { @@ -63,10 +66,126 @@ impl AllocatedNum { ) -> Result, SynthesisError> where CS: ConstraintSystem { - let bits = self.into_bits(&mut cs)?; - Boolean::enforce_in_field::<_, _, E::Fr>(&mut cs, &bits)?; + pub fn kary_and( + mut cs: CS, + v: &[AllocatedBit] + ) -> Result + where E: Engine, + CS: ConstraintSystem + { + assert!(v.len() > 0); - Ok(bits) + // Let's keep this simple for now and just AND them all + // manually + let mut cur = None; + + for (i, v) in v.iter().enumerate() { + if cur.is_none() { + cur = Some(v.clone()); + } else { + cur = Some(AllocatedBit::and( + cs.namespace(|| format!("and {}", i)), + cur.as_ref().unwrap(), + v + )?); + } + } + + Ok(cur.expect("v.len() > 0")) + } + + // We want to ensure that the bit representation of a is + // less than or equal to r - 1. + let mut a = self.value.map(|e| BitIterator::new(e.into_repr())); + let mut b = E::Fr::char(); + b.sub_noborrow(&1.into()); + + let mut result = vec![]; + + // Runs of ones in r + let mut last_run = None; + let mut current_run = vec![]; + + let mut found_one = false; + let mut i = 0; + for b in BitIterator::new(b) { + let a_bit = a.as_mut().map(|e| e.next().unwrap()); + + // Skip over unset bits at the beginning + found_one |= b; + if !found_one { + // a_bit should also be false + a_bit.map(|e| assert!(!e)); + continue; + } + + if b { + // This is part of a run of ones. Let's just + // allocate the boolean with the expected value. + let a_bit = AllocatedBit::alloc( + cs.namespace(|| format!("bit {}", i)), + a_bit + )?; + // ... and add it to the current run of ones. + current_run.push(a_bit.clone()); + result.push(a_bit); + } else { + if current_run.len() > 0 { + // This is the start of a run of zeros, but we need + // to k-ary AND against `last_run` first. + + if last_run.is_some() { + current_run.push(last_run.clone().unwrap()); + } + last_run = Some(kary_and( + cs.namespace(|| format!("run ending at {}", i)), + ¤t_run + )?); + current_run.truncate(0); + } + + // If `last_run` is true, `a` must be false, or it would + // not be in the field. + // + // If `last_run` is false, `a` can be true or false. + + let a_bit = AllocatedBit::alloc_conditionally( + cs.namespace(|| format!("bit {}", i)), + a_bit, + &last_run.as_ref().expect("char always starts with a one") + )?; + result.push(a_bit); + } + + i += 1; + } + + // char is prime, so we'll always end on + // a run of zeros. + assert_eq!(current_run.len(), 0); + + // Now, we have `result` in big-endian order. + // However, now we have to unpack self! + + let mut lc = LinearCombination::zero(); + let mut coeff = E::Fr::one(); + + for bit in result.iter().rev() { + lc = lc + (coeff, bit.get_variable()); + + coeff.double(); + } + + lc = lc - self.variable; + + cs.enforce( + || "unpacking constraint", + |lc| lc, + |lc| lc, + |_| lc + ); + + Ok(result.into_iter().map(|b| Boolean::from(b)).collect()) } pub fn into_bits( @@ -315,7 +434,6 @@ mod test { use pairing::{Field, PrimeField, BitIterator}; use ::circuit::test::*; use super::{AllocatedNum, Boolean}; - use super::super::boolean::AllocatedBit; #[test] fn test_allocated_num() { @@ -422,31 +540,25 @@ mod test { // make the bit representation the characteristic cs.set("bit 254/boolean", Fr::one()); - // this makes the unpacking constraint fail - assert_eq!(cs.which_is_unsatisfied().unwrap(), "unpacking constraint"); - - // fix it by making the number zero (congruent to the characteristic) - cs.set("num", Fr::zero()); - - // and constraint is disturbed during enforce in field check - assert_eq!(cs.which_is_unsatisfied().unwrap(), "nand 121/AND 0/and constraint"); - cs.set("nand 121/AND 0/and result", Fr::one()); - - // now the nand should fail (enforce in field is working) - assert_eq!(cs.which_is_unsatisfied().unwrap(), "nand 121/enforce nand"); + // this makes the conditional boolean constraint fail + assert_eq!(cs.which_is_unsatisfied().unwrap(), "bit 254/boolean constraint"); } #[test] fn test_into_bits() { let mut rng = XorShiftRng::from_seed([0x3dbe6259, 0x8d313d76, 0x3237db17, 0xe5bc0654]); - for _ in 0..100 { + for i in 0..200 { let r = Fr::rand(&mut rng); let mut cs = TestConstraintSystem::::new(); let n = AllocatedNum::alloc(&mut cs, || Ok(r)).unwrap(); - let bits = n.into_bits(&mut cs).unwrap(); + let bits = if i % 2 == 0 { + n.into_bits(&mut cs).unwrap() + } else { + n.into_bits_strict(&mut cs).unwrap() + }; assert!(cs.is_satisfied());