zkSummit6: Cairo: A Turing Complete STARK Framework – Shahar Papini - StarkWare

Transcript

[Music] um now i'm here with the first speaker shahar papini from starkware and uh he will be talking about cairo so i'm very excited to hear your talk take it away i'm shahar sharpa piney i'm an engineer at starkware and i'm the co-creator of cairo in which you will soon see what it is all about so i'm going to talk about uh our journey in starcraft from a asic to cpu in the stark world it's at least i'll

start by presenting what are stocks like very generally uh i'll show the early stages and start of how we develop stocks and how we progressed and how we ended up at last at the so-called holy grail please currently the universal machine written in stock and we call it a cairo so what do i mean when i say asic to cpu well asics are application specific integrated circuits there are specialized hardware looking

for some specific goal they're usually very fast they're also expensive to make and they're notoriously hard to design for on the other hand we have cpus central processing unit they are some specific chip specific asic they support general computation they are usually a lot slower and they are cheaper to make they are very easy to program for at least compared to asics this trade-off between essex cpu is one of the efficiency versus flexibility cpu is very flexible but it is usually less efficient than red essex

and okay so this analogy is a very it fits very well for our journey in starkware and and uh and share it in a minute but first i'll give you a brief overview of starks what are starks stark is a family of cryptographic proof systems that can be used for both privacy and scalability stock proves statements these statements are about some computation that a computation was executed correctly a few examples of statements we can

prove for example the 1000th number in the fibonacci sequence is some specific number or another statement could be i have these 100 signed bank transactions and when i apply them one after the other on some specific state they are all all turn out to be valid and i get some other state at the end at stark where we chose to focus on the scalability part of the starks and a major reason for this is uh first of all starks are very efficient to verify their verification time is exponentially

smaller than naive computation of a same computation problem and this fits very well to applications like the blockchain where it it's very costly to run something on the blockchain because everyone on the blockchain needs to verify it so if we can take this huge competition of a hundred thousand ten thousand day transactions and compress them to a small proof with some very small verification time then the blockchain needs to work a lot less

and it's a lot cheaper to use this so this is mainly what we did today though stocks have the capability of be being zero knowledge and preserve very privacy as well all right so a bird's eye on how stocks work you have this statement the program we we want to uh verify like the fibonacci or the bank transactions the first step is to translate them to some algebraic representation we call it air after we did this transformation to an error

we can throw this on a bunch of algorithms fry ld merkel the stock protocol and basically in the other end we will have this short succinct proof so how does this representation look like this error well to represent our statement we use a table we call a trace this table has some constant number of columns and the number of rows is some power of 2 and each cell in this table in this trace is a field element in some finite field

and it has some meaning regarding the statement we want to prove for example if we wanted to prove the fibonacci statement then probably the ife row would correspond to the i fibonacci number or something like that together with the trace we have constraints on these cells these are polynomial constraints and act in the field on these three cells in the fibonacci example the constraint would probably be a some cell equals to the sum of the two cells above it

like in the fibonacci recursion and if this was a bad transaction that again each cell would probably correspond to something this statement like the balance of the user the amount in the transaction and the constraints would be be something relevant to the statement like a new balance is the old balance plus the amount of the transaction things like that all right so now we can start the journey we had from asic version to cpu so how did we build stocks at the beginning and we put them pretty much from scratch

we needed to design the trace you know we think about how many columns we we needed assign some meaning to each tracer what it represents and then we need to need to add constraints and we can only use constraints which are polynomial of low degree if we had higher degree we needed to break this up perhaps with auxiliary phase cells and maybe we need to change the number of columns in response and this is this is like a very manual process and also if you want to optimize it it's all done manually and the the way we measure efficiency in stocks

is the size of the strings that is the number of cells in this table this uh tray space directly affect proven time and the memory and the other way we can measure efficiency is the size of the constraints which corresponds to the verification time so the main thing we want to optimize for is the trace space and the secondary is the constraint size usually well this menu process is nice for very small problems but when the problem gets more complex this process gets very complex very fast and it's hard to

do very big projects in this way all right so the next stage is a developing tools and frameworks to help us stopper we develop developed multiple tools and things that we can help us and these are a few examples and what you see in front of you is the visualizer and you can see the columns of a trace of some problems and each cell has some text on its meaning and you can see the constraints that apply on it there's also some verifications and another thing we developed is some framework for errors which gives us

a way to deal with abstraction for example if we have some repeating logic in the air that we want to use in multiple places or in specific air multiple times with multiple sizes different parameters and obviously we don't want to write the same thing manually over and over so we need some framework to help us do that so this is another thing we did and another thing is automatically placing a the cells with meanings onto this trace and without need to do it manually just find the empty places or trace and put things on

it so all these uh helped us a lot and actually the first product we we used is stockx version 1 and used these kinds of tools to create okay so this is a nice but it's still not ideal what we would like is probably something that resembles more a programming language so the next uh step we we could take is writing some domain specific language for errors now we eventually didn't do this step actually we had a few

designs for it but ultimately we decided to move on to the final step which you will soon see so this stayed in the design phase but what does it mean a language for aries well we can think of this imaginary language that has some logic in it and we can take this code something that looks like code and translate it to a trace and constraints for some problem uh well this is seems nice but there are a few problems that rise from this for example

if we have some branch some if we always have to pay for both branches and we don't know in its compile time which branch will take so we need to allocate some trade space for one branch and some trade space for another and write the constraints for both so we pay for both a another thing is loops and the loops are always a of constant size because they're basically unrolled to have like 16 repeating the code block inside and that means we need to

pay for all the trans the iterations this means this is we can't really implement general logic with this and do a a calls or i think recursive calls or similar things uh so uh some reason the the reason we wanted to do something like this is to have a flexible way to program this stuff more like programming language in a higher level but uh some of the drawbacks no memory branch branching is expensive no recursion it's not your complete everything takes space and also one specific for stocks a

a cool feature of stocks is if you design your constraints and trace for for example for eight transactions then you can later take the same error deployed contract whatever and put 16 transactions or 32 transactions you can put a repetitions of a this problem instance and they verify it in the same stock it's a very nice property of stocks which help it scale somewhat but the downside is that if the program is not repetitive in nature then this doesn't really help us

for example if you wanted to first execute a lot of transactions and then to compress then we don't get this feature of stocks which is a shame please stay in the dcl way well we wanted to solve all these issues it's something really flexible a so-called the holy grail and this is why we developed cairo now what is cairo cairo is a specific air specific cpu error it can verify general computation and it's a

efficient it's a turn complete universal machine with one human machine and we have a single air single verifier to verify every kind of program we can think about it that is written in air these are a few snippets of the cargo language that ultimately compiles to these cargo instructions that our air can verify these are examples for library functions it's it's a developing language we are expanding it all the time uh our new version of stockx is written with cairo and

the all the new projects are written using it what you get in cargo first of all you only pay so-called with the three cells what the efficiency measurement of errors you pay only for what you actually run if you have a branch you only pay for the branch you've been in if you have a loop that only occurs five times that's what you pay for it can support very complex non-repetitive logic you have recursion and various conditionals and it is a very efficient for example where we took some real word application that we had an air for it

had handwritten air we written the same logic in the cairo language this yielded something that is about 20 to 30 percent more expensive which when you keep in mind the asic analogy it's very good because cpus are usually a lot more [Music] expensive a lot slower i mean compared to essex then 20-30 is pretty good however uh when we use the power of cairo and implemented some logical optimizations that are really easy with code but very hard when you write the error in hand

and with this logical optimization picara version was actually a lot cheaper which is a very maybe surprising but it's a very cool property of cargo we got flexibility and we got efficiency in this case at least so like i said we are developing cairo all the time we have a lot of tools for it i would say the compiler we have virtual machine whether the solidity verifier it's also already deployed to mainnet in the diversify setup you can look at it today and we have integration with the ides via studio code and vim

or the formatter language server we have a tracer which is similar to debugger you can see it up here we also have the playground and which we plan to release in the next few weeks so you can play with you can see it in the image down below all right so i want to share with you a few considerations we had while designing this cpu error this comparison also shows why it is not a very good idea to just take some existing architecture for physical cpus

like x86 and just writing an air for it if you do that you'll get something that is not efficient and because it really doesn't fit to the i would say physical aspects of air so first of all how do we measure efficiency in physical cpus it's execution speed whatever runs faster is better in air the efficiency is mostly the tray size the number of trace cells this also means that it is easier to do optimizations for the execution time in physical cpu you can usually add more

hardware like branch prediction or out of order execution this is more harder but it makes the execution faster so it pays off in air it's a usually a lot harder because if you add logic if you add trace cells for some hardware you by the finish and get something that is a lot less efficient so although you can do things sometimes usually it's better to just keep it simple keep it lean keep it fast and fast i mean less trace cells uh regarding the registers usually physical cpus have multiple registers they are relatively cheap in a physical

cpu in air they are more expensive they make your constraints be a lot bigger because you need to choose from a lot of registers so if you remember bigger constraints means a bigger verification time so so the verify side will pay if a we have a lot of registers another difference the native word and usually in physical cpus we work with bits usually 32 or 64 bits in air the basic word is finite field element because this is how the trace works and this also means that while bitwise operations in physical cpus are relatively cheap it is

very hard to do a bit wise operations and more expensive in error a cool feature we have in errors is the non-determinism in physical cpus you know it's deterministic you have some computation veils as before you know what you get at the end in errors you can use a non-determinism and if you know the class np for example this is what i mean by non-determinism you can guess things and then prove them for example if i would like to search an element in a list of size n in a physical cpu i will have to go over this list it is n steps in the cpr i can you just

guess where this element is at the at what position and just show it's there hey see the element hundred is what i want and i would say of one iterations another aspect is the memory and memory is also very different and memory access is usually expensive in cpus it has a large delay with respect to other operations in error it turns out it's a relatively cheap to access memory it's not that expensive and and the freeing memory is beneficial physical cpus for example if you have this constant

size of ram and used it up then you can free memory and then use it to allocate other stuff in errors it doesn't really work that way because once you use some memory some information it stays in the trace because it needs to get in the in the proof you need to prove that this computation actually happened and was correct so there is no meaning to freeing this memory you still need to prove things about it all right so uh cairo now in the future and like i said we use cairo today in stockx

version 2. and start is live on minute we diversify soon with immutable as well and we have the upcoming perpetual contracts project with dydx soon we will release the white paper of cairo so you can see all the details inside like i said we will plan to release the playground and then sometime after it maybe some developer tools so you can use it at home we also plan to promote community projects regarding cairo for example compiling from high level languages so it will be easy program in your favorite language and it will be translated to cairo and be able to prove

it all right so thank you very much and that was me that was my lecture and i hope you enjoyed i think now there would be clapping so i'll do it for you thanks um so there's some really great questions in the chat and i just want to pull some of those out um let's see let's start with oh yeah dara i was hoping you could actually elaborate a little bit on yours because i was uh yeah elaborate on what

uh so there we go so dara just elaborated um so a question have you considered a hybrid of specialized non-turing complete circuit blocks and a cp blocks and a cpu style block a yes we did and and we do and not every everything is actually implemented in cairo when we need to do something very fast we have some more specialized error component that finds a runs alongside it just too so we can get very efficient programs um i think two people were asking if the code is open sourced

if it's available publicly i see so some of it might get open source we are not sure yet uh exactly what we want to open or not but uh some of it we will remain close but we we hope to to give enough tools for everybody to use it even if they don't use software but like i said we don't know yet what you want to open source or not okay one more question was how do you choose the finite fields you used in cairo okay so we we have this specific prime use because it's sufficient to do

computations with and we have some architectural limitations it needs to be big enough to contain the instruction coding uh but other than that it can be a lot of things and there are no very very hard limitations other than like at least 60 bit and efficient isaac asked what is the concrete efficiency like i said for it's hard to measure apples to apples but in the real application when we in stockx version one

when we moved from the handwritten which was very efficient to the current version with optimizations it actually became faster so i would say very good overall bobbin was asking how cheap is memory access in cairo for example how many cpu cycles does it take to read write from to memory actually it doesn't take multiple way cpu cycles every cycle has a few memory accesses and it just repeats this way the efficiency is measured by the number of three cells and

it's not big like if i i don't know exactly how much but maybe five six seven tray cells something like this can isaac was asking can you explain the arithmetization specifically how do you iterate over vm instructions in memory access it's a very similar to i would say transactions if you you know general stocks like fibonacci does this logic that repeats all the time the one element is the sum of the previous two so we have just a very uh a lot more complex logic

about the cpu iterations that uh needs to decode the instruction to understand what it tries to do and to update the registers and access the memory and for the next cycle when the white paper is released you'll see all these details a little better than what i can explain to you right now in a few minutes sergey asked what is the field well if it i think someone asked a similar question we use a specific prime defined field is multiplication

modulus and big prime about 250 bits um alan was asking does cairo relate at all to tiny ram uh it doesn't really relate to tiny remnant anyway was some i'd a version of a computation model that can run a general computation but it's not related at all i would say um isaac or kev asked again and i know that you probably don't want any others but will it all be eventually open sourced it seems

a lot of questions about this so yeah actually some of this will be uh open source as far as okay i don't want to commit if all right or okay if i commit then the people will hit me but i think the vm part and the compiler and things you can run it to your place and you can obviously the verifier is all is open because you can see it on the blockchain right now so you can see the the verifier and all the air the mathematical constraints are there

in the blockchains you can see right now uh my colleagues shouldn't hit me yeah but they do okay yeah cool should it be efficient in solidity well the do you mean the verification insulative because the verification solidity is a similar to other errors it doesn't uh because the constraints of a car are actually quite simple so it's not a very expensive to verify in solubility

if you mean to run the virtual machine commands in solidity then it might get more expensive yes i think the idea is just to verify the proofs instability and not just run the instructions directly yeah that's actually a question i would have is this is this sort of built for one particular network in mind or is it really built as an all-purpose no cairo in its core is a general it doesn't know ethereum it's just general framework to prove a general computation things and get some succinct proofs for it uh for example we all also would like to

uh okay everything you can you can do in your computer you can use it to just create a proof but we have also some layers on top of it that help it interact with the blockchain oh there's some continuation about the solidity question sergey said it was about the field selection and solidity i believe i hope i'm understanding that yeah it was should it be efficient in solidity uh it was about the field selection maybe actually sergey if you want to rewrite that question maybe fully then i'll i'll ask it in here yeah okay um yeah okay i see buddy next question i want to answer

uh two maximum degree of constraints okay okay that's what is the maximum degree of constraints in cairo yeah two exactly two okay got it got it um there was this interesting question are there any use cases where i should not use cairo if you don't want to create a proof for general computations don't use cairo if you have some tasks that is important for it to be very efficient and it is repetitive in nature and it's not very very complex it doesn't have very complex logic for example maybe just a uh verifying

this stupid computations in a lot of times maybe some hushing a lot lots of hushes and that's it then maybe you should use a the handwritten air version so probably better carol is more for a complex logic [Music] things ivan was asking could you expand on non-determinism what does it mean in practice to guess the position of some element in memory uh it's hard to explain it but not only but generally it means that you won't need a lot of instructions to a to search for an element in a in a list like a the approval would have

to do this work obviously because we can't ask i know god something like that but the approval will search for it and uh the instruction that we will actually enter the the proof will just be like very very few it guessed the position and and that's it so in terms of the uh the algorithms of the all the ld we talked about which are the major time things uh it won't go into them and it won't go into the proof size dara was asking is the cpu design parameterized i think i said that right so that it can be specialized for the circuit

uh it is parameterized uh yes a cool feature we also have i didn't mention that we can take a bunch of programs maybe even unrelated and put them in the same proof so we have like one pro program second third even if they're totally unrelated like one is transaction the other is fibonacci and then after the trend we can choose the right parameters to do all of this very efficiently isaac was asking can we swap out the prime for a for another one with a sufficiently large binary root of unity a gary yes yes you can

bobbin had another question about field was it 256 bit prime or is it smaller and then a bunch of people yes so what is it 252 bits 252. dara's asking would it be possible to use prime fields that match those used in other proof systems so it's sufficient to use the same embedded curves uh well our prime like someone said has a very uh [Music] it needs a have a root unity root of a very large power of two way order so no

uh isaac you just added but in your code but i don't know if that was referenced in your previous question if you want to write if there is if it is maybe just write out that question again because i'm trying to link them together anyway um dara was asking would it be possible to use prime fields that match those used oh yeah that we just did this one right um bobbin actually where are we let's check keep the questions coming if i've missed your question by chance just put it again because i'm trying to follow this as well as possible so isaac question okay so isaac said that the question about in your code had

something to do with dara's question but i'm not exactly sure [Music] what that would mean so yeah are there any other questions about cairo i i mean i was kind of curious when you were talking about the use in like is it already being used in diversify or is this like a test realm like i i couldn't quite figure out how right now in production it is not used v1 but in all trust environments it's called the v2 and we are planning a an update yes very soon to use this cargo but the the contracts are as far as i know i

already mean it but i can check their in robson definitely so you can check it out there you might have actually mentioned this earlier in your presentation but what are like if you were to like just list quick benefits like why would they start to use this well it's like i said it's very hard to do some complex logic in an efficient way in current solutions this is the main benefit you would get you get something that is very much like programming in any other thing you you don't have to think about oh wait this is only a constant number of loops

i can't do this recursion and my program will blow up uh in cairo you just it's just like a very simple way like programming language you don't have to think a lot different a lot more different maybe just the fact that there is a a prime field except for native words but it's very similar to programming languages and if you want another benefit that we will play we plan to uh maybe have some service that you can all just say play with and it should be like very easy to just experiment with dka proofs yourselves just write some code

in the playground and press enter you get your proof something like that um kev asked this is kind of related if i'm using a snark currently to do a big circuit should i switch to cairo maybe i'm doing zk roll ups but there wouldn't it be switching to starks as well but maybe you can answer that okay so some of the drawbacks i mentioned in the dsls also apply for your stocks even especially if you're working with some of the existing frameworks that look like code you get the same drawbacks of a not able to do during complete computations and paying a lot for things

you don't actually use and another material drawback that you get in a lot of them is that you write your circuit for a certain size of program it can't put a large instances of the program and in this area need to write a new one and all these are drawbacks that exist in some of these current tools and don't exist in cairo bobbin's asking what is the reason for not using smaller primes 64-bit 128-bit well 64.

exactly i think it's just a less than what we we need uh for cairo uh we could use a 128 but we use a bigger primes it lets us do more easily our hashes that are 250 something bits it can be done but currently we just do that not a lot worse isaac i think is joking what do you think would you consider switching to this prime two eight nine four eight zero two two three zero nine three you smack your your your work i i promise i will consider it

[Laughter] ah he says this prime has i think two to the 32 root of unity not joking okay uh he wasn't joking sorry okay okay okay so these are great questions i'm trying to think if there's anything else that we could talk about since we have shahar here with us actually shahar maybe i i mean i'd be a little bit curious to hear about you getting involved in this project like what led you what were you doing before that got you working on this particularly this is such a podcast question by the way i'm sorry like i said at the beginning we did everything manually we

worked a lot to develop our framework and do things and like it's a thought that we all had at the time that things are very hard to to create right now when we need something better we need to give to some of this complex logic that we just near impossible without it so uh no it's it's an idea i'm not the only one doing cairo it's leo goldberg did a lot of work and a lot of other people in in stockwell and like we had a lot of uh design this uh table showed before what the consideration is these are all things that we had like a lot of meetings about and trying to think what is the most efficient

thing we can do in cairo and and no it's it was sort of a passion it was fun very very fun to create something like this and it obviously paid off we were working on it like a lot of times and like over a year a year we were working on this project maybe even more and then we see the fruits now yeah that's amazing so if there aren't any more questions which i don't think there are then i guess we can wrap up the section um we unless you wanted to say anything else but no way thank you all for listening you've been a great crowd yeah thanks so much for all these

questions it was really great oh oh then we got a few more okay we got two more and i've been asked this again and this is a question that is again about the open source how can we verify what we're proving if it's not open source well first of all like i said the verifier is open you can see exactly what it does in the logic these equations it verifies you will have the the compiler and the run so you can see exactly the instructions that come out of your program when you're approving it and yeah if the verifier if it works then mathematically this is a

this verifies your statement cool and kev kev has one here um yeah this is kind of related right so if i were to make my program using cairo would there be parts of the compilation project a process where i apparently need to trust darkware no you don't need to trust soccer at any point you can uh first of all the part that will generate the instructions like i said it will will probably be open source you can most likely be open source you can see the instructions of your program you can see the verifier so you don't need to trust anything

yeah the compiler should be will be open source you need to compile your programs and the vm will also be open source and you can so you can generate the instruction list and the trace of your programs very cool by the way shahar i don't know will you be sticking around the event for a little while yeah where you are but later on today we're actually doing something called on gather.town where you can actually we can go up and meet other people and i feel like there's quite a bit of dialogue happening here and so if you can stay up i know it's a little bit late but it would be great because i think

people have more questions um but a lot of these seem like they're kind of deeper conversation and maybe something okay very good well thank you again everyone um i think we're gonna wrap up here and um yeah we'll be back on this stage in about like 12 minutes with john adler and we're going to be talking about zk roll ups and optimistic roll-ups very cool thank you