feat: non-deterministic NIVC example#52
feat: non-deterministic NIVC example#52mpenciak wants to merge 20 commits intolurk-lang:devfrom mpenciak:nivc_example
Conversation
| let new_pc = AllocatedNum::alloc(cs.namespace(|| "next_pc"), || { | ||
| if self.next_pc { | ||
| Ok(F::ONE) | ||
| } else { | ||
| Ok(F::ZERO) |
There was a problem hiding this comment.
What purpose does self.next_pc serve here? Why not just look at the value of next_pc_bit?
There was a problem hiding this comment.
In other words, why do you need any hint in the ShaCircuit struct? I don't think you do.
| chunk | ||
| }) | ||
| .collect::<Vec<_>>(); | ||
|
|
There was a problem hiding this comment.
I think you could just pack the 80 bits you want into the preimage here — same as you do for the digest below. That would save the need for the strict decomposition and to constrain the unused bits (so savings of 200+ constraints).
There was a problem hiding this comment.
This only works if the inputs will always be 80 bits, but I think that is the case for all the internal inputs, if all of your outputs are 80 bits (stuffed into a field element). So if you similarly restrict the initial input, then this would work.
examples/nivc_dynamic_phi.rs
Outdated
| impl<F: PrimeField> BlakeCircuit<F> { | ||
| fn new(next_pc: bool) -> Self { | ||
| Self { | ||
| next_pc, |
There was a problem hiding this comment.
Same comments/questions about the need for this hint as in the sha circuit above.
examples/nivc_dynamic_phi.rs
Outdated
| struct ExampleSteps<G1, G2> | ||
| where | ||
| G1: Group<Base = <G2 as Group>::Scalar>, | ||
| G2: Group<Base = <G1 as Group>::Scalar>, | ||
| { | ||
| next_pc: bool, | ||
| _p: PhantomData<(G1, G2)>, | ||
| } |
There was a problem hiding this comment.
I don't understand the need for or idea behind this struct. The name implies a collection of steps, yet you're only representing a single bit of information. Moreover, this is 'redundant hint' as described above. And as far as I can tell, this is a second level of indirection that redundant hint — since you're also keeping such hints in the individual hash circuits.
make it so that the bit decomposition is computed out of circuit
|
I think the primary need this worked toward addressing is fulfilled by #92. Can we close this, at least for now? |
2 participants
This PR adds a pair of NIVC examples.
The first,
nivc_static_phi, incorporates non-deterministic hints from the prover to prove the chain of computations of cube and fifth roots.The second,
nivc_dynamic_phi, calculates theprogram_counterdynamically at each step as the least-significant bit of the calculated hash (eithersha256orblake2s).