ZK14: Miden's Arithmetic Circuit Evaluation (ACE) chiplet - Adrian Hamelink (Miden)

Transcript

Okay, let's get started. Go ahead, Adrian. So, hello everybody. I'm Adrian. I work for Maiden. I do cryptography there. And today I'm going to be talking to you about a very specific part of our proof system, which is the arithmetic circuit evaluation chiplet. Now, it's technical, but I want to bring this more into the light of like our overall recursion strategy and how we try to put everything together uh to make it uh to to to make it work. So, as a reminder, Maiden is a private ZK blockchain, which >> Oh, I'm sorry guys.

Uh Maiden's a private ZK blockchain, which means that clients generate proofs locally. These are sent to the network. Uh they're batched and aggregated together. So this single proof gets posted on chain. Um, one of the requirements is we only want a single VM. We want to keep things simple. And so for recursion, we don't really want any specialized circuits or anything. We just want to use the same VM. Yeah. Uh, the binded VM itself is a very narrow stark. It's composed of two traces. The main trace is basically the CPU. It does a decoding stack operations. Uh, you write programs in Maiden assembly. It's a stack based u CPU and for expensive operations you have the chiplets trace which

accelerates some things with custom air constraints like the hashing uh for now we use Poseidon 2 we'll see later uh bitwise operations memory and this is where we're going to put this uh arithmetic circuit evaluation chip uh to help accelerate things um there you go so so um like if you think about verification like a lot of it is very much like imperative it's just like doing a b bunch of beta data checks via chamir etc uh and for this like a standard VM is pretty good but there's two things that actually dominate the proof verification time the first one is the uh the merkel tree verification for the fry queries um this is actually supported by default because we have the

hashing chip uh and so this is not really a problem but the other problem is the uh fry or deep ali check uh which is essentially evaluating your air constraints instead and out of the main point and so this is a part that we still that we wanted to optimize. So uh but why do why do we need to optimize it like this? So the VM already supports extension field arithmetic uh directly but uh we tried to do that directly in Men assembly but the problem is when you're evaluating an arithmetic circuit um the even though your operations are cheap it's how you store and treat u uh uh store the data and it ended up with a lot of overhead because

of a lot of stack manipulations lots of memory reads and writes. Uh the other problem is that we would have to generate code maiden assembly uh which is not easy uh and we didn't want like an extra uh compiler pass on all of this. One of the requirements is we wanted a single source of truth for our air constraints and so basically this was not an option. Uh as a reminder we so we write our constraints in air builder. Uh this is just a simple example. Um you can represent circuits as like small DAGs uh where the leaves are the input values and then you compose them to build expressions. Uh why is this okay? Um if you have multiple of them you can share

variables between them. So you see the the s variable here participates in both constraints. the but when you're doing this out of domain check you're you need to build this uh composition polomial including the quotient the zerifier and so on and so this is a polinomial that when you that you evaluate as part of a verifier and you want to check that it evaluates to zero so this is what we want to use the ace for it's to take this graph evaluate it and check that the root evaluates to zero so actually if you think about it like most CK protocols are essentially just checking arithmetic circuits Uh so we had a lot of things to choose from. We chose to go with something plunkish actually because it's simple and uh we all know how it works and as a

reminder the idea is that you represent uh you create a table uh each row represents one node in the graph. Um you you connect them using wires. These wires are instantiated with a permutation argument. Uh but we or log up for example. And so what you do is you check each row uh that each row is correct and uh you you you then check that the multiplicities of the wires match up so that all the values which are supposed to be the same are actually the same.

Um the other thing is like so like we could have just built a plunk zk proof system but that just means that's just really complicated. So instead we wanted to integrate that as part of the VM and so this is sort of the pipeline that we use. So we have the circuit description derived from air builder we read that as a witness and as we're reading it we hash it using Poseidon. So this is a bit inefficient. Some projects use pre-processed tables and so on but um this gives us dynamic behavior. As we're evalu uh hashing the circuit we write it into memory. Uh in the same memory region we also write the other proof input. the out of domain points, the public inputs and stuff like that. And then we just call the ACE chiplet and ask it to evaluate the

circuit with the data in this memory region. So this just plugs in very easily to our existing workflow. This is what it looks like more concretely. So on the left hand side you see how the memory is laid out. There's a couple of optimizations we do uh or pessimizations if you want. Like for the constants, we treat everything as an extension field element. We try to align things to the hashing hasher rate. So that's uh we use Poseidon. So that's with with width 12. So we have eight elements permutation. Uh our operations which need to encode the operation and the node indices that those fit in one goldilocks element.

And so as the when we eval when we call the ACE chiplet um we start by loading all the inputs into into the circuit uh writing the wires as we go along uh along with the multiplicities of how many times they're used and then we go into an evaluation section. And this is the plunkish part where we go over every single row, evaluate it, and um the the wiring check is actually implicit thanks to logup. And we're actually able to use the same logup bus that we use for other parts of the system. And yeah, then there's the final um zero assertion.

So yeah, so that's kind of like what I wanted to like bring up overall is that like the way we optimize things at Miden is not always like optimizing. We try to optimize uh for simplicity, uniformity, um also not giving us too much work either. Um we find that like often even though we might do things less efficiently, it actually ends up faster overall. We care about the end-to-end uh performance like how fast can you recursively verify a proof on a consumer device. Um this means that sometimes we include more data than we need to but to make the actual implementations faster.

Um and so just for some numbers like we have so as I mentioned the chiplets trace is like only 20 columns uh our entire stark is 80. Um, so ACE fits really nicely in that. We can recursively verify a proof in about 32K cycles. Um, and on a consumer laptop, it takes about a bit less than a second, though we expect that to get a lot better. And for now, depending on the security parameters, we're between 100 and 200 kilobytes. But the advantages are more than that because uh even though like it might be inefficient to hash the circuit using Poseidon dynamically inside of the proof inside of the program. What this means is we have a very dynamic system and so

we can very easily support different errors uh verify multip proofs of uh different um uh I mean different errors. It's very easy to upgrade because you can use the same VM. can you can just uh upgrade uh the hash of the circuit and so everything works the same. So and in fact like this uh when we transitioned to multi-table support in Starks uh the change was almost trivial and we expected also to work super simply with our upcoming pre-ompile VM which maybe I'll talk about in another time. Um so yeah that's it. Um I hope if you have any questions like uh feel free to ask

me. There's also the docs which are a bit complicated but check out the source code if you want. Thanks. >> Thanks Adrian. So we do have time for questions. >> Is it available to application code as well or just for recursion? >> Um wait you mean like can you verify arithmetic circuit? Yeah. Yeah. Yeah. You can. Yeah. Yeah. Just Yeah. >> Might be a bit of work, but >> how and where is the commitment to the air supplied to the guest program or does the guest program bring it baked in

or how does that work? >> Uh so I think the way it works is so we have recursive verification program. I think we embed as constants the hash of the circuit and so as you're recomputing the hash uh once you've recmp computed the hash you compare it against that. So technically the program itself depends on uh like you would re get a new program if you upgrade the circuit but this is something we can change later on. You could get the hash from like the network or whatever. This is not directly rel related just a related question about proof size here

like you say 100 to 200 kilobytes. Uh so what are roughly the parameters? How many columns are you running? And >> we have 80 columns. >> And blow up is kind of >> Yeah, we use blow up eight because we we one of the things we optimize for is uh like we want to pack things as much as possible and for that we often use degree 9 constraints. So this is like a part of the whole design. So with the with blow up 8 uh we get to also reduce uh the number of queries >> in LDR I suppose.

>> Uh you might want to ask the person on your right about concrete details. >> I don't know him. >> Um have you so you mentioned you use Fry for the the PCS. uh have you looked at other perhaps more recent uh PCS such as we or tensor switch? >> So we just recently upgraded our proof system. We were using Winterfell and now we have a custom implementation using plunky 3. Um what it's actually lifted fry. This is something I talked about last uh last edition. Um we chose fry because the recursive verifier was already written. Um it works. We are looking into others. Uh I think for now

if it ain't broke don't fix it. Uh but if anything we'd look more into stir uh than were because of the recursive verification like the multilinears are hard to evaluate uh in mazm. Well thanks a lot guys. Thank you.