PQ Ethereum Workshop - Day 2 Recap

Transcript

Okay, congratulations to everyone who made it till the end of the second day. Uh we're going to do some uh debriefs. I think it's been a long day. We've had three tracks uh all all working in parallel. So, first what I'll do is invite the DevNet track lead O to give us a summary of some of the learnings today. Yeah. Uh so for de I think it's a very exciting day. Um so we we try to get um clean ream and seam talking together. Um so far we are able to get it to talk but it's not talking the same language

exactly. Uh but yeah so we discovered you know networking issues, concept issues and so on and so on. We're getting to the consensus issues for between team and team. Um and still for clean and seam is on the gossip sub um hand shaking. Um so hopefully we're are going to continue um over tonight after dinner as well trying to get it up. Uh finger crossed we should get them up PQ dropped them at zero without speaking uh hopefully tonight. Um and then what else then? Oh sorry bindings.

>> Oh bindings. Yeah. So we we discussed a lot about bindings. Um I I probably can't summarize part if anyone could chime in on the bindings. Maybe some lessons first. >> Um um yeah so we've been actually just uh discussing how how to simplify the life of people not having to program their code base in Rust. Uh there's been several solutions that were proposed. I was actually trying some of them this afternoon. Um I think in the short term it's pretty clear that we're going to stick with the Rust libraries external R libraries. There was a good uh

suggestion by mam to uh to use n to to generate C so that for example go and zinc could implement that. So that's something I'm quite interested in. So we'll see about this and otherwise there was an idea by Morgan to use op copy. So I did try that that was that seems to be working pretty well. Um but yeah like I think over at least I am not convinced that in the long term we we can just deal with with ROS libraries but yeah lots of lots of needs to to explore and reach a definitive conclusion.

So if I understood correctly, we have this um reference implementation in Rust of the the Lin and the aggregation and the different clients and also the different languages have to import this library. And the main pain point is the compilation because there's a lot of overhead. >> Yeah, it's there's overhead but there are also incompatibilities between each compiler that is like Rust evolves a lot. So you have different flavors of the language that can conflict. >> We have we Z haven't run into that yet, but it's going to happen soon.

>> Okay, great. And when I when I met up um earlier today um to the the net room, it was a completely different vibe to the rest where everyone was on their computer hacking which is great. And yeah, hopefully we can have a demo uh tomorrow, but no pressure. Okay. >> And there's uh the third part of today. Uh we talked about networking with Rahu there. >> Yeah. >> So we specifically went over some uh erasia coded broadcast techniques that we can apply for local aggregations and global aggregations to disseminate the output and the the result of those aggregations. We specifically applied

some of the parameter space that have been discovering today from Emil and others in terms of aggregate sizes and um and other things. Um, we also kind of like went over what the uh signature like what the authentication the chunk authentication scheme would look like and if that in any way kind of like relates to the key genen of the protocol or if we need another identity that is kind of like okay for it to be ephemereral because it's just going to be used at the networking layer for transient data. Um, we also kind of like sculpt what a prototype for DevNet one.

Um, and that involves synthetic synthesizing aggregates because we don't actually have the mechanics to produce them yet. Um, and just like putting them through the network and like testing them with different subnet arrangements and different validator accounts and so on. So yeah, that's anything else that I'm missing out. >> Um, there's some action items for tomorrow. I think um my personal worry is about delivery risk uh now that we have uh stuff to do for Pico signatures and then we have like the networking eraser coding that we could also potentially experiment as well for the net one. Um so I think there's kind of like unknowns on how much of the PQC that we can actually do right now. Is it

just the the signing and verification and just basically concatenate all the signatures or are we doing some sort of like one layer aggregation there or or or yeah others and I guess like the the other important part is how much of the say the aggregation part if we are going to do that for the signature aggregation um how how far is that for example like if it's only say you know 10% of what we are trying to achieve and then for networking it seems like it could be I don't know 50% I don't know what what measurement it is you know um should we actually go for networking rather than aggregation something like that so I think that's where the the kind of inter

between say networking and post quantum comes tomorrow >> probably need to prioritize that at some point um cool thank you next up we have the formal verification >> uh yesterday we had three sessions today which covers actually all our sessions for the week. Uh so I think the first session was about encoding and some of the work that has done on formalizing scientists in lean already. I think in the end we actually focused more on the fact that he was doing it with an agent which was very interesting to see. So I think that was probably discussed more than the specifics of the encoding formalization. Uh but it was quite interesting to see. So hopefully if he

publishes it we can we can try and evaluate that agent or that model on on other things and comparing to other agent workflows that exist which will be very nice to see. Uh and then we had two longer sessions in the afternoon. So the first one was on end to end for verification for CK was on the L1 which Julian talked a bit about because done has covered a large stack of a large part of the stack with their work on this given they have quite a large and very competent team. Uh I think in the end the discussion mainly devolved in discussions around compilers in particular uh and around choices of languages and how many they are for verification and how to perhaps move towards a formally verified compilation stack or something of that kind. Uh I

don't think we necessarily settled the question. Um perhaps we should just use him, who knows? But um but but it was quite interesting to get obviously some opinion and feedback from people who actually work with compilers um and to hear a bit more a bit more about that. And then we covered a few kind of other aspects and that led quite naturally into your second afternoon workshop which was on Art where Kong and a bit of Judah gave us a bit of a walk through of the current state of Arl. In particular, we looked at some basic examples in coding Siri and some more interesting and relevant examples in terms of cryptography by looking at both the interactive oracle reduction frameworks that we have in the course been working

hard on as well as the forest specification that we now have uh which was merged in I guess last this week. >> This week I think pressed the merge version on Thursday um before before coming here. uh and I think we were quite happy to get some eyes on this from cryptographers. It's obviously a big thank you to Jacoma uh and Orick and and Nico in particular and Benedict uh you're able to give some interesting feedback and comments about some of the work there. Uh and hopefully we can continue to engage with the wider community to make sure that obviously what we're doing is going in the right direction in terms of uh choices and definitions and choices of how to formalize things. uh as well as hopefy being able to show off uh nice resources

that you know with sprite we're very close to having something that says this construction is sound and this construction is an actual program to choice which will be a very exciting milestone which will probably come very soon >> do you foresee a world where you know maybe in two three years where academics will write proofs >> I find it very interesting that math are doing it and computer scientists are not >> and um for the the encoding for verification do you think that's something that could be done in art as well?

>> Uh I think we could do a bit I mean it uses uh for oracles it uses vcbio which is what we also use in art so we're already sharing the kind of oracle back end um whereas it fits in art in terms of seam because art right now is just for snarks I think is maybe more relevant question that it might not fit in terms of scene and could just be in a library would be alongside of it. But if that's something we'll probably just discuss. >> Is Julia? >> Yeah. >> Yeah.

>> Do you have any words to share? >> Uh I mean I No, I think Alex pretty much covered everything other than like I mean I can add a couple more details like >> Yes. Yeah. But still responding that very important Yeah, I I mean in a little more detail, we did specifically talk about the verification of risk 5 CKBMs, the work by like risk 5 spec extraction and work we've already done with a bunch of DKBMs to get them verified against a small risk five spec. But yeah, >> yeah, once we can do risk five, we can eventually do VM.

>> Sorry, once we can do >> once we can handle the complexity of risk, we can also handle that of >> uh Yes. Yes. Yeah. And and in fact, we have one VM which is virtually and verified against spec. So, >> open the second. >> Yeah. >> Okay. What's the name of that? >> Secret. >> Yeah. He he can tell he can tell you privately. We have an NDA, but we will be announcing this in a few days. So, >> interesting. Thank you. And next up, we have the theory group with >> Yeah. So, we have two cool sessions today. The first one was uh in morning the toy problem session. Uh so Albert gave a great talk about the toy problem

and his latest results. >> I guess the summary is that the toy problem conjecture is wrong and >> yeah maybe we should not trust too much in it because it's wrongly in >> Right. Right. So I guess the the conclusion of it is that yeah it's wrong and not particularly helpful because it's also interactive and we like it's part of the interactive protocol but we care about the security of the non-interactive schemes. Um and yeah so maybe to understand attacks it's a good thing to look at these simplified settings but to understand concrete security level uh of snarks and starks

it's not uh the right thing to look at >> and I I believe that almost immediately after the session Angus found that there's a better attack and it's even more wrong than >> right this morning >> yeah for the interactive case so >> okay quite a long discussion. Okay. Yeah. And then in the afternoon we had a long mutual correlated agreement session with Aon and uh they both gave great talks. Uh Alon's talk was more about like what is correlated agreement? what is the current state-of-the-art there was a great table on the slides uh to to see that and uh talk was about sort of what is the common theme of of proofs

for correlated agreement and I think that was also quite quite helpful for us >> anything to add >> so for in the mutual credit agreement spends a whole hour just through the statement the definition of mutual product >> right and we discussed what is is this a good way of writing it down and I guess that's that's sort of useful discussion for the proximity price >> and also if I could lower down because I mean it take more than one hour to >> okay great um and finally we have the implementation group with

So like today we had two session. The first one was about NBM and we went through uh the white paper wrote by by uh with different stuff. So we learned about like the the memory models the different op codes that are currently in the DM. Uh the way we we proof like the final execution, the way we are organizing the code a bit, the compiler also the read only memory that we have and a bunch of question how to design minimal ZKVM the choice that we made compared to to the other ones the recursion that we have to deal with.

So all of this question reading like page by page the the lin VM paper that can be found directly as a PDF in the repo. So that was quite a useful session and then we had like a second session about memory argument. But this was like aki presenting like um a new way to handle like minimal CVM the way that they took at no with like Merkel tree um in order to represent like to abstract the language and a nice way to represent the old code. has nodes of the maker tree and then to compile the program

with quite an elegant way before going into like a final table. Uh yeah, so another way to see minimal ZKVM and before we started this post quantum workshop we had a dedicated lean VM day on October 3rd where we have about seven hours of content on lean VM. So if you want to the extended version of the one hour recording, it will be made available uh on YouTube. Um great. So that that pretty much uh wraps up the day. Uh we don't have any planned dinner, so you're free to just stay around here. We don't need to vacate the

room, I believe. Um and you're free to just break out in small groups for dinner. Thank you so much.