ZK7: RISC Zero: Encoding Von-Neumann Architectures in Zero-Knowledge Proof Systems - Risc0

Transcript

[Music] hello everyone i'm brian and this is jeremy we're the some of the founders of risk zero which is what we're going to be talking about today it's a general purpose zk vm um before i go into that i want to talk a little bit uh about our team because people always ask what our background is uh we're all from seattle we met like 20 years ago um through the seattle hacking scene um jeremy wrote one of the first uh wi-fi crackers or the first wi-fi cracker um and yeah this is our third startup together uh before this we were doing tensor compilers for ai and genomics and various other things like that so we have a pretty diverse

background and we're pretty our last project was also a fairly successful open source project okay so uh when we hopefully people are roughly familiar with the idea of zkbms i'm going to explain how we think about it in a second but risk five is a general purpose of zkvm so when you say on general purpose we mean it can run arbitrary code um so zkvms like as different from something like aleo's doing or circom you know these languages are dsls that uh that produce some kind of circuit and then you run inputs through them you get a proof out uh when i think about what a zkvm is it's something that

your circuit is the vm and the program comes in as an input sort of the key difference there's sort of like three classes of zkvms um i mean they're all broadly similar but you have bespoke virtual machines like cairo and maidan you have people doing zk evms there's a lot of those coming out these days and then you have what we're doing which is zk risk v or uh instruction set that actually mirrors a real commercial instruction set so people well i guess it's not super commercial but um so risk five of people aren't familiar is uh it's like arm it's a reduced it's a risk iso variant but it's a um like an open source chip so

they have a lot of uh like verification tests that you can run on your chip your fake chip okay so risk five uh or risk zero the zkvm just like any other zkvm you have a circuit the circuit here actually describes the risk five microcontroller um and programs come in just like uh in any other system but the format that we accept programs in is just a standard elf file compiled for uh risk five because it's slightly not standard but that l file can be generated um you know through llvm or gcc and really like any language and libraries associated with those languages can can be run now in a zkvm concept context

so we also have this system for interfacing with ram in a read write manner sys calls limited set assist calls and we also have uh sort of accelerator units we can add so we have a very specific fast sha-256 circuit that we are fans of um yeah so the project is open source it's released under apache 2. the prover and the verifier are available we have a blockchain integration demo you can see down in our booth currently it's on near uh that's because the it's very easy to port our verifier to wasm chains so we'll probably support other wiseman chains in the near future we have some examples um for from

different uh sort of verticals that you can see on our um yeah on our github and then we just did put out an article sort of explaining uh how battleship works yeah hand it over to jeremy to actually talk about how we create the respirator uh hello everyone one second let me just get this mic attached there we go all right um cool so basically i wanted to describe sort of how we actually implement the risk five sort of um micro controller inside of the uh fry based proofing system we also use plonk as part of it so i'm

kind of going to walk into that in a little bit of detail so um it's going to be somewhat technical in that i'm going to make some assumptions that people are at least basically aware of how sort of um stark based proof systems work but so before i get into that i wanted to talk about sort of how time works uh the sort of set of steps that occur in our vm's execution so in a stark bass proof system um the same sort of circuit uh is run repeatedly over multiple sort of logical time steps uh and those logical time steps um the way that those actually execute

arbitrary code in our case is that at the dawn of time there's an initialization um well one thing to note by the way is i'm going to talk about how we emulate ram using planck and one thing to note is that for every logical cycle or for every stark row we allow one memory transaction to occur in that cycle and so at the dawn of time the program is initialized and then we go into a phase where we basically load the elf file into ram this is done in advance of executing anything and this would be in the normal computer a non-vm this would be done by the operating system loading the elephant to ram right then we basically reset the chip which you know sets all of the registers to zeros and the program counter to the

beginning of the elf at which point we enter into this sort of three cycle process by which the the circuit loads an instruction from ram decodes it um possibly reads data from memory um does some computations and then writes data to memory updates all of its registers and that continues until such time as the it terminates by a special call a special instruction in risk five that basically normally calls back into the operating system at which point we consider the execution finished so this is sort of how we basically embed a uh the risk five uh process into uh the stark um so in terms of the stark's column structure so the column and stark represents a portion of the witness that

is variable and there are sort of three different types of columns in our proof system each of which is held in a separate merkle tree um the the control columns are actually uh publicly known to both the prover and the verifier um and that's how we actually encode the data representing the elf binary itself and the public um columns also are used to control execution so they contain flags as to like whether it's in the you know it's in the reset phase or it's in the um you know normal execution phase and that sort of thing um the the data columns basically hold the state of the actual risk five uh processor so for example

the register state um when you're decoding an instruction how the instructions decoding you know breaks up into multiple fields and so on and they basically perform the execution additionally the data columns also hold the memory subsystem so they also hold what we'll talk about in a minute which is the um basically for every uh every row every time step there's basically a memory transaction and a memory verification and then finally the last set of columns are basically used as part of the the planck mechanism to verify the memory and those are have to be in a separate uh

merkle tree because these can't be set until these have been committed uh due to the way that planck sort of uses the um five shmear trick to do stuff um so basically uh hopefully that will make a little more sense to me here um so i want to talk a little bit about the memory transactions um so the way that we represent memory is that okay so in this case what we have here is this is the witness and this represents multiple cycles of time and these are columns in the data section of the witness um and this represents sort of the the the whatever

the processor is doing with memory so um this is saying okay at cycle zero the processor is going to write because this right flag is one the value 17 to address three so we're writing to memory at address three then later we write um uh you know something to address seven and then we read from address uh three and then we you know write to address seven again read from it right so so on and so forth um so basically uh what happens is during we actually sort of do the execute the generation of the witness in two phases the first phase we actually execute the risk five processor and we produce these memory transactions

and there's no specific verification of the memory transactions we just are recording um we just model ram outside of the proof system and we just record the transactions that happen then what we do is we resort all of the transactions so that they are sorted by uh address first and cycle second and put them into a different set of columns in the execution trace so what you see here is that the um these are of course the add all of all the transactions on address three and all the transactions on address seven they are all together because they've been sorted by address first and cycle second and these are in cycle order uh now what that means is that once you've

sorted them that way we can verify that a memory that the memory traces are correct that they represent a normal actually functioning version of ram by just looking at local relations between multiple rows specifically uh we can basically say that well okay if the addresses are the same then we then it must be the case that uh the cycle is going up and also if we are not writing if we are reading then we need to have the data match the data in the line above so that basically what happens is oh actually this first one is supposed to be a one sorry about that that's a one um uh so so so in this case this was a read so

it must match must read must match this is a write so it can be whatever it wants this is a right it can be whatever it wants this is a read it much matched the previous line right so basically by doing that we are able to make all of the checking of all of the memory transactions local now of course we also need to prove relevantly that these memory transactions which are occurring in order and being used by the rest of the system to actually emulate the risk processor actually match our our permutation of these transactions and that's exactly what planck is designed to do so planck allows you to verify that two sets of data inside of a zero-knowledge proof are in fact permutations of each other and so in combination with the check that we do on the plonk side that these

are permutations this then verifies that all of our memory transactions are valid so that's how we implement basically ram inside of the proof system so i want to talk a little bit about how this system interacts with the outside world so in the case of the program code that's initially loaded and that's sort of part of a special set of columns that are known to the proven the verifier but in terms of the program data how does the the the vm talk to the host that's running it how to see how do you put your secret data into your uh you know system how do you get secret data out of it um and so in order to do that um what effectively happens is that

when you're executing the program in normal order cycle order when the when when the guest the vm writes to some well-known address the host who's doing the emulation just notices that and certain special addresses are just considered to be um io addresses and so when there's a write that's written there the um the host is like oh i'm some data for me right and so that's how you send data from the guest to the host for the host of the guest we actually rely on the fact that if you look at our constraints for the memory there's no check about what the first read of an address that's never been written to is so when you read an address that's never been written to it can be any value you want at all and so what happens is the guest

simply when it wants to get more information from the host reads from previously unread addresses in a special area the host detects that there's a read occurring there and just fills in the value with whatever the host wants to communicate to the guest and so that's how we actually send the data from the host to the guest so the guest is referring to uh your vm code or guess is referring to the risk five code running in your the guest is it's referring to the the vm and the risk five code running inside there yeah so i think we like to think of the so we just we're just using we're we're trying to like the anything running inside the vm is guest code and it's running in the guest and anything that's being run outside of the zero knowledge proof system is the

host so the guest is secure the host is not to be trusted necessarily if the guest code should not care what the host is doing well this is the ah so generally the guest code will want to do some verification of some property or whatever you're trying to prove so for example for the battleship game we have um the guest wants to verify that all the ships are positioned properly and that they don't overlap with each other and that there's five of them and they have the right links and all these other sorts of things so in order to do that the first thing it needs to know is where are the ships located you don't want to put where the ships are into your actual code that you're running because that's known publicly right by everyone so the guest has to have some way of getting

its initial data from the outside world and so this is the mechanism by which we get data from the outside world and then thereafter you typically would oh yeah okay okay um uh and then and then of course so this represents basically the private data um and then uh what generally happens is that uh we have the notion of a journal uh that we that it's basically a special area of memory inside the vm that gets written to that basically stores whatever the uh proof prover would like to publicly assert so whatever in this case for example it would be the hash of the battleship state or something like that and so that they just we just write that to a region of memory then we use our

sha acceleration circuit to sha that up inside of the proof and then that's output by the proof and uh comes along with the proof so effectively the output of the proof the public part of the output is only displays this sort of journal so you basically decide what you want to make publicly available on the proof um uh so yeah that was pretty much the the the memory system as it is right um we were going to have uh in the booth we have this battleship demo it was going to be we were trying to make it high stakes that part didn't get done so we were really hoping you could bet on battleship uh here at battleship but we'll have to wait for the next conference um with that i just questioned i'm guessing most of them are going to be for you

yeah and so we have plenty of time for questions we're going to try to sync up with the main stage so take your time they're about 10 minutes late so yeah go ahead how wide is the execution trace how many columns do you have uh about 160 currently um so right now we have a so by the way this is all open source you can go to um uh you know github and go download the prover and the verifier um oh yeah that would have been good uh but it's it's uh risc the number zero is our github uh um handle anyway uh so right now we're it's about 160 columns wide for the data

portion um that includes uh but a lot of that right now is actually being used to do range checks uh via bit decomposition and a bunch of other things that you know basically as of the invention of pluck up and some other things obviously are a little bit old school i suppose i would say and so we are currently in the process of working on a new version of the circuit that we anticipate um will be significantly more concise in terms of the the representation the degree of constraints uh five yeah so we actually do have expansion of four basically for the for the start i'll go ahead yeah for people less familiar with

all these all these fractions says is there uh is it fixed with code format or not yes so it's unrelated but they just no no totally so the risk five uh okay so the question was um uh the op code for the risk five uh you know isa the risk five instruction set what is um whether it's a fixed size and uh yes uh so risk five we picked for a number of reasons um one um it's a very small uh isa uh the necessary uh instructions that you were required are very very limited but it has extensions and uh has a very principled way to add extensions so you can you know you can you can have or not have a multiplier you can have or

not have floating point right it's also got a very simple instruction decoder it's meant to be implemented in a very small amount of silicon and while digital circuits and arithmetic circuits don't look exactly the same they do share enough that it actually is a innately a good um architecture for implementing for any of existing architectures yeah yeah and the second one is for curiosity what is your memory model in terms of addressability by bytes oh yeah so so yes that's a very good question um our memory oh yeah so the question is is the memory model how does it work is it bite addressable is it word addressable and as you notice we

have one white one right transaction per cycle and so in order to make that um have a decent amount of memory bandwidth we actually write an entire word or read an entire word at a time and they must be read uh with alignment luckily for us the risk 5 processor spec allows you to require strong alignment and falter if you're unaligned so um so that works out very well for us um so you can do read a byte or a short um uh in risk five instructions as well but we read the entire word and then you know and actually by the way that's also why we also have one we have a read on one cycle and a write on the other because if you want to write a

byte you have to read the whole word modify the byte write it back out again yes so this is all sort of microarchitectural things right so um but people who are familiar with um you know asic design would certainly know all these types of things anyway all right time for one more question i would say go ahead yep no no fundamentally what we're because we actually look like a risc-v processor which is a standard kind of an isa that's well understood by the industry i mean there's already versions of gcc that compile to risk five and we fully implement the entire processor spec we are compliant we pass all of the um

compliance tests made by the risc-five committee so we're completely real we look like a completely real processor running inside of a zero knowledge system so c plus plus go um you know rust now we do have some standard libraries that do things like read and write to these magic memory addresses and then turn that into something that looks like a you know operating system read and a write call and some so there's like you some standard library support you want for your language in order to make it easy to use but fundamentally anything you can compile with llvm you can compile with our stuff it's helpful sweet thank you [Applause]