A Functional VM for Verifiable Computing over Binary Fields

Everyone, sounds like this is working. I'm Jim, and I'm going to – my goal in this talk is that you fully understand the title by the end of it. So if you don't right now, that's okay. I work at Irreducible. We're basically trying to build high-performance verifiable computing technology.

So verifiable computing, what is it? It is a cryptographic technique for verifying the integrity of a computation, and I believe this is the secret to scaling blockchain and peer-to-peer systems securely without compromising their essential properties. It's really important for our whole space, in my opinion, but there's also some forward-looking applications that may seem more speculative right now, but I think that this could be used to combat deep fakes and inauthentic contents using generative AI in the future. I think potentially it could be used to verify the safety of machine learning models, making decisions with real-world consequences, and there is a variant of verifiable computing that provides privacy guarantees, which are zero-knowledge proofs. So in this talk, I'm going to give a little bit of snark background, just the basics of what you need to know to understand the rest of it.

I'm going to talk about the design of our virtual machine, which is the PetraVM, a little bit about our compiler stack for it, and then some of the early performance results that we've gotten. So rewind to sort of the early days of verifiable computing and snarks. You had to express something that you were interested in checking in a computational model. So let's say we were looking at – I wanted to prove to you that a PDF document contains the words protocol BERG in it. How would you even express that statement?

The original snark models were based on Boolean circuits, meaning you had to express a full digital logic circuit for checking that the string protocol BERG was in a PDF document. That doesn't sound very practical to do. It turns out it's a little more efficient to use arithmetic circuits, which are a sort of mathematical generalization of Boolean circuits, but that's still pretty difficult. So there were languages and frameworks designed for this, like Halo 2 and Zocrides, but this is very difficult to program. It has issues with control flow, meaning if you want to branch and do an if-else statement in a circuit, you basically need to execute both sides, and they're pretty inflexible.

So virtual machines have taken over basically in the space as the easier way to deploy verifiable computing because they offer a good developer experience, they efficiently handle control flow, and a really essential part of this is having a good way of checking memory. So what are our classes of virtual machines? Broadly speaking, we see virtual machines that have backwards compatibility with an existing standard, like RISC-V or ZKVM or MIPS, and that's nice because we can use standard compiler technology, but on the downside, there are design decisions that make them efficient on CPUs and standard architectures that do not make that much sense when you're proving things with a SNARK or with a zero-knowledge proof. So there are SNARK-optimized VMs as well, like the Cairo VM or TinyRAM, which was a really early work going back to 2012, and Petra VM is one of these virtual machines that's specially designed for efficient proving to take advantage of the complexities of the underlying model. So here's what you need to know about SNARKs to understand this talk.

You have a prover and a verifier, and the verifier runs a non-deterministic computation, meaning the verifier knows the inputs, but they also get advice or hints from the prover that they might not even be able to compute on their own without this hint. The other thing you need to know is that, like the native data type of SNARKs, is a mathematical object called a finite field, and your primitive things that you can do instead of, say, logic gates, are polynomial-related. You can take the sum of a polynomial over some domain, or the product over a domain, or you can evaluate a polynomial. You can do polynomial things over finite fields. That's what you need to know.

And our underlying proof system, concretely for Petra, is the Binius SNARK, which is what my company, Irreducible, works on. And the data types that Binius uses is a structure called a tower of binary fields. It's actually a family of data types. So we have a 1-bit data type, an 8-bit data type, 16-bit, 32-bit, 64-bit, so on. The native addition operation over this finite field is XOR, so we can do that very cheaply.

Multiplication is complicated, but the thing that you need to know about it is there's a property that if you start with a particular point called a generator and take its powers, it will go through the entire field and then get you back where you started. So it has a symmetry to integer addition. That's the property of being cyclic. If we want to do something like integer addition, that's not an algebraic operation in binary fields, but we can check it with a Boolean circuit. So I'm going to spend most of the time in this talk about talking about the design philosophy of PetraVM and want to explain what types of efficiencies we can get by designing a custom ISA and what Petra uses.

So our goals here are we want to balance flexible program expression with efficient proving. We want to have, you know, a high-level language with great performance. And to be more concrete on that, we're targeting primarily, or to begin with, applications of verifying cryptography. So we wanted to design this actually for recursive proving of the Binya SNARK, meaning a language that will help us express the verification logic of the underlying zero-knowledge proof system, which is really important, but we also think this is useful for verifying digital signatures and logic on the inputs of hash functions. And as a secondary goal, or as another design goal, we want this to actually be a compilation target for WebAssembly.

So we want a really great developer experience where someone can write a WebAssembly program and prove it using Petra by compiling the WebAssembly bytecode to Petra. And that would enable proving of high-level languages like Rust. So I'm actually going to start with verifiable memory arguments because this is one of the most influential things in terms of designing a verifiable VM. So one technique that was kind of the earliest for doing authenticated memory is Merkle trees. So that means every time you do a read, you need to verify a path in a Merkle tree, and every time you do a write, you have to update that Merkle tree.

That's very expensive. No one really uses that for memory reads anymore. What has become very common is a technique based on a cryptographic paper called SPICE. And I'm going to walk through some of the steps quickly to just show what has to happen. So effectively, a prover will, if the VM wants to verify a memory operation, we're going to treat it as a read-write pair.

So first, the VM initializes all the memory addresses with their initial values. And then every time you want to do a read-write, you pull in the address, the last value that was written there, and the timestamp that it was last written. You're going to write back the address with the new value and the new timestamp and the VM needs to check that the old timestamp that it received as prover advice or a prover hint is less than the current timestamp. Because if it didn't do that check, then it would be getting a value from the future and things would be insecure. So this is the sort of complexity of doing a standard read-write memory.

Petra instead prefers to use read-only memory arguments. So this is basically simpler and more efficient inside of a VM because you just have to pull in the address and the value. The value is always, you know, uniquely bound to an address. And you don't need to write it back. On the other side, there's a lookup provider who just counts up all the times that a particular entry in your ROM is read and pushes it with multiplicity.

And without going too much into cryptography, it is cheaper to do a read into a ROM than a verifiable RAM argument with a read and a write back. Phineas uses a technique called channel pushes to do this idea of like reading from a memory and so on. I'm not going to explain too much about what a channel is here. So the Cairo VM, which was originally written by, or which is a technology by Starkware, introduced this idea of a non-deterministic read-only memory model. So it's easier to think about this as a write-once memory, but it's actually a little more flexible than that.

And basically, if you have a write-once memory, you can do, they show that you can create a Turing-complete virtual machine on top of this. If you're familiar with single static assignment, which shows up in compiler technology, it's sort of similar to this in the sense that values are written once, but actually it's stricter than SSA because SSA has this notion of a phi node, which would let you overwrite a register. So it's not actually as easy to use ROM as to, you know, execute an SSA IR. So here's an example of if you wanted to compute the fifth Fibonacci number, and all I'm trying to show here is that you can think about doing it with a sequence of variables that are only written to once. What does non-deterministic ROM mean?

It just means that the read-only memory is pre-populated according to the prover's choosing, and then the verifier, the first time it does it right, it just checks that the value that it's reading is actually what it wanted to write. So what does it look like to program something more complicated with the non-deterministic ROM? So what if we wanted a Fibonacci program that doesn't just compute the fifth number, but computes the nth number? This on the left is something that's sort of like Cranelist IR, which is an intermediate representation used in the Wasmtime compiler, and there's a, I basically want to show on the right-hand side the call stack that happens if you write a recursive implementation of Fibonacci, in which every function only writes each local variable once, or at most once. So at the top of your call stack you have the Fib3 count, the Fib3 call, that calls the Fib helper with an initial count of three, the next call decrements that to two, the next call decrements it to one, the next call decrements it to zero, and then the final call returns the value two, which gets propagated back up the call stack.

This is basically just like any function call sequence. One thing to note here, though, is if you run this recursive call stack on a regular processor, your stack is, you know, you're going to push a stack frame, and then you're going to pop a stack frame, and potentially create a new stack frame in the location in memory where your old stack frame used to exist. That's the idea of a stack, that it's going up and down. In the non-deterministic ROM model, your memory is right once, right? So what that means is our function frames are going to sort of live forever.

There's not a stack that shrinks, it's just you keep pushing function frames. Another thing to see here is that in Fibonacci we're making tail calls, so we can actually do an optimization here, where instead of returning everything through the call stack, we just return something directly back to the initial caller. And the observation that we wanted to pursue is that the non-deterministic ROM model is efficient for proving, and it's very compatible with functional programming paradigms, because functional programming is based around having immutable values and computing functions over them. So we were inspired by this and wanted to design a VM that would be programmable with functional techniques. So our calling convention is similar to a regular function calling convention.

You allocate a function frame, the top of it has space for arguments. The way return values are handled is that they are non-deterministically provided by the caller, meaning the prover needs to sort of say ahead of time what will get returned, and then the execution of the function is just checking that the thing that actually gets returned is equal to those initial inputs. So the return value can also go at the top of the frame. Some other interesting things about the paradigm of verifiable computing is we need all of the values that ever existed in order to produce the proof, so there's no reason to do garbage collection. We're just, every object that we allocate lives forever, and then we'll clear it at the end of the proof.

There's also no benefit to having general purpose registers or a cache hierarchy, so we can design around that, and what this means is we're not, don't have general purpose registers to operate on, we just operate off of our local variables. We use the mathematical structure of the binary field to create a address space for the program memory that is using the cyclic multiplicative group. I was supposed to edit these so that they were actually different numbers, but the idea here is you're going to start with a generator, and every time you increment the program counter, it's going to go to the next one, not the same one. So this lets us increment the program counter more efficiently than regular integer arithmetic in a binary field. The PC equals zero is not in our cyclic group, but it's, we can use it for a special purpose of like an exit code.

The main data ROM, which is where all of our intermediate values live and where we allocate objects into, is called the value ROM, the VROM, and the pretty interesting thing about this is that we're going to use XOR for pointer arithmetic. So in a normal CPU, you would use integer addition and integer multiplication for pointer arithmetic, but it's cheaper and viable for us to actually use XOR, meaning the function frame should be allocated with an alignment that is equal to the size of the object. So like the bottom bits of the object pointer address are clear, so that if you XOR in like a local offset, it won't go backwards in the address space. The other thing that we're allowed to do here is because we have a read-only memory, the verifier doesn't actually need to check the allocation algorithm. Only the prover needs to run an allocation algorithm, and it's going to provide the addresses of allocated objects non-deterministically.

So it's just going to declare that my next function frame is going to exist at some address, and this doesn't introduce any security problems because the values are immutable. So if two objects overlap, it might mean that the prover would be unable to prove the program, but that's sort of their fault for choosing objects that overlapped in the first place. But it's not a security problem for the verifier, and this is another thing we can take advantage of. What are some of the benefits that we get from using the Binius proof system as a binary proof system that's sort of different from some of its competitors? Well, the binary tower fields, because we have these different data types of different bit sizes, eliminate a bunch of range checks, which are a common tool that other VMs using prime fields need to do.

And so by dropping these range checks, we can save a lot of work. Our work and our research work at Irreducible shows that we can reduce one of the main bottlenecks of SNARKs, which are commitments, by committing to small values cheaper. And this is a pretty unique property of binary fields, or at least fields of very low characteristic. We can efficiently arithmetize bitwise operations. And we also know from hardware design that if you were to produce a custom ASIC for binary fields, the raw resource efficiency and clock speed that you could run binary field operations at is about five times better than prime fields or integer operations of an equivalent bit size.

I'm not going to walk through the Fibonacci assembly code for lack of time, but you have a function frame. It has local variables. You do instructions. It looks sort of like normal assembly code. How do we program this thing?

We decided to create a language called PetraML, which is not a new language. It's a strict subset of an existing language, which is standard ML. You might not be familiar with it, but you might have heard of a sister language called OCaml. There's a family of languages that are ML languages. They're basically strongly typed functional programming languages, and standard MLs are a pretty clean one.

So we picked a subset of that that omits some features that we don't want to support. And this gives us the benefits of great developer experience. You can write a program in standard ML, use the standard tooling, get fast native execution, because it actually compiles to native, and then go and make sure that it's compliant with the subset of the FML language that we support. This is what FML code sort of looks like on the right. This is actually PetraML compliant.

PetraML does support integer operations and 32-bit unsigned interdrops. It has lists, options, algebraic data types. It's a pretty rich programming experience. And then we add some built-ins for things that we want to specially accelerate. So accessing the write-once memory or the VROM has a special module for invoking that, and then we can also add built-in instruction operations for hash functions and so on, and binary field operations in the case of recursive verification.

So here's what the FML code for Fibonacci would look like. We have one intermediate representation called the core IR. This matches an analogous concept from the OCaml compiler, and this is very, very similar to that. And we can do optimization passes on the core IR. And then this is what the final compiled assembly code running through our compiler today looks like.

I'm short on time, but I know people would ask questions about performance. So take these numbers with a grain of salt. They're more of performance indicators, or like early performance indicators. Benchmarking is hard, but bear with me. We ran RISC-V VMs, FP1 and RISC-0 on both CPUs and GPUs, and ran the Fibonacci program, which is one of the early things that we're able to run on PetraVM.

Here's the cost of the AWS instances, so basically the GPU instances about twice the cost of our CPU-only instance on the on-demand hourly rates. All the proof sizes assume the Frye conjecture, and basically the cycle count is similar. It's about, this is for the 100,000 Fibonacci numbers, so it's something like 10 cycles per Fibonacci number. And our CPU performance multi-threaded on an eight-core machine is basically very close with the GPU performance of these competitor systems right now. I do think there's some overhead to, we basically picked a number that would fit within a single proving shard of both of these systems.

I think if you have multiple shards, their throughput might go up by two or three. Their CPU numbers are, I mean, I put them in there to run them, but I think neither of these systems are optimizing for CPU anymore, so I'm sure their CPU numbers could come down, but I'm not really sure how much. So that's what we got here. This is a trace of our profiling execution that's too small for anyone to make sense of. And the project status is, the Petra VM is open source.

It's functionally complete. The compiler is still in progress. We can compile programs that don't have algebraic data types today. We're working on a bunch of things, including finishing the compiler, optimization, sharding proofs, the recursive program to recursively verify Binia's proofs, and we want to add an optional read-write memory. And that's what I've got.

So here's some links if you want to follow progress. And thank you very much. Thank you. Thank you, Jim. Thank you.

We've got a couple of questions for you. First one here is, should Ethereum switch to Petra VM? Not yet, because it's not ready yet. But I'm excited about a partnership with Powder Labs is building this WebAssembly to Petra compiler. And I'm very optimistic about the performance we're going to be able to achieve with a ref compiled to Wasm compiled to Petra.

So I hope it's in Ethereum's roadmap at some point. Cool. Next one here is, why did you use Fibonacci for the benchmarking? And something like ECDSA signature? Because we're still building up towards ECDSA signatures, and this is what we can run right now.

What about the possibility to do client-side proving? Very interesting question. I'm increasingly optimistic about that. I think we've learned a lot about how to make Binia fast on CPU. And if anyone has concrete client-side use cases, I would love to hear them.

And the last question I see here is, what will be the main difference or optimization for CKVM to be hardware optimized? Custom instruction sets, perhaps? For an instruction, I mean, most of the hardware efficiency is coming from the design of the underlying proof system. So we've done a lot in Binia to make it friendly for hardware. That includes using fields that let us compress the trace representation, because hardware acceleration devices have limited memory.

So making them space efficient, using finite field objects like binary fields that are hardware efficient, carefully looking at whether a computation is compute-bound or memory-bound, and designing around that. Those are the things we've learned about hardware efficiency. OK. We've got the last minute. We've got two more questions.

We've got one minute left here. So we'll try and speed through these two last ones. Doesn't Wasm require actual RAM and not ROM? Yes. So we would need an optional RAM in order to do that, but that would be only for actual memory accesses.

The Powder Lab guys are brilliant and have figured out ways to do all of the stack accesses and local variable accesses that are done in Wasm with the ROM. Got it. OK. And last, last question here. Do we need any additional compiler optimizations for the ISA or VM?

Yes. There's a whole lot of compiler optimizations that, I mean, I think we're seeing, we're pretty optimistic about the performance that we'll get with something naive. But one thing that I can say off the bat that we're interested in is reducing the cost of copying data from one function frame to the other, and also doing less pointer indirection, so sort of inlining data structures into function frames. Great. Thank you so much for all the questions.

Thank you so much, Jim, for the talk. We have about five minutes until the...