Onchain decider circuit for Protogalaxy

[winderica]

Following #157 and #162, this PR implements generic on-chain and off-chain decider circuits GenericOnchainDeciderCircuit and GenericOffchainDeciderCircuit{1, 2} that can handle all folding schemes (Nova, HyperNova, and Protogalaxy, hopefully even Mova and Ova in the future).

The abstraction in #157 and #162 provide a unified yet flexible usage of these objects, leading to highly reuseable decider circuits. As an example, we can take a look at the definition and internal logic of GenericOnchainDeciderCircuit below:

sonobe/folding-schemes/src/folding/circuits/decider/on_chain.rs

Lines 64 to 110 in 7add907

	pub struct GenericOnchainDeciderCircuit<
	C1: CurveGroup,
	C2: CurveGroup,
	GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
	RU: CommittedInstanceOps<C1>, // Running instance
	IU: CommittedInstanceOps<C1>, // Incoming instance
	W: WitnessOps<CF1<C1>>, // Witness
	A: Arith<W, RU>, // Constraint system
	AVar: ArithGadget<W::Var, RU::Var>, // In-circuit representation of `A`
	D: DeciderEnabledNIFS<C1, RU, IU, W, A>,
	> {
	pub _gc2: PhantomData<GC2>,
	pub _avar: PhantomData<AVar>,
	/// Constraint system of the Augmented Function circuit
	pub arith: A,
	/// R1CS of the CycleFold circuit
	pub cf_arith: R1CS<CF1<C2>>,
	/// CycleFold PedersenParams over C2
	pub cf_pedersen_params: PedersenParams<C2>,
	pub poseidon_config: PoseidonConfig<CF1<C1>>,
	/// public params hash
	pub pp_hash: CF1<C1>,
	pub i: CF1<C1>,
	/// initial state
	pub z_0: Vec<CF1<C1>>,
	/// current i-th state
	pub z_i: Vec<CF1<C1>>,
	/// Folding scheme instances
	pub U_i: RU,
	pub W_i: W,
	pub u_i: IU,
	pub w_i: W,
	pub U_i1: RU,
	pub W_i1: W,
	/// Helper for folding verification
	pub proof: D::Proof,
	pub randomness: D::Randomness,
	/// CycleFold running instance
	pub cf_U_i: CycleFoldCommittedInstance<C2>,
	pub cf_W_i: CycleFoldWitness<C2>,
	/// KZG challenges
	pub kzg_challenges: Vec<CF1<C1>>,
	pub kzg_evaluations: Vec<CF1<C1>>,
	}

sonobe/folding-schemes/src/folding/circuits/decider/on_chain.rs

Lines 232 to 321 in 7add907

	// 1. enforce `U_{i+1}` and `W_{i+1}` satisfy `arith`
	arith.enforce_relation(&W_i1, &U_i1)?;
	// 2. enforce `u_i` is an incoming instance
	u_i.enforce_incoming()?;
	// 3. u_i.x[0] == H(i, z_0, z_i, U_i), u_i.x[1] == H(cf_U_i)
	let (u_i_x, U_i_vec) = U_i.hash(&sponge, &pp_hash, &i, &z_0, &z_i)?;
	let (cf_u_i_x, _) = cf_U_i.hash(&sponge, pp_hash.clone())?;
	u_i.get_public_inputs().enforce_equal(&[u_i_x, cf_u_i_x])?;
	#[cfg(feature = "light-test")]
	log::warn!("[WARNING]: Running with the 'light-test' feature, skipping the big part of the DeciderEthCircuit.\n Only for testing purposes.");
	// The following two checks (and their respective allocations) are disabled for normal
	// tests since they take several millions of constraints and would take several minutes
	// (and RAM) to run the test. It is active by default, and not active only when
	// 'light-test' feature is used.
	#[cfg(not(feature = "light-test"))]
	{
	// imports here instead of at the top of the file, so we avoid having multiple
	// `#[cfg(not(test))]`
	use crate::{
	arith::r1cs::circuits::R1CSMatricesVar,
	commitment::pedersen::PedersenGadget,
	folding::circuits::{
	cyclefold::CycleFoldWitnessVar, nonnative::uint::NonNativeUintVar,
	},
	};
	use ark_r1cs_std::ToBitsGadget;
	let cf_W_i = CycleFoldWitnessVar::<C2>::new_witness(cs.clone(), || Ok(self.cf_W_i))?;
	// 4. check Pedersen commitments of cf_U_i.{cmE, cmW}
	let H = GC2::constant(self.cf_pedersen_params.h);
	let G = self
	.cf_pedersen_params
	.generators
	.iter()
	.map(|&g| GC2::constant(g.into()))
	.collect::<Vec<_>>();
	let cf_W_i_E_bits = cf_W_i
	.E
	.iter()
	.map(|E_i| E_i.to_bits_le())
	.collect::<Result<Vec<_>, _>>()?;
	let cf_W_i_W_bits = cf_W_i
	.W
	.iter()
	.map(|W_i| W_i.to_bits_be())
	.collect::<Result<Vec<_>, _>>()?;
	PedersenGadget::<C2, GC2>::commit(&H, &G, &cf_W_i_E_bits, &cf_W_i.rE.to_bits_le()?)?
	.enforce_equal(&cf_U_i.cmE)?;
	PedersenGadget::<C2, GC2>::commit(&H, &G, &cf_W_i_W_bits, &cf_W_i.rW.to_bits_le()?)?
	.enforce_equal(&cf_U_i.cmW)?;
	let cf_r1cs = R1CSMatricesVar::<CF1<C2>, NonNativeUintVar<CF2<C2>>>::new_constant(
	ConstraintSystemRef::None,
	self.cf_arith,
	)?;
	// 5. enforce `cf_U_i` and `cf_W_i` satisfy `cf_r1cs`
	cf_r1cs.enforce_relation(&cf_W_i, &cf_U_i)?;
	}
	// 6.1. partially enforce `NIFS.V(U_i, u_i) = U_{i+1}`.
	D::fold_field_elements_gadget(
	&self.arith,
	&mut transcript,
	pp_hash,
	U_i,
	U_i_vec,
	u_i,
	self.proof,
	self.randomness,
	)?
	.enforce_partial_equal(&U_i1)?;
	// 7.1. compute and check KZG challenges
	KZGChallengesGadget::get_challenges_gadget(&mut transcript, &U_i1)?
	.enforce_equal(&kzg_challenges)?;
	// 7.2. check the claimed evaluations
	for (((v, _r), c), e) in W_i1
	.get_openings()
	.iter()
	.zip(&kzg_challenges)
	.zip(&kzg_evaluations)
	{
	// The randomness `_r` is currently not used.
	EvalGadget::evaluate_gadget(v, c)?.enforce_equal(e)?;
	}

With GenericOnchainDeciderCircuit, creating the on-chain decider circuit for Protogalaxy is as simple as giving a type alias and implementing the TryFrom trait:

sonobe/folding-schemes/src/folding/protogalaxy/decider_eth_circuit.rs

Lines 74 to 150 in 7add907

	pub type DeciderEthCircuit<C1, C2, GC2> = GenericOnchainDeciderCircuit<
	C1,
	C2,
	GC2,
	CommittedInstance<C1, RUNNING>,
	CommittedInstance<C1, INCOMING>,
	Witness<CF1<C1>>,
	R1CS<CF1<C1>>,
	R1CSMatricesVar<CF1<C1>, FpVar<CF1<C1>>>,
	DeciderProtoGalaxyGadget,
	>;
	/// returns an instance of the DeciderEthCircuit from the given ProtoGalaxy struct
	impl<
	C1: CurveGroup,
	GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
	C2: CurveGroup,
	GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
	FC: FCircuit<C1::ScalarField>,
	CS1: CommitmentScheme<C1, false>,
	// enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
	CS2: CommitmentScheme<C2, false, ProverParams = PedersenParams<C2>>,
	> TryFrom<ProtoGalaxy<C1, GC1, C2, GC2, FC, CS1, CS2>> for DeciderEthCircuit<C1, C2, GC2>
	where
	CF1<C1>: Absorb,
	{
	type Error = Error;
	fn try_from(protogalaxy: ProtoGalaxy<C1, GC1, C2, GC2, FC, CS1, CS2>) -> Result<Self, Error> {
	let mut transcript = PoseidonSponge::<C1::ScalarField>::new(&protogalaxy.poseidon_config);
	let (U_i1, W_i1, proof, aux) = Folding::prove(
	&mut transcript,
	&protogalaxy.r1cs,
	&protogalaxy.U_i,
	&protogalaxy.W_i,
	&[protogalaxy.u_i.clone()],
	&[protogalaxy.w_i.clone()],
	)?;
	// compute the KZG challenges used as inputs in the circuit
	let kzg_challenges = KZGChallengesGadget::get_challenges_native(&mut transcript, &U_i1);
	// get KZG evals
	let kzg_evaluations = W_i1
	.get_openings()
	.iter()
	.zip(&kzg_challenges)
	.map(|((v, _), &c)| EvalGadget::evaluate_native(v, c))
	.collect::<Result<Vec<_>, _>>()?;
	Ok(Self {
	_gc2: PhantomData,
	_avar: PhantomData,
	arith: protogalaxy.r1cs,
	cf_arith: protogalaxy.cf_r1cs,
	cf_pedersen_params: protogalaxy.cf_cs_params,
	poseidon_config: protogalaxy.poseidon_config,
	pp_hash: protogalaxy.pp_hash,
	i: protogalaxy.i,
	z_0: protogalaxy.z_0,
	z_i: protogalaxy.z_i,
	U_i: protogalaxy.U_i,
	W_i: protogalaxy.W_i,
	u_i: protogalaxy.u_i,
	w_i: protogalaxy.w_i,
	U_i1,
	W_i1,
	proof,
	randomness: aux.L_X_evals,
	cf_U_i: protogalaxy.cf_U_i,
	cf_W_i: protogalaxy.cf_W_i,
	kzg_challenges,
	kzg_evaluations,
	})
	}
	}

Below I list several additional modifications made in this PR:

• A trait EquivalenceGadget that can check the equivalence (equality for native field elements, congruence for non-native field elements) between two in-circuit variables.
• Modified logic of decider circuit. In sonobe docs, the circuit only checks the generation of challenge ( r ), while the rest of NIFS.V is done by the verifier in step 10. In contrast, this PR follows the approach in the DeciderEthCircuit of HyperNova, which verifies the field operations in NIFS.V in-circuit. (Note that in c447906, I mistakenly ignored the group operations in NIFS.V. In fact, these operations are expensive in-circuit and should be handled by the verifier, which is added in 5dc7e5f .)
• Shorter public inputs in decider. Because the field operations in NIFS.V are handled by the circuit, field values in committed instances (e.g., u and x in Nova) are no longer necessary to be public. They are thus removed from public inputs to reduce the verifier's costs. The smart contract for on-chain verification is also updated.
• Simplified trait bounds.

---

P.S. While this PR should already be ready for review, please focus on what you are working on now (such as #133). I don't want to bother the other contributors with merge conflicts due to this huge PR and am happy to rebase at my end after the pending PRs get merged :) Conflicts resolved :)

[arnaucube]

Awesome work!!!! This is really great! 🙌
Big improvements with the abstractions! Great job!

[CPerezz]

LGTM!!!
What a PR. This one might be one of the best ones I've seen in quite some time. Really well documented and with a nice abstraction.

Congrats on this work!!! 🔥

[CPerezz]

Love that you added these types of justifications! <3

[CPerezz]

Not sure I follow exactly how do we have these constraints. COuld you briefly explain? Or refer me to somewhere to get the intuition?

[arnaucube]

@winderica can explain better the specifics in this call, but for context: this comes from Nova impl. The idea was that in the U.hash() call, internally the vector of field elements that represents all the parameters (including points coordinates) of U is computed, and later in other parts of the logic of the decider circuit this vector is needed again. So instead of computing it 2 times (inside the circuit), it is computed once and returned so that it can be reused without needing more constraints later.

[winderica]

Thanks @arnaucube! The use of U_vec here is exactly inspired by CommittedInstanceVarOps::hash.

The reason why reusing U_vec saves constraints, or why recalculating U_vec requires constraints, is due to the implementation of NonNativeUintVar::to_constraint_field.

sonobe/folding-schemes/src/folding/circuits/nonnative/uint.rs

Lines 509 to 521 in 6d8f297

	impl<F: PrimeField> ToConstraintFieldGadget<F> for NonNativeUintVar<F> {
	fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
	let bits_per_limb = F::MODULUS_BIT_SIZE as usize - 1;
	let limbs = self
	.to_bits_le()?
	.chunks(bits_per_limb)
	.map(Boolean::le_bits_to_fp_var)
	.collect::<Result<Vec<_>, _>>()?;
	Ok(limbs)
	}
	}

In a NonNativeUintVar, there are many limbs, and each limb currently stores a FpVar that has a small number of bits (much smaller than the field order) for efficiency of integer operations like addition and multiplication. However, a small number of bits per limb will result in more limbs, and consequently, hashing a NonNativeUintVar will require more rounds of permutations and thus more constraints.

To save the costs of hashing, we convert the limbs of NonNativeUintVar to a compact form in NonNativeUintVar::to_constraint_field, such that each new limb now stores as many bits as possible (i.e., F::MODULUS_BIT_SIZE as usize - 1), and the number of limbs becomes as small as possible. This process introduces constraints because it decomposes all limbs into bits and then recomposes the bits back to FpVars.

By reusing U_vec, we no longer need to call NonNativeUintVar::to_constraint_field multiple times, thus saving constraints.

Having said that, I think it is possible to avoid constraints in NonNativeUintVar::to_constraint_field while producing short hash preimages. To this end, we do not decompose and recompose limbs. Instead, we directly compose several limbs into one via linear combination, which does not introduce any constraints. Although the number of bits in each new limb is unlikely to be the optimal value F::MODULUS_BIT_SIZE as usize - 1, the number of limbs should still be pretty short. In this way, converting U to FpVars becomes nearly free, and we may remove U_vec in favor of a user friendlier API.

[CPerezz]

This forces us to always use Cyclefold I assume right? Not that I'm against it. But would be nice to maybe mention somewhere that "vanilla Nova" isn't supported.

[arnaucube]

This has been like this since Sonobe was started, always Nova+CycleFold (in all combinations (onchain&offchain deciders, also in the IVC without deciders)), also for HyperNova & ProtoGalaxy, both using CycleFold.

I mean, is not that this specific new line forces to use CycleFold instead of 'vanilla Nova', but that the entire project is around CycleFold.
Not sure if adding a comment in this line would make it clearer, it appears in the docs & readme, and in many comments along the code.

[winderica]

Do you think it is a good idea to rename the circuit to something like CycleFoldBasedOnchainDeciderCircuit? The point is, when someone propose a new paradigm for converting folding schemes to IVC, we can implement the corresponding decider circuit for all folding schemes, and the user can choose the best decider circuit for their use case.

[arnaucube]

Maybe once that new paradigm appears and it is implemented we can then rename the current method if needed, but in general I try to not abstract in advance, like for the moment this struct is the only possibility in the code, and it's mentioned in the comments that it is cyclefold-based. On the current code we would be only making the name of the struct longer while not distinguishing from another struct since it would not exist yet.
If at some point we add another alternative to the OnchainDeciderCircuit that is not based on the CycleFold approach, then agree that renaming it into this name is what would make sense.

How do you see it? maybe I'm missing some part of the point, and at the end making the name longer would not be a problem neither, so if you think it makes more sense I'm happy with it too, but with the info at hand seems that it would not make things clearer or help to distinguish from other cases.

[winderica]

Agreed! I am neither a big fan of premature abstraction, so let's keep the name as is until a new scheme is proposed :)