Jim Posen of Irreducible @ ZK Hack Meetup in Berlin, 24 Apr 2025

Transcript

[Music] Yeah. Hi everyone, welcome. I'm Jim. I'm the CTO and one of the co-founders of Ireducible. uh I'm going to tell you about binius and the programming model that we use to express like verifiable computations. So this is going to be a technical talk.

Hopefully you don't need to know that much about zero knowledge and hopefully you learned something. Um but first I am obligated to tell you about irreducible and who we are. So I is a a startup that as of uh 2025 is has a Berlin based headquarters. Uh we're accelerating the zero knowledge revolution with the world's fastest proof generation. This basically means our whole mission is we go every day and try to build the fastest technology for verifiable computing. Um why? Because first for blockchain applications I believe this is the only way to securely scale blockchains and peer-to-peer systems. uh we need cryptographic verifiable

computing in order to get you know the worldwide adoption um without compromising the essential auditability auditability and transparency guarantees that make blockchains important. But there's also future applications beyond the blockchain space that I'm excited about. Um this is a fundamental technology that can be used to verify content authenticity and in a world with more generative AI hopefully combat deep fakes. um potentially be used to check the safety and and bias of uh machine learning models or AI models running remotely. Um and then there's all the zero knowledge and privacy applications. So uh there's a lot to be said about this. You can come find me

afterwards if you want to hear what other applications I'm excited about. What I is doing is we're building a vertically integrated stack for verifiable computing. So this is uh actually a lot of technology going from the top layer of virtual machines that you can that can uh run some computation that you want to prove and verify succinctly uh through the proof system layer which for us is binius and we have a lot of technology in the custom compute layer that uh this little box doesn't do justice to. Uh basically we're designing custom hardware. We're running servers. We're designing hardware uh instruction set architectures, building a system on

ship, custom drivers, custom languages for all this stuff. It's very cool. Um but uh I'm going to focus on the middle uh for today. Um and on the virtual machine side, we're partnering with uh some other companies in the ZK space like Polygon and Risk Zero to develop virtual machines. And the talk is going to be about how do you express a computation that is provable or succinctly verifiable. And at the very top we want to be able to verify programs that are just in Rust like regular programs that you would run. And how are you going to do that?

Well, you're going to compile this Rust program to a virtual machine architecture. So for example, Risk 5. And then you need to prove the execution of your risk 5 machine with a proof system. So binius is the proof system that uh we're developing. It's based on binary fields. I'm not going to talk too much about that, but it's sort of a alternative modern alternative to other proof systems that you might have heard of like Halo 2 or Plunky 3 or Stew. And a proof system has a prover and a verifier. they're communicating uh the prover is doing a lot of work and the verifier is reading a proof and not

doing that much work and they both need a front-end API which is how you're going to express the the computation. You may have you've probably heard about ZK circuits like you're programming a ZK circuit and then you're going to prove a circuit. Uh we're not talking about circuits. We have another framework for expressing computation. So like what can we prove with Phineas? Um I'm going to give a totally random uh example here. So let's say you're escaping a maze. Like imagine you're in the middle of a maze in like some corn fields and you don't know how to get out and you

would actually don't even know if you can get out. You don't know if there's an escape to this maze. So how would you figure out if you can get out of the maze? Uh well, one is you can wander around in circles until you get out or not. Um that's not very good. Uh the second is I can shout directions at you and then you're going to follow my directions and I'm trying to convince you you can get out and you're going to follow my directions and eventually you'll end up at the exit and and you'll walk out and you'll be convinced that there was an escape to the maze. Uh, and then I'm going to say basically that there's some way to succinctly convince you without you walking through the whole maze that there is some way for you to get from where you are to the

exit and and walk out using M3, which is the the programming model for Binius. So let's say uh oh no your start location is is 00 and the exit location is 100 zero and you're just going to follow my commands. Um so I shout step up and you're going to uh have your location state which is like a two-dimensional coordinate in this grid.

And when I shout step up you're going to update from x to y + one. Step down, you'll update your y-coordinate. Step left, you update your x coordinate. Uh these should probably be x's. Yeah. Um there's one problem, which is uh if you just do this all the time, you you might run into a wall. So you actually need predicates for each of these commands. Like you can only follow the command if some predicate is satisfied. So you can update from x+ y to x+ y + one if uh that that cell is empty if there's not a wall

there. So we're going to express this in this sort of weird graphical model uh that looks like a state machine but instead of it just being a state we are going to think about these green boxes as tokens that you can you can take and you can put back. So you have a place where you can put your location tokens. And if you want to step right, you pick a location token from this this spot and uh you go and modify it and you can put it back.

And what I'm claiming is that if you initialize this diagram with one thing in the location spot which is 0 0 and you follow these transition rules and you end up finally at 100 then it must be the case that there's an escape to the maze. Uh assuming that the transition functions have the predicate of the walls being empty. Um that's uh so the the new thing here is that you're following these commands but there's this tokenbased model where it's like I can pick up the location token and I can put it back after some updates. I haven't talked about walls

yet. So how do I check that there are no walls? I'm going to introduce a new place and a new type of token. So the location tokens were the green tokens. The map tiles are the blue tokens. And a tile has a xy coordinate and either it's empty or it's a wall. And the new So this is the step up transition. So when I step up, I have to take my xycoordinate from locations and I also need to take an xy + one empty token from the map tiles. And if I can take these two tokens, then it means like I am at XY and the place I want to

go is empty. And then I'm gonna put back uh my my empty token. So it it returns there if I ever want to try to go through there again. But I'm going to update my location. So this is now uh I have this mechanism for checking through wall for checking for walls. And basically, if I if I ever shouted to go through a wall to you, you just wouldn't be able to pick up the the empty tile, it it wouldn't be there. It would be a wall instead. Uh, and now I'm adding doors. So, you didn't see that coming.

Okay. How are we going to handle doors? What can I do with a door? Uh, when I shout open door, it's you're going to stay in the same place, but you're going to try to open the door. You're going to update the map. So, where there was a door, now it's an empty spot. And I you in order to um open a door, you need to take a location token. You need to take a uh a token with xy + one and a door in the place where you want to open the door. Um, and you have to have a key. And um, the way I've written this is actually the key gets stuck in the door and it goes away forever. So you might like start with a

finite number of keys and then every time you open a door um, it it goes missing. So if you don't have any keys, you know, you wouldn't be able to open the door. You wouldn't be able to follow my command. Um, but then so what happens? Well, I'm going to put my location back to the same one. I'm actually not going to move. I would have to move on on like say the next transition. But I'm gonna take where there was an x y + one door. I'm gonna put back an empty spot in its place. So this is the sort of transition rule for uh for opening a door. Um oh this is basically the model.

This is the whole model. And what I'm not really going into in this talk as much as why this is efficiently provable. Um but to say it briefly for the people who are more familiar with zero knowledge techniques um we can check these um what we need to check I thought there was a slide actually. Oh, well. Um, wait. Oh, I I feel like I have time to do this. I think there's a skipped slide if I can. Oh, yeah.

Uh, wait. Shoot. Oh, well, I guess it's here. Okay. This is briefly uh a bit about like why why this is an interesting model for proving. And this is an efficiently provable paradigm. If you can express the rules of provability as being consuming tokens, putting tokens back that are derived from them, having predicates on when these fire, uh we can use cryptographic arguments. And so if you go and look through the binas documentation, we have slightly different language for this stuff, but we can basically use permutation arguments to check this channel balancing equation that you're going to

put some initial tokens in some places, you're going to expect some final tokens. And if the initial tokens plus the set of all the tokens that you you put into a place equals the set of final tokens plus all the the ones that you've you've taken away. If that's true then the statement must be true. And um this is this is really powerful and it lets us express arbitrary computation. That's a big claim. What does it mean that this this model is powerful enough for us to express arbitrary computation? Is there a slideshow. Well, virtual machines are mazes, right? So, the location that

you're in is the program counter. It's pointing at an instruction. The map tiles are main memory. Remember how we could we could read a door and then put back an empty. I can go and modify memory by having, you know, cells with a with an address and a value. And the commands that I'm shouting at you are instructions. So we in Binineas are going to express the uh semantics of our virtual machine using these commands. You know if I am in a location where my program counter is pointing at an ad instruction and the memory satisfies the predicate of AD then I can I can accept that AD instruction. And so Vinius can prove mazes, Vineas can prove VMs.

Uh I glossed over a lot of technicalities. Um I want to say that the model I presented here is uh a well-known model in programming language theory called colored petriets. They're they're very well studied and are amenable to formal verification. Um M3 which is the binius arithmetization is closely related. There are some technicalities um you need to add timestamps for security but it's very very closely related. And uh if you can model something as a colored petriet, you can model it as a binius m3 program and prove it. And that's my talk. So here's where you can learn more about irreducible. If you want to learn more about binas, our proof system and m3, uh binius.xydz is the place to go. And um

does anyone have questions? I'll just say I have a reducible t-shirts at the entry door but only for the people who ask questions, right? I got encouraged encouraged to ask questions. Um I have a question here and maybe this is very example based but is the main example zero knowledge because at least how you put it it seems that I could I could read let's or learn the the path basically. Uh no, there is nothing I talked about that um gives you an idea of why this would be zero knowledge. Uh

it could be this programming model like um could be this sort of gets into the how you take a so again the the paradigm is you set up the maze and then all I'm trying to claim is that if you start with some initial tokens then you'll be able to reach the state where there are final tokens. The verifier shouldn't need to do every command. Instead, it's going to get compiled into the proof system and there's going to be polomial magic that happens that convinces you that the final state is reachable from the initial state, but you're not going to do every command. You're going to check polomials and you're going to verify this succinctly. That was not really part of this talk.

Yeah. And then there would be you know if you wanted to make it zero knowledge you would add random blinding factors to your polomials and then it would be privacy preserving. So something like that maybe another one um M3. Okay. This is kind of like a new way of basically. Yes. But you use kind of or like you use like own for this uh we use a multilinear IOP um so it's using the uh a toolbox of things that other are familiar to people

we use sum checks we use grand product arguments we do permutation arguments we use fry for the PCS um that's actually if you go to binius.xyzb XYZ blueprint. The blueprint kind of lists all the polomial IOP ingredients that go into the binas proof system. Yep. Chris, your example. Yeah. because binary fields is more complicated. I assume operations are not operations.

They're not elementary. Yeah, they're they would be constrained with nonlinear constraints. And so that we have a sort of mapping of um so what what does a binius proof consists of? You have a witness which is a list of all the events that will ever fire. So every time like arrows go into a rectangle, that's like a transition event. And we list out for every one of those boxes all the events. And so for something where it's like you're putting back x + one, you would have a table that has three columns like x, y, and z. And you would have a predicate constraint that z= y + one as integers. that would not be a say algebraic thing in binary

fields but it would be like a nonlinear constraint that we can check bitwise um pretty efficiently and and then you would you know put the x y token in one place and the xz where z is y + one in another place. Does that make sense? read operations if you want to use operations. Yeah. So in binius the in the actual programming framework um we have we have these tables and then we have a library of gadgets and gadgets encapsulate the common like nonlinear constraints that would be common. So we have like a U32

edition. We have like a barrel shifter, bit shifter. Um and then you can actually implement those predicates using lookup arguments or bitwise constraints or binary field operations or like you have a lot of tools available to do that. Uh yep. What's the computation? Uh so every ele like we define a a table and a like a flushing we call them a flushing rule but it's like every arrow from the table means that every event that fires is going to you know send something and that ends up being a

leaf in a grand product argument. So, um, it's proportionally linear. Um, we can measure basically I don't know the numbers off the top of my head, but we measure like the throughput of our grand product arguments. Um, I can actually show you where to find these numbers online. If you go to benture.dev and you search for the binas project, there's like a site that lists open source benchmarks and we put stuff up there. So we would look at like the grand product argument of doing a grand product over a table with like a million entries and then you would divide by a million and then you would get the sort of latency cost or throughput cost of doing uh of flushing one

event. Yeah. So but I guess uh a channel flush corresponds to one leaf in a grand product argument per per event. Think there was one more question. Yeah. limitations compared to other systems. Um, so there are a couple of tools that we've gotten rid of. It is just as expressive. So this is I mean you can express any problem in NP in this language of of M3 or colored petriets or whatever. Um, there are some constraint systems in like an air that would maybe be more efficient to

prove than in M3. But we think that in all of the in VM design and in basically all of the real constraint systems that we've seen in the wild, M3 is more efficient. Why is it more efficient? Because we can handle control flow through flushing where most other proof systems have some combination of control flow coming through like selectors where if you need to do an if or an else then you like do both of them in parallel and then you multiply one one by one and the other by zero. um in if you do control flow through flushing, you're actually only executing you're actually only paying for what you execute. And so um it ends

up being really efficient for uh a lot of natural use cases including VMs. Okay.