From a9871b4a71bd868f8ff23290ae4095346e83172c Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Wed, 6 Mar 2024 16:49:12 +0100 Subject: [PATCH 01/21] Replace verbose fold. Add rayon `into_par_iter`. Fix tabulation Add missing import --- src/spartan/polys/eq.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/spartan/polys/eq.rs b/src/spartan/polys/eq.rs index 22ef1a1..cbe0884 100644 --- a/src/spartan/polys/eq.rs +++ b/src/spartan/polys/eq.rs @@ -1,6 +1,7 @@ //! `EqPolynomial`: Represents multilinear extension of equality polynomials, evaluated based on binary input values. use ff::PrimeField; +use rayon::iter::IntoParallelIterator; use rayon::prelude::{IndexedParallelIterator, IntoParallelRefMutIterator, ParallelIterator}; /// Represents the multilinear extension polynomial (MLE) of the equality polynomial $eq(x,e)$, denoted as $\tilde{eq}(x, e)$. @@ -35,8 +36,9 @@ impl EqPolynomial { pub fn evaluate(&self, rx: &[Scalar]) -> Scalar { assert_eq!(self.r.len(), rx.len()); (0..rx.len()) + .into_par_iter() .map(|i| rx[i] * self.r[i] + (Scalar::ONE - rx[i]) * (Scalar::ONE - self.r[i])) - .fold(Scalar::ONE, |acc, item| acc * item) + .product() } /// Evaluates the `EqPolynomial` at all the `2^|r|` points in its domain. From de83ff742723668cfcba1c9583fd431e0e39281b Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Thu, 7 Mar 2024 14:50:29 +0100 Subject: [PATCH 02/21] Add benchmarks Fix random `Fp` slice creation Fix formatting --- Cargo.toml | 4 ++++ benches/bench.rs | 23 +++++++++++++++++++++++ 2 files changed, 27 insertions(+) create mode 100644 benches/bench.rs diff --git a/Cargo.toml b/Cargo.toml index 89994ef..8aa97b6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -56,3 +56,7 @@ default = [] # Compiles in portable mode, w/o ISA extensions => binary can be executed on all systems. portable = ["pasta-msm/portable"] flamegraph = ["pprof/flamegraph", "pprof/criterion"] + +[[bench]] +name = "bench" +harness = false diff --git a/benches/bench.rs b/benches/bench.rs new file mode 100644 index 0000000..0ca4ea9 --- /dev/null +++ b/benches/bench.rs @@ -0,0 +1,23 @@ +extern crate core; + +use criterion::{criterion_group, criterion_main, Criterion}; +use ff::Field; +use pasta_curves::Fp; + +use spartan2::spartan::polys::eq::EqPolynomial; + +fn benchmarks_evaluate_incremental(c: &mut Criterion) { + let mut group = c.benchmark_group("evaluate_incremental"); + (1..=20).step_by(2).for_each(|i| { + group.bench_with_input(format!("2^{}", i), &i, |b, &i| { + let eq_polynomial = + EqPolynomial::new(vec![Fp::random(&mut rand::thread_rng()); 2usize.pow(i)]); + b.iter(|| { + eq_polynomial.evaluate(vec![Fp::random(&mut rand::thread_rng()); 2usize.pow(i)].as_slice()) + }); + }); + }); +} + +criterion_group!(benches, benchmarks_evaluate_incremental); +criterion_main!(benches); From eeb230ab5192d23ddbfe831a64309c0cd07cba9a Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Wed, 13 Mar 2024 19:04:50 +0100 Subject: [PATCH 03/21] Fix random `Fp` vector creation --- benches/bench.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/benches/bench.rs b/benches/bench.rs index 0ca4ea9..eab2dcd 100644 --- a/benches/bench.rs +++ b/benches/bench.rs @@ -9,11 +9,17 @@ use spartan2::spartan::polys::eq::EqPolynomial; fn benchmarks_evaluate_incremental(c: &mut Criterion) { let mut group = c.benchmark_group("evaluate_incremental"); (1..=20).step_by(2).for_each(|i| { - group.bench_with_input(format!("2^{}", i), &i, |b, &i| { - let eq_polynomial = - EqPolynomial::new(vec![Fp::random(&mut rand::thread_rng()); 2usize.pow(i)]); + let random_point: Vec = (0..2usize.pow(i)) + .map(|_| Fp::random(&mut rand::thread_rng())) + .collect(); + let random_polynomial = EqPolynomial::new( + (0..2usize.pow(i)) + .map(|_| Fp::random(&mut rand::thread_rng())) + .collect(), + ); + group.bench_with_input(format!("2^{}", i), &i, |b, &_i| { b.iter(|| { - eq_polynomial.evaluate(vec![Fp::random(&mut rand::thread_rng()); 2usize.pow(i)].as_slice()) + random_polynomial.evaluate(random_point.as_slice()); }); }); }); From 3ccd639dc61f89e12b2a7d4ee9d0af6ad243e072 Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Thu, 14 Mar 2024 14:21:34 +0100 Subject: [PATCH 04/21] Remove duplicate poly definitions --- src/spartan/polynomial.rs | 163 -------------------------------------- 1 file changed, 163 deletions(-) delete mode 100644 src/spartan/polynomial.rs diff --git a/src/spartan/polynomial.rs b/src/spartan/polynomial.rs deleted file mode 100644 index 18387f1..0000000 --- a/src/spartan/polynomial.rs +++ /dev/null @@ -1,163 +0,0 @@ -//! This module defines basic types related to polynomials -use core::ops::Index; -use ff::PrimeField; -use rayon::prelude::*; -use serde::{Deserialize, Serialize}; - -pub(crate) struct EqPolynomial { - r: Vec, -} - -impl EqPolynomial { - /// Creates a new polynomial from its succinct specification - pub fn new(r: Vec) -> Self { - EqPolynomial { r } - } - - /// Evaluates the polynomial at the specified point - pub fn evaluate(&self, rx: &[Scalar]) -> Scalar { - assert_eq!(self.r.len(), rx.len()); - (0..rx.len()) - .map(|i| rx[i] * self.r[i] + (Scalar::ONE - rx[i]) * (Scalar::ONE - self.r[i])) - .fold(Scalar::ONE, |acc, item| acc * item) - } - - pub fn evals(&self) -> Vec { - let ell = self.r.len(); - let mut evals: Vec = vec![Scalar::ZERO; (2_usize).pow(ell as u32)]; - let mut size = 1; - evals[0] = Scalar::ONE; - - for r in self.r.iter().rev() { - let (evals_left, evals_right) = evals.split_at_mut(size); - let (evals_right, _) = evals_right.split_at_mut(size); - - evals_left - .par_iter_mut() - .zip(evals_right.par_iter_mut()) - .for_each(|(x, y)| { - *y = *x * r; - *x -= &*y; - }); - - size *= 2; - } - evals - } -} - -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct MultilinearPolynomial { - num_vars: usize, // the number of variables in the multilinear polynomial - Z: Vec, // evaluations of the polynomial in all the 2^num_vars Boolean inputs -} - -impl MultilinearPolynomial { - pub fn new(Z: Vec) -> Self { - assert_eq!(Z.len(), (2_usize).pow((Z.len() as f64).log2() as u32)); - MultilinearPolynomial { - num_vars: (Z.len() as f64).log2() as usize, - Z, - } - } - - pub fn get_num_vars(&self) -> usize { - self.num_vars - } - - pub fn len(&self) -> usize { - self.Z.len() - } - - pub fn bound_poly_var_top(&mut self, r: &Scalar) { - let n = self.len() / 2; - - let (left, right) = self.Z.split_at_mut(n); - let (right, _) = right.split_at(n); - - left - .par_iter_mut() - .zip(right.par_iter()) - .for_each(|(a, b)| { - *a += *r * (*b - *a); - }); - - self.Z.resize(n, Scalar::ZERO); - self.num_vars -= 1; - } - - // returns Z(r) in O(n) time - pub fn evaluate(&self, r: &[Scalar]) -> Scalar { - // r must have a value for each variable - assert_eq!(r.len(), self.get_num_vars()); - let chis = EqPolynomial::new(r.to_vec()).evals(); - assert_eq!(chis.len(), self.Z.len()); - - (0..chis.len()) - .into_par_iter() - .map(|i| chis[i] * self.Z[i]) - .reduce(|| Scalar::ZERO, |x, y| x + y) - } - - pub fn evaluate_with(Z: &[Scalar], r: &[Scalar]) -> Scalar { - EqPolynomial::new(r.to_vec()) - .evals() - .into_par_iter() - .zip(Z.into_par_iter()) - .map(|(a, b)| a * b) - .reduce(|| Scalar::ZERO, |x, y| x + y) - } -} - -impl Index for MultilinearPolynomial { - type Output = Scalar; - - #[inline(always)] - fn index(&self, _index: usize) -> &Scalar { - &(self.Z[_index]) - } -} - -pub(crate) struct SparsePolynomial { - num_vars: usize, - Z: Vec<(usize, Scalar)>, -} - -impl SparsePolynomial { - pub fn new(num_vars: usize, Z: Vec<(usize, Scalar)>) -> Self { - SparsePolynomial { num_vars, Z } - } - - fn compute_chi(a: &[bool], r: &[Scalar]) -> Scalar { - assert_eq!(a.len(), r.len()); - let mut chi_i = Scalar::ONE; - for j in 0..r.len() { - if a[j] { - chi_i *= r[j]; - } else { - chi_i *= Scalar::ONE - r[j]; - } - } - chi_i - } - - // Takes O(n log n) - pub fn evaluate(&self, r: &[Scalar]) -> Scalar { - assert_eq!(self.num_vars, r.len()); - - let get_bits = |num: usize, num_bits: usize| -> Vec { - (0..num_bits) - .into_par_iter() - .map(|shift_amount| ((num & (1 << (num_bits - shift_amount - 1))) > 0)) - .collect::>() - }; - - (0..self.Z.len()) - .into_par_iter() - .map(|i| { - let bits = get_bits(self.Z[i].0, r.len()); - SparsePolynomial::compute_chi(&bits, r) * self.Z[i].1 - }) - .reduce(|| Scalar::ZERO, |x, y| x + y) - } -} From 111eec5b6186ab69def2daf7e04c7ef2a167d6a6 Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 8 Mar 2024 11:31:53 +0100 Subject: [PATCH 05/21] Co-authored-by: Cesar Descalzo Blanco MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove unnecessary `PhantomData` Co-authored-by: Antonio Mejías Gil Progress until 08/03 Co-authored-by: Antonio Mejías Gil constructing range check, wip working on padding println nightmare, issue apparently fixed Remove redundant padding. Fix import. code cleanup further cleanup found better way to fix padding the 'better way' to fix padding actually broke other tests - reverted This reverts commit d4727ba905065c3f5662699d48c2efb0a3e87feb. moved example to examples folder, refactored, tested many cases --- README.md | 6 +- examples/less_than.rs | 138 ++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 11 ++-- src/spartan/snark.rs | 28 +++++++++ 4 files changed, 175 insertions(+), 8 deletions(-) create mode 100644 examples/less_than.rs diff --git a/README.md b/README.md index 2986250..66b57a7 100644 --- a/README.md +++ b/README.md @@ -31,4 +31,8 @@ This project may contain trademarks or logos for projects, products, or services trademarks or logos is subject to and must follow [Microsoft's Trademark & Brand Guidelines](https://www.microsoft.com/en-us/legal/intellectualproperty/trademarks/usage/general). Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. -Any use of third-party trademarks or logos are subject to those third-party's policies. \ No newline at end of file +Any use of third-party trademarks or logos are subject to those third-party's policies. + +## Examples + +Run `cargo run --example EXAMPLE_NAME` to run the corresponding example. Leave `EXAMPLE_NAME` empty for a list of available examples. diff --git a/examples/less_than.rs b/examples/less_than.rs new file mode 100644 index 0000000..2f8a173 --- /dev/null +++ b/examples/less_than.rs @@ -0,0 +1,138 @@ +use bellpepper_core::{ + boolean::AllocatedBit, num::AllocatedNum, Circuit, ConstraintSystem, LinearCombination, + SynthesisError, +}; +use ff::{PrimeField, PrimeFieldBits}; +use spartan2::{ + errors::SpartanError, + traits::{snark::RelaxedR1CSSNARKTrait, Group}, + SNARK, +}; + +fn num_to_bits_le_bounded>( + cs: &mut CS, + n: AllocatedNum, + num_bits: u8, +) -> Result, SynthesisError> { + let opt_bits = match n.get_value() { + Some(v) => v + .to_le_bits() + .into_iter() + .take(num_bits as usize) + .map(|b| Some(b)) + .collect::>>(), + None => vec![None; num_bits as usize], + }; + + // Add one witness per input bit in little-endian bit order + let bits_circuit = opt_bits.into_iter() + .enumerate() + // AllocateBit enforces the value to be 0 or 1 at the constraint level + .map(|(i, b)| AllocatedBit::alloc(cs.namespace(|| format!("b_{}", i)), b).unwrap()) + .collect::>(); + + let mut weighted_sum_lc = LinearCombination::zero(); + let mut pow2 = F::ONE; + + for bit in bits_circuit.iter() { + weighted_sum_lc = weighted_sum_lc + (pow2, bit.get_variable()); + pow2 = pow2.double(); + } + + cs.enforce( + || "bit decomposition check", + |lc| lc + &weighted_sum_lc, + |lc| lc + CS::one(), + |lc| lc + n.get_variable(), + ); + + Ok(bits_circuit) +} + +// Range check: constrains input < `bound`. The bound must fit into +// `num_bits` bits (this is asserted in the circuit constructor). +// Important: it must be checked elsewhere that the input fits into +// `num_bits` bits - this is NOT constrained by this circuit in order to +// avoid duplications (hence "unsafe") +#[derive(Clone, Debug)] +struct LessThanCircuitUnsafe { + bound: u64, // Will be a constant in the constraits, not a variable + input: u64, // Will be an input/output variable + num_bits: u8, +} + +impl LessThanCircuitUnsafe { + fn new(bound: u64, input: u64, num_bits: u8) -> Self { + assert!(bound < (1 << num_bits)); + Self { + bound, + input, + num_bits, + } + } +} + +impl Circuit for LessThanCircuitUnsafe { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + assert!(F::NUM_BITS > self.num_bits as u32 + 1); + + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(F::from(self.input)))?; + + let shifted_diff = AllocatedNum::alloc(cs.namespace(|| "shifted_diff"), || { + Ok(F::from(self.input + (1 << self.num_bits) - self.bound)) + })?; + + cs.enforce( + || "shifted_diff_computation", + |lc| lc + input.get_variable() + (F::from((1 << self.num_bits) - self.bound), CS::one()), + |lc| lc + CS::one(), + |lc| lc + shifted_diff.get_variable(), + ); + + let shifted_diff_bits = num_to_bits_le_bounded::(cs, shifted_diff, self.num_bits + 1)?; + + // Check that the last (i.e. most sifnificant) bit is 0 + cs.enforce( + || "bound_check", + |lc| lc + shifted_diff_bits[self.num_bits as usize].get_variable(), + |lc| lc + CS::one(), + |lc| lc + (F::ZERO, CS::one()), + ); + + Ok(()) + } +} + +fn verify_circuit>( + bound: u64, + input: u64, + num_bits: u8, +) -> Result<(), SpartanError> { + let circuit = LessThanCircuitUnsafe::new(bound, input, num_bits); + + // produce keys + let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); + + // produce a SNARK + let snark = SNARK::prove(&pk, circuit).unwrap(); + + // verify the SNARK + snark.verify(&vk, &[]) +} + +fn main() { + type G = pasta_curves::pallas::Point; + type EE = spartan2::provider::ipa_pc::EvaluationEngine; + type S = spartan2::spartan::snark::RelaxedR1CSSNARK; + + // Typical exapmle, ok + assert!(verify_circuit::(17, 9, 10).is_ok()); + // Typical example, err + assert!(verify_circuit::(17, 20, 10).is_err()); + // Edge case, err + assert!(verify_circuit::(4, 4, 10).is_err()); + // Edge case, ok + assert!(verify_circuit::(4, 3, 10).is_ok()); + // Minimum number of bits, ok + assert!(verify_circuit::(4, 3, 3).is_ok()); +} diff --git a/src/lib.rs b/src/lib.rs index 5a60502..b55f0f0 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -76,6 +76,7 @@ impl, C: Circuit> SNARK Result<(ProverKey, VerifierKey), SpartanError> { let (pk, vk) = S::setup(circuit)?; + Ok((ProverKey { pk }, VerifierKey { vk })) } @@ -108,15 +109,12 @@ mod tests { use super::*; use crate::provider::{bn256_grumpkin::bn256, secp_secq::secp256k1}; use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; - use core::marker::PhantomData; use ff::PrimeField; #[derive(Clone, Debug, Default)] - struct CubicCircuit { - _p: PhantomData, - } + struct CubicCircuit {} - impl Circuit for CubicCircuit + impl Circuit for CubicCircuit where F: PrimeField, { @@ -178,8 +176,7 @@ mod tests { let circuit = CubicCircuit::default(); // produce keys - let (pk, vk) = - SNARK::::Scalar>>::setup(circuit.clone()).unwrap(); + let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); // produce a SNARK let res = SNARK::prove(&pk, circuit); diff --git a/src/spartan/snark.rs b/src/spartan/snark.rs index a1ad696..8520650 100644 --- a/src/spartan/snark.rs +++ b/src/spartan/snark.rs @@ -101,6 +101,26 @@ impl> RelaxedR1CSSNARKTrait for Relaxe ) -> Result<(Self::ProverKey, Self::VerifierKey), SpartanError> { let mut cs: ShapeCS = ShapeCS::new(); let _ = circuit.synthesize(&mut cs); + + // Padding the ShapeCS: constraints (rows) and variables (columns) + let num_constraints = cs.num_constraints(); + + (num_constraints..num_constraints.next_power_of_two()).for_each(|i| { + cs.enforce( + || format!("padding_constraint_{i}"), + |lc| lc, + |lc| lc, + |lc| lc, + ) + }); + + let num_vars = cs.num_aux(); + + (num_vars..num_vars.next_power_of_two()).for_each(|i| { + cs.alloc(|| format!("padding_var_{i}"), || Ok(G::Scalar::ZERO)) + .unwrap(); + }); + let (S, ck) = cs.r1cs_shape(); let (pk_ee, vk_ee) = EE::setup(&ck); @@ -121,6 +141,14 @@ impl> RelaxedR1CSSNARKTrait for Relaxe let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); let _ = circuit.synthesize(&mut cs); + // Padding variables + let num_vars = cs.aux_slice().len(); + + (num_vars..num_vars.next_power_of_two()).for_each(|i| { + cs.alloc(|| format!("padding_var_{i}"), || Ok(G::Scalar::ZERO)) + .unwrap(); + }); + let (u, w) = cs .r1cs_instance_and_witness(&pk.S, &pk.ck) .map_err(|_e| SpartanError::UnSat)?; From 618623d4323e55f3ef760b62049f353e7dc6eb5a Mon Sep 17 00:00:00 2001 From: mmagician Date: Thu, 14 Mar 2024 17:04:25 +0100 Subject: [PATCH 06/21] fix minor clippy warnings --- src/provider/keccak.rs | 2 +- src/spartan/sumcheck.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/provider/keccak.rs b/src/provider/keccak.rs index 119478e..849ae30 100644 --- a/src/provider/keccak.rs +++ b/src/provider/keccak.rs @@ -155,7 +155,7 @@ mod tests { fn test_keccak_example() { let mut hasher = Keccak256::new(); hasher.update(0xffffffff_u32.to_le_bytes()); - let output: [u8; 32] = hasher.finalize().try_into().unwrap(); + let output: [u8; 32] = hasher.finalize().into(); assert_eq!( hex::encode(output), "29045a592007d0c246ef02c2223570da9522d0cf0f73282c79a1bc8f0bb2c238" diff --git a/src/spartan/sumcheck.rs b/src/spartan/sumcheck.rs index 08fd1da..a547b0d 100644 --- a/src/spartan/sumcheck.rs +++ b/src/spartan/sumcheck.rs @@ -142,8 +142,8 @@ impl SumcheckProof { pub fn prove_quad_batch( claim: &G::Scalar, num_rounds: usize, - poly_A_vec: &mut Vec>, - poly_B_vec: &mut Vec>, + poly_A_vec: &mut [MultilinearPolynomial], + poly_B_vec: &mut [MultilinearPolynomial], coeffs: &[G::Scalar], comb_func: F, transcript: &mut G::TE, From a88763f0ef76a341ddc53ab710277e809940bc55 Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 15 Mar 2024 11:28:27 +0100 Subject: [PATCH 07/21] Add LessThanCircuitSafe example. Pass arguments as field elements instead of unsigned integers. --- examples/less_than.rs | 128 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 106 insertions(+), 22 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 2f8a173..973f5f7 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -3,6 +3,7 @@ use bellpepper_core::{ SynthesisError, }; use ff::{PrimeField, PrimeFieldBits}; +use pasta_curves::Fq; use spartan2::{ errors::SpartanError, traits::{snark::RelaxedR1CSSNARKTrait, Group}, @@ -49,21 +50,32 @@ fn num_to_bits_le_bounded(n: F) -> u8 { + let bits = n.to_le_bits(); + let mut msb_index = 0; + for (i, b) in bits.iter().enumerate() { + if *b { + msb_index = i as u8; + } + } + msb_index +} + // Range check: constrains input < `bound`. The bound must fit into // `num_bits` bits (this is asserted in the circuit constructor). // Important: it must be checked elsewhere that the input fits into // `num_bits` bits - this is NOT constrained by this circuit in order to // avoid duplications (hence "unsafe") #[derive(Clone, Debug)] -struct LessThanCircuitUnsafe { - bound: u64, // Will be a constant in the constraits, not a variable - input: u64, // Will be an input/output variable +struct LessThanCircuitUnsafe { + bound: F, // Will be a constant in the constraits, not a variable + input: F, // Will be an input/output variable num_bits: u8, } -impl LessThanCircuitUnsafe { - fn new(bound: u64, input: u64, num_bits: u8) -> Self { - assert!(bound < (1 << num_bits)); +impl LessThanCircuitUnsafe { + fn new(bound: F, input: F, num_bits: u8) -> Self { + assert!(get_msb_index(bound) < num_bits); Self { bound, input, @@ -72,20 +84,20 @@ impl LessThanCircuitUnsafe { } } -impl Circuit for LessThanCircuitUnsafe { +impl Circuit for LessThanCircuitUnsafe { fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { assert!(F::NUM_BITS > self.num_bits as u32 + 1); - let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(F::from(self.input)))?; + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(self.input))?; let shifted_diff = AllocatedNum::alloc(cs.namespace(|| "shifted_diff"), || { - Ok(F::from(self.input + (1 << self.num_bits) - self.bound)) + Ok(self.input + F::from(1 << self.num_bits) - self.bound) })?; cs.enforce( || "shifted_diff_computation", - |lc| lc + input.get_variable() + (F::from((1 << self.num_bits) - self.bound), CS::one()), - |lc| lc + CS::one(), + |lc| lc + input.get_variable() + (F::from(1 << self.num_bits) - self.bound, CS::one()), + |lc: LinearCombination| lc + CS::one(), |lc| lc + shifted_diff.get_variable(), ); @@ -103,15 +115,70 @@ impl Circuit for LessThanCircuitUnsafe { } } -fn verify_circuit>( - bound: u64, - input: u64, +#[derive(Clone, Debug)] +struct LessThanCircuitSafe { + bound: F, + input: F, + num_bits: u8, +} + +impl LessThanCircuitSafe { + fn new(bound: F, input: F, num_bits: u8) -> Self { + assert!(get_msb_index(bound) < num_bits); + Self { + bound, + input, + num_bits, + } + } +} + +impl Circuit for LessThanCircuitSafe { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(self.input))?; + + // Perform the input bit decomposition check + num_to_bits_le_bounded::(cs, input, self.num_bits)?; + + // Entering a new namespace to prefix variables in the + // LessThanCircuitUnsafe, thus avoiding name clashes + cs.push_namespace(|| "less_than_safe"); + + LessThanCircuitUnsafe { + bound: self.bound, + input: self.input, + num_bits: self.num_bits, + } + .synthesize(cs) + } +} + +fn verify_circuit_unsafe>( + bound: G::Scalar, + input: G::Scalar, num_bits: u8, ) -> Result<(), SpartanError> { let circuit = LessThanCircuitUnsafe::new(bound, input, num_bits); // produce keys - let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); + let (pk, vk) = SNARK::>::setup(circuit.clone()).unwrap(); + + // produce a SNARK + let snark = SNARK::prove(&pk, circuit).unwrap(); + + // verify the SNARK + snark.verify(&vk, &[]) +} + +fn verify_circuit_safe>( + bound: G::Scalar, + input: G::Scalar, + num_bits: u8, +) -> Result<(), SpartanError> { + let circuit = LessThanCircuitSafe::new(bound, input, num_bits); + + // produce keys + let (pk, vk) = SNARK::>::setup(circuit.clone()).unwrap(); // produce a SNARK let snark = SNARK::prove(&pk, circuit).unwrap(); @@ -125,14 +192,31 @@ fn main() { type EE = spartan2::provider::ipa_pc::EvaluationEngine; type S = spartan2::spartan::snark::RelaxedR1CSSNARK; - // Typical exapmle, ok - assert!(verify_circuit::(17, 9, 10).is_ok()); + println!("Executing unsafe circuit..."); + //Typical example, ok + assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + // Typical example, err + assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + // Edge case, err + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + // Edge case, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + // Minimum number of bits for the bound, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + // Insufficient number of bits for the input, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + + println!("Executing safe circuit..."); + // Typical example, ok + assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); // Typical example, err - assert!(verify_circuit::(17, 20, 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); // Edge case, err - assert!(verify_circuit::(4, 4, 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); // Edge case, ok - assert!(verify_circuit::(4, 3, 10).is_ok()); - // Minimum number of bits, ok - assert!(verify_circuit::(4, 3, 3).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + // Minimum number of bits for the bound, ok + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + // Insufficient number of bits for the input, err + assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); } From 7f84d287103a18dad4d612e3b6377fc2a5d70aa6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 11:41:00 +0100 Subject: [PATCH 08/21] added some documentation --- examples/less_than.rs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 973f5f7..6d5a0b9 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -63,9 +63,10 @@ fn get_msb_index(n: F) -> u8 { // Range check: constrains input < `bound`. The bound must fit into // `num_bits` bits (this is asserted in the circuit constructor). -// Important: it must be checked elsewhere that the input fits into -// `num_bits` bits - this is NOT constrained by this circuit in order to -// avoid duplications (hence "unsafe") +// Important: it must be checked elsewhere (in an overarching circuit) that the +// input fits into `num_bits` bits - this is NOT constrained by this circuit +// in order to avoid duplications (hence "unsafe"). Cf. LessThanCircuitSafe for +// a safe version. #[derive(Clone, Debug)] struct LessThanCircuitUnsafe { bound: F, // Will be a constant in the constraits, not a variable @@ -115,6 +116,10 @@ impl Circuit for LessThanCircuitUnsafe { } } +// Range check: constrains input < `bound`. The bound must fit into +// `num_bits` bits (this is asserted in the circuit constructor). +// Furthermore, the input must fit into `num_bits`, which is enforced at the +// constraint level. #[derive(Clone, Debug)] struct LessThanCircuitSafe { bound: F, @@ -203,7 +208,9 @@ fn main() { assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); // Minimum number of bits for the bound, ok assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); - // Insufficient number of bits for the input, ok + // Insufficient number of bits for the input, but this is not detected by the + // unsafety of the circuit (compare with the last example below) + // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); println!("Executing safe circuit..."); @@ -217,6 +224,8 @@ fn main() { assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); // Minimum number of bits for the bound, ok assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); - // Insufficient number of bits for the input, err + // Insufficient number of bits for the input, err (compare with the last example + // above). + // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); } From 7cd65ad608c1717610f68e2256144243853ef864 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 11:44:04 +0100 Subject: [PATCH 09/21] added message --- examples/less_than.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/examples/less_than.rs b/examples/less_than.rs index 6d5a0b9..6cee258 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -213,6 +213,8 @@ fn main() { // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + println!("Unsafe circuit OK"); + println!("Executing safe circuit..."); // Typical example, ok assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); @@ -228,4 +230,6 @@ fn main() { // above). // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); + + println!("Safe circuit OK"); } From f6725c8cc265bbf3eea5599bcb6f7535255857b9 Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 15 Mar 2024 13:04:54 +0100 Subject: [PATCH 10/21] Remove unnecesary u64 hints. Cleanup get_msb_index. --- examples/less_than.rs | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 6cee258..9d5e3a8 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -51,14 +51,13 @@ fn num_to_bits_le_bounded(n: F) -> u8 { - let bits = n.to_le_bits(); - let mut msb_index = 0; - for (i, b) in bits.iter().enumerate() { - if *b { - msb_index = i as u8; - } - } - msb_index + n.to_le_bits() + .into_iter() + .enumerate() + .rev() + .find(|(_, b)| *b) + .unwrap() + .0 as u8 } // Range check: constrains input < `bound`. The bound must fit into @@ -199,37 +198,37 @@ fn main() { println!("Executing unsafe circuit..."); //Typical example, ok - assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(17), Fq::from(9), 10).is_ok()); // Typical example, err - assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + assert!(verify_circuit_unsafe::(Fq::from(17), Fq::from(20), 10).is_err()); // Edge case, err - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(4), 10).is_err()); // Edge case, ok - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(3), 10).is_ok()); // Minimum number of bits for the bound, ok - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(3), 3).is_ok()); // Insufficient number of bits for the input, but this is not detected by the // unsafety of the circuit (compare with the last example below) // Note that -Fq::one() is corresponds to q - 1 > bound - assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), -Fq::one(), 3).is_ok()); println!("Unsafe circuit OK"); println!("Executing safe circuit..."); // Typical example, ok - assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + assert!(verify_circuit_safe::(Fq::from(17), Fq::from(9), 10).is_ok()); // Typical example, err - assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(17), Fq::from(20), 10).is_err()); // Edge case, err - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(4), 10).is_err()); // Edge case, ok - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(3), 10).is_ok()); // Minimum number of bits for the bound, ok - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(3), 3).is_ok()); // Insufficient number of bits for the input, err (compare with the last example // above). // Note that -Fq::one() is corresponds to q - 1 > bound - assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); + assert!(verify_circuit_safe::(Fq::from(4), -Fq::one(), 3).is_err()); println!("Safe circuit OK"); } From eb2843e26ff653d074ecaef5b1a47876e832f964 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 15:33:47 +0100 Subject: [PATCH 11/21] fixed clippy warning --- examples/less_than.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 9d5e3a8..9f4d3aa 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -20,7 +20,7 @@ fn num_to_bits_le_bounded>>(), None => vec![None; num_bits as usize], }; From 9c71a23156ac0bb4d34c7a05e99089940a22a915 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Mon, 18 Mar 2024 17:10:46 +0100 Subject: [PATCH 12/21] tweaked documentation --- examples/less_than.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 9f4d3aa..a3bac59 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -60,8 +60,9 @@ fn get_msb_index(n: F) -> u8 { .0 as u8 } -// Range check: constrains input < `bound`. The bound must fit into -// `num_bits` bits (this is asserted in the circuit constructor). +// Constrains `input` < `bound`, where the LHS is a witness and the RHS is a +// constant. The bound must fit into `num_bits` bits (this is asserted in the +// circuit constructor). // Important: it must be checked elsewhere (in an overarching circuit) that the // input fits into `num_bits` bits - this is NOT constrained by this circuit // in order to avoid duplications (hence "unsafe"). Cf. LessThanCircuitSafe for @@ -115,8 +116,9 @@ impl Circuit for LessThanCircuitUnsafe { } } -// Range check: constrains input < `bound`. The bound must fit into -// `num_bits` bits (this is asserted in the circuit constructor). +// Constrains `input` < `bound`, where the LHS is a witness and the RHS is a +// constant. The bound must fit into `num_bits` bits (this is asserted in the +// circuit constructor). // Furthermore, the input must fit into `num_bits`, which is enforced at the // constraint level. #[derive(Clone, Debug)] From a090d69e8b2643310938f3076359b57d359a1e4a Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 8 Mar 2024 11:31:53 +0100 Subject: [PATCH 13/21] Co-authored-by: Cesar Descalzo Blanco MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove unnecessary `PhantomData` Co-authored-by: Antonio Mejías Gil Progress until 08/03 Co-authored-by: Antonio Mejías Gil constructing range check, wip working on padding println nightmare, issue apparently fixed Remove redundant padding. Fix import. code cleanup further cleanup found better way to fix padding the 'better way' to fix padding actually broke other tests - reverted This reverts commit d4727ba905065c3f5662699d48c2efb0a3e87feb. moved example to examples folder, refactored, tested many cases --- README.md | 6 +- examples/less_than.rs | 138 ++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 11 ++-- src/spartan/snark.rs | 28 +++++++++ 4 files changed, 175 insertions(+), 8 deletions(-) create mode 100644 examples/less_than.rs diff --git a/README.md b/README.md index 2986250..66b57a7 100644 --- a/README.md +++ b/README.md @@ -31,4 +31,8 @@ This project may contain trademarks or logos for projects, products, or services trademarks or logos is subject to and must follow [Microsoft's Trademark & Brand Guidelines](https://www.microsoft.com/en-us/legal/intellectualproperty/trademarks/usage/general). Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. -Any use of third-party trademarks or logos are subject to those third-party's policies. \ No newline at end of file +Any use of third-party trademarks or logos are subject to those third-party's policies. + +## Examples + +Run `cargo run --example EXAMPLE_NAME` to run the corresponding example. Leave `EXAMPLE_NAME` empty for a list of available examples. diff --git a/examples/less_than.rs b/examples/less_than.rs new file mode 100644 index 0000000..2f8a173 --- /dev/null +++ b/examples/less_than.rs @@ -0,0 +1,138 @@ +use bellpepper_core::{ + boolean::AllocatedBit, num::AllocatedNum, Circuit, ConstraintSystem, LinearCombination, + SynthesisError, +}; +use ff::{PrimeField, PrimeFieldBits}; +use spartan2::{ + errors::SpartanError, + traits::{snark::RelaxedR1CSSNARKTrait, Group}, + SNARK, +}; + +fn num_to_bits_le_bounded>( + cs: &mut CS, + n: AllocatedNum, + num_bits: u8, +) -> Result, SynthesisError> { + let opt_bits = match n.get_value() { + Some(v) => v + .to_le_bits() + .into_iter() + .take(num_bits as usize) + .map(|b| Some(b)) + .collect::>>(), + None => vec![None; num_bits as usize], + }; + + // Add one witness per input bit in little-endian bit order + let bits_circuit = opt_bits.into_iter() + .enumerate() + // AllocateBit enforces the value to be 0 or 1 at the constraint level + .map(|(i, b)| AllocatedBit::alloc(cs.namespace(|| format!("b_{}", i)), b).unwrap()) + .collect::>(); + + let mut weighted_sum_lc = LinearCombination::zero(); + let mut pow2 = F::ONE; + + for bit in bits_circuit.iter() { + weighted_sum_lc = weighted_sum_lc + (pow2, bit.get_variable()); + pow2 = pow2.double(); + } + + cs.enforce( + || "bit decomposition check", + |lc| lc + &weighted_sum_lc, + |lc| lc + CS::one(), + |lc| lc + n.get_variable(), + ); + + Ok(bits_circuit) +} + +// Range check: constrains input < `bound`. The bound must fit into +// `num_bits` bits (this is asserted in the circuit constructor). +// Important: it must be checked elsewhere that the input fits into +// `num_bits` bits - this is NOT constrained by this circuit in order to +// avoid duplications (hence "unsafe") +#[derive(Clone, Debug)] +struct LessThanCircuitUnsafe { + bound: u64, // Will be a constant in the constraits, not a variable + input: u64, // Will be an input/output variable + num_bits: u8, +} + +impl LessThanCircuitUnsafe { + fn new(bound: u64, input: u64, num_bits: u8) -> Self { + assert!(bound < (1 << num_bits)); + Self { + bound, + input, + num_bits, + } + } +} + +impl Circuit for LessThanCircuitUnsafe { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + assert!(F::NUM_BITS > self.num_bits as u32 + 1); + + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(F::from(self.input)))?; + + let shifted_diff = AllocatedNum::alloc(cs.namespace(|| "shifted_diff"), || { + Ok(F::from(self.input + (1 << self.num_bits) - self.bound)) + })?; + + cs.enforce( + || "shifted_diff_computation", + |lc| lc + input.get_variable() + (F::from((1 << self.num_bits) - self.bound), CS::one()), + |lc| lc + CS::one(), + |lc| lc + shifted_diff.get_variable(), + ); + + let shifted_diff_bits = num_to_bits_le_bounded::(cs, shifted_diff, self.num_bits + 1)?; + + // Check that the last (i.e. most sifnificant) bit is 0 + cs.enforce( + || "bound_check", + |lc| lc + shifted_diff_bits[self.num_bits as usize].get_variable(), + |lc| lc + CS::one(), + |lc| lc + (F::ZERO, CS::one()), + ); + + Ok(()) + } +} + +fn verify_circuit>( + bound: u64, + input: u64, + num_bits: u8, +) -> Result<(), SpartanError> { + let circuit = LessThanCircuitUnsafe::new(bound, input, num_bits); + + // produce keys + let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); + + // produce a SNARK + let snark = SNARK::prove(&pk, circuit).unwrap(); + + // verify the SNARK + snark.verify(&vk, &[]) +} + +fn main() { + type G = pasta_curves::pallas::Point; + type EE = spartan2::provider::ipa_pc::EvaluationEngine; + type S = spartan2::spartan::snark::RelaxedR1CSSNARK; + + // Typical exapmle, ok + assert!(verify_circuit::(17, 9, 10).is_ok()); + // Typical example, err + assert!(verify_circuit::(17, 20, 10).is_err()); + // Edge case, err + assert!(verify_circuit::(4, 4, 10).is_err()); + // Edge case, ok + assert!(verify_circuit::(4, 3, 10).is_ok()); + // Minimum number of bits, ok + assert!(verify_circuit::(4, 3, 3).is_ok()); +} diff --git a/src/lib.rs b/src/lib.rs index 5a60502..b55f0f0 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -76,6 +76,7 @@ impl, C: Circuit> SNARK Result<(ProverKey, VerifierKey), SpartanError> { let (pk, vk) = S::setup(circuit)?; + Ok((ProverKey { pk }, VerifierKey { vk })) } @@ -108,15 +109,12 @@ mod tests { use super::*; use crate::provider::{bn256_grumpkin::bn256, secp_secq::secp256k1}; use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; - use core::marker::PhantomData; use ff::PrimeField; #[derive(Clone, Debug, Default)] - struct CubicCircuit { - _p: PhantomData, - } + struct CubicCircuit {} - impl Circuit for CubicCircuit + impl Circuit for CubicCircuit where F: PrimeField, { @@ -178,8 +176,7 @@ mod tests { let circuit = CubicCircuit::default(); // produce keys - let (pk, vk) = - SNARK::::Scalar>>::setup(circuit.clone()).unwrap(); + let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); // produce a SNARK let res = SNARK::prove(&pk, circuit); diff --git a/src/spartan/snark.rs b/src/spartan/snark.rs index a1ad696..8520650 100644 --- a/src/spartan/snark.rs +++ b/src/spartan/snark.rs @@ -101,6 +101,26 @@ impl> RelaxedR1CSSNARKTrait for Relaxe ) -> Result<(Self::ProverKey, Self::VerifierKey), SpartanError> { let mut cs: ShapeCS = ShapeCS::new(); let _ = circuit.synthesize(&mut cs); + + // Padding the ShapeCS: constraints (rows) and variables (columns) + let num_constraints = cs.num_constraints(); + + (num_constraints..num_constraints.next_power_of_two()).for_each(|i| { + cs.enforce( + || format!("padding_constraint_{i}"), + |lc| lc, + |lc| lc, + |lc| lc, + ) + }); + + let num_vars = cs.num_aux(); + + (num_vars..num_vars.next_power_of_two()).for_each(|i| { + cs.alloc(|| format!("padding_var_{i}"), || Ok(G::Scalar::ZERO)) + .unwrap(); + }); + let (S, ck) = cs.r1cs_shape(); let (pk_ee, vk_ee) = EE::setup(&ck); @@ -121,6 +141,14 @@ impl> RelaxedR1CSSNARKTrait for Relaxe let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); let _ = circuit.synthesize(&mut cs); + // Padding variables + let num_vars = cs.aux_slice().len(); + + (num_vars..num_vars.next_power_of_two()).for_each(|i| { + cs.alloc(|| format!("padding_var_{i}"), || Ok(G::Scalar::ZERO)) + .unwrap(); + }); + let (u, w) = cs .r1cs_instance_and_witness(&pk.S, &pk.ck) .map_err(|_e| SpartanError::UnSat)?; From 7eef1340d2b9d89226f34734819fc1069a1cca54 Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 15 Mar 2024 11:28:27 +0100 Subject: [PATCH 14/21] Add LessThanCircuitSafe example. Pass arguments as field elements instead of unsigned integers. --- examples/less_than.rs | 128 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 106 insertions(+), 22 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 2f8a173..973f5f7 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -3,6 +3,7 @@ use bellpepper_core::{ SynthesisError, }; use ff::{PrimeField, PrimeFieldBits}; +use pasta_curves::Fq; use spartan2::{ errors::SpartanError, traits::{snark::RelaxedR1CSSNARKTrait, Group}, @@ -49,21 +50,32 @@ fn num_to_bits_le_bounded(n: F) -> u8 { + let bits = n.to_le_bits(); + let mut msb_index = 0; + for (i, b) in bits.iter().enumerate() { + if *b { + msb_index = i as u8; + } + } + msb_index +} + // Range check: constrains input < `bound`. The bound must fit into // `num_bits` bits (this is asserted in the circuit constructor). // Important: it must be checked elsewhere that the input fits into // `num_bits` bits - this is NOT constrained by this circuit in order to // avoid duplications (hence "unsafe") #[derive(Clone, Debug)] -struct LessThanCircuitUnsafe { - bound: u64, // Will be a constant in the constraits, not a variable - input: u64, // Will be an input/output variable +struct LessThanCircuitUnsafe { + bound: F, // Will be a constant in the constraits, not a variable + input: F, // Will be an input/output variable num_bits: u8, } -impl LessThanCircuitUnsafe { - fn new(bound: u64, input: u64, num_bits: u8) -> Self { - assert!(bound < (1 << num_bits)); +impl LessThanCircuitUnsafe { + fn new(bound: F, input: F, num_bits: u8) -> Self { + assert!(get_msb_index(bound) < num_bits); Self { bound, input, @@ -72,20 +84,20 @@ impl LessThanCircuitUnsafe { } } -impl Circuit for LessThanCircuitUnsafe { +impl Circuit for LessThanCircuitUnsafe { fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { assert!(F::NUM_BITS > self.num_bits as u32 + 1); - let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(F::from(self.input)))?; + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(self.input))?; let shifted_diff = AllocatedNum::alloc(cs.namespace(|| "shifted_diff"), || { - Ok(F::from(self.input + (1 << self.num_bits) - self.bound)) + Ok(self.input + F::from(1 << self.num_bits) - self.bound) })?; cs.enforce( || "shifted_diff_computation", - |lc| lc + input.get_variable() + (F::from((1 << self.num_bits) - self.bound), CS::one()), - |lc| lc + CS::one(), + |lc| lc + input.get_variable() + (F::from(1 << self.num_bits) - self.bound, CS::one()), + |lc: LinearCombination| lc + CS::one(), |lc| lc + shifted_diff.get_variable(), ); @@ -103,15 +115,70 @@ impl Circuit for LessThanCircuitUnsafe { } } -fn verify_circuit>( - bound: u64, - input: u64, +#[derive(Clone, Debug)] +struct LessThanCircuitSafe { + bound: F, + input: F, + num_bits: u8, +} + +impl LessThanCircuitSafe { + fn new(bound: F, input: F, num_bits: u8) -> Self { + assert!(get_msb_index(bound) < num_bits); + Self { + bound, + input, + num_bits, + } + } +} + +impl Circuit for LessThanCircuitSafe { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + let input = AllocatedNum::alloc(cs.namespace(|| "input"), || Ok(self.input))?; + + // Perform the input bit decomposition check + num_to_bits_le_bounded::(cs, input, self.num_bits)?; + + // Entering a new namespace to prefix variables in the + // LessThanCircuitUnsafe, thus avoiding name clashes + cs.push_namespace(|| "less_than_safe"); + + LessThanCircuitUnsafe { + bound: self.bound, + input: self.input, + num_bits: self.num_bits, + } + .synthesize(cs) + } +} + +fn verify_circuit_unsafe>( + bound: G::Scalar, + input: G::Scalar, num_bits: u8, ) -> Result<(), SpartanError> { let circuit = LessThanCircuitUnsafe::new(bound, input, num_bits); // produce keys - let (pk, vk) = SNARK::::setup(circuit.clone()).unwrap(); + let (pk, vk) = SNARK::>::setup(circuit.clone()).unwrap(); + + // produce a SNARK + let snark = SNARK::prove(&pk, circuit).unwrap(); + + // verify the SNARK + snark.verify(&vk, &[]) +} + +fn verify_circuit_safe>( + bound: G::Scalar, + input: G::Scalar, + num_bits: u8, +) -> Result<(), SpartanError> { + let circuit = LessThanCircuitSafe::new(bound, input, num_bits); + + // produce keys + let (pk, vk) = SNARK::>::setup(circuit.clone()).unwrap(); // produce a SNARK let snark = SNARK::prove(&pk, circuit).unwrap(); @@ -125,14 +192,31 @@ fn main() { type EE = spartan2::provider::ipa_pc::EvaluationEngine; type S = spartan2::spartan::snark::RelaxedR1CSSNARK; - // Typical exapmle, ok - assert!(verify_circuit::(17, 9, 10).is_ok()); + println!("Executing unsafe circuit..."); + //Typical example, ok + assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + // Typical example, err + assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + // Edge case, err + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + // Edge case, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + // Minimum number of bits for the bound, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + // Insufficient number of bits for the input, ok + assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + + println!("Executing safe circuit..."); + // Typical example, ok + assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); // Typical example, err - assert!(verify_circuit::(17, 20, 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); // Edge case, err - assert!(verify_circuit::(4, 4, 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); // Edge case, ok - assert!(verify_circuit::(4, 3, 10).is_ok()); - // Minimum number of bits, ok - assert!(verify_circuit::(4, 3, 3).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + // Minimum number of bits for the bound, ok + assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + // Insufficient number of bits for the input, err + assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); } From 24cb75bee0389c353fe620977a93f18b1b4281c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 11:41:00 +0100 Subject: [PATCH 15/21] added some documentation --- examples/less_than.rs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 973f5f7..6d5a0b9 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -63,9 +63,10 @@ fn get_msb_index(n: F) -> u8 { // Range check: constrains input < `bound`. The bound must fit into // `num_bits` bits (this is asserted in the circuit constructor). -// Important: it must be checked elsewhere that the input fits into -// `num_bits` bits - this is NOT constrained by this circuit in order to -// avoid duplications (hence "unsafe") +// Important: it must be checked elsewhere (in an overarching circuit) that the +// input fits into `num_bits` bits - this is NOT constrained by this circuit +// in order to avoid duplications (hence "unsafe"). Cf. LessThanCircuitSafe for +// a safe version. #[derive(Clone, Debug)] struct LessThanCircuitUnsafe { bound: F, // Will be a constant in the constraits, not a variable @@ -115,6 +116,10 @@ impl Circuit for LessThanCircuitUnsafe { } } +// Range check: constrains input < `bound`. The bound must fit into +// `num_bits` bits (this is asserted in the circuit constructor). +// Furthermore, the input must fit into `num_bits`, which is enforced at the +// constraint level. #[derive(Clone, Debug)] struct LessThanCircuitSafe { bound: F, @@ -203,7 +208,9 @@ fn main() { assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); // Minimum number of bits for the bound, ok assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); - // Insufficient number of bits for the input, ok + // Insufficient number of bits for the input, but this is not detected by the + // unsafety of the circuit (compare with the last example below) + // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); println!("Executing safe circuit..."); @@ -217,6 +224,8 @@ fn main() { assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); // Minimum number of bits for the bound, ok assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); - // Insufficient number of bits for the input, err + // Insufficient number of bits for the input, err (compare with the last example + // above). + // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); } From d447c63ec572881ddc6574aa2f41e8e1e5c0cfda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 11:44:04 +0100 Subject: [PATCH 16/21] added message --- examples/less_than.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/examples/less_than.rs b/examples/less_than.rs index 6d5a0b9..6cee258 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -213,6 +213,8 @@ fn main() { // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + println!("Unsafe circuit OK"); + println!("Executing safe circuit..."); // Typical example, ok assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); @@ -228,4 +230,6 @@ fn main() { // above). // Note that -Fq::one() is corresponds to q - 1 > bound assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); + + println!("Safe circuit OK"); } From e38e357511092c6a0c4c982d94568cc14745a69b Mon Sep 17 00:00:00 2001 From: Cesar Descalzo Blanco Date: Fri, 15 Mar 2024 13:04:54 +0100 Subject: [PATCH 17/21] Remove unnecesary u64 hints. Cleanup get_msb_index. --- examples/less_than.rs | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 6cee258..9d5e3a8 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -51,14 +51,13 @@ fn num_to_bits_le_bounded(n: F) -> u8 { - let bits = n.to_le_bits(); - let mut msb_index = 0; - for (i, b) in bits.iter().enumerate() { - if *b { - msb_index = i as u8; - } - } - msb_index + n.to_le_bits() + .into_iter() + .enumerate() + .rev() + .find(|(_, b)| *b) + .unwrap() + .0 as u8 } // Range check: constrains input < `bound`. The bound must fit into @@ -199,37 +198,37 @@ fn main() { println!("Executing unsafe circuit..."); //Typical example, ok - assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(17), Fq::from(9), 10).is_ok()); // Typical example, err - assert!(verify_circuit_unsafe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + assert!(verify_circuit_unsafe::(Fq::from(17), Fq::from(20), 10).is_err()); // Edge case, err - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(4), 10).is_err()); // Edge case, ok - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(3), 10).is_ok()); // Minimum number of bits for the bound, ok - assert!(verify_circuit_unsafe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), Fq::from(3), 3).is_ok()); // Insufficient number of bits for the input, but this is not detected by the // unsafety of the circuit (compare with the last example below) // Note that -Fq::one() is corresponds to q - 1 > bound - assert!(verify_circuit_unsafe::(Fq::from(4u64), -Fq::one(), 3).is_ok()); + assert!(verify_circuit_unsafe::(Fq::from(4), -Fq::one(), 3).is_ok()); println!("Unsafe circuit OK"); println!("Executing safe circuit..."); // Typical example, ok - assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(9u64), 10).is_ok()); + assert!(verify_circuit_safe::(Fq::from(17), Fq::from(9), 10).is_ok()); // Typical example, err - assert!(verify_circuit_safe::(Fq::from(17u64), Fq::from(20u64), 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(17), Fq::from(20), 10).is_err()); // Edge case, err - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(4u64), 10).is_err()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(4), 10).is_err()); // Edge case, ok - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 10).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(3), 10).is_ok()); // Minimum number of bits for the bound, ok - assert!(verify_circuit_safe::(Fq::from(4u64), Fq::from(3u64), 3).is_ok()); + assert!(verify_circuit_safe::(Fq::from(4), Fq::from(3), 3).is_ok()); // Insufficient number of bits for the input, err (compare with the last example // above). // Note that -Fq::one() is corresponds to q - 1 > bound - assert!(verify_circuit_safe::(Fq::from(4u64), -Fq::one(), 3).is_err()); + assert!(verify_circuit_safe::(Fq::from(4), -Fq::one(), 3).is_err()); println!("Safe circuit OK"); } From cf5388f9ea6335fb326859ac032d612dc0807b96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Mar 2024 15:33:47 +0100 Subject: [PATCH 18/21] fixed clippy warning --- examples/less_than.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 9d5e3a8..9f4d3aa 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -20,7 +20,7 @@ fn num_to_bits_le_bounded>>(), None => vec![None; num_bits as usize], }; From 900e34c2e3ba00f36c6595373cb2cc24f233ac2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Mon, 18 Mar 2024 17:10:46 +0100 Subject: [PATCH 19/21] tweaked documentation --- examples/less_than.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/less_than.rs b/examples/less_than.rs index 9f4d3aa..a3bac59 100644 --- a/examples/less_than.rs +++ b/examples/less_than.rs @@ -60,8 +60,9 @@ fn get_msb_index(n: F) -> u8 { .0 as u8 } -// Range check: constrains input < `bound`. The bound must fit into -// `num_bits` bits (this is asserted in the circuit constructor). +// Constrains `input` < `bound`, where the LHS is a witness and the RHS is a +// constant. The bound must fit into `num_bits` bits (this is asserted in the +// circuit constructor). // Important: it must be checked elsewhere (in an overarching circuit) that the // input fits into `num_bits` bits - this is NOT constrained by this circuit // in order to avoid duplications (hence "unsafe"). Cf. LessThanCircuitSafe for @@ -115,8 +116,9 @@ impl Circuit for LessThanCircuitUnsafe { } } -// Range check: constrains input < `bound`. The bound must fit into -// `num_bits` bits (this is asserted in the circuit constructor). +// Constrains `input` < `bound`, where the LHS is a witness and the RHS is a +// constant. The bound must fit into `num_bits` bits (this is asserted in the +// circuit constructor). // Furthermore, the input must fit into `num_bits`, which is enforced at the // constraint level. #[derive(Clone, Debug)] From af47fa1e73d5e780ac8594d4b568cb1b31f99989 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Mon, 11 Nov 2024 15:06:08 +0100 Subject: [PATCH 20/21] removed unused --- src/bellpepper/shape_cs.rs | 9 ++++----- src/bellpepper/test_shape_cs.rs | 9 ++++----- src/spartan/math.rs | 7 ------- 3 files changed, 8 insertions(+), 17 deletions(-) diff --git a/src/bellpepper/shape_cs.rs b/src/bellpepper/shape_cs.rs index 5a50649..51646ff 100644 --- a/src/bellpepper/shape_cs.rs +++ b/src/bellpepper/shape_cs.rs @@ -15,8 +15,8 @@ struct OrderedVariable(Variable); #[derive(Debug)] enum NamedObject { - Constraint(usize), - Var(Variable), + Constraint, + Var, Namespace, } @@ -222,7 +222,7 @@ where { fn default() -> Self { let mut map = HashMap::new(); - map.insert("ONE".into(), NamedObject::Var(ShapeCS::::one())); + map.insert("ONE".into(), NamedObject::Var); ShapeCS { named_objects: map, current_namespace: vec![], @@ -272,8 +272,7 @@ where LC: FnOnce(LinearCombination) -> LinearCombination, { let path = compute_path(&self.current_namespace, &annotation().into()); - let index = self.constraints.len(); - self.set_named_obj(path.clone(), NamedObject::Constraint(index)); + self.set_named_obj(path.clone(), NamedObject::Constraint); let a = a(LinearCombination::zero()); let b = b(LinearCombination::zero()); diff --git a/src/bellpepper/test_shape_cs.rs b/src/bellpepper/test_shape_cs.rs index cf43a7a..988835f 100644 --- a/src/bellpepper/test_shape_cs.rs +++ b/src/bellpepper/test_shape_cs.rs @@ -16,8 +16,8 @@ struct OrderedVariable(Variable); #[derive(Debug)] enum NamedObject { - Constraint(usize), - Var(Variable), + Constraint, + Var, Namespace, } @@ -224,7 +224,7 @@ where { fn default() -> Self { let mut map = HashMap::new(); - map.insert("ONE".into(), NamedObject::Var(TestShapeCS::::one())); + map.insert("ONE".into(), NamedObject::Var); TestShapeCS { named_objects: map, current_namespace: vec![], @@ -274,8 +274,7 @@ where LC: FnOnce(LinearCombination) -> LinearCombination, { let path = compute_path(&self.current_namespace, &annotation().into()); - let index = self.constraints.len(); - self.set_named_obj(path.clone(), NamedObject::Constraint(index)); + self.set_named_obj(path.clone(), NamedObject::Constraint); let a = a(LinearCombination::zero()); let b = b(LinearCombination::zero()); diff --git a/src/spartan/math.rs b/src/spartan/math.rs index 691fec5..44c9f2c 100644 --- a/src/spartan/math.rs +++ b/src/spartan/math.rs @@ -1,16 +1,9 @@ pub trait Math { - fn pow2(self) -> usize; fn get_bits(self, num_bits: usize) -> Vec; fn log_2(self) -> usize; } impl Math for usize { - #[inline] - fn pow2(self) -> usize { - let base: usize = 2; - base.pow(self as u32) - } - /// Returns the `num_bits` from n in a canonical order fn get_bits(self, num_bits: usize) -> Vec { (0..num_bits) From 19c381f0823a5de9c101994720c11649a87c1325 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antonio=20Mej=C3=ADas=20Gil?= Date: Fri, 15 Nov 2024 21:41:29 +0100 Subject: [PATCH 21/21] fixed clippy warning --- src/provider/keccak.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/provider/keccak.rs b/src/provider/keccak.rs index 849ae30..2046072 100644 --- a/src/provider/keccak.rs +++ b/src/provider/keccak.rs @@ -87,7 +87,7 @@ impl TranscriptEngineTrait for Keccak256Transcript { fn absorb>(&mut self, label: &'static [u8], o: &T) { self.transcript.update(label); - self.transcript.update(&o.to_transcript_bytes()); + self.transcript.update(o.to_transcript_bytes()); } fn dom_sep(&mut self, bytes: &'static [u8]) {