'Cairo Deep Dive' - Shahar Papini

all right so coming up next we are having shahar papini from starkware um who's um co-creator of cairo um and uh one of the main engineers there so um i this talk basically goes is from asic to cpu it's a start journey and this will be a recorded video also because of the time zone so apologies for that um but the starcraft team is always super happy to answer any of your questions um in their channels we have internally or on your own personal challenge channel um so without further ado we will be getting on with the video just setting up the technical side hello i'm johar papini i'm an engineer at star prayer and the co-creator of cairo cairo is a language we developed to help other people use zdk stocks today i'm going to talk to you about the asic to cpu journey with stockwear head regarding to developing stocks so first i'll explain what i mean by asic to cpu and explain this analogy i'll then briefly explain how starks work and how the protocol does what it does i'll show the early stages we had while we developed stocks and the intermediate steps uh reaching to the so-called holy grail the universal machine building in stock which is a cairo and then i'll have some deeper dive into cairo and look at its features and what's planned ahead so let's begin a6 cpu a6 are application specific integrated circuits they basically basically chips they are specialized for the task they are very fast they are expensive and very hard to design for cpus on the other end are for general computation they are a lot slower they're cheaper cheaper and very easy to program for software is a lot easier than hardware and cpus are a multi-purpose single architecture it's like like a single a6 you can call it that can run a lot of things it's basically a trade-off between efficiency and flexibility and there are a few intermediate steps i would say at the one end we have the asic fpga is an architecture which is a bit more generic easier to program for it's a still not as a flexible cpu we then have some gpu which is a lot more flexible and the other end we have cpu so for each of these i'll have a an analogy in the star cord and obviously it's not a perfect analogy just an analogy so stocks what is stock stock is a family of cryptographic proof systems that can be used for both privacy and scalability this basically lets you prove statements and for example for a statement we can prove the thousands number in fibonacci sequence is some number x something and another example statement can be i have a hundred signed bam transactions they're all all signed correctly and maybe after i apply them to some state and they get some specific other state and basically everything you can do a computation for and then you can make a statement of stock statement starcraft will focus currently on the scalability part of this of stocks not on privacy stocks can do both but right now the most burning issue i would say is scalability on blockchain this is our focus now if the verification time of starks that is the time it takes to verify a proof someone made is exponentially smaller than time took for the prover and for the length of the computation itself so they are very very well suited for scalability so in bird's eye view how does stock work we have some statement we want to prove first step is expressing it as a polynomials basically we call this representation an error algebraic into intermediate representation and i'll focus on this in just a moment after we have this error we just throw it on a bunch of algorithms that and fry ld marble and then which comprise of the stark protocol and at the other end we get some proof so how does this air look like it basically comprises of a trace which is a table with some constant number of columns let's say two in this example the number of rows is some power of two and each cell is a field element in a stock friendly field and we use some specific filled with 250 bits but any stock friendly field would be okay here alongside this trace we have uh constraints that we want to prove that uh the trace holds and each constraints need to be some polynomial on some local area of trace for example here you can see this second constraint it works on the x column at the current row and the y column and the next row the repetition for this constraint needs to be a power of two and the number of constraints is a proportion to the verification time so we don't want a lot of constraints we want their degree to be a relatively small otherwise it will be very expensive and how can we use this to express statements for example if we took the fibonacci statement we could have a let's say a thousand row rows here 124 and say that the first and second element are one and our constraint will be that x2 equals x1 plus plus x0 and which is exactly the fibonacci statement and if we have these constraints throughout all the trace then it will guarantee that if the first two cells are one in one then the thousand cell is the thousands fibonacci number so in addition we can also add some constraints and say this is one this is one and this last one is i mean one two three something now that we have this representation if you can show we have a trace that holds all the constraints then we are done the other person can be sure that the thousands number is indeed what we said so let's start with the the journey at the first stage we had with some very rough tools you basically building stocks from scratch we need to design how the trace looks like how many columns it has what is the meaning of each tray cell in the fibonacci example it's pretty easy each one is the i will not yourself but when you have very complex logic you have to assign some cells to be for example the current balance of the of an account the amount we want to transfer the signature the public key all kinds of things and we need to represent the connections between them these are the constraints we want constraints of low degree and if we need some constant of high degree we will need to break break it up using some more auxiliary trace cells there is a lot of manual optimization work involved here so uh you can call it some it's kind of a puzzle sometimes to do it do this but it's also very hard and doing complex logic is complex it's a not easy i do want to state here that the main metrics we use to define how good an air is is first of all the trace space which is the number of trace cells we need you know columns times the number of rows this affects both approval time and memory and we also have the number of constraints which affects the verified time in a linear fashion so we don't want a lot of constraints the trace space also affects the verifier but the only level is a polar algorithm is the way it's not that important so this was a how we did things at the beginning then we started to develop some better tools for example one of them was a visualizer you can see at the bottom how it looks like this is basically there you can see it's one with 11 columns and some rows each each cell and you can see the constraint that work on it and we can add some visual features to these things like output cells and some things repeated in other periods and in addition to tools like the visualizer we it's also important to have some abstraction and the ability to not think of all the components in the entire area at once but do some sucking like this part does hashes this the signatures this dial does a amount or state transition things like that so doing it on top of air requires some things about america placement on the trace and the referring to some specific parts inside components so we had some in-house framework to do all these these things took a while it really helped developing things but it was still hard in some complex logic a lot easier but very hard a third step which i would call the gpu the previous tape state for the step was like the fpga equivalent the next step is actually something we didn't do something we considered a lot doing and we had some designs for it in the end we chose to skip to the fourth step all together but i'll show it anyway and the issues that are in this step so we could design some a domain specific language that compiles to an error it can look a for example like this is an example code of this imaginary dsl you have a you can call functions you can multiple problems first of all you always pay for branches basically you need to unwrap all the possible flows into the trace so each possible flow at each possible time stamps time step needs to have some specific cell in the trace so you don't say gain efficiency by doing branches you pay trace cells for both the first branch and the second branch similar similar thing we can do you can save for for loops or a recursion it's not possible to do a variable number of for loops you must also always be bounded because you need to allocate specific trace space for it and you cannot really do recursion for for the same reason you don't really know where in the trace and you need to work right now and all you can also only have things but have this constant flow pretty much you also always pay for all the iterations if you even if you right now only need 10 you need to pay for all the power to it evasions or and if you you know sometimes sometimes you need only 10 something you know 12 then you will always pay the highest so these are drawbacks we have here another drawback is there is no memory or it's very hard to implement memory in this thing it's obviously not too complete and another issue for starks in this case is the way starks i would say not scale but there are dynamic in the sense that if you have stock that works for thousands uh thousand rows you can take the same stock and apply it on 2 000 volts to have like twice the number of transactions for example if you make a stock that handles a bank transaction you can put 100 in it 200 you can use it even for thousands of of the transactions because it naturally repeats itself doing this repetition in this dsl is a is not very natural natural and if you need to do some complex logic it it goes out of the window and all together for example if you need to do something at the end for example doing some transactions and compressing at the end the outputs or checking something at the end and then there is repetition goes out of the window so we don't we don't really want to give up that part of stock that they don't work on an instance of a single size but can work on the instances of various sizes this is something we want to keep okay so what we eventually ended up doing uh carl carmen stands for cpur like a regular cpu is basically an asic that can do general computation and so is carol is specific error that can run a general computation it's a universal machine it's still complete it's a funny machine it has a random access memory and nice feature is it only has a single verifier because it's single error so we can and we do and we can put a single verifier contract on ethereum for example and the entire world world can use it to ever to know some statements are true in cairo and you don't have to deploy it every time for every project to use we can audit these contracts only once and therefore it will be more secure because we can invest more resources inside of things there are a lot of benefits i would say to having a single verifier these are examples of the ohio how the caramel cover looks like so cairo is actually two things it's the air and the instructions it can run we call it the the cairo virtual machine and we have some high language high language that works on top of it which you can see here and we don't have the drawbacks we present before for the dsl we only pay for what we use because each repeating part in the air of cairo is just executing an instruction similar instructions so if there is instruction we didn't run in another branch it signed the trace we can have complex non-imperative logic we can have recorder we can have basically everything uh the phoneme and a machine can do and a nice uh thing i think we noticed is it's actually very efficient and when we took the car version and of uh handwritten air air version when we tried to translate it to cairo it was only about 20 to 30 percent more expensive and main reason for that is a lot of applications that this one in particular is a lot of some built-in components says in this case hashes and the verification of signatures which are written in in handwritten error but just all the logic on top of it is written in these virtual virtual machine so we basically get the best of both worlds and the hard parts are optimized using heavy error components and we get the logic of a tuned complete machine in a high-level language and so yeah it was all only about 20-30 more expensive however the expressibility of cairo lets us do something more complex logical optimizations which we did and action was a lot cheaper than than the henry version and for example in in the reddit demo we managed to do 300 000 transaction in a single proof lately we even did 600 thousands and this is mainly due to this logical optimization that lets us save a lot of instructions and hashes so hey it's better and cheaper what can we ask for so some of the tool tooling we have for cairo first of all obviously we have the compiler and virtual machine and these are available today you can check them out on our site we have the solidity verifier which is deployed today on robson and on mainnet basically everyone can use it and there are also the there is a sharp tool you can use to to so we can prove your statements basically i'll touch it later we have integration with ides specifically visual studio code which we use and vim which some of us use and language server there is a tracer and a profiler out there in here and it's similar to debugger you can see it up here and basically you can after you make a specific run you can check it out and then go through all the steps in your computation and we have the playground we can which you can use today you know site and play around with the carol and how it looks like it's very fun i recommend okay so and important things our thing i want to touch is why we designed cairo the way we did there are some things that may seem unnatural to uh common developers that come from common languages which we did differently mainly because we want car to be efficient and we did it so it will be very compatible with the the air architecture i would say so this is a comparison between physical cpus and the air cpu and why some things are should be one way in this one and another way in this one so first of all how we measure efficiency in physical cpus it's mostly the execution speed how much time it took to run some computation in air the main metric we use is the number of trace cells they say this leads to the observation whereas in physical cpus adding more hardware on the chip can lead to better times like a branch prediction and caching and in errors it's not really equivalent when you add things you add trace cells by definition so we do not want to add trace cells we want to keep the architecture as simple as possible and so when we won't have a lot of trace cells and in cpus having multiple registers and it's relatively cheap and adding some hardware and some links it's usually okay in errors it's it's a bit more expensive to have multiple registers especially on the verifier side because every time we use a register we need to choose between all the registers and this chooser leads to a big constraint of multiple constraints which affect the verifier side we want our constraints to be simple so the verify verifier won't work hard the native word in cpus is bits 64 bits usually and here it's the field element because that's how stocks work every cell in the trace is a finite field element and this means that bitwise operations are easy in physical cpus because they work with bits and they're hard in air so we don't have some up code for example to do bitwise operations and we do plan to add some built-in in the future which will be a lot faster to do it manually in in in cargo operations but it will still be a lot more expensive than physical cpus and i think nice thing we have in ears is non-determinism basically because it's language for the verifier and which means when i write a program i care that it holds some constraints and not necessary that it's deterministic for example when i want to find some element in a big list in a physical cpu i would have to go over every place in this system in this array i have to go one by one until i find my element or don't find it in air it's a lot easier with non-determinism i can sort of guess the index where this element appears and i can just check but this is indeed the right element obviously the approval will have to do this linear work the proof still needs to go over the entire thing to prove but once the proof finds the right one you can you can write just a few current instructions that say oh i guessed it's in the 500 place i check i read from it i check it's okay so the the number of trace cells will be a lot smaller memory access in physical cpus memory access is a usually a lot more expensive you need to access things that are far from the cpu and it's obviously because metric is execution speed in air memory access is actually a quite cheap chip i'd say it's a it costs about five tray cells even less say three in something if you we have some optimizations which is very cheap so instead of using registers in cairo we use a memory access every instruction has some memory accesses and we have a very minimal amount of registers an important thing to note is the memory frame thing and in cpus you want to free memory if you don't remember it takes up the entire capacity capacity of memory you have when you free you can add more so it's very good to free memory in air there is no really not the concept of freeing memory as everything you ever did in your program in your run is in the trace it must be on the trace because you need to prove that everything was consistent so after the entire run you have this big trace has everything there is no point in freeing anything that also means we don't need garbage collection for example which is very nice you can access everything in the past and our memory is also immutable some mutable memory you cannot change it and again because that's basically how it works in in air in air you at the end have this big table if you have the specific cylinder it has one value at the end of the proof it test one value and we can simulate mutable memory on top of this but it will it will be more expensive and it's not very necessary there are a lot of languages to date have the immutable memory and model functional languages for example and it's we implement a lot of things in cairo it's not an issue almost at all uh when it is we have some constructs construct that you you can use that act like uh we drive memory like i said it's basically simulating and we drive memory on top of this immutable memory but mostly we don't need it and it gives a very big efficiency bonus i'd say so cairo today we are using cargo live on maintenance and we use it both in diverse diversified and mutable and dydx and this is a website for the current language you can see all the developer tools and playground and documents everything you need to know is there we have the shop which is the shared prover services it's available in robsten you can send from the playground for example straight to shop or using our developer tools to check it out it basically runs on our approvers and then the fact of your run is registered on chain we also have a few and obviously want more and to support community projects for example from for compiling from higher level languages to cairo so it would we want it to be easier for developers to use cairo is efficient it lets you do zero knowledge proofs sometimes you don't need all these efficiency sometimes you just want to compile from your favorite language you want to enable that and the way white paper of cairo is coming soon hopefully and you can see you would be able to see all the intrinsic of the air and a virtual machine how things work from the inside and we're currently working on our stark net which is a sort of a i would say a side chain which uses a theorem for its consistency and the safety and every pro developer could just deploy his own cairo contracts and run them and they will be proved on this chain and you can communicate with the ethereum with l1 and hopefully it will be seamlessly so very easy it's upcoming in the next few months so i hope you learned a bit about cairo and about why it's cool and why it's efficient and why should use it i'm sure and you can email me you can tweet because you might really andrew and if you have some questions i'll be very happy to answer so uh thank you and goodbye thank you for to all the star quartering and shahar for this very informative video it was a great talk