zkSummit: Axioms for Zero-Knowledge Proof Pricing- Tarun Chitra (Gauntlet), Georgios Konstantopoulos
15 May 2020 · 45:59
Tarun Chitra of Gauntlet and Georgios Konstantopoulos present a zkSummit talk on axioms for pricing zero knowledge proof generation. They work through a framework for modeling the cost of proving, connecting choices in proof system design to the economics that determine what users and protocols should pay for zero knowledge proofs.
Speakers
Topics
Transcript
hello everybody I realize I just possibly pulled you out of Oh legs talk mid-sentence so if you want to finish up with him feel free to go back for a moment but now I want to present our next speakers Tarun Georgio's we're gonna be talking about pricing ZK Peas with their talked economic equal equilibria in zero knowledge proof generation all right I'll pass it to you cool is the slides are the slides on full screen cool right great yeah they are now they're now okay so thank you everybody for coming to the stop so for the past
few years we have seen a kind of Cambrian explosion in the world of sexing trance pint and universal knowledge proof systems and many of these systems were created to help create private scalable blockchain based 100 platforms and in this context we have a group of participants that create proofs in order to operate a decentralized network and they are certified to do so via some reward and you can think of it as similar to Bitcoin where some miners are incentivized to compete to produce the next set of admissible transaction and it is apparent that incentive choices are crucial to ensure that proofs
continue to be produced and the network stays up so in this talk we extend the axiomatic framework from a recent paper to construct what we call like reward allocation rules for zero knowledge proof generation and we will then use this action to produce a set of an expected and desired properties with your protocol will possess so let's start with some examples of the architectures that we have seen today so let's take coda for example so in coda you have the block producer which is kind of similar to a minor it is chosen with some way which we do not investigate and they choose some transactions from their mental
and again how they choose their transaction rates off independent interest and then they publish these transactions and wait for snark bids on them and this is because a transaction in coda is only valid if it's included in the chain alongside do this not which proves its validity and you have this parties called smart kids that are watching for transactions which then they generate groups over its transaction and they post a snark along for instance action with their of it and then the block road user chooses like looks at the order book and chooses the probably presumably the cheapest transaction from the door that book and that turns I can get included included
and the whole idea here is that if there is free entry to the snark market there will always be at least one proof per transaction so the system will be Bruce censorship resistant at least from the side of the snackage and just to be clear here economic model has said that the block producers and approvals will be separated but will have coupled incentives but we cannot really be sure that this will be the case in a permissionless world it is likely that maybe some block producers will also be approvers and so we need to evaluate fairness and competitiveness under these assumptions and just as a note that I have added an asterisk here on the free entry because in coders case the snark
for one transaction can be cheap so free entry you could say that if you have enough participants yes free entry is easy but what if the snark is costly to produce then you'd better have some issues with proof free entry due to the proof size so you need to start thinking about how you can start distributing large groups so this kind of gets us to the next architecture which we have seen which is leveraging a paper called proof of necessary work by catties and bono which was released earlier this year which basically intertwines Nakamoto consensus with snarks showing my motor home sensors you have the head there and you grind the nonce over it so what happens here is that instead of grinding over a block in owns over a
block header you input you use this as in you use the norms as an input to the snark and then you choose you generally thus not proof and you check that the snide proofs cache is less than some difficult but this not proof can be huge so we can look at some other later tool called Disick which which basically is a framework for doing distributed proof generation and a set up for block 16 in Apache snark and if you put these two together they give you something that start to look like snack mining pools and there's no free lunch though because when they when we start distributing this there is some loss in
efficiency that occurs from making the marketplace more fair so like if you look at this like from like a more in-depth perspective you had a man pool where mining pool gets the block template and then using the technique from the proof of necessary work they choose the gnomes and using the technique from this they split the proof in chunks they will distribute the chance to the profits the workers the workers will perform the computation and then they will submit the work back to the mining pool remaining who then will assemble the proof like each chunk into one big proof they will check if they approve cash is less than T and submit it to the chain and then the chain
should give you some subsidy which could be their block reward and some feeds from all these transactions and what happens is that the chain the mining pool will take some tax and then the rest will be distributed as a block reward and but the question here is how will they do that so we start to get some intuition that there is some room for investigation here so like our whole question around this is why do people do this so why do people join a snack eat place like in coda or why would people mine in a snack hole and the answer obviously here is that there are some there may be some attractive the subsidies on the launch or there might
be some protocol phase which dating opportunity cost and everything else in mind they will be more attractive but again like how do we choose this like what's the intuition so the goal of this work is that we take into account that we have multiple agents who have multiple roles which may overlap so maybe I'm I spent some of my resources on being a blogger do share some of my resources on being approver and would lead a simple like formalism to look at the design space and see how the revenue should be split and then economics the way of doing this is to specify actions which enforce constraints on agent preferences and these rules and actions they will provide us with the
information that we're looking for and the most important product is that we want to encourage is the proof generation to be competitive and fair and the natural then the natural question becomes what is fairness so and our focus on this will be in the incentives for proof miners the profits at the timescale of generating a single proof so in Coda's case generating a single proof is for one transaction in the mining pool case it's one block so the design question becomes how do we allocate rewards rewards for our proof system and for our circuit for the provision relation to be fair so the desiderata if you will in this case the design properties are we have a
enumerated like the following properties some are taken from the paper that we base our work on some are specific let's say for this work so firstly we don't want dependence on identity so if me and I don't commit the same resource the system should have more or less the expected the reward the system should be simply resistant in the sense that I should not be able to split myself in multiple entities and get a higher the word from not splitting and it's opposite they should do it the system should be collusion proof so I should not be able to combine pool resources from multiple people to gain more than our collective fair share there should be no gain to amortization so formally
doing this is a bit tricky so intuitively you can think of this as that if I've made five proofs in a row the six proof should not take me less time than computing just one proof so I do not have some sort of caching that I can do to get him disproportionate games there should be something that we will call with Miss dependence so if I'm a proof and I'm given a circuit and any put I should be able to get the same fee for an I should not be able to get the same fee for an input that is easier to compute a proof on versus a harder input and finally we want to minimize prove a extractable value such because clearly
the proving marketplaces will have the same problems as a front running or censorship in the normal minor markets so now I will pass it on to the room to move on with our formalization cool thanks yes so we're basically going to kind of go through some of the mechanism design and game theory the main sort of tool that's used in the space is kind of an allocation function now an allocation function is really a map from a resource space usually some that risible measurable space to sort of a space of rewards which is usually in
this case positive reals cause important I guess and so the idea here is that you kind of bake in all the properties you want into your allocation function and then you try to say okay does this function represent all of the economic properties that I'm looking for and the intuition is that at some high level alpha includes all of the macroeconomic that's written either that before for instance it should be encoding this notion of fairness or the notion of civil resistance and so you know historically you might say okay well you just chose the random function why should I believe that that function is the correct function for ensuring X Y or Z well if we look at certain history you
know the famous sort of on-demand Morgenstern theorem and I can seven shows that for every quasi-convex assumption of the swarm you automatically define the set of constraints on economic preferences users of the system can have and what that means is the duality between the atoms and or preferences and utilities now what do I mean by axioms and their preferences well a simple axiom for instance is say I have a society and all of them prefer good a to good B then in the total societal preference sort of the average the the ranked vote of every one a has to be preferred to be so that might be one of the axiom to choose so
that's sort of a constraint that made but that constraint translates to a constraint on the function that is allocated and you know in crypto tell me this paper by Chen Hrothgar and and publisher basically tried to amplify this and proof of proved working first to kind of show that for a certain definition of fairness that sort of a unique allocation function now protocol designers specify this leave to extraordinarily different outcomes so in bitcoin of course we have proportional allocation based on hash power of course you don't know the total hash bar so you don't really know the proportion with perfect certainty but there's also it also has a balanced budget blocker words
go out to everyone the cash on the other hand doesn't have a balanced budget it has a network tax by the developer fee and then the theorem 2.0 for instance is proof of stake with the square root allocation and the square allocation actually quite changes the kind of distribution in of itself quite a bit so what is our resource base well if we step back and look at proof of work at stake both the product in pieces so they're all abilities and things of things that sum to one but so the difference is in proof of work you don't actually know the denominator in the sense that you don't totally an individual doesn't know the total ass power system and improves sake everyone
has to know the total money supply um what about zero knowledge proof I'm not sure what my video disappeared but not as well journalists have a you know a lot of different sort of resources that end up being used that have very different hardware properties and or algorithmic properties in terms of like how well you can paralyze the sort of communication lower bounds or sort of properties of a certain group like random walks can't mix fast enough etc but at a high level we have things like Fourier transforms which you as in fri days systems and a
lot of systems that basically do any type of error correction that isn't isn't done by polynomial commitment you have to do an FFT or over in a building group okay this could be big yeah yeah a lot of way to make that the computational issues with that quite large you have to do multi exponentiations which is obviously time consuming on purpose and in something say like the prior talk on polynomial commitments without MIT is you have way more polynomial evaluation so this n log n Jacobi polynomial and the ground polynomial that summations are more expensive and then finally you have these circuit specific computations for
calculating witnesses these costs are extremely non-uniform so the resource base needs to account for the heterogeneous nature of kind of the resources use so what we did is we try to make the simplest non-trivial model of this so assume there are K computation types so computation type mode might be Fourier transforms something whose lower bound on complexity is n log n minus communication complexity of course and then you know computational type 2 might be multi exponentiation etc we define this vector lambda which is the relative average cost competition type I relative to computational type one then we define
a vector that each agent has that is the amount of out resources allocated to each type of compute and then finally we have a sort of lower bound you in order to do a Fourier transform you need at least 100 units of multi exponentiation power this way we sort of choose one computational unit as a new Moreira and we measure everything relative and the simple example how this looks say we have three computational resources say we have two of them take double the compute of the first then we can measure the total units of c1 compute by taking their dot product so
what does this look like formally well the first completely basically again have this kind of graded structure where we're graded by the number of agents but there is another thing in the partition product the first component the first component really corresponds to this lambda vector which is sort of the cost relative cost vector and then the other component is sort of you know your resource distribution allocation for each agent so you know the naive thing to say Mikey hey doesn't the proportion work since that's a personal rule is you know should be kind of kind of the the
only fair rule but the real question is in zero knowledge proof plan the question is how much computes it approver I actually compute so in George's earlier slide you saw the the allocation of the behaved pool and the interesting thing is if we try to write the naive version proportional rule what it looks like here is hey how many units of compute one compute this agent I have relative to all the other agents the problem is it doesn't respect this constraint which is that there's sort of a minimum amount of compute you need to to get things to work so we're going to look at that in pictures so on the Left we have the rough garden paper which
basically is what sort of the three types of principal agents look like yeah we have the risk-neutral which is quasi linear utility again the Mondrian von Neumann Morgenstern theorem gives you uniformization purse for any strictly convex strictly concave or win your class and so the risk-neutral ones are defined to be the quasi linear utility and you can basically see that as a function of resource and risk seeking users you know has this your contacts function the risk-averse has this concave function risk-neutral linear the difference is ek proof gender shown the right you see
that the utilities aq0 until we hit our constraint line and that constraint line is really important because unlike in proof of work where for proof of stake where if I have a very small amount of state I'd still they're still technically a nonzero allocation to me in infinite time in zero knowledge proof generation that just isn't true to because of how all these components interact and because of cutting empirical evidence that so we have from running these applications um so the idea is that this little little constraint causes some differences in how collusion works so let's say we have these three malicious using want food
and if you notice on the left and the right one of them it is kind of below this threshold now the normal version of collusion basically you'll find that if you're risk neutral risk seeking your collision resistant but if you're risk averse you're not which is kind of what you expect in because if I'm risk-averse that means I optimize I want lower variance if I won't lower variance that means I will pool together with someone else because my I'd lower the variance and expecting reward on sampling by doing that since the sampling is proportional to my stake times one minus my state times concert okay the the other type of solution at
doesn't work because if I'm an agent who's below the constraint so I have had enough resources to meet minimum I joined persons with people such that we get over the minimum I actually do increase my reward but that's not necessarily bad because that actually means that we've been able to take participants who were unable to participate at a certain time and by polluting they actually were able to generate new proofs so there is a sense in which you want collusion up through this constraint and that's the type of stuff you want to define correctly so now let's go to the active first action known get no game to amortization this basically says if you have a positive expecting reward then you need to
necessarily have more compute than the l1 norm of the minimum and why is this this sort of force of the linearity lower bound because this means that every prefer every proof I generate I have to commit at least the l1 norm of the lower bound / / proof I have some type of math another camera is Asian and I'm asked I can position the second so this is this back for strength because the constraint is somewhat circuit dependent so what we do is we define a notion of collusion proof that is street dependent and the way that the circuit dependent C works is take the set of users and s we
basically in this picture we have three types use we actually the adversarial ones we have the honest ones who are the runners and then we have the people who don't have enough compute resources we're in Orange and basically we we basically redefine the collusion proof constraint based on a the circuit through the circuit there's a circuit dependent lower bound and then beef by allowing anyone who's above the circuit dependable are bound to combine arbitrarily and so what this says is hey all of the addresses even if they combine and become you only see 13 public keys instead of 16 the rewards are still the rewards are never greater than if the other two constraints
another sort of natural constraint and this is this comes from the rough ground paper is budget balance budget balance basically corresponds who do I spend all of the Block rewards on subsidies or not do the taxes he is that essential people basically probably every proof of state hook in to some extent that has slashing is a non budget bounce and also burning feeds can also just be that think the frameworks don't dust for done dynamic fees so you usually you consider feels good now the last two things are civil resistance is entry which are injury so symmetry basically says take any element
of symmetric group on n letters permute the resources and then can compare that to muting the hoods and they should be the same which basically says if I contribute a certain amount of resources and Georgio's contributes a certain amount resources and they're the same amount then our expected reward should be innocent this hormone system if I can't split up my coins and get more so what did sort of what kind of properties to improve first property is sort of direct analog of the roughgarden property which is you know proportional rule has these is sort of the unique rule that satisfies symmetry similar is the sense strong
budget balanced inclusion business now for satisfying something that that is unique to zero knowledge firstly because there's no Gantt amortization the unique rule is kind of this convex optimized version where we constrain so one is the indicator from eight weeks but indicator function that restricts to this half space which is constrained by the circuit lower bounds of circuit defendants again so we have a circuit dependent everything wrong thankfully these are all convex problems because we're constraining into an optimization in a convex optimization problem over a convex set so we can construct your standard in the ground schools and the
job transform type of things and you can actually show that you have a circuit dependent utility function so you can review this entire constraint as I have agents who are getting proportionally allocated fees but they their utility function is constrained to a convex set and the convex set is basically defined by the half planes defined by all the circuits and this generalizes to non uniform constraint so you can actually combine multiple circuit constraints and get a polytope sort of like the thing you see above and the cool part is we wanted to compute Nash equilibria in this setting thanks to the fact that it's a pump structure polytope you can use some standard algorithm like the lengthy house a auger lempke house an algorithm which basically walks along the edge of
the polytope akin to the same kind of simplex algorithm and tells you kind of where the Nash equilibrium for a particular agent is so now George is going to present a couple last few things so ok so using the thing so far we will try to extend them in some ways to get some extra properties that we might want from our protocol so firstly there was a question in the in crowd cast which directly relates to this which we call witness dependence again so basically this equation says that very word I get for computing over one
witness - the reward that I get for computing on another witness must scale more or less proportionally to how the cost the for computing on each witness respectively it changes and this kind of reminds us of like at least reminded me of constant time cryptography and we saw that such an attack on a snark and a timing based attack will seen on a recent paper on the timing based attacks on Sica's snark well basically you had the mooncakes pronunciation and if there was a zero the feds on doing the commutation could skip some computation
so in the zika's attack if you're skipping a computation you have a timing attack so in this case margin the multi explanation of say like a hundred elements and you distribute it so the first ten elements go to some proof where and so on and so forth but what if a prove it gets an array let's say the Iranian spots and the approver gets a man segment of the computation which is all zeroes so if it's all zeroes the approver may try to say that a I did my computation I calculated the chance that I was assigned to correctly give me my word but your protocol should not reward him because basically anytime you're skipping any computation based on
whatever you should be not rewarding are my slides didn't yeah thank you okay so if you can skip a computation you should not be rewarded for this moral assess you get rewarded paid computation step which depends on the witness not only a sacred level and the second kind of extension that we want to propose is the minimizing the approver extractable value so there are some kinds of attacks which miners can do inclusive world
systems and it turns out that these attacks can kind of carry over to this sort of proving ground proving mining market so basically the one is censorship with where basically the pruvit sees something that is available for proving and they just don't compute the proof on it which maybe they don't want to make a proof on it because it was some CDP maybe that was a transaction which would bite their CDP below some amount and they would lose money or maybe they just want to prevent you from transacting this is solvable by just having a large number of prove it so if there is a lot of people available for generating proofs you can you avoid censorship and also by distributing the
computation if you have a large circle but in the case of reward during the probate basically what they do if you're receiving a blow is that you have a bunch of transactions which you receive in a certain order and if these transactions you perhaps need benefit by reordering these transactions so currently our allocation rule does not take into account for doing so we must kind of like fix this and the solution that we propose for this is that you should basically just penalize recording by adding an extra term in the reward function and we explain this extra term as a distance metric so basically this says that your reward
will decrease the more the permutation of the transactions that you are computing they proof over differed from the original transaction order that you save so if the block sequencer the block producer gave you transactions 0 to 9 in an ordered 0 to 9 and you suddenly put transaction 9 in the fetch slot and the first load on the last slot you should lose some money and the practical instantiation of this would be that the moment that you try to reorder anything just reduce the reward to 0 and any penalties taken from this they get they get held by the protocol and you can choose how you will allocate them it's
obsolete interest so to wrap up this presentation we have some final takeaways so it seems for you do that I actually need to go into the next session in order to get it started so you are welcome to stay in this session as long as you need to I'm just gonna let you know that and I'll see you soon I'm gonna be pulling some of the audience with me though so if anyone wants to kind of make sure that they're still following this one just make sure that you're in this particular session ok thanks guys cool so yeah so the final takeaways are that it seems to be that we expect that in
the marketplaces and distributed proving systems for knowledge groups we'll go to the moon and it's hard to figure out what is the unit of course in their knowledge groups because there is the resource space is much more complex and so we want to have fair entry ideally to have nice and symptoms and the room do you want to finish this yeah so you know we kind of were inspired by this with this recent work to kind of give economic understanding via axioms to to some of the rules that people are using in protocols I kind of reverse engineers
the allocation rules and makes them kind of much more salient and in a lot of ways by doing that you can start thinking about fairness directly such as how do you prevent clinical ization how do you you know kind of prevent interference with consensus and you know fundamentally the allocation functions must match tax and you want and if you want to have a rigorous protocol you need to kind of construct both of those correctly and so the last thing as you're just mentioned is there's kind of an advantage to having a weak weak budget balance protocol in a lot of ways there it's just it just makes makes things a little more flexible for instance having an insurance fund which
comes is paid for by the minimizer reject all value fees that are collected or potentially I guess what people seem to like to call a public goods but it doesn't necessarily matter what it gets spent on I'd say the insurance fund is probably the most salient version but I think there's a lot of there's a lot of room in that design space to have the allocation allocating efficiency of these systems grow quite good thank you and you very much thank you yeah anyone that is there any reason you know
analyze it yeah do you want to take down there yeah sure so yeah that's what I wrote there in the comments but let me just say so by short cut off in the talk what I meant that the moment that there is some reordering in the transactions you can just cut the reward to zero another approach to this would be to somehow force the ordering of the transactions on the snark level so the way you could do that would be that there would be that they prove it no sir if they block reducer posts let's say to the chain the cache of the transactions so sequences the transaction serialize them generate
the hash posted and then the snark would need to prove or you'd add some sort of consensus rule to the snark that the the cache of the transactions given his inputs to the snack must match hash the cache which was published earlier by the province so by the block code users so you kind of tie the two octaves together in that way but not increases yours not complexity complexity and and if we added that as a rule to the these properties maybe it could be too restrictive so we just choose to say you know just analyze it yeah and the
distance used there's not too many constraints on it it just needs to be unimodal and monotonically decreasing from the the true ordering it can't be like multimodal we're like if it's if it's sitting with I mean isometric but then because then you get a lot of like weird problems so there are some constraints on that D but just just pointing out oh okay I think all right thanks okay we are in what someone yeah yeah