Halo 2 - with PSE, Present by CC Liang
Learn & Share with PSE · 26 Aug 2022 · 1:00:07
A research presentation on Halo 2 - with PSE, Present. The session explains the construction, its security or performance properties, and where it fits within modern privacy and proof-system research.
Speakers
Topics
From Learn & Share with PSE, hosted by Privacy Stewards of Ethereum.
Transcript
thank you charlie hello everyone thanks for coming um today i'm going to talk about a hello to overview and [Music] yeah so um thanks for coming uh so i assume like like uh most of the audience comes from the uh circum background and uh and probably learned uh learned about how to and and want to explore it and today i'll give a very high level
overview to lower your barrier of entry and yeah and for this talk i i didn't like do a lot of uh like fact checks that uh to the degree that i'm comfortable uh it's mostly from my brand dump and if i missed something or like uh didn't mention your uh your your contribution or some people's contribution
uh the errors are my and um and please let me know i'm very uh sorry for that so some uh basic info about me uh you can call me cc i'm working on a zkevn project uh with austria ash berry carlos david i do marios mihanik and owner into and many others people from scroll tech and lubrin and many uh external contributors and about zkevn the goal is to build a sustainability proof for the ethereum blocks
and it has uh two main usage one you can scale l14 nodes with the proof so the funeral can verify more computations than it can now so that means more transactions and more gas for compilation and the second usage is that you can use this validity proof to build the l2 zkro app that is ethereum compatible and to do that we need a tool to build such a validated proof circuit so uh we use hello too
it is developed by the electric coin company okay z cash team and it's now released in uh mit and apache 2.0 so feel free to use it and uh it can build plunkish circuits um what we mean by plonked circuit is uh it contains the um the probing system of the plonk paper and uh custom case and lookups and uh that's the core of our talk i'll i'll talk about that later and uh pse we we have a fork of halo 2.
we did some customization that that that works uh for the uh z k uh for for the zken project so uh so the first uh first half part of the talk i'll be uh talking about some differences first you might be very curious about what's the main difference between hero2 and circum so in circum you can build circuits and that use the growth system or plonk
um but in how to um it's a it's many plonk and but with uh extra support of a custom gate and luca arguments uh this is what makes a punk system powerful and uh in second you can you do you can you can um use prong too but um like we say that it has no custom can look up arguments as far as i know but it gives you the universal setup benefit mobile data the arithmetization
scheme is um plonk has uh itself has a very special arithmetization scheme um the average arithmetization means that uh you have to turn your application logic uh into uh multiplications and additions uh those kind of uh arithmetics uh unlike you when you program in your usual language like uh pythons or uh rust you you build your application logic with if else with for loops with those kind of things
but in uh to build a circuit you need to turn your application logic into numbers adding together multiplies together so that's that's what arithmetic hydration means and uh circumvents r and cs and so um this makes uh when building hello to circuit and circum we need to have very different mindset and uh can we verify a proof in solidity uh in circumless like you can done it
from the since beginning but uh how to uh there are some prototypes and uh i hope so we can we can do it and uh if you are interested in this part talk to me and uh how do you uh build circuits in circum it's a domain specific language it has a language that looks like javascript and you you build a circuit using their language but in halo 2 it's all rust api so you need to compose your circuit with that api that's the big
developer experience difference and question oh sorry okay the difference between punk and growth 16 yeah it has a different algorithmization scene and the trusted setup the plan is universal that means you can reuse the phase one trusted setup and apply it on different applications but growth system is application specific when you build a new application you need to do a phase 2 chassis setup if you want to change some circuit code
in your application you need to do another phase 2 transit setup so plonk is a little bit more convenient proof size growth 16 has minimal uh probe size uh planck is larger and depending on what gaze you use and what planck can give you is the it can improve the average magic operations with custom case it can improve the bitwise operations and branch check with local arguments and uh for groceries thing if you want
to do like big wise operations uh you uh it it uh it takes a lot of constraint um to build that uh so that's why like uh usual hash functions like uh catcard or or shop256 uh it's uh very expensive to build in uh growth 16. and the difference between the pse fork and the dk shot string is that uh for example supported curves are different they can shut screen use password curves and pse fork we want to support bn256 curve uh we want this curve
because it can we can verify this curve using ethereum's uh pre-compiled contract the the ethernet has a pairing contract and it currently supports a bn curve um the problem scheme uh z cache is in a product argument and we the the pse fork use uh kcg commitments and uh also a strong optimization and zero knowledge uh for the cache uh privacy is the uncompromisable default so uh circuit always comes with zero
knowledge and um for pse fork sometimes we want to explore scalability more so we want to make it optional and there are also extra features like uh gpu or memory optimizations by uh scroll and break from low ring and we have processing transcripts we have evm verifier supports and in our circuit report there's a constraint builder they can build very complicated circuits but with more abstractions so
any questions so far okay uh oh sorry okay so thank you um so now um let's talk about some uh household basics so in how to um [Music]
you have to uh think in the agree agreed of columns and rows and cells uh like excel spreadsheet and the column is a polynomial and a row is it's a like the rules of unity is like uh x coordinate and the cell is the evaluation um of the polynomial and that rules of unity but um i think this information is uh more useful if you want to know how it works uh behind the
scene but um generally speaking uh more column is more costly because you you need to have more uh kg opening for curves and if you utilize uh more cell more rows uh more cells uh it's more cheap because they are all in same polynomial and and it's um it's basically free and [Music] uh here uh that at the right hand side you can see uh this is a circuit uh you can print out with uh hello2
this circuit has four columns the red the red columns are advice columns it is uh you fill in the cell approval fills in the cell cells when uh in the proving time and at the right hand side there's a this bluish purplish column it's fixed column and you assign the value at a compiling time and the green green cells are the cells that has a values field and there are also instance columns i'm not showing here
it's a public input and uh fill in those public values at the proving time and uh the red uh reddish uh pinkish advice columns they like private values and okay and in in how to you have three building blocks to build your circuit um one is custom gates one is look up gates and one is the copy constraints we'll go into them one by one so a custom gate is
expression that cells in the gates must hold for example you can have a custom gate that reference to a column a to a column b or current c you can reference to the uh current cells at the current row you can reference to a cell at the previous row or next row they come in with the extra cost but that's what you can do you can even reference to like 20 20 rows later and you uh this uh this gate will apply to
the uh to the every rows of the uh of the of the circuit and unless yeah but you you always need to define a selector the selector is zero or one and so when it's one it means we need to enable the the check for that expression to hold but if it's zero then we we don't want to check the expression at that particular row so so for example this is the expression uh we defined we want
the selected particle row times the expression on the right hand side to be zero so um if the selector is zero then uh no matter what the right hand side is it's it's always zero but if the selector is one and then the right hand uh then the right hand side must be zero so the a a minus b must equal to the b next so uh so this is how how you um define the custom gate you choose cells and define the selectors and define that equations and make it zero
for example this is the fibonacci example i borrowed from inktones ripple fibonacci series is a series of start with one and one and then the next one is the addition of previous two for example two is one plus one three is one plus two five is two plus three so um what we can do we can define uh three columns left right and sum and then fill in the previous two values and and add the sum at the
the next column we can define a custom gate that takes the current cell of the left column at the current cell of the right column and take the current cell of the sun and we want to uh we want we defined a selector called cue fit when it's one that means the gate is enabled in this row and it never in this row in this row but not in the last final row and so uh so we we are able to uh check uh the circuit in this way uh note that we we still need a copy constraint to copy the
thumb to the to the right and some to the left um but uh but uh the emphasis is the the custom gate now and uh this this is not the only way to uh define custom gate for this particular circuit you can also define a custom gate like this we can use the um left right and the next cell of the right so the the next cell of the right must equal to the left class the current cell of the left plus right so um
here we reduced one column but we we we add another uh cost of opening the next sale so so this is a custom gate and uh the other uh powerful uh component for the uh header two is the lookup argument and the logar argument uh is useful to do a range check and bitwise operations uh so to uh to define the lookup argument um yeah you still need a selector and the current current cell at the
advice columns um and then you give a column of a rent of the table you want to look up this is a range check so for example i want to check if the advice value is between 0 and and and 7. so so we can define the range table it's a fixed column it it has value 0 to 7 and then a network argument can check that if that selector is enabled in the first three
rows then the three first three cells in the advice columns must be in within that range there must be a corresponding value in the lookup column equals to that advised cell for example 6 is 6 exists in in the range table here 2 exists in the range table here and four exists in a range table here and if you win at something like nine then the lookout will fail so this is uh used for a building wrench check
if you think about what uh how to do it in in silicon it would be a huge pain and the other useful thing is to build a bitwise operations you can you can define two lookup columns and that has like uh a x or b the value of x or b and they must equal to the the the xor's result so let's look argument and the final component is the copy constraints um
the copy constraints uh bind uh two cells so that their values might must be equal to each other um for example if uh this this this cell value is 100 the other must be 102. um it's the cheapest constraint and and use as much as possible as we can and yeah so so that's some uh that's the three basic uh building part for the uh for the header two circuit so uh i gave some uh one like a real um like
example example code so um so usually like you want to break down your um application logic it might be very complicated for for example a decentralized mixer you have like hash you have you have a like identity commitment different components then you you start by defining like configs for the individual components it contains the selectors and columns interact with then we defined a
constructor and that has the and that defines a custom gate or lookup gate inside you can see this expression it creates a gate and then it queries the lectures and query advice column at the current cell and there are some other expressions that might form constant from fixed table or instance table and then uh once you down uh so so uh yeah the first part is defined a gate and then the second part is define an api of how
how to assign values to the cells so uh in this um in this assign api you enable the selector and then you assign the value into the advice column at um is uh you specify a name suppose uh specify a column specify which rows is that uh it is called offset it's offset uh relative to some region so you don't need to remember the absolute
row of the of the circuit it it you just specify the relative position of that of the rom and the dummy is uh um the value to fill in now that the approver and the verifier then runs the same assignment assignment api but the difference being the approver run this to assigns the sale and also the values in the cell but for the verifier verifier only assigns the cell but if it's a fixed column it
assigns the value too but for the advice columns the uh verifier has no way to know um know the value at a uh at the compiling time and it makes make no sense for the verifier to know the actual value so this value has like um two outcomes one is a non-value one is unknown value so the uh the the verifier uh when whenever arrived runs the assigned device the verifier does not assign the value to the cell
and then uh you start a compose some like parent config and like organize your subconfigs in that parent config then finally you uh design define a circuit trade um so so this uh circuit trade you need to define a config here uh the eq1 config we defined in previous slides and then you create columns here and then there's a synthesize you run the assigned api finally you
you can use the mac prover to verify the verify the code so um this uh this my circuit is it is for poorer to run it it gives a known value oh sorry and then you uh you select the polynomial degree uh this determines like how many rows you can use um usually you you might choose like k equal to 16 so it means you have 216 rows you can use but like in our example circuit this is a very tiny circuit so three is enough
and then you run the mac prover and run the verify then then this is uh this is usually used in testing but like in in a real production you you there is another uh real purpose drug but you still like uh a like building that sends like similar arguments in into that uh into that structure yeah uh so yeah this is uh uh give you that um a glimpse of how the depth experience of the halo 2 looks like and
there are some advice here but i don't want to go through all of them until you you really really really tried uh really stuck in there there i i just um write them here as a as a full note uh so yeah that's the end of my presentation any questions yeah i've got one um so the pse team swapped uh bn or i guess
the pasta curves for bn254 um is there or do you want to talk a little more about why that decision was made uh yes so uh because like eventually you want to um like like we want uh like most of our uh application we want to uh verify the proof in ethereum and uh that uh the choice of the curve matters because like the
um we have a pre-compiled contract um on ethereum that's the only uh verified uh bn uh 253 uh 6 or 254 uh curve and uh there are plans to um support like uh like bls 12381 in the future but um bn256 is what currently works so so so that's why we choose uh the bn curve that's um that's a curve that you can verify it in um on ethereum today like like
almost all our projects and applications use a bn curve so that's it makes sense uh or do you want yeah so i guess then my my real question is the flip side of that um the pasta curves um what is there to be gained by using them if um the decision was made to kind of just switch back to bn254 for um like compatibility uh so passer curve is uh uh specifically uh specifically built for uh the z cache applications um
okay i don't know much about pasta curve but like it's uh essential for the um for the recursion proof that required uh by the dks uh the cash client um or or uh the the problem scheme yeah the the cyclic so if i wanted theoretically to build something recursive i would need to use pasta or could i still do bn254 um i think you have to do pasta okay that's good to know thank you
okay um which table yeah sure so i guess if no one else has got
anything um uh the other thing that's really kind of crazy is optional zk um personally i'm a little more motivated by the scalability anyways um how is is that just kind of you take all of the parts that go into the algorithm and then you strip away the zero knowledgeness part and it all still proves like that it exists and you can use it so okay uh the the dk uh for the pancake system is actually adding
uh blinding factors at the um end of the rows uh roughly speaking um so uh to make it optional that means we want to uh remove those blending factors and um like adding more uh rows at the edit a button of the circuit uh not sure if that answer your question yeah totally um does it is it as efficient like in that it looks like it's 20 or 30 percent uh but that's like visual it how
efficient how much more efficient is it to omit the blinding factor if that's something you know off the top of your head uh i i actually have no data off this so yeah little okay very cool anyways thank you that definitely did clear out um
oh good question um i actually don't know the detail um the but like the the bottleneck um i think that the bottleneck of the proof uh specifically specifically on zkvm uh is is that we use a lot of memories like um like 100 or 200 gigabytes and and uh so so it would be like a
more uh more more efficient or to reduce our uh like cost of computation by like optimizing the memory or like if you can use gpu to uh speed up the proof that means like in in the in in zkrov you can create a proof faster and yeah that that uh so you can uh if you can create a proof faster that means you can uh finalize the transaction faster
that makes sense again so
how do you do the push to talk better yeah i'm looking up the key now it's in user settings and i had to set up my own binds oh it's not on by default there's not a default button yeah okay i will turn voice activity back on anyone should be able to ask a question
now yes another
yeah sure wow [Music] the oh sorry i think we started pkevn since uh one year ago and yeah and and like uh i think i've been in in pse for like two more years
uh at first like i helped um some semaphore projects and messy projects and then the hubble ultimate cigar and then the ckvn oh yeah
yeah i've spent the past month uh going down the rabbit hole asides from all of it um it's it's definitely a big leap from sircom you really have to understand uh the the fundamentals of the math going on whereas you can kind of fake it with circumstances hello thank you
i just want to give him a chance to ask if they i don't want to like dominate the i have a ton of questions but uh yeah if anyone has questions please interrupt me um but um i guess i'll fire off one more question that's pretty related to what i'm doing um so we built uh the we built privacy preserving proofs in circom for a battleship game and uh eventually we wanted to be recursive so we had to switch from circum to halo to even accomplish that but now we're back to square one with the proofs um and right now uh we have a 10 by 10 board which is basically
their binary zero or one and what i'm trying to figure out right now is whether i should have a region um i think that's the right way to refer to it like a region that is uh 10 by 10 cells or i should have just like a single cell that i then like extract out as a bitmap um within the code and then work with it that way i'm wondering if you have thoughts on that uh how how do you uh verify the yours your proof um
like what constraints do i place on it uh no i mean oh uh okay yeah yeah let's talk about like like uh what what kind of uh like uh validity condition you need to check like like what what makes the um like selecting a sale valid so there's a range check that make sure it's makes sure it's between um inclusive zero and nine um and then there's also some more custom logic that makes sure uh there's an x and y and then a z because it's like
battleships you start from one spot and extend based on the ship's length um so then we have to check basically if in this 10 by 10 grid any of those placements overlap and we want to prove that basically all of once we've placed them all uh all the cells are still um now that i'm actually talking about it we do probably want it to be cells yeah so you would want to check though that once you've placed them all down they are all still binary none of them are like two or three possibly um but yeah if that makes sense yeah that makes perfect sense so
yeah and and how do you need to make a like a commitment to like for example uh hashing all the grades together to get a public input yeah so that's um the very first step of of playing this game um is to commit to a certain board state so essentially exactly that whether we run it through like poseidon or um we're looking at like cincinnati because that seems to be popular with halo halo 2 but yeah
oh okay so so you just uh like encode the the board as a like binary string and then and then um or maybe like you know as a field element and then and then run poseidon or something to commit that okay oh and that's that was a question yeah i mean i i think actually almost talking through it um because a lot of what you showed with like the visuals um for some reason it just looked a little
more um with how the cells work but i i think that um it might not be possible like to like it would be the best idea to have uh 10 by 10 cells um to do this check rather than having it be a single cell oh okay and i i guess um yeah if you if you think that's uh the wrong idea please let me know but otherwise i think i'm gonna go forward with that yeah i think that generally makes sense and
yeah uh yeah just thinking uh like uh okay but like uh when you when you want to do a placement of the ship then you only need to uh like select the cells that um for example your ship has a text for sales on the checkboard and you only need to check that for sales that's not like having a value uh two or more right so i could potentially not check every
single cell is what you're saying uh yes yes that was okay because i did that with the previous one i did have to check every single cell okay that's very cool that that would be a material like upgrade to show to it oh glad that's helpful yeah thank you so much thank you for sharing me your project yeah i hope to share more soon hi hello
can you tell me yeah oh okay this is a great talk i have one question what's the transformation i take when i write a circle using hello tool and what are the main considerations thank you uh sorry i i didn't get a question one can repeat my question what's the trades format should i take when i write a circuit using halo 2.
trace format trace format uh what's that price moment what such as i want i want to let my friends yeah if you if you feel more comfortable in mandarin i can translate it for you can ask big chinese
yeah yeah yeah yeah yeah feel free okay okay okay just yes uh wait me a minute yeah sure yeah
yeah i'm sorry i i i still have trouble figuring out for the for the for the chinese part like i i think he mentioned hello okay uh good question okay uh so i think the question is like um
like we we uh we said that the hello2 works on uh columns and rows and like uh how many um columns we have and then like uh like how many rows we have and and what's inside a cell so um i think the answer is like you can have as many columns you want but like each new every new columns you add adds more uh proving cost and verifying cost um also like like uh
proving time verifying time and then uh the cells uh are the rows like uh so we we talked about like like uh you [Music] you choose the value of k this one uh you you have the like the maximum rows you can use so for example if you choose k equals to 16 that means you have a polynomial degree 2 to the 16.
um there's a maximum depending on what curve you use for example uh in in uh bn256 uh there's a property called like uh two area to ethicity or some something like that like like i think it it it kept your maximum possible roles at like two to the uh 26 or 28 some something like that so like you you cannot use uh like as many roles you can use
and also like adding rows uh also adding the uh overhead of uh fft operations and it means that like um you have more proving time and yeah so so that's a column and rules uh to summarize like you can add more columns and more rows uh you can add unlimited columns but not unlimited roles but then they all comes with proving costs but the cell what's inside the cell is a field element it's basically a very big integer but like
taking modules uh to the uh curve order like like uh just treat it as a big integer and it's a positive integer um yep uh not sure if that answers your question pen yes absolutely thank you thank you thank you and i have another question and i asked this for my friend yeah sure can i speak chinese yeah yeah you will describe this question thank you just so the question is that uh
if i um if i want to program a custom gate and it has three input one output um and like like uh what what kind of columns should i use like it's a three advice column or and one instance column um so my uh answer to this question is that um the gate the custom gate does not work like that um it's not a it's not a um it's not a
gate like the like uh like a physical circuit um uh per se um it um or maybe gates uh is um rather very confusing it um it don't it only uh defines uh a set um defines the equation that must hold so um it's there's no such thing as like like three inputs or one output you can reference to um
as um like as as many cells or like different cells as you like you can compose arbitrary expressions you like you can for example you can like reference to cell a or cell b multiply them together add to another cell d or something like that um so uh i guess like um you you uh if you want to simulate a case of like physical circuit like for example you have three inputs one output um you can define uh three cells as
input one cell as output and you can choose uh you can choose that cells for either advice columns from fixed columns or instance columns uh you can choose it arbitrary like like choose anything that fits your need but um let me uh uh like repeat here like like the advice column is for private input from prover instance current is the public input from prover and the fixed column is the uh the value is assigned at the compiling
time that uh both the prover and verifier has this value so uh i guess depends on what's your application logic uh choose what columns you need does that make sense i said thank you thank you thank you charlie for posting
thank you thank you for coming thank you bye thank you