Little Things I’ve Learned in Developing Halo2 Circuits by Chih-Cheng Liang | Devcon Bogotá

foreign [Music] developer experience for programming the circuits CK circuits so we know in ZK snark well we allowed the approver and a verifier they agreed on the algorithm and then proverb can provide a proof input and the output to the verifier and then verifier can be convinced that the computation the output is a correct corresponding to the input without re-computing the algorithm again so lots of scaling and privacy we are getting from this Nars and I'm going to unroll this uh process more it's not a full story but U.S circuit developer uh you are on the uh left and side you define some constraints and uh and then you send a verifying key and program key generate generated from the these constraints and send it to a verifier and approver we call this a setup time this is like when you like finish the circuit development and the deploy the project and setup is ready but at a proving time like whenever you need to send a proof so approval would have run the computation and get the computation traces and fill them to the circuits and using the proving key to generate the proof and then send the proof to the verifier uh today we don't care about like how sausage is made like we care about like uh how how do you like like turn the computation into circuits so if you're coming from like a normal programming world for example if you write pythons the rest same thing you might your brand you works with a function loops and if else this kind of good stuff but when you enter the circuit world you need to do the uh agreement algorithmetization and you need to get the circuit tray so you're thinking in the computation phase of the whole computation and you think to verifying these computations with a math and equations so it's like that so before we going to introduce some tricks and uh development tips that's uh talk about the rules of the game like how how this uh circuit thing work um so first of all like all computation is represented in finite field algorithmetics so a financial element is you can think it as an integer and it's a positive integer and less than a number P and let's say if P equals to 3 then if you have two field elements two and two you're adding together you actually got a result of one because we need to do it in module of three modular p and p is usually a very large number for example it's uh 254 bits um so uh the takeaway is that we need to represent like your computation in in Via numbers insteads or bits and buys and uh you need to watch our uh watch out for the wrap over and over for all that stuff and then uh we get this uh uh grid of stuff uh like a paper you can fill in the field numbers inside those cells and uh for if you you can expand this grid with more columns and but like for every new columns you edit it it would be more costly and but the raw rows are basically free but they are uh kept up to some limit uh let's say 2 to the 18 like this is uh 260k roughly so uh ideally you want to use as much row as possible until like maybe you have more uh computation you need to do then you add more columns and approving call scoring times verifying costs something like that and we have to uh distinguish some types of columns uh this this columns are distinguished by like who can see what and uh when they are like uh when values are assigned so we have the pink one is the advice column it is only visible to approval it is uh determined at approving time the witness the value inside this column we have a fixed column fixed column is a assigned at a setup time so uh both approval and the verifier has have a copy and then the instance column so this is uh the value is visible to verifier so we can um the program can fill in the input then the output in a proving time so uh so that we can have the scenario in the first slide that uh the further within some private values and then some uh public instance values for the input and the output using the proven key to General proof and then verifier can uh verifying the proof and also take the 10 and 100 there you can verify in a contract or do other verification if you may um right okay so um now we have the grid we have the columns we need to Define like uh what values in the cells are correct or valid like what what of values uh are allowed to put in their cells so these are constraints and I'm going to introduce two types of constraints in Halo 2. the first one is the custom Gates so this defines the content in uh polynomials so decade looks like this or we have a we we choose the uh a sales uh from column a sales from column B and sales from currency you can uh choose a whatever column you want and you can choose the relative position for example uh I want the next oh sorry next column of the red in relative to the H cell and then you can Define the uh uh sorry you can Define you can divide a polynomial to constraint like okay a must equal to the B plus uh uh b b the next cell of the B and then but like uh this gate will be applied to all roles in in a column so sometimes we don't want to do that so that's why we have a selector here so this selector will be the one or zero value so if this selector is one then the whole uh then then this expression here must equal to zero then our constraint is enforced but if selector is zero then the whole expression is already zero so uh this constraint doesn't necessarily hold for for that particular role I just want to call the the sentence from vitalik I heard from his talk he said like everything's a polynomial I'm a polynomial and so to give an example a viral example for in terms of Fibonacci uh circuit example and we want to prove the ends turn of the Fibonacci number and then we can fill in the value of uh one one two three uh by anything into the grid and we Define the gates that left plus right must equal to the sun advance that means that left y minus sum equals to zero and we use the selector qvip to determine like which uh which role we want to enforce this constraint so here is one way to do it like we we make this gate looks uh like very straight they are on the same rows but you can see that we are using three columns here um so this is an uh the other way you can do it you can you can make it like uh the sum you can for uh fold it to the next sale and it used less columns and but it works the same way it it still can give you your desired computation results so it's flexible you can determine the shape of the gates uh depends on your your problem to solve and the second second tools to uh constrain the Great Value is copy constraints so I have this yellow tab here to grow the values of two cells together and if they are glued so this value assigned in a cells must equal and this is determine the glue must be determined at a setup time there is no way you can change it at a proven time uh but it's very cheap and use it as much as possible the final rule is that the approval can be evil like I like to see improver or like everything with the verifier miners things like that as a cyborg uh they are the human who runs the machine and like machine runs the algorithm but like human are attracted by incentives and they they could do all kinds of stuff so if you didn't write your circuit right program can witness the wrong values and still convince the verifier to do stuff so if you are like designing a decentralized mixer for this and further witness some value they can like withdraw the money out of the air then your your project is hacked okay so let's get into tricks um okay let's start from the simple one and how do we limited limiting the options in one's sales for example I want this cell to allow only values one or two or three nothing else so to do this we we can Define the gates that has this expression uh the sale value minus 1 times 7 minus two times sales value minus 3 equals to zero if you plug in the three into the cell this expression will be zero but if you plug in this 100 then um this expression will be like 99 times 99 times 97 uh it won't be zeros of uh this constraint is not satisfied if you witness zero uh this would satisfy either next that's converting if and else um so for example we have this sample program here we have uh we have input a input B and uh there are like field elements and happy is a like a Boolean value and if happy then we do a plus b uh if we are not happy we do eight times V and then so for example we could have a circuit that looks like this I used the glue to glue the topic instance value to the private value in the left left one we can see that uh awareness a S5 and bs6 and happy yes one so we are doing the addition test so we got the uh value 11 and the second one we still have sent a b value but heavy zero and the desired output is 30. uh we we just give an example here we haven't constrained them the way uh you you turn this uh if else into the gate expression will be happy times uh a plus b plus one minus Happy Times uh a mill test by B minus output equals to zero so that uh if you uh if you're happy it's one then this expression will be enabled and this expression will be disabled uh the other way is then if the happy is zero then this expression is enabled and this expression is disabled so uh let's see um we we have like a example value witness in here uh these are all satisfied but uh like we kind of forget something here like forever can win us free here and still got the three times uh five plus six and brother and like get the output minus 27 equals to zero so what's wrong here uh it's because that every input is a finite field element but uh if we want Boolean value here we need another constraint to make it boiling so we need this additional constraint here to limit the happy to be one or zero so using the tricks before okay uh next uh we need to cover the loops into the circuit and uh this uh let's start with the easy one this function uh initiate the variable rs0 and then it runs the loop five times and at the five at our at 5 to R and 35 times and like five is our constant so uh it'll be easy to lay down like uh the value of R starting with zero and the next uh plus five plus five plus five all the way to the output and then we constrain the uh value 0 to 0 25 to the output to the output so uh we will have this uh gate expression like this easy but uh what about this uh this looks like exactly the sand Loop uh it said uh like how many times of Love is determined by the approval input and here so this will be uh about trickier because um you might have a uh so we can imagine that the tension Trace looks like this um first uh per input the N here and the output 25 here and uh straight or input three here put here and notice that this uh this algorithm this is basically the a very in efficient way to to find Phi times n and also note that this end could be like arbitrary large but like we don't have a arbitrary large circuit so like we cannot do the infinite Loops we can only do like only up to certain amount of uh computation so we need to like restrict this how big this end could be let's say we receive it to five and then we need another check to make sure the end is actually less than five but it's out of score of this talk um we want to focus on how like to uh determine the computation of R inside so uh yeah that's first uh do the copy gate for zero to zero and the output to Output but because the copy Gates uh output can only locate it at the same place of the a cell so so if the end is free we need to like repeat the result here all right uh so um one attempt is uh to solve this is we add the program witnessed uh selector here so uh let's put one one one here uh when we uh when when we are still in a range of N and then zero zero zero here to do a repeat and using the if else trick with that before we can Define this guide expression uh but then how do you prevent like like the purple doing this so like uh if forever like they don't follow the rules they've uh witnessed zero and like one and then go back to zero and one and uh if you do the math you can realize that program can win the three and like output to to be 10 then you convince you that five times three is ten then yeah it's a it's a failure that people say it's like blockchain is about trust I would say blockchain is all about trust issues and [Laughter] so uh let's observed like like the um like different cases of end like n is 0 and it's three and is five and uh we after that s can only like follow a valid case that uh you can start with zero but once you are zero you can only go with zeroth of the rest of the row you can start with one and you can turn one to zero anytime but like once you turn to zero there is no way to turn back so we can identify the state transition uh like this uh so this is a trigger Han told me so you uh when you start you can start at a eighth stage that means we need to add five and you can from any state you can go back to a state you can go to the pet state which is which is a zero and like like the RS Remains the Same um but uh the point here is that once you enter the past State there's no way to go back to the S state so we can Define the constraint here and actually the only thing we need is here like if you if the current cell s is zero uh for example here then the next cell must be zero so uh this constraint can help you achieve that and also we need to make sure the selector is binary now we have the final touch like to um make the input uh accumulate this input value and copy back to input this still follows the same same rules for the program witness selector um so like uh why are we uh doing all these trees why why uh why we need to like doing this uh repeating and like stay transition thing um because like in CPU uh we take instruction one of the time and if you have a if else branch and if the branch you didn't enter that just you can forget it and you don't compute it but for a circuit um you need to flatten all the computation all paths you need to include it in your circuit and then so you can see here even though uh we only witness input 3 here and these three rows we still need to need them and like we need some dummy values there because we need to consider the case that proverb could witness five here and I use all these spaces the takeaway here is that the challenge for Authority developer is that uh we are working with the computation Trace instead of the execution itself so we need to flatten the pad and like uh work uh all possible pace of your computation uh the second is that because we are working with a field element instead of bits and bytes so we need to do some math and equations there and the third is that we need to work with the verification mindset because Uber could be witnessed uh malicious values inside your circuits and the tricks we talked about here are like using the Boolean value and one one time times the true path and the other times the false path this can convert the if else statement into the uh the the circuit expression and for the complicated Loops you need to identify the state transition of of the uh your program logic and then design uh constraints for them uh yeah that uh that's my talk thank you thank you for listening yeah I thought that in Planck yeah the copy constraints were expensive um can you expand on why they're cheap in Halo 2 um I think they are I think they are the same I think that they are cheap in terms of when you use uh once and like you use it million times they are they are the same cost so I I think yeah that's that's the idea thank you great presentation it for somebody that wants to learn more about CK proofs what part do you recommend to go right now I think the secret explanation is really good but I got lost in some bits so what will you recommend me to to read in order to to follow you better I would recommend try to find a simple circuit project and try to run it try to tweak it like removing something and and try to start it I think that would be the good way to learn how circuit works you mentioned like in the yeah here take away points that you have to prevent the prover from achieving how often do you see when you're riding the circuits that how often do you find bugs because your circuit was under constrained and the proofer can cheat oh good question uh so the question is that uh like how do we find if there are bugs or how often does it happen that you find a bug because it's under constrained and the proofer can cheat uh or because the constraints if the constraints are wrong if the gates are wrong or just trying to compare it to like usual software development where you just basically write the logic wrong right how often do you see that the gate that you come up with are doing the wrong thing um so when we are developing the circuit uh oftentimes we'll uh like realize oh we forget this connection and like program could witness that bad values uh like we found a lot of bugs in like development stage but like once you want to go to the production uh like we would like do some external updates and like try to find as much bugs as possible and uh like when you and really enter the production uh like you can only like cross your fingers and but like I heard vitalik has an idea that says they they can use like two Proverbs for the Roll-Ups and like if they can win it uh like they can create a value proof or two different outputs then you can like stop the raw or stop your application then and then do the fix so you when you write the Halo 2 circuits you're writing and using the rust lab right um do you think that that adds a lot of overhead compared to if you were using a DSL like circom or circuites for example I definitely feel like circum or like like DSL are more readable more outdidable but the thing is when you don't have DSL you just have to so you so you would like to have a DSL for Halo 2. uh I like what would you like to have a DSL for for hello too yeah yeah yeah yeah that that would be that would desire and great to have a DSL for help too yeah I thought someone released one some months ago didn't they or maybe I dreamed that but I don't know anyone up here no I think it was someone from dark fight that posted on the the ZK podcast telegram group uh maybe I also dreamed that I don't know thank you