zkStudyClub: How to Minimize Foreign Arithmetic in ZKP Circuits (Michele Orrù: French CNRS)

Transcript

Hello everyone. Welcome back to ZK Study Club. Really excited to have everyone here for another edition. Today we're very excited to welcome Michaela Uru um who's going to be talking today about um techniques to minimize foreign or non-native arithmetic in ZK Snark because I think he'll be introducing a couple of his co-authors. Michaela, thank you for being here. Um really appreciate it. The mic is yours. Hi. Hello everyone. Um hope you can hear me properly. Um this is joint work with um uh George Kadinakis who is just next to me and will assist me in any question you might have and um Mary Mer and uh Greg Zavucha who is at Microsoft research and um um he's a bit more

senior than this community. he invented the KZG commitment scheme for instance which everybody I think here knows about and um yeah I think uh in this paper a lot of other people participated like Melissa Chase like Trevor like Andrea and but um yeah so I'll be like it seems that this paper has a bunch of different applications and hopefully I'll try to cover at least uh some of them during this talk in a way that is uh clear to everyone and um yeah as it was said um the this paper which is um 2024 slash 265 and um yeah um this paper is essentially um a combination of three different

tricks. Um the first one is about um proving um that two commitments are to the same values across uh different fields. So imagine and this was our use case at the beginning. Imagine that you have um a credential or a pedig commitment over curve 519 and then at some point you're like oh no now I want to migrate all these commitments to BLS 12381 how can I do it and so this is a very efficient proof to prove that you have a commitment to the same value um and it can be easily generalized also to um you know longer commitments or um um or other um other different values.

Um then um we proved that this can be done with a simple sharp proof. Um and there was some previous attempts before some of them from Melissa Chase some others from Wen. Um but the first one was using more garbo secrets technique and the other one was using fry proofs which are sort of a bit more cumbersome and heavy. Here we'll just do it with a single sigma protocol using a technique called rejection sampling. Um the second contribution of this paper um is also something that comes pretty often and it's this sort of mix of algebraic and non-algebraic statements where you want to prove that you know a secret key associated to a public key and then you want sometimes to prove that for

instance the secret key is in a miracle tree and and so here you have got these um um let me see if I can have a laser in here um well I don't know really know how to do it. But um but yeah, so the idea is that you want to um we give you a way of mixing this algebraic statement with this um more symmetric statement. And the way to do it is that we defer um the we we we have a single big snark proof for hash images which we know how to do it and we already have gadgets for it and instead of having in the same circuit also the proof of the scal multiplication which seems to be very heavy and cumbersome in modern knacks

this we defer to a different proofs and the trade-off here is that we need to add another um hash pre-image proof in this um in this protocol and the third and last one is that um often times we also want to mix secret key operations so differently from before it's not public key operation it's more like secret key operations like AAS and commitments so we have say a Person commitment to a value and then we want to prove that this message that I committed to as Pederson is also um encrypted as an AS cipher text and the cool thing that we get with this is for instance um verifiable encryption that is made very easy because then you end up only proving things about the Person commitment rather than the cipher text of as itself and this is also compatible

with other generic uh um snark techniques that we know of. Okay, so this is sort of the initial framework um and um all these protocols are very easy. Oh, there let's go. Um oh yeah, if there's a question um we should just remember to read it out for the uh the listeners on YouTube, right? So the question is what if X is larger than one of them modul? Yes, we will cover this case and rejection sampler really tries to deal with this.

I will go over it in a sec. Um all of this is done using very simple snorroof. Surprisingly also um this AES proof despite obviously you can do it also with compressed sigma protocols or more involved techniques. The way that we present it initially in the paper because we want to have something really really simple is uh is just using shore proofs which is sort of ironic but um we will see then how it plays out. Um so in terms of notation for the rest of this uh study club um I will uh um talk mostly about three message protocols. Um I'm going to define the first message as commitment called K, second as challenge and the third one as response R. And um yeah in um in a classic schnore proof

the way that this is done um the scenario is that I want to prove to you that I know a secret key associated to a public key. So what do I do? I select a random element that is going to be useful for zero knowledge later. I commit to it namely I create an ephemeral key. I get a random challenge and then I compute the response as the line that goes through K and X where X is my secret. We know that these protocols have at least two very important property. One of them is um special soundness um which essentially says that um this is a this is uh morally speaking is a zero knowledge proof and and satisfies very strong soundness properties and the

soundness is defined um roughly speaking as if I have um if the proof is is a is a really a good proof then it should be able to reply to um many different challenges with valid responses and in fact if I have two protocols that have the same uh commitment but different challenges and responses. It is trivial to recover X from it and this can be proven then using rewinding techniques or in the algebraic model using straight line extractor but that's um that's another story. Um so this protocol I just want to convince you it's sound and this is some sort of a like 101 lecture about schnore that will be useful for how we frame the the rest of the talk later. It is also zero knowledge.

Namely, we do not reveal any information about little X in this protocol. And the reason for it is that it is always possible to create a transcript that um is done by a simulator that does not know anything about um about X itself. And the way to do so is to sample the response and the challenge and then recomputee the commitment from it in such a way that it satisfies the verification equation. This is sort of all known. I'm just trying to set up the notation and get um as the grips of it together. Um so this is our starting point and from here I want to start with the first of our targets which was the ZKDQ and um and again here the scenario I'm I'm slightly simplifying it. So I

just want to prove to you um that I have two values of which I know the discrete log across two different groups and that um their discrete log is the same. Um this the scenario here in my case at least was um that was this infrastructure change and then you wanted to change the the public keys from one um one secret uh to from one group to another and um and we wanted to prove for instance that X was the same 128 bit value. So in order to simplify even more the problem I'm going to assume that X is um a somewhat small secret. If X is not mold, there are generic techniques by which I can sort of split the commitment in two and then

um prove run this protocol twice for each of the two parts of the commitment. Um but for now, let's just keep it easy and simple. Um I have two public keys in two different groups and I want to prove that they are um have the same secret. And so the protocol is going to go roughly as follows. I have again my commitment. I have again my challenge and I have again my response and um I'm going to send a commitment BK that is again little K times the element over P and the element over Q.

So I'm again sending an ephemeral key over the two groups and normally what I would do is that I you know hash K in here which is again the two elements and then in a normal proof I would also send you the response as this one and then I would check that it satisfies the verification equation. The idea for this protocol, the idea is that if X is small, if X is small and C and K are also small, then think about this over the integers, R will be also small. So there is a um so

if r is small then um and c is small then k and x are small. So coming back to the question the idea is that if we have a way of um assuming that um if we know that over p for instance x is already small then if we think about the argument only over the integers we can perhaps hope to show that um x is not wrapping up in the second group if p is less than q and the way to do this is um something called

rejection sampling. which was a technique that was introduced by Lasheski in 2008 in 2009 and then done by other people in the same ENS lab in Paris and um roughly speaking this technique is is um thinking about the following um it's used a lot in latisbased techniques by the way and the idea is again that if I choose the challenge to be small enough and k to be also small enough then I have some hope of making sure over the integers that x is also small however I must make sure also that k is

still hiding x so there is really a small window of um of bits where um k is still hiding x um not revealing information and we're still able to prove that x is um is within a window where it does not wrap up modulo P or modulo Q and um um let me down. So we have essentially these parameters to deal with. We have the number of bits of X.

We have the number of bits of the challenge and we have the number of bits if the protocol um um of of like margin where we can expect the protocol to to stay within a random distribution um which I'm going to call it the failure probability this part over here. And so um the way that we do this is that we take instead of just taking a random C in the field, we just take a C

that is small between zero and Q to the C. So that we are taking a challenge that is potentially smaller. And obviously this will affect soundness. In particular, soundness will have an error that depends on to the C. K. Instead of sampling it uniformly random, we will sample it from um zero from true to the X the number of bits of X plus the bits of U the challenge oops bit of the challenge plus the bit of failure probability.

So let me show you what's happening here. um if let's let's think about this operation again for computing the response over the integers and um and try to compute the bits. So if C has number of bits B of C and X has number of bits B of X then this multiplication will give us at most BC plus B X bits and then we have B of K A then we have K which has number of bits B of C plus B of X plus B of F and as you can see B of F is really um sort of an extra mask that allows us to have zero knowledge because we there in the paper we will

show with a lema that is really inherited by these previous works that these extra bits that I'm putting really mask completely x and um and whenever I add them then r will have roughly speaking bc plus bx plus bf bits um plus one and um I at this point I will play with these parameters um a little bit in order for r to be still smaller than the size of p and the size of So rolling back rough idea of how does the this DQ DQ works is that we have two public keys across two different groups.

uh we want to prove that um they are pro they are for the same x this x is small and um the way that it works is that I will um compute challenges and commitments in a short proof um in such a way that the response will not wrap around. Now for making even the proof simplers in in in general like in our in our protocol we also give a arrange proof for x in one of the two fields. So we still need to prove that X is small but depending on the use case for instance in our case one of the true public key is already is issued by a trusted third party. So we don't really need to prove anything about it. Um but in a in a generic context if we assume that X is more over one group using this

rejection sampling technique we're able to show it that is the same value as in another field and um the value does not wrap up and it's really the same secret key that's used across the two groups. Okay, if this is okay, I will go to the second question contribution. But I'm also happy if there is any question over here to take it.

Okay, let's go ahead. Um, sigma bus. The idea here is that I have now instead a public key and a hash function of the same uh on the same secret key. And I want to prove that it's uh that I'm using the same value for both. Um, the way that I do this is again I have a commitment, I have a challenge, and I have a response. And I'm just writing here how I would do a normal snorke.

Now what I would do is I would verify that this satisfies the verification equation and I'm still left with proving like this is the sort of the starting point the I still have to prove that also h of x is equal to the hash of x. Uh the idea here is that if the commitment in addition to the normal commitment I also send a hash of it still compute the challenge as before and then I send back the response. I can instead of proving everything into a single proof, I can just send um a snark proof for instance of knowledge of K and X

such that the hash of X is equal to H of X. The hash of K is equal to the hash of K. And then test this last linear relation in the group in in the field. So I have k + cx is equal to r. What is happening here? Here what I what what I'm doing is I'm having a short proof that is made outside of the snark circuit. If I'm thinking about programming this in a in a sort of a programming in in a language that has gadgets for rash functions and then I in a separate zero knowledge proof I will prove the relation only over the fields which I know how to do efficiently with

arithmetic circuits and then that I know the true harsh pre-images of the commitment and of the secret key. Again the cool thing here is that then I do not have to write in the circuit how to do the public key operation. Now I mean if I have to think about why this protocol is secure is that soundness will depend on collision resistance of the hash function and on discrete log assumptions. For the zero knowledge part I have to introduce a new joint assumption zero knowledge.

I have to add a joint assumption in here that says that the public key and the hash of x are really indistinguishable from the public key and the hash over a random element. Um in a way I need to prove that the the hash is not really based on discrete log assumptions but morally this we can assume that it works for any reasonable choice of ash function and and groups. Um so um yeah like from from here like there are really easy extensions that are possible because I'm using such an easy

framework. I can for instance just just instead of considering a single element I can think of like um commitments. I can think of proving multiple keys and the complexity of the proof will scale linearly with the size of the response. Here for instance I would dash an entire vector. Here I would ash an entire string of elements and then I would compute the response as a vector. The all these protocols are linear so they are really prone to be easily extended for many keys and many signatures. Why is this nice? Because then if I have um like if I have to think about how

much does it cost to prove this uh uh operation uh this public operation inside a circuit then we will where we'll be talking about at least thousands of constraints whereas if I have to think about ash functions like proidon we will stay more within the within the range of hundreds of constraints though so in fact like what we show in the paper is that we have at least a 100 factor improvement over normal R1CS constraints. that you might put on over these u over these protocols. Okay. So from here

the last contribution that I wanted to talk to you about is um tiny bear. Uh that's a code name. Um and it's about um proving symmetric encryption. Again, what we're trying to prove here is that I have a message and a key and given um and I want to prove that the message in the key are what is used to as encrypt a cipher text given the message committed as M and K committed as BK. Um I'm assuming that these are fed commitments for the rest of the of this part. And um there's been actually part of the work about these um in lasso and in Ulvetana about also how to prove similar

relations and most of the ideas that are in here are also used in these papers um and they were already sort of known even before I think in Zcash who had already to develop a circuits for doing sponge functions and use already some of these tricks. Um in order to look at this I will have to tell you a little bit more about AS. So AS is a symmetric encryption cipher that works over elements over byes and in particular we will study the field galva field of 256 elements. So is a encryption over

eight elements and the block size is 16 bytes. So we will have a state of 16 of these guys over here. And as is composed of two big parts, the key schedule and the cipher. For simplicity, I'm going to exclude the key schedule from this analysis, but just think of it as operations that are already contained inside of the cipher. The cipher acts in a number of rounds which are I think between um 11 for as um 10 for as 128 um and then 14 for as 256.

Um and each of these rounds is composed of some sub operations. The sub operations that we have are shift rows which is reordering the elements in the state. So we will have a state that is um generally represented as a matrix 4x4 and shift rows is just reordering the elements in this matrix. um subbox no um well I mean the SBOX operation um that is very similar to the inverse in this particular field um but it is generally implemented as a lookup table um and then we have the mix columns

operations which is doing a linear operation over the elements in uh in the state and then finally a round key that adds the round key that was generated via the key schedule. If we look at what internally these operations are doing, um this is just reordering the state. So it's not really performing any operation over the single elements. Um the sbox operation is really just looking up in a table. Then I'm just going to call it for simplicity sbox. um mixed columns is going to do a linear operation and this linear operation can be expressed as a sequence of sort operations more precisely I think five of them and um an operation I'm going to

call gal 2 that is essentially multiplication by the primitive element in this field so um the matrix for mix column is of the form 0 1 2 3 that multiplies the state and what I mean here by two is the element in the field that can be expressed as alpha + one for instance And um Galu is really multiplying by this alpha. This is to be a bit more technical. And um so it's really treating you can it's really treating things as field elements.

Exactly. Not just as as as eight bits uh but really as like Yeah. Yeah. For now we're thinking of them as as field elements. Yeah. And finally a key is just doing the sore operation with the state key. So in sums all as can be expressed as three different functions function this multiplication by the primitive field element and the sbox function and uh sbox again goes by elements over here and then maps them to um you know the sbox of x also here we are just mapping x to alpha * Yes. And then where is

taking two of them and then mapping them as XY mapped into X sore with Y. Okay. And so very roughly speaking the way that we're going to implement this protocol is just by using one big lookup protocol for these three functions and then prove that all the operations are to prove that all these operations are done correctly. Um coming back to the question, we don't really encode the ele I mean at the end of the day we're really just encoding the elements as numbers modulo p and and we're checking that all these functions are being done properly via a look at big lookup proto.

Um looking ahead the way that we prove this is going to give us proofs that at least on this MacBook which is an M1 Pro runs in around 30 milliseconds. So it's going to be something very fast and I think actually there could be even further improvements that can be done that maybe I will leave space more for it at the end of the talk. So um how do we look up given these functions how do we transform these things into a lookup table? Well, this is essentially sword zippo and uh I mean very roughly speaking um the way that I check if a function is equal to y

is with very high probability. I just give you a challenge and then I check that x + c * y is inside the set of x + c * um f of x for each of the x in the domain. So what we note is that in here we have the sbox which is how many elements are there in the domain 256. How many elements there are in galva 2 256 and here we have roughly 16k elements. What we note also is that theor has a particular structure by which by which because we're acting at the bit level um it doesn't really um we don't really

have to encode this big table. we can actually encode for instance at two tables or deduct on four bits and then also have this table to be only 256 elements. So roughly speaking how does the protocol work? Um the protocol works that the prover will send a commitment to the witness. What is the witness? All the intermediate states of the as computation as I described it here. The verifier will send a few challenges. one for the sbox, one for the um galvan multiplication and one for the sort table. And then we will be checking instead of checking the function

evaluation we will be checking that all these elements are in the possible function evaluations that we wanted to have before and um the table where we want to look all these elements is as small as 256 * 3 which I think is in the range of 700 elements. So the table is going to be really small. We have a bunch of elements to test. The elements that we want to check membership for are all the intermediate computations and those are more in the order of between a thousand elements and um when you start looking at this number because you have only 700 elements to look into it. You don't

really need um the table the table is really small. So you can also assume that the verifier can be linear time. And in fact, this is what we do in our proof to really squeeze as much um optimizations out of the um of the prover and um and have a really nice performances. So the lookup protocol that we are going to use to prove this part is um I mean this has been uh already widely used and it's the the lookup from habok but it was already pro present in bulletproof plus from Liam and others and um the

idea is that to prove that um some elements are contained in a larger um I can just prove that there exists a vector m that I'm going to call the multiplicity vector such that the sum of the inverse polomial that has fi is equal to the sum of m i's x - t time.

So the proof intuition for this um so this is already previous work. Um I think like in in what we do in our work is really that we assume that the table is easy to compute. So we play a little bit more with this uh with this idea. But internally what we are what already was remarked by Uric was that um if um f is really entirely contained in t then there must exist a vector m um such that the polomial that has as roots all the elements of fi in the in the initial vector f is equal to the

polomial that has as roots all the elements of ti times some multiplicity I. So if you think about it, no because all the elements are internally maybe some vectors of the multiplicity are zero. So maybe repeated many times. In this case, I will just increment m and um and uh this is really a way uh by checking the roots that the order where the order is not really relevant. And um this is like a technique that was always used in uh uh in proof in uh in like more in analysis classes. But the idea is that you if you apply the log over the two sides of the equation, then you end up with a sum over the log of x - f_i and the sum of mi * the log of x -

i. And um if you think now about the derivative of this, so I'm really like using L's notation. I don't I'm not even saying where these elements are anymore. But if you apply the derivative to this, you end up really with a with a final statement of x - fi and the sum over i of m i and x - ti on the other side. Um and so rolling back we need to prove as we saw that AES is a composition of different functions. We saw that these functions can be um evaluations correct evaluation of these functions can be done with uh what I'm going to call a lookup

protocol. So checking that a lot of elements are in the same table and um that this relation can be reduced to this other relation over here proving existence of another vector for which this relation is satisfied. So how does the protocol for proving AES work? Um now that we have all these little ingredients well the protocol works that the prover will send a commitment to all the intermediate computation of AES. We will get the challenge for checking the valuation of all these functions and then we will run at this point the

lookup protocol to check that all the elements are done correctly. How do I do this? Um well I will send a commitment to the all the inverses that I'm going to call Q. So Q is the vector that is 1 / fi well um I mean this is for all of the elements so it's going to be for the sbox for kalwa and for over i and um I'm going also to set the commitment to them multiplicities and then the claim the valuation y and at point I just have inner products to

prove. I have to prove that Q admiral product with F is equal to 1. Why? Because I want to prove that the inverse is computed correctly. I want to prove that f inner product with one is equal to y and that this is the same as um the message together the multiplicities together with the table. Okay. So roughly speaking in the as proof we have

one commitment of very small group elements a bunch of challenges that are being sent some commitments where again m is really small and um because it's just a vector of multiplicity and the vector of inverse that is being sent and given all of these elements we need to fe to do a bunch of link linear proofs um um one like one over here which is just what I'm going to call a linear evaluation because the vector of all ones is public and can be computed by the verifier.

One proof over here where the table is also public because it can be evaluated by the verifier. We saw earlier that is very small and we're just left with this proof for which there are techniques that just reduce it to the um to an inner product proof. So we have the way to do this in general is that you have Q and you do the inner product with a vector of random elements and f this is called twisted scalar product and you want to prove that this is the sum of the powers of R I and this can be computed in logarithmic time because it's a geometric series.

So really all this big AES proof becomes essentially a bunch of linear evaluations which are really easy to do and an inner product proof. This inner product proof using something called samche that I'm sure has been explained in here uh quite a bunch of times can be reduced to true linear evaluation proofs and that's what we do in order to avoid costly inner product proofs. Um and so it's going to be a linear evaluation over a tensor product over here. I can I can go into more details of why this is the case if needed.

And um and this is going to be the reduced y and these um sub claims are also linear evaluations. So all in all we will have few commitments being sent um a sum check to reduce the inner product to two linear evaluations and then four linear evaluations to prove together. Now these linear evaluations are all over different element. So yeah, I mean and and this we know how to do we this we could do it with compare sigma protocols which are very efficient give us like log space

um or we can do it even with sigma protocols but with the sigma protocols we end up with proofs that are in the order of 80 kilobytes. This is the gist of it and I just wanted to like maybe conclude this part by saying like what were the optimizations that were used internally to make things a little bit faster and to achieve these good performances. And I guess the first one is that we have many linear evaluations. So we have um a linear evaluation over Q, we have a linear evaluation over F and a linear evaluation over M. And all these different vectors um have different points where we want to evaluate all of them. And it is difficult to batch

linear evaluations that are or even multivaried evaluations that are over different points. And the way to do so that that we're able to batch all of them together is by introducing another round of sum check that takes um this evaluation over I'm going to call it evaluation point one, evaluation point 2, and evaluation point 3. And these are all reduced to the same evaluation point. I'm going to call it evaluation subject vector. Let's call it that. And because these are all evaluation

across the same point, I can just take a random linear combination of them and just um send a single proof and um I think this is what really lower the cryptography cryptographic operation that were really the bottleneck in our case and also avoids us sending three different proofs which also increased the proof size. So I think one of the things that has been also said in a in a lot of other places is that some check can for us it was really a way of reducing the number of public key operations because and and increase um a lot also and increased a lot of the speed because it's only dealing with field operations and we didn't have to deal anymore with uh um with public keys column multiplication and multiolor

multiplication um added complexities. Um the second thing that I think was uh um was maybe really helpful in our case is that um there is this vector f but they didn't really say well how it was computed the vector f um is um if you we start from the witness the witness vector I said was all the state of the intermediate computation so it was maybe the state zero the first element the state zero as the first element and so on and so forth and then um where these elements over here are the initial a state matrix.

So I have s 000 in here, s01 and so on and so forth. And then um I'm concatenating with the state at the first after the first operation is being computed let's say the sbox computation and so on and so forth and this is the state is the m the as matrix as at the first state. So, S10, S11 and so on and so forth. And um what I want to check is that um how do I go from the state of the witness to the um to the vector that I want to look up? Well, this is a linear operation, right? Because I have

to take this element and then take C of Sbox times this other guy. So f can be seen as a matrix times vector operation where the matrix a is really selecting the the the points of w that I want to check. For instance, it will be in this case it will be one then zero 15 times and then c of s box and then zero again and so on and so forth. And um when I multiply with w over here I will end up really with the vector f that I want. So s 0 0 plus c of sbox time s 1 0 again so on and so forth. And

what we notice that instead of um because I need to at some point compute this linear evaluation over f. The way to do it is that I notice instead of um I notice that a w and e of some check I can instead of having an additional commitment to f I can save on it again exploiting the fact that the verifier is linear by just multiplying by a on the other side. So what we have is a um we will have the prover just send a commitment to the all the intermediate state never send a commitment to f and then the verifier on the other side will take care of doing

all the operations in order to rearrange the challenge in such a way that this linear evaluation will be equal to the desired evaluation on f. This also allows us to really never pay for um shift rows which I skipped before because it's only rearranging the elements of the state and we can just similarly as I showed here for the SBOX rearrange also the elements for computing the shift rows operation over the changed state. Um I don't know what were the other optimizations that we did. Um the sorry the last one yeah the last one was and that maybe I mentioned the the it also

briefly at the beginning is that if you really look at the exor operation it can be considered over um smaller sizes of a table and so that m means that we have to commit the vector w not as vectors of bytes but as vectors of four bits and so what we end up having is that we have um a witness that is twice as big. it ends up being roughly the size of 2,000 elements that we have to look up in a table of 700 elements again and the the matrix also similarly has to be changed a little bit because now we have only the first four bits of the state and then here we have maybe the second part of the state. So we will have more a matrix that has the form zero 2 to the^

of four so that we can squash together the first elements then all zeros again then the sbox um challenge and then for instance true to the fourth time the challenge for the sbox again and then again when you multiply you end up with the the right element that you want to look Yeah. So wrapping up what did we do? Um let me go back to what were the contributions.

So the idea like again that sort of motivated this work was that we saw a lot of places where you had different fields where you had foreign arithmetic that had to be put in zero knowledge proofs and we showed a bunch of different techniques in which um these zero knowledge proofs can be made more efficient by just removing this foreign arithmetic from the field and using other tricks for playing with it. The first one was using rejection sampling and I think um this technique is used a lot in latises because there you need to prove that a vector s is small and I think it can also be used to make really efficient arguments in the discrete log setting and maybe we sort of forgot

about it in the community but where one example where I think was really useful and allowed us to save a lot of uh computation over I don't know generic proof systems like fry etc um is um is to use it for proving that two commitments are to the same value. The second techniques that I thought was uh that that we think is sort of nice and can be used also elsewhere is that in order it is possible to trade off one scalar multiplication with a new hash evaluation and the way to do it is to put a not proof for X and then you have one additional commitment to um to prove the hash image of. So again also in here you remove um proving the elliptic curve

formula from the circuit and instead you just prove hash per images. And the third way in which uh all these uh foreign arithmetic can be removed and this was sort of widely known already in the community I think was is by using Luca protocols. And with LUA protocols again you can check a correct function evaluations and especially if these functions are boolean it is really easy to play with them and even to split um the complexity of the table into smaller tables that then can of which then later you can prove um membership of.

So yeah this was roughly it. I am happy to take any question and uh also to go more into the the detail of uh any nitty-gritty tricks that were used internally to make things even more efficient. Thanks for that. Yeah, just opening the floor to anyone else who might have some questions. Oh, I think Victor, I think feel free to jump up. Yeah.

Yeah. This this is this is really helpful. I'm looking forward to like diving into these in great detail and like there's a lot to learn here. Um just like a full great tricks. But one thing I was wondering about with the linear time verifier, it's a like basically offloading operations to the verifier is a really useful trick. I guess one things I'm one of the context I'm thinking about though is like when you want to integrate this proof into larger proofs, especially when you want to start doing recursive compression of proofs, I guess basically then the verifier becomes another circuit. And basically I'm curious about how to manage that. Basically if you're if if you're throwing your finite field over operations out to the verifier but the verifier is also a circuit then it's like you might end up back in the same situation again. Does that make sense?

Yeah, makes sense and it's a it's a really nice question. Thank you. I think um in here the idea would be that um I haven't really thought about the recursive setting also because um even if you read the paper we're really using like a legacy technology and I think part of the reason was that uh um when I was initially thinking about it was was with Trevor and and Trevor sort of was very familiar with snorofs and I was trying to keep everything to that simp level of simplicity. So without throwing in any sort of recursive snark or any fancy uh construction but I think also the idea here is that um we try to bring uh to have a little gadget that sort of maps as to a person commitment and so I think the idea here is that then um you

can prove separately whatever you want about the as proof uh about whatever it's in about the as encryption by just proving things over the patterns and commitment and it's really easy to rerandom my Person commitment, you just add a new planning factor to it. And so I think the idea is that um maybe whenever you approve many things about them, you end up only having to prove things about M and K as Person commitment and you sort of keep the same sort of a proof separate, the same proof gadget for the sephertex outside. I don't know if that is satisfying or if you think like it would really be needed also to reprove everything because you want to make it unlinkable or if having a separate proof you know for proving

properties about M and pictures of the cipher text would be um sufficient. Yeah know it's I think there's a lot to a lot to think about here and I think that the focus on using like much simpler primitives is really valuable. Um yeah, I'll be thinking about this some more and I think like that what what was sort of seen with the with the with Tana Fox is that again like trying to also bridge with the rest of the research is that exor operation you don't and all the linear operations you don't really need to do them if uh um if you're working over a binary field which is a a really

nice result because then you can just remove all of these tables and you are just left with the SBOX operation which by the way I think sort of sorry like trying to bridge also with with other research fields in in the MPC in the in the head community the Sbox operation can also be done with a polomial of degree 7. So I wonder also more in general if there are tricks from the MPC in the head community which has really been optimizing as for for their purposes if there are tricks that we can also inherit in our community. But this is more of an open question and a longterm thing.

Great. Anyone else have something to share? Seems like people got what they came for. Very cool. All right, thanks so much for uh this presentation. Uh yeah, and thanks to everyone who came through. Cheers. Thank you. Bye. Bye. Bye.