supernova implementation with naive opcode commitment for argumented circuit sequence. #204
Conversation
|
@microsoft-github-policy-service agree |
|
Thanks for the PR! Given this is a relatively big code contribution, it will take some time to review it. |
Well noted and thanks for update! |
src/supernova/circuit.rs
Outdated
| //! There are two Verification Circuits. The primary and the secondary. | ||
| //! Each of them is over a Pasta curve but | ||
| //! only the primary executes the next step of the computation. | ||
| //! We have two running instances. Each circuit takes as input 2 hashes: one for each | ||
| //! of the running instances. Each of these hashes is |
There was a problem hiding this comment.
It would be great to rephrase this in order to refer to the l (!= 2) running instances you'd expect to find in the list.
There was a problem hiding this comment.
Fixed, all the supernova docs/comment are preliminary rephrased in latest commit.
| r1cs_shape_primary: R1CSShape<G1>, | ||
| ro_consts_secondary: ROConstants<G2>, | ||
| ro_consts_circuit_secondary: ROConstantsCircuit<G1>, | ||
| ck_secondary: Option<CommitmentKey<G2>>, | ||
| r1cs_shape_secondary: R1CSShape<G2>, |
There was a problem hiding this comment.
This seems to be precisely the same struct at PublicParams. Would some sizing of the (R1CS) contents of the ROM be more appropriate than r1cs_shape_primary and r1cs_shape_secondary here?
There was a problem hiding this comment.
r1cs_shape_primary and r1cs_shape_secondary are not the same shape, since secondary circuit is just a trivial circuit and do nothing while primary circuit got the application logic. Not sure I understand correctly, would you kindly elaborate more on this :)
There was a problem hiding this comment.
Setting heterogeneity aside for a moment, the sizing of the public parameters depends on the shape of the circuit they are used for. In particular, you would want the CommitmentKey (in practice, a vector Pedersen) to offer enough generators for the size of the step circuit. How this is done is expanded upon in PR #203 .
With heterogeneity, I would expect that same dependency to still exist, but the circuit bookkeeping to be different. More specifically, I would expect the R1CSShape of the largest circuit among those in the ROM to drive the size requirements for the public parameters.
There was a problem hiding this comment.
In this earlier version (shell) of SuperNova it was noted that the user would choose the largest circuit for the public parameters; They know the part of the ROM that is largest. I think the notes were possibly lost on this.. (or there is possibly a way to automate choosing?)
There was a problem hiding this comment.
This was hinted at in a prior comment.
Nova, as a library, is quite safe in sizing public parameters:
- Nova runs through circuit synthesis (which is costly!) to size the public parameters precisely, see here.
- see feat: Make commitment key generation configurable with an optional parameter #203 for other nitty-gritty details.
The approach of simply recommending the user to pass the largest circuit among those in the ROM here may be error-prone -- as I'm worried a user might miss the requirement. If there was a ROM API in the form of an indexed iterator of circuits (perhaps with a cached way to determine their shape), I suspect it would make automating this part of the setup possible.
There was a problem hiding this comment.
This was hinted at in a prior comment. Nova, as a library, is quite safe in sizing public parameters:
- Nova runs through circuit synthesis (which is costly!) to size the public parameters precisely, see here.
- see feat: Make commitment key generation configurable with an optional parameter #203 for other nitty-gritty details.
The approach of simply recommending the user to pass the largest circuit among those in the ROM here may be error-prone -- as I'm worried a user might miss the requirement. If there was a ROM API in the form of an indexed iterator of circuits (perhaps with a cached way to determine their shape), I suspect it would make automating this part of the setup possible.
For current version, the automating way to identify largest primary circuit is relying on user to implement logic to sizing the largest circuit to setup commitment key based on it. demo in Supernova test
I admitted the ideal way is to exploring way to hide it from user to be more error pruning. The challenges for moving this part inside framework is mostly due to the circuit generic Ca, Cb defined on Supernova RunningClaims to adopt heterogeneous of the primary circuit. I had explorer few way to fine tune this design but no satisfying version
In this earlier version (shell) of SuperNova it was noted that the user would choose the largest circuit for the public parameters; They know the part of the ROM that is largest. I think the notes were possibly lost on this.. (or there is possibly a way to automate choosing?)
haha, I clean up and re-design the largest in earlier version since IMO 1. this variable design and naming is ambiguously and confusing 2. it still shift the responsibility back to user.
For current design, I try to solve point 1, however point 2 still lefted open
hero78119
force-pushed
the
supernova
branch
4 times, most recently
from
3f2b308 to
3ed8f19
Compare
|
Hmmm. It's hard for me to see how this fits in inside of this lib instead of being a standalone crate. SuperNova is actually a nice use-case to have |
From my viewpoint, supernova is a generalized version of current Nova implementation (Nova is a special case for 1 augmented circuit version) Would like to hear more opinions from author later :) |
src/supernova/mod.rs
Outdated
| ) as usize]; | ||
|
|
||
| let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| { | ||
| if augmented_circuit_index == OPCODE_0 { |
There was a problem hiding this comment.
This demo have some code duplication on opcode multiplexing, due to slightly hard on handling heterogeneous type of augment circuit. I try few options to beautify this part and no satisfied version.
If you have better suggestion kindly let me know, thanks
My opinion is that it would belong here as a 'feature'. Other things I would include:
A user would come and say: "I want a Nova proof of xyz, the verifier needs to work on xyz blockchain/environment", My 2 cents. |
@CPerezz, regarding a stand-alone crate with nova-snark as a dependency, wouldn't it need access to several internal methods of Nova (e.g., nifs.rs), which is not currently exposed? This would also require nova to move to being a workspace right? Or, is there a different and better approach to multiple packages? In general, I do like the layering approach, but I will have to look through the new code to see what code will need to be exposed for the layering to work. |
|
Updated: Also run benchmark recursive-snark for Nova vs Supernova-1-augmented-circuit version Benchmark is on windows-subsystem-linux so perf will be variant. Will be better to run benchmark on other neutral server to get more accurate result. |
hero78119
force-pushed
the
supernova
branch
2 times, most recently
from
9482a6f to
6d76659
Compare
|
Updated: fixed a soundness in supernova implementation. More detail: in Nova, In Supernova Non-Uniform IVC, there will be > 1 augmented circuit, each will have different primary circuit R1CS shape, and in each round of folding, different augmented circuit will be invoked and fold to get {i+1} running instance. Soundness is introduced in this implementation as In latest commit 6d76659, this is fixed by have a |
|
Thanks @hero78119 for your prompt updates to the PR! I will review the PR more carefully and provide inputs as necessary. |
| // check the satisfiability of the provided `circuit_index` instance | ||
| let default_instance = RelaxedR1CSInstance::default(ck_primary, &pp.r1cs_shape_primary); | ||
| let default_witness = RelaxedR1CSWitness::default(&pp.r1cs_shape_primary); | ||
| let (res_r_primary, (res_r_secondary, res_l_secondary)) = rayon::join( |
There was a problem hiding this comment.
In Supernova's paper the verifier need to check every related instance-witness pair (U, W) satisfys relaxed R1CS constrains. However, it seems only the claimed pair is checked here.
There was a problem hiding this comment.
REMOVED AS THE FOLLOWING ANSWER IS MORE COMPLETE
There was a problem hiding this comment.
@wyattbenno777 I'm confused a bit by your explanation. In SuperNova instantiated over a cycle of curves, if there are \ell different step circuits, we will have \ell running instances (on the first curve), a running instance (on the second curve), and a fresh instance (second curve). We need to check that all \ell + 2 instances are satisfying. In the case of Nova, \ell = 1, so we have 3 instances verified in the main branch.
There was a problem hiding this comment.
In code, we are giving a PrimaryCircuit and a TrivialCircuit to a RunningInstance object. It runs with these as many times as mentioned in the ROM (there is an instance being folded in at each step). In the case of Nova the user is still specifying a primary and a trivial circuit. So should I be explaining this as 3 things to be verified for each opcode? (Primary, Trivial, Thing to be folded on second curve) or as the things the user specifies (Primary and Trivial circuit)?
There was a problem hiding this comment.
Extra info for any future reader: pg. 15 https://eprint.iacr.org/2022/1758.pdf
There was a problem hiding this comment.
They are all verified in their own step. opcode 1 runs x times and is verified, then opcode 2. If the ROM is something like [1,2,1,1] it is run and verified for each step with the code you commented. At the very end a valid SuperNova proof would have both 1 and 2 be valid.
More addon. I think opcode 1 runs x times is indeed a bit confusing haha, because it sounds like we can run opcode 1 x times first then follow by opcode 2 runs y times, ...., this mindset can explain well on Uniform-IVC Nova, but on Supernova, non-uniform with sequence need to be emphasised.
Giving example of sequence [1, 2, 1, 1], Supernova assure
- i=0, augmented circuit 1 is correctly invoked
- i=1, augmented circuit 2 is correctly invoked
- i=2, augmented circuit 1 ...
- i=3, augmented circuit 1 ...
and supernova need to capture soundness from the maliculous prover giving another sequence [1, 1, 1, 2]. Since order matters, and y1 != y2, for y1=F_1(F_1(F_2(F_1(x)))), y2=F_2(F_1(F_1(F_1(x)))).
Giving there are N opcodes on 2 cycles curve, there will be N running instances (on second curve) + 1 running instance (on first curve) + 1 fresh instance (second curve)
In each round of folding for the sake of efficiency, we can just verify One running instances (on second curve) + 1 running instance (on first curve) + 1 fresh instance (second curve). The One is the opcode being folded in this round. Of course we can verify N running instance (on second curve) all together, but it's not nessesary (even from security perspective) since they will be verified on their own round.
Actually, invoking verify on RecursiveSNARK (here verify is not the same as NIVC verify circuit!) at each round is more for demo purpose. In production I think we can just update RecursiveSNARK and have a final SNARK prove via CompressSNARK is enough (Terminlogies borrow from nova implementation, not paper)
There was a problem hiding this comment.
This is a very well thought out answer!
*CycleNova will change this if/when implemented 😊
|
Update:
|
src/supernova/circuit.rs
Outdated
| // Now reduce to one is safe, because only 1 of them != G::Zero based on the previous step | ||
| // TODO optimize this part to have raw linear-combination on variables to achieve less constraints | ||
| let U_to_fold = U?.iter().enumerate().try_fold(empty_U, |agg, (i, U)| { |
There was a problem hiding this comment.
The logic presented here makes me nervous because you are relying on every element of the unselected instances being zero for the selection logic. This is a picky coupling making the correctness of this code very dependent on invariants elsewhere in the code base, when those might not actually be guaranteed.
In fact, as far as I can tell, the empty_U returned from AllocatedRelaxedInstance::alloc(…, None, …) is not actually constrained to be entirely composed of zeros. Therefore, although the defined behavior of the prover's code does do that, nothing guarantees that it will — so a witness containing other values could also be chosen. This means the prover could supply alternate unconstrained values such that U_to_fold can be chosen freely (even though the Nova code base does not choose such values). That seems to violate the intent and requirements of this sub-circuit.
I think the problem would not exist (at least in this form) if you implemented a version of AllocatedRelaxedInstance::alloc that guarantees that what it returns is constrained to be all zeros.
To be very explicit, look at the code:
You can see here, for example, that when inst is None, then Allocated::Point::alloc is being called with None.
let W = AllocatedPoint::alloc(
cs.namespace(|| "allocate W"),
inst
.get()
.map_or(None, |inst| Some(inst.comm_W.to_coordinates())),
)?;
Then in AllocatedPoint::alloc we see that an input of None allocates the 'default infinity point' (including zero for the x and y coordinates), but does not constrain those allocations.
You could also use something like Lurk's multicase gadget, to abstract the selection logic and not entangle it with ad-hoc scalar/curve arithmetic. Although that might be too heavy to pull into Nova just for this purpose, I still believe such non-trivial control logic should be abstracted so it can be reviewed and audited in isolation. It's too easy for an assumption to slip through when having to 'rebuild' understanding of clever constraints embedded in a context where assumptions are hard to check. I think that's actually what happened here, but I needed to check it over more carefully.
For clarity, I'll repeat what I think happened:
- the computation of
U_to_folddepends on all but one of the allocated instances inUbeing zero (from the perspective of addition) in each of its components. - all non-matching (unselected) instances are indeed constrained to be equal to
empty_U. empty_Udoes indeed contain 'zero values', but these are unconstrained.- therefore the invariant required to make the calculation of
U_to_foldvalid does not actually hold.
See if that makes sense to you, and if not, please let me know what I missed.
There was a problem hiding this comment.
Hi, Thanks for catch up this and point out that!
Yes this is an under-constraints, due to there is no constraint for the empty value declaration.
I refered your idea and reviewed again of this logic.
Then I realized a better way to solve it is just rewrite this logic to avoid empty allocation, instead just iterate through the list to get the selected value when index match.
More detail in pseudo code
a := the array
index := target index
res0 = a[0] // default value is first element
res1 := index == 1 ? a[1]:res0
res2 := index == 2 ? a[2]:res1
res3 := index == 3 ? a[3]:res2
...
return resN
In particular, this ad-hoc N-reduce-1 optimisation is only applicable here , giving assumption that prover have no choice but need to honestly choose correct witness last_augmented_circuit_index to hint the fold(fresh instance, U[last_augmented_circuit_index]) in NIFS verify circuit, otherwise error will be catch up in the final CompressSNARK check.
Besides, This selection logic also abstract to util. However, by default it will return first element which is not general for other usecase, so just make it dedicated to supernova crate.
Updated with a938f29
Thanks again for the review :)
There was a problem hiding this comment.
Yes, I think this repeated conditional works. Given the size of the values (15 field elements for the allocated relax instance, I think), a multicase will be cheaper at about 6 clauses (i.e. 6 running instances). We don't need to worry about that now, but I think we can create an ergonomic and secure solution for this in general. I'll show my work later, perhaps elsewhere, so we can work through the details. For now, I think doing as you suggest would fairly simply solve the soundness issue.
There was a problem hiding this comment.
Issue follow-up:
Updated a commit 4475884 to fix another relevant soundness issue
Background: there is existing and related soundness cause by last_augmented_circuit_index usage, once malicious prover set it outside range [0, #num_opcode). More explicitly, It will cause no-matching of running instance selection in the code, which means NO UPDATES of running instances U[..]_i+1.
The solution I adopted is to propagate the processed last_augmented_circuit_index through whole circuit. The mindset behind is we already have ad-hoc logic to set last_augmented_circuit_index=0 once outside range. Then circuit need to use this new variable to assure U[last_augmented_circuit_index]_i+1 updated accordingly.
I expected this simple solution just fit well in last_augmented_circuit_index usecase.
Along with new fix, I also document more on this part
Lines 411 to 428 in 4475884
|
Hi all, just a quick note, which I've discussed with @hero78119 and @srinathsetty already. Because this work is going to still require further work on the right interfaces and general polishing, we'd like to move it to our (Lurk Lab's) Arecibo Nova fork. That will let us iterate on design, and especially simplify using from This PR and valuable discussion will remain open so @srinathsetty can review the crypto and circuits, with the goal of merging to Nova under a feature flag. Meanwhile, we will continue active review and development of this work in arecibo. Once better answers for some of the unknowns/questions posed by the current work have been incubated, the plan is to bring those back as PRs to Nova. |
|
@hero78119 To reiterate, we intend to merge this PR here in Microsoft/Nova once comments are addressed. I'll do a detailed audit of the circuit code and the entire PR soon. We will merge this code under an optional feature flag "super". @porcuquine It likely makes sense to wait for this merge to happen before further work elsewhere, to avoid duplication of efforts. |
Yes I have already discussed with @porcuquine and @huitseeker, it makes sense to incubating and polishing more on interface for applications, and (Lurk Lab's) Arecibo is nice candidate to explore more on it.
Yes it sounds great to me. (+ cc co-author @wyattbenno777 ) |
Share benchmark result on latest commit vs old commit 
(y-axis millisecond) Summary
|
We don't mind a little duplication, and bringing this in sooner will let us start iterating on things we need to bring into existence for our own purposes. We'll make sure any outcomes of your review are incorporated. |
|
Based on the offline discussion, @porcuquine and team will submit a new PR that has been improved in their fork of Nova. We will review the PR once it is stable and submitted. |
|
Another review ongoing PR lurk-lang/arecibo#48 which is to unlock the full power of Nova to support read-write lookup in cheap cost, leveraging offline-memory-check tricks mentioned in various paper. It's related to this SuperNova PR where the ROM based on this to achieve constant size of Nova state instead of linear to ROM size |
|
We will close this PR given alternate plans to get this back. |
Related to issue #146
This works majorly based on the initial works credits to @wyattbenno777, who initiatives a neat and clean skeleton then make further refactor possible! 🥇
This implementation idea is mostly followed supernova paper https://eprint.iacr.org/2022/1758, with some modified details described as below.
Feature flagged under a
supernovaflag that is off by default, so it has no impact on other parts of the code or users of the Nova library.Comments are welcome!
Implementation rationales
consolidate
Φ(zi, wi)functionality into step_circuit/F circuitIn realistic ISA design, program counter can be set as arbitrary value by opcode itself.
Take RIV32 JAL opcode for example,
pc_{i}will be added byimmoffset to obtainpc_{i+1}.In other words,
pc_{i+1}manipulation makemore sense to be constrained by correspondence opcode implementation, i.e. step_circuit.This PR make above feature possible, by enhancing
synthesisfunction to passpc_ialong withz_ias input, and output correspondingpc_{i+1}andz_{i+1}in supernova, andpc_{i}will be assumed to be checked by step circuit, along with a memory commitment to prove memory[pc_{i}] matched with current opcode. A Read-only-Memory, ROM is introduced as a naive memory commitment demo. More detail of ROM will be elaboration below.extract circuit index selector against program counter, execution sequence correctness
In supernova paper, one of implicit part is how to choose i+1 argumented F' circuit to fold previous relaxed r1cs and r1cs.
To assure next F' argumented circuit is invoked in pre-defined sequence, each F' circuit should constraint it order with each pc_i.
This implementation demo a naive prototype of RAM machine: a Read-Only-Memory, ROM for opcode sequence constraints. ROM is passed as public input z as a flattern vector, [<stepcircuit_1>, <stepcircuit_2>, …], then each step_circuit constraint
rom[pc_{i}] == step_circuit_index. In the later works, it should be replaced by more advanced memory commitment, such as merkle root + merkle proofs, or other batched KZG commitment. This can be combined together as4.4 Optimizations, p27in supernova paper.secondary circuit logic
For supernova secondary circuit, program counter just assign 0 for each folding step. There is no non-trivial logic in supernova secondary circuit.
Enhance debugging ability
This PR also introduces debugging friendly feature to
is_satandis_sat_relaxedfunction to point out failed constrain’s correspondence annotation. This improve a lot comparing with show true/false only.Follow-up works (thought can be future PRs)
4.4 Optimizations, p27in supernova paper.