Cool, so earlier this year I was exploring Circle Starks, right, and basically trying to understand how the hell this very weird new primitive based on spooky stuff that's apparently called Mersenne-Rock spaces is supposed to work. And so I figured that as part of that I would do a fun experiment and basically try actually building the whole thing, right? So first, you know, started off the usual way I do things, which is just write it out in Python. The point is not to be performant, the point is to just understand how everything works from front to end, make sure that you have a prover and a verifier that actually works at all. But then I, yeah, at some point I decided I would try to take this experiment a step further, right? And what I basically ended up doing is I ended up using first NumPy and then CuPy, which is a CUDA GPU array that follows the same interface as NumPy, to write a prover in Python where the underlying logic is vectorized. And so you're basically using Python to operate over long, big lists of numbers at the same time, and the actual one-by-one work of doing all of the arithmetic is done on a GPU, right? So this is basically how we do AI, right? There's a huge amount of AI code that is written in Python, and it's basically the underlying logic is done with C, with some kind of CUDA wrapper, like usually Torch, sometimes something else, and it still manages to be extremely fast, basically because the Python is only doing this relatively small amount of glue logic, right? So I figured, okay, fine, let's try to do this exact same thing but for Circle Stark provers. So this is an implementation of a Circle FFT. So the code is surprisingly simple. FFTs were extremely scary up until I implemented them from scratch like about the fifth or tenth time, and then at some point they actually just eventually magically stopped being scary. FFTs were one of those algorithms where even after I implemented them and even after I wrote an entire post on them back in 2021, I still thought they were scary. I think the only thing that's even scarier than them was elliptic curve pairings. Like that stuff is maximum voodoo. Okay, so I'm actually happy that this stuff is hopefully just going to out-compete elliptic curves out of existence. So the FFT is implemented, and the underlying logic is all being done through a CuPy Python wrapper around CUDA on a GPU. Then this is Circle FRI, and specifically the folding step. So the folding step is similar to an FFT, except instead of taking the two different pieces and proceeding to the next round with both of them, you basically randomly combine them and you keep going further. Actually, wait, this is the implementation that's just in Python. There is another implementation that just does it vectorized, which is not this one. So this is arithmetization of Poseidon, right? So I got excited about this because people were starting to talk about how you can prove Poseidon hashes extremely quickly. And for a long time people were thinking like, oh, maybe you can only prove like 1,000, maybe 2,000 hashes per second and this stuff is impractical. But then suddenly StarkWare came out with their super impressive numbers and they're like, oh my god, you can prove 500,000 hashes a second. And then it's like, okay, well if we have that then we can basically skip half the Ethereum roadmap and go straight to Poseidon and hashing everything. So the one challenge there is that we have to actually be confident that Poseidon is secure, right? And so we're not confident about that yet, but hopefully we should. And the Ethereum Foundation, I think, will soon announce some kind of program about trying to encourage more people to participate in checking that Poseidon is secure. But basically Poseidon is this hash function, like I've always found it beautiful just in its sheer and extreme simplicity, right? And a basic implementation of Poseidon you can literally fit in like eight lines of Python, right? And so this is not an implementation of Poseidon, this is an arithmetization of Poseidon, so implementing verification of it inside of a Stark. And one of the fascinating things about it is that it's actually surprisingly compact, right? Like you can do an arithmetization of Poseidon inside only about 200 cells, right? So inside of your entire trace you need only 200 field elements for each individual Poseidon call. Basically, even though Poseidon does have 64 internal rounds, it turns out that for each internal round you only need like a couple... I think actually for each of the inner rounds except for the first four and the last four, it turns out you only need actually one extra trace value. And the reason is this very weird trick where you basically use powers of the MDS matrix instead of using the MDS matrix directly, right? And so I basically actually just wrote that out, and the arithmetization itself is only something like 50 or 60 lines of Python. And you can find this in the GitHub ethereum/research repo and read it yourself, and it's actually surprisingly not scary and not hard at all, right? So results: proved over 10,000 hashes a second. So note, I'm a noob, this was my first time ever writing a CUDA kernel. So StarkWare did 500,000 hashes a second, and so I am absolutely certain that there are 50x optimizations somewhere here that I am completely missing, right? And at the same time you get code that is surprisingly easy to read and that is surprisingly accessible, right? So when I did this, right, so this is probably the first time anyone's written a prover in Python that can actually do serious work. But it was still surprisingly not that difficult to do. So at the beginning basically all of the code was put in this one single file and you just do everything directly on top of the CuPy library, right? So then I decided, well, why not actually take the code that is specific to optimizing M31-related modular operations and just put it into a separate library, right? So we have Torch, which is a library that basically does... it's like CuPy, it's like kind of a CUDA wrapper, but it also has a huge amount of extra optimizations that are specific to doing AI code. Let's do something similar to that, except instead of optimizing for AI code, let's optimize specifically for the needs of zero-knowledge provers, right? And so here, this whole file basically has an implementation of all the different Mersenne-31 arithmetic, and then further down I also have extension field multiplication, extension field modular inversion, regular modular inversion, all kinds of things. Again, definitely done totally not optimized at all, but even still, you basically can package this into this really nice and clean library. And what you get as a result is, you know, you get code like this, right? And basically if you think about what this arithmetization is doing, inside of here you just have like expected equals prev plus RC times times 5, and it looks like plus, it looks like times. And then in a Circle Stark, sometimes you have to run the constraint checking function over the base field, sometimes you run it over the extension field, and then here you just have an abstraction where you just write the code once and it just automatically does both, whichever one you need depending on context. So basically that's the idea, right? It's like you write this code once and then you can have this super beautiful, super clean code that just does everything that you need. So basic principle, right, is like AI code is written in Python. So this is a screenshot that I've taken out of some code from a Transformer implementation, and I'm sure the nerds here understand exactly what it does. I mean it's a forward pass of a Transformer. And basically, why Python? Because Python is the best language, right? Python is the apex of readability and good aesthetics. The problem is that historically Python is just crazy slow. But because we're dealing with vectorized computation where we can create Python objects that are individual objects that wrap potentially millions of numbers, that you can just do lists of billions of numbers, so you can do computation around simultaneously, and so basically Python overhead actually ends up not mattering, right? And so I wrote a post about two months ago on this topic that I call glue and co-processor architecture, right? Where the basic principle is that for any kind of what we might call heavy computation or intensive computation, you can almost always in practice split it up into two parts, where one of those parts is very general-purpose computation but fundamentally light computation, and then the other part is heavy computation but computation that is very, very structured. Right? So one example of structure is in AI. AI is basically just vector-matrix multiplication, and vector-matrix multiplication is one specific way of doing additions and multiplications on massive lists of numbers at the same time. And so basically you just create specialized modules that are really thoughtfully designed around the specific task of adding and multiplying lists of numbers, and you really optimize the heck out of those, put a lot of work into them, and then you have these nice clean abstractions, and then you can just work on them in some language that just optimizes for readability and just shows you the actual logic of the code that is being done, right? And in the case of ZK work, obviously the more common structure is polynomials modulo some prime number and in extension fields, and also sometimes you actually get vector-matrix stuff like we have R1CS. But it does seem like the faster stuff these days is polynomial-based, and then now we're also talking about polynomials over hypercubes now. And so you have lots of these abstractions that just basically mean do the operation on massive lists of numbers at the same time, and you do that in the fast language, then you do the high logic in the slow language, right? So basically the prompt here is, let's code provers that are in Python as well, right? So this is just a random part of the prover logic here, right? Basically what's happening here is that in the constraint checking polynomial you want to prove that it has the starting value at the starting coordinate, the ending value at the ending coordinate, and so you just divide it and interpolate by the line that passes through those two points, and you generate the quotient, right? And you see it's like, hey, Trace minus I over V, it just looks really nice and clean and beautiful, which is the way that code is supposed to look, right? So this is all again basically just an experiment by myself, and I think part of the goal is also to try to just make this whole space more accessible. So other existing work that I know about: so IceClap from Inama, of course, great work here. I've looked at the repo and it seems like there's no ZK, no Python support yet, but there is intent to do Python support. And so if this and that could just merge and we have a nice library that does what we need to do with Python, then I personally would be overjoyed. Also CuPy and PyTorch themselves obviously have massive optimizations in them, and I think some of those optimizations are things that are relevant to doing ZK as well, right? So I'm sure they have stuff that has to do with optimizing memory usage and doing operations in place when some computation is not needed anymore, operations to do with pre-compiling kernels and then executing them all at once, and a whole bunch of crazy stuff. But then they do have other things that are just inherently optimized for AI. It's like if you look at PyTorch, it has support for lots of different floating-point types, it has support for doubles and float16s and all kinds of stuff, but it does not even have, when I used it, it did not have u32, right? And of course for this you need u32, right? And so the direction in which you'd add certain features is going to be somewhat different if you want to go in the cryptography direction. And so I think if you have some combination of these things, then you're able to make something that's much better, that's just a really nice library that you could use to just make it very easy for people to write these kind of provers. So conclusions: this accelerates ZK, and my plea for today is let's accelerate ZK developer time. So I view this as being somewhere in between Circom and full-on advanced people doing advanced stuff, right? Basically, Circom makes it very easy to write circuits, but at the same time it hides huge amounts of logic in the background, the outputs are not very inspectable, it makes the arithmetization, and generally we're supposed to just trust them. Whereas here, the idea is that we could create these more middle-level toolkits and basically create things that still expose the fundamental mathematical components, and that basically not just make long-running existing algorithms more accessible, but also make more accessible frontier stuff where you have to fiddle with the algorithms yourself, where you have to make really crazy custom arithmetization, where you have to work over different fields, you have to work over different types of SNARKs. In Zorch, one other thing that I did not talk about is that I also wrote a basic implementation a bit earlier in the year, and so I just folded the binary field stuff from that into that. And so basically, let's actually make these more crazy and more frontier aspects of ZK accessible, and basically learn from how the AI space has made very performance-intensive code very hacker-friendly. And so the call to action here that I have is basically, I'm a blogger, I'm a noob dev, I wrote stuff, and I encourage people to basically just take it and build on it and combine different components together, and let's create something that makes it actually practical for people in Python or any language to just go and write provers that can do things like 500,000 Poseidon hashes per second with any of these new algorithms that come up. So thank you.
