zkSummit: Fractal, Post-quantum recursive snark - Dev Ojha (UC Berkeley)

Transcript

I want to uh welcome Dev uh who's going to be talking about fractal so please take it away hey I'm Dave talking about fractal postquantum recursive snarks this is Joint work with alandro kza and Nick Spooner so let's dive into it so as you saw in the title it's going to deal with curse of snarks so I'm G to say everyone here is familiar with snarks you may may not be familiar with Rec cursing them uh though if you saw like Michael's or pardon Michael's talk earlier today he started like going into this this recap so recursion here means verifying a snark proof within a snark so an example what this comes up is verifying iterated function application like f of f ofx equals y so here's an example

iterated function application and strategy for proving this is to prove it step by step so first you prove that F of Z equals Z1 and check this you just check the proof pi1 in the next iteration you prove that F of Z1 Z2 and that the proof Pi 1 is valid therefore when you check Pi 2 by induction you know that Z2 equal F of f of Z and so repeat the same process for the next iteration where you prove F2 equal Z3 and the proof for Z2 and then by induction you know Z3 is fully valid so recursion here has like uh some nice properties first like the size the

statement that you prove is going to be independent of T and the proof size is independent of T another nice property is that you can verify any intermediate state so you have a computation that goes on forever like a blockchain you can then verify the latest State you don't have to wait until the blockchain is like over before you can verify anything so so applications of recursion are succinct blockchains like Koda in that context f is your block transition function and uh like you one way to do it is typ the proposer prop uh include a proof of the block another applications like continuous verifi delay functions or snarks from ruce and more like see E3 search for many examples so that's one like some more of

the theory find recursion like The cryptographic Primitives that you want to build are incrementally verifiable computation IBC reply what was on the previous slide and proof carrying data PCD basically that's just like recursing on any sort of directed asy graph and so when can you recurse a snark well there's this theorem from a couple years ago that every adaptively secure Su sync verifier snark recurses so you take a snark you recurse it and you will get proof carrying data and moreover this like compilation procedure preserves many nice properties so a zero knowledge snark gives you zero knowledge PCD recursion sort of preserves your transa setup type doesn't introduce

anything new so if you have a circuit specific setup your PCD will still be circuit specific you have an updated will chust a setup your PCD you'll still have an update TR set up and you a transparent snark you'll get a transparent PCD system but what about being postquantum bcct says nothing about this so this is the first result of our work yes recursion will preserve postquantum security you start with a postquantum snark and you recurse it you'll get postquantum PCD and this is not a direct uh like straightforward thing from BCC one of the problems is that uh your Quantum adversary can create its own Randomness so in the classical setting suppose you

had a problemistic adversary what you can do is you can sort of fix its Randomness and make it terministic by essentially you set a seed for its Randomness and drives everything from that in the quantum setting you can't do this so the solution is to define a sufficient notion of like post Quantum knowledge soundness and to prove it secure like for our Construction in the quantum roral model so let's move on to like recursion and practice here's a set of many snarks and here are the synct verifier snarks so from like Theory we have that ASM totically all of these should recurse however empirically in practice we haven't seen this empirically we've only been able to get like practical IVC and

PCD from gr 16 plun Sonic and Marlin this is a very restricted set Like These Are all uh trusted setup pairing BAS snarks so what is it that makes snarks suitable for recursion are there like transparent snarks in the set are there like postquantum ones in this set also I want to add like as a slight note uh bullet proofs are now recurs with new techniques from Halo but these recurse in a different sense than uh like sort of way I showed in slide two like they still will achieve increment of airall computation but uh it be a different Technique we can elaborate more on this like in the questions later but uh that's all I want to like talk

about Halo for now you also do PCD oh cool good to know so next uh contribution is like we we' identify what it is that the property that made these snarks like recurse well and it's pre-processing so a pre-processing snark is one in which like your verifier is given a small cryptographic digest of your circuit and so now don't have to read the entire circuit so the next contribution is like for any pre-processing snark the cost of uh proving your cursor step is in a mathematical sense like effectively the same as proving your original circuit so here on the left is the time of proving

your statement plus recursion then uh it's this is a sublinear additive overhead the time to proving your original circuit like this a sort of categor this little o one term so if we compare this to the prior uh known method recursing what you would do is You' start with like a snark for a machine relation where the pre wants to convince the verifier that for this machine on input X the machine will output accept within T time steps and the verifier has to read the machine description so essentially as you go to recurse you have to keep on changing this machine description because you're verifying a slightly different machine each time and to get unbounded recursion you'll need a universal

simulator which means that you get a universal simulator overhead so this means that you blow up the statement the size of the statement you're proving by a multi factor and practice like it's at least greater than one in practice these are very large constants so uh this means it's a high overhead to like recurse a general uh snark so this tells us that like it's pre-processing that is made like PCD efficient and therefore if we want to get efficient PCD our goal should be to create a pre-processor snark so that's exactly what we're going to do the next thing we do is create a pre-processing snark for R1 CS that postquantum and transparent all prior

constructions of pre-processing snarks were prequantum and like required a chest setup so our constru fractal has the following astics these all match the best known like non preprocessing postquantum snarks so linear approver logic verifier logic proof size and like proof Pro times in minutes very times in milliseconds proof size is like stand regime for Starks in the 100 200 kiloby range but many people here are probably interested in like seeing some actual numbers and graphs for this and we have an implementation so we can do this so to run fractal you need to fix a random Oracle so we fix as Blake Tob and here I've plotted like fractal Aurora

Marlin Groth Aurora is like St Co Quantum snark for uh circuits Marlin and Groth are so they're like pairing based uh Starks so we see that Aurora has a linear verifier time whereas fral has a logarithmic one so we've got an exponential Improvement in time verifier time due to pre-processing and the constants for uh verifying this like FR uh fral proof are quite good they're in the same regime as Marlin and close to Groth like around 10 milliseconds in terms of proof size we're uh twice as big as Aurora it's around 250 kilobytes this is a nice exchange like now you get an exponential

verifier time Improvement I didn't plot like grth and Marlin here because I have to stretch the graph really far down those proof sizes are tiny like one to two kilobytes and then improver time uh all these grow the same way like n logn and uh the difference between the fastest and slowest snark approver is around like factor of 10 and and uh you know some of this could even like be explained by differences of finite field implementation Etc so now it's like going like recursing uh fractal so what you do is you start with fractal cre insure in the quantum random orical model you apply the random moralistic to get it as a snark and the random orle hero stick is

instantiating R Oracle with like a strong hash like Blake or Shaw and use security carries over and this is used in like an increasing number of snarks like some IC Marlin plon bulletproof Starks Etc and then you recurse it to get PCD so this gives you the first PC construction that is a post Quantum has a transparent setup and supports arithmetic over any large field so now we can use binary fields or fields that don't support secur otic curves uh and more so realize recursion for fractal first like the first step is always to express your verifier in language as snark understands so to describe

verifier in R1 CS which always leads to new efficiency considerations so to recurse growth you have to use pairing or previously have to use pairing friendly Cycles Li the curves a couple talks today suggesting new ways we may be able to avoid this and this would this induces Pro overheads so the fractal verifier has two components algebra and hashes and when we go to run this as a standalone snark it's actually kind of remarkable these are basically exact almost exactly the same but when we go to express this in R1 CS it's more like this hashes are over 99% of the constraint system size so the choice of hash function is really important if we use a standard hash like

Blake or Shaw that's optimized to run well in your Hardware use a simd etc it runs very fast like 200 NS but the number of constraints each one takes is over 20,000 which means when we go to just write down fractal we're going to have a system of size like larger than 2 to 228 we can't really run snarks this big so instead we have to use this new line of work called algebraic hashes which includes stuff like Poseidon rescue Vision MC more and now the time to do each hash is much slower it's around like 10 milliseconds because we're doing a bunch of finite field arithmetic but the constraints for every hash is much better like 300ish which

means our constraints size is less than 2 million constraints we can run this like uh as a general rule of thumb like your biggest cost of recursing a thing is going to be doing cryptography inside of your snark so like vation so we can look at how it runs since the hash is so critical the random Oracle I'm considering is Poseidon so uh here I've plotted the number of constraints that you're proving in blue against the verifier size in in Black it's like the verifier size of just uh expressing the verifier for your circuit not uh your circuit plus verifier so we see that this like

recursive overhead grows logarithmically as we'd expect and uh the crossover points at around like two million constraints are a bit under it so this like blue shade triangle sort of the feasible region of recursion taking a candidate point in here like uh a circuit size of six million uh the size the recursive of the circuit that proves C plus the verifier is around 8 million and terms of like concrete times of proving things this is a very small overhead and since like this black line represent your verifi size grows logically or very slowly the uh the size of your cursive circuit that proves C

and verifies aacy is around like your original circuit size plus 2 million constraints do you want to add couple important notes here that this Rec overhead is like an unoptimized proof of concept and the pro time here is actually way slower than Stalone snark sorry Stalone fractal because you have to do so many uh faidon instantiations for your Merkel trees but there's like a lot you can do to improve both these parameters like you can prove prove your time by and uh the recurse overhead but that's all I want to say on like the theorems behind and now I want to explain a bit how do you actually go and construct a post Quantum processing

snark so all snarks have these two parts an information theoretic proof system and a cryptographic compiler add these together you'll get a snark so as we want a postquantum snark we're going to use a postquantum graphic compiler since we want a pre-processing snark we're going to use what's called a holographic Pro System more than a second and by combining this we'll get a postquantum PR processing snark that'll be secure in the quantum Rand morle model and transparent so uh to explain holographic proofs first I'm going to go explain back to a PCP in a PCP the prover wants Quin verifier that for a circuit C uh it knows a witness W such that circuit on

xw outputs except so the verifier has to know what algorith is verify and theover is going to Output this uh large Pro p and the verifier will check it at a couple random locations and so because the verifier has to know what it's verifying it runs in time at least linear in C a holographic verifier has access to like an error tolerant encoding of your circuit so a holographic PCP is similar set up to as before the Prov outputs a large proof string Pi but now the verifier doesn't have access to the circuit instead there's this third trust entity called the indexer who does know

the circuit and outputs the uh encoded Nar to coding the circuit and the verifier to check the proof will query the proof at a few random locations and query the encoded circuit at a few random locations so since the indexer has to read the circuit it runs in time at least linear in C but now the verifier can run in time like much much less than C and now the indexer is a trusted uh party but what we're going to do is we're going to transform that into a pre-processing step as follows so first we start take our holographic PCP it convert to a holographic snark this is done using like the mall transformation where essentially you the pro like merkes as

proof string pi and hands a Merk rout to the verifier and whenever the verifier wants to query uh the proof string it gets an authentication path as well this is a black box thing so this holographic snark verifier V Prime just uses V as a blackbox sub routine so therefore this didn't touch how uh V Prime deals with indexer so V Prime is still holographic and then we uh compile this into a pre-processing snark we really are doing the same trick over again the uh encoded circuit is going to be merized and the indexer outputs a mer rout and when the I wants to query it

gets authentication path as well so uh this connection between holography and pre-processing was first noticed to Marlin sorry in Marlin and uh we extend it to apply to this postquantum setting and work mer trees Etc and you can replace the mall transformation with any blackbox transformation on a uh information proof system so we're going to do is we're going to convert this to what's going called VCS 16 to preprocessing snark from holographic iops and IOP is really just this interactive analog of a PCP a multi round PP sort of and but so now our goal is to make a holographic

IOP but when do we get efficient holography holographic pcfs were first introduced in uh the90s by bfls and a bunch of protocols have like natural holographical analoges gkr and Aurora there are examples of this like the natural encoding of a circuit is super linear in with gkr your encoded circuit is going to have a polinomial blowup with Aurora we deal with R1 CS so the matrices are n byn but they're typically like sparse and that's how you get an efficient improver but the natural way to encode a matrix is to use a byari polinomial like one one variable represents uh your row

index the second varable column index and then each uh the each variable in polinomial is of degree n which means you'll need an n^2 time preprocessing step which you can't actually run it's too inefficient for large circuit sizes of Interest so instead we need to use the same uh Spar that we use for a fast prover in our indexing so what we're going to do is we're going to make an encoding for a sparse Matrix so let's take a sparse Matrix M and we're going to describe it with a three vectors representing the values the row indices and the columns so like a here appears in row three column one so here it's like Row three in its Associated

entry and column one in its Associated entry and each of these vectors is uh linear in the number of non-zero entries in m so really it's a number of nonzero entries in m so the total uh size what we're encoding is uh still linear the number of nonzero entries not quadratic and in order for this to be useful we're going to need to wait a way to uh recover M from these vectors in like an algebraic fashion in order to like make our SAR for it so to do this we introduce uh the Quality Function which as the name suggests uh you take the quality of two numbers is like the quality of I J equals 1 I equals J otherwise it equals

zero and then the arithmetization which arithmetic expression is as follows uh it's just like so m is this function I represents the row index and J represents the column index and we're effectively iterating over uh this domain that represents the elements in the vectors but T explain this equation I'm going to use an example so M31 so when k equals 1 row of K is uh the CTI here three so equality of 3 comma 3 is Will these are equal so it's it'll output one the quality of a column of one is one sorry column of one is one so equality of 1 comma one is also one

so this first term in the summation is the value of one which is a but now for every other term the summation it will be true that the row either the row index is not three or the column index is not one therefore like one of these equality equality Poes will be zero so all other terms in the summation be zero and so uh M31 will equal a and hopefully it's clear that like uh that if the both indices in here didn't correspond to an element of the Matrix I like it was one three right here the there would be no nonzero entry so so the whole thing would be uh zero which is what we want and then to make a sark

for this what you essentially do is you low degree extend all the relevant uh Pol vectors if you're not familiar with this it's essentially converting a vector into a polinomial form and then use a Univar sum protocol from Aurora and all I wanted to talk about for like the uh how we construct the fractal and let me zoom out in like summarize we talk about so first we showed that postquantum recursion yields postquantum Pro carrying data then uh pre-processing is what implies efficient recursion third we then construct fractal just's an efficient postquantum preprocessing snark and the way we got fractal was by compiling a holographic IOP into a pring snark and we use sparse Matrix en

codings in order to get holographic IOP together like by combining these you get the first construction of efficient postquantum brief carrying data and we provide as as an implementation fror pre-processing snark and fral is a recursive snark that uses algebraic hashes uh thanks for your time the paper and code are both line the following links the code fors to get her repo and if anyone has any questions like please ask cool I think there are two questions actually in the in the chat check those out yeah um so shall I ask the questions sure yeah go for it um so so um how do you intiate um Poseidon well oh and um

yeah let's s that question first sure so what we're doing is uh we actually use a uh what's it called a near MDS Matrix which lets you use just zero and one uh entries so we remove them the multiplications and MDS multiplic matrix multiplication uh so and then we use uh we use a small state size like State size three and we're on a 256bit field so we don't have to do any uh so one field element is one hash output so this means you don't have to like do multiple PID permutations and we get to use a minimal sized uh State vector and I think we use uh Alpha like

this exponential parameter as 17 reason we chose something this high was that three wasn't available and then it turned out that by removing more rounds we saved on time and executing oh I see that's slightly CH but I yeah I guess that makes sense um I I was thinking maybe um so you said that using Poseidon um increased the Prov Time by what was it factor of 10 yeah I was thinking maybe um memy might be better because it's it doesn't have the inversions uh Poseidon also doesn't have inversions Poseidon's like uh am I confusing it with rescue I think so

posid in as you start with the vector you add some like round constants you mul mply by an NBS Matrix and You exponentiate by three or 17 or something and you need like 50 rounds or something of that order yeah I am confusing with resue okay but like your middle 40 rounds only have to exponentiate like one element because those exist only for like uh algebraic attx security not for uh phal like St statistical taxs uh think did you try um various different Alpha to see which was most efficient

okay I spent a lot of time like playing around with sideen parameters cool yeah we we used rescue for Halo but mainly because we uh we only had time to um look at one of them so it may be that um besided it's more efficient for Halo too yeah uh out of circuit like rescue took way more time I think it ended up being a bit better on large States sizes in circuit any other questions comments uh so another question do you

think it might be practical to to get the proof sizes down from hundreds of kilobytes to less than 100 kilobyte I think so I I don't think it'll ever get down to like below 50 kilobytes but I think by uh know repeatedly recursing and so first sorry step one improve this uh recurse overhead step two like repeatedly recurse and there's this trick in Starks it's kind of in the weeds but you're you're using read Solomon codes and you have like some rate or some blowout Factor like to write it down a degree D polinomial I'll write it down at maybe 64 du points I can if I increase the number of points I write I write it down at I

increase the pro time but I need fewer verifier queries which lowers proof size oh I see so if you get this what's the trade-off there so how many times do you increase the proof size H the the verify the sorry how many times do you increase the Prov time to get a given reduction it's like this one over X thing so uh if I double the prover time uh sorry okay the verifier queries are like uh are going be like Lambda divided by blow Factor so let's say normally we use blow Factor like 32 sorry Lambda over log of the BL Factor so like we set

the number of if to write down degreed polinomial we normally write it down at 32 D points or so it's the number of queries is like 128 over log 32 or 12 over 5 just like 40 queries so if we double the pro time you could then make it like 30 queries double it again 26 or something I see okay yeah I see this go so the idea would be if you get the recursor overhead to be really good then you do a proof on this of the smaller size statement but you increase that blow Factor you now get a decent like pretty good proof size or pretty good like meaning under 100

kilobytes yeah I I guess um for recursive snarks it's not quite as important to have a really small proof size M yeah because the idea would be to have just one proof per block right cool is there any other questions oh this is my mic anyone else I wonder so what I'm going to be trying to do is put these videos up on the crowdcast platform and I feel like there will be people watching them later so it might be worth it for you to also check out like maybe we can even

encourage them if they're watching this on that platform to leave questions in that chat as well uh after the fact so you could actually revisit that at a later time sure cool so thank you so much and thanks to everybody who came through this is this is our last talk so wow what a journey and what a nice what a nice place to to land on too this is a really great talk and it was great to see it thanks cool so I guess see you all in the interwebs and tomorrow and thank you all for coming and for bearing with us and I feel like we're a band like a

we've gone through the internet in all sorts all these platforms feel close to all of you you know those cheesy films where people go down the wires and exactly yeah we've been on a journey uh yeah so I guess till next time and yeah thanks again see later thank you