ZK12: Sonobe, a modular folding schemes library - Arnau Cube

Transcript

[Music] hello everyone and thanks for being here I'm surprised that like there is actually people like because there are very interesting talks in the main stage and side pH uh so yeah so today I'm I'm here to like uh talk a bit about uh folding schemes and and sonov uh the idea is to First U give a bit of motivation and and introduction to the ideas of folding schemes and and the building blocks to to build the IBC and and how to end up verifying this stuff um and then to talk a bit about like the sonov library a bit of benchmarks and and and the like the the main idea behind it and so on so first of all as a

bit of motivation uh we are in this like snar system snark world where uh we care about like proving like uh computation and sometimes hiding stuff usually the way how we do this um like snark uh programs is that we want to be able to to prove um some this uh set of constraints that we Define as this program which on language and and IDE is that we want to prove this a set of constraints that we encode as polinomial as a as a simple example like this R1 CS rang one constraint system um we have this like Matrix Vector uh operations that we kind of um translate into like some polinomial with the qap and then once we have this in the shape of polinomial uh then we can use um a

variety of Tricks uh in the cryptography realm so that we can prove um like uh the relation of those polinomial with some um witnesses that satisfy the relation and so on for example like gr 16 Marlin Spartan whatever um so those are like examples of like different like uh snark zik snark schemes uh that allow us to prove these polinomial relations uh tldr we want to prove polinomial relations so like just to have this uh Fier Insight uh towards the the folding ideas then why folding the idea is that um when you have uh some kind of um shape in your um computation that you want to prove uh in this those Asar

programs that uh require some repetitive computations this end up taking big circuits which translates into large proving time and in some cases also it takes uh too much memory and cannot even be computed or if you have like a some limitation in terms of like the device that you are using to prove um this stuff it's like it it it might take uh too much memory for example like if you want to prove a hash chain of 10,000 sha 256 hashes like uh I hash this input and then the output I Hash Hash it again and the output I hash it again and so on uh 10 10,1 100K uh iterations of this this ends up taking too much uh like uh constraints in the a1cs example and with most traditional ARS uh if this grows

enough um this takes too many constraints and it's not feasible like in in in in those um cases also if you want to put for example like the ZK VM um you need to do some extra like uh acrobatics to because like and also the thing is that the op code like you are um iteratively proving the same op codes again and again and again so like the same um set of constraints that you are proving again and again and again so one way to to to to kind of like uh cover this is with a traditional recor or how Justin calls it Brute Force recursion so the idea is that we verify inside the circuit uh the proof of the same circuit uh being proved in a previous itation so here you have this this like this will

be like the circuit layout and you have the the part of it is like verifying the new instance data in in this case it's just verifying a signature or could be like Computing the hash or whatever and then also you have part of the circuit that is verifying the proof in this case grow 16 the issue with this is that um the verify grow 16 proof within a circuit of row 16 with R1 CS uh ends up being a bit expensive like some some millions of of constraints um so that that's a bit of the motivation on why we are interested into folding we use folding but we use it in this uh um context of IBC but also sometimes with u PCD like um proof of carrying data here the IBC stands for incremental verifiable computation comes

from a paper from the 2008 from Balian and the idea is that um I we can prove that applying n times some function f which will be the circuit that we want to prove um we apply n times this function f to some initial state after after any iterations we obtain this final state so that's kind of the mental model of of the IC and this is like the kind of simplified view of of of this where it's basically like like you compute F applied to some z0 initial state with some extra winess and then to the output of this you apply F again and you apply F again blah blah blah Etc until you have applied this end times and then you obtain some State and you put this together with some proof that

proves that uh that this this relation holds after these n iterations which could be like this hash thing then um this diagram will be appearing uh many times Well three more times during the slides just to have the context where we are at each at each moment of the of the slides so the folding schemes pipeline or kind of anatomy the idea is that you have the circuit that you want to fold um you kind of um input this as a through some frontend interface um this is what gets you from the ZK language defined uh circuit to some arithmetization then we wrap this circuit in into kind of like a an augmented circuit that this wrapper for for the folding and then this is fold uh

through the IBC uh shape of um doing things um end times and after these end times we actually compress the IBC proof through the deider uh this is in the high level now we are going to dive in in each of those parts um so first of all a bit of Rec on folding um I will focus on into the Nova folding because it's like kind of the simple one to to explain now but we'll give a bit of intuition also in hypernova Proto Galaxy so the idea with folding is that as as we said at the beginning we we care about like proving polinomial relations so one thing that that we well that Nova proposed um is that um usually you prove the polinomial relation but

also you use some tricks so you commit to the polinomial and then you work also so with the you need to deal with the commitment to the Pol polinomial so here we use homomorphic additively homomorphic commitments and the idea is that uh in this example is like using Pon but you could use kg commitments or stuff like this and the idea is that um if you do a random linear combination of the polinomial and on the same time you do the same random linear combination um so V and W they are two original polinomial um and then um this R is just a random value some Challenge and then you basically do a random line combination is like V plus uh the W multiplied by R and then you obtain this

uh y polinomial if we do this in the polinomial or in a vector and on the same time we do the same operation but with the commitments to this vector or to this polinomial um the obtained uh polinomial or vector and the obtained commitment uh will still hold the relation of commit commitment between them so doing this operation in one side and then um just doing the commitment to the why obtained here will will obtain uh will result also into getting the commitment of Y this is like the the kind of the one the key idea of of this uh random linear combination which is uh Nova and some other folding folding schemes u based on on that this is the the idea then if we try to apply this to

to R1 CS instance because in in in our case we care like folding those polom relations uh it could be R1 CS it could be plish arithmetization CCS stuff like this right um if we try to do this um we will not go now into the details but like you end up having some inequality with the plain original R1 CS so the solution that Nova proposed was to relax the R1 CS so instead of like the typical a1cs uh relation we work with this uh relax a1cs basically the main difference is that we had this U term it's a like a a scalar and then this is like a vector of of Scholars this e which is the error term or slack term depending on on the paper and then we have the witness

instance which now it's not only the witness but also the error terms this vector and then we have the commit committed instance which contains the public inputs this new U parameter and then the commitments to W and the commitments to e so this is like um what we deal with in Nova uh very recommended the in the Nova paper in Pages 13 to 15 this is explained very well with like first attempt second attempt third attempt and and so the the paper guides you through the logic of why we do this the thing in in this way so then once we have this um rela1 CS relation uh and we have this idea of uh random linear combinations we can put things together and we can build this kind of a protocol where the pro and the verifier interact

in a way that later will be transformed through the fistic into a non interactive protocol but the idea is that they both will fold those instances that we have for a valid uh Witnesses for the R1 CS that we are checking they will both uh fault like random L combine those things in in a way that um the the verifier and the approver will obtain the folded committed instance like the commitments folded from the two original instances while the prover also obtains the witness to this folded committed instance so the folded witness so the idea here is that um both will start from two valid instances and well two valid commit instances the Prov also will have two valid Witnesses for those

uh respectively um committed instances and then both will end up uh comp Computing those random linear combinations this is very simple math it's just like doing additions and multiplications of vectors of itive cure points or or justed scalars and then um the obtained folded uh like random linearized uh instances uh will still hold both the relaxer 1cs relation and the uh commitment relation the idea here is that we are kind of like reducing from two instances to a single one so that that's kind of like the the the power of of folding so at the end we need only to to generate a like a a snar proof for one instance instead of the two original instances and if you do this end times so you are kind of like

accumulating or aggregating those uh n uh different instances so the issue with R1 CS uh is that when you try to do this with more than one um uh sorry more than two instances if we try to fold 10 instances the issue is that here there are some cross terms like the this T parameter uh well in in some of the places here done up and and the thing is that this will grow like linearly um as more instances we try to fold do like when you try to do the the math of the um random linear combinations so so this um does not scale well but then some papers appear later like hypernova protogalaxy and and so on which uh provides solutions to be

able to fold uh multiple instances so before we were talking about uh kns like non- interactive folding a scheme uh now we talk about nymphs which has this m which is stands for the the multiple uh instances um so non um interactive uh multi-folding scheme uh the idea here is that in hypernova we we use some S Check tricks and and and so on with multilinear extensions and and the and Hyper Cube and so on and Proto Galaxy uses the L basis but also has a variant in the paper uh explained where they say if you have more than K instances to be fa it might be worth also to to use Sam Che and and multilinear tensions so basically the idea is that uh with those papers uh it

allows you to fold more than two instances per folding step um just a a bit of like um visual um idea on on on how this looks this is like in in the hypernova we are the first one is like 2 to one folding so we are in uh we have the running instance and then the incoming instance we just fold them and then we obtain a new running instance and then we will fold this again with a new uh incoming instance and we will obtain a new running instance and we keep doing this on and on this is two: one then hypernova allows us to do this k21 fault where we have still the running instance but then the incoming instance you can have a bunch of them so you can have like 10 or whatever um and you keep folding them so for each folding step

you are kind of like folding more more more stuff so just do so in the same way that we were saying that in in in Nova the folding scheme is based on just doing random linear combination so it's just like you take this Scala and you add it to the multiplication of the other scalar multiply it by by R and you obtain the new thing and all this thing apply to all the parameters of the instances you obtain the new folded instance that is basically like a random linear combined from the two previous instances in hypernova um we use different tricks uh also we we use random combinations but also we use Sam Che to provide a um like a better consistency on on on some things which

ends up allowing us also using the multilinear setting and and so on allows us to have this like M multi folding uh that we can fold uh multiple instances per per step this is a screenshot from the paper and in protogalaxy also different tricks um so hyper protogalaxy are a bit more complex than the Nova way of of folding but at the end is is like like building blocks that we have also on other snarks in fact hypernova uh the tricks that is doing this here uh is is similar to the Spartan uh ideas which makes sense because the authors uh are like almost the same so yeah so recal this is the the diagram that we already saw um we have this folding schemes pipeline we what we've seen now

these folding SCH schemes that we do the random line combination or the S Check depending on the on the folding SCH scheme the the idea is that we don't run this as a interactive protocol we run this as as this non interactive through the fistic and in fact the verifier of this protocol we um encode it inside a a ZK circuit which will be actually the circuit that we actually fold so it's a bit of like Inception but the idea is is pretty simple it's like we want to ensure that when we fold the things uh the folding itself is well computed so the way is like since we are folding already uh some circuit uh we will encode the the kns verify like the folding scheme verification uh which in the Nova Cas is just doing these random

linear combinations uh we will do this also inside the circuit uh in in in a way that we um in in the circuit is we are enforcing that this um those operations are are well done and also um so we have the this is the circuit that we want we want to fold this F circuit so we wrap it in in this augmented F circuit is this wrapper this is the folding scheme actually that that sorry the folding circuit that actually we we we will fold which contains the the original circuit the F circuit the ni verification which in the Nova case is just doing random l recombinations in the case of hypernova is doing Sam check and and and some other stuff in protogalaxy is dealing with the lrange basis uh instead of random linear combination we do the linear combination

using the larange bases or Sam depending on the variant of the Proto Galaxy and then also we need to run some hash uh checks and some other checks so kind of we WRA the f circuit into this augmented F circuit adding these other like checks that's the main idea so now we have the folding scheme how do we ensure that or how do we build up uh an IBC uh uh layout from from just the folding scheme so we need to ensure that each folding step the NS is correctly done we do this through this um NS verify um also um yeah um the main idea is this and and we need to run also some some other hases

and and and and so on so um yeah yeah in the case of of Nova this is doing uh this um this packet here NS verify this is doing um scalar field operations which are native in the circuit that where we are working and also this means uh doing um group operations from the elliptic cures which is point operations uh in in hypernova we also have this plus the S Check verifier which also contains like the expensive part is like the hash that you need for the transcript of the S Che and then in protogalaxy is like also similar but also with the L bases involved and and so on the issue here is that um we need to run this circuit over the fce curve

and and this NS verify needs to do the random linear combination of some points of this elliptic curve uh one the issue here is that the the the litic Cure operations uh involve uh doing operations of the um coordinates of the point uh which those are uh over the U base field of the curve of the group um and and here the circuit we are dealing over the scalar field of thetic curve so then this is what we call the non-native or um yeah um fake no wrong field arithmetic or um different names but it's like the nonnative arithmetic so doing nonnative arithmetic inside the circuit of snark is very expensive so what Nova proposed uh is that uh they

will mirror the entire circuit this wrapper Circuit of the folding they mirror it into a secondary curve like fully duplicating the entire thing here and then this circuit in inside will be doing the the whole checks and folding and so on but this will be uh Computing natively the point operations of the circuit on the first curve and then the Circ in the F Curve will be uh like checking the point operations of the secondary circuit in the second curve the this is fully duplicating um some a couple of or one year and something later cycle fault appeared um and cycle fault is so just so you can appreciate the difference is is almost the same but uh we are reducing from duplicating like

mirroring the full circuit into just having this like a smaller circuit where where we just do the the specific computation and and yeah but that's I mean some details but that's the main idea uh that and in in son we implemented cycle fault and we use it for for the three other schemes that we have like the Nova hypernova and Proto Galaxy we are relying on on the cycle fault ideas this is actually how the circuit looks like in Nova so the circuit that just to provide you a bit of like intuition on on on what's going on this F here is the circuit that we want to fold this is the actually circuit that as a developer I want to fold this circuit that verify signatures or hashes or whatever this is the F here then uh the ni's verification this randomly Rec comination or or other

stuff um is this one this box and the rest of things are just extra checks extra hashes this is doing the KN verification of the cycle fault circuit um and some extra hashes so this adds as you can imagine this adds some extra overhead on the folding so if I want to fold a circuit that has 100,000 constraints this F circuit has 100,000 um once we wrap it in this uh rapid folding folding circuit this AED circuit this uh adds an ex of in in in this unoptimized case it it takes about 50,000 constraints so this would end up being 50,000 constraints so it's it's

one thing that we um take into account when when we do the folding um the full diagram is in in in in the sonov documentation then okay so we are here we just seen the IBC now we are going to see this final stage of the decider so the thing is that we keep folding using cycle fold uh and keep moving between cures and at the end we end up having three instances which these are the the the the witnesses but also the commitments to the instances that we end up having folded after an iterations so if those satisfy the relation of the relaxer 1cs and the commitment relation this means that all the previous um folded uh instances that we've been folding uh at

each folding step uh they were also satisfying the the relaxer 1cs ation and the commitments so the thing here is that uh those are quite big like megabytes of of data so the the idea is to compress them through a final Zar proof those are the checks that we need to do in in this decider theid the name comes from some of the papers and it's like it decides if whether the IPC proof is correct or not another way to to refer to it is this compressed snark final proof so we need to check uh some uh folding verification some extra checks with some but then the correct relax1 CS relation um and the commitments for this final

instance and the same for the cycle fault uh instance the thing here is that this is over the first curve those are over the second curve so you can imagine that this um brings some issues when we try to converge things into a single snark so those will be not native and this will be native but this is like if it's Pon this might take like five million constraints or so on so the thing is that in in the original Nova they modify Spartan to also use the commitment to prove the commitments inside and they generate two Spartan proofs one for each of the curves um the thing is that in our case we were uh aiming for verifying the folding scheme in in ethereum and as as you know ethereum has some limitations uh or some

constraints restrictions and so we can for the moment we can only use the BN 254 uh curve which has the pting and also we get would like the gas the gas costs so we needed to do a bit of gymnastics to verify the the folding proofs in in ethereum so those are the checks that we will do in a normal setting that we could distribute those between different like the two curves so things are native this is part of the checks that we do for the onchain decider um here you have more details but it's in the in the in the Docks but basically it's like um instead of doing Pon commitments on both cures one of them we do KGC commitments along all the way of the I so at the end uh instead of needing to

do them non-natively in the circuit which will be prohibit prohibit um we do them outside of the circuit as kg directly in ethereum um which is not so expensive so yeah this is the idea so from this final um iteration of the folding uh some of the things are proven through some growth 16 and then uh the the commitments some of the commitments are proven through skg so at the end in the ebm we solity we verify two KGC proofs and one growth 16 proof so okay so just to wrap up uh all this stuff is like okay um how to use it so we we've been for this past year in this joint effort between zero spark where I'm from zero spark and and PSC

where uh folks here are are are in in this room also um so this joint effort between Z spark and PSC we've been building this uh Sono Library uh son is a concept from the origami world so since we are folding it was a fun uh word to use the idea is that we have this um library to to to add and Test new folding schemes because there was this period of time where new schemes were appearing every few months so was like okay we want to be able to uh quickly iterate and Implement them and and and and reuse part of the code and so on uh compare aples to aples and and also that researchers can easily add their own schemes for example the nether me research team publish this MAA paper and for the paper they implemented the MAA uh scheme on top of the the

implementation that we had so and now they open it a PO request uh so now in son we also have the part of the Moa implementation and also so this is for the research part but also we were trying to make it easy for deps to to use the folding the idea is that uh as a developer you just need to care about the minimum code uh like PL and fold uh also thanks to arworks it's easy to switch between folding schemes and curves also supporting multiple uh circuit languages like artworks and and and Noah come and no name remark important remark it's everything is very experimental and unoptimized so uh just if you use it just for experimental things um the the developer experience is just like you define the circuit to

be fold so this was the first part is the the pipeline but this is like the actual experience of of the de developer so you define uh the circuit to be fold um satisfying some interface uh you can do this with different Z languages then uh you give this to the folding engine uh you do n iterations of of the folding with the ABC and at the end you can generate the the descided proof which you can choose between uh generating an onchain or offchain proof the onchain is for ethereum and and also the library generates the solidity verifier that you can deploy and then you can verify the proofs so the current status of the library is that we have the this the the the schemes implemented uh like fully implemented which includes like you can

do the full the full flow with Nova uh hyper nova and Proto Galaxy all of three using um fold and recently um we started to add the Moa and AA variations of Nova those um variate uh the Nova uh random line combination um avoiding uh dealing with the with in some way with the error terms um so we have this started the next thing is to add for them like the folding circuit the IC the deider and and all the pieces and also as as frontends like the the the by default we have artworks because it's like the entire library is built on top of artworks but as experimental we have circum no and no name so just very quick um maybe we don't have time but we started late yeah okay but it will be

just 30 seconds so just as an example um so here uh there is a bit of boiler plate but the IDE is um okay so here we I hope that you see it but we can zoom a bit um so here we Define that we want to use as folding scheme we Define that we want to use Nova with some M curves uh with kg commitments and uh for for the first uh cure commitments and then Pon commitments for the second cure commitments if we like to not use kcg because uh some uh thing we can just uh use the same thing but here I SWA the kg by Pon for the F curve or now I say oh no you know um I already have Al the code working for Nova I want to try now

hyper nova so I just do this or if I say if I say uh no okay now uh protogalaxy uh the same and here you Define the the commitments and so on there are some combinations that currently are not supported um like if you want to verify on chain in ethereum uh the the the proofs of using without the kg this is not possible um but but yeah that's the idea and and then uh yeah so here uh we initialize the folding uh this is the the initial state in this Cas this is this case is doing the the typical I = x^ to 3 + x + 5 um the typical example from the ballic uh blog post from maybe seven or six years ago uh this is so

okay we initialize the folding skip uh scheme and then here we do three iterations of the proof step for three iterations it's not worth like in terms of like the time that you need and so on but you would here do I don't know 1,000 something like this but anyway so you you just call this proof step and this internally this builds the this wrapper folding circuit and and it will fold it uh using the whatever um folding scheme that you choose uh in this case we are with Nova then uh you obtain the IBC proof and then you can just verify it then uh you will get also that this proof is some megabytes of of data you could still compress it with zip or something like this but then what you do is you define some decider which is this final Pro uh and the same here thanks to

artworks modularity you can uh just swap it in cures or or or the the the commitment scheme even here now we only support growth 16 but eventually uh you could put here the Spartan Pro uh if it fits the trade of artworks of snark and then yeah uh just um decider proof and de decider verify and furthermore if you are using the unchain decider you could also here like uh generate the solidity code uh that allows you to to to verify on chain so last uh slide because the last one is just links um some numbers uh again remark uh this is um very highly experimental and unoptimized code

and and just for kind of research so don't don't expect to use it in in in in in some project that will depend on it uh so the current folding step with a small circuit and and using the the pasta Cur like the palas and besta it's around 300 milliseconds um this is um amortized as as your folding circu uh is bigger so when your folding circuit is very small since we have this overhead in The Dropper folding circuit the AED circuit um thinks uh so this in fact this 50k uh so if if your circuit is 10K uh the 50k of the overhead uh takes most of the percentage of your actual uh full folding circuit um so you need to design

the your system in a way that this 50k is a small part of your full folding circuit then the of shine desider proof this is uh the current na implementation is less than one minute but then the thing that we was kind of the objective of this project was to be able to verify uh folding schemes on chain um uh because so far uh there were no options so the this final circuit that that we Pro to verify chain is like around roughly uh 10 million constraints it takes like 3 minutes in this uh like uh ThinkPad um and this is unoptimized and then the gas cost currently is around 800k of gas uh it's basically like two KC proofs and one growth 16 proof and the idea is that

you can do some tricks hashing the public inputs but so Bing the paying check and ideally uh we could be able to reduce it to 500 K of gas or or less and again this is the the cost to verify this uh this very very big uh kind of like iteration of of proofs that you are proving that after applying n times this function f to this initial State you obtain this uh final state so yeah so that that's it uh uh I uh I hope that in the documentation website you can find uh a bit of more like insights on on the ideas so so there are two sections one is like how to use it and then the other section is about like uh some design choices that we made like the the circuit or the decided approach and and and so on this QR code points you to the

repo and in the repo you have all the links and yeah so that that will be it thank you [Applause]