ZK13: Redesiging Proof Rules for Efficient ZK Proofs of Mathematical Proofs - Brandon Moore

Transcript

[Music] Hello, I'm Brandon Moore here from Pi Squared here to talk about our work on cryptographic proofs of mathematical proofs. Um, so I guess a little bit about why we want to do this and it's kind of the whole company the pi squared is proof of proof. Um but some mathematical proofs, they're flexible. You know, you have kind of a single fixed logic that works for all sorts of applications. Um and we're particularly interested in proving things about programs according to a language definition, you know, formal verification of security. You can even just prove the result of a concrete execution if you can do that efficiently

enough. Um so then you end up with a very small trust base just the the language definition and a simple proof checker that doesn't change for the different languages no compilers or interpreters or whatever. Then on the other hand, using a snark gives you, you know, a very small proof. Uh, pretty fast to check. Um, and I say zk or zk snark or snark. Uh, a lot of times we don't care too much about the zk part or the the proof of knowledge part if you just want to know that something is true, that your your contract, you know, is formally verifiable. Um, just knowing that there exists some proof is is as good as knowing that the the prover. Um and also leaking the details

might not matter. But there are also other applications like you know if you want to if you're trying to use this to encapsulate actual concrete execution and there's maybe secret input. So uh yeah snark is fine some of the times. Um but uh then the this talk is not about the the the big picture there. It's about you know how how exactly we uh uh prove our mathematical proofs. Um so your first thought might just be hey run a proof checker in a ZKVM you know you compile whatever well you can do it but it's very slow you might even run out of guest uh VM so we tried to design something to uh you know more directly use the capabilities of the snark proof

system to check the proofs and also adjust the design of the proof language itself to be uh more easily proofable. Um so here's an example of the kind of proof we're talking about. Yeah. Um so you know sort of derivation you see and there's all these proof rules. Um um so this is just sort of a propositional logic uh with a little bit of complexity and the idea is that these are like meta variables that can be substituted with terms. So we have a little more going on. Um may have seen this in something like metamath. Um you have modus ponins for applying implications.

um this substitution step data is that instantiates meta variables and then here's these propositional axioms you may have seen uh I named them after the S and K combinators because that's the only way I can remember to uh prove anything with them but so here's here's like a tree structured proof uh another format that you might see is a Hbert proof uh where sort of each step is a a proof rule usually you just write down what you proved and what earlier uh earlier steps you used. Um, and so in both of these cases, we saw the same general structure that the there's some set of proof rules. The proof is a bunch of instances of these proof rules. Um, so you need to check that it's locally,

you know, actually shaped like a instance of the rule you say it is. And then also check that all of the hypotheses are satisfy the by the conclusions of another step. Um, and also it's maybe sort of implicit in both of these, but you need to make sure that that this is like an asyclic graph. um of which which proof satisfied which other one. Um yeah, so here's maybe the the proof rules that we've used so far. Um if we're being a little more careful, we would say that the proof rules can have parameters like this a and b terms of the modus ponins that get substituted in the rules can have hypotheses and conclusions. Um and in general the the hypothesis or conclusions might be

different kinds of statements but here the only thing we've got going on is we're saying okay this this is proved this term is a a true proof um the axioms and then um but we also have the substitution operation that can just instantiate it with the substitution and uh that that function application thing is not a uh not really a term and you know ordinarily you know, pen and paper proofs or or even, you know, automated uh proof assistance, you know, it's it's fine to have things like that. But, uh, for our case, you know, we think a little bit more, you know, what happens if you were consider trying to run it on a ZKVM or you more generally have a ZK circuit. Uh, well, every little

instruction that goes into doing the function application is gets materialized onto the transcript and takes up space. So in a conventional setting, you know, leaving any easily computable, decidably checkable things out of a proof format, you know, it's good. It it saves you disk space and stuff and you can recomputee it quicker than you can read the bytes from disk maybe. Um, but then in a ZKVM, you know, everything u shows up in the transcript. All the intermediate terms you compute into memory show up in the transcript. Um so the first first kind of thought here is okay don't don't try to hide these things just you know you can give everything up front give it as part of the proof file if it saves you more work

recomputing it than it took up in space then um you come out ahead so um and then also if it if it's a term that would have been computed at runtime you know referring to that term up front doesn't cost you anything so now we can say the substitution rule you know one of the parameters is okay what the result is and Now you're checking as a hypothesis um that this uh uh substitution comes out and then it's a similar story for computing the substitution itself. um you know maybe some things arithmetic maybe crypto things you can come up with a super efficient ZK circuit for proving that specific thing but for something

like recursing over a term well you know certainly again in your ZKVM execution you just have the the whole computation tree would become laid out on the transcript anyways um and as far as I know if you're you know designing a more direct circuit you get the same sort of thing Um, so at least for recursive stuff, you might also just say instead of having some notion of executable functions, um, just let's define define things with more proof rules. Also, if the execution ever had to like do tests, make choices, backtrack, you know, that's all just more wasted work. You

can just tell it to do the right thing from the beginning, supply it as advice to the the ZK computation, whatever. Um so uh so kind of the first first thing is say remove any functions um and just make them more hypothesis. Um yeah so I said there were only two two relations. Well now we've got a third relation here saying that hey this or we've got a second relation saying that you know the result of this substitution is this. Um and then if you start thinking what the rules would look like say that you're substituting a term that's an implication. You you need to figure out what the substitution of the subterms is and you make a substitution

into a variable and then you know hey we've got this new judgment for looking up a single variable. So we've got a few uh few relations running around. It's not the the details of what exactly they are isn't that interesting. Just that in general for a proof system especially a proof system about a programming language you might have a lot of relations. You might have a type checking judgment. You might have memory lookups. You might have uh stack things all all and then all sorts of auxiliary functions too. Um but it's it still fits into the same notion. You just you know you have hypotheses and conclusions. You make sure that your hypothesis is the conclusion of some other step um including being in the the right kind of

relation. Um so now we talked already a little bit about what ZKVM can do efficiently. Um but now we need to think a little more about what what these snark proof systems uh support. So I'm going to talk in very high generality here and this is also kind of how we we thought of them. Um but in the the high generality there's you know some some witness that you're proving satisfies some constraints or some problem. Um the witness is always made up of a bunch of numbers from a finite field usually primes although the binius people use towers. Um and then your your basic like the sort of primitive constraints that

you can just put put down freely are uh some kind of lowderee polomial or even even slightly more restricted in the rank one uh constraint systems but lowderee polomials over a small fixed number of variables. Um, and then the the main thing that lets you do any sort of global collective operation are permutation and lookup arguments. Um, and if anybody can suggest a third uh global operation, I'm missing out. We'd certainly want to see if that's uh something we can put to use. Um, yeah.

So, the the exact realization of this is a bit different. You know in the the stark plonish kinds of things your witnesses are u arranged in a two-dimensional table and your polomials are checked between each pair of rows. So it kind of has this uniformity. Um the rank one constraint system they're just in a vector and you have arbitrary matrices and then you can think about general arithmetic circuits compile them to one or the other. Maybe even think about like a GKR circuit evaluation. But in all these cases, the basic things you've got going on are, you know, simple addition, multiplication, constants over a finite field. Um, and also, um, really built on top of that math is the permutations and

lookups. Um, just kind of seem to be the, uh, common denominator. Um, just to yeah, recall the functionality. So, so both of these are things you sort of build into the uh constraints or circuits when you're um yeah setting up the instance. Um uh so you pick two lists of the witness elements. Um I guess I'll say in a in like a stark it might they might need to be like two complete columns of the table or something or segments. Um but anyways given those two lists so the permutation argument is just a way of enforcing that one list is a permutation of the other.

Um the lookup argument lets you enforce that the set of values in one list is a subset of the set of values um in the other. Um, and it's uh maybe easier uh maybe you can use permutations to get like a multi-et thing, but but we really want a a set. So you can look it up with more, you know, more times on the in the A's than it than it was in the B's. Like you can use the conclusion of a proof step in a bunch of later steps. Um so anyways, you can do these things. They also generalize uh very easily to uh having the list be lists of like a fixed size say three tupils of field elements.

Um and then internally it's you know compute some sort of polomial expression incrementally and then you know they only come out equal if the things work. Um but yes uh I guess I said I'm not not going into the implementation yet. Um and then the also key trick with permutation um usually the way that you use the permutation for anything really interesting is um you use it to make a sorted copy of a list that's sorted by you know something else that makes the the check that you want to do local. Um important thing ZKVM like the memory arguments you know they have the this

kind of linear instruction stream with the read and write operations and you need to look back many instructions to see okay where's this value that I'm reading coming from um but then they emit these tupless address and something like the cycle count um and the values and then by making a a copy of that that's sorted first by the address and then by the cycle time then everything's a nearest neighbor. Um that's that's how we'll be applying permutation arguments. Um right so with that uh review of what what the uh what the snark systems give us um and we can think how this kind of matches with what we've got going on with the proofs. Um

so the the local shape of the proof rule you know the hypotheses and conclusions of the individual rule are for the most part just like simple expressions involving the parameters. Um also I guess because we we said that we're not going to allow you to have complicated functions like a substitution going on really they're um yeah that's uh also not there. And then the the non-local check that you're doing is checking that the the hypotheses of your proof step are satisfied. Um so the you know filling out the exact form of the hypothesis and conclusions given the parameter is just you know local fixed relationship. So probably we can use the

local constraints for that. Um and then we would really like to use the lookup arguments for the um uh for the hypothesis. But there's a few problems with that. Um so one is that it's just just checking the subset. There's no notion of order. Like the Hbert proof was only supposed to refer to earlier proof steps. The you know the the more tree structured proof was supposed to be as cyclic. Uh so it doesn't do that. Also the lookup only works over field elements and uh you know we've got all these expressions running around. Um so we can address both of these things by uh changing the form of

our rules and I guess a little more functionality. Um so the the general strategy uh we can enforce that things are not cyclic directly in the rules by kind of adding a depth counter where necessary and having explicit inequalities. So then the proof checking can try to match them up freely but the the inequalities will uh break any cycles. Um and then replacing the terms with numbers. Um so generally the idea is to just you know kind of arbitrarily assign numbers to terms just like you might arbitrarily have say a memory address that the term got allocated at or you know some index into a table but um uh there's a little more uh complexity

there. Um, so yeah, here's the idea for uh how we can prevent there from being cyclic proofs even if that's not directly enforced by the the lookup. Um, so you just add this extra argument which is interpreted as the depth. Um, and then uh add some inequality saying that the depth of your hypothesis to the extent that they need to carry depth are less than the depth of your conclusion. Um I think the inequality is trick is cheaper than taking a specifically taking the max and as long as we break the cycles it's uh it's good there. Um yeah and guess other comment

is that that yes it's you know kind of messy fairly mechanical you might imagine some sort of translator that sticks these in automatically. Um and I'm going to put these aside for a little bit but uh so you need to you need to modify your proof system to include these uh uh also so uh right the hypothesis and conclusions. Um I guess the first step is these uh the the entire claim you know like we said say this substitution comes out or this this term has been proved um feeding those into the lookup argument. Um well it's really the expressions that are the problem. Uh if

those become numbers then you know they're already these relations that are just taking a fixed number of arguments. So um you can just assign a different constant to the different relations pack them all into a uh you know single tupole pat it with uh trailing zeros. Um zeros can even be free depending on the the back end. Um, so now we've got uh all the kinds of claims we're dealing with uh you know in a form lookup likes it uh presuming we can handle the terms.

Um and this is maybe not as bad as it sounds because if you think about what just a you know efficient conventional program for doing proof checking is well it uh you know it'd already be dealing with the terms of some sort of sharing preserving representation. you know, maybe it's pointers, possibly it's table offsets, but there's already some uh some number. And you even have this structure that the you know, the the pointer or the the table entry is like one constructor of the term. Maybe it says, "Hey, I'm an implication. Here's my children." And again, numbers for the children.

Um, and then the the sort of thing that your code does to handle the part of the proof rule that you know had an expression in the hypothesis or conclusions. Sort of taking this term and walking step by step down the constructors of the term to uh, you know, make sure it matches another one or has the right shape or whatever. Um, and as before, we're we are assuming that you know everything is sort of provided in advance. So you don't need to know how to guess what the say what the implication between these two terms is given their number. You can just you know be provided the the answer. Um also this this is actually the approach taken in metamath zero

which ended up with a very fast proof checker. They sort of prefeed it tables with all the terms that it'll ever need to deal with hints step by step of how to do the any unifications or whatever that's going on and all of that. Um so within the the stuff we've been talking about about what the proof rules look like we can uh make at least a few few steps towards this approach. Um so rather than directly writing like that term a implies b as an argument to a relation. Um you know we can say okay the argument needs to be a single number add extra parameters which are going to be the names of any non-trivial term. So it's not a a implies b. We're going to

say t if t is proved and a is proved and b is proved. And then we're going to have a separate hypothesis for this work of uh um checking that t really is an implication between a and b. Um so again this is kind of messy looking but also a fairly mechanical transformation. just take take all of your expressions and kind of lift them out step by step naming naming all the subterms and having uh uh you know explicit hypothesis for checking the shape instead of uh um you know expressing expecting to get the whole thing in one go. Um so slightly larger example is this you know

substitution on the implication rule. Um so again you see there's just two terms in the conclusion that have like syntax in them. So we give them names T2 and T1. Um have new hypothesis checking that there's the expected shape. So uh it's not too complicated in any individual step. It just kind of uh flattens the structure down. But uh so now we've ended up with all of our uh original rules. um being in this form of you know fixed relations over fixed size numbers that the you know zk proof systems will be happy to handle. Uh but the one thing

is where are we getting these uh these new facts from? Um so now if you uh probably the most related prior work would be you know there's some people that use like data log for analyzing programs. um we have to do a very similar kind of relational transformation of things um and in that kind of setting the idea is that you would pre-populate a table saying uh what the shape of all these terms are you'd pick some ID say you know which things are which constructors or you know have which forms um but we need to populate these facts um and then I guess the first approach we're going with

uh just to kind of not go too far from the design, not to add a completely new construct. We're going to say, okay, we're going to get these facts also for uh from instances of extra proof rules. So, we have this kind of axiom looking thing that says, you know, hey, I'm declaring term T to be the implication between A and B. Um, so this rule is a bit too simple, but uh um you know, look at what goes wrong and uh try to fix it. So, one thing is that A and B can just be completely random numbers that have no interpretation as a term. Um, well, that might not actually be bad. Maybe it's just sort of acting like a opaque term.

Uh, worse, nothing stopping it from being a cycle. Um, your logic probably doesn't want to have uh uh cyclic terms like that. Um, although some logicians do that, but but yeah, not not the logic you're trying to define probably. And then uh but the worst thing is that nothing is stopping you from making conflicting definitions. Especially you can define it as something provable. Define term one to be a implies a and you go prove a implies a and you also define term one is a implies b and then well term one is proved so you can use that. Um so now the first thing about stopping cyclic terms and and maybe uh

unknown terms is is the easier thing. Um we just have uh make a new judgment that says hey this number is known to be a well well- definfined term and we use the the depth arguments you know as we already did to stop your main logical derivations from being cyclic. Um so now each of these terms that's you know defining a term emitting a constructor just uh has a conclusion saying emits two conclusions which is the first time we've seen that but I mean it it doesn't really break any of the rest of the the framework. Um just you know either of them is available to

satisfy hypotheses elsewhere. Um, so now along with your specific shape telling you, okay, what constructor is term T made from, you also just say, hey, it's well defined and here's its depth. Um, but this did not prevent you from making conflicting definitions. And to deal with that, we'll need to actually add a new uh new kind of primitive mechanism to the rule definitions. Um, and the thing is to just say that uh certain outputs are unique or I mean it really doesn't even have to interact with the ordinary hypothesis. So it's just a sort of unique uh tag to things.

Um so the idea is that there's a special thing that you know you write it by the conclusions but uh it's not not necessarily a conclusion itself. Um that says uh you know something is unique. And then when you're checking the proof um you need to check not just that the rules are wellformed and all the hypotheses are satisfied you also need to check that there's no duplicates of these unique things. Um and then this can be enforced with the permutation argument. you gather up all these tags sorted by uh you know sorted by the the tag and then sorted by the number and make sure that no neighbors are equal. Um and then also yes if you're having a um if you have other kinds of

constructors of your term maybe you have uh like conjunction terms or something um you'd have a rule that it that would say that the new term being defined t like maybe is a conjunction instead of t as an implication but they would all still say it's a well- definfined term and I'm defining a term. Um, I guess another thing to note is that we didn't want the depth argument here because uh you don't want to say that term t means one thing with one depth and another thing with another. That would just let you make conflicting definitions again. Um but yeah, so now that we've got this machinery of uh uh having these unique things so that you can can flatten the terms uh you can

uh you make a pretty mechanical transformation of ordinary proof rules into uh something that's more friendly for u zero knowledge proofs. Uh so each rule has parameters, has hypotheses, conclusions, optionally a unique output. Um I guess I didn't talk about what's what's public. Um so you know ZK things usually have the notion of public data and the private part of the witness. Um so here a natural thing to do seem to be just to say that certain of the certain of the steps of the proof are public.

Um, and then further you might want to say that there are certain rules that are only allowed to be used in the public part. So like here we've got a rule that just asserts a new statement as an axiom, which is fine if that's a known part of your definition used publicly. All your clients are expecting it. Not okay as part of the the secret proof that your your code's secure or whatever. Um so you have this little little feature that you can tag uh tag rules to only be used as part of the public data. Um and then the question is how how exactly you uh uh how exactly you check this and uh so here there's multiple approaches um

and I can describe the way we did it but there's um other things we've thought of and other other approaches you might uh might have in mind. Um but basically we're going uh uh going for the approach of making uh dedicated circuits for the individual rules like translated to circum um and you make a circuit for checking a bigger proof that has a bunch of copies of the rule circuit. You disable the excess copies you don't need. Um and then we figured out a way of using multiple instances of a circuit together.

Um so I guess the the I think the important things of any design are that um you don't want to have to generate a fresh circuit for a larger proof. Certainly not if you're doing something with the trusted setup but even even with the more scalable thing you know maybe there's client side computation or whatever. Um and then the other thing is uh whether you're trying to design a system for uh checking a specific uh specific logic, a specific set of proof rules or something a little more general that somehow reads a description of the logic and processes it. Um and we have some ideas about how to do the more

general thing, especially on like a Stark style transcript. um sort of making something kind of like a stripped down ZKVM that doesn't have general purpose control flow and general purpose memory and uh that sort of thing. But uh I think the uh uh making the dedicated circuits is probably going to be more uh uh more efficient. So that's what we started with. Um and then the other thing is that to use a single fixed uh uh single fixed circuit or machine or I don't know uh not sure there's a general term but to have a

single definition that covers any size of proof. Um um so we wanted to use something like recursion but uh um but then again we know with uh with R1 R1CS families and with with circuits there's these uh folding schemes where it's lighter weight on the prover and verifier. Um, and with the Stark systems, it seems like people only do full full recursion of completely checking uh uh having a circuit that completely checks another ZK proof. Um, which um yeah, seemed like a more complicated way to go. So anyways, that's that's the background, but our

the basic idea is to translate the the rules to a subcircuit that implements those rules. Um, and the only thing going on here that's super specific to the form of the rule is um taking the parameters and outputting the different tuples that are the hypotheses and conclusions. Um, and then you feed them into the uh lookup argument and the so there's a big sum or product um and you can rearrange the terms of that sum and product. So both the uh uh definitions from the conclusions and the lookup from the hypothesis can all be uh boiled down into one single number which is the

output of the you know what's this what's the effect of this rule on the claims. Um and then also you can disable this rule if you uh just by having it output the identity. Um, so then you know this way if you're if you're having just one fixed hardwired circuit, you need to to pick in advance, hey, I'm going to put a thousand modus ponent step in one copy of the circuit. Maybe you don't need them all. Um, so you can turn some off. Um, okay. Yeah, I guess we don't really need to review the uh the exact uh formulas here. Um yeah, I guess the one thing is that the two poles are

coded as a polinomial like that. So the trailing zeros just drop out and if you're hard coding a circuit for a specific rule where it knows that will always be a trailing zero, you don't need to put any uh any gates uh in there for that. Um and then also for the uh for the lookup argument, we're working in particular with the logup argument where everything is just additive and the multiplicity is handled just by you know multiplying something by the count of how many times this is being used uh rather than needing to have like a longer array where you physically put extra copies of it.

Um okay right then to add the uniqueness then there's an additional tupole or outputs from the circuit um and you do some extra extra local math to make a second number which is the accumulator for the the permutation argument. Um and then in the overall overall circuit there will be a second uh second chunk of it which is like a big list which is the the second sorted version of the list um which is fed into the permutation argument and compared with the uniqueness from there um and also has the local constraints that do the sorting and and no

duplicates thing. Um so then the overall you get a circuit what we call a segment circuit that has room for a bunch of rules. Um and it has all these uh all these sort of private inputs but the well not necessarily private but all these local inputs and then the only thing you really need to know to check if it's like well behaved is uh you know these single numbers that are coming out from the accumulators and you need to make sure that your fiat parameters are behaving themselves um um because once you have uh this small public interface then um you can have many segment

circuits sitting next to each other and just add or combine the accumulators across them. Make sure they're using the same randomness and uh um then you can check that this the inputs to this whole collection of circuits together uh form a single uh single valid proof. Um, so yeah, and we're using in particular these folding arguments where you can take a bunch of instances of the circuit and you don't need to do a full snark. You do little more than a vector commitment to your witnesses and then combine all those together to get a a single instance of something about the

same size of the starting problem. um such that then you need to do one one final snark of that final instance and you need to know that the folding was done properly and then you know that all of the instances were individually well behaved. Um and uh yeah so basically you have the public outputs of the circuit the the fiat shmeir parameters the accumulators um and then the the vector commitments to the witness um then also to to do the fiat shmere thing at all we break the uh uh we just treat the witness as two halves the the pre-randomization part and the remaining ones uh we compute a

separate vector commitment to the pre-random randomization stuff and use a hash over that to generate the uh uh the fatmere parameters. Um yeah, so you can compute like a in the leaves take a hash over the vector command build a merkel tree as you're grouping them up. Um and then at the the root of this combination you draw the actual parameters which um so you needed to compute so you need the entire proof to to set this up. You you compute the prefaceion inputs everywhere commit to those cache them up come up with these random parameters

that will be used for the the randomness um then fill in the rest of the parameters and then fold it together. Um this is uh another thing that seems to be pretty unavoidable that if you're doing these polomial lookup or permutation arguments um you really need the the entire list of input to be fixed in advance before you generate the fiat parameters because it's just um the security is entirely based on this idea that drawing a random number is very unlikely to hit a root of a polomial unless the polomial is zero.

But if you know the polomial before you pick then then um you know it's easy to engineer a collision. Um so I it's uh seems difficult to not require preparing some things in advance but still it's just the input vector. So all this this heavy cryptographic work of taking the vector commitment and some of the the folding and things uh can be done in parallel on the segments. Um yeah so then to pack this entire thing as a snark um so the the folding process itself just uses these small small bits of data which are the uh you know the vector commitments and

some of those public numbers about how the the segments connect to each other. Um so the folding process itself only manipulates these small numbers. Um and then uh the prover is carrying along uh the prover is carrying along the witnesses but to know that the the small commitment to the result was folded properly you only need to to work with the small bits. So then these are you know in practice maybe even small enough to just send the uh list of everything and that's how we uh initially are testing it. But, you know, also you could have a a snark of the folding process. Oh, the Oh. Oh, I see. I'm I'm moving a little

too far. Okay. Uh, right. So, what you'd like to to end up with a constant size result is to have a single snark saying that, hey, these parameters came from some some set of coherent looking leaves, you know, whatever they are. And the the user doesn't care how big the proof was. They don't care how many leaves they were. or they just care that there were some, you know, consistent segments that together make up a proof. You could have a snark of the folding process and then you need a second snark that the the prover has this combined witness to the folded instance that um so here they're doing a full snark that they actually know a witness that satisfies the property, not the lighter uh folding thing, but then by doing that

one final snark, you know, you convince people that the the prover had the witness all along. So here's the overall design for how you get to uh get to a a constant size snark of a scalable scalable proofs. All right. Um yeah, this is the approach that we've been implementing um using for simplicity just the nova folding scheme, not the not the IVC scheme, just the pure folding part.

Um yeah um but then I think also the ideas about uh simplifying the form of your rules are more general and you might imagine like a I don't know data parallel GKR evaluation or some other kind of backend. All right. Well, I think um that's about as much detail as I necessarily wanted to get into without further questions. So, you get a microphone.

Hello. Is it on? Okay. Yeah. Just just curiosity. So you show that in a Hilbert style formal system. I'm just wondering which former systems have you implemented you know whether you also even maybe implemented I don't know let's say the Isabel Hall logic or something you know just we haven't gotten quite that fancy uh we have a fancier propositional logic um it's based you know on this meta variable substitution stuff for uh metamath uh the other thing we've done we implemented rules for resolution Um so so just sort of so these rules are more

about you know searching through the clause lists to find uh find where the variables are. That's I guess that's what we have the most concrete evaluation. Um so there's dedicated zk unsat system for making unsat proofs. Um, and it's a little bit of a uh a odd comparison because they're actually using an interactive ZK proof system, one of these uh V vector oblivious linear something evaluation I think. Um, but uh yeah, so our preliminary result at least is that we're like a little bit slower but not even twice as slow. and uh sort of unclear how much speed up

they're they're supposed to be getting from being interactive. Um I mean some of the papers say numbers as high as like 30 times faster than a a non-interactive snark but a little unclear. Um then also there's lots of ideas for uh optimizing what we're doing. um you know there's like known entries in these witness vectors that are small field elements compared to arbitrary field elements you can do the um I guess we're we're you know using these uh multiscalar multiplications for the commitment so yeah it's still still very preliminary but uh yeah resolution proof system is I guess the other uh very different sort of uh logic that

we've got Thank you. [Applause]