e2e Formal Verification

Transcript

We're rock. >> Yeah. >> Cool. >> Let's go. >> So, uh, yes. So, today I'm going to talk Well, hello. I'm Julian. For those of you who don't know me, I actually I can see that many in the crowd do know me. So, but uh but yes, I lead the uh the formal verification team at uh Nethermind. And uh I guess these days we focus very strongly on ZK related stuff. So both like constraint verification, witness uh gener like witness generator verification as well as like functional correctness but also then the underlying proof systems right so we've been working on the with the archive efforts to formally specify fry which I think hang will be telling you about it a

little bit later today so getting obviously the feedback from all of you guys who uh you know hopefully well there'll be some people who know more about pry than us and we'll be able to fill in some further the generalizations or whatever we'll see uh but yeah as I said today I'm going to be talking about end to end formal verification here specifically of what is required for uh L1 proving right and so I have sort of this uh no I don't I want to go to the next there excellent cool uh so we have here sort of an overview of the trust base which is actually required as part of the uh that will be sort of added in I as part of the L1 improving effort. Um

I mean some of these obviously were sort of already there before and so we won't be talking to and people have been working on sort of this to a large extent for some time. to verifying solidity u and these other things. We'll do a very quick overview of that. Uh but in particular with respect to verification uh these particular solidity and viper don't have actually any formal semantics. So formally verifying the compiler for the moment is not really uh a possibility which is >> potentially an arrow as well. >> Sorry am I?

>> Even by code and risk five execution clients. >> Uh ah yes yes >> cuz you have to lower it to risk five now. Uh yes yes yes yes. Fair fair point actually fair point. So uh the uh yeah so okay I guess I guess that would be an extra arrow that would be added in. Uh I don't know if I'll be able to quickly add that into but actually well anyway >> if you want to take a marker and >> yeah exactly but anyways um but yeah anyways uh but then on the uh what then yeah so the the rest of this though is uh a little bit more interesting and we'll be going into

a little bit more depth there. So obviously we have sort of like implement traditional implementations of execution clients like ref g etc that we may want to >> client >> sorry >> ne >> uh thank you very important very important and the nether >> which compiles to fine now >> uh I' I've heard I've heard people tell me so so there you go but yeah nether mind client and in fact a number of client minor clients that I discovered while searching about this I hadn't previously heard of so so there you There's also Bessu which I didn't know about too much. This is apparently one that's used quite a lot in industrial banking context but yeah I I I uh was sort of yeah interested to learn a bit

more about that. But yes so so obviously we would want to to verify these we'll get into details of how then obviously these will be compiled we'll need to compile from whatever language they're written in and we'll see well I mean those are primarily really like rust go car if you're client client and a number in Java in fact right uh and obviously we would have to so we'll want to verify those we'll want to have a verified compiler to uh risk 5 essentially from that right so really have endto-end verification and then this risk 5 execution client will obviously then everything here is uh I tried to add this in tix and I got all sorts of weird stuff happening so I eventually gave up

there was meant to be a dotted line around this that says uh like risk 5 ZKBM >> right couple questions so first question uh this solidity bubble does that represent like some particular solidity contracts or what does that represent Uh yeah. So I mean it's just that uh when I mean we're just representing here sort of the the flow of dependencies here. Let's say that yes you would write a solidity contract. You would compile this down to EVM bite code right this would be executed on an execution client which would then be uh which for which we then like generate a zk proof inside of a risk five um zkm essentially right that that's sort of like the flow that

this is trying to represent. the sorry >> represents whatever particular solidity contract. >> Sure. Sure. Sure. Exactly. Exactly. And as I said really one of the key issues here is that none of these things have any formal semantics. So, but this is actually kind of fine in the sense that uh you know uh if if you really want to particular with solidity you can compile this down to Ule and then Ule does have a formal semantics which uh we'll we'll talk about a little bit later and uh the Ule to sort of EVM by code pipeline is s is quite is a lot sort of shallower and simpler than obviously going all the way to from solidity to EVM by code. So actually verifying such a compiler is much more plausible than say you know

verifying sort of a viper compiler or something like that. >> Okay. Thank you. So second question is the distinction between a verified compiler and a verifying compiler in play area. >> Uh no not. Yeah. So I'm just talking about a verified compiler as in like one where we verify semantics preservation. So we have the semantics of the language we're compiling from and we have the semantics of the language we're compiling to and we prove that the uh the compiler will sort of preserve this if that makes sense. >> Okay. Sure. Sure. So so I'm just wondering like you know would it suffice to have uh a verifying compiler i.e. one which uh constructs along with the object code that it produces a proof

that it preserved the semantics in that particular instance or do you suppose we need to prove a universally quantified >> state fair I see I think in the case of smart contracts because you're interested in fairly arbitrary smart contracts you probably want the verified compatifying one >> typically when you're interested in a satisfying one you do you're okay with restricting yourself to a subset Okay, fair enough. I see. I see. Interesting. Uh yeah, I didn't actually I didn't quite realize what you meant by a verifying comp. Yeah. So certifying is going to compile. I see. Yeah. Yeah. So now I understand what you mean. Uh yeah, I mean obviously both of them at the end of the day as long as you know they you

have a proof obviously of a verified compiler or you're certifying compiler outputs certificate in both cases you're certain of the semantics preservation. Right. Right. Uh so those are are pretty uh the outcome is equivalent with respect to knowing that the EVM bite code is equivalent to your high level whatever your high level >> right yeah the difference in practice is going to be if you have a verifying compiler it's not a verified compiler then maybe at some point one of your users will run into an issue of like hey I have a perfectly good program that your compiler tells me it can't prove the compilation of >> yeah yeah so I think it's sort of the the best example a certifying compiler you would find in our industry would be um the Cairo compiler but what it it

only was proof for certain programs for which they have pre-written specifications in link for example. >> Yeah. >> And so it's not it were sort of pre-ompiles and not any nothing else. >> Oh because otherwise it would it like it would prove something about the composition of a program but it would have nothing to prove against for most things because there would be no specification against which is very fine as a compile program. Okay. Is is equivalent to um because otherwise if you have a certified compiler for every program you have a verified compiler >> um I so does certified certifying compiler mean something different from verifying compiler >> in my mind they're the same.

>> So for yeah for I mean I I didn't know the term verifying compiler. I know the term certified compiler but I I'm assuming these are equivalent right? But I I mean what we mean here is something that outputs a proof that the high level code is greater or the output. Yeah, we agree on that definition. >> Yeah. Excellent. >> Okay. Excellent. Good. Good. Um cool. So where were we? Ah yes yes yes. Uh yes. So we've were actually were there any other questions before I question. >> Okay. Excellent. Excellent. Yes. So we've covered this bubble. We've talked a little bit about this and then of course we uh basically would end up if we wanted to execute a specific uh solid like a specific contract in a certain

context we would end up basically throwing both of these in and this is the pipeline that we're currently well that the Ethereum Foundation is currently targeting which is both of these would be thrown into the sort of witness generator. As I said all of this is now sort of the risk 5 ZKBN bubble. So these would be end up being thrown into the RIP witness generator for some risk five ZKBM be that you know risk zero sus whatever right uh this would then essentially execute the uh we would then generate essentially a trace of the execution of our execution client right and then this would obviously get uh the the trace would then be passed to the snark prover which would also receive a set of constraints right which is are

meant to verify ly well to these constraints are meant to imply essentially the semantics of the risk five is right uh and then obviously this prover would output a zk proof would be which would be verified on the start the snark verifier which in turn obviously also needs to know the constraint set yeah and so obviously there this itself uh involves a new set of statements that we need to verify so of course we want to know most importantly because this is what enforces a security properties, right? The most important parts of this is that obviously the constraints generated imply the risk five semantics, right? And that that the snark verifier is sound, right? So with those two

properties, we know enough to know that the the system now enforces the security properties that we desire, right? Of course, there are still all sorts of things that can go wrong here that would a which would affect uh the sort of livveness of the system. So for example, the the witness generator could be buggy. It could generate tra invalid risk traces that the constraints wouldn't accept if they were verified, right? Um and then of course we could have uh the snot prover also being buggy and generating for certain inputs proofs that will never be Oh, sorry about that. Yes. Excellent. Uh in fact, we need to finish this talk. So excellent. Um so yeah so so so basically

there within this bubble there are two sets of uh properties that we want to verify that are sort of broadly partitioned into this enforces security properties and this enforces the sort of lightness properties that that we want. Um so yeah so now I'm just going to sort of start going through these uh these things one by one looking first at the verification of uh of these execution clients right uh and then we'll look very quickly at specifically ver verifying constraint systems for uh risk 5 uh well constraint systems generic and then we'll look specifically at constraint systems of risk 5 uh zkms and

then we'll talk very briefly about uh the verification of the underlying proof system. Quang will be talking about this at much more length this afternoon, so I won't go too too much detail. Um, cool. Okay. So, obviously the first thing if we want to verify an execution client that we're going to need is a formal semantics of the VM because we need to know, hey, we need to have a specification for this thing, right? And obviously in the case of a VM the specification is often but not always going to be somewhat complicated. All right. Uh and so these are sort of the the the main EVM u EVM models uh that uh exist. So obviously there's this K there's a KVM model developed by runtime

verification uh which is which is quite interesting. Obviously, it's it's mostly targeted uh at the K verifier and I don't want to like uh like obviously I can't speak for everyone in the room but personally looking at K semantics for me is not they're not very easy to decode a lot of the time right and now obviously there are experts we have uh someone on the team who used to work at runtime who worked on K quite a bit who just looks at this and that understands it but they're not the easiest to uh to understand but actually runtime has recently been working on a K semantics to uh lean extraction and so now they've extracted their KVM semantics into uh into lean and interestingly they have

been working on actually proving equivalence with this uh with the the with our EVM model in that much progress >> uh yes yeah yeah I talked to Juan recently and uh they I I think essentially the issue is that the um the extracted lean is very difficult to work with. Essentially, >> the extracted lean is kind of difficult to work with, but you also actually have a lot of things that you represent differently to them. >> Yes. >> Ranking in fruits and then beyond that like gas safety proofs are basically in a go safety. I see. Yeah. Yeah. Yeah.

Fair enough. Um although uh actually but sorry, why are gas safety proofs in a go? >> Just hard in general. >> Fair enough. And actually same when they're trying to verify the uh EVM interpreted 25 to gas AC proves to nightmare. >> Fair enough. Yeah. Um yeah I mean we're obviously we saw uh so I mean I'll I'll mention a little bit of our experience. So we developed this EVM ule model which is well like all of the others in fact is executable and so we actually executed it again. We ran the execution client tests with it, right? And in fact, it passes 99.99% of them. uh and in fact the the two that it does the two tests it doesn't pass

essentially are tests where we I mean I think we the discussion was essentially that they were buggy tests in the sense that the test itself included an error outcome that wasn't actually uh that we no one was able to give us semantics for like no one knew what this >> we have a lot of new tests now >> excellent wonderful well >> related to ZKVM >> oh really okay fair enough uh so so we should look at obviously doing that but yeah so our EVM And your model though is only uh Cancun compatible. We're hoping to in the not too distant future uh work on upgrading that to also be Petra compatible and >> sorry and for Saka. Yeah, of course. And for Saka, of course. Um and and obviously passing all of these uh these

new tests. But yeah, it was it was actually quite interesting in the sense that uh actually getting most of the semantics right took was very quick without you know without wishing to sound too conc right. The real difficulty in getting all of these tests to pass were was uh twofold as Alex is probably is pointing out in the sense uh getting the gas model to be correct. uh there are a lot of subtleties there some of which are not particularly well documented uh which we ended up having to dig through implementations through the KVM model these sorts of things to be able to actually figure out. Uh so that was quite interesting. And then yes once again actually the uh the execution test

the majority of um clients out there they only require that the their client passes execution test in so far as the faulting tests. It requires a test to still fault but it doesn't actually require the client to match the specific error required in the fault. Right? And so we actually held ourselves to an even higher standard and we required the output of the errors to exactly match the uh the what the Ethereum execution client tests required essentially right and that as I said this was very much an 80/20 problem where getting most of the semantics right was like pretty quick relatively quick uh but then actually

overcoming this getting the tests the test errors to come out perfectly and getting the uh um the gas model uh to come out perfectly was was pretty hard, but we got there eventually. Um, and then there's also the uh some work at KTH on a rock EVM model. Okay. Or not. >> Uh, nothing worth talking about. Yes. >> Uh, yeah. Yeah. I I wasn't I I know there's on Okay. There's ongoing work uh on Oh, yes. Go ahead. >> There's something in as well.

>> Yes. There's a model in but it's not maintained. It was also not that useful. Um, and then there's some there's a partial model in ACL 2 >> which will actually be completed soon and then there's also a partial model in hall 4 uh which may get completed soon. >> Yes, fair enough. Okay. So, I wasn't aware of the the progress on the whole model. So the these ones were the ones that I thought were sort of progressing slash already at uh relatively high specification compliance uh like or test compliance. Uh it seems there are a couple more uh but yeah I mean this uh I

I'll be interested actually to see particularly with ACL 2 how what the outcome will be in terms of what we'll actually be able to verify and work with this. But um but yeah so we need some form of semantics of the EVM. These are some examples. There are a couple more that I missed. Um, and then of course we're going to need uh a model of the language that the underlying execution clients are written in. Right? As we said, well, Ross, Go, C#, and Java are the main ones. Uh, for the moment, out of all of these languages, Rust is really the uh the language with the biggest formal semantics effort, right?

Effort to actually have uh a full full semantics of the language. the other ones I mean the I know there's like a go formal uh thing which seems to have been dead for a number of years now to be honest I don't know if anything is happening there there have been some sort of liken net formal model there has been some formal formal model work on net but pretty older versions not with new versions as far as I've seen and then I know there's a k java thing but it was for like java 1.4 before and I don't think any updates have been done since. So really out of all of these languages uh the easiest to target in terms of actually having a formal model of the underlying language is really uh is really rust right uh and that is

really what this this program this program has been uh targeting and the there are uh really there's a bunch of tools >> why we should say >> okay I will actually live correct this two seconds >> it's fine I don't think they'll be watching this >> uh I It will literally take me uh two seconds. So, okay, my bad. There we go. >> And alias is also wizard. >> Uh >> well, it's surprising that Java doesn't have formal verification because Java has the best >> they're too busy doing homicopy type

series for semantics of Java. Uh, wait. What just happened this? Okay, I think it's randomly skipped to another another slide. Okay, there we go. Cool. There you go. >> Is the other one. >> A How Wait, is that is that how that's spelled? >> A E N E A S. >> Okay. Uh oh, great. A E N >> cuz I think you can also pronounce this anus rather than an I've never known how to pronounce this. Oh, that's on on Wednesday. >> A E N E A S. >> Yeah. Yeah. A >> so a instead of you. There we go.

>> Okay. >> All right. We've got the slides type check now. >> Thank you. Excellent. >> Can I like a concern I have about this? I think um >> like this is flashing like boondoggle to me because uh of this last sentence. Um, so like currently the Rust compiler consists of like about 5 million lines of C++ code and like what about a million lines of R code something like that. >> Sure. >> This this I don't think is feasible to do within the budget of like $20 million.

>> That's completely accurate. Yeah. Yeah. Completely. >> So we saying that we need it, not >> Yeah. Yeah. >> Well, I'm going to say that we don't need it. But I think what is a more viable approach would be to create execution clients in such a way that we thought about how we're going to prove them correct from the beginning and constructed. >> So this is actually the idea was to rock one which is actually pass through. >> Yeah. >> Oh, so you're going to extract the rest to Is that the idea?

>> No, no, no. writing there's a client being written in rock which will be compiled down to this side. >> Okay. Okay. >> So no nothing involved other than rock and >> yeah so so that's an alternative means that so I mean I think >> I I I think that the focus on ROSS was particularly in the context of the DRA certified Rust compiler project which is now dead. >> Uh so uh >> sorry. >> Yeah. Yeah. So, so >> right. But it's not dead because it wasn't working. They were actually making good progress on just you know the president came in and did >> Yeah. Yeah. So this is a was a political decision not a technical one.

I think so I mean there is a point which is of course you know should we try to think of okay do we want to do you know formally verified general purpose compilers for languages like Rust which are going to be obviously huge tasks that would involve many years for many many people or are we okay doing you know perhaps verified compilers which are highly domain specific because we are dealing with mostly domain specific code for most things. Yeah, you could just use like a simpler language like n maybe could be a good choice. >> But it's the is the idea saying that you know I spend the next year of my life basically becoming a n evangelist so that every >> well I also

>> I don't think you have to like sell like outside people on them. You could just be like here we're gonna we're going to make an execution client and then and the verify used >> right right >> that's the issue >> well there is already a verified C compiler or you have to >> yeah but using console is not what I said I'd rather have bugs and use concept >> it's proprietary is that like allowed within the constraints of the >> it would be an issue >> I see like so the licensing is one issue. Um I'm not even sure how it would work because also like um like we have to give clients that people

can build from source. So everyone who wants to do that would have to pay a license. >> So that that doesn't work >> which is a huge it um the other thing you'll say is that it uses C99. So you would have to go and you're not even running kind of you know very modern C code >> and then your execution client is in C. I talked with a guy, interviewed a guy who worked for uh like the Department of Defense uh like uh proving correct C code that is used to launch missiles and things of that nature. Um and and and what they were able to accomplish was like um you know, I want to prove this program terminates. I want to prove this program doesn't run out of memory. Like it was very like laborious work with

kind of rudimentary results. >> Yeah. And these are multi-year projects for one program. >> I can actually I can give you a number. So there was a discussion at some point is do we want to get CKZG formally verified right and so the issue here is that people are using CKG instead of KG or RKG but anyway people are using CKG and the EF said you can use it for the next I guess there's two more years they can do this before they finally move on to Russ and go um there was a proposal to do preliminary work to formally verify this and the proposal to do preliminary work to formally verify audience with a million noise.

>> Well, well, sure. Like when you when you when you have C code, like it could buffer overrun. It could, you know, it could do all kinds of crazy stuff that um you have to rule out with ad hoc proofs in each instance, whereas if you just write a programming language that has more protections built in like all, right? Like you could you could for example write in a language where all programs are guaranteed to terminate and then you have to prove every single program terminates. You just know that >> the thing is but once you want to optimize you still use some safe r for instance >> and then also the trade-off is that okay thing is the unpaid is clearly eliminated and you have tools for me >> so we discussed with uh the z the z team

and they have issue with rust due to um uh building rust uh the genetic code size the fact that when you try to merge everything into um a static library. you have symbol uh conflicts and the thing is CDG44 is uh a very restricted set of C there is no uh array accesses for there is no ber there is no um almost zero memory allocation uh because the blast uh library side uh can be run on TE and on T you have you don't have MAC so everything is stack based

>> and on the KG side you have some mal but it's very very restricted >> um and also blast has a formal implementation in GA crypto >> so >> but crypto is unusable I >> I wasn't fan of of what they did so GA was when I said they're like million dollars for like preliminary work that was >> okay >> and it was and they said then you're locked into crypto which means you're locked into GA >> so they're very good but there's a locking effect which is not always.

>> Okay. But um uh like for me C is uh it's fine if as uh for cryptography because uh to write cryptography code you need to restrict yourself uh to avoid um a lots of memoration etc. So you don't run that much into those uh for overflow etc. >> Well, but in each instance, right, every time you do an array indexing, you would have to prove that you didn't overflow the buffer or no, >> but you don't have arrays in blast for example.

you do have rules in GCG but the thing so once again you do have to get back like what I was saying because we are doing in many cases something that is highly domain specific you can write domain specific compilers which are then much easier to verify whether you're using C or something else right >> yeah in any case like um a ranch check it's like it's the very first thing anyone that does uh SMT solver or for verification implements because it's easy to add um invariant uh or pre um precondition post condition that accesses are within the range.

>> So for me that's that's not a blocker. Uh yeah and even on the rest side those accesses are not proven at compile time you have a runtime error. >> That's true >> but we're also using rust because people use rust right. Yes, like the rust preexists, you know, this whole ide verify this through S&T software that our accesses are uh can be compiled away without the exception.

>> Okay, nice. Um where was I? Um yeah, so debatable whether this is the right way to go clearly. Um >> but I think it is in the sense that currently the code that we want to perform the verifying pages in Rust >> that's correct >> is the way to go. If you want to rewrite verify as a n >> then we'll look at >> right. >> Yeah. Um and and of course actually like a lot of the tooling I was talking about in the previous side particularly the uh snark provers are also written in rust.

So there is a sort of like although yes once again without the rust compiler being verified. Yes. But um but yeah, so so but but I mean part of the the advantage of going for ROSS tooling is that it has a sort of like a multiple effect where it can be used for the execution client. It can >> the other thing is as far as languages like those which on the side go, Rust is by far the easiest to verify because you get a lot of like insight from the types which will preserve price. So when you're extracting Russian via hacks, the extraction is done from tier and so you preserve a lot of type information which is extremely useful when you're trying to do proofs.

>> Yeah. >> Yeah. Exactly. Um cool. >> So just just one more question assuming you know you get to the point where you have a R. Yes. Like >> presumably that would be valid for that particular version that they work. So like when a new rest version is released like how much work would one expect to have to do with the >> depends on the release. Um I think so one it depends on the release two it actually depends on the methods by which it is verified. So if you look at traditional let's say old school compiler verification and this is the reason that com only works for C99. Uh you you have manual proofs for each compiler pass right? So if you add a new compiler pass you have to do another

proof. Back in the day, I talked to someone who did her PhD thesis on this one like formally verifying a type of pass would be a paper in a top conference and that was like you know six plus months of work for one person. So this is unreusable to maintain and so that's why if you want to use concert you're doing C99 and and that's it. Now we now have much better methods to automate these proofs compared to when people doing concert which is like 2008 you know in that era. Um if you look at some of the work that's being done for example on verification of ML uh by someone who is in Cambridge actually who we're going to see on Tuesday um they have proofs which are pretty close to automated

um so it's much easier to verify these things they also benefit from ML having these starts which do this bigger so things are like nicer representations um so it's possible that if you find a way to automate most of the proofs you can get maintenance which is trackable within not within okay push button and everything is fixed but within for a new release it's like less than a month or something to like verify reverify the compiler considering the obviously the manpower that go into this so like with rust and other aspect is you know AWS are huge on rust replication they're doing this effort to formally verify the entire rust you know sedd um a lot of other companies are obviously interested in rust Google has been you know also running along this like rerunning in

rust just cuts down bugs by off. Um so so this is the reason there's also all of these tools for Rust verification and this is this tool is non-exhaustive. There are like 10 other ones. >> Yeah. Yeah. >> Um >> these are >> so so that that's also where that was also why DARPA had this interest in a Rust compiler which is that it is heavily used across industry and that there are you know if Microsoft did Google wants a verified Rust compiler they will have the engineers to maintain it. Um which is so so that's I think like it's not something to ignore. M >> it's not what's blocking it from happening.

>> Well, there's also this effort by the uh Department of Defense to uh >> to >> rewrite safe languages, rewrite C into >> well well they standardized on ADA um as their safe language and and and now they're trying to replace ADA with Rust. Um but yeah, so this is quite cool actually related to so the current status of this is that actually now when people want to verify C++ or C code they actually translate it to Rust and then they verify the Rust and then they have a uh proven translation from Rust to C to get back into C. Oh, interesting.

>> That that's how back when trying to verify C++ is rocking sitting back and there's a couple very cool papers about this actually. Um that is the that's quite >> they use spark right >> they use spark for verification because spark ad spark is um a subset of a uh and spark is their um formal verified pilot back end and then spark is trying to add some borrow checking uh is they were trying to do that three years ago uh as well to because perform lots of stuff but not memory.

>> So So maybe maybe the approach is um like just make a a new Rust compiler that is way simpler than the reference one. >> So I I would I would be down a Rust compiler for cryptography basically >> and just say okay just you can use this like you know whatever functional subset of Rust or something like this which also happens to work well with an um and then and then Well, I can say m but you know um and then and then you just kind of lower down you know mir or something which is tractable as a compiler tool chain to verify um and I think this is why every time you mention you hear me mention mir

it's basically because if I have to pick a compiler framework for me verify like it will be >> um because there's just tooling around to do this and a lot of people interested in doing What's the um for execution of lean code is there a decent story of interoperability as in if you wanted to pursue a story of like write the execution client in lean and accelerate special you know bottlenecks of the execution client computation in something that's faster is that feasible >> uh yes so I mean the the performance of extracted lean code is not really uh >> I think the idea is you would write a

back end to something that's optimized and then you would limit yourself to a subset of lean which also because I mean some some reasons like lean is slow depending on like your integer type >> so so yeah exactly exactly so the so so leans like basic representations of certain types can be quite inefficient but like for example the natural numbers their like default representation is like piano style Right. Uh but but obviously lean has the capability of actually substituting a lot of the type representations with optimized uh sort of uh representation. So for example, NATS in uh runtime compile in like compiled lean typically get substituted

by like some GMP representation essentially right. Um but >> I mean you could like we we have ML data structures in lead >> which are actually quite fast. So if you could just write a mapping from your lean code to those data structures then you would be straight through an M pipeline and you could fast. >> Yes. >> The question there actually that's interesting is whether limiting yourself to types which are Freddy to this would hurt then the proof ergonomics of proving your lean program. >> Yeah.

>> Yeah. >> And but that might be circumvented by running a bunch of intermediary levels >> to ultimately. >> Yeah. Uh >> so we're back to >> Yes. uh as always. Uh cool. So yes. Okay. So this is Ross compile. Sorry, I've completely lost the flow of what I was going for, but that's that's okay. >> Yeah, I told you compilers would come up. >> Yeah. Yeah, you you you did say so. You did say so. Um but yeah, uh anyways, we'll see. We'll really see, I guess, what happens with this uh in in the future. We may end up as you said maybe targeting a subset of Rust maybe using some other language but ideally you know we would want uh sort of a verified some sort of verified Rust compiler at least

for a subset of the language although as Alex pointed out the maintainability of these things is still to some extent an open question and when when talking about this I do want to I always there's always one story that actually involves Ilia who sedated right there that I I always like to say in context which is that I I think it's important not to underestimate how much um the uh like how much automation has come into proof assistance in the last couple of years and how much that has sped up and already knows now what story I'm going to talk about but and how much that has sped up like the the the rate at which the speed at which we can write proofs right so uh two and a half years ago we were working with risk zero to verify

some of their uh core or constraint system and at the time obviously it's a risk five uh it's a constraint that's trying to like model risk 5 semantics and so we needed a lot of theorems about bit vectors essentially and at the time lean had a definition of bit vectors in like batteries I think it was right it wasn't was it even in math lab it was >> oh it was it was in math okay so so lean had a uh model of bit vectors in math but it had essentially no associated theorem Right. Uh and basically Ilia spent about 3 months of his life writing a bit library in lean. Uh which took a tremendous amount of time. Well 3 months

and and on top of that one also has to account for the nosuous sanity. So you know so it it was a pretty big impact but uh and then the the really sad thing is that like two or three versions of lean later they changed the definition of bitex which completely destroyed all of these proofs once again. But now the definition of bit vexus is fixed. And on top of this there are a bunch of like tactics that are specifically designed for proving things about bit vectors right that uh use a variety of techniques extracted from different areas including stat solving and these sorts of things. Um that means that the vast majority of proofs that IA wrote are now a single line right are

either already in in math lib or a single line right which is just dv decide bit vector decide right and so I think it's so so basically in those two years it took >> and bid vectors is carried on improving >> yes yeah exactly exactly so so there's there's continuous work on this and the thing is so basically in those two years it's gone from like it took him three months to write this. So probably he could have gotten most of his proof done in a day now, right? Or less, right? So uh so I think it's it's important to understand that like uh there have been in the past the number of certified compiler efforts. Oh damn, sorry. Um they obviously uh were extremely tough, took years, had limited results, uh

difficulty with like really having to limit yourself in terms of the compiler, optimize compiler classes, these sorts of things. But this hasn't been done in a bit of time and I actually would be very curious to see it done again just because the improvement in in automation has increased so much in this time but I heavily suspect that you know it will be for some definition of easier easier than it was in the past. So there you go. Cool. Um okay before we move on from execution >> please please go ahead. um what one of the interesting uh things I've heard, I don't know if it's true or not, but um I've heard that um some of the uh people in finance like big banks um are

formally verifying some of their software and they're also formally verifying the hardware that they're running on. >> Correct. >> Sure. Yeah. Okay. Yes. So, uh that seems like a necessary step in order to really know that the computations that are actually happening are the right ones. >> The hardware part you mean specifically? >> Well, yeah. So, so software as well because I mean so Jane Street is a prime example but a lot of them basically do care about even basic things like safety because if markets are volatile and they're getting potentially random streams of data as inputs they want programs that are not going to you know

up. >> Yeah. Um but but part of it too actually I know I know when I was hiring one of the mechanics I had actually uh is going to work on FPJ replication for some uh headphones like high quality or something >> right so so like you you so in order to have you know this this verified compiler you would need uh a formal semantics yes for the source language but also for the target language >> which would be risk five in this case. Um >> so so um and and and then are there risk five chips that their circuitry has been proven to implement the semantics of risk five?

>> There is >> yes >> risk five >> there is formification of risk five hardware as a sync um where there are people who use these chips >> for something isn't it? Yeah, risk five hardware is not you like real risk five hardware is not used very frequently of course in practice but but actually the the models that do exist I mean a lot as you can imagine uh form of verification is more popular even more popular in hardware in the hardware industry than it is >> and also better >> and better yeah I mean the there's sort of a >> so if you just UK >> yes yes so so I there are reasons that it's sort of in quotes uh better one of them is that I mean hardware is

fundamentally a finite state machine, right? And so in in some senses it's kind of easier to reason about, right? Um >> the other thing as well as hardware when when we verifying the hardware circuits, the model is quite different because for example for them an under constrained circuit is basically actually a positive sync. >> Yes. Um >> ah okay. What sorry why is that? Uh if you if your thing is if you have a if you if your socket is under constraints but you still have something that works then you're basically handling something more general than your socket and so it's fine. I see. Okay. Interesting.

Interesting. Um but yeah for the obvious reasons though obviously this is very popular in the hardware industry which is that uh you know if they make mistakes on this a hardware record is much more expensive than patch. And then actually another quite important aspect of the hardware side of things is also that a lot of hardware verification happens kind of as a black box where all these hardware people have like whatever else they're using they've been using for like 20 plus years and a lot of the things are not form verification tools but they do have you know like SM backends and things like this and so it means you can give all of these things to hardware engineers who don't care or know about form verification and for verification happens nonetheless whereas software is hugely different because of

software you give people some language sketchy compiler and nothing happens. Um so so there are a lot of differences in the kind of hardware and software replication models. uh and people used to seeing that software verification would be solved if you we're in Cambridge there was um Mike Gordon who was one of the early people who software replication switched from software replication to hardware verification in the 80s because he saw software replication was about to be solved >> and then instead he saw hardware for verification and software verification is still a nightmare. Um, so there there's a lot of like interesting things going on in hardware, but there are a few actual parallels between hardware and software in that sense. The tooling is very different. The problem space is

very different. Um, and the um the size of the space that you're looking at is very very different. >> Okay. Okay. So presumably the execution clients that participate in the network will probably not all be running on verified hardware, but that could be okay if if enough of them are running on verified hardware. >> Well, everything is run on verified hardware like production. >> If you have if you have an X186 CPU, it's a Y64. It's fully verified.

>> Yeah. >> Oh, well that's good news. >> That is good news. the one which is not fully >> verified. Um so yeah but I but to be clear we are actually what we're doing with respect to the actual EVM client is what we're checking is that when you're interpreting the EVM B code to risk 5 that risk five B code executes the same uh produces the same outputs on the same inputs as would a formal semantics of EVM and we're doing this because we're just looking at the risk five assemblies independent of the source language for the client it's just tedious because you do produce about risk five assembly just a bit.

So then you can write your client in in name or ra something else and it's you just have to be able to compile to >> so would the execution clients then be required to run on risk 5? >> Well they will >> they will because they're going to be running inside a risk 5 ZKVM. So all all ZKVMs that are participating no all execution clients that want to participate in L1 proving need to be able to be compiled to S5 somewhere right which the nethermind client now can adding a quick ad in there. So is this making sense?

>> Okay. Okay. So the execution clients for the purposes of this discussion are running on a z. >> Yes. Yes they are. Right. Right. Well, I mean, yeah, no, no one is I mean, risk five hardware hardly I mean, it exists, but it hardly exists, right? It's not very easy to to get. So, we're not assuming that people are going to have risk five machines to be running this uh in any kind of way. But yeah, no it will be running on the CKVM and uh then of course actually the correctness of the VM itself is sort of as we said looking at the uh the the oh no sorry looking at previous diagram right the correctness of the VM itself is sort of in the witness generation right and like

the trace that it it executes but even if that's not correct as long as the constraints are verified against formal risk 5 semantics That's kind of fine because uh well the prover won't accept it right if it's correct and if and well if it's not certainly if we verify at least the verifier uh it it will also uh reject such an incorrect proof of such an incorrect trace if the proof was wrong shall we say too if I'm making sense here >> uh yeah I believe so >> excellent believe sorry to to get another question when I was I was totally I'm just going to mention for the I thought that I was planning to be about like 5 minutes in by the time I got past this.

>> I I told him yesterday he's like, "Oh, what am I doing?" I was like, "Talk about refiners." >> Yeah. >> No, I just want to ask about that. >> Sure, please. >> Running an execution on like >> I suppose I mean that makes sense on some level, but like >> Well, you mean it is a strict requirement. You have to commit to it. >> Yeah. Yeah, that but like normally the the client would be like a long running and the ZKP is going to produce a proof at the end of the program execution. >> Well, what's usually done is you run uh your client for one block. Yeah.

>> Ah okay. So >> so it runs it runs it runs execution for a full block and then it like certifies the proof certifies execution for the whole the state update that corresponds to the execution. Does that make sense? I just assume like the normal client that would be running%. >> Oh yeah, sure. But here we just run it for to verify the state diff for a single block. Oh yeah, makes sense. >> Yeah. >> Uh okay, cool. Uh okay. Uh so now I wanted to go on a little bit to the verification of the constraint systems and whippers generators, right? And so the first thing that I wanted to talk about is the fact that well there are basically two ways of writing these constraint systems

and witness generators right which have somewhat different profiles with respect to uh for like what what it means to formally verify them and what can be formally verified about the algorithm right so there is obviously the ED the ZKDSL direction like clock3 and that um obviously embeds uh ZKDSL into an existing language typically well in both of these cases rust but there also things like McKn which embeds into Go and these sorts of things right um and there obviously there are a bunch of pros so obviously you can uh use the existing compiler tool chain and all of these sorts of things you can use a bunch you probably have a bunch of

libraries in your host language that you can also use all of these positive things however this uh advantage has a bunch of downsides when it comes to uh form verification, right? So firstly, you basically have sort of two uh options in terms of verifying some uh like constraint set in the CKDSL uh which is either you need to have a full model of the host language, right? Or you need to instrument the DSKDSL and this is the direction that my team has gone for a bunch of things at least for the moment. So for example for plunky 3 and Halo 2 we have instrumented versions of the ZKDSLs where like the functions

that generate extra constraints are also uh have basically an instrumentation that also that keeps track of these and then at the end can uh extract these into the ascension right and so obviously that that has some uh some impact there which is obviously for the in the instrumentation action, we need to trust the correctness of the instrumentation, right? So, we could have made a mistake when writing the the the instrumentation that extracts us into lean. Uh often without being able to reason about the full language, we're not really going to be able to uh reason about the witness generator, right? And so, uh and I'll talk a bit about some

options where you can uh in a second. And then of course uh it's also the case that you kind of have to trust that the uh the constraints are deterministically generated. I don't mean the constraints are deterministic in the sense of like a deterministic CK circuit. I mean that every run of the constraint generator will always generate the same constraint set. Right? uh because otherwise uh otherwise obviously you would be formally verifying potentially against a uh well against a constraint set that may not be used for every single run in practice right so that's that's an extra like dependency that you have to add in the case of instrumentations which is suboptimal and the uh the zkdsl and then

you have the DSL route where you actually use a specific domain like you actually create your own domain specific language for this like circen right in the risk zero case and these basically have kind of the opposite pros and cons profile right in that uh well you have to develop your own tool chain you need to write all of your own libraries from scratch etc right um however it's easier to extract because well typically your DSL will have uh you know uh will be relatively simple have well- definfined a well- definfined semantics etc uh and so it's fairly easy to write a full model of the syntax and a uh a sort of like full model of the underlying

semantics and in fact so we worked uh with ris zero to create a model of zer and in fact we've embed so this is actually to be specific zenv v1 uh that we worked with now there's zerenv3 which hopefully we'll be working on at some point in the not too distant future um but uh but yeah so essentially there we in fact this is A very cool feature of Pini specifically which is it has this sort of elaboration step before the um before like it has a first elaboration step in the which allows you basically which can be arbitrarily programmed at uh within the language right within

within the language itself and so you can basically actually arbitrarily embed syntaxes into and in fact what we have uh for zer you can actually just basically copy and paste Zen code into lean and it just knows what that means, right? It will automatically pass that into an A and you'll have an A that you can listen about. That's also the case for our U model, right? So you can actually copy and paste U with the right libraries included. You can copy and paste into lean and it will just automatically pass that into an A for you, right? Um and then you we have like as I said like a full model of uh the semantics of this and also in in the case specifically not so much of circum but at least in the case of Zurgen it describes both the

witness generator and the constraints generator within the same DSL and so we can basically get constraint we can get models of both of these things and then we're able to prove soundness and completeness of the constraint system against the witness generator and vice versa right uh which obviously primarily like primarily obviously this is primarily useful for proving alignment properties because as we said just knowing that your constraint set implies your specification is enough for safety properties but uh you know uh but but certainly if you want to know if you want to have livveness you probably want to know that your constraint um your sorry your witness generator is always going to generate witnesses that satisfy your constraint system right um cool

yeah I I think I think those are most of the points here. Any questions on this? Just one regarding right system like for example three with the that you have that you use in to construct your air. >> Yeah. Um like in principle you can have like a symbolic right. >> Yes. Oh we do in fact that's how this works. Yeah that is exactly I was about to say if you have like you can use that symbolic that is exactly how this works. So uh you can go on to yeah so if you go on to we have a plank3 fork on the nethermind uh e github and you can go and look at this and yeah we have some some simple demos working for the moment

um one obviously also issue with the zkdsls which you've just reminded me of thank you is that every single person makes every single company makes their own flavor of the zkdsls unfortunately so we've tried to write these in such a way as to be as uh generic as possible. So that and and in fact we've now worked with two companies, two different ZKVMs that use their own PL3 flavors and we were able to adapt their in-house pl3 flavor to to extract within the space of a day or two essentially right so we've written it in a way that's generic enough and really actually kind of serves uh you know as you said using uh

sort of like symbolic builders and these sorts of things that mean that really to to a large extent And we can basically do almost drop and replacements. We also have like a um a rust uh trait that sort of describes uh what do you call it um interactions with uh with permutation and lookup arguments, right? So you can write these sort of in in an abstract way so that we can extract those. And then obviously this allows us to then extract multiple airs and reason about their interactions. And this is very good in terms of modular reasoning right because now a lot of CKDMs particularly have uh an architecture where there are uh essentially there there is typically like a decoder which decodes a given

instruction fetches some basic information and then really like references a bunch of other airs that really do the do the computation right essentially so this is a very common architecture in zkm these days and so by allowing us to extract on an airbyair basis exist like this and then being able to extract implementation or look up constraints between these different errors, we're then able to actually verify things in a very modular way essentially, right? Um okay. Uh yes. Okay. So giving giving some ideas of sort of real world uh extractions that exist out there, right? I mentioned a couple. So we've developed this uh halva and I actually am missing one the ray labs extraction anyways.

Yes. Yeah. Okay. So I'm missing one in this list as far as I'm aware possibly more but but yeah so we have an extraction from Halo 2 into lean set3 into lean R1 CS constraints into lean right uh and then we have as we said uh generic like air models permutation lookup log up models as well as sets of relevant theorems and lemas as well as this uh finite field extraction and proof reconstruction that allows us to then easily well hopefully easily write proofs about this the resulting extracting the extracted constraint system into uh intellf extraction and proof reconstruction just uh for context is there is an SS SMT

theory called like a an SMT theory for finite field reasoning which basically uses group uh groupness solving essentially through CBC with a CBC 5 SMT solver it calls something called cocoa and we have actually written our own uh fork of C of of this of CBC5 that allows us to actually extract this rubler these grouper reductions and then so basically we're actually able to fully reconstruct these proofs into uh into the right so that we don't even have to actually trust the group of basis solver a couple of issues with this for the moment is uh well uh in the future uh CBC5 itself is going to add proof extraction for the uh

finite field SMT theorem which is going which is going to be good because essentially lean already has uh lean SMT which is allows you for the uh the existing uh like theories that allow for like proof extraction on SMT solvers. It already allows you to reconstruct these proofs in essentially but it CBC5 doesn't yet extract the finite field theory. So but when this is the case we'll be able to fully integrate our work into the existing EN SMT and then you can have queries over sort of multiple theories right so you can have queries that range over constraints on vi fields but also natural numbers you know ADTS these sorts of things right which are permitted by this proof

extraction so that will become much more powerful in the future because in a sense we kind of got a little bit overtaken here because there's a new tactic in being called well relatively it's a few months old But this came up while we were working on this called grind which itself actually has a built-in grub basis solver right that already does a lot of this but uh one of the key advantages is obviously cocoa is a highly optimized C++ implementation of ribbon basis solving so we can actually solve some slightly larger examples than grind is able to so grind will time out uh on a lot of these examples where we won't although because we have an external call to CBC5 And the tactic is still not highly optimized. There's some

initial very like high fixed costs to creating another thread and running CBC 5 which means that for shorter queries grind can be considerably faster. uh but we're we're working on improving that in the future right and as I said certainly once this gets u embedded into the broader SMT uh like uh the the broad like we we have like foolproof extraction for fine field into the whole like SMT lib uh like um proof calculus essentially will then be able the power of this tactic will be increased quite uh quite a lot cool so as I said we have uh these sort of extraction into this one is a little bit special in that as I said zurgen here is

a zkdsl rather than a zksl. So we can extract both the constraint system and the um what do you call it uh and the the witness generator in lean and so we were able to actually prove uh what do you call it uh soundness and completeness of the these witness generators against the constraint system and vice versa. Um and in fact actually so in our our work on risk zero v1 we formally verified I think a bunch of small circuits but most importantly once again I hard work on bid vectors paid off because we were able to fully formally verify the instruction component of risk zero uh against the spec that we extracted at the time from

uh the sort of like natural language specification of risk 5. Great. Um now of course in lean uh thanks to uh the hard work of uh Gwa and Lindy Labs uh as well as Cambridge I think also possibly >> a lot of Cambridge as well actually. >> Okay. Thanks to the efforts of a bunch of people. We now have a uh sale to lean extraction which is complete enough to uh support the uh the full extraction of the risk five the formal risk 5 sales spec which is sort of the meant to be the epistemological source in in the sense that it's the official one.

>> Yeah, it's it's basically a risk five process if risk 5 CPU does not satisfy the spec what is not a risk 5 CPU. This is what this is the meaning of risk life right and we have the extraction of that into um uh into lean which obviously we didn't have uh at the time uh then there are a bunch of other tools so there are two two tools one of which I didn't actually mention here so apologies to relapse there if you're watching without mention it uh but then yes pyus by dice which extracts a bunch of different things so they have a gark a circom and all cs extractor into uh SMT lab specifically the finite field theory right uh and and in fact I mean this is

actually a bit of an oversimplification because as I understand it there are a bunch of closed source simplifications and these sorts of things which are actually applied to this before it t&mt solver right >> the magic is not actually >> yeah yeah exactly so there there's a there's a bunch of magic in this era that is not shown because I don't even know what that magic is uh they don't tell me so they have They're in IR and they do >> Yeah. A bunch of stuff. >> Yes. Yes. Well, and we're going to we're going to mention LTK uh yeah in uh in a second. Uh and then the other one that uh is not mentioned here is that Ray Labs has an extractor from Gnok into uh into E2, right? Um but yeah so one question that's also comes up very

naturally here is okay so you've got a bunch of extractors and it seems that no like the ZKDSL like ZKD new ZKDSLS and ZKDSLs are still coming out right and there's no necessarily reason to believe that hey any of these are in any way fixed so is it the case that >> well none of the most of these are not used right like half I guess it's not that useful anymore so Yeah. Yeah. Not and then Zen also not because it can't converge it. >> Yes. Yeah. Yeah. So, so basically these three are dead essentially, right? Uh Surveyor Surveyor Surveyor was a is a like a toy tool that I wrote over like a weekend.

So, so yeah, Survey Surveyor is very >> But I think beyond that there are also even other extractions by other teams, you know, to stuff. So, GAW have >> Yes. Yeah. G also have their own like the >> Yeah. Yeah. Yeah. Okay, I'm I'm just going to add as a what do you call it? A qualifier for all of this. I don't guarantee that any lists in this form are complete anyway because there are lots of people working on >> and if you're watching in the future >> Yes. If you're watching Exactly. >> Definitely not complete. >> Exactly. Exactly. Um but the the point that I'm trying that I was trying to make here is of course there are uh as I said just evidenced by the fact that a bunch of these things are essentially already dead, right? Um the uh the you might say you might think hey isn't

there some space here for um uh what to put an intermediate representation of some form that can both be extracted into a bunch of different uh different constraint systems right different arithmetizations but also uh allow us to actually reason in a unified way on this right so one one like very nice way of doing this might be of taking like writing extractions from all of these into some intermediate representation which then has a bunch of extractions into as I said different arithmetizations but then also has uh extractions towards a uh bunch of formal verification tools like extractions to lean other proof systems and um and SMT solvers right and in fact

this is something that once again uh I think that very dice has been working on and this is actually the IR into video representation that Pyus uses called LTK. So uh >> so they had to persus used to have its own IR. >> Oh okay. But now but as I understand >> now it also runs on LCK. >> Oh okay. >> They had their own IR previously. >> Oh I see. >> And obviously some of the good made it into LLCK. So in some sense part of LLCK >> it's inspired.

>> Yeah. Yeah. Yeah. Of course. So, so there is this LLC KIR which has now been open sourced and PUAS also extra like is able to support this and extract it into uh what you call it SMT lib to be able to uh verify some simple properties about it but >> actually on the SMT but even better than that the plan is actually that there is an SMT MN dialect and so the idea is actually to take these the MML DX we have and then lower those to the SMT dialects really that because get much easier to add new dialect and still have that lowering to SMT.

>> Yes. >> Sm that. Yeah. Okay. That that's that makes sense. >> Which is another Tobias bailing me out with paper type of situation. >> There you go. >> Um yeah. Okay. So, so anyways, there is this this uh this sort of like uh universal ZKIR in quotes that uh that is being developed and that there is also a lean model of this being developed as I understand right I think >> yes started two weeks ago this week >> there okay there you go so so very nice has started working on the lean model of this IO and >> Cambridge got mainly >> okay there you go as you can see Alex has a lot more of these details than I do so because really I'm trying to give a talk here on a uh what do you call it

on a a program a research program which is actually led by Alex so so there you go and yeah I'm actually kind of >> there's a lot of things happening >> there's a lot of things happening and I'm trying to resume as best as I can and there are certain moving parts which I'm not fully which Alex has more familiarity with me clearly uh than me clearly but yes anyways try my best in the context um but yeah so anyways this CKR exists it's going to be hooked up to so there'll be a formal model in lean uh there'll be extra and test and tib and that means that uh and then also they're going to be developing extractions into all sorts of arithmetizations but of course it's this is going to be an ongoing pro process and that well we've participated a little bit in uh the like

discussions on what should be on the design of LTK because in particular when we were working on our plunky 3 extraction so LTK came up during started being a thing during this process and uh we were thinking of basically just extracting from point 23 into LCK and then basically just building the LCK. Sorry, >> it was not ready. >> Yeah, it turned shock. So uh and then extracting energy came to lean and but it turned out that it was it was not ready and in particular plunky 3 uses very common a lot of flavors of plunky 3 uses uses log up arguments and you know log up arguments specifically allow you to set like the you have to set the

exact multiplicity of all the values in your shared bus and these sorts of things and there was just no way of modeling that in um in L in LTK at the time. And now I believe there is then >> I think it was merged last week. They they merged they merged something last week and actually they wanted feedback about if it was enough for you. >> Okay. Well, >> we can look at that in the breaking. >> Excellent. Well, we'll get back to them in the coming days. So, there you go. Thank you for the update, too. So, so there you go. Uh so, yeah. So, until recently, this this um this ZKR Yeah. was missing some features that we kind of needed for what we wanted to do with Maki 3. So, so we ended up actually just going directly to the lean extraction as

we sort of originally intended, >> right? Um but so one of the interesting points actually about the leaning structures which might be relevant because we have some compiler people in the room is that something that hurts proonomics a lot is that at the moment when we do these in extractions most of them are kind of done in and naive is maybe not the right word but basically you read off the constraints from the ASC and then you unfold all of these constraints in which lacks a lot of structure compared to the way that the circuit is written and this is visible when you try to write the circuit in itself. where you have a lot of structure in my proofs. And so an interesting question this relates to the compiler aspect is what would be the best way to actually get you know structured constraints from

if not the as something else from the compiler to be able to extract it into the >> okay um so uh I have like kind of a out ofthebox suggestion about this. Um I'm not convinced that it's good but I'll throw it out there. Um so uh the thought is that rather than um having manually constructed the constraint system in something like clonky3 or circom we take um a description of the semantics of risk five you know maybe maybe this one that exists that was mentioned or or maybe a different one in some DSL that's more amenable to this use case um and

and we generate from that the constraints um in a way that uh you know it's a it's an automated way that um you know is is creating the structure that that Alex is referring to. Um and uh so this would be virtually rich circuit something like the using a life spec. >> Yeah. So, so I've done I've done some R&D on this type of approach before. Um, I found >> so we we were planning on well not to miss five initially but we do for the like the event one of the milestones is to basically do a minimal VF and so that will give us a taste of what it looks

like. >> Um, so so so I did I did some R&D on this type of approach. which I found a subset of predicate logic that's equivalent in strength to Halo 2 circuits and I made a compiler which can go from predicate logic to Halo 2 circuits. Um and uh like so so so so the advantage of an approach like that uh well one of the advantages anyway is that um you uh no longer have the problem of um verifying in an ad hoc way that the constraint system is correct.

You just sort of need to uh you know look at the predicate you express and make sure that it's the right predicate. um and then and then you get that the circuit is right out of um the circuit compiler being right. I think the the major uh issue with this approach for something like this use case of the ZKBM is that the circuit that you get um is uh probably not going to be you know as as optimized and parsimmonious as a manually generated circuit. And so you know it could take like 10 years of R&D or something like that to actually get to the point where you have like uh you

know a circuit with the type of efficiency that is required. >> Yeah. So actually so this is a good question. So have you seen the parasetization first or the logic paper? >> Well yeah I actually my my research predates that it's a little more than that >> but I think so I'll use that because at least it's kind of public as a reference. So there's this paper which shows you basically come up with an arithmetization first of the logic and the um the encoding is like fairly simple where obviously you have like a nice encoding from you know like and to you know a constraint.

>> Um now the thing is like you say it's like it's clear that you can have an efficient encoding of the basic building blocks of your predicates into constraints. M >> it's unclear that obviously when you're formulating your predicates as a whole you don't end up with something that's too big which leads to more constraints that you would want even if the encoding is kind of a priority efficient but the interesting question is that actually there is quite a bit of research going on with the people who do sorting and what not into reducing the size of predicates and so it seems like there's an alternative optimization approach which is to just throw S&P sources at this and say like you know here's what I have just reduce the size of this whilst proving along the way that you know it's logically equivalent Um and that would

be interesting to explore. But actually I'm curious if did you have your work working over a specific finance field or arbitrary finance fields or something? Because obviously the first the first paper was written by um this guy >> Murdoch. >> Yeah. Yeah. Murdoch. Do I actually know him? He lives in Edinburgh. Um >> yes. He also wrote the first like what was it? Skyro compiler I remember like >> Oh yeah like >> yeah it was a what proof system to Cairo Idris >> Idris yes it was to actually I' actually met him >> quite a character actually >> I I actually had met him long before I realized that he was writing this paper and we only realized because we bumped

into each other in B in June >> oh like oh like you happen to also work in >> I see >> um but anyway the thing is like in his paper he's targeting like the constraints over like the rational numbers or something >> like he's obly not a cryptographer just like I have people doing conraints like paper about this >> and so I think there is actually like potentially quite a bit to explore in that the other interesting aspect we looked a bit into this was then like >> um when you're trying to write obviously your circuits for a program let's say then obviously you have to translate your program to that logic and that requires some amount of expertise >> um yeah I I think like when you're trying to prove a program correct uh you

would write you know maybe the predicate that you're trying to express to this program and then you have the problem of proving uh that that program implements that predicate. So um yeah it does require particular expertise but um I think it's beneficial because you know you save an entire staff of having the proven program correct >> um I think and I actually you know implemented in software um this this this uh translation method from predicate logic to circuits um and so you know I found that um like uh there there are like some major issues that you're ly to run into when doing something like that generally around

like the polomials just turning out to be way too large. Um and uh I think I think >> the number of constraints at least when I did some examples by hand for the like first of the logic the degree of constraints was okay just the number of constraints we get is the same >> right you could either have too high degree or too many constraints um I and and and you know I I made some progress on addressing that but not all the progress that needs to be made I think I think the other issue with like Gab's work in specific as applied to this is that uh it only does first order logic and I don't think that's >> so you should be able to do higher order logic pretty much the same way. Well,

yeah, I did I did do a version of second order logic. Um, and that does work. Uh, I don't think that it would work very well with polomials as the target. Um, but I did it with Halo 2 circuits as a target and and that worked fine because there's actually, you know, I actually uh was able to show an equivalence um at least in my own mind that showed an equivalence between the version of second order logic that I arithmetized and Halo 2 circuits. Um so I think there's something natural there.

>> Yeah, that that makes a lot of sense. That makes a lot of sense. Um and in in a sense actually uh as part of the uh risk zero tool we were kind of doing something a little bit related in the sense that we were whenever we had our extracted arithmetization we had basically like a simplification a simp set that we would always apply to it which would automatically simplify it into a much smaller set of uh constraints right which is which obviously is not not doesn't have the generality but also does uh well >> can you say more about this because otherwise surely they were going to upstream having that smaller set of constraints. Uh yes. Yeah. So the thing

is it wasn't only the the thing is so it wasn't only like constraint simplification itself. It was also actually like moving it a little bit into the uh ambient like lean lean terms. Right? So it was in a sense a little bit of the opposite and that it was taking a constraint system and trying to reconstruct from it something that looked more uh more logical, right? Essentially. And so for example like the the example that always comes to mind is the like is zero example which uh in like as a zk circuit is uh you know relatively straightforward in that basically you say hey well either you assert that either this thing has an

inverse in which case it's uh non zero uh or or it doesn't in which case it's zero right sort of how this works and with the constraint set that we extracted by running the sim set that we had on it. We basically actually just got an if uh we basically just got like a very simple branching on like hey does this thing have an inverse and from there we were very easily able to say well like from lean we know that like the final field theory tells us that something has an inverse if only if it's zero and then like basically with like two rewrites we got the spec we wanted. Uh so it's a little bit kind of like the opposite of that a little bit.

>> That's very interesting. >> Yeah. >> Um but I mean there wasn't too much there wasn't really any secret source to this. It was just uh you know some I I'm not going to say that we did this in any way in a systematized way. It was literally like as we went along we found that these adding this to the sim set was useful and so it was developed in a very like ad hoc manner but it worked out working fairly well in practice and this is uh open source so you can have a look at it yourself if you so desire. uh that that that could work like take like for example the the constraints for risk zero and and show you know through a series of simplification steps that it implies the predet and only if with the so we actually had

that so we actually had a really interesting simplification engine which I hadn't planned to talk about and we're now over time for not only what I was meant to say but the whole session but I'm going to say I'm going to say it anyway so if anyone wants has to leave feel free to do so. >> Uh as I always say when my talk's over so but I won't continue talking. So so there you go. Um but essentially we uh with the extracted zer we did a bunch of interesting things where firstly we would actually because when we ended up extracting sometimes fairly large circuits into lean right and then trying to simplify them we ended up in it with some issues where we would get timeouts because the turns generated would be so huge right so the first thing that we

did is we did basically like some circuit partitioning where we would cut up the constraint systems automatically ally into subsets of them, right? We would also do reorderings of the damn it of the generated zeren to minimize the lifetime of every variable, right? So we would basically like move uh like the creation of like a new value as far forward in the uh as possible, right? And we would use its law we would push its last use as far back as possible. And then we would even we would even uh insert explicit uh annotations into an extension of Zurgen that told the uh underlying semantics you're not going to

need this anymore, right? And so this basically like minimally like created a an underlying state that was minimally complicated. And in fact this essentially complic like compilation step. It was a very simple compilation but this compilation step was a certifying compilation step and that it would simultaneously generate a proof that the original zer is symmetrically equivalent to the simplified one right at that point in time >> by like are you able to like treat them as like a sub type or something >> uh to treat the to treat what as a sub type sorry >> uh when you're refactoring them can you treat them as like is there some fancy way to like treat them as a sub type I don't think that's what you're doing I'm

Not not really. We could I >> then you would automatically carry your fruit. >> Yeah. Yeah. Yeah. You could we didn't in practice we didn't right. So we just generated a separate lema that uh just said that would just show that hey the semantics of these two things are equivalent right uh and this was completely automatically generated and then for each one of these blocks we would then basically just unfold the semantics apply our so we would generate the constraints or the witness generator that was equivalent to this. we would apply our simplification set and then we would get and then we would like sequence all of the specs for each one of the subcircuits we created and then reimplify again right and as I said with this we were able to for a bunch of like

fairly non-trivial circuits get things that were generated completely automatically generate a proven specific like weakest precondition style specification that was already very close to the desired spec >> okay so we have like two directions we to sort of accomplish the same thing. I guess like the the pro of going from the circuit to the stack is that you uh you don't have to like try to make a compiler which is sophisticated enough to generate an efficient circuit. >> And the con of that approach would be that um there could just be like immense computational complexity.

>> Yes. >> Yeah. Yeah. Exactly. >> Um cool. Okay. So, uh, since we're massively over time, I'm just going to say one more thing and then I'm going to let Kang do all of the proof as I'm talking later. >> Time over time. No. >> Yeah. >> Yeah. >> So, it's not we're not horribly time. >> We're not horribly, but we are over time. Yeah. >> But uh I I'm uh so what I'm going to do is I'm going to speak a little bit about our work on risk 5 ver verification of risk 5 specifically circuits specifically just a tiny bit and then as I said the proof system stuff I will let Juan talk about mostly this afternoon if that's I mean I think you were going to do that anyways right so so uh so I

think this is this is kind of fine um but yeah so uh to to give you some interesting sort of outcomes from all of this work right because I've talked about some relatively simple stuff we've done in the past with risk zero but uh with uh particularly so there are are two risk 5 ZKVMs one of which unfortunately I can't name but some people in the name were in the yeah NDA is very soon going to stop being a thing we're making the announcement in a couple of days but I I I'm not allowed still to mention the name uh but we've worked with two big risk 5 KVMs one of which is sinct uh and we have uh basically verified almost well no in their case we

verified all of the ALU chip right uh against the formal risk 5 semantics so the basically we have the constraints for the ALU chip 100% are like 100% proven against the formal risk 5 semantics and then for the other uh ZKVM that I cannot name but definitely exists this is not in my imagination uh we've Yeah, >> sorry. >> Exactly. Yes. Exactly. Exactly. Um, but uh we've worked with another ZKBM where we've gone even deeper. We have verified all of the ALU uh against the former risk five semantics and we've also fully

verified the memory argument assuming assuming basically the semantics assuming the semantics of the lookup argument that otherwise it essentially uh and so so that is virtually now 100 like that one is virtually 100% verified other than the the take up and put down code as well as the system calls. Uh but we're looking at also doing that in the future. But yeah, basically >> the system calls are probably going to change. >> The system calls are and obviously also frequent pass sorry pre that's important. >> Yes. Yes. But it's both the way that the frequ these parts of the system are kind of like not stable enough really to be verified at this point in time anyways.

But essentially there is a ZKVM there which is out there that shall not be named uh that is has basically almost reached the uh the standard required in terms of constraint verification for on proofing. So one company who will be announced in the next couple of days has reached that standard already. Uh cool and I think that will I will finally let let you all be free and uh go and have some food and these sorts of things and you'll hear some very interesting things from Quang this afternoon. >> And we're on this room again. >> Sorry. And we're in this room again. Okay. Excellent. Perfect. Thank you so much for listening and uh thank you all for watching.

This ended up being a very interactive session. Uh as I said, >> this is the goal. >> Yeah. Yeah. Sure. I was I was expecting all of it like to talk for like 20 25 minutes and then have interactive questions, but it ended up not being like that. But actually this was very I think this was actually a more interesting outcome. So thank you all so much for your participation.