zkSessions: Ying Tong Lai — UltraPLONK Arithmetisation

Transcript

so this talk is about the ultra plunk arithmetization which is currently used in halo 2. so ultra plunk is an extension of plonk and like any arithmetization it's a way to express statements in the form of relations between variables and once we have relations between variables um that's amenable um to be expressed as polynomials which we can then commit to and once we have a commitment scheme we can instantiate an accumulation scheme so this flowchart is basically what halo 2

is but my point here is actually that if you wanted to substitute in your own commitment scheme and accumulation scheme then as long as your circuit is still using ultra plunk um you can still make use of our library and the gadgets and apis in this talk so the mental model we're working with here is a circuit as a rectangular matrix of values um and we have to specify certain parameters of the circuit so firstly the finite field that it's working over

um secondly the shape how many columns and how many rows it has um and also importantly the polynomial degree bound this is an upper bound on how complex the relations in your circuit can be so right um there are a lot of questions about what exactly the columns rows and cells correspond to so um for each column i that corresponds to a lagrange polynomial a i such that for each row j uh where j goes from zero to n minus one

a i evaluates to um this cell a i j um on the evaluation point omega to the j and omega here is the nth root of unity in your field yeah um the last bit of terminology that's quite special to halo 2 is the column types so i'm just going to list them here and then we'll explain them as we encounter them later so advice columns and instance columns are columns that vary with each proof instance

whereas fixed columns and selector columns they do not change from one instance to another and they're fixed at the beginning of the circuit so they actually form the circuit description um or the statement and um this is the setup or configuration phase of the circuit um and this is used to then generate a proven key and verification key which we can use to generate and verify um all our proof instances yeah and we're actually going to talk about the configuration process first so there are about four parts to

configuration the first is basically assigning values to the fixed columns the fixed cells so over here selectors are kind of special cases of fixed columns so selectors act as sort of on off switches for gates and part two of configuration is gates so you can see here custom gate zero and custom gate one they're being controlled by these selectors um and what a custom gate or what a gate corresponds to is a polynomial constraint that must hold between the cells that are involved in this gate

and oh and these gates don't have to be contiguous they can be pretty arbitrary shapes one thing to note is that um if you if you want to specify a cell in a different row you have to use a relative offset like plus one minus one um and the implication of this is that actually how you order your rows in the upa circuit is significant um and compared to r1cs where the ordering of rows is not significant um the next part of configuration is permutations or equality constraints

so yeah per 0 here is is working over cells and columns a0 and a6 for example and perm 1 is working over a2 a4 so basically what you're saying is that um you're constraining a source cell to be equal to destination cell and this comes in useful when you want to copy a cell into a convenient location so for example if you if for your custom gate um you need a cell to be in this specific offset um then you might want to copy it from

some far away place in the circuit too where you can actually use it and the last part of configuration is lookups so this is basically a subset argument where we are constraining some tuple of input expressions to be a subset of table expressions like for example uh you you can say a6 plus i0 must be a subset of f0 times f1 for example and these values can repeat um we simply require that they appear at least once in the table expressions so yeah that's that's configuration

we're done with configuration a one-time setup um and we can actually now involve the prover so we move on to synthesis and so the priver has this witness that they claim satisfies your circuit and what they should do is assign the witness into the advise columns um and then we also uh deal with the instance columns here so instance columns are used for any elements that are shared between verifier and a common example is public inputs so a proof instance is yes some assignment that

hopefully satisfies all the constraints that we've set up in the circuit description and here's an actual example of a circuit uh layout this is our shot 256 implementation i don't think i'll go into detail here but we've documented it somewhere and and i've put the link in here um yeah you can see configure this is just how it looks in the code test input into your sha-256 hash function

we've also implemented the poseidon hash so this is how it looks as a circuit um yeah you can see over here these are the full rounds and then these are we did two partial rounds in one row yeah the advice columns are on the left and the fixed columns are on the right in selectors and the poseidon encode it looks like this um so yeah the reason why it looks so neat um in the code is because these chips are like basically designed for

circuit writers to compose and they're they're basically modular um pieces of functionality that we hope um circuit riders can simply compose and yeah the the chips um have to know about their own configuration so which columns they use which gates permutations and lookups they set up over those columns and you can have actually a hierarchy of chips sharing the same configuration and a chip's responsibility is to handle relative offsets in a region such that the custom gates are satisfied so and one one level of abstraction

above the circuit is a gadget so oh right actually what i showed these code examples were for gadgets so um yeah these are very familiar apis for example permute initial state pattern at or initialize digest finalize um and yeah for a single gadget you can have multiple chip implementations and you can choose between the chip implementation that you want for those familiar with bellman and lipsnark this is a similar gadget and finally a circuit will make use of

multiple gadgets so for example um file coins proof of replication circuit it does use poseidon and sha-256 um and the final concept here is a floor planner that's working at the circuit level so once the chip has finished all its region level assignments um and within a region you only care about relative offsets um it hands control over to the floor planner which then moves the regions around using absolute offsets in the circuit yeah i think that is all i have um these are the links for

code and documentation yeah thank you so much for the talk