# Recursive ZK Applications and Affordances | Devcon Bogotá

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2023-10-07
- Duration: 24:46
- Watch: https://streameth.org/watch/yt-VmYpbFxBdtM
- YouTube: https://www.youtube.com/watch?v=VmYpbFxBdtM

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/recursive-zk-applications-and-affordances/

Recursive zkSNARKs are poised to hit production in the next two years. We discuss how to think about the new affordances and potential applications that recursion unlocks for both scalability and privacy. These include proofs-of-proofs-of-knowledge like ETHdos, on-the-fly "programmable" SNARKs, incrementally verifiable computation, distributed proving, and tactics for reducing verification cost or proof size.

Speaker(s): Ying Tong, Nalin Bhardwaj
Skill level: Advanced
Track: ZKPs: Privacy, Identity, Infrastructure, & More
Keywords: zero-knokwledge,recursion

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

foreign [Music] I'm Nolan I'm ingtong and today we're going to talk about recursive ZK snarks the kinds of applications they unlock and how we can Implement them so first we should talk about what recursive proofs even are so in the context of snork recursion is usually the ability to verify a smart proof inside of another snug proof so this is the ability to say something like I know is not proof that when I run the smart verification algorithm on it returns true inside of another is not proof and the sort of key part here is that verification of regressive ZK snarks is usually not significantly slower than ordinary regular CK smart verification so now that we have this primitive in mind we should think about the sort of natural question is why would you want to make recursive smart proofs so typically regular ZK snarks you know we think of them as having two uh sort of properties such signals and their knowledge so recursion in fact unlocks powerful versions of both of these properties in the form of compression which is a stronger version of the cygnus and multi-party composibility from zero knowledge so first let's talk about compression we think of compression as supercharging succinctness and in particular usually the applications of compression tend to share a sort of common pattern um and this common pattern looks like you know let's say we have a prover who wants to show a verifier um some n pieces of knowledge how do they do this they make a proof showing two sort of things first they show one piece of knowledge and then they also show you know Additionally the N minus one other pieces of knowledge but for these n minus one pieces instead of showing each piece individually they will show that they know a another smart proof of these n minus one pieces so the next question is how do you make the smart pool for the N minus one pieces of knowledge um and in fact we use the same kind of strategy again the N minus one pieces of knowledge we show one piece of knowledge and additionally we show that we know another proof of n minus two pieces of knowledge and so then you know you just Cascade down this sort of strategy and you end up with the situation where you're verifying uh one uh snark proof and in that it's automatically verifying these n items of knowledge another instance of compression that's particularly helpful to point out is the setting where you want to compose between different proof systems or arithmetizations and at the time also pick the good features of each of them so for instance you can have some setting where you have two different proving schemes one where you have a fast prover but unfortunately the verifier is slow and another where the approver is lower but you get the trade-offs that the verifier is fast so using recursion you can compose between the proving system from The Wider setting to the narrower setting and get a tiny proof output as well as fast-provers getting sort of the best of the Both Worlds um a concrete sort of instantiation of this interoperability is the setting which starts and grot16 in particular grads grad 16 is very cheap to verify whereas Starks are very easy to prove so if you verify a stark roof inside of a graphics scene snark you end up with a proof of the original statement with the fast-prover as well as a fast verifier so generally compression has this sort of property that is very mechanical and usually you're rolling up some giant list of computation or items of knowledge increment into a single proof so just to give a flavor for sort of what applications this unlocks let's look at things that are interesting to roll up so first is signatures over the summer we built applications using sort of this primitive of recursive compression of signatures called isocratia where we end up with a low trust low cost sort of roll-up of off-chain modes and end up securing governance and then more related to sort of blockchain land you can do the same kind of trick with light climb boots and in fact plumo which is solos light client is based on this sort of idea and there's also another group named Axiom which is exploring sort of more cooler use cases for this with aggregating and providing historical data through the use of recursive snarks and then finally the sort of Hot Topic in blockchain land these days is making roll ups of transactions two particular ones that are sort of interesting to point out are Mina who sort of use this recursion primitive as a consensus player primitive and polygon Hermes who use the exact strategy of like using Starks for fast-prover settings and grad 16 or snarks for fast verification settings next let's talk about composability my personal favorite property unlocked by recursive Snooks so to give some context for this let's take a step back let's think about what a normal ZK proof uh you know what's the context of a normal ziki proof we usually think of you know DK proofs in this context where approver is showing knowledge to a verifier without revealing the underlying fact of the knowledge with recursion in fact you can unlock something more powerful approver can show knowledge to a verifier without fully knowing the underlying facts themselves so this is a bit hard to model so I'll just lead with an example over the summer we build this application called eat dos which is a dash number is on social graphs so these social graphs are sort of graphs of relationships of people saying I am your friend kinds of things and for instance here we have this graph and vitalik sent someone who sends someone who sends someone and finally I ended up with a four degree path to vitalik now I can prove that I have a four degree path of italic without reviewing any or without knowing any of the intermediate parties in this path so how do I do this I say I am a friend of adhian and adyan has a ZK proof that he is three degrees from italic so in this process I do not know the three degrees that precede adyan and I have still convinced any external as well as myself that there is a valid path of four degree between me and vidalic so of course this is not the only application you can build um in general we think composability is particularly cool to think of in sort of incomplete information game kinds of settings and of course the sort of very typical example the the phrase starting point we thought of was games like telephone or Chinese Whispers where you know you pass a word around or something and you want to make edits to it uh incrementally and then you can make more complex applications like party games like Mafia those kinds of things and then more relevant to blockchain land you can build private State channels and roll ups of that sort so now that we have some intuition for the high level properties of recursive proofs and now that we've seen some classes of applications that are enabled by them you might be feeling that recursive proofs are kind of unreasonable we get unlimited compression and compostability so I guess the natural question now is how do we Implement and construct these systems so right now there's broadly three classes of recursive proofs in production and as we descend the hierarchy we are relaxing the requirements on the proof systems which are eligible for recursive schemes so at the very top of the hierarchy we have really the most stringent requirements so we we need proof systems with verifiers that are sub-linear that are succinct in the size of the statement being proven and this enables us to do full recursion at every recursive step so this has been implemented for the growth 16 and Fry priv systems so if we relax our requirements a little bit and we say even if we don't have a succinct verifier maybe we're happy enough just with a succinct accumulator so intuitively what this means is that we want a verifier with this shape that they have a succinct check a cheap check and then separately they have an expensive check and so here we can instantiate an atomic accumulator and at each recursive step we only perform the succinct checks and we accumulate the expensive check and delay checking it until the end of a long batch of proofs and doing this gives us amortization of the expensive check and finally if we relax even more um we don't even require a succinct accumulator well now we're just happy with a succinct public accumulator and the idea behind this split accumulation is simply that you split your accumulator into a public and private part and the public part is short and this is what we accumulate at each recursive step um where whereas we delay the verification of the private part of the accumulator until the very end so let's go through these constructions at a high level one by one just so you can see the shape of it so probably the cleanest shape is the the cleanest shape would be full recursion so over here we start with our application circuit and it's f um F of w-i-z-i gives you z i plus one right it's a normal relation now we bundle that together with a recursive verifier and um basically this recursive verifier takes in a proof instance that was produced by the previous instance of the recursive circuit and so if if we look forward we we need to generate a proof of the whole recursive circuit in order to input to the next recursive instance so in this way we're chaining recursive circuits and at each step we are fully verifying the previous instance and when we get to the final verifier we no longer need to bundle it with the applications are getting here we can just perform a final verification of the proof outside the circuit so this is full recursion is is the cleanest API um now we're gonna get slightly more messy and we're gonna relax our requirements um to get an atomic accumulation scheme so now if you recall here an atomic accumulation scheme our verifier is not sublinear so in fact the verifier inside the recursive circuit is just the accumulation verifier and it only concerns itself with the succinct checks of the verifier um and the expensive check is accumulated and deferred um at each step so here we are chaining basically instances of proofs and accumulators um and at each step we're just procrastinating on performing the expensive check well until we're finally satisfied at the end of a long chain of proofs we perform the final decider sub-particle that finally bites the bullet and does the linear time check but at this point we can do it outside the circuit and at this point the cost of the linear time check is amortized across a big batch of proofs now from here to Atomic accumulation is just a small step so it's just splitting up your accumulator and your proof instance into a public and private part and now the verifier the recursive verifier gets even smaller and it concerns itself only with accumulating the instances the public parts and it does not perform it does not have access to the private parts of the accumulator and rather it relies on the Pervert to provide some commitments to the private parts which it then performs accumulator checks on so a lot of these constructions I've described are really cutting edge and they come from a feature of our modern proof systems that are very modular in design and as we get a better understanding of the building blocks and the components of our proof systems this lets us customize our proving Stacks with a lot finer granularity and recursion as we saw also allows us to compose proof systems and to get the best of both worlds in many cases so here's an example of a modular conception of a proof system so I work on the proof system Halo 2. and I think of Halo 2 in terms of these four components so at the very front end is where you're interfacing with your business logic so you take a relation and you arithmetize it into um so in in Halo 2's case we encode our values in the LaGrange basis and we encode constraints on these values as polynomial identities we then input these polynomials into this information theoretic polynomial IOP that basically checks the correctness and the consistency of the polynomials encoding our circuit and then we realize this polynomial IOP using a cryptographic compiler so in this case it's the inner product argument that and the Fiat Shamir transform that allows the proverb to Define their interaction with the verifier and at the very end of it Halo 2 is a recursive group system and we can in fact instantiate an atomic accumulator over the inner product argument so these are the four sort of modular pieces of modern proof systems that I think of now we can do pretty funny things um composing these pieces so I've set up three cases um so the first one is information theoretic compilers and an example of this is MPC in the head um what this does is it converts one information theoretic protocol to another one and in this case it's the proverb sort of pretending to run a multi-party computation in in her head um so she's really simulating the multiple views in an NPC and committing to those views and now the verifier is only checking the outer protocol being the NPC instead of checking the inner protocol which is the ZK proof so this is one very interesting way to compose proof systems another way that we've seen before in this presentation is more or less just implementing verifier X and prover Y and you would do this also for efficiency gains and um sort of the last Clause of composition that I came up with was really just thinking up better cryptographic compilers so there's this recent paper by a group at consensus um and they they took this protocol gkr that's highly optimized for repetitive computations like hash functions now but the problem of gkr is that it has a slow verifier and um so and it also uses the Fiat Shamir hash as a cryptographic compiler and this makes it very inefficient in the context of recursion so what the team at consensus did was they came up with their own cryptographic compiler that was custom made for their target proof system and the target proof system here is like a growth 16 r1cs per system and so really like that's going in the middle and making changes like customizing proof systems at a very low level um for efficiency and yeah I think this this leads me to ask um whether or not we can systematize this process and um whether or not we can I don't know um explore this optimization space in a well-defined way so you can think of this as kind of a call to action so I think there's certain nice to have certain to Do's that all proof system implementers would really like the first being good benchmarks Fair benchmarks of heavily used Primitives like hash functions like big and arithmetic so benchmarks of these Primitives across different proving stacks and the second would be it's a kind of a meta requirement is to think of like what metrics we're interested in for example efficiency for example proof size and basically how to optimize towards these Magics so on what basis are we comparing different compositions and configurations and the last sort of call to action would be to think carefully about how security properties also compose like excuse me like is it the least secure approved system the the fewest bits of secure 30 or like some weird composition when we mix and match proof systems so all these are questions that it would be great to have everyone's input on like even this taxonomy that I came up with I'm not sure that it captures um all features of proof systems in the best way so Nolan and I actually help out at a group called Xerox Park oh we didn't put the name on the slide it's 0x Park um and there we're setting up this task force to look into this area of recursion aggregation and composition um yeah and I think like I might as well take this opportunity to shout out Xerox Park and they supported a lot of our work a lot of those fun apps and a lot of these Community efforts yeah I think that is all I have so thank you awesome well thank you so much we have time for one or two questions if you have any questions please raise your hand we've got a question here on this side hi I didn't think this would work for years and years and years um and I also I'm not I'm not even sure that does work it does seem way too good to be true so can you prove and how do you prove that that it's secure to do recursive like proofs like this like where where is the security proof you know I don't know how to convince myself that this works actually yeah I mean that is a good question it seems very unreasonable that you can prove like an arbitrarily long history of computation with a constant size proof um it does seem unreasonable so I will say that security proves exist there in papers um but now and do you have like some intuition as to why the security should hold uh yeah for sure I I think one sort of physics-based view that we've seen before is like it's like oh you're 3D space and you're collapsing into like a 2d surface um I forget the exact name of this but the holographic principle uh so I I think there is like some sort of meta justification you can come up with to convince yourself if that's like this sort of thing but there is fruits of all kind that are actually substantial it's a good question any last minute questions we have one at the back all the way over there so recursive proofs are real fun but if you do it at scale then you're you know it's like you you you have skill and corruptus snapping at your heels uh because of the proof carrying data right if you want to build on recursive proofs and it doesn't happen at the same time so let's say you do a proof and you do recursive proof and then you have to wait for a state change for something else it might happen much later you need to keep the proof carrying data around and as you know if as you know but most here that is typically a very large amount of data um so it's like if you're doing it at scale you're really running into the issues of data provisioning and all the fun part can get really expensive really really quickly not even talking about like the the um you know the the computational overhead that you have yeah yeah for sure I think I don't think recursive proofs are a silver bullet and I think they're better suited for some shapes of applications so recursive proofs are very commonly used to reduce proverb space complexity so breaking up a large circuit into many smaller parallelizable circuits so yeah but I I agree like in context of applications with more complicated and like timely data flows it's it's we have to put some care into how and where we are inserting this proof carrying data yeah right and also just to add uh I think there's also some interesting like sort of clean separation here of like rules versus data availability sort of problems um and if you just look at you know data availability as a sort of Black Box problem you know you have lots of blockchain kinds of solutions for it and for instance isocratia explorers um one sort of solution that um maybe you can check out The Blog on yeah also to add on to that like I I really like knowledge thing about composability the fact that um you know you you can play incomplete information games so I think sort of fun applications like that that are unique to PCD are also very interesting to explore amazing that's all the time we have for today please give Ian and Elaine a big round of applause [Applause]