From 5268c2084821955c5953c29c7e179b2052523b5d Mon Sep 17 00:00:00 2001 From: Matej Penciak <96667244+mpenciak@users.noreply.github.com> Date: Fri, 22 Mar 2024 15:38:40 -0400 Subject: [PATCH] CycleFold (#273) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * skeleton * (wip) scalar <-> base confusion * (wip) fix W_new def * (wip) fixed base <-> scalar confusion * (wip) new gadget scaffolding and allocated witnesses * (wip) fix prove_step * (wip) synthesize_non_base_case * (wip) synthesize * (wip) synthesize_base_case * (wip) fix absorbs * (wip) stuck * (wip) CommitmentKey macro * (wip) some gadgets filled * (wip) some more progress * (wip) Gadgets done, some cleanup * (wip) Scalar <-> Base confusion in verify * it builds! * make clippy happy * Delete `RecursiveSNARKTrait` and cleanup * refactor: Refactor data types and function signatures in Cyclefold module - Updated and harmonized data type usage in `cyclefold/gadgets.rs`, `cyclefold/circuit.rs`, and `cyclefold/nova_circuit.rs` - Replaced `AllocatedPoint` with `AllocatedEmulPoint`, `AllocatedRelaxedR1CSInstance` with `AllocatedEmulRelaxedR1CSInstance` to avoid confusion, and simplified required bounds, - Refactored `cyclefold/gadgets.rs` to remove use of needless bounds, - no `CurveCycleEquipped` bound was used anywhere in this commit * refactor: remove uneeded params in PublicParams, RecursiveSNARK * refactor: Remove option in CycleFoldInputs, remove a few needless types in tests * test: use expect_test on brittle test * chore: update expect tests * (wip) addressing comments * (wip) add recursive_snark test * (wip) add generic bounds for allocatedr1csinstances * make the cyclefold test more **fun** * fix cyclefold circuit IO * uncomment num_io cyclefold check * update constant * fix link * cleanup output * last couple circuit pieces * add comm_T to inputs and add cyclefold IO checks * fix ro absorb numbers * remove extra unneeded comm_T allocation * properly constrain `always_equal` in `mult_mod` and `red_mod` * some allocation fixes * eliminate clone * make RO absorb numbers make sense * fix cyclefold scalar alloc * chore: update Bn256Engine -> Bn256EngineKZG * chore: run clippy * update `expect_test`s * fix EmulatedCurveParam allocation * fix nifs RO absorb count * make `test_augmented_circuit_size` an `expect_test` * fix: typo * fix: `RecursiveSNARK::new` sets i to 0 * fix: Fix RO absorb count in verify * fix: `RecursiveSNARK::new` should set r_*_primary to default values * u <-> U in folding data Alloc * fix: add trivialization for cyclefold checks in base case * make prove_verify test more fun * fix: fix hashing order * fix: r_bools was always None * make prove_verify test longer * clippy * test_augmented_circuit_size should check synthesis works * chore: fix rebase * chore: bump msrv * chore: cleanup, documentation, and split cyclefold test * fix: Fix CycleFold circuit IO to only have arity 4 Also fix CycleFold folding soundness issue by absorbing running instance * chore: update cyclefold_circuit_size expecttest * fix: fix RO absorb counts and logic * chore: update cyclefold primary circuit size expecttest * chore: cleanup and docs * fix: fix rebase * chore: fix clippy lints * fix: constrain `AllocatedEmulPoint::default` * tidy: use `AllocatedNum::add` * chore: fix rebase errors in `src/gadgets` * fix: fix import * chore: update expecttests * tidy: add new constant * tidy: Cyclefold -> CycleFold --------- Co-authored-by: François Garillot --- Cargo.toml | 2 +- src/constants.rs | 3 + src/cyclefold/circuit.rs | 287 +++++++++++++ src/cyclefold/gadgets.rs | 695 ++++++++++++++++++++++++++++++++ src/cyclefold/mod.rs | 9 + src/cyclefold/nifs.rs | 156 +++++++ src/cyclefold/nova_circuit.rs | 567 ++++++++++++++++++++++++++ src/cyclefold/snark.rs | 563 ++++++++++++++++++++++++++ src/cyclefold/util.rs | 89 ++++ src/gadgets/mod.rs | 5 +- src/gadgets/nonnative/bignat.rs | 2 +- src/gadgets/nonnative/util.rs | 3 +- src/gadgets/r1cs.rs | 4 +- src/gadgets/utils.rs | 27 ++ src/lib.rs | 7 +- src/nifs.rs | 43 +- src/supernova/mod.rs | 4 +- src/supernova/snark.rs | 2 +- 18 files changed, 2441 insertions(+), 27 deletions(-) create mode 100644 src/cyclefold/circuit.rs create mode 100644 src/cyclefold/gadgets.rs create mode 100644 src/cyclefold/mod.rs create mode 100644 src/cyclefold/nifs.rs create mode 100644 src/cyclefold/nova_circuit.rs create mode 100644 src/cyclefold/snark.rs create mode 100644 src/cyclefold/util.rs diff --git a/Cargo.toml b/Cargo.toml index ef6bf8523..d86b2b4f5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ readme = "README.md" repository = "https://github.com/lurk-lab/arecibo" license-file = "LICENSE" keywords = ["zkSNARKs", "cryptography", "proofs"] -rust-version="1.71.0" +rust-version="1.74.1" [dependencies] bellpepper-core = { version = "0.4.0", default-features = false } diff --git a/src/constants.rs b/src/constants.rs index acda5628a..2504cb4e5 100644 --- a/src/constants.rs +++ b/src/constants.rs @@ -4,8 +4,11 @@ pub(crate) const NUM_CHALLENGE_BITS: usize = 128; pub(crate) const BN_LIMB_WIDTH: usize = 64; pub(crate) const BN_N_LIMBS: usize = 4; pub(crate) const NUM_FE_WITHOUT_IO_FOR_CRHF: usize = 9 + NIO_NOVA_FOLD * BN_N_LIMBS; +pub(crate) const NUM_FE_WITHOUT_IO_FOR_NOVA_FOLD: usize = 7; pub(crate) const NUM_FE_FOR_RO: usize = 9; pub(crate) const NIO_NOVA_FOLD: usize = 2; +pub(crate) const NUM_FE_IN_EMULATED_POINT: usize = 2 * BN_N_LIMBS + 1; +pub(crate) const NIO_CYCLE_FOLD: usize = 4; // 1 per point (3) + scalar /// Bit size of Nova field element hashes pub const NUM_HASH_BITS: usize = 250; diff --git a/src/cyclefold/circuit.rs b/src/cyclefold/circuit.rs new file mode 100644 index 000000000..46e3c4dbb --- /dev/null +++ b/src/cyclefold/circuit.rs @@ -0,0 +1,287 @@ +//! This module defines Cyclefold circuit + +use bellpepper_core::{ + boolean::{AllocatedBit, Boolean}, + ConstraintSystem, SynthesisError, +}; +use ff::Field; +use neptune::{circuit2::poseidon_hash_allocated, poseidon::PoseidonConstants}; + +use crate::{ + constants::NUM_CHALLENGE_BITS, + gadgets::{alloc_zero, le_bits_to_num, AllocatedPoint}, + traits::{commitment::CommitmentTrait, Engine}, + Commitment, +}; +use bellpepper::gadgets::boolean_utils::conditionally_select; + +/// A structure containing the CycleFold circuit inputs and implementing the synthesize function +pub struct CycleFoldCircuit { + commit_1: Option>, + commit_2: Option>, + scalar: Option<[bool; NUM_CHALLENGE_BITS]>, + poseidon_constants: PoseidonConstants, +} + +impl Default for CycleFoldCircuit { + fn default() -> Self { + let poseidon_constants = PoseidonConstants::new(); + Self { + commit_1: None, + commit_2: None, + scalar: None, + poseidon_constants, + } + } +} +impl CycleFoldCircuit { + /// Create a new CycleFold circuit with the given inputs + pub fn new( + commit_1: Option>, + commit_2: Option>, + scalar: Option<[bool; NUM_CHALLENGE_BITS]>, + ) -> Self { + let poseidon_constants = PoseidonConstants::new(); + Self { + commit_1, + commit_2, + scalar, + poseidon_constants, + } + } + + fn alloc_witness::Base>>( + &self, + mut cs: CS, + ) -> Result< + ( + AllocatedPoint, // commit_1 + AllocatedPoint, // commit_2 + Vec, // scalar + ), + SynthesisError, + > { + let commit_1 = AllocatedPoint::alloc( + cs.namespace(|| "allocate C_1"), + self.commit_1.map(|C_1| C_1.to_coordinates()), + )?; + commit_1.check_on_curve(cs.namespace(|| "commit_1 on curve"))?; + + let commit_2 = AllocatedPoint::alloc( + cs.namespace(|| "allocate C_2"), + self.commit_2.map(|C_2| C_2.to_coordinates()), + )?; + commit_2.check_on_curve(cs.namespace(|| "commit_2 on curve"))?; + + let scalar: Vec = self + .scalar + .unwrap_or([false; NUM_CHALLENGE_BITS]) + .into_iter() + .enumerate() + .map(|(idx, bit)| { + AllocatedBit::alloc(cs.namespace(|| format!("scalar bit {idx}")), Some(bit)) + }) + .collect::, _>>()?; + + Ok((commit_1, commit_2, scalar)) + } + + /// Synthesize the CycleFold circuit + pub fn synthesize::Base>>( + &self, + mut cs: CS, + ) -> Result<(), SynthesisError> { + let (C_1, C_2, r) = self.alloc_witness(cs.namespace(|| "allocate circuit witness"))?; + + // Calculate C_final + let r_C_2 = C_2.scalar_mul(cs.namespace(|| "r * C_2"), &r)?; + + let C_final = C_1.add(cs.namespace(|| "C_1 + r * C_2"), &r_C_2)?; + + self.inputize_point(&C_1, cs.namespace(|| "inputize C_1"))?; + self.inputize_point(&C_2, cs.namespace(|| "inputize C_2"))?; + self.inputize_point(&C_final, cs.namespace(|| "inputize C_final"))?; + + let scalar = le_bits_to_num(cs.namespace(|| "get scalar"), &r)?; + + scalar.inputize(cs.namespace(|| "scalar"))?; + + Ok(()) + } + + // Represent the point in the public IO as its 2-ary Poseidon hash + fn inputize_point( + &self, + point: &AllocatedPoint, + mut cs: CS, + ) -> Result<(), SynthesisError> + where + E: Engine, + CS: ConstraintSystem, + { + let (x, y, is_infinity) = point.get_coordinates(); + let preimage = vec![x.clone(), y.clone()]; + let val = poseidon_hash_allocated( + cs.namespace(|| "hash point"), + preimage, + &self.poseidon_constants, + )?; + + let zero = alloc_zero(cs.namespace(|| "zero")); + + let is_infinity_bit = AllocatedBit::alloc( + cs.namespace(|| "is_infinity"), + Some(is_infinity.get_value().unwrap_or(E::Base::ONE) == E::Base::ONE), + )?; + + cs.enforce( + || "infinity_bit matches", + |lc| lc, + |lc| lc, + |lc| lc + is_infinity_bit.get_variable() - is_infinity.get_variable(), + ); + + // Output 0 when it is the point at infinity + let output = conditionally_select( + cs.namespace(|| "select output"), + &zero, + &val, + &Boolean::from(is_infinity_bit), + )?; + + output.inputize(cs.namespace(|| "inputize hash"))?; + + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use expect_test::{expect, Expect}; + use ff::{Field, PrimeField, PrimeFieldBits}; + use neptune::Poseidon; + use rand_core::OsRng; + + use crate::{ + bellpepper::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, + }, + constants::NIO_CYCLE_FOLD, + gadgets::scalar_as_base, + provider::{Bn256EngineKZG, PallasEngine, Secp256k1Engine}, + traits::{commitment::CommitmentEngineTrait, snark::default_ck_hint, CurveCycleEquipped, Dual}, + }; + + use super::*; + + fn test_cyclefold_circuit_size_with(expected_constraints: &Expect, expected_vars: &Expect) + where + E1: CurveCycleEquipped, + { + // Instantiate the circuit with trivial inputs + let circuit: CycleFoldCircuit> = CycleFoldCircuit::default(); + + // Synthesize the R1CS shape + let mut cs: ShapeCS = ShapeCS::new(); + let _ = circuit.synthesize(cs.namespace(|| "synthesizing shape")); + + // Extract the number of constraints and variables + let num_constraints = cs.num_constraints(); + let num_variables = cs.num_aux(); + let num_io = cs.num_inputs(); + + // Check the number of constraints and variables match the expected values + expected_constraints.assert_eq(&num_constraints.to_string()); + expected_vars.assert_eq(&num_variables.to_string()); + assert_eq!(num_io, NIO_CYCLE_FOLD + 1); // includes 1 + } + + #[test] + fn test_cyclefold_circuit_size() { + test_cyclefold_circuit_size_with::(&expect!("2090"), &expect!("2081")); + test_cyclefold_circuit_size_with::(&expect!("2090"), &expect!("2081")); + test_cyclefold_circuit_size_with::(&expect!("2090"), &expect!("2081")); + } + + fn test_cyclefold_circuit_sat_with() { + let rng = OsRng; + + let ck = < as Engine>::CE as CommitmentEngineTrait>>::setup(b"test", 5); + + // Generate random vectors to commit to + let v1 = (0..5) + .map(|_| < as Engine>::Scalar as Field>::random(rng)) + .collect::>(); + let v2 = (0..5) + .map(|_| < as Engine>::Scalar as Field>::random(rng)) + .collect::>(); + + // Calculate the random commitments + let C_1 = < as Engine>::CE as CommitmentEngineTrait>>::commit(&ck, &v1); + let C_2 = < as Engine>::CE as CommitmentEngineTrait>>::commit(&ck, &v2); + + // Generate a random scalar + let val: u128 = rand::random(); + let r = < as Engine>::Scalar as PrimeField>::from_u128(val); + let r_bits = r + .to_le_bits() + .into_iter() + .take(128) + .collect::>() + .try_into() + .unwrap(); + + let circuit: CycleFoldCircuit> = + CycleFoldCircuit::new(Some(C_1), Some(C_2), Some(r_bits)); + + // Calculate the result out of circuit + let native_result = C_1 + C_2 * r; + + // Generate the R1CS shape and commitment key + let mut cs: ShapeCS = ShapeCS::new(); + let _ = circuit.synthesize(cs.namespace(|| "synthesizing shape")); + let (shape, ck) = cs.r1cs_shape_and_key(&*default_ck_hint()); + + // Synthesize the R1CS circuit on the random inputs + let mut cs = SatisfyingAssignment::::new(); + circuit + .synthesize(cs.namespace(|| "synthesizing witness")) + .unwrap(); + + let (instance, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap(); + let X = &instance.X; + + // Helper functio to calculate the hash + let compute_hash = |P: Commitment>| -> E::Scalar { + let (x, y, is_infinity) = P.to_coordinates(); + if is_infinity { + return E::Scalar::ZERO; + } + + let mut hasher = Poseidon::new_with_preimage(&[x, y], &circuit.poseidon_constants); + + hasher.hash() + }; + + // Check the circuit calculates the right thing + let hash_1 = compute_hash(C_1); + assert_eq!(hash_1, X[0]); + let hash_2 = compute_hash(C_2); + assert_eq!(hash_2, X[1]); + let hash_res = compute_hash(native_result); + assert_eq!(hash_res, X[2]); + assert_eq!(r, scalar_as_base::(X[3])); + + // Check the R1CS equation is satisfied + shape.is_sat(&ck, &instance, &witness).unwrap(); + } + + #[test] + fn test_cyclefold_circuit_sat() { + test_cyclefold_circuit_sat_with::(); + test_cyclefold_circuit_sat_with::(); + test_cyclefold_circuit_sat_with::(); + } +} diff --git a/src/cyclefold/gadgets.rs b/src/cyclefold/gadgets.rs new file mode 100644 index 000000000..fe20163ce --- /dev/null +++ b/src/cyclefold/gadgets.rs @@ -0,0 +1,695 @@ +//! This module defines many of the gadgets needed in the primary folding circuit + +use super::util::FoldingData; + +use crate::{ + constants::{BN_N_LIMBS, NIO_CYCLE_FOLD, NUM_CHALLENGE_BITS}, + gadgets::{ + alloc_bignat_constant, f_to_nat, le_bits_to_num, AllocatedPoint, AllocatedRelaxedR1CSInstance, + BigNat, Num, + }, + r1cs::R1CSInstance, + traits::{commitment::CommitmentTrait, Engine, Group, ROCircuitTrait, ROConstantsCircuit}, +}; + +use bellpepper::gadgets::Assignment; +use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError}; +use ff::Field; +use itertools::Itertools; + +// An allocated version of the R1CS instance obtained from a single cyclefold invocation +pub struct AllocatedCycleFoldInstance { + W: AllocatedPoint, + X: [BigNat; NIO_CYCLE_FOLD], +} + +impl AllocatedCycleFoldInstance { + pub fn alloc>( + mut cs: CS, + inst: Option<&R1CSInstance>, + limb_width: usize, + n_limbs: usize, + ) -> Result { + let W = AllocatedPoint::alloc( + cs.namespace(|| "allocate W"), + inst.map(|u| u.comm_W.to_coordinates()), + )?; + W.check_on_curve(cs.namespace(|| "check W on curve"))?; + + if let Some(inst) = inst { + if inst.X.len() != NIO_CYCLE_FOLD { + return Err(SynthesisError::IncompatibleLengthVector(String::from( + "R1CS instance has wrong arity", + ))); + } + } + + let X: [BigNat; NIO_CYCLE_FOLD] = (0..NIO_CYCLE_FOLD) + .map(|idx| { + BigNat::alloc_from_nat( + cs.namespace(|| format!("allocating IO {idx}")), + || Ok(f_to_nat(inst.map_or(&E::Scalar::ZERO, |inst| &inst.X[idx]))), + limb_width, + n_limbs, + ) + }) + .collect::, _>>()? + .try_into() + .map_err(|err: Vec<_>| { + SynthesisError::IncompatibleLengthVector(format!("{} != {NIO_CYCLE_FOLD}", err.len())) + })?; + + Ok(Self { W, X }) + } + + pub fn absorb_in_ro( + &self, + mut cs: CS, + ro: &mut impl ROCircuitTrait, + ) -> Result<(), SynthesisError> + where + CS: ConstraintSystem, + { + ro.absorb(&self.W.x); + ro.absorb(&self.W.y); + ro.absorb(&self.W.is_infinity); + self + .X + .iter() + .enumerate() + .try_for_each(|(io_idx, x)| -> Result<(), SynthesisError> { + x.as_limbs().iter().enumerate().try_for_each( + |(limb_idx, limb)| -> Result<(), SynthesisError> { + ro.absorb(&limb.as_allocated_num( + cs.namespace(|| format!("convert limb {limb_idx} of X[{io_idx}] to num")), + )?); + Ok(()) + }, + ) + })?; + + Ok(()) + } +} + +/// An circuit allocated version of the `FoldingData` coming from a CycleFold invocation. +pub struct AllocatedCycleFoldData { + pub U: AllocatedRelaxedR1CSInstance, + pub u: AllocatedCycleFoldInstance, + pub T: AllocatedPoint, +} + +impl AllocatedCycleFoldData { + pub fn alloc>( + mut cs: CS, + inst: Option<&FoldingData>, + limb_width: usize, + n_limbs: usize, + ) -> Result { + let U = AllocatedRelaxedR1CSInstance::alloc( + cs.namespace(|| "U"), + inst.map(|x| &x.U), + limb_width, + n_limbs, + )?; + + let u = AllocatedCycleFoldInstance::alloc( + cs.namespace(|| "u"), + inst.map(|x| &x.u), + limb_width, + n_limbs, + )?; + + let T = AllocatedPoint::alloc(cs.namespace(|| "T"), inst.map(|x| x.T.to_coordinates()))?; + T.check_on_curve(cs.namespace(|| "T on curve"))?; + + Ok(Self { U, u, T }) + } + + /// The NIFS verifier which folds the CycleFold instance into a running relaxed R1CS instance. + pub fn apply_fold( + &self, + mut cs: CS, + params: &AllocatedNum, + ro_consts: ROConstantsCircuit, + limb_width: usize, + n_limbs: usize, + ) -> Result, SynthesisError> + where + CS: ConstraintSystem, + { + // Compute r: + let mut ro = E::ROCircuit::new( + ro_consts, + 1 + (3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS) + (3 + NIO_CYCLE_FOLD * BN_N_LIMBS) + 3, // digest + (U) + (u) + T + ); + ro.absorb(params); + + self.U.absorb_in_ro( + cs.namespace(|| "absorb cyclefold running instance"), + &mut ro, + )?; + // running instance `U` does not need to absorbed since u.X[0] = Hash(params, U, i, z0, zi) + self + .u + .absorb_in_ro(cs.namespace(|| "absorb cyclefold instance"), &mut ro)?; + + ro.absorb(&self.T.x); + ro.absorb(&self.T.y); + ro.absorb(&self.T.is_infinity); + let r_bits = ro.squeeze(cs.namespace(|| "r bits"), NUM_CHALLENGE_BITS)?; + let r = le_bits_to_num(cs.namespace(|| "r"), &r_bits)?; + + // W_fold = self.W + r * u.W + let rW = self.u.W.scalar_mul(cs.namespace(|| "r * u.W"), &r_bits)?; + let W_fold = self.U.W.add(cs.namespace(|| "self.W + r * u.W"), &rW)?; + + // E_fold = self.E + r * T + let rT = self.T.scalar_mul(cs.namespace(|| "r * T"), &r_bits)?; + let E_fold = self.U.E.add(cs.namespace(|| "self.E + r * T"), &rT)?; + + // u_fold = u_r + r + let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || { + Ok(*self.U.u.get_value().get()? + r.get_value().get()?) + })?; + cs.enforce( + || "Check u_fold", + |lc| lc, + |lc| lc, + |lc| lc + u_fold.get_variable() - self.U.u.get_variable() - r.get_variable(), + ); + + // Fold the IO: + // Analyze r into limbs + let r_bn = BigNat::from_num( + cs.namespace(|| "allocate r_bn"), + &Num::from(r), + limb_width, + n_limbs, + )?; + + // Allocate the order of the non-native field as a constant + let m_bn = alloc_bignat_constant( + cs.namespace(|| "alloc m"), + &E::GE::group_params().2, + limb_width, + n_limbs, + )?; + + let mut X_fold = vec![]; + + // Calculate the + for (idx, (X, x)) in self.U.X.iter().zip_eq(self.u.X.iter()).enumerate() { + let (_, r) = x.mult_mod(cs.namespace(|| format!("r*u.X[{idx}]")), &r_bn, &m_bn)?; + let r_new = X.add(&r)?; + let X_i_fold = r_new.red_mod(cs.namespace(|| format!("reduce folded X[{idx}]")), &m_bn)?; + X_fold.push(X_i_fold); + } + + let X_fold = X_fold.try_into().map_err(|err: Vec<_>| { + SynthesisError::IncompatibleLengthVector(format!("{} != {NIO_CYCLE_FOLD}", err.len())) + })?; + + Ok(AllocatedRelaxedR1CSInstance { + W: W_fold, + E: E_fold, + u: u_fold, + X: X_fold, + }) + } +} + +pub mod emulated { + use bellpepper::gadgets::{boolean_utils::conditionally_select, Assignment}; + use bellpepper_core::{ + boolean::{AllocatedBit, Boolean}, + num::AllocatedNum, + ConstraintSystem, SynthesisError, + }; + + use crate::{ + constants::{NUM_CHALLENGE_BITS, NUM_FE_IN_EMULATED_POINT}, + gadgets::{ + alloc_bignat_constant, alloc_zero, conditionally_select_allocated_bit, + conditionally_select_bignat, f_to_nat, le_bits_to_num, BigNat, + }, + traits::{commitment::CommitmentTrait, Engine, Group, ROCircuitTrait, ROConstantsCircuit}, + RelaxedR1CSInstance, + }; + + use super::FoldingData; + + use ff::Field; + + /// An allocated version of a curve point from the non-native curve + #[derive(Clone)] + pub struct AllocatedEmulPoint + where + G: Group, + { + pub x: BigNat, + pub y: BigNat, + pub is_infinity: AllocatedBit, + } + + impl AllocatedEmulPoint + where + G: Group, + { + pub fn alloc( + mut cs: CS, + coords: Option<(G::Scalar, G::Scalar, bool)>, + limb_width: usize, + n_limbs: usize, + ) -> Result + where + CS: ConstraintSystem<::Base>, + { + let x = BigNat::alloc_from_nat( + cs.namespace(|| "x"), + || { + Ok(f_to_nat( + &coords.map_or(::ZERO, |val| val.0), + )) + }, + limb_width, + n_limbs, + )?; + + let y = BigNat::alloc_from_nat( + cs.namespace(|| "y"), + || { + Ok(f_to_nat( + &coords.map_or(::ZERO, |val| val.1), + )) + }, + limb_width, + n_limbs, + )?; + + let is_infinity = AllocatedBit::alloc( + cs.namespace(|| "alloc is_infinity"), + coords.map_or(Some(true), |(_, _, is_infinity)| Some(is_infinity)), + )?; + + Ok(Self { x, y, is_infinity }) + } + + pub fn absorb_in_ro( + &self, + mut cs: CS, + ro: &mut impl ROCircuitTrait, + ) -> Result<(), SynthesisError> + where + CS: ConstraintSystem, + { + let x_bn = self + .x + .as_limbs() + .iter() + .enumerate() + .map(|(i, limb)| { + limb.as_allocated_num(cs.namespace(|| format!("convert limb {i} of x to num"))) + }) + .collect::>, _>>()?; + + for limb in x_bn { + ro.absorb(&limb) + } + + let y_bn = self + .y + .as_limbs() + .iter() + .enumerate() + .map(|(i, limb)| { + limb.as_allocated_num(cs.namespace(|| format!("convert limb {i} of y to num"))) + }) + .collect::>, _>>()?; + + for limb in y_bn { + ro.absorb(&limb) + } + + let is_infinity_num: AllocatedNum = + AllocatedNum::alloc(cs.namespace(|| "is_infinity"), || { + self + .is_infinity + .get_value() + .map_or(Err(SynthesisError::AssignmentMissing), |bit| { + if bit { + Ok(G::Base::ONE) + } else { + Ok(G::Base::ZERO) + } + }) + })?; + + cs.enforce( + || "constrain num equals bit", + |lc| lc, + |lc| lc, + |lc| lc + is_infinity_num.get_variable() - self.is_infinity.get_variable(), + ); + + ro.absorb(&is_infinity_num); + + Ok(()) + } + + fn conditionally_select>( + &self, + mut cs: CS, + other: &Self, + condition: &Boolean, + ) -> Result { + let x = conditionally_select_bignat( + cs.namespace(|| "x = cond ? self.x : other.x"), + &self.x, + &other.x, + condition, + )?; + + let y = conditionally_select_bignat( + cs.namespace(|| "y = cond ? self.y : other.y"), + &self.y, + &other.y, + condition, + )?; + + let is_infinity = conditionally_select_allocated_bit( + cs.namespace(|| "is_infinity = cond ? self.is_infinity : other.is_infinity"), + &self.is_infinity, + &other.is_infinity, + condition, + )?; + + Ok(Self { x, y, is_infinity }) + } + + pub fn default>( + mut cs: CS, + limb_width: usize, + n_limbs: usize, + ) -> Result { + let x = alloc_bignat_constant( + cs.namespace(|| "allocate x_default = 0"), + &f_to_nat(&G::Base::ZERO), + limb_width, + n_limbs, + )?; + let y = alloc_bignat_constant( + cs.namespace(|| "allocate y_default = 0"), + &f_to_nat(&G::Base::ZERO), + limb_width, + n_limbs, + )?; + + let is_infinity = AllocatedBit::alloc(cs.namespace(|| "allocate is_infinity"), Some(true))?; + cs.enforce( + || "is_infinity = 1", + |lc| lc, + |lc| lc, + |lc| lc + CS::one() - is_infinity.get_variable(), + ); + + Ok(Self { x, y, is_infinity }) + } + } + + /// A non-native circuit version of a `RelaxedR1CSInstance`. This is used for the in-circuit + /// representation of the primary running instance + pub struct AllocatedEmulRelaxedR1CSInstance { + pub comm_W: AllocatedEmulPoint, + pub comm_E: AllocatedEmulPoint, + u: AllocatedNum, + x0: AllocatedNum, + x1: AllocatedNum, + } + + impl AllocatedEmulRelaxedR1CSInstance + where + E: Engine, + { + pub fn alloc>( + mut cs: CS, + inst: Option<&RelaxedR1CSInstance>, + limb_width: usize, + n_limbs: usize, + ) -> Result + where + CS: ConstraintSystem<::Base>, + { + let comm_W = AllocatedEmulPoint::alloc( + cs.namespace(|| "allocate comm_W"), + inst.map(|x| x.comm_W.to_coordinates()), + limb_width, + n_limbs, + )?; + + let comm_E = AllocatedEmulPoint::alloc( + cs.namespace(|| "allocate comm_E"), + inst.map(|x| x.comm_E.to_coordinates()), + limb_width, + n_limbs, + )?; + + let u = AllocatedNum::alloc(cs.namespace(|| "allocate u"), || { + inst.map_or(Ok(E::Base::ZERO), |inst| Ok(inst.u)) + })?; + + let x0 = AllocatedNum::alloc(cs.namespace(|| "allocate x0"), || { + inst.map_or(Ok(E::Base::ZERO), |inst| Ok(inst.X[0])) + })?; + + let x1 = AllocatedNum::alloc(cs.namespace(|| "allocate x1"), || { + inst.map_or(Ok(E::Base::ZERO), |inst| Ok(inst.X[1])) + })?; + + Ok(Self { + comm_W, + comm_E, + u, + x0, + x1, + }) + } + + /// Performs a folding of a primary R1CS instance (`u_W`, `u_x0`, `u_x1`) into a running + /// `AllocatedEmulRelaxedR1CSInstance` + /// As the curve operations are performed in the CycleFold circuit and provided to the primary + /// circuit as non-deterministic advice, this folding simply sets those values as the new witness + /// and error vector commitments. + pub fn fold_with_r1cs::Base>>( + &self, + mut cs: CS, + pp_digest: &AllocatedNum, + W_new: AllocatedEmulPoint, + E_new: AllocatedEmulPoint, + u_W: &AllocatedEmulPoint, + u_x0: &AllocatedNum, + u_x1: &AllocatedNum, + comm_T: &AllocatedEmulPoint, + ro_consts: ROConstantsCircuit, + ) -> Result { + let mut ro = E::ROCircuit::new( + ro_consts, + 1 + NUM_FE_IN_EMULATED_POINT + 2 + NUM_FE_IN_EMULATED_POINT, // pp_digest + u.W + u.x + comm_T + ); + ro.absorb(pp_digest); + + // Absorb u + // Absorb the witness + u_W.absorb_in_ro(cs.namespace(|| "absorb u_W"), &mut ro)?; + // Absorb public IO + ro.absorb(u_x0); + ro.absorb(u_x1); + + // Absorb comm_T + comm_T.absorb_in_ro(cs.namespace(|| "absorb comm_T"), &mut ro)?; + + let r_bits = ro.squeeze(cs.namespace(|| "r bits"), NUM_CHALLENGE_BITS)?; + let r = le_bits_to_num(cs.namespace(|| "r"), &r_bits)?; + + let u_fold = self.u.add(cs.namespace(|| "u_fold = u + r"), &r)?; + let x0_fold = AllocatedNum::alloc(cs.namespace(|| "x0"), || { + Ok(*self.x0.get_value().get()? + *r.get_value().get()? * *u_x0.get_value().get()?) + })?; + cs.enforce( + || "x0_fold = x0 + r * u_x0", + |lc| lc + r.get_variable(), + |lc| lc + u_x0.get_variable(), + |lc| lc + x0_fold.get_variable() - self.x0.get_variable(), + ); + + let x1_fold = AllocatedNum::alloc(cs.namespace(|| "x1"), || { + Ok(*self.x1.get_value().get()? + *r.get_value().get()? * *u_x1.get_value().get()?) + })?; + cs.enforce( + || "x1_fold = x1 + r * u_x1", + |lc| lc + r.get_variable(), + |lc| lc + u_x1.get_variable(), + |lc| lc + x1_fold.get_variable() - self.x1.get_variable(), + ); + + Ok(Self { + comm_W: W_new, + comm_E: E_new, + u: u_fold, + x0: x0_fold, + x1: x1_fold, + }) + } + + pub fn absorb_in_ro( + &self, + mut cs: CS, + ro: &mut impl ROCircuitTrait, + ) -> Result<(), SynthesisError> + where + CS: ConstraintSystem<::Base>, + { + self + .comm_W + .absorb_in_ro(cs.namespace(|| "absorb comm_W"), ro)?; + self + .comm_E + .absorb_in_ro(cs.namespace(|| "absorb comm_E"), ro)?; + + ro.absorb(&self.u); + ro.absorb(&self.x0); + ro.absorb(&self.x1); + + Ok(()) + } + + pub fn conditionally_select::Base>>( + &self, + mut cs: CS, + other: &Self, + condition: &Boolean, + ) -> Result { + let comm_W = self.comm_W.conditionally_select( + cs.namespace(|| "comm_W = cond ? self.comm_W : other.comm_W"), + &other.comm_W, + condition, + )?; + + let comm_E = self.comm_E.conditionally_select( + cs.namespace(|| "comm_E = cond? self.comm_E : other.comm_E"), + &other.comm_E, + condition, + )?; + + let u = conditionally_select( + cs.namespace(|| "u = cond ? self.u : other.u"), + &self.u, + &other.u, + condition, + )?; + + let x0 = conditionally_select( + cs.namespace(|| "x0 = cond ? self.x0 : other.x0"), + &self.x0, + &other.x0, + condition, + )?; + + let x1 = conditionally_select( + cs.namespace(|| "x1 = cond ? self.x1 : other.x1"), + &self.x1, + &other.x1, + condition, + )?; + + Ok(Self { + comm_W, + comm_E, + u, + x0, + x1, + }) + } + + pub fn default::Base>>( + mut cs: CS, + limb_width: usize, + n_limbs: usize, + ) -> Result { + let comm_W = + AllocatedEmulPoint::default(cs.namespace(|| "default comm_W"), limb_width, n_limbs)?; + let comm_E = comm_W.clone(); + + let u = alloc_zero(cs.namespace(|| "u = 0")); + + let x0 = u.clone(); + let x1 = u.clone(); + + Ok(Self { + comm_W, + comm_E, + u, + x0, + x1, + }) + } + } + + /// The in-circuit representation of the primary folding data. + pub struct AllocatedFoldingData { + pub U: AllocatedEmulRelaxedR1CSInstance, + pub u_W: AllocatedEmulPoint, + pub u_x0: AllocatedNum, + pub u_x1: AllocatedNum, + pub T: AllocatedEmulPoint, + } + + impl AllocatedFoldingData { + pub fn alloc>( + mut cs: CS, + inst: Option<&FoldingData>, + limb_width: usize, + n_limbs: usize, + ) -> Result + where + CS: ConstraintSystem<::Base>, + { + let U = AllocatedEmulRelaxedR1CSInstance::alloc( + cs.namespace(|| "allocate U"), + inst.map(|x| &x.U), + limb_width, + n_limbs, + )?; + + let u_W = AllocatedEmulPoint::alloc( + cs.namespace(|| "allocate u_W"), + inst.map(|x| x.u.comm_W.to_coordinates()), + limb_width, + n_limbs, + )?; + + let u_x0 = AllocatedNum::alloc(cs.namespace(|| "allocate u_x0"), || { + inst.map_or(Ok(E::Base::ZERO), |inst| Ok(inst.u.X[0])) + })?; + + let u_x1 = AllocatedNum::alloc(cs.namespace(|| "allocate u_x1"), || { + inst.map_or(Ok(E::Base::ZERO), |inst| Ok(inst.u.X[1])) + })?; + + let T = AllocatedEmulPoint::alloc( + cs.namespace(|| "allocate T"), + inst.map(|x| x.T.to_coordinates()), + limb_width, + n_limbs, + )?; + + Ok(Self { + U, + u_W, + u_x0, + u_x1, + T, + }) + } + } +} diff --git a/src/cyclefold/mod.rs b/src/cyclefold/mod.rs new file mode 100644 index 000000000..ae5f97bab --- /dev/null +++ b/src/cyclefold/mod.rs @@ -0,0 +1,9 @@ +//! This module defines CycleFold folding scheme and its related functions. + +mod circuit; +mod gadgets; +mod nova_circuit; +mod util; + +pub mod nifs; +pub mod snark; diff --git a/src/cyclefold/nifs.rs b/src/cyclefold/nifs.rs new file mode 100644 index 000000000..1fd66a9f8 --- /dev/null +++ b/src/cyclefold/nifs.rs @@ -0,0 +1,156 @@ +//! This module defines the needed wrong-field NIFS prover + +use std::marker::PhantomData; + +use crate::{ + constants::{NIO_CYCLE_FOLD, NUM_CHALLENGE_BITS, NUM_FE_IN_EMULATED_POINT}, + errors::NovaError, + gadgets::scalar_as_base, + r1cs::{R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness}, + traits::{commitment::CommitmentTrait, AbsorbInROTrait, Engine, ROConstants, ROTrait}, + CommitmentKey, CompressedCommitment, +}; + +use super::util::{absorb_cyclefold_r1cs, absorb_primary_commitment, absorb_primary_r1cs}; + +/// A SNARK that holds the proof of a step of an incremental computation of the primary circuit +/// in the CycleFold folding scheme. +/// The difference of this folding scheme from the Nova NIFS in `src/nifs.rs` is that this +#[derive(Debug)] +pub struct PrimaryNIFS +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + pub(crate) comm_T: CompressedCommitment, + _p: PhantomData, +} + +impl PrimaryNIFS +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + /// Takes a relaxed R1CS instance-witness pair (U1, W1) and an R1CS instance-witness pair (U2, W2) + /// and folds them into a new relaxed R1CS instance-witness pair (U, W) and a commitment to the + /// cross term T. It also provides the challenge r used to fold the instances. + pub fn prove( + ck: &CommitmentKey, + ro_consts: &ROConstants, + pp_digest: &E1::Scalar, + S: &R1CSShape, + U1: &RelaxedR1CSInstance, + W1: &RelaxedR1CSWitness, + U2: &R1CSInstance, + W2: &R1CSWitness, + ) -> Result< + ( + Self, + (RelaxedR1CSInstance, RelaxedR1CSWitness), + E1::Scalar, + ), + NovaError, + > { + let arity = U1.X.len(); + + if arity != U2.X.len() { + return Err(NovaError::InvalidInputLength); + } + + let mut ro = E2::RO::new( + ro_consts.clone(), + 1 + NUM_FE_IN_EMULATED_POINT + arity + NUM_FE_IN_EMULATED_POINT, // pp_digest + u.W + u.X + T + ); + + ro.absorb(*pp_digest); + + absorb_primary_r1cs::(U2, &mut ro); + + let (T, comm_T) = S.commit_T(ck, U1, W1, U2, W2)?; + + absorb_primary_commitment::(&comm_T, &mut ro); + + let r = scalar_as_base::(ro.squeeze(NUM_CHALLENGE_BITS)); + + let U = U1.fold(U2, &comm_T, &r); + + let W = W1.fold(W2, &T, &r)?; + + Ok(( + Self { + comm_T: comm_T.compress(), + _p: PhantomData, + }, + (U, W), + r, + )) + } +} + +/// A SNARK that holds the proof of a step of an incremental computation of the CycleFold circuit +/// The difference of this folding scheme from the Nova NIFS in `src/nifs.rs` is that this folding +/// prover and verifier must fold in the `RelaxedR1CSInstance` accumulator because the optimization +/// in the +#[derive(Debug)] +pub struct CycleFoldNIFS { + pub(crate) comm_T: CompressedCommitment, +} + +impl CycleFoldNIFS { + /// Folds an R1CS instance/witness pair (U2, W2) into a relaxed R1CS instance/witness (U1, W1) + /// returning the new folded accumulator and a commitment to the cross-term. + pub fn prove( + ck: &CommitmentKey, + ro_consts: &ROConstants, + pp_digest: &E::Scalar, + S: &R1CSShape, + U1: &RelaxedR1CSInstance, + W1: &RelaxedR1CSWitness, + U2: &R1CSInstance, + W2: &R1CSWitness, + ) -> Result<(Self, (RelaxedR1CSInstance, RelaxedR1CSWitness)), NovaError> { + // Check `U1` and `U2` have the same arity + if U2.X.len() != NIO_CYCLE_FOLD || U1.X.len() != NIO_CYCLE_FOLD { + return Err(NovaError::InvalidInputLength); + } + + // initialize a new RO + let mut ro = E::RO::new( + ro_consts.clone(), + 46, // 1 + (3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS) + (3 + NIO_CYCLE_FOLD * BN_N_LIMBS) + 3, // digest + (U) + (u) + T + ); + + // append the digest of pp to the transcript + ro.absorb(scalar_as_base::(*pp_digest)); + + // append U1 to the transcript. + // NOTE: this must be here because the IO for `U2` does not have the data of the hash of `U1` + U1.absorb_in_ro(&mut ro); + + // append U2 to transcript + absorb_cyclefold_r1cs(U2, &mut ro); + + // compute a commitment to the cross-term + let (T, comm_T) = S.commit_T(ck, U1, W1, U2, W2)?; + + // append `comm_T` to the transcript and obtain a challenge + comm_T.absorb_in_ro(&mut ro); + + // compute a challenge from the RO + let r = ro.squeeze(NUM_CHALLENGE_BITS); + + // fold the instance using `r` and `comm_T` + let U = U1.fold(U2, &comm_T, &r); + + // fold the witness using `r` and `T` + let W = W1.fold(W2, &T, &r)?; + + // return the folded instance and witness + Ok(( + Self { + comm_T: comm_T.compress(), + }, + (U, W), + )) + } +} diff --git a/src/cyclefold/nova_circuit.rs b/src/cyclefold/nova_circuit.rs new file mode 100644 index 000000000..9ffd259be --- /dev/null +++ b/src/cyclefold/nova_circuit.rs @@ -0,0 +1,567 @@ +//! This module defines the Nova augmented circuit used for Cyclefold + +use crate::{ + constants::{BN_N_LIMBS, NIO_CYCLE_FOLD, NUM_FE_IN_EMULATED_POINT, NUM_HASH_BITS}, + gadgets::{ + alloc_num_equals, alloc_scalar_as_base, alloc_zero, le_bits_to_num, + AllocatedRelaxedR1CSInstance, + }, + traits::{ + circuit::StepCircuit, commitment::CommitmentTrait, Engine, ROCircuitTrait, ROConstantsCircuit, + }, + Commitment, +}; + +use abomonation_derive::Abomonation; +use bellpepper::gadgets::{ + boolean::Boolean, boolean_utils::conditionally_select_slice, num::AllocatedNum, Assignment, +}; +use bellpepper_core::{boolean::AllocatedBit, ConstraintSystem, SynthesisError}; +use ff::Field; +use serde::{Deserialize, Serialize}; + +use super::{ + gadgets::{emulated, AllocatedCycleFoldData}, + util::FoldingData, +}; + +#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Abomonation)] +pub struct AugmentedCircuitParams { + limb_width: usize, + n_limbs: usize, +} + +impl AugmentedCircuitParams { + pub const fn new(limb_width: usize, n_limbs: usize) -> Self { + Self { + limb_width, + n_limbs, + } + } +} + +#[derive(Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct AugmentedCircuitInputs +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + pp_digest: E1::Scalar, + i: E1::Base, + z0: Vec, + + zi: Option>, + data_p: Option>, + + data_c_1: Option>, + data_c_2: Option>, + + E_new: Option>, + W_new: Option>, +} + +impl AugmentedCircuitInputs +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + pub fn new( + pp_digest: E1::Scalar, + i: E1::Base, + z0: Vec, + zi: Option>, + data_p: Option>, + data_c_1: Option>, + data_c_2: Option>, + E_new: Option>, + W_new: Option>, + ) -> Self { + Self { + pp_digest, + i, + z0, + zi, + data_p, + data_c_1, + data_c_2, + E_new, + W_new, + } + } +} +pub struct AugmentedCircuit<'a, E1, E2, SC> +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, + SC: StepCircuit, +{ + params: &'a AugmentedCircuitParams, + ro_consts: ROConstantsCircuit, + inputs: Option>, + step_circuit: &'a SC, +} + +impl<'a, E1, E2, SC> AugmentedCircuit<'a, E1, E2, SC> +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, + SC: StepCircuit, +{ + pub const fn new( + params: &'a AugmentedCircuitParams, + ro_consts: ROConstantsCircuit, + inputs: Option>, + step_circuit: &'a SC, + ) -> Self { + Self { + params, + ro_consts, + inputs, + step_circuit, + } + } + + fn alloc_witness::Base>>( + &self, + mut cs: CS, + arity: usize, + ) -> Result< + ( + AllocatedNum, // pp_digest + AllocatedNum, // i + Vec>, // z0 + Vec>, // zi + emulated::AllocatedFoldingData, //data_p + AllocatedCycleFoldData, // data_c_1 + AllocatedCycleFoldData, // data_c_2 + emulated::AllocatedEmulPoint, // E_new + emulated::AllocatedEmulPoint, // W_new + ), + SynthesisError, + > { + let pp_digest = alloc_scalar_as_base::( + cs.namespace(|| "params"), + self.inputs.as_ref().map(|inputs| inputs.pp_digest), + )?; + + let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?; + + let z_0 = (0..arity) + .map(|i| { + AllocatedNum::alloc(cs.namespace(|| format!("z0_{i}")), || { + Ok(self.inputs.get()?.z0[i]) + }) + }) + .collect::>, _>>()?; + + // Allocate zi. If inputs.zi is not provided (base case) allocate default value 0 + let zero = vec![E1::Base::ZERO; arity]; + let z_i = (0..arity) + .map(|i| { + AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || { + Ok(self.inputs.get()?.zi.as_ref().unwrap_or(&zero)[i]) + }) + }) + .collect::>, _>>()?; + + let data_p = emulated::AllocatedFoldingData::alloc( + cs.namespace(|| "data_p"), + self + .inputs + .as_ref() + .and_then(|inputs| inputs.data_p.as_ref()), + self.params.limb_width, + self.params.n_limbs, + )?; + + let data_c_1 = AllocatedCycleFoldData::alloc( + cs.namespace(|| "data_c_1"), + self + .inputs + .as_ref() + .and_then(|inputs| inputs.data_c_1.as_ref()), + self.params.limb_width, + self.params.n_limbs, + )?; + + let data_c_2 = AllocatedCycleFoldData::alloc( + cs.namespace(|| "data_c_2"), + self + .inputs + .as_ref() + .and_then(|inputs| inputs.data_c_2.as_ref()), + self.params.limb_width, + self.params.n_limbs, + )?; + + let E_new = emulated::AllocatedEmulPoint::alloc( + cs.namespace(|| "E_new"), + self + .inputs + .as_ref() + .and_then(|inputs| inputs.E_new.as_ref()) + .map(|E_new| E_new.to_coordinates()), + self.params.limb_width, + self.params.n_limbs, + )?; + + let W_new = emulated::AllocatedEmulPoint::alloc( + cs.namespace(|| "W_new"), + self + .inputs + .as_ref() + .and_then(|inputs| inputs.W_new.as_ref()) + .map(|W_new| W_new.to_coordinates()), + self.params.limb_width, + self.params.n_limbs, + )?; + + Ok(( + pp_digest, i, z_0, z_i, data_p, data_c_1, data_c_2, E_new, W_new, + )) + } + + pub fn synthesize_base_case::Base>>( + &self, + mut cs: CS, + ) -> Result< + ( + AllocatedRelaxedR1CSInstance, + emulated::AllocatedEmulRelaxedR1CSInstance, + ), + SynthesisError, + > { + let U_c_default = AllocatedRelaxedR1CSInstance::default( + cs.namespace(|| "Allocate U_c_default"), + self.params.limb_width, + self.params.n_limbs, + )?; + + let U_p_default = emulated::AllocatedEmulRelaxedR1CSInstance::default( + cs.namespace(|| "Allocated U_p_default"), + self.params.limb_width, + self.params.n_limbs, + )?; + + // In the first folding step return the default relaxed instances for both the CycleFold and + // primary running accumulators + Ok((U_c_default, U_p_default)) + } + + pub fn synthesize_non_base_case::Base>>( + &self, + mut cs: CS, + pp_digest: &AllocatedNum, + i: &AllocatedNum, + z_0: &[AllocatedNum], + z_i: &[AllocatedNum], + data_p: &emulated::AllocatedFoldingData, + data_c_1: &AllocatedCycleFoldData, + data_c_2: &AllocatedCycleFoldData, + E_new: emulated::AllocatedEmulPoint, + W_new: emulated::AllocatedEmulPoint, + arity: usize, + ) -> Result< + ( + AllocatedRelaxedR1CSInstance, + emulated::AllocatedEmulRelaxedR1CSInstance, + AllocatedBit, + ), + SynthesisError, + > { + // Follows the outline written down here https://hackmd.io/@lurk-lab/HybHrnNFT + + // Calculate the hash of the non-deterministic advice for the primary circuit + let mut ro_p = E1::ROCircuit::new( + self.ro_consts.clone(), + 2 + 2 * arity + 2 * NUM_FE_IN_EMULATED_POINT + 3, + ); + + ro_p.absorb(pp_digest); + ro_p.absorb(i); + for e in z_0 { + ro_p.absorb(e) + } + for e in z_i { + ro_p.absorb(e) + } + data_p + .U + .absorb_in_ro(cs.namespace(|| "absorb U_p"), &mut ro_p)?; + + let hash_bits_p = ro_p.squeeze(cs.namespace(|| "primary hash bits"), NUM_HASH_BITS)?; + let hash_p = le_bits_to_num(cs.namespace(|| "primary hash"), &hash_bits_p)?; + + // check the hash matches the public IO from the last primary instance + let check_primary = alloc_num_equals( + cs.namespace(|| "u.X[0] = H(params, i, z0, zi, U_p)"), + &data_p.u_x0, + &hash_p, + )?; + + // Calculate the hash of the non-dterministic advice for the secondary circuit + let mut ro_c = E1::ROCircuit::new( + self.ro_consts.clone(), + 1 + 1 + 3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS, // pp + i + W + E + u + X + ); + + ro_c.absorb(pp_digest); + ro_c.absorb(i); + data_c_1 + .U + .absorb_in_ro(cs.namespace(|| "absorb U_c"), &mut ro_c)?; + let hash_c_bits = ro_c.squeeze(cs.namespace(|| "cyclefold hash bits"), NUM_HASH_BITS)?; + let hash_c = le_bits_to_num(cs.namespace(|| "cyclefold hash"), &hash_c_bits)?; + + // check the hash matches the public IO from the last primary instance + let check_cyclefold = alloc_num_equals( + cs.namespace(|| "u.X[1] = H(params, U_c)"), + &data_p.u_x1, + &hash_c, + )?; + + let check_io = AllocatedBit::and( + cs.namespace(|| "both IOs match"), + &check_primary, + &check_cyclefold, + )?; + + // Run NIVC.V on U_c, u_c_1, T_c_1 + let U_int = data_c_1.apply_fold( + cs.namespace(|| "fold u_c_1 into U_c"), + pp_digest, + self.ro_consts.clone(), + self.params.limb_width, + self.params.n_limbs, + )?; + + // Calculate h_int = H(pp, U_c_int) + let mut ro_c_int = E1::ROCircuit::new( + self.ro_consts.clone(), + 1 + 3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS, // pp + W + E + u + X + ); + ro_c_int.absorb(pp_digest); + U_int.absorb_in_ro(cs.namespace(|| "absorb U_c_int"), &mut ro_c_int)?; + let h_c_int_bits = + ro_c_int.squeeze(cs.namespace(|| "intermediate hash bits"), NUM_HASH_BITS)?; + let h_c_int = le_bits_to_num(cs.namespace(|| "intermediate hash"), &h_c_int_bits)?; + + // Calculate h_1 = H(pp, U_c_1) + let mut ro_c_1 = E1::ROCircuit::new( + self.ro_consts.clone(), + 1 + 3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS, // pp + W + E + u + X + ); + + ro_c_1.absorb(pp_digest); + data_c_2 + .U + .absorb_in_ro(cs.namespace(|| "absorb U_c_1"), &mut ro_c_1)?; + let h_c_1_bits = ro_c_1.squeeze(cs.namespace(|| "cyclefold_1 hash bits"), NUM_HASH_BITS)?; + let h_c_1 = le_bits_to_num(cs.namespace(|| "cyclefold_1 hash"), &h_c_1_bits)?; + + // Check the intermediate-calculated running instance matches the non-deterministic advice provided to the prover + let check_cyclefold_int = alloc_num_equals(cs.namespace(|| "h_int = h_c_1"), &h_c_int, &h_c_1)?; + + let checks_pass = AllocatedBit::and( + cs.namespace(|| "all checks passed"), + &check_io, + &check_cyclefold_int, + )?; + + // calculate the folded CycleFold accumulator + let U_c = data_c_2.apply_fold( + cs.namespace(|| "fold u_c_2 into U_c_1"), + pp_digest, + self.ro_consts.clone(), + self.params.limb_width, + self.params.n_limbs, + )?; + + // calculate the folded primary circuit accumulator + let U_p = data_p.U.fold_with_r1cs( + cs.namespace(|| "fold u_p into U_p"), + pp_digest, + W_new, + E_new, + &data_p.u_W, + &data_p.u_x0, + &data_p.u_x1, + &data_p.T, + self.ro_consts.clone(), + )?; + + Ok((U_c, U_p, checks_pass)) + } + + pub fn synthesize::Base>>( + self, + cs: &mut CS, + ) -> Result>, SynthesisError> { + // Circuit is documented here: https://hackmd.io/SBvAur_2RQmaduDi7gYbhw + let arity = self.step_circuit.arity(); + + // Allocate the witness + let (pp_digest, i, z_0, z_i, data_p, data_c_1, data_c_2, E_new, W_new) = + self.alloc_witness(cs.namespace(|| "alloc_witness"), arity)?; + + let zero = alloc_zero(cs.namespace(|| "zero")); + let is_base_case = alloc_num_equals(cs.namespace(|| "is base case"), &i, &zero)?; + + let (Unew_c_base, Unew_p_base) = self.synthesize_base_case(cs.namespace(|| "base case"))?; + + let (Unew_c_non_base, Unew_p_non_base, check_non_base_pass) = self.synthesize_non_base_case( + cs.namespace(|| "synthesize non base case"), + &pp_digest, + &i, + &z_0, + &z_i, + &data_p, + &data_c_1, + &data_c_2, + E_new, + W_new, + arity, + )?; + + let should_be_false = AllocatedBit::nor( + cs.namespace(|| "check_non_base_pass nor base_case"), + &check_non_base_pass, + &is_base_case, + )?; + cs.enforce( + || "check_non_base_pass nor base_case = false", + |lc| lc + should_be_false.get_variable(), + |lc| lc + CS::one(), + |lc| lc, + ); + + // select the new running primary instance + let Unew_p = Unew_p_base.conditionally_select( + cs.namespace(|| "compute Unew_p"), + &Unew_p_non_base, + &Boolean::from(is_base_case.clone()), + )?; + + // select the new running CycleFold instance + let Unew_c = Unew_c_base.conditionally_select( + cs.namespace(|| "compute Unew_c"), + &Unew_c_non_base, + &Boolean::from(is_base_case.clone()), + )?; + + // Compute i + 1 + let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || { + Ok(*i.get_value().get()? + E1::Base::ONE) + })?; + cs.enforce( + || "check i + 1", + |lc| lc, + |lc| lc, + |lc| lc + i_new.get_variable() - CS::one() - i.get_variable(), + ); + + // Compute z_{i+1} + let z_input = conditionally_select_slice( + cs.namespace(|| "select input to F"), + &z_0, + &z_i, + &Boolean::from(is_base_case), + )?; + + let z_next = self + .step_circuit + .synthesize(&mut cs.namespace(|| "F"), &z_input)?; + + if z_next.len() != arity { + return Err(SynthesisError::IncompatibleLengthVector( + "z_next".to_string(), + )); + } + + // Calculate the first component of the public IO as the hash of the calculated primary running + // instance + let mut ro_p = E1::ROCircuit::new( + self.ro_consts.clone(), + 2 + 2 * arity + (2 * NUM_FE_IN_EMULATED_POINT + 3), // pp + i + z_0 + z_next + (U_p) + ); + ro_p.absorb(&pp_digest); + ro_p.absorb(&i_new); + for e in &z_0 { + ro_p.absorb(e); + } + for e in &z_next { + ro_p.absorb(e); + } + Unew_p.absorb_in_ro(cs.namespace(|| "absorb Unew_p"), &mut ro_p)?; + let hash_p_bits = ro_p.squeeze(cs.namespace(|| "hash_p_bits"), NUM_HASH_BITS)?; + let hash_p = le_bits_to_num(cs.namespace(|| "hash_p"), &hash_p_bits)?; + + // Calculate the second component of the public IO as the hash of the calculated CycleFold running + // instance + let mut ro_c = E1::ROCircuit::new( + self.ro_consts, + 1 + 1 + 3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS, // pp + i + W + E + u + X + ); + ro_c.absorb(&pp_digest); + ro_c.absorb(&i_new); + Unew_c.absorb_in_ro(cs.namespace(|| "absorb Unew_c"), &mut ro_c)?; + let hash_c_bits = ro_c.squeeze(cs.namespace(|| "hash_c_bits"), NUM_HASH_BITS)?; + let hash_c = le_bits_to_num(cs.namespace(|| "hash_c"), &hash_c_bits)?; + + hash_p.inputize(cs.namespace(|| "u_p.x[0] = hash_p"))?; + hash_c.inputize(cs.namespace(|| "u_p.x[1] = hash_c"))?; + + Ok(z_next) + } +} + +#[cfg(test)] +mod test { + use crate::{ + bellpepper::test_shape_cs::TestShapeCS, + constants::{BN_LIMB_WIDTH, BN_N_LIMBS}, + provider::{Bn256EngineKZG, PallasEngine, Secp256k1Engine}, + traits::{circuit::TrivialCircuit, CurveCycleEquipped, Dual}, + }; + + use expect_test::{expect, Expect}; + + use super::*; + + fn test_augmented_circuit_size_with(expected_cons: &Expect, expected_var: &Expect) + where + E: CurveCycleEquipped, + { + let params = AugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS); + + let ro_consts = ROConstantsCircuit::::default(); + + let step_circuit = TrivialCircuit::::default(); + + let circuit = AugmentedCircuit::, TrivialCircuit>::new( + ¶ms, + ro_consts, + None, + &step_circuit, + ); + let mut cs: TestShapeCS> = TestShapeCS::default(); + + let res = circuit.synthesize(&mut cs); + + res.unwrap(); + + let num_constraints = cs.num_constraints(); + let num_variables = cs.num_aux(); + + expected_cons.assert_eq(&num_constraints.to_string()); + expected_var.assert_eq(&num_variables.to_string()); + } + + #[test] + fn test_augmented_circuit_size() { + test_augmented_circuit_size_with::(&expect!["33289"], &expect!["33323"]); + test_augmented_circuit_size_with::(&expect!["35125"], &expect!["35159"]); + test_augmented_circuit_size_with::(&expect!["33856"], &expect!["33890"]); + } +} diff --git a/src/cyclefold/snark.rs b/src/cyclefold/snark.rs new file mode 100644 index 000000000..930823333 --- /dev/null +++ b/src/cyclefold/snark.rs @@ -0,0 +1,563 @@ +//! This module defines the Cyclefold `RecursiveSNARK` type with its `new`, `prove_step`, and +//! `verify` methods. + +use crate::{ + bellpepper::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, + }, + constants::{ + BN_LIMB_WIDTH, BN_N_LIMBS, NIO_CYCLE_FOLD, NUM_CHALLENGE_BITS, NUM_FE_IN_EMULATED_POINT, + NUM_HASH_BITS, + }, + cyclefold::circuit::CycleFoldCircuit, + errors::NovaError, + gadgets::scalar_as_base, + r1cs::{ + self, CommitmentKeyHint, R1CSInstance, R1CSResult, R1CSWitness, RelaxedR1CSInstance, + RelaxedR1CSWitness, + }, + traits::{ + circuit::StepCircuit, commitment::CommitmentTrait, AbsorbInROTrait, CurveCycleEquipped, Dual, + Engine, ROConstantsCircuit, ROTrait, + }, + Commitment, CommitmentKey, DigestComputer, R1CSWithArity, ROConstants, ResourceBuffer, + SimpleDigestible, +}; + +use super::{ + nifs::{CycleFoldNIFS, PrimaryNIFS}, + nova_circuit::{AugmentedCircuit, AugmentedCircuitInputs, AugmentedCircuitParams}, + util::{absorb_primary_relaxed_r1cs, FoldingData}, +}; + +use abomonation::Abomonation; +use abomonation_derive::Abomonation; +use bellpepper_core::{ConstraintSystem, SynthesisError}; +use ff::{PrimeField, PrimeFieldBits}; +use once_cell::sync::OnceCell; +use serde::{Deserialize, Serialize}; + +/// The public parameters used in the CycleFold recursive SNARK proof and verification +#[derive(Clone, Debug, PartialEq, Serialize, Deserialize, Abomonation)] +#[serde(bound = "")] +#[abomonation_bounds( +where + E1: CurveCycleEquipped, + ::Repr: Abomonation, + < as Engine>::Scalar as PrimeField>::Repr: Abomonation, +)] +pub struct PublicParams +where + E1: CurveCycleEquipped, +{ + F_arity_primary: usize, + ro_consts_primary: ROConstants>, + ro_consts_circuit_primary: ROConstantsCircuit>, + ck_primary: CommitmentKey, + circuit_shape_primary: R1CSWithArity, + augmented_circuit_params: AugmentedCircuitParams, + + ro_consts_cyclefold: ROConstants>, + ck_cyclefold: CommitmentKey>, + circuit_shape_cyclefold: R1CSWithArity>, + #[abomonation_skip] + #[serde(skip, default = "OnceCell::new")] + digest: OnceCell, +} + +impl PublicParams +where + E1: CurveCycleEquipped, +{ + /// Builds the public parameters for the circuit `C1`. + /// The same note for public parameter hints apply as in the case for Nova's public parameters: + /// For some final compressing SNARKs the size of the commitment key must be larger, so we include + /// `ck_hint_primary` and `ck_hint_cyclefold` parameters to accommodate this. + pub fn setup>( + c_primary: &C1, + ck_hint_primary: &CommitmentKeyHint, + ck_hint_cyclefold: &CommitmentKeyHint>, + ) -> Self { + let F_arity_primary = c_primary.arity(); + let ro_consts_primary = ROConstants::>::default(); + let ro_consts_circuit_primary = ROConstantsCircuit::>::default(); + + let augmented_circuit_params = AugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS); + let circuit_primary: AugmentedCircuit<'_, Dual, E1, C1> = AugmentedCircuit::new( + &augmented_circuit_params, + ro_consts_circuit_primary.clone(), + None, + c_primary, + ); + let mut cs: ShapeCS = ShapeCS::new(); + let _ = circuit_primary.synthesize(&mut cs); + let (r1cs_shape_primary, ck_primary) = cs.r1cs_shape_and_key(ck_hint_primary); + let circuit_shape_primary = R1CSWithArity::new(r1cs_shape_primary, F_arity_primary); + + let ro_consts_cyclefold = ROConstants::>::default(); + let mut cs: ShapeCS> = ShapeCS::new(); + let circuit_cyclefold: CycleFoldCircuit = CycleFoldCircuit::default(); + let _ = circuit_cyclefold.synthesize(&mut cs); + let (r1cs_shape_cyclefold, ck_cyclefold) = cs.r1cs_shape_and_key(ck_hint_cyclefold); + let circuit_shape_cyclefold = R1CSWithArity::new(r1cs_shape_cyclefold, 0); + + Self { + F_arity_primary, + ro_consts_primary, + ro_consts_circuit_primary, + ck_primary, + circuit_shape_primary, + augmented_circuit_params, + ro_consts_cyclefold, + ck_cyclefold, + circuit_shape_cyclefold, + digest: OnceCell::new(), + } + } + + /// Calculate the digest of the public parameters. + pub fn digest(&self) -> E1::Scalar { + self + .digest + .get_or_try_init(|| DigestComputer::new(self).digest()) + .cloned() + .expect("Failure in retrieving digest") + } + + /// Returns the number of constraints in the primary and cyclefold circuits + pub const fn num_constraints(&self) -> (usize, usize) { + ( + self.circuit_shape_primary.r1cs_shape.num_cons, + self.circuit_shape_cyclefold.r1cs_shape.num_cons, + ) + } + + /// Returns the number of variables in the primary and cyclefold circuits + pub const fn num_variables(&self) -> (usize, usize) { + ( + self.circuit_shape_primary.r1cs_shape.num_vars, + self.circuit_shape_cyclefold.r1cs_shape.num_vars, + ) + } +} + +impl SimpleDigestible for PublicParams where E1: CurveCycleEquipped {} + +/// A SNARK that proves the correct execution of an incremental computation in the CycleFold folding +/// scheme. +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct RecursiveSNARK +where + E1: CurveCycleEquipped, +{ + // Input + z0_primary: Vec, + + // primary circuit data + r_W_primary: RelaxedR1CSWitness, + r_U_primary: RelaxedR1CSInstance, + l_w_primary: R1CSWitness, + l_u_primary: R1CSInstance, + + // cyclefold circuit data + r_W_cyclefold: RelaxedR1CSWitness>, + r_U_cyclefold: RelaxedR1CSInstance>, + + // memory buffers for folding steps + buffer_primary: ResourceBuffer, + buffer_cyclefold: ResourceBuffer>, + + i: usize, + zi_primary: Vec, +} + +impl RecursiveSNARK +where + E1: CurveCycleEquipped, +{ + /// Create a new instance of a recursive SNARK + pub fn new>( + pp: &PublicParams, + c_primary: &C1, + z0_primary: &[E1::Scalar], + ) -> Result { + if z0_primary.len() != pp.F_arity_primary { + return Err(NovaError::InvalidInitialInputLength); + } + + let r1cs_primary = &pp.circuit_shape_primary.r1cs_shape; + let r1cs_cyclefold = &pp.circuit_shape_cyclefold.r1cs_shape; + + let r_U_cyclefold = RelaxedR1CSInstance::default(&pp.ck_cyclefold, r1cs_cyclefold); + let r_W_cyclefold = RelaxedR1CSWitness::default(r1cs_cyclefold); + + let mut cs_primary = SatisfyingAssignment::::new(); + let inputs_primary: AugmentedCircuitInputs, E1> = AugmentedCircuitInputs::new( + scalar_as_base::(pp.digest()), + as Engine>::Base::from(0u64), + z0_primary.to_vec(), + None, + None, + None, + None, + None, + None, + ); + + let circuit_primary = AugmentedCircuit::new( + &pp.augmented_circuit_params, + pp.ro_consts_circuit_primary.clone(), + Some(inputs_primary), + c_primary, + ); + + let zi_primary = circuit_primary.synthesize(&mut cs_primary)?; + let (l_u_primary, l_w_primary) = + cs_primary.r1cs_instance_and_witness(r1cs_primary, &pp.ck_primary)?; + + let r_U_primary = RelaxedR1CSInstance::default(&pp.ck_primary, r1cs_primary); + let r_W_primary = RelaxedR1CSWitness::default(r1cs_primary); + + let zi_primary = zi_primary + .iter() + .map(|v| v.get_value().ok_or(SynthesisError::AssignmentMissing)) + .collect::, _>>()?; + + let buffer_primary = ResourceBuffer { + l_w: None, + l_u: None, + ABC_Z_1: R1CSResult::default(r1cs_primary.num_cons), + ABC_Z_2: R1CSResult::default(r1cs_primary.num_cons), + T: r1cs::default_T::(r1cs_primary.num_cons), + }; + + let buffer_cyclefold = ResourceBuffer { + l_w: None, + l_u: None, + ABC_Z_1: R1CSResult::default(r1cs_cyclefold.num_cons), + ABC_Z_2: R1CSResult::default(r1cs_cyclefold.num_cons), + T: r1cs::default_T::>(r1cs_cyclefold.num_cons), + }; + + Ok(Self { + z0_primary: z0_primary.to_vec(), + r_W_primary, + r_U_primary, + l_w_primary, + l_u_primary, + r_W_cyclefold, + r_U_cyclefold, + buffer_primary, + buffer_cyclefold, + i: 0, + zi_primary, + }) + } + + /// Update the `RecursiveSNARK` by proving a step of the incremental computation. + pub fn prove_step>( + &mut self, + pp: &PublicParams, + c_primary: &C1, + ) -> Result<(), NovaError> { + if self.i == 0 { + self.i = 1; + return Ok(()); + } + + let (nifs_primary, (r_U_primary, r_W_primary), r) = PrimaryNIFS::>::prove( + &pp.ck_primary, + &pp.ro_consts_primary, + &pp.digest(), + &pp.circuit_shape_primary.r1cs_shape, + &self.r_U_primary, + &self.r_W_primary, + &self.l_u_primary, + &self.l_w_primary, + )?; + + let r_bools = r + .to_le_bits() + .iter() + .map(|b| Some(*b)) + .take(NUM_CHALLENGE_BITS) + .collect::>>() + .map(|v| v.try_into().unwrap()); + + let comm_T = Commitment::::decompress(&nifs_primary.comm_T)?; + let E_new = self.r_U_primary.comm_E + comm_T * r; + + let W_new = self.r_U_primary.comm_W + self.l_u_primary.comm_W * r; + + let mut cs_cyclefold_E = SatisfyingAssignment::>::with_capacity( + pp.circuit_shape_cyclefold.r1cs_shape.num_io + 1, + pp.circuit_shape_cyclefold.r1cs_shape.num_vars, + ); + + let circuit_cyclefold_E: CycleFoldCircuit = + CycleFoldCircuit::new(Some(self.r_U_primary.comm_E), Some(comm_T), r_bools); + + let _ = circuit_cyclefold_E.synthesize(&mut cs_cyclefold_E); + + let (l_u_cyclefold_E, l_w_cyclefold_E) = cs_cyclefold_E + .r1cs_instance_and_witness(&pp.circuit_shape_cyclefold.r1cs_shape, &pp.ck_cyclefold) + .map_err(|_| NovaError::UnSat)?; + + // TODO: check if this is better or worse than `prove_mut` with a clone of `self.r_U_cyclefold` + let (nifs_cyclefold_E, (r_U_cyclefold_E, r_W_cyclefold_E)) = CycleFoldNIFS::prove( + &pp.ck_cyclefold, + &pp.ro_consts_cyclefold, + &scalar_as_base::(pp.digest()), + &pp.circuit_shape_cyclefold.r1cs_shape, + &self.r_U_cyclefold, + &self.r_W_cyclefold, + &l_u_cyclefold_E, + &l_w_cyclefold_E, + )?; + + let comm_T_E = Commitment::>::decompress(&nifs_cyclefold_E.comm_T)?; + + let mut cs_cyclefold_W = SatisfyingAssignment::>::with_capacity( + pp.circuit_shape_cyclefold.r1cs_shape.num_io + 1, + pp.circuit_shape_cyclefold.r1cs_shape.num_vars, + ); + + let circuit_cyclefold_W: CycleFoldCircuit = CycleFoldCircuit::new( + Some(self.r_U_primary.comm_W), + Some(self.l_u_primary.comm_W), + r_bools, + ); + + let _ = circuit_cyclefold_W.synthesize(&mut cs_cyclefold_W); + + let (l_u_cyclefold_W, l_w_cyclefold_W) = cs_cyclefold_W + .r1cs_instance_and_witness(&pp.circuit_shape_cyclefold.r1cs_shape, &pp.ck_cyclefold) + .map_err(|_| NovaError::UnSat)?; + + // TODO: check if this is better or worse than `prove_mut` with a clone of r_U_cyclefold_E + let (nifs_cyclefold_W, (r_U_cyclefold_W, r_W_cyclefold_W)) = CycleFoldNIFS::prove( + &pp.ck_cyclefold, + &pp.ro_consts_cyclefold, + &scalar_as_base::(pp.digest()), + &pp.circuit_shape_cyclefold.r1cs_shape, + &r_U_cyclefold_E, + &r_W_cyclefold_E, + &l_u_cyclefold_W, + &l_w_cyclefold_W, + )?; + + let comm_T_W = Commitment::>::decompress(&nifs_cyclefold_W.comm_T)?; + + let mut cs_primary = SatisfyingAssignment::::with_capacity( + pp.circuit_shape_primary.r1cs_shape.num_io + 1, + pp.circuit_shape_primary.r1cs_shape.num_vars, + ); + + let data_p = FoldingData::new(self.r_U_primary.clone(), self.l_u_primary.clone(), comm_T); + let data_c_E = FoldingData::new(self.r_U_cyclefold.clone(), l_u_cyclefold_E, comm_T_E); + let data_c_W = FoldingData::new(r_U_cyclefold_E, l_u_cyclefold_W, comm_T_W); + + let inputs_primary: AugmentedCircuitInputs, E1> = AugmentedCircuitInputs::new( + scalar_as_base::(pp.digest()), + as Engine>::Base::from(self.i as u64), + self.z0_primary.clone(), + Some(self.zi_primary.clone()), + Some(data_p), + Some(data_c_E), + Some(data_c_W), + Some(E_new), + Some(W_new), + ); + + let circuit_primary: AugmentedCircuit<'_, Dual, E1, C1> = AugmentedCircuit::new( + &pp.augmented_circuit_params, + pp.ro_consts_circuit_primary.clone(), + Some(inputs_primary), + c_primary, + ); + + let zi_primary = circuit_primary.synthesize(&mut cs_primary)?; + + let (l_u_primary, l_w_primary) = cs_primary + .r1cs_instance_and_witness(&pp.circuit_shape_primary.r1cs_shape, &pp.ck_primary) + .map_err(|_| NovaError::UnSat)?; + + self.zi_primary = zi_primary + .iter() + .map(|v| v.get_value().ok_or(SynthesisError::AssignmentMissing)) + .collect::, _>>()?; + + self.r_U_primary = r_U_primary; + self.r_W_primary = r_W_primary; + self.l_u_primary = l_u_primary; + self.l_w_primary = l_w_primary; + self.r_U_cyclefold = r_U_cyclefold_W; + self.r_W_cyclefold = r_W_cyclefold_W; + + self.i += 1; + + Ok(()) + } + + /// Verify the correctness of the `RecursiveSNARK` + pub fn verify( + &self, + pp: &PublicParams, + num_steps: usize, + z0_primary: &[E1::Scalar], + ) -> Result, NovaError> { + // number of steps cannot be zero + let is_num_steps_zero = num_steps == 0; + + // check if the provided proof has executed num_steps + let is_num_steps_not_match = self.i != num_steps; + + // check if the initial inputs match + let is_inputs_not_match = self.z0_primary != z0_primary; + + // check if the (relaxed) R1CS instances have two public outputs + let is_instance_has_two_outputs = self.r_U_primary.X.len() != 2; + + if is_num_steps_zero + || is_num_steps_not_match + || is_inputs_not_match + || is_instance_has_two_outputs + { + return Err(NovaError::ProofVerifyError); + } + + // Calculate the hashes of the primary running instance and cyclefold running instance + let (hash_primary, hash_cyclefold) = { + let mut hasher = as Engine>::RO::new( + pp.ro_consts_primary.clone(), + 2 + 2 * pp.F_arity_primary + 2 * NUM_FE_IN_EMULATED_POINT + 3, + ); + hasher.absorb(pp.digest()); + hasher.absorb(E1::Scalar::from(num_steps as u64)); + for e in z0_primary { + hasher.absorb(*e); + } + for e in &self.zi_primary { + hasher.absorb(*e); + } + absorb_primary_relaxed_r1cs::>(&self.r_U_primary, &mut hasher); + let hash_primary = hasher.squeeze(NUM_HASH_BITS); + + let mut hasher = as Engine>::RO::new( + pp.ro_consts_cyclefold.clone(), + 1 + 1 + 3 + 3 + 1 + NIO_CYCLE_FOLD * BN_N_LIMBS, + ); + hasher.absorb(pp.digest()); + hasher.absorb(E1::Scalar::from(num_steps as u64)); + self.r_U_cyclefold.absorb_in_ro(&mut hasher); + let hash_cyclefold = hasher.squeeze(NUM_HASH_BITS); + + (hash_primary, hash_cyclefold) + }; + + // Verify the hashes equal the public IO for the final primary instance + if scalar_as_base::>(hash_primary) != self.l_u_primary.X[0] + || scalar_as_base::>(hash_cyclefold) != self.l_u_primary.X[1] + { + return Err(NovaError::ProofVerifyError); + } + + // Verify the satisfiability of running relaxed instances, and the final primary instance. + let (res_r_primary, (res_l_primary, res_r_cyclefold)) = rayon::join( + || { + pp.circuit_shape_primary.r1cs_shape.is_sat_relaxed( + &pp.ck_primary, + &self.r_U_primary, + &self.r_W_primary, + ) + }, + || { + rayon::join( + || { + pp.circuit_shape_primary.r1cs_shape.is_sat( + &pp.ck_primary, + &self.l_u_primary, + &self.l_w_primary, + ) + }, + || { + pp.circuit_shape_cyclefold.r1cs_shape.is_sat_relaxed( + &pp.ck_cyclefold, + &self.r_U_cyclefold, + &self.r_W_cyclefold, + ) + }, + ) + }, + ); + + res_r_primary?; + res_l_primary?; + res_r_cyclefold?; + + Ok(self.zi_primary.clone()) + } +} + +#[cfg(test)] +mod test { + use std::marker::PhantomData; + + use bellpepper_core::num::AllocatedNum; + + use super::*; + use crate::{ + provider::{Bn256EngineKZG, PallasEngine, Secp256k1Engine}, + traits::snark::default_ck_hint, + }; + + #[derive(Clone)] + struct SquareCircuit { + _p: PhantomData, + } + + impl StepCircuit for SquareCircuit { + fn arity(&self) -> usize { + 1 + } + + fn synthesize>( + &self, + cs: &mut CS, + z: &[AllocatedNum], + ) -> Result>, SynthesisError> { + let x = &z[0]; + let x_sq = x.square(cs.namespace(|| "x_sq"))?; + + Ok(vec![x_sq]) + } + } + + fn test_trivial_cyclefold_prove_verify_with() { + let primary_circuit = SquareCircuit:: { _p: PhantomData }; + + let pp = PublicParams::::setup(&primary_circuit, &*default_ck_hint(), &*default_ck_hint()); + + let z0 = vec![E::Scalar::from(2u64)]; + + let mut recursive_snark = RecursiveSNARK::new(&pp, &primary_circuit, &z0).unwrap(); + + (1..5).for_each(|iter| { + let res_proof = recursive_snark.prove_step(&pp, &primary_circuit); + res_proof.unwrap(); + + let res_verify = recursive_snark.verify(&pp, iter, &z0); + res_verify.unwrap(); + }); + } + + #[test] + fn test_cyclefold_prove_verify() { + test_trivial_cyclefold_prove_verify_with::(); + test_trivial_cyclefold_prove_verify_with::(); + test_trivial_cyclefold_prove_verify_with::(); + } +} diff --git a/src/cyclefold/util.rs b/src/cyclefold/util.rs new file mode 100644 index 000000000..34e8f89d7 --- /dev/null +++ b/src/cyclefold/util.rs @@ -0,0 +1,89 @@ +//! This module defines some useful utilities for RO absorbing, and the Folding data used in the +//! CycleFold folding scheme. + +use crate::{ + constants::{BN_LIMB_WIDTH, BN_N_LIMBS}, + gadgets::{f_to_nat, nat_to_limbs, scalar_as_base}, + r1cs::{R1CSInstance, RelaxedR1CSInstance}, + traits::{commitment::CommitmentTrait, AbsorbInROTrait, Engine, ROTrait}, + Commitment, +}; + +use ff::Field; +use serde::{Deserialize, Serialize}; + +/// Absorb a commitment over engine `E1` into an RO over engine `E2` by absorbing the limbs +pub(super) fn absorb_primary_commitment( + comm: &impl CommitmentTrait, + ro: &mut impl ROTrait, +) where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + let (x, y, is_infinity) = comm.to_coordinates(); + + let x_limbs = nat_to_limbs(&f_to_nat(&x), BN_LIMB_WIDTH, BN_N_LIMBS).unwrap(); + let y_limbs = nat_to_limbs(&f_to_nat(&y), BN_LIMB_WIDTH, BN_N_LIMBS).unwrap(); + + for limb in x_limbs { + ro.absorb(scalar_as_base::(limb)); + } + for limb in y_limbs { + ro.absorb(scalar_as_base::(limb)); + } + if is_infinity { + ro.absorb(::Scalar::ONE); + } else { + ro.absorb(::Scalar::ZERO); + } +} + +pub(super) fn absorb_primary_r1cs( + u: &R1CSInstance, + ro: &mut impl ROTrait, +) where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + absorb_primary_commitment::(&u.comm_W, ro); + for x in &u.X { + ro.absorb(*x); + } +} + +pub(super) fn absorb_cyclefold_r1cs(u: &R1CSInstance, ro: &mut E::RO) { + u.comm_W.absorb_in_ro(ro); + u.X.iter().for_each(|x| { + let limbs: Vec = nat_to_limbs(&f_to_nat(x), BN_LIMB_WIDTH, BN_N_LIMBS).unwrap(); + limbs + .into_iter() + .for_each(|limb| ro.absorb(scalar_as_base::(limb))); + }); +} + +pub(super) fn absorb_primary_relaxed_r1cs(U: &RelaxedR1CSInstance, ro: &mut E2::RO) +where + E1: Engine::Scalar>, + E2: Engine::Scalar>, +{ + absorb_primary_commitment::(&U.comm_W, ro); + absorb_primary_commitment::(&U.comm_E, ro); + ro.absorb(U.u); + for e in &U.X { + ro.absorb(*e); + } +} + +#[derive(Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub(super) struct FoldingData { + pub U: RelaxedR1CSInstance, + pub u: R1CSInstance, + pub T: Commitment, +} + +impl FoldingData { + pub fn new(U: RelaxedR1CSInstance, u: R1CSInstance, T: Commitment) -> Self { + Self { U, u, T } + } +} diff --git a/src/gadgets/mod.rs b/src/gadgets/mod.rs index 7022edcf2..5841f6ec2 100644 --- a/src/gadgets/mod.rs +++ b/src/gadgets/mod.rs @@ -3,7 +3,7 @@ mod ecc; pub(crate) use ecc::AllocatedPoint; mod nonnative; -pub(crate) use nonnative::{bignat::nat_to_limbs, util::f_to_nat}; +pub(crate) use nonnative::{bignat::nat_to_limbs, bignat::BigNat, util::f_to_nat, util::Num}; mod r1cs; pub(crate) use r1cs::{ @@ -15,5 +15,6 @@ mod utils; #[cfg(test)] pub(crate) use utils::alloc_one; pub(crate) use utils::{ - alloc_num_equals, alloc_scalar_as_base, alloc_zero, le_bits_to_num, scalar_as_base, + alloc_bignat_constant, alloc_num_equals, alloc_scalar_as_base, alloc_zero, + conditionally_select_allocated_bit, conditionally_select_bignat, le_bits_to_num, scalar_as_base, }; diff --git a/src/gadgets/nonnative/bignat.rs b/src/gadgets/nonnative/bignat.rs index 66dead141..e1bc32df4 100644 --- a/src/gadgets/nonnative/bignat.rs +++ b/src/gadgets/nonnative/bignat.rs @@ -349,7 +349,7 @@ impl BigNat { ) -> Result<(), SynthesisError> { self.enforce_limb_width_agreement(other, "equal_when_carried")?; - // We'll propegate carries over the first `n` limbs. + // We'll propagate carries over the first `n` limbs. let n = min(self.limbs.len(), other.limbs.len()); let target_base = BigInt::from(1u8) << self.params.limb_width as u32; let mut accumulated_extra = BigInt::from(0usize); diff --git a/src/gadgets/nonnative/util.rs b/src/gadgets/nonnative/util.rs index 3a4f30aa8..c63108f07 100644 --- a/src/gadgets/nonnative/util.rs +++ b/src/gadgets/nonnative/util.rs @@ -155,8 +155,7 @@ impl Num { Ok(()) } - /// Computes the natural number represented by an array of bits. - /// Checks if the natural number equals `self` + /// Checks if the natural number equals an array of bits. pub fn is_equal>(&self, mut cs: CS, other: &Bitvector) { let mut f = Scalar::ONE; let sum = other diff --git a/src/gadgets/r1cs.rs b/src/gadgets/r1cs.rs index 85b87f7c2..3314393f9 100644 --- a/src/gadgets/r1cs.rs +++ b/src/gadgets/r1cs.rs @@ -4,7 +4,7 @@ use super::nonnative::{ util::{f_to_nat, Num}, }; use crate::{ - constants::{NUM_CHALLENGE_BITS, NUM_FE_FOR_RO}, + constants::{NUM_CHALLENGE_BITS, NUM_FE_WITHOUT_IO_FOR_NOVA_FOLD}, gadgets::{ ecc::AllocatedPoint, utils::{ @@ -229,7 +229,7 @@ impl AllocatedRelaxedR1CSInstance { n_limbs: usize, ) -> Result { // Compute r: - let mut ro = E::ROCircuit::new(ro_consts, NUM_FE_FOR_RO); + let mut ro = E::ROCircuit::new(ro_consts, NUM_FE_WITHOUT_IO_FOR_NOVA_FOLD + N); ro.absorb(params); // running instance `U` does not need to absorbed since u.X[0] = Hash(params, U, i, z0, zi) diff --git a/src/gadgets/utils.rs b/src/gadgets/utils.rs index 1b256c9d7..fcae1350e 100644 --- a/src/gadgets/utils.rs +++ b/src/gadgets/utils.rs @@ -169,6 +169,33 @@ pub fn alloc_num_equals>( Ok(r) } +// TODO: Figure out if this can be done better +pub fn conditionally_select_allocated_bit>( + mut cs: CS, + a: &AllocatedBit, + b: &AllocatedBit, + condition: &Boolean, +) -> Result { + let c = AllocatedBit::alloc( + cs.namespace(|| "conditionally select result"), + if condition.get_value().unwrap_or(false) { + a.get_value() + } else { + b.get_value() + }, + )?; + + // a * condition + b*(1-condition) = c -> + // a * condition - b*condition = c - b + cs.enforce( + || "conditional select constraint", + |lc| lc + a.get_variable() - b.get_variable(), + |_| condition.lc(CS::one(), F::ONE), + |lc| lc + c.get_variable() - b.get_variable(), + ); + + Ok(c) +} /// If condition return a otherwise b where a and b are `BigNats` pub fn conditionally_select_bignat>( mut cs: CS, diff --git a/src/lib.rs b/src/lib.rs index de0f9cc2a..8763f0df2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -25,6 +25,7 @@ pub mod r1cs; pub mod spartan; pub mod traits; +pub mod cyclefold; pub mod supernova; use once_cell::sync::OnceCell; @@ -538,7 +539,7 @@ where let l_u_secondary_i = self.l_u_secondary.clone(); // fold the secondary circuit's instance - let nifs_secondary = NIFS::prove_mut( + let (nifs_secondary, _) = NIFS::prove_mut( &*pp.ck_secondary, &pp.ro_consts_secondary, &scalar_as_base::(pp.digest()), @@ -579,7 +580,7 @@ where cs_primary.r1cs_instance_and_witness(&pp.circuit_shape_primary.r1cs_shape, &pp.ck_primary)?; // fold the primary circuit's instance - let nifs_primary = NIFS::prove_mut( + let (nifs_primary, _) = NIFS::prove_mut( &*pp.ck_primary, &pp.ro_consts_primary, &pp.digest(), @@ -850,7 +851,7 @@ where recursive_snark: &RecursiveSNARK, ) -> Result { // fold the secondary circuit's instance with its running instance - let (nifs_secondary, (f_U_secondary, f_W_secondary)) = NIFS::prove( + let (nifs_secondary, (f_U_secondary, f_W_secondary), _) = NIFS::prove( &*pp.ck_secondary, &pp.ro_consts_secondary, &scalar_as_base::(pp.digest()), diff --git a/src/nifs.rs b/src/nifs.rs index e116e55b6..f0630e533 100644 --- a/src/nifs.rs +++ b/src/nifs.rs @@ -2,13 +2,13 @@ #![allow(non_snake_case)] use crate::{ - constants::{NUM_CHALLENGE_BITS, NUM_FE_FOR_RO}, + constants::{NUM_CHALLENGE_BITS, NUM_FE_FOR_RO, NUM_FE_WITHOUT_IO_FOR_NOVA_FOLD}, errors::NovaError, r1cs::{ R1CSInstance, R1CSResult, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness, }, scalar_as_base, - traits::{commitment::CommitmentTrait, AbsorbInROTrait, Engine, ROTrait}, + traits::{commitment::CommitmentTrait, AbsorbInROTrait, Engine, ROConstants, ROTrait}, Commitment, CommitmentKey, CompressedCommitment, }; use serde::{Deserialize, Serialize}; @@ -21,9 +21,6 @@ pub struct NIFS { pub(crate) comm_T: CompressedCommitment, } -type ROConstants = - <::RO as ROTrait<::Base, ::Scalar>>::Constants; - impl NIFS { /// Takes as input a Relaxed R1CS instance-witness tuple `(U1, W1)` and /// an R1CS instance-witness tuple `(U2, W2)` with the same structure `shape` @@ -48,9 +45,25 @@ impl NIFS { W1: &RelaxedR1CSWitness, U2: &R1CSInstance, W2: &R1CSWitness, - ) -> Result<(Self, (RelaxedR1CSInstance, RelaxedR1CSWitness)), NovaError> { + ) -> Result< + ( + Self, + (RelaxedR1CSInstance, RelaxedR1CSWitness), + E::Scalar, + ), + NovaError, + > { + // Check `U1` and `U2` have the same arity + let io_arity = U1.X.len(); + if io_arity != U2.X.len() { + return Err(NovaError::InvalidInputLength); + } + // initialize a new RO - let mut ro = E::RO::new(ro_consts.clone(), NUM_FE_FOR_RO); + let mut ro = E::RO::new( + ro_consts.clone(), + NUM_FE_WITHOUT_IO_FOR_NOVA_FOLD + io_arity, + ); // append the digest of pp to the transcript ro.absorb(scalar_as_base::(*pp_digest)); @@ -79,6 +92,7 @@ impl NIFS { comm_T: comm_T.compress(), }, (U, W), + r, )) } @@ -101,7 +115,7 @@ impl NIFS { T: &mut Vec, ABC_Z_1: &mut R1CSResult, ABC_Z_2: &mut R1CSResult, - ) -> Result { + ) -> Result<(Self, E::Scalar), NovaError> { // initialize a new RO let mut ro = E::RO::new(ro_consts.clone(), NUM_FE_FOR_RO); @@ -127,9 +141,12 @@ impl NIFS { W1.fold_mut(W2, T, &r)?; // return the commitment - Ok(Self { - comm_T: comm_T.compress(), - }) + Ok(( + Self { + comm_T: comm_T.compress(), + }, + r, + )) } /// Takes as input a relaxed R1CS instance `U1` and R1CS instance `U2` @@ -279,7 +296,7 @@ mod tests { // produce a step SNARK with (W1, U1) as the first incoming witness-instance pair let res = NIFS::prove(ck, ro_consts, pp_digest, shape, &r_U, &r_W, U1, W1); assert!(res.is_ok()); - let (nifs, (_U, W)) = res.unwrap(); + let (nifs, (_U, W), _) = res.unwrap(); // verify the step SNARK with U1 as the first incoming instance let res = nifs.verify(ro_consts, pp_digest, &r_U, U1); @@ -295,7 +312,7 @@ mod tests { // produce a step SNARK with (W2, U2) as the second incoming witness-instance pair let res = NIFS::prove(ck, ro_consts, pp_digest, shape, &r_U, &r_W, U2, W2); assert!(res.is_ok()); - let (nifs, (_U, W)) = res.unwrap(); + let (nifs, (_U, W), _) = res.unwrap(); // verify the step SNARK with U1 as the first incoming instance let res = nifs.verify(ro_consts, pp_digest, &r_U, U2); diff --git a/src/supernova/mod.rs b/src/supernova/mod.rs index bc109261f..92df409c0 100644 --- a/src/supernova/mod.rs +++ b/src/supernova/mod.rs @@ -765,7 +765,7 @@ where assert_eq!(self.program_counter, E1::Scalar::from(circuit_index as u64)); // fold the secondary circuit's instance - let nifs_secondary = NIFS::prove_mut( + let (nifs_secondary, _) = NIFS::prove_mut( &*pp.ck_secondary, &pp.ro_consts_secondary, &scalar_as_base::(self.pp_digest), @@ -839,7 +839,7 @@ where ) }; - let nifs_primary = NIFS::prove_mut( + let (nifs_primary, _) = NIFS::prove_mut( &*pp.ck_primary, &pp.ro_consts_primary, &self.pp_digest, diff --git a/src/supernova/snark.rs b/src/supernova/snark.rs index ab7b55c60..b7085858b 100644 --- a/src/supernova/snark.rs +++ b/src/supernova/snark.rs @@ -109,7 +109,7 @@ where &recursive_snark.l_w_secondary, ); - let (nifs_secondary, (f_U_secondary, f_W_secondary)) = res_secondary?; + let (nifs_secondary, (f_U_secondary, f_W_secondary), _) = res_secondary?; // Prepare the list of primary Relaxed R1CS instances (a default instance is provided for // uninitialized circuits)