Reinventing PLONKish Circuit Design

Transcript

yes hi everyone I'm Alexi from Neil I'll be talking about circuits so circuits are an important part of ZK systems if you want to prove that a computation is correct you have to represent it by a circuit every computation can indeed be represented by a circuit but no one said it would be easy so it's more like you can doesn't mean you should and implementing a ZK program requires special skills like yeah sorry thank you so implementing a ZK program requires

special skills like renting over how circuits are complicated then hating a little bit the non-native arithmetic and eventually being frustrated about your circuit being under constrained and you need all that but nobody talks about it people actually prefer to talk about proof systems implementing proof systems creating new proof systems Etc while the circuits are neglected they are like a stepchild or maybe he who must not be named so question is why don't people enjoy working with circuits well there are some people who actually do enjoy but they don't tend to speak up there

are probably multiple reasons I guess the foremost reason is that circuits are very complicated uh if you're working on your own circuit and you make a pause getting back to your own circuit is really really difficult understanding someone else's circuit is like nearly Mission Impossible at some point at Neil we had designated people responsible for specific circuits which is obviously not a viable solution and getting from traditional programming to Circuit design is not easy at all traditional techniques do not work so it's like hey come to the dark side we have no Cycles no ifs no

bitwise operations no nothing we might have zero knowledge eventually and debugging gets a whole new dimension because now you have to worry about getting correct output if you had incorrect input that actually might be sign of a security issue so can we fix all those problems I actually don't know but I think that we should stop ranting about circuits and just embrace them as they are and try to understand them better obviously we don't start from scratch there is a number of systems for spe circuit specification and these systems allow different approaches to

Circuit specification on one end of the spectrum you have the sort of Gadget or chip approach which actually tries to breach the gap between circuit design and sort of traditional programming techniques because it implies using predefined ready to use circuits combine them and solve your task this is very much like shell scripting you just combine something that is already made to achieve your goal and just like shell scripting well it is not very optimizable not too flexible and you actually rely on those who design the gadgets on the other end of the spectrum

you have hardcore circuit design where anytime you need a circuit you just design it from scratch this is very much like Assembly Language programming well it's a bit outdated but if you feel nostalgic you're welcome and at Neil at some point we were very much towards this end of spectrum room doing a lot of circuit design eventually ending up with a whole library of Home rot circuits and then we realized that it actually impeded our progress so we thought that we would like to move to something more designer friendly still the gadget approach seemed too limiting for us we wanted to have something more flexible

and optimizable and not worry too much about the back end something like a high level programming language but that would be really circuit oriented before I give you details of this transition I will actually have to explain what a circuit is so behold crash course on circuits circuits are called circuits because they originate from the combination circuit model it is a pretty simple thing you have inputs outputs they are connected by gates for the purpose of my talk gates are addition and multiplication they should be over a finite field but disregard that you can just treat inputs and outputs as numbers

and a circuit is represented by a directed graph like the picture you see on the slide so this one computes X1 + X2 * X5 the output is labeled X6 and I have put labels on the output of the addition gate which is X3 and the input of the multiplication gate which is X4 they are obviously the same thing but for illustrative purposes I put two different labels now this circuit can be represented as the table on the right hand side of the slide this representation is pretty easy you just put all Gates inputs and outputs into the table and then you write equations that relate the table cells to one another and this is equivalent to the

picture that is over there so when we are saying circuit we actually mean the table and equation equations we don't need mean the cute picture on the right hand side we don't need it and when ZK proofs work with circuits they work with tables and equations the equations are called constraints and the table is often called the trace table circuits are intended for proving relations the relation in our case would be that X1 + X2 * X5 is actually X6 and all these values X1 X2 X5 and X6 are the public input to the Circuit they would be included into the proof directly the

values X3 and X4 are sort of hidden they are not included into the proof but they are needed to construct this proof in our case here there is hardly any point in hiding X3 and X4 they are easily obtainable but that's not always the case so circuits are not circuits they are Trace tables and equations and they are intended for proving a certain relation now if we accept the fact that a circuit is actually a table and equations and we do not follow the cute picture with arrows and Gates we have a problem that assigning uh the hidden

values which are often called weakness values is no longer easy you can actually have a circuit with a simple system of constraints where finding witness values is a difficult task for instance suppose that you want to prove the system of equations that's over there down uh has a solution the circuit way to do it is to actually constrain a solution XY with the coefficients AB bcde F the coefficients are public input the solution is the hidden witness value now in in order to construct the proof you need to know these witness values

and if you somehow can construct the proof without knowing them that is a big security issue so to construct the proof you need a procedure for finding witness values in our case here you can actually write out explicit formulas for the witness values that is not always the case sometimes even with a simple constraint system finding the witness values is extremely difficult that is actually the whole point of having ZK proofs you delegate the burdensome task of computing witnesses to the prover and then you have a short way of checking that the prover did the job correctly that is verifying the proof so actually

besides Trace table and constraints we also must have something that assigns values to the Witnesses in the circuit and that is something that I call the assignment procedure this procedure is an integral part of the circuit you can't do without it and it is like the evil twin of constraints it might be much more hard but still they always go together and in some way they Define one another now before I actually uh yeah quick recap first so a circuit has a table which has cells they are either public input or Witnesses and

you can also have constant cells which are part of the circuit setup then there are things that are outside the trace table those are constraints and the assignment procedure since I'm talking about blanish circuits constraints can be pols like over the cells of the table the simplest constraint we can have in terms of polinomial is just one cell equals the other another cell that's called the copy constraint and we can have a special constraint where the value from a certain cell should appear in a predefined area of the trace table somewhere else and this area is called the lookup table and the constraint is

called the lookout constraint now all these things are an integral part of the circuit and if we want to implement some language for circuit specification all these should be supported before I get detailed details of our transition to a new circuit defining syntax there is one more thing to observe do we actually like the fact that constraints in a circuit can be just arbitrary polom well the honest answer is no not really because well circuits are intended for proving that a certain computation is correct but the easiest way we know to verify that a computation is correct is just to redo

the entire computation from scratch and then check that the result we get matches the result that is supposed to get and this process is described by the equations that are here so X is the input y are the intermediary values and Z is the result we get and that's how that is the easiest way of verifying a computation you take the input compute something use what you have computed to compute something else and eventually you get the result you can check against the supposed result this is the most natural way for doing a computation it is the way that programmers tend to think it is what gadgets actually do they break up everything into blocks

that have inputs and outputs it is like the way combination circuits work initially it is a designer's First Choice it is very easily verifiable and maintainable do we want to avoid this type of circuit no we actually want to promote them this is like what we would like to have but we cannot always guaranteed to have so another thing like there's more these are sort of instructions for computing values witness values for the trace table but you can also look at them as constraints that actually limit these

witness values so it goes as a combo you have have constraint assignment proced uh witness assignment procedure and constraint definitions in the same equations and that leads to the core observation we had behind our transition to a new syntax so initially in our circuit uh defining language that we used previously we had separate procedures for constraint generation and assignment generation but they always go together actually usually we would have circuits where one would be just a copy paste of the other that was a redundancy and obviously it wasn't helpful at all and in some cases like uh

not like the previous slide but in some others these procedures may be different but they are still interdependent and when you modify one you have to modify the other so our idea was that you actually need a unified procedure you may have blocks that are assignment specific specific and constraint specific but the part where specific values are placed into the table should be unified for them both and so this is what I call allocation in the unified procedure and we actually move to a unified procedure for every circuit this procedure is run at least twice once when you generate the constraints and

well every time you need to generate an assignment you also run this procedure feature uh in the best case scenario like the previous slide it is actually just one same procedure where you Define cells as pols of other cells and then you allocate them in a more General way you can have assignment specific stage and then allocate cells and then write constraints on the way like along with this important transition we try to get rid of technical details where possible so the allocation procedure is automated you don't have to worry about where data goes in the table cells unless you want

to and you don't have to worry about preparing specific data for the proof system it is done automatically and we Implement some optimizations along the way and finally well it's a bit of a minor detail but if you want to use pretty fine constant lookup tables you don't have to worry about the size of the table table it is adjusted automatically with all that we get our new language for specifying circuits we call it the BBF the core ideas and PR and Primitives for circuit design are listed in this slide so we have self adapting variables they either contain values that are going to get into the trace table or they contain cell addresses in the T Trace table depending

on the stage we have polinomial operations with these variables obviously and we can have stage specific blocks like some parts can be executed only at the assignment stage other at the constraint stage and the major instructions are allocate to well perform different actions depending on the stage but mainly like interact with the trace table constraint to create constraints and specific instruction copy constraint for copy constraints and obviously some interfaces for lookup tables we actually have a lot of other marvelous things but the margins of this presentation are too small to contain them um a little example of code with

all that so you get a feeling so type is the self adjusting type I've been talking about the x i and r variables have a type that depends on the execution stage at assignment time there are values and at constraint time there are expressions with table cells now there is a stage specific if block which is executed only at the assignment stage and this is where X and I get their values now this defines a circuit for verifying whether the variable X is zero or not so we actually put the input X into X and we Define I as the inverse of X or zero if it can be

inversed and since this this is executed only at the assignment stage uh when we arrive to allocation uh we either have the values or if we are at the constraint stage X and I are just variables they are undefined then comes the allocation and these values are placed into the table or the X and I get the addresses of the cells where the values would would be placed at the assignment stage then we have the variable R which is defined polom so this works both for constraint stage and assignment stage and then we allocate the variable R and at assignment stage it just places places

the according value into the trace table and at constraint stage it actually creates the constraint r = y - x i this is the first constraint we get in our circuit and it actually assures that whenever X is zero R is one but uh for other cases when X is non zero it actually can have other Solutions so if we go with just this single constraint the circuit is under constraint and in order to be sure that the only solution is the one we specified in our assignment stage block we need another constraint and that one is specified by the instruction constraint x * R so

constraint takes a polinomial expression and assures that it should be equal to zero so we add the equation XR equals z which obviously assures that a nonzero X implies having a zero R and that is the entire specification of the circuit quite concise just like we wanted it does all this actually work well I dare say yes this is already implemented it's part of nil's um GitHub repository and if you want to try it you can go there and try it but well when I say work I mean we really use it uh the syntax we are promoting has native

support for naming table celles it is used the technical details are hidden and all this makes circuit designed more readable and better understandable and maintainable which is acknowledged by our designers our old circuits were actually easy to Port because we maintained a lot of comp compatibility with our previous syntax and we are currently implementing circuits to verify evm traces and the new syntax actually helps us a lot in that so I think that our transition was a step in the right direction that is all thank you very much

[Applause]