ZK7: Latest developments in Halo2 by Ying Tong Lai

Transcript

[Music] for now i want to introduce ying tong from electric coin company who's going to be telling us about the latest developments in halo 2. [Music] hello hi i'm ing tong i'm a core engineer at the electric coin company and yeah i'm bringing you the latest developments in halo 2.

so the halo paper was published in 2019 and we came up with halo 2 in about 2020 that basically replaced sonic with plonk and ever since then we've just been implementing it we've been learning um we've been finding mistakes and bugs and we've been seeing adoption in other community projects such as the zika evm and so i'm here today to share what we've worked on and what we're looking forward to so an overview of the halo 2 proving system is basically in these seven steps and we probably won't have time to go

through all of them i'm going to spend the most time on the first step and the last step because these are the ones that we've basically found the most interesting and the first step is the arithmetization this is a topic that has been discussed in previous sessions such as kimchi and vampire and um yes and i know this is like this seventh or eighth time we've seen the vanilla planck constraint i show it here to demonstrate that basically it's a single constraint whose

selector values you can tweak in order to express different constraints so you can tweak it to be an addition expression or a multiplication expression and this is a different paradigm from ultra planck ultraplanck introduces custom gates so for each expression you can define a bespoke gate and then later on you can linearly combine these gates with a random with powers of a random challenge and um we we visualize ultra planck in this sort of matrix format whereby um each gate can be enabled or disabled on

a row um in the matrix so how how um ecc's ultra plunk differs from kimchi or vampire is we basically expose all the degrees of freedom to the circuit rider and we make it entirely customizable and so the the mental model of our circuit is very visual it's rows and columns and the circuit writer has full control basically over the configuration and over every single assignment in this matrix

[Music] so we we we know we know this already each cell contains a value from a finite field and each column corresponds to a lagrange interpolation polynomial that evaluates to that cell's value at omega to the power of i where i is the rho and omega is of course the primitive nth root of unity it's our multiplicative subgroup so because we expose so much freedom in the circuit configuration it's important to understand the different types of values

that go into the circuit so we have different kinds of columns the first kind is the instance column and these contain values that are shared between the privilege and verifier for example public inputs the second kind of column is what we call the advise column and these hold the previous private witness values so the instance and advice columns change with every proof instance whereas the last type of column is the fixed columns and these are pre-processed at key gen they define the circuit and they're hard coded and they never change so i'm going to show an example of

an edition custom gate that basically concerns itself with those three advice columns on the same room and with ultra planck you have the freedom to define the shape of your gate so for example if i wanted to access an offset in the next row or the previous row i could specify that in in my constraint and i'm as the circuit writer i'm responsible for choosing the shape of my gate that is the most optimal so for example in z cash's orchard circuit we've had multiple gates shaped such that we can stack them

and pack fully pack the circuit and we all know that how these offsets work is simply by shifting um the evaluation point um by um omega the primitive and threat of unity so yeah now this this introduces some kind of tension because on the one hand we need to think of gates locally we need to think of them in terms of relative offsets but on the other hand we want to lay out our global circuit as optimally as possible and we want to

automate that layouting laying out process as much as we can while while retaining control over the local offsets so to to deal with this tension we've introduced the abstraction called regions and what a region is is basically a self-consistent block a self-consistent area of assignments that are defined um relative to the same global offset so you can think of it in terms of um all the cells in a in one region share the same zero and what this means is that

one region is independent from another meaning that if i'm within one region i'm completely unaffected by offsets by gates by assignments in in the other region and i can basically move regions relative to each other and rearrange them and pack them however i want without worrying that my gait assignments will be affected [Music] so but this region abstraction introduces another problem which is how do we maintain some kind of link between regions if we're moving them around freely

how do we still ensure that values across regions are consistent with our constraints oh before that i want to show why being able to move regions freely is good so what it comes down to is your layouter strategy we're giving you the freedom to move regions and how how are you deciding to move them so this is our symbol layouter that just lays out regions one after the other as the developer assigns them whereas this the exact same circuit the exact same regions

this is our dual path layouter that does the first pass to get the shapes of the regions and then the second pass to vertically pack them and this just this one change in our layout strategy reduces the circuit by an order of magnitude by a power of two and this reduces like your ffts this reduces everything um so the the power of the layouter and the region it it gives the circuit developer so much freedom and so much freedom to optimize so yeah but as i was saying between regions we still want to maintain some kind of relationship some kind of

consistency and what you see on this diagram is all the equality constraints um in the orchard circuit that are tying one cell to another so every every line there is basically an equality constraint and forcing that two cells have the same value and with equality constraints you can then link together cells from different regions because equality constraints are global and they will they will be enforced even if you move regions around the last sort of setup in our ultra

planck circuit is the lookup argument and this is basically um this is basically a relaxed version of the permutation it doesn't enforce a specific permutation but rather it just enforces a subset argument so for example here we're enforcing that values in those two columns are a subset of values in our in our fixed table and one nuance of the lookup argument is that it has to hold true on every single row so when the lookup argument is not enabled zero

we need to actually look up a default value in the table so that the lookup argument still passes on that row [Music] and it's come up in certain talks before right now um in right now in our implementation we only support fixed columns for lookup tables and this is a decision um this is a decision we made for safety basically we if if the lookup table is fixed then we can pre-fill it fully with a default value however

our partners have come up with use cases that actually require dynamic lookup tables it requires basically the the ability to look up witnessed values as well and this is one of the areas we're actively working on in this issue we're writing up an api so feel free to contribute if you have opinions so yeah the the sensamia gadget is one example um where we heavily use uh the lookup argument to basically look up fixed generators that are used in the sensemia

hash function and what you see here are printouts of the gadgets we've written we've written a gadget for the poseidon hash function as well and elliptic curve cryptography as well as the an experimental sha256 chip so the point of these gadgets and chips is that they are meant to be reusable they are meant to be modular and we we do want them to be primitives that um our other projects can consume i do want to mention that the ecc circuit in particular it makes use of lots of manual optimizations so

for example for fixed base scalar multiplication uh we actually witness the coefficients of a lagrange polynomial that interpolate to the x-coordinate of the fixed base so this is an example of a non-trivial optimization that could only have been done with direct manual control over the circuit um and if we were to explore moving to an ir perhaps we could encode this strategy as uh one rule or an alias in the ir yeah but currently um

we've made full use of the freedom we've been given in the api and we've fully optimized the orchard circuit so that being said we are actively exploring moving to the next phase of this api so we're looking at dsls and we're looking at irs um there's an issue yeah add an api to construct a halo 2 circuit from a set of constraints so strat just wrote that issue um proposing a strategy to integrate halo 2 with vampire and yeah we are always trying to just

improve the floor planner ergonomics and make make our apis more usable so if you have wish a wish list or features that you would like to see just come talk to me or open an issue on our get up so our arithmetization has been used in the zk evm community edition project and basically we found that yeah our arithmetization has been expressive enough to support evm opcodes and it's been expressive enough to do

things like switching [Music] on gates and also to to enable linking different sub circuits um through lookup arguments so yeah i think scrolltech gave a great talk about the zk evm community edition earlier and i encourage all of you to take a look and basically i've i've been inspired by how they've taken this api and pushed it to its limits and there are lots of great um optimizations coming back from the zkavm project so optimizations like

introducing a multi-round a multi-stage prover meaning that the prover that can actually uh commit in the first stage and query randomness in the second stage um [Music] they've also introduced various optimizations like at low level like fft assembly so it's been a great collaboration with the zika ibm project yeah so that's our arithmetization um how am i doing on time [Music] i have i think you have like eight minutes eight minutes okay um eight minutes in that case

i'm going i'm going to skip over the intermediate steps um these steps are describing how we go from our polynomial constraints to basically some polynomial that we can put into our inner product argument and the inner product argument um so up to this point um we've implemented all of these and this will be deployed in our next network upgrade so our inner product argument is what we use to construct an accumulation scheme

and the accumulation scheme is how we achieve recursion so halo 2 is a recursive proving system with no trusted setup but the recursion part of halo 2 will not be in our next network upgrade so we are currently implementing the recursive api the the inner product argument is amenable to an accumulation scheme because it has a cheap check and an expensive check and basically at each at each accumulation step we only perform the cheap check and we delay the expensive check to

the final decider in effect we amortize the expensive check across a whole series of cheap checks and the accumulation scheme where i don't know if people here are familiar with ivc incrementally verifiable accumulate computation let me put my glasses on so yeah an ivc basically an ivc proof consists of both the snark proof and an accumulator and the first of all we compute a state transition the state transition function

that's the application logic of our snark then we accumulate the inputs from the previous proof instance into our accumulator and we produce a new accumulator and this is the job of the accumulation proverb and we also have an accumulation verifier that's checking that the accumulation was done correctly so the the accumulation verifier and the state transition function are what we call the are what we prove in the snark prover and

um the proof of those two circuits gives us our next proof instance pi i plus 1. so we continue this [Music] for as long as we want until we reach the final stage which is the decider and this decider d is what's going to perform the expensive check the expensive check is basically the check that our accumulator that we've been just providing thus far is actually well-formed um and also in our final with our final decider that's a snark

verifier that runs the final snark verify that that checks the final snark proof so with this ivc scheme planning to we we we're planning to apply it to filecoin and we have a collaboration with filecoin that's um underway right now so filecoin basically has a problem with they have too many proofs um on chain so for each sector each file coin sector um they need 10 snarks right now it's growth 16 proofs they

need 10 gross 16 proofs to prove one sector and basically there is a limit to how many of these girls 16 proofs you can stuff into a single block so they're running out of space in their blocks first of all and then secondly even if you could put it all into a block you would run out of time or you would run out of gas trying to verify it so we need to cut down on the proof size and we need to cut down on the verification time so the plan is to accumulate all these proofs into one recursive proof

and then just submit that to the block and we only need to verify one proof yeah that's all that's all i have thank you [Applause] great talk are there any questions oh yeah we got one hey uh great talk i had a question about the last slide so if they have graph 16 proofs how are they using the accumulation with those oh yeah now that's a great point so right now filecoin is rewriting their circuits using halo 2. okay so they're these are not gross 16 proofs anymore

they're halo 2 proofs all right yeah anyone else have some questions i guess another question about this slide and so you're replacing 10 growth 16 proofs with a single um halo 2 proof at the end right so like how much space are you saving by that like how much smaller is the single halo 2 proof versus 10 growth 16 proofs yeah that's a great question so i think right now filecoin has deployed um something called snark pack yeah which actually already does proof aggregation

um but they even even with snark pack they run into a limit to the number of proofs they can aggregate whereas with halo 2 it's like basically unbounded yeah makes sense yeah very cool anyone else i think if not then thank you so much yeah cheers [Music] [Applause]