zkStudyClub: Izaak Meckler o1Labs - Pickles

Transcript

so okay so we are here for a zk study club it's been a little while i think it's been like a couple months since our last one and for this session we have isaac mechler from o1 labs who's going to be talking about pickles he's going to be doing an overview into the entire concept and then look into the techniques and some of the lessons that were learned along the way there is just fyi a bit of a lag on this so if there's some awkward pauses that is because there might be some the sound delay uh through the zoom call but isaac if you hear me if you're good to go then take it away when you're ready

cool yeah thanks anna um so um yeah today i'm gonna be talking about pickles um it's basically uh a new snark construction which is you know based on a lot of work that others have been doing as well um and the library um what's significant about it is that there's no transit setup um that's like what's most significant for us like working on mina or you know what used to be koda um it has a pretty small proof size you know compared to some of the other systems that you might see out there like um starks for example um the provers is quite fast and the batch verifies quite fast as well and

then the thing that i'm sort of you know well that i really hope other people learn from especially is um there's a really nice interface for for doing recursion um and i think it's sort of like a it's a great way to program with a version i recommend people do it so um let's like talk about the kind of ingredients that that go into this smart construction um there's sort of two sides there's like the crypto side and then like the software engineering side so on the crypto side there's um halo type batching technique um or what what are people calling it accumulator technique and um curves that that dara constructed

um a kind of plonk system with specifically tailored custom constraints um and like a very sort of tuned poseidon hash function um on the software engineering side yeah there's this sort of kind of really nice simple recursion proof composition interface um and also backwards compatibility with ranking constraint systems and um all of the other kinds of constraints that we were using already in uh oh yeah if it's confusing to people so like i used to work on a project called well i worked on a project that used to be called coda and now it's called mina so i'm gonna say mina um yeah so this backwards compatibility is really uh

essential for me now because it means we didn't have to scrap anything so um i i might also talk a little bit at the end if there's time about snacks snaps which are uh essentially snark based kind of smart contracts on you know and that's what we're using pickles for also okay so i mean i probably don't need to do it for the people here but maybe i'll just do it for the sake of the video because i watched some other ones and everyone else did kind of an overview of what snarks are so i guess i guess i will too um right so you know the kind of uh uh you know ideal functionality that snarks provide are like you're a little verifier um and uh you want to learn some some truth

some statement and you know somehow like some god or something sends you down a proof which is sort of you know on your scale not on the scale of a god who can comprehend uh the the real the real facts that would lead you to believe the statement and the verifier can be convinced of this statement without having to sort of you know be a god shall we say um and what's cool about snarks is even if you're not really talking to a god but you're talking to some devil you can also still uh be convinced and there's no way the devil can trick you so um you know in in reality there well at least i haven't had experience

with the gods or devils there's just people and um you know you want to learn something some knowledge produced by some other people in in reality so you know these these proofs are not really produced by gods or even devils they're produced by other people um and uh you know let's this is to kind of motivate recursion um think about you're like a student and you want to learn a very refined idea but that refined idea it builds on you know say the sum total of human knowledge and so it's not really reasonable for you to sort of reread all this yourself that would be too hard it would take too long so you know the ideal situation would be we could call call up some god and they would

you know compress them some total human knowledge into some little proof uh whenever we need it on demand and we could just add that to the student um but you know that that's kind of expensive because it's very you know we don't get to uh talk to a god very often um so what we really like is some way that even if even if like later um you know uh someone kind of makes some partial progress like they build on top of this idea we don't then won't have to go call a god again and have them recompress the whole pile because you know ideally we could just sort of update what we what the the sort of proof that we got from the god prior and uh without having to recontact them it's very tricky to contact about so uh what's uh you know what what kind

of saves you in the situation is that very often your computations will be sort of have some kind of local structure where each part of the computation only depends on a small amount of uh information from uh uh other parts of the computation shall we say um and you know so what what this looks like is you sort of have all these little provers maybe maybe you know greater than the student but not so much greater who uh throughout time build on each other and at the end you know they sort of have some way of combining all of their knowledge across time and they can give you uh the latest the latest knowledge easily digestible at any given moment um okay so that's some kind of silly motivation

um right so the usual setting with the snark you have statement um and you you know you get some proof corresponding to that statement and then you can easily check this this proof statement pair um with recursive starks what that lets you do is is basically take the previous proof um and previous statement and uh kind of update it so let's see so uh you know suppose we had some statement s1 and that arrives at the first moment and then later on we get some statement s2 and we would like to prove their conjunction s1 and s2 say without having to do all of the work uh that was required to produce this

proof pi 1. so what recursive stocks enable is the ability to do just this to basically reuse the computation that was done previously to produce pi 2 or pi 1 rather in producing this new statement which is sort of composed of uh s the previous one and also some some new information um and you know that can just go on and on so like then sometime later a proof s3 come comes around um and we can prove some statements say like s1 and s2 and s3 um while only relying on pi 2 not having to go all the way back

and redo this computation or redo this computation or even to look at this proof necessarily so uh to kind of sum it up recursive snarks or recursive composition of snarks uh is useful for when you want to prove a sort of ever updating uh usually kind of over time statement in such a way that the previous proof can also be updated along with the statement without having to redo all the work and just to make it maybe a little bit more concrete um with snarks we know uh let's say you could prove a statement of the form oh iterating f yields 43 you know like f of f of blah blah of zero or something

equals 43. and we know with snarks like even if this took a thousand years you could you could convince someone uh easily that that uh that that would be true but you know with sort of vanilla snarks or whatever if then you wanted to say oh but if you do it for a thousand one years you know you get 45 you'd have to redo the whole whole computer i think we lost your audio i it's gonna work this time i can tell um cool so yeah we were talking about like let's say you wanted to prove to someone like

yeah if i iterate the function for a thousand years like you get you got 43 and you wanted to run it for another year um with regular snarks you just have to recompute everything from scratch with recursive snarks you can do this kind of 01 update um where you can reuse the computation that you did before with the old proof um to produce this new proof that has the sort of extended information um cool so you know and like the kind of example that uh is i don't know my day-to-day example is uh you would have a statement like there is a blockchain of length 1000 such that the final state is s1 then you know you'd want to add one block and prove there's a blockchain of length 2001 such that the final state is s2 i mean

you wouldn't want to recompute everything um cool so i'm just going to move on a little bit just for time we can go back maybe later and i will talk just give a little bit of a brief review on um accumulation what dare what is this called accumulation scheme accumulation uh yes yeah something like that um so uh this is a this is a technique for for doing recursion it's like the halo technique and um it's it's very important so uh let's say that we have like a narc which i never heard anyone say that but that's would be un like a non-succinct snark

i say that you say narc yes okay yeah so we have an arc where the verifier has sort of two components it has a fast part um v sub f and when i say fast i'm saying like you know the real relevant metric is like arithmetic circuit complexity but you know we can sort of imagine our minds the fast part is like 1 to 30 milliseconds let's say and then there's a slow part which is like 100 milliseconds to like a second or so and uh the verifier has this structure and moreover um there's sort of an update algorithm which uh and a notion of like a proof state okay such that uh instead of you know when you want to

verify a proof pi 1 instead of running the both the fast part vf and the slow part you can just run the fast part and sort of run this update algorithm to transform your proof state as zero into a new proof state s1 which then later if the mood strikes you you can feed into v slow this the slow part of verifier and sort of finish off the verification but crucially you don't need to do that if you don't want to so uh let's say you know then let's say you're in the setting where like you're sort of repeatedly extending a statement right like like we were kind of talking about

before um what you can do uh let's say you want to sort of do recursive composition and you know update kind of the previous proof with some new information when you're recursively composing you don't have to stick this whole uh v sub s in the circuit uh instead you just put the update algorithm and vf in the circuit and then outside the circuit you sort of expose the proof state as like a public input and uh then outside of the circuit you can run the s at any given point to sort of finalize the verification um right so uh the the the kind of idea here is that somehow this like

this this proof state and update algorithm and vs they kind of work together in some way so that this accumulated proof state somehow kind of like encodes all of the other uh proof states that you had to run into vs also and kind of lets you you know implicitly run um oh this should be s v s on on the old proof of states as well so somehow you know by the way this update algorithm works it works in such a way that the proof stated spits out it includes all it accumulates all of the previous ones as well and as i mentioned this this is sufficient for recursion you don't need a full uh snark you just need an accumulatable narc or whatever for uh recursion in some sense um depending on

what exactly performance characteristics are sufficient for your application because as i mentioned this gray outline you should think of as like a circuit this is like the boundary of a circuit so inside your circuit what you'll put is the fast part of the verifier and the update algorithm and what you'll prove is like i know a proof pi 1 such that the fast part of the verifier passes and i know the previous proof state such that if you feed that with pi 1 into the update algorithm the output is s1 um and this s1 will then be a public input which then the next time you go to compose um you'll prove

uh you know i know a proof by two um such that the fast part uh you know of the verifier passes on pi 2 and also pi 2 passed you know our recursive statement with output pi s1 and if you feed that s1 into the update algorithm with pi 2 you'll get some new proof state s2 and so the whole time you're never running this slow part of the verifier in the circuit um until the very end uh let's say you compose one more time until the end you take this uh accumulated proof state that's s3 um and and and you do feed that into the final slow verifier and because of how the accumulation scheme works

um that uh is equivalent more or less to you know in terms of the information content to also having verified uh all the sort of previous proofs um cool so does that appeal these people interrupt me as well um i'm gonna try and keep an eye on the child but so so just to clarify at the end you need to run both the last vf and uh vs is that right right yeah and i don't know i never i i have to admit i actually didn't read that paper where they formalized uh this concept so my notation might clash with theirs i don't know uh i think that's roughly correct the thing about that paper is it doesn't

formalize the sort of the bouncing between two curves but i guess you haven't got to that anyway yeah i yeah i mean i i feel like you're in the formalism you can kind of hide that underneath like this is general enough to capture that under the covers you know i don't know anyway um okay so i i yeah i don't know if i'll talk about that it's somehow that's kind of hard to talk about so um right so and you know practically speaking uh there's this fact from halo which is if you have well i guess it's sort of implicit in halo and then maybe made more explicit by that uh followed paper um if you have like an

iop let's say um like an interactive oracle proof an algebraic iop like where the messages are polynomials like marlin or blanc or sonic um and you have uh this well there's this uh a particular inner product argument from which you can construct a polynomial commitment scheme then uh you can you can build a sort of quasi-succinct uh recursive snark i don't know if there's an existing terminology for this equality's same kind of made sense to me where um the verification time is not constant or logarithmic necessarily ins well the verification type is just different from the kind of verification time we

usually talked about for snarks so usually you know you said something like the verification time is constant in in the circuit size or the verification time is logarithmic in the circuit size or square root of the circuit size here the verification time is linear in the size of a single sort of step of the proportion and we can talk a little bit it's really easy to understand what a single step means from examples maybe if you haven't spent too much time programming with these things or thinking about them then like it's not totally obvious but anyway um cool oh i guess i am going to talk about it so there's kind of one hitch with this whole setup uh which is uh right this v f it's not really monolithic it really kind of

splits into two little fast verifiers one of which operates on a field f and the other other one of which you know performs operations in the group g and uh you know the trouble with this whole recursive snark thing always is that uh this field f is is not the base field of this curve so you know you run into a situation where like uh oh only one of these is going to be efficient to put inside of a circuit that they can't both be you know uh okay maybe if someone wants to tell me about uh look up look up or whatever we can talk later but um anyway straightforwardly like one of them's gonna be really efficient one of them's not gonna be

even if you have lookups it's it's maybe 10 to 100 times slower so okay cool um all right so uh right so then there's this technique uh which we can call say deferring arithmetic which is you know remember before we had what did we do inside of our circuit we we we ran v sub f and we ran um uh u the update algorithm so instead um what we're going to do is sort of you know we take our v sub f it splits into v sub math vba math bbf and v sub math bbg and um we pull out the the field part of it

outside of the verifier outside of this first circuit and uh we only perform the v sub g part and the u part and we uh you know we we sort of exposed the bits of the proof that are necessary in terms of um in order to run this v sub f part of the verifier um and you know you want to try and be as clever as you can be here in in computing like what are the parts that are really necessary and you know trying to shrink that down as much as possible um because we'll get into it but like you pay quite a price for public input for public inputs maybe dara has some scheme i don't quite know what you all are doing with that but um so yeah that's that uh now you know now

that we have maybe some idea and if people are like uh i don't really understand anything you said so far we can take a break here because i'm about to sort of change topics does anyone uh have any questions or you can roll in the sort of this pi i minus one limited to the stuff required for vf into the the state s i i g s q or whatever s i right yeah yeah you can i guess you can think of yeah logically separate but yeah you can bundle them together i mean they don't have to be logic i mean if you like go to the accumulation scheme this is basically you can make it as part of the accumulator right

so so normally you want to make the accumulation scheme as simple as possible so that you can you can kind of plug and play between different accumulation schemes and they don't depend on the um the proving system um i guess it just depends on how you want to define your predicate that is being accumulated but anyway sure yeah sure you you clearly can do that um it's just that you if you want um for example so when we're switching from halo 1 to halo 2 that's just changing the proving system it's not changing the accumulation stream at home so it's

convenient to be able to do that let's carry on all right um i'll move on i suppose so um right so now let's kind of talk about concretely like what are some of the tricks uh to really optimize recursion in this setting um so i i ran just kind of for fun i guess i i ran like an encoding of uh the the circuit just using r1cs and um uh you know the naive like just reducing from r1cs it was like two to the 20-ish constraints or something like that and then with custom constraints for a circuit that i only really know about circuits that

verify two proofs uh and i think i have a profile from one that verifies one proves i don't quite remember um for for once they verify the two proofs it's like two to the 17 ish you know with a little more work it would be to the 17th um but right now like two to 18-ish constraints so like uh quite a quite a big factor um you know what's important to to look at uh you always want to just look at like what are the main operations that are being performed and just optimize the heck out of them so there's hashing um from from the sponge in the feature mirror um there's scalar multiplications there's like this endoscaling thing um there's unpacking uh fields into bit

strings and then there's checking boolean-ness actually i prefer boolean-ness than booleanity of uh of bits and thankfully like due to you know how plonk works this is mostly free in almost every uh instance which is really cool um so let's like just this is a a flame graph uh of the actual circuit um that does the what we saw before with the v f v sub f and so on um uh let's like just take a look at it just to kind of get a concrete feel for for for what things look like um so you can see the whole thing is like oops it's like 85 000

constraints um oh shout out to matthew for making this awesome flame graph tool uh it's it's great um that is really cool isn't this great yeah it's i i don't know how i would have uh like fixed all the performance bugs without this um so uh right so we didn't talk about it but you yeah so okay there's this technique i feel like everyone knows about a banana but maybe not which is like you all you sort of alternate because there's this mismatch between the field and and the group operations you you like alternate uh circuits from two different proof systems which have sort of matched

like you know the field of one is the group is the group size of the other and the the group size of the other is the base field of the one um so you sort of go back and forth so this uh first bit here is like running b sub f kind of on the previous um the previous guys uh you know uh pi pi restricted f or whatever um this is probably longer than it should be i don't know 10 000 constraints seems like kind of a lot to me um this uh this is like processing um the public inputs which are like these deferred values you can see it's like a real waste of time so you know there's so many public inputs i

don't know one two three four five six seven it's like 20 something and these are a bunch of scalar multiplications all these purple little purple blocks this is hashing these little stripes here that's like in the sponge that's fine um and then this bit is the inner product argument verifier like the v sub g the group operations part of the inner product argument verifier um you have some scale multiplications the planck verifier has to do some scalar multiplies and then this you can really just look at this and see that well if you thought about it long enough or if you worked had to work with it long enough you can really look at this and just see the inner product argument verifier because here uh you know this bit here is like computing all the challenges um for one per round and this bit here

is is doing all of the uh endo scalings uh in the kind of logarithmically sized the msm or whatever 18 rounds right yeah this is like eight we can count one two three four okay okay um cool so uh that's just you know gives you a flavor of like okay what's left optimized blah blah you there's definitely like a lot of room to fix like like i feel like this being ten thousand constraints is absurd like that just should not um your your intuition is correct yeah um like uh let's see what else uh we we haven't uh we haven't spent much time on like we've

designed custom constraints for like different column numbers or whatever but this is just using three columns um and so i think probably if you use some other number of columns you can probably get better performance but whatever um yeah otherwise i don't know so uh let's see moving on let me just uh you know probably not that many people have really spent that much time with kind of punk style custom constraints so just some some notes um what these are for it's for letting you take advantage of repeated structure in your circuit so like as you can see like the circuit is very repetitive right like it does a bunch of hashes it does a bunch of like scalar multiplications it does a bunch of these like

endoscaling things like the fact that you can just like you know make a flame graph and just like see all the components of the circuit tells you that the amount of like kind of one-off logic is like pretty low um so uh and as we said you know what are what are these repeated things like scaling endoscaling oh running the poseidon hash function and um packing bit strings actually we didn't do this yet there's a lot of performance to gain from doing that um or you know just any operation performed frequently there was one little question in the chat by the way um maritza maurizio do you want to say it i suppose these timings are just for

witness computations oh these are actually constraints so um yeah this is like it's not really time it's just number of constraints does that make sense so it says milliseconds but one millisecond equals one thousand constraints yeah um cool yeah we just reused the chrome thingy um so uh yeah with hashing like let me just talk a little bit about kind of the choices hash function um there's a few you know reasonable possibilities you could go with like there's rescue there's poseidon um i guess there's

peter snatching i guess not really because you need like random article but i didn't yeah i don't know i didn't think too much about it um rescue uh you know it has this uh this s box sometimes which is like x to the you have to take an alpha root for alpha equal to like five or something um so uh you know this is really slow um on like a cpu so this was kind of what ruled this out for us um and then also let me just say like potentially this is not a huge deal because like there's only two kinds of rounds but um the fact that there's this like alternating round structure

um you know sometimes you have x the alpha and sometimes you have x to the one over alpha that does increase the the price that you pay um in in terms of verifier performance a little bit and verification key size um and i guess proof size a little bit um uh yeah for your final proof because because it's not totally homogeneous um so the more homogeneous the better um poseidon it only has these x the alpha s boxes the sort of you know usual way is they did this partial rounds thing to try and make it more efficient on cpu but the thing is it's already way more efficient than um rescue is because of these x the one over alphas so actually what we've done is it makes

sense both from a security and uh prover performance you know circuit performance perspective is we just don't have any partial rounds so like only four rounds um in in our poseidon um and and that is better because uh you know you have a more homogeneous circuit structure more yeah so you know you don't pay you can save on verification key size uh proof size uh verifier time a little bit um interesting um i think if you go with um a larger number of columns then you can pack um a full rescue round so two steps into a single row of the circuit for a planck style circuit yeah that

that makes sense we we haven't um but it's it's still really expensive to compute outside the second yeah um cool so uh let me tell a bit about this endoscopy technique because i think actually this technique is actually really useful um and this is something that i i shawn and dara are and i'm not sure who else uh came up with um i i think i think this was something that people used to spend a lot of time on uh using like curve endomorphisms to speed up scan multiplications and stuff but it's really useful inside of circuits um so uh what's the idea here uh the idea is there's some function

like fee um which takes a bit string and a group element and and gives you a group element and uh this function it's you know it's equal to some other function just of the bit string which maps like into the scalar field of g times g so it's like this function like somehow it lets you compute uh a scalar multiplied by some scalar which is related by varfy to um the the bit string s um and this function varfee is injective on small enough uh inputs um we're small enough you know i'm not

sure what it is but it's small enough um yeah so why do you care about this uh because actually this capital fee is more efficient than just like straight up scaling by a number um and and this is good whenever uh you you can use this wherever like the specific number that you're scaling by doesn't really matter um so for example uh if very often in in you know elliptic curve or whatever group d-log group-based protocols you have you scale something by some random challenge this is a perfect setting for this optimization because you don't really care what the challenge is you just care that it's sampled from a large enough uh set of positive distribution of

possibilities and for those who are familiar with this inner product argument thing like you have these challenges like x i and um uh well depending which one you're using it could either be x i squared or maybe just x i vanilla um to the one um and so uh you know in that setting uh uh yeah you you it's great because you these don't have to be like a real you don't have to be like a real scalar multiplication because you don't really care what the x's are you just care that they're sort of have enough entropy and because uh this varfee is injective enough or injected on small enough bit strings then it will have enough entropy uh by the way if if you want to compute whether it is injective on a

given curve there's some code in andera slash tweedle to do that okay cool um right so uh unfortunately sometimes you don't have total control over the scalar um and it's like you know it has to be some specific thing um and so uh you want some fast ways to do scale multiplication um dara has given a fast algorithm for the following function um which uh is scalar multiplication but then you have this kind of thing that you need to correct for which is like uh you know you want to do you want to do

t times g but this algorithm doesn't let you do that it lets you only do t plus two to the size of t and bits minus one times g so you need to come up with some uh way of uh kind of correcting this and there's depending on the set like exact setting there's a bunch of um things you can do often uh when s is part of the witness you can replace it you can just replace it with uh you know s s minus two to the n and just kind of witness that instead and then as long as in that setting you won't hit any of the edge cases um this is fine and you can just compute s times g this this way um uh the other way of doing it is if if

the base of the scalar multiply that you want to do is sort of statically known or almost known you know known up to a small amount of computation that you need to disambiguate you can also just pre-compute this correction of like two to the n times g and just kind of subtract it off at the end um yeah uh cool so now uh that's just kind of on on optimization broadly and we'll at the end we'll visit like okay what are some other optimizations you can do and so on um in future um but let me just talk a little bit about programming with recursion now because this is really in my opinion like the best interface and whenever if people ever like write other libraries in other languages i hope that they use a similar interface

because i think it's great um okay so like let's see an example of actually using the recursion library so let's say we want to prove statements of the form uh our statements which are like you know the public input will be x okay and what we'll prove at x is x is of the form hash of hash of hash of hash of hash to pass of zero some number of times you know exists a number of times such that x is out of this form so uh here's how we do it we give basically a set of uh inductive rules you could say so the first rule just says okay uh this is a public input the first rule just says um uh x you know

x is of the correct form if it's equal to zero right because then that's equal that's uh of this form with hashing zero times uh and then the second rule inductive rule just says okay assuming that we have some x exprief of this form then x is of the correct form if uh x is equal to the hash of x brief okay does this more or less make sense to people does that scan yeah is it confusing maybe maybe i really like it sorry go ahead i really like it um i'm gonna try and um make our implementation of hello tuesday the

same thing oh cool awesome yeah yeah i think it's great and then you know what happens is you get two provers corresponding to each of the two rules so the first prover you know the base prover that will let you prove according to this rule this first rule and the second prover inductive approver will let you prove uh according to this rule and for each one you sort of declare like okay what was like how many previous instances of other proofs do i depend on um and it's really cool like it lets you compose like across different proof systems with different verification keys and anyway whatever um cool so right so uh let me just say a little bit like the

underlying kind of formalism or whatever of this library there's this formalism of kind of an inductive rule which uh an inductive rule um it says how one can turn previously proven statements into new new new statements um for example these two rules so you sort of declare what are the previous statements that i depend on here i don't depend on any previous statements um and how do i get from the previously proven statements to the new one it's this this description um then you know same here i depend on one previously proven statement of type you know myself and uh this explains how to uh how to do that and i i think this is a nice you know like this is kind of like i guess the same thing as what people call

pcd but um i i guess i don't know uh well i guess all i can say about this is it lends itself to easily writing programs described in this way um the the presentation in the pct paper is not that easy to follow yeah yeah um and uh this kind of language you know being able to talk about like sets of inductive rules as defining proof system it you kind of need it to talk about performance because for example like um the complexity uh of the verifier for a recursive snark system whatever is the maximum of the complexity of the inductive rules defining it so

you need to be able to say things like that um and and this is like what when i talked about before like one step of the recursion it's like one application of one of these inductive rules um so we used to use marlin uh instead of you know some kind of plonk system as our underlying proof system and i just wanted to share for the benefit of other some lessons on uh uh you know what was good about marlon what's good about plonk um marlin is i think much friendlier to compilation from rank or from r1cs and and the reason for that is um in marlin the the cost for the prover is the maximum over like your three matrices your a b and c of the number of non-zero coefficients

in that matrix okay people know what i'm talking about i know purchases here at least so at least protrusions i'm talking about but um this is really nice because it lets you sort of when you have a constraint and you're reducing from a rank one constraint you can choose where am i going to put the non-zero coefficients am i going to put them in a am i going to put them in b or am i going to put them in c and you can do that to make them as balanced as possible do people see what i mean because you're taking a max like you want you want it to be perfectly balanced do people see what i mean yes yeah so uh you know for example like let's say you have a constraint that's just like x equals y okay where x and y are some linear

combinations there's so many ways that you can reduce this to uh like a you know coefficients in the in the in the marlon matrices you can do x times one equals y you can do one times x equals y you can do y times one equals x you do x minus y x minus y times y equals zero and each of these lets you put the nonzero coefficients in different matrices so like this one lets you put in a and c this one lets you put in b and c this one lets you put an a and b so um you know in practice our circuits were like basically perfectly balanced um you know the discrepancy between uh the three matrices was like in the low hundreds maybe i don't even remember it was very small so uh that was a nice thing uh but you know planck marlin is is okay

but plonk really has much higher optimization ceiling uh with custom constraints and there's no reason why you couldn't use custom constraints um with marlin but it's a bit awkward in any way what you're really paying for is the some check thing and or the lint check whatever and and um you know if if you're not really using that then it's not really that much of a point um uh yeah and the other thing is that there's there's fewer evaluation points and i know there's some variant of marlin that lets you eliminate one of the evaluation points but still um which that leads to improved efficiency for the verifier and also uh better proof size um cool so like some future directions uh here um one thing that i'm really

curious about is combining these with like air starks i i this is what most people just call starks but like the proof system that we just talked about is also a stark so i called air um this is like starkware starkware tm starks um uh other kinds of custom constraints as i mentioned there's like a few operations that we have yet to custom constraintify like uh bit packing um i i'm also still kind of curious about brute force recursion um like uh with flick up or whatever so you don't have to use the cycles thing because as you can see like half half of the verifier is like dealing with the public input from the last one so if you don't have to deal with that like that would be cool

um and then like on the kind of library side or software engineering side um uh at some point there will be a wazer improver so you can just run it super easily in your browser and also like a javascript interface for this whole recursion library um right now it's it's in a camel and i showed it in reason syntax so it kind of looks like javascript but the difference between kind of looks like kind of javascript and javascript i think is like a step function so for most people so um yeah let me just talk about like a little bit about snaps um which is our like uh kind of facility for computational uh mina um uh yeah so what is you know what's the idea here okay so

like just broadly probably everyone's already on this page but i made these cartoons so i'll just use them so like let's say you're a computer user um you're using your computer it's cool uh and it's it's great because you're using uh like open source software so you're really happy like you can look at your computer you can look at the program your computer is running you know it's not doing anything nefarious and you know you know it's just doing some pointer stuff or whatever um so that's that's great but the you know this is kind of uh not reality because what is the reality the reality is that like your your computer is just kind of a thin client that really just sends uh your data off to some demons who then you know i mean you have really no idea what they're doing with it you

don't know what computations they're running um you can't look at them you can look at the source code blah blah so uh that kind of sucks but what's cool about snarks is they let you kind of force these demons to uh become on a human human scale and uh you you know you can have kind of the same uh or a sliding scale of the same visibility into the kinds of computations they're performing uh locally with you know um so uh that's kind of the like at a high level like on a societal level i guess like why are snark powered verifiable computing privacy applications useful and concretely like a snap in mino what

does it have it has uh like a state so this is some small number of field elements and some kind of transition function or really transition relation which comes from a snark circuit uh saying how is that state allowed to be updated and then some other stuff which kind of controls uh you know which lets you deal with the kind of asynchrony of this model um that i didn't make any slides on but i can talk about it um you know there's lots of cool applications you can think about um like flexible private elections and in in many settings um having sort of private computation uh happening kind of quote unquote on chain or at least being verified on

chain um and having and i think another cool one that i'm excited for someone to build at some point is uh like partial information peer-to-peer games where um you know you use snarks to sort of like as you know like moves in the game kind of be revealing partial correct information to the other player um and it's the most important thing for all these things is having no setup um or at least having universal setup i suppose um because if if you don't like come on i mean you're not going to run a ceremony for every smart contract if it doesn't make sense um i think that's all i have slide wise yeah but you know we can chat or whatever if you want to cool thank you [Laughter]

hi so yeah are there any more questions or thoughts you you went over the um comparison of the marlin based on the plonk base quite quickly um didn't quite have time to oh yeah you want to chat about it oh this slide yeah so um yeah i i mean it it's clear that you have to do at least with the current state of the art you have to do more work designing your circuit for planck

um or at least you because to get the full benefit of it you really need to use custom gates so yeah i guess there's that trade-off um i how um so do you have numbers on how much uh the uh verification circuit costs um for the marlin based one on the plunk based form so uh i only really remember for uh things that have two verifiers inside of them um that yeah that's a typical case yeah uh and you know just uh

for the benefit of everyone else uh there is something that's kind of quadra that you have to do that's sort of quadratic in the number of verifiers that you stick inside of uh your circuit but um i think i think the i so with marlin i think the domain was like for uh the number of non-zero coefficients was something like 2 to the i think it was like 2 to the 19. um and with uh the plunk one right now it's just above two to the 17 and like we'll probably push it down to the 17.

okay yeah i think that that corresponds quite well with figures for second size that i've seen before comparing mum and plank yeah yeah that's not a surprise to me isaac was that with um sort of the new version which has like only two some checks and um uh with the sort of roll call optimization as well uh it was with the roll call optimization not with the still with the three the three some check rounds okay all right yeah this isn't there's been like a few optimizations also to the basically how you handle the opening so

that you're actually opening uh you transmit fewer evaluation points and you do fewer field operations that might also reduce the sort of uh verification cost right because uh so waking one of these students has been in i mean and nick and other folks have been implementing a marlin verifier like you know standard pcd style um bctv style and they get something close to i think 300k constraints um using the kcg10 style polynomial movement yeah yeah even i mean even with the yeah even with the inner product

argument one it wasn't that much it was maybe around 300k also so maybe i maybe i should to try and share my optimizations with you because i don't know because you could probably get it to be lower um yeah so it's yes then that didn't do any accumulation so i think once you account for accumulation you come down um i mean i don't want to be too negative on marlin i definitely think that's a line of investigation that that needs taking further you know i think i think i said a lot of interesting avenues there flambook i think maldon i think that generally you can sort of combine these um i polynomial algebraic iop kind of

systems to just have you know you can come combine errors with marlin or plonk custom constraints with like the marlin side where you can just share the witness polynomial across the systems really yeah i haven't thought about it enough detail but i'm sure it's something it's too easy one thing i'll say about um uh marlon plonk i had this idea and i don't know where i got it from that like that plonk would just be faster like with even without custom constraints than marlin and that was definitely not the case um because the production from r1cs is so uh nice with marlin um

yeah basically in malin you don't pay for like some of like the total number of addition gates you pay for like sort of the max of addition gates across the three matrices whereas in planck you pay for like the sum of the edition gates yeah and in practice because you can balance things so well it's basically number of addition gates divided by three yeah i mean i i think of it as being a trade-off between engineering effort and performance so so with planck you need to put in more engineering but you get a smaller circuit out but we'll probably have compilers that

can do that for us eventually so you mentioned that there are two very cars usually what are the two variables say that again so you mentioned that you usually verify to like to i guess proofs universe well what what are the two oh yeah so um in oh yeah okay in in uh meena where uh you know we we basically do proof composition in a tree so uh you you're it's like a there's a binary tree of proofs and you're composing uh up that tree does that make sense to kind of history so yeah there are no no i'm

curious about your comment because you said it's commonly what you do oh oh sorry that will probably be what we end up doing eventually anyway um i i was interested when he said that the um there was a quadratic dependence on the number of verifiers oh yeah yeah what is that i'm trying to remember uh so let me remember uh okay i i okay i'm not gonna remember completely

but basically um each proof um has to expose the you know restrict the field restriction of of the two proofs that are inside of it right um you know what i'm saying um yeah and uh and uh i don't remember i could look at the code but because there's a part in the code where there's like a vector of vectors of something you know and the length of the vector is equal to the maximum number of verifiers inside of a circuit i

i i can find it easily if i look at the code but uh i it's hard to make sure my brass on my head the the reason why it didn't occur with my intuition is that if you think about something uh like the uh bc tv 14 um recursion um in that case you're needing to do um some pairings but you can whenever you um you just need a computer pairing product um you can just do a single um final exponentiation so it actually ends up um more efficient to do

uh multiple um say grout 16 verifications um right yeah let me i can take a look and get back to you okay cool um actually there if you don't mind me asking i was curious to hear are you all um so like for public input handling we just compute the polynomial commitment to the uh we basically just do like a multi-scale or multiplication um to compute the polynomial commitment to like you know the low degree extension the kind of low degree extension of the input do you know what i'm saying but you all have some yes peterson commitment or something which is an alternative to this um i don't think we've exactly decided what

the most efficient way to do it is okay yeah okay cool it's it's not obvious yeah yeah yeah you can see from the playing graph it really it's like a really crappy part of this let's see let's go back to the plane graph because um lots of interesting things there uh do just um tell us what what the various pieces are again so this is running like the field part of like finalizing the the previous guy's proof yep um doing the arithmetic this uh what is i don't i don't know what this is a sequence of i think endo scalar multipliers i i'm not i don't remember what it is here this is

okay um and then like this bit from like 15 to 20. i don't remember what that is um this is well there's there's one parent it looks like so oh yeah that must be challenge process uh i think that shows up later so i'm i'm yeah whatever we yeah we can look maybe it could but um this is uh i believe this is computing the commitment to the public input polynomial okay um that that's expensive yeah super expensive yeah so you you can save because like

a little bit because like a lot of the a lot of the elements are just challenges so like you know that obviously uh is less costly um but yeah super expensive um this i think is just running the sponge so that's actually really cheap so this is just like running yeah i either rescue or precise and they're really really cheap yeah um and then this is the inner product argument so um oh actually sorry this is in plank you compute this commitment to like this i think it's called f this f polynomial um and there like the complexity depends

on how many con how many kinds of custom constraints you have but that's what this is um so yeah i guess if you have fewer kinds of custom constraints that's better um and yeah this is the actual running of the inner product argument um verifier so you have a bunch of i i have to remember what all what all these are i'm a little confused on what this block in the beginning is but these this is i guess this is running the sponge um for the inner product argument um yeah it looks like there's a lot of overhead each time you do that

yeah maybe i think that's from like unpacking i think that's where i'm unpacking bits and using like only the low bits for the challenges yeah maybe paying more attention to optimizing that yeah um so yeah like that'll probably go away when we implement the bit packing constraints um and then this is the these are the endoscalar multiplications and then there's a few scalar multipliers that you have to do in that verifier as well right so i see okay yeah i mean it's it's not there's not obviously one huge chunk that um well i mean i guess the processing

deferred values is the biggest chunk yeah that looks as though it might and isaac we're still experimenting with marlin so we're we've got you know the idea is a gross system one on one hand and marvin on the other one so we haven't seen we haven't looked into blanc yet but uh can you tell me something about the the the form of this cast on gates so degree variables you know oh um so right now uh our gates i this is like this is definitely not optimal at all and i think there's probably like one or two factors of two like a factor of two to

four to be picked up by optimizing um how we set this up we have like three columns uh and uh each uh each custom constraint i think the max degree of one of our custom constraints is like five or six or something which kind of sucks because then you like pay for this big fft but actually that's not the dominating part of the approver so you know whatever um yeah so like given that we're already on one of the custom constraints uh going up to degree five or six i forget what it is i'm sure there's like other stuff that we could be doing the other ones um to to take advantage of that because

you pay for like the max degree um and how many sorry how many different uh so we have constraints for um what do we have there's uh scale multiplication there's poseidon round there's the endoscaling um the scale multiplication i think that has two constraints associated to it then two or three i forgot at the end of scaling i think has two or three um the uh poseidon there's just one um then i mean bit packing will just be one uh yeah

thank you and overall i mean what has been the improvement that you've seen moving from marlin although you were with the old marlin maybe but yeah so right now right now it's been a factor of like between two and four um i think it will be i think you know we're we're very close to the next power of two so then it will be somewhere between four and eight um so pretty good it's very huge yeah cheers thanks i i think sean said that there were two sweet spots in the max degree max degree 5 and max degree 9. okay that's interesting what is that based on i i don't remember okay

how fast does the verify like it says 85 milliseconds um how fast does it need to be or what's the oh so this is actually uh we we we we repurposed the uh chrome debugger for profiling uh train systems so 85 milliseconds means 85 000 constraints how fast does it need to be i guess that depends on your application um uh yeah the yeah can you i just haven't played with this tour it looked like a beautiful tool and i just i saw 85 milliseconds i was like how fast does it need to be so

i think i just need to play with it oh yeah yeah um i think it leads to my next question like how do we get started like how do i start playing with rules and do you have like an example that we can play with or is it school oh that's a great question i think uh let's see what's your level of comfort with o'camel that would be the first question uh play with something uh for a hackathon but that's kind of the extent of it who was asking also i can't see just so i know adrian okay yeah um i think the the best thing to do would be to wait until there's javascript uh interface which shouldn't be too long um and uh

yeah should be very easy to use before then i mean the code is all open source so like if if you're really gung-ho about it please you know send me a message and i'm i can i can try and help you out cool so i think if i think now we've done a good good session on pickles and uh i want to say thank you isaac for putting this together and sharing this project and your awesome slides there's been a lot of chatter all the whole time about the drawings and they're really good all right yeah thanks thanks anna for for inviting me this one cool and i guess if there are any links or anything

that viewers might want to check out just send them my way and i'll put them in the show notes okay uh as well cool thanks everybody thank you bye everyone