L14 - Introduction to Halo2 | by Nullity | BlocSoc Lecture Series
BlocSoc Lecture Series · 33:37
Nullity introduces the Halo2 proving system and Plonkish arithmetization, explaining the foundations for readers interested in zero-knowledge proofs.
Speakers
Topics
From BlocSoc Lecture Series, published by BlockChain Society IIT Roorkee; community: Blockchain Society IIT Roorkee.
Transcript
okay so I'm NTI I'm a Zer knowledge security researcher at y Academy we uh run fellowships previously we've had five smart contract fellowships and just now we wrapped our second ZK fellowship and um yeah I'm here to talk about this thing called Hill do um so let's get started uh we'll brush up a few basic terms and then we'll move on to Halo 2 so before we dive really deep into Halo to we'll have um some background on provs and
verifiers and constraint systems so you know it doesn't feel odd to get those terms inh to so typically when you read any Zer knowledge protocol or any introduction to zero knowledge protocols you see that there's a prer and a verifier and there's an interactive protocol where the prer tries to prove something to the verifier uh it could be um any computation like basic math like um uh is the addition of two numbers the third number or um is the hash of a string some other um string or H so uh the prer tries to prove some
logic and the verifier is there to see um if the computation has been done correctly or not uh most Zer knowledge protocols introduction to Zer knowledge protocols or interactive protocols start that way but in reality uh a lot of protocols Z Protocols are non- interactive in the sense they are computer programs so the pro and the verifier over here are not people or characters um such that they can interact but uh computer programs such that they face a lot of um computational difficulties and are um and have limited resources and
constraints so in reality you would build up a circuit which encodes all your computation and this circuit uh would then produce a proving key which is given to the prer and the prer tries to generate a proof which would be an uncomp comprehendable a bunch of alpha numeric characters and like uh yeah just some just just some gibberish which is done uh which is then given to the verifier which then tries to make sense of the proof which was received by the prer and all the verifier does is um it gives a yes or no yes in the sense yeah the proof is correct no in the sense
that uh no this is uh not the right one so uh in reality there's no interaction between the prer and the verifier let's focus on the part where we generate the proofs so um the proof generation process is just the the uh this one this part where you take the circuit and you give it to the prer and you generate a proof this part can be then broken down into multiple set steps uh this is like a basic building block of proof generation there are even more um minute steps micro steps I would
say uh so here you have the circuit which is then broken down into a constraint system uh a very popular and uh known constraint system is the R1 CS constraint system R1 CS which is um rank one constraint system uh which is here on the screen if you see uh then the constraint system is broken down into pols and then you run operations on those pols and then finally you get a ZK snark which is your proof so um yeah we we know what a circuit is but uh we haven't
dived uh deep into a constraint system uh yeah uh if you guys are uh don't have a clear understanding of what I said MH okay yeah yeah if you guys don't have a clear understanding of what a circuit is it's just a computer program where you have logic which you uh are here to prove so constraint system and specifically R1 CCS rank one constraint system rank one constraint system is uh this Set uh this Con St system where you can express a logic in terms of addition and multiplication only so you can have
any logic but in the end you have to boil it down to one of these two operations um for simple programs this is much easier but for complex ones this becomes pretty difficult um uh let's have a small example uh you might be familiar with circom or or if you have an um electrical engineering background you might be familiar with um what's that thing very the hgls and like the digital circuits where you have the wires and the inputs and outputs so here we have one such circuit where we have three inputs a b and c and we have one output
d uh what we do is uh we multiply a and b and we add C to the the product of A and B and that's our output now this is a pretty simple program and this is uh best when it's done in the R1 CS constraint system but uh let's say you want to divide two polinomial or you want to calculate the um the 100 square of some number I I don't think that would be feasible when you have R1 CS so clearly there are shortcomings in R1 Cs and um they can be stated as um there's no custom uh there's no support
for custom Gates so there is only addition and multiplication you cannot express your custom computation or function uh I mean not every function or computation can be boiled down to multiplication addition I think um that's bad and there are no lookups uh typically in all the computer programs when you're running programs lookups are pretty useful and uh the third one is um R1 CS systems like Groth 16 16 is this proof system and this proof system uses um R1 uh rank one constraint system
and this one requires a circuit specific trusted setup meaning that every time you write uh every time uh you build a circuit you would have to uh do a trusted setup for that circuit so uh R1 CS was uh I think used back in 2016 and bro 16 I mean Gro 16 was used back in 2015 2016 when the Z cash folks were using sapling and they were coming up to uh with um techniques to do um shielded transactions in zcash and uh
the people of zcash uh obviously noted this problems of um uh these three problems that is the uh the lack of custom Gates and no lookups and uh the thrusted setup issue and they thought they would come up with a new uh um proof system and a constraint system so they created Halo to so uh it's Shan Bo D Hopwood and Jack Greg who then created Halo 2 to uh facilitate shielded transactions in zash and it used a different constraint system called plish arithmetization
now what is plish uh yeah in R1 CS we saw this uh we saw this logic where we had a into B plus C seemed very simple uh in terms of rmcs this would be broken down into two equations first you would calculate the product of A and B and then you would add that to C so uh not everything is done in one single step and this is kind of uh this kind of takes a lot of time and space uh whereas we have limited resources enter plish plish arithmetization
so this is an equation at first it sounds it looks scary and you can't even read it but once you get a hold of this this is really awesome and you can do you can do great customization with this equation so the equation on screen is the Bare Bones of blanish erization uh and uh yeah you would see a lot of Q's there's ql QR qo qm QC all these cues are called selectors and selectors in the sense you can turn it on or off depending on your um equation and the
values there there is XA XB XC and the X values are all inputs and outputs so this equation you see on the top is is created on the assumption that you have two inputs which are X a and XB and one output which is X C now how do you bring life to this equation or how do you use it um yeah let's say you want to uh yeah let's say you have a very simple gate where you add two numbers and you print the output of it the gate would be then a + b = c where C is the output and a and b are
inputs so here our x a will be a XB will be B and x c that is the output would be C so we have configured the values the variables now it's time to configure the selectors now ql stands for uh left wires selector QR is the right one qm is for the multiplication one qo stands for the output selector and QC is for the constant selector so here we'll say we have one left input which is a so we put one uh
QR is one because we have one right input over here right and left are it is with respect to this this uh addition operation so to the left of your addition symbol you have a so it could be the left wire and B will be the right one there's no multiplication happening so qm would be zero and QC would be zero because we don't have any constants like 1 2 three or yeah anything so QC would be zero and if you um yeah substitute all these values in the plish equation you would get a + b equals uh A + B minus Cal 0
which is the original equation which you wanted to represent so yeah this is the uh yeah this is what uh the selectors mean um you can take another example of multiplication let's say you have a multiplication G and you want to express that one so uh qm would be one here and ql and QR would be zero because ql and QR come into place only when you have addition uh and the rest would be same and you would get a into B minus C = 0 which is the original equation you wanted to
prove now yeah again we are proving addition and multiplication so is plish arithmetization just a glorified equation which has um extra variables or is it something more uh so yeah if you take an example of this equation let's say z = x into y CU in R1 CS what we would do is we would multiply Y and Y once and then we would multiply uh uh the square of Y with Y again to get y Cube and then we would multiply that with
X to get uh Z so this one would actually span into multiple equations this is in the case of R1 CS but in the case of plish what we could do is we could take the barebones of blanish equations which is this one the first two lines and we could add our own selector which is Q Cube and uh we can uh we can represent this part of Y Cub as XB cub and we would be done so this is the this is the part where plish equations really stand out you can add your own selector
and your own computation and you can customize the equation just however you want so this part is the basic block equation and the one where we uh where we had Q Cube Q is the selector over here and XB is the input it would be y over here so this is our custom addition to the blanish equations and you can do this to any circuit without much of a hassle so yeah the advantages of the plish constraint system is that it is very customizable it it kind of gives you a lot of control over your equations
and your circuit so yeah you have a lot of uh customizability and the second one is the concept of selectors itself is cool you have granular controls and you can create multiple complex structures um based on these two properties so yeah we just had a look at plish arithmetization um if if you've got any questions fire away yeah so we still can't like make Gates that like correspond to bitwise operations in this H
to uh which operation and specific can you give an example like any zor gate or orgate specifically uh you can but yeah even with all the advantages of blanish um you can actually with a few tips and tricks but yeah it's it's not that easy right now in ZK yeah yeah I understood okay yeah um yeah so coming back to Halo 2 we we just had to look at funish
arithmetization and then we know what Halo to is right now it is uh flish constraint system with a commitment scheme so zcash uh the people who created H2 they use a different commitment scheme called IPA and the PC folks who foged it from zcash they use kzg to for it to be compatible with ethereum and uh as you know if there's a proof system you have a commitment scheme and uh an IOP and we use the plon IOP so yeah this is H to uh in simple words
so uh in Halo 2 we we would write circuits we would write circuits using the Halo 2 API and the inputs which we give to the circuits are represented in form of a matrix or a table even in R1 CS they are represented in terms of Matrix matrixes and um in Halo to it looks more like a table because it's huge and we use colors to um segregate the types of inputs which you would see just in a second uh yeah so the Halo 2 system is now um the the Halo to table has uh three
sections which is uh you would see you would see there's like a white one a white column then there are pink columns and there's this blue Violet columns um each of these columns stand for something so the white one are actually instant instance columns um instance columns are um public inputs which are shared between the prer and the verifier so um these are placed in the instance columns the pink ones are advice colums which contains your um private values or Witness
as we would say and these values are accessible to the prer and not the verifier and then you have the fix it columns uh which are filled at the time of key generation uh and most of the times fixed columns are used by lookup tables or something um something which is known beforehand or yeah as as I said that's preprocessed values so the whole table has um 2 to the^ K rows and um I don't think there's a limit on columns but yeah uh you have two paret
rows but not all of those rows are usable um usable in the sense you cannot assign values to some of the cells in the table um so the first 2 K - t - 1 rows are usable you can assign uh values to the cells and the last T rows are called blinding rows because they contain um blinding factors now what is blinding factors uh so blinding factors are these gibberish numbers um or uh yeah they are the ones which add the ZK the Zer knowledge stuff to the proof uh so if
you uh sort of remove the blinding factors there wouldn't be uh ZK to your proof so it would just be proof of math it wouldn't be a zero knowledge proof um so in simple words for a proof to be zero knowledge it has to be hiding and binding and by taking away the blinding factors you would take away the hiding property so how do you fill in these values and where do you get these values so um you can generate these values by hashing the witness polinomial witness polinomial are the ones you get um in the advice columns so yeah that is about uh pling
factors and this is your hello to table um let's let's go back where we started we started with the whole prer verifiers out where we knew that this these aren't two characters but um two computer programs interacting with with each other um and uh we would see that often in interactive protocols uh there is the scer who which sends a commitment to the verifier and the verifier to check if the commitment is right or not sends a random uh R to the prer and the prover
has to evaluate the commitment at the random hour and send back the commitment to the verifier uh this is an interactive protocol which would happen in ideal situations possibly in books but in in practice in when we're dealing with programs it doesn't work like that so we have a pro a program which would um which would have this commitment commitment of p uh to get a random R it wouldn't go to the verifier it would use a hash function and hash the commitment which a bunch with a bunch of other variables uh now these variables are
really important and if you mess any of these you can compromise the security of this zal system so uh the prer would hash the commitment and a few other variables to obtain a random R and then it would evaluate the random r on its own and um calculate the commitment at the random R and send it back to the verifier so this process which you just saw is called fear chare transformation fear chare is nothing but um transforming this interactive protocol into a non-interactive one where there's no communication between the prer and the verifier um using um a hash function and
in books or in papers this hash function is often referred to as um random Oracle model but yeah this is enough information for us to go on and yeah this is how you obtain these uh blinding factors you hash the witness pols and you put it in the last row of the table uh yeah we have we've successfully completed did um the structure of how um values in a Halo to Matrix or table are represented now we're going to dive into
the Halo to API and before we do that um do we have any questions yeah so for now you talked like there are 2 to the power K rows and T of them are not usable because they because they are blinding factors so is there any relation between like K or t or like how many blinding Factor rows we should have ideally or like we can increase it or decrease it yeah you can actually it there is this calculation that's a nice question uh it's usually less and it's based on your uh based on your witness
size so let's say you have um let's say you have five Witnesses like five witnesses and advice columns I think the T would be somewhere around three but yeah there is a relation there's not a relation relation between k and t but there is a connection between the witnesses you give to the table and T So T is roughly estimated of that yeah I I'll I can show you the code where we calculate the but I don't have it right now yeah yeah also in the fat Shamir model
uh what happens if the verifier itself is malicious and will like not accept even like our like commitments that we have that's a like reject our any like correct computation we would have done M uh that's a good question uh so typically in um ZK proof systems what happens is that everybody runs their own prer but there is one common verifier which is public which is auditable by other people so if the verifier is malicious or has incorrect code which can potentially um uh destroy the system
or uh stop the process and create a Doss um people would know that so yeah the verifier here is a public entity and if it's malicious we would know that and that's the Assumption here yeah yeah okay that's it for okay uh yeah so let's start with the Halo 2 API so far we've had a look at how the Halo 2 table looks and how we would represent values in a table but how do we actually assign values and how do we calculate and um create our circuits so the hello2 API has a few
components um let's start with the first one uh before that uh the Halo to table has uh we talked about columns and rows we didn't talk about cells so the cells in the blinding rows are called as uh poison cells so you cannot access poison cells you cannot assign values to poison cells um the other cells which are in the usable rows are either assigned or unassigned and the unassigned ones have a default value of zero and the assigned one will have the value which you assign it to them so a lot of times there are issues um with the unassigned cells and the default
value of zero you would like face it a lot um so yeah that's the cell so we were about to start the components of Halo to API and um yeah let's start with chips so chips are like functions in Halo to API you they are like the basic building block you can have multiple chips or you cannot have any chip at all and you can just have one big circuit with all the computation in it so chips like ease the work you do and inside a chip you can create gats you you can Define lookups you can uh yeah you can add all the logic you want inside chips and usually there's like a chip config
where you uh specify um the inputs the or the kind of columns the inputs would take and the rest of the stuff and where you would assign those uh values and regions uh you then have a layouter so once you have a chip chip is like function uh you would need a layouter to um add the chip to the circuit and assign the values which come out of a chip onto the table so uh this method the assigned region method is the most common way of assigning regions it's kind of the only way to assign regions on to the Halo to table and the layouter
is the one responsible for creating the uh the shapes and the layouts and the assignments uh you then have a floor planner so what the layout it does it is it would uh create shapes on the tables these shapes represent regions uh which are chips which uh regions which use a certain gate or which use a certain logic now the the leou job is to just assign these regions the floor planner's job is to optimize the table itself is to see um the best way to uh arrange these regions such
that um we have the most optimal Pro and the verifier cost so uh right now in Halo to we have a a floor planner call as a simple floor planner and it uses this strategy call the first petch strategy to arrange these regions and regions are in green color like uh yeah we have colors in everything we have white for instance we have pink for advice columns we have um Violet for fixed columns so there's green for um regions so regions are the cells which are
assigned um yeah why do we have to optimize uh why can't we just leave it as it is um so yeah we are we are people who have computational systems with limited resources so we obviously want um a small proof and a faster prer and a low verification cost so uh we uh most people optimize based on their U requirements so if they want a low verification cost they would have fewer columns and if you if they want a a low proing cost they would have fewer rows so that's the logic um between yeah that's a trade-off you have
between cost and the number of columns and rows you use so uh zooming out you have initially the circuit which you would build using the Halo 2 API and then you have the plish constraint system and you can uh so whatever Gates you have in your circuit are then broken down into the plish equation we saw earlier and which is greatly customizable so you don't have to worry like you do in R1 CS um then this is fed into the plong proving system uh and in the end you get your proof uh because we have uh because of
the time box nature of this session I I haven't deep diving to plon because plon itself is like a huge topic with multiple rounds and a trusted setup and um yeah it's huge so uh if you want to learn more about how plon works from the beginning from the scratch uh I would highly recommend going through this repository called platon um in my GitHub uh which kind of has a huge uh explanation of uh how the polinomial are converted in the rounds and plon and how the final proof is generated
so yeah and if you want to learn more about Halo 2 I highly recommend um looking out for y Academy's um second CK Fellowship we haven't made it public yet it uh would be public in the upcoming weeks um and you can expect a a lot of Hal to Alpha there um yeah uh thank you to you guys for being so patient and if you have any questions um feel you ask