zkSessions: Shahar Papini on Cairo

21 May 2021 · 9:24

Recorded at zkSessions: The ZK Languages Rundown, Shahar Papini of StarkWare presents Cairo, the programming language built for writing provable programs for StarkWare's zk-STARK based systems. The talk is a short technical introduction to how Cairo fits within the wider landscape of zero-knowledge proof languages.

Speakers

Topics

Transcript

hi i'm shahar i'm an engineer at starkware and the co-creator of cairo and so i just want to talk about a why you should use cairo what it does well uh carol is truly complete from what i just heard it has a lot in common with the zinc and decay vm in the sense it also doesn't compile to a constraint system like the other things there is only a single constraint system a single air that verifies a cairo and basically when you compile

your program and you just compile it to where we our vm is actually cargo vm there is something else uh but we took uh some different trade-offs when designing cairo uh carol is i would say a bit harder to use because it uses a black release of a full field elements as basic types and things are your memory is immutable and you have a functional like language with a cursion but all these were designed so that it would be a lot more efficient and for each instruction

you get a whole an overhead of about a times 50 gates which is a bit less than some other things but i very much agree with what alex said that a lot of times the logic is a small portion of what you actually use so if you have a lot of hushes a lot of signatures a lot of things that we do have efficient circuits for then this might be negligible although there are some cases where you do want a lot of logic uh in in these cases i i think cairo is a better option uh but you know in other

things that it might be negligible um and okay here are some numbers of uh its efficiency uh we uh in f-star which is the open source version we can do over 10 000 hashes per second in improving system we did big batches of 600 600 000 means we will get uh like i said before there's a single circuit which means there's a single verifier which is deployed today on the theme that everyone can use and to verify every

program yeah it's very easy to get started if you want you know just go to this link here caroline lang and you know you have a playground which you just type code press enter it verifies goes unchained just play with it you have a lot of documentation and just take a peek it's nice uh other features which are nice is piggybacking um on the big players like immutable dyds diversified today they run on uh on the use cairo and they use the shared proving services of cairo which you call sharp

if you run today on sharp then you basically get the benefit of scaling from all their big batches even if you have very small programs that you want you get the benefit of their scaling another nice thing we have are a lot of tooling and the ide support so this is an example of how karma code looks like and we have user-defined structs and types and functions uh you know recursion calls and the dictionary accesses uh basically what you would expect from regular languages it is a special language called cairo

uh it's more of a functional language you instead of loops you use a function calls and requiring and memory is immutable and for better or worse it's also a minimum memory actually sometimes can make your programs a lot safer and this is an example of some of our tooling this is the compiler vm that you can interface with we have the solidity verify that is deploying deployed on chain you can use it today integration with ides we have a tracers and and we have a debugger actually today as well

profiler and playground you can see online in the future we plan to there are currently projects working on compiling from other high-level languages so you won't have to use the cairo language you know to benefit from the car of vm and everything else and plan to add the zero knowledge it's already expressible and cairo with zero knowledge just prove it right now doesn't support it but we will plan to edit a very big thing we want to uh go with is star connect which is basically a

permissionless generic computation l2 dk roller community okay it's like ethereum it's security is based off of ethereum because it talks to it and you can publish your a camera-like contract it will be a sort of dialect of cairo with contract keywords that they can use as contracts and publish transactions like you're used to ethereum and other things and also additional buildings and buildings led to uh do specific things very efficiently today we have pedersen hushes you know of our projects that plan to add other things but ketchup today cairo

is obviously live we have a lot of projects running with it with a big scale uh diversify immutable dydx this is a web page this is a discord and i hope that was fast enough yeah okay let's see that was very great and there are a couple questions here um one of the questions was how does cairo check that a load instruction from a given address is actually the value that was stored previously uh well it's it's it uses a technique uh i don't remember its name we plan to release that white people

soon but it permutation a trick that you have all the accesses on one side and all the sorted axis on the other side you prove it's the same permutation in the time solid axis you can see that if it was previously accessed then the next cell which is the next access is consistent this is what we did darath what other high-level languages are you planning to support first yeah right now we are okay there are a few way options and we are starting to work on uh going from things like haskell or idris

or other functional programming languages because it feels more natural for cairo it's what we have undergoing today bobbin was asking what would be what would be the overhead for prover time for execution for executing a program with or without zero knowledge in cairo uh there will be in nowhere negligible overhead it's like adding a constant you're not just a matter of developing it's it's basically adding a few random and strong random values across the tree somewhere it's a not an efficiency a multiplier cool um isaac asked for a link so maybe

that's something you can do after okay um and jordy asked maybe this is the last question i think and then we'll we'll wrap up but what's the current gas cost for verifying a stark on for verifying a stark proof it's about five million gas but it's mostly regardless of the size of the proof so we have like for example in the example the six hundred thousand mints it was uh about six million girls so ten guys per transaction if we put more things in the battery less got it you