One-Shot Native Proofs of Non-Native Operations in IVC - Patrick Towa

Learn & Share with PSE · 4 Feb 2025 · 1:22:07

A research presentation on One-Shot Native Proofs of Non-Native Operations in IVC. The session explains the construction, its security or performance properties, and where it fits within modern privacy and proof-system research.

Speakers

Topics

From Learn & Share with PSE, hosted by Privacy Stewards of Ethereum.

Transcript

so we are here with uh tohu and also with Patrick uh they were with us already uh like a year ago or something like that and they already presented uh zomorph to us now they are coming to do another learn and share session and this time on their latest work on uh IBC uh related uh stuff in particular here proving non-native operations uh taking profit of IBC uh as always thank you very much for um agreeing to come here and and and take some of your time to to present all of this work to us and the floor is yours so whenever you want Patrick thank you for for the

introduction so um so this work is with uh with the team at Aztec in general and also T who worked on it while he was still at Aztec and um also Liam Ean who has been you know discussing with us uh these issues quite a lot so it is about proving non-native operations in IBC um natively and in one go at the end of the computation and we're going to see what all those words mean uh throughout the the talk so first the context of the work is is incrementally verifiable computation so in this context there is one

computation here is denoted F that is is applied repeatedly throughout the time so start with some input x0 and then you have like some um some nonuniform advice W in general and you can comp can continue the computation like this and um this occurs for instance when you're trying to build for people who in the audience probably familiar with this like a VM so you probably have like some fixed instruction set and uh throughout your comput you want to break your your computation in small pieces and you only want to like execute a certain number of uh CPU Cycles at each time and then you know this is how you proceed to our

computation to time and importantly you want to be able to prove at each step that what you have execute is thus far is actually correct so want to say okay given x0 and some output XI you know I want to produce a proof pii such that proves that basically a new intermediate uh witnesses that led from x0 to XI and importantly one can then take uh just XI and the proof that is correct and do one more step of the computation without knowing all the intermediate computation output and Witnesses so if you look at one precise tab you know so

uh you start there should be an XI here so you start with XI and you want to do one step of the computation so I'm just zooming in into step I here and you also have like your proof Pi like I just said and um because you also need to know whenever your Computing improves you need to know the starting point of your computation you also have like a wire for for x0 and then you feed all of this into approver uh at step I and then you produce your proof that the next output x i + one is correct so this is what is happening here and um so to look a bit more at the syntax of of IBC so just

basically just writing in math what is already depicted on the diagram so the prover gets like at the starting point of the computation and some claim output and also then CLA also get as known as advice XI pi and wi basically from which you can compute the proof the next proof and really you know when valali on 2008 introduced IBC the idea was computation can run for an Astron astronomically long amount of time and uh you know at some point you only need to know the last output and prove is correct to continue and it doesn't even need to be the same party that continue the computation but now today we have those applications and uh for instance it's

also what would use at Aztec for instance to prove that we have correctly executed a function privately so for those who know a bit about us you know we're trying to have like this programmable smart function where you have like some private State and know you can also prove that know new state is results from the computation of some the execution of some function that is in some set of allowed functions so what I just describes in this stack proof paper that came out maybe around a month before this one and um given you know the computation output and proove the there's a verifier that can check if that is correct or not so um to go so I've just given the context so far and now we need to see

okay what is exactly a problem but I cannot explain what a problem is that we're trying to solve before I show you how these IVC uh schemes are usually built and um I forgot to mention at the beginning if there's any question please feel free to ask throughout the the talk so a first construction of IBC is from Universal snark so you basically have a snark where you know you you can pick whichever circuit that you like and uh you can prove the satisfiability of that circuit using that snark and there's a very neat and simple idea to build IBC from it is to say you know I the prover knows XI so and wi so the prover just says well if I

start from XI and have advised wi then I do result in XI + one and also simply prove that the IVC approver for the previous step would accept the previous proof that I know which is a secret so XI wi and Pi are private inputs and uh yeah my claim is just I've done one IVC step correctly and I proved that the previous output would have been accepted by the IVC verifier of the previous step and I do this using the universal snark so the circuit to which I'm applying this Nar is you know that it depends on the step which you

are and um that's very simple idea and that works except that is not super efficient in practice and one reason is that the if you look at the efficient snarks today like I don't know if you think of uh plon um hyper plon all these they somehow eventually run like a kzg verifier or you can even use transparent schemes and everything so at some point you end up having to deal with some multiscale multiplications and especially some pairings so and then constraining those pairings is very expensive so later there was another idea that

came out um so there are ways which we going to talk about to sort of mitigate this issue when it comes to multiscale modifications but paing is a bit more annoying but you know to avoid pairings all together you can think of using you know folding schemes and what are folding schemes um so let's say you start with some NP relation so meaning that you know you have some relation that sort of captures all you know efficient computation that you may want to do in practice and and you want to like for instance let's say the satisfiability of a circuit dtic circuit and and you want to basically divide a two-party scheme

where you know you have some prover and some verifier and they interact and the goal is to reduce the proving the satisfiability of two instances to just one so at the end of the interaction you know the verifier just gets like a um just only one instance and the Prov has a witness for this one instance if indeed the first two witnesses for each of the circuits is given of each of the instances that is given are indeed valid so essentially F in cm is just a way to reduce you know checking that one instance into some relation that two instance are in some relation to just

one and this only makes sense if the time to check one instance plus the time of the verifier is smaller than the time it takes to check two instances otherwise it's not really is really useful so but using using these folding schemes now one can build IBC as well and the idea is like origin is I think yeah there's this um paper proof car like proof carrying data without uh sexing arguments and there's also the Nova paper and there somehow the same idea around there so you start with a folding scheme do not need FS here and I should probably say here that the

folding schemes I usually devis are interactive but you use fat me to make them non interactive um to be able then to use them into some IVC constructions these are some implications as to you know what is actually the security of the IVC we get because we're using the the random Oracle that will eventually instantiate in circuit but let's ignore that for for now so you start with some fing scheme fs and um there are going to be two instances for some ration and there's an instance Capital UI which is an accumulator and it basically attest to the correct computations of all the steps before the previous one so you had step I and U Capital UI attests

to the correct computation of all the steps before I minus one and lowercase UI attest to correct computation at step um sorry here it's written I I should be I minus one and they have your corresponding Witnesses those are actually going to be part of the proof the Witnesses are going to be part of the pro P that the Prov gets as a as as a witness uh sorry as a device and from it what one is going to do is to fold the two so basically checking the satisfiability of UI capital and lower case to just one instance Capital UI and this is where folding schems are useful and also there's also one is also going to run

the pr to get a witness for this and now there's a main circuit and what this main circuit is doing is basically checking one step of the IVC computation it is checking that this cap New Capital UI +1 is indeed the folding of both uis so basically we went from you know attesting the correct computation from Step 0 to step IUS one to step 0 to step I and one thing is Al one subtlety is also that um we need to make sure that the output of the first I minor of the first of Step Zero to IUS 2 that output is was what was fed

to step I minus one to change the computation basically and this is what you check in that in that circuit and this is what Nova calls the augmented function so you basically check that the we check all this and the instances are actually instances of that circuit itself so that circuit is checking you know one step of the IVC and then the the instance is getting attached to Prior invocations of that circuit itself this may seem SEC but it's actually not because um The Way Nova is written you can Define that augmented function just in terms of like the sets in which the

UI is in U live belong to and um it's only afterwards that you interpret those uis as as attesting to the correct computations of the IUS one and um then at the end you know you have your circuit and you basically generate an instance for for the circuit at step I and you have witness wi to prove that you have correctly executed the circuit well and uh and wi and you and capital UI plus one makes sure that you know the output at step I is what is was fed afterwards

so this is how the Nova construction works for for IBC and um but now it backs to so now there was something slightly different than what we saw before with snarks is that you weren't directly dealing with a proof because the the the proof here um it consist of two I'm sorry it should be a capital uh I'm sorry no that is correct so the proof here is a pair of instance witness pairs one instance for you know the I step and one instance for all the steps before and witnesses that all these things are correct but what this circuit here was getting was circuit was not

dealing with um the witnesses was is physically folding the instances so this circuit did not consume the entire proof in a sense um whereas before what was saw with with snarks um the snark was the the pro was proving that the verifier of the previous step would accept the previous proof so it's sort of more or less the same idea but not exactly and um the question is then what do they what do these constructions have in common and I don't mean just the twool that I presented now I also mean you know the construction of Stack proofs or these things that are related to memory

checking uh these techniques basically the goal being I want to have a framework into which I can cast all the incremental constructions that we have which is simple and from which I'm then going to do what we do what we're going to talk about is called so I first want to understand okay what is the commanded Eliminator between these constructions so that's what like the first section of the like past the preim the first section of the paper past the preliminary is trying to do and basically um what all those constructions have in common is that they all Define some like core function

or circuit for the IEP and this function has basically two ter inputs so there's the public input which is x i + one and x0 and there is the output at the previous step and then there's the witness to go from the previous step to the to the next output and there is some string row that comes from the proof it's computed from the proof but it's not necessarily the proof itself and so for instance in the case of the of we're going to see what r is for instance and uh the rationale is that if XI with x0 x i plus one with x0 are in

this language then you know so the constructions guarantee that you have done one step of the IVC correctly and it's also very likely that the verifier the previous step would accept so this is what I have in common so for instance in the case of recursive snark uh bootstrapping you know fi is just basically well it's not exactly um VI it's fi a slight mistake here fi is checking one step of the correct computation and then checking that VI of the the verified PR step would accept the proof and row is just the proof itself but as we saw in the case of

foldings it was directly it was slightly different you know Roi was just basically the instances you dealing directly with the with the the witnesses but you also use the check like the proof that you had correctly folded these things together in the uh Sor uh a quick question uh so this is similar to split accumulation right so an accumul so in in my understanding perhaps it's it's incorrect but you you have that accumulation is similar to folding is that

correct is similar I mean it's the same and it's the same yeah I mean uh split accumulation is similar to folding yeah first there was notion of atomic accumulation which is like something like like Halo 2 yeah uh yeah okay but here I'm talking about the construction of the IVC after you already have your your folding SL accumulation okay so you have your accumulator or or you have your your folding scheme and from it you construct an IVC right so it's not you're building one primitive from the

other is that is that okay or does that answer your question uh no but let's continue okay come back to it so here we have the so basically I just exhibited the framework like another framework but basically yeah a framework in which the constructions U like of IBC fall into and uh then um like I mentioned before stack proofs also fall into this sort of idea and memory checking so basically if we start from this framework we can then you know have a technique that applies to the

constructions that we know incremental all the incremental constructions that we know that t eventually fall that fall into this framework so what is the problem U that we're trying to solve so the issue is that Stark and falling verifiers they usually perform you know at least group operations plus other things and usually you have like a you know let's say group that's going to be like a of the points of an elliptic curve defined over some field fq and in this case can be like you can think of bn2 54 something and then this group has like some uh Prime order like

R and you then have a scal of field F being Q which are uh sorry for you then have like a scaler field which is also Prime and in the case of B and 254 you have like a q which is in between R and 2 R anything and since we always then fi constrains the correct execution of a snark or folding verifier to be correct that it means that you're writing a circuit over F FR uh which needs to simulate operations in fq because whenever you're going to add two points or double points you're going to do those operations over fq but you're working over fr so this is

what it's called nonl operations so this is what we're trying to solve basically and there exist Solutions already which leverage what is called Curve Cycles so essentially you're going to work with uh with a curve such that you know if I start with my field sorry with my group that um it's called GQ that was a subset of the points of an elliptic curve defined over fq then I want to know that so so then I I demand that there is I require that there is a elliptic curve that is defined over FR now for which you know I have an order subgroup which is of order

Q the issue um with this is that in the IBC constructions you eventually need to basically all the operations that you don't want to do all the non-av operation that you don't want to do you have to put them in the other curve which means you need to have two folding um sorry two um folding instance pairs so remember before we had like already two instant witness pairs of folding you know one for all the computations up to the previous step and then one for a current step and now you need to have it twice because you need one per curve because you want to delegate all the

operations from which are non native to your native curves basically so which means that eventually you have like two circuits to prove atend at the complete end of the computation there is a paper called tyo that tries to minimize uh this the size of the Circ curve uh complet that try to minimize the size of this second circuit so of the circuit on the second curve so sort of should already you know make the the situation already better but we want to avoid this uh completely soor yeah so this then brings us to Goblin plong what's in the in this work

and um just going to try to explain first the idea and then we're going to see together how the scheme is built so you start with you know the the framework that I exhibited here so you're saying okay there is some function fi uh that I want to check and this is how my IBC construction works and what you do is you basically decompose fi into into two series of operations so some cheap parts like mainly only field operations I'm going to call f0o and some more expensive Parts where you have like all the group operations that uh that um you have to prove and the main idea is to say well

all the expensive operations I'm not going to do them I'm only going to record the input outputs in a table and only prove the the inexpensive part and at the end I'm going to somehow shift all those operations that I didn't want to prove uh that I didn't want to that I didn't want to prove sorry there's a there's a typo here it should be proven n in in fq um I going to shift all the operations I didn't want that I didn't prove so far to D field and I'm going to prove it there the question is how am I going to shift all the operations at the end this is what we're going to

see and one of and one the main challeng is really to prove that throughout the computation your record of operations was consistent that basically you didn't throw away some computations that you were supposed to do and prove at the end um and get away with it as a cheating Pro and you want to prove this consistency but without having to do then expensive operations again while proving this so that's really the main challenge is what really make things really complicated eventually but there is it work it eventually it works and this only makes sense if you know the cost of proven

consistency plus the cost at the end for proving that those non-native operations are correct are strictly smaller than the cost of you know just doing IBC but without any of these ideas like proving things non non natively so this is what we would ideally like to get and um the issue now is that I mean not an issue like from a theoretical standpoint at each step I said you're only going to prove the cheap part and you're only going to you know record the input output of the expensive part and

you're going to continue the operation as if you never um as if you never um sorry you're going to continue the operation using the output that you claim to be correct but you never proved it so it means that now that I give you when I give you an IVC proof Pi I + one you are not completely guarantee that XI + 1 is correct you guarantee that XI + one is correct only if the proof is correct but also the information that is in the record is also correct that the operations that are in the record also correct

so the way to like a way to model this is to say well throughout the computation the proof is going to maintain like some state which is B basically containing uh the the record of operations that went up the record of operations thus far into computation that were not proved yet and the verifier is only going to be given like a short representation of this record so like aary input there going to be a commitment to that and like I said the eventually you know outside of the scheme there needs to be an extra mechanism to make sure that these operations that were recorded

and to and for which the verify is given a commitment that they are correct so IBC really requires normally that you know the the the proof assures that sorry the proof Pi I + one assures that x i plus1 is correct so this is not really an IBC scheme anymore because this is not true there's an extra condition and this extra condition is not checked by the by the algorithms of the scheme it's going to be something that we're going to see later that comes on top of it but it's not part of the scheme so one needs to give a precise meaning to what this means so this is what is introduced in the paper and called like IVC W proof information so

where you have you know your proofs but you also guarantee only correct extraction you grantee correct extraction only if the auxiliary input is valid and by valid I mean that the opening to that commitment is a valid set of operations so this is the just sorry another quick question but this is already a situation with folding that you don't have a proof of uh like like when when you have your set of commitment your extraction is not

guaranteed uh it only happens if the final decider uh accepts it right so this is kind this is kind of similar so this is what I was trying to say before we are going to use a folding scheme to build this scheme it's like you have your folding scheme that is just one building block from which you are going to build the IVC with o improve information no I'm just confused why is it not IVC because like folding is a particular kind of IVC and it has exactly the same problem uh like I'm sorry maybe it's just pedantic but uh in folding your

proof also does not a test that your uh commitments actually correspond to Solutions of the circuit or uh correct execution right they only correspond if they they like if the final decider accepts them so in the similar way you could say that and also your transcript is correct so your decider for transcript is like saying that it's correct consists of correct nonnative operations or whatever uh so I'm just confused why are you not accepting this as an IVC though te technically your transcript is probably limited from above in size but uh but otherwise I don't see why it would not be like

IC okay so if we go back to the definition of folding here um that I used um I mean of course remove the parameters and key generation that's in Nova here if you look at your folding scheme you know there is there is no concept of I've executed this amount of steps there's just I have two two instances and I reduced to one there is no notion of having a computation that you're competing you're just this is just a building block that you're then using to build an IVC so fulling is not by definition well I could say that my

relaxed instance has a transcript of deferred operations and like I mean it looks very similar to like normal definition of folding and since that I could probably Define relations that that would satisfy this up to the fact that your transcript is of limited size but otherwise okay whatever no no so sorry well we can defer that to the end but let's perhaps yeah let's defer this discussion to towards the end what I'm just trying to say is that by definition an IVC well folding scheme and an IVC are two different things and

you use the folding schem to build an IVC and what I'm trying to introduce now is an IVC regardless of however you want to build it whether it's with folding schemes or not you could use actually even snarks again you can put strap sarks again there I want to build an IVC where I just have this relaxation on the noise sence requirement where I don't necessarily want to extract intermediate Witnesses so I think let's perhaps discuss this afterwards but I think that there is a like a confusion between you know how I'm going to use fold to build my IC and actually what an IVC standard Lo is regardless of how you want to build

it but yeah we can we can finish the conversation afterwards um so wait so where was I so here yes so compared to the picture that we had before with um with um the IBC where you know we just had the proofs and and the outputs now I'm just adding two things I'm adding the auxiliary input the aux proof information and also the state to the syntax basically and now the question is how we going to build it so the starting point is to say assume that you had an IVC you know that fell in or an

incremental construction that fell into the framework that I gave before regardless of whether the um regardless of how the the the the IVC was built even though to be fair what I'm going to show now is not blackbox completely because you sort of need to assume certain things about how things work but you're not going to um but basically this is like satisfi all constructions so you know I gave the main idea here what I was saying where I was saying record all the operations you only prove the cheap part and you prove the

consistency of the record without introducing expensive operations so here we can start um so we start again with the uh with an idea so what I'm going to Define I'm going to Define uh like a function like a core function GI the same way before we had fi and what's going to get is like the public part so XI + one and the auxiliary proof information at that point and what is going to get as uh also private uh like as advice is going to be the previous output the string that is computed from the previous proof and the O and the O

information that came from that proof and a witness that uh that the you know xi+1 is really com from XI and what is also going to get are the the expensive operations the record of expensive operations at the current step because you remember I said you only you know you want to record those operations and prove consistency later but basically I want to I want to Define such a COR function and one thing I definitely do not want is that it takes the whole accumulated operations throughout the entire computation otherwise then you know the cost proving this is going to be proportional to that

all accumulator so is going to be proportional to the length of your IC and this I don't want and the first thing we're going to do is just make sure that the output of the cheap part is recorded in the operations at the current step now let's see how we're going to do the rest that I mentioned and uh first we need to say well these operations I'm going to focus then in the case of of where we have like elliptical operations that we have to prove so in F1 how do it look like how can I write them how can I like Express them in a way that I can then check them later and which is AD meable to you know proving you know correct accumulation throughout

time and for this I'm going to define the what you call TIC curve State machine so it's basically just like an abstraction of you know sequential operations elliptic curve operations and in this state machine why is the state basically I have the second component is a bit it's just a bit telling you in the past has there already occurred uh a computation that was incorrect and the the part that is really useful is the first part which is a state and from this state is like you start from some group operation is sorry

you start from some group element and this is basically most of what is is the state in your machine and you also have like the neutral element of your elliptic curve but you also have like two special uh states which are like zero which is like initialization and infinite which is like I turn off my machine basically and the operations that you're allowed to do is to say when I start from a group element I can add another p and then my new state is just G Plus P other thing that I can do I can you know say to the current ele like to the current element I'm at right now which

is G I want to add a p basically and you can imagine that you know if you do like this operation much like add AP many times is the same thing as just saying I'm doing a multisale multiplication and another at some point uh you want to check if you know your you want to check if your computation software is correct so you're going to say where I am is it equal to this claim output so if the claim output in the G where you are you go back to the start of the machine and then you can do some different computation some different series of elliptic curve operation you

know by saying okay I start to zero I I go back to zero is my accumulator like the the neutral element of the group or I can say okay I'm done with my computation and I finish and then just put the infinite input and then the machine is turn off but there's also the case where you know your computation was incorrect or like your claim output you say you ask is is where am equal to some P which is not g and then you know you go back to the start of the to to the initialization step uh state but now you have a bit one which says there was some computation that was incorrect so far and you can in the row below you can

do the exact same thing as above basically so this is basically just a machine that says this is how this is how you sequentially this how like you're going through your computation of uh this is how you're going through your eptic curve computations basically and the way you yes quick quick question sorry um maybe I missed it or misunderstood can you don't support negating a point or it's the same thing you can say time okay okay okay never mind then thank yeah but uh it's great the reason why you're doing like times a is really to support msms because you the idea is to

say you want to do it repeatedly makes sense thank you and this is just an abstraction and then how do you actually in instantiate this abstraction is that let's say the example I'm taking now is what is the pl armatization you know where you have like an execution Trace which is simply just a matrix with the center number of columns and the row is your execution Trace size is the basically size the circuit and in the pl metiz one applies you know um constraints to consecutive rows like one or like one or two consecu like two consecutive rows or just one row basically TR computation so this is how the execution Trace looks like at two consecutive rows basic I just zoomed in

there so uh why did I pick four sir you can pick whichever number you want but the larger the number of columns the more the um the the more the communication size grows and four basically allows you to do for instance just even just Artic Gates where you're saying you know I have my left input my right input and my output and I also have like an extra column where I'm going to put basically the permutation polinomial that permutation polinomial is role is to Simply guarantee the correct wiring of the circuit basically saying that you know the output at gate five is indeed the left input at gate 10 for instance so I just focus on column of

size the table of size four columns and um yeah what I'm going to do uh remember that in the case where we're working over a circuit defining F FR and we may want to do some operations with group elements which are in fq so each element in fq uh sorry a group points in your elliptic curve is going to be a pair of points X Y with X and Y each in fq so I can break X in two parts x0 and X1 and similarly for y and uh also the scalar by which I may want to multiply this point I just

recorded here and remember the scalar is in so I don't need to break it into and the operation here I can just say is just some arbitrary fixed element in INR it can be 0 1 two 3 four they just represent if you're doing you know uh an addition like so so that's where that's how you can basically you know at each step say this is the input to my this is the input to my machine and this is basically yeah basically this is all the inputs to to to to my machine starting from the state where we are and you don't need to to write down you know the

the the bit uh indicating whether all the operations are correct so far because all your operations are correct so far only if you know basically the when you apply your constraints to the entire Matrix your constraints you always end up with zero up to negligible probability so so this basically just gives a structure to the record this is how the record is going to look I see there is a question in the chat it's so I think so we can ignore I think um so basically now now that we have this record we want to prove

consistent C right so during your computation you're going to hold the proof is going to hold the Matrix and the Matrix of the computation up to the private of the operations expensive operations of the P previous steps I'm going to call it A1 the operations at the current step I'm going to call them A2 and the concatenation of the two I'm going to call them a z and basically what the proof is going to what is going to be contained in the auxiliary proof information that they verify will be given are the three commit the commitments to the three and how can one basically prove that you know a z is really the concatenation of A1 and

A2 think of A1 the proof is going to work column by column so you can really think of just a z A1 A2 as just being one column and if you look at basically the polinomial if you look at in the monomial bases you look at the polinomial that represent in the mon monomial basis you know it's really the correct conation if this polom equation is true the thing is you need to know what the length of A1 is but remember A1 is the whole accumulator of all the operations thus far and you don't want to give A1 as input because then your circuit is going to be very large to prove so one way to do this is to say

well I'm just going to declare a length for A1 and I'm I'm going to let circuit throughout the competition check that I always add the correct amount at each step we're going to see that afterwards but basically now assume that you have an L that is declared and it's not necessarily true but for now we assume that L is really the length of A1 so you want to prove this equation here when you're given this this commitments and uh so you say okay I know a0 A1 A2 the coefficients of the the polinomial just that you know if the verifier first picks an X randomly then you know this polinomial here when I evaluated X it is

zero as simple as that and you can use kg for this s proof sorry Patrick one one quick question um I got a bit lost in here because like the main the main thing that we said so far is we are splitting the operations and field operations go to some place and elliptic curve operations go to another one because we don't want to execute it in in the main circuit so what what I'm failing to follow is those two things are usually like interlift and like entangled let's say on a on a main circuit or or follow some main logic which is not I have all these set

of operations and all these other set of operations like they might have connections between them meaning copy constraints or stuff like that that you want to be sure that I don't know some some coordinate is this or I don't know whatever you want to Hash to point I don't know whatever kind of stuff it is so in here it you I mean at least me it doesn't look like you are accounting for any of this like original order maintaining or whatever you want to call it so I mean am I just having the wrong Intuition or like how how can we um I'm going to try to answer question I'm not sure I completely understood it correctly so if at some point sure so what I'm trying to say here is that um

I'm looking at you know the record of operations all the previous steps the record of operation at this step and I want to prove consistency so the part about splitting the competition between F0 between ECC operations and and group operations is somehow already done it's basically in A2 so at a current step in A2 what I write is the input and output of the ECC operations I don't do the operations I just write this is the input this is the operation I was supposed to do this is the output and uh this is what I write in those tables A2 at each step and when I pack them all together this is what

gives a z um to going back to um you know you need to like what's the relation to the output of the field operations this is why I was saying that in your main circuit you're going to pretend that the that the the clent output is correct you're not going to check it but you're just going to consume it you're not going to check in circuit that these outputs are correct you're just going to you know list you're just going to make sure that the list is is okay that the list of operation is okay but each time you just take the output and you you pretend you can continue as if it was correct because like what you mean is you are

proving correct accumulation or correct like yeah correct accumulation essentially if your statement so on that I agree but I guess uh the question is uh we are not allowed to have absolutely any extra logic that it's not simply he I have a set of elliptic curve operations and a set of field operations and I want to prove them correctness you cannot add any extra logic to that so like they are treated as completely independent operations and you cannot add extra logic that I don't know allows you to do assumptions between them or I don't know like the output of this one is the input of this other one like having some kind of permutation argument or whatever it is

you are just proving correctness of computations that's all so I I think you can defer anything in the same way sorry I didn't understand that what you said could you please repeat yeah I I think you can defer any operation in the similar way uh just you can have more of codes for example you can also defer hashes or whatever you like yeah that is true but I'm not sure if that is true by the way but I'm not sure if that's that's what he I mean kind kind of answers in the sense you are like the main goal here is we are building some kind of uh call it BM or Call It Whatever that it only task is I check correct accumulation of

elliptic curve operations and then I allow you to verify all of those extremely cheaply uh and and like that's the task of of this of like the construction the task of the construction is not like uh in the Nova case or some of the other uh IBC folding schemes where the computation that you are proving is essentially like whatever you want to be like this this has a very concrete and specific application only in uh non-native uh arithmetic proving let's see to be honest I'm I'm not entirely sure at what you're touching so in the

sense that all the operations that you so basically all the extra logic that you that you want to apply to the output of these expensive operations you can do them in circuit it's just that you don't want to do in circuit those expensive operations and in this case I just looked at um ECC operations but like Le said you could put any other operations that you wanted there but the extra logic as as long as it's cheap you can you can put it there and yeah I and and even like you know I I chose to put ECC operations outside but I

could arbitrarily you know say I only want to do half of the ECC operations outside and the other half inside which wouldn't make sense so obviously you want to want to defer anything but what I'm saying is that you can really play around with what you decide to put to put in those records okay I see I want to exp I want to expand maybe on this a bit uh you can actually have arbitrary set of promiles that you accumulate in this transcript uh and then uh and then you have some custom way of checking them more efficiently that's only thing that you need for this to make sense so if you have some customized system which allows you to check some particular kind

of precom let's I don't know defer operation let's call it precompile uh then then this thing makes sense moreover I I think in some VMS uh people are actually doing promiles in similar way so uh so so indeed it's very general way of deferring operations I'll just let's just continue I don't want to take over more time from from this Patrick but maybe I can get back at you at the end if I still not yeah and I have another another question so I'm confused why is it so like as far as

understand when you are doing this concatenation you're making some kind of randomized check in a point right MH so my question is uh okay so in in each step of IVC I presumably know the size of my transcript right and it's it's constant sized you have let's say you have yeah so what just prevents me from shifting already existing transcript left and uh sort of uh just adding a new one uh I mean you point you could just say I pick L well I know what L is going to be so I just use that

value yeah I mean l is uh program counter multiplied by amount of operations that you need to do in a single circuit so it's it's pretty clear what it will be yeah well yes and no so there's this case for instance where for instance in the case of of Stack proofs where you know you have like some predetermined amount of functions that you want to execute at each step they do not necessarily all entail the same number of uh of operations well okay I can make an accumulator and comput it directly this is what's going to come afterwards so oh okay but I see I see so basically isolated the proof system

where I said you have some L that you're gonna you you hope is going to be is going to be the correct value and then in circuit in the logic we are going to make sure we're going to have that accumulator like you said so the point is that because L is dynamic you need this l l is not determined by uh the circuit itself uh and this somehow Dynamic and depends on previous steps uh you forced to do this randomized check instead of just static shift yeah and okay and and also by the way remember that I'm doing this check like the verifier is only doing which the

which the circuit is going to run the verifier is only given the the commitments so the verifier I mean there is no way of checking a z is really concatenation of the two and doing a static shift if you don't have the them in in clear text or at least no I can I I definitely can if if I is static I can make okay whatever but without having A1 remember I don't want to give A1 to the circuit is that okay I think I have shifted A1 beforehand okay no it's it's not okay I agree I agree okay you're correct if you

do not give me A1 it's it's the same problem yes [Music] I only want to give like commitment to it but yeah so like I said before so this thing is only useful if you know indeed that L is the correct length and uh by the way um you know since I'm using kggg to verify this they're going to be pairings but I'm just going to ignore them in this talk because it's just add an extra complication which is in in spirit not very different from what we're going to do from the rest so let's look at what the the auxiliary proof information that we talked about is going to look like so you're going to have you know your commitment to the record of expensive or

input outputs of expensive reperations at all the previous steps you're going to have a declared length U and you're going to have uh A2 the record of input outputs of expenditures operation at the current step and then a z is going to be the the concatenation of the two and then you have a commitment to that and I'm also going to compute like I showed before a proof that a z is the concatenation of the two assuming that L1 that L is a correct L okay so this is going to be in the in the oxil proof information which is public so now given that what does the core function do so remember we already had um we constrained the output of the

cheap part to be recorded in the table of operations at the current step so in A2 and now I'm going to check that you know um the a0 which was the new accumulator at the previous step is what is the old accumulator at the current step so basically a z that was in oxide I want to check that it's the A1 in Oxy plus1 that basically didn't change between the two so that's an easy check then I'm also going to check that the length L that is an XI Oxi + one is the sum of the length that was in

oxide plus the size of the operations at the previous step so which means that to G I need to give the operations at two consecutive steps precisely to check that the I've correctly updated the length so G is only going to depend on the size of operations at only two consecutive steps basically and by checking this this is the accumulator idea that left mentioned before I can always guarantee that you know the the length is correct this is really how I guarantee that the concatenation proof that I'm going to also consume is also useful and guarantees correct concatenation and in G what I'm going to

do is I'm going to you know check the inexpensive part because remember the verifier we again have a kg thing where you know you have some field operations some group operations and even some pairings but I'm ignoring the pars and I just want to run the inexpensive part of the verifier basically the proof that is going to be in oxide because it needed to be checked somewhere I needed to check so basically I take the proof of concatenation at the previous step and I check it at this step and I want to make sure that the input output of the expensive part of the verifier is also recorded because then I'm going to check that at the next step and that's basically the main

logic of uh of the circuit of course I've ignored things here like um I've ignored the pairings like I said there's also the question of how do we generate this challenge X because here it's in a circuit so it needs to be n it needs to be you know deterministic how you derive it these questions I'm just sing out under the carpet because it's just technicalities that obstruct what's the main logic of the of the circuit and um maybe going to do a pause now to see if there are some questions I have questions but about the decider so willing to wait if that's

there's more to come on that side such that it makes sense to ask it ah yeah yeah so right now I just basically guaranteed that you know I correctly recorded all the operations but we're going to see how we check the things at the end and U one important thing here is that yeah the proof size and verification time they're only proportional to you know the size of your operations record of the operation record at the current and previous step not the whole accumulator right the other thing is that the verif finally gets a short commitment to those records like you know doesn't get like full record or anything and the pro time increases with the record size because the pro needs to compute the the the concatenation proof if you're doing kggg

proof then you have to compute this question polinomial but the size of the circuit because we're only proving the inexpensive operations we end up proving the expensive operations the size of circuit is also much smaller so this compensate so now okay I'm going to see you know I have my record of operations I want I said you know I want to prove them natively in fq know remember we had so now I'm going to show you how you can go from record of operations from a from FR you can put them to to fq and then you're going to see how they present natively at so we need to make sure that this translation is done

correctly and you start with you know we have R is smaller than q and and to R and this was the look of this operation here so you had a matrix a r which was basically your record of operations so basically this is going to be your a zero final at the end you know whatever the end is you decide it is and what I'm just going to do is I'm going to write in in fq now I'm basically just going to recompute x0 and X1 and basically reconstruct X and Y and a was a scalar in F FR but R is smaller than Q so I can just embed it in fq interpreted as an

element of N fq and you see that by doing this I just basically half the size of the of the record so I had a commitment to AR I'm also going to commit to AQ and um now let's and I want to prove that this basically that this was done correctly that this reconstruction of AQ from AR was done correctly so for instance I want to prove that you know the op here is really the same as here how do I do that so if you look at the entire Matrix and you look at all the rows together you can interpret you know all the elements in the first row as some coefficients of some

polinomial you know in in fq so it's the same thing as proving as saying that you want to prove this basically so one thing that and so if you want to prove just this there's also the other thing that you could say I want to prove that X is really the sum of x0 and X1 at all steps the the the the Reconstruction of x0 and X1 at all steps but if you understand for the first one you understand for the rest so from here you know you you are given a commitment to to AQ and a r as well and what you're going to do is you're going to evaluate this First Column at some random

point x and now you're going to in F FR prove the correct execution of an algorithm which computes this sum m q because you're doing this mod q and compare you know the output of that algorithm to the claim VX and the killing part here and this is where you have to eventually pay because you know you're trying to go from non-native to Native so this is where you pain because you're proving the execution of an arithm that is doing these operations mod q and let's see how you can write such

an algorithm so you can basically you can just do a polinomial evaluation algorithm where you know you you start with uh the first element and then it's basically horn except that you're like skipping one step every time be the indices because the a table was half the size you know and you basically just multip multiply what you had so uh yes should be sorry should be W here WX so you multiply whatever you have here by X and then you update your your record and you're doing this multiplication mode q and at the end you check if you know the output of this INR is really the

claim output that you had inq uh wait you're actually doing this sorry what it so this is like the actual algorithm that you use so basically I'm just saying that you can use whatever algorithm that you want and this is no I mean the but but but this is not efficient at all there are far more efficient methods of computing this of of comput I I completely agree I'm just giving just one example okay okay okay you know I'm just taking I'm just saying I want to evaluate that polinomial and I'm just you know I just want to evaluate that polinomial and I'm just like a compute

the output with the other output that I had you know it's just that this is a very simple example where you then have you know the multiplications mod q that appears and the mod Q you have to do it in Fr I'm just trying to to exemplify this this the simplest algorithm do for this and um the thing is you know at each step I only had here here I only have one multiplication because I only looked at the left column but we had four columns so you have four equations to prove so you have four multiplications m q to prove in so basically per operation that you had to do you have to pay for multiplications mod q and uh at the end then you know so this is how you can you can prove the

correct translation between the two tables and then of course in fq you can then um prove natively the operations there once you have done the translation but the core part is read the translation once you have done the translation natively you have you can prove it cheaply in fq So at the end you have like some Pro Au proof information have some auxiliary proof information like this and if you want to check its validity you know you check that this proof is correct so which would ATT test that uh c0 is really the concatenation was in C1 and C2 assuming the length here to be correct but the length is

correct because the circuit checked it with the accumulator that we saw and now you use the commitment c0 as in what I showed before as the commitment to each of the columns of AR and there you can do the translation proof and then do the proof in fq so we're we're almost at the end already so um in terms of performance so the way I so the metric I want to use to to compare this like to to sort of assess the efficiency is the gate count the number of gates that this method entails compared to if you weren't using this method at

all so the the the the really the gate that you're paying are the gates for this translation especially with the mue operations and the M multiplications that you have to do plus the gate count in the proof that you're doing natively and this is versus you know if you were doing all the multiplications for all the operations in F without using this method at all so this is the performance metric and in the paper then I is a section where there are like different parameters for this and U basically if you do some very stupid um if you do some very stupid um MSM algorithm that you use then you can

already go up to a factor 50 second of course you don't want to do a stupid MSM algorithm you want to do something uh by factor of 56 I mean the gate count is is reduced by a factor 50 56 but if you um do something more efficient you're still not going to stay in order of magnitude more yeah but this is compared to nonnative uh the nonnative version not compared to cycle fault and compared to cyle to cycle fold that is like 2. half or something like this well cycle fold looking at the paper and I'm trying to discuss with three and a half at the moment to really get the numbers

the issue in cycle FL that I had personally perhaps you you you have a better method for this is that I didn't see really the parameters that were plugged in to obtain the numbers so I couldn't really do an apple to Apple comparison there um if then you can then check okay cycle for what a cycle for clim compared to if you're doing non native um there cyle says you have like a 3,000 like that the side of the circuit in the second group is like 3,000 Gates only but I'm not sure exactly again what the parameters are there that he's playing with so so I just want to ask him that and try to figure

out we coded cycle fold with Nova and I I I don't think you can make it 3,000 constraints like it's not extremely higher but definitely higher than that for sure uh I think in the tradeoffs for cycle fold to be honest are more in the deser side of things than elsewhere because in the deider in like you basically need to if you want to verify in the ebm you need to verify one of the proofs non natively in the main case proof that proves one of the sides of the cycle and if you have cycle fold turned in um it turns out that the final

decider is uh significantly bigger so therefore you need to but by this met but by this metric this method is just infusible because it tries to commit it commits to all your elliptic curve operations over a second group and you get hit by a large actually a large circuit over a second group so if you want uh evm decider then this method seems like even sort of worse right so you're committing to to I mean the operations you're not like you're just writing down the execution tra but natively so this yeah yeah I mean thei the final decider will consist

of still of two parts first part is like your normal decider and this interface which then uh moves your operations to a second uh to the second curve and then you do this them all the second over the second curve the point is that the circuit is large it is like multiple elliptic curve operations depending on the amount of steps that you did but in cycle fold the size of the circuit is one operation so uh if the cider for cycle fold is already large then for this thing is it will be like much larger what do you mean

proportionally sorry what do you mean by one operation for cycle fold for the decid well Cy in cycle fold like your second circuit uh simulates a single operation and basically what you are doing you folding a lot of these instances uh to to you're you're sort of doing the same thing but but not not at the final step but you are just sort of delegating the separations to singular instances of this cycle fold circuit and then folding them together this of course has larger other head but in the end what you are getting is a is already a folded instance of a circuit which is

able to do a single elliptic curve operation so the amount of stuff that gets popped out to the second curve is smaller okay I see so you're saying for the final decider only comparing the deciders is not a metric that is accurate enough yeah I mean yeah yeah yeah yeah like pays more during the competition but at the end is cheaper and you're saying we're cheaper during the competition that at the end we pay more B yeah but but also you probably don't not need to pay any of those because right now like we have the jar M research and now you probably can just uh instead of committing to the second

curve uh you probably can just like avoid this commitment all together and just run and on Native gkr at the very end uh but then are you sure that we would then be benefiting from all this because the whole point of this was precisely to do all the operations natively at the end right so I'm I'm not entir yeah but but but because they're already in JKR it's almost so so B basically our trick is very similar to what you're doing in a sense that you're sort of proving that you have copied the data between your original like transcript commitment and

second commitment right but we do not have the second commitment and we treat it sort of has a synthetic commitment scheme over a different field so in a sense that you are asked to evaluate this polinomial in a point and then we run this computation but we do it for multivariate polinomial and not univariate but the idea is very same like very similar so now we can just run gkr uh over this different field f r uh or fq I mean the second field your nonnative field um and then you just do not get exposed to the commitments over the second curve

ever okay I see that's that's the trick if you have a WR up love to to see oh we have an implementation we have better than write up we have an implementation uh but uh yeah we also have a write up okay yeah I would I would love to see it if you have one please yeah okay yeah yeah we can discuss that I'm curious to know it works in detail um also one thing is that you know at the end um usually whenever you have like your your IBC proof refolding at the end you don't want to actually um you know reveal the witnesses you're actually computer SAR that you know um witness for your folded instance at the very end so you're

doubling because of that when you're using cold because you also have the second the second not doubling because the circuit smaller but you have to run also a second proof for second curve cycle F so this cost also needs to be taken into account yep and I guess in line well sorry please finish first Patrick and maybe okay okay thank you thank you very much um I have uh one question um which is mainly related to the deci but in another sense um so have you done any benchmarks uh that allow you to know

basically when it's worth it to use all this Machinery uh like from which amount of elliptic curve operations delegated Mak sense to use all this Machinery versus hey I'm going to just eat this up and and that's it because at least with folding it has happened to us a lot that it's never clear completely um when it would make sense to go with a stark uh which almost free recursion let's say versus going folding which can fold much faster than recursing but uh at the same time you need to pay for the final decider so do you have any numbers unfortunately I do not have numbers right now to

inition also think so I do know that for the side of circuit that we're targeting like 29 220 you know like this definitely makes me much more sense um the the lower bound um I unfortunately don't have like n b because it also depends like what's the size of the MSM you're going to do in circuit for instance um like for instance let's say you have you have a a function that you're executing that's doing some size 64 or size more you know um and this is fairly Dynamic and moving so there are like a lot of

parameters to tweak because like I said we're not just doing like just one IBC right the context to which we want to use this actually I mean this is presented for building IBC but I said stack proofs also fall into this and this is where we really want to like you know prove that you've correctly executed a function and there at Le time the function that you're executing does not really depend just on ASC on us um so I don't really have an like there are a lot of moving Parts there I don't really have a good idea a good answer now uh as to that I can try to ask more to have more uh um benchmarks and I can try to for the numbers but if I say anything right now I don't think it's going to be remotely sure sure no

worries thank you anyways thank you are there any other questions from the rest of people I will okay I will assume not so I have one more if it's okay and you have the time um I don't know if that makes any difference or not but is it more worth it to run like larger MSM like msms of a lot of points or like a lot of msms but really small ones like meaning a single elliptic curve operation but do it a lot of times or lots of elliptic curve uh

multiplications combined in an MSM but do it less times is it the same cost or changes changes because um like if you're doing so it also depends okay this first one parameter how you going to split the binary representation of your of your scalers that's the first thing so assume if you want to use like an arithm X algorithm or whatever you know you can go around let's say you spin in chunks of four bits or something like this and um now if you depending on your MSM algorithm um you may actually minimize number of steps compared to if you were just doing operations one by one because if if I'm just doing one scal multiplication then adding you know

this scal of multiplication if I do double and add algorithm or enironment of that that's more efficient then I pay a cost is going to be proportional to the size of like to the number of chunks basically and I do this for each term in my MSM so if you have if you do one Ms larger MSM you probably minimizing the number of steps that you're doing compared to the first approach and if you're minimizing the number of steps you're minimizing the number of group operations that you need to record and then the number of group operation you need to do at the the very end so I would rather say I would rather go up than down in terms of the sizes then but then yeah there's also you how large can you go given the other parameters but

definitely more yeah I just wanted to add that uh n scalar operations can can always be reduced to an MSM of size 2N using random linear combination and uh um P if you use Pinger uh then pretty fast uh multiscalar multiplications becomes much more efficient yeah so answer is almost always that makes sense um any other questions otherwise I'll let you leave because I want to take more of your time we have

asked a bunch of stuff already no no I'll get I'll take it as a no so again thank you very much uh Patrick and to for your time I appreciate it a lot you coming here and and taking the time to to go through the paper and explain like all the com sets and and Di Deep dive on it uh yeah mainly say say thank you and hope to hope to see you soon and congratulations on your work thank you for thank you bye bye cheers everybody and Le please I would like to see the the writer please don't don't forget if you sure sure