UltraPLONK Arithmetisation, Applied ZK - Day 2

[Music] thank you um i left my laptop on a tram this morning so i'm sorry about the delay so yeah i'm in tongan i work at the electric coin company and today i'm gonna tell you about ultra planck arithmetization so this is a way to represent a statement or a relation as a series of polynomial constraints using planck and using custom gates since coming to devconnect i've actually learned about a whole series of plonkish arithmetization efforts that are like ultra plunk and so at 4am today i decided that i i want to talk about them as well i want to mention them and i want to talk about ultraplank not just in its current state but also in terms of its open problems and its future developments so the standard planck gate is basically what you see here it's one constraint with different selectors that you can tweak so if you set the selectors to certain values you get certain types of expressions so this is an addition gate for example and you can have a multiplication gate as well so ultra planck basically generalizes this idea to let you define custom gates that are arbitrary expressions and we simply combine different custom gates with a random linear factor to keep to keep them linearly independent and then so on each row of the circuit you can choose to enable or disable whichever gates you want so one area of development that we were thinking about is to actually have this randomness be an in-circuit feature so this is an idea by han i don't know if it's here but um for for example we can allow the prover to first commit to certain witness values and then using those commitments derive some randomness to then use in the expressions themselves and in general the mental model of plonkish arithmetic arithmetization is a matrix of rows and columns so each value in the matrix is a field element from a certain finite field um can i get rid of this sorry about that um now what do the rows and columns represent in this matrix each row sorry each column maps to a polynomial a lagrange interpolation polynomial that interpolates to that value assigned at the cell when evaluated at the point omega to the i so omega here is the primitive nth root of unity in your evaluation domain and yeah so each column evaluates to that the cell f x i j when evaluated at omega to the i we have different types of columns in this table so instance columns are basically those contain values that are shared between the approver and the verifier so for example your public inputs will be provided in the instance columns advise columns are where the approver witnesses their private inputs and the instance columns and advise columns change from one proof instance to the next and um yeah they're they're basically what's unique about your proof instance whereas the fixed columns are a different beast altogether they're pre-processed values and they're computed at key generation time by the verifier and these are hard coded they define your circuit and they never change from one proof instance to the next so here's an example of um a custom gate so let's say we have an addition gate q add that checks that these that the cell in a2 is the sum of the cells in a0 and a1 so on the rows where we enable it we we check that this constraint evaluates to zero now the thing about custom gates is that they can have an arbitrary shape so you're able to access values in other rows and you're able to specify an arbitrary offset by which you're rotating your row so if you have a certain shape of gate that's more efficient for your circuit then this is a good chance for you to express that and how we achieve these relative offsets is by making use of the fact that our evaluation domain is over the primitive the powers of the primitive and root of unity and we can simply rotate um by multiplying by powers of omega so from from here we have basically the idea of the custom gate as a template like as a tetris piece and what we eventually want to do is have some kind of macro that describes a gate and if we input into it our configuration so the number of columns and number of rows that we have and we input into it some expression that we want the gate to check we should get out of this macro the optimal gate shape basically right now we don't have a macro like that and um everything is manual and the the developer has full freedom but if we could write some kind of compiler that's smart enough to figure out the gate shape that would save us a lot of effort i've since at devconnect i've learned about a few efforts like this for instance the vampire intermediate representation and also protocol's kimchi so we're definitely interested in basically converging on a standard intermediate representation hopefully so if we if we think about laying out the circuit it's really a question of optimizing the global use of space but at the same time our gates are very local in nature we're reasoning about offsets relative to the point at which the gate is enabled so how do we reconcile these two scopes at the ecc implementation has this abstraction the region that aims to serve as a boundary between the global layout and the local gate so each region is basically a self-consistent block and each region is defined by the fact that it uses the same global offset and what this means is that one region is not affected by another and we can move regions around without without affecting their internal gate logic and this gives us a lot of freedom for optimization so for example our layouter can be authorized to to compress regions um this this layouter on the on your right um basically slides region slides regions up vertically and you can see the the huge the huge efficiency gain we have we basically have reduced our row usage by by half yeah um and a for a further layouter optimization that we want is basically just horizontal packing as well we don't have it currently because that would require the layouter to be able to change the configuration so you have to authorize your layouter to like reduce the number of columns you have for example and right now the layouter doesn't do that yet but it would be cool oh yes yes definitely the colors um so the pink colors um the pink columns are advised columns the light purple columns are fixed columns and the dark purple columns are what we call selectors which are basically just a special case of fixed columns they are binary fixed columns yeah i've tried to stick to this color scheme in like here as well so it's consistent um [Music] yep so the besides custom gates we have another tool which is the equality constraint so these are global constraints that enforce the equality of one cell with another cell so this is a this is the orchard action circuit we have a lot of equality constraints but yeah basically it's just made up of a series of permutations like these and we form a global permutation it's a huge cycle or many cycles yeah and equality constraints allow us to link regions together even after you move them around you can still apply a global constraint that basically lets you copy a value from one region to another and that that's highly useful the final tool that we have is a lookup argument and you can think of this as like a special case of an equality constraint that doesn't enforce a specific permutation rather it enforces just a subset check so over here q lookup is saying that um these two values in a0 and a1 must be a subset of this table the fibonacci numbers and it's perhaps a kind of a technical note over here but for a lookup argument a lookup argument must hold true on every row so on the rows where q lookup equals 1 these values must be a subset of of the table but on the rows where q lookup equals 0 then these two expressions would go to zero zero by default right and if your table does not have the row zero zero in it your lookup argument will fail so when you're writing a lookup argument you have to think about the default case and that's what i've done here i've put in a 1 minus q lookup so when q lookup is 0 we check this constraint and i've put in the default 1 1 value that basically we'll allow the lookup argument to pass on every row yeah so um and if you want to learn more about this stuff at this level of detail you can come to our workshop me and chung's workshop in the afternoon um yeah what what we want from lookup tables that we don't have yet is the ability to make them dynamic to look up values that the approver has witnessed so right now the zcash halo 2 supports only fixed table columns and this is a safety and api concern we basically want to be able to pad the lookup table for you with default values but there are many use cases that require more flexibility and that require looking up values that change from one per instance to the other so yeah we we're definitely thinking about this um and we're we're brainstorming some apis that um make dynamic lookups safe so those are pretty much all the tools you have in out and plunkish arithmetization and using these tools we've built you know many interesting circuits so for example the poseidon hash the sensamiya hash which is our own like in-house hash we've built gadgets for elliptic curve cryptography and an experimental sha256 gadget and all these gadgets are highly optimized and make make full use of the freedom that we have over over the layout of the circuit we also have some great examples from other projects such as the zika evm community edition and they've been they've been able to express the evms opcodes um using ultra plunkish arithmetization and they've also been able to build up a complex structure of interdependent circuits making use of the lookup argument yeah and it's a really impressive effort a lot of the issues and improvements that i mentioned came directly out of this effort some other projects that i know of include dark fi so this is a a private blockchain that allows allows private coordination something like that i just took a look at their repo this morning and i saw like our chips and our gadgets being used in their code and it was really cool another project i know about is orbis which is a zika roll-up on cardano so they're using halo 2 in like a haskelly way because it's cardano and it is very cool to see what they've built on top of just using halo 2 as a back end and that's all i have if if you have some project or use case that you're working on and you want to see if like we can build it just come to our workshop in the afternoon or like talk to me at any time um yeah that's all i have thank you [Applause] cool thank you any questions uh one thing i'm curious about is when will the halo 2 like libraries slash apis be uh or i guess like what is the relative level of stability right now for developers outside uh and about what do you see as the timeline yeah that's a good question right now we're in beta um and we want to do a point release soon um timeline okay uh i'm gonna say the next few months yeah we we've also recently undergone a license change so halo 2 will be licensed under mit apache yeah and that that's going to come with the point release as well so we're working to stabilize our apis um for that release cool i have a related question for someone in the audience hi jen does scroll tech have a solidity verifier for our fork of halo 2 uh yeah we're still working on like a version that can take the uh the the proof like generated by the halo 2 and then just convert it to some verified smart contract using the solidity like it would be like working uh trying to build like some compiler that can take that and then uh just directly output some verified contract but like i would work just we can like keep like update on that and then give out some news like once we have something here um i think that verifier it's important to clarify is for like kzg commitments right whereas z cash halo 2 like barry mentioned there's the arithmetization and there's polynomial commitment um z cash halo 2 uses the inner product argument not kcg yeah and it uses like pasta curves not bn254 so coming out from the discussions that we had yesterday related to ketchup i was wondering if not only for ketchup but maybe in the future for also other cases and like complex circuits that are really hard to optimize for like this kind of constrained language um do you how do you see the future of uh writing custom layouters uh to further optimize your sequence do you think that that would be kind of the way to go for for some kind of circuits or how do you how do you envision that yeah that's a great question um i do envision the future as being like uh a layouter centric future so i think the we should move developers customization efforts to the layouter level the layouter strategy yeah and if we can define the layouter strategy well enough we shouldn't have to think about the minute details of every constraint um yeah we should be able to just concern ourselves with the configuration based on like the efficiency we want the limitations we have and concern ourselves with the business logic but pick a layout or strategy that we like and then not worry about other things yeah any other questions how worried are you about security and do you have any tooling to help with that we are we are concerned about security that's for sure um so the orchard action circuit was audited um independently by q edit um but i think even after the audit we found several bugs on our own and auditing zk circuits is not easy so i think there are a few things that could help with that first of all if we move the complexity to the layouter and we keep the expression or the business logic level human readable firstly i think that would help a lot um but yeah secondly i think coming together with other implementers to figure out like common gotchas and pitfalls and common things that we miss out that would also help and yeah with regards to tooling there is no [Music] formal or mechanized proving that i know of for zero knowledge circuits i i think there's a session today about it yeah so i i would be interested to to find out more as well cool anybody else okay that's thank you [Applause] [Music] you