ZK11: o1VM: Building a Real-World zkVM for MIPS - Danny Willems

18 Apr 2024 · 15:09

o1Labs cryptography engineer Danny Willems presents o1VM at ZK Summit 11 in Athens, a general purpose zkVM built to prove correct execution of MIPS programs. He details the encoding techniques used to implement hash functions like Keccak efficiently, the folding scheme and RAMLookups approach used to handle long execution traces, and how the work feeds into bringing validity proofs to Optimism's OP Stack.

Speakers

Topics

Transcript

[Music] hi guys hi everyone uh thanks for coming so I'm Danny Williams cryptography engineer at o at owlaps so owlaps uh incubated the Mina protocol uh we also been working on o Jess which is a typescript uh framework uh that can be used to build uh um ZK app uh that is backed by our uh Rec cive layer called Kim called pickles and under the hood we use kimchi our library uh and here uh today I'm going to present you a work that we've been doing in the previous

months uh that uh we call O VM so it's a ZK VM uh built uh for the meeps architecture at the moment but we can extend to other uh instruction set architectures in the future uh it's initially mips because it's uh a project that we've been working uh with optimism uh and we think in the future to integrate it also in Mina um so uh what I'm going to talk about today uh so I'm going to start by uh describing the design of the1 VM uh I'm going to after that talk about the uh additive lookup or log up or I don't

know how you want to call it uh that we use to represent uh memory uh and register accesses uh we call it Ram lookup uh we also have a way to have let's say specialized instructions uh in our VM uh and we use uh we implemented uh a version of Kack using additive lookups and also one way to represent um Boolean operations using field additions uh and also I'll describe uh how we plan to support long traces uh using using uh folding um so let's get by let's let's start by describing how the VM Works uh

so you take any program written in any programming language you compile it in uh the instruction set uh that you want at the moment is the myips uh instruction set um and it creates a binary and you're going to load this binary in the VM um and uh we start by uh correctly setting the instruction pointer uh and we start by uh going through The Interpreter The Interpreter is going to be the piece of the1 VM that's going to build the witness uh that can be used after that to build uh the commitments and the uh accumulations for the cryptographic protocol uh so how it does work uh we first read uh the instruction pointer we

also read the next instruction pointer uh we read the memory um that uh located at the given Address given by uh uh by the instruction pointer we decode it it's specific to the mips and after that we execute the instruction and when we execute the instruction it means that we're going to build constraints between different columns and we also going to perform some uh memory uh and register accesses and we're going to use it uh we're going to use uh our lookup argument uh for this so how does it look like um so we've got at the moment uh 93 columns uh we have columns for the

instruction pointer and pointer the next instruction pointer uh different columns for the decoding of the instruction um uh and also uh we've got a column to keep uh the um uh the the index of the instruction the instruction counter uh the you know in the trace uh which instruction at which Step uh we are at the moment that's going to be used for uh the the lookup argument um and also we've got a way to communicate with other um with other instruction uh I'm not going to describe it uh I'm not going to describe here and also uh for each instruction we going to

have a certain set of uh of columns and that's going to be the one that is used by uh the lug up uh the lookup argument um quickly about performances uh at the moment uh it's uh on consumer Hardware on any uh any laptop that you can run it uh it's on the CPU uh it has a small Ram footprint at the moment around 100 megabytes uh and if you take the master branch of the1 labs proof system repository you're going to reach around 100,000 uh 100 khz it means 100,000 instruction per

second uh and there are some open PRS that we've got to polish before merging it was more proof of concept uh we realized that we were always inverting at each step uh a field element uh which is useless we can do it at the end and so by doing that we uh we can get uh 1.7 mahz by doing the batch uh by doing a batch inversion and also uh for the memory of the VM uh at the moment is uh in master is a page index memory layout is not efficient at all uh to implement it like this so by using a linear uh memory layout we can use the CPU cache and um uh is going to have far

better performance uh and it give us uh on uh on on one laptop 6 MHz uh for the witness Generation Um we also have other IDs to improve the witness generation like using more structure in the code using more the CPU cache uh and also regarding commitments uh most of the columns are only small values uh and they are U they have a certain shape uh so we think that we can also uh improve the comput the computation of the commitments and also the commitments uh can be done in parallel of the other course uh while we building uh the

witness uh and to give you an idea on the kind of application of uh of the number of instruction for real world application for optimism we've got around 2.5 billion instruction so uh let's describe uh how we uh perform um memory access uh so if you check at the Lo the look up the log up or additive lookup equations uh you can see that it's a uh additive accumulation uh scheme and um um you can see that the the value that you look uh that you look up uh the value F very

often in the paper uh can be seen as a value that you add into an an accumulator and the table T that you look into can be seen as a a value that you decrease from an accumulator and therefore uh we uh represent uh when we want to overwrite uh a value into memory uh we use a vector lookup uh so when we want to override the memory cell x with the value y we keep uh we have a as I said we've got a column where we keep the instruction counter uh so toe is the instruction counter that I described before uh in um in the list of column uh and we also keep

the last time that we access the value uh and we also keep it in a column and therefore we simulate the fact that we overwrite a value by adding a certain uh value and we remove from the accumulator uh when we read the old value and the same thing for uh reading a memory uh cell we simulate the fact that we uh read the old value at the previous step and we over right with the current step so how do we differentiate um registers and memory uh we use a table ID in the vector lookup so we add oops uh ooh or is the other button um so we

add the table ID in the vector lookup so R is a random combiner that you use beta is the the evaluation point from the log up uh or look up or how do you want to call it um is the evaluation Point uh we also have to do a range check on the instruction counter to be sure that we uh we we are we do not overwrite a value uh before that we uh we do not read a value before we write into the memory um also all values that are included in the vector lookup uh are committed as commitments as columns um and the verifier sends the random values so the evaluation uh

Challenge and also the random combiner after re after receiving uh the commitments of the columns and also the initial and final memory are [Music] committed um that was for Ram lookup uh so now let's talk about uh Kack um so we uh implemented a version of Kack using additive lookup and uh and also one way to implement um uh Boolean uh operations using field using field addition um our design is uh to have the whole K Shack uh uh Kack permutation on

uh one row uh the 20 um sorry um to have one row is equals to one permutation of kak um so we've got around 2200 columns 2200 lookups and around 900 constraints and how do we do that is um normally it's a five on five square but yeah it's six here uh so the Kack State can be seen as uh 25 values of 64 bits what we do is we split each element of the state in four chunks of 16 bits and we're going to expand um going to get back a 64 bit value

by inserting intermed intermediary zeros and these zeros are going to be used as um as scary values as scary values uh by uh by the field addition so um how Kack uh works is like most SPN uh construction uh you've got a function that you repeat uh a few times over a certain state so here here that's the construction of Kack uh you can see that it's always exor operation or rotation or end and so what we want to do is we want to remove the EXO operation because

you know it's very costly in circuit you've got to decompose in bit and after that you've got to do bit by bit operations we don't want to do that um so what we want to do is we want to perform the field addition on the expansion of uh the 16 bit as I showed you before um everything is described in an RSC is long so I'm not going to describe here in the talk you also have the implementation uh there um and so in a nutshell how it works uh if you want to if you've got two vectors A and B and you do the EXO On A and B you can see that in blue um you're going to have so the in red and blue is the real bit uh uh of the expansion so you've got here

the 64 bits expansion and uh when you do the addition on the same Vector uh you can see that at the same place you going to have the result of the EXO operation and on the bit uh the on the left uh bit you going to have the result of the end operation so you can see that if you do one and one you're going to have one which is on the left so it's a bit more complicated than that everything is in the RFC feel free to have a look you've got all the different constraints uh that is described uh and you also have the [Music] implementation um so regarding folding uh so uh you know that the programs is quite long uh

we've got 2.5 billion instructions uh to handle so how do we want to do that uh you can see uh instructions as a multivariate polinomial uh so what we do is you can also see each instruction as a relation uh each instance uh is a folding uh instance we split our Trace in um in Chun in chunks of the same instruction so we've got always the same circuit uh we fold the N minus one for the i1 uh circuit we hold the M minus one for the I2 circuit and we combine uh after uh the two Circuit by adding a

virtual uh uh by adding virtual selectors and we do that for the um for the uh the the whole Trace uh we also use a look up argument and also we uh reduce uh all polinomial to degree 2 at the moment uh we also um delay uh the uh the multiscalar multiplication and we also have a way uh to um avoid doing the scalar multiplication and replace it only by doing elliptic curve addition that uh and look about argument that I'm not going to describe here but we can talk about that after uh on on a piece of paper I can draw it if you want so

yeah um um that's it thank you um we also hiring so if you are interested in O Labs uh we're doing cool stuff so uh feel free to come if you want to check the code please check the code uh can check ands Mina and also the different rfcs that we try to write every time um so yeah that's it [Applause] [Music] [Applause]