Support non-determinism in NIVC circuits.

[porcuquine]

The initial SuperNova implementation diverged from Nova's pattern for non-deterministic step proofs — by saving a prototype circuit in the RunningClaim then reusing it with new 'public' inputs at each step. However, since each step's computation may depend on non-deterministic private inputs, prove_step actually needs to receive an instance of the primary circuit per-step.

This PR accomplishes that but continues to use the previous method for the secondary circuit, on the theory that the approach to NIVC implemented and supported here assumes and requires that a trivial deterministic function will be proved in the secondary circuit.

Because downstream work depends on this change, this PR is a minimal patch. Future work should add a test modeled on the equivalent Nova test, exercising the change through an example that requires it.

[hero78119]

Hi, would you kindly elaborate more on how to achieve non-deterministc private input work under current design, maybe provide a test example?

[porcuquine]

Hi, would you kindly elaborate more on how to achieve non-deterministc private input work under current design, maybe provide a test example?

Yes, a test will make it clearer — but I need this downstream sooner, and the current test does exercise the change itself still. In other words, I (or someone) can add something that uses something similar to (or exactly the same as) the test_ivc_nondet_with_compression test that Nova has in a follow-up. That example has a circuit that 'calculates' fifth roots — but actually generates the data in reverse, so the roots are supplied non-deterministically, rather than directly calculated.

The point is that in general a bellpepper circuit (something that implements Circuit, which Nova reframes as StepCircuit, as does SuperNova) doesn't provide only a shape — but also unique data per-circuit. In some cases, like in the TestROM example, the circuit data is just a parameterization of the shape. But in the general case, it can also provide the non-deterministic hints needed in order to generate a satisfying witness for the circuit. An even more compelling example than the fifth-root would be hash preimages.

Consider a circuit whose input is the digest output from a binary hash — and whose output is the sum of the two field elements of the preimage. The preimage needs to be somehow communicated to the synthesize method, so the auxiliary variables can be correctly assigned. In this example, the circuit struct might look like:

struct Foo<F> {
    preimage: Option<(F, F)>
}

The Option is there because when synthesizing the shape (for public parameters), there are no real values with which to compute. This is fine for the value used to compute the public params for the RunningClaims, but the individual calls to prove_step will need the actual preimage values in order to witness a satisfying assignment.

[hero78119]

Yes, a test will make it clearer — but I need this downstream sooner, and the current test does exercise the change itself still. In other words, I (or someone) can add something that uses something similar to (or exactly the same as) the test_ivc_nondet_with_compression test that Nova has in a follow-up. That example has a circuit that 'calculates' fifth roots — but actually generates the data in reverse, so the roots are supplied non-deterministically, rather than directly calculated.

The point is that in general a bellpepper circuit (something that implements Circuit, which Nova reframes as StepCircuit, as does SuperNova) doesn't provide only a shape — but also unique data per-circuit. In some cases, like in the TestROM example, the circuit data is just a parameterization of the shape. But in the general case, it can also provide the non-deterministic hints needed in order to generate a satisfying witness for the circuit. An even more compelling example than the fifth-root would be hash preimages.

Consider a circuit whose input is the digest output from a binary hash — and whose output is the sum of the two field elements of the preimage. The preimage needs to be somehow communicated to the synthesize method, so the auxiliary variables can be correctly assigned. In this example, the circuit struct might look like:

struct Foo<F> {
    preimage: Option<(F, F)>
}

The Option is there because when synthesizing the shape (for public parameters), there are no real values with which to compute. This is fine for the value used to compute the public params for the RunningClaims, but the individual calls to prove_step will need the actual preimage values in order to witness a satisfying assignment.

Thanks for explanation! In test_ivc_nondet_with_compression the non-deterministics input are implemented by multiple copy of primary circuit instances each have different field values, and those instance are instantiated in early stage. I believe there are some space to further polishing this design later on.

For this PR, how about further tuning of the design of Supernova RecursiveSNARK by passing &Option<C1> in prove_step and iter_base_step instead? With that, for deterministic primary circuit instance can still retrieved from running claim, and for non-deterministic primary circuit the new instance will be used instead.

Besides, also suggest add sanity check to assure non-deterministic primary circuit instance Shape matching with shape in setup phase.

[hero78119]

Here should be primary_circuit(1) otherwise it should fail on verifying due to mismatch shape.

[porcuquine]

fixed

[porcuquine]

Besides, also suggest add sanity check to assure non-deterministic primary circuit instance Shape matching with shape in setup phase.

This would be very expensive. Synthesizing the Shape is meant to be a one-time operation, and asymptotic assumptions of performance analysis require that it remain that way. I understand the appeal of a safety double-check, but this is exactly the same situation as Nova.

I think the best approach to the SuperNova work will be to fall Nova as closely as possible, ideally in a way that allows even more shared code than currently. This will simplify treating the folding scheme as a black box (as much as possible) and will in turn make it easier to extend NIVC to work with future developments.

[porcuquine]

For this PR, how about further tuning of the design of Supernova RecursiveSNARK by passing &Option<C1> in prove_step and iter_base_step instead? With that, for deterministic primary circuit instance can still retrieved from running claim, and for non-deterministic primary circuit the new instance will be used instead.

I would rather avoid complexity (especially complexity which gratuitously deviates from Nova) whose only purpose is convenience in a special case. If the prover knows a given circuit doesn't require any hints, then nothing prevents passing a reference to the identical object to prove_step every time.

[hero78119]

For this PR, how about further tuning of the design of Supernova RecursiveSNARK by passing &Option<C1> in prove_step and iter_base_step instead? With that, for deterministic primary circuit instance can still retrieved from running claim, and for non-deterministic primary circuit the new instance will be used instead.

I would rather avoid complexity (especially complexity which gratuitously deviates from Nova) whose only purpose is convenience in a special case. If the prover knows a given circuit doesn't require any hints, then nothing prevents passing a reference to the identical object to prove_step every time.

My point is to keep the original simplified api to just passing single running_claim in deterministic primary circuit use case. But I see your point that it should be better to align design with Nova first, and refactor with Nova once got better design.

other part LGTM!