ZK11: Sharing Randomness in Distributed Proving - Tamir Hemo

Transcript

[Music] thank you all for being here um my name is Tamir uh from cinct and I'm going to talk about uh the continuation argument we use in sp1 so the short outline of the talk is we're going to start with like an overview of the basic architecture of sp1 then we're going to mention uh the problem of spilling large proofs then talk about the succinct solution or just the succinct solution uh and then we'll see the trade-offs with this solution the implications and then hopefully have time for

questions so sp1 is a new general purpose ckvm that we released uh last month or so and just a few details about it it's verifying risk five instructions um um and we use fry over the baby bear field this might change soon uh with circle Stark but so far we're using baby bear uh the arithmetization is based on uh an air or as you would know it as a stark with lookups so a stark air with Randomness and one of the key principles is to have a modular design so that it's

really easy to add other tables or as we call them promiles so how does it work uh what's the basic architecture so in the basic the most basic building box are the the air tables so for every simple unit of uh logic we have its own air table so we have a table for a CPU we have a table for ketak we have a table for uh elliptic curve operations and some people that in the community added their own tables and they can easily integrated uh into sp1 and it doesn't matter how many tables there is you only pay for the tables you use in our

prover um and the missing link for them is that they communicate through a bus that is based on some uh I'll I'll later explain how it's implemented but basically like what the bus is is you can send every table can send arbitrary tles of information into the bus with a certain Multiplicity and the bus argument is that all the multiplicity add to zero uh another nice thing about this bus argument is that the memory uh check that we have is also implemented entirely in the bus so there's no memory table it's just uh sort of a virtual table and it's all through the lookups

it's this memory argument by uh Bloom at all offline checking of memory now let's see how this works really so let's say I want to execute the instruction add so I'm going to use the same symbol for the registers and the values just to save notation so I want to fetch the values in b and c and put in a the sum B plus C so these are u32 or i32 whatever you want then the CPU will like know the CPU table will have a row that says the instruction is now add on a b and c and these are the values and it won't prove that a B plus C it will just put this stle the clock cycle add ABC into the

bus with multiplicity one so now the bus is loaded with this thing and someone has to take it in order for the argument to work and the ALU table which is responsible for all the u32 operations actually the L is several tables in our implementation will contain a proof that a is equal to B plus C and we'll send this topple into the bus with mul icity minus one minus one is really just P minus one um and this is using glog up but again it can be um any permutation argument works for this I'm just using our our own um convention so this is nice I can just do

that let's see what happens with the precompile so the same principle let's say I want to make a KCK permutation and I have the pointer to the uh the the spawn State then the CPU will just say oh KET permute this sponge uh slice and put the pointer into the uh the bus and the bus will then have to satisfy it so the Kat table will actually interact with memory on its own because everything is done through the lookup will make the proof that it's valid and will put the the same topple back into the bus with multiplicity minus one so that's basically how

everything is glued together great but now what is the challenge so as any ZK VM general purpose has to do uh if we have a large execution Trace we have to split it into several proofs well first it's necessary because the size of the trace is limited especially in baby bear where it's really like just two to the 26 or something so we really hit that limit also proving large traces takes a long time there is asymptotics that are unfavorable for large traces and most importantly actually in practice more parallelism is enabled with smaller uh Shard sizes so if my sh

for example we use like 2 to the 19 right now is default you can change it as a it's just a variable you can change so really like then you can just prove stuff in parallel and it's completely parallel almost we'll see but basically you can enable more parallelism control agency and lower your costs now how do we split the claim really there's two stuffs you have to do so sp1 so the boxes that I showed earlier has two things there's the boxes themselves the traces each Trace is just an air table so you have to verify the table constraints so there is initial

constraints final constraints and transition constraints then you have to verify the bus argument that each multiplicity sums to zero now the first part is actually not a problem because you can because the air is already kind of like transition local you can just cut the table at any moment and you can split your table that's fine the problem is really the bus argument how do you like now that you split the table the sum is no longer zero so how would you even verify that or how would you even do a bus argument with independent proofs if you guys know how permutation arguments are actually implemented so this is really the big

problem so really the problem is how to split the bus argument and how would you do it so the common Solutions are usually uh make your transaction or like your Atomic unit of execution small enough that you can just stop the program start a new program you don't have to save any State uh another thing which is for example what risk zero does is modify your claim so that there's really no interaction in lookups between the different charts so in Risk zero thing they will meriz some of the memory so they commit to the memory State between continuations um and we kind of like when we were going to implement um our

continuation argument I was really kind of lazy to do I just didn't want to do it so I was trying to think like what if we try to pretend that it's really just one proofs and maybe not split exactly in the beginning of the proof but split in some other way so you can pretend uh but this pretend has a cost like any pretense um so in order to understand this cost we have to kind of know how the bus works so this is the most equation heavy slide bear with me so how does the bus work as I said you can send arbitrary topples into the

bus but with some multiplicity and then someone else has to pick it up in order for the argument to be valid so what do you do let's say you have a topple t0 T1 T2 like our add ABC clock tople that we had before um first I'm so I'm used doing that by using verifier challenges so I'm getting two challenges from the verifier the first challenge Alpha I will use to fold the topples into one value so these challenges are in an extension for baby bear they're in a Big Field they're is an extension field so first I will fold these uh topples into one extension

element using this uh first challenge Alpha now that I have a folded thing I can add it to our uh bus so our bus is represented by one value really in the extension field initialized to zero every time I want to input something into the bus I add with some multiplicity M I add M over beta minus this read Solomon fingerprint of it that's just the name of it but it's really just folding it as a random linear combination with powers of the challenge and because all these denominators are unique so this is like a this is basically the idea of log

up I can do any multiplicity here and it's really cheap to change the multiplicity and each value here is unique so it will only be valid in overwhelming probability if all the multiplicities match up to zero or if and only if this Sigma bus is zero so this is what we want to split so if we want to split this between shards what do we need first the basic thing the basic issue is we need them to share Alpha and beta but Alpha Beta are derived from F chamir so we can't just like take values derived in one Shard and use them in another we have to have everything inside the F of course there

was a talk about this earlier today everything must go into the F so how do we do this well we can still do this by paying some cost in um complexity of execution so I kind of made y work easier but the work of all the people doing the cluster stuff is harder but I I assure them that it would pay off and so far it seems to pay off so what do we do we basically commit to all the execution traces of these tables without doing any permutation stuff and that is part of the computation that is usually for us not the bottleneck um

so we do this computation and then we can load the Challenger from this this is the how you if you had one proof this is what you would do so this is the pretend part you get those random challenges and now you can do fry proofs separately so after the challenges you have constraints and proofs and the important thing though is all those charts have to start from the same same Challenger that has the entropy from all of them so there is a two-phase process instead of continuation being one phase a one-phase process it's a two-phase process but it saves a lot of overhead it's basically zero overhead um on on the intera on the continuation so that's basically was our

reason for it and we kind of like we started from the fact that like this is easy and if we want to change it we can change it and we still might like we'll see in the end if if this is this is only the you know version one maybe it's in the end will be more efficient to do other things so what are the advantages of disadvantages so for us the advantages um first it started with just continuations but actually then we found more advantages um so zero overhead for the memory but then we can also realize it makes it made it easier for us we had another problem what about pre-compile so if I have a long program I only have if I have a few billion cycles of a

program but only a few hundred cats I don't want to have a Katch at every Shard I want to have Katch in one Shard so obviously we could do that without this scheme but this scheme actually gets zero overhead on that too so one chart can have only ketak and just put all the katak stuff in the bus and not know about the CPU so we can prove the katak separately and prove even the add instruction separately and we can divide the shards however we want so that's a really nice uh solution we got from that our shards don't have to be um causally related to each other they could do whatever they want as long as each table is correct and as long as the CPU is

correct so the CPU is kind of like the king of this um proof so that was really nice um so yeah so the F the last point is this is aggregation of different operation across shards right so I can use only one Shard for a precompile of course the disadvantage is I have to wait for all the commitments to be computed before I start proving so it's a two-stage process instead of a one- stage process but we actually found that there's not much overhead um naively you may have some communication overhead but we kind of eliminated that but just like when we continue proving every Shard will just recompute the commitment of the main Trace which is really again

not the bottleneck and really fast so we found that this was like very zero very minimal communication overhead the only overhead is of course a two-stage process another issue though is of course you cannot execute arbitrary programs like this if you have a single proof the security of your proof is limited to the length of the entire Trace along all shards together because that's what the challenge is canceling out that's what the you know if you know the trma this is what appears in the denominator so of course um this is a a limitation but for us it's actually not a problem because the only programs you

will prove in ZK are small enough that it's fine or if they are so long it means we need more PR compiles maybe so in practice we didn't really have an issue with that the number of shards is usually controlled and again we'll have like soon we'll have also like a little assert that will tell you your program is not Kosher but again this is not happening so to conclude um we went through the basic architecture of sp1 and actually any like lookup oriented VM also like is basically looks like that or most VMS like Risk zero is a little different um but a lot of lookup based

VM kind of look like that um then we talked a little bit about continuations and really it's just about the bus our solution was to share challenges via two-stage process and for us there's a lot of um s uh advantages which is like zero overhead very simple in the code the code is very simple because the arithmetization doesn't have to account we don't have to augment your rust code with like hashing memory tables and do more assist calls of memory management and so it's faster cheaper proofs and we also have flexibility in organizing the workload which we experimented with a little bit and it could be beneficial so

like for example some machines can be heavy and do the big tables and some machines can also do the small tables so it's kind of nice to have that um and that's basically all question thank you thank thank you thank you very much it was a great talk uh we are officially on break but if there's like one question what a quick question here can we get the mic um that will be can you come to the front hello thanks for the talk very

cool I was wondering for security do you need multile challenge because you're working on a small field no so it's actually the challenges are already in a Big Field we take challenges that are in an extension field of the G four right but you need two challenges because you're doing two different things com because you're also folding so they have to be orthogonal to each other so you're first folding and once you folded you you do this also like if you notice another fun thing for that is um here we need to have the clock here to make the message message unique so there's a lot of like we have to make sure the messages are unique and the multiplicities are really

representing what they are