WIP: HyperKZG verifier circuit

[imikushin]

This is a work in progress with the goal to build a complete Jolt verifier circuit and prove it with Groth16 or Polymath.

The ultimate goal is to implement #371.

HyperKZG verifier circuit

• define CommitmentVerifierGadget trait based on CommitmentScheme trait
  • look at how SNARKGadget and CommitmentGadget are structured
    • VK could be modeled after Groth16VerifierGadget::ProcessedVerifyingKeyVar
  • design the first iteration of the gadget
• Implement PairingGadget
  We can't rely (as arkworks' PairingVar does) on the circuit native field to be the base field of the pairing curve of the HyperKZG verifier. The verifier circuit's native field is the scalar field of BN254 or BLS12-381 (as the most widely available pairing curves). Unfortunately, there are no pairing-friendly curves with the base field being the scalar field of either BN254 or BLS12-381.
  • Port an existing pairing (BLS12-381), from arkworks circuits
• implement HyperKZGVerifierGadget
• test cases
  • ➡️ test_hyperkzg_eval
    • commit using native HyperKZG
    • verify using native HyperKZG
    • verify in a circuit using the HyperKZGVerifierGadget
  • test_hyperkzg_small
  • test_hyperkzg_large

[GUJustin]

I'm not sure the benefit of looking at MNT4 or BLS12-381 given that our main goal is on-chain verification on Ethereum, so we need to run Groth16 over BN254?

We could just run both HyperKZG and Groth16 over BN254, but this would obviously mean that all the pairings and scalar multiplications the HyperKZG verifier does have to be done non-natively. That seems too expensive though?

Here's my back-of-the-envelope calculation: The HyperKZG verifier does 2 pairings and 2 or 3 MSMs (not sure which, would have to check) of size n where n is the size of the committed polynomial (say, 2^24). The 2 pairings done non-natively would be about 6 million constraints. If the MSMs are implemented naively (i.e., no Pippenger's, as I'm not sure how much Pippenger's helps when implemented in constraints) that's 48 scalar multiplications. Each of those is about 1 million constraints if implemented non-natively (based on the current way people handle non-native arithmetic in constraints anyway). So that's over 50 million constraints. That seems like too many constraints to run Groth16 on without a beefy machine (maybe it's several minutes of proving time with 32 threads? It's also not that much lower than the 2^27 constraint count limit for Groth16 over BN254).

Please correct me if my estimates here seem off.

Another possibility would be to do a two-step composition to get Jolt proofs on-chain: Jolt-with-HyperKZG-over-BN254 proved by Spartan-with-Hyrax-over-Grumpin proved by Groth16-over-BN254.

This would keep all arithmetic native. We would need both a Hyperkzg-over-BN254-verifier expressed as R1CS over Grumpkin, and a Hyrax-verifier-over-grumpkin-verifier expressed as an R1CS over BN254.

[danielmarinq]

@GUJustin the second two-step recursion system is actually how we've dealt with Nova + CycleFold proof compression to reach Ethereum verifiability. i.e., (modified)Spartan-with-Zeromorph-over-Grumpkin proved by Groth16-over-BN254. Still, we needed very beefy machines to run this process.

This kind of complexity for doing proof compression for EC-based systems is likely a good reason to move out from them, is my gut feeling

[imikushin]

@GUJustin Definitely working towards on-chain verification, so yes, doing Groth16 over BN254. To clarify, the BLS12-381 port I'm mentioning above is for the non-native in-circuit pairing check for Jolt-with-HyperKZG-over-BLS12-381 verification proven by Groth16-over-BN254.

Choosing BLS12-381 because it has an existing R1CS circuit implementation in arkworks.

I'll update here on the non-native pairing costs when I'm done with a pairing circuit PoC.

I do like the idea of keeping arithmetic native. I'm also curious if there are other ways to do this than the two step composition.

[srinathsetty]

This kind of complexity for doing proof compression for EC-based systems is likely a good reason to move out from them, is my gut feeling

@danielmarinq Hash-based proving systems use more layers to get to apply Groth16. I think most systems I’m aware of have three (or more?) layers of recursion to compress proofs and require beefy machines for those layers: (1) switch from “big” proof to “small” proof mode by altering rate of RS codes, (2) switch from “small” field to “big” field to match the scalar field of a curve, and (3) apply Groth16 or Plonk. I don’t think hash vs curve is affecting the complexity here and switching to hash based schemes doesn’t seem to magically solve the problem and the switch may make it somewhat harder.

[srinathsetty]

Spartan-with-Zeromorph-over-Grumpkin proved by Groth16-over-BN254.

@danielmarinq how do you run zeromorph over Grumpkin? Doesn’t ZM need a pairing-friendly curve for succinct verification?

[imikushin]

Just pushed the PoC code for the pairing gadget in the non-native field (circuit is over BN254, the pairing is BLS12-381). The results are chilling: I haven't even got to the pairing itself yet, but just allocating a G1 element is more than 2M constraints. Allocating a G2 element is ~22M more. Here's the printout from the test run (the relevant part is in generate_constraints):

····Start:   Constraint synthesis
[jolt-core/src/circuits/pairing/mod.rs:120:13] cs.num_constraints() = 0
[jolt-core/src/circuits/pairing/mod.rs:125:13] cs.num_constraints() = 2341491
[jolt-core/src/circuits/pairing/mod.rs:128:13] cs.num_constraints() = 2346643
[jolt-core/src/circuits/pairing/mod.rs:134:13] cs.num_constraints() = 2346643
[jolt-core/src/circuits/pairing/mod.rs:139:13] cs.num_constraints() = 23268489
[jolt-core/src/circuits/pairing/mod.rs:142:13] cs.num_constraints() = 25619652
[jolt-core/src/circuits/pairing/mod.rs:148:13] cs.num_constraints() = 25619652

[imikushin]

Hey folks, I understand this may not be a priority, but here's an implementation of HyperKZG verification in a SNARK. To make it work, I had to offload MSMs and multi-pairings to be performed by the SNARK verifier: this dramatically reduces the number of constraints in the circuit allows building the circuit over the pairing scalar field. Enjoy 😉

[imikushin]

I did cheat a little: the transcript is implemented using a mock calling the native ProofTranscript. For actual production use, the transcript should either be implemented using a circuit-friendly hash (MiMC or Poseidon) or BSB22-style commitments (like in Gnark).

[imikushin]

btw, here's how you can see it in action (having checked out this PR's branch):

RUST_TEST_NOCAPTURE=1 cargo test --package jolt-core --lib circuits::poly::commitment::hyperkzg::tests::test_hyperkzg_eval

[Forpee]

To make it work, I had to offload MSMs and multi-pairings to be performed by the SNARK verifier

How did you offload the MSM's?

[imikushin]

@Forpee I've created a wrapper around Groth16 (other SNARK implementations, like Polymath, would also work). This wrapper uses special MSM and pairing gadgets to remember MSMs' scalars and G1 elements and pairings' G1 elements, and adds them to the public input. The verifier simply has to make sure MSMs and pairings evaluate to 0.

It's all in the code 😅

[wyattbenno777]

Just a note: for the FFA which occur in MSM there are tricks in SigmaBus that push FFA to the verifier circuit which can be accumulated in a Cyclefold instance. We will likely get all of this work into Cyclefold and then use the PSE tricks to get Cycefold on-chain.

On L1 we pay for:
1 Cyclefold instance for FFA in MSM. (could be multiple of these amortized)
1 Groth16 for native field circuit.