CycleFold #273

mpenciak · 2024-01-19T04:35:11Z

This PR is a WIP for CycleFolding with Nova IVC.

TODO:

~~Incorporate the changes from Remove absorbing of running instance microsoft/Nova#291 in this RecursiveSNARK implementation~~ (The same assumptions in this PR do not hold for the CycleFold folding, so it would be unsound to include these changes)
~~Incorporate the changes from move fold step from CompressedSNARK to RecursiveSNARK microsoft/Nova#295 in this RecursiveSNARK implementation~~

…ims (Arecibo backport) (argumentcomputer#273) * `snark.rs`: factor out batch evaluation Sumcheck (argumentcomputer#106) * Factor batch eval * Comments * refactor: Remove nedless pass-by-value instances, turn on clippy (argumentcomputer#122) * refactor: Remove nedless pass-by-value instances, turn on the corresponding clippy lint - Updated function parameters in `ppsnark.rs` and `snark.rs` from `Vec<G::Scalar>` to `&[G::Scalar]` (introduced in argumentcomputer#106), - Modified the `prove` function in `ppsnark.rs` to also convert `T_row`, `W_row`, `T_col`, and `W_col` from `Vec` to slices (`&[G::Scalar]`). - Enhanced the `xclippy` alias in `.cargo/config` by adding `-Wclippy::checked_conversions`, `-Wclippy::needless_pass_by_value`, and `-Wclippy::unnecessary_mut_passed` and reorganizing its elements. * `PolyEval{Instance, Witness}::pad` Accept `Vec` rather that `&[T]` to avoid copies Co-authored-by: Francois Garillot <francois@garillot.net> --------- Co-authored-by: Adrian Hamelink <adrian@hamelink.com> --------- Co-authored-by: Adrian Hamelink <adrian.hamelink@gmail.com> Co-authored-by: Adrian Hamelink <adrian@hamelink.com>

src/cyclefold/circuit.rs

src/cyclefold/gadgets.rs

src/gadgets/nonnative/bignat.rs

adr1anh

First batch of comments

src/cyclefold/circuit.rs

src/cyclefold/gadgets.rs

adr1anh · 2024-02-12T13:07:06Z

src/cyclefold/gadgets.rs

+  use ff::Field;
+
+  #[derive(Clone)]
+  pub struct AllocatedPoint<E>


I think we should avoid the is_infinity bit here. In order to properly constrain it, we need to evaluate the curve equation non-natively which will be very expensive. Instead, (and if the properties of the curve allow), we could define (0,0) as the identity and let the CycleFold circuit check that this holds.

src/gadgets/nonnative/bignat.rs

src/cyclefold/nova_circuit.rs

src/cyclefold/circuit.rs

src/cyclefold/gadgets.rs

src/cyclefold/circuit.rs

src/cyclefold/gadgets.rs

src/cyclefold/circuit.rs

src/cyclefold/gadgets.rs

wyattbenno777 · 2024-03-06T20:28:45Z

What would you say the best test against this would be for Nova vs ParaNova?

test_ivc_nontrivial_with vs test_trivial_cyclefold_prove_verify_with?

mpenciak · 2024-03-06T22:00:08Z

What would you say the best test against this would be for Nova vs ParaNova?

test_ivc_nontrivial_with vs test_trivial_cyclefold_prove_verify_with?

I would say those two tests are the most comparable.

But a word of warning: The current folding circuit is not in its final state. I'm nearing the end of a re-work for the way the public IO for the CycleFold circuit is dealt with. Right now the primary folding circuit has ~80k constraints, which is largely coming from the fact that the CycleFold IO has arity 16 (5 per commitment + 1 scalar). This will make the CycleFold circuit moderately larger (up to ~2k constraints), but significantly reduce the size of the folding circuit (numbers TBD soon).

Hopefully in the next day or so these updates will be pushed and there can be a more fair comparison.

Also fix CycleFold folding soundness issue by absorbing running instance

mpenciak · 2024-03-08T00:12:34Z

What would you say the best test against this would be for Nova vs ParaNova?

test_ivc_nontrivial_with vs test_trivial_cyclefold_prove_verify_with?

Just a quick update: I just finished the IO refactor, so the comparison should be more fair now.

src/gadgets/nonnative/util.rs

src/gadgets/r1cs.rs

src/nifs.rs

src/circuit.rs

src/supernova/circuit.rs

huitseeker · 2024-03-19T15:11:34Z

src/cyclefold/gadgets.rs

+  pub fn apply_fold<CS>(
+    &self,
+    mut cs: CS,
+    params: &AllocatedNum<E::Base>,
+    ro_consts: ROConstantsCircuit<E>,
+    limb_width: usize,
+    n_limbs: usize,
+  ) -> Result<AllocatedRelaxedR1CSInstance<E, NIO_CYCLE_FOLD>, SynthesisError>
+  where
+    CS: ConstraintSystem<E::Base>,


This really looks like crate::gadgets::r1cs::fold_with_r1cs with a different RO setup.
It would be good to refactor the common part in an auxiliary function and call it from both places.

huitseeker · 2024-03-19T15:17:32Z

src/cyclefold/nifs.rs

+impl<E: Engine> CycleFoldNIFS<E> {
+  /// 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(


This really looks, like crate::nifs::NIFS::prove with a different RO setup and internal fold function. Would it be possible to have a trait implemented differently for NIFS / CycleFoldNIFS for the RO setup & fold, and then have prove defined in a general way as an extension method which code should be shared between the two instances of the trait?

We don't have an instance of prove_mut here, which is key to performance (see Acceleration of SpMVM in folding #75). It would be good to implement it, and solving (1.) above would be key to doing this without too much extra work.

huitseeker · 2024-03-19T15:32:24Z

src/cyclefold/nova_circuit.rs

+    Ok((U_c, U_p, checks_pass))
+  }
+
+  pub fn synthesize<CS: ConstraintSystem<<E1 as Engine>::Base>>(


This really looks like crate::circuit::NovaAugmentedCircuit::synthesize, perhaps unsurprisingly because most of the differences are in some setup functions, as well as in the auxiliary functions (alloc_witnesses, synthesize_base_case, synthesize_non_base_case).

Here the reason you're duplicating most of the synthesize code is because in one case you want to route to the CycleFold methods, and in the other you want to route to the Nova methods.

You could instead put those three method signatures in a trait, have them implemented in different ways in each of the Nova/CycleFold circuit, and then have the top-level synthesize defined generically for all implementers of the trait?

huitseeker

I've created #375 for the code duplication. THis looks great, thank you so much!

mpenciak · 2024-03-22T19:38:11Z

I've created #375 for the code duplication. THis looks great, thank you so much!

Thanks!

mpenciak force-pushed the cyclefold_new branch from 7243360 to 6088d31 Compare January 23, 2024 20:13

mpenciak force-pushed the cyclefold_new branch from 3a4137a to 4dac5e0 Compare February 5, 2024 22:11