An Assembly Language for building zkEVMs.

Transcript

Okay, I think we are about ready to begin. All right, so my name is David Pierce. I'm going to be talking to you today about an assembly language for building ZK VMs. And in particular, this is a system that we are using at Linea for the Linea ZK EVM and it is running in production on Linea mainnet. Okay, so just a little bit of history about Linea ZK EVM. So as you may know, ZK EVM uses direct arithmetization to sort of implement our constraint system. So what that means is that we we manually write the constraints to implement the semantics of the Ethereum virtual machine. We do not use, let's say, a risk-5 ZK VM for example. We actually write the constraints directly.

So when the ZK EVM was originally kind of envisioned, I guess, we used this domain-specific language. It was a Lisp-like language for writing our constraints and you can see an example kind of at the top here. And so yeah, it has the Lisp syntax, of course. And what we're doing in this example, you know, the first thing I'm doing is defining some columns and giving them some types, so we know how wide they are. And then I'm writing a constraint down here as the increment constraint. And it's basically just a logical or of two equalities. And and this would would actually be translated would need a little bit more processing to be actually translated into an air constraint.

But you kind of get the idea. So I guess the the thing about these constraints is that, you know, they're very low level, right? We are literally writing constraints directly. And so that that is, you know, challenging to do for a complex system like the EVM. It's also difficult in the sense that people coming into the project are not familiar with this. It's It's not like a programming language. You know, even if you've like programmed and did something like Prolog, which is a declarative language, this is still a pretty foreign world. And so what we what we sort of wanted, what we're looking for is something that allows us to kind of iterate faster to make it easier for people to onboard, to come in to our project and you know, get up to speed. And we wanted something

that was more like a programming language. And I should add should add actually that that the constraints themselves are only half the story, that we also have to have a trace generator as well. And the trace generator is implemented in Java because we're connected with Besu. And so the trace generator is another chunk of code which has to be kind of synchronized with the constraints in order for the whole thing to work. And so that adds its own sort of level of complexity. Yeah. Okay, so so the idea that we came up with was this idea of ZK assembly. And so yeah, as we'll see, so this is a a small example trying to illustrate ZK assembly.

It's a max function over 256-bit arguments producing a 256-bit result. And so there are a whole bunch of things about this. But the first thing obviously is that we've got 256-bit arguments. And so you're immediately asking the question, I hope, how do you fit 256 bits into your field, right? That's a kind of a key question. And so the first thing about ZK assembly is that actually it's field agnostic, which means we will compile it down to the target field. So currently we support BLS12-377 and a koala bear as well. And so what that means is that and we'll see a bit more later, but it will split the variables into smaller variables, limbs we call them, which fit in the target field. So

it does that automatically. The next thing you'll see is that it's unstructured. So it is like an assembly language in the sense that it's it has unstructured control flow. So we can see the use of if go to here to implement our conditional. But it's different from an assembly language in the sense that like our assignment here is somehow more complex. It actually has an expression on the right-hand side. It's not like a just a a single sort of unit instruction. Yeah. So yeah, so we will look The obviously the main thing about the max function is the comparison. We'll We'll look at that in a little bit more detail in a second.

So So one of the sort of main ideas behind ZK assembly is the destructuring assignment. And so So this is an example of a destructuring assignment. The idea is that the amount of information on the right-hand side has got to fit in exactly to the variables that we have on the left-hand side. So the we we produce some number of bits and we consume some number of bits. And so in this case, we've got two um two variables, arg1 and arg2. We're adding them together. They both have type U8. And so that means we're producing a value which is which, you know, fits in nine bits of information. And so we need to have nine bits of information on the left-hand side. And so we've In this case, I've set it up so that we've got

our result is a U8. And then we've got this this extra variable C, which is In this case, it's a carry flag, which is just a U1. Now it doesn't really matter how we divide it. It doesn't have to be U8 U1. It could be you could do it differently, however you wanted. You could just make res a U9, for example, if you wanted to do that. Whatever you want to do. So the key thing is that this destructuring syntax is quite powerful. And we can actually use it in a number of ways, for example, implementing our comparisons that we'll see, but also other things like doing shifts and various things that we do. So it turns out to be quite powerful.

And also for those that are familiar with constraints, it's relatively easy to see how we would actually compile that into a vanishing constraint. It's actually quite easy. Cool. Okay, so if we look at the comparison, so this is essentially the same as before. The only difference is that this time instead of doing an addition, we're doing a subtraction. So we're subtracting arg2 from arg1. And so in this case, my flag over here, B, is not a carry flag, but it's a borrow flag. And so the idea is and this sort of takes its roots from computer architecture. The idea is that if arg2 is greater than arg1, then we're going to underflow and the borrow flag will be set to one, right?

And so we can use that to implement our comparison. So down below, we're basically making a check, is the borrow flag zero or one? And if it's one, then we're going to go to handle that case where arg2 is greater than arg1. And in this case, temp is is actually just It's basically just a unused variable that's there. It's It's a witness really is what it is. It's a witness to the subtraction. So yeah. Cool. So yeah, that syntax is is reasonably powerful for for doing comparisons, for example. Okay, so this is a slightly more complex example. The details are not that important.

But it's a counter. It counts up from It counts up M steps from from N producing a result. It doesn't really matter that much. The key thing is it has a loop, right? So we have a go to loop. So we have a sort of unstructured loop, as you might imagine in assembly language if you've programmed in assembly language. And yeah, so we support loops. We also support function calls, including recursive function calls. And recursive function calls turn out to be quite powerful actually. They're a fairly good way of implementing kind of unbounded computation because they're implemented using lookups and they they tend to be quite quite powerful. So we we we often use recursive calls rather than loops, actually. They're generally a bit more efficient.

Okay, so we talked a little bit about sort of the syntax of ZK ASM, how it looks. So now I'm going to talk a little bit about how we map functions in ZK ASM onto cryptographic primitives. So the cryptographic primitives that we have in our system are basically reasonably standard. So we have kind of these modules, which are sort of I've got module M1 and module M2 here. And these are basically tables. Each module has its own set of columns, has its own trace. And so they can have, you know, different numbers of columns. They can have different heights in their trace, you know, different modules can have different heights and so on. And then we can write vanishing constraints.

And there's actually a slight typo here. That should be M2, by the way. But we have a vanishing constraint here, which is basically saying that the columns, you know, there is some constraint over the columns of M1. Likewise, I've got a inequality here for the columns, which should be of M2. Obviously, that would be further processed and implemented using like a multiplicative inverse or something like that. And we've got a lookup argument down below at the bottom. And so the key thing here is that polynomial constraints go within columns in the same module. They cannot go across modules, but lookups can go across modules. And so we start to see how we're going to translate ZK ASM functions into this kind of model. So what we're going to do is every ZK ASM

function is going to correspond to one of these modules. Instructions of the of the function are going to be implemented using vanishing constraints. And function calls will be implemented using lookups. And that's the kind of base idea. And in our system, we also do have like permutations and stuff, but I'm not talking about them today. Okay, so when we're translating when we're mapping a ZK ASM function to an air constraint module, there is kind of two approaches that we take depending on the function. So the simplest approach is what we call a one-line function. And so max here, it turns out, is not perhaps obvious from the the source of the function, but this

actually can be implemented using a one-line function. And what that means is that every row in our trace corresponds to an instance of function call, if you like, of the max function, right? And so we can see, if we look at the middle row, we can see we've got arg1 is three, arg2 is one, and the result would be three cuz this is the max function, right? The borrow is zero because arg2 is lower than arg1. And my temporary is just arg1 minus arg2, which is two. Right? So that is one complete trace for max.

And so the key thing is obviously how do we go from this kind of sequential view of a program to this horizontal view of a program. And we're going to come and look at that in a in a little bit in a moment. Um so then the the second kind of uh function that we might generate is of course a multi-line function. And so this is a function where um we have multiple rows uh in our trace correspond to one um instance of a function, right? So yeah, one instance can correspond to one or more rows. Um they're they're not necessarily fixed. They can be fixed, but they're not necessarily fixed. Um and so in this case it's the counter.

And so essentially every time we go around the loop, you're going to get a new row in your trace. That's the way to think about it, right? Um uh and there are a couple of things that to note here about this. So in order to make this work, we've added some control registers here. So we've got a program counter. This tells us what instruction we're on. We've got a return signal, which tells us uh when we've reached the end, basically when we've reached the return instruction, right? And so the idea is that with the return signal, we're going to use our lookup to get the result out of the function only when the return is one. All right? Um what's not obvious is how the program counter maps to the program because basically it doesn't, right? The program counter here is only going to be

between zero and one. Obviously there are many instructions, but it's to do with this process of flattening our instructions, um what I call vectorization, that that gives us the actual program counter value. And so you can't really This one does not correspond really to that text over there in in an obvious fashion, I guess. Um a couple of other things just to note um so for example, arguments in this are constant. They don't change, but the return value can change. That can be built up as it goes along. And then obviously we've got all the other temporary values that we're using um and they're being accumulated and so on.

Cool. Uh yo. Okay, so we've looked a little bit how we map ZK functions to uh to the sort of cryptographic system. And now we're just going to look a little bit about how we actually compile the constraints itself and some of the challenges, I guess. Uh so the first one and I think the most interesting one is is vectorization. And so the goal here is to well, you know, what we want to do is we want to flatten these functions so that um ideally they take up as few rows as possible. We don't want to have, you know, lots and lots of rows with lots and lots of constant values because that's quite inefficient, right? So we want to kind of package them up into these sort of larger instructions. And so I call them a vector instruction. And so basically what the algorithm does is

it walks through the function and it just packages [snorts] them up into these vectors. And so um you know, the idea comes from sort of like uh you know, VLIW VLIW architectures, very long instruction word architectures, um or there are some other ideas um which are called superblocks as well. But anyway, it doesn't matter that much. But the point is we build up these vectors and then that is a is effectively one instruction for our trace. And and it will correspond to one row in our trace. And obviously there are some kind of rules that we can't just put a we can't just always put a whole program into one vector instruction. In this case, this is the body of the max function. In this case, I can put the whole body into one vector instruction. But for example, if it's a loop, then I can't

put it into one vector instruction. I'm going to require at least two vector instructions. And there are a few other scenarios. So for example, because we're flattening it, um there are issues around right conflicts. So uh so basically the algorithm has to detect right conflicts. We can't assign to the same variable twice. We well, actually that's not true. So actually as I'm doing it here. >> [laughter] >> But you can't assign to the same variable twice on the same execution path because then you would have a right conflict, right? So uh it basically has to do a a sort of analysis where it looks at the read and write conflicts. Um but there's some kind of cool things that I do here.

So we do some forwarding and stuff, which takes all of the inspiration from computer architecture. Um and also we do have control flow, which are these what I call the skip instructions. And so the skip instruction can go forward um basically in this case it says B does not equal zero, then skip two. And so it would then skip over to this instruction. So you can have some limited control flow in the vector instruction itself, um but you can't have a loop, for example. That's not a permitted. Um they basically the skip instructions always go forward. So that limits what you can do. Cool. All right. Uh so yeah. So then the next thing is what I call um branch table optimization.

Um so this is just a this is an optimization really. Uh so we end up often with these chains of um sort of it's almost like a switch statement where we're saying, "If op code is, you know, EVM add, then go to the add label. If op code is like EVM sub, go to the sub label." And so on and so forth. And so the kind of simple way of translating that is to go, "Okay, so on the true branch here, we're going to go to the add label." And so that's kind of what I've done down here. We've got if the op code is one, then the next program counter should be whatever the add label is. Um and then you go and then we have the false branch. So we get the false condition and then the true condition.

So if the the op code was not one and the op code is two, then go to set the next PC to be uh the sub label. But obviously we can see this is actually redundant, right? Like op code being two kind of sort of uh subsumes this issue of op code not being one. So in fact, what we want to do is just simply clean that out. And so that's the branch table optimization. And uh yeah, it's yeah, it's a little bit more complicated than that in some places, but that's the idea. Uh and that works quite well. Um and so then finally, the the issue of field diagnosticity and I yeah, I'm only going to touch on this really. Um there are a few issues to it, but you know, like a few challenges to go through, but um the goal here is that if we imagine

we're compiling a variable um to a like a variable that is sort of you know, bigger. So let's say uh so let's say in this case, we've got 256-bit variables R, X, and Y, and let's say C is just a one-bit variable, okay? And we're going to compile to our BLS curve, which means we're going to split each register into 128-bit register, double limb. Okay, so you can see the mapping down here. The mapping for R is the R is going to go to R1 and R0, where R0 is the least significant uh word and R1 is the most significant, and so on. Um but you see that C is not in the mapping because C will just map to itself because it's not it doesn't like overflow the field that we're we're targeting. Um and so the key thing then is that we've got to take this

constraint and we're going to translate it in this case to two constraints. Um and so I introduce this uh as dollar variable here, um but it's basically just a temporary variable that's introduced by the compiler, and it represents the carry coming from the first sort of adding the first word, and then it flows into adding the second word. And if you've studied computer architecture, then this is very much basically follows the line of a ripple carry adder. If you've if you've seen that, then you'll know what it is. Um it's fairly standard technique, obviously. Um if things do get more complicated when we have multiplication and so on. So it's yeah, this just gives you the flavor of what it does. And the tool does this automatically. You don't have to do this. You just write 256-bit value, it compiles it down, and that works.

And uh I think that is all. Cheers. Any questions? Thank you. Uh for your branch uh optimization technique, do you guys use also branch prediction or is this something is not really related to the uh language? Uh yeah, branch prediction is more of a runtime technique. Yeah, so we have to compile the constraints to a like a static kind of form. Um but yeah, so it's not so related, I think, but yeah.

It's more it's you know, it's a sort of like a standard kind of compiler optimization where we're just trying to optimize the code that's generated, I guess. Yeah. Just a question on terminology. What do you mean by unstructured unstructured uh branch flow, et cetera? Uh unstructured control flow, yeah, is just when you have um so like in an assembly language, you typically have like conditional branches and a and a branch goes to uh an instruction position.

Whereas in a programming language, you'd have like block structured control flow, where you have if true block, else false block, and so on. So it doesn't have that block structuring. It's kind of like a flat go-to oriented structure. Yeah. Uh and uh yeah, sorry if it was uh clarified during the talk, but uh how do you manage function calls? Do you use lookups for that? Yeah, so yeah, so that's a good question. Um so yeah, how do we do function calls? I didn't really show a function call, unfortunately, but yeah, uh a function call will be translated as a as a lookup into the function we're calling. Uh there are some like if you have multiple calls to the same function, it will try to reuse

it. Creates a kind of bus for the lookup, and it will reuse that. Um and if you have multiple functions, then it will create like multiple calls to multiple functions, it will create multiple buses so that you can still have a one-line function, for example. I'm not sure if I I got it, but is it a stack-based language? And how do you handle if so, how do you handle stack overflows if if it could happen? It's not really a stack-based language, no. It does support expressions, and you can you can write kind of arbitrarily deep expressions, um but it will it will translate them. It It does a kind of check to make sure that they don't well, if they overflow the field, the

underlying field element, then it will split the constraint to make sure that they can't overflow effectively is what it will do. So if you if you end up with very deep expressions, it can end up generating a lot of constraints potentially. But but generally, our constraints are things like z equals i equals i plus one and you know, relatively simple things. Yeah. Yeah. Thank you. This Yeah. I don't really understand like the zero knowledge part in this presentation. Like are you trying to generate a proof for the execution of the program? Oh, how does it exactly relate relate to what you presented? Okay, I mean that's a It's a fair comment. I haven't really I haven't really talked about at all the constraint proving side at all. Um so my

my friend Alex here, he does all the he does the prover. He He implements our prover. And so I generate these constraints and I pass the constraints to the prover along with like a we generate the trace witness. So I haven't talked Yeah, I haven't talked at all about the trace witness, but to generate the trace witness you execute the ZK ASM program and just extract the value of the variables at different points. And then I pass it to Alex and he does the actual constraint proving using a lattice-based system. Yeah. Yeah. Um when you had multi-line functions, does it generate also like certain scaffolding constraints to

sort of impose a structure? Is that implicit? Uh Uh for the control variables. Yeah, it does add um yeah, I don't know what you would call them. Yeah, constraints specifically to manage those control variables. Yeah, to make sure certain things like um you know, the return value uh once you the return is one, the next program counter has to be reset and things like that. Yeah, that's right. Yeah. Yeah. >> [applause]