feat: implement SuperNova #283

huitseeker · 2023-12-18T22:43:44Z

What's in this PR?

This implements Supernova, allowing:

a 'pay-as-you-go' cost structure for folding operations, through the SuperNova folding scheme,
a final SNARK that efficiently compresses an instance of this folded proof, through batching techniques.

This is the work of a team including @adr1anh @hero78119 @mpenciak @porcuquine @samuelburnham @winston-h-zhang and @wyattbenno777 .

We're of course happy to receive feedback on this PR.

References:

the blog post goes into our construction, and links where relevant to two more specialized notes on the CompressedSNARK for Supernova along with our variant of the public input padding issue.
the Readme at src/supernova/Readme.md

Provenance

This backports a number of Arecibo PRs (click for a list)

srinathsetty · 2024-01-02T19:33:19Z

Hi! Thank you very much for creating this PR!

This is a very large PR (which is understandable), but it combines many unrelated improvements. Since we use "squash merge", it will make it hard to audit the history of the code.

So, I've some high-level suggestions to make this PR easy to review and keep the history in an easy-to-audit state. I'll make more suggestions to split this PR into multiple pieces as I look through all the different improvements. Here is one I can that is immediate:

code to check that W is appropriately padded with zeros instead of making two calls to EvaluationArgument in ppsnark.

This change is clearly independent of the SuperNova feature.

Are there other such features here? How about sum-check related changes?

Cargo.toml

huitseeker · 2024-01-03T14:34:27Z

I have:

rebased the changes on the latest master, thereby incorporating the NovaError type changes from Improve error handling #286 into the SuperNovaError type,
removed the erroneous import of the pairing library (sorry),
removed the changes to the ppsnark introduced by apply bound witness fix to ppsnark argumentcomputer/arecibo#182,

The changes to the sumcheck are an integral part of the batched_ppsnark construction, which is used in the CompressedSNARK for Supernova. In fact, the WitnessBoundSumCheck instance was, in Arecibo, built for Supernova first, and then ported to the Nova ppsnark.

Cargo.toml

src/spartan/polys/masked_eq.rs

srinathsetty · 2024-01-03T18:16:35Z

Thanks for pulling out the changes to reduce the scope of this PR!

It still seems like masked eq polynomial should be part of a predecessor PR that introduces more efficient bound checks on W polynomial. Would it make sense to get that PR created and merged before we review this further?

I also have some general suggestions: can we move all the supernova related files (e.g., circuit_supernova.rs) and changes (additional traits) into the supernova module? This will ensure that supernova related code is contained in a centralized place that one does not need when using just Nova. This will also help audit/review changes to core Nova made as part of this PR, in support of SuperNova.

src/lib.rs

src/r1cs/mod.rs

src/spartan/macros.rs

srinathsetty · 2024-01-04T18:44:45Z

src/spartan/polys/eq.rs

 pub struct EqPolynomial<Scalar: PrimeField> {
-  r: Vec<Scalar>,
+  pub(in crate::spartan::polys) r: Vec<Scalar>,


Is there reason to make r visible?

MaskedEq has an access to those scalars that doesn't exactly match an evaluation. And you can look at evals_from_points which has allowed us to save a ton of allocations:
argumentcomputer/arecibo@13773b9

src/spartan/polys/eq.rs

srinathsetty · 2024-01-04T18:48:59Z

src/spartan/ppsnark.rs

-  val_A: Vec<E::Scalar>,
-  val_B: Vec<E::Scalar>,
-  val_C: Vec<E::Scalar>,
+  pub(in crate::spartan) row: Vec<E::Scalar>,


Why do these fields need to be made visible within spartan module?

The batched_ppsnark, which is the batched variant of this file, needs access to the fields in order to construct sumcheck instances and evaluations (similarly to what ppsnark itself does).

src/spartan/ppsnark.rs

src/spartan/snark.rs

src/supernova/Readme.md

srinathsetty · 2024-01-04T19:00:32Z

src/supernova/utils.rs

@@ -0,0 +1,179 @@
+use bellpepper_core::{


Nit: If this is used only from the supernova circuit, it would make sense to make circuit_supernova.rs a module and then put this file inside that module.

src/traits/circuit_supernova.rs

srinathsetty · 2024-01-04T19:01:47Z

src/traits/snark.rs

@@ -55,6 +55,43 @@ pub trait RelaxedR1CSSNARKTrait<E: Engine>:
  fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<E>) -> Result<(), NovaError>;
 }

+/// A trait that defines the behavior of a `zkSNARK` to prove knowledge of satisfying witness to batches of relaxed R1CS instances.


Nit: It likely makes sense to move this trait inside the supernova module.

I remark that the two instances are not in the Supernova module, so I would need to move at least their implementation of the trait to the Supernova module.

Specifically, considering that snark and ppsnark are, respectively, instances of batched_snark and batched_ppsnark at batch_length = 1, the later could subsume the former.

This gathers the changes to the pre-processing SNARK excerpted from the Supernova implementation in PR microsoft#283. The main changes extracted here are the introduction of the masked eq polynomial (and its use fixing [this issue](https://hackmd.io/@adr1anh/Sy08YaVBa)), additional sum-check tooling, removal of two calls to evaluation argument. Main reference Arecibo PRs: - argumentcomputer/arecibo#106 - argumentcomputer/arecibo#131 - argumentcomputer/arecibo#174 - argumentcomputer/arecibo#182 - Enhancement of polynomial related code in Spartan protocol including new polynomial types, modified existing types, better evaluation methods, and improved polynomial operations. - Introduction of `squares` function and change in the generation of `t_pow` in Spartan. - Addition of a new polynomial type through `MaskedEqPolynomial` with methods for its creation and evaluation. - Enhancements in `UniPoly` struct by addition of `PartialEq`, and `Eq` traits. - Improvements in `snark.rs` for proving and verifying batch evaluation claims, leveraging `gamma` and `rho` for random linear combinations, and optimizing various variable computations. - Updates in `multilinear.rs` with refactoring, optimization, error handling, and supplementing unit tests. - Refactor in `spartan/mod.rs` with import updates, function overhauls, struct visibility changes, and asynchronous operations for efficient calculations. - Additions and amendments in `sumcheck.rs` for batch verification, handling of vectors of claims, handling of cubic bounds with additive terms, visibility adjustments, and typo fixes. - Modifications in `eq.rs` including a debug derive for `EqPolynomial`, enhanced visibility of `r` vector, provision of `evals_from_points` for enhanced evaluation, and addition of `FromIterator` implementation. Co-authored-by: porcuquine <[email protected]> Co-authored-by: Matej Penciak <[email protected]> Co-authored-by: Adrian Hamelink <[email protected]>

…ns (#293) This gathers the changes to the pre-processing SNARK excerpted from the Supernova implementation in PR #283. The main changes extracted here are the introduction of the masked eq polynomial (and its use fixing [this issue](https://hackmd.io/@adr1anh/Sy08YaVBa)), additional sum-check tooling, removal of two calls to evaluation argument. Main reference Arecibo PRs: - argumentcomputer/arecibo#106 - argumentcomputer/arecibo#131 - argumentcomputer/arecibo#174 - argumentcomputer/arecibo#182 - Enhancement of polynomial related code in Spartan protocol including new polynomial types, modified existing types, better evaluation methods, and improved polynomial operations. - Introduction of `squares` function and change in the generation of `t_pow` in Spartan. - Addition of a new polynomial type through `MaskedEqPolynomial` with methods for its creation and evaluation. - Enhancements in `UniPoly` struct by addition of `PartialEq`, and `Eq` traits. - Improvements in `snark.rs` for proving and verifying batch evaluation claims, leveraging `gamma` and `rho` for random linear combinations, and optimizing various variable computations. - Updates in `multilinear.rs` with refactoring, optimization, error handling, and supplementing unit tests. - Refactor in `spartan/mod.rs` with import updates, function overhauls, struct visibility changes, and asynchronous operations for efficient calculations. - Additions and amendments in `sumcheck.rs` for batch verification, handling of vectors of claims, handling of cubic bounds with additive terms, visibility adjustments, and typo fixes. - Modifications in `eq.rs` including a debug derive for `EqPolynomial`, enhanced visibility of `r` vector, provision of `evals_from_points` for enhanced evaluation, and addition of `FromIterator` implementation. Co-authored-by: porcuquine <[email protected]> Co-authored-by: Matej Penciak <[email protected]> Co-authored-by: Adrian Hamelink <[email protected]>

srinathsetty · 2024-01-24T01:47:55Z

@huitseeker This branch needs to be rebased with main right? It looks like some of the code in here was merged with your recent PR.

* refactor: move mlkzg -> hyperkzg * refactor: Refactor HyperKZG comments This is a port of the following upstream PRs: - microsoft#299 - microsoft#300 * refactor: Refactor engine and testing parameters in pcs.rs - in the IPA Evaluation Engine, transitioning from GrumpkinEngine to Bn256Engine, - avoids noise due to field arithmetic differences

TL;DR: splits off one major source of diff lines from PR microsoft#283. Inherently, there are many R1CS shapes to consider when tailoring public parameter creation to non-uniform step-circuits. However, the commitment key generation should only be done once for all circuits (once a suitable size has been determined by looking at all R1CS shapes). This splits the relevant Nova functions into `r1cs_shape_and_key`, `r1cs_shape` and `commitment_key` to enable the flexibility deamnded by the above model. In detail: - Renamed the `r1cs_shape` method across various files to `r1cs_shape_and_key`, indicating its functionality is to return both `R1CSShape` and `CommitmentKey`. - Altered function calls from `r1cs_shape` to `r1cs_shape_and_key` in files such as `direct.rs`, `nifs.rs`, `lib.rs` and `circuit.rs`, - Split the creation of `R1CSShape` and `CommitmentKey` into separate functions in the `NovaShape` object in `r1cs.rs` - Removed the `R1CS` struct in `mod.rs` as it only contained a phantom data, with related operations performed elsewhere. - Implemented changes to enhance code readability, including the addition of a new `commitment_key_size` function, and overall code reformatting for clarity.

- removing public modifier in src/spartan/ppsnark.rs - removing public modifier in src/spartan/sumcheck/mod.rs - removing public modifier in src/spartan/mod.rs - removing public modifier in src/spartan/polys/masked_eq.rs - removing public modifier in src/supernova/mod.rs

* Refactor 'CircuitShape' references to 'R1CSWithArity' - Implemented terminology update: all occurrences of `CircuitShape` have been replaced with `R1CSWithArity` - Corrected method return descriptions to reflect changes in terminology - Amended related notes and comments to maintain consistency and clarity in the codebase. Leftover from argumentcomputer/arecibo#235 * Fix Supernova module documentation and code comments - Update comments for struct `PublicParams` in `mod.rs` to reflect the correct association with `R1CSWithArity`. - Alter codeblock tag in `Readme.md` from `ignore` to `text`. - Revise mathematical formula in `Readme.md` for the current iteration of $F$ by including brackets around `0` in the base case inputs.

srinathsetty reviewed Jan 2, 2024

View reviewed changes

Cargo.toml Outdated Show resolved Hide resolved

huitseeker force-pushed the supernova_upstream branch from b56a3eb to c5196fc Compare January 3, 2024 14:28

srinathsetty reviewed Jan 3, 2024

View reviewed changes

Cargo.toml Outdated Show resolved Hide resolved

srinathsetty reviewed Jan 3, 2024

View reviewed changes

src/spartan/polys/masked_eq.rs Outdated Show resolved Hide resolved