Fast Binary Field RISC-V Proving

Transcript

So, this talk is about Magnetar. Before I start, I have two two disclaimers. I'm operating in Pacific time zone, so it's I think 2:00 a.m. or 3:00 a.m. there, so if something I say doesn't make sense, please ask me tomorrow. Uh So, uh thank you for having me. Uh so, this talk will be uh about Magnetar, which is a ZK VM for RV64 programs. It's fast, it's post-quantum, and its security rests on standard hash functions.

Uh so, this talk has two parts. First, I'll discuss what Magnetar is and uh how it differs from prior ZK VMs. And then, I'll give a look inside Magnetar. So, let's recap what a ZK VM is. So, a ZK VM proves that a program ran correctly. So, the developer writes a program in some normal programming language like Rust, Go, or C. An existing compiler turns this into RV64 machine code. The prover runs this program, outputs a result Y, and a proof pi.

The verifier checks this proof and without re-executing the program. So, the circuit that the prover uses here encodes the processor once, so we don't have to encode every program inside a circuit. So, there are no circuits to write. So, for Ethereum, what this means is we can take EVM written in Rust or Go, and then directly obtain a ZK EVM that can prove existing contracts. Once we have this, nodes can now just verify a single proof without re-executing the blocks. So, this is all I'm just recapping uh uh what a ZK VM provides.

So, of course, the proof system underneath determines the speed, security assumptions, and recursion. Uh let's start with security assumptions. An analogy with uh signature scheme uh schemes could help here. Of course, both signatures and ZK VMs face the same question. What does the security rest on? ECDSA, for example, relies on elliptic curves, so it's not post-quantum. I think the ZK VM analog for this is Jolt with Dory PCS. It's the the analogy is not exact because Dory also requires uh pairings.

Uh, ML-DSA rests on lattices. Its ZK VM analog is uh Jolt with the Akita PCS, which also relies on uh hints. For hashes, the signature scheme is SLH-DSA, but my claim is that the ZK VM analog of SLH-DSA is missing. There is one example, Lean VM. It uh rests on standard hashes, but it targets this simplified Lean ISA, so it's a specialized machine, uh does not cover a general ISA like RV64.

You might wonder what about other ZK VMs, for example, SP1, Hypercube, Risc Zero, Risc, or many others. Many of these are called hash-based because they commit to their witnesses with Merkle trees, but the security relies on more than a hash function. For example, SP1 relies on an elliptic curve-based uh multi-set hash function for checking memory consistency. So, it's not even post-quantum. It also targets just 100 bits of security. This comes the closest. It uh relies on Poseidon, but recently they switched to Blake3.

But even with the switch, uh uh it still uses a lattice-based multi-set hash function called LT-Hash for distributed Fiat-Shamir hash generation. These schemes also rely on uh grand products or grand sums. As a result, they uh lose soundness that's proportional to the size of the instance that's proven. So, for example, if you an instance of size million, you instantly lose 20 bits of security. So one call to action, I think we should reserve hash-based ZK VMs for the ones that rest on standard hash functions alone.

So, this brings me to what do we want from a ZK VM? I think there are three properties that we want. One is general-purpose proving. So, it should target a standard ISA like RISC-V. So, so we can use existing tooling and languages. So, we want post-quantum security from standard hashes. For example, it should use SHA-256 or SHA-3 across the entire proving machinery. No elliptic curves, lattices, or algebraic hash functions like Poseidon or Poseidon 2. Should not require a trusted setup. Also, no conjectured proximity gap results.

Finally, the system should support efficient recursion. This means that a verifier of the proof system is is very cheap, and also it's an efficient workload for the proof system itself. As a result, [snorts] the the system can scale to any size computation, and it can also support applications like succinct blockchains. So, a key question that we ask in this work is can a single ZK VM have all these three properties and be faster than all the existing ZK VMs?

The answer turns out to be yes. So, Magnetar is the first ZK VM that meets all the three properties. So, it proves RV64I programs. So, for example, an EVM in Rust or Go becomes a ZK VM automatically with Magnetar. It provides 120-bit security from standard hashes. Uh it uses SHA-256, no curves, lattices, or Poseidon. It proves uh 6.5 to 7.7 million cycles per second on a laptop. This is an order of magnitude uh more faster than existing systems.

Proofs are about 600 kilobytes and can be verified in 12 milliseconds. And the verifier itself does only hashes and binary field arithmetic. So, proving a a verification of a proof is an efficient workload for the prover. So, where does uh Magnetar come from? Uh so, here is a a small depiction of uh all the works that lead to Magnetar. So, at the proof system layer, uh we rely on Spartan from 2019. So, in 2019, there was a a variant of the Spartan called Phalanx, uh which made Spartan apply to this uh computations that have repeated

structure. And this is uh uh this repeated structure shows up uh when proving a processor. For example, every cycle So, you uh for proving a processor, you have many cycles, and in every cycle, the same thing happens. Uh and then uh in few months ago, I built this binary Spartan that takes Phalanx and Spartan itself and applies uh techniques from the binary field uh uh line of work. For example, the ring switching Lego Lego uh to get a proof system, and it targets R1CS. So, the immediate predecessor for Magnetar is this binary Spartan proof system, which proved R1CS constraint systems.

So, in parallel to uh uh proof systems, so we also have memory checking protocols, which are crucial for building a ZK-VM. So, back in 2023, we created a a proof system called Lasso. This was a a specialization of Spartan to uh uh to up arguments and memory checking. And this is what led to JOLT, which is also a ZK VM for risk five. And then more recently we have this twist and shout, which improves upon Lasso to get a faster memory checking argument.

And Magnetar builds on both of these lines of work. One is binary Spartan and twist and shout. So the story makes sense. It seems simple, seems sensible. But I argue that Magnetar is a contrarian bet because these are some of the codes Justin earlier was talking about how there were codes from various experts on how many things may not work. And here are things that uh uh claim that Spartan cannot work over binary fields or twist and shout cannot work over binary fields. But turns out both of those can be made to work.

The main reason is both of these protocols don't commit to large values. And they also just commit to binary value. For example, twist and shout uh just commits to address vectors in one hot form as I'll show you later. And this can be committed very efficiently in a binary field. So before I switch, I want to open up and ask if there are any questions before I go inside Magnetar. >> Uh just a for this particular work at the moment you just focus on scalability not on ZK for now I assume.

>> Uh Sorry. >> Uh sorry, just to understand at the moment currently no privacy in this in Magnetar or but that's something that probably you can add easily afterwards. >> Yeah, so right now the implementation does not support ZK, but it can be added very easily. For example, I think there is a bunch of works including Bale. I think you also have some paper science pattern. I think there should be an easy way to add this to the minor system. >> I agree. I just wanted to check whether it was already the gate decay or just decay.

>> Yes, yes. It's for now it's it has no ZK. >> Thank you. >> So, one quick question like the numbers you have shown were on native CPU call or were you already using metal CPU acceleration on the Mac? >> No, this this is not using metal. This is just using 12 cores. >> Okay. >> I think I think with metal we might get another two three X at least. >> All right. Thank you. >> And the this the six to or five to six or six to seven million per second, is that implemented and benchmarked and do you feel like there's further room for

improvement? >> Yeah, so this is implemented fully and it's benchmarked on a real machine. I think there is some on the I think there may be two or three ways of improving this further. One is just prove it optimizations without changing the verifier. I think there is some room there probably like 1.5 X to 2 X there. And then I think even within the protocol there may be ways of reducing the work itself so it gets faster and then of course metal acceleration. So, I think all of them should give significant improvements.

>> So, we might be looking at tens of millions of cycles proven per second on a laptop. >> It's possible, yes. Also, this was on M4. I think on M5 we can already see probably another big speed up. >> And can we can we use like look up arguments inside this and offload computation because you usually in five we where we see get check we don't do get check like we we send it to a specialized circuit. Like can we do this cross table communication? >> Uh so it turns out not doing cross table communication helps lot more. I I'll come to this maybe it will get answered in the next few slides. So All right. So this is part two inside

Magnetar. I'm going to use these three things. So binary fields, one witness, one commitment. I think it will answer your question as well. We start with the core proving system which is binary Spartan. So binary Spartan is Spartan instantiated over binary fields. So here it's operating over F2. The addition XOR is an addition and AND is the multiplication and all the bit operations are native. So we pack 128 bits into a single field element and then commit to that packed witness.

Uh so we run SIMD Spartan which is an extension of Spartan that applies to repeated copies of the same circuit. Then we apply ring switching and then we just do one PC evaluation argument. Uh so the witness is all binary but the challenges and the sum check argument run over the extension field. And using this we build Magnetar. Uh it has five stages. So we first execute the program, we commit to this witness once and we're going to use a single commitment to the entire witness.

I'll I'll discuss what this means later. And then we run what I call virtual Spartan. So this runs a a dual SIMD R1CS. So there are going I'll come to this in the next slide. There are two circuits defined over different fields. I'll explain why this is necessary or why this helps. And then we do memory checking called into binary twisted shout. The I refer to the binary field instantiations as binary twisted and binary shout. We also have a new sum check argument called binary router. This is used for handling shifts and subword stores. And then we just open once.

There are no permutation of grand product arguments so and also because there is a single witness, there is no second trace to reconcile with. And all the claims descend from Spartan and they get resolved by the protocols downstream. So what I mean by dual Cindy R1CS is we create a single binary witness but apply two separate circuits. One of them is defined over F2. Another defined over an extension field. The reason we do this is if you look at the logic that's inside a a CPU, some of them are binary operations that efficiently represented in F2 but some of them require word level operations

and if you try to do that inside F2, they are significantly more expensive so we split constraints across two separate circuits but they both of them operate on the exact same witness. And we also have some cross step constraints because step J must read some state from step J minus one. So we use this next multilinear extension to link the witness values. And because there is only one witness, this is enforced through a commitment. So there's a single commitment and then it's evaluated at the exact same point for both relations.

And the CPU logic just runs in the field wherever it's the cheapest. So I mentioned virtual Spartan. So the starting point here is we take this witness and we lay it out in segments. And some of them are going to be committed, but most of it will not be committed. So, they just stay virtual. Uh for example, the values that are read from registers or written to register values related to RAM and so on. They just are available to the R1CS to check.

Uh but they're not committed. Uh so, these registers are then the directly direct segments are going to be committed with this PCS. Uh but the other values which is run Spartan on it and then after two invocations of the sumcheck protocol, the prover just sends evaluations of these segments that are not committed. The verifier checks some random linear combination and then we take those claims and send it to the downstream protocols. For example, claims about uh witness values related to registers is directly sent to binary twist.

Uh and for example, uh the witness values related to the lookup values from bytecode are sent to binary shout and so on. So, this virtual segments is used in many other works. For example, one canonical example is the GKR protocol, also Spartan where we never commit to these easy breezy CZ which are intermediate values that show up in the constraint system. And virtual Spartan just extends this idea of virtual segments to a a wide set of witness values.

So, the third component that we use this is binary twist and binary shout. So, we have two instantiations of twist protocol, one for registers where in each cycle we do two reads and one write per cycle. And binary twist for RAM where there's a single right read and a single right per cycle. We also use shout for doing read-only lookups. So, the key idea here is all centered on this one-hot vectors where you have a collection of vectors where all the values are zero except for one which is set to one.

And the reason this one-hot vectors are useful is a lookup check becomes a single inner product. For example, RV is the vector of looked up values. RA is a matrix that just is a collection of one-hot vectors and Val is a lookup table. So, now to check the values are correct, you just need to check this inner product relationship. Of course, over binary fields uh this you also have to ensure this RA which is committed by the prover is really one-hot and over F2 some of the tricks that typically work over prime fields no longer works. So, we devise this collision polynomial

which is identically zero if and only if the row has a weight of at most one. And then we can just do a single sum check to check if the entire vector has one hat or one-hot rows. And all we commit in this protocol is one-hot addresses and because this if you do this naively this matrix will be quadratic in size. So, we observe that this RA itself has tensor structures. So, we can commit to smaller polynomials and then virtualize the the real quadratic size polynomial.

And for twist which I'm not going to go into the details, but we end up committing only to this increments which are values that are the XOR of the old and the new values. And everything else stays virtual. So, there's one operation in RISC-V which is not very efficient if you try to do it in an R1CS. It's this shift operation and also the store operations. I'll come to what the store means. Uh so for shifts, uh typically in a prime field setting, this is handled by multiplications, whereas in uh binary fields, because the multiplication itself could be expensive, uh we devise a special sum check

argument. Uh we could have used this Jolt style lookups to uh into a large structure table. Turns out it's it's expensive in the context of binary fields, so we devised this very special sum check. All it's doing is it writes the output Y as a function of the input X. And then there is this one-hot selectors, which uh also are very inspired by Tristan Shox. And then there is a R polynomial, which is a public value that uh describes how the bit values are routed. So for example, in this picture, uh let's say we want to do this uh shift by two, the output bits are a function of the input bits. So they could be zero or one of the

uh existing bit values. So we check this directly by using this relation. So in RISC-V, the other uh place where these type of bit operations show up is uh uh uh subword stores. What I mean by this is we use a word addressable memory, but there are also instructions that just manipulate a byte or a half word. So sometimes you have to make sure you write back a value, but uh the other bytes of this word are uh not modified. So we use the exact same protocol to prove those uh statements.

Finally, uh uh there's uh a Mosaic PCS. Uh it's uh in a hash-based setting, because there are so many polynomials, if you commit to them separately and uh uh prove their evaluations, the proof size just blows up. Uh so what we do is we take all the polynomials, we know the sizes of those polynomials, so we just arrange them in a grid aligned on the hypercube. And then we run the PIOP and each of them reduces to the evaluation of one of these polynomials. We can immediately deterministically with no help from the prover lift those claims into a claim about this mosaic TCS committed polynomial and then just do

one opening. This is a folklore idea that's used in many places. The key takeaway here is this does not affect the throughput and it does not require any additional help from the prover. So in terms of security we target the 120 bits of probable security from standard hashes. We only use SHA-256 here. It's transparent no trusted setup. Every round has soundness error at most 2 to the minus 120. We just use we work in a unique decoding radius. Use only proven results, no conjectures. And because there are no grand products we have very small loss from the

sumcheck argument even if it's run over 128 bits. And I think there are some ways of taking this 120 bits and go all the way to 128 bits without changing the field and we plan to do this. We also evaluate we implemented this whole system. We evaluated it compared it to a a set of baselines which are listed here. Here is one diagram that lists the speed up over baselines at 2 to the 22 cycles.

And each of the each bar here represents one workloads. We picked 15 workloads and the bar represents the speed up of Magnetar over these baselines. As we can see, there is significant speed-up on all the existing baselines. It's faster than all of the baselines on all the 15 workloads. We also compared the Magnetar to Zcash and Lineth. One caveat here is that these provers take minutes on a laptop. I think they are not optimized for proving on a laptop. Uh for example, uh on 2 to the 22 cycles, Magnetar is about 290 times faster.

I think this is possible compared to Zcash, but this might just be because they're not optimized to run on a laptop. Uh So, here is one table that captures proof size verification and memory. The proof size is less than 600 600 kilobytes. Verification is fast. We also get good memory efficiency. For example, compared to SP1 Hypercube, it's about three to four times lower space usage. We still use more space than Jolt. Uh Jolt is really memory efficient because they don't use RS codes.

Uh but I think there is more uh uh uh room for optimizations here. Also, Jolt's proofs are significantly smaller. For example, they are less than 100 kilobytes, but I think they can be fixed or addressed in the context of recursion. For example, we could use uh smaller code rate or different uh regimes uh to reduce the proof length significantly at for example, the last step of recursion. Some proof systems like Jolt, uh they get better throughput as we go up.

Uh so, here is one table that shows uh uh uh the throughput of different systems at their best lens. Even uh when we go to 2 to the 28 or 2 to the 27, and if you look at their throughputs, uh Magnetar is still faster than all the existing baselines. So, to summarize, Magnetar is the first ZKVM that meets all the three properties that I outlined. So, it's general-purpose, it uses standard hashes alone, it supports efficient recursion, which we haven't implemented yet, but I think uh uh it's going to be efficient. It's also fast uh uh 6.5 to 7.7 at the moment, and there's a lot of room to optimize.

Thank you. Happy to take more questions. >> [applause] [cheering] >> Thank you. >> Uh thank you. Amazing. Uh in in cruise, in two centuries, you need to divide each um address index in uh small chunks of bits, I I I assume. Um what uh size for these small chunks did you use? >> Uh so, you're talking about the RAM index, the the address bits of lookup argument.

>> Uh yes. >> Yeah, yeah. So, it it We have a a way to tune this depending on the size of your RAM or bytecode. So, we try to keep this so that you never have to commit to more than 128 or 256 bits per um uh lookup. >> Okay. Um one one question is uh I switch marks up to the 2 to the 22. Uh in for Ethereum blocks, we will you need something like 2 to the 30?

>> Yes. Yes. >> So, that you you you have some scheme in mind or something to to be able to keep pushing to bigger and bigger amount of cycles? >> Yes. Yes. Yes. So, the goal is to do uh for example, either 2 to the 22, I think 2 to the 24 we can sustain the same throughput. So, we can do chunks of size 2 to the 24, but then take all those proofs from So you divide your 2 to the 30 execution into smaller chunks. Do all of them in parallel and recursively compose all the proofs.

I think this is the same thing that all of the existing real-time provers use. So the same idea works here. Does that answer your question? >> Uh super impressive work. Um I guess two questions. First, what do you do for integer multiplication instructions? And also, what is the rough What are the most expensive argument sub arguments? And how do the RAM and ROM um arguments wait uh you know, factor into that?

>> Yes. So um the second question was about the how do the different components like what's where is the time spent? Comes out it's spent equally among all the uh three components. Um Spartan, Twist and Shout. So they are all roughly the same. And it also the proportion also varies depending on how much memory is used by the guest program. So but they're roughly in the same ballpark. And I would say for small memory cases, Spartan is dominant. But as you go in higher memory, uh the other components could dominate.

Uh I think you asked about the integer multiplications. I think um uh We're thinking multiple different options. For example, uh one potential way is just add a precompiler that does the integer multiplication in a binary circuit. I think that could just work well. Uh it could already reach like 5 to 10 million multiplications per second. Uh and then as long as you connect the CPU to that lookup table, I think you can already sustain similar throughput as we are seeing from the CPU, but I think maybe there are more advanced techniques to borrow from uh >> Hi.

Uh next question. Um do you have a feeling for what the VM overhead is? So, like for example, if I was proving um like some software uh program uh ex- like computing some hash function, how much slower would that be over having custom circuit improving it in binary spot in for example? >> Oh, I see. Um I think um let me recall. Um it's probably about an order of magnitude to two orders of magnitude, I think. I I can give you the exact number.

Uh but it's roughly in that range. >> Yeah. Cool. Thanks. >> Zack. >> Uh sorry. Thanks. Um yeah, amazing amazing work. Um really really fascinating. So, I might have missed it, but do you do you do you have any numbers um or like estimations for what the cost of recursion is going to look like? >> Um I we don't have it implemented, but a lot of the work involved is uh just proving these hashes.

>> Mhm. >> Uh for example, even for 600 kilobytes, if I'm calculating this correctly, you probably need only like 10,000 or 20,000 hashes, which should be a a very um I'm sleepy, so I don't uh have that factor, but I think it's going to be very fast. Uh >> Um yeah, you you mentioned um like in your benchmarks proving Ethereum blocks. Is Is kind of is client-side proving something that you you're interested in in in um focusing on it in a in any way because the tech- the techniques you like in that you're describing look really really interesting just for very very fast client-side CPU provers.

Um but um yeah, it's just that for that for that recursion is going to be essential because otherwise the memory consumption gets too large. >> Yeah, I think the recursion cost is going to be pretty efficient. I think it's still DBD what the the entire ZK-EVM recursion will be, but I think it's going to be fast. So, what are you asking about Ethereum workload? Like what what do you mean? >> No, no, I'm just thinking like if you, um, it just looked like you were it just, um, looked from the benchmarks that you're kind of you're you're feeling you're you were looking at proving Ethereum blocks, which is like a very different shaped problem to, you know, like doing client-side VM proofs. I'm just I'm curious if you're if you if you if you, um, have any particular focus or area of interest or

if that was just, um, like um or or not, basically. >> Yeah, yeah, so I think, ideally, we want to be able to prove any workload. I think these were the benchmarks that we used to uh drive uh optimizations and, uh, get better proving performance. But, I think, uh, by adding precompiles for multiplications and for other operations, we should be able to handle any workload. >> Cool. Thanks. Yeah, really really fascinating.

>> Um, I'm curious if you have any intuition on how it would perform if we were using G"{o}rgs, um, G"{o}rgs is the idea uh, for uh, twist and shout plus log up star, where you commit instead of committing to those um uh, sparse like one hot vectors, you commit directly to the index, and then you lose log up star to virtually access the one hot matrix, if that makes sense. >> Yes, yes, yes, yes. I have seen that idea. Yes. So, I think, um, there may be something in between that could work better.

Uh, if we just try directly to commit to these sparse vectors using, uh, a dense representation and then try to uh turn that into a lookup. I think we uh would end up uh using grand sum arguments or grand product arguments. Uh which like for example, I I think for lookup, uh maybe there are two paths. One is you commit to those inverses, which I think is going to be expensive. You don't want to commit to the inverses. Or you keep them virtual, but then you run GKR, uh which brings back some of the overheads. Also, soundness loss. I think there are some tradeoffs there. But something in between could be better than either of them.

>> I think also one to hold back would be that um you would have to commit twice. Once you have you have to commit once, get to the get some challenge, and then commit to push forward. >> Yes. >> While and so proof size and verification would be maybe a bit too >> Yes. Yes, I think there are uh yeah, there are tradeoffs, I think. It's not clear when uh at least to to my understanding. >> Um do you uh happen to know uh hey um how you parameter or like basically what's the smallest uh unit vector size that you end up committing for twist and shout? Is there a standard that you chose or something?

>> yeah, I think uh we have this uh the D parameter uh to control the size of these vectors and the size of the total commitment that we're going to do. I think choosing smaller D reduces the cost in the sum check, uh but increases the cost in the commitment. So, it's a it's a balance. Uh so, we choose D large enough so that for each lookup you are each memory operation, you never have to commit to more than say 256 bits. So, roughly two field elements or one field element, depending on uh >> Okay. Yes, thanks.

>> Yeah, thank you. Um yeah, my understanding with Twist is that you're now able to exploit uh sort of locality. So, like the registers uh for RISC-V, if you access them, they would be cheaper than accessing uh memory. Uh do you see this playing out in any of your benchmarks? >> Yeah, yeah, yeah, definitely. Like uh we can leverage all of the optimizations that are present in the prime field setting over to the binary field setting because the sum checks are essentially the same, except uh we replace the booleanity checking with the collision check. So, it's all of the nice properties that exist in the prime field setting carry over to the prime binary field setting.

>> Right. Uh yeah, I guess uh do you see that programs that heavily rely on registers are a lot cheaper or faster than programs that use a lot of memory? >> Uh I I don't think I have a a benchmark to demonstrate that yet, but I'm uh I can I can look at look into that, and we can chat offline. >> All right, thank you. >> Srinath, absolutely amazing work. Thank you so much. >> Thank you.