A SNARKs Tale: A Story of Building SNARK Solutions on Mainnet | Devcon Bogotá

foreign [Music] so the next talk is going to start in a bit it's going to be a tail a snark's tale a story of building snark Solutions on the mainnet by Savvy Accord from from the graph uh but before we get ready uh does anyone have any interesting snark Tale where's the do people do people actually use uh zkps here uh in any like user way or is one person that's nice could you could you tell us could you tell us your snark tale what is it what is your first time you know just sit backs close your eyes and and tell us about the first time you ever use a snark oh there's he doesn't have a microphone but I'm going to I'm going to run there well to to send the transaction on the media Network which is a ZK um layer one nice that was a that was a nice and not push at all shell of Mina uh um but yeah appreciate it thank you for sharing uh so so yeah finally please welcome on stage Savvy uh from the graph [Applause] all right thank you yeah so uh I'm a cryptographer at semiotic labs and this is a joint work with Jackson blazinski from Edge node except we're core developers from the graph and basically we're just kind of going to walk through one of our stories of uh trying to you know build Solutions using snarks and then actually running them on ethereum mainnet so first I think everybody here has at least heard of a snark um so let's just kind of quick recap of the main character of our story this is the you know the expanded acronym of snark succinct non-interactive arguments of knowledge in particular what we care about is the sickness property of these snarks so it's kind of like that computation compressing uh the scalability solution for ethereum uh those properties one like notable Omission from our uh from our snark here's we don't have the ZK piece and so in our Solutions we don't necessarily care too much about the ZK the Privacy piece which is like really this scalability piece that we're after um and also as I'm laying out the acronym snark I notice something that one of my co-workers 10 year old daughters noticed and she said shouldn't it be called a snack and she's not wrong so all right so our story every story has a challenge a reason for it to exist and this is our challenge um let's see you can't really see the bottom line there but that's all right the so basically what we're trying to do is we are trying to use a snark to uh resolve like one million independent payment channels within the graph protocol so the graph protocol the way that the ensure indexers get paid is they have an entity called the gateway and every time the indexer provides a result from a query you know they get paid some amount and so then the Gateway issues them a receipt that's been signed by the by it's been signed by the Gateway and then it says you know what's the value uh of your of your transaction right so the nice thing about the payment channel that the graph uses is that you can basically instantiate up to a million independent kind of payment channels right and these are all asynchronous so the Gateway can just be firing away receipts as the as the indexer is serving queries and so the indexer ends up with a bundle of you know say a million different receipts uh and their total uh amount that they're owed is kind of the sum of the total value over all of those receipts and so for the indexer to be able to prove that you know they're owed the total amount that they're owed they need to somehow prove that all one million of these receipts uh have valid signatures that none of these receipts have been repeated and that the total value adds up to the total value that they claim that they're owned and so one way they could do this right is they just take that bundle of a million receipts throw that uh on chain and then run some you know BL signature verification on all one million receipts but you know that's a little costly so we want a better solution and so the solution seems like really well suited for a snark right basically we want to take this computation of you know a million different signature verifications uh throw it into a snark that can say yes all one million of these are valid total value adds up to the claim total value all IDs are unique and then you get out just one nice little succinct proof with some claimed total value amount that goes on to chain and you run your snark verifier uh algorithm on chain and the indexer gets paid and so let's look a little closer at this problem and why it's interesting this table here that we're generating right this bundle of receipts we've got a million different receipts and so whenever we talk about snacks there's always this talk of like okay what circuits are used to verify your computation and all that type of stuff so basically our circuit needs to take in uh easily needs to prove one million different signature verifications so initially we're thinking about using BLS signatures you can maybe see that a BLS signature can be uh proved with the circuit of size say two to eight if you wanted to prove all one million of those transactions with this size to the eight circuit you could just take that to the Circuit copy and paste it and then you have some huge uh size 2 to the 28 circuit that you're going to be using in your snark to verify and and to prove and verify and so what's interesting about that is 2 to the 28 is about the biggest circuit size you'll see right so in all the literature and all this but people run their asymptotics and they go up to size 2 to the 28 and we haven't really seen much bigger than that and so already we're talking about trying to prove statements that are at the edge of what people have have used another really interesting thing about this primitive is we're trying to use a snark as a black box so really we're just trying to get incorporated into this payment Channel protocol and we don't really want to have this snark impose any extra requirements on the protocol itself right we just want this snark to be this black box we plug in a scalar table we get out of proof that proof goes Unchained you can verify it and you don't really impact the security of the system in any way based off of your snark uh and then yeah the final thing here the business side of of this oh yeah can you make this whole process of proving and verifying costs less than thirty dollars otherwise it's not very useful to the indexer so thanks go all right so so now we're going we got our challenge we're trying to prove this massive table of data and basically prove this massive table of signature verifications how do we know whenever we're done right how do we know that we've succeeded there's a bunch of different metrics to quantify snark performance we use prover time prover memory proof size and verifier compute so approver time is basically just it's the amount of time that the approver spends generating their proof right so in this case it's the indexer the indexer has their big table they're going to run this proving algorithm it's going to take them some amount of time to generate that proof prover memory this is like an actual physical requirements of the machine that they're using to generate this proof right so they they've got uh if they got a laptop with 16 gigs of memory you're not gonna the algorithm requires more than 16 gigs of memory you're gonna run into issues you're not gonna be able to generate a proof proof size this is the size of that proof that could spit out of the snark this is what gets sent on chain so this is obviously important right the bigger your proof is the more expensive is to store it and then verify or compute these are the computations that are run on chain uh in the verify algorithm and for the purpose of this talk whenever we talk about the verified compute we're really going to just highlight the most expensive operations that the verifier is going to run and so this gives us kind of like a quick way to filter out uh techniques and estimate gas costes and all that uh just another thing on this on these figures right we'll see them repeatedly this x-axis basically this is showing our statement size as it's growing right so we said we want to prove this big table of signature verifications uh the goal is to get to this kind of size 2 to the 28 instance and then by seeing you know how this how these uh these metrics Trend we can kind of get an idea for like engineering Solutions right and we get an idea how our problems are growing and stuff like that so those are our plots and now we start our story and I like maps and I like stories with maps and so we're going to have a map but a quick caveat about Maps is this is a map of the world in 450 BC it's accurate but we can tell it's not the full truth right there's a whole lot to be discovered still um so here's our map this is cryptography land as we saw it at the start of this program and especially in particular when we're looking at snarks so we've got kind of two major continents of snarks we've got transparent snarks and we've got these non-transparent Starks and so non-transparency arcs these are snacks that require some sort of trusted setup right so we saw yesterday when we're talking about dank sharding and we're going to have you know this kcg uh trusted setup ceremony that ceremony is what is required for these non-transparent snarks transparent snarks the idea is they don't require this kind of trusted set up ceremony um you can kind of run them out of the box so that's our map um now we say Where Do We Begin right how do we start this story and really the the when we started out we said okay one of these unique properties of the problem it's a black box like we said we don't want the snark to impose any security requirements on top of the system that we're using and so when we think about this trusted setup we can debate how like the Practical implementation the Practical implications of this uh trusted setup right like if you only have two people running the trust a set of ceremony you have to trust that both of them are honest you know as you increase the number of participants you know that level of Trust might change but the point is you're still making an argument right there's still some other additional argument that goes on top of the math of your proving system and so initially we said we want this thing to be as black box as possible we don't want to have to deal with those extra arguments so we want to start with the transparent snark all right so now knowing that we're going to be using a transparent snark where do we go from here and so we start by looking at our problem statement and we start trying to find you know what's the the next best snark to use the thing that's unique about this problem statement right is it's highly structured so basically we're kind of proving the same function you know a million times so if we could basically if we could kind of reuse these circuits right maybe we could uh significantly reduce costs either proof size verification time that type of thing and so in particular what we're curious about is we could come up with one circuit this is some f circuit that can be used to prove all of these uh snark things for a single row and so then if we could if we could do that then could we you know generate proofs for each individual row and then somehow like aggregate them all together and then we get some aggregate proof and the hope is that aggregate proof will cost only about the same to to verify uh as verifying this single small proof so people have been looking in stocks you can see where we're kind of going with this we are going to recursive snark land um and so in this space there's a couple of Primitives uh Halo is one of the big ones we hear about uh and there's there's talks on it this week uh but at a very high level recursive snarks it's kind of like what I was saying right we we have the idea is we have a circuit we want to repeat the computations on that circuit and then kind of like aggregate these proofs together and the way that recursive Stars tend to get around this in practice is you take your original circuit you can like augment it with some uh snark verify circuit so it runs the verify algorithm of the of your proving system and then you have some resulted F Prime circuit and then this F Prime circuit is kind of what you start chaining together to prove all of your rows in our case privilege rows with a Scala table and the the really important thing here is the cost to verify and like the cost improved size is really only tied to the cost for proving and verifying this this one F Prime circuit so that's really encouraging uh maybe you know we could uh significantly reduce our problem uh using this we use a primitive called Nova so it hasn't seen too much uh Traction in this community that I've seen yet but it's a it's a newer primitive it was presented at crypto this year uh the it's what it really has going for it is it can do kind of what Halo does but it has like the smallest constant size verifier circuit so we remember that F Prime we have that little verify circuit the Nova is is the smallest that exists in the current literature and it's constant size so it doesn't depend on uh the size of your original F circuit uh yeah just a note for in our case this this F Prime circuit ends up being about size 2 to the 15 and so this is this constant proof size and the the verifier work is tied directly to this kind of two to the 15. another interesting thing about Nova is it uses another uh uh IOP called Spartan and what Spartan does or it's its Advantage is it's a very fast prover uh and it it might still be the fastest prover in the literature uh it doesn't use any ffts and it also has a relatively efficient verifier um some more notes about Nova the actual open source implementation that they have they've instantiated it with with bulletproof's IPA so this is kind of like the expensive IPA that people talk about in the literature sort of expensive polynomial commitment scheme um but that is you know this bulletproof is only used to uh for a circuit of this size so you end up with a bulletproof instance on your polynomial it's tied to this size uh and then just another note on their open source implementation they're using these pasta curves so similar to Halo when you're generating these these recursive proving systems you have something like kind of unique uh mathematical Primitives that you got to use and so in that particular is called these cycles of elliptic curves and nobody uses the same thing that pasta does and it actually worked together on this so I think too surprising there what gets surprising now is whenever we actually start looking at our costs uh the first thing that we notice is these constant size here right so the proof size is constant this verify is compute is constant so basically what we're saying is as we increase on our x-axis here we're basically proving more and more rows in our scalar table and this proof size in this verifier compute stay constant because again the proof and the the proof size in the verifier compute are tied only to that F Prime circuit so we get this nice kind of constant proof size verify compute that doesn't depend on the the number of rows that we're trying to prove the prover time here this is pretty much linear in the instance size that we're trying to prove so linear in the number of rows that we're trying to prove because basically like the prover has to do the work right so in in this particular instantiation the prover is just kind of going row by row uh kind of proving and accumulating so you kind of just see this linear growth here um and so I mean based off the implementation that we have available you know we would estimate you know 51 hours to prove uh using Nova for a an instance as as big as we want to get uh that may or may not be a a fundamental limiter um but really what we see the big limiter is this verify compute so even though verify compute is constant uh it still is a very expensive operation that needs to run and so in particular it's part of this bulletproof's polynomial commitment scheme you have to run this elliptic curve multi-exponentiation and it's you know size 2 to the 15. so 32 000 uh basically up to the curve uh multiplications and so the problem really is nobody's going to work with pasta curves ethereum only has pre-compile support for one curve all to be in 128 and so this is kind of a famously known problem at this point um so if we wanted to run this verify algorithm we would have to implement smart contracts for pasta curves so that in itself is a cost that we would have to absorb uh and then if we did we would see you know based off of some people have done a similar work a scalar amount would still cost about 350 000 gas and so if we could use you know some algorithms for speeding up this multi-exponentiation we could get these these total costs down to you know 764 million gas or you know seventy six thousand dollars off of some uh estimate of gas to dollar ratio so clearly this isn't the solution that we're looking for um maybe there's some engineering things we could do we could take advantage of all bn128 it also has a cycle um but for now we'll table this and we'll go look elsewhere so where do we go from here um again we want a transparent snark and we would really like to use Primitives that can take advantage of you know things that are supported by ethereum so we look for uh Primitives that use Albion 128 Albion 128 is a pairing friendly curve so we're going to look for transparent stock Primitives that use pairings uh and we don't really have to look too far so Nova the same authors who wrote Nova they also uh authored something called quarks and so this is a another transparent uh snark primitive uh and in particular what's unique about it is they invent some pretty unique polynomial commitment schemes that use pairings but they don't require trusted setup and so they can get some significantly better performance than say bulletproofs uh from a verifier from a verifier standpoint so it's pretty unique again similar to how Nova was written they're using Spartan as their IOP so basically they take one of their polynomial commitment schemes either Copus or Dory pair it with Spartan and then now they have a snark uh the nice thing about them they've got fast and spaces fast and space efficient provers that's a property of both polynomial commitment schemes and the Spartan primitive the proofs are they're a little bit bigger than what you would get out of something like bulletproofs uh but they could be manageable and then the nice thing about them too they have relatively cheap verifiers oh yeah then just another comment there's actually some more research by the same uh kind of group of authors about Spartan that is used to prove kind of like simdi computations right so uh you have basically our scalar table right we have one circuit we have multiple inputs uh single input multiple data and so they've got some stuff off the shelf that can seemingly help us with our problem so we get really excited about this so let me start digging in to uh quarks and we want to use it and we want to try to try to build snacks with it the first problem that we run into is there's no open source implementation so that in itself makes things pretty challenging uh there's no copis nor is there a Dory uh PC although I was talking it sounds like there might be a door implementation uh available somewhere as of a couple days ago but I haven't seen it yet um so knowing that this polynomial commitment scheme is kind of like the primary cost driver for these snarks we implemented the Copus PC using uh the rust Arc Works libraries and then we ran it to get some some benchmarks right and kind of get some estimated costs uh and so these are the the results for Copus PC the one thing that we see in approver time now is is pretty nice right that's 565 seconds for the biggest uh incidence size that we'd want to prove so uh yeah that's nice uh the prover memory requirements you know the if you have a machine that has four gigs of memory you should be able to run this again this is our proof size so we're in the orders of kilobytes here right so the small basically at the biggest InstaSize we got a proof of about nine kilobytes and then this verify compute this is again the we'll see this this becomes the big problem um we're talking about doing electric curve arithmetic again sometimes how bulletproofs was doing the instant sizes are significantly smaller but there's still significant work to be done there uh to contrast copis with you know Dory which is the other polynomial commitment scheme Dory takes advantage of some pre-computation to reduce this verifier time or this verify compute work even further and as a consequence like their proofs are about three times bigger so just take these proof sizes multiply by three and then the verify compute is significantly less like we'll see on the next slide so Quark slick promising at least the polynomial schemes look promising on paper uh the problem is now if we want to start again running this verifier on ethereum the problem is particularly even though there's all bn128 support uh there is no GT exponentiation support so yeah and so uh yes that's that's a significant problem and basically we simulated we implemented some GT arithmetic we simulated the total cost and we got down to about 4 million gas to do one exponentiation and so a whole Dory verify would cost about 125 million guests or you know 12 000 so smaller but we're still not there yet and so now we start asking questions you know where do we go uh is do we really want to use a transparent uh snark uh let's go see what this plonk is all about that everybody's using so you know plot's very popular it's got a ton of support proofs are small verification is uh the cost is known and really what we'll see really importantly is uh plunk is supported the verifier is supported by uh pre-compose in ethereum so all of the the heavy arithmetic is cheap so we dig into Planck uh fortunately like I said Planck is so popular there's a lot of high quality open source implementations there's a lot of high quality uh blog posts describing Planck and we see you know the famous small verify compute small proof size uh the problem with pumpkin this is a known problem too and this is why everybody is trying to make this prover efficient and try to optimize circuits is this prover time improver memory is expensive so Planck needs to run ffts ffts require you know n log n work and they are also not space friendly and so if we try to prove just a raw two eight a two to the 28 size incidents we're looking at you know that that's 500 minutes so we're looking at like about eight hours and you need about three ten three terabytes of memory on your machine to be able to complete a proof of this size uh you could do it you could you know go to the cloud uh rent a gcp instance and you can get it done for about 200 um but you're not gonna be able to prove this out of the box all right so now we start asking our questions uh We've we started getting introspective we've surveyed we've surveyed some snarks we've flip-flopped between transparent snarks to to trusted set of snarks uh uh what are the important questions here so one thing that really popped up is why is Planck's verifier so much cheaper than say dory's verifier and so if we just look at the algorithms that are being used Planck's verifier requires pairings pairings require GT exponentiation so a pairing should be more expensive than a DT exponentiation and if you actually do the math it's uh in dory's PC should cost only about 16 times the uh what plant costs and so that's uh that seems like a reasonable trade-off that somebody would be willing to make if they don't have to uh run a trusted setup and so the the reality is as we saw the cost is about 500 times uh plunk uh verifier and so really it's this pairing check uh EIP and so one of the one of the big points that we're trying to take away here is we've seen that there are kind of cost competitive transparent Primitives in particular there are interesting polynomial commitment schemes these Copa schemes Dory schemes uh that could be useful but we're not going to build a room we'll never be able to run on ethereum being that because things are too expensive because they're not supported by say pre-compiles um and so one of the questions and this is kind of just like a a thought question right is ethereum ecosystem artificially selecting for snark Primitives with costly don't reflect reality we say ethereum is driving snark research uh and it is and we're seeing like a flurry of development especially for Primitives like Planck uh but is I mean the reason is it's cheap to verify and so the question is you know that costs aren't uh reflecting reality we want to address this question uh if there are other people who've kind of run into some other things like come talk to us we have ideas of how to address this um yeah with the last minute where do we go next right so we've gone all over the place uh We've surveyed a bunch of snarks actually there's a ton of snarks in practice right and we look at all of these this is this is this was our path but you know there's a whole bunch of places we can go uh the other point here is snarks generally we think of them as proving kind of arbitrary programs NP complete or mp uh NP statements that power as a cost there are other proving systems that have cheaper costs uh signatures are one such proving system so we sell away from the land of starks to the land of homomorphic signatures and so what a homomorphic signature does is it basically allows you to assign data and then if you like sign two messages you can add those two messages together and the result is a side uh message for the sum of the two underlying messages so it's a pretty cool primitive uh I haven't really seen it used much in practice but we have a unique application here on blockchain uh and so we can take advantage of that and run you know this this reference scheme uh and basically the the bottom line is we get small proofs small verify time similar to plonk uh these costs are about the same cost of aggregating just regular signatures so elliptic curve arithmetic um and we can get something done for you know less than 30 dollars quote I like it's worth thinking about um again this is we are Edge node semiotic labs for core Developers for the graph I'm with semiotic AI we're looking for people who are interested in these type of problems we're also looking for people who are interested in you know AI reinforcement learning all kinds of good stuff we're looking for people if this was interesting Reach Out thank you [Applause]