Awesome

Nova Scotia

Middleware to compile Circom circuits to Nova prover

This repository provides necessary middleware to take generated output of the Circom compiler (R1CS constraints and generated witnesses) and use them with Nova as a prover.

Why?

Nova is the state of the art for recursive SNARKs, Circom is the state of the art for ZK devtooling, so it makes a lot of sense to want to do this. Since Nova uses ~R1CS arithmetization, its mostly just a matter of parsing Circom output into something Nova can use.

As Justin Drake talks about it, I think the right way to think of Nova is as a preprocessor for zkSNARKs with lots of repeated structure -- Nova can shrink the cost (in number of R1CS constraints) of checking N instances of a problem to ~one instance of the same problem. This is clean and magical and lends itself well to a world where we take the output of Nova and then verify it in a "real" zkSNARK (like PLONK/groth16/Spartan) to obtain a actually fully minified proof (that is sublinear even in the size of one instance). Notably, this pattern is already used in settings like zkEVMs, but with STARK proofs instead of Nova proofs. IMO, Nova (and folding scheme-like things in particular) lend themselves better to the properties we want with the preprocessing layer vs. STARKs: fast compression, minimal cryptographic assumptions and low recursive overhead.¹

Nova Scotia comes with extensive examples, as well as a in-browser usage example. We will describe the proving/verifying workflow in more detail below.

How?

To use it yourself, start by installing Circom as described in the Circom documentation.

Writing Nova Step Circuits in Circom

To write Nova Scotia circuits in Circom, we operate on the abstraction of one step of recursion. We write a circuit that takes a list of public inputs (these must be named step_in for the Nova-Scotia interface) and outputs the same number of public outputs (named step_out). These public outputs will then be routed to the next step of recursion as step_in, and this will continue until we reach the end of the recursion iterations. Within a step circuit, besides the public inputs, Circom circuits can input additional private inputs (with any name/JSON structure Circom will accept). We will instrument the piping of these private inputs in our Rust shimming.

When you're ready, compile your circuit using circom [file].circom --r1cs --sym --c --prime vesta for the vesta curve. Compile the C++ witness generator in [file]_cpp by running make in that folder. Alternately, you can compile the WASM witness generator using circom [file].circom --r1cs --sym --wasm --prime vesta. We will later use the R1CS file and the witness generator binary (either C++ binary or WASM), so make note of their filepaths. You can independently test these step circuits by running witness generation as described in the Circom documentation.

Since Nova runs on a cycle of elliptic curves, you must specify the curve via traits and in the Circom compilation command. Currently, Nova Scotia supports any cycle supported by Nova upstream in provider and by Circom's --prime flag. You can see example circuits for both the Pasta (pallas/vesta) and bn254/grumpkin curves in the examples directory.

Rust shimming for Nova Scotia

Start a new Rust project and add Nova Scotia to your dependencies. Then, you can start using your Circom step circuits with Nova. Start by defining the paths to the Circom output and loading the R1CS file:

// The cycle of curves we use, can be any cycle supported by Nova
type G1 = pasta_curves::pallas::Point;
type G2 = pasta_curves::vesta::Point;

let circuit_file = root.join("examples/bitcoin/circom/bitcoin_benchmark.r1cs");
let witness_generator_file =
    root.join("examples/bitcoin/circom/bitcoin_benchmark_cpp/bitcoin_benchmark");

let r1cs = load_r1cs::<G1, G2>(&circuit_file); // loads R1CS file into memory

Circom supports witness generation using both C++ and WASM, so you can choose which one to use by passing witness_generator_file either as the generated C++ binary or as the WASM output of Circom (the circuit.wasm file). If you use WASM, we assume you have a compatible version of node installed on your system. Note that for proving locally, we recommend using the C++ witness generator for performance (except on M1/M2 Macs where it is not supported). For in-browser proving/verifying, you must use the WASM witness generator. We will describe in-browser proving and verification workflow later in the README.

Then, create the public parameters (CRS) using the create_public_params function:

let pp = create_public_params::<G1, G2>(r1cs.clone());

Now, construct the input to Circom witness generator at each step of recursion. This is a HashMap representation of the JSON input to your Circom input. For instance, in the case of the bitcoin example, private_inputs is a list of HashMaps, each containing block headers and block hashes for the blocks that step of recursion verifies, and the public input step_in is the previous block hash in the chain.

To instantiate this recursion, we use create_recursive_circuit from Nova Scotia:

let recursive_snark = create_recursive_circuit(
    FileLocation::PathBuf(witness_generator_file),
    r1cs,
    private_inputs,
    start_public_input.to_vec(),
    &pp,
).unwrap();

Verification is done using the verify function defined by Nova, which additionally takes secondary inputs that Nova Scotia will initialise to [F<G2>::zero()], so just pass that in:

println!("Verifying a RecursiveSNARK...");
let start = Instant::now();
let res = recursive_snark.verify(
    &pp,
    iteration_count,
    &start_public_input.clone(),
    &[F<G2>::zero()],
);
println!(
    "RecursiveSNARK::verify: {:?}, took {:?}",
    res,
    start.elapsed()
);
let verifier_time = start.elapsed();
assert!(res.is_ok());

For proper examples and more details, see the toy.rs and the bitcoin.rs examples documented below:

toy.rs

toy.rs is a very simple toy step circuit meant for testing purposes. It is helpful to start by looking at its Circom code and the Rust code that instantiates it in Nova. It is a simple variant of fibonacci that additionally takes a private input to add at each step.

bitcoin.rs

bitcoin.rs is a more complex example that uses Nova to create a prover for bitcoin chain proof-of-work. For nearly the cost of just one block proof-of-work verification, Nova can compress the verification of the entire bitcoin chain. The Circom circuit is more complex for this construction (since it runs hashing and other bit-twiddling to verify each block in ~150k constraints). This is also helpful to look at for benchmarking purposes, since you can play around with the number of blocks verified in each step of recursion. Here are some simple benchmarks for different configurations of recursion for 120 blocks being proven and verified:

Note that the verification times are linear in the number of blocks per step of recursion, while the proving time reduces with fewer recursive steps. In practice, you would use the output of Nova as an input to another SNARK scheme like Plonk/groth16 (as previously mentioned) to obtain full succinctness.

Additionally, these are numbers on my (not great) laptop, so you should expect better performance on a beefier machine, especially because Nova supports GPU accelerated MSMs for proving under the hood.

In-browser proving and verification

Nova Scotia also supports proving and verification of proofs in browser, along with serde of proofs and public parameters. We provide an example of in-browser proving using Rust compiled to WASM in the browser-test folder of the repository. The test-client in the folder is a Create React App demonstrating in-browser proving and verification. If you are interested in similar usage, please look through the folders to understand how they work. It may also be useful to look at the halo2 guide to WASM compiling.

Notes for interested contributors

Please see GitHub issues if you are interested in contributing. You can reach out to me directly on Telegram at @nibnalin if you have any questions.

Credits

Credits to the original Nova implementation and paper by Srinath Setty/Microsoft Research, and the Circom language from the iden3 team.

The parsing and generation strongly borrows from other similar repos like plonkit, ark-circom, zkutil etc.

I have never been to Nova Scotia. This repo is named Nova Scotia because crypto already has Tornado Cash Nova and Arbitrum Nova besides Microsoft Nova, so its time we start adding suffixes to the term to maximize confusion around it.

The art at the top of the page is by Tadashi Moriyama, all credits to him. I'm just a fan of it. :)