zkSummit - Halo: Recursive Proofs without Trusted Setups - Sean Bowe (Electric Coin Company / Zcash)

Transcript

[Music] this is joint work with Jack Craig and Darrell hopper who are also my co-workers at the electric point company so the current progress of halo is that we have a paper outs on a print it is not very formalized there's no security arguments or anything like that right now it's actually quite a bit out of date I need to go home and push some things to it but and it's it's a work in progress but it's not really a shot in the dark it's what most of the ideas are pretty pretty grounded in existing protocols existing concepts so there's to me there's nothing new and there's there's not very many barriers in in the

way of actually getting formalization and security arguments especially with all these new papers coming out that are creating frameworks for helping analyze and communicate these ideas so we actually have an implementation so alongside the paper and we posted an implementation it's not just like work-in-progress one sort of because it really does work you can create recursive proofs with it we have a little demo where it where it recursively proves that the Bitcoin block hash is the result of like after ten blocks or something like that it goes to a depth of ten so it works but it's pretty slow and I'm in the progress

of making it a lot faster so I think it would be like five or eight times faster once I get around to pushing the code so to kind of motivate what's going on here with Halo let's imagine that you have a computation and you'd like me to run it for you so what you could do is you could split it up into a bunch of different steps and then in each step I could give you a proof that performs some state transition that corresponds with the step for the computation and then I give you all these proofs and you check them and now you're convinced that I perform the computation so far correctly and I can continue this on and if the computation doesn't stop for example if it's checking a blockchain or something like that but obviously one of

the major downsides of this of course is that I have to give you a proof every single time and if I give you a proof I need to give you all the previous proofs so you can check them so although this is iterative and it's quite nice it doesn't it's not succinct in that sense so you can't really create what we know is a succinct blockchain for example using this so what we need is we need a proof that can verify another proof so for example in this little diagram here we have a proof proof 2 which checks proof 1 as part of its verification circuit in common parlance and so it's responsible not only for checking proof 1 but it also checks to see if the state transition between state one and state two is

correct and proof three goes on to take proof 2 and check that and so in the end you can keep doing this over and over and ultimately you only have one proof that you check and that it sort of inductively proves or verifies all the proves that are nested underneath it which is great and this is kind of forms the foundation of its distinct blockchain there's two problems one is that in practice obviously creating proofs that are really efficient to verify inside of these circuits are really difficult but we have new proving systems we have snarks so that's that's something that we've begun to solve and then the other problem is that usually the verification procedure has to be

expressed in a language that the proving system itself can efficiently reason about so that it can actually verify it so this is something that you can solve for example just as a quick example of something that was done in the sexy paper where you have so we create to proving systems to pairing based snark proving systems built on two separate elliptic curves so we have this BL s12 curve that's about a 377 bit curve and then it is embedded within another curve that's created using the cox pinch method and the relationship between these two curves is that the scalar field for the cox pinch curve is the

base field for the BLS 12 curve and so the cox pinch curve can be used to efficiently vary by or perform group arithmetic inand and target target group arithmetic and so on is all the arithmetic you have to do as part of the pairing function efficiently for proofs that are created using the BLS twelve curve and then you can use the BLS twelve curve to also create snark curves so this is kind of an example of a fixed depth proof composition so you have a depth of one which is useful for sexy because that's all it needed was a depth of one for four what it was doing but this doesn't scale I mean if you want to do another depth you'd have to create another curve and these curves get larger and larger so this this

doesn't really work but this has been solved before the many years ago by le Benson son and I was Andrew Chia and around trim Erin medoras Roza back in 2014 where essentially we take a cycle of curves that are both pairing friendly that have it's the base field of one is the scalar field the other and vice versa we only know of one way to construct cycles like this and it's using these special MNT curves with very low embedding degrees and so as a result the the bit sizes need to be pretty large to compensate for the security

loss so what what does that mean well well there's a few different downsides one is that the keying material is large not symmetric but like a symmetric keys like elliptic curve points and things like that depending on your protocol that's not really ideal a little bit worse is the fact that the larger bit sizes mean that the multi axis are slower the scalar multiplications and FFTs and all this stuff are much more expensive proof sizes become larger blah blah blah but even worse is that it requires a trusted set up and set up for each curve and also up until recently for each circuit but this is something that we've begun to obviously fix so it's beginning last year with Groton and the others Mary

malar and so on had a paper that introduced the concept of updatable in Universal snarks and then sonic which was earlier Serg kind of introduced the first actual practical example of such an proving system and then obviously we've heard today about plunk and Marlin and all these other approaches that are improving on on Sonic now the interesting thing to note about Sonic is that Sonic isn't just a snark so it actually didn't start out as a snark it only became a snark in the last month because we really wanted to call it a snark so to get accepted the conference so he came up with a way to make it a snark so that's kind of the accident that really happened so so plunk and

Marlin are are really improvements on the succinct the fully succinct version of Sonic but before we had come up with that we actually had this only amortized succinct version of Sonic so I'm gonna go into detail about what that means here in a second so you've heard about polynomial commitment schemes 100 times today you they allow you to commit to a polynomial you can evaluate the polynomial at a point and the proof that you did so correctly and then we have these succinct polynomial commitment schemes which are essentially the the commitments and the proofs and the verification procedure all really fast usually so using kata scheme they're constant in the degree of the polynomial so these are really great for creating snarks like sonic and marilyn and so on

so I'm not going to really be talking about succinct polynomial commitment schemes today not very much so I'm just gonna focus on just a normal polynomial commitment scheme this isn't really formal description you need to be able to extract the polynomial and you want hiding properties and stuff like that but I'm just just curious about a formal description some of the previous talks did a better job of that so I'm gonna talk about the core protocol of Sonic real quick if you want to learn about how Sonic works in detail I have a talk that I did at Zeke on one which actually goes over all the arithmetic which I'd invite you to to watch so to start the prover in verifier this is an

interactive protocol a public point interactive protocol the prover verifier agree upon this polynomial K which is used to encode the public inputs the statement that's being proved and the the prover starts by committing to this polynomial R which encodes the witness or the auxilary inputs of the circuit and then the verifier replies with a challenge y and the prover responds with two commitments to Paloma commitments 1/2 this polynomial T which I'm not going to go into why or what it does it's essentially used as part of the argument to prove that the constraint system is satisfy to the circuit and another polynomial a commitment to this polynomial s and so actually the verifier needs to check to see if these

polynomial commitments are do the correct polynomials which it does here in a second but this polynomial s is important it encodes the circuit and so we're trusting at the beginning we're trusting or we want to check to see if the prover actually committed to the correct polynomial that encodes the circuit where Y is fixed but X is unknown so in the next step the the verifier replies with this this challenge X and then we checked a few things using the polynomial commitment scheme first off is the constraint system satisfied so we established this technicality but we establish this by checking that the commitment to the polynomial T has a constant term of zero and this is something actually the

polynomial commitment scheme gives you for free in our case we also have to check to see if this our polynomial is degree bound at a particular degree again a technicality I'm not going to go into but then we proceed to check these commitments that the proved assent and they'll in the previous round so we check to see if the T commitment is correct and so essentially we the polynomial commitment scheme to query these polynomials and then we check to see if some identity holds and then we're happy with that the real trick at the end of this so everything before this is actually at least in Sainik is really inexpensive to do the the hard part at the end is is the commitment to this s polynomial correct so did the

prover really commit to the correct polynomial that encodes the circuit so in Sainik we had two approaches one was a fully succinct approach which was really slow and people have been improving on it with like Marlon and plunk and so on but then there's a second approach which is actually really cool where if you have this third-party untrusted third party called a helper which is willing to construct an advice string for you using the proofs they can convince you that a batch of proofs many proofs are correct and that that this relationship that this polynomial of the commitment to this s pono meal is correct for each one of these proofs they can convince you with the same amount of effort that it takes to

asymptotically to check for one one of these proofs so this is really cool and so we call this amortize distinctness because essentially we're we're making it so the cost of verifying a bunch of proofs is about the same cost as verifying one using external help so how does this amortize the sickness work well okay like I said each proof has their it's a commitment or an alleged commitment to this s polynomial evaluated at the different Y's that correspond to the challenges for each one of these protocols and we want to check to see if each one of these commitments is correct now we could use linear work to check each one of them using some protocol but instead of doing this we have we we perform an

interactive argument where the the verifier with the helper where the verifier sends this challenge x and the helper responds with a commitment to this polynomial asks the same polynomial all these proofs uses the same polynomial because they're based on the same circuit it's the same polynomial but with X set the Y unknown and we proceed to in fact use the polynomial commitment scheme to evaluate the commitments that are adjacent to the proofs as well as the commitment that the helper provided at the points to check to see if they agree and if they do and if the polynomial commitment that the helper sent is correct this one that I've highlighted in right here then with

high probability the original commitments that are adjacent to the proofs are also correct and so now I only have to perform a linear amount of work to check that this last polynomial commitment is correct so that's that that's kind of the amortization procedure so I'm going to kind of abstract what just happened basically the proof had some value in it and the the the approver claimed that that value is the output of some function over some inputs and we had some strategy for taking a batch of proofs that have similar values but using different inputs but all over the same function and we amortized it so that the verifier could be convinced that all three of these values v1 v2 and

v3 were correct as long as this fourth value v4 is correct so this amortization process is kind of one of the core components of the technique that we use in Halo so the actual core component of halo is this thing called nested amortization so let's take an example where let's say we have a proof proof one in order to check the proof I'm just a computer or a human being I'm checking this proof I need to perform this expensive operation f over some input that's usually a challenge or something like that from the verification of the proof so okay that sucks now when I want to nest the proof

verification this gets tricky so instead of proof two checking the proof proof one completely which would require the proof two to verification circuit to actually encode the entire procedure F in it which would be expensive and what would it be linear time because this is representing a linear time operation instead of doing that the prover provides the value instead so here actually let me make sure that I'm explaining the correct slide so okay so the basic idea is that the prover is

going to witness the correct value of the output of this function f they're not going to compute it inside the circuit they're going to witness it they're gonna claim that it's the correct value and then as public inputs we're going to shuffle out the inputs and the outputs of this function and outside of the circuit the verifier is responsible for not only verifying proof two but also for verifying these additional values that were shuffled out as public inputs so the trick is when we get to prove to and this should actually say proof one there but when we get to proof two and we want to check proof one we have a problem inside of the proof to sort of predicate the circuit it not only needs to check

proof two which will involve running this F function of our new input but it will also need to check the inputs for the that I just spoke about that are the public inputs for proof proof one that were deferred that the proof two is responsible for checking so this is where the amortization product the procedure comes in play essentially instead of performing these two checks which are linear time we again we run this amortization process and then this produces two new values one value that's witnessed by the prover that's the output of the function and and the input to the function and we export that as public inputs so instead of you know in the previous slide instead of just

returning as four outputs for public inputs or whatever you want to call them to represent the the checks that need to be checked the linear time checks for the inner proofs we we combined them in each step of the recursion or each step of this nesting process so that you only ever have to check one and so outside of the circuit the verifier has to perform this check and this keeps going on and on so proof three when it checks proof two it takes these two values the public inputs and it amortizes them with the values that are created when it checks proof two and so on so this is a kind of an image that better captures what's going on it's essentially the same thing

as the previous slides it just shows that the the proof at any given time is given the amortized information from the previous proof it performs a verification procedure on the previous proof and now it runs an amortization operation between those two values to produce a new value that it exports as a public input and it just continually does this and so the the verifier on the on the outside of the circuit only needs to check this once so the consequence of this is that the the recursive proof doesn't grow in size and it doesn't increase in verification time regardless of how deep the this nesting goes how deep the recursion goes so the first thing that we can do with this technique

this nested amortization technique is we could for example we could build sonic on top of the mt 4 mt 6 cycles that the ones that for example code is going to use and we can use this nested amortization technique to make it so that we don't have to perform the entire succinct verification inside of the circuit we perform it outside of the circuit which which could be much more efficient because sonic is actually quite efficient when it's not in the fully succinct mode compared to plunk and Marlin so another thing we could do for example is we could actually switch and move to a different curve cycle so

instead of this MT for m and T 6 cycle where both curves are pairing friendly we could switch to a different cycle where we have a B n curve which is a prime order curve which forms a cycle with with another with another prime order curve a 381 bit curve for example which isn't prime which isn't pairing friendly and then over this non pairing friendly curve we could build any we could use any proving system which is bulletproof sore whatever now naively that this would seem to be really expensive because the verification circuit for let's say sonic or gosh 16 or whatever you build on top of this pairing friendly curve would have to do all the expensive multi exponentiation steps that are involved in verifying a bullet-proof so to solve that we can

apply the nested amortization technique so we construct a variant of Sonic built on top of the inner product argument which is from bullet proofs and so it it turns out it's pretty simple this is something that's been done before you know in the hyrax paper where they essentially took a piece of the inner product argument out and created a polynomial commitment scheme with it they I think in that paper they were using multi linear polynomial commitments but it doesn't really matter you can use you know very opponent commitments is what we need for Sonic and so we can take this protocol and it's actually proven zero knowledge and then and so on

and it fits all the definitions and requirements that we need once you finagle it a little bit for Sonic so what's really interesting is something I noticed is that the in this inner product argument is actually amenable to this amortisation strategy I go into this in the paper I don't have enough time to explain it on these slides but essentially we can apply the exact same amortization strategy that we do with the polynomials of for Sonic with the actual inner product argument itself as well and so as a result we can create this helped version of Sonic this this amortize distinctness without a trusted set up using the inner product argument using Sonic on top of this inner product

argument so as a result you can go back to our parent friendly non pairing friendly cycle and build a use and use halo instead of this variant of Sonic instead of Bullock roofs or whatever and you get a really efficient cycle that doesn't require the MNT curve so that's just step one it kind of gets you allows you to avoid the amenties curve cycle it's also in a cent it can be made fully succinct as well because the verifier of the grass 16 proof is constant so this the verification circuit for the halo proof is also gonna be constant sized so this this and with some other tricks you can make this fully succinct as well so

this is an interesting step but actually obviously the next step is pretty simple we just build a curve cycle where neither of the curves are pairing friendly and we use halo on both sides of this cycle and you get recursive proofs without a trusted setup so so in our paper we actually constructed to a curve cycle like this a 255 bit curve cycle which we affectionately call tweedledum and tweedledee and these are specially designed to work with the sonic proving system but I mean SEC P 256 k1 has such a cycle and I'm sure you could avoid needing to design specific curves for Sonic we just did this

because we wanted certain endomorphisms to be in play and we wanted larger roots of unity so we could do polynomial or a thematic really efficiently but so so so that's why we constructed our own curves for for a perfect concept so there's some more optimizations that go into Halo which I'd love to talk about but we take forever some of them are really interesting like circuit optimizations I think are really useful so I'll just go through kind of go through these real quickly so during the verification of a halo proof inside of this verification circuit sometimes it needs to perform field arithmetic on a non native field the native field to the other proving system on the other side of the cycle and so something that

we do is we actually commit to these values or we shuffle them and as public inputs to the other proving system and the other proving system is responsible for performing the arithmetic and checking for us so that's something that we do to avoid scalar or themá-- taking the wrong field arithmetic in the wrong field we also don't use the full challenge space because the when you're when you're verifying these inner product argument proofs the challenge space being extremely large that's full size of the field it's not necessary and it's really expensive we have to really conserve as many gates as possible so on that point we come up with several optimizations where basically instead of

mapping a challenge 128-bit challenge as a scalar and performing a point multiplication instead we map the challenges to special scalars in a in a still quite large challenge space that can be very efficiently computed using an ax and a morphism inside the circuit and we actually use a similar strategy to accelerate Peterson hashes so we have a more efficient version of Peterson hashes over over sapling which we use inside of our proof of concept the inner product argument the verifier needs to perform multiplications by squares we hash directly to the squares using some things that cause some potential soundness problems that I think can be fixed but so we're being very aggressive

and coming up with these ridiculous optimizations to eke as much performance out of this as possible and then this last point which actually hasn't been implemented yet but we can actually collapse all the inner product arguments inside of the verification circuit into one and that that gives you a huge boost in performance as well so I don't have a slide for this but the actual performance numbers for Halo I don't have them yet but I think the proofs will be around 10 to 15 kilobytes and we'll take I don't know it depends on your hardware but seconds or less than seconds they're less than a second maybe potentially to verify our recursive proof which is really good but of course that requires potentially a multi-threading on your on your machine

the proving time is actually really competitive with let's say fractal or whatever it's been the benchmarks that I've seen so conclusions like I said before there's a number of different techniques that we're using in Halo the most interesting technique is this nested amortization strategy which I think is really useful I think you can use this to improve all sorts of different protocols halo cheese recursive proof composition for the first time yes obviously debatable because we haven't really provided any security claim so you don't really know what we've achieved I claim that we have according to some abstract definition that's in my head of what we've achieved

we've achieved it like I said the necessary authorization technique is useful for for other things for example the MNT curve cycles where you can avoid that menti curve cycles but then also for example if you wanted to use fractal to achieve recursion and you didn't want to use halo for example hailer still very useful because the fractal verifier for example can check a large number of these halo proofs and use the nested amortization strategy so that the proof size is much smaller because fractal proofs are quite a bit larger than the kilobyte size lower bound or or so of Halo proofs the batching technique that we came up with for the inner

product argument isn't just something for Halo it's something you can use to accelerate bullet groups so a lot of people are really interested in that and I hear about it a lot the tricks that we're coming up with for the circuit using anamorphisms and all this other stuff I think will be really useful as people consider building public point interactive protocols and Fiat ramier implementations inside of verification circuits I think these kind of tricks will come in handy for protocols that do that I think we're one of the first protocols that are beginning to actually implement this sort of thing in practice we using elliptic curve arithmetic like I said faster Petersons hashes these interactive strategies between the

proving systems are really interesting and I think that opens some doors for some performance improvements and that's about it for me thanks cool all right I think we have time for like a few questions we are pushing a little bit back with Georgia so we can get set up in the meantime but if there are any questions or comments leave it for a moment anyone so it's a bit of an odd question just because my memory is really bad um the Tweedledee and Tweedledum curves are they are they twisted up let's go so

short barristers curves this reversers a it wouldn't be possible to make a curve cycle with twisted Edward's curves because they would the cofactor in the hospital all right are there any other questions okay the in the recursive step the the the the circuit the predicate is it growing like an iterated lock is it is it what right there looks like there's some iterated log growth it would be small but so every time you basically you have the log size circuit then you get some

new log size components you do the recursive step where you prove that you've run the verification circuit do you not get the growth of that circuit to be like an iterated log no the circuit stays the same size at every depa size are the same size not even a iterated log like log of n plus log no yeah it's the exact yeah it's the same size that it each step the recursion it doesn't change at all there's no additional state or anything it's just the same size [Applause]