Day 1 Learnings

Transcript

[applause] So, uh this is day two of the post AI cryptography workshop. We have Giacomo and I who are going to be um moderating uh a quick debrief. The idea here is for anyone who has learned something interesting, anyone who has some alpha, you know, you're welcome to just come to the stand, grab a microphone, and just share something that that you've learned. Um one quick piece of alpha breaking news is that um last night there was a 5%improvement in one jump on the number of qubits required to break ECDSA.

Um so yeah. Uh congrats to to the very famous bitwanka that is now like cited in multiple academic uh papers, by the way. Um >> Do we know bitwanka is? Is that uh public information or >> a call with him, so >> So, he's a real person. >> He's a real person, yes. But he doesn't disclose his real name. >> Good. [laughter] Can we put him in like in a room and make him farm theorems? Is there like something that ethically not >> we just give him lots and lots of tokens. [laughter] Um so one one thing that I learned yesterday, just to get things started, is that um

there might be an opportunity to get from Nvidia a the formal semantics of PTX. Um so it's possible formal semantics of PTX. Uh in in in info, hopefully, possibly. Um uh so maybe they have already done this internally, and maybe there's an opportunity to share it with the community. And if we have this, then we're off to the races in having, you know, formally verified provers that don't crash uh and that are, you know, live and then and then So, that would be that would be amazing. Um Yeah. Who else wants to share some some alpha?

>> Yeah, for me like I Does this work? I think this works. Okay. Yeah, I don't know. I don't know. Just to kick start a conversation off like I think yesterday for me was a great day to see all the progress that's been done in binary fields like both like with the tricks with the universe keeps, you know, the new ZK VM using binary fields and like the the BTC techniques. So, for me that was extremely exciting to see. And you know, I don't know if I have fully internalized all the things that were going on. There was a lot were a lot of things going on, but I think it's really exciting to see the numbers that, you know, we couldn't have believed like maybe 2 years ago. So, for me this is like really exciting. So, yeah, this is what I learned to yesterday to kick

start the conversation. >> Yeah, and what I had in mind before yesterday was 10 million cycles per second for RISC-V proving on a laptop CPU. Now, what I have in mind is tens of millions of cycles. Um great. Um Who else wants to share some alpha or share something that they learned? Come ahead. >> Um so, there are a couple of events that Professor Matsuo and I are running across the next I guess 3 years.

One in particular is crypto agility for post quantum competition that's sponsored by Nedo, which is Japanese government agency, and we're looking for participation from the Ethereum community with your different PQC techniques. Similarly, we're doing a call for papers in the evaluation committee at the moment. So, there will be a more academic SSR sort of conference and call for papers for crypto agility over the next month or so. So, this is an opportunity for some of your techniques and work to get published on Springer. And sort of have peer review in in the meantime.

And we'll be using that evaluation as the assessment criteria for the two and two and a bit year competition where we identify different sort of crypto agility techniques and run a test bed of the Ethereum nodes or Bitcoin nodes as well. So, yeah, just wanted to let the community know about that and feel free to reach out to me directly for an invitation. The Block 15 meeting will be hosted next week and there's online attendance as well and I know Connor will be attending and Alex from Project 11 will be providing a keynote

on the PQC side of things. So, yeah. >> Awesome. Thank you. Okay, who else wants to give us their thoughts? Proprietary thoughts, they're not going to be fed into any other land, so you know. Or maybe, I mean, I cannot guarantee that, but uh >> So, one piece of alpha that I learned this morning is that tomorrow [clears throat] a new paper will be posted to ePrint which can aggregate tens of thousands of Falcon signatures per second.

And two of the authors of this paper happen to be in this room. And they are willing to present their result prior to the ePrint um today. So, we're going to make a last minute change to the agenda. We don't have any planned dinners today, so we can basically order in food or whatever. If you know, the idea is that small groups just have, you know, dinner as they see fit. But we're going to be extending the agenda from 5:30 to 6:00 with this very special uh talk which has this this unpublished result which is really exciting.

So, that's Alberto and and Quang who will be presenting at 5:30. >> Does this mean we might change from Sphinx to Falcon? >> Not for Ethereum. [laughter] I guess one one piece of logistical detail is that um

we have these 20 licenses uh that we're hoping that you can make use of. Um so, I guess I wanted to invite Nico to just uh share a bit of information about how how those licenses uh could be used by by you guys. >> Uh yes, so end of the day we'll have the seek.golf workshop and we have uh 20 licenses, so 10 Codex and 10 flood code seats uh that we're going to share uh for those who wants to try to prompt uh during the the session.

So, if you need the one more license, um what we can do is like during the day before the workshop, yeah, you can come to me and I will let you log in. I will give you the login on one of the accounts. Um So, if you didn't max your weekly limit, try to max yours. Uh but if you did already max it, then you're going to be stuck and you want to participate, uh just come to me at some point during the day before 4:00 p.m. uh and I will let you log in into an Ethereum account which is cloud uh {dash} PQ something.

Um So, yeah, come to me if you need one. And then during the workshop uh what we're going to do is like small presentation at the beginning, but then we will try to uh eventually improve uh the frontier on two uh new tracks for constrained devices and regular laptops. So, yeah. If you didn't max your weekly limit, please use yours, but if you did max it, just come to me and we will give you one. And you can go uh you can come to me anytime during the day. I'll be around here.

>> Awesome. Thank you. [clears throat] So, that yesterday Emil told me about a very interesting idea to potentially um have a much simpler roadmap for for post-quantum privacy. Do you want to share this idea real quick? >> So, um Ethereum wants to be able to verify ZK STARKs, meaning post-quantum SNARKs, which is currently possible, but not like uh SNARKs that that are not post-quantum.

And the current plan is to enshrine and expose a new ISA. Typically, it is five for instance. That would let users prove execution in this new ISA. And the yesterday's night idea was to instead simply expose a new PCS open precompile. Typically, you fix a field and you let user call uh let's say we're we fix we're in a field um and you and you essentially um have this we're precompile for a a um

PCS opening. And the key idea is that in a ZK-Stark, most of the verification work is the PCS. The PIOP is like 5%of the verifier work. And so, you would only need to um handle uh the PCS opening um aggregation in because you don't want every um weird opening proof to end up in the on chain. So, you would still need to aggregate them uh typically in the main pool but it would be potentially simpler than exposing a new ISA. Because in some sense, you only need to enshrine a field and a PCS, and it lets user write their own PIOP in

the EVM um as long as you expose a new uh multiplication restriction anyway, and potentially that would be simpler. That's it. >> Cool. Thank you, Emil. Uh on the ISA, uh one of the goal is also to make it um faster to prove, right? And we have uh this project by ZK Security and Yoichi uh called EVM ISM uh to directly um implement the EVM uh in Lean and so in ISM. But, what if we have um AIR directly uh

uh formally specified? Uh I think it's actually easier than uh a real ISA because it's uh just equations. And so, instead of having the AI doing ASM, and then relying on an assembler and whatever, let's just do AIR, and we'll get the fastest possible implementation for SHA-256, Keccak, and all those precompiles that are being plugging us and having have to have workarounds. And now that we have AI as good as this, uh Uh, I I used to work at Tyco and I was leading a team that was implementing circuits for Halo 2. And after a month,

everyone talked to me in private and said, "Can I work on something else? I'm getting crazy." [laughter] And so, let's just unleash Claude and Codex. Sorry, Claude and Astra on those kind of problem as well. >> Yeah, we might go full circle and uh, basically re-implement linear. Um, linear. >> Yeah, yeah, yeah. Cuz linear was basically do do doing that. Um, and you know, there's the saying that there's there's no bad ideas, there's only too early ideas. And and I think we're going to see a lot of old ideas that were too early being revisited. Um, another idea that was potentially too early was Valida.

Um, in the sense that, you know, it's kind of a a new optimized ISA inspired by RISC-V, but sufficiently different that you have to redo the whole compiler toolchain and whatnot. >> So, because I used to work on Valida, we have [laughter] we have an archive paper. Yeah, yeah. I was one of the engineer working on Valida and I we have an archive paper with the ISA formally specified. Uh, the main advances from Valida compared to RISC-V was uh, uh, you've seen in the Magnetar talk yesterday, you have to tweet and shout to prove memory.

And one of the main gain is to avoid pushing and popping the memory. So, Valida has a special calling convention that avoided that. And the other thing is, compared to physical architecture, you don't need um, registers. You can have an infinite amount of register. And so, we can very much have a special calling convention, for example, in LLVM. Uh, there is one called internal and that just do what we want and we don't need a specific ASI. We can just release uh use RV64 IMAD and some underscore Ethereum that just do don't do register movement between function calls and you

gain maybe 80%of what the validator gain is. And our benchmarks show that it's about 10x improvement compared to RV32. Uh and this is orthogonal to the cryptographic improvement that was done in the past 2 years. >> Just to complement this information, just uh explain a little bit uh the internal architecture of of this because it's very relevant to that. So, this is a very So, internally it's not RISC-V.

It's an internal It's a ZK VM. The VM I can explain to you how this VM works in 1 minute. The idea of this VM is just it has a single instruction. So, it's a VM that has a single instruction. This instruction very very much what it does, it loads two values. It can do it from memory or from an immediate value. You put it in let's say in kind of a register, but it's not even a register. It put it in A and B. It does one operation. You can choose operations. Here is XOR and multiply, whatever you want.

It have a result and a carry. And then it has two jump values. If carry is one, goes to the first jump value. If carry is zero, then it goes to the second jump value. This is the only instruction that VM has, okay? And this happens to be very interesting because with just this minimal instruction, you can convert This is maybe slightly a little bit more, but you can convert You can convert any RISC-V instruction one-to-one to this instruction. We can do this in in in a ZK environment because we are not limited by the 32 sides of an instruction in our case our instructions

are many polynomials there. Okay? So, the cool thing of this architecture is that of course we are risk five compatible just we are transpilation. Uh but we are also for example there is people there is actually a pull request that somebody that Guillaume did for wasm. So, there is a direct transpilation from wasm directly to this zk. And you could go I mean it's also memory based I mean it's what you were explaining so you can you can you can implement we we haven't because it's a lot of work but we we can do a a full LLVM back end on on that. Okay? So, and this VM has its own assembly.

So, one of the things that we are thinking is maybe implementing or porting the a wasm work somehow to let's say a native zisk assembly. With probably with direct formal verification that the equivalence of that but just explaining the internal architecture because I think it's relevant how we are doing. No, Pllee is Pllee is a language for writing the for writing the the the the the arithmetization of the of the stark. I mean all this VM is written I mean we it's implemented using Pllee. Okay? By the way we are removing Pllee and and doing in lean the

asset that we are doing was explaining that in order to have a Pllee verified. But that's I mean just explaining because I think this architecture is quite interesting because it allows you the best of all the worlds. >> So, we have four ways to do this EVM ASM which is there. We have the valid approach we have risk five modified and we have a one instruction VM. >> There's another way as well. Okay come [laughter] >> So, all of all of this can be in the auto such that you design zkVM home and verify and the guest home and verify both on the e-size just an intermediate dilemma.

One One idea from last night's dinner was maybe GKVMS can expose this primitive over sending doubles and receiving doubles. Uh because they many cases in the game in the EVM guest as well like sometimes I have to make a list and put things and read things and everything is written once and everything is consumed once and but that's very that takes many many steps I I have to split things up but like 64 bits and I put the things in the memory and sometimes allocate memory and whatsoever but if I have this send and receive primitive you you have to implement anyway in the guest then that will be very easy.

And that's something quick to do and that will improve the performance a lot. >> Right, so if it is...oh, so there's also a completely ISO agnostic way to do this, which is that you take, let's say, RISC-V because that's what we have now, and then you pick whatever representation you want to prove your program in, and you do a SNARK of that, and then you do a SNARK of compilation to RISC-V, and you combine both, and then you have a SNARK of, you know, proving whatever program you want from whatever representation you want. >> So you just choose whatever representation you want.

>> Yeah, so you pick any representation and as long as you can do a SNARK that you can show that it is composed to RISC-V then you can prove that IR and you know it will also accept that it would compile to RISC-V and run and produce the same result. So you can do a very prover friendly representation, do a SNARK of that execution and then SNARK of that. >> SNARKs of lean formal proofs? >> Uh yeah, you so you would have to formally model the compiler to make sure that you get the same program in the end. Yeah. But if but if you have a formally verified compiler and you SNARK that [laughter] then it's fine. But but then you can prove whatever you want.

Then it's then it's completely ISO agnostic. Anything you can compile down to like RISC-V or whatever you enshrine you can prove. So it's completely agnostic. >> I think it's simpler to just prove uh implement the EVM as circuits directly prove Well, well have LLVM fully formally verified soon, so >> Okay, Dara, and then we'll start the keynote. >> Okay, so um if you think in terms of um ISAs, then you're missing a lot of the techniques that um proof systems can give you an asymptotic speedup. Um because if if you give um your smart contract access to things

like permutation arguments and um uh probabilistic checking and um all of these nice things that you can do specifically in um uh SNARK circuits, then that can be um an asymptotic speedup of any possible ISA that doesn't include those features. >> Uh the way we solve that is very much using what we call precompiles. I mean, precompiles at the end are very specific circuits that uh do something uh some fancy uh thing using some arithmetizations. Examples are Keccak or um I mean, um arithmetic, I mean, elliptic curve

operations and things that you can use interesting things at the arithmetization level, okay? Um interesting thing here, I mean, something is a debate because in the the main three KVMs, we are doing we're implementing this in a slightly different way. When explain Yesterday, I learned uh three ways. So, in Zcash, we are doing it um thinking very much as a hardware as a hardware uh board that you block in the board of the Z5. So, the idea is that and then we have like a input-output that is a CSR uh interface with this board, okay?

There is other interface, I mean, I think that uh SP1 is doing it with equals. So, okay, they they they they they are interacting a little bit like a kind of an operating system uh on that, which is another way. And I think that Open BM is doing it with their defining their own instruction I mean they are extending ISA so they are defining another instruction. At the end we are very much doing all of them the same. This is what we are interested to to we are we are we are talking for a standardization but again this is the way we are interfacing and and this is at the end you can pack all this in a kind of a library and then you you you you you get advantage of that.

Always is a balance between standardization everything RISC-V or optimization. And and and the frontier is not clear what's better in one side or the other, and these decisions are very specific. And here the new foundation is doing a great work, uh um, setting up this interface so that some holes becoming kind of a standard. And I think it's it's even more than a standard; it's a good way of cutting, um.

So what makes sense to be a pre-compile with some arithmetic decision and you can play on, and what should be in RISC-V. >> I think it's I think in power is still a function that someone has >> Yeah. >> And if you want to talk more about this Kev should be in the room somewhere like that is one of the things he is in the corridor okay. That's one of the topics that that that he has spent a lot of time on. [applause]