Refactor to allow non-determinisim. #76

porcuquine · 2022-05-24T01:36:29Z

This PR refactors proving in a number of ways. At least some of these changes are necessary to support determinism in the computation of F. The existing code didn't allow this, since compute was always called on the same circuit prototype contained in the public parameters.

separate circuit/output computation and synthesis into two traits
at the lowest level, support caller-controlled stepping of the proof
for convenience, allow caller to provide iterators yielding successive outputs and (un-synthesized) circuits
most simply, and consistent with current implementation, automatically create such iterators when ComputeStep is implemented

This change also makes num_steps optional, and the state accumulated in a RecursiveSNARK tracks the actual number of steps used. This allows for applications where the number of steps is not known in advance.

It's likely that further small changes may be needed when integrating downstream consumers who will need this functionality, but until integration happens, it is difficult to anticipate what that may entail beyond my best guesses here.

NOTE: in the future, we should support a recursive proof which does not expose the number of steps. This will be important for applications in which knowing the number of steps required to compute a final result leaks information. Having the option to generate proofs without revealing the number of steps will eliminate effective 'timing attacks' on such applications.

UPDATE: I added support for non-unary functions, building on the first part. I know that makes this a fairly large PR, but I had to rework a fair amount of the foundation to get here.

The basic idea is that for higher-arity functions, the implementer should implement methods (compute_inner and synthesize_step_inner, which operate on and return a vector of scalars. The goal was to make the actual mechanism as hidden from the caller/user as possible, but some leakage was unavoidable so far.

Under the hood, at each step, the inputs are hashed to get the true unary input for the step function, F — and the outputs are again hashed to produce the unary output. Both hashes are proved in the circuit.

Because we need to avoid storing the initial input (Z0) in the public parameters, it's necessary to first create an 'empty' input used to generate the R1CS shape. That means the caller does (unfortunately) have to create the poseidon constants for the relevant scalar and arity. This is not especially difficult, but it would be nicer if it could have been avoided. This wart means that the constants are generated twice in this case. With more machinery, the public parameters and IO enum could be more symbiotic, but for now I think this is a reasonable tradeoff.

src/traits.rs

src/lib.rs

srinathsetty · 2022-05-24T11:32:54Z

src/lib.rs

      <G1 as Group>::Scalar::one(),
      <G2 as Group>::Scalar::zero(),
    );
    assert!(res.is_ok());
    let recursive_snark = res.unwrap();

+    assert_eq!(num_steps, recursive_snark.num_steps);


Same comment as above.

srinathsetty · 2022-05-24T11:34:57Z

Thanks, @porcuquine for the PR! I left some preliminary comments.

Given the focus is to allow non-determinism, could we add/extend one of the tests to include some non-deterministic step function (as a sanity check and to demonstrate the use of public APIs)?

porcuquine · 2022-05-24T17:10:58Z

Given the focus is to allow non-determinism, could we add/extend one of the tests to include some non-deterministic step function (as a sanity check and to demonstrate the use of public APIs)?

Yes, that was my next plan. I'll put something together and push it soon.

porcuquine · 2022-05-25T01:57:02Z

Okay, I added a test exercising the new procedure by precomputing nondeterministic hints and storing them in the circuit. I needed to tweak the implementation a little to make this work (so the test was especially useful!). This also revealed that the concrete circuits never needed to stored in the RecursiveSNARK, so I removed.

src/poseidon.rs

src/lib.rs

porcuquine · 2022-05-27T05:31:39Z

src/lib.rs

+    let pp =
+      PublicParams::<G1, G2, TrivialTestCircuit<S1>, CubicIncrementingCircuit<S2>, U1, U2>::setup(
+        TrivialTestCircuit::default(),
+        CubicIncrementingCircuit::new(IO::Empty(&p)),


The PoseidonConstants are used here, in the blank/empty circuit.

src/lib.rs

srinathsetty · 2022-05-27T07:59:09Z

src/lib.rs

  ) -> Result<Self, NovaError> {
-    if num_steps == 0 {


How do we handle this case without this code in the new version?

The error will be returned if an iterator has no first item: https://github.com/microsoft/Nova/pull/76/files/3986df4f2c580d49f449f84ab84c02eb0db1668b#diff-b1a35a68f14e696205874893c07fd24fdb88882b47c23cc0e0c80a30c7d53759R394-R401

src/lib.rs

srinathsetty · 2022-05-27T08:03:28Z

src/traits.rs

+  }
+}
+
+/// A helper trait for computing a step of the incremental computation (i.e., F itself)


Is there a (fundamental) reason to have two traits since it seems like we end up implementing both StepCompute and StepCircuit on the same types right?

Yes, a caller might want more control, in which case they can implement Iterator directly. This will bypass the iterator automatically created using ComputeStep. That is also why prove_with_iterators is public. When the caller implements an iterator, they can bypass prove and call the lower-level function.

srinathsetty · 2022-05-27T08:18:13Z

src/lib.rs

  params_primary: NIFSVerifierCircuitParams,
  params_secondary: NIFSVerifierCircuitParams,
+  c_primary: C1,
+  c_secondary: C2,
+  a1: Option<PoseidonConstants<<G1 as Group>::Scalar, A1>>,


I think we should be using ROConstants instead of PoseidonConstants (there was a TODO at the top of the file to completely avoid including poseidon.rs from lib.rs). In the short term, if the goal is to support a few arities of interest (e.g., 2 for VDFs and 6 for Lurk), could we just add those aritites to the hard-coded constants that we generate? This will likely avoid a lot of complexity. What do you think?

We could then make implementations of ROConstants be able to handle arbitrary arities via the sponge construction.

I agree with you on the general topology, and I have pushed a commit which I think finally addresses the issues. I moved the arity poseidon constants into the verifier circuit. I didn't put them in ROConstants directly for several related reasons:

If we retain generality, that would require putting an Arity type parameter everywhere, including places it didn't belong.

If we discard generality, it would actually have added a lot of complexity and cost around 'dynamic allocation' of specific constants.

They're not really part of the RO anyway. As implemented here, they're a helper for the application function F.

In any case, my recent commit now successfully hides the PoseidonConstants from the caller almost completely. In the case that a caller wants to implement the ComputeStep trait for a non-unary function, they need to handle (but not generate) constants in the compute_inner method. This can probably also be eliminated, but I think it's livable for now.

srinathsetty · 2022-05-27T08:19:56Z

src/lib.rs

@@ -138,26 +223,30 @@ where
  zn_secondary: G2::Scalar,
  _p_c1: PhantomData<C1>,
  _p_c2: PhantomData<C2>,
+  a1: PhantomData<A1>,


Should these be _p_a1 and _p_a2?

These fields are actually used to simplify initializing IO::Vals later.

porcuquine · 2022-05-31T18:18:42Z

@srinathsetty I have resolved the conflicts with main, which involved adding arity support for CompressedSNARK.

porcuquine · 2022-06-03T08:52:40Z

I have pushed a few more small changes, including a small refactor allowing for cleaner trait implementations. The first-order goal of this PR is now complete; the interfaces are now sufficient to use Nova recursion in the VDF proof as implemented here: protocol/vdf#14.

porcuquine · 2022-08-15T23:20:59Z

I'm closing this, since its purpose is and/or will be fulfilled by other work now.

porcuquine force-pushed the proof-control branch 2 times, most recently from 34db470 to 5500c6f Compare May 24, 2022 01:48

srinathsetty reviewed May 24, 2022

View reviewed changes

src/traits.rs Outdated Show resolved Hide resolved

srinathsetty reviewed May 24, 2022

View reviewed changes

src/lib.rs Outdated Show resolved Hide resolved

srinathsetty reviewed May 24, 2022

View reviewed changes

porcuquine force-pushed the proof-control branch 3 times, most recently from eb2d59e to 6b097a9 Compare May 25, 2022 01:53

porcuquine commented May 27, 2022

View reviewed changes

src/poseidon.rs Show resolved Hide resolved

porcuquine commented May 27, 2022

View reviewed changes

src/lib.rs Outdated Show resolved Hide resolved

porcuquine commented May 27, 2022

View reviewed changes

porcuquine force-pushed the proof-control branch 4 times, most recently from b18baa5 to f4cdf76 Compare May 27, 2022 05:39

porcuquine added 8 commits May 26, 2022 22:42

Refactor to allow non-determinisim.

8b0571b

Check num_steps when verifying.

23dbe23

Rename ComputeStep to StepCompute.

9ae888f

Cargo fmt.

a828d44

Clippy.

402a941

Add nondeterministic test.

82be057

Clippy.

c6935f4

Support non-unary F.

08f3c65

porcuquine force-pushed the proof-control branch from f4cdf76 to 08f3c65 Compare May 27, 2022 05:44

Clippy

3986df4

porcuquine force-pushed the proof-control branch from ca02b47 to 3986df4 Compare May 27, 2022 07:14

srinathsetty reviewed May 27, 2022

View reviewed changes

src/lib.rs Outdated Show resolved Hide resolved

srinathsetty reviewed May 27, 2022

View reviewed changes

src/lib.rs Outdated Show resolved Hide resolved

srinathsetty reviewed May 27, 2022

View reviewed changes

src/lib.rs Show resolved Hide resolved

srinathsetty reviewed May 27, 2022

View reviewed changes

src/lib.rs Outdated Show resolved Hide resolved

srinathsetty reviewed May 27, 2022

View reviewed changes

porcuquine and others added 6 commits May 27, 2022 10:24

Rename primary_circuit to circuit_primary, etc.

efa05d2

Don't make internal functions public.

a472ee9

But do make prove_with_iterators public.

1489bd5

Move arity constants into verifier circuit.

bc48b31

Support CompressedSNARK.

5ffa997

Merge branch 'main' into proof-control

eccf7e6

jpeg07 mentioned this pull request Jun 2, 2022

Tracking issue for Nova refactoring PR (#76) lurk-lab/lurk-rs#101

Closed

porcuquine added 2 commits June 2, 2022 14:43

Derive Debug for IO.

6973678

Refactor.

5d2fb8b

porcuquine mentioned this pull request Jun 3, 2022

Use Nova Recursion. protocol/vdf#14

Merged

Expose TrivialCircuit for use downstream.

60cd61a

porcuquine closed this Aug 15, 2022

huitseeker pushed a commit to huitseeker/Nova that referenced this pull request Oct 25, 2023

Upgrade to Buildjet runner (microsoft#76)

5a21b12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor to allow non-determinisim. #76

Refactor to allow non-determinisim. #76

porcuquine commented May 24, 2022 •

edited

srinathsetty May 24, 2022

srinathsetty commented May 24, 2022

porcuquine commented May 24, 2022

porcuquine commented May 25, 2022

porcuquine May 27, 2022

srinathsetty May 27, 2022

porcuquine May 27, 2022 •

edited

srinathsetty May 27, 2022

porcuquine May 27, 2022

srinathsetty May 27, 2022

srinathsetty May 27, 2022

porcuquine May 27, 2022

srinathsetty May 27, 2022

porcuquine May 27, 2022

porcuquine commented May 31, 2022

porcuquine commented Jun 3, 2022

porcuquine commented Aug 15, 2022

Refactor to allow non-determinisim. #76

Refactor to allow non-determinisim. #76

Conversation

porcuquine commented May 24, 2022 • edited

Choose a reason for hiding this comment

srinathsetty commented May 24, 2022

porcuquine commented May 24, 2022

porcuquine commented May 25, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

porcuquine May 27, 2022 • edited

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

porcuquine commented May 31, 2022

porcuquine commented Jun 3, 2022

porcuquine commented Aug 15, 2022

porcuquine commented May 24, 2022 •

edited

porcuquine May 27, 2022 •

edited