Chih Cheng Liang: Lookup TLDR | 14th Oct 2023 | Sunway University | ETHKL 2023

ladies gentlemen our next speaker is a very interesting speaker because many of the projects the protocols here are actually built on this ZK evm right we're actually going to be listening from the guy who built the code ah so everybody is taking his code and building the protocol so this guy is really really big name he's you can see online his name is in the same sentence as vitalic buin so chi chang yeah he's from the psse ethereum foundation so very very interesting and of course this session is a little bit more technical so please feel free to stay back if you're a developer and if you're not and it's a little bit beyond your knowledge with me don't worry I think just listening also helps a long way right it helps you get a little bit more involved in the developing infrastructure of ZK evm so he's going to be talking about something called lookup and he's going to be explaining it you see more people coming in already I think because they know he's speaking so please come in come in come in please take your seats uh yeah this is one of the rare opportunities we get to listen to an OG from the ZK evm infrastructure who has created the code that allows other protocols to go and make their projects okay so that's quite interesting when we can get a look into his mind all right please put your hands together and let's welcome CC thank you that's a very introduction and thank you for having me very welcome thank you uh yeah so today yeah the topic is a little bit more Technical and I I'll be talking about uh looka protocol it is a very exciting uh cryptography technology that's been improved over the last year like if you see the paper like they're publishing months five months and uh now we are already uh kind of um reaching some kind of Lookout Singularity but most of this uh talks or introductions were like more research focused and today I'm going to talk about some uh engine engineering side like when you are a circuit developers how do you like actually use lookups in in your uh how to Circuit code AS then say like uh most of ZK ckvm team we use a very like very custom languages and and uh there are um uh some some detailed in it so for me I'm a member of uh privacy and scaling exploration and we're building a uh dkv and Community version uh the report is uh and CK EVN circuits and we're building as ass same proof of EVN execution we're WR written in h to and we're targeting uh L1 use case uh specifically uh Z EVN light kind so uh before we talk about look up let's uh see how the uh the proving system work and and also uh how how the how to uh lay out the circuit so we have the setup time uh where we need to Define some constraints you as a developers uh you kind of uh Define this uh sud puzzle which uh defines some rules uh that uh the solution is must satisfied and then we compile this circuit into uh proving keys and uh verifying keys and uh we send a verifying key to the verifier and uh key to approver and in approving time uh the approver has to fill in the computation Trace into this Sudoku board so everything happen in a proving time right in uh the red uh like handwritten uh bont and then the appr uh generate appr proove uh from uh this uh Sudoku board um using the proving key and uh the proof is just a list of btes but this uh uh this this bites will be sent to the verifier uh who use the verifying key to verify the proof and determine if the proof is uh correct or not and then how do we uh Define the rule of this uh Sudoku board like what value uh filled into the sto board is uh correct or incorrect so uh in how to we kind of uh defined the circuit in uh in a grid so it uh a cell in the grid is a finan field number uh it's a very big integer and uh it wraps over uh so it's final field arithmetics and the rols are kept they have a maximum uh the maximum like two to the 16 or two to the 20 rows uh determined by the setup parameter you use but they are uh free try to use as much row as you can and uh for columns uh they are uh they add additional uh cost and verifying uh cost so if you um need more computations you need more uh sales to fill in values and you um so and and if you you're running out of space you add more columns try to think this is a truck and like loading a bunch of computations and now uh there are different kinds of columns uh deter uh so if uh we we determine the uh Sudoku uh puzzle with this uh fixed column which is determine a setup time and the values are filled in the setup time so I used the uh uh this uh black font to represent the um f column numbers and also use the uh this blue purple uh color encoding for it and this this is determined setup time we call the fixed columns and then the advice column is for the approver to fill in um The Proving time uh proving time values into this cells and they are determined at approving time and they are visible to approver and the verifier doesn't has uh doesn't have the access to to these values and uh the last one is the instance column so uh those value are both visible to the prover and the verifier so so uh so to recap uh when that we fill in the computation trace the pro fill in uh the advice column and the in instance column and generate a proof and the verifier can see the uh information on a fixed column and the instance column and verify the proof so uh for example if you're uh writing a tornado cach application you might uh need to put your public inputs on the instance columns there might be merro roots and uh the pro witness secets and uh like a mer path inside the advice columns so now uh we can express the constraints how do we uh determine the rules uh are correct or not there are three ways you can uh Define the constraints in the circuit one is custom guge one is look up and the last one is copy constraint but uh in this talk we'll focus on lookups so what is look UPS uh for a simple example let's say uh the first cell of this column uh Prov can put in every numbers but let's call this number X and we want to constraint this x to be uh either one through three four or 11 like you can choose like arbitrary numbers you want but we just want to um constrain that in either this uh four so uh as a secc developer you are building these four numbers in the uh fix columns and uh and then you we Define the look up constraint as the sales to look up and the table columns to to look up for so uh what happened in a look up foral is um for example the pro Fielding three in the advice column and the workup will check uh if three is inside this lookup table so as you can see three is inside the table so this uh this circuit is satisfied and for another example if the pro building number 11 in the first cell and then the look up uh scan down the uh fixed column and then uh if I 11 is indeed in the column then this is also satisfied but if the appr fill in uh number 100 and then you uh scan down the lookup table but there's no 100 in the table so this is unsatisfied so it it is uh in invalid proof If you send uh send a proof to the verifier this uh this proof will be rejected so uh that's how uh look up table works you fill in the uh all the possible value value in the in the table column so one uh simple use case which is very common is a range check so we we can check if x less than equal to a and greater than equal to zero if you use other constraint to program this this will be very costly and very complicated but with the look up you just fill in Z to A into this table and then uh it's done like you can uh and you can constraint like multiple uh different cells with the same same cost and the other very common use case is the bit wise operation um so so bitwise operation is something like uh end or X or something very very common in your first programming language but it's very hard to do in a circuit because circuit only allows you to do uh additions and multiplications and let's say we have three variables X Y and Z uh each are one bit um for the look up you just uh put in uh the truth table inside the table columns so uh the X will uh look up to the First Column y look up to the second column and Z look up the thir third column and uh there have to be bit wise operation to satisfy the whole uh the the constraint and here the more advanced use case which we use in our uh zkn circuit all the time is that it allows you to create an interface between different circuits so we use look up table as a I know bridge to group different circuits together so each circuit can focus on their own core application logic uh for example uh we have a mer Tre circuit this is dedicated to the tree logic and it uh it needs catchup uh hedge functions uh uh to compute the parent nodes but we don't need to write the whole cater hedge function inside the mer Tre circuit because uh catcher hge function is a very complicated circuit inste we create a lookup table uh which we filled in the ketak input bites to the KET bites and then we use a Keta circuit to verify the correctness of of the table contents and then for mer Tre circuit it just look up to the table and find uh the corresponding output to the corresponding input so the mer circuit can uh fully trust this table and uh but we verify the table using the Kat circuit so let's create a good separate concern of uh different circuit and for the future or maybe it's uh we're getting close to that like uh what if we can create a bitwise operation table that can handle uh many bits uh like for example uh in previous example the XY Z they are one bits but what if we can do 32 bits um the table size will uh increase it increase greatly um to a degree that that's uh not visible in the current her to setup if you think uh her to roll has like Maxim like two to the 20 uh 20 rows but like if you have 32 bits uh like X would be it would need uh two to the 32 and Y need two to the 32 and the the two table would have the two to the 64 like it's very crazy big so uh but uh so but if we can do that then we'll have uh this what B white had call it look of Singularity which we no longer need to program circuit in like custom Gates and and like all the crazy uh polinomial and and and like additions and multiplication of finan fields we just use the regular like uh like good old days like like bit wise operations 32 bits arithmetics you can write it this circuit like your all programs um and we can forget everything about like writing like fin finan arithmetics and uh this year there is a new paper called unlock the logout Singularity with SLO by uh uh serti Justin F and R WBY so uh uh the idea of paper is that uh if the if the lookup table uh fit it fit into a structure then uh we don't have to commit a lookup table and and send that uh to the to the uh Pro verifier because like the the cost of the look up is uh like you need to pre-process it and then you need to commit it and and you have to do your trit setup and which takes a very long time but if it fits uh some structures you you don't you no longer need to um like commit and set up and send it send it somewhere like you can you can use the lookup table uh directly uh so yeah the uh that's my talk and I put this picture because like it's the one uh I used in the previous like ZK introduction talk and see if you can find a cat among these dogs uh thank you so much thank you let's give him a big round of applause thank you CeCe you said there's a cat there is it where yeah yeah there's a cat I'm looking for it it's a illustration from Yashin anybody found the cat yeah oh you found the cat okay don't don't tell a minute so if I can find the cat I can become a zkm developer yeah I hope so I wish okay thank you very much C I'll open the floor for questions anybody has any questions about lookup uh you want to ask okay yeah I got one over there I'll pass you the mic give me a second okay here we go you're very welcome hey my name is alas so I didn't I heard a lot about lookup but never understood so thank you today now I understand thank you so much maybe you have a dumb question so maybe there simple answer but for example in Koo we sometime use rain check to check that you're um less than a u128 yeah so how would you do it with your um limitation of two to the^ 16 yes so uh that's a very good question uh so for one to the8 uh you have to break it down like um so uh let's say uh if your lookup can process uh uh maybe eight bits or 16 bits of um uh of bitwise operations and you can break down your 128 bits integer uh or value into like this see how many eight yeah eight eight chunks so and you do the bitwise operation for each a chunks and then you assemble the a chunks result together using you multiply multiply them by like two to the eight and two to the 16 and then you you you sum them up together again so that's how we how you do big yeah I hope that answers your question my brain is slowly melting uh I hope I'm not alone uh anybody else had a question thought someone raised the hand in the back if anybody else just raise your raise your hand no question is uh too small or too big I always tell my students that no such thing as stupid questions only stupid politicians uh all right it's a bit technical it is quite technical I'm not developer myself I'm just learning a little bit here and there oh we got one one more we got one here and then I'll do one last one with you yeah we got bit of extra time time before 1 p.m. so go ahead well thanks for for the awesome presentation awesome illustration by Ain but uh yeah I actually had a question on the interface part so uh like how how large is the lookup table for that one and because I'm I'm looking at the input and output that's like input for KCK is well you can put in anything right so right curious about that exactly so so uh yes so I kind of uh cheated here a little bit so for K input you actually have to um so yeah the the the input could be like infinitely long right and and so there's a uh limit for that and in kak uh it kind of have U 64 bits a word and you have to split your uh input into bytes and then like uh fill them then down and and the output is kind of like four words and then so uh the output has actually a lot of gaps in this in in this column and the input um you can uh use the whole circuit just to do one cack or like you can um if your input is very big but if your input is very small you can do many and we have to design the circuit in a state transition way so you could have uh like this is the first CA and then you continue to absorb absorb absorb the inputs and and then finalize we generate output and the next next input absor abs abs absor and uh until the end so yeah it yeah so so yeah to sum up it's like a state transition trick and then um to to uh to try to uh take the catch up for different input size yeah thank you you're welcome all right a question good question I didn't understand it but it's good you want to ask something else okay one day one day my dream cc is that I'll become smart enough to understand all of this one day I just have a question on benchmarks like how for something just I don't know proving it could be a block because we've been talking about that kvms could be proving I don't know just inclusion uh how well does a lookup form compared to normal normal I don't know put it constraints yeah that's a very good question and I don't have a good answer for this one like uh we know like one look up is kind of um it takes like three more like three times more cost than a uh a custom Gates but I don't have a really very good good sense of The Benchmark so far no worries maybe in the future you might have a good sense of it once there's more development on it ladies and Gentlemen let's give CC Lang a big round of applause thank you so much right it's an honor to have you with us