Provekit Local Proving

Transcript

All right, hello everyone. I'm just going to last talk of the day, so I'll I'll keep it simple. Um this is going to be about proof kid. We already did the incredibly interesting hard part earlier this morning. So I was left okay, what am I actually going to talk about in proof kid and I decided to talk about the next two cool things that I think are in in proof kid, um which is dependent R1CS and um how to avoid instantiating the R1CS matrices in the first place.

Uh quick introduction of what is proof kid. Proof kid is a project I started within world a couple years back with the goal of getting really good at client-side proving in a post-quantum way such that we can do things like verifying an entire passwords um a government-issued passport document integrity and age verification and all that on a crappy user's mobile device. Um how do we do that? We do that by cheating uh because proof kid is not a snark. Specifically, it is not verifier succinct. The properties we care about are zero knowledge, small proofs, and um fast proving time. We don't actually care about the verifier being fast.

Um To not scare you too much, you can actually make it verifier succinct with additional proof steps um in the same way that you can do Spartan with Spark. Um high level, the way the protocol works is um it's it's deliberately simple because simple things are easy to optimize and simple things run fast, right? Um so the entire protocol of proof kid version one is is is on the right here. Like you um you you commit to your witness, you get a random uh random challenges, you commit the you compute the second part of your witness, you commit to that, and then you um concatenate the witnesses and you run a single zero check, a single sum check to verify the R1CS relation.

That results you with three claims that you can then linearly combine together and then you just need to do a single linear opening. I'll go into a little bit more detail here, but the the there's three key ideas that that make proof kits so fast. Um the first is using the Spartan and G K protocol where you kick the kick the work over to the verifier. Um the second is to use where commitments and open them in in a linear form. Um and the third is to use uh split witness R1CS, which actually allows you to add lookup arguments directly in R1CS. And this combination leads to a very simple protocol that is very

efficiently provable. Where we are currently, we've released version one. Um it's been released. It's audited. It's running over BN254 scalar field. And this is primarily for like 100% compatibility with Noir that that assumes this. Um it it it uses the protocol I just described. Version two, we're currently working on. Uh the main difference is that we're going to be supporting smaller fields here for better prover efficiency. We're going to use do a slight tweak of split witness R1CS that I'm going to introduce here.

And then um yeah, again, same where commitments. Uh we're now using Zook for ZK, which is a little bit more efficient. We will uh deviate a bit from plain Noir because Noir has a lot of built-in assumptions on the field size that are no longer true. Um we also need to write our own Noir compiler in order to make that all work. So, that's what we've done. In the process of writing this compiler, we found a very cool way of computing all the prover values and verifier values you need. So, that's cool. Then uh once that is out, we'll work we'll work on a Noir circuit that can do recursion because we want recursion for this system. We already have a Groth16 back end, so um we can also run this R1CS instance on a Groth16 and then have it efficiently verified on

chain. Now, version three that I won't be talking about here, um estimated early next year, that's where we will go all in on uh bits and all it has to offer. Um and in addition to our Noir front end, we'll add a Lean front end. And I'm also thinking of an LLVM front end, so you can just compile your programs directly to it. Let's start with dependent R1CS. How am I on time? Good. So, basic R1CS, um you have your public inputs, you have your witness entries, and you have constraints um represented as as matrices.

Um what you do is you commit to a witness and then uh like call it W1. Uh and then you create this artificial witness which has this fixed one in there um to make it a fine. Then you have your public inputs and then you have your W1 that you committed to. And then you test this um this bilinear [clears throat] relation, right? Split witness R1CS is a um small variant of this. I don't know if people are as familiar with this, but it it's very powerful and I'll show you why in a moment. The only tweak we make to R1CS is that we commit to um W1 and W2. And in between, we allow um the circuit to sample random values. So, now you can do

a one-round interactive protocol inside of your R1CS. Uh and as we all know, random challenges give you a lot of expressive power. Um the rest actually is completely the same. After you've done the commitments, you just proceed as if you do a normal R1CS, only in the end you need to do a batch opening of both witnesses. Now, the motivating example for this is lookup arguments. Um I'm not going to go into the details of lookup here, but I just want to show how how this would work. Like in in in witness one, you commit to the queries and the multiplicities.

Then you receive your lookup challenges, and then the prover computes the second witness where it proves the entire lookup relation using these challenge values that it now knows. And this entire computation is just again expressed as R1CS constraints. Um, and this helps a lot. This is what makes Proof Kit version one so fast, so much faster than, let's say for example, Circom, which also runs on R1CS, but doesn't have the split witness mechanism, and therefore every single range check needs to be broken down to individual bits. Where we can easily do 16-bit range checks efficiently.

Um, it is not a new trick. This is This has been done in Gnark for a while. I think they were the first ones to run this at scale in production. Um, but we have a slight variation of this now with um, dependent R1CS, where we again use a split witness with the W1 and the W2, but now the realization is that um, these public inputs and these challenges, they are known to the verifier as well. So, we don't actually need to stuff them in the witness. They're not secret. They're public. Um, so we can have them embedded directly in the R1CS matrices, and make the matrices themselves functions of these public values.

Um, and then you get this slight variation of the R1CS relation. Um, and surprisingly, this buys you a lot, even over the split witness one. Uh, the motivating example and the reason we got here was to embed wrong field math, or more generally, integer arithmetic. And here, to embed a product, we present represent them as limb polynomials. Um, so you just take like if you took these polynomials and you evaluated them in the radix beta, that's where you get your integer value back. Um then in order to show that uh your product is correct over the integers, it suffices to commit to an additional carry polynomial and then uh prove this particular

expression. Um and now the protocol you can run is uh commit to all your limbs in in W1, sample a swatch simple evaluation points depending on your field size. For a smaller fields, we need to use a little bit more than one. Um and now for uh in in order to test this relation um over your prime field you just evaluate it limb-wise in all these S points. And this looks like a daunting expression, and if you had split witness uh R1CS, it is because you need to compute all these powers of X here. But if you have dependent R1CS, those are

all public. So in fact, this entire relation is a single um R1CS constraint. Um and in fact, we only need S constraints to to do all of this, and we don't even need to commit to anything in the W2 witness. Um at least not for this protocol. We still need range checks on all the coefficients to show that um they they are they are proper limbs. Uh and the lookup protocol still needs commitments in W2, uh but also the lookup protocol needs fewer. In particular, y- all the table size stuff is public, so that can all be embedded in the matrices, and you end up with a lookup argument where

the W2 witness no longer has any table size dependency in there. It just depends on the number of queries, which is um nice because range checks are expensive. So that was the dependent R1CS. Uh now I want to talk about the second cool trick, which is matrices as programs. So, we have these nice protocols and we like to turn everything into matrices, but these matrices are huge and we don't want to actually create them in memory. So, how do we avoid doing that at all? Um let's go quickly in a little bit more depth through these Spartan and ZK protocol.

Um let's ignore for now the public inputs and and ZK and so on. Um and I'll define a MLE equality vector um such that if you take the inner if if you take the vector for some like random challenge point X and you took the inner product with your um vector, then that would be equivalent to evaluating the the multilinear extension of that vector at that point. Um The reason for this notation is that a lot of the things we do here will be linear and this is the linear algebra notation just makes things easier. In fact, the only thing not linear in the entire protocol is this single zero

check. Um Now, how does our ZK work again? Uh we commit to the witness. Um we compute these A, B, and C vectors that we need for um that we need for a zero zero check. Uh we'll see that this actually makes sense to compute them directly with the witness itself. Now, you receive a challenge for your zero check and the next step is to show that these um satisfied our ZK relation. So, you do that. You run a zero check and that reduces this MLE claim to um an evaluation claim in a in a single point, um which is the expression you see there. The prover sends these MLE

evaluations in this point and the verifier checks that if the prover isn't lying about these values, then indeed um this relation the zero check relation holds. So, then the only remaining thing to prove is that indeed the three values you received from the prover were correct. Now, recall these these values each are um some matrix times the witness vector in a product with some EQ vector. And what we then can do, and this is the the key trick that we use all over the place, uh is move one matrix to the other side. Um take the take the conjugate and move it to the

other side of the inner product. And what you now end up with is just an inner product opening claim over the witness. Uh we then send random values, we make a little random linear combination, and now we have a single claim that the prover needs to prove, which is just an inner product claim over the witness. And this we can do using an inner product opening protocol like War, where we can This is literally directly your opening. Um any sum check-based protocol like base fault and so on will be able to do this. Um that that's opening protocol still leaves you leaves you with a residual claim because the factor you use for opening itself needs to be evaluated in an in a multilinear extension. So, now we

get this funny-looking double multilinear contraction of the matrix. Um you can again do a little bit of algebra and it's a single scalar value and it's basically you have this M matrix and you sandwich it between two EQ uh EQ vectors to contract it to a single scalar value. And the verifier needs to check that this value is indeed what we ended up with after the opening. So, that was that's the protocol. Now, what actually do we need from the matrices?

Um let's define again the like random linear combination of the matrices. So, the prover needs uh needs three things. It needs the witness vector. It needs these ABC vectors so that they can run the zero check round. And then it needs this opening co-vector. Um This is this empty EQ gamma. The verifier needs a single scalar value that is this double contraction of M. And again, the reason that the verifier needs to compute this is the only reason it is not succinct.

Now, our goal is to compute all these values without ever physically constructing these ABC matrices. Turns out we can do that and it's pretty efficient. Um as a lot of systems, uh we have a witness virtual machine. Uh ours is in fact an interpreter. We we don't compile to native because iOS doesn't like you to download native binaries um after the fact. They need to be code signed and go through the App Store. Um so, we actually have a really fast interpreter. Um simplified, leaving out the control flow, this this VM looks like this. You have an instruction witness that can take a hint. It will witness this value, store it in the

witness vector. You can have constants, additions, uh scalar multiplications. That's just your standard field operations. And then you have an operation called constrain where you give three values and you say these three values need to satisfy the R1CS relation. And then there is a um a a value release that means I no longer need this local variable. Which is explicit in this VM because it will turn out to be useful later. Let's take a simple example program where we have two public inputs. We compute a linear combination and then we compute two products.

Uh if we do that in our simple VM language, it will look like this. Uh we take our witness in we we take our input values, we witness them, which effectively stores them in the witness. Uh, we construct our T. Then we witness the two products. The hints are, of course, the product values, and then the constraints below guarantee that these uh hint values were indeed computed correctly. Um, yeah, we witness layout is pretty basic. Uh, T itself needs no witness slot because it is only linear, so it gets absorbed in the um, constraint matrices, as we will see.

Let's start with the simplest case, which is just your just regular forward execution, where we compute simultaneously the witness vector and the ABC vectors. Um, yeah, so we uh we set we we we set our inputs. Um, as we as we work along, each witness instruction will append that value to the witness vector. So, we start with the witness vector initialized with one. We we uh witness the the the the two inputs. They get concatenated. We do some field operations.

Um, and then and then we witness a product, um, which is concatenates that raw value to W. Then we uh witness a constraint, which concatenates these three values to the ABC vectors, and so on. Um, we can ignore the the releases mostly. They don't really do much here. Um, and as this executes, um, we already compute all these four vectors. And you can really see the advantage of doing this in a single pass here, because this is not unexpected, but these ABC vectors are just intermediate values in the computation of these witness vector in the first place. So,

by computing them together in one pass, you save a lot of work versus first computing the witness, and then computing these matrix witness products, which really just replicate work you already did anyway. So, that's the forward pass that gets us most of our values already. Now, I want to start with the verifier pass because it just makes things a little bit easier to explain. So, the verifier needs a single scalar operation a single scalar value, which is this double contraction. Um we're going to run the VM again, but this time we're going to do things slightly differently. Uh when we see a witness instruction, we just ignore the hint. We do nothing with it. We don't even compute it. Instead, the witness returns um this EQ delta

at coordinate J. The next coordinate that is that is like we we pop the next value. Um constants just become constant Sorry, constants become the constant times the first witness value or like the the EQ delta zero value. Um all other operations just remain regular field operations. And now, whenever we see a constraint, we accumulate that particular combination of the arguments that we see. Um and again, release does nothing. Um so, we run this little accumulator, which is initialized to zero.

Um the witness is initialized with this EQ delta. And and we run our program again. And our internal state, uh I have it in full expressions here, but all of these in the end I just field values things, and it evaluates really quickly. So, we yeah, we keep popping our um our witness EQ values. Whenever we have a constraint, we add the accumulated combination um with all the right random factors to S. And at the end of running the program again, we will have our S computed correctly.

So, no need for doing anything, instantiating the matrix, or anything. So, that's cool. Now, um the hard one, uh which is this uh which is the co-vector for opening. This one is more challenging because it contains the transpose of the matrix. And how do we get the transpose of the matrix? Turns out that this is uh automatic differentiation of of the program um which is something very well studied thanks to back propagation.

But, recall what the verifier pass computed. Um for some uh for some witness value, uh in that case it was EQ delta, but it could could have been anything really. It computed EQ gamma uh times M times this W, right? If we consider that as an abstract function in in in the witness value, then um consider the Jacobian of this function. Turns out this Jacobian is exactly the expression uh that the prover needs to do. So, yeah, let's just run the verifier pass in automatic differentiation over the witness.

Um and the the way we do this is uh by constructing an evaluation graph as we go along. Um whenever we see a witness instruction, we create a uh [clears throat] an an an independent a new independent variable. Um whenever we see a constrain, um we see the operation. And the remaining abstract the remaining instructions become abstract expressions that get accumulated in an in an uh expression graph. And then each node will store an accumulator, um which is just a field uh field value, that will equal the um the partial derivative of that node uh with respect uh sorry, uh the partial derivative of

the the whole function with respect to that node. So, that changes our instruction semantics. Like before, we ignore all hints, but this time we create an abstract value each time we see the witness. A constant is represented as a multiple of the abstract value representing the first witness value. Add and scale now create now create an expression graph. And constraint now seeds the operands with random values again. So, now like whenever we see you constrained, we know that the partial derivatives get this value added to them.

And now the now release actually starts to do something. Whenever a a node in the graph is released, its partial derivative gets propagated to its children. And the node itself is freed. And when we're freeing a leaf node, we just write the partial derivative because now we have the partial derivative of the witness function with respect to a witness element. So, we just write that directly. So, let's let's go to our example again. We initialize our output vector at zero, all node accumulators at zero. The witness now creates independent leaves.

Our linear operations just construct a nice expression graph. And on release this this release doesn't reduce any reference counts to zero because all of them are contained within T, so nothing happens here. Then we create a witness of the product. We just create a fresh new leaf this time pointing to index three. Now, when we hit the first first constraint, we add this random combination of values to the partial derivatives of our graph nodes at these

of our graph nodes that were added to the constraint. And then we release C. This is the first time a leave node gets freed, so what happens is we write at the Z position in the witness vector the value of um the partial derivative of Z at that point, um which happens to be exactly the the thing we need, of course. Um and we just keep going with these semantics, running the program again. And then at the end, when we do the uh final release, all the ref counts uh pop to zero. So one by one we start uh we start writing all these um all these elements to the witness

vector, which now happen to correspond exactly to the thing we were supposed to compute for a cofactor. And uh there you have it. You have one program, you execute it in in in three different ways, and you compute every single thing you you need without ever having to create the entire ABC matrices. Um Yeah, fun trick. It actually uh it's it's in a way a generalization of the trick that that Flock uses. It uses uh it calls it circuit walking.

Um I think we we had this this predates Flock um and I think the realization that it is a um a partial like a Jacobian is a little bit more powerful because it kind of applies to any program. Um but there's definitely a lot of similarities there. And then future directions, well, we do want to get succinctness. Um one interesting question is like if the program contains repeated code, like loops for example, can we compute this verifier value more efficiently? Uh I suspect we can. Just haven't had the time to really nail it yet.

Cool. I'm out of time. A- Any any questions about either dependent R1CS or programs as matrices. >> Yeah, so right, the matrices [clears throat] you you know them you know them in advance. You can pre-process them. So I'm a little surprised you so much want to like not sort of use them. Like for example, I mean So here here right here you're computing the this value without using any pre-processing on the on the matrices.

But >> Yeah, we want to avoid anything matrix size because the these matrices are order of magnitude your witness size. >> Yeah, but maybe there's a sparse representation. >> Yeah, yeah, we do that. We do that. No, they would be quadratic if it wasn't. >> Yeah. >> It's it's already sparse. Proof kit V1 actually stores the full matrices. It doesn't use this trick yet and it results in circuits that cannot be represented under like a couple megabytes and this is kind of a hard goal for us. The only way to get under a megabyte is by representing the program succinctly and the only way to do that is to actually keep the loops in the program encoding.

That you cannot fully linearize the the bytecode. You need to keep the loops in there and this whole strategy is compatible with that. As long as the execution order remains the same, you can just keep looping things. >> I see. So so typically it's a you start with a program with a branches, loops, stuff like that. So that representation is is much smaller even compared to the like a sparse >> Yeah, oh yeah, that's right. >> the representation of the matrix with only the non-zeros, it Yeah, yeah, that's right. It would be very large compared to >> Kilobytes versus megabytes. It's a huge difference because you usually have a lot of repeated code in constraint systems.

>> Hey, if the So if the if the go the desire of dependent CS is because you don't want proved kits to store the like this large 2 megabyte matrices in the app, why not just store the front-end code and just run the compiler to compile the the R1CS? Is that too slow? Um sorry, so maybe I'm misunderstanding like What is What is the the desired like You mentioned earlier like the that that the R1CS matrices are about 2 megabytes, and that's too big.

>> Yes. >> Um too big in what context? Is it like downloading from some server or storing in the app or >> Um >> [sighs] >> downloading uh is the is the biggest one. Um the the other is that doing these matrix multiplications is just an expensive step in the prover. Doing it this way is is turns out to be a lot more efficient. >> I will see. Okay. >> So, I I mean the one of the arguments that was always made in the in StarkWare's papers is that um the the scalability in uh the PLONK and Stark um was an inherent advantage over approaches that require you to materialize these um kind of large matrices for circuits. I

I Have we just made AIR obsolete? >> Um if you can solve this problem, uh you you're a long way there. They I Like not yet because AIR is is very efficiently verifiable, right? Um it it captures repeated expressions efficiently. There are similar things you can do in multilinear land um where like if your M has a very clear power of two repeated block structure, then it almost becomes trivial to do this. Um I think you can also do it for more complicated structures, but if this is an arbitrary program, it's a harder problem to solve.

But it seems solvable. >> So So, if your program has loops, then do you pay just the the program size or do you pay the execution time? for the loop >> In this case, you will As it is now, you would be paying for the full execution. Every loop would be fully unrolled in execution trace. Um but if you can figure out hey, this loop is just doing the same like block over and over, so we just need this random linear combination of the like EQ or whatever, and run it against that.

That's That's when you would start seeing the gains. >> Okay, that seems worth exploring. >> Yes. But even even as it is, um this execution step, it runs in a VM. It's a very optimized direct-threaded VM. It's like yes, technically proof kit is not succinctly verifiable. In practice, it's like tiny millisecond values that it takes to to run this. You You're not even computing um all the all the hint and and and like complicated things. The only thing you're computing is like the small little gap that you have from your witness to your constraints.

>> Yeah, you would need that the execution time of the program to be quite large in order for that to pay off, I guess. >> Yeah. >> I think we had time, but >> Oh, you want >> Almost the time. >> Oh, okay. All right, well All right, so If Yeah, if it's a program with a very uh smaller presentation is it clear that it's it's worth going to to R1 CS?

>> In in our case, it is we have very ugly in homogeneous programs that combine hashes and and C bar parsing and ECDSA and in all sorts of crazy fields that don't support FFTs and you name it. Um Yeah, probably you can handwrite a GKR circuit that performs better. I I want to, no thank you. Um and honestly, it will be hard to make it perform better because a big chunk of what make proof get so fast is that we're doing a we're doing like two commitments.

We're doing a zero check and we're doing a batch opening. Um yes, they might be larger than like the values in your GKR, but good luck getting that faster than my super SIMD very simple thing. >> I I I I guess I was thinking just compared to um to air to like I don't know whatever StarkWare would traditionally >> Yeah. Air constraints are hard to write by hand for circuits of that complexity. What tends to happen is that you would use them to write a ZK VM and then run the Z run your program in ZK VM. Um but >> [clears throat] >> my my argument is that the circuit compiler is always going to outperform a ZK VM.

>> Right. >> If your circuit is fixed. >> So I I came in after the start of the talk. Did I miss any benchmarks? >> No, I didn't have any here. >> have any benchmarks. Okay. Okay. Can Can you Can you remember any benchmarks that might be >> actually on my I have on my website um some benchmarks on what dependent R1CS does. I don't have benchmark yet on um what the uh programs as matrices does.

But, it is partially implemented already. >> I always said that um kind of building lookups um and grand product arguments and and so on into proof systems is the wrong approach because you can just use this um uh this extra challenge trick um to build it more compositionally. >> Mhm. >> Yeah, it's uh I've been saying that since um kind of Halo one. >> Yeah, GTR has and and grand products and everything that are derived from it has the advantage that you don't need to commit to as many witness values. That's the That's the main benefit.

Um and I'm kind of wondering if there are like tricks that are worthwhile to incorporate it here. You could imagine like a multi-step R1CS where you derive a dependency chain and then you you close the loop by tying it back to the witness again, but you avoid having to commit to the intermediate values. >> So, the the split um R1CS um you can only sample a single witness value. Have Have you come across any cases where it's useful to have multi-stage where you you're the verifier is um sampling more than one witness value in different stages?

>> Um only recently. Um yeah, we are aware I mean, it's trivially extendable to multi-round, right? Um only recently did I find a case where it makes sense to have more and then this for ECD ECDSA verification. If you um you can implement this with probabilistic soundness using um incomplete addition formulas as long as you first commit to the witness, then you like randomly offset everything, and then you run your integer constraints, but they then again need a randomness to be checked.

So, that's where you would naturally end up with a tree with a two-round protocol. >> Last question. >> Yeah, I'm interested if you've thought of sort of exposing that functionality to the user. I just means that basically every time the user needs random value, like you add another round. Um yeah, have you thought about doing that? >> Uh that would require a new new language extension.

No, we we definitely thought about that. Um >> [laughter] >> I think right now um we're still just using it internally. Um to to do all the range checks and look up arguments and and also some some auxiliary um uh look up tables for like binary operations. >> Right. >> Um but yes, if you if you did that in the language itself, like the maybe the prover it doesn't even need to implement that and um all those look up arguments just become a library function in Noir. >> Right, exactly.

Yeah. >> Yeah. Al- always looking for ways to simplify things work more and make the verifier work harder so the prover has to do less. >> [laughter] >> Thank you. >> Yeah. >> [applause] >> Thank you.