ZisK Recursion in Lean 4

Transcript

[applause] >> So, a big disclaimer before starting is that this is totally work in progress. So, there are things that are halfway through it. There are things that are just basic ideas or future ideas that we want to tackle on uh anytime soon. Uh but at the end I think like the idea of this talk is to present uh the road map that we have to prove the recursion for Fisk. Okay? I'm not going to talk about proving the linearization in Lean and so on. This is probably a topic another topic. But I'm going to focus on the recursion. Okay? We are we are in fact planning to use Lean like in two different roles. I would say a

passive one and active and an active one. By passive one I mean um uh like the traditional way you you've using Lean. Say, for example, you have a paper proving uh that your recursion is safe or or that your recursion is safe. Okay? And you basically implement uh the specification in Lean. You write down the proofs. You see that the kernel is giving you the okay. And then uh basically the the the trusting limit that you have is that you have to be sure that what you've written in Lean versus what you have in the paper is consistent with each other one-to-one.

Okay? And the active role of Lean is that we are planning to use uh Lean to substitute some parts of the current uh tool chain of Fisk. Okay? In particular, let's say we have something that we call the setup that is like the entity that is in charge of generating all the circuits, all the verification keys, uh and in general all the artifacts that the prover has to consume in order to generate the proofs for all the recursion um uh all the recursion topology. Okay? So, that would be like the active role.

So, but anyways, before everything, let's start with the basics. Uh and let me recall like the four different steps that you need to take into account when you design the recursion for a zkVM. So, in essence, the common input is a a program and a an input to this program. This program can be written like in a high high-level language like Rust or C. There is also people writing this part in uh in in low-level languages like writing directly in RISC-V. Like for example, I think the EF is writing the full state transition function in RISC-V. And this is very funny.

Uh which from an optimization point of view, that's like like it's like the perfect objective. And also from a formal verification point of view, this is probably the best idea. Okay? So, anyways, uh uh We compile the program to RISC-V. Or in our case, we also do a transpilation step from RISC-V to what we call the CISC ESA that you have to imagine like it has a one-to-one relationship between RISC-V. So, at the end is RISC-V with some CISC decorators.

You compile the program, you execute the program, and you got you got all these traces that you use them to generate the proof. And finally, you verify these proofs. And really, the simple goal of the whole verification of this is that you have a proof, okay? And the idea is that you are able to uh go from a proof to uh getting getting to prove that this program has been executed with this input, has it stopped, and it generated the expected output. Okay? So, that's the overall goal.

So, if we move to the limitation part, things get a slightly slightly funny. Okay? So, the first idea to do the limitation uh of a ZK VM was to come up with a complete set of constraints trying to constrain all the operations involved. Okay, so there you have the memory operations, binary operations, arithmetic, and so on. Okay, and that was like a very complex approach. So, I think we and the rest of the ZK VM teams decided to do this like of modular design. Okay, in the sense that we grouped all these constraints in a specific five short chips. Okay, so either if you go for a CPU-based um

design or a non-CPU-based design, um you have these uh groups of constraints, the chips. Okay, and then you have a method to interconnect or to uh to to make these chips talk to each other. Okay, this is normally called a bus or a channel, but the the idea is that whenever uh some chip does not know how to do some operation, like for example, the main CPU does not know how to do memory operations, it will as it will assemble this operation, it will get somehow the output of this operation, and it will create like a necessity to this bus. Okay, in the sense that this necessity will be uh

will have to be proven from from on from other chips in the whole limitation. Okay, here also you have the notion of the multiplicity that basically encodes the number of times this operation is performed. Okay, it doesn't matter if it's memory or binary one. So, the previous objective has has changed in the sense that now we are not only looking for uh a witness that satisfies all the constraints of every chip individually, but we also need to prove that the whole thing is balanced. Okay, so that the interchange of messages between all the chips uh, has been taken properly.

Okay? There is an important issue that you don't need to take into account when you do the recursion and is the unbounded the the unbounded nature of the recursive recursion. Okay, normally when you when you design this arithmetization, uh, you normally do a trade-off to find a an optimal size for these chips. Okay, you take into account the GPU, you take into account the memory, the proving time, and so on. And you fixed, uh, uh, let's say a maximum size for the arithmetization. Okay, but programs are unbounded in nature. Okay, so you have to pro- bring in this notion, uh, of continuations. Okay, you have

your execution, you cut it horizontally, and then the idea is that you generate a proof for all these gaps individually. Okay? Uh, anyways, there are there are two problems that you need to to solve and is that there are some chips that have a state by nature. Okay? You have like the owner state of your machine that you have to imagine this as being, uh, a set of registers holding some finite field element that you need to in some sense freeze and restore in the between segments of these proofs. Okay?

And then you also have the problem of memory. Okay, the memory is much bigger than the state and you need to prove that you have not changed, uh, any address of the memory in any of these cuts. Okay? So, what some teams do is that they take the execution, they cut it horizontally, and within these cuts, there are, uh, let's say, a lot of operations. Okay? They generate a proof for this back of operations and they next they they they move to the next back of all operations.

Okay? The main issue with doing it like that is that um is that all these proofs will have uh unavoidably uh a lot of padding. Okay? And some teams like SP1, what they did is well, they they come up with fancy cryptography like the Jac PCS. And instead of paying for all these padding in all these proofs, they packed the the traces in a smart way in the in the sense that they only pay a small portion of the padding uh which is uh was taking into account the the the the power of two that they are using.

Okay? In Fisk, we do things slightly different. I'd like to say that instead of cutting the trace horizontally, we cut it vertically even though it's not a vertical cut. Okay? But instead of proving this chunk of execution, we prove we need a proof for each operation individually. Okay? So, we have we we have Let's say that we have these chips. Okay? So, we generate a proof for each instance instance of each chip. Okay? So, you have to imagine like we have uh we have an entity that reads the execution and it groups uh it groups the we group the operation by their by their by their limitation and then they prove the segments in the gas of the

limitation. Okay? Okay so at the end uh we end up with a bag of proofs that we need to somehow verify. Okay, so the naive solution would be, okay, let's take these proofs and let's verify them all. We can verify all these proofs and we can verify naively naively that the the proof is balanced. Okay, but they will be contradictory with the fact that we want a succinct verifier.

Okay? So, in essence, recursion is used as a strategy to reduce all these proofs to a sufficiently small set of proofs that that we consider so that the verifier is succinct. Okay? So, in essence, there are three things that you need to verify using recursion. The first, for sure, is that all the proofs are verified. Okay? So, moving all up to the top in the recursion, all all of these nodes will basically encode a verifier of the previous layer. So, it's like implementing all over the verifier of the previous layer. Either you use the same proving system or not, you have to

take into account the proving system in particular. But, there is also you also need to verify the dependency between these proofs that boring measure. Okay? With this notion of whose balancing. You need to also verify that. And you'll see that there are a lot of attacks to these to these recursion if you also not take into account the specific shape of the tree. Okay? So, at the end, the overall goal that you'd like to formally verify is that constraints are satisfied, the tree is well is well shaped. You'll see in a future slide why.

And finally, that the witness that the witness that you're providing is fully balanced. Okay? So, we in essence encode these in Lean uh with two relations. What you call the final relation and the thesis relation. Okay? And the idea is is the the soundness of the aggregation aggregation simply means being able to go from the final relation, okay? Which basically says that the verifier was able to verify the final proof, to the thesis relation, okay? We discuss this about having well-shaped tree, the satisfaction of the constraints, and the balance of the

bus. Okay, so let's try to see all these pieces individually. And let's start with the verifier. So in the verifier is is is is a is a tough task, but it's probably one of the easiest ones, okay? At the end, you need like three things, three things, yes. You need to You need the specification of the verifier in in in your in code, okay? In particular, you have to write it in Lean.

On the other side, you have the circuits. And the third component will be the proving system itself. Okay? And there are like two reductions that you need to to prove. One is the proving system itself, and this is very static and and and and very straightforward, I would say, given the promise that there are in this reduction. So, in essence, you have to specify both the prover and the verifier. You have to define what are the notions of security of this proving system. In particular, we're interested in the round-by-round knowledge soundness of the proving system itself. Okay? And this basically allows you to prove

that the specification of your verifier is compliant with the security notion that you already defined. Okay, here is where you have to look at the papers, look at the implementations, and the different components of your verifier, and check that everything matches. Okay, this is a big task, but it's a quite a straightforward one. The second part, which is not the that easy, is the circuit part. Okay? There, basically, the idea is that you have given the specification, you have to prove that the circuit, so that the constraints given by the circuit can be reduced to the satisfaction of the specification.

Okay? And for that, what we are doing because most of the circuit that we have written for this is everyone CS based, we are we are actually actually using Selene. Okay, I think if I'm if I'm not wrong, they have support for everyone CS support and reasoning about circuits written in in everyone CS. So, in essence, we are rewriting most of the part of our verifier in Selene. Okay, in order to reason in order to be able to prove this reduction.

Okay? So, Basically, here you have like the full STARK verifier within Lean. Okay, and at the end is use a con- conjunction of various checks that you need to you need to to perform. Okay, this is an example of a univariate STARK fry based verifier fully written and working in Lean. Okay, in fact, we used to test this verifier before proving the equivalence with the circuit. We generated like I think a couple of thousands proofs with our current provers and checked that it matched this verifier. Okay, in

Okay, then we have the circuit and here is where things get a slightly more complicated for us. Okay, because I think we have a highly optimized verifier. Okay, and and and basically the main idea that we took was to mix up some some arithmetizations. Okay, so at the end you got to you you you have to generate a proof of a proof. Okay, you have to generate a proof of the specification of the verifier. So, you have to write the limitation of the verifier in a way that is amenable for a stark proving.

Okay, that means you have to write it using mainly the 80s plus lack of the limitation. Okay, but the problem is of the verifier is that it is one shot. Okay, that means that the uh So, it starts are very good at proving the same computation with different inputs many times, given that the computation itself is not that complex. And the verifier is completely different, okay? Verifier you you just have to prove it once. And the thing is that inside the verifier, it's true that there is a lot of repeated computation, okay? You have hashing, you have vehicle trees, you have entities, and so on and so forth.

Okay, so what we did at the end was writing the let's say the bulk of the logic of the verifier using R1CS. In particular, we use Circom because that's the tool we are used to it. And then we encoded all these repeated logic directly in a in in let's in in a in a dish. Okay? So, after uh writing the verifier in Circom, we needed to transform the generated R1CS uh to something that is amenable to the air. And that was uh transforming this to Plonk.

Okay? The whole history of this is that uh we had and we already have a lot of third-party external tools across all these setup generation, okay? We have Circom, so we need to trust the Circom compiler. Uh we have this series of transformations from moving from R1CS to Plonk gate, so we have to also trust or verify that these are done correctly because otherwise if we miss some constraints this is not the verifier anymore. And finally, we have the arithmetization itself that we write in our own DSL that probably most of you know which is Plonk. So, we also need to trust the

Plonk the Plonk compiler with this. So, two compilers and three transformations that we need to believe. Okay, so that's that's like the current state. So, one idea to let's say formally verify this will be to well, let's take some of these steps like take some of the artifacts that we generate through all this process and let's try to at least formally verify some of them. Okay, that would be an idea but still you have the compiler, you have some transformations that you probably won't be able to to probably lean and things get a little bit messy. Okay, the second idea is the active role that I was talking about at the beginning of

the talk and probably what and in fact what the things that we are doing at this moment is okay, this is part of the setup. This is only generated once and then we can start generating proofs. So, why not this is a super good candidate for being written directly in Lean. Okay, so instead of passing through all the compilers and through all the steps, let's just take some things like Lean probably extend them with our notions um of constraints in the AD system and from the Lean we are planning to generate all the artifacts that are compatible with the previous

ideas and basically bring them to our prover to generate proofs. Okay, this is mainly for the soundness part. So, for the verifier, if now we take into account the prover as well, well, things get this something probably for the future because we have our prover in Rust, our GPU prover base as well. It is in Rust and C. It's a combination of both. And well, in order to prove completeness, let's say, there are two options. The first one which I think is someone tackled.

And so, probably the Ethereum Foundation is using tools like ideas and hacks just to extract the already Rust implemented code of the prover from this extracted Lean and then prove the equivalence between this extraction of code and the specification in Lean. And the second is writing everything writing the prover as well in Lean. Okay? For that, I've recently seen very good results of this library called ComPoli, which basically provides you a set of polynomial operations very efficiently in Lean. And I think I read like a couple of days ago that for example,

they were comparing the entity implemented in ComPoli and the entity implemented in Plonky3 and they were giving the same numbers. Okay? I don't know if these tools can be extrapolated to GPU-based provers but that would be interesting to follow. Okay? So, it's like but so that that's finish up like the first thing that you need to check in the recursion. So, the second thing is let's say just to because I don't have a better name, you have to prove that the tree is well-formed.

Okay? So, in essence, that avoids many stupid attacks in the recursion. For example, we are doing a couple of interesting checks. We are checking that the set of let's say the set of chips that you are verifying are from a white listed white listed list. Okay? And the main reason is because if not, for example, you could take a balance witness with your own chips and you could aggregate that with let's say an outside chip from possibly another different and outside organization that is still a valid balance and then even if you departure from for something that is balanced, you can aggregate that with another chip that is as well balanced

and but is from an outside, okay? Another possible attack, for example, will be departure from a non-balanced witness and then introduce in the aggregation dummy air, which for example has no constraints, but is thought to balance the rest of your witness. Okay? So, this is a disaster attack because you're departing from a non-balanced thing and then you're proving trivially a balanced thing. Okay? There are sorts of more attacks regarding to the to the shape of the tree.

Okay, and finally, uh we'll need to prove that the bush is balanced. Okay? And we are also going to use recursion to prove the third point. Okay? So, remember what I said at the beginning that bush balancing was at the end and in the exchange of messages between one chip and another one and a good way to model this even in lean is to view this like a multi-set. Okay? So, whenever you let's say whenever you use the bus, it's like you are taking things from a defined and shared multi-set and when you are adding things on the bus, it's the same as saying as that you are introducing things to this multi-set.

Okay? Now, if you take into account the multiplicity, this can be modeled as the balance can be equivalently equivalently be stated as that the sum of the whole messages taking into account this this multiplicity that works as the sign is equal to zero. Okay? Uh the problem is that checking this directly is not succinct is by far not succinct from one side because the all the chips the chips do not have access to the witness of the other one and and the second one is because you have to have access to the witness itself.

Okay? So, there are different strategies to solve this problem. The most famous ones are using lookup and get product. But they depend on a set of challenges. A more novelty one is using EC multi-set hash, which I think this was used by SP1 at least in the past. Okay? The problem with this one even if this one does not requires any use of challenges, but the main the main issues that well, it's not post-quantum resistant in theory, right? So, here either you use one or the other one, there is an interesting open problem for me.

That is that it would be nice to be able to come up with a way with these ways of computing a digest that is computational, which means that it does not depends on any challenge because challenges create these dependencies on the chips. That is post-quantum resistant and that makes no use of hashing. Okay, which is like the current bottle neck of the recursion. Okay, in the particular case of Fisk and this is something that we'll be proving in the recursion is that we use lookup.

And the way we derive the challenge is by using LT hash. So, it's a a very trivial uh, lattice-based hash construction in the sense that we, in essence, take the witness uh, of each of each chip. We commit to individually to to each of, uh, these witnesses. We hash to a vector, okay, taking into account the particular type. And then we use vector addition to derive, uh, let's say, a a common resulting vector to all the to all the to all the chips, okay? With this, uh, with this result together with the public inputs, we, basically, we do

plain hash, uh, from which we can obtain all the challenges needed in the in the lower argument. Okay? So, when we, so, it we we we do like, uh, two-way proving in the in the, in the same iteration, we, like, we compute all these commits for the first time, and from these commits, following the the argument that is I described before, we're able to compute all these challenges. That is exactly what all the layers need, uh, for the lower argument to be to be sound.

Okay, so, this is like public inputs to all the brewing structure. Uh, well, and from this, we do a typical recursion ideas, okay? So, we aggregate the proofs, and through all these aggregation, we check that the root is balanced because we get the contributions that we add them all until the top. And we also check that the previous derivation from the previous slide is done correctly, okay? So, we have the contributions, we map them to vectors, we add up the vectors, and then in the final verify in the root of this tree is when we certify that all the arguments are being hold, okay? So,

there we are checking that the log up is consistent and then the challenge has been derived correctly. Okay? So, aside from that, we have to deal with the cryptography side of the recursions, which basically means that we have to be able to prove that from a satisfying final proof, we are able to extract all the proofs on the bottom of the tree. Okay? And well, following quite closely what the ZK-VM did for their ZK-VM architecture, we were also were able to give a bound for the soundness of an adversary trying to

extract all these witnesses. Okay? Very intuitively, the soundness analysis basically takes into account the the first three terms, taking into account the particular proving systems that you are using throughout the recursion. The fourth term is the log up soundness, okay? The fifth term is the hashing thing done in the challenge derivation, and the final term is the is the security of the commitment scheme. Okay?

And well, basically, that's it. Thank you. >> [applause] >> ANY QUESTION? >> UM CAN YOU EX- go back to the very last Yeah, thank you. No, that Yeah, the the theorem. How do you model the like heuristic instantiation of the random oracle here? >> Yeah.

Yeah. so So, if you I I don't know if you have took a look at the paper, but there is a there is a couple of uh idealizations that are taken in this paper. One regarding to that. Okay so So, the the the idealization is that this is in essence done for granted, basically. Okay, so So, Q Q basically measures the number of uh random random queries that you do to the random oracle model. And we over assume that you can know that you don't do more than that.

>> Okay, so maybe let me explain because like the what what Zcash did follows the thing in the in this vanilla CKVM thing. Um So, what we do in that paper is that we just use a idealization of knowledge soundness that came up when we talked to a lot of people and like, you know, we had this issue this very issue in mind that, you know, you actually you cannot do it in the random oracle model. Um And the idealization is very stupid.

It's essentially saying, you know, you when you get a proof and it verifies, you press a button and you get the witness. And uh this is also that there will be a session tomorrow about this. There's also a uh sort of a lean analog of this vanilla CKVM paper where we also have right now this over idealization and it's like very active work now to find a much better heuristic because this is a stupid heuristic. So, uh uh and this will be the topic of of the session tomorrow with Ron. But I think, yeah, what what Zcash is doing is just following what what we did in that vanilla thing and currently the best we have even though it's pretty bad.

But yeah. Thank you. >> I have a question maybe about um about what you said at the beginning and middle of the talk about the usage of Lean, both passive and active. So, in you said in one of your slides that in the active side, you wanted Yeah, exactly this one. You mentioned that in the future you want to do the prover in Lean 2. Did you measure like the performance that you may lose or gain in this case?

Because I am a very beginner like in in Lean, but my first experimentation were about the fact that this kind of slower, potentially and sometimes much slower due to the fact that for example, there is no SIMD instruction and stuff like this. For the GPU context, I don't know exactly what does mean, but maybe this could represent a huge slowdown. >> Do you mean the CPU based or the GPU one? >> Both.

>> I mean Regarding the CPU, the CPU one, so as I said, there has been a lot of progress using this company library for the compared CPU implementations of of the proving side and they seem very competitive because numbers are very similar to what you have from Plonky So, so from what you have from Plonky 3. So, in the CPU side, probably it will soon be solved. In the in the GPU side, I have no idea. If Which which numbers will we get and what is the progress in GPU proving with the Lean?

>> Um I have a question with say I want to audit like this FE work and I want to make sure that it's it's faithful to like the Zisk. Uh I don't know if you're using rust like implementation. Um what what will I actually need to like me as a person needs physically read? I'm assuming like verify a spec the proof of spec when my uh is finished and how much of it can I just sort of like ignore because it's been proved through some theorem or whatnot. >> So, which is the question? Can you Can you >> So, like how much like how many lines approximately do I need to read through to be confident that like this FE of the specs and the FE is like faithful to to the actual Zisk?

>> You mean if it's You mean if it's practically possible or do you mean how many time we're going to take to do all of that? >> Yeah, I mean how long will it take me to audit? Like I I want to you know because the the FE project as of right now because you're not using like extraction or something is proving properties about something which could be different to what Zisk is actually running right? >> Yes. >> Um and I want to be make sure that what you're actually running in production and on the blockchain is equivalent to what you've proven theorems about and not just some some other similar like protocol. Um how much do I need to read to to to be

confident that that's the case? >> So, in this presentation I only discussed like the recursion part which I think is probably the majority part across all the ZK-VMs. Then you have which is I would say like this is like the back end part of Zisk. Then you have the probably the more problematic one which is the front end which is proving that your set of chips or your circuits are consistent with the with the you say you know our computer modeling the risk five offset. Okay, I I I think that for the for this back end part for the recursion it's just a matter of um just a matter of months I would say to finish this all

up. And because it's like the part that is more reusable across all the teams we are going to fit each other. Uh for the front end part, I'm not that sure. Okay, we're exploring things. For example, we have uh so there is people within our team who is trying to explore the use of SMT solvers for putting the consistency between some of the chips and their specification. Okay, and that would be awesome because then because these chips are changing a lot from a version to each other, it would be awesome to use change the version, press a button, and everything is still formally verified. Okay, but still there is a lot of work to do in the front end

part. I think there is a guy in Foundation called I don't know if if he's around here, but he worked on the front end part and he was able to prove consistency between a subset operations and this side. Okay, and he did it successfully. In fact in fact he found let's say a good amount of bugs in the fiscal immunization. Okay, but I think I think he spent like three or four months just to prove a subset of all the operations. I think he just proved the basic ones like the ones included in in this side without taking into account pre-compiles. Okay, and this took some months.

>> So one comment is like you still needed to read either the last compiler or the output from the last compiler even after you prove the last source with any S or something. You had some comments about verifying trust to some compilations for circuits from Circom and PLONK. Yes, so what I will do here is to make uh many formal circuits in clean for each of these intermediate things and all of them have uh very similar or the same specification and the proof of which uses the previous step and uh the equivalence of the compilation step.

And so the the the point here is that uh you don't have to verify the compiler for general cases. Just uh the artifacts you have in the middle. >> have to verify >> Yeah. >> like the the the >> Yeah, we dump all compilation process with explanations and uh you ask the agents to write down that into the improve or something like that. >> Yeah, we can we can take the constraints, we can extract from the constraint line and just check for this specific version that uh it holds. And if we change version because we are changing some of the files when we run it again. Yes, I agree with you. >> Yeah, while you are changing things, yes, this is not economical, right? Yes, I I think so.

>> Thank you. >> So, for the clean uh verifier formal circuits, do you intend to include the security properties of the proof that it's verifying in it? >> No, for for Selene, we are just aiming for the circuits themselves. So, you have the for example, you have the implementation of the entity, then you re-implement the entity with Selene in the in circuit shape, and then you prove the relationship between these two. So, you you you have to prove that you go from the from the constraints to the spec safely.

And this for the all the parts of the verifier. >> Well, out of time, Hector. Thank you so much for your presentation. >> Thank you. >> [applause]