Bitz Are All You Need

Transcript

Yeah, I just want to do some some quick words of praise and introduction and why we're so excited about beats and then Albert will get into the because Albert has been the lead researcher here. Um so how do how do we So I'm working on a thing called proof kit which is for client side proving. The goal here is to be able to do digital identity in a private preserving way and that requires a lot of verifying existing um existing cryptography. So a lot of traditional hashes and traditional signature schemes and these tend to be really hard to zero knowledge proof.

Albert has been working for a couple years on a series of schemes called sync and sync plus that allow you to do zero knowledge proofs over the integers and this allows you to embed all sorts of weird wrong field math really efficiently. Um so we started collaborating over the summer. We had a wonderful research get-together for a week in Warsaw where some of you were here where I was well. And then one morning over breakfast Albert had this little note with like a completely new construction and we started implementing it and optimizing it and we were just like blown away after once like after and after by what it can do because it it like initially and what most schemes do the strategy is well you

have your binary field constraints and then you have your like integer constraints or your prime field constraints and you find a way to connect the two. But these schemes can just do all of that in one operation. Um Yeah and that kind of changed our entire road map for the next versions of proof kit which is going to go full on on beats and I think a lot more people will want to consider using this as well for all the interesting properties that it has. So Albert I'm going to hand it over to you to to present it.

>> Okay. Let me put the timer just in case. All right. Thanks uh thanks for the introduction, Remco, and for the invitation. It's a pleasure to to present this research here and so let's get to it. So, I'm going to explain So, Bit Z is a is a BCS and mainly the construction is mainly a BCS. I'll explain how we use this BCS in several applications.

Um but the the the construction itself is a BCS and I'm going to explain what it allows to do, the properties it has, and then I'll explain how we how we achieve these properties and all these functionalities. So, the idea is that we have a ring S, any ring, for example, a finite field, the integers, a lattice, integers modulo 2 to the 32, and so on. I will quickly just for now I will this I will use abstract rings, but at at some point I will just set I will just fix S to be Z or a finite field.

But just bear in mind that everything works on any ring here. So, the Bit Z allows to commit to a a vector of elements from the ring. So, our witness is going to be denoted F and L is the size of the witness and it's full of ring elements. So, we commit to F and then we are able to prove linear relations on this F. So, inner products for this F. V is a public vector, mu is a public value, and we want to prove this type of relations for F.

And not only that, it's a bit it's a bit weird. Uh we want to we we we extend the the functionality in the following way. So, let's say that we have another ring R and I have a morphism from to R, so think for example Think for example that S are the integers and R is a prime field, and I will explain later why this example is relevant. So we also want to be able to prove claims of the following form. So our witness lives in Our witness lives in the in the integers, but then we have for example a relation over a prime field. So we have a linear claim on the projection

of F over the prime field. Okay, and of course if we have inner products include MLE evaluation claims, which is what we are after at the end of the day the day because we are constructing a a PCS and we want to use it inside a PIOP. Okay, so this is the functionality we we construct. The properties of the PCS we end up with are that it is paper bit. So essentially all the costs of the commitment and the the opening proof depend almost exclusively on the amount of bits you have in your witness vector. They don't depend on the rings or the the projection.

We achieve commitment plus opening throughputs of 2 to the 31 bits per second on my MacBook Air. As I said, because we we work with fully abstract rings, you can use this PCS in essentially any SNARK or for constraints over essentially any domain. Or you can even have more than one domain in your constraints, and as I will explain, we build a SNARK that proves constraints that are expressed both in Z and a binary field at the same time.

It also provides free range checks because as as you will see we commit to the bits of the witness really. So committing to the bits of the witness already gives you it gives you an automatic range check for for the entries of the of the witness. Um Yes. >> So, just small question. You're saying PCS, but it looks here like you're you have a more general functionality like inner product with arbitrary vector V. Is that like just >> Yes.

>> So, it work it you can do that. You >> Yeah, yeah, we can do arbitrary linear constraints. Yes. We yeah. Maybe PCS is a is the wrong term. >> I assume you need some sort of succinctness from V. >> If you want to verify to be succinct, yes, of course, yeah. Yeah, and for practicality we want some kind of we want to have at least a tensor decomposition for V. Okay. Oh, uh yes, and I will the use cases I will discuss during the talk are are these ones on the on the top corner.

I'll discuss even your multiplication, exponentiation modulo an RSA prime, RSA, SHA-256 DSA, SHA-256 multiplication modulo 2 to the 32, and Falcon signature. And I'll present some results for this. And then the protocol is very simple. If you For example, for all these applications except except the last two or maybe except the last one, we build a SNARK that uses Bit Z and this SNARK is very simple.

It consists of Weir or Ligero over a binary field. You could or you could use another PCS over a binary field. Uh Spartan over a finite field or if you want any PIOP for finite fields. Uh a GKR for grand products over binary fields as a protocol. If you forget about optimizations, this is just GKR for grand products, nothing else. And then maybe you have projection to a random prime field, meaning that you sample a random prime and then you project your constraints o- o- over there. Though that that step is avoidable.

So, if you forget about optimizations at that protocol level, this SNARK is is just made of these components. Okay, so let's start with a use case first and then I'll explain how how B Z works. So, one of our use case is proving multiplications. So, we we want to prove 2 to the n multiplications of w-bit integers. What we can do is we can we either arithmetize it over the integers or we you can arithmetize it over a finite field of sufficiently large characteristic.

And then you write range constraints, but these range constraints don't really exist for us because, as I said, they they come for free. Uh the PIOP works as follows. So, if we do the R1CS over the integers, i- if it if the R1CS is over F, it's just a normal PIOP. You just essentially run Spartan. If you write the R1CS over Z, it works as follows. So, we commit to the witness, integer witness, with B Z. Then the verifier samples a random prime, Q. And then we take psi to be a reduction modulo Q. So, that's the example I I pointed to before, where S are the integers and R is a prime field.

And then the program verifier run a PIOP over the the field FQ with a projected witness, psi F. So, they just run a standard PIOP over the finite field with the projected witness. And, as we all know, at the end of the PIOP, you have a MLE claim for for your witness. And now this thing can be proved with Oops. So, this thing can be proved with B Z because that's what the >> [laughter] >> the functionality that B Z enables you to do.

This whole step is called fingerprint plus pattern. So, step two is a is called fingerprinting. Uh it's due to Campanelli and and Matias Hall Andersen. Um and yeah, these are our results. So, in this for for these slides I'm only comparing to B news because B B news is the scheme that I found that's most close in performance to B Z. The every other scheme I I tried uh lacks uh significantly, but if you think something's missing, please let me know.

B news optimized is a I just asked AI to optimize as much as possible the latest version of B news without changing transcripts for for total fairness because we also did that with with B Z. So, we we go over 12 uh multi million multiplication per second of 32-bit integers as a highlight. Uh another highlight is that proof sizes can be reduced quite a lot by increasing the rate without damaging too much the the the prover time because the prover time is dominated by the grand product that I mentioned. And the grand product is not affected by the rate. So, this is at at rate 1/2, but if you decrease the rate

and you put it to say 1/32, the prover time is not done is not significantly damaged and the proof size is decreases a lot. Okay, another use case where fingerprinting is is very relevant is RSA. So, say we want to prove four This is an uh a computation from from a a recent paper called Limber. Um say we want to prove some exponentiation modulo an RSA modulus. So here we do really want here we we want to arithmetize over Z instead of over a big finite field of big characteristic because here the fingerprinting part uh becomes quite quite helpful because

our witness is is going to contain entries that are thousands of bit long. Um so what we do commit to the witness F over over the over the integers and then you run fingerprint plus Spartan, the technique I explained before. So you run Spartan over a random prime field and you end up with an anomaly claim for for the projected witness. The nice thing here is that the prime you are using has say 128 bits and the entries of your witness have thousands of bits.

So once you have once you have projected your constraints and your witness to the prime field, you have compressed your witness elements by say 10x in bit size. Uh so for this application arithmetizing over integers plus fingerprinting is is quite uh beneficial. So we get this this performance. Um so yeah, the the computation is taking uh is taken uh as is from the Limbo paper.

Okay, so let's build the PCS. So on the top is the functionality we want to to build. I'm going to fix for simplicity S to be the integers and R to be a prime field and size reduction modulo Q. So the step first step we are going to do is we are given the witness F. So first step, we assume there's a public bound on the bit size of the entries of F. Uh so, we assume that whatever witness the prover might ever need, uh the entries are bounded by B, and this is a parameter a public parameter.

So, now we can decompose we can so-called so-called we say we bitify the witness, which means we take the witness and create a longer witness that's made of bits. And this longer witness is related to to the original one via linear relation. So, we we create vectors that correspond to the binary decomposition of F in this case because we we are working on integers. And we define bits the the bit vector of F to be the the concatenation of these of these uh bit vectors.

And now if we take the claim we want to prove, the inner product claim we want to prove, and we express F in this as as a as this linear combination of the bit vectors, we get this new inner product for the bit vector F. We just have a the a linear claim on on F is a linear claim on the bit vector of F for a different weight vector. So, now instead of proving the initial claim, we are going to prove this new claim in here.

over the ring R, which is recall a prime field. Second step, we commit to the bit vector over a binary field in packed form. So, we group every 128, so this new here is 128 for us. We group every 128 bits of the bit vector, look at them as one binary field element. Uh so, we create this new vector, which is 128 bits smaller than the bit vector, and then we commit to it with a with a linear code. Though, you could commit to it with if if you're using another PC as you could use what whatever PCs you're using.

Okay, so there are some issues uh that will arise as I try to to build bit Z. I will solve some of them, and some of them I will only mention. This one I will only mention, which is how do you do the bitification step if S is an arbitrary ring? That probably I won't solve because of time. Okay so the first line here is the thing we want to we want to build functionality for this. Now, we have a ongoing claim, which is an inner product claim on the bit vector for some new weight vector, this one, and also the verifier has this uh an oracle to this to this the

encoding of the packed vector of bit of the bit vector. So, step three is we lift the constraint to the integers. This is a constraint over a prime field, so now we replace this constraint with a new constraint over integers, and this is just just you take the weight vector U, and you look at the at the entries of U as integers. So, you we write psi minus one to emphasize that we are looking at the entries on integers, but this is like this is an oop if you think of prime field elements as integers between zero Q minus one.

The prover provides the the value of this inner product, so mu prime is provided by the prover. And now the verifier checks that mu prime modulo Q is equal to mu. And now if once the verifier has checked this, proving double star implies star. So, prover and verifier are going to prove double star now. And step four, we lift this constraint to an exponent of the binary field. So, we take a generator of the binary field following the lead of other other approaches like Binius, uh though in a different context. I will explain I I will discuss more the difference

later. So, we just take this equality and we lift it to an exponent of the binary field. And now I'm skipping some soundness. I should discuss soundness. I will do it at some point. But now prover and verifier are going to try to prove this constraint here, uh which because the this back the because the witness vector is made of bits, you can rewrite it in this form. So, every factor of this grand product, so if if the ith entry of the bit vector is zero, then this factor is one.

If the ith entry of the bit vector is one, then this factor is g to the ui seen in in the integers. So, you get exactly this this inner product in the exponent of g. Okay, but look at this. This is a polynomial on the bit vector entries. So, the we are now in known territory. We have a polynomial constraint on a vector that we call So, the polynomial is over a binary field and the witness for the constraint is a vector that lives in the binary field and we committed to this vector. So, now we are on on known territory. In principle, uh all fields match,

which is nice. Um Another thing is that another issue is in principle, we want to allow for constraints in any ring, not just a prime field, so one uh one question that arises is if this constraint is over a arbitrary ring, how do we do the lift to integers? Because then uh it's not completely obvious how you transform the inner product claim over an arbitrary ring to an inner product claim over integers. Um maybe I'll I'll discuss this later.

Issue three is that as I said uh there are some soundness considerations here, so lifting to an exponent doesn't prove proving this constraint only proves the the double star, the integer constraint we want to prove, modulo the order of G. It doesn't prove it over the integers. So uh we'll this one we will resolve uh afterward. Okay. So again, first line is what we want to build. The second line is the the claim that the program the ongoing claim that the program verifier want to prove.

Uh now so now I'll I'll do uh naively I will try to prove this claim with a grand product GKR over the binary field, like as again this is a known constraint, it's a grand product involving a a witness that we committed to over binary field so we can do the a simple one, for example, grand product. So if we do a grand product for this constraint, we end up with Emily evaluation claims for the bit vector and this public part of of the factors of the grand product.

And the claim for the bit vector, you can prove it with Weir or Ligero or any any uh PCS over a binary field. Uh and we use um we use the ring switch from Venus, of of course, because we committed to the packed vector. We didn't commit to the bit vector. Uh and then one of the biggest issues with this approach is that the grand product is very expensive, so here there's there's not much we can do in terms of of optimizations. If we improve this grand product directly, all all terms in the sum checks we we end up with are are big. They are big field elements of 128 bits. So, there's no small field trickery we can we can

use. We can we cannot do univariate skip and other optimizations. Also, uh the verifier or someone needs to prove this MLE or check this the the claim for this part. And this is not a succinct vector, so if the verifier checks this this MLE claim, then the verifier is not succinct. So, that's something we'll have to resolve as well. So, let's let's jump into these four issues to these last two issues. So, issue four is that the grand product is is expensive. Issue five is that the verifier cannot check the claim if the verifier is to be succinct.

So, what what we are going to do is assume some structure on V, which is a harmless assumption because at the end of the day the day we want to use bit Z as a PCS, so V in general is an EQ vector. Usually, so usually V has this form. What we are going to do is we assume that V decompose has a tensor decomposition with somewhat flexible dimensions, which is the case in practice because V is an EQ vector and the EQ vector decomposes however you want.

Then, remember that our new weight vector is U, which is the tensor product of V and these powers of two. So, again, if if V has a flexible tensor decomposition, then U does as well. So, we assume U has the tensor decomposes uh into two vectors of dimension L1 and L2 with approximately L1 L2 being square root size. Okay. So, now we are in this setting.

And remember, we are trying to prove what what we really want to prove is this equality, this integer equality in an exponent. So, now we take the inner product and write it as an inner product of inner products. So, as a linear combination of inner products, leveraging the tensor decomposition of U. So, there's a it's a linear combination of square root many inner products for vectors of size square root.

So, now instead of proving this integer inner product claim, we are going to prove Well, first of all, the prover will send purported evaluations for these inner inner products. So, these ones over the integers. And the verifier checks consistency, so it checks that if you replace these inner products by the purported values, you get uh the appropriate equality. And now the prover and verifier are going to try to prove these square root many inner products for vectors of size square root.

So, the new claim is this one. So, there's there's now square root many gram products, uh but now every gram product has square root many factors. Okay. And now So, this is the current claim. There's L2 run products, each with L1 factors. L2 L1 are essentially square root. In total, there's L factors. But, let's look at what these run products are. So, what are what are the factors in each of these run products? So, the bit vector this this part in here is always zero or one.

So, every factor is either one or G to the one entry of U U1. So in in total, all the factors are contained in this set. And this set has size square root L. So, there's L factors in total, but the amount of values that these factors take is square root of L only. And because of this, we say that this collection of run products is has low entropy.

And now we are what we are going to do is we prove these run products with the GKR protocol in a a batch version of GKR protocol, pretty standard one. But, we use we use a lot of optimizations that leverage the fact that the run product has low entropy. So, for example, we use tables of of size square root L that compute um compute values that are needed by the prover in different sum check rounds of these batch run product. Um if I have time, I'll I'll I'll go more in depth into what these optimizations um allow, but may mainly we manage that we

manage to, for example, for the biggest sum check, the first three rounds, the the first three messages of the prover are computed during square root many multiplications. Um the next Yeah and it's actually the first the first five prover messages are doing are computed with only square root many uh multiplications, and the same happens for the next layers, but every time you go up one layer, you you you have one less round where you do square root many multiplications.

Okay, and this also automatically resolves the the problem of the succinctness for the verifier, because at the end of these grand products, you end up with an MLE claim for the bit vector or many MLE claims. Oh, I I didn't say I'm organizing the bit vector in in a in matrix form, right? Probably it's it's clear. And yeah, the MLE claim for this public part is is a an MLE claim for a vector of size square root. So, this can be evaluated by the by the verifier directly.

And note that every >> [clears throat] >> This means that the proof sizes and the verifier have square root are are square root. And proof sizes are of square root size, because the prover sends these the values of these inner inner products. Um we are working on a poly-log version of of Bit Z, where the prover, instead of sending these values, commits to them with Bit Z, and then the check whatever the verifier checks with these values is proved by the prover with a Bit Z. I provide some numbers for for this logarithmic version of Bit Z, but they are preliminary. We We haven't reviewed them too much.

There's another option, which is to prove this batch grand product, you could also use some lookup to skip some GKR layers. Uh for those who who are familiar with this type of of proofs, so you you create a vector U, whose entries are products of several factors. Uh we tried that, uh but we we got worse performance. We we got basically twice the prover time and twice the proof size, because uh the lookup usually the lookup requires extra commitment.

Okay so a recap. The first line is what what we enable, what we construct. After the bitification step, we have an inner claim for the bit vector over uh the prime field. We assume that the weight vector decomposes into square root factors, uh in tensor form. We lift to Z. So, the prover sends the value uh yeah, so this is a recap with the with the necessary patches, the the patch I just explained. So, the prover sends uh the the value of the inner product lifted to Z, but here we lift every factor the two factors separately.

So, we don't lift U1 tensor U2, we lift So, so the weight vector is the lift of U1 tensor the lift of U2. Which uh is important, because if you lift if if your weight vector is the lift of U1 tensor U2, then you don't have tensor decomposition over integers. Uh then this is split into a batch of claims, so square root many claims. And the verifier checks consistency, and then we lift each of these square root many claims to the an exponent in the binary field.

And now it is a good time to revisit issue three, which is that when you lift to the exponent, you are only uh now if you we prove this uh this constraint we are only proving the original integer constraints modulo the order of G. So modulo 2 to the 128 minus 1. So in general but but we want equality in Z. So the issue is that there could be overflow and then we wouldn't we wouldn't be proving these inner products over Z.

So in general you could for example choose a binary field that's large enough so that no overflow. But we really want to stay on a small binary field because as I mentioned the grand product part is the most expensive part of the protocol and we really want to keep that that cheap and increasing the size of the binary field goes against that principle in a big way. So we really want to stay on 128-bit binary field and use the G high representation.

So yeah so I didn't say but if if this inner product this inner product because the bit vector is made of bits and this is guaranteed by the PCS this inner product has size at most square root times Q. So and the claim value again is is should be on a range between zero to square root times Q. And this can be checked by the the verifier. So the the difference of these numbers if the prover is dishonest is at most square root times Q.

So as long as square root times Q is smaller than the field of the binary field at the size of the binary field then we are fine like then proving this modulo 2 to the mu 2 to the mu minus 1 is fine. It implies the quality on integers. But otherwise we are in trouble and we don't want to increase new. New is fixed to 128. We don't want to change new. So, if this equality doesn't happen, and it is very likely that it doesn't happen because this FQ maybe comes from the fingerprinting the fingerprinting technique. So, this the Q is probably 128-bit itself.

So we In general, this equality does not hold. So, what we do here is we do primary sampling. So, before step three, if the if this overflow inequality doesn't hold, we have the verifier sample a random prime that's small enough so that there's no there wouldn't be overflow if we were able to use this prime. And now we replace the original claim in FQ by a new claim in FQ prime for Q prime a bit So, Q prime now is a bit smaller than the original Q, but it is small enough.

So, we replace this claim by this one, which is So, what we do is lift this claim to the integers and then project it modulo a random prime with the prime being small enough. And then start over again. Now, you lift it again to the integers and So, you go back to you you go you get into step three with this new claim. So, again, if you have your initial claim is on a prime field and the prime field is too large, you lift it to the integers, you mod random a new prime that's small enough, you you lift it again to the integers, and you are off to the races.

You continue with with the protocol. Yes? >> Um why don't you just choose the Q prime in the beginning? >> Uh because maybe you're maybe you're >> Q comes from the fingerprinting approach and you want to have 128 bits of security. And you you you've run a PIOP over the Q over SQ before. So, maybe you needed a 128-bit prime. >> I see. >> Okay, so there's this step 2.5, which is primary sampling, which you have to do if Q is is too large.

Then uh this equality here is proved with a GKR grand product, as I said, and then at the end you use weird or or any PCS over a binary field. Okay so uh uh a point here is that the reason why so so a key point that makes BitZif uh, practical is that we are able to leverage these techniques for the these low entropy techniques to optimize the grand product. Um, uh, yeah, so we were able to to prove the grand products because we split them into a bunch of low entropy grand

products and then we designed optimizations for these. So, the reason we were able to do that is that in BitZif we are only interested in proving linear claims on the witness. Uh, so we prove statements for values of of of this form, very intuitively speaking. So, we have a public value times witness over over the exponent. And and the public values have a tensor structure, which is very important. So, for example, in Venus 64, Venus 64 also uses um, Venus Venus 64 uses uh, they prove integer constraints in the exponent as well, but what is going on is they are proving the actual entire

integer constraints that the initial constraints that should be proved they are brought to the exponent which means that you are proving non-linear constraints in the exponent so it means you are handling elements of the form G to the witness times witness which prevents any splitting and and leverage of low entropy. There's some there's some There's some some some splitting related to a Frobenius twist but they are not of square root size they are of factor size.

And yeah. So so only handling G to the public value times witness which is a weaker type of statement and so G to the public value times witness is a weaker being able to handle those elements is weaker but the point is we only need to handle these values and we only need to do that because the non-linear constraints are treated outside of the binary field with a PIOP over a ring that's friendly to these constraints. So non-linear constraints we treat them outside of the binary field with a a good PIOP and then we raise to the exponent only linear claims on the witness.

Okay, and a nice a nice trick is that now that at the end of at the end of everything we have a Emily claim for the bit vector of F on the binary field and we committed to this bit vector but we might for example now have a an extra constraint on this bit vector. We might be interested in saying that this bit vector is a linear a linear a linear expression of some other vector which is smaller.

Uh so, in that case, if we added this extra constraint, we would have that the MLE claim on the bit vector is an inner product for this new vector G. And then so, we could, for example, commit to G only and then at the end of this entire protocol, we would have a claim on bit on the bit vector of F, which is exactly which is actually a linear an inner product claim on this smaller G. And I'll explain why this is relevant uh now.

So, another application is uh proving several hashes followed by ECDSA verification. And we arithmetize this computation as an R1CS over integers, but then we uh we add uh this this uh this constraint over F2 as well. So, the hash part I'll I'll I'll talk more about the hash part later. Actually, we are quite good on time. So, I'm going I have some I have slightly longer slides for for this. So, I'm going to use those.

Okay. So, we arithmetize the SHA part of this computation as an instance of this constraint in here, which is this constraint consists on integer integer constraints, integer linear constraints, and then uh linear constraints over F2. We call this relation the CM relation. It turns out to be NP-complete because you cannot arithmetize any Boolean operation with uh just integer linear integer constraints and linear F2 constraints.

And for this computation in particular, we arithmetize SHA as in this form. And yeah, this is the So, the nice thing about arithmetizing SHA followed by ECDSA with this constraint is that the witness is very small and the the witness we commit to, which in this case is G, is very small and this is for rate rate 1/2, but if we if we say if we do, for example, say rate 1/16, the prover time doesn't increase too much because as I said, the cost is dominated by the ground product, which

is not affected by the by the rate, and the proof sizes go below 60 kilobytes. So, we we have uh hashing of, say, 8 kilobyte messages followed by ECDSA verification and proof sizes below below 80 kilobytes. Okay. >> Uh Albert, before going into the the details of this new use case, I just wanted to open it up for for questions from from the audience. I guess I have a a question for uh for for Remco. Um as far as I can tell, you have a very big team of engineers working on this and you have a very high conviction that, you know, all of this

is is uh very powerful and uh and worth investing in. Can Can you talk at a high a more high-level kind of what is your conviction in in in in this approach? >> I mean, high-level, what we're seeing is that uh the concrete performance is amazing. And the expressiveness of this constraint system that you see here, that just has these these three matrices running over the integers and then there's one matrix uh running in F2. It's insane how expressive this is. We're able to arithmetize SHA-256, and the only additional um witness bits we need to commit to outside of literally the state that is

transferred between the rounds is like a handful of overflow bits from the additions, and that's it. There's no additional commitment. So, compared to all the other arithmetizations that are out there, um the witnesses witnesses are just so much smaller. That that I think is is already a big factor in in its its performance. Um and then, of course, these these ABC matrices are over the integers. So, in the very same constraint system and with the very same um commitments, you can also prove ECDSA or RSA. RSA, as you saw, thanks to fingerprinting, also reduces into something like only 17 constraints that you need in in R1CS. Um so, the expressiveness is just through the roof.

Um plus, since it's all in the same commitment, you don't need to re-express your um message first in your binary domain, and then in your RSA domain. Like, there's no duplication of commitments either. Um Yeah and this plus the concrete performance led us to like okay this is our new road map for client-side proving for our use case. >> This this this will be impossible to beat, at least using the conventional methods that came before.

>> Uh yeah, so I'm I'm trying to kind of understand the the the what's the punchline. Uh so, what what I'm a little confused about it you're saying so you're going to write SHA-256 over Z? Uh so, that seems good for the mod 2 to the 32 stuff, but then, isn't it expensive for the the bit rotations and the bit operations? >> Those are all captured in M. So what M allows you to do we're talking about individual bits here, right? So you have your witness bits.

Any combination of sources of your witness bits, any permutation or source of the witness bits can be expressed through M. The only thing that you cannot express in M is products over the binary field. >> So so you're saying this R1CS it it doesn't capture all of the SHA it just captures the Maybe yeah, maybe I don't understand it. >> the Z times the Z this linear this one linear constraint that you have in in Z is enough to to capture the additions because you just say that well bits of A plus bits of B plus one carry bit

equals their sum, right? >> Yeah, no I'm I'm asking right? So in SHA you have the mod two to the addition mod two to the 32 and you also have a lot of bit ops like rotations bit majorities. >> Yes. >> Are you saying just to see if I'm following this R1CS it only does the additions mod two to the 32 it doesn't do the bit majority and that stuff that somehow in this >> No no not even R1CS you just need the CM relation for that. The CM relation can already tell you that an integer linear combination of combinations of witness bits needs to reflect a mod two sum.

>> Oh I see you're saying the the SHA is captured in this in this second bracket. >> Yeah fully. You you don't need the AP matrices to to arithmetize SHA at all here. They they come in handy when you want to do the ECDSA part. >> You're saying okay for the SHA I can ignore the first bracket I can just look at the second bracket, sort of? >> Yeah. >> Correct. >> That's sufficient for most hash functions. The only thing that is maybe not obvious here is >> It's a bit confu- >> Because we do as easy the ECDSA part. >> Oh, the first bracket is for the ECDSA.

>> Yes. Well, yeah. >> Oh, okay. >> need a non-linear integer constraint for because of the ECDSA. >> This slide's a bit >> The only thing that is maybe not obvious is how you would arithmetize AND operations, but they decompose uh quite naturally into XOR operations and integer linear constraints. >> So so you're saying you're saying this bits is system you can have linear constraints over Z and linear constraints over F2? >> Yes.

>> And the yeah, and without sort of with less or without overhead in this sense. >> Yeah, I think the compared to other imaginable binary constraint systems what we don't have is binary extension field multiplications over your witness. You can't express those. But turns out you kind of don't really need those most of the time. >> So Remco, is it fair to say that this proof system is so incredibly flexible at the arithmetization layer that it it in some sense it's a one-shot thing where if you want to prove isogenies or you know, lattices or RSA or whatever crazy cryptography,

this proof system can just do it all, right? >> In in the sense that it's NP-complete already that the tiny little part can. >> Right. >> The the top part adds a bunch more expressiveness to that. For lattices specifically, Albert has a couple more interesting tricks that make that even more efficient because you can use the lattice ring directly in your arithmetization. So instead of converting your lattice problem to a problem in Z, you can just solve it directly in its natural ring. >> Okay. Can I say something?

Uh so the in this for SHA 256, we are arithmetizing SHA in this bracket. But if you if you want to prove a lot of hashes you and you and you care about the prover speed and not much about proof size, you might want to just arithmetize them over binary field and use Plonk. Because even though with this arithmetization the witness is smaller, the performance um at least for BitZ is is not as good as in Plonk. So, I we have this experiment where we have the if you are only proving SHA and you arithmetize it over this relation

we have this this throughput. The proof size can be reduced a lot. This is rate 1/2 and doesn't doesn't damage BitZ uh, too much. So, but if you want prover speed you you it's probably better to arithmetize SHA over the binary field. With you can also do if you are interested in lots of hashes and then other types of operations, you can arithmetize the hashes over the binary field and the other operations over Z or another another ring, for example, which is what we did in for SHA-256 in this experiment here.

>> Oops. >> Um, have you tried the recursion? >> Uh, we are working on it, yeah. We have we are trying, yeah. Uh, do you want to say something about it? >> Yeah, um, so where Proof Kit is going to apply this is in the circuit compiler. Um, the current version uses Noir as an input language. For this one, we actually use Lean 4 as an input language and and we used some like auto research to optimize the circuits, which is a lot of fun. Turns out there's actually not much to optimize because you just the most natural encoding is actually already close to optimal, at

least for SHA. Um due to the expressiveness of the constraint system, so that was a nice result. Um but uh in in in a for recursion, the way we want to do that is by just implementing the recursive verifier in a natural way in in say Lean 4 and run that through the same compiler pipeline. >> Thank you. >> [clears throat] >> Cool. Albert, you have uh 5 more minutes and then we'll take a quick break and then after that we'll the group will split into two parts. So, we're going to have the the privacy workshop with Post-Quantum Techion starting. Ulrich will be moderating

this. And then we're going to also going to have ThreeNouns present Magneto, which I believe is a uh you know, it's a similar kind of breakthrough. Go ahead. >> Okay. So, just one last uh just let me discuss I'll just mention our work in progress on on lattice-based type computation, tying it with what I mentioned about uh So, as I mentioned, the BZ is essentially the cost is essentially the cost is related only to the amount of bits in your witness. It works on over any ring finally generated. So, we are also working on proving Falcon

signature. This is work in progress, but we have these preliminary numbers. So, if if you want to prove a we can prove a a thousand Falcon 512 signatures without hashes in 100 milliseconds. And if we put the hashes and hash to point and etc., we we get to half a second. And the reason is that the cost is essentially the same as proving integer multiplication for the same witness size. >> And then this is using um the arithmetizations from the sync plus paper, right? Like once you get to the fingerprinting step, a lot of this is >> Yes.

>> reusable. >> Which hash function? >> Um SHA-256. Okay, and that's it. >> [applause] >> Yeah. Um yeah, thanks for the presentation. Uh one question, a lot of the benchmarks were done on a MacBook M5, I believe. Is this the hardware that you care about?

>> Yeah, no. Um for Proof Gadget our our first benchmark target was a um a Raspberry Pi. Um and our our lowest-tier hardware is a 32-bit Android phone running it in WASM in the browser. That's literally what we're trying to support with this. Um I think the the biggest delta is that from the beginning we focused on very tiny devices and not on GPU clusters. That being said, uh I think all of this will naturally extend to any kind of hardware and give similar performance improvements. >> Right. Uh could you say more about sort of the peak memory uh consumption here?

>> I Where are we with that, Albert? I think I >> Peak peak memory is quite small. There's numbers in in the paper and we can also discuss them We can also show you now after the the talk. >> Okay, thanks. >> But the generally requirement there is to to keep it under a gigabyte because that's when mobile phones start like losing like killing your processes. >> Any final questions?

If not, thank you so much and we're going to have a 5-minute break. Thanks again. >> [applause]