Introducing Core Solidity - Rodrigo Ribeiro

Transcript

My name is Rodrigo and I'll be talking about my the project I've been working on Argo with Solidity. We start by giving some context. Solidity is currently the most used smart contract language. It successfully secures billions of dollars in value. However, besides of its success, it has some limitations. uh the type system of solidity lacks some expressivity. It's not able to produ to allow us to define a reusable library code and also the type system does not allow us to uh ensure s certain

safety properties and also solidity does not have compile time of all. Currently in the current implementation, we believe that adding this a new type system, a more expressive type system and compile time evaluation in the current implementation would be a lot hard. So at Argo, we decided to rebuild the language type system and its compiler pipeline and that's what we call core solidity. The type system will include a lot of new features that will uh make the language more expressible expressive and we also plan to develop a formal

semantics for the language in order to enable for static analysis and verification. Uh what are these new features that we are planning? Basically, we plan to add generics and type classes. From the audience who has a Rust background, type classes are equivalent to Rust traits. We plan to add algebraic data types and pattern matching also type inference, high order and anonymous functions and compile time evaluation.

Uh the first feature that we start commenting is algebraic data types which allow us to define data types using the concepts of sum and product types. And each algebraic data type defines a type name and a set of data constructors names. And these constructors can hold values that can be stored inside this this type. As an example, we have here uh a data type for representing an 18 decimal fixed point numbers.

Another example of algebraic data type is this data type for modeling an auction state. It has four constructors in order to represent different versions of the state of an auction. These different uh constructors represents the subtypes and alternatives which are basically different ways of building values of this type. The products can happen inside each constructor and because each constructor can hold a an order of different types.

So we can as an example here this the console constructor can hold an u into 56 and an address as its arguments. However the true power of algebraic data type come comes with when combined with pattern matching which allow us to change the control flow of execution based on the shape of the matched values. Uh here we have the definition of a type safe multiplication function for this W data type. The pattern match is made by a pattern match block which should have a discrimin which is the

pattern which will be analyzed in this match block. Using the discriminate, we can then have a pattern describing its structure and based on this pattern, we can introduce new values, new variables into context which can be used to build a block for these values. In this case we are building the multiplication of this function and return it inside the constructor of this type.

Another nice feature that we are introducing cor solidity is the generics or for people with a function opering background generics are also known as parametric polymorphism. The idea is that such feature allow us to define functions that will work in a uniform way for all types. Here we have the definition of an identity function which will work for any type T. In order to define the signature of this function, we first need to declare its type variable using the keyword for all and then we can use this type variable in the whole definition scope. For

instance, we are using here as a parameter type and also as a function return type. Also, generics allow us to define polymorphic data structures. For instance, here we have a data type which takes a type argument. It's a polymorphic type variable which is used in the type constructor error in order to express the payload. Using this definition, we could use this data structure with any type expressible in the language.

However, while interesting, generics are a bit limited because very few functionality works for all types. Uh the most interesting functionality functionalities work for some types and that's why type classes come into play. Type classes are the b the standard solution to combine parametric polymorphism with function overloading. And here we have an example of a type class for defining a multiplication function.

A type class defines a name of this type. For instance, here the name is moo. And also together with the name, we define a type argument. And in the body of the class definition, we define a a set of function signatures which could mention the type argument which are defined in the type class. The implementation of a type class is given by an instance definition where the type argument of the type class is replaced by a concrete type. As an example here we are implementing the type class for multiplication for the

previously shown type of 18 small number fixed point the wad type and in the definition of the instance every place in the class declaration that we have h a variable a type variable it the type variable is replaced by the concrete type. So we have the both in the function signature and in the instance argument the type variable is was replaced by the concrete type and instead of having only the signature the instance should provide the implementation of this functionality for this concrete type.

One interesting feature uh is that sorry is that we can using type classes we can define functions that allow us to restrict the set of polymorphic types in which the function can operate. As an example, we have here a function square which will work for any type T which has an instance of this MO type class. We can restrict the set of possible polymorphic values within a function using a type class constraint.

Here we say this type class constraint is specifying that this function would be valid for any type which has an instance definition for the type class moo. Uh another interesting extension that we have in core solidity is that the language will now support both high order and anonymous function. This means that functions are now a first class in core solidity and they could be used as both function parameters and return values.

As a short example of this, let's consider uh a simple utility which will allow us to count the number of calls a given function is called. Here we are using inside this definition an anonymous function. We start the definition of anonymous function with using the lamb keyword. After the lamb keyword we have as uh the arguments of this anonymous function and then its body.

An anonymous functions can capture any values which are present in their definition scope. As an example, we can see in this function body that we have the definition of the counter variable and it's mentioned inside the body of this anonymous function. So here we have a capture value for this anonymous function and also this utility shows an example is it serves as an example for high order functions because it takes a function as argument and returns a function as a result.

uh we use this syntax in which arguments are represented as a cur tpple and the return type of the tpple of the function is follow is marked by this arrow operator. Uh another interesting feature that we are adding to C solidity is type inference which could be used to to help the readability of programs because we can use type inference in order to omit unnecessary type annotations and but also having the guarantee that the the all static checkings done by the

compiler are done properly. Uh since you are dealing not only with parametric polymorphism but also with overloading some ambiguities can occur but they occur in very hair situations when you are doing for instance some sort of type level programming which is possible within core solidity. As an example of the utility of type inference, let's consider this simple array literal definition in classic solidity.

This definition is rejected by the soci compiler with an error message which says that the type u8 is not implicitly convertible to uit 256. In order to fix that uh this happened because Si use a limited support for inferring the type of array literal. The idea is that the the elements types of the array will have the type of the first expression such that all other elements can be implicitly casted to it. In this example, the first element has type U with eight. So it considers that all

elements have this type and u int 8 cannot be casted to in 256 implicitly. The solution in classic solidity is to add this type coercion into the first element of the array. However, in core, this would work as it is because thanks to the more general strategy used by the type inference, we can simply eliminate the need of this type coercion predicate.

Okay, I showed several features that we are introducing in the language, but a question probably is remaining. how those features would help us to develop better code. Let's take a concrete example. Uh here is the some snippets from the forged std implementation of console.log utility. This implementation has a combinatorial explosion of overloaded functions. For instance, for logging one argument, we have more than 30 different function definitions.

This happens basically because currently solidity does not provide uh support for polymorphism. And in a simple way all these more than 30 functions just call this one which makes a static call to some specific address in order to implement the console login. This same definition could be expressed in core solidity by one just one single function.

The idea is that thanks to type classes, we can restrict this function to receive only arguments that implement a type class for AI encoding. So if any type has an implementation of AI encoding, it could be logged without any problems. So basically the code work as follows. We take the argument AI encode it to get its payload. Then we convert the payload to a representation which would which would be passed through assembled blocks which inside core solidity is

called the world type which basically a type which represents a U variable. So we convert it into a U variable and make the same assembly block to make the static call. So basically the usage of type classes and uh and generics allow us to reduce this uh repetitive definitions. Okay. But uh during the development of core solidity it was clear that would be really useful for us to add another mid-level IR which called sale which stands for solid algebraic intermediate

intermediate language. It's basically a a low-level language with more some high level features like functions and low-level contracts, algebraic types and pattern matching, assemb class and generics, variable introduction assignment and a short circuit if expression. uh the idea one of the main motivations of course solidity was to make easy to extend the language. So in order to achieve this we plan to use sale as the main definition language

and the all core solidity high level constructs would be the sugared translated into sale and standard library definitions. Such approach is really is used by several programming language uh several proof assistants like the link prover which also relies on several the sugaring steps into uh a more more verbose representation. This the ultimate goal with this was to will be to allow us to extend both the language and standard library using some sort of RFC style process.

Uh well, one thing that might be concerning the community is that we are planning a major review of the language and this is a challenge thing and our we are really concerned to make this transition as smooth as possible to avoid a language split. So basically our plan would be to keep the AI compatibility. Also we try as much as we can to minimize syntax change and we also are planning to develop tooling for automated migration from classic to core code whenever this

migration is possible. uh as a concrete example how core would be close to the classic solidity. Let's take the very first example of solidity code which present in solidity docu documentation. It's basically a simple contract which which defines a storage variable and a get and set functions for it. The same code in core solidity would be exactly as this. The only syntax change would be that in core we will use postfix types and also we have a slight difference on the

function signature syntax because we try to minimize the to make the s the syntax of the prototype as simple as possible to start to develop the type theory and the type inference without bogus too much trouble with this to to make to replicate the syntax of function signatures in solidity because they have a lot of stuff like function modifiers and stuff like that. So it's possible to see that the syntax is almost the same.

Well, what remains to we reach production? We have a prototype implementation and also a prototype implementation of the standard libraries which provides functionality for AI compatible contracts, AI encoding and decoding, dispatch generation and storage access. And our prototype is able to compile an ERC20 contract expressed using the standard library. Well, while we have done a lot of stuff, we have some steps that we need to finish. We need to define compile time

evaluation because and also a module system. Once we have this two features defined, we believe that we have would have a a a stable prototype and then once we have an stable prototype, we could split the the development of core solidity in two fronts. The first one would be starting to produce a prototype implementation and another one would be mechanizing the meta theory of the language use a proof assistant in order to have a verified semantics for it. This would be useful to for instance to fuzzing the compiler

against its specification which would be the meta theory of the language. Well, our focus would be to define the language as it was present here in this talk. But we have a lot of cool ideas that we want to explore in future iterations like adding linear types which would allow us to have uh compiler verified resource control because it's would be really useful in the context of solid applications. also refinement types which will allow programmers to add logical properties to their code which

which would be automatically verified since our objective is to make the addition of high level constructs to core solidity to be implemented as the sug steps. One thing that we want to to check how to include it in the language would be macros because they allow us to implement new features. These disagreeing steps just as normal library code that could be imported implemented it like in language like the link prover dialect like racket. And also we would

like to investigate how we could add theory improving capabilities to the language following uh system language with this capabilities like bedrock 2 or ATS. So basically this is our core solidity which is our reimagination of the language. The all these changes aim to make the language more expressive, more secure and mathematically sound.

And that's it. Here is the car code for the Solidity Corey core Solidity repository and for the feedback forum. and we love to hear your opinions on the language design and suggestions to help us to build the next generation of smart contract language. Thank you. >> Thank you so much Rodrigo. Um we have quite a few questions but luckily we also have some time uh reserved for these questions. So let's tackle them one by one. First question, why does the

simple contract in core solidity need to import std? >> Uh because we need to generate uh the dispatch for this simple contract. So the dispatch generation is part of the standard library is not part of the compiler itself, the compiler code itself. So a lot of the functionality which is currently built within the soc compiler will be moved into the standard library of core solidity. This uh would help us into make the language more extensible because whenever the community wants to make a a new addition

to the language, a new uh we could just implement it is a part of the standard library without even touch the compiler source code. That's our ultimate goal. Um, five people have voted already on these questions. Um, what's the timeline or when core? >> Uh, that's a tough one because uh, uh, producing uh, a new language like core. It's not an easy task because we want to be sure that the type theory we are developing is sound and not incur in any

unoundness. So we need also to develop this thing of compile time evaluation that would be demand a quite of time. It's quite complicated to to give a precise timeline for that. Sorry. Um I'd like to just chime in. We've been writing about core solidity and as well as classic solidity and the road map around it. Um these blog posts are have been regularly coming out. We plan to write more about it. So please keep your eyes peeled for the upcoming um blog posts in that series. That should also tell you um a lot more about the team's progress with the new language and also

like how we're making our way through the road map. Um, it might not give the concrete timeline for the entire thing right away, but at least it will keep the community in loop. Um, and I hope that answers the question a little bit. Um, moving on. Are algebraic types going to be AI encodable? >> Yes. >> Yes. >> Okay. Yes. >> Yeah. The because AI encoding would be implemented as part of the standard library. So any type that uh is defined in the language could be an instance of this type class for AI encoding. Currently we do not have this

feature like language like ling and hasll which supports type classes has a feature which allows the automatically derivation of instances for newly defined algebraic data types. Our plan is to make within the compiler this gen automatic generation of AI encoding for through this deriving mechanism in a similar way which has happened for within Haskell and ling but since it's part of a library it gives the users the possibility to develop their own AI encoding in a more efficient way if they want to basically Awesome.

Um, does core solidity also have the same caveats as classic? Example, stack to deep errors during compilation. >> Uh, well, stack too deep is basically a problem of the back end. The core solidity is more concerned about the front end of the language about the type system and and the verification of let's say highle constructs. Basically uh this stack to deep error happens when all type checking and all verification of the code has already been done. So uh if it's a problem of the back end well core is not able to solve it

>> and what kind of features would make the language more secure. >> Well basically when we have algebraic data types and pattern matching we could allow a more precise representation of the types that are being used inside applications. This uh thanks to pattern matching could avoid issues like you have a gigantic strct which have a field to represent different situations like for instance you have an application that uses let's say three different kinds of tokens and we use some field inside the strct to represent that a specific token is value

is being represented by this strct. And then you need to complicate a lot the logic for that. U also uh having let's say a more type- safe language would allow the compiler to catch mistakes as soon as possible without having to to the whole compilation pipeline. So uh in order the plan is to make the language more secure to make the type system of it more expressible more expressive. So we could express safet properties like making invalid array access and stuff like that

uh represented within the types of the compiler itself. This next question is a little less technical and more about the standard library. Who will be building the standard library? Will it be Argo? Will it be someone else? And will we have competing standard libraries like we have competing compilers and smart contract libraries? >> The plan would be not having complete standard libraries. Uh the idea for now is that we are the the library we are building are basically as a test to to assess the how the language is how expressive is core solidity. So we made using the language

we are able to define AI encoding dispatch generation which are things which are basically implemented in inside the solid compiler itself and they are now in the user space. So it's possible to define it as you want using the language. This is a good sign of how the language is expressive. But uh the plan would be that as I told in the talk that both language chains and this standard library chains should be defined by the community using some sort of RFC style comments that the community should prepare an RFC and some

sort of committee decides if this would enter or not the standard library or the language itself. self. >> Yeah. Um, do you have any plans to add higher kinded types? >> Uh, well, we are we would love to hear if you have some example of higher kind of types that would be useful. Please reach us with this example because up to now we didn't see the need for higher kinded types. They are interesting of course but uh we are very cautious to not uh put too much type theoretical

features in the language in order to make it as simple as possible. >> I hope we're not wearing you out. It's um clearly an important topic. So we have a few more questions. Um have do you have any idea if any LSP is on the works for supporting this new type system? >> Well, no clue. I don't know if uh how much work would be involved in that.

>> Okay. Um does the example of foundry polymorphism have zero additional gas cost compared to the current version? Well, we do not measure gas costs for now. We are making let's say experiments regarding on how expressive the language is. Uh basically since core solidity will compile down to you basically the gas costs would be uh similar I would say but we need to do some experiments to to be sure on that.

So we do not have data on this yet. >> Okay. And um are the data types just internal or will we be able to use them when doing calls between contracts? >> What I do not understand. >> Are the data types just internal or will we be able to use them when doing calls between contracts? >> Yes. would be you would be possible to to do it because basically uh algebraic data types could live outside contracts. So you can have literally modules in the code which define functions and algebraic data types without

uh being attached to an specific contract. So >> okay awesome. Um, and what are the gaps you see for Solidity to reach um, version 1.0? >> It's a better question to be answered by Camille. >> I was about to say that. I think it's a Camille [laughter] question. Well uh the main thing we need is stable implementation of uh corality which means right now we have the sol the prototype and there are those um things that Rodrigo mentioned like uh

modules in the prototype like uh designing the uh compiler evaluation system this will complete the type system then we proceed to implement the kit in the soc compiler and there will be some period of stabilization and 1.0 So like as we stated in our blog post is basically when core is deemed stable enough bug free enough uh feature rich enough to become the default front end and uh then we'll for for a time we have them side by side and eventually retire the uh classic solid but for now it's basically uh about when we'll get a stable production

implementation. Thanks so much Camille. Um not a question please share the slides publicly. I just wanted to say that uh after every solidity summit we basically because all of the talks are um recorded. Uh we do publish the recordings along with the slides. So keep your eyes on the solidity official blog. Um we will publishing we will be publishing a blog post with um a recap of solidity summit where you can find all of these slides um that will be made public and yeah um I think okay one more is it hasll and move that is inspiring these changes

>> uh >> and how long from production are we that's also another question in the same way as is it one year >> basically that we took inspiration not only for Haskell but also from Rust which quite popular among this blockchain domain but surely Haskell is a great inspiration uh and also the ling language so yes Haskell ling and rust are the main inspirations for this new extensions to core solidity well regarding the timelines as I said uh it's not easy because to be ready for production on this We would have would like to have a formal proof that the

type system we define is sound with respect to the semantics and not a just a pen and paper proof because papers accept anything. So we would like to have a formally verified proof of this using some proof assistant. So it takes some time. >> Thank you so much Rodrigo. >> Thank you. >> That's all of the questions for you.