ZK13: Programming Binius with M3 Arithmetization - Tobias Bergkvist

Transcript

[Music] Thanks for the introduction. Um, as he said, I'm Tobias and I'm going to be presenting basically how to build things on top of business using something we call M3 arithmetization. And yeah, I'm Tobias from Norway. I'm a senior software engineer working at Ireducible. And you can see my GitHub handle brist. And uh so we're going to start with a small challenge here. Uh can anyone like guess or see a pattern in these numbers? Um like what do you think uh this sequence is a part

of? Anyone? [Laughter] Yeah. So, uh if the number is even, we divide by two. If it's odd, we multiply by three and add one. And this is essentially known as a colet's orbit. Uh and to understand what the colet's orbit is, we should look at what the colet conjecture is. So the collapse conjecture says that if you start with any positive integer and you put it into this formula here basically you divide

it by two if it's even you multiply by three and add one if it's odd and you keep repeating this you will eventually end up at one that's the conjecture and so the ales orbit is basically the path you take to get from some starting value down to one and it's a conjecture it hasn't been proven uh though there are no counter examples where uh this isn't the case that has been found and we've searched yeah some pretty big numbers to kind of here's an example where we essentially start with uh the number six and that's even so we divide by two we get three three is odds we multiply by three uh add one and we get 10 and so on and you can see this

eventually uh gets down to one after you reach one if you keep going actually go back to four and then two one. So you kind of loop 4 2 1 4 2 1 infinitely. But we can say that we terminate once we reach one. And so uh like you might have heard about air arithmetization and uh you could arithmetize this kind of thing using air uh by putting it in the table like this.

uh and you can see we have n is the uh current value that you put in and here you compute both the rule if the number is even and if the number is odd and then you have this selector called odd which you then use to essentially recombine and pick either the even or the odd number. Uh so you can see uh to basically get what we should start with on the next row. Uh so you can see six is the input on the first row. Three is the output. Next uh line here we have three which is odds. So uh the result should be 3 * 3 + 1 which is 10 and so on.

But you might see that there is some redundant computation here like uh for all the odd numbers we're computing according to the even rule and for all the even numbers we're computing like the odd rule and then we're also like recombining them at the end. So this is kind of inefficient that you need to compute both branches and then select the right result at the end. there's a bunch of extra computation here and so uh like a big question here is how can we avoid this extra computation and that's where M3 is going to come into the picture but before I reveal how we do that I'm going to tell

you first a bit about the irreducible text stack you might have heard about binus uh otherwise maybe you wouldn't be here now uh that's kind of like the center piece of uh irreducible as a company uh business which is an open- source uh protocol for proving and verifying things using something called binary fields. Binary fields are particularly hardware friendly and so we use FPGAs to accelerate proving uh within irreducible as well. That's a like lower layer here.

And then on top of this uh you have risk uh zero building a risk 5 VM uh basically using this M3 front end. Uh and we also build Petra VM together with Polygon which uh the intention is to enable recursive proving and kind of proof compression. Yeah. So, our focus today is going to be on the M3 uh front end. Any questions so far?

Okay. So, here's an overview of all the things we're going to go through. We're going to we've already seen part of the Colette's air example and then we're going to show how M3 is more efficient, how to think about M3, how to think about binary tower fields and work with them to get them to do what you want. And we're going to show you how to do U32 addition uh using a reusable gadget uh in M3. And then uh finally we're going to essentially look at uh the code for proving and verifying coletes uh as it's like specified in M3 constraints. Okay. So we can go back to

the air example I showed right before we like took a little detour. And uh essentially we have a bunch of computation that's not necessary that we want to get rid of. And so the first thing we might want to try to do here is essentially split all the even and all the odd numbers into separate tables. And if we do that then we get uh like uh basically uh on the odd column only zeros uh for the even numbers and only ones uh on the odd numbers. And so we can kind of take

advantage of this and plug in zero and one into the formulas here. And we get that the next number on the even table is n even. The next number on the odd table is n odd. And so when we have this turns out some of these columns are no longer necessary in both of the tables. So we can basically remove the uh odd uh rule for the even table and the even rule for the odd table. So we're left with only like the even rule where we divide by two for the uh odd table or I mean even table here. And

then likewise we're left with only the odd rule. And we also don't need to recombine the results using a selector at the end. So we can basically just get rid of these. So now we have two tables one with even and one with odd. And so uh the question now is how do we deal with uh essentially boundary values for the problem? That is boundary values are kind of like public inputs and outputs of the proof we want to construct. uh in the air example uh we would have like the first row and the last row would contain our inputs and

outputs. Uh but here things are kind of split into two tables. And so here we to solve this uh we essentially introduce something called channels where you can push and pull uh boundary values. And you can see we kind of push six into the channel here which is then pulled by the even table and three which is the result of computation here is pushed back into the channel. uh and so on and you essentially keep going until uh you finally pull out one.

And so at this point all the pushed and all the pulled values uh need to be the same uh in order for the channel channel to be balanced. So that's kind of this abstraction of channels where you have pushed and pulled values and you want all the pushed and all the pulled values to to be equal uh in the end. Uh they don't need to be in the same order though. Uh but yeah, so this basically by starting at six and then going through all these steps and finally getting to one at the end, we are kind of proving uh essentially that we know the collateral bit from six to

one. And yeah, let's see. Yeah. And this is also an example. You can see that we can reshuffle the rows with M3. You can think of the rows as being kind of unordered because we're comparing uh all the pushed and pulled values not as vectors of ordered values but as something called multi-sets where yeah all the pushed and all the pulled values are essentially counted. do count occurrences of all of them and then uh yeah you expect the same counts on both sides but it can be in any kind of order. Uh we're going to look at how

boundary values would look in air as well just briefly because that's something I didn't show earlier. So that's actually going to be two extra columns. And this might be how you would uh constrain air to have like an input value of six and an output value of one uh by adding uh like essentially two new selectors, one for the first and one for the last uh row. And then yeah, you use two polinomial constraints to to constrain it. Cool. Um, so now I'm just going to show you some code. Uh, this won't make sense to you

quite yet, but it's kind of nice to see it. Uh, and I'm going to highlight what the different regions of this code are. Uh, like what their purpose is without diving into the details yet. We will do that later in the talk. Yeah, go ahead. tables. Just because it's nicer with M3, right?

So we do that to avoid uh redundant computation essentially uh like as you saw in the if I go back to basically computing the next value as if the current one is odd and the next value as if it's even in all cases you're it's a bit like branchless programming. You're kind of taking both branches and selecting the result. We want to avoid computation. So that's where M3 comes into the picture. So here you have coletes which kind of only has two different rules but for a CKVM maybe you have one rule per instruction and so you can imagine that the amount of selector polinomials would be uh like

you would have a much a lot more redundant computation. Uh but uh by splitting up like every rule into its own table you essentially avoid all of that. Yep. I mean, obviously you wouldn't do this, but like would this kind of like arithmetization structure that like we're going toward would it still work if you basically just try to like directly translate the the air type table over into just like a vine M3 table? Uh so you could uh I not saying you should do it, but like would it would it still work with the setup that you're doing?

So uh like one thing about the M3 tables is you can think of them as kind of unordered. You don't have transition constraints. All the transitions that you want to constrain you do through channels by pushing and pulling. So that's kind of a different paradigm uh uh in a sense. So it's not but yeah it's a fairly like straightforward and simple process to transform something from air to M3 by splitting up into a bunch of tables and then basically based on like the selectors is how you do it. Yeah. So whenever you have a selector that would be a like good place to split into multiple tables essentially. Okay.

Thanks. Hi. Uh would could Yeah. Could you stay on that slide for a minute with the um with the channel uh this one? Yeah. One thing I don't really understand is um so you're pushing six and pulling one from sort of outside of these tables. What logic determines sort of which table that six goes into? I mean obviously it doesn't fit in the odd table, but like what what like routes it to the right table? So uh you could say by default there is no constraints that prevent you from putting that into either table. So we would use polinomial constraints to restrict where it's allowed to go. Uh so for the uh like even table we can have a polinomial constraint that says that

anything we put in here has to have uh a zero in the odd column and odds can be then computed based on n in some kind of way. Uh and in that way you can restrict it to only be allowed to accept even numbers in the green table and only allowed to accept odd numbers in the other one. But otherwise, there's no restrictions on where you could put something uh like which table you would pull it into or push it from or in what order you do it. Uh so you're like making sure that one of the tables pulls six and there's only one where it's legal to pull it into. Yeah, exactly. Cool. Sorry. So you lose all order for the table which is as you say

is not a table anymore. It's is a set of values. Yeah. It's like a multi-set instead of an ordered table you could say. Uh so the the order is is is dictated by the channel. Uh then so the prover can choose whatever order uh works and kind of uh fits with the polinomial constraints. Um and of course you can't pull the same value twice if you only push it once. So that's also a limitation there.

But yeah, this unordered nature is uh it forces you to think about it uh like in a slightly different way from air you could say. Doesn't that make it much more complicated? Like um actually it's uh like you avoid a bunch of uh unnecessary computation and it's actually not uh not that much more complicated. It can seem a bit intimidating at first, but it's actually not too bad as long as you remember to yeah put these constraints. So you make sure that values are only allowed to be pulled into a specific table.

So you pull five for example and then you you look at your multi set where five is and then uh say again like when you get for example six you see like you get six from your your what do you call a channel? Yeah. So you push six into a channel and then on the even side here we then pull six. So that means the tunnel is balanced with regards to six because it's both being pushed somewhere and pulled somewhere. The like blue boxes here boundary values you can think of those as being like public values of the proof inputs and output values and they're kind of known by both the prover and verifier and separate uh separated from

the tables pretty much. And then when when six you basically you should enforce it out which should be three because that is Say again when when six when you pull six then you you go to the multis set and choose the one that has six and then you decide. So you don't need to pull and push in the same order. You could uh like pull six first or you could do it later and p pull other things that haven't been pushed yet to the channel. Uh like there's no ordering there. It just has to be balanced in the end where the number of uh there's no end. That is the problem now. So what do you mean no end or because there's no order. You have a

multi set that has one in it and that's that's the proof that if this multi set has one then we reached one but maybe you never reach it. I don't know how this order is enforced. Maybe we should wait. So if you never manage to balance the channel then uh you won't be able to construct a proof essentially. Um yeah, cool. Any other questions? Okay, then so this is like code for proving and verifying one of these collects and there's like different parts of this code.

First here we define all the constraints and channel interactions. That's like the first few lines here. We will dive more deeply into this later but now I'm just giving a high level overview of different parts of the code. Then we have witness generation which is only done by the prover uh basically filling all the tables uh with data and committing uh to that data and so on and then we have the statement which is containing these boundary values and the sizes of the tables. Uh so this is something that both the prover and verifier has access

to and you can think of this as being like a specific this is what uh creates a specific instance of the problem while the constraints at the top they define a more generalized version of the problem. So the constraints define like a generalized collapse orbit uh using M3 while the statement here is like a specific instance of that for example starting at six ending at one. Um and then last part is the actual proving and verifying and proven and verify they can obviously be run on different machines. You don't have to do it in the same chunk of code like I did here. Uh you can see that proving uh it

takes in constraint system which is like the generalized problem statement. It takes in the statement which is like specific instance of the problem like with six as an input and one as an output and takes in the witness uh which the verifier doesn't take in. Uh you could say that you essentially switch out the witness with a proof to verify. Uh yeah, cool. So to summarize, uh we have a bunch of we have two tables here with a bunch of even numbers and a couple odd numbers. And you can see that we use

polinomial constraints to uh limit what can be accepted into each of the tables by asserting that all of the n values in the even uh table needs to be even and likewise that they all need to be odd in the odd table. And so six and one here are kind of the inputs and outputs uh to the proof. And to kind of uh like give an idea, you you essentially have two primitives when working with uh M3. You have channels and you have tables. And the tables interact through channels. And you don't need to only uh pull and push a single column at a time.

You can do multiple that you push and multiple that you pull. And the channel kind of you can think of it as having a type uh in terms of how many columns you pull and push. So you can't reuse the same channel for pulling and pushing a different number of columns. Uh to give some more concrete examples here. Here you can see we have two columns that we push and two columns that we pull. And so you can see 1444 is being pushed on the left side here and it's being pulled on the right side but in a different location. So uh but notice that 14 and 44 it stays together kind of like a tupole. And

that's also a rule that when you push and pull multiple columns uh it's kind of like pushing and pulling uh one tupole per row. And these tupils are kind of atomic. You can't split them up. uh and they have to stay together on both sides. You can also have multiple tables that push and pull. So you can do this split at any point kind of and there's no restrictions by default to where values can end up or like be pushed from or pulled to. uh unless you have like polinomial constraints to to limit that and then uh like we also have

boundary values that are the public values uh used by both a proven and verifier as kind of inputs and outputs to the program. Yep. Um I remember vaguely reading something about that you can use like columns from the table directly but also some kind of like virtual column that was like generated like as like combinations or computations based on columns is maybe we're going to talk about later but that's the case right there's virtual columns and committed columns we'll actually get back to that later so oh in that case never mind so uh yeah you can uh look forward to that um yep And so here's kind of the like most

trivial example we have of both uh boundary values uh columns being pushed and pulled from a channel and polinomial constraints. So, and this is a single table even though it looks a bit split up where you have X and Y as different columns in that table and you have a polinomial constraint that says that whatever you put in Y has to be one more than whatever you put in X. So, for this to be balanced basically you push zero and then zero comes in here, you add one. So, you get one and then push that back you pull one add one or get two and so on until you get to five. And so this is basically yeah you start at zero and at

five and you have this rule for going from one value to the next. So it's kind of like inductive proof in mathematics where you have some initial values and some uh allowed transition. And yeah in this case we basically get a proof that we can count from 0 to 5. Um yeah so to summarize here we have channels and we have tables. Channels contain two multi- sets. Uh those are pushed values and pulled values. And for a channel to be balanced these must be equal the pushed and pull values. Uh and you also include like the boundary values in that uh which are

kind of yeah separate from the constraint system. In the constraint system you specify like columns to p pull and push but then in statement you can have individual values. So tables they contain multiple columns that all have to have the same height. Uh we'll get back to what that means a bit later. Uh for them to have the same height columns uh yeah you can flush them to channels and you can put polinomial constraints between the the columns.

Um yeah so we yeah I've pretty much gone through this that we have this uh extra computation here and we can get rid of that by transforming it into kind of two tables wherever you have a selector and yeah you can essentially think of uh all of this as like a way to construct inductive proofs where you have like some initial values and you have a set of rules that can take you from uh one value to another one uh in these transitions uh with limitations on which rule you're allowed to use. So that can be a good way of thinking about

it. But yeah, so far we've been pretending that we can just do integer addition and multiplication. And uh that's not necessarily as straightforward as I made it look so far. You have a question. Um, so just going back to to your second example with the with the with the columns that was constrained with one plus one. Oh, uh, this one. So here you put them in order, but you say you don't need it. It doesn't need to be ordered, right? Again, it doesn't need to be ordered, right? No, it doesn't need to

be ordered. You can change the order and still you get the same proof. Yeah. Um, and this is not even an odd, right? No, there's no like here you only have one rule you're allowed to use. So there's no need for like selectors of restricting which table they're allowed to pull into and so on. So how so so the prover can pull from for any like can start with any any table they can pull for any table like whatever you call yeah pull. So so you say the boundary value is zero they can put in the column one or two right?

Uh so say again the oh okay they always pull into the no sometimes they pull into this column Y right these two columns are part of the same table right yeah but oh it's one table this example has one table yeah it kind of looks like two uh because I put the broken over there but it's it's one table and that kind of only matters because we only we can only have polinomial constraints between columns in the same table. We can't have them across tables because they have potentially different heights which could lead to problems. But I understand. So, so there's no constraint between tables.

There's no constraints between tables only within in the one and and then the table decide when to push into the channel. So the prover decides the order and of the elements and so on. And then you have polinomial constraints to essentially limit what's allowed. Uh yeah. Okay. Let's see. Thank you. Okay. So uh as I said we've been pretending we can just do addition and multiplication in these polinomials so far. though uh that's actually not that straightforward uh because binus is uh a protocol over towers of binary fields

which do not behave exactly the same as integers and uh we're going to see this this is basically the primitive type we have to work with uh for all our constraint polinomials and all the values they have to be like towers of binary fields and then multiplication and addition has specific meaning. So now I'm going to introduce binary tower fields. We have a few different sizes all from like one bit up to 128 bits.

You can see I grayed out B2 and B4. Since it's kind kind of uncommon to use two bit or four bit values, we don't export these uh like types uh or use them much at all. Uh just because yeah, most things you do on the computer, you work either with individual bits or bytes or something bigger than that. Uh we've gone up to 128 bits. There's like nothing that would prevent us from going further. like every time you go to the next binary tower uh field, you double the number of bits.

And so this is like the sizer for all of these are exactly 16 bits, 32 bits, 64 bits and so on. It's not like with prime fields where you have to uh like think about which bits you're using and so on. This is like a very nice fit for uh basically the way that computers store data and you basically avoid all the embedding overhead that you would have with uh like baby bear fields or things like that. But yeah, so in terms of how they work, you have um addition plus 0 is 0. 0 + 1 is 1. 1 plus 0 is 1. And then 1 + 1. I guess we would

want this to be two, but two would take more than a single bit to represent. So that's not really possible. Uh and it's zero in this case. You can think of it as overflowing to back to zero. Though uh does anyone recognize this kind of bit pattern? Do you know what kind of logic gate uh this is? Exor. Yeah, exactly. So this is B1 addition is an exor gate. So multiplication looks like this. So far it looks like integer multiplication where you have anything * 0 is zero and then 1 * 1 is one. What kind of gate do you think this

is? It's an endgate. And so for B1 fields uh essentially addition is exor multiplication is and and let's go to B8 arithmetic which is a next step up. We're skipping two and four bits. uh here since this is an extension field of the B1 field that means it behaves the same over like uh B1 values that is like single bit values here. Uh but what do you think 1 plus 2 is in B8 addition?

It is three. What do you think 13 + 13 is? It's zero. Yeah. And so if we write it in bitwise notation, it looks like this. And does anyone see or see the pattern as to what this uh B8 edition is? Yeah. So it's still exor but now it's bitwise exor between all the individual bits and there's no like crosscontamination between the individual bits you could say. Uh it's all like this is like very very hardware

friendly to to do uh on CPUs or FPJs or pretty much anything. So additions are very cheap. Let's look at multiplication. What do you think uh 5* 2 is? Any guesses? No, that's 10. So, so far it kind of looks like integer multiplication, but what do you think 2 * 2 is?

It's three. You should say more. So what what about 3 * 3? It's two. And then 3 * 2 is four. So like basically B1 multiplication is an AND gate. Uh B8 multiplication is not as straightforward anymore. It seems it's not just bitwise and uh just like the addition became extraord this is not

that clearly. uh and in general be like multiplication above the B1 field is not something particularly useful to us when using writing M3 constraints unless you are doing something to do with as encryption or gestal hashing or or this kind of stuff because that uses binary fields and the different types of binary fields are isomorphic to each other that means you can transform from one into another do a bunch of computations there and then transform the result back uh and get the right uh result.

So do you have any idea of how we can uh express integer addition with these uh like primitives we have now so I will yeah exactly so we can use the rule for individual bits uh where we have uh like and and exor gates at our disposal essentially.

Uh and yeah, so a full adder circuit the way you would do it in hardware uh or an 8- bit adder in this case, it uses a bunch of smaller circuits called full adders uh which take in three inputs and produce two outputs. You have uh x and y which are individual bits and then c in which is a carry in from the last addition operation. Carry out which goes to the next one and then s out which is a like sum. So here you have like eight bits plus 8 bits with uh eight bits of output plus plus a final carry out.

And so if you Google what a full adder circuit looks like, uh you might see something like this. Uh and that that corresponds to what is inside a single one of these boxes essentially. And you also have a truth table for this. There is uh one problem with this circuit though. It has uh two X or gates, two AND gates and one ORgate. But we don't have orgates. It's possible to build one using and ANDgates and X or gates, but that would be kind of inefficient. So, uh maybe there's a way to create a circuit that produces the exact same lookup table, but using

only and exorgate. And it turns out there is. And it looks like this. And you can see this has four exor gates, one andgate. It produces the exact same output as the other circuit uh like the exact same lookup table. And here you have the formula for computing s out and see out which is some output and carry output. And you can see the ring with the plus in is exor and the like wedge is bitwise and. So if we use binary or B1 fields essentially exor becomes plus bitwise

and uh becomes multiplication and we've also seen that like when you extend the field into higher uh fields and addition remains cheap but multiplication it gets more expensive. So it's also good that we only have a single and gate here uh and not more. So this basically covers the basic uh theory uh before we're going to jump into uh the code. Um yeah, are there any questions so far? Yeah, could you elaborate on that that last bit? The um if you go back to the last slide um this one. Yeah, that

I I don't quite follow the leap that you made from um like I thought you showed us a few slides ago that multiplication doesn't extend the same like um exor principle or or and principle. So when you go into the extension fields, it doesn't behave the same. But when you stay in B1 uh fields, then uh addition is exor, multiplication is. Yeah. So as long as you only work with single bits, you can take advantage of that. Okay, got it. So like when you've now replaced the symbols in these equations, you're not saying that this generalizes to higher fields. No, this is only for B1.

Okay. Um and and you're just zooming out a little bit. You're talking about how you would write polomial constraints to implement an adder so that you could create tables that do integer addition. Exactly. Yep. Thanks. Uh any other did you did you work out the circuit by hand or you use synthesis tool? Uh so I use like Python package called scam draw where I would like draw one component at a time and uh all the lines. Yeah. Just just comes to me straight ahead. We can use inversion as a sore gate that both

inputs are the same value. So that can be used as a vehicle of conversion of or to the other way around. Cool. One more question behind. Um, so here you can do the X or in in B4, right? You could do X or in B4, but uh the problem is the multiplication here. Once you go to B4, like the multiplication would also be a B4 multiplication. You can't mix math. So you want to stay in B1 because you have multiplication. Okay. Yeah, exactly. But if there was only additions here, then you could do that in B4 as well and it would like be the same

behavior. Cool. So, are you ready for some codes? So, this is how we essentially define uh a U32 ad gadget from the constraint system point of view. Not witness generation yet. This is only kind of creating the constraints. As you can see um we have some committed columns here s out and see out and when you commit the data like it can contain any data there's no restrictions on that by default uh but that's where like assert zero comes into play where you have zero

checks where essentially you assert that s out uh minus the part behind there is zero. Basically, those are the same. You just move it to the other side of the equal sign. Minus is overloaded to do the same thing as plus. Uh it's just to make it like a bit more readable, but this is exor for both addition and subtraction. So, uh if they're the same and you add or subtract them, you should get zero. Uh yeah.

Um, so when you're defining like S out, C out and C in up there, I see that like you're defining them probably to like B and B1. Uh, what's the values per row of 32 up there? I'll get to that uh very soon. I'm sorry I keep on asking things you're about to talk about. That's a very good question. Uh, I guess I'm I'm trying to understand like the the allowed operations at which level of the stack. So it looks like the assert zero that you're doing is basically just checking the addition how you would do it you know normally in code uh and it's not breaking it down into these circuits but the table itself has to break it down into these single bit operations. Um so you can see in the column type here I specified B1 as the

uh column type and then you have this values per row which I'll explain in a moment. uh that means that when you do this assert zero here, you're essentially operating over uh B1 values when you specify these constraints. And that's basically encoding that circuit that we saw earlier with like a way to compute S out and C out. I guess in this case it doesn't like reuse any computation between S out and C out. But yeah, I don't know if that answered your question. Yeah, I'll I'll wait a little longer and see if it becomes clear.

Okay, so that was the question. What is this values per row thing? Uh so I've said previously that uh all the columns in the table needs to have the same number of rows, but sometimes we want to stack multiple values inside of a row uh like together. Uh and essentially this might not be intuitive when you look at it like B1 here uh is a single row for X. Then two B32 values is considered a single row in the column Y and then four B8 values is considered a single row uh for the column zed. You can see they're

kind of stretched like one bit uh is obviously much smaller than two 32-bit values, but this kind of shows how it aligns uh in terms of rows and not how it's laid out in memory, let's say. Yeah, I guess you can kind of think of it as like a embedded tupole inside every every row kind of. There's still only two rows. There's only two rows in this table. Yeah. 32.

Yeah. Exactly. So that's the like number of values inside a single row. That's the like values per row constant that you put in basically. Um yeah. Was that clear or any Yeah. Cool. So next up we have this thing called add shifted. And that's kind of the next uh mysterious thing. Um basically we have something called shifted columns which are virtual. That means the result is not committed. So uh we save a bunch of work uh for the prover um in terms of entities and Merkel

hashing and so on. But basically the way they work you can see they have like three parameters. It's a type of shift. There's a offset and a block size. And you can see this one has a block size of four. That means a log block size of two. The block sizes can only be powers of two. The offset here is one. So you shift everything up one row. And you can see we pad with zeros uh inside of every block. So you can see the five here even though it's kind of in the middle. We lose that value uh when we do the shift uh because the shifting happens independently or individually inside of every block. the blocks they can be smaller than the number of values per row but they can't be

bigger. So this is a logical right shift. We also have logical left shift where you just go the other way you still pad with zeros. And we have circular left shifts where instead of dropping the values and padding with zeros we kind of put them on the other side. We don't have circular right shift. Can you think of why it's redundant? Yeah, because if we change the offset to three and have a right circular right shift, that would be the exact same like pattern here. Cool. Yeah. And as I mentioned, shifting is creating a virtual column,

not a committed one. So it saves a bunch of work. It's cheaper to compute committed columns uh requires extra prover work in terms of yeah number theoretic transforms and uh Merkel tree hashing. So now we've seen uh pretty much how to define the constraints. Next up is going to be witness generation. basically how do you populate the table from the prover side uh as part of like generating the proof and here's an example we have this table witness segment which contains uh

essentially a segment of the table the reason it's called segment and not the entire thing is because uh it allows for running multiple of these in parallel you can see it's sequential inside but yeah essentially you have uh x in is kind of an input to the U32 addition gadget. So we don't need mutable access to this. We assume it has already been populated and so we get access to this data and we interpret it as a slice of U32 values and then we can use that down here and basically uh when you index into it you get a single U32 value.

If you put U8 instead of U32, it would cost to that instead. But that would like cause problems because uh you have 32 values per row which fits nicely here. But if you cast into U8, you would suddenly have four times as many values as you want kind of. And then you have get mutest which gets a mutable reference to this slice instead which means you can assign to it. And basically that's what we're doing here. And we've seen U32 addition now which is something we needed for the collect example. So we can now go back to that. You might remember uh this code

where you have like the constraints being defined and you have witness generation statement and proven verify. Let's start by looking into the events table how we define that and that looks like this. So you create a new table uh called evens. Here you add the committed column for the like even input. And then this is how we essentially constrain uh that only even numbers are allowed to go into this uh uh table. U so we're using something called add selected.

I'll uh give you a visualization of what that does. Essentially when you have multiple values per row and you want to select a specific index within every row then you can use selected. So here index number two is being selected. So you got three and seven. So it's kind of yeah just mapping out those values. Yeah. Uh so that's this is odd thing. Uh and essentially we're asserting that this is zero.

And that means if the prover tries to pull odd numbers in here, this is going to fail. Then we have half. Turns out that uh bit shifting is a nice way to divide by two. So that's very convenient uh for us and we can use a shifted gadget for that. Uh here's the next thing that uh uh like might seem new or mysterious is ad packact. Essentially ad packed is a way of uh upcasting uh or reinterpreting data as a bigger type. You can see the like you have four U8 values here and then when you pack it uh from four B8

values into one B32 values, you get a B32 value that uh like yeah on this form instead which kind of reinterprets four bytes as a single U32. And why are we doing that here? The reason is because we're pushing and pulling these values when we have 32 individual bits. Uh we like we don't want to push and pull them because uh like directly because that means someone else could pull and push those bit values but reorder the individual bits uh because there's no like ordering

between the rows. So whenever you push multiple individual bits like this, you want to pack it first to ensure that it's pushed and pulled in the same order or same atomic unit where the bits can't be reshuff reshuffled or put into other numbers and so on. And you can see basically this is how we pull and push columns. In this case, we're pulling and pushing a single column, but you could do multiple by comma separating them inside calls. Cool. So, that was evens table. Um, now let's look at odds table. This one is slightly more complicated. Yeah, I guess I'm on

time, but should I keep going or Yeah. All right. Uh yeah, odds table we have uh this is slightly more complicated but like like the other one we have uh this is odd thing which now we want to assert that it's one instead which means uh we add or subtract one from the value it should be zero. uh we have uh double which we just like when we were dividing dividing by two we can double by shifting the other way and to compute three times the value we can

then do a U32 add using the gadget we defined earlier to add the n to like 2n uh but then we have like 3 n we want 3 n plus one so for that we also want to add the constant which is one and this is like a transparent thing that both the prover and verifier knows how to interpret. Essentially, you have some kind of transparent constant and you keep repeating it um like this. That's kind of how that works. And just like with the even numbers, you pack it before you uh pull and push. Yeah.

And then next up is witness generation. I'll just go a bit fast now because uh like I'm over time. So basically we generate all the odds and even events in this call trace generate by running this while loop. Um yeah uh then we fill tables and the way this works is fill table sequential expects this table filler trait to be implemented for the table which specifies a type of event and then just like the uh user to add populate function uh we essentially like get mutable access to columns and write into

Um um and for odds it's pretty much the same thing here. We take in odd events instead. So you can think of um like we generate a bunch of events that are interled and then we kind of uh transpose them into like separate tables. Yeah. So the builder methods I've shown so far are like highlighted in bold here. There's a bunch more that I haven't gone through. As you can see, we also have uh lookups which is uh as easy as like pulling from a channel in

practice though I don't have time to go into that. And yeah, this is a tech stack and uh I can also mention that we recently open source Petravm which is a uh like community project/c collaboration with polygon uh that we're doing and the purpose of this VM is uh to run the business verification circuit inside the VM and in that way we can verify two proofs inside that VM and then we get a single proof that is kind of compressing two proofs into one. So it's like for proof recursion or compression. Uh

that's like the main motivating factor behind that. And yeah [Applause] thanks if there's any questions. Yeah. Yeah. A couple questions about the um like API. I saw that when you're doing uh shifting, you're providing the log of the shift side can size. Can you only shift in um powers of two? Uh no. Uh I'm providing the log of the block size. Log of the block size. Yeah. Yeah.

So the shift is like not logarithmic. It can be Yeah. Do your blocks have to be powers of two inside? Block size has to be power of two. Yes. And you have um packing. You also have unpacking. We only have packing right now. Uh Okay. So, got do what you need to do with the bits before you pack them because then you can't unpack them. You should release that on Christmas. [Laughter] It's more of a general question, but um you presented the collat uh function in the beginning and what

you showed after how much of it is specific to collats and how much is kind of general general functions or how much can it be be generalized? Uh how much you can generalize coats or what kind of functions can can you actually model or implement with this? Yes. So the the reason I picked collat as an example is uh it's an example that uh kind of acts like a very simple VM which is by no means touring complete but you have like different rules for progressing to the next state and it kind of shows how you can put things into different tables uh to like have these different multiple possible

transitions. So it's I would say probably the like simplest example I know of that demonstrates this like splitting into tables and that is very useful for CKVMs in particular and we yeah we're using that in Petra and the in the risk zero collaboration as well. Uh sorry to answer the question uh the the model or give another answer. Um the model's very powerful. It's sort of um similar to predicate logic programming in like a prologue sense. Um I have a bunch of uh kind of reasons to believe that it it's capable of proving anything

in MP and um can very naturally model lots of types of systems including virtual machines. Yeah, I can mention as well it has a bunch of similarities to something called colored lending petriets which uh some guy invented to model chemistry basically and what is possible like transitions between different molecules and so on. So thank you. Thanks.