Implement NIVC Coprocessors. #677

porcuquine · 2023-09-18T01:09:28Z

This PR addresses #637, though some details differ from the precise plan described there.

The current approach demonstrates that we can indeed use a coprocessor defined for IVC and the existing framework, then deploy it to NIVC via a new SuperNova prover type. Because the underlying backend is incomplete and its interfaces not quite worked out, this leaves some gaps. We need to fill in those gaps and massage the result to make switching between NIVC and IVC as smooth as possible, but we should not try to do all that now. Rather, we should incorporate the current work quickly then focus on incremental improvements. I will itemize some of these in a separate issue.

The code here is quite focused and does little more than is strictly required to make this work. The main change that needs to be noted is that in order to keep each coprocessor circuit simple, I made a slight change to the coprocessor contract. Previously, the coprocessor circuit was nestled into reduction such that it could return its evaluated argument directly to the ApplyContinuation phase. However, this does not allow for clean division of circuits.

Now coprocessors return an unevaluated argument and a tail continuation. This is conceptually simple, but does increase the cycle count, as well as the size of each coprocessor circuit. Although not optimal, this has the benefit of being understandable and simple enough to fully implement in a way that yields a consistent design.

Alternative approaches to improving this situation can be considered in a separate issue.

porcuquine · 2023-09-18T01:32:06Z

CI failure should (🤞 ) be fixed once lurk-lang/arecibo#50 merges — though CI will need to be re-triggered to notice.

arthurpaulino · 2023-09-18T11:23:46Z

#678 implements some simplifications in Lang

arthurpaulino

I'm on board with these changes, except for supernova.rs for which I don't have enough context

porcuquine · 2023-09-18T18:40:24Z

Ideally, someone could work on #683 before we merge this PR.

porcuquine · 2023-09-18T18:40:44Z

Meanwhile, here's the outcome of running the sha256_nivc example:

➜  lurk-rs git:(nivc-coprocessors) cargo run --release --example sha256_nivc
    Finished release [optimized] target(s) in 0.50s
     Running `target/release/examples/sha256_nivc`
Beginning proof+public-parameters step...
Proofs took 8.90511775s
Congratulations! You proved a dynamic SHA256 encoding in 8.905117792s time!

huitseeker

Plenty of inline comments, but nothing blocking !

Most important comments are about padding I/O and verification. Thanks a bunch, this is a nice step forward!

huitseeker · 2023-09-19T13:49:56Z

src/circuit/circuit_frame.rs

+        // we need this count, even though folding_config contains reduction_count
+        // because it might be overridden in the case of a coprocoessor, which should have rc=1.
+        // This is not ideal and might not *actually* be needed.


Please open an issue.

src/circuit/circuit_frame.rs

huitseeker · 2023-09-19T14:55:05Z

examples/sha256_nivc.rs

+        let mut bytes = hasher.finalize();
+        bytes.reverse();
+        let l = bytes.len();
+        // Discard the two most significant bits.


We may want to leave a TODO & an issue here, as this will need revisiting when we are dealing with a different field.

Throughout the code base, unless I missed it, we probably want to write a map-to-field that's a tad more rigorous and systematic (i.e. works through modular reduction when we don't care about collision, sensible truncation valid for any field passed as parameter when we do).

Although you make a reasonable point, I don't think it's especially relevant here in particular. Here sha256 is just being used as an 'expensive circuit', and the example itself doesn't pretend to be meaningful in any way. I do agree that a toolkit and strategies for writing applications that may want to do 'strange things' might be useful. However, I don't think it's core either to Lurk or to this NIVC coprocessors example.

True, not essential for the sake of this particular example.

huitseeker · 2023-09-19T15:17:52Z

examples/sha256_nivc.rs

+    // println!("Verifying proof...");
+
+    // let verify_start = Instant::now();
+    // let res = proof.verify(claim, &z0, &zi).unwrap();
+    // let verify_end = verify_start.elapsed();
+
+    // println!("Verify took {:?}", verify_end);


Yep, it would be really great to have this as well.

Yes, it would. It's not entirely obvious what the right interface for this will be. Whereas a Nova RecursiveSnark contains the z_i needed to verify itself, a SuperNova RecursiveSnark does not. It needs to also be provided with a RunningClaim. In order to provide an interface as much like Nova's as possible, it may be necessary to refactor SuperNova in arecibo. @mpenciak is looking into this. I'll create an issue to track this understanding, and if we end up deciding to hack around it in Lurk, we can. For now, I assume the right thing is to reshape the upstream interfaces.

src/circuit/circuit_frame.rs

src/proof/supernova.rs

That PR was on auto-merge.

- uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova, - For references on the latest work defining this trait, see lurk-lab#629 (and its history, incl. lurk-lab#642, lurk-lab#707) and lurk-lab#677. - make the benches use the generic trait, so LEM can bench similarly, - make the examples use the generic trait, so LEM can example similarly, - make Supernova use the generic trait, so LEM can NIVC similarly,

* feat: Introduce MultiFrame trait Mutability leftovers (see #680) - Updated benchmarking scripts to no longer mutate the `store` variable during evaluation frames retrieval. - Reformed `get_evaluation_frames` method across several files to use immutable references to `store` instead of mutable references. Multiframe definition - Introduced several new traits - `CEKState`, `FrameLike`, `EvaluationStore` and `MultiFrameTrait` to manage complex evaluation and circuit proof operations in the `proof/mod.rs` file. - Detailed implementations of the above traits introduced in `circuit/circuit_frame.rs`, providing methods for handling evaluation frames, synthesizing data from multiple frames and more. * refactor: make nova proofs use the generic trait - uses the generic MultiFrame trait introduced in the prior commit to generically prove using nova, - For references on the latest work defining this trait, see #629 (and its history, incl. #642, #707) and #677. - make the benches use the generic trait, so LEM can bench similarly, - make the examples use the generic trait, so LEM can example similarly, - make Supernova use the generic trait, so LEM can NIVC similarly, * use a type alias to simplify test calls --------- Co-authored-by: Arthur Paulino <[email protected]>

porcuquine force-pushed the nivc-coprocessors branch from f75ec09 to 838d4c5 Compare September 18, 2023 01:19

porcuquine mentioned this pull request Sep 18, 2023

Self can be immutable. lurk-lang/arecibo#50

Merged

porcuquine force-pushed the nivc-coprocessors branch 3 times, most recently from a0b1024 to 2312def Compare September 18, 2023 04:38

This was referenced Sep 18, 2023

Use arecibo::supernova::NonUniformCircuit #637

Closed

extend and reconcile sha256_nivc/sha256_ivc bench/examples #681

Closed

porcuquine marked this pull request as ready for review September 18, 2023 18:28

porcuquine requested review from a team as code owners September 18, 2023 18:28

arthurpaulino previously approved these changes Sep 18, 2023

View reviewed changes

porcuquine mentioned this pull request Sep 18, 2023

SuperNova test #683

Closed

porcuquine and others added 2 commits September 18, 2023 11:36

Implement NIVC Coprocessors.

de50e66

simplify Lang internals (#678)

cdcd48a

porcuquine dismissed arthurpaulino’s stale review via cdcd48a September 18, 2023 18:37

porcuquine force-pushed the nivc-coprocessors branch from 97538a3 to cdcd48a Compare September 18, 2023 18:37

arthurpaulino previously approved these changes Sep 18, 2023

View reviewed changes

arthurpaulino dismissed their stale review via 8e5677a September 18, 2023 22:45

arthurpaulino linked an issue Sep 18, 2023 that may be closed by this pull request

SuperNova test #683

Closed

arthurpaulino force-pushed the nivc-coprocessors branch from 8e5677a to 00ad4d1 Compare September 18, 2023 22:47

sha256 nivc test + fix some arecibo API calls

b4aeb4d

arthurpaulino force-pushed the nivc-coprocessors branch from 00ad4d1 to b4aeb4d Compare September 18, 2023 22:58

porcuquine mentioned this pull request Sep 18, 2023

better NIVC coprocessor circuits #686

Closed

mpenciak approved these changes Sep 19, 2023

View reviewed changes

porcuquine enabled auto-merge September 19, 2023 01:22

emmorais approved these changes Sep 19, 2023

View reviewed changes

arthurpaulino approved these changes Sep 19, 2023

View reviewed changes

huitseeker approved these changes Sep 19, 2023

View reviewed changes

porcuquine added this pull request to the merge queue Sep 19, 2023

Merged via the queue into master with commit 2a2d555 Sep 19, 2023

porcuquine deleted the nivc-coprocessors branch September 19, 2023 16:56

huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 20, 2023

refactor: Tidying up changes after lurk-lab#677

e6a955a

That PR was on auto-merge.

huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 20, 2023

refactor: Tidying up changes after lurk-lab#677

8c58e95

That PR was on auto-merge.

huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Sep 20, 2023

refactor: Tidying up changes after lurk-lab#677

9319d85

That PR was on auto-merge.

github-merge-queue bot pushed a commit that referenced this pull request Sep 20, 2023

refactor: Tidying up changes after #677 (#690)

ee2f0f4

That PR was on auto-merge.

This was referenced Sep 20, 2023

Return cdr of coprocessor form in case of error. #693

Closed

implement NIVC verification #695

Closed

Remove unnecessary tail. #700

Merged

huitseeker mentioned this pull request Sep 27, 2023

feat: prove through a Multiframe trait #709

Merged

huitseeker mentioned this pull request Oct 7, 2023

On duplication in LEM integration #639

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement NIVC Coprocessors. #677

Implement NIVC Coprocessors. #677

porcuquine commented Sep 18, 2023 •

edited

Loading

porcuquine commented Sep 18, 2023

arthurpaulino commented Sep 18, 2023

arthurpaulino left a comment

porcuquine commented Sep 18, 2023

porcuquine commented Sep 18, 2023

huitseeker left a comment •

edited

Loading

huitseeker Sep 19, 2023

huitseeker Sep 19, 2023

porcuquine Sep 20, 2023

huitseeker Sep 20, 2023

huitseeker Sep 19, 2023

porcuquine Sep 20, 2023

Implement NIVC Coprocessors. #677

Implement NIVC Coprocessors. #677

Conversation

porcuquine commented Sep 18, 2023 • edited Loading

porcuquine commented Sep 18, 2023

arthurpaulino commented Sep 18, 2023

arthurpaulino left a comment

Choose a reason for hiding this comment

porcuquine commented Sep 18, 2023

porcuquine commented Sep 18, 2023

huitseeker left a comment • edited Loading

Choose a reason for hiding this comment

huitseeker Sep 19, 2023

Choose a reason for hiding this comment

huitseeker Sep 19, 2023

Choose a reason for hiding this comment

porcuquine Sep 20, 2023

Choose a reason for hiding this comment

huitseeker Sep 20, 2023

Choose a reason for hiding this comment

huitseeker Sep 19, 2023

Choose a reason for hiding this comment

porcuquine Sep 20, 2023

Choose a reason for hiding this comment

porcuquine commented Sep 18, 2023 •

edited

Loading

huitseeker left a comment •

edited

Loading