L1 zkEVM Breakout #3

Transcript

Ladislaus: Hi, folks.

Kevaundray Wedderburn: Testing…

Ladislaus: Oh, hi. Perfect.

Kevaundray Wedderburn: Okay, great.

Ladislaus: We need to improve that prompt calf for the font size.

Kevaundray Wedderburn: I think it's just on a larger screen, it looks pretty big.

Ladislaus: I'm not so sure about that.

ben bencik: On the stateless summit, it looked nice. No, they send me the same template, right?

Kevaundray Wedderburn: Yeah, I think it's my screen. You need to stop giving away the fact that I, prompt my slides that.

Ladislaus: It's a meme by now.

Kevaundray Wedderburn: I think no one knows. Second…

Just gonna give it one more minute.

Okay, I think we can, get started. Well, but… My screen. The Zoom is recording… okay, cool. Welcome to the L1 ZKVM breakout call number 3. Today… We have 3 items on the agenda. The first one is an update on EVM ASM. The second, which can be rolled into the project updates, is an update on the DevNet for the ZKCL, and the third one is the project updates. So just starting off with the first one, Derek, if you can… unmute to give us maybe an update on EVM ASM, and maybe a small introduction to what it is, in case folks don't know.

Derek Sorensen: Yeah, absolutely. It might be easiest if I can share my screen. Okay, perfect. Let me… Okay, how's the font size?

Kevaundray Wedderburn: It's looking good on my end.

Derek Sorensen: Okay, anyone… Does anyone want it any bigger?

Alex Hicks: A bit bigger would be good on my end, because I'm on a laptop screen.

Derek Sorensen: Let's see, is that better? Okay. Right, so, a… EVMASM is a project that was, started recently by Yoichi. At ZK Security, and, I have recently started to contribute to it, and so any caveats on, I guess caveat on, on… I don't know. There are probably some details that UHE will know better than I do at this point, but let me just kind of give you an overview of what this is and where we're at. Evmasm is an attempt to write a guest program for, L1 ZK EVM… ZKVMs, the EVM in… directly in RISC-V assembly. And so there are some good reasons for doing this. Yeah, lean… Lean4 is a good place to do this. First of all, we can formally verify and have really high assurance at a very low level. Second of all, AI… Gen AI is very good at,

if it's constrained within the context of a, like, a proof system, like Lean 4, you can get it to reliably write good code that is also correct, because you have to… you force it to be proved correct with regards to a spec. So, we have a formal specification of RISC-V through SAIL, and we have a formal specification of the EVM, that was done by NetherMind that was extensively tested, and there's kind of a whole story there. So, the idea here is to, write the EVM in assembly for RISC-V, Prove the RISC-V bit of it correct with regards to sale, prove the EVM bit of it correct with regards to our EVM spec, and have it as optimal as possible, and importantly, have it maintainable and kind of generatable through AI.

And, because everything is proved correct, we have high assurance that the AI has done its job. So, no human has to do all of the super low-level, painful, painful things. So, let me just give you… a quick overview, so in EVMASM, there are two key components. There's a model of the RISC-V, of RISC-V, and within that is the EVM implemented with RISC-V semantics. So, I'll start really quickly with the… looking at RISC-V. If we go to, Yeah, if we… if we just go to this basic file, RISC-V has… we have, I think, 55 of the, RISC-V opcodes implemented here. Which is a subset of the full RISC-V, as I understand it, but kind of the ones used by the EVM.

And their semantics are given in this execution, file. So, for example, add. I have been working today, to prove this… there's… there's sort of a… there's the… The state is, modeled by this machine state type, And there's, kind of the program counter, things like that, and so today I have been proving it equivalent, with regards to the sales spec, which is kind of done here. And so, I've made my way through. We've been able to prove so far that 24 of the 55 opcodes are correct. And then, on the EVM side, we have, as I understand it, so I guess here are the opcodes we have implemented. Each opcode, for example, AND, Here has, the format is pretty consistent, and so there's,

There's a program, file which gives you the actual opcode, in… so, yeah, this is, in, kind of, RISC-V instructions, and so, yeah. And this is all done in 64 bits, and so, And so the spec of this comes in kind of a limb spec, so you're looking at, the behavior of the opcode based on its 64-bit limbs, and then a more high-level like, spec for the full 256-bit. And all of this uses horror triples and separation logic, if that means anything to you. so, where are we at? From a high level, I guess… So, from the EVM, this is, this is, We're having Claude maintain a plan and keep it up to date, so if you want to know at any time, you can always look at the plan.

Like I said, we have many of the opcodes on the RISC-V level implemented. And we're working on formally verifying those. And we've done kind of the more basic ones, and there are some more advanced ones, to… to do next. From the EVM side, as far as I know, so the kind of 54, these, like, primary opcodes, they're all done. They're all at least, implemented, and they have a spec. We haven't yet formally verified anything against the EVM spec done by NetherMind, which is a little bit of a higher level of abstraction, so that's kind of… that's a to-do. But… and then, there's stuff, relating to, like, memory, state transition function hasn't even been started yet, I don't think.

And, you know, so there's a lot to do on that side, from the implementation perspective of the EVM, as well as from the verification. But… this has all been done in the context of, I think, just a couple weeks, maybe 2 or 3 weeks so far, and And… yeah. So we're… the goal is to, make this as secure as possible, of course, with the goal of it being bug-free, as efficient as possible, and then also as easily maintainable as possible. And so, a lot of the work here is going into the workflow for GenAI, so that, So that we can reliably have the most high-assurance guest possible. So in some ways, it's kind of an experiment, but we've seen a lot of… we've seen enough, really high-quality

products of Gen AI when handled by experts, that we, are optimistic, I guess. So, I think that… that is my… that is my update.

Kevaundray Wedderburn: Thanks, Derek. There's a question in the chat by… Alexandra, it seems that the overall size of the EVM implementation is very small. Is that around 1,000-ish RISC-V instructions for the EVM?

Derek Sorensen: That's a good question. Let's…

Kevaundray Wedderburn: I guess…

Derek Sorensen: me.

Kevaundray Wedderburn: VM implementation's not fully complete yet.

Derek Sorensen: No, it isn't fully…

Alexandre Belling: Yeah, so just to clarify, it's because I saw that, the implementation was using, like, 20-ish PIS5 instruction per opcode, and, for 50 opcodes. I believe it's only, 25% of the VM up codes, or something like that. If my count is right. So yeah, that's why I was, basically eyeballing, 1,000, research instruction, but I remember seeing a complete health program for the EVM, and it was, like, more in the 100 thousands. So that's why…

Derek Sorensen: Maybe… So something like Byte is… more involved. Mole was more involved.

Mamy: So, I think one of the reasons is that a complete ELF program generated for a ZKVM is likely to have lots of extra functions for, Accounting, for example, gas costs, function calls, etc, while, if you start from assembly, you remove all of that overhead.

Alexandre Belling: Yeah, that makes sense. Because the compiler would intuitively try to minimize the number of instruction code per EVM execution, while here it's, basically minimizing the program complexity, because it would just be too complicated, to do one function for Gaza counting or stuff like that.

Mamy: I can't say. I haven't looked at EVMAs yet.

Derek Sorensen: Hard for me to say, I… yeah, yeah. Things may get more complicated with the STF, that will definitely be, quite an involved… Yeah, hard to say.

Mamy: if we start doing, those kind of efforts, on, formally verifying low-level primitives, I'm wondering if we shouldn't try to formalize, air, representation, because I know that in the past, some of the teams that were trying to add GPU acceleration, they basically reused the weakness generation from, let's say, SP1 over 0, and then they plugged that trace into their own GPU prover. And if we have this kind of, formally verified serialized error, we can also have in that AVM ASM, some kind of, some of the opcodes are really, they have no branches, like all of those divMod, Add, or etc, and we can… Decide to generate, how do you call that?

An optimal, error constraint, because if you look at the ad… opcodes. Right now, it's very inefficient due to, all the carries. I would even implement it differently in RISC-V using unsaturated arithmetic, but we could bypass that by having, similar to EVM ASM, some kind of EVM error. formally verified for just the opcode that are… that don't have, branches. Because we… we can just, we know that the trace with error that we generate will be minimal for them.

Kevaundray Wedderburn: This might be too in the weeds for this, for this particular call. Maybe we should take it off.

Alex Hicks: So, if I can add one quick comment, just for the sake of, kind of, completeness, and then we can move on. So, one interesting thing, actually, that came out of, of this effort, Mammy, is that Yoshi did… had a look at basically comparing some of the assembly that Claude was generating for this to some of the assembly that was being generated by the Rust compiler. And, one interesting thing was that Claude produces more straight-line code, whereas the Rust compiler produces more branching. And so, for some quirky reason, Claude is actually producing, at least in some cases, more optimal assembly than the Rust compiler does, because it has less branching.

Kevaundray Wedderburn: Thanks, Alex. I guess one.

Derek Sorensen: restaurant.

Kevaundray Wedderburn: Before we wrap this up, Derek, do you have, like, any aspirational, Goals as to when you think we could possibly prove The SDF, or even just the EVM part.

Derek Sorensen: aspirationally. I think we can make a lot of progress in the… in the next couple of months. I think it's… it's not… it's not… Out of the question that within a few months, we have something that's… that's working? I… yeah. I hesitate to commit to any, you know, any of that, or, you know, I, I feel very optimistically about the speed of this project, but I also… I also don't want to raise expectations, unreasonably. This is… this is… yeah, this… this is a really interesting exercise in low-level programming with… with Gen AI. And I think if we succeed here, then that may have other implications for ZKVM's optimal implementations of things.

But yeah, personally, I would, you know, during the summer. I would really like to have something, like, working that we can actually Try to plug in places and see what we get.

Kevaundray Wedderburn: Great, yeah. I mean, yeah, that sounds amazing. I look forward to, sort of, more updates on this to see how far you guys go. And yeah, thanks, Derek, for sharing this.

Derek Sorensen: Yeah, yeah, no problem.

Kevaundray Wedderburn: The next one, I think we can just go onto the project updates, so just going into the execution witness and, the guest program. updates by Ignacio. We can do the DevNet updates, once we get to Francesco.

Ignacio Hagiopan: Sure, can you hear me?

Kevaundray Wedderburn: Yep.

Ignacio Hagiopan: Yeah, we'll share the screen. Can you see my screen?

Kevaundray Wedderburn: Yo.

Ignacio Hagiopan: Cool, yeah, so just before the project number one updates, I just wanted to mention that, with Cody, we did a presentation from… for the EPF study group of CKVMs for Ethereum. So, if you are interested in having, like, a, let's say, complete picture of what is CGVMs for Ethereum, I highly recommend Looking at this, Youtube video on… Or the slides, if you watch. So, regarding project number one, which is the execution witness, we have some updates, So, developer Rucha has been working on this new Engine API RPC proposal, which is called Engineer Paddle with Witness. So, the idea here… is that we have a specialized engine API RPC that… can, do…

Like, two things, in a single call, which is getting the execution witness for a new payload, Which is something that now we have to do with two different RPCs, the usual engineer payload and the bug execution witness. So he has been working on formalizing a spec for this new engine API RPC. And, there are pretty good results into this strategy. So I highly recommend anyone interested in this in looking at his, execution API PR and his E3X implementation branch, that is a work in progress. Regarding the specs and tests for execution witness generation, We have been working pretty heavily on this in the last month. We have, Yeah, 139 new tests covering a wide range of

Important cases to check that the Execution witness generation ELS is built correctly. The current testing coverage is pretty good, in the sense that all the fields of the execution witness are covered, you know, like. reasonable scenarios. There are still some of them that should be covered, mostly regarding really weird water cases of getting out of gas in Particular situations that can create some kind of partial execution witness, but we will keep adding them in the near future. And also, all these releases, that we are making are for… Tests that… Can be run in the current… In the latest, Val DevNet, chain. So, basically, this is mainly to simplify EL's life, because they are mostly working on the latest Baldemnet for Amsterdam.

So, they're gonna use the same branch to run these tests and see how it works. Regarding, ELs working on this, we have some progress here, so I3X is already passing the, this version, this version of the, of the release. So that's pretty good. They are not passing the latest one, because I created this latest release, like, just some days ago. But there's good progress there. Reth is starting to… More formally build the correct branch structure to start running these tests. Kept these some, GAF PRs to… Also be able to facilitate running these tests. And, some from Silkworm has wrote an… a cool document that goes through a more, like, step-by-step reasoning on why checking execution windows in a guest program is needed.

Maybe for many of us, this was somewhat obvious from the start, but… I think this is very useful to really keep explaining the logic behind all these decisions, so highly recommend you read his document. And yeah, that's everything for project number one. I will continue with project number two, which is about guest programs. On this front, we also have a new release. In this case, in the last update, we have some kind of draft-ish spec of the guest program. Now we can say we have a fi- like a… kind of finally complete, spec. Of course, things can change, but the spec is complete, in the sense that the host program is in the spec. And, we also have, 25, tests for testing that the guest program

will reject invalid execution witnesses. This is extremely important to test correctly, because Even on… even if you are running budget blocks, if you get a wrong execution witness, being because you don't get enough information. For example, you don't have all the bycodes that you need for execution, or the NPT proofs of the state accesses are not correctly constructed. The guest program must fail, and… Because it cannot really act on data that cannot really be checked correctly, so this is very important to have good coverage. So, yeah, the release is the same as the execution with those tests. And the strategy for… Running them is the same as I mentioned before, you can run it on…

Your EL working branch, that is targeting the latest PADEV nets. Yeah, that's it for project number 2. I have updates for project number 6, but I can't do them later.

Kevaundray Wedderburn: Perhaps we don't do it numbered and just do number 6, because, the benchmark in Leeds Follows on from just the guest program.

Ignacio Hagiopan: Cool, I'll continue then. So, regarding benchmarks and metrics, we have some interesting new library. This is a lib SST library, written by Lambda class. So this, Rusts… SSC library is mostly constructed to be really performant, focused on CEVMs, but it also has good performance in normal execution. There's a interesting blog post, that goes into more detail, so maybe you are, if you are interested in this topic, you can read this blog post. And also, this library is constructed to be no STD, which is a requirement for for the CGVM standards case programs. I integrated this library into AirGuests, which is our repository, which has the Ethrex and REST guest programs. And I confirmed that this is, this had a 2x speedup in the public input calculation, because the public input is calculating the history root of a structure.

So yeah, in the overall picture, this is about, like, a 5% speedup on the whole block proving time, which is pretty nice. And this also allowed, to comply to being OSTD, for all the dependencies of the guest programs. So, any CKVM that supports running OSTD programs, It would work. So yeah, and on the right, I have some screenshots of the repository, benchmarks, that is comparing to other known SSC libraries out there. So something else, that, I, I did is, like, a refresher of this CG, these 6… emulator profiling tool that the Six team has. This is basically a way to provide guest programs. Without, like, actually proving the blocks, so it's basically kind of an error cost, kind of profiling.

I did this a while ago with a version 0.14 for CISC, and I kind of refreshed it with the latest release and some improvements in the guest programs. And we have seen really good results. This also materializes the ellipse SSC, your library, improvements, and allow us to keep Keep track of, like, where the proven cost is going. So, yeah, this is pretty nice. And finally, I am working on some integration of how to transform all these benchmarks, proving time results from the East benchmarks. Into concrete repricing proposals. And we already have, like, our own dashboards for things, but I thought it was interesting to say Maybe we can use the same methodology that is being used… that is being used for Glamsterdam repricings.

Because at the end of the day, if you use re-execution times of logs, or proving times of logs. The analysis for concluding which is the right repricing for opcos or pre-compiles should be… applicable. So, what I did is I took, Maria's, repository, where she has, all this analysis pipelines to conclude your repricings for from re-execution times, and I kind of adapted it to proving times. and basically… yeah, what I want is to, yeah, stand the shoulders of this world, so… We can reuse, the analysis part of, of… Of what we need to get into the conclusions, because… hopefully we know how to reinvent the wheel on how to conclude new prices from data. So that's kind of the idea, and these reports are automatically generated whenever we have new benchmarking numbers, so the whole idea here is to just go from data to conclusions.

In an automated way, and pretty fast, so we can see how things look like. And yeah, that's all from my side.

Kevaundray Wedderburn: Great. Thanks, Ignacio. Checking to see if there are any questions, while it's happening, Margin, if you wanna… share your screen. I guess some things to note, just as a small summary, is that the witness generation, as I wrote, has gone down by 20x, and this was just from switching from JSON RPC plus JSON to HTTP plus SSD. The 2X in ZISC cost reduction, was mostly from optimizing the DMA in the GPU, and I believe, memcopy. And… Yeah, I believe those were the two big optimizations that we saw. There are no questions, so… Martin, do you want to take it off?

Marcin Bugaj: Yeah. So, can you hear… can you hear me?

Kevaundray Wedderburn: Yeah.

Marcin Bugaj: Yeah, fine. So, today we are doing a quick recap of Project 3, which is CKVM Guest API standardization. All standards are in the ZKVM standards repository. We now have 5 standards accepted. First is RISC-V target triple, which is a minimal 64-bit ISA for proving Ethereum blocks. Second, is the I.O. interface, a portable ZKVM-independent way, to receive private inputs and emit public outputs. Enabling zero, copy support for data transfer. Third is Cryptographic Accelerator C interface, which is basically a C header exposing EVM precompiled equivalent operations through a common C API. And two new standards, were merged since the last

ZKVM breakout call, those are execution termination semantics. Does a standard, That happens… the standard… the standard… it standardizes what happens when a guest program ends. And it says that successful execution may produce valid proof, but failed executions cannot. The next standard is memory layout restrictions. Ckvms are free to define their own memory layouts, and CKVMs must provide linker scripts. So, the standard is basically permissive. It says that, each CKVM is free to define their own memory layout, A quick reminder on what these standards mean in practice for ZKVM vendors. So, many ZKVMs still run on 32 bits, and the migration to 64 bits is expected.

On the Rust side, the Rust target is bare metal, that implies no STD support. So, every guest program has to be compatible with no STD. And if it depends on STD, it won't… it basically won't compile. On the AIO and accelerator side, please make sure that these are part of the SDK. Good news is that, some ZKVMs already implemented partial API conformance for accelerators. It's actually close to completion in at least one of them, and we'd like to see the rest of the KVMs Implement those standards. And finally, Ethereum Foundation can dedicate engineering time to help the KVMs, to help vendors implement those standards, so,

If any support is needed, just reach out. And two new proposals. The first one is Mimo Memory Resources. The problem that it solves is that the memory layout restriction standard, which just was accepted, lets each vendor define their own memory layout, and that's a right call, but it creates a gap, because every vendor can lay out memory however they like. And guest, guest program authors have no idea how much stack and heap they can safely use across all the KVMs. So this proposal closes that gap, mandating a minimum. Every conforming ZKVM must provide at least a certain amount of stack, and at least a certain amount of heap. If a guest program fits within those minimums.

It's guaranteed to run on any conforming implementation. The specific numbers for the stack and heap size aren't in the proposal yet. They are, they are placeholders. We need to profile the most demanding guest programs under, realistic Conditions before we commit to… values. That work is ongoing. The next standard is memory safety guard regions. Right now, the KVMs have no reliable way to catch two of the most common low-level bugs. No pointer dereferences and stack overflows. ZKVMs are bare metal systems, so without operating system or hardware support, and these kind of bugs would lateralize silently. The program corrupts memory and keeps running. Potentially producing a proof of a broken computation.

This proposal fixes that with, two mandatory guard regions. Small zones of memory that are deliberately left unmapped, so any access to them triggers abnormal termination. The first memory region is, It's for, catching null pointer traps. The first 4 kilobytes of the address space are reserved, so any reference immediately causes abnormal termination instead of silently corrupting memory. The second is a stack guard region. Also, 4KB region sitting just below, the stack, so that when the stack overflows, it hits the guard region, and the program terminates. There is one limitation worth mentioning. The stack guard doesn't catch, stack clash. vulnerabilities, that is when a single large allocation skips over the guard… the guard entirely. There is a compiler-level fix for that, but we can't mandate compiler… compiler flags in the Zacavian standard.

They are basically recommended in the standard, so we recommend that guest programs enable those flags when compiling their guest programs. We implementation, we expect, The implementation costs vary, quite a bit across different proof systems. Yeah, that's no data for that yet. Please review the proposal, and leave feedbacks for the last two proposals, which are under review. Yeah, so that's it from my side.

Kevaundray Wedderburn: Great. Thanks, Machin. Checking for questions, tao, if you want to share your screen while… Ruben says, for the accelerators, I proposed… Two of these, maybe we can take that async, Because I think I'd need to review those. I can see your screen, Tyle. But I can't hear you. Oh, mic issues…

Francesco Risitano: Walter, can you hear me now?

Kevaundray Wedderburn: Great, yeah.

Francesco Risitano: Okay, cool.

Kevaundray Wedderburn: But I can't see your screen anymore.

Francesco Risitano: Yeah, I'm gonna reshare that for one moment.

Kevaundray Wedderburn: Okay, cool. While that's happening, Ruben, I think, exposing Catch ActF is probably a good idea, actually. Maybe the same with Shorty 56, Okay, cool, yeah, I can see your screen now.

Francesco Risitano: Cool. Yeah, so the key update is, we've essentially been able to deploy a test network And run it end-to-end with a GPU-based, prover backend. the kind of initial tests that I've run are… more focused on integration as opposed to performance, but the general idea is, you have a single, kind of, property or YAML file which defines the, test network services, so we deploy multiple beacon nodes, multiple validator clients, we have a proof node. And, some additional, kind of, auxiliary services, Grafana, Prometheus, etc. So we've, we've… heavily leveraged, the kind of frameworks that PandaOps provide, and I'll speak about them

shortly, but ultimately, yeah, we have a pretty, kind of, easy-to-use framework now, or at least it's, there's PRs open to, kind of. Provide this functionality, so sometime soon, we should be in a position for, yeah, just single command deployment of, test networks. As I say, I… we can't do it now, but it's across many, kind of, PRs and branches, so, once that's cleaned up, I will, share the… share the commands, and if anyone's interested in using this, then, do reach out, and I probably will share, some… Instructions in due course as well. On that note as well, I did speak with Manu from Prysm, and we have kind of provisionally kind of targeted the tail end of next week for, an initial interop, DevNet, so that would be between both Lighthouse and Prism.

I need to touch base with Manu to see the status of his progress, but, you know, hopefully if progress is going well on his end, then we'll be in a position to, to proceed with that at the end of next week. Moving on to the consensus specs, there's been some updates to the P2P protocol, specifically the introduction of two new message types, the first of which is execution-proof status. And this essentially allows peers to communicate, the latest block that they have been able to validate using execution proofs, such that peers can, kind of strategically Choose, you know, which peer to request and sync proofs from. And secondly is execution proofs by range, which essentially just allows you to request,

Proofs for a specific range of blocks. We've got a more general refactor, and this, Covers a number of, kind of, open… Issues or unresolved, points in the, in the specs. One of the big changes was the proof node API, so ZKBoost, which is essentially the service that the consensus layer uses to generate proofs. It's an external service. The API for that changed, so we had to kind of propagate that through to the consensus specs. And that there's one open question, relating to the execution proof status, which I just, touched upon. The proposal here is to introduce proof types as well, so that, peers can gossip And essentially, like, announce or publish which proof types they support, such that we can kind of dynamically,

You kind of iterate or migrate to new proof types, So, that could potentially be used for bug fixes. That was a proposal by Kev. But yeah, it's still a bit of an open question at the minute, and we haven't concluded on a… on, you know, how we're going to proceed, but there's an open PR for those changes. Then, yeah, we made some changes to Kurtosis, so this is the ETH PandaOps framework that we use to orchestrate deployment of DevNets and testnets. So you essentially just need kind of a container orchestration backend, either Docker or Kubernetes, I believe, are supported. And yeah, you can just, kind of spin up these environments with a single command. Previously, it didn't have support for GPU backends, so we introduced that.

And similarly, in the Ethereum package, which is essentially the layer that sits on top of Kurtosis and defines the shape of the network, we added GPU support for that as well. Then on the Lighthouse side, introduce some… observability, observability features, so essentially just, metrics which are pushed to Grafana, sorry, to Prometheus, and then Grafana consumes them. And, I've provided a link here to the, to the network parameter file, so essentially the DevNet, config, config file. And if anyone's interested, they can use this to spin up a GPU, backed, proven network. And yeah, on top of that, there's just been various different, Lighthouse changes to align with the updated specs, and, yeah, a few optimizations as well.

Yep, that's all from me.

Kevaundray Wedderburn: Thanks, Tom. Just looking for any questions in the chat. Are the lighthouse changes upstreamed already. So currently no, but we're in talks with Lighthouse for upstreaming, these changes. Checking for any over questions… If not, then, Han, do you want to share your screen?

Ladislaus: Oh, there's another question by Bonamas, whether the prism changes the upstreams.

Kevaundray Wedderburn: It's been done by Manu, who is on the Prism team. I believe we're using a Prysm branch, so it's not necessarily in the main Prism Like, the main branch that they use? Cool. Yeah, this is great. A lot of progress, and yeah, I know, Tal, you've been working on it for quite a bit, and pushing a lot, so yeah, this is great. Han, do you want to share your screen?

Han Jian: Yeah, sure. Tao, could you… oh, yeah. Can you see my screen now?

Kevaundray Wedderburn: Yeah.

Han Jian: Okay, so, yeah, I'll get some update on the project file. So, on the ZKVM integration side, we upgrade the disk to 0.16.1, and we see some good performance improvement. And on the proving pipeline observability side, we integrated open telemetry in Array and ZKBoost, so we can see the proof traces from Grafana clearly. And we also added another separate simple dashboard in DKBoost for real-time event and historical proof monitoring, and you can see more details in the latest release in DKBoost. The Grafana dashboard looks like this. You can see, for each block, you can see the trace in each part, how it takes, how much time it takes. And if you don't want to set up the whole stacks, the ZKBoost also provides a single page that shows what's going on internally.

And next, we'll try to integrate the cluster client directly into ZKBoost, if we are going to eventually request the roof creation on the cluster, so we can bypass the array, hub. And also explore the proof cancelling, so if the block proofing takes too long, we can cancel it to avoid the proof request queuing up, and then keep improving the observability. And that's the update for me. Thanks.

Kevaundray Wedderburn: Thanks, Helen. Just checking for any question, are all of these dashboard views provided via Grafana?

Han Jian: Some of them, yes, and the custom one that you just see is… is, like, the… is separated. You don't have to set up the co-funnel to see that.

Kevaundray Wedderburn: Cody, do you want to share your screen while we field for more questions? Okay, cool.

Cody Gunton: Alright. Yeah, so on security… The structure of the slides is almost the same as last time, but with some updates on each. So, regarding RISC-V compliance, I mentioned this Act 4 upgrade, which is a change to the testing infrastructure from the RISC-V community, from RISC-OF to, this Act 4 framework, and having run that, I've found quite a lot of compliance issues and some new bugs, which I have reported, to the various ZKVM teams. And I'll say more about those down the line, but it's very fruitful. This is coming from… from new tests. And also extending some of the testing. To a new extension, which is, to do with misaligned instruction, loading. And…

Oh yeah, and also, the testing is now doing proving of these, test binaries. Like, my monitor is doing this, and not just executing them, and also verifying, and there were some interesting results there as well. We have some grantees working on fuzzing, and they're finding, bugs, which we'll disclose, eventually, but we have good progress there. And, on the topic of speccing, I was speaking with Alex Hicks about the question of whether the sale spec, which you heard mentioned in Derek's presentation, will cover this, these unaligned accesses. And the relevant extension is this one here, which is listed in the ETH Act standards. And, Alex found this active PR and engaged with them there, so it looks like they're working on

I'm giving good spec coverage of this extension imminently, as well as, broadly speaking, Improving some of the… The testing and configuration framework to make it clearer what, You know, what your model spec is covering. When you're doing, testing or formal verification from sale. I also mentioned, this question of what does formal verification give us last time, and I pointed to a paper by Nadeem Kobasi, that found some issues in, formally verified libraries, and just yesterday, another paper came out, by the same author that is now finding some issues with the HACS framework. So I don't have firm conclusions for that, but it feels like a noteworthy development to make people aware of. He does point out some strengths of hacks, but he's also able to push through some buggy code and have it be accepted.

In some… in some sense, so… It's something that we'll want to look at when we, start to adopt formal verification. And I posted these kind of preliminary SNARK specs that I had been working on. The idea just to extract really simple Python implementation of ZIST's approver… And, this time I now have something similar for OpenVM, and the goal here really is to see whether the workflow that I developed for doing this before translates well, and I think it does, based on this experiment with an OpenVM ProverSpec, because it was done with I would say less than half as much effort, both in terms of time… wall time spent. I spend even less of my own personal time prompting

And, I mean, less than half… And in terms of token consumption. So, I think we can produce really simple implementations that are reinforced by strong testing as the beginning of a specification. If we want to go with Python specs. So, that's my update for today.

Kevaundray Wedderburn: Thanks, Cody. Any questions? Let's see… I guess I have one question, Cody. Could you maybe say your thoughts about, this Nadeem Kerbesi… Paper, and yeah, what are your thoughts with respect to formal verification?

Cody Gunton: I… I've only read a bit of the paper, so I don't have much of an impression of it. it seems to point out that there is a complex pipeline that transforms Rust into something functional, which can then be transformed into F-star. I… I don't know if we would be using F-star, I think… we would be using lean. I don't know if the same, I suppose, similar issues apply. Yeah, I don't know. I mean, I don't know if we plan to use hacks or where we plan to use it. For me, the question is… sort of where… You know, on the timelines that we're talking about, say. well, for optional proofs, I don't think we require formal verification,

But maybe as a security requirement for mandatory proofs, we would. And… the question for me is, like, where can we be really, really confident in the correctness of the software based on formal verification? And that has to do with being really explicit about the boundary and assumptions. And making complementary test coverage to that. So, progress is moving really fast. I'm always trying to Pin down exactly what the progress means. And… for now, I don't feel I have a strong confidence in any particular, formal verification, assurances, but I, broadly speaking, am very confident we'll have some, and so it's kind of a conversation with the practitioners, to know where we need to provide complementary efforts.

Kevaundray Wedderburn: Cool. And, Alex Hicks from the snarkification team wants to quickly comment, I think we have, like, one minute.

Alex Hicks: Yeah, so on… on the hacks bit, just because you were… you were asking about it, so I think, it was a really interesting paper, I think, so any extraction from Rust, or any language, C++, Java, whatever, that people commonly use to any proof assistant is always trusted, because the language that you're… Extracting from typically does not have formal semantics, and so you always have an issue in that sense, that the translation has to be trusted. With respect to… what Nadeem found. It's actually quite interesting, because, well, we kind of assume that there can be bugs in these tools, because they're trusted, and the tool chains can sometimes be quite extensive. But it was very nice to actually see concrete instances of such bugs being reported. There are other bugs that we know of, which are just kind of routinely fixed, so with respect to the…

would be the one that we might use and tease as well, on evaluating this, and they've been fixed. But it's possible that there are more. And one approach that we're taking also to deal with this is, obviously, that we've explored other options to verify things, one of them being just writing assembly. EVMASM is an example of this, and then the other is just actually compiling from, specifications in our clib with, what would be a formally verified compiler, and so we're, we're luckily not over-committed, you know, to using these toolchains, because we know there can be bugs, and they also have other limitations, actually, which they don't support all of Rust, because some Rust features are just hard to map into Lean safely.

Let alone someone who do map and have some bugs. So it's, it's nice to see the work that's being done on this. I was quite happy Nadeem worked on this, and, luckily it doesn't affect our plans too much, other than being a good reminder and, to the point, Cody was making, I think, it was a plan from the start of the product to have a final report at the end, for whatever we use to verify production code, to have both an audit of it, and obviously detailed documentation of boundaries. So that is, that's still the plan. And we'll have, obviously, more to say about this, and I'll be very happy to discuss this more in other calls, actually. I think it's quite important.

Kevaundray Wedderburn: Yeah, great. Yeah, thanks, Alex. And, yeah, just on time as well. Yeah, so that's the end of the breakout call. Thanks everyone for joining. I will see you guys in roughly one month.

Ladislaus: Folks.

Transcript adapted from ethereum/pm, CC BY-SA 3.0.