Nova/IVC REPL

Point of contact: Nalin

Past few months of recursion-related work has revealed a requirement for ZK Proof Recursion, Aggregation and Composition friendly tooling. In particular, we’ve observed that https://zkrepl.dev has had an outsized impact in accelerating Circom learning/ZK educational programs for beginners and increased developer velocity for everyone else. It has also inspired other work on tooling/understanding zkSNARKs. Long term, we’d like to do the same for recursion.

In the short term, a REPL for writing ZK proofs using Nova in-browser is quite doable and would be a huge value add to accelerating Nova/SNARK recursion landscape, besides being a technically interesting and accelerationary challenge for the proving/application stack.

Nova is based on R1CS, so Circom is a great beginner friendly programming language as a substrate, and we have tooling in the form of https://github.com/nalinbhardwaj/Nova-Scotiato consume the I/O from Circom compiler and use it directly with Nova.

Additionally, the Nova/Nova-Scotia setup has full support for in-browser proving and verifying, serde for proofs/proving keys/verifying keys etc., so there’s no major technical blockers. That said, there would be a lot of product dev work to build a great REPL in understanding the recursion use cases well and providing a understandable, beginner-friendly but powerful enough scaffold to write Circom code for Nova-based recursion.

Strawman Proposal

• Fork ZKRepl with its existing Circom setup and Monaco integrations (with Circomspect etc.)
• Input format for the REPL
Copy

pragma circom 2.0.3;

// Prove that I know some set of "witness" adders such that starting a
// Fibonacci sequence with some starting public inputs and getting to
// some output public inputs
template Fib () {
    signal input step_in[2];

    signal output step_out[2];

    signal input adder;

    step_out[0] <== step_in[0] + adder;
    step_out[1] <== step_in[0] + step_in[1];
}

component main { public [step_in] } = Fib();

/* INPUT = {
		"starting_step_in": [1, 1],
		"witness": [
			{"adder": 1},
			{"adder": 2},
			{"adder": 1},
		],
} */

• Adds some basic metadata about recursion here (number of steps etc)

• Separate logs by step index, same with output for each step index, and one for final output

• The first step of artifact generation remains the same (but we need the wasm and r1cs only, others optional nice to have)

• Add a check that input length at each step = output length at said step and error in witness gen if so
• Actual proving: buttons to generate output change to “Generate params”, “Prove”, “verify”

1. Internally, these use some WASM compiled package that is quite like the browser-test practically. Minimal 4 functions include:
• Public Param Generation: Generate CRS, return $pk, vk$
• Proving: Run $N$ steps of recursion given starting public input ($z_0$, $W_1, W_2 \dots, W_N$) and returns RecursiveSNARK $proof$ and $z_N$, the output
• Compressing: Input RecursiveSNARK $proof$, output CompressedSNARK $proof$ using Spartan compression
• Verify: Verify CompressedSNARK $proof$
• These will require the WASM/r1cs generated by the previous step to be accessible by the rust runtime. Figure out how to.
‣
Nice to haves

I expect this can be done in one FTE week to a reasonable degree of polish. Additionally, there is likely a lot of optimisation work that can go into the Nova/Nova Scotia repos to improve performance and quality based on learned experience from building this strawman REPL, and on the other end we’ll learn more about what the devex want/love the most.

This probably wouldn’t cover all use cases for SNARK recursion, but should be extendable to cover IVC (incrementally verifiable computation) use cases really well (including with other SNARK schemes in future).