Episode 277 - Nova and Beyond with Srinath Setty

Transcript

foreign [Music] welcome to zero knowledge I'm your host Anna Rose in this podcast we will be exploring the latest in zero knowledge research and the decentralized web as well as new paradigms that promise to change the way we interact and transact online [Music] and I interview srinath seti principal researcher at Microsoft research and the author of Spartan Nova Supernova hypernova and many more works we talk about his early research that led him to working on snarks the work he did on

folding schemes some check protocols and what he thinks is next for the ZK space Nova style accumulation schemes seem to be the Talk of the Town at the moment so it was great to finally get a chance to meet the author of a lot of this work now before kick off I do want to direct you to the ZK jobs board there you'll find jobs from Top teams working in ZK so if you're looking for your next job opportunity be sure to check it out and if you're looking to find great talent be sure to add your job to the jobs board today now Tanya will share a little bit about this week's sponsor foreign is changing the world and until now building ZK applications meant learning new chain-specific languages and complex cryptography but not anymore with snarkyjs the

easiest use of ZK SDK developers can add the magic of ZK to their apps using typescript whether you're targeting Mina the leading ZK blockchain or off-chain applications snarky Js from o of one Labs has you covered with support from infinite recursion in browse improving and so much more the full power of ZK is available to everyone visit snarkyjs.01 labs.org to get started you can also find the link in our show notes and now here's our episode [Music] today we're here with srinath seti principal researcher at Microsoft research welcome to the show srinath thank you Anna for inviting me here it's

great to be here and talk about I guess the Nova line of work amazing I've also invited Nico to join us hi Nico hi Nico you were recently on the ZK hack CK Summit episode and we had actually in that episode discussed sangria the work that you did which uses similar techniques similar folding techniques but in a different context and so yeah I asked you to join this episode to also help us dig into the topic a lot has changed since uh ZK hack ZK Summit so very excited for this discussion yeah I want to make a little side note too this episode came about because I mean I've just for the last month or so been immersed in Nova conversations and Nova workshops I also

saw Arielle gabizon get Nova pilled by Justin Drake Over dinner just a few weeks ago and we also had actually a listener Joseph who had emailed us a few months ago asking us to bring you on so a little shout out to Joseph for that tip and we're really happy to be able to do this episode I think as a starting point srinath let's learn a little bit about you how did you get to be working on ZK topics okay so I'm going to start with using ZK uh to mean something broader which includes all kinds of succinct arguments where there's a proof that is small and quick to verify uh so it all began when I started at least my journey into this area started

in my grad school where I started working on this system it's a storage system and we wanted to run it in a cloud but we wanted to guarantee that even if the storage service is compromised the clients of the customers of the service can get some security guarantees and liveness guarantees from the system so we wrote a paper about the system called Depot this was back in 2010 and as a result of working in this project I was thinking about how to sort of broaden this kind of work to also cover arbitrary competitions for example let's say there is a cloud service and the customers offload some sort of competition to the cloud this could be a

mapreduce job or it could be a database that executes some types of transactions and we want to guarantee that the cloud service cannot cheat so in particular it should be able to prove that it actually executed what it claims to execute so this sort of made us to explore this notion of probabilistically checkable proofs so we started looking into this area at the time there were no implementations of this Machinery so it was all in theory paper so we sort of uh asked this question can we actually implement this and use it in practice so it turned out that there are a lot of theoretical work like or many decades but if you look at the constructions

they sort of had this two properties one of them was their asymptotically efficient but they had gigantic constants or they were asymptotically I guess not as efficient but they had relatively smaller constants so either of them was not a good starting point to implement and they're also very very complicated to even write the algorithm and implement it in code so that's what that was actually the starting point of my PhD work at that time we're talking 2010 when you talk about this probabilistic proof work you weren't looking at snarks yet were you ah so it wasn't really I guess so the name snark didn't exist back then okay

uh so but if you look at this probabilistically checkable proofs uh they are very long proofs but you can't send them to the verifiers so the Brewer would commit to such long proofs using something like a Merkel tree and then the verifier uh checks some parts of this probabilistically checkable proof so there was an interactive protocol for doing this and then it was also turned on interactive so the snark protocol existed but the term snark did not exist back then okay but was this Proto snarks then were you kind of like were you working alongside the same work that became snarks yes so we sort of started exploring implementations of this PCP based arguments but it was very

difficult to implement in fact if you estimate the cost of doing this it would take trillions of years to just prove even simple statement so we spent so much time digging into this Theory then we came across this other work which was published in 2007 so this was also based on pcps but it was based on something called linear pcbs uh so these are pcbs that are sort of also used in the uh the other PCS which are also sometimes called short pcbs because they are asymptotically short but they are used as a first step to constructing the more efficient or more asymptotically efficient pcps so this linear pcbs are like if you write

it out they're exponentially large but the Insight in this 2007 paper was that you can commit to that exponentially such PCB with some polynomial work um and then you can have the verifier query this PCP at some points and then do its checks so this approach was actually very simple because it used a simple PCP and the cryptographic missionary was also somewhat simple it was used based on additively homomorphic encryption so it sort of served as a good point for us to implement and also optimize is this the line of work that eventually culminates with cross 16 yes exactly so what happened was uh so this

the linear PCP based sucks into argument so at least the the iko07 which is the paper that we started building and the system that we built was called pepper so this this first version was interactive so it had two rounds of interactions so the prover sent something the verifier asked some question and then the prover sends the answer and there is one more round of interactions and it was all based on standard cryptographic Primitives so actually there was one more downside to this approach which is uh this the Proverbs work in this construction is quadratic in the size of the circuit so in this work pepper we sort of try to mitigate this problem at least for some computations for example if you had a

structured computations like matrix multiplication or some polynomial evaluation we were able to avoid this quadratic blow up and then we were as like as follow-up work we were exploring this um a way to do this automatically where can we automatically build this linear PC piece that don't have this asymptotic overhead or the quadratic cars then what happened was there was this breakthrough work by ggpr this was back in 2012 that introduced the a snark that had a quasi-linear proverb for all computations but the snark was described as a sort of a monolithic object and then one of the observations that we made because we had already started

working in this linear PCP based arguments what we uh sort of realized was there was actually a linear PCP inside this ggpr uh so we uh did two things there one was we sort of separated um the constraint system that's used inside ggpr and also show that there is a linear PCP inside this construction and then we combine that linear PCP with the cryptographic Machinery that was inside this pepper we wrote another paper called zatar based on this work and then eventually there are like I guess refinements to ggpr that led to growth 16 and all of that was not interactive The Works that I did was interactive but based on standard

cryptographic assumptions so for Avid listeners of the podcast this is right in chapter one of Ariel's snark trilogy yeah we just recently did a three well Arielle gave us sort of a chapter by chapter history of snarks and this is actually very this this episode it might be good to listen to in tandem to sort of map it srinath I want to ask you as you were doing this work were you already at Microsoft no this was uh I was doing my PhD at UT Austin okay uh so this was between 2010 and 2012. so when did you join Microsoft yeah I joined Microsoft end of 2014. okay um so by then already there was ggpr uh there I

guess zatar paper resurrect and Pinocchio people was written yeah and there are also other papers that we had written in between what was the step to Microsoft were they building out some sort of cryptography do they did they already have a cryptography I don't know Institute or like part of their company like I'm just kind of curious like what was the draw to Microsoft what kind of work were you seeing yourself doing there so Microsoft research works on a broad range of topics in computer science and also Beyond as a as a grad student working in this computer science this was a very natural place for me to go and continue my research because there was potentially uh applications to cloud computing and other forms of

computing uh based on my work did they have focus on Starks or were you kind of bringing that into the org was there anyone else there working on ZK stuff yes so there are a lot of other researchers who worked on interactive groups they were already working at Microsoft research okay then tell me a little bit about the work you did there like what kind of research and I mean we definitely want to get to Nova but what kind of maybe led to Nova in your time there yeah so so when I joined Microsoft research I also spent a little bit of time on doing formal verification of distributed systems and cryptographic algorithms but then at some point I started working on this system called

spice so the goal of spice was to sort of continue the work that I was doing back in grad school but try to do it in a much more large-scale manner where we wanted to run a concurrent system in the cloud but have that system produce a proof that it was actually executing all the transactions in a succinct manner so this was a paper that we wrote back in 2018 where you can run a concurrent program or a system that executes different transactions concurrently and then there is a succin proof internally it uses growth 16 but it requires new techniques to both represent State and also execute transactions in a concurrent Manner and

in parallel so we also wrote another paper called piperine this has a timestamp of 2020 but it actually happened around right after the spice paper was published the goal of this piperine was to use this spice but in a blockchain context so what we wanted to do was execute these transactions in the cloud but to verify the execution on the blockchain by producing a succinct proof and this I guess around the same time there are also discussions in the ethereum community around roll ups so it's it's sort of I think one of those academic papers that described how to do this off-chain execution and

then verify on the blockchain and there was one property that we achieved in this piperine which is uh to provide liveness so even if this off chain entity goes away there is a way to recover the funds or tokens that were present in the off-chain system without really trusting the softchain systems I guess now a lot of this might sound obvious because everyone every system I suppose has this kind of functionality but back then I think it was one of those properties is always 2020 right yes exactly I had a question actually because you're mentioning Academia and academic papers and I sort of get the sense that your position is kind of at

the intersection of Industry Microsoft research and Academia is that actually what's happening or do you think you're more of an academic where would you situate yourself yeah that's a good question so uh I sort of think of myself as a person who works at the intersection of two different fields one of them is this uh systems or distributed systems and the other is cryptography uh so what I what I mean by this is uh I not only work on the theoretical aspects but I also work on the Practical aspects where I implement the algorithms build it in the context of an application evaluate it and it sort of goes both ways so the theoretical work is inspired by the

systems work and sometimes the system's work is inspired from the theoretical work going back to Nico's question do you see yourself as academic or industry do you have still a connection to the school or did you make the full shift over to Industry so Microsoft research sort of operates in both worlds on the one side we do research but on the other side we are also a company like we are part of a larger company so there is a blend of both the academic side of things and also industrial side of things so nice let's move in into the topic of the day Nova and I say Nova which is like the group of novas because there's now a few papers around this

topic tell us a little bit about like what inspired Nova where does this idea come from and what is it doing yeah so so one of the uh things that I always focused on in my work was to drive down the Proverbs cause so we want this proof generation cost to be as low as possible and this has always been a thorny problem going back to uh 2010 or even before well the cost of producing this proof has always been very high so when I worked on the systems like spice and pipine one of the patterns there was that the same kind of computation was executed over and over again

for example if there is a batch of transactions for every transaction the Brewer sort of has to do the same thing so one of the motivations for this normal work was to can be the question was can we leverage this pattern and speed up the Brewer substantially this led us to think about a way to uh compress the work that happens in two separate transactions into one which eventually led to the creation of folding schemes are folding schemes sort of the result like is does it follow the idea of recursion or would you say it's like a different kind of compression is it like working at a different level oh this this entire line of work was

definitely inspired by other projects that try to uh do better recursion like construct better recursive snarks most notably the Halo line of work okay so in Halo if the verifier circuit the circuit that verifies proof of a prior statement perform some checks and then it defers some expensive parts of it to the Future so in Nova what it's doing is it does not produce a snark instead it's able to fold statements at the the level of a statement itself where the Brewer commits to the stair the witness and then it runs this simple or inexpensive protocol to combine two statements into one but Halo didn't do

folding right was it doing the compression part kind of almost like a different point in the operation yes so so if you look at uh I guess the internals of the very fire there is some amount of folding that's going on in terms of uh the inner product statements so it is doing folding uh but at a a lower level of abstraction it writes out the proof and then while verifying this proof it folds certain steps in the verification is that Halo or is that a Nova oh this was Halo that's Halo Halo is doing that okay okay yeah the the way I like to see Halo is you do most of the verifiers work you get down to polynomials and rather than

checking uh your polynomial commitments you defer that to later so what you are folding is claims about polynomials you're like oh I have all these evaluations all these commitments I don't know if they match we'll see that much later and this is Halo not Halo 2 or are we kind of just grouping Halo work into one so we're grouping them together because they they sort of work uh pretty much in the same way got it so kind of moving towards this folding thing though what you said when you started to describe it was the fact that all of these operations are similar or like there's a similarity in what you're actually able to fold together would you say that this was inspired because Roll-Ups had kind of taken off this idea for and and as I understand it those

have that property which it's repetitive and consistent yes exactly I think uh if you look at the large-scale statements that uh I think people want to prove today I think most of them have some amount of structure to them and maybe explain what that means like and you can see I'm struggling a little bit to say this but it's like what's similar like I know that there's a similarity and there's these things that are similar to each other but what exactly does this data look like let's take the simple example of a roll up that's just doing some payment transactions okay for a batch of transactions if you look at the circuit it takes one transaction and then maybe checks some balances uh

updates State and then it goes to the next transaction it does the same thing so if you look at this circuit for executing a batch it consists of a sequence of sub circuits where each of those sub circuits are the same so you're saying though in a context like this Nova is useful but is it compressing multiple actions together in a folding sequence or is it like compressing steps that are coming one after another yes so so no uh targets uh what's what we call a sequential computation so let's say you have a a program uh where a teach step uh you execute some function f or some circuit

C and in The Next Step you execute the same thing maybe with different inputs potentially taking inputs from the previous step so it Targets this kind of sequential computation so I guess a little comparison question here because so this is what a VM does right the virtual machine it has a step function and it applies it many many times so so far people have been designing VMS inside Starks right because with each row of your Stark you have a step of your VM we could also do this with Nova right with steps of recursion I guess do you have any sort of comparison between these two methods maybe some back of the envelope calculations yeah I think they they sort of both Target a similar

computational model where there is a same sub circuits that are executed I guess uh one difference might be that with no uh because it's a recursive proof system uh and it also provides low recursion overheads uh you're able to do this in an incremental fashion where let's say you executed this computation for n steps and now you can take the proof produced at the end of the 10th step and update it with more steps and produce a proof for the updated computation whereas with Starks you can do the same thing but first you're done roll all the steps of the computation producer proof but then if you have to continue executing then you need something or

something people refer to as a recursive stock so more flexibility and I guess less prover work in the end Justin Drake had the slide that sort of shows this bifurcation in snarks like now we have this curve based uh arguments like Nova and then there is this hash based arguments one of those examples might be this fry based snarks like Starks so that is I think now these two lines of work uh I think there is more work needed to understand the trade-offs but at a I guess in a nutshell uh Nova provides inexpensive recursions I wanted to talk a bit more about the

internals of Nova because we've we've mentioned this folding idea of this repeated structure uh what else goes into Nova is there I guess a snark an arithmetization yes so uh so in Nova itself we uh focused on this simple R1 CS uh so that was the arithmetization that we used uh in that work and then uh after that it's it's mostly the folding scheme that allows you to recurse and the folding scheme internally uses a commitment uh to vectors uh some and it needs to be additively homomorphic meaning you can take two commitments add them into uh one to get a commitment to the sum of the underlying vectors those

are the only ingredients that are necessary to construct a recursive proof system but of course there is one downside I tell you to this in my thoughts whenever I talk about Nova is uh when you produce a proof with Nova the size of the proof is proportional to the size of one step of the recursor computation typically you don't it's it's going to be large because you might have large step sizes so what what we describe in our paper is a way to take that large proof and compress it into something smaller and that step requires a general purpose snark because we need the properties from the snark to compress this you just mentioned this additive

homomorphic property that it needed I think in a in the episode I did with Ariel I think we also talked about that like kzg it has that property right yes so in Nova we require this commitments to vectors that are additively homomorphic and you could instantiate this in different ways one of the ways we instantiated this was with Patterson commitments where uh you have a set of group elements that are sampled where nobody knows the relation discrete log relationship between them and now you can commit to the vector using that and this requires no trusted setup but of course I think you can also use kzg's SRS in place of these group elements to

as a commitment to vectors got it I want to ask a question a word that came up a lot in the workshops that I was at focused on Nova was like IVC I don't know if it was in the original Nova or later novas but what is that yeah IDC stands for incrementally verifiable computation so this um can be thought of as a primitive that defines the notion of producing a proof in an incremental manner where the poor executes a step produces a proof and then it executes another step and takes the proof that was previously produced and updates it to produce a proof for two steps and it keeps doing this so

This primitive defines this kind of proof generation process and was IVC already in the original Nova paper or was that introduced later so IVC the concept of IBC was introduced back in 2008. oh okay so Noah is a way to realize this uh IVC primitive in a more efficient manner what was the 2008 paper if you remember so this was a paper by Valiant okay I forget the name of the title then we we always quote it as valiant08 and I don't think people remember the title of it yeah we can try to dig it up and put it in the show notes okay so IVC is sort of what we're

realizing here with Nova and I wanted I guess to keep digging at the internals how does the folding scheme work or what's the like main mechanism behind it the main trick is uh something that we see very often in the proof systems take a random linear combination of different things so we start with two R1 CS instances that has their own witness vectors and the solvent CS instances have the same matrices meaning the same they are about the same circuit uh now if we take a random linear combination of these witness vectors there is this extra cross terms that show up so what the folding scheme does is it has the proverb commit to these cross terms or the error Vector first

and then the verifier sends a challenge that's going to be used for the random linear combination then the Brewer can combine the two witness vectors and also the two error vectors using this cross term and then the verifier can do the same but just by using additively homework commitment so the verifier is doing some group operations to do this so with this um description of folding there's also a similar thing described which is accumulation or split accumulation and I think there's been some confusion these days as to what these things mean or how do they compare do you have any insights there or any nice Frameworks for us to place this back together yeah one way to think about folding scheme is it's a

very simple version of a split accumulation scheme I think it places fewer requirements on the perimeter like all it needs to do is take two statements combine into one I think split accumulation captures even larger class of protocols these foldings can be described with the error term works for r1cs right and I think I've been noticing this thing where Academia likes to work with oncs but industry likes to work with this sort of plonkish arithmetization I was wondering if you had any thoughts and yeah if that motivates any extra work yes exactly that's a great question so we we were using R1 CSM though uh and then as you said like everyone Building Systems in

practice seem to be using plonkish yeah of writing circuits these days so we wanted to I guess extend know what to support these kinds of higher degree constraints is there a specific reason why people like plunkish or is it kind of a to know the the masses gathered around something and we can't move them anymore if you look at the R1 Cs long-ish and there is also this algebraic intermediate representation or air uh I think they have their own pros and cons for example in R1 Sears under some proof systems uh you can get linear combinations for free but the downside is you know it's restricted to certain types of degree two constraints and in

prolong cash uh this linear combinations don't exist but there are other features like higher degree constraints and also lookups sometimes people associate lookups with blockage but they can also be done in all of the three so there are I think pros and cons for each of these arithmetizations in fact this motivated another work that we recently published right before hypernova called customizable constrained systems so as we described in the paper one of the motivations for this work was to unify all these different constraint systems that people were using in practice and one of the observations that we made in this paper was there is a way to

describe a new constraint system system but that happens to be a slight generalization of r1cs and this generalization allows us to capture all of the three popular arithmetizations and it can do so with almost no overheads or no overheads in most of the cases and does that mean we can adapt the existing proof systems for r1cs to this new CCS yes exactly I think that was one of the results in this paper uh besides describing the constraint system was to show that if you had a snark for R1 CS here I'm talking about the non-recursive snarks something like Spartan which was originally designed for r1cs Marlin which was originally

also described for r1cs it easily translates to the CCS with almost no modifications and then because CCS covers flankish and r1cs we suddenly get a proof system for Planck ish [Music] Nico sangria was that kind of doing that as well so yeah sangria happened so when Supernova came out actually I suddenly got very excited about folding schemes and thoughts are it's a shame that it's only described for r1cs can we do this for plonkish so I sort of literally copied the ideas right like oh we take a random linear combination if it doesn't work we put in

a narrow vector and certainly we have this sort of generic way to do it for any kind of degree I think CCS goes further in saying like okay here's how you would describe plunkish in a different way but that is still amenable to being proven by things like Spartan or marlin so I guess I've now thrown in a new word Supernova um I think that was the paper that came out after and over right in the in the series before CCS like there we kind of skipped a step there uh can you tell us more about Supernova and how it compares to Nova yes so know why if we recall this computational model so it was executing uh same circuit at every step of the computation so this this model is

General as you said where we could encode the step of a VM as the circuit that's executed at each step so it's General enough but one issue is if you try to encode a step of a VM and that VM has many instructions or many op codes then the size of the circuit is going to be at least the sum of the sizes of circuits for each of those OP codes so at each step if you even if you didn't execute an opcode you're paying for that cost uh one extreme example might be let's say you have a VM where there's an instruction for executing some expensive hash function like catch act and there's another op code that just executes maybe an addition or a

multiplication then in the actual execution if you're doing an ielt or a model you're still paying for this other instructions like kit check that were not even invoked so our goal was uh what we call a la carte cost profile where can we build a proof system or a system where the Proverbs cost is proportional only to the cost of the instruction that was actually executed not on all of the supported instructions or opcodes and this led to this work called supernova nice and so that is kind of tangential to the other axis which is or when CS to more general or NCS and then from the

CCS you build hypernova yes yes it is uh tangential and also orthogonal so when the CCS abstraction existed one of the natural questions was uh can we apply this to NOAA can we build no one that can prove ccs uh I think around the same time sangria came out uh it was also using this error vectors or slack vectors so we could do the same in CCS where if we introduce relaxed CCS you could apply know what this relaxed CCS but the issue was that the degree of the constraint is D then you need uh need the prover to commit to D error terms or order DD spectrums so

this this was not useful because uh there was another application that we have been working on called this vdf which internally executes a a delay function and this is a very simple function that happens to be degree 5 uh so if you try to represent this delay function in CCS you can encode this degree 5 relation as one constraint whereas in R1 CS it's going to be three constraints but because the proverb is actually committing to D terms it does not actually give benefits over uh just using R1 CS so the girl in hypernova was actually to be able to prove CCS without

requiring the proverb to send this order the cross terms and then comes the mighty subject protocol right yes exactly and so the subject protocol was also used in this pattern paper so the way this pattern prover works is it starts with some statement and it applies the subject protocol and then it ends with some claims about some polynomials and then it proves those claims using additional invocations of the subject protocol so this sort of made me think about using the subject protocol as a 4 which eventually became hypernova hmm it's funny how this tool keeps popping up in different places does it have a

very specific cost profile is that why it's so attractive yes so so for example if you look at hyper nova itself so at each step the prover commits to the witness the minimal thing it's supposed to do and then to do the folding all it's just doing finite field operations which are much less expensive compared to cryptographic operations it's funny actually in the I keep throwing back to that episode with Arielle but at the very end we talked about folding Nova and then he had said that he had been like some check protocol pilled as well by Zach the same week he was Nova pilled and we talked a little bit about like would there be a way to combine it and

then the hypernova paper came out like two days later I think so because there you're using both of these techniques but you're not using like you're not using some checks all the way through you're just using them in a specific place right so I don't know why uses the subject protocol uh but it performs a single invocation of the some check protocol whereas if you look at a full-fledged snark like Spartan uh in the main protocol there are two invocations of the subject protocol and then Spartan also has something called a sparse polynomial commitment scheme where there are additional invocations of the subject protocol so if we compare Spartan with hypernova uh it's doing fewer subjects and fewer commitments actually I want to make a quick

correction actually to a previous episode I think in the I did an episode with Justin thaler and I think I incorrectly added him as an as an author of that but he wasn't he said he told me that after I just like set it on on the air so quick correction you were one of the authors of Spartan were you the only author there are other authors okay well I'm glad that we we get to make that correction officially on the zoon launch podcast and apologies for for mixing that up in the earlier episode no worries so that's super interesting though that you had actually been working on the some check work and then moved over to the fully and now you're starting to combine them in hypernova where do you go from here like do you add more some checks do you find

new ways that they can be combined if you look at hypernova itself if you look at the Proverbs work I think it's doing somewhat minimal work something that we expect the proverb to do commit to the witness and maybe do some finite field operations this might be a strong statement but maybe we have reached the sort of optimal point in terms of proper costs there but there are of course there are other aspects in hypernova that may be less optimal today I think one of those is the lookup argument I think this is an active area there are already like so many proposals for lookup arguments in the context of recursive arguments uh I think it's not clear what's the best one yet so there's also this this

protostartwork that came out recently which I think also proposes kind of a folding scheme using kind of some check ideas or are these related yes that's that's another interesting work uh that came out recently uh I think um the Brewer is doing somewhat similar work so the prover is committing to the witness and I think it's doing a similar number of finite field operations so the both the protostar and hypernova Brewer might have the same cost concretely as well I think the paper describes protostar for long cache uh whereas hypernova was described for ccs and there are some differences between the two in

particular CCS Witnesses are smaller than blankish Witnesses by an additive Factor equal to the number of copy constraints so maybe there are some differences in terms of the witness commitment costs there but I think one of the places where a protostar does better than hypernova is in the the verified circuit size in hypernova we require more hashes than protostar but in practice when using snark friendly hash functions I think the the difference might not be as much protostar paper also has a different lookup argument than what we described in hypernova so as I said this lookup argument the topic of lookup argument in

the context of recursive snarks might still be an open problem where what's the best lookup argument in this context you were mentioning in practice does that mean there's plans of implementations for hypernova yes we do plan to implement hypernova provider reference implementation for it in the near future yes I think that's one thing that's been widely loaded about Nova was the quality of the implementation so really looking forward to a hypernova repo thank you there's two concepts that you talked about just now and I actually don't know that we've really defined it so we mentioned some check you also mentioned vdfs which we have defined in

the past on the show maybe I'll start with the vdf side verifiable delay function why is that connected to what we're talking about why do vdfs matter in this in this case of like Nova or accumulation I I don't understand why they're connected yes so PDF which stands for this verifiable delay function the goal is to execute some delay function and also produce a proof that it was executed and there has been a lot of work on PDFs itself how to realize this and one of the ways of doing it is to combine what's called a delay function this is some function that takes non-trivial sequential time to compute

one of the examples is what's called min root and then take this delay function and combine with an IVC scheme where at each step the approver executes the delay function and also produces a proof that it has executed that so when the Nova paper came out so there was a lot of interest in using it to realize a vdf because it provided a less expensive power than prior recursors not constructions or require IVC schemes uh so this naturally led to this joint project between MSR supranational ethereum Foundation protocol labs and filecoin Foundation there was a blog post about this uh

using no and also I think Halo 2 to build a PDF using IVC I see okay so this is more like using Nova for a vdf yes not vdfs within accumulation schemes or anything like that yes exactly that was definitely where my confusion came because like I couldn't understand how it was used in that part of the stack okay I now want to Define and we probably should have done it a little earlier but like some check I feel like we've done a pretty good job of talking about accumulation of folding but not really the sub check that we've now introduced so what is that the subject protocol is a powerful Tool uh it's a it's an interactive proof it's again a protocol between a prover and a

verifier and uh it has this very specific interface where there's some polynomial let's call it G and then the evaluations of this G over some space are sum together so it's sum of evaluations of G or some space and the goal is for the proverb to be able to prove the sum equals some Target value T and obviously the verifier can just take the polynomial G evaluated toward all the points sum them together and check if it equals this target value T but the subject protocol provides a more efficient mechanism to do this check and the only thing that it requires from the

verifier is do some logarithmic number of operations and also evaluate this polynomial G at one point so in a hypernova starts using some check but were there other types of checks been used in the previous works the previous Nova works so the previous Nova work we would just do this random linear combination and have the poor commit to this extra terms that arise called slack terms or error terms and there was no need for the sump check protocol I see no I think what you're going for Anna is how did we construct snarks before the soundtrack protocol was so prevalent oh yeah Fair um and in that sense of all the snarks

that are popular today are using univariate polynomials and so they use very different techniques and a whole different toolbox where we like to do quotient checks and that's something completely different and from quotient checks we can build zero checks and from zero checks we can build other things similarly in the world of multilinear polynomials we can use the subject protocol to check a sum but checking a sum also allows us to check other things like checking that a vector is all zero elements and so that actually reduces to a subject there's a lot of there's a little toolbox essentially that you can build out with the some check as your core element yes okay so actually uh if you recall I had this slide in ZK Study Club uh there were I guess there was a

trilogy there a different Trilogy I think uh in the middle second stage there were all these works like plonk modeling on one side there was Spartan hyperplunk on the other side so the second one was called univariate polynomials and the first one was based on multi-linear polynomials so in all of these works on the the multilinear polynomial column they were already using some check and in the second one they used this quotient check for the same purpose cool we should dig that up and add that video to the show notes since we touched upon univariate multivariates I kind of have the sense that are the multi-linear polynomials allowing essentially more powerful

protocols it feels like you know all these linear time proofers come from protocol based on multilinear polynomials do you think there's some kind of trade-off there or is it just like strictly Superior yeah that's a good question I think um so this multi-linear polynomial sort of allow us to use the some check protocol internally it does not require doing any super linear operations like ffts or fast Fourier transforms which are also sometimes called entities so it does not require those operations uh one downside though is uh the proofs are logarithmic in the size of the statement proven so for example in the context of snarks so the proof size is going to be

logarithmic in the size of the circuit itself that's being proven whereas I think the schemes that are based on univariate polynomials the information Theory component I think has a constant number of field elements uh so when you combine this univariate polynomial based techniques with something like kcg you get a constant size proof whereas on the multi-linear side even if you combine with the best polynomial commitment scheme you still end up with some logarithmic number of field elements in the proof I think that's the trade-off that exists between the two one of them has a fast proverb but a log size proof in practice it might be small enough but on the other

side you have potentially more expensive Brewer but a smaller proof yeah that makes a lot of sense so I wanted to touch on a few technical questions since I have you here and since I've been also looking at similar ideas one thing is with hypernova protostar all these things the terms folding multi-folding accumulation split accumulation simple accumulation all are all being thrown around and um I have my own opinions on how they map to each other but do you have a simple framework for listeners who like me are very confused by all this yeah I think that's a good question uh so these different Primitives I think they're all different definitions there is a lot of overlap among them and it can get

confusing so I think uh affordings came in particular can be viewed as a simple version of split accumulation schemes so it's more specialized and also I think more easy to realize and also analyze and practice do you think that's why people have been latching on to folding recently more than these other schemes yeah I think the folding scheme definition itself is simple so it just takes two statements combines into one and the the security definitions are also easier to read because it's focused on this very simple goal perhaps that

makes it easy for someone to follow it and build on it nice okay and now slightly I guess on related question but still in the technical realm so we've been talking about IVC so incrementally verifiable computation how far can we increment I know there's like some I guess theoretical debate on how do we prove these systems and how do we prove these things secure is the limit real or is it just our inability to prove further I think it's so it's the latter so for example in our proofs we sort of assume or require that the depth of the recursion is a constant uh this is the case in all of the prior recursive arguments in the literature

but I think there are ways to mitigate this for example instead of doing this linear folding where at each step you take the prior proof and fold you could do binary trick folding this way the depth of the recursion is kept logarithmic in the number of steps and I think there are also other ways of getting around this issue where use stronger assumptions about the underlying Primitives okay and when we say a constant recursion depth do we have a number for that constant I think this is something that many people are investigating to establish concrete security bounds for these kinds of recursive arguments so I think we're at the end of the interview but I have a question I sort

of hinted at this before you've gone Nova Supernova hypernova what is the name of your next work where do you go from hyper do you go Goblin Nova I don't know if you've heard of goblin plonk but yeah there was a joke on Twitter they suggested a name I think if it was a gamma ray burst yeah okay ah very good so I had drawn up this little diagram this little Venn diagram it's the intersection of ZK anything astronomy and alcoholic beverages because ZK and alcoholic beverages we have plonk and

I'm trying to wiggle in sangria into there ZK and astronomy we have Supernova protostar astronomy and alcoholic beverages I'm sure we can find many there's amongst other there's a Champagne Supernova song but maybe there's something unexplored there right the intersection of CK alcoholic beverages and astronomy is that the next paper or is it time for spices to make a comeback ooh because you had pepper and zatar right yes so there was actually a long line pepper Ginger zorder allspice Buffet spice pepperine okay okay we have we have a new little circle in our Venn diagram and we need to find all the

intersections now yeah so funny how some of these works like if you think of the Poseidon that was all the um Greek gods I think and then you have the rescue which was all some superhero track that's funny cool so srinath thank you so much for coming on the show sharing with us sort of the story to Nova Supernova hypernova some checks folding schemes yeah thank you so much for this interview thank you Anna and Nico this has been great absolute pleasure thank you very much and I want to say thank you to the podcast team Henrik Rachel and Tanya and tour listeners thanks for listening