Zero-Knowledge Proof: Halo2 for Dummies
ETH Vietnam 2022 · November 2022 · 19:14
Khai Hanh Tang of Orochi Network gives a beginner-friendly workshop on zero-knowledge proofs with Halo2. It introduces the proving system and how developers write circuits with it, aimed at people new to zero-knowledge. Recorded at ETH Vietnam 2022. The level is introductory.
Speakers
Topics
From ETH Vietnam 2022, hosted by ETH Vietnam.
Transcript
let's learn about zkb how to for dummies with our r d specialist from rot Network please welcome on stage [Music] hi everyone my name is Kai Han tang and I am from orot Network for research and development specialist so today I will talk about zero noise group and it's in Harrow to foreign this is a kind of describing the Royal Rim into something that can be combined into a zero noise
groups and next one I saw how to implement this one in Ross programming language so for the first part by talk about blankets arithmetization so um first one I would like to talk a little bit about zero noise problems so uh for zero instruct you would like to prove a step one that you would have to convince someone else that the customer is true so uh for example if you buy a cigarette then maybe the seller asks you to to be at least 18 years old so um one way for you to show that one is to provide your IC I mean I need an identity card or
either the smartphone the passport so uh so you can show no information to them however if you saw that one you may review the name the address your play request something I'd ask so um we will not be review all the information but they just want to know that whether you are at least at the user or not so um that's why we we have a technique called Zero running through and in this one uh this one can be programmable and when whenever a rhyming it has the following properties the first one is completeness is mean that
if you are actually sorry if you are actually at least 18 years old then you can always convince them for the orders probably you see the sun is property so in this property if you are under 18 years old then you have no way to convince the seller that you are at least 18 years old so the sun has probably gone data you cannot choose this means you cannot control the last property is zero knowledge so this is the importance property of then it can hire information and the
only thing you can reveal to them is the quality validity to investment so uh for the example of buying cycle rate they only know that you are at least 18 years old and they have no other way to know that something like your address your name or anything else and in the matter of blockchain we sometimes we would like to grow a puzzle program about our consumer contracts execution so um thus has a very small group size so uh
and another property that we also need from the sequence now is the fast prediction verification property so uh for example if you would like to grow maybe a hundred to thousands of smart contract execution so by applying this one you can throw them in one group only one group and they're probably very small because uh after the second snap property I mean a sexy property it's had a very small group size and then when you send to the verifier the verify will verify as one quickly with a fast verification property so um
so now I installed about how to so how to use a customer Library not implemented in Ross programming language so uh in particular for this one is help you to to transform a program into some some cap or ending so for example the program here is like an aromatic circuit you have uh two inputs u and v at the beginning and then you can use wire from you by uh use Y is equal to new term U and then you can compute UV from U and B then next you can compute uh three UV
from uv2 and use wire Plus for UV and by doing this one up to this one you you get the result that is it a function Computing fuv equal to use where I'm not trading UV plus v and plus five so um plus argumentation and this one is very special because it can help you to program custom get so is it called the blanket arimeterization so uh so this one is built upon the plant's aromatization from 2019
you can combine the array materials to a cs9 problem so the purpose of Halo 2 is to help you transform a circle to a way to supply thus can destroy the circuit and then you can compute the second group by using the hello tool so I give an example of this foreign so you can see here that we have a table an additional table and multiple constraints here and also all the copy constraints of us of the circuit so you notice that in the circuit we have four different gate
um the multiplication gauge here the additional constant gate is here this means you can compute this one you get this one plus five and you get the final one uh multiplication here multiplication we can stand here and addition here so you foreign we have four different columns for the selectors so the columns are to indicate which scale you use for for each computation so you can constrain those computations by the following selectors in in this constraint here click on the gate constraint so
we have three three advice column here at by zero advice one in a battle and we have a constant column two so uh if you you know test that the translator here they are said to be one either one or zeros so uh if the selector is one for example here if this one is one then you need to guarantee that s by 2 is equal to X by zero plus s by 1. so this one must be zero if if the z letter is zero then this one is zero already I use this one to to my simplifier because uh
in the real one the sum the addition of D4 must be zero and finally the final thing is that you need to connect the wire upper circuit like it's A1 is B1 letters they are on separate and then you need to connect them by the copy constraint yeah so for describing a circus like this you need to specify the gate the table and the company constraint and you can transform this one to this one so now I will show this one uh I want to implement this one in Halo 2.
thank you so there is a modification here I split the table into two reasons the first and the second reason so the first region is like the multiplication reason you can see here the selector for multiplication and multiplication we can stand set to be one and the second reason the selectors for addition and additional constant they are said to be one two so uh so now um we have the The Columns advise zero f51 f52 can start selectors so we specify an account here so uh in the beginning of the code we
have S by zero F5 one and two then you see an array of three elements a three advice column secondly you you know that you need to have the grouping input at the end so here you have an an additional instant column here and and that's the constant column you have this one so uh here we have a custom columns to and before selectors that I just described uh addition multiplication addition we constant and multiplication we can stand
here so that's one for this one you specify the false letters and the columns first and the next you uh you specify the gate so by specifying the gate um I go to this easier so for each grade you specify the column to be used like y 0 and by one and by two Foundation advice one and five zero one or two and for the constant here for additional three constant you also need to specify the constant in the constant column um and then at the end you need to
guarantee that you need to add a constraint to the inspector so the constraint here guarantee that this one must be zero specify the gate and similarly for for multiplication and additional constant and also multiplication we constant so those are the gate you need to specify an account and next one for the for the table so previously I told you that anybody table into two regions one and two the first one is for addition and the second one is for Monday I'm sorry uh the first one is for multiplication and the second one is for
addition so um so here I uh I like all this one to be the multiplication reason and then for each row like the first row operation here I specify um the value the contrast only the corresponding values to to the reason to the rows this is for the first row is a one is B1 and C1 so they are a one B one c one here and then you also specify for the second row you also I'm sorry um you also specify the selector too so this one you have the multiplication selected to be enabled
so here you have a selector here S1 must be S multiplication must be enabled so next for the second row you do similarly you specify that one together with the values and and for the second reason it's easy for additional reason and then you specify for the entire below reason here so finally uh so you we already have the the description of the gate and also the the table of values with two two reasons and now we specify finally the Copic constraint
so uh for this one we required us as i1 equal to S A2 and S A2 equal to sp1 so so for Capital strength we just put one of them here so sa1 must be equal to si2 as I2 must be equal to sv2 I'm sorry sp1 so similar to this and for another line like this one you need to have s A5 equal to sc4 so we have s f i equal to S4 here so we already have the table to get the columns and now we already have the copy
constraints here so uh for those things already said we can run the Rover here in account proof and later on we can verify the problem by using this command and to check whether the problem is correct or Not by using the sfaq foreign language I wrote an example here so there's no errors or the cost will successfully so for example uh if there is something wrong I try to to make a phone statement
uh FB if I try to make this force that one then you can see here the costly era and we we have the the background of the code so I checked back to the previous one without without any error then I guess the resulting successfully
okay so uh thank you for your attendance [Applause] thank you our speaker do you have any questions for him he's a very interesting I don't know much about online too and uh zero knowledge however I want to learn more about this presentation the first one is uh can you show me more application a
bit when you apply zero knowledge to like to in a similar in previous case for example some some between communication between layer 1 and layer 2 and the second one is about a terrorists use so many formula in mathematics in the presentation however I don't see that is there any proof or Samsung or if so uh difficulty when a hacker tried to hack the formulation for example if you in crypto with your circulator a digital signature and has function and they are
proof in and they have they have a difficulty in this problem but I don't see any difficulty in job for the first question as I try to to aggregate many smart contract executions into one group by you have many program right then you appreciate them into one single program one big problem and then you apply the second group on that program so because the CK has the executive has a specific property here
is ensure that you have a very small group size so you can press a very big execution tries into a very small group size and then you send that one to do the first layer so uh for the first layer we required is have something like Fast verification so it can read your group of many smart contract executions there and then it verifies quickly by this uh for the for the second question about the security of uh in fact our
currently I think we reduce the sound s property this means that for the group if you try to convey something from then the soundness property will guarantee that you have no way to convince that one so uh like come back to my assemble like I'm going to buy cigarette but I am under 18 years old so I have no way to convince them because the verifier can check can detect my my phone proof that's all anyone do you have any other questions
okay so I think that's pretty much it thank you so much for joining us today and thank you everyone for being here I it had a room for our workshops