ZK9: The Red Wedding: Marrying DEEP-AIR + PLONK – Ferdinand Sauer & Alan Szepieniec (Neptune/Triton)

12 Apr 2023 · 24:00

Ferdinand Sauer and Alan Szepieniec of Neptune and Triton VM present The Red Wedding at ZK Summit 9 in Lisbon, a technique for combining the DEEP (Domain Extension to Eliminate Pretenders) method with PLONK to speed up STARK verification. They explain how STARK verifiers normally check a system's Arithmetic Intermediate Representation through repeated evaluations, and how merging both tricks collapses that into a single circuit verification at an out-of-domain point.

Speakers

Topics

Transcript

foreign [Music] speakers are Alan and Ferdinand from Triton VMS slash Neptune and what will you be telling us about something about a red wedding if I recall correctly oh well that sounds terrifying but good luck to chilly indeed thank you very much for the introduction hi everyone um my name is Ferdinand next to me is Alan we both work at and for Neptune which is a new cool upcoming L1 and we also both work on Triton VM which is a zero knowledge virtual machine

using Starks and this is also the topic of today's talk right we're going to start with a short summary off the talk so obviously we're going to be talking about Starks now Starks have obviously used fry all the time for the purpose of this talk we'll be treating that as a black box sort of delegate stuff to our vassal and I'm sure that's going to go all well um oh I guess these are a slightly outdated version of the slides

um there's about it's supposed to pop up the word fry now you'll see it in a bit um Starks also extensively use air or algebraic intermediate representation which encodes the rules of the computation that the Stark is talking about now there is a very well known trick to accelerate the computation of this air which is deep air and we'll be talking we will be presenting this year also but we claim no novelty here but as far as we know for the first time we'll also be throwing Planck into the mix and this final construction

will give us the Red Wedding and once we have that we can use that to lower the degree of our air which is really quite cool why do we want to do that well speeding up Starks is just generally cool but more importantly if you want to have recursion you really want the verifier to be as fast as possible because that means that you have pure psych accounts and that the recursive verifier is even like it benefits from this largely and a short note on the notation that

we're going to be using so we say Planck because that was sort of the working title or the work that we use during development of this um you can use plonk but you're not limited to that it's basically any snark and for the purpose of this presentation just imagine that we will be using fry also for this snark so it doesn't it's not limited to Kate commitments or anything like that and we will also be using that as mostly a black box right let's quickly review Starks so that we're all on the same page

so a stark works by initially having the execution Trace off your virtual machine this is the AET every row is a state that the machine had at some point and every column corresponds to a single register as it evolved over time the first thing you do is to low degree extend this this amounts to evaluation of sorry interpolation of every column as to get a polynomial and then evaluating it over a larger domain which then gives you what we call the base tables the prover commits to that by doing a

lot of hashing hashing every single row and then putting all those digests into a Merkle tree sending that commitment to the verifier allows then the verifier gives some Randomness back and that allows the prover to extend the space table which then arrives at the extension table and the semantics of this is basically to tie together several otherwise separated parts of your base table so in the case of the VM you can imagine that you have a main processor and maybe you have a [Music] chip and like a harsh co-processor and random access memory and so on and these this extension table

allows you that these components can talk to each other in a manner that is sound the prover also commits to this table in exactly the same fashion and then evaluates the air constraints to get a bunch of quotients this is then this is essential to prove that the rules of the virtual machine were being upheld the proof then also commits to this entire quotient table in exactly the same way get some more Randomness from the verifier sums up all the columns and then runs Fry on the resulting

combination code word what is abbreviated CC in the slide here running fry produces some indices where the verifier would like to get knowledge about the concrete row that is being used and so the approver Reveals All Those rows to the verifier upon receiving one such Row the verifier first checks that this row had actually been committed to and then it evaluates the air circuit itself to check that the row is actually consistent and it does that for every single row that it receives

lastly the verifier also sums up every individual row to get the combination code word the parts of the combination code words where the green arrows are pointing at and runs fry over that and that is the basic Stark and now we will start hacking on it Alan take it away Perfect all right strap in because this picture is about to get a whole lot more complicated so first thing instead of Computing the the combination code word we want to verify it so the prover is

going to commit to it giving us a new Merkle tree this Merkle tree was already there because it was part of fry but we were treating fry as a black box and now it's the same Merkel tree but now the Merkle tree is no longer inside the black box it's outside of the Black Box because it's there before fry starts so the prover Supply is the Merkel tree and the combination code word is going to be verified so we're going to pull out this summation symbol the green summation symbol and plug it into the circuit which we can totally do so the circuit is enlarged with the summation next up we're going to compress the quotients

given that the circuit already contains a sum with random weights we can actually move a part of this sum earlier on in the circuit and shrink the table the excuse me shrink the quotient rectangle down to a single column boom yay now we have more space on our slide there we go okay up next this is the Deep trick which we claim no novelty over I think it was first used in eth Stark um maybe even before that the idea is the fry verifier supplies a bunch of row indices where it wants a point in

order to run fry the Deep trick you can think of the fry verifier is indicating a new row but this row doesn't live in the table it's an out of domain point that does correspond to a row because you just evaluate the polynomials in that out of domain point but you can think of it as a row that doesn't live in these tables and then the verifier really just runs the circuit on the single out of the main row thereby generating a new pink Point corresponding to the evaluation of the combination code word

in that out of domain point and can use that pink point to update the fry points using the Deep trick so we went from T many evaluations of the circuit down to one evaluation of the circuit which is a big deal because the circuit is kind of big and we want to avoid having to do that work more often than necessary of the mechanics is just observing that some of the columns are redundant in a very particular sense that sense being they are fully determined by other columns

and so they don't really contribute much in a in some sense for example oftentimes we have constraints of this form if a equals zero then stuff happens and the way you algebraize that is if a excuse me a is different from zero or something happens and the way you arithmetize that is by introducing a new variable called B which contains the inverse of a if it exists and zero otherwise in the end you get multiple constraints and the key takeaway is that b is fully determined

after a is known in fact you can write b equals a to the power P minus two um and so B doesn't really contribute that much more information and and the prover can't even cheat with a high degree polynomial corresponding to B because B is bound to a and so we don't even need to prove the low degreeness of B anymore so we can omit B from the sum in the uh combination code word so basically uh we have fewer commands less something to do yay small small win

um also the prover doesn't actually need to transmit the entire out of the main row because the deterministic columns can be computed by the verifier from the variable part so in effect the rows become shorter yay more win this principle reminds me of something should remind you of something also the only reason why we're including those deterministic columns is because we need them for the circuit but for all other purposes we're trying to hide them and that's

sort of what snarks are supposed to do in a snark you're allowed to commit to a very long input with a very short string of cryptographic data effectively hiding all the witness information and so the question is what happens when we try to mix snarks plonk into the mix well the prover now has to evaluate the circuit and it has to prove the correct evaluation of this circuit on a commitment to the out of domain Row the purple Point corresponding to the

quotient and the pink Point corresponding to the combination code word still have to be explicit inputs because the sequence is important and the prover commits to the out of the main row then gets Randomness computes the quotient then gets more Randomness and computes the the combination codeword point in this construction the circuit is still not committed to so in order to prove the this circuit is satisfied the prover has to run through every gate and so does the verifier so the only thing that's achieved by this is actually shrinking the row um shrinking the proof size effectively

and the verifier gets to verify this partial Planck but still it's a rather slow verifier because the verifier has to run through every gate of the circuit now this point is rather artificial because once we're introducing a commitment to the row well we might as well commit to the circuit as well and that's where we're getting the the biggest speed up from essentially we're we're replacing the explicit representation of the circuit with a polynomial commitment to the circuit this uh allows us to Outsource a lot of

work to the indexer and so the online prover doesn't have to do that work anymore and certainly the verifier doesn't have to do that either this is where the big speed up for the verifier comes from because the verifier no longer needs to run through every gate of the circuit it can just run the Planck verifier and that is by assumption much much cheaper than running through 5000 Gates of the air circuit but this is not where it stops right because the entire orange row is hidden by a commitment and and so we don't really feel the cost of a long orange row

and that allows us to lower the degree of the air for instance if this is a constraint a times B squared minus C this constraint has degree three in three variables what we can do is we can introduce a new variable to lower the degree of this error at the expense of one more variable this represents the same circuit but the circuit that's not part of the slide the circuit is not as tall but is wider now but it's it's fine it's still equivalent but the nice thing is that a lower air

degree means a smaller blow up factor and therefore gives tables that are not as tall and so we have to run entities on smaller tables so that's the nice thing about chilled air yes and we need to do less hashing and the fry domain size is smaller meaning fry is faster too indeed so the picture changes quite dramatically we start from the a algebraic execution Trace and we extend this to the base table which is a lot less tall and we only care about the variable columns to begin with

we extend those to the extension table and so on still a single quotient column still one combination code word the rest of the picture is much the same the key point is already in this part of the slide the tables are a lot shorter which gives rise to a speed up for the prover which was not the objective of this entire exercise right we were trying to speed up the verifier and we succeeded in speeding up the verifier and and somehow we ended up with a faster prover too yay I guess absolutely uh yeah so the picture doesn't really change that much the point is is you can get get away with an air degree of two

at basically zero cost oops no that's all right I think we're there um right thank you very much Alan um so we're prepared a cost summary for this entire thing and this slide is the little dense in information so I'm not gonna run through the entire thing it is more meant as a consultation for later you mean this slide is the dance one yeah I figured this one is probably one of the most denseless ones so the point of this slide is um showing that the very far and the prover both Foster and as Alan said um well did you I'm not sure let's

highlight that again if you have a first approver and a faster verifier for the recursive verifier which is both that means that we have a compounding effect so in a sense the original goal of like getting a faster recursive verifier was very much achieved in that and I would like to leave you with about three insights from this talk the number one is put a snark inside your Stark it shifts workload from the verifier to the prover which is generally good the second point is that the verifier

does not need to know the out of domain row it only needs to be convinced that it exists and the third realization is that deterministic columns exist and that fact can and should be taking full advantage of that was the Red Wedding I'm glad that you all made it through thanks for having us [Applause] and with that we have a few minutes for questions does anyone have any questions oh all right uh it's got sort of a Zach and there's someone else in the

back as well if you have any questions raise your hand now just so I'm not like real time pointing at people hi everyone um now um I was wondering could you like would it be possible to articulate kind of the key differences between the Red Wedding and um just basically like doing the kind of the the stupid Brute Force thing of like taking the entire stock verification and everything out verification algorithm including you know opening all the commitments Etc and just shoving that inside a snark does that make any sense it doesn't make sense uh you would have a huge circuit for your indexer but since that's done uh offline

that cost is tolerable I I don't think I've thought about this line of questioning have you yeah yeah we I'm afraid the the cost comparison slide was already full uh so we weren't looking for questions uh to answer in addition to to the costs that were mentioned already there sorry sorry for adding confusion um Okay so sorry I'm I'm my I'm very supervised and sort of a munching up time but like would it be possible then to say like so what what specifically could you could you repeat again what specifically are the algorithms that you're shopping inside you the the snark What specifically are the algorithms

inside the the snack like this no there's this like the snock circuit you're creating um because it's it's like a subset of the of the stock of the stock verifier um yeah so the circuit in the snark yeah corresponds to the air constraints of the Stark okay great thank you that was it I think so okay all right there was one question in the back over there of our call correctly uh hi thanks for talk so is there any uh generic algorithm to do the automatic degree

um reduce uh yes yes there are uh you just uh iterate over a description of your multivariate polynomial and you find the first monomial with degree higher than two and within that monomial you find the first uh factor with degree higher than two and you introduce an extra variable Z equal to that factor and apply that substitution throughout so after apply the substitution you always get the highest degree of two right yeah you can't do lower than two unfortunately I can do lower than two I didn't get that but anyway uh I get answer thanks

does anybody else have any more questions all right Jeremy so just in terms of the snark inside the Stark so you're basically verifying a single row of the Starks circuit using a snark inside the Stark what like commitment schemes so don't you in order to make the snark verifier run inside the Stark you have to have some commitment scheme what sort of commitment schema are you using for that inner snark or am I missing something entirely we would be using fry again basically or still I suppose and then you can you can't even batch those fries

together does that make sense oh yes okay so in the end you even only have to run one fry I'm happy about that reaction cool no more questions from the audience well in that case I guess you're being released from your you know presentation early thank you both so much a round of applause [Applause]