From 839442f2778386d5a96627232816ec2ab68e2100 Mon Sep 17 00:00:00 2001 From: Srinath Setty Date: Wed, 3 Jan 2024 22:07:01 +0000 Subject: [PATCH 1/2] add bitwise AND example --- examples/and.rs | 342 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 342 insertions(+) create mode 100644 examples/and.rs diff --git a/examples/and.rs b/examples/and.rs new file mode 100644 index 00000000..3c3c0a65 --- /dev/null +++ b/examples/and.rs @@ -0,0 +1,342 @@ +//! This example executes a batch of 64-bit AND operations. +//! It performs the AND operation by first decomposing the operands into bits and then performing the operation bit-by-bit. +//! We execute a configurable number of AND operations per step of Nova's recursion. +use bellpepper_core::{ + boolean::AllocatedBit, num::AllocatedNum, ConstraintSystem, LinearCombination, SynthesisError, +}; +use core::marker::PhantomData; +use ff::Field; +use ff::{PrimeField, PrimeFieldBits}; +use flate2::{write::ZlibEncoder, Compression}; +use nova_snark::{ + provider::{mlkzg::Bn256EngineKZG, GrumpkinEngine}, + traits::{ + circuit::{StepCircuit, TrivialCircuit}, + snark::RelaxedR1CSSNARKTrait, + Engine, Group, + }, + CompressedSNARK, PublicParams, RecursiveSNARK, +}; +use rand::Rng; +use std::time::Instant; + +type E1 = Bn256EngineKZG; +type E2 = GrumpkinEngine; +type EE1 = nova_snark::provider::mlkzg::EvaluationEngine; +type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine; +type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK; // non-preprocessing SNARK +type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK; // non-preprocessing SNARK + +#[derive(Clone, Debug)] +struct AndInstance { + a: u64, + b: u64, + _p: PhantomData, +} + +impl AndInstance { + // produces an AND instance + fn new() -> Self { + let mut rng = rand::thread_rng(); + let a: u64 = rng.gen(); + let b: u64 = rng.gen(); + Self { + a, + b, + _p: PhantomData, + } + } +} + +#[derive(Clone, Debug)] +struct AndCircuit { + batch: Vec>, +} + +impl AndCircuit { + // produces a batch of AND instances + fn new(num_ops_per_step: usize) -> Self { + let mut batch = Vec::new(); + for _ in 0..num_ops_per_step { + batch.push(AndInstance::new()); + } + Self { batch } + } +} + +pub fn u64_into_bit_vec_le>( + mut cs: CS, + value: Option, +) -> Result, SynthesisError> { + let values = match value { + Some(ref value) => { + let mut tmp = Vec::with_capacity(64); + + for i in 0..64 { + tmp.push(Some(*value >> i & 1 == 1)); + } + + tmp + } + None => vec![None; 64], + }; + + let bits = values + .into_iter() + .enumerate() + .map(|(i, b)| { + Ok(AllocatedBit::alloc( + cs.namespace(|| format!("bit {}", i)), + b, + )?) + }) + .collect::, SynthesisError>>()?; + + Ok(bits) +} + +/// Gets as input the little indian representation of a number and spits out the number +pub fn le_bits_to_num( + mut cs: CS, + bits: &[AllocatedBit], +) -> Result, SynthesisError> +where + Scalar: PrimeField + PrimeFieldBits, + CS: ConstraintSystem, +{ + // We loop over the input bits and construct the constraint + // and the field element that corresponds to the result + let mut lc = LinearCombination::zero(); + let mut coeff = Scalar::ONE; + let mut fe = Some(Scalar::ZERO); + for bit in bits.iter() { + lc = lc + (coeff, bit.get_variable()); + fe = bit.get_value().map(|val| { + if val { + fe.unwrap() + coeff + } else { + fe.unwrap() + } + }); + coeff = coeff.double(); + } + let num = AllocatedNum::alloc(cs.namespace(|| "Field element"), || { + fe.ok_or(SynthesisError::AssignmentMissing) + })?; + lc = lc - num.get_variable(); + cs.enforce(|| "compute number from bits", |lc| lc, |lc| lc, |_| lc); + Ok(num) +} + +impl StepCircuit for AndCircuit { + fn arity(&self) -> usize { + 1 + } + + fn synthesize>( + &self, + cs: &mut CS, + z_in: &[AllocatedNum], + ) -> Result>, SynthesisError> { + for i in 0..self.batch.len() { + // allocate a and b as field elements + let a = AllocatedNum::alloc(cs.namespace(|| format!("a_{}", i)), || { + Ok(G::Scalar::from(self.batch[i].a)) + })?; + let b = AllocatedNum::alloc(cs.namespace(|| format!("b_{}", i)), || { + Ok(G::Scalar::from(self.batch[i].b)) + })?; + + // obtain bit representations of a and b + let a_bits = u64_into_bit_vec_le( + cs.namespace(|| format!("a_bits_{}", i)), + Some(self.batch[i].a), + )?; // little endian + let b_bits = u64_into_bit_vec_le( + cs.namespace(|| format!("b_bits_{}", i)), + Some(self.batch[i].b), + )?; // little endian + + // enforce that bits of a and b are correct + let a_from_bits = le_bits_to_num(cs.namespace(|| format!("a_{}", i)), &a_bits)?; + let b_from_bits = le_bits_to_num(cs.namespace(|| format!("b_{}", i)), &b_bits)?; + + cs.enforce( + || format!("a_{} == a_from_bits", i), + |lc| lc + a.get_variable(), + |lc| lc + CS::one(), + |lc| lc + a_from_bits.get_variable(), + ); + cs.enforce( + || format!("b_{} == b_from_bits", i), + |lc| lc + b.get_variable(), + |lc| lc + CS::one(), + |lc| lc + b_from_bits.get_variable(), + ); + + let mut c_bits = Vec::new(); + + // perform bitwise AND + for i in 0..64 { + let c_bit = AllocatedBit::and( + cs.namespace(|| format!("and_bit_{}", i)), + &a_bits[i], + &b_bits[i], + )?; + c_bits.push(c_bit); + } + + // convert back to an allocated num + let c_from_bits = le_bits_to_num(cs.namespace(|| format!("c_{}", i)), &c_bits)?; + + let c = AllocatedNum::alloc(cs.namespace(|| format!("c_{}", i)), || { + Ok(G::Scalar::from(self.batch[i].a & self.batch[i].b)) + })?; + + // enforce that c is correct + cs.enforce( + || format!("c_{} == c_from_bits", i), + |lc| lc + c.get_variable(), + |lc| lc + CS::one(), + |lc| lc + c_from_bits.get_variable(), + ); + } + + Ok(z_in.to_vec()) + } +} + +/// cargo run --release --example and +fn main() { + println!("========================================================="); + println!("Nova-based 64-bit bitwise AND example"); + println!("========================================================="); + + let num_steps = 32; + for num_ops_per_step in [1024, 2048, 4096, 8192, 16384, 32768, 65536] { + // number of instances of AND per Nova's recursive step + let circuit_primary = AndCircuit::new(num_ops_per_step); + let circuit_secondary = TrivialCircuit::default(); + + println!( + "Proving {} AND ops ({num_ops_per_step} instances per step and {num_steps} steps)", + num_ops_per_step * num_steps + ); + + // produce public parameters + let start = Instant::now(); + println!("Producing public parameters..."); + let pp = PublicParams::< + E1, + E2, + AndCircuit<::GE>, + TrivialCircuit<::Scalar>, + >::setup( + &circuit_primary, + &circuit_secondary, + &*S1::ck_floor(), + &*S2::ck_floor(), + ); + println!("PublicParams::setup, took {:?} ", start.elapsed()); + + println!( + "Number of constraints per step (primary circuit): {}", + pp.num_constraints().0 + ); + println!( + "Number of constraints per step (secondary circuit): {}", + pp.num_constraints().1 + ); + + println!( + "Number of variables per step (primary circuit): {}", + pp.num_variables().0 + ); + println!( + "Number of variables per step (secondary circuit): {}", + pp.num_variables().1 + ); + + // produce non-deterministic advice + let circuits = (0..num_steps) + .map(|_| AndCircuit::new(num_ops_per_step)) + .collect::>(); + + type C1 = AndCircuit<::GE>; + type C2 = TrivialCircuit<::Scalar>; + + // produce a recursive SNARK + println!("Generating a RecursiveSNARK..."); + let mut recursive_snark: RecursiveSNARK = + RecursiveSNARK::::new( + &pp, + &circuits[0], + &circuit_secondary, + &[::Scalar::zero()], + &[::Scalar::zero()], + ) + .unwrap(); + + let start = Instant::now(); + for (_, circuit_primary) in circuits.iter().enumerate() { + let res = recursive_snark.prove_step(&pp, circuit_primary, &circuit_secondary); + assert!(res.is_ok()); + } + println!( + "RecursiveSNARK::prove {} AND ops: took {:?} ", + num_ops_per_step * num_steps, + start.elapsed() + ); + + // verify the recursive SNARK + println!("Verifying a RecursiveSNARK..."); + let res = recursive_snark.verify( + &pp, + num_steps, + &[::Scalar::ZERO], + &[::Scalar::ZERO], + ); + println!("RecursiveSNARK::verify: {:?}", res.is_ok(),); + assert!(res.is_ok()); + + // produce a compressed SNARK + println!("Generating a CompressedSNARK using Spartan with multilinear KZG..."); + let (pk, vk) = CompressedSNARK::<_, _, _, _, S1, S2>::setup(&pp).unwrap(); + + let start = Instant::now(); + + let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &pk, &recursive_snark); + println!( + "CompressedSNARK::prove: {:?}, took {:?}", + res.is_ok(), + start.elapsed() + ); + assert!(res.is_ok()); + let compressed_snark = res.unwrap(); + + let mut encoder = ZlibEncoder::new(Vec::new(), Compression::default()); + bincode::serialize_into(&mut encoder, &compressed_snark).unwrap(); + let compressed_snark_encoded = encoder.finish().unwrap(); + println!( + "CompressedSNARK::len {:?} bytes", + compressed_snark_encoded.len() + ); + + // verify the compressed SNARK + println!("Verifying a CompressedSNARK..."); + let start = Instant::now(); + let res = compressed_snark.verify( + &vk, + num_steps, + &[::Scalar::ZERO], + &[::Scalar::ZERO], + ); + println!( + "CompressedSNARK::verify: {:?}, took {:?}", + res.is_ok(), + start.elapsed() + ); + assert!(res.is_ok()); + println!("========================================================="); + } +} From 9cb16e894ed2e9d3522412d86acc4879bdb3a3ef Mon Sep 17 00:00:00 2001 From: Srinath Setty Date: Wed, 3 Jan 2024 13:42:47 -0800 Subject: [PATCH 2/2] fix cargo clippy --- examples/and.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/examples/and.rs b/examples/and.rs index 3c3c0a65..20daa112 100644 --- a/examples/and.rs +++ b/examples/and.rs @@ -84,12 +84,7 @@ pub fn u64_into_bit_vec_le>( let bits = values .into_iter() .enumerate() - .map(|(i, b)| { - Ok(AllocatedBit::alloc( - cs.namespace(|| format!("bit {}", i)), - b, - )?) - }) + .map(|(i, b)| AllocatedBit::alloc(cs.namespace(|| format!("bit {}", i)), b)) .collect::, SynthesisError>>()?; Ok(bits) @@ -278,7 +273,7 @@ fn main() { .unwrap(); let start = Instant::now(); - for (_, circuit_primary) in circuits.iter().enumerate() { + for circuit_primary in circuits.iter() { let res = recursive_snark.prove_step(&pp, circuit_primary, &circuit_secondary); assert!(res.is_ok()); }