zkSummit - Introducing OpenZKP Stark - Remco Bloemen (Technical Fellow, 0x)

Transcript

[Music] Stark's it's a protocol family developer elephants and machinery observe clear Goldberg Alessandro at and others and they went on to found stark where and they've developed high-quality variants and implementations of this protocol an open C KP stark is an independent partial implementation of the variant used in the stark text alpha that was released about half a year ago so starix what's so interesting about them well first of all they have a transparent so a non trusted set up they have I would argue relatively simple math compared to some of the other journals proof systems

although for most in the audience here all of it should be fairly familiar by now they have excellent proof or a verifier performance and they have relatively small proofs not tiny but small enough by modern internet data standards but the coolest thing about them and the main subject of my talk is that they have a unique completely different constraint system and I say that with some irony so what are stark constraints so you take your computation you turn it into a computational trace so like take all the intermediate values of all your operations roll it out there long table of a size that needs to be

some power of two or some root of unity available in your field but very working with powers of two here then you pick a root of unity of the size the length of your trace table and for each column you create a polynomial that is interpolated on these values such that if I take omega to the power I and I feed that in my polynomial I get the value in the try stable at row I and that particular column I'll go into a concrete example soon but just to give you a high-level overview so now that we have this trace table committed to in polynomials what we can do is do

our constraints as rational expressions algebraic expressions over these polynomials and the standard way to do it is you write your expression such that it would evaluate to zero on the rows where it holds and then you divide out all the zeros of this polynomial and this division will only be exact and result in a low degree polynomial when the constraint indeed holds where it should concrete example everyone's favorite one Fibonacci so we have this function it takes two inputs and index which is like the Fibonacci number that were interested in and to make matters interesting it also takes in a secret

starting value so we're not starting with one one we're starting with one secret and then we iterate index times and we update our Fibonacci and return the value at this particular index so this is our problem now we can create an instance of this problem where we say hey we want the Fibonacci at index 200 starting with secret 42 and it just so happens to be this very large number here all right now we want to create a zero knowledge claim around this and our claim is going to be this we have the Fibonacci which has input 200 and something that I'm not going to tell you but the outcome will be this and I'm gonna prove you that I know what needs to go into these

question marks so first thing we do we create the trace table so it's really this you go through the algorithm you take your variables you table eyes their values which looks like this and then it's like you start with one and then your secret and then 42 and then this value here B will be the sum of the other two and so on we need to at some point we'll hit 200 and we'll have an A or a value that we return and want to approve but since we're constrained to a power of two we need to extend this to the next highest power of two so we'll

end up with 256 rows so it needs to continue a little bit longer words okay this is our trace table this encapsulate sour computation now what do we do next we have some constraints that need to hold on this trace table for it to be valid for this particular instance of the problem we need the first value to be 1 so like I comma 0 so like this is the trace table as a matrix I would mean the generic row which in this case is 0 you'll soon find out why and 0 is the column so first column the row needs to like the first column the

value needs to equal 1 on row 0 another constraint is first column needs to equal our output value at row 200 these are so-called boundary constraints because they hold only on a single row and then we have state transition constraints so what we need is that row I plus 1 at column 0 needs to equal row I column 1 so this value here needs to equal this value this value here needs to equal this value and so on this needs to hold for all the rows and then we have a constraint that says this

value here needs to equal the sum of these two that's this little thing here again needs to hold on all these rows right next step we interpolate this as two polynomials so if you look here the trace table itself didn't really change but instead of it being some arbitrary matrix it is now two polynomials weights are evaluated on these x coordinates where Omega is a food of unity of order 256 and if I if I were to take the first column polynomial I will get my first column values back second column is p1

and so on now that we have these pollen the next step is to convert these constraints into expressions that become low degree polynomials when they hold and there's a couple of steps involved in doing that the first thing is to turn them into expressions that evaluate to zero when they hold this is very simple we just subtract the right hand side from the left hand side and we're pretty much done here next step we need to turn them into we need to turn them into expressions over the polynomial so wherever you have t.i comma zero we replace it by p 0 comma X same thing

here now when you whenever you have t.i plus 1 comma zero like we have here it turns into p 0 Omega times X how does that work well if this is my current X the next X would be Omega 4 so if I take X and multiply it by Omega I get the next value so now that we have now we have this encoded and this is also why we needed to stay in the abstract I mean instead of giving specific values but because we need to have these X's in here but we still have this thing over here that we need to incorporate in it so first thing we can do is say that

okay it needs to hold on these values of X again pretty simple transformation I just take omega to the power whatever number is a year and so on the next thing that we that we do is that this expression is a polynomial that is supposed to be 0 at exactly this value of X same thing with this one it is supposed to be 0 at exactly this value of x and these two need to evaluate to 0 at all the values in this table right in other words this is a polynomial that can be divided by X minus Omega to the

power 0 and this one can be divided by X minus Omega to the power 100 and this one can be divided by a little bit more complex expression but let's show you the expression so if it's in one row I can multiply this thing by this expression where I and the result would still be a polynomial for the on every row constraint instead of creating a really complex expression that has like multiple monomial terms in there is one of these it actually turns out that you can get all of these zeros together using just this one expression here and

this is kind of the critical thing that makes these air constrains efficient if this efficient expression didn't exist the verifier would still have to have linear time evaluating these things there's one caveat though this thing will also be zero on the very last row which is actually not what we want because on the very last row if you do x times Omega you'll actually end up on the first row again and we'll have a constraint between the first row and the last row which is not what we want so what we do is we take that one point value and put it back in the numerator to remove it from this thing so now we have an expression that the zero on everything except the last row and we

can divide it out from this thing okay so we divide those out and what we're left with now is these four expressions that will be low degree polynomials if is what we want from it so we've reduced our problem from our original claim from hey I know this people nachi question mark there - hey I know of a trace table that satisfies these that turns these four expressions into low degree polynomials so this is how errors work on a very low level and we've

implemented a stark revert and take these expressions and turn them in like a proper start prove and verify your interest so what does it look like if you want to code this up there's basically this is more or less the entire public API of the library if you want to take the sort of syntax shared interface and what it is is you have two traits that you can implement on your claim in the first thing in order to make something verifiable we need to reduce it to a set of constraints which is this function it takes an object and then returns a set of constraint the

object is kind of arbitrary here returns a set of constraint and if you if you give or the library that in return it will give you a function verify that takes in a proof and will tell you if the proof is valid or not so that's all you need to implement the verifier if you want to implement the prover in addition to implementing the verifier you also need to implement a function that will give you the trace table if you implement that function in return it will give you a function that given a witness so like secret input gives you the proof that then in turn can be verified using okay how does that look like for the particular people not see

example first we implement our claim in a witness the claim struct in our case is simply the index and the final return value the index is you size an arbitrary number the value is a field element and then we have our secret or witness and which is just a single field element which we are going to put in the second step in the Fibonacci Chiang okay so we have our two types that are relevant now we can implement our trace table we want to start with the trace table because it's a little bit easier you implement provable given a witness for a claim so self in this case would be the thing

with index and value and witness here will be a secret so we initialize and we've round the trace lengths up to the next power of two we create a new trace table of sufficient dimensions in this case trace length and two columns this one better sounds even more Viki we initialize the first row 2d values that we want we iterate to the remainder of the row and basically just execute or Fibonacci algorithm as you would and returned the trace next thing we need to do is implement the constraint function so

given a claim object it has a function constraints that ultimately returns the constraint expression but let's step through it I'm including the rational expression class here which does a bunch of things like overload the multiplication operator and basically makes the math intuitive again we need to round up the trace length to the correct value we need to compute our Omega which is a root of unity of sufficient of size trace length then I'm trading two helper functions one is on row which is basically this on row expression that I showed the other is every row which doesn't take any input but it returns this more complicated

expression that is on every row except for the last all right giving these helper things now we can just return our constraints from expression we pass or delay dimensions we can put in a seat value that will acts as a seed in the future Muir transformed in the prover let's ignore that for now and then you give it a factor of all the constraints that you want to hold so in this case it is or this is the repeating constraint for the diagonal copy which is on every row so we just multiply it by that expression the division is already happening there same thing with the same thing with the Fibonacci addition

constraint on every row we have our first fixed value and it needs to be won on Rosie row and we need to have the output value at the row that we have on the index this is also a good time to mention that Starks have a funny property that the constraint system is a function of the public input and not a function of the problem that you're trying to do which gives you a little bit more flexibility and haven't seen any actual practical uses of that but it could be interesting alright so now that we have these how do we actually use it very simple actually we just create a claim object and we create a witness

object and then we can do claim proof given this witness and there is your proof and then we can serialize this proof to bytes or we can use it immediately here and used to claim those verify and this function will words in an error when something's wrong okay so that's how you do a Fibonacci time left so we can do one more thing so let's go into Mimzy which is interesting in its own right so mimsy has some constants let's say in this case it has 16 constants it takes an input it keeps it at the constant repeated through the through the list and then returns it

right so we only have one variable so we end up doing this with one column and we'll end up having a constraint that looks like this the next value is the cube of the previous value plus this constant which should be repeated and the reason I'm bringing it up is because this is a cubic example which is a little bit different although mostly in the prover end and because it has this repeating pattern in there which is interesting so how are we going to handle that well first we can do this straightforward conversion to polynomial forms of columns it works but what do we do with this K here let's look at it a little bit more let's say

so here's how you can solve this so let's say we have these values of X we want to somehow get access to values that are a repeating pattern of these 16 values that we have here so let's first look at X to the power 16 if you look at what this does to the value of x you'll see that it has this it has this structure of Omega to the power 0 Omega to the power 16 and so on all the way to Omega to the power 240 which will already happen at Omega to the power 16 here it will be a 240 here and then it will wrap around and we will have at Omega to the power the next one we would have Omega 0 here again and this would

cycle and cycle until the last row where Omega to the power 255 would correspond again to Omega to the power 240 so basically we've already created a repeating pattern of our omegas here this is a repeating pattern with 16 values in it and it repeats 16 times to Pat it out to 256 values okay now we can take a polynomial over that value which we'll have let's say this is some arbitrary polynomial it will have 16 different values here and then it's pretty much forced to cycle because its input cycles so the next one will be repeated again and so on which means that we can interpolate this and come up

with some degree 15 polynomial that gives us a repeating pattern with exactly the values that we need in order to satisfy the constraint that we want so this gives us the answer we have this degree 15 polynomial expression over X which we can evaluate over X to the power 16 and then we have our constraint expression again and now we can kind of forget about B numbers at the beginning we don't really need them like in the end you still have a trace table that only has one column you just end up with a more complex constraint expression and the remainder of MEMC is nearly

identical to Fibonacci you need to divide out the zeros where you want to constraint the whole you need to have an input and an output boundary constraint but it's pretty straightforward from here so this is where our library is right now with our stark implementation so some of the future directions that we want to do is have constraints that go over multiple rows so right now we were limited in our examples to the current row in the next one future things would be to have longer offsets where you can refer back to values further back and actually this change just got in this week so you can already do that we have more examples in our system we have

Mimzy implemented we're working on a PDF implementation we want to build EVM verifier contracts ideally automatically generated from the constraint system higher-level language will be interesting because as you saw this is a really low level an awkward way of dealing with things there was just a really great talk on air script which is a very promising direction in doing this so what we end up implementing that performance should already be pretty good but you know it can always be better we love to optimize this stuff and in fact it seems viable to implement this on GPUs or even FPGAs to get more performance and another thing is that it it has a good try implementation low

degree testing implementation so it should also be doable to implement transparent no trusted setup marlene plunk Fraxel etc on it which would be an interesting direction and of course it's open source and you're all invited to contribute your ideas and code and issues so yeah thank you very much you