Cairo - Writing Provable Programs

Transcript

[Music] [Applause] thank you hello everyone um I'm Gil I am a developer in the Cairo compiler team if you know don't know what Cairo is don't worry you'll know in a few seconds so what is Kyle um in yeah um I'm going to talk about today about why we're doing Cairo but I'll start a bit with what is Kyo Cairo is our programming language to work in starware in starnet um to prove your computations on stet um let me start by telling a little bit about Cairo um as I say it's a

programming language it's a high level modern language we aspire to make Cairo as easy for you to use as possible um it's the sibling of Kyo Zer if you had the pleasure to use Kyo zero then you know that it was a sketchy I think is a good good word language it was not good yeah it was not good um so we dropped everything we started from scratch and we built Cairo One KIRO 1 is our new new language to use in Stark net and it's a modern language it's easy and that's why I want to show you you today h it's only

also open source you can check us out and we are always adding new features and new improvements so why do we need Cairo let me tell you a bit about stet stet is our L2 validity roll up over ethereum we scale the operations of ethereum by using proofs we are generating proofs of what we're doing on Stark net and then later down the chain if you have seen kerit talk about the pro later down the chain we are verifying it on ethereum but the question is what can we prove what do we prove

so we prove kazm code what is kazm code kazm is chiro assembly in our company we developed this really unique and compact Assembly Language that we can prove and think that run that is written in km but I don't want you to write in an Assembly Language right so on top of kazm we want to achieve two things we want to achieve a language that is safe and ergonomic I'll start with the safe part how do we do how do we make a language safe so we introduced another l ler

above km which we call Sierra which is safe inter intermediate representation and Sierra is like really it's more similar to i l languages but it's not and about Sierra we can prove a lot of stuff we can prove that every execution path can be terminated given that you have enough G um we can prove a lot of thing about K and that's that giv is giving us the safety that we want but I don't want to talk about SRA just know that it make it it is what making us safe above SRA we have Cairo Cairo is what most of you developers we want you

to interact with what is Cairo KIRO is our ergonomic new language um and that's it this is our stack that we are working on today from Cairo to Sierra to kazm to proving on St stet and what I want you to to see today is that Cairo is not that scary Cairo is nice if you develop in Rust it is very much rust likee so you should feel at home and let's see how Cairo is looking so I'm going to show you a lot and lot and you'll get tired of it implementations of the Fibonacci

function let's start with the first first one in here we have a really regular implementation of Fibonacci function just if we are at the end return a otherwise do it recursively why do I do I show you this you can see that we have this weird type we call felt 252 well felt 252 is shortcut for field element with roughly 2 252 bits um the pro technology underneath Cairo use elements of finite fields in this case of size roughly 252

bits we don't want you as a developer to be exposed a lot to the underlying technology of proving when you you are eting code but you should be familiar with the felt 252 why because this is the most efficient a native type that we have um it is essentially a type that if you add too much to it you'll get a wrapped around to zero um so we have the F 252 but rather than this it's really similar to any other language um if you don't want to use if you can also use match which is a similar to switch case if you know from C or JavaScript I think

um we can use match we're matching on a and doing something accordingly so if we are at zero do a otherwise do if we are at one do B do a plus b otherwise do recursive call um that's nice but uh I'm ining match now to talk more about it later it will be very much to you it will be put in much in much to use later um but if you don't want to use f 252 you don't know what this nonsense is about so as I as I said before we want to make Cairo as easy to use as it gets you have all the types that you are used to H from rust if we know we use rust

notation but you have uze int of uh 64 bits um and this is an implementation using usze now if you use this type you will need to pay a little bit of overhead for the verification that it is indeed it is indeed fit in you in u64 but it's a trade-off that you'll need to make as a developer it doesn't cost that much on top of it we have many other types I don't think that I'll talk about that much um so this is the basics of Kyle we have nice language it should look like any regular language we don't

want you as a developer to feel that oh we are working in order to prove something we want you to just write your regular code we'll do everything in order to prove it and give you the security that you want let's look a little bit more deeper into Cairo again if you worked with Kyo Z you know that there is a painful point that there were no Loops in Kyo zero I told you it was sketchy um so now in car we have while Loops um it should look like any other while loop that you've seen nothing special um before the while loop like one year ago we introduced the loop

loop which was even simpler it just while true um but now we have y Loop soon we'll have four Loops we needed something for the four Loops but in the next version we'll have four Loops as well so again not that scary um arrays we have a few native data structures one of them is array another is a dict type um it behaves a little bit different than the arrays you know but you can do many many uh things with it again Fibonacci now you can put everything in the

arrays and it all works as you can see if you know rust this is rust code okay it will work in Rust you can just plug and play it um but uh as you can see it's a regular language nothing special um let's continue okay now we're getting into a bit of chyo specific stuff so uh we have an array we can return a from H our Fibonacci function we don't have to return only the array or only

the result we can return the topels of the array you can see that we can unpack the tapel in here okay and we get the results of Fibonacci 10 using the array that we defined okay and we just adding into the array um so that's it about race I'll go now into a few deeper things in Cairo and then I'll tell you about how Cairo is used in stet so in this part I'm going to not going into very much details because it's a

little bit deeper so if you know rust in Rust you have trait tra is a way to define an interface because up until now I only talked about functional languages traits is a way to define an interface that you can Implement for a type or not for type so in here we have a trait that we call combine and our new Fibonacci function doesn't just Add A and B it does combine A and B how does it know how to combine which combine to use I only have a trait we we give give as a generic parameter we give an

implementation of combine we call it t combine you don't have to to give this name but we give an implementation of combine that the FIB function will use um if we want to be even fancier we can change the trait of combine to use the self keyword and then we can just do a do combine B and we we are getting methods for types um how can we Implement a trait well it's simple we just add an impel function impel with some name combine u64 of the trait combined with u64 as

generic parameter and um and we do self plus other now you ask yourself what I need to Define which impel I want to use everywhere no if you'll create an instance of FIB that we infer use the type u64 we will infer also that we need to use the combin u64 so you only need to state that your Fibonacci function needs an impel of H combine of T and we'll find for you the correct implementation

uh the inference mechanism of CYO is really strong um we try to make it even stronger the next version will have some improvements in this field but it is already really strong um if you know rust by the way this is the place we derived we we strayed as far as we got from rust in Rust impels are not named but we choose to do it we are thinking that this is better um another thing that we have is user defined types what do we mean by that we have structures you can Define structures as in any other programming language that's nice

D and so we can Define structures it is really self-explanatory for developers and also we have attributes attributes are decorators for any kind of item or statement so in this case we we are saying oh this struct F result I want it to derive implementation implementations to the copy and drop trait I want it to be copyable and I want it to be dropable by droppable I mean I can just forget about it and then we can make another FIB implementation so that's it about Stu

and another user defined type which is not that common in any language is an enam what is an enam it's a type that allows you as a developer to have one of a few possibilities of types of variant we call them so FIB operation can be either add or ADD const and in this case it have the added like the echo wasn't enough um the added data of u64 type and it can be mo and remember that at the beginning I told you that match can be used for another thing where it can be used

to choose which variant we have and act accordingly in h in your code so you have an inam you choose which you do a thing according to the variant and that's it that's like a crash course of Cairo and it's like the most B Basics things you need to know about Caro but up until now it was like any other functional ER program language I haven't said anything about stet or about smart contracts it's

dripping on the TV um yeah um okay so I haven't told anything about stet or smart contract but what can you do with what I've shown you until now you can write any code you want and you can prove that you ran it and later verify using our Stark technology so let's see how you can write smart contracts with it um this is maybe the most basic contract you can write in

Cairo um we have at the top we have an interface that we Define for the contract we have set balance and get balance nothing fancy here we have a storage that we Define for the contract this means that this contract can access a balance field in the storage and then we implement the interface that we defined above there is nothing fancy you do self. balance. right New Balance if you developed a little bit in your life it should see it should look familiar for you okay the same with read

you can do whatever you want um all the attributes that we add it's because the smart contracts are like an additional layer on top of our language we don't want it to be a part that is embedded in the language itself but the compiler know all about smart contracts what all else can you do you can add events to the smart contract and just then emit the event event is an inam of events and you can emit any variant of event

and I won't talk much about this but if you want to have some shared shared uh cases between contracts then you can add components what is a component a component is like a module like an helper function for contact we here we Define the component of upgradeable I won't get into it much it it uh implements the function upgrate and then I just can say I want to embed this component in my contract how do I do it I just say on top oh I have this component this is the path to the

component this is the storage of the component this is the event and boom you have the component in your contract it can be like upgradable it can be an erc20 ER component and you just oh I want to use uh the earc implementation of this Library you add it as a component and you have rc20 capabilities in your contact um so that's it about components um I'll skip this you can call of obviously call other contracts and that's it um what's next uh we are adding Associated types oh that's nice

that quiet um we read in Associated types uh if you know you know what it means I won't talk about it much but it opened the door for us as the core developers to add iterators and then for Loops uh better storage access D trate all of these are derived from associate Associated types we had a default implementation to traits and we had some tools to reduce cost um it's a little bit bit obscure because we added like disability to write lowlevel code in Cairo not really but uh it is good enough approximation uh a lowlevel code that will be very much efficient and you

can use libraries that will implement it h in order in order to get cheaper transactions um that's what we have in line for the next version that is just around the corner and I think that that's it um thank you very much I hope that you will now I I have heard in the last few days that many people are saying oh I know about stet but I need to learn this new language Cairo I hope that now we'll see that it's not as scary as it sound thank you very much thank you so much Gil thank you and well done for braving the the elements and thank you also in the

audience for braving the elements I know that a couple of you were hid by the water from above um does anyone have any questions before you disappear please yes young gentlemen there um you'll have your microphone a second thank you uh does uh chyo compiler do uh comp compile time checks and uh optimizations yes of course um we are doing a lot of compile typ type checks uh it is a type language so it you must we must infer all the types you don't need to annotate the types but we infer all the types from like the signatures of the functions and so on

and we have this middle intermediate representation that I haven't uh mentioned and in this phase we are doing a lot of optimizations um inlining uh graph compacting and many others um you can check it out in our repo you can ask me later if you want um but yeah we are doing a lot of optimizations the previous version that we released um we we added a lot of these optimizations and we cut the costs of transfers of fly transfers for example by almost a a factor of two thank you very much for a great

question and a great answer one more question here please you okay do you would you consider Kyro to be an object oriented program language uh what oriented like object oriented um that's a question that is raised a lot about trust because the traits are not bound to a type there is not an interface of a type you can Implement a trait for a lot of a lot many kinds of objects so you can make it look like an objectoriented but I think it is it's a philosophical question that the rust Community is struggling to answer so I can't really answer it um the rust arore development

says that trust is not so I won't say Cairo is is object oriented because it is really similar to rust it is interface and trait oriented I'll say thank you thank you very much um we have one more question if anyone would like to ask ask now or forever hold your pece otherwise I'll have one okay fine I'll have one Gil when I was talking to your fantastic colleagues um at the at the store yesterday they were saying that one of the things that you're aiming for is also Mass adoption and giving uh developers from outside a chance to kind of get into blockchain development what do you think is in store for you for the

for the next year do you think that there'll be a much like higher intake for from uh from people that have just until now only been familiar with rust yeah I open it it can be like the gateway to the web 3 world because solidity it's not really comparable maybe JavaScript but I'm not sure it is comparable to any main used in the in the web to Industry language and for a r developer using Kyo should be like