Lightning Talk: Binius64: Binary Proofs for Bitwise Operations by Jim Posen, Irreducible

Transcript

Next up is Jim Posen from uh Ireducible talking about binary proofs for bitwise operations. >> Thanks. >> Yeah, [applause] >> let me set my uh stopwatch here. Hey everyone. Uh thanks for being here. I'm Jim. Uh I'm going to talk to you about Binius 64 which is the latest version of the binas proof system that we've been working on and I'm going to I want to talk about basically the journey to get here some of the learnings along the way. There were a lot of new ideas but also a lot of discarded ideas um and uh it's ended up in this this new proof system. So to start with the basics what

is binius? Actually not that easy of a question to answer. A lot of people think it's this paper that we published uh two years ago which curiously does not have the word binius in the name. Uh and it turns out that that was a good thing that we didn't put it in the name because uh we ended up taking some ideas but actually discarding many of them. So the core uh contribution of this paper was a polinomial commitment scheme for binary tower fields and we shortly f after this found a better polomial commitment scheme and actually binius 64 doesn't even use tower fields instead binius 64 still uses binary fields but it's a simple and standard degree 128

extension over uh gf2 that we ended up using. So instead of describing what is binius by like the cryptography techniques that we use, I want to go to like why is binius like what are the founding what are the principles that we're trying to achieve with this system. So when we started profile or when we started profiling the existing ZK snarks that were out there uh proving was very slow and we set out to build a computationally efficient proof system especially targeting custom hardware as in if we could build hardware specifically for ZK proving which is what we were doing. Um what is the most computationally efficient and we

basically found these three bottlenecks. So the first is all proof systems just boil down to like lots of finite field operations. So you need to make your finite field arithmetic really fast. Now it's well known that in custom hardware binary fields are the most efficient. What not everyone does realize is actually on modern CPU processors the fastest 128 bit cryptographically secure finite field available is the G# 128 bit finite field because modern processors have acceleration for this. The second thing is we termed this uh this phenomenon of embedding overhead which basically all the proof systems suffered from. And in order to emulate bitwise operations which are are common like

exor and and you would pay the full cost of a finite field operation to do something on one bit of information. And this is really pronounced when proving classical hash functions which is not uh a niche use case. It's of fundamental importance for backwards compatibility and security. So the way that most proof systems including BSV0 went about this is to throw a lot of arithmetization tools at the problem. So if you have too many gates then we're going to make some custom gates and uh to handle range checks we'll we'll add some lookup arguments and then to handle control flow uh we're going to build a virtual machine which uh can emulate um program

execution and we'll we'll use recursion for memory usage. But then each of these tools sort of creates more uh things that you need. So when you have uh custom gates, you're going to start doing like table layout planning and the virtual machine needs a memory argument now. And uh you you might want a custom language for that machine which means you have a compiler. Uh we have some pre-ompiles and now our tables are getting really wide. And when we have you know custom gates now our our verifier logic is getting dynamic and it's uh maybe so dynamic that our recursion architecture like needs to itself be a virtual machine in order to just handle recursion. And we sort of wound up in this in this tangled mess of

complexity. And so Binius original v0ero uh basically took all of these techniques and and tried to throw everything at it and and some more that were specific to our settings. So we had this idea of we were going to arithmetize over multiple binary tower levels that our arithmetization had different data types. Um we have we wanted to leverage derived columns that were not committed because uh if commitments are slow then we can use these sum check based reductions and this sort of um got too complex to handle. And so we wanted to change to building okay how do we make just a

simple zero knowledge proof of a identity credential like a concrete use case that's not block proving and all this stuff was getting in the way. Um and so we for these this client side proving use case that we then wanted to tackle kind of went back to the drawing board and said okay how do we make a much much simpler proof system that's taking the advantages of what we have but otherwise um you know trying to be as simple as possible and we arrived at at bineas 64. So we basically kept these uh these four crucial components. So the first is a polinomial commitment scheme that can efficiently commit to bits without embedding overhead. So we can

commit to the individual bits of a system that uh we want to use. We can very efficiently prove uh the bitwise and relation. So this and we can also prove exory because that's native in binary fields. And the way we prove bitwise and is using uh an idea called the univariate skip. and um sort of optimizing specifically for that use case. We also have a a special integer multiplication accelerator which is a GKR circuit. So we have a a specific technique for uh doing an integer multiplication check sort of in the exponent of our finite field using a GKR circuit. And the last kind of unique

thing about this system is word level wiring. So instead of sort of containing instead of having wiring information per bit, we group all the bits into 64-bit words and um do the wiring that way and that is very natural for programs which are you know a lot of hash functions are are based on 32 or 64-bit words. I will mention that this is not a VM. This is not capable of proving Ethereum blocks. This is for simpler client side use cases and it's in a circuit model. So this is the like one picture diagram of how things work. So we have a witness on the left and for every witness word which is 64 bits we get to apply some

bit shifts. We can exor accumulate as many bitshifted uh things together as we want and then we can either um apply or constrain them with bitwise and relation or the integer multiplication relation. And um this is only a few tools but it's really powerful and lets us prove a lot of hash functions. It lets us prove we've uh written circuits for elliptic curve uh signing. We can do ethereum signature verification um using the the mole constraints and our performance numbers are uh are really good uh compare for on the CPU compared to stew and plon 3. our single threaded and multi-threaded performance

for hash functions um are are the best that we benchmarked against. Um, so the point I'm trying to make here is with just a few primitives that are sort of carefully distilled out of the research that we did with Binas optimizing specifically for bitwise relations, we can have this very powerful uh prover model and um and it's working for for client side proving. Now, as I said, this is not a VM, but this these techniques I think could be adapted really well to the VM setting. And in fact, our bottleneck with this system is is one that was surprising to us, which is uh the wiring argument. And I think that could be optimized away in a VM

context. Um I want to aside from the cryptography here, make one final point about simplicity. So we're building systems and technologies to secure like global financial infrastructure and there's been this explosion of ideas in the space and this process of building Benv0 and then Bine 64 has really enforced um not just the importance of simplicity to me but that simplicity requires sacrifice but it's worth it because the complexity of these systems compounds and um if you you know, that was my experience with this. So, uh, thank you very much.

[applause] >> Okay, thanks Jim. I've got a couple questions here. Um, first question, uh, any future plans roadmap for BIA 64 that you have in mind? >> Um, definitely. So, BIA 64 is not zero knowledge yet. uh that is on the road map intended to get it done within a few months and then it will be a zero knowledge proof um with you know proof sizes on the order of 100 couple kilobytes and then beyond that the road map's unclear.

>> Um is the wiring verifier linear? If so, how do how do you uh plan to address this? >> Is the wiring verifier linear? Um the verifier is I mean it's a it it will be a succinct argument with um so oh sorry the ver the wiring verifier right now is it needs to do a matrix evaluation. So it is not succinct but it can be made succinct using the standard spark technique that's in in Spartan. So um it would be a sublinear verifier for wiring once we go and implement that. And personal question, well from me, not a personal

question, but have you checked out the new client side proving dashboard on ETH proofs that just launched? >> Uh, someone sent me a screenshot of it that needs to go 64 is a top several leaderboards. So >> cool. >> Interested to see if you have feedback on it. If you do, I'd love to put you in contact with the team. >> Absolutely. Thank you. >> All right. Thank you very much. Uh, up next we got Leo Alt from Powder talking about pre auto pre-ompiles.