zkEVM #03 - Devconnect AMS'22

[Music] okay so here's honor he's gonna he's gonna talk about mpt hi uh it's honor thank you for having me here i will be talking about non-native arithmetic in circuits i tried to prepare some slides but in the end it turned out to be something like a guide and i will walk through this document so equations here might not be so accurate my goal is to give some intuition how it is done so we say we have two fields one is native and other one is wrong native field where we constrain equations in circuit and wrong field is a which one it which is not equal to the native field i couldn't find however how i can do that if we can't figure it out fast top right corner the triangle triangle wait no that's not a direction i don't know how to do this either who's laptop so there are some applications that we use this wrong field arithmetic one of them might be aggregation or recursion of the same circuit this is where it's a there's a multiplication a plus the a multiplies the point x and y and x and y is a is in base field which we call wrong field here this is a scalar multiplication and the other example might be the ecdsa and in with the ecdsa we use that curve say p256 and in that curve scalar field also is non-native so in the recursion site we have the scholar in the native field so for that purpose we built some stack that uses holo 2 as a background we in that stack we support the original the zk hello 2 which uses the ipa commitments and our fork it's applied the kp slash hello2 and supports kcg commitments so our stack looks like this on top of hollow 2 we have a main gate that implements a standard like blanket with additional multiplications and stuff on top of that we have integer a big integer crate on top of that finally we have ecc so with that stack we can implement recursion or ecc circuits so other implementations are we follow we mostly followed the aztec spec aztec spec is also implemented in baltimore and metal labs also very similar implementation also scroll has other inter independent implementation of big integers so our main gate is looks like this it might not be the best way to represent a gate but so i hope this is familiar to you in we have five witness columns a b c d a b c d and e and two multiplication gates here and we have a one further rotation and in the end there's a cost constant fixed call so we have a 5 bit gate because it is good for arranging 4 limbs which we often use and further rotation is used for running sums and the two multiplication in a gate is a good for applying conditional selections in a single row so main gate also implements this basic arithmetic conditions assignments and equalities between witnesses we also want this skate to be visible to verify on chain because this gate will be there where we implement recursion stuff and this gate will be verified in layer one contract so let um zoom out a bit this is how we represent integers in this example where we see four limp representation first of them are b bits and the last one the most significant one a bit shorter than the others so we also have another special limp that holds the nature failure which is a combination of these limbs under the native field so we will need this native value in multiplication process also in synthesis time when we synthesizing this circuit we want to keep the maximum value this integer [Music] might be to defer some reductions so we apply reductions when this integer goes beyond some specific limit so when we assign new witness integers we arrange these limps first to be b bits and last one must be b most bits and then we also constrain the native value under native modulus this is trivial to compute because it is under the native field so we also in since this time a maximum value will be assigned to 2 to the power m which is the next power of two of native value for example we have native field for example we have 11 for the native field modules and then this value should be 16 minus 1 right 16 is the next power of 2 this modulus so how we arrange these integers when we are assigning we as we said we have two columns witness columns we just split a limp into a sub limbs in our implementation this in our implementation a limp uh is a 68 bit here and b most will be 18. but in the sublimps we divide this integer into four uh sorry uh four uh [Music] sub beams will be um each of them will be 18 bits so we just combine them together and see if it's equal to the actual lip and we also range a b c d e a b c d these four columns to be in this specific limit for the most significant bit we have a special range for b column which also arranges the overflow which is shorter than the actual table so we also combine them to see if it is equal to the e column a so addition is a pretty straight forward we just add limps together and don't apply reduction until it's strictly necessary when until it's go beyond some limit and in the synthesis time we also attract the maximum value of the new witness subtraction if we apply subtraction in a way that we applied addition this might is probably this limps resulting in probably underflow so we want to stay about zero uh this underflow which can be a pretty big number just less than modulus to avoid underflow we pick an auxiliary value and add to the a beforehand this executable axillary value must equal to the wrong modulus non-native modulus but it should also move left hand side operand do left hand side apparent above b and how we can do that because we tracked what maximum value b right hand side can be and we pick an auxiliary value this auxiliary value will be constant and can be take place in a fixed column so this will be these regular will be assigned in synthesis time multiplication a bit will be a bit trickier but in the end we want to satisfy this equation two operands and the right hand side questioned and remainder will be the our new witnesses and as they are near they will be assigned and they must be subjected to range checks we will constrain this equation in two fields or rings first one will be under native field which is pretty straightforward and a single row equation we remember we keep all integers native value just after this limp so we can just compute or constrain this stuff uh press it for so uh we will also do this thing under modulative what is tt is the uh for example example will show it better let's say our limbs are 68 bit sized let's say we have four limbs then t will be 2 to the power 2 7 2 okay this number also should be larger than our other two fields why we are doing this second stuff modularity stuff because we were about to use china's remainder theorem so if our goal is that if two equation holds in a different modulo so it must imply that same equation must also hold in wrong field modules but in some certain conditions say we have we constrained these two equations to be zero that's holes in a t and native so this problem has a solution in a key multiplies native and t so we want k to be 0 also if not left hand side equation a and b and the right hand side might wrap n times t then it would be some soundness errors because plural can find other values that actually not holds this equation but with some valid witnesses question and remainder so we need to arrange this guys accordingly remainder will be a next integer that we will be using so it should be arranged as usual which is the next power of the wrong modulus and the quotient should be in this range so for sorry the right hand side should hold this equation it means it should not wrap n times t so we find the maximum value for the coefficient quotient so arrange this quotient accordingly so we also want these two operands maximum value of them should be less than right hand side because if not even if this guy less than n times t if this left hand side maximum value of this hand side exceeds the right hand side so we couldn't find some valid witnesses so there might be some completeness errors [Music] oh yeah one thing before we start multiplication constraints we need to check if operands are under maximum apparent possible value if they probably if they likely exit so we want to apply reduction just before the multiplication reduction is also very is actually very similar with multiplication but some simplifications uh quotient uh we keep quotient as single limp okay so quotient is not a big integer just for example 68-bit number so yes this is a simplified equation uh which is very similar with multiplication uh equality we said the value can exceed the modulus because we arrange it with next power of two of the wrong field modules so if we need to really check this value should be under a wrong field we should be in a field so we have a third less than modulus constraint so it can be used when we compare with some value comes from public inputs i think that's all and there is some appendix here about this multi constraints if you want to look at link is uh here in there thank you [Applause] um any questions for honor yes we support division and inversion actually they are how we do in the native field just check the if a multiplication is one yes but in the base we use for example multiplication in what this multiplication cost rate to make division thank you okay [Applause] [Music]