ZK7: zkEVM circuit arithmetization - Ye Zhang - Scroll Tech

Transcript

[Music] uh hello everyone my name is yeah i'm the co-founder and vk researcher at scroll so today i'd like to introduce the evm circuit optimization so like so this will be more technical talk like more technical than like yesterday at layer to beat so the first house will be very very similar because i still need some background for talking about zikira up and evm to you know like because there are so many cryptographers who are not even familiar with with zero up and second half we'll be talking about the circular relation and how we are writing constraints to constrain the ziki uvm circuit so basically like first introduction of scroll like you know because many people even haven't heard of that so we are building an evm equivalent or they carry

up so that's one sentence introduction so that's then we can move to more like introduct engineering part so the problem with blockchain layer one is that for each transaction you need to broadcast that into a p2p network and every node need to re-execute this transaction to move from state one to state two and this is problematic right because it says you know there is a large redundancy there because every node needs re-execution so the idea behind security is that instead of sending out all the transactions in the p2p network you send all the transactions in a layer to a layer two node and then like this layer 2 node will run some liquid algorithm and generate a proof and instead of broadcasting all the transactions it will just broadcast the proof with some public input data for needed for application but there are some problems

because you know building a you know to generate such a they're not proof you need to build the arithmetic circuit right like all all the zika actors here must know like you know how hard that is to write some arithmetic circuits and also it needs to be application specific for example like if your transaction is on decks you need to build a specific circuit for this dex application for example like you need to build it you need to prove that your signature is cracked you have enough balance and your pass is updated correctly in the mercury mercury path and so this is problematic and worse like you know even you build multiple liquid labs there is still like no compatibility between two liquid graphs you'll see we need some bridges to to bridge to the kilowatts and so like so what digibam is doing is that

like in a nutshell like the given circuit is like verifying what you see and virtual machine is doing in a circuit so instead of writing circuits for each smart contract you write a circuit this is more general and for verifying the execution of a econ virtual machine so basically like you need to verify that your signature is correct the smart contracts are loaded correctly the execution trace is valid and your storage is updated correctly so basically here like your smart contract is just the input of this evm circuit it's not you know you're building some circuit for specifically for some smart contract so like we have one universal circuit serving for all the smart contracts logic and before diving into even more detail like you know to give you a sense of what is evm so basically for for you

know they are like smart contract developer and they can write solid code which is a high level language for for developing depths on ethereum and then like you know there are three different levels on the language level you compile solidity and like other other evm compatible languages down to some intermediate representation ir which for example you so this ir is still very high level but it gives you enough information like for the low level details and because it still remains some like high-level semantics and secondly that the barcode level where it's you know well defined in the e3 yellow paper like so it's basically include like push pop and all those stuff and like so and the like third is that you you have some runtime like it's a use ethereum virtual machine and which run your evm bytecode up code of code so

evm is a stack visual virtual machine and that's why like you know another reason why it's hard to build like an executive circuit because in zk like it's more easier to build something which is register based so like you know this is evm and a little bit more like a buzzer comparison like you know there are several approaches and on the left hand side like software and ziggy think they are building some like language compatible uh leaky evm so basically like for startware if you want to you know uh write some smart contract in in their circ net you need to compile solidity using some external compiler called work and then compile that down to some readable cardo and then like run on their like current assembly code and then finally run on their ziki virtual machine and what they think they are using the rvm compiler infrastructure

and so they have they also have their circuit language called zinc but they are still compatible with solidity because you know like this lvm ir front-end you can support the error of solidity and also link and then it also has its own bytecode and compile that down to z-vm and for what we are building and also what polygon hermes is building is that we want to build some evm equivalent uh liquid up which means we need to interpret the bytecode of ecm virtual machine and so this they can even circuit the input will be the buy code it's even lower level and more compatible so but there are still some slightly different technical uh like approaches to to to do this like you know for political hermes for efficiency they also like you know compile the spy code to an even smaller subset of micro up code and then run on

their design still machine or called uvm and we are doing a more straightforward way like for each op code we will have some sub-circuit or several class gates to constrain like this opcode is executing correctly and then it will run that on our zika evm so and another maybe technical difference is that from the pruning system side we are using like uh the before they serve for to write the circuit we are using blockage optimization and then you for the recursive circuit we are also using planck and we directly handle the non-native field optimization but for polygon hermes i think they are using stark for to dealing with their their evm circuit and then use use planck or growth 16 to to frequently prove size and reduce the verification cost so that's basically some some differences

and now let's move to more more technical part and uh so the workflow of zika vm is shown like in this graph so basically uh you have a sequencer and you have prover so this sequencer will like is a fork of gas and you can receive transactions and then you execute transactions on your guest node and then it will generate uh some some like the execution trees like for them like include execution logs block headers transactions contract barcode and mercury proofs so those will be used as witness to fade into this leak even circuits so so i use the event circuit because it's actually composed of many different sub-circuits for example there is a cache circuit for for proving that cache has relationship is correct

and there are a lot of other sub-circuits and those are all some components of the given circuit so after you know using this witness and running some you know the given circuit you got multiple proofs and each for for one specific circuit and then you've got some aggregation circuit to verify that those proofs are correct and then you generate some aggregated proof and then you submit this proof on chain because you you want to reduce the verification cost because you don't want to verify too many proofs like you know in smart contract and then together with some data and you can you know like your transaction is valid so now let's move to some even more technical part like the architecture of the leak even circuits so basically from the top there is the evm circuit which is built for verifying

the the execution or the state machine because you know like when when evm is executing the bytecode it will up execute opcode of code right so each op code will be a statement one state in the state machine and so this evm circuit is for writing constraints to constrain that this state machine moves correctly from state one to state two and state three so let's use evm circuit and uh so you basically you need to write some constraints to constrain the consensus machine and also like for for each like you know within one state there is up code right so you you still need to write some constraints to verify that this op code execute correctly so then you meet challenge one because there are so many zkm friendly op codes for example like there are the bitwise

of course which is super hard to to to to prove in z circuits because you need to basically you need to decompose the value into beat and prove that every bit is zero or one and then like you know combine them together and prove that it's it's your value and and secondly that you know you have char three and all those you know really the key efficient uh op codes and so what we are doing is that instead of doing all those constraints in this evm circuit we will just do some lookup operations so basically i will just give an example like for example like if you want to prove that some value is within the range between like for example like 10 0 to 10 so what you do is that you generate a table so this table like each entry is just you iterate from 0 to 10 so it's

basically this is a table single column it's zero one two three and uh under two ten and then like instead of proving that some value is within the range of zero to ten you just prove that this value belongs to this table because if you belong to that table it's absolutely true like you your range is within 0 to 10. so that's fixed table like you can when you are doing some bitwise of operations you can just look up that you know you have some table which just iterates all the possible you know like possibilities for for the you know for example like we are doing operations you just iterate all the beats and then get the result and you prove that this entry belongs to that table and that's enough and for catch-up table uh it's the same like you know when in evm circuit for example like you

need to prove that this input and this output has some uh hash relationship and instead of writing all the constraints in event circuit you just look up whether this input and this output belongs to some table and that table is actually you know storing like you know all the input and the possible output for for calc now let's just assume that this table is generated correctly because you know just assume that there are some magic like you you can generate this table and which you know has all the correct relationships between the input and output uh and the challenge tool is that as i mentioned like you know your easier virtual machine is a stack based virtual machine so you need to verify that stack memory and storage operations are all correct so what you do is that you have some ram table and for each operand you

will just look up that whether these operands belong to that table or not and also like you know i will give more detailed example like later and so that's that's how you do like stepper stack and memory operations and the third is that you also need to prove that the op code you fetch that is correctly fetched from from your bytecode so you need a barcode table and also you need some transaction table to prove your signature and broad context table to prove some other context variables and now like you know because like basically what i i just do is that you just assume that there are some magic and there is a table there and you just you know look up everything there but you know like in the first place you don't even know like whether those tables are correct right so you need a

lot of sub circuits to constrain that those tables are correct so basically for example like in catch-up table you have some cache circuit like for for for proving that you know this input and this output has this cache relationship so in this case circuit you prove that this cache table all the entries in this cache table input and output has this correct mapping relationship and for ram table because you involve some storage operations so you also need some markup potential tree circuit and because you you know like ethereum virtual machine your mpt is actually also composed of cachex so you also need to look up your cache table and the front to to get to know that this cache is correct and also like you have some ram circuit for constraining that ram table so i will give more detailed example like you know

it's still a high level overview and for back code table you prove that your your bytecode has some correct code hash and there is a transaction circuit for constraining that you know there are your signatures cracked and you there is a ecdsc circuit for proving that your signature is turbo is correct and there is a block circuit now let's move into some more zk and technical detail which you know it's especially for for for you guys like you know who are they already zk experts so uh to write a circuit what we are using is that we are using some ultra planck or sometimes called plunk case optimization so basically idea is that instead of you know r1c is just just linear combination times linear combination equal to linear combination so but you know we are using a more flexible way we are using a table

to represent your your your your constraint system so when you need to fill up you know your values or your weakness you need to fill up some you need to put your values into some cells and then like you know after after you fill up all the weakness this table will be full of variables and then like you can define some customized relationships for example there is gates for example like we pick up some region which is you know in the right right area and you can define the relationships for those cells like within this region i will give now a more detailed example for example like you know you have you have some layouts like like that and you have you have variables zero vb zero vc0 and all those you know those are values you filled up in this

table and then like for example you want to prove that v5 times vb5 times vc5 minus vb6 equal to zero so you just write that as your constraint and what you are generating in the backhand is that you generate three parts you generate one polynomial constraint which is what i call custom gate so basically so the first column you interpret that and you will get a polynomial for the first column you and similarly you will get the polynomial for the second column and the third column and so like you know because we 5 belong to the first column and so you write a 1 x times a 2 x times a 3 x minus a 2 omega x because omega is actually your shift because you are because your your interpolation actually happens on some

fft friendly field which is um two factor of of uh it is just some some two two factor and exponentiation of two factor so that's how you are writing constraints but you know uh if you are more familiar with zkn you know like uh at the end of the day like you need to linear combine all those gates and using one vanishing argument like you know it needs to be divided by some x powers n minus one because it's it's need to vanish on all all those rows but so so basically you know these constraints can prove that all the v i times v bi times v c i minus v v i mean i plus one is equal to zero but what you really want is that you just want that specific area so what you do is that you you can have some

selector polynomial which is an actual column so that this is a pretty sparse and you just open at a certain position like that that area is one and then you multiply with this this polynomial f x is a selector polynomial which is interpreted from that column so that's you know other entries are just zero and there is just one there and so so because you know all so this equation should be hold for all like you know iterate from omega power zero to omega powers a minus one and because you know only only that row like you you got you cause you got zero you you've got one there so you only you can you you can only your constraint is just constraining that specific area so that's like you know how you are writing custom gate and the second thing you can

use in plunkish optimization is that uh you can have some very flexible lookup arguments for example like your traditional lookup argument says proving that uh like a0 a1 and a2 columns all the values in those three columns belongs to a table like t0 t1 and t2 so that's what you would what you have like in your traditional arguments but what we really want is that we want to look up some specific entry right so it's similarly you can also have some selectors there and just multiplying with your input expression and you just prove that this polynomial belongs to this table and that's it so that's basically like two tools we can use for writing our circuits one is custom gate and one is arguments now let's look at the event circuit layout so as i

mentioned like evm circuits for writing constraints for constraining your your state machine so basically you have a lot of states and the freedom and like we use law to distinguish that in your your position in circuit for example like you there is slot i meant one there slot i there slot i minus i sorry i didn't yeah and like each slot will correspond into some op code here like for example like the first two rows are for push and then like next several rows are for add and those laws are for multiplication so basically you need to write all your constraints to constrain those up codes like within that certain number of rows and more specifically there are three different uh like ranges like within one one

one slot so there are the context because you need to store the context of your state machine for example there is program counter there is stack pointer there is a guess and a lot of other stuff it basically means that you know when you are executing your your sim machine like like when you reach that step like you know what's your problem program counter with your stack pointer and what like how much gas i did you left and secondly the up code and switch region like so basically like you know when this if this region is at then you need to open a selector at this selector add cell so basically we are not using too many extra uh selectors for constraining a certain area but instead we are just putting them all in some some region and then like you multiply with that with that

number and third is that uh we have some operating values which is three allocated for some up code specific circuit for example like you know when you are writing add and you need to you need three operands right you need to prove a plus b equal to c and sometimes you need to carry and those those more of course specific weakness will be filled up in that region and now let's look at a more more detailed example like how we are really writing constraints so for example like after you're getting the execution trace you'll know like what of course you are executing and all the related witness so firstly you need to fill in the context of the machine like you know if you're executing this state and what's your program counter number what's your stack pointer number and what's your guess and

second is that you need to set uh as as add to be one others are just zero uh and then like you you need to fill in the operand of add so there is way a v b and v c and carries because evm word size is 256 and we are working over the scalar field of bn254 to be compatible with the serums pre-compiled so each cell you know it works over a finite field which is 254 bit so like it's it's not enough for for you know just putting one 256 bit so we just decompose that into 32 eight bit numbers and so that's why like we have uh you know a long a sequence of variables there and so that's that's how like you know a more concrete you know deeper looking

to the the add up code and so how are writing constraints so basically to because we are not using actual selectors we are we just put everything here so we need to prove that the switch here there is just one switch open so for example like we we need to prove that uh s at times 1 1 minus x at equal to zero because you know although that should be one or zero and also you need to prove that there is at most one open so in proof that everything open equal to one and secondly that as i mentioned like you need to proof for some ad specific logic right so you it's it's so as i said like you know uh you you can you can define relationships over over certain cells so you can just open that as add and multiply with other

constraints you have because only if that as add is is one you need to prove for those relationships so those are the constraints you needed like you know v 0 plus v b 0 minus v 0 and minus some some carry because you are using eight bit for each cell so that's why you have like 256 here and now let's move to some constraining the context of this uh three translation uh so basically you have you have as adds two as added there because if your this slot is proven for for add and then it means when you move to the next slot your program contains plus one so you prove that if s add is open and then your program counter your next problem program counter minus this program

counter minus one equal to zero and then similarly you can you can also prove with stack pointer and guess so that's that's for uh the the unrolled constraints for for certain up codes and now let's move to a more more more complicated uh like example like the ram table and how we are we are using circuit tool to constrain that a table is generated correctly so basically for example like you you you this example is u for add for example like you uh your ad is you need to prove that v a times v b equal to v c right so your first operand is a second operand is v b third operand is in is vc so you you first really need to prove that this va is fetched correctly because you know for example like you when you are doing

add you need to pop two elements from the stack and push one element back so you need to prove that this this popped elements is exactly you know when you you push in previous operations right so you prove that this operand belongs to some to some entries in this table so there are so many columns and you need to prove that so i'm doing the stack operation this is my stack pointer and there i'm doing read all right and with the value and then you need to prove that it's consistent so this is basically how this run table look like you need to prove that some operand belong to this table and now here comes a question like you know and this is for you know you pop two and you push push one so every operand you need to prove this

relationship post three minutes oh okay okay yes sorry i just need to go very quickly so so like you know here's some question like as i mentioned like you know because your each sale is just 256 feet and you can't actually fill v8 here right so what we are doing is that instead of putting there here we are using some random linear combination to combine different eight cells into eight bit number into one one encoded value a and then like we just put the rlc encoded random linear combination combined value here like in our ram table and then instead of you know looking at that one you look up this linear combination and then the problem is that you know your table is not constrained so i i need to write some circuits here like to constrain that you

know your table is generated correctly but you know like during the execution you are not you know doing all stack operations one by one you are actually doing stack operation memory operation and then maybe you again like stack operation storage option so it's it's a it's just math here this is your real execution trace but but you know the problem is that when you need to prove a stack you need to prove that it's it's consistent with previous stack operations so you need some sorting so when we are filling with the table we store the rows based on tag address and rewrite index and then second we we can more easily prove that the previous rewrite value is equivalent to the value you are using now because you know the address and the tags are just consistent and you need to prove that the the column values are

valid because for example like you there is just three steps three tags and uh and all those stuff and you prove that you know some other other related variables and finally that uh it's not just built by us it's actually we are using the the hello to optimization so we are highly using the halo 2 repos so we really appreciate that the builders who build hello to repo and also like there are a lot a bunch of members from mission foundation especially the applied kp team and we just credit all the community members who build this together so this is our roadmap we will firstly have some poc demo for the key vm and then testnet and then like you know we will have some other features like outsourcing and move to mynet and finally last sorry last night like we are hurry and check

out this website and uh thanks for that so if there's a question we can take questions to implement and why like for example uh yeah yeah i think you know there are like different different groups working on different i think like car check spends the most long time because i remember like they take it takes a month for for the especially for the variable paddings but that's a different sub-circuit but if you are talking about the specific evm circuit the switching logic i think is called because you need a lot of variable related to the code

context and also like you know you also need to care about the reward which i think revert and call should be the two to you know hardest op codes in this evm circuit but you know there are some other operations for them like you know you need to massively optimize for non-native field for ecds circuit to make that really small and also catch so there are like different challenges like you know all around but if you are just talking about the state machine transition i think it should be core and rework okay go ahead uh as i understand we have like really a lot of variables and so your blanket is a little bit modified yeah and what is the maximum number of constraints you have

uh i think roughly we have over 1000 customer gates like there are so many polynomials there we are still doing some messy optimization for this part and also like i think around like 100 lookup tables that's a rough very rough number before we we do we have done more optimization for for for call because for call like it needs like just over 100 lookup tables to look up all those all those bytes in this ram table so like the conclusion is that we need like for example like one thousand customer case ones on customer polynomials for for for writing those constraints and it will definitely result in a lot of ffts and multi-scale multiplications in the backend if that's does answer your question it's good sure

but you're you're eating into your own lunch time yeah we can talk offline maybe yeah go ahead oh god group okay and data recursive course how are we talking these two problems and also if it is with a non-native field for the recursive part how efficient is that yeah i think i i guess i got some numbers but i can check that offline but i think it's maybe around like it depends like how many columns you are using i think uh like there are two versions one is a highly automatic highly optimized version where you use slightly more up more columns but it can roughly get down to i think 30k for for one non-native field of uh optimization on

ud curve if you are using slightly smaller columns then like you you need over like 100k i think like i can check with you later like perfect so thanks for everybody for coming [Applause]