HyperNova: Toward practical zero-knowledge virtual machines with Abhiram Kothapalli | a16z research

Transcript

so I'd like to welcome everybody to snark week um pretty informal week I think uh we have uh three excellent talks I'm excited about one in a moment and uh another on Wednesday by fantini and another on Thursday by our own intern Quang um other than that we'll just have uh some visitors is coming through um and I might be uh pinging you to to talk to them but they're they're all just uh people who are really pushing this technology forward um so we're we're lucky to just have people in the in the same room this week uh so just uh looking forward to some exciting conversations auam is going to tell us about hypernova uh which is a

significant Advance uh in a particular approach to snark design uh called folding schemes uh one major benefit of them is keeping the prover space uh smaller than pretty much any current approaches at least that I've seen implementation and possibly in general um and so he's going to tell us about ideas that have been really influential over the last year or two um and I'm looking forward to hearing the details so thanks all right well thank you so much Justin and you know I'm really appreciate that you guys are putting this together and especially thank you to Justin for putting together this Nar week it's a little rare that we're starting to like have these opportunities where we all get together and start to really bash out these cool ideas and feel really this is a great

step forward um so you know I I am trying to make this talk just a little bit uh more high level we'll see if I actually do achieve that goal or not with the whole full idea that later in the week we can maybe dig into the technicals of hypernova itself but really what I wanted to talk about today is yes hypernova for sure but also the general idea of you know how we can start pushing towards practical zero knowledge virtual machines and where hypernova Falls within that larger landscape and before I begin I'd like to point out this is a joint work with shat said my co-author over MSR this talk will be roughly divided into three parts in the first part I'll talk about what a ZK snark is or a zero knowledge the sync non-interacted argument of knowledge now

in short a ZK snark is a short certificate that proves the correctness of computations without revealing any of the secret inputs to this computation okay and in the second part I'll talk about zero knowledge virtual machines an expressive Target application where we consider this idea we can potentially prove the correct execution of an entire virtual CPU using the power of snarks and hopefully I to convince you that this has the opportunity to significantly scale certain aspects of decentralized computing and finally in the third part I'll talk about our own work hypernova which is a performance ZK snark which can be used for applications such as zero knowledge virtual machines

now before I get into the main meat of the talk I just wanted to give a very quick uh elevator pitch for the experts in the audience who might just want to get a quick idea of what hypernova is about so the core idea with hypernova is that we effectively uh uh design new techniques for proof recursion and that's this idea that you can write ZK snarks that prove the validity of other ZK snarks okay and we've made a lot of progress in last 5 years and trying to make proof recursion faster and faster and hypernova can be viewed as one of the latest Works in this line now in particular hypernova uh designs an efficient uh efficient new techniques for proof recursion that reduces the

overall overhead especially for computations represented using High degree constraints Now High degree constraints are useful in practice because they allow us to represent computations more efficiently using fewer but more expressive constraints and this ultimately leads to more efficient zero knowledge virtual machines now the core technical piece in hypernova is something as just mentioned called a folding scheme which allows us to take multiple proofs and compress them into a single proof of the same size and in particular hypernova core technical contribution is to design a new folding scheme for proofs over computations represented using High degree constraints and in particular we

can show that hypernova folding scheme indeed has a very small recursion overhead that performs favorably when compared to related work especially in the context where we're trying to fold many proofs over computations represented using High degree constraints at a very high level uh hypernova uh recursion overhead is dominated by just K Group scalar multiplications where K is the total number of proo we folding and a log logarithmic number of hash operations okay so what's the when you say folding and when you say recursion like what's the relationship between those two is folding a specific style of recursion or how should yes that's a great way of thinking about it so there's like different ways we can take a a proof of like I steps of some computation and recursively convert it

into a proof of I plus one steps and folding is one of the latest techniques and trying to do this more efficiently as compared to Prior approaches but roughly they're all centered around this General nebulous idea of like recursively sort of proving things about things is there like a one sentence thing of what recurs what folding corresponds to in particular or that'll come later yeah yeah so what folding does recursively is we we maybe have many different proofs and we recursively compress all these proofs uh layer by layer into a single single proof so kind of a tree agre exactly like a tree is a great example okay great question okay so now in addition to the core technical results of hypernova which is a folding scheme We additionally have several additional technical results which augment the core ideas of hypernova to further improve our techniques for the

purpose of virtual machine execution in particular in Supernova we show that possible to scale the overall prover running time uh in a way that only scales with the instruction run at each step rather than the full universal circuit that encodes all instructions and in cycle fold we show how to uh more efficiently modify our folding scheme to more efficiently work with cycles of Curves which are a particular structure of of elliptic curves that are used for the particular use case of recursion and finally in hypernova itself we show how to take this overall proof of virtual machine execution and blind it at the very end and just ensuring that any secret inputs to the virtual machine are not revealed to the final verifier of this proof but with all of that out of

the way let's get back to the more general part of this talk which is what is a ZK snark and then we'll get into what is a ZK VM and eventually we'll get back into typer NOA itself okay so at a very high level a ZK snark is a short certificate that attests to correct execution of some function f without revealing some or all of the secret inputs okay now as a concrete example we can imagine this function is something like sha 256 okay and in this particular example then we can use a ZK snark to prove that I know a pre-image to a shot 56 hash without actually revealing what that pre-image is now we can imagine this being used online everywhere today for instance if I wanted to log into my

banking application and their servers can just store the hash and I just have to provide potentially randomized password and I don't have to R Ral my password directly instead I can just give them historic proof that I know the password and that allows me to log onto their servers so this this prevents me from having to move my password in plain text uh thus reducing the overall attack factors now ZK snarks are are incredibly exciting because they enable a large class of exciting applications with additional integrity and privacy guarantees okay and today I put together two examples one which showcases what zkx can do for online privacy and other which showcases what they can do for protecting the in of online data okay so in the particular case of digital

privacy we can imagine that in near future where all of us have a digital identity okay and this digital identity can have our name it can have our social security number it can have our date of birth it can have additional metadata that's only Rel relevant in the context of online applications we can of course imagine that such an identity is signed by a trusted Authority such as the US government and this is what prevents these identities from being uh spoofed by uh me you know I can't just make up a new identity and show it to some party okay but now given such an object given a digital identity and given it signed by a trusted Authority we can imagine that we can use it all sorts of applications for instance I can file my taxes online and I can go log into my

bank account and I can vote all of these things I can do just by Furnishing my own digital identity okay but there is a key limitation to this particular technology which is this idea that well now I have to start Furnishing this identity for less important tasks like proving my Costco membership or proving that above 25 so I can get a better insurance premium for a car rental agency or checking out a library book right in all of these cases I I'm stuck with trying to reveal my entire social security number my date of birth even in applications where it's like not really necessary to show these terms to get around this issue we can use ZK snarks which allows us to prove the necessary

properties about such a certificate without revealing any of the confidential information on the certificate for each particular application okay so now to give you a concrete example we can imagine okay that we write a function okay it's called verify age which all this function does is just check that my certificate is signed correctly and then above 25 and if that's the case then it will output a new blinded certificate which only reveals that I'm above 25 and that it has a valid signature but no other private information about me at this point we can use a ZK snark which will effectively prove that this function was run correctly and therefore

proves that this blinded certificate is indeed the result of inputting a valid secret certificate as input and this ZK snark will reveal nothing about the secret certificate okay so now going back to our particular application I can go to a current agency and furnish my blinded identity alongside the ZK snark proving that it is indeed a valid blinded identity and then they can give me a better insurance premium because I'm above 25 without them having to even check my social security number or even check my age because they know I'm above 25 so now that was a great example for how snarks could be used in the context of uh uh private certificates okay but they can also be used today for the

particular use case of fighting digital disinformation which is becoming more relevant than ever you see in this particular use case we can imagine that well actually this is actually what's actually happening so the Associated Press has a a strict set of rules for what sort of modifications photojournalists can do on some initial photograph that's signed by some trusted Hardware right in fact they're like okay all you can do is crop an image you can recolor it but that's about it right so now the core problem is that well if a website like a News website wants to serve an image to me okay then to Pro to me that it's been modified correctly they probably need to show me the original image and then show me all the modifications they made so this is maybe

dozens and dozens of images along the way and every time uh my browser can then check all these images along the way and then check okay indeed yes this image uh does not have any illegal modifications according to the rules of the Associated Press but this is this is an issue because this is really cumbersome and slow our browsers now need like 10 times the number of like image data being passed around right so to get around this issue we can again use the power of ZK snarks which can then hide all the intermediate images and just prove that yes there exists a valid set of images but you really don't need to look at these images okay in particular how this works is we can imagine that in the future all of these images are taken by a uh cameras with trusted like Hardware inside that signs

off on these images okay and there's like an authorized signature and then you can write a a computation or function which only does valid modifications on the original image and also checks the original signature and then perhaps outputs a correctly modified or a validly modified image okay and now at this point we can once again use the power of snarks to prove that this modified image indeed did start off from a valid signed image okay and it was permissibly modified along the way at that point you know now we can imagine a future where you know if you look at this image in your browser your browser can also check a very quick and short snark proof that the image was indeed generated correctly okay and it

doesn't need to look at all the intermediate images along the way so those are just two examples of how today snars can be used to protect digital privacy as well as digital Integrity of data today and in fact there's many many many more examples of just how powerful snarks can be they can be used for private voting protocols private database retrievals they can be even used to enable private cryptocurrencies okay so it's because of exciting applications such as these the snarks are being quickly adopted by both industry and Academia for and developed by both industry and Academia to protect integrity and privacy of modern applications so with that I want to move on to the second part of the talk which

is the particular application of zero knowledge virtual machines so what we've been seeing about 5 to 10 years ago is this idea that you know we can start to converge upon one particular application which is this idea that perhaps so we can prove the entire execution of a virtual machine using a ZK snark and the core benefit of this is scalability you see instead of writing a new zero knowledge proof system for every new application instead you can write a zero knowledge proof system for the underlying substrate running all of these applications now when this idea first came out back in 2013 uh at least the memory efficient versions due to Ben San and others we simply did not have the snark Machinery fast enough to

actually make this a reality but in the last decade we've made significant leaps forward into making this more and more practical okay and the exciting implication of such a technology is that it has the potential to significantly scale certain aspects of decentralized computing the core idea with decentralized Computing is that you have many participants in a network all together running a single Global computer okay now the way they do this is that they all run the computer locally and then they check the output State and then they all vote on what the output state of this computer should be right and you can imagine now that you can run all sorts of secure applications on this computer so long as he trusted

the majority of the participants in this network are honest the core issue with this however is that now to run a single computer you need to replicate the execution of the computer on thousands and thousands and thousands of nodes which is simply just not scalable one potential solution for this is that you know well instead of rep ating over and over again we can just have a single participant write a proof of a virtual machine running that particular particular chunk of that computer okay and then send off this proof to every other uh minor or node in the network okay and all these nodes can then just check that short proof and instead of replicated computation they can just say okay well you know like the output of this many steps of the of the computer

is this and then trust that result and then just keep going and moving forward because they have a snark proof which attests to it all right so now the question is how do we actually build these virtual machines the direct approach which has like shown a lot of Promise recently is this idea that well perhaps all you have to do is take a single cycle of the virtual machine okay and replicate it many times just unroll the entire execution of the virtual machine into a giant trace and then just use the ZK snark to prove that this Trace was actually executed correctly and this Trace can be represented as a of a bunch of algebraic or arithmetic constraints okay and it turns out but because of recent work

especially here a16z with respect to jolt we have that this approach is incredibly fast what we're seeing is that we can prove almost 17 million iterations of shot6 in just 125 seconds and this is significantly faster than what we knew was possible just half a half a decade ago while this approach is great in terms of runtime it does have a significant ific an memory overhead okay in particular with current implementations of this direct approach what we have is that the prover memory also scales linearly with the trace of the entire execution okay and it's a little hard to get the concrete numbers for how much the memory overhead is but

roughly I've measured on my own MacBook Pro that yes indeed as we expect the overall memory overhead does increase linearly over time what we've seen is rough uh you know based on our estimates if we want to prove maybe uh 100,000 iterations of shot6 then this would roughly take a trace that's like much much higher so now the question is how can we augment Joel how can we improve it even further to to maybe handle this memory issue okay and the core idea is that we can use something uh that's been known for about a decaded to at this point called incrementally verifiable computation okay and this is core idea that well okay well instead of globally

considering the virtual machine Let's only locally consider each piece of the virtual machine okay and locally process it and write a proof and now with each additional step of the virtual machine we can update a proof alongside okay so now with two steps of the virtual machine we can update the proof such as it does not grow in size but now is a proof for two steps of the virtual machine and so on and so forth until we have a final proof for the entire execution of the virtual machine uh that scales with just a single chunk and indeed today using modern techniques especially from works like chol we can ensure that the proof size and the memory overhead only scales with the latest chunk of execution while also ensuring that the run time remains

comparable to the direct approach the story of how we made incrementally riable computation or increment proofs for IBC faster and faster is very interesting in its own right you see this idea or the innovations that led to this first started back uh around uh 2013 I'll say by Jano and others who showed that it's possible to design a snark that is just constant sized regardless of the size of the computation it's proving so you know even if your computation is a billion cycles or trillion Cycles or or or or Gates or constraints or whatever what they show is that the proof itself only consists of seven group elements now if I remember correctly their proof itself is like roughly 288 bytes just incredibly tiny now us using such a

proof system what Ben San and others show back uh in around 2014 is that they can then use this idea of proof recursion to very efficiently prove at least at the time very efficiently prove uh virtual machine execution okay and the core idea back then is that well to prove I +1 cycles of a CPU all you have to do is write a proof of the latest step of the CPU as well as prove that there exists a proof for eye cycles of the CPU and thus you can take a proof of I steps and convert it into a proof of i+1 steps exactly as we need for in currenly verifiable computation now unfortunately the original approach due to Ben San and others was while it was theoretically elegant it still wasn't

quite practical and it remain that way for about a decade and we didn't really know how to do any better than what we had back in 2014 until in 2019 bobrick and Hopwood introduced a fundamentally new approach towards proof recursion known as proof defer where they show how to amortize away some of the overheads associated with recursion okay and at that point they brought down the number of total constraints of the recursion overhead so the recursion overhead is effectively the total number of additional computational constraints you need to prove on top of the original proof top of the original computation that you're proving for recursion okay and they bring that down all the way down to like roughly 250k constraints

okay now given that that this this proof defer approach was was fundamentally new at the time and uh just over a year uh we saw a roughly 5x speed up uh for the overall recursion overhead so this was brought down all the way down to around 50,000 Gates by buns and others back in 2021 what we see now is that with Nova our own work we saw an additional 5x speed up by introducing this concept known as folding which showed us that we can take multiple uh proofs and compress them into Tas of checking just a single proof okay and now our own work hypernova can be viewed as taking some of the great ideas from Nova and extending this to high deegree

constraints that means not just quadratic constraints or low degree constraints but any constraints uh this allows us to represent competitions more efficiently for the particular use case of memory efficiency kbm one other thing I wanted to point out that this speed up I'm only talking with respect to the recursion overhead okay and in particular when we look at the improvements to the Prov runtime as well per constraint runtime we see an even bigger differential from where we were just 3 years ago in particular for Halo We roughly had to do about um 10 group scalar multiplications per constraint and this has been whittel down all the way down to just one group scalar multiplication per constraint so putting everything together we've seen almost a 100 times Improvement ever since the

original uh uh uh approaches back in uh 2019 us B and hop this is the prover doing this is the Prov yeah so everything in Orange is the Prov run time overhead right yeah so and and you're saying like the size of the MSM is number of constraints if that's one that's what you mean by one yes yes yeah that's what I mean that's what I mean yeah great question any other questions about this particular graphic so I'm I'm trying to figure out how to interpret your y AIS like what is is 200,000 constraints a lot or a little like yeah so you have some fixed computation in mind yeah yeah 200,000 is I would say that's a lot it's like a little hard again like to sort of like give an idea for like what's

expensive and what's not expensive but I would say roughly like when we're trying to prove computations they range from like roughly like the computation itself ranges from like 1 to like 30,000 Gates so 200,000 is a huge recursion overhead on the original computation we want to improve so the original computation was what were you saying so one particular computation is around 30,000 30,000 yeah so yeah 200,00 just give you very rough like finger in the wind sort of comparison um uh but also like again like there's all these improvements with the pro of runtime too so even even like uh you know even if like 250k Gates is cheap uh in particular application like the number of pro operations per gate is still quite high in the original approaches were was IBC introduced initially for zkv Ms or for

some other reason no it was generally it was introduced more generally for just recursive applications of a particular function and zvm seem to be the most interesting application right now for IBC that's a great question as well for the remainder of the talk I really just want to talk about hypernova and the particular details about hypernova itself okay and why it helps us get B better and faster zbm but before I do that I want to take a quick step back and just really compare and really think about how the field has been moving over the last 10 years based on what we've been seeing so far so my belief is that snarks today are developing much in the same way that computer architecture developed half a century ago and the core idea is well computer architecture back in the designed specialized hardware for special specialized

applications and in much in the same way in the early 2010s we were designing snarks for particular applications such as private database retrievals secure voting protocols and private blockchains and so on and so forth but what we saw with computer architecture is that well in the 60s and 70s we started developing CPUs for General computation okay for General instruction sets Okay and in much in the same way we started developing snarks for general purpose virtual machines in the late 2010s okay and the great thing about this stage of evolution is that we get significantly more scalable results right because you can conceivably run any program with like very little developer overhead but

the core um core cost of this is because of the additional abstraction overhead this is actually just objectively more expensive than the original approaches so now we're in a stage of development where we're trying to design optimized snarks for the general purpose task of virtual machine execution much in the same way where CPUs we're now today we're designing highly highly optimized architectures for general purpose instruction sets Okay and now our own work Supernova hypernova Nova itself can be viewed as the latest work in this line of optimized snarks for virtual machine execution so now with that I want to move on into discussing some of the highlevel technical ideas in hypernova but before I move on did you

guys have any questions about Zer knowledge virtual machines in general maybe I'll ask this after you introduce hypernova it's like comparison between hypernova versus just using continuations in jolt and do a final step of proof aggregation I see oh I see so like so this continuations approach is it basically just taking each chunk writing a proof and then like having a bunch of proofs and like folding using a tree like process yeah yeah yeah yeah um so I think really this might uh just be a memory thing uh it could be uh again like there's like you might have to you can get rid of some of the cion overhead potentially with the continuations but again like it's like not empirically tested yet at least I wouldn't know immediately off the top of my head okay so before I explain what folding is what

hypernova is like you know all the particular techniques specific to us I want to talk more generally about Valiant original approach to incrementally verify about computation that will help set the stage for what hypernova changes from the original works okay this is Paul Valiant there's a lot of valiant uh I think it's Paul Valiant yeah that's a good question um okay so to do so uh it will help to generalize a little bit let's not talk about a single version Mach machine cycle let's instead just talk about a general function f okay which could be a version machine cycle but it can be pretty much anything else and now our goal now is to prove recursive iterations of this function f that is you know if you apply FN times uh to some initi input z0 then you get

some output ZN okay so now the core goal here is how do we take a proof of I steps of F and convert it into a proof of I Plus one steps okay now valiant's original approach is incredibly elegant basically what he says is that well instead of just proving that function f instead let's prove that function f plus a little bit of extra gluc code okay and what this gluc code is going to do is run a snark verifier and what the snark verifier will do is check a snark that attests to I iterations of the function fime okay now we know by the nature of snarks and especially du to construction gener and others that this snark is it's only seven group elements it's constant size regardless of the computation it's

proving but now what we can do is we can write another snark for the correct execution of the computation fpre okay just literally take a look at the trace of this computation fpre and prove that indeed it runs correctly okay and we'll call it snark Pi i+ 1 now what pi I plus1 attests to is that well the latest iteration of the function f was run correctly but also that there exists a snark proof of um I iterations of the function fime and as such it effectively serves as a proof for i+1 iterations of the function frime so we've converted effectively a proof of I steps into a proof of i+ one steps okay now while this approach is incredibly elegant in

theory it turns out that it's still not quite where we want it to be for practical purposes the core issue is that this forces us to effectively uh witness the entire trace of the snark verifier inside this trace for the competition f-prime when we're writing a proof about its correct execution okay what that means is that roughly you would have to encode all sorts of complex cryptographic operations such as pairings and elliptic curve operations and so on and so forth just using a bunch of addition and multiplication Gates and you can see why that would quickly start to become very expensive very quickly now in fact when this was empirically tested by Ben San and others back in 2013 2014 uh when they first designed uh one of the first uh zkm

space recursion what they saw is that well okay using the best uh snar proof systems of the time this would require roughly three pairings okay in each of which takes around 20,000 Gates okay so a total recursion overhead of 60,000 you might say Okay 60,000 sounds a little bit cheaper than what Halo was achieving at 250 you have to imagine you have to remember that these pairing based curves are a lot more expensive roughly 10 times more expensive than standard elliptic curve curves okay so this really starts to blow up the overall uh recursion overhead for using or trying to represent a snark verifier inside the trace of this computation okay now empirically when this is tested what basan and others found is that the

virtual machine itself runs at roughly 0.041 cycles per second which is incredibly slow when considering native execution which is currently in the billions of Cycles okay so now keeping that in mind okay we looked at this and we said okay what could we possibly do to make this as fast as possible that is reduce the overall recursion overhead all the additional glue computation you need on top of the original function f to construct the computation F Prime so just to be clear so the issue is that the pies get really big especially as I gets large no it's not they all stay the same it's just that like the snark verify itself even though it's constant size it's very expensive to express and where does that show up here

like the or that's this like verification function right there that black box that just gets very expensive yeah it's still constant though it's just an expensive constant yeah and uh yeah so what when you take the verifier and put it into constraints like that's that's bit that's a lot of constraints yeah um on top of that I guess it's it's the cycles of pairing friendly curves that are 10x more expensive yeah yeah to make this all work out no worse than a has already said it is you you need to use special kinds of Curves for technical reasons that that's where that 10x is coming from on the slide which means even once you have these many many constraints proving them is 10 times worse than you think it is since the

Prov is doing all these operations over these gross curves so in terms of the picture the the chunk of pii plus one that's part of the black box is just kind of a lot of stuff plus like heavy computations involved yeah that's right yep okay great questions any any other questions about this particular valiance original approach and why it falls short in practice Cycles was that introduced by bctv 14 yes that was indeed their like that's like one of the things that Justus mentioned like they they showed that to even make Valance approach even remotely feasible we need these like cycles of pairing friendly curves and even that still very expensive so we looked at the original uh bctv approach okay and we said okay well in the last five years like as as a when I say we I mean Collective as a field right and

what we realized is that well what we could do instead of you know directly checking these proofs inside the circuit we know that's ensive but what we could do instead is perhaps defer the task of checking these proofs and in particular Nova introduces a particular abstraction known as folding which allows us to take a prior proof and compress it into a running proof okay in a way that this running proof does not grow in size over time and what we show is that this compression procedure is significantly cheaper to execute inside a uh inside a trace or or set of constraints then um than a snark verifier okay okay so a little bit more concretely what we end up doing is to say okay

well how about we have two certificates or two snark proofs one which proves uh the latest execution of the function fime so F of z f applied to zus one is equal Z and one inductively let's assume that's of the same size which attests to I minus one prior iterations of the function fime you can see that checking these two proofs together when you collect them together the two claims you have a claim of I iterations of the function fime or proof of that property okay and now what we can do is do this compression procedure and take a proof of the latest step and then compress it into running proof to get a new proof Pi + 1 that's of the same size now the core idea here is that well checking this new

proof is equivalent to checking both prior proofs and as such uh you know we effectively have a new proof for I iterations of the function frime and now on top of that we can write a new proof for the correct execution of the uh latest iteration of the function f Prime and now we have two new proofs which now iterate attest to i+1 iterations of the function frime so we effectively converted a proof of I iterations of the function frime which is these two small proofs into a proof of I plus1 Iration of function f Prime which is those two small proofs one particular question you showed before that the difference in performance to BCL lms2 is like 5x compared to Nova oh no it's it's uh BC oh yeah yeah that's right yeah right

they do like the split accumulation stuff which is like roughly similar right um uh where exactly does the 5x performance Improvement come from yeah so that's a great question so there's like two things first like the folding scheme itself requires fewer group scalar multiplications okay uh we improve that by a factor twoo and on top of that the prover itself to like you know actually participate in the folding scheme needs to do some amount of work and we improve that by a factor of two as well so we reduce both the folding verifiers work okay by a factor two and the floating impr is because he need to do half the number of scal multiplications and like you know concretely adding everything up they're like concrete costs around like 50k and ours are like around 10K so that's like the total 5x great question yeah would

you is is this slide would it be accurate to summarize it as saying like the old the Valiant way was sort of proving you verified a snark proof yeah and the folding way is take two snark proofs don't verify them but Smosh them into one exactly yeah smushing is nicer than verifying the whole exactly that's that's a great way of thinking about it yes but you still have to prove that the folding was done correctly right no yes yes so that that's like the uh elegant part of this right so when you are writing a new snark proof Pi + 1 okay that attests to the fact that the function f itself was run correctly and that the previous step of folding was run correctly so if if

you know the final verifier checks the lowercase pi plus one is checking that folding was done correctly in the previous step as well as F was run correctly okay and then now by by the the folding property itself you know if you check this final uh running proof uh Capital pi plus one you're check you're effectively checking that all prior folding steps were done correctly so this is like fundamentally different from this approach of just like taking a bunch of proofs running the folding scheme and checking the folding proofs along the way because the folding proofs themselves are being checked recursively by uh each of these uh recursive updates there is one caveat which which I haven't really talked about which is this idea that if we were to directly fold these snark proofs inside the circuit that's still a little too expensive oh sorry when I say circuit I

mean Trace I tried to take all references to circuits here um okay so instead of directly uh folding uh what we want to do is instead have short commitments to these proofs and those are the pieces that's being folded inside the trace and externally the actual IVC prover in its own head is taking care to fold the actual underlying openings to these commitments in a similar way okay so that's a sort of minor technical caveat which is not really important but like this is sort of the key Innovation that started with the split accumulation and so on and so forth okay okay so now with that out of the way oh yeah one more piece I guess is that you can complete the recursion

cycle by uh writing a new commitment uh to the latest St okay so now with that the core idea Nova effectively is to show that well what we could do is we could design a very efficient folding scheme for an NP complete constraint system known as relaxed R1 CS which we designed specifically for the task of folding two particular statements expressed in this language okay and in particular what we show is that well if you have two relaxed R1 CS instance witness pairs okay then you can fold it uh into a single relax star1 CS instance witness pair that's of the same size and structure and so on and so forth in fact what we show that is the recursion overhead that means all the additional constraint you need to express this

computation F Prime is dominated by just two group scaler multiplications and you know after optimizations and you add everything else together Nova's overall uh um recursion overhead is just 10,000 constraints okay now one other thing is that like taking advantage of the 10,000 constraints we can show that the prover itself is also concretely efficient in fact if you want to prove a million gate circuit per recursive step roughly the provers runtime C responds to about a second in each recursive step so we're getting closer and closer to practical virtual machines while Nova makes important contributions for allowing us to get faster and faster virtual

machines one of the key limitations in Nova is that it is limited fundamentally the folding scheme itself is limited to the language of R1 Cs and while R1 CS is a great really powerful language it only supports degree 2 constraints okay and degree constraints technically you can represent any computation you want using only degree 2 constraints but the problem is that you need a lot more degree 2 constraints for certain types of computations so the core idea is that well maybe we can try to improve this by by building a folding scheme itself that supports higher degree constraints and thereby allowing us to represent computations more efficiently and this is precisely one of the problems we tackle in hypernova where we show that we can design a folding scheme for a

generalization of R1 CS called CCS okay which supports High degree constraints the core idea in hypernova is that we can have a running CCS proof a proof for computations represented in CCS language okay and fold it into a simpler running proof okay called linearized CCS or this running proof is for a language called linearized ccs and we can keep doing this folding in a way that this linearized constraint system or linearized CCS proof does not grow in size okay and the core idea for doing something like this is to use some check protocol which will allow us to linearize nonlinear constraints into a linear format which will then allow us to sort of compress it directly into the

running linear proof effectively we show that the recursion overhead for hypernova is dominated by just one group scalar multiplication as opposed to Nova 2 and just a larg number of hash operations so now I want to get into how exactly the folding scheme itself works but here is like really where it just starts to get really mathematical and like very polinomial and just a bunch of mess so I'll try to keep it pretty graphical we can definitely get into the math itself but I'm going to try to avoid that as much as possible now for the experts in the audience I have placed some of the math inside the the black box but that's really not necessary for understanding here okay so the core idea for our folding scheme our goal okay is to try to take a proof of a computation represented in CCS okay and a proof for

a computation represented for linear ccs and then compress them together to produce a new uh proof of the same format so a proof of linear CCS okay that's of the same size that does not grow in size okay now that's that's the core idea now how do we do that right and this starts off with this observation that checking this CCS proof is effectively equivalent to checking that a polinomial q is equal to zero on a bunch of points okay and that's a complex check but I'll show you in a moment how we can reduce down that check into something simpler okay and then this linear SCS proof that's actually a lot simpler checking that proof is equivalent to checking a bunch of pols on the same random Point okay and these bunch of polinomial are really nice but there's multi-linear okay they're a lot

simpler to check in general now the core idea okay is that well we have a bunch of polinomial checks why don't we try to reduce that down to the task of checking just a single giant polinomial we'll call that g okay so effectively what we do is we embed the evaluations of Q and evaluations of L1 and L2 and L3 and so forth into this giant polinomial by by effectively embedding them as lrange coeffic ients into this polinomial G and then we can take a random linear combination of all these coefficients as well uh to effectively ensure that you know uh instead of checking a bunch of uh evaluations of G and then checking the corresponding evaluations of Q and L1 L2 L3 we can instead check over a sum of evaluations of G so in particular you

know we get this very complex equation that just embeds all the evaluations of Q and L but obstructing that all way really what we're asking is a question about a sum of evaluations for this giant polinomial G and this is a textbook sum check statement which basically asks the question okay well prove to me that if you take a polinomial and evaluate in a bunch of points then you sum all those points you get a particular value of V so for those of you who are unfamiliar this can be viewed roughly as taking a discrete integral of this polinomial G okay so now the question is okay what can we do at this point this is still really a hard question you know like you know checking a bunch of points on the polinomial G and adding them all together but this is where the textbook

some check protocol comes in which is this General protocol or this General system to reduce a task of checking many points on this polinomial G to task of just checking a single random point on this giant polinomial G this is still quite a bit too complicated because this polinomial G is very complicated but what we observe next is this polinomial G can really be decomposed into a bunch of multi-linear polinomial effectively two sets of multilinear polins such that evaluating these multilinear polinomial in a particular random point R is effectively the same like you know after you get all these evaluations as evaluating G itself on that random Point okay so now we have these two sets of polinomial and what we observe is roughly the first set is is roughly

equivalent to checking the the original Pi ccs and the second one is roughly equivalent to checking the linearized proof okay and the other observation here that's important is that both these sets roughly have the same structure these pols have terms that are similar in certain parts okay and then what we can do at this point point is by linearity okay we can take a random linear combination of the evaluation checks on these polins to be just a single set of polinomial and we'll call that L1 Prime L2 Prime and L3 Prime okay and here's what the magic is remember at the very beginning I've mentioned that well checking the linearized CCS proof Pi is equivalent to checking a bunch of multilinear polinomial on the same point what we've effectively done here is now

reduce the task of checking a multi bunch of multilinear polinomial on the same point so now what we can do is just repackage this back up into the task of checking a new updated linearized CCS proof and we'll call that Pi Prime lccs so now effectively we've converted the task of checking a CCS proof and a linear CCS proof into a task of checking an updated linear CC proof CCS proof and because we've taken a random linear combination along the way we've made sure that things do not grow in size so effectively the output proof to be checked is equivalent to size of each of these input proofs to be checked okay so now with that effectively that concludes the high level idea of how hypernova folding scheme Works taking a step back

it's important to note that hypernova is not the only folding scheme out there and there's many many other folding schemes in particular so we introduced Nova in the spring of 20121 and introduced a uh full implementation that fall okay and ever since there's been a significant growth in adoption for this idea of Designing folding schemes for the particular application of Designing memory efficient uh uh incremental proofs okay and each of these folding schemes each of them gives different efficiency trade-offs with different benefits so you can pick the right folding scheme for your particular application okay and it's also important to keep in mind that taking an even further step back that really this this is just just another step in this larger picture of trying to design faster and

faster zero knowledge virtual machines in particular this idea started back in the early 2010s and kept growing at an increasingly rapid Pace until today we're at a was a significant growth in adoption for trying to design snarks for the application of virtual machine execution yeah what is does hypernova PCD work oh yeah so that that they didn't really have a name for their system um but it's like a generalization of hypernova to achieve uh PCD where they show effectively how to fold multiple instances at once uh instead of just two so the initial version of hypernova when we first released hypernova and fled two at a time uh they show how to F multiple and then like multiple instances at a time enables a more General primitive known as PCD

which considers IVC but for arbitrary dags which is useful for distributed computations as opposed like just VMS jolt um I guess by making heavy use of lookups or offline memory checking techniques only winds up with degree 2 constraints do you have a sense of sort of what that means for um hypernova and the need for high deegree constraints sure sure sure that that's a great question right so like in that particular case yes certainly we might not need hyd constraints then the key benefit of hypernova is the going from the two MSM to the 1 MSM so it'll just be the prover overhead that we'll be getting a main benefit from for jolt uh of course you know if you see ways to like Leverage hyd experience it's all

the better because hypernova definitely supports it but it's like not necessary to support it to get all the full benefits of hypernova um yeah so I I think that's what I would see the the benefit of hypernova versus Nova for jolt makes sense yeah and the uh guess another thing it'd be good to if you have thoughts on um is so I I guess the the folding approach um looks to minimize like the overhead of recursion like sort of how much work the prover is doing to prove it like dealt with proofs correctly along the way yeah rather than proving you know uh that it actually ran the program correctly sort of useless work yeah um and something that's not based on

folding inherently although it can hopefully combin be combined with folding like um you know jolt or pick your favorite zkm um that's deployed today or something um it you know doesn't try to you just sort of do Brute Force recursion not not minimizing the overhead of recursion um so I guess the question is um do do you just see the two approaches merging together uh do you think that there are um uh you know benefits of of what like should you should you just use pure folding um when you care about Pro space as Paramount and and otherwise uh you should um you know not focus just on

overhead of recursion just general that's a great question yeah so in general I would say that like yes eventually I do see a future where we use like something like jol's front end with like some sort of way to increment proof over time to save on the memories right and that could be hypernova or Nova in the back end um yeah so in general like for shorter programs today just like using like uh something like Spartan in the back end of jol that's like perfectly uh works for like the use cases for many use cases today right but if we want to imagine the future we want to improve upon memory you know we can use the hypernova back end and another question is you know like at what point like is the verification overhead actually worth it right because like jol's constraints if I remember

correctly per step is like below a 100 like some some crazy small number right and this is like compared to like the verification overhead of like like Nova right now which is like 10K right it's like orders the magnitude more so where I see these two techniques being like combined is we get this like approach where we amortize away the verification overhead um per many cycles of the virtual machine so we have like a maybe like a 600 6,000 Cycles or something like that then we can maybe start using recursion where the verification overhead won't be such a big hit anymore um so finding the right trade-off there that's a really cool like open question I think but I think eventually we'd fall somewhere in that trade-off instead of one end or the other yeah so the these

are two ends of a spectrum and you might not want to be at either oh yeah I think so does hypernova comes with uh zero knowledge or is it easy to add zero knowledge to Hova yeah that's a great question yeah so um this was uh what I had mentioned um in the second slide or something basically this idea like recursively hypernova immediately doesn't come with zero knowledge we could make it zero knowledge but um what we really need in practice is just you just have a final proof okay and you just want to make that zero knowledge and like maybe compress it even further uh before giving it to a verifier and that we've shown can be made zero knowledge so we add like a zero knowledge layer that proves the knowledge of an IVC proof very efficiently I guess there are like

still situations in practice where you actually do want the incremental proofs to be published and and there if you additionally need zero knowledge yeah then is there a simple way yes yes yes yes so this uh there's there's several things we're working on right now and trying to make it simpler but the sort of uh prototypical approach is to sort of use the split accumulation paper introduced I think it is Bens no uh buns and others back in 2020 uh basically this this idea that you could like fold in additional like a random instance effectively uh and that effectively ensures that your incremental proofs themselves also don't

reveal any information about what's uh what's going on under the hood great question is there more to to that um just getting the final proof rather than the incremental proofs ZK then using a ZK snark to prove you know the yeah so yeah it's not as as simple as just you know like throwing your your IVC verifier in circuit uh so we leverage the fact that our our the proofs the IVC proof itself for us for hypernova and for Nova and just the general architecture in general is is basically just a bunch of CCS instances or a bunch of relax R1 CS instances so and so forth so we can do some optimizations where we first fold them and then we prove it using spart or something like that so it's a lot more

efficient than using Universal circuits what sorts of cryptographic assumptions you use to build this yeah so uh a really just discret log for both hypernova and Nova basically we're just using a Pon uh commitment scheme and you only get the sound miss or because it's it's a recursion right if you want oh right okay so you're talking about like the recursive ass assumptions as well yes yes okay there are several non-standard assumptions associated with recursion as well uh specifically uh this is really digging into the weeds but uh effectively like we need to make a non-black boox assumption somewhere in there right because this is like a succinct proof of like a something that's like non- interactive right the non-black boox Assumption specifically is we have an interactive folding scheme uh we we prove his his knowledge sound

and then when we turn it into like non-interactive like using Fe mirror Paradigm we assume that the result is secure that's the sort of assumption we need to make like it's like an instantiating the random Oracle assumption and we assume that this is like compatible with recursion so if you have a folding scheme that's like sort of instantiated with the random Oracle and that's secure then you can recurse on top of it and you can still maintain security is is that the so those are still holistic even assuming random orle so this is like even deeper into the weeds you actually can't like unless you use like very specialized random Oracle models you actually can't prove the security of IBC in the random Oracle model specifically because you need to run the folding verifier inside a circuit and this folding verifier if it wants to inside a circuit like you can't

call a random orle um so that effectively forces us to have to instantiate the folding scheme uh ahead of time instantiate the orle ahead of time and this is like fundamentally built in into the sort of idea of recursion so popping up a level how does the comp views this kind of theistic based non-standard cryptography exemp well you get the efficiency that's fine but yeah from a craphy point of view are people worried yeah I um it varies a lot I'd say uh some people are like more open to these assumptions and other people are less open to it what I can say for with certainty is that there is like a lot of exciting research happening right now and like trying to like design like new like models that

like are are feasible like like you know we can believe these models but we can also prove the security of like things like IVC like complex cryptographer protocols like IVC inside these models um the the real question though is like you know can we actually believe these models CU these are like random Oracle models with like all sorts of weird like tweaks uh to actually make them compatible with the recursion um so yeah I think maybe maybe the lowest order bit right now though is like like exactly as like Halo quoted like there's like just no known assumptions on no known like attacks on recursion and like it's like sort of fair I think for now just to assume that like these sorts of sh consumptions are safe uh we we should continue studying them of course just like we studied the random Oracle model

um but you know I think like it's not going to like break any sort of systems anytime soon I think just to add to the discussion um there's there's a recent work that sort of uh overcomes this heris instantiation of random oracles okay uh what they did is they just say well let's let's take some hash function say it's uh like correlation intractable with with respect to some uh folding relations and then you can extract with the folding scheme like assume you're in the algebraic group model and then you just extract the witness through that through that R not using random oracles I see okay we should definitely talk about it then that sounds interesting

yeah we can talk about that great great great okay any other questions yeah so I think you said um even if you just go from Nova to hypernova um and you don't use anything greater than degree 2 I think you said there would still be some performance benefit um does that mean you've made like two sort of dependent improvements to Nova one in expressibility and another in performance yes so definitely you could view it that way but fundamentally like the big change from Nova to hypernova is we change the folding scheme and this folding scheme happens to have multi like dimensional benefits yeah like one is indeed like the overall Pro runtime is improved um from True group scale multiplications to just one so like

roughly per constraint you only have to do one group operation versus two um and yeah the other one is like hypernova more efficient supports a high degree constraints now Nova's own folding scheme can be like sort of like like extended in like a sort of natural way to support hydr constraints as well but that would like sort of quadratically blow up theer runtime and overhead and things like that that you don't want that so hypernova is like main like goal is to like get rid of these sorts of quadratic blowups and still handle hydrog straints efficiently [Applause]