Sumcheck circuit #28

arnaucube · 2023-07-10T22:27:00Z

Add SumCheck verification r1cs-bellperson gadget.

This PR:

add gadget for univariate polynomial evaluation
add gadget for sumcheck verification
add sumcheck prover for a single multivariate polynomial on Spartan submodule
- this is used in the gadget test, but in the future can be used by the multifolding prover

To do after this PR:

add gadget for the transcript compatible with the rust-native transcript from Nova codebase ( Implement Transcript bellperson gadget #27 )
ask for some bellman/bellperson knowledgable person for input on the gadgets constraints handling

once the transcript gadget is ready, we can then compare the number of constraints with the arkworks sumcheck-verify gadget number of constraints.

resolves #25

asn-d6

I don't know much bellman so my review is not very useful I'm afraid... I left a few comments though!

asn-d6 · 2023-07-11T09:09:27Z

src/gadgets/sumcheck.rs

+    );
+    eval = eval_aux;
+  }
+  let allocated_eval: AllocatedNum<Scalar> =


Can you use the allocated_eval from the loop above here? Or do you need to reallocate?

The allocated_eval from the loop before has a different value than the eval once the loop ends. But we can use allocated_eval_aux which has the desired value, although then the code gets a bit less clear.
Added this change in the next commit among other updates related to the comments.

asn-d6 · 2023-07-11T09:10:44Z

src/gadgets/sumcheck.rs

+{
+  let mut eval: Num<Scalar> = Num::<Scalar>::from(coeffs[0].clone());
+  let mut power = r.clone();
+  for (i, coeff) in coeffs.iter().enumerate().skip(1) {


These functions get quite complicated even though they are supposed to be doing simple things. This might just be how bellman is, or maybe you can define two helper methods here?

For example one could be multiply_and_add() and the other would be multiply_with_r() and both of them would return their aux variable? This way you could simplify this func, and you could also separately test the helper functions as well?

asn-d6 · 2023-07-11T09:11:38Z

src/gadgets/sumcheck.rs

+    assert_eq!(res.get_value().unwrap(), p.evaluate(&r));
+
+    let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &ck).unwrap();
+    assert!(shape.is_sat(&ck, &inst, &witness).is_ok());


How can we have some basic negative tests here, to make sure that not everything is satisfied?
Can we make a shape that is obviously not satisfied and then check that it is indeed not satisfied?

The uni_evaluate gadget does not check that two inputs satisfy the checks, it internally computes the evaluation of the univariate polynomial and outputs the result, while internally adding constraints for the operations of the evaluation.
But there is no 'wrong inputs' for that, what we can check is that the output of the gadget is the expected result of the evaluation (which is what the test does).

Is like a gadget that we can name "add" that outputs the result of a + b, we can not input 'wrong' values that will not satisfy the shape, as it is just computing a+b and adding a constraint that ensures that the output is equal to a+b, but to test that gadget we can instanciate it and assert that the outputted value is the expected one.

asn-d6 · 2023-07-11T09:15:02Z

src/gadgets/sumcheck.rs

+  use crate::spartan::polynomial::MultilinearPolynomial;
+  use crate::spartan::sumcheck::SumcheckProof;
+
+  fn synthetize_uni_evaluate<Scalar, CS>(


What is the role of this function? Are the commented stuff needed?

The role is the same as in other synthesize_ methods in the tests of other gadgets such as
https://github.com/privacy-scaling-explorations/Nova/tree/b53229d07c50cd135006b319995bd29799cfc2e7/src/gadgets/ecc.rs#L1020
which is to prepare the inputs and run the gadget, which is later used in the test first to get the r1cs shape, and after that to run the gadget with real values, getting it's output.

The commented stuff will not be needed, leaving it for the moment meanwhile the PR is in draft mode, in order to check stuff while the PR is in progress.

Note about typo: in the sumcheck.rs code the word synthetize should be synthesize as in the rest of methods with that word in the other Nova files, I'll update this in the next commit.

oskarth

Nice one! Would it be possible to include some reference comments in the code to what you are basing the the algorithms etc on? It'd make it easier to check for correctness and to better understand the flow. E.g. if it is HyperNova paper, or Thaler book, or anything else used as a reference.

CPerezz

First pass.

CPerezz · 2023-07-14T09:29:52Z

src/gadgets/sumcheck.rs

+    );
+    eval = eval_aux;
+  }
+  let allocated_eval: AllocatedNum<Scalar> =


Can't you copy constrain the value at least? So that there's no way to cheat values here?

What do you mean by 'copy constrain'? (in the context of R1CS)

What I mean is that we need a way to ensure that the inner loop allocated value is the same as the one created later.
Otherwise, there's an equality not being checked.

src/gadgets/sumcheck.rs

CPerezz · 2023-07-14T09:32:31Z

src/gadgets/sumcheck.rs

+  let allocated_eval: AllocatedNum<Scalar> =
+    AllocatedNum::<Scalar>::alloc(&mut cs, || Ok(eval.get_value().unwrap()))?;


Same here. Can't you copy constrain this? Otherwise it looks like there's nothing that constraints this.

src/gadgets/sumcheck.rs

CPerezz · 2023-07-14T09:33:32Z

src/lib.rs

@@ -5,7 +5,7 @@
  future_incompatible,
  nonstandard_style,
  rust_2018_idioms,
-  missing_docs
+  // missing_docs


I'd re-enable this and add all the required comments before merging.

src/spartan/sumcheck.rs

spartan::SumCheckProof's didn't had a generic prover, added its implementation to be used for the sumcheck-verifier-circuit tests and probably for the HyperNova's Multifolding step 3.

Add test to SumCheck verify gadget, for the SumCheck example of g(X_0, X_1, X_2) = 2 X_0^3 + X_0 X_2 + X_1 X_2.

oskarth · 2023-07-28T07:18:55Z

src/gadgets/sumcheck.rs

@@ -0,0 +1,336 @@
+#![allow(unused)]


Can we add some basic documentation to this gadget?

yes, agree. @CPerezz also mentioned it (#28 (comment)) and is planned once the impl is more solid (and before removing it's draft status).

hero78119 · 2023-09-06T08:15:50Z

Hi @arnaucube
Recently I wrote up a tricks which aim to solve lookup scheme under R1CS in pretty low cost way.
which leverages sumcheck verifier as a circuit in the end compression snark stage.

Notice you implemente sumcheck verify circuit in r1cs-bellperson, may I know your following up plan, such like do you plan to upstream this feature to Nova repo or not and when?

arnaucube · 2023-09-06T16:58:00Z

Hi @hero78119 , so this was a line of work started with the objective to end up having the HyperNova multifolding verifier in-circuit, but recently we stopped that line of work.
We're working on an arkworks-based implementation of it, so no plans to upstream this SumCheck verify circuit. But feel free to reuse it ^^
I'll DM you to be in touch regarding this and future stuff regarding the arkworks-based folding library.

…rivacy-scaling-explorations#28) - Modified `SuperNovaAugmentedCircuitParams` to be passed by reference in `test_recursive_circuit_with` function and associated instances in `test.rs`. - Updated `SuperNovaAugmentedCircuit::new` method to match changes in the `test_recursive_circuit_with` function. - Revamped arguments handling in `synthesize_non_base_case` and `synthesize` functions in `circuit.rs`, changing from owned types to references to reduce unnecessary cloning. - Altered function body to accommodate the changes for referenced values in `circuit.rs`.

arnaucube marked this pull request as draft July 10, 2023 22:27

oskarth force-pushed the hypernova branch from 87391af to af959fb Compare July 11, 2023 05:23

arnaucube requested review from oskarth, asn-d6 and CPerezz July 11, 2023 05:41

asn-d6 reviewed Jul 11, 2023

View reviewed changes

arnaucube force-pushed the sumcheck-circuit branch from 103b1d6 to 8183971 Compare July 11, 2023 12:08

oskarth reviewed Jul 12, 2023

View reviewed changes

Base automatically changed from hypernova to main July 12, 2023 10:22

arnaucube force-pushed the sumcheck-circuit branch from 8183971 to b53229d Compare July 12, 2023 10:41

CPerezz requested changes Jul 14, 2023

View reviewed changes

arnaucube force-pushed the sumcheck-circuit branch 2 times, most recently from a6fe8d7 to 49f38d9 Compare July 17, 2023 08:29

arnaucube added 7 commits July 20, 2023 09:39

Add gadget: uni_evaluate, with test

6103fa2

start sumcheck verify circuit (without test & constraint checks)

09d4cbb

add SumCheck prove method for a single polynomial

b29b2d7

spartan::SumCheckProof's didn't had a generic prover, added its implementation to be used for the sumcheck-verifier-circuit tests and probably for the HyperNova's Multifolding step 3.

Add SumCheck verify gadget test

8394407

Add test to SumCheck verify gadget, for the SumCheck example of g(X_0, X_1, X_2) = 2 X_0^3 + X_0 X_2 + X_1 X_2.

add {gadgets,spartan}/sumcheck random values test

32d2081

gadgets/sumcheck add pending cs.enforce

862113e

updates after PR reviews

4b5a606

arnaucube force-pushed the sumcheck-circuit branch from 49f38d9 to 4b5a606 Compare July 20, 2023 07:44

oskarth reviewed Jul 28, 2023

View reviewed changes

oskarth mentioned this pull request Aug 21, 2023

Add initial experimental HyperNova multifolding support microsoft/Nova#175

Draft

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sumcheck circuit #28

Sumcheck circuit #28

arnaucube commented Jul 10, 2023 •

edited

Loading

asn-d6 left a comment

asn-d6 Jul 11, 2023

arnaucube Jul 14, 2023

asn-d6 Jul 11, 2023

asn-d6 Jul 11, 2023

arnaucube Jul 14, 2023

asn-d6 Jul 11, 2023

arnaucube Jul 14, 2023 •

edited

Loading

oskarth left a comment

CPerezz left a comment

CPerezz Jul 14, 2023

arnaucube Jul 14, 2023

CPerezz Jul 17, 2023

CPerezz Jul 14, 2023

CPerezz Jul 14, 2023

arnaucube Jul 14, 2023

oskarth Jul 28, 2023

arnaucube Jul 28, 2023 •

edited

Loading

hero78119 commented Sep 6, 2023

arnaucube commented Sep 6, 2023

		let allocated_eval: AllocatedNum<Scalar> =
		AllocatedNum::<Scalar>::alloc(&mut cs, \|\| Ok(eval.get_value().unwrap()))?;

Sumcheck circuit #28

Are you sure you want to change the base?

Sumcheck circuit #28

Conversation

arnaucube commented Jul 10, 2023 • edited Loading

asn-d6 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arnaucube Jul 14, 2023 • edited Loading

Choose a reason for hiding this comment

oskarth left a comment

Choose a reason for hiding this comment

CPerezz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arnaucube Jul 28, 2023 • edited Loading

Choose a reason for hiding this comment

hero78119 commented Sep 6, 2023

arnaucube commented Sep 6, 2023

arnaucube commented Jul 10, 2023 •

edited

Loading

arnaucube Jul 14, 2023 •

edited

Loading

arnaucube Jul 28, 2023 •

edited

Loading