Proof recursion

[wyattbenno777]

Proof recursion will eventually be needed for on-chain Lasso proofs.
There are multiple verifications being done within Lasso and only some will need to be 'made into circuits' for this to work.

Why?

• Reducing proof size.
• Better memory usage in some zkVM settings.

I want to open this ticket up early as it should influence design decisions such as hash selection.
Also, if there is already a plan for this I would love to learn about it!

[wyattbenno777]

Update - I starting working on this in a fork.

• Primary Sum-check as a circuit (re-used a lot from Testudo)
• CombinedTableEvalProof (Hyrax / DotProductProof)
• Memory checking that uses an adapted GKR protocol (Tha13, SL20).

[wyattbenno777]

I have done most of the MSM module and the Hyrax PCS as a R1CS circuit :)
After this tedious bit is over, I plan on going back in to optimize.

• Should bit shifts (from MSM) be in the R1CS setup? (they would be free in this case).
• Better ways to do non-native field work.
• Other optimizations.

[wyattbenno777]

There has been recent work on non-native field arithmetic that we are porting and modifying a bit to generalize.
It should be useful here.

https://eprint.iacr.org/2024/265

Will also post the resulting generalization / results for reducing recursion overhead in another proof system.

[sragss]

@wyattbenno777 – we can work on the adapted GKR from Quarks. Does the rest of the recursion circuit work? Is it OS?

[wyattbenno777]

Hey @sragss .

Last attempt was for Lasso and was not very clean.
Very much OS! Appreciate acknowledgments if it ends up being useful :)
https://github.com/wyattbenno777/Lasso/blob/r1csVerifier/src/r1cs/r1cs_verifier.rs

I stopped when I saw the MSM constraint blowups from Hyrax.
The ArkWork's emulated fields are not super great for this use-case.

https://github.com/arkworks-rs/r1cs-std/blob/master/src/fields/emulated_fp/mod.rs

For reference, tricks for getting CycleFold to ~10 millions constraints:
and other notes on the technique there: (HyperKZG, etc)

privacy-scaling-explorations/sonobe#88

https://privacy-scaling-explorations.github.io/sonobe-docs/design/nova-decider-onchain.html

I have an upcoming research doc that may help!
The best way to do this is not going to be just a naive code attempt.

Likely will need some input from @GUJustin as well.

[sragss]

@wyattbenno777 we now have Zeromorph and HyperKZG which should decrease the constraint count quite a bit (constant size mulitlinear poly opening proofs).