Generic VM Compilation Architectures

Transcript

So today I am supposed to be talking about memory arguments but um I felt like it was a better idea to give you a generic picture of what um out of this work with the guys very rewarding and um and in a sense it's the uh highle idea that I want people to understand here and then um and then I can afterwards and maybe we could pull up some of the specifics of of the spec for the programming language that they use to to demonstrate how we can actually use these generic objects to deal both with the execution trace

and the memory trace in a fully modern way. So um I'm not going to be talking specifically about memory architecture arithmetization but I will be giving you the underlying generic uh compilation process by which you can uh take any ISA that satisfies some specific properties which hopefully will be intuitive by the end of the presentation. So that then you can take that and use all of the analysis that we have in the paper to just get um get the architecture that is efficient enough um to implement. So the idea is um that we want to figure out what the optimal design principles are for making VMs. Okay. So we want to figure out what exactly do we need for

virtual machines um to be optimal. And by optimal here I don't mean the underlying engine. I mean the actual AI itself or the actual um uh RAM that we use. So, so overall the the so this is just the motivation for why we're going to do this whole process. So, we want a very small number of constraints. Um, you know, the underlying TK engine is out of scope here. We want to to be usable with anything. Um, and you know, if it's small enough, then we can get recursion without needing to do magic at the engine level or sort of like work very specifically with um with you know, difficult constructions. But honestly, the most important part of this whole is the auditability. So um in general a lot

of VMs production grade VMs industrial sort of like um scopes VMs are massive especially when we're talking about things like resp um these things are really really large and we want to make sure that they're tiny and and that's because bugs exist and um they will keep on existing and the bigger it gets the more complex it is and so you know I put in a bunch of things I don't know if any of these are really controversial but um this is why this is why we're going sort of go down the the theoretical work that um that we did here. So okay so um this is actually fundamentally a problem of code design um and um so really um you know you start consensus transaction engine

layers um and then really for us it's just about the what ISA are we going to use and we need the execution of memory traces to have very specific properties um and also what this does engine needs to be and this is stuff that you know people have been working on a lot um but I want to sort of make clear that what we're doing here is really fundamentally miss this. Okay. So, we're not going to touch any of the engines. We're not going to touch any of the machinery. We are going to try and start from a first principles approach to designing an ISA which makes our life easier downstream.

So, we want to make sure that if I have certain properties to my ISA, this thing is only going to require an extra three or four gates uh in addition to it transition function to be fully memory and execution. So, this is This is sort of where we cut off. Um, and it really just boils down to what outputs are we going to use. So do they need one, two, three constraints and what the degree of these gates are. And then fundamentally what the memory orization is that we can use. And and overall in this talk what I really want people to understand or at least be convinced of to a certain degree is that we can actually use the same process for both memory and execution. And this sort of goes back to the modularity um concept that you know we want to have

that we want to make sure use exactly the same audit constraints as much as possible and this is important because um it's less code to maintain and there's a much lower surface area for issues. So the the first really existential question is what is the representation of computation and and and that's really the question that we're all digging at the very basis. So if I have a program um what's the mathematical object that fundamentally specifies what I'm trying to get off. So I'm giving you a sequence of op codes right which is the program execution and I'm giving you a full object of memory and the your work here is to ensure that these things can be

encoded in some wrap or or or some you know rank one constraint system or something um such that you know only the valid programs actually uh verify right and and and this really is just a question of abstractions and and overall I felt that these you know this work and pretty much work that everybody's done the two fundamental objects that matter are the execution memory traces and I'm pretty sure somebody who's you know done a lot of research into PL etc would say that every program for every type of ISA can be composed in this way so that is really the starting point so um I just kind of want to talk a little bit about what the objects are here so we have the actual initial opose so this is stuff

you code up right um this is your um your actual program. Um then you have the initial input data that comes inside. So it's a program with with some starting points um starting data points. Um the sequence of output resolution is when the program uh starts, right? Um you've got the initial up codes, but you start pretty much uh resolving them, right? And and as you resolve them, you're making a sequence of up codes that are coming out of your program. So this would be for example, if you have a for loop um in your initial input data.

Um this is just the unrolling of the forum, right? And so this is external sort of like computational creation of more outputs by resolving previous ones. And this is what for example abstract syntax tree would be doing. You would be mapping these things and this is sort of relevant intuition for us to unlock. Um then you have the final output data. So it needs to output something and you need to know you've terminated. I know this came up a little bit earlier today. Um and in the memory traces things are a little bit easier. So you have your initial memory register value. So how it starts and if you're going to do read write um you just need to keep track of that and and you need those two tables to be consistent with each other and there's a lot of work that's being done

there. So I'm just going to go through that really fast but this is sort of as generic as it gets when it comes to um to abstractions. So um yeah so this is probably uh very well known to everyone. Um the idea is that you know um we have our execution table, memory table and we're just going to add a bunch of columns in the end and these columns are going to be the input out output columns. This is like offline memory checking um fully generic with a star in the sense that um this this really is got nothing to do with what's going on in the execution memory tables.

It's just its own thing. It's just a bus that connects the two parts. And the way I like to think about it is that in the execution table, we're asking questions. We're saying, well, you know what, fetch me part K of memory. Um, and in the memory table, it's checking that part K is actually indeed the correct one. And there's an IO consistency check, which we use for, right, and and load up sort of related um kind of concepts in order to sort of reconcile those two things. And usually in the responding model, every request needs to be answered and Those answers need to be consistent.

Now, I know this is not very exciting, but I kind of want people to see kind of how we arrived at our idea. So, the consistency checks here, you know, we we we in a sense, you know, this is this is the the generic way people do it. Um so, you know, we use all these techniques. you know the the execution table um basically commits to the elements of your uh the elements that you've you're requesting. it gets a random value, an extension field. Um, and then we're building accumulating sets, right? Um, and in a sense that what what we like about this and why I think this has sort of become the standard in in in the ZK VM design

is that it's a fully local process. So, as we're going down the rows of what we are asking, we just aggregate a multi set, right? We're we're taking our multis set and then we're adding elements to it based on whatever kind of flavor of or or similar systems that we need and and that's just enforced by constraints in every row, right? So every single row has basically one big addition constraint and it's just putting it in there and you know whether you use multiplicative or sort of the the more uh recent works, it all really just follows the same underlying structure and and really um you know um the the the final output is just one single extension field element which has every single thing inside it that we

have asked. Then you know we feed that requests to the memory table and as the memory table goes down this accumulating will set is deconstructed. So every time we hit an element of memory um we we pull it out and we check that the optimistic thing that was added in the execution table is exactly what is being verified at that memory record. Um so the proofer is deconstructing the accumulating multiset. Um and again it's being decomposed locally. The randomly combination is unrolled. is basically the inverse operation of what we are doing in the execution table. And so the final uh output title is need to equal zero. So everything that has been asked needs to have been answered. So we start

at zero at the top. We're pushing everything into the accumulator. We get something out that is pretty much a massive aggregation of every single request we've done. We take this at the top of the memory table and we unroll it down and we go down to zero. And if this is equal to zero and that output is equal to that input, I'm pretty sure I can convince you that everything that has been asked has been answered. So that's sort of the starting point. I kind of want to take a quick pause. Does this make sense? Does this compile with people? This is normal. We this is the the kind of stuff they do and various other sort of generic modular approaches. So if people don't don't see it, I think it's a good time to sort of double click to Yeah.

what you just mentioned with the with the things that you have on one side that you send on the other side and then you check at the end of the proper number. This is quite similar to the log or approach right where you have one additional column when you run like kind of the sum and you check at the end that your sum is one or whatever. >> That's exactly right. Yeah. The only reason I'm really bringing all this up is because I want to show you what part of that process is powerful and and what we have identified.

What is powerful is that you are doing the local decompositions which is a big deal. That's one gate, right? Um and then you're doing one final global check, right? And that's pretty much all you need. And in a sense we kind of want to use this exact approach when doing everything else as well. This is sort of why um why why I started with this because this is relatively uh well understood. So okay um so the costs for this are pretty small. Um I just put them here. K here's our extension field but I don't think I need to spend any time with that. It's basically free at this point. Right? So you're just adding the number of columns you're adding on

both sides is equal to the extension degree and um you're just doing the aggregations and all you really need is that one alpha and beta that needs to commit to the IO so that you can do the wrap and you can do the log. Okay, so this this is sort of the starting point. We're pretty much going to do the same thing downstream which is why I'm bringing it up here. Um but this is sort of um in my view already like quote unquote optimal as like an approach to deal with um to deal with IO. And so the question that this leads to is well this was fully local updates right that we did before and that's why this was so cool and so nice. So the real question I think when designing an ISA when you

have the full canvas to actually do whatever you want is well actually can I make an ISA that I can verify with only fully loable transitions and that really ends up being I think the most important property that an ISA can have because if you do do that um with some additional ingredients that we're going to get into in in this talk then you can really use the exact same structure but on the actual ISA itself and more specifically on both the execution trace and the memory trace and this is why I'm not differentiating between the two and double clicking into exactly how we build our memory trace and what the specific uses of the indices are etc. So I want to show you a generic framework

so that if you can enumerate your execution trace and your memory trace in a very specific form that you can use three or four gates to do the whole thing. So that's what we're going to try and do and hopefully I can convince you that this this sort of is is interesting. So that's what that's sort of the starting point of the design. So this is where we sort of get into this idea of stateful verifiable traversals. So uh I hope we're for not putting too many equations in there because they're very odd. Um and I I think you missed the point. Um but one thing that people should notice is that there is actually one very uh well understood

uh mathematical data structure which has a fully locally updatable uh transition function and that is the tree data structure more specifically um the the computational process of verifying every element of a tree. So when I'm doing breath first search for example I start at the root and there is a very deterministic specific process by which I access every single number. Now of course bread for search is just a search function. It's not really checking any knowledge or doing any anything cool.

But the key is that as I'm going down this knowing what the next thing to pick is a local constraint. It means that I know exactly by just looking at this. No need for any jumps or or any bookkeeping or anything that's like extremely heavy on just keeping track of. I know exactly where I'm at. I know exactly when I need to go and I can check this very easily. Okay, so that's one thing. So what really um what really this kind of leads to is an idea that we had is that well okay I have I have a treat reversal that I can do. Now if my execution and my memory traits are trees. Okay. And the way that I can check if they're valid

uh is just by checking an extra set of local constraints on their labels. Okay, so they'll have a label which is their off code and their output. So their result output. I've got this written up in the next slide. Then by using sort of the label of the parent and the labels of the children and only doing constraints on that local part, can I actually fully verify my ISA? And even more so, can I fully verify my memory? Because if I can give you a really cheap way to do this for an arbitrary binary tree or energy tree, then it's just a a plug-and-chunk situation where I'm just constraining that really tiny small thing, which in

my view is very powerful. When you say tree, do you mean like a perfectly balanced tree or do you mean like one that is very very ugly and very spy? >> That is great intuition, but I mean a proper enory tree and and we're going to go into that because you're hitting exactly at the part that is important. This tree needs to have structure and and this structure needs to be that at every node the total number of children is fully initialized and it's always equal to um a certain value. So it's an enter tree that's proper. Okay. So there's no sort of park trees etc. Like we we are using this. Now of course with some work uh with some work you can sort of pan it and and and do things and

these are resolvable problems but but it is a concern that that we can we can talk about. Yeah. But what are the tree? Because if it's instruction when you execute uh it's linear. So it's a tree but it's degenerate because there is only one instruction that Yeah. So, so I'm going to go specifically into into an example, but the way that I think about it is that um every node has uh an op code label, right? And it has a data output. Now, we can nest uh op codes in each other, right? So, if I have the addition op code, the addition op code would be over two other variables, okay? Which could also be additions of data.

>> That would be a tree, right? In the sense that you have the plus at the top with the output that leads to another plus with the two inputs and it sort of does it like that. Does that make sense? >> Uh it's a duck event. >> Yeah. Yeah. Yeah. It's a D. Yeah. Uh but I mean a proper entry tree is the is the precise formulation for formally treating this >> because um let's say you have a variable X can be used uh in multiple places. So that's the tree. Well, I guess it's just semantics.

>> Everything I'm going to talk about today is semantics, unfortunately. Uh, but you're right. And the the the thing I want you to build in terms of intuition for that question is that the execution trace is completely independent from the memory. So every single time that I use the same variable, let's say twice or thrice, I'm using the same memory or two or three times. What I'm actually doing there is not messing up with my proper tree which I need to do all this all this fancy stuff. I'm just actually doing a request to the memory tree to give me that variable. You see what I'm saying? So I have a memory tree that's fully structured with proper entry tree.

I have an execution trace that's fully structured as such a tree true. By the way, the ends can be different in the two and they fully depend on the ising and the memory orization you use. And every single time that I'm asking things from memory, I'm actually like running a special offload where I'm just pulling that out. >> So, I am still in the proper energy tree world, but I agree with you that if I was going to sort of merge these, I would then get into and I actually, by the way, did fall into that trap for for a couple months and it sucked. Um, but but you're right to to sort of inquire about that. So, the real claim that I'm going to make is that um there actually do exist minimally to complete ISAs that are actually traversible and by

traversible I mean that they can be fully verified by just doing a walk over a very specific local transition function over both memory and execution and I know this is a strong claim um but bear with me and hopefully um you'll read the the paper and be convinced but that's sort of the the big idea okay um yeah just a small comment this is quite similar to actually how a frame smart contract are stored because you have account tree and a storage meal tree as well. >> Yeah. Yeah. Yeah. And and this is actually why I I thought it was very exciting um that the kind of stuff that we ended up getting out of this um sort of look very similar to a lot of the data structures that are used in

Ethereum and even more specifically the signature scheme that lean is supposed to work with is also fundamentally um a proper tree and and you know I cannot claim to know sort of if there is some sort of holy grail design right there and and maybe there is I'm always optimistic but I was very reassured that those things were uh were simpler. So okay, let's look at some a little bit more um I mean stuff. This is pretty much me writing down everything I told you about what these things are. So in a sense we want to be verifying tree walks over label nodes. Um and we need to have like a proper tree data structure to do this over right yeah >> by by property you need has at most children or have exactly

>> exactly but we can have the child as a no sometimes and this is not um but in a sense it's at most and non null children but for the purposes of the formal arguments they are proper trees but um because some op codes may only require input from let's say may have different fan out um then you p the rest of them as zero but that's a great question so uh yeah okay so this so we define this data structure that we call the recursively verifiable proper entry tree so I'm sorry for the name we couldn't find a better one uh over transition function TF which is you know you've got the the underlying tree. So every single node except the leaves have exactly children and so each node has a label.

So this ltel is sort of a tuple of s and out and s is the state value. So for our case would be the output selector index. So we're working in the one hot encoding. Every index is an integer and um s basically tells you which one that is and the output value is the output of that op code on on everything else. So it's the actual final value that comes out from for example doing the addition on the op code um and sort of feeding that upstream. Um and so in a sense the key property here is that and this is the local property that every internal node the transition function so the state and the output in addition to sort of the outputs of all the children

because all the children of it are sort of the recursive further depth. So if we take all of the of the children which are the inputs to the current node alongside what the off code actually is and its output that needs to verify. So that is already set in stone by your state. So if this is the plus it would just add all the children and double check that they are equal to out if that makes sense. Okay. >> Maybe just a question about the fact that sometimes you need to pat. Does this increase the cost of your proof?

No, because well, we'll get there. We'll get there. That's a great question. Um, so hopefully people will agree with me that um at least at this informal level, the above data structure is basically fully locally verifiable for this resolution function TF. Okay. And the real question then becomes can we use this data structure to encode an ISA trace and and a memory trace because if we can and I can convince you that this thing can be done with two or three gates then I I would compelling sort of use case. Um but but we'll we'll get to the sort of the important technical point. So I apologies for the latte. Uh but um there is actually a very simple thing

that makes what I'm saying concrete and it's the people not you example right and and and sort of this you can be thought of as like so I'm building an IA that is really stupid and it does only two outputs okay it does the decompose output and it does the halt op code okay and I'm going to use this um to along with a specific transition function to verify uh that some uh the f for example uh and n here are basically Fibonacci okay so n and f of n all right so I'm going to start with a certain value so the fourth number which is um you know uh f= 3 and I'm just going to go down and double

check that uh indeed at the top what I have is actually a number okay and and in a sense what I'm doing here is I'm saying all Right. Um, so I'm going to uh run a decompose on this. Okay. And this decompose leads to two parts because at the top when I run decompose the transition so the transition function takes in decomposes the state and when it takes in decomposes the state. What it does is it in a sense splits it up. So this is so the n= 3 f= 2 and n= 2= 1 are the out right from previously. So this is sort of the outputs of the the further nodes down. And the point is

that that transition from the top node to the two bottom nodes um is local in the sense that it checks that the top thing is actually equal to the sum of the two. So 3= 2, right? Excuse me. >> Yeah. I hope not. But maybe um Yeah, sorry guys. Uh, but I I hope that this you get it though, right? >> Yeah. >> I can't help. Um, so yeah. So the point is that like what this demonstrates, right, is that if my op code here is sort of so pretty much my initial

program is decompose n= 5= 3. Okay. And what that is supposed to be checking is that actually you know that is a correct Fibonacci tool as we define up there. Okay. So what it will do every time it runs decompose it's it's so we defined what what what the transition function verifies um when it sees decompose and what it verifies is the sum of the two ones lead to that. Now if it's a 21 one or a one one then the state has to be held. We can constrain that too. Again, we're talking one gate here. Okay, we can constrain that too. So then it just ends there. It it won't ask for any more children. Whereas here, it's just going

to keep going down and we're going to go from decomposed and you need to provide these two elements. And because there are two one and a one, it's going to work out. Yeah, right. How do you how do you know the two one like should there be a proper tree? to help you. >> Yeah. So, so the so yeah, so I mean the the point is that you can you can basically have a special symbol for null and because the halt states are actually identified. So every state that is an ending state, we call it terminal state and we know these from the beginning and I'm going to actually very specifically like um tell you um exactly the

restrictions that we require on on these transition functions because it's not a free for all. Um but when these transition functions are what we call terminal transition functions then we know exactly that if any of the children are not no ops then it fails okay and that's already provided to you by your ISA okay and we know this from the beginning and this restricts the the design space a bit but does it in a way that makes life a lot easier. Basically the key property and I think this is actually the next slide is that for every op code the fan out has to be possible. Um okay so this this kind of goes to your question. So are any really traversible is really the question

because if they are traversible then we should basically look at the cheapest locally updatable walk and just implement. So well what we found in this paper was that there are specific sufficient conditions for your ISA to be traversible in a cheap sense in a sense that the questions you're asking and the question you're asking are not a problem and not show slumpers. Yeah. >> So for Fibonacci specifically do you agree that we can have a local only computation with linear tra like what does the tree structure give us? So the tree structure gives you um an ontology. So a structure by which you're in so it's basically like a PCB

if you think about it like it gives you a low a recursively verifiable way to check people matching. So in the same way that when you write a piece of code that is recursive that is very small right but then when you're actually executing it you have to unroll the whole thing much here we will unroll the whole thing op codewise but we still keep the compact nature of the recursive part and that's the big idea that we are not like we are leveraging the fact that it has recursive structure So that we can have very very few constraints that are then recursively

checked at every level. >> Justin proposed is that the head of what we are doing here. This is quite compact because thanks to to the leaves and the tree structure, you have something with a very small hay rather than if we go via what he proposed, the hay will be larger. Right. >> Exactly. So you really just want to make sure that you reuse as much structure as possible in a recursive fashion because that saves massively on constraints and bookkeeping. That's the idea. And the big question is if Fibonacci is a contrived example, can we do this for something that isn't contrived?

>> Does this future affect you a lot on the proof side? >> Yes, >> it's a proof generation. It brings some benefits. So the main benefits you get are you have a very small number of gates. So for knock we basically were able to get to the same level as the startware um the cyro number of gates um we have degree four gates for that specific ISA and the total number of columns is very small um so we're talking like 20 30 columns something like that it's basically really really small and every row is a different I'm going to I'm going to show you the generic design of the table right now. But the the main thing you win is that you make

it really small tables with very few constraints and it's basically optimal in a sense because every row is an op code. So there's no moving stuff around. It's just the minimal number of information that we need. So um yeah, does the simplicity of the structure give you benefit for verification? >> Yeah. Well, the the it leverages this fundamental concept in the stark and the air world where the transition function needs to work for every row.

If it's recursive and we know that the recurs the recursive nature of this thing is enough to prove veracity then the only thing we need to do is have the local constraints for just one um for for one transition which are way fewer than if you start moving stuff around because you you you basically get rid of every bookkeeping thing like I put that there so now I need to keep track of that and if I don't keep track of that correctly, somebody's going to inject something in there. So, it it gets rid of all of that and makes it really simple. And I think at this point it's important to just show you the canonical table representation that we have. But uh so okay, so this is the

quote unquote formal definition. The point is so nice to be traversible. What I mean by traversible I say one there's a bjection between every valid program, right? every valid input program that I code and input data to these um uh recursively verifiable proper ny trees. Um in a sense what this means is that there exists local transition functions for the memory and the execution table specifically uh and some n1 and n2 um you know tree number of tree branches um such that these are one to one mappable.

So for every program and every input there exists a unique um a unique tree of the special type that we have um that um that is exactly what the trace is for the execution and exactly what the trace is for memory and if I have if I can show that for my ISA I can generically compile it with very few constraints. Yeah. >> How many out codes do you do you have because you say that each node is one of code but how many out codes? Sorry. So just to be clear, each node is the execution of an op code from the set of all op codes.

>> Yeah. And how many op codes in total? >> Um you mean how many op codes does the ISA have or oh so for no for example has nine op codes. >> Uh but and and I think the op code 10 is read write. Um but the minimal touring complete version is three op codes. It's the memory lookup op code and then two very specific uh recursive ops. I have that on the paper. I can pull that up after the presentation if you want to see it. I just purposefully did not talk about knock because I want to make the point that this is generic but it's free output. It's called baby knock.

>> Yeah. So like the thing that confuses me like um if you just consider uh the execution of a program uh and you view that as an algebraic circuit then like fundamentally this is already like a tree structure to some extent like that right but it to me it seems like it doesn't matter what the op codes and therefore like kind of the nodes are right because fundamentally any op code can always be written like a tree like that or well Okay. To to a large degree, you can write any programming language as an abstract syntax tree, which I think is what you're getting at. Um that you can sort of write it like that. The key though is that um you need to be a

little bit careful about the interdependencies between those. What what we're saying here is that I start at the top and I follow the terministic process as I go down everywhere fully execution. Every time I need to talk to memory, I have a special that I I fired to talk to the deterministic memory as well. It's a bit more constrained. >> The that seems to be the distinction between the as of a program in the source language and the you know tree you would construct from the actual execution you saw you know during your execution.

>> Yeah. I mean I I believe that you can always map um the the the actual execution tree to a version that we can compile very trivially. I'm just making that claim for generic things because there's weird stuff going on with some things like for example there's like like weird loops and lists that sort of give you corner cases etc. So we just built it in a fully like recursive bottom up way. So if you read the paper um we basically um start from first principles and we build out exactly what that tree looks like and we don't start from the PL perspective where it's like all languages can be described by this ontology but I I leave it very open and plausible that you can the vast majority

of languages and put them in this world. And then the question that you have is how structured or unstructured is their memory and whether you can actually completely disengage the question of memory queries from this specific uh transition function in the execution so that you can definitely get just two walks and be done. I don't know if that covers you >> more or less. >> Okay. Um so yeah. So okay. So that's the say that we want to find um and so um okay so this is goes back to everybody asked us this question already which is you know exciting um so what are the sufficient conditions for this

thing to be cheaply verifiable cheaply it's traversible okay and basically it's actually one very simple thing um which is that like for every off code in the ISA so every state variable label for our node that state variable is get has all the information I need to know how many children it has. Okay. So I cannot have an op code that if the first value is seven it has seven children and um you know if it's not it has two. It always needs to be a constant number and that's because then you don't deal with problems like what you mentioned like

the tree can change and you can have many different like depending on variables you can have different sizes of sub trees etc. What it does however not resolve and this is not resolvable is that some of them need to be no ops. So some of the children need to be null but you know exactly which ones they are because every op code has a fan out value which is known beforehand. So if my op code is you know op code one has a fan out of three in a in a tree then I know that only the first three are not no ops and then I explicitly check that the last two are no ops. Okay. So I'm done with that issue. Yeah. But are there ISAs with a variic number of um arguments?

>> To be completely honest with you, I didn't actually double check the risk by spec. Uh maybe it's always three or four things. >> Awesome. That means it's canonical. Uh it means that this is fundamental as a as as an issue. Yeah. >> How do you determine the of your tree? Is there a specific? Yeah, it's the maximum uh fan out the whole top. Yeah. So in a sense like this we could go on and I could formalize for you show you how we do it in knock etc. But we have that all written up like we can we can talk about it offline but basically your ISA if it has unary out codes binary codes turnary

out codes is basically the maximum over that. That's sort of the maximum that you get. That makes sense. I understand how the um the tree for the instructions works but how does the tree for the memory look? >> Okay. Uh that is uh the hard part. Uh and um unfortunately I I that is where you need to do some more ISA specific work um to make it happen. So for not we were able to do it and and I'm very happy to discuss this if people have interest um and sort of get together um like a really quick overview of how we managed to do this in no but the the techniques are very generic but you need

basically one piece of special sauce which is that um you need to label your tree in a specific way. So you need a local update function in your tree as well um and In a sense, the way that we do it is that, you know, I start at the root and the reference of the root is one. So that's it its address label. And then if I go left, I double that. And if I go right, I double that and add one for a binary tree. And that's like a basically a purely local update function. And then I use the fact that as I traverse that tree, I can locally update these addresses from the

beginning. So the way that it works in knockch, which I'm not going into here, but the way that it works in knock is that well I start uh at the top and I have a query right from the execution table and the query in the execution table says well okay here's the root um here is the address that I'm looking for and this is the value I posit to be true and you're using this your execution table works etc. Right? You stick this into your IO thing that I put at the beginning and then you know you start at the top and then you're going down, right? But what are you doing?

You're traversing a tree, right? Where so in knock the the memory is a tree and the addressing is the one that I mentioned. So the the I call it the collat addressing scheme, but um it's it's actually kind of messed up like how powerful that is. Um but uh and as I go down this tree uh I can actually keep track of that locally as well. So at the top I start at the rooe and I say okay this is the root. So I start counting and then as I count down I I bring down all these things and then when I hit the exact address point I do the check and I remove the whole memory query from uh my accumulator.

This is really high level. I can I can explain to you offline but um that's that's the way we do it um in knock. And by the way that is modular like it's not specific to knock. You can just slap that addressing system into what you're doing. Yeah. >> Okay. Um Okay. So, so the only thing I got for you here that's a real gadget um is this thing. So, the semantics of how we do this reversibility. So, um we need a local stack data structure. Um and the way we do it is that every row is an off code uh resolution. So, it's the the selector is the op there, the child node information. We put all the child nodes there. We do the X in there for the transition. But then we just need three

things. So we need the line number. So this is the row number I which is encoded as the exponent of some alpha which is taken by the randomness. Uh and CT is the total count. So the total number of nodes that we have been observed until now but which haven't necessarily been resolved. Um and the point is that updating these two things is a purely local process. So every time you go down to the next row, you multiply ln by alpha and every time you go um uh and and you'll see what what CT does, but this is basically emulating a stack. Um uh so yeah, so so the process is basically that um so the process is that we're we're updating the line numbers um and we're keeping them in

this unique representation. Alpha is you know the response from the verifier of the commitment of the underlying table. Um, and so the count is the only thing that's really new here, which basically says that um, the count is how many new op codes now do we need to check from the stack. Okay, and this is just like a like a hack way to build a very very efficient stack for this, which is all you need in order to do the DFS. Um, and then finally, the prover builds the accumulator using this alpha. And it's not the same as in the IO setting. And you know if I have a couple minutes I can tell you what we do. But the point is that this creates a stack and every new row we pop from the stack. Um the value that was indexed to be resolved at

that line if that makes sense. So um I have it right here. Um so yeah so the the accumulator is really the key the key new gadget here. So it keeps all the children that still need to be resolved. Um so we remove like you know every time that we reach a new line we remove from the accumulator the node committed with that index which is unique. Okay so we can't cheat and then we add to the accumulator all the child nodes that are non- terminal and then we give them unique indices that strictly increase. Okay. And then you know when we add all of them it's the fan out. So that's how we get the CT. Okay. So this is just a local way of keeping a stack

that only requires two columns and two constraint gates which is very cheap. Um basically it's a K store the keys are the powers of a and with a couple of gates that's all I need to do my walk. Okay so that's the the key sort of technical idea here and I have this actually done for your match even though it's wrong because I got the end wrong up there. Um but basically here it is right so um the state is the first thing so this is decomposer hub it's it's one hot encoding so that's easy um the label is basically the data right then we also have the data for the left and the right child and this is sort of the part I want you guys to to gro so the first

line number is alpha to the zero at the input right so that is always multiplied by alpha as it's going down that's a unique identifier and the count so is preloaded at the beginning as alpha a commitment to um the first element. Okay, so think of it as seeding my my program with its initial input. And so what it does is in the first row it pulls that out. Okay, and moves the and moves it into the label. Okay, and it pulls it out because it has alpha as the leng. So it pulls out the alpha value from that. And then because it has to put in two children, okay, the decomposing the half, the count goes up by two alpha cub and then it adds into

the accumulator um the the index of alpha squ which is the left and the index of alpha cubed which is the right. Okay, then it goes to the next row and the next rows ln is alpha squ. So it pulls out alpha squ decomposes that pushes that back in. Okay, updates the total count, does the whole thing all the way down until the stack is empty. And by the way, this is important because it's a very nice way for us to make sure that our computation is terminated when the stack is done.

It's a purely local way of verifying the termination of the whole stack because there's literally nothing more being pushed in. There is no special thing we need to do. It's like a very simple process. So by the way this allows for infinite programs too right in because you know whenever you have any program you come up to tell it terminates it's a halty problem right so it allows for infinite programs so it is fully generic of course for us we cut it off after a certain number of rows but that is the process by which we do the walk. Yeah. So if the tree is nary tree, >> yeah, >> you have constraints between each um of n consecutive rows or like maybe n plus

one consecutive rows. >> No. So so all constraints that that's the key thing. You don't need that. You don't need that because you're pushing them all in with unique identifiers and these unique identifiers specify what line they need to be resolved down. >> Okay? So like it's you give the Are you optimistic optimistically? And so so here there's nothing optimistic going on. The the point is that I'm I'm updating the ln in a verifiable way. And then what I'm saying is I'm updating the count in a verifiable way too because I'm multiplying it by alpha to the fan out which is already known from the beginning for the specific op code. And what I'm saying is that in a sense um every time I need to push children into

the stack, I don't want to keep do any bookkeeping. Like that specifically what you asked is exactly what I don't want to do, right? I don't want there to be any crazy interactions between everything. There's literally only two gates in this thing. So the point is that I'm actually taking the um the output. So So the hot 21 and the half one, I'm looking at ln that's alpha. I'm taking the first one. I'm multiplying alpha squar by alpha to the one and I'm adding that in. But the key is that the only thing that can be pulled out is the one that actually matches the line number. So the point so the moment I'm pushing in alpha cubed

time that thing, I'm literally saying the only way that this whole thing is going to verify is if in the alpha cubed line I pull that one out. If I pull anything else out, it's not going to verify. >> That's the key. Like you really honed in on the key point here. It's a purely local stack. By the way, I can do five different programs like this. I can just instead of having alpha* r= 3, I can the z can just be alpha plus alpha square plus alpha cub. Like I can see many parallel programs with this. I don't need to do any bookkeeping. I can literally just do the walk and it's basically a walk over a forest.

>> Yeah. >> Yes. So don't take me wrong but I really don't understand the difference with a lookup argument that needs to be zero at the very end and which is zero if you have I mean at the end added fraction and removed fraction in independent lines. So I'm probably missing something but I don't see the difference. >> Well these are different objects right? So here um so they're using the they're leveraging the same sort of power >> right? Um, this is why I I started off with the log up idea as a gadget. The the difference here is that I'm not like log up really doesn't really make so I'm using the logup idea in order to sort of add to my accumulator. The only

difference is I'm changing bases and I'm adding it. I'm I'm using I'm indexing by powers of a random extension field element to do that. But you're right that it's the same power. The thing that makes it in useful for me and in my opinion model is that I'm constraining what I can pull out of this based on a unique value at every point which then allows me to push things into the stack purely locally so that it can ensure that they get read later. It's more like a how do I leverage the log power in a way for me to do local updates. So when we talked about hand checking things before and you said I want to remove the hand check. So you sort of do this here

to remove the hand check and you want to make sure that you consume the value that has been added before thanks to this changes that you add to the value. >> That is correct. >> Okay. >> And if I understand correctly the difference with the log you replace the multiplicity stuff by some random challenge. >> That is correct. So I I haven't written this up uh as like a standalone gadget but uh basically what this is is log up but with a different basis and the basis is the powers of alpha. And by the way if we're going to double click into this in no this is ridiculously powerful because it allows you to batch queries because you can just the sums of alphas and you can do the plus two plus one thing in batch which is where you get

optimality for the knock queries. But that that that's we can we can talk about that. Yeah. >> Um I've linked some code uh because I use this technique uh but uh in a completely different context for different uh to build uh trees of workers uh that communicate with minimal uh but you have this um so the reason I used that was uh to have an implicit stack uh using the indices uh to the two multip by n + one is a child. n + 2 is a child and the parent is n / two and well I have a 100 line example on how you do traversal uh efficiently and range uh

traversal both write first um and death first if you want to look channel >> that's excellent and one thing I point out is that this enumeration process of 2n and 2n plus one is exactly the labeling function of bre of depth for search so if if you do depth first search and you put these in in in sort of increasing order. Um the the order in which it hits all the nodes is exactly that increasing order. So it's in a sense very canonical in that sense. Do you guys have any questions? >> Maybe last question. So how do you infer the the count colon here?

>> So how do you prove that the count is greater than the in? >> You don't need to do that. You don't need to do that. Um the the point is the count in a sense you can think about it as the pointer of my of my stack right. So like I use the count to add things. So like um let me let me see like so current. So so okay so we start with the seed and my count for seed is alpha which means that I only have one element inside. Okay I go to my I go to the the first row. So well yeah the first so the first is the zero row then I go to the first row and I the only thing I can do is pull out the thing that is indexed by alpha right so I have to pull out the right thing

which is what I seated it with now I know because this is decompose that the final is two okay so I know for a fact that the previous count needs to be multiplied by alpha squar okay so I can update the count locally but then um the point is that I take the previous um the previous count and I need to use that as the basis to push things on it. >> That's why I need to keep track of it because I I I start with alpha, right, which is the the previous count. And then I say the left child will be indexed previous count time alpha. The right child will be indexed previous

count time alpha squared. That's why I hate the count because it's it's just a it's it's the it's the it's it's the address variable for my stack. >> I need to think about it. >> Yeah. By the way, all the proofs are online. So you can you can look at that too. But but the point is that in a sense like look at this. So my count here is alpha to the five, right? So then I pull out um I pull out the so I pull out my alpha my alpha squared that I got from the floor right 32 um but um and you know and I have the children sorry I like so if you look at the hot one that's that's a better way so in the

hot one count doesn't change right so we're not changing here because this is a terminal state so you're not pushing anything more in the stack so the total number of elements that have ever been pushed in the stack is still five. So we don't need to add anything more. So think of it as like a two like two pointers, right? The count is the pointer of everything that has been added. The line is the pointer of everything that has been resolved. So the way it works is that like I start somewhere, I go up and count and I go up in line. I push the thing. Count goes up. I take the next thing from count.

Line goes up. So it kind of goes like this. And at the end they need to resolve with the same thing. Happy to chat about it afterwards. Yeah. If the ISA has some kind of memory, yes, you can understand correctly. Some nodes, some leave nodes with memory accesses. Um, so leave nodes. Okay. Oh, the execution tree. Um, there are terminal states.

Yeah. And if they want to do computation of two memory cells addition. >> There will be one node addition and two nodes that each look into memory. >> Mhm. >> Yeah. >> And so there will be some kind in the execution trace some kind of column allocated for the memory. >> That's exactly right. That's the IO stuff that in which case I don't see why we would need a second tree for memory.

Isn't it simply lookup problem? Like we you want to commit the memory and then you want to ensure that some index column and some value column has coherent access. >> Yeah. So, so you can definitely design something that completely abstracts the out of there. Um the reason we didn't do that was mainly because NOC had that memory address space and we wanted a feature complete system. Um but secondly, so this is where it gets a bit more subtle and this is something that for your use case is something to elucidate. But the idea is that if you want to read write memory, you basically need a way to arithmetize RAM.

And the tree structure is a very nice way to do that because if I'm writing things to it, I can just take two already existing nodes and sort of like link them up in a forest. So it's feature complete in that sense. But if you're looking for a super minimal thing that has really stupid memory that is read only, I agree with you that you can literally just do a look up and be done. >> Okay. >> So tree one committed memory and you're going to look up for some into this memory. >> Yeah. All we have to do is update the IO gadget at the beginning. That's why I kept it generic to the one that you want. So it's fully fully usable um with any kind of IO system as long as everything that's asked is responded to.

So all our formal results do not actually are not opinionated about the structure of this IO. So you can absolutely roll your own. What I'm what I'm saying is that you can do the same tiny thing on both memory and um and execution. And that's relevant if you want to make your memory to read right as well mostly. >> Okay. So, so the memory tree is useful first if you want your memory read right or second if you want some address space in your memory. Correct. >> Yeah. So, so the memory so so this is the the reason I didn't go into this in detail was that um one of the nice things about having a tree memory in something like no is that in a sense it's it's it's all fundamentally one

variable. So even the internal nodes in memory are still data points because they're lambdas. So it's like you can pull a program out as well in like if you if you don't pull just leaves from memory. You can pull out parts from memory that are more complex and it's sort of like looking up a library. And this is really cool because you know you can have like specific subsets of memory that are programs and you can pull these out in memory and stuff but that's that's complicated. That's higher feature stuff. If you want the most basic thing, the lookup does suffice. But but because we wanted to make a generic thing for capturing everything, that's why we we also put it in there. Uh yeah, so overall these are the costs. It won't be a fest commitment and three K columns. K

is the extension field. The transition constraints are three degree 4 gates and the transition function constraints which are black box which are the state constraints. and and if we're using one hot encodings and we have three off codes that's like what two gates three gates. So that's why I'm excited about this because you pretty much get everything here. You offload all of your costs in something that a start or an AIR system can absolutely handle um by putting everything in every single row. So you fully leverage the fact that um the start security property is that this constraint system applies for every single row. That's the part that you really leverage here you that's how you double sort of your power um to use this

recursivity property because that's actually how stark a is defined the dark a says that um you know the polinomials I have at every single row sort of adjacencies satisfying a local transition function that's that that that is stuck right that's the whole thing so we're actually just taking that blueprint and we're saying well actually I'm going to make an ISA that exactly looks like that so that every row is an op code and the only thing we need to check is these local constraints and the start does all the heavy lifting in the engine. So you don't have to worry about keeping track of all the things and this is pretty much all you need. Um and hopefully I've convinced you that the only reason we can do this and it's

not cheating and crazy is because they're all local. Yeah. >> Just a question. Is there a maximum stack depth that you can handle with your framework? >> Yeah, that's the closest to the something at the end of the >> Yeah. So there's a bunch of bookkeeping stuff you need to worry about. So the maximum size is the total number of rows. The total number of row maximality has to do with the set and co- sets that you use for your underlying thing and the uh like all that stuff. But that's really the only limit. Of course, there's security bounds, right? Which is one over the size of the extension field because um you know that those are the standard logout security bounds um which still apply here in our case because um you need to make sure that the underlying field that you're using is

big enough so that sharks simple can can sort of save you. Um, but you know, as long as that is resolved, so as long as it's big enough, okay, and you're only really paying for that in columns, like if you're doing extension five instead of extension three, it's two extra columns. It's nothing, right? So, uh, the maximum is the maximum that your engine can support. Yeah, that's all I got, guys. Um, and that's super lame slide, but that's the that's the paper. Um, that's what I got. Yeah.

So, you can't have jumps in your ISA. Uh well so you can have jumps in the context of something like C or um you know the Cairo stuff or or that but you can like query anything you want at any part of the ex of the execution trace at any point in the memory. How hard is it to program for this I say?

>> So yeah so the this is sort of goes into sort of the UX questions. Um, a lot of software engineers are going to hate it. I mean, I know that, we all know that. It It's what it is. Um, so I would say that probably there are so I don't know if you guys know about knock, but there's there's a lot of sort of people that have worked with it and and sort of that are you know very really into it and a lot of other lisps that are similar to this that have the kind of structures are very easy to do this all have their own sort of followings and honestly I would refer to people who know about programming languages and and sort of

and sort of like development etc to sort of inform that opinion, but it's not going to be something fundamentally trivial. But this is the part that I kind of wanted to keep for last. There is one candidate of normal normal um of like you know standardly used ISAs that is fully stack based, fully typed in a way that we can use and is um amendable to being a traversible language and that's was okay. So if you really want to part then you can just take this and figure out how to do the traversal over was and because the the wasome sort of memory model and and whole system model is

fundamentally stack based. So that's what I would say is that if you want to take this to the next level it would probably be using it with something existing like that or find some sort of exotic mapping from um from risk 5 to LLVM IR that looks like this too. I think that could also work. Of course, it's more expensive because there's a lot of uploads, but you know, it's one big selector anyway. So, how big is this going to be? Not that big. >> Yeah. >> But if you don't have jumps, um you how do you do your if else? You use find like >> so so the the memory model that we are going to use in if you're going to adapt

this to LVM and disclaimer, I haven't spec that out fully. So, there may be some fundamental issues that make this much less compelling for that for that use case. Um, but the the fundamental thing that you need to do which I I don't have the answer to is you need to figure out your memory arithmetization so that you have a fully deterministic execution trace that is super cheap and super small and gives us everything nice. And then probably what you're going to have to do is you're going to have to um make sure that you're you you've defined your lookups from memory in a way that emulates um the normal sort of way that that it works. But I'm

not an expert in modeling. What what I noticed was that it's structured in a very similar way and that I think with a little bit of work you can actually get something ridiculously cheap. So I think for the lining it's possible because um you can obviously aggregate signatures two by two and then you have um uh obvious uh tree structure but for general programming um this seems very hard. >> Yeah. So really I would say that the two open problems if people want to leverage these kinds of ideas uh but also deploy ZKVMs that are usable by people that don't actually work with this kind of

stuff um would be either to have some kind of transpiler from their languages to something like this which nobody really likes to do but that's obviously the one way to do it. Well the other way to do it um of course is to try and see if you can do a bjection between something like WASU and the specific formal um objects that we have here. Um and if you can do that then you can generically compile but actually doing that mapping is sort of where a lot of the magic lies. The issue wasn't that it's um 500 lines of spec uh a lot of instruction way like three four times more than five. Um it's It's a pain to

work with. >> Oh, for sure. Many companies like um Polycarot uh has been moving was VM to Spive for example. Um yeah. >> Yeah, that's that's good context. So the reason I said was initially was because it's tight and it has all these really nice things that make it very clear what these would look like modules and questions around the jumps. But it's not really that different from finding an intermediate representation for LVM that is risk five as well. You literally just need to find a representation of risk 5 that is um bjective to a label tree and you're done in the same way. I just don't really know much about the way

that risk works. >> If stack based language uh ISA are amenable to this, I think we should just uh like the EVM is stack based so probably for CK EVM but there is only one the one from Linda >> yeah yeah no that's a very good point and and I think there is very interesting and low here about sort of what are the like can you give me a generic from a stackbased VM into this thing I think you could probably do that very easily especially given the context you provided about the way that you do the memory addressing in the EVM so yeah maybe this could be a way to do EVM really easy. I know for a fact um that a lot of the formal verification work

people are doing on the EVM also just involves making a really large transition function and checking all these transitions, right? That's that's what we do here really also. So I think in a sense we're all kind of approaching the same thing from two different directions. But again, this stuff right now I'm saying it's more speculative. Like I haven't drilled down on the specifics, but it's it's very plausible to me that you would be able to leverage this very cheap stack um and any structure you have for your EVM or or any stack based languages to actually get generic compilations of these architectures. I guess the main takeaway that I hopefully come from Vinc is simplicity is really great if we can get

it and that I think there is something here to look at because we could potentially get a really really simple system that is true and complete and and that just requires us to do the right abstractions at the memory and execution level and if we actually can do that then we don't actually need more than a couple like thousand lines of code for Yeah, I think we agree on the the design goals with with new Isa. We ended up with you know a very similar very minimal ISA. Um I think a lot of the instructions are very local like the add also have a memory. Um I guess the the

main difference that I see is just the jump. Um, but I'm I guess in what we the way that we've checked the the execution traces, it's all using local local checks. It's just that it's on the line as opposed to on the tree. I I just don't completely understand what is the advantage of the tree line. >> So, um I mean we're going to have to take a look at exactly what they did. Um but um so the first two out of the mole they also exist in the knock thing. So those are um the real difference is the the other two if I remember correctly that deal with memory that's the real

sort of part where we actually diverge in a substantial way. Um so I don't really know how small your actual uh execution trace is. You can actually compare constraints. elements committed per cycle. >> Five base >> five base field elements committed per cycle. So how many constraints do you have? >> I'm saying like 10 >> 10 constraints per cycle. And is each cycle one op code? >> Yeah.

>> Okay. So it's probably like a little bit bigger than than what we have, but it it's very similar size um like in order of magnitude for the execution table. Um actually the constraints are degree five. So >> okay so I was able to get I don't know what it was degree two or three here. Um but again these are you know like I I agree. So that might not move the needle for you guys. Uh but what I think is important is that you're getting exactly the same thing in the memory table here for us. So in your memory table, if you do it this way, you're pretty much looking at the exact same um sort of uh costs as your execution table. So the

the the difference is I don't have to deal with the overhead of jumps and drefs, but you do. And that might cost you and it's also an attack record because it's not clearly sort of like rigidly defined in a way that we can very like There's overflows, there's that kind of stuff. >> Indeed, there is one thing that is very costly currently. The fact that there is a look up from the execution table into the memory and it's like every part of the execution can touch every part of memory and this thing is indeed costly.

uh we could have some different subaces of memory to have some locality and make it cheaper would be possible but I wasn't able to find an elegant way because there are obviously ways to gain performance using some locality but I wasn't able to come with an elegant way to do it. Yeah, I know. And and that also tracks with my attempts to get something very similar uh for for this stuff. And what where I landed is that you don't actually want that service. You don't want everything to be able to look into everything else. You want to have specific local constraints that do not allow for anything other than verifying

lookups in the memory address space in the exact place where they were asked by specific points in the execution. So this is very high level. I think we can drill down. I can give you exactly what I do from the uh memory from memory table side. But basically the way I solved this problem was that when I go down the memory table, I go down the memory table once and I've already checked all the queries in. So it's a one pass thing. It's optimal in that sense. So I don't need to like you like I don't need to do Merkel checks for every new thing. I do one pass check and I do my bookkeeping locally.

Is there a simple question in your frame in your framework to how many field elements are committed by additional additional memory cell like each each time you want to if your memory has size M and there are M accesses like okay sorry A indexes and B memory cells what is the cost in terms So you have >> a in like there will be a memory accesses.

>> Yes. >> And the memory of size b it's it's linear b it doesn't a a is awesome we it actually doesn't scale with the number of queries >> but you still have to commit to the indexes you access memory. >> Yeah. So these are committed. So as you're going down your rows in your execution table, if you hit an off code that's an access off code, you stick stuff into the the accumulator. So you don't pay any extra cost for that. That's just part of the transition function. When you get into the memory table, you start at the top of the root and you keep going down. And there's like a very specific way that you only need to traverse the tree once and

you've checked every single query even with multiplicity. So if you have a indexes that you cut into a memory of size B you in your framework you you don't pay for the A >> and you pay you commit exactly to B >> and B elements in the extension in the imagine your in the base field do you pay for the commitment is a sorry is B elements in the base or in the extension field Um so so so the way that we did it um was that we had a tree which is the memory

and this is base field. Okay. The the only things we need the extension fields for are stuff that use the logup and stack based stuff. That's the only stuff where we where we use that. But there was also it's a bit more complicated because for not we use the specific commitment to um the underlying um trees but that's overkill for you guys. So it's not relevant. For instance, if we use the original log paper, we need to commit to the memory, commit to the indexes, commit to the excess data, commit to the accumulators. So you only you have to pay 2 a plus 2 b instead of >> Okay. No, now I understand your

question. You mean in the sort of in the table building phase where I am basically getting my random values. What do I committed to send to the verifier to get my random value for log out? >> Uh yes. >> Yeah. >> Okay. Because I guess the construction is based on the VCS. >> Um I mean we we abstract all the engine stuff. the construction is basically based on um on sort of these like stack objects in the in the constraint system and basically the like the two accumulators which are extension field elements. So there's the IO accumulator um and then there's the stack accumulator and these are just extension field elements. So there's it's just K columns

where K is the extension field. >> Is there the PCS at some point or >> uh no there is no poly? >> I mean we use commitment schemes in the underlying sort of engine. So when we're compiling the um the AIR, we're going to use the IOP and the PCS and whatever, but that stuff is, you know, abstracted away like this is literally just at the surface level of the AI. It's not it's not dealing with like it's assuming the rest. you're giving me an AI and which is what what we do here and you know you can do whatever you want with that afterwards like you don't have like you know as long as it's you know encoded as an algebraic circuit you can compile it

to whatever snark you want it doesn't make any assumptions about the underlying zones [Music] >> yes of course uh well I have I have the paper let me hold it Um, so let me just Yeah, I was sort of thinking it might be useful.

So here they are. I'll tell you which ones are sort of relevant for intuition here and I can explain to you what it all means. Um so here here's the idea. So this is the transition function. Um so there's 11 op codes. Um this is the full set. Now I've got a lot of jargon here that was defined in the previous sections because we basically define so the the fundamental variable is binary tree.

Okay. And there's only one operator which is the star operator and the star operator operates over two binary trees. Um and so for example op zero is um sorry op codes because then there's operators as well which are like these three or four fundamental things u zero says um yeah so the reason I couldn't go into this because I need to explain to you all the all the all the terminology but the point is that um what you're looking But obs1 is left child zero n2 is right child and the right child is a tree for whom the left child is zero and the right child

is m2. So what it does is it takes this tree and if and and if the star operator is is in like basically if the right left is a zero you know that the op code is op code zero and then you do what is a lookup and basically you're saying look up tree n2 at address n1 that's what the first output does code one says um well you look at you look at your tree left child is n1 right child is um is is a tree for whom the left is a one, the right is a two. And what it does, it takes this and it just spits out uh right. Right. Okay. The really key and important off code. So actually one, two, and three I think unless you

also need maybe some equality are enough for um completeness. Um so up two here is the really the the key one. It basically distributes star over the children. So what it does is it so so you understand how I'm parsing it here, right? So I'm basically like when when that's the the current node um I am basically pulling out n1 the left child and pulling out um 2 and2 the right child. I'm checking the right child's left child. I know that's all code two because it's a two. And then what I do is I I do a recursive call on the children.

Um I should be reading from the beginning because this is like a little bit said you add operators and false as a plus multiplication etc. There's four of them. Yeah. But the the difference is that the operators are are are strictly operations over binary tree elements whereas star is operations um basically um that distributes star within the binary tree if you think about it. So so the first one is not really a program. It's more like a deterministic mapping of one binary tree to another. Um for example, OP zero says convert this binary tree for whom the

you know the like this sort of binary tree tupole into the lookup from the binary tree of the internal load of memory I'm accessing where whereas the operators on top are things like um yeah so that's an operator so op zero is basically just a wrapper around an operator whereas op code for example two distributes star inside. So it basically like that's the execution that's why these are all codes whereas the other ones are just like mappings over over this thing but you should read if you want if you want to understand the whole thing it's it's fully formalized like you can read the

whole section 4 because there was so when we started there was no formal sort of treatment of no I think it was developed in like the early 2000s um and because we wanted to build a VM for it I actually to go in and fully formalize knock as well. Um, and so I actually, so in the initial knock paper, there's only three operators, but I realized that that that's sort of not really broken, but um, it it it needed to be patched. So I I did all that work there. It's it's only two pages. I I I think that you will you'll be able to parse it without much um sort of um without so many questions. It's relatively straightforward. Uh, but the only issue is that it does a lot of jargon.

But it's actually a relatively simple concept. And so yeah, so if we do if we use the first three or the first four, I forget what it is. That's perfectly. So you can actually if you really want to maximize how small things can get. This thing basically is tiny. And by the way, you can you can do this I mean I'm pretty sure these are not canonical like you can do this with with like you're up your own seven two or three off you can literally just access off code one recursive sort of like distribution off code and one like pull out the part that you know is at the specific point of code and I think those

three together are turning now they're not something I would like people to code for for for normal stuff. But if you're looking at getting really high efficiency, very small lines of code, um, and you have the engineering overhead to sink into getting optimal things for security, I think that this kind of approach is is is useful. >> Okay, time. Thank you so much.