Ovidiu Damian - Bringing all the programming languages to Ethereum with Formal Semantics

GMGM everyone. Um, I'm glad to be here. I am Damian from Pi Squared and what I want to show you is basically how we at Pi Squared are developing a way to upgrade Ethereum so that it supports an infinite amount of programming languages. And in order to get to the point, uh, what we're trying to solve by doing all this is one of the biggest issues in web 3, which is fragmentation. Liquidity is fragmented on different chains.

Uh, um, e ecosystems are fragmented in the sense that you can't interact directly with different ecosystems because they're on different chains. Sometimes you need different wallets and so on. Up until recently, you couldn't use the same wallet or at least the same mainstream wallet uh for example for Ethereum and Solana and so on. Uh we have assets on different chains. They have different uh UXs and so on.

So basically uh this is one of the main things that we're trying to solve and part of this fragmentation is the fragmentation of developers. What I mean by that is solidity is solely used to code on Ethereum and it's very very specific and there's very few uh solidity developers in this world and basically the way in which we're solving this is by bringing verifiability and I'm I'm going to have a word on this u as an asterisk for for the end but basically the way in which we're bringing verifiability to uh in order to solve web free fragmentation in this case is through having verifiable programming languages that can be run using EVM. Our solution is first of all universal in the sense that it supports all programming languages and uh any program that's executed in a known programming language. The only thing you need in order to do that is um is to have the definition of set uh programming language in a in a as a set of mathematical rules. And I'm going to get to how we do that in a in a few minutes.

Second of all, we bring verifiability and proof mechanisms because if you have a definition of set programming language, you are then easily able to create a compiler on the spot. sorry to skip the compiler and create an exe an executor on the spot and to have proof mechanism that that code was executed correctly according to the mathematical definition of it. Now we also have uh we also have uh a specific consensus mechanism which helps us keep everything secure from this point of view but that's not as interesting as the parts above for now. So I'm introducing to you the pi squared verifiability stack which is composed of three different parts that work together in order to bring this to Ethereum and not only we have the verifiable language machine which is basically for now a modified EVM client that allows you to support multiple programming languages. Basically, think about programming languages that can be uploaded onchain kind of like a smart contract.

You upload your language on chain, then anybody that knows the address of that programming language can code in that language. We have the verifiable settlement layer which is just a few days ago launched in a devet that you can try out. If you go to our uh Twitter page which will be uh in the final slide you'll be able to basically see uh a form in which you'll be able to sign up to try out our uh VSSL DevNet. And we also have the consensus protocol which basically makes sure we have uh we have the u we have the protocol consensus part correct and uh unattackable and basically uh allows us to keep what we call a weak consensus protocol working and secure. Now what does each part of this mean for the VLM?

The the main um the main issue solved by the VLM is the fact that now anybody can be a web 3 developer. You don't need to know Solidity specifically or Rust or any other programming language that's very fancy and only for web 3. You could code smart contracts in Python, TypeScript, whatever. For VSSL, it means that you can have the correct execution of any app in any language verified instantly and you can have different chains communicating through the VSSL as a let's say as a layer zero in order to get information for that for uh to use to use those programs on the on the VLM on their protocols. We also have the universal consensus which allows us to quickly settle the transactions quickly and process billions of transactions because uh we have lots of parallelization in uh in our system.

Now in terms of market opportunity if we look at some studies that have been done in late 2023 2024 not by us but by uh specific by uh specific uh agencies that do specifically this we have solidity uh 8,865 developers that are constantly developing in solidity in the whole world which is a very very low number. To think that almost all smart contracts on Ethereum have been written by such a low amount of people is crazy. And the thing that we're initially going to solve is the fact that we'll enable other web 3 developers to come in, which is 26k more. and we'll will enable web two developers to become web 3 developers with C, Python, Rust and so on. And finally, by 2030 with AI integration, we'll have prompt engineers being able to safely create smart contracts in this way as well.

So basically our goal is to expand who can code on Ethereum from about 10k people or less to 100 million or more. And this has been a way for us to shift the way we think about the way we think about uh the problem in the sense that instead of thinking why we need verifiability, we simply shifted we we're simply by giving this system and allowing such easy verifiability, we're shifting the question to why not yet. And what we mean by this is that security is something that's often overlooked by people until they get hacked or until something goes wrong in the system. And this is why we offer quick verifiability in our system. And I'll get to the technicals of that soon.

But until then, let's see what exactly is the issue for which the issue because of which Ethereum only allows EVM. So for any programming language that you want to run currently for example EVM you need an interpreter, a compiler, a symbolic exeutor, a model checker, a program verifier and so on to check that everything is executed correctly and to actually be able to execute it which is very complicated. Basically for any tool you create you need to create all these from scratch and that's taking lots of time. You then have different opinions from different developers that say hey I would I think uh this should be done differently. You also have bugs that you have to solve and it gets very complicated very quick.

This means that in theory to allow coding of Rust and EVM on on the same chain, the chain would pretty much need to offer all these uh by default. Well, this is exactly what we're changing to say so in the sense that by using formal semantics instead of having this these implemented for all languages we simply get them through this K framework. Now why do we call it the secret sauce? It is because the K framework which is a framework that uh was created by was created and is open sourced by NASA and one of the main contributors is our CEO Grior Roshu and he created while he was working at NASA is this is basically an a framework that allows one to define a programming language as a allows one to define a programming language as a set of mathematical rules. And basically the cool part about it is that if you have a programming language written in K, then you can automatically on the spot generate an interpreter for it, a compiler, a symbolic executor, a model checker, a program verifier.

Which means that if you can exit, if you can create all of these on the spot, you don't need to create systems that are able to run everything and have them available in a deterministic way. Now, in order to explain what's here and how this works, I'll show you how a simple programming language is defined in in uh K. So this might look complicated in the beginning, but I promise it's not. And I'll tell you why. Because this is usually what u university students learn to you to create as a first programming language after one uh lab.

Basically, if you take the formal semantics course at uh at university and you learn about K, this is one of the first things you learn how to write. This is a simple syntax in which you explain okay if you have uh if you have a plus something happens, if you have a minus something happens, you have different l rules in which okay uh integer plus integer does something and so on. Basically coming up with this allows you to create a very simple uh programming language and this is just after two or three hours of learning about the K framework. So obviously sorry for the short breaks but I caught a cold and it's horrible. Um so basically how this helps is that okay you can create your own programming language here fine but after you get better at it you're able to mathematically define already existing programming languages such as C Python Java and what's fun is that once you have created the once you have created the definition of set programming language you can then actually use uh you can actually use the mathematical definition to check whether already existing compilers are for example actually working fine.

Um, one of our friend companies to say so runtime verification has created a mathematical definition of C uh of C++ sorry and then they have ran some tests using their mathematical definition against the GCC compiler which in case you don't know GC compiler is like the very well-known uh very well-maintained C++ compiler that's basically used worldwide. And they actually found bugs inside the compiler using this mathematical definition. And they actually got they actually got the maintainers of GC compiler to um to change some things that were not working as they should in the compiler thanks to uh the thanks to the mathematical definition in K of C++. Now um now how it works is that once you have such uh once you have um this mathematical definition on our chain that uh on the VLM what you can do is you can encode this and once you have encoded it you can basically put the definition of the programming language on the chain and it will receive an address kind of like a smart contract and anybody that wants to use that programming language further can basically when they deploy a normal smart contract they they basically specify where's the address of the programming language in which that smart contract is written and thus the node knows where to look for the definition of the language that the contract is using when the when it's trying to execute execute the code and when that happens well you can basically have any node running any sort of programming language for which the definition is available on chain and let's say that at some point you realize that there's something wrong with some type of definition you can simply add a version two or so on of the of the definition and it will work it everybody can then switch to that version. Now to go further into uh more principles and how this can be used on Ethereum.

So basically we have already talked about how this can be done on our very own chain which would be called the VLM. But it should be noted that in an ideal world, an ideal scenario, we would get val Ethereum validators to agree to let's say uh switch from the classical EVM they have to an EVM that has K inside of it to run uh multiple programming languages. We have already done that ourselves. Basically we have modified uh we have modified the ref and made it so it uses K for executing EVM and we have made a chain that's available on our platform as a demo. We have made a a small chain that supports um that currently supports EVM Rust.

Um so it's EVM Rust. It's simple. Simple being uh this language here. It also supports solidity directly like you don't compile it to EVM you can execute solid directly. And it also supports uh WASAM.

Basically, you can either run RAS directly or compile it to WASOM and run it on the same chain and everything everything works just fine. Uh the main drawback for now was the fact that it was a bit slower than the normal EVM execution engine. But considering it was just a proof of concept, the results were extremely promising. Now, but this is not an ideal world. What if we can't convince all validators or to do that?

If we can do that, then what we're going to do is the uh what we're going to do is the following. We're going to have our own chain in which basically you can run everything using multiple programming languages and so on. And different chains could work through our chain as a relayer. For example, I'm on Ethereum and I send a transaction to a smart contract asking, hey, what's the result of executing 2 plus2 in Python? Then a relayer listens to that transaction and once the transaction is actually received on the Ethereum chain, it executes on our chain the actual Python code, then sends the result back so it is available on Ethereum.

This is a more simple solution so that validators uh don't need to necessarily cooperate. It's just uh relay the execution and the result can be available back and not just that the result can be available but we can besides the fact that we can have a result available we can have a mathematical proof that that result is correct. But because that mathematical proof can be huge, what we're doing is that we're encapsulating that mathematical proof in a zero knowledge proof that can be then checked with any uh ZK uh technology. So let's look over the whole work workflow again to make sure that everybody understands. So we have a programming language by using K we can basically generate an interpreter for set programming language and with then we have that interpreter that's going to be used as long as we want.

That program is interpreted by the the following interpreter and it will uh execute code and generate the math proof set for set code and then we have using ZK VM and other any type of ZK uh any type of ZK tech we can have uh we can have a ZK proof that can be then checked. So this is the general workflow. Uh the beauty of it is that you don't have to understand it all. You can just enjoy multiple programming languages on the same chain. And uh do I still have how how much time do I have?

I I've run out. Oh, okay. Oh, almost. So, okay. So, very quick uh we had faster than expected prog uh progress on this in the sense that for February 24, what we wanted is to do the following here.

basically be able to in some cases be faster than GEF and we were able to do that and uh we basically overachieved in February and since then we have launched for another product our devet that you can check out but the point is we're making huge progress on this and you will soon be able to check multiple programming languages on the same chain uh in a public environment but until then you can basically uh check out our demos uh on chain and that has been shortly all from me from me. Um of course I'll take questions but before that if you want to follow pi squared onx uh you can you can scan that and basically also there you have a form to go and check out our devnet and here's also our developer portal where we can you can also check the the demo for the multiple programming languages on the same chain. Thank you so much, Damian. Really going into it now. I I don't know how how to code at all.

I actually had to ask a friend for help on this one for questions for you for later. But first, I want to ask everybody here, do you have any questions for Damian today? Ah, perfect. Thank you. Yeah, I guess it's a general question.

What was the biggest challenge you guys had while working on this project? Sorry. So I would say the main challenge is the following. Um you have multiple programming languages like Python, Java and so on. And each of them have their own ways of inputting of getting inputs and spitting out outputs.

So the most complicated things was to create an environment which only allows these languages to function and give inputs and outputs that are specifically for example AI encoded for EVM to actually use them and to make sure that these environment is restricted so it can't u it can break any system and part of the system and it can it can't uh go into uh parts of the system that it shouldn't access. I would say that's the most uh complicated part of it all. Thank you.

So um if I got it right, what's the purpose of the proof of the proof? So you have let's say a smart contract written in uh rust and then the the sense of the proof of a proof is to actually prove that the execution of the smart contract is correct or is there a way you can specify what's the you know the correct execution based on on a on a specific semantic?

Yes. So the point of proof of proof is the following. So let's go for so the first proof in proof of proof is a mathematical proof. So think about it like this based on formal semantics you can have a mathematical proof that 2 plus 2 is four. You execute in Python in Python 2 plus 2 is four and you have the mathematical proof that it is so.

But the mathematical proofs are usually very very large like you can have a few megabytes or even more for a proof to put it all together. and it would take lots of gas to put it on chain. So what we're doing with is we're encapsulating it in a ZK proof. That's the proof of the mathematical proof. So then if if any if that ZK proof is onchain, then anybody that uses a type of ZK circuit can then check that the mathematical proof is valid by looking at the ZK proof and doing the necessary checks on it.

That's the proof of proof point.

Okay. And then there's a follow-up question. So basically you are verifying the correctness of the smart contract for example but in terms of the execution and not like the the logic right so for example if there is a transfer from the address A to B how is the proof checking that the execution was correct like the transfer really happened. So um normally the execution is checked in basically as part of the proof of execution you also have like a a uh witness you see which accounts interacted with said execution you know which op codes were executed and what resulted out of it and that's part of the mathematical proof of the whole execution that that can be checked.

Okay. Okay. I got it now. Thanks. So we are coming to end of everything for this time.

But first off I actually have one I I had to ask a deaf friend just to try a little bit to be involved. How does proof first model reduce the trust assumption developers make moving beyond fragile compilers or VVM trusted chains?

So I hope I understood the question correctly. So basically uh I think so actually could you could you repeat it please to make sure that I got it right.

How does proof first module reduce the trust assumptions developer must take moving beyond fragile compiler or VM trust chains?

Well um the answer the answer is pretty blunt. com compilers is as you said compilers are as you said fat and generally buggy. Um whatever compiler we or our friends at runtime verification have checked we have found some sort of bugs in them. So basically we completely jump over the compiler part. No need to have a compiler on the chain anymore or not necessarily on the chain but you don't you don't need to compile the code anymore.

you can execute directly according to the mathematical uh definition which basically helps you skip over the fat part u directly.

So shortcut in short

basically.

Well, thank you so much Damian and thank you for everyone for coming. Please give a big hand up for Damian.