Cost estimations for IPA wrapped with KZG style systems

As done by Polygon with Fri/Starks and Groth-16, would be nice to know how worth would it be to use IPA for complex and ammortization friendly situations, projects or schemes, and verify the final proof (Decider) with a KZG-based proving system such as TurboPlonk or similar.

Enabling then succint constant and sub-linear verification times. This is particularly useful for projects like the ZKEVMs, rollups, Proof of Validity of a chain etc..
Where we might have no constraints or limitations for the prover but we have a restricted envoiroment where we must verify the proofs (like the EVM).

How we got here?

Well, the first impression that we had was that why not using Pluto-Eris curves which have a cycle (so we can recurse with them) and where Pluto in particular has a Pairing too?

The curves have a larger field-size than Bls12-381. (446 bits to be exact). This will imply slower operations for all algorithms such as: ECDSA, ECDH…
Proof sizes will become bigger. Same with SRSs, key pairs etc.. Prover requirements in terms of computation and memory will also increase accordingly.
More importantly, there's no formalisation yet for Triton (the curve that operates on the Pairing field
$G_{t}$ ).
Also, there's still no implementation for the pairing itself. See: https://github.com/arkworks-rs/curves/pull/54

So, at least for now Pasta curves seems a much better option. Even it lacks the pairing and that is really painful, it has other attractive properties such as the ones noted in the Pasta curves blogpost^[1]

Unlike with the Tweedle curves, both Pallas and Vesta have low-degree isogenies (both of degree 3) from curves with a nonzero j-invariant. This is useful when hashing to the curve using the “simplified SWU” algorithm, and perhaps for other not-yet-known purposes.
They have the same 2-adicity, 32, unlike the Tweedle curves that had 2-adicity of 33 and 34. This simplifies implementations and may assist in square root performance (used for point decompression and internally to Halo 2) due to a new algorithm recently discovered; 32 is more convenient for this algorithm.
They are both constructed over 255-bit prime fields. This gives 126-bit security against Pollard rho attacks, and allows the compressed representation of points to be an even 32 bytes.
Both moduli have sparse bit representations in order to improve the performance of Montgomery reduction and other common operations.
They both support an endomorphism that can be used to improve performance of scalar multiplication, similar to that available for secp256k1. This is even more useful after the recent expiry of related patents.
They have the same curve equation,
$y 2 = x 3 + 5 y^{2} = x^{3} + 5 y 2 = x 3 + 5$ . For curves using this cycle construction it is also the case that an x-coordinate of zero is not valid, which allows a convenient representation of all zeroes for the point at infinity.
Both fields do not have 5-order, 7-order, etc. multiplicative subgroups, so that exponentiation by these small primes is a permutation — a crucial requirement for algebraic hash functions such as Rescue and Poseidon.

Aside from these, there are other factors that influence this line of thought:

Pasta curves have been in production in Zcash since Nu5^[2] without any kind of issues and no reported vulnerabilities after multiple security audits.
Halo2 proving system with it's slightly modified IPA version with a custom accomulator scheme has also been tested for some time without any issues and has passed several security audits.
They both have rust implementations^[3],^[4] which are actively mantained and used widely across the ecosystem.

The idea per se.

We have a Virtual Machine(VM) which serves as a way to execute all the state changes performed on a blockchain to which we want to add support for KZG-based proof verification (pariring checks).

We also have an application like a Rollup or similar which consistently aggregates proofs for Txs, Blocks or whatever. And from time to time, wants to commit this to a big chain like Ethereum, Cardano, Zcash etc..

The application uses Halo2 with IPA and the modified accumulation scheme. On that way, it is capable of aggregating proofs until the decider needs to be validated.

NOTE: For context, from a really high level prespective, with the Halo2 IPA version, when aggregating proofs and recursing, we only aggregate the sub-linear time checks.

The linear part of the proof verification which is O(N) usually called `Decider` corresponds to the latest verification performed which indeed verifies all the other ones.

So what that means is that in the Plonk/Groth-16 proof, we will need to verify the IPA Decider (linear part of the accomulation scheme argument).

This implies that we need to construct a circuit for Halo2 that verifies a Multiscalar Multiplication/Multiexp of N items where

N = n e x t_p o w_t w o (I P A_P R O O F_C O N S T R A I N T S + 1)

Notice we don't discard here the possibility of using IPA/halo2 verifier with Pasta curves directly in the VM.

By simply computing using the halo2_cost_estimation tool it's easy to see that until we don't surpass the 2^24 constraints aprox, the speed verification isn't critical.
We've checked this by estimating 2^16 and 2^20 Degree circuits with maximum gate degree of 4 (which is decent enough) and 3 advice columns.

2^16 constraints

cargo run --release --example cost-model -- -a 0,1 -a 0 -a-0,-1,1 -f 0 -g 4 16
    Finished release [optimized] target(s) in 0.05s
     Running `target/release/examples/cost-model -a 0,1 -a 0 -a-0,-1,1 -f 0 -g 4 16`
Circuit {
    k: 16,
    max_deg: 4,
    advice_columns: 3,
    lookups: 0,
    permutations: [],
    column_queries: 7,
    point_sets: 3,
    estimator: Estimator,
}
Proof size: 1760 bytes
Verification: at least 91.174ms

2^20 constraints

    cargo run --release --example cost-model -- -a 0,1 -a 0 -a-0,-1,1 -f 0 -g         4 20
   Compiling ff v0.13.0
   Compiling group v0.13.0
   Compiling pasta_curves v0.5.0
   Compiling halo2_proofs v0.2.0 (/home/kr0/Desktop/HDD/dev/halo/halo2_proofs)
    Finished release [optimized] target(s) in 5.60s
     Running `target/release/examples/cost-model -a 0,1 -a 0 -a-0,-1,1 -f 0 -g 4 20`
Circuit {
    k: 20,
    max_deg: 4,
    advice_columns: 3,
    lookups: 0,
    permutations: [],
    column_queries: 7,
    point_sets: 3,
    estimator: Estimator,
}
Proof size: 2016 bytes
Verification: at least 1176.901ms

That, is only possible if the VM works directly in the field of these curves of course. Otherwise, bignum arithmetic or field simulation is required which may blowup the gas costs. (There's alternatives to that such as precompiles or host functions. But this is another discussion).

Wrapping up the Decider into KZG

Based on the results obtained in ZKEVM Community Edition the pippenger implementation of multiscalar multiplication necessary to execute the decider takes 19k constraints per term in the MSM.
This result is obtained using wrong field arithmetic to emulate non-native curves. We could expect a better ratio of constraint/MSM term when using a bigger wrapper curves such as Bls12-381.

In any case, 19k

\approx 2^{14}

so the verifier circuit for a moderate sized cicuit of

2^{16}

constraints would go up to

2^{30}

which is already problematic for the prover. Even if prover resources are unlimited, Bls curves can only fit circuits with up to

2^{32}

constraints.

Further reasoning and exploration has to be done here but requires us to take a deeper look to https://github.com/zcash/halo2/issues/249 & Aggregation strategies.
For example, there might be a smart way on which we can accumulate differently so that we take a bit more penalty during recursion but at the same time, we get benefits when we need to prove the Decider.

Questions for the future

What other accomulation schemes can we apply alternatively that benefit this usecase?
Are there any provers actually digesting 2^30 constraints and being performant enough to be used in production?

Some helpful threads to pull from and adquire knowledge are:

Cost estimations for IPA wrapped with KZG style systems

How we got here?

The idea per se.

NOTE: For context, from a really high level prespective, with the Halo2 IPA version, when aggregating proofs and recursing, we only aggregate the sub-linear time checks.

The linear part of the proof verification which is O(N) usually called Decider corresponds to the latest verification performed which indeed verifies all the other ones.

Notice we don't discard here the possibility of using IPA/halo2 verifier with Pasta curves directly in the VM.

Wrapping up the Decider into KZG

Questions for the future

References

Read more

Summary on A short note on PQ-Verkle

A short note on PQ-Verkle

Privacy-preserving & secure web-search

Privacy is power.

The linear part of the proof verification which is O(N) usually called `Decider` corresponds to the latest verification performed which indeed verifies all the other ones.