Exploring SNARK Recursion without pairing cycles

[ebfull]

In order to achieve recursive composition of zk-SNARK proofs we need to somehow verify a proof within the circuit over Fq (the scalar field of the pairing friendly curve), which involves extensive arithmetic over Fp (the base field of the pairing-friendly curve). The current approach used by e.g. Coda is to leverage a pairing-friendly cycle of MNT4 and MNT6 curves to bridge between the fields, and there are no other known (practical) methods of finding secure pairing-friendly cycles with other embedding degrees. As a result, they are forced to use large primes (over 700 bits) to compensate for the security loss.

I'd like to explore a different approach. Instead of a pairing-friendly cycle, let's use a cycle where only one of the curves is pairing-friendly. The curve over Fq (which has subgroup order p) can be used e.g. to instantiate a proving system for all of the arithmetic over Fp. Crucially, it's not necessary for the inner proving system to be succinct, it just needs to allow us to outsource Fp arithmetic more efficiently than it can be naively simulated in Fq. ~As an example, we could perhaps use Spartan.~ Nevermind, use Halo!

It is trivial to build cycles of the kind needed using BN curves. In order to meet conservative security margins, we need primes roughly around 2^384 at least. However, if the inner proving system is efficient enough to verify within the circuit this could potentially be considerably more efficient than the larger >700 bit primes used by Coda. (Large primes increase the cost of FFTs, increase the size of parameters, increase the cost of group arithmetic, increase the cost of multi-exponentiations, increase the cost of the pairing function, and increase the size of keying material.)

[ebfull]

Terminology Reference

• Fp is the base field of the pairing-friendly curve.
• Fq is the scalar field of the pairing-friendly curve.
• E0/Fq is the embedded elliptic curve constructed over Fq, with order p.
• E1/Fp is the pairing-friendly elliptic curve constructed over Fp, with order q (sub)group G1.
• E2/Fp² is the elliptic curve constructed over Fp², with order q subgroup G2.

[daira]

Here is a sage program to find such cycles of BN curves: https://github.com/daira/curvesearch/blob/master/halfpairing.sage

Run using sage halfpairing.sage <min-bitlength> [<min-2adicity>]. For example:

$ sage halfpairing.sage 394
bitlength 394
p = 0b1011011110000100100100000000000000000000000000000000000000000000000001010110010111001000000000000101011001011100100000000000000000000000000011110011110110000000000000011110011110110000000000000001010001010010000100110010000000000000000000111001011000000000000000000100110010000000000010010000001100110000000000100100000000000000000000000100100000000000000000000000011000000000000000000000000001 (weight 80)
q = 0b1011011110000100100100000000000000000000000000000000000000000000000001010110010111001000000000000101011001011100100000000000000000000000000011110011110110000000000000011110011110110000000000000001101100011000000100110010000000000000000000111001011000000000000000000110011000000000000010010000001100110000000000100100000000000000000000000110000000000000000000000000011000000000000000000000000001 (weight 81)
u = 0b10001000000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000 (weight 3)
E0/Fq : y^2 = x^3 + 10
E1/Fp : y^2 = x^3 + 26
gcd(p-1, 5) = 1
gcd(q-1, 5) = 1

bitlength 394
p = 0b1001000000000000010010000000000000001110000100000000000101010110000000000011001111110110000011100001110110000001111001101110000100011100010101110010010000000100010000010111011100111101100100101010010001000000011101110100000101000101010111110000010101011001111110000010011001000001001000001000000100000000100100001111000000000100100000001100000000010010000000000000000000110000000000000000000001 (weight 123)
q = 0b1001000000000000010010000000000000001110000100000000000101010110000000000011001111110110000011100001110110000001111001101110000100011100010101110010010000000100010000010111011100111101100100101010101001000000011110001100000101000101011110100000010101011010010110000010011100000001100000001001100100000000100100010010000000000100100000001100000000011000000000000000000000110000000000000000000001 (weight 120)
u = 0b10000000000000000001000000000000000000000010000000000000000000000000000000001000000000000000000000 (weight 4)
E0/Fq : y^2 = x^3 + 5
E1/Fp : y^2 = x^3 + 10
gcd(p-1, 5) = 1
gcd(q-1, 5) = 1

Potential curves are searched in a specific hamming-weight-minimizing order for u (with some heuristics limiting the search), so the results are deterministic for a given bit length.

[daira]

In the case of Spartan-opt with arithmetic circuits over Fp and group E0/Fq, we require arithmetic in both Fp and Fq for the verification. However, it appears that the amount of Fp arithmetic needed is quite limited, in particular the number of multiplications (and more importantly, reductions) in Fp for circuit size |C| is O(log(|C|)), even though the overall verification is O(sqrt(|C|)).

See #4093 for optimization of the Fp arithmetic in an Fq R1CS circuit. (TL;DR: it looks feasible.)

[daira]

In order to maximize the efficiency of the recursion, we should have the Spartan circuit batch-verify as many SNARK (e.g. Groth16) proofs as possible, and have the SNARK circuit verify only one Spartan proof. This is optimal because:

• batch Groth16 verification is very efficient in terms of constraint cost (see #3425);
• the O(sqrt(|C|)) cost of Spartan verification means that it is wasteful to use a small Spartan circuit; if we multiply the circuit size by 4 then the verification cost in the SNARK is less than double (because part of the cost is logarithmic), whereas verifying 4 Spartan proofs in the SNARK would cost 4 times as much.

This approach also makes sense to maximize the benefit of the Spartan proof system being universal. That is, we would only need to do one trusted setup for the SNARK to verify a Spartan circuit of a given approximate size (power of 2 limit on the number of arithmetic gates), and could still use the universality of Spartan both at the leaf layer and to optimize the SNARK batch verification circuit.

[daira]

Note that this approach to recursion obtains the security advantages of a SHARK (the two leafmost layers of recursion are essentially the generic construction of a SHARK; alternatively we could use the optimized SHARK construction for those two layers). That is, we can retain the non-pairing-based proofs and be able to reconstruct the rest even if the SNARK is broken, or if there's some implementation problem with the recursion — such as an error in either recursion circuit.

Only the leafmost proof system needs to provide zero knowledge. We might be able to instantiate the non-pairing proof system used for higher layers without zero knowledge, if that turns out to be more efficient.

[daira]

BN curves are always "towering-friendly", i.e. p is 1 (mod 6), which allows efficient implementation of extension fields Fp^k outside the circuit.

p-1 and q-1 are always multiples of 3, which means that cubing is never a permutation in Fp or Fq (several of the proposed circuit-efficient hashes are more efficient when cubing is a permutation). I modified halfpairing.sage to print out the smallest primes r for which r^th-powering is a permutation in each multiplicative group.

[daira]

BTW, a cycle of curves, not necessarily all pairing-friendly, is called an elliptic aliquot cycle [Stange and Silverman 2009]. If the cycle is of length 2 then it is called an (elliptic) amicable pair. So what we're using here is a "half-pairing-friendly amicable pair".

---

Later edit: strictly speaking, the cycles that Stange and Silverman were studying require that all curves in the cycle are reductions of the same curve over Q (i.e. with the same curve equation). In our case we don't strictly need that, and so halfpairing.sage doesn't necessarily construct a aliquot cycle or amicable pair as Stange and Silverman define it. However:

• The class of curves we're considering have j-invariant 0 –since all curves of the form y² = x³ + b have j-invariant 0– and so all curves in the class are isomorphic over the complex numbers (but not necessarily over Q). This means in particular that the possible orders for various b range over a set that is determined by the base field and the endomorphism ring. When the absolute CM discriminant |D| = 3 and p = 1 (mod 6), which is true for BN and BLS12 curves for example, this set is of size 6.
• Tweedledum and Tweedledee in the Halo paper are actually an amicable pair, since they both have b = 5.

[ebfull]

The inner product amortization technique from Halo can possibly allow this half-pairing idea to be much faster than SNARKs over the MNT4/MNT6 cycle; at the very least it should be competitive, which is great for avoiding giant fields.

[bpfarmer]

I would be curious to learn a bit more about the half-pairing recursion approach with pairing-friendly E_1(F_q) with order p and non-pairing-friendly E_2(F_p) with order q. It seems as though the approaches are to (1) use Groth-Spartan, (2) use Groth-a variation of the Halo amortization technique, or (3) use Groth-some other proving system that uses a dlog polynomial commitment/evaluation scheme rather than one based on pairings. Is it the case that the challenges for each approach are the following?

(1) I don't think that there's an implementation of a Spartan prover, and the cost of non-native field arithmetic for the sum check might be prohibitive.

(2) The cost of verifying the amortized Halo checks might be expensive.

(3) It's unclear whether there exists an efficient proving system with this property.

Just trying to get a sense of whether the half-pairing idea is immediately feasible and lacking an implementation or still requires theory, thanks!

[ebfull]

Spartan is a non-starter and I should edit the OP comment to point at Halo. You'll want to use Halo with Sonic or PLONK or Marlin. I am not aware of any theoretical barriers for achieving the half-pairing recursion.

[daira]

@imeckler is actively working on this approach; not sure about the detail of which proof systems: https://twitter.com/izmeckler/status/1203755421053276160

[imeckler]

Currently using a system based on Marlin, instantiated on the pairing friendly side with Kate and on the non friendly side with a batched variant of the WTS scheme.

[bpfarmer]

Oh nice, thanks, we've also been working on something similar in rust, will post here when it's open sourced.

[jon-chuang]

@imeckler What is your progress on using a BN curve on the pairing-friendly side? Since the verification circuit for Halo seemed larger than for pairings, does it truly reap the benefits of a smaller field size in terms of proving and verification times and proof size?

[daira]

@imeckler By WTS you mean Hyrax?

I believe there's a flaw in the poly commitment scheme in Appendix A of the Hyrax paper. @ebfull would know more.

[ebfull]

@imeckler is aware that the WTS scheme cannot be used as-is, and I think he is already using the scheme from the Halo paper which resolves this concern.

The "flaw" is that the WTS scheme effectively takes the polynomial commitment P and the claimed evaluation v and computes

P + [v] U

for some fixed U, and proceeds to use the Bulletproofs protocol modulo the second vector, which the verifier can handle itself. But in a polynomial commitment scheme the prover has arbitrary control of P and can include terms involving U in P to counteract the addition of [v] U at the beginning. In fact, they could commit to the zero polynomial in all their commitments so they can leverage this without even knowing the evaluation points in advance.

I'm not very familiar with Hyrax, so I don't know if this is a problem for them, but it's definitely a problem for us. U needs to be sampled after the prover and verifier have agreed on the commitment P. Hence, we do so in the Halo paper.

[daira]

We're "all-in" on this approach now with Halo 2, but I think this particular ticket is only of historical interest and can be closed.

[daira]

For anyone looking for a half-pairing cycle I suggest Pluto-Eris. It has many of the same engineering advantages as Pallas-Vesta, and it is 446 bits which conservatively achieves strict 128-bit security against STNFS attacks.

[jon-chuang]

I suppose it could be a future "upgrade pathway" for zcash?

[daira]

No, we're using the Pallas-Vesta curves and are unlikely to change, since Halo 2 doesn't need pairings. Pluto-Eris was/is just a personal research project, since I think that approach has merit for further usage outside Zcash (and it's fun).

[wyattbenno777]

This is a great historic thread. Is there any new work on this being done, any write ups, or did it reach its theoretical conclusion?