Keccacheck: towards a SNARK friendly Keccak

Transcript

Hi everyone. My name is Greg. I work at Rail Labs. It's a zero knowledge and formal verification research and development company. And today I'm going to talk about how we made proving Keccak fast in zero knowledge circuits. For context, Keccak is the hash function used by Ethereum. It's quick to compute, but it's famously difficult to prove in zero knowledge circuits. And SNARK is a type of proof system that generates succinct proofs that are cheap to verify on Ethereum. Therefore, they're widely deployed on Ethereum.

We call the protocol Keccatek from Keccak and Sum check. And let me start with some numbers. This is a comparison against proving Keccak in GNARK. And the charts are in log scale that log scale that doesn't really matter. But the key insight here is that um we start winning only if you have at least a dozen Keccaks to prove. Uh so we sort of strike start breaking even at about 16 to 32 Keccak instances or Keccak permutations. But at 256 instances, we're already 10 times faster than GNARK. And we just, you know, continue scaling much much better. Um and on average, if you have thousands of

Keccaks to prove, we're about 1,800 R1CS constraints at the current version of Keccatek and it actually gets better in a future release. So the first question is is this is this even practical? Like, do do we need a proof system where you're proving dozens, if not hundreds or thousands of Keccak instances? And I think the answer is yes. If you're doing storage proofs, if you need to prove anything about Ethereum state, then every single fact is going to involve, you know, 20 or 30 Keccak hashes to verify Merkle proofs.

Um and then if you have more than one fact that you want to prove, then obviously you're going to have more and more. Uh second obvious use case is ZK-EVMs. They have to calculate a lot of Keccaks inside to calculate addresses for mappings and addresses for accounts and all of that. So they also typically deal with hundreds, if not thousands, of Keccak hashes. And then also ZK-EVMs, not necessarily EVM-based, are going to can benefit from this solution. So the way ZK-EVMs typically work is that you have your program. It can be Rust.

It can be some domain-specific programming language. And then you run run a protocol like a STARK that's very fast to to your computation. But STARKs tend to to generate fairly large proofs in the order of dozens of kilobytes. Which are still too big to be able to verify in Ethereum. You'll take, you know, hundreds of dollars to be able to if if it's even possible to send that to Ethereum. So STARK proofs not really usable on EVM chains. You typically need to wrap them into another proof system, a SNARK, that's going to produce something that's more Ethereum-friendly.

And what the STARK prover is going to do is essentially verify the STARK proof and provide a level of recursion and generate a proof that's fairly tiny and easy to verify on Ethereum. And the SNARK is something that needs to do um thousands of of hash computations to be able to verify the STARK proof. So because of this, the way ZK-EVMs are typically structured, you have a STARK proof and then you have a SNARK proof and you have to deal with some hashing on on Merkle tree. And typically projects do something like Poseidon or Poseidon 2, which is cheap to compute in SNARK, but it's about 10 times slower

than Keccak. So you end up with additional overhead for your STARK. And what we're trying to do with Keccatek is if you have enough of those hashes, on average, it might not be that expensive to switch from Poseidon back to Keccak. But by doing so, your SNARK is slightly slower, but your STARK is Keccak itself is 10 times faster than Poseidon. You spend about 40% of the time in Merklization. So your STARK ends up being four or five times faster by switching to a faster hash function.

So how does the protocol work? We only have 10 minutes, so I'm going to give you a core idea. But the idea is that we use something like GKR where you represent your input data as a multilinear polynomial. Your output, your hash digest, is also a multilinear polynomial. And then you layer polynomials that represent hash operations. So they they can be something like XOR operation, bit rotation, stuff like that. Um But the problem with GKR is that this graph is very dense. So typically, the way it's phrased is that it's almost looks like a general-purpose programming language where you have a predicate function that's going to tell

you which inputs go to which outputs. Um and then each of these little dots is like a gate, which may be addition, multiplication, or some other binary operation. This GKR protocol is great because this is what allows you to to scale with as you add more instances, the number of variables in these polynomials grows logarithmically. So this is what gives us the benefit for scaling. However, the GKR protocol is in the usual formulation is fairly slow. Um and so because we have to do all of that wrapping, it ends up being not worth it because the GKR prover itself is very slow. So what we did instead for Keccatek is instead of doing the regular GKR where you go layer by layer, you

have to propagate all the data. You have these constraints on how you structure your computation. We forgotten about all of that and we decided to sort of handwrite polynomials for every single operation that happens in Keccak to make it super optimized for that one specific computation. We got rid of the usual constraint of going layer by layer, so we can have like a side polynomials that represent some arbitrary data that we need in the algorithm. Again, this is not enough time to go into full details of the protocol, but we have a fairly approachable blog post that gives you a better overview of what's going on inside.

Inside that blog post, you're also going to find a link to a white paper where we give you all of the polynomials involved. There are like seven different operations in Keccak that are repeated 25 times. So even though the the algorithm has like 200 layers, it's just seven polynomials that you need to understand and they're fairly easy to understand. There's nothing nothing magical about them. And then in the blog post, you're also going to find a link to GitHub repository where you'll find the existing implementation. Uh And then we already started working on a version that's even faster for larger batch sizes. I don't know if it you can see, but like this is GNARK. This is current Keccatek and this is sort of the new version. The reason why we were able

to get win at the bigger batch sizes is because we use weird commitment scheme um that gives us high fixed cost, but then we can commit faster to really really large instances of the problem. So like the end result is like a curve like this. Um And then we're also looking into Blake 3 hashing. Blake itself is faster than Keccak. It's a little more involved, so the polynomials to be written are are much more difficult, but it's something that that might be interesting. Um and then after I submitted my slides, I saw there was a tweet from Justin Thaler, who's like a godfather of GKR.

He was listing all of the ideas to make Sum check, which is the underlying protocol, faster. And I think he mentioned it's like 10 times faster in Jolt after they implemented Sum check improvements. So this is another thing that we might want to look into. Thank you. This is the same blog post, by the way, if you haven't had a chance to scan it before. I don't know if I have time for questions. So questions? I have time for questions. So you've mentioned that you're using some weird commitment scheme. Can you tell us a little bit more about that?

Weird commitments? Uh I I cannot. I was not involved in the sort of like the second stage of the project. But essentially I don't know much about the commitment scheme itself, but one of the ideas was that in the original version, we have to commit to like every bit is its own field element. And then with the new version, we can commit to sort of like wider words that are like 64 bits. Weird itself, I'm not entirely sure how it works. So but I'm happy to get back to you with input from my colleagues.

Um it it sounds like you're what you have is a a custom arithmetization maybe of of Keccak. I wonder how you envision that integrating into general-purpose ZK-EVMs. Maybe as a precompiler like some custom Yeah. Yeah, so the way ZK-EVMs would typically work is that they have precompiles for hash functions, for elliptic curve operations, and for all of all of that. And they have some sort of like an accelerator on the side that does its own proof for those precompiles. So the way you can integrate Keccatek is you take the GKR part, which is the sort of accelerator, and then instead of wrapping it into a snark like

we did uh for Ethereum uh verification, what you what what you can do is you can like do whatever recursion you're doing in your own uh ZK VM to verify the GKR proof uh that we're producing. Uh a quick follow-up, I guess, is um do you have any insights on these custom handwritten polynomials? Like what um what are you improving on? Um and yeah, what's what's the what's the special secret sauce there? Yeah, there's uh lots of cool little tricks.

Uh one is uh in in GKR, uh you typically sort of like a have a flat array of your state. Um and that ends up being very wasteful for Keccak because the state array is 25 words, and then sometimes you need to uh carry on 10 auxiliary elements, which is ends up being 35. Um but the way GKR is structured, you have to have 64 uh sort of words. Uh so, you know, most half of the space is wasted, and you pay for that computation. Uh so, what we do instead is we have uh sort of like 25 separate polynomials, and then we do random linear combination, and that that trick saves us, you know, uh half of computation time. Another trick we use is for XOR

gates. Uh if you represent bits as ones and zeros, uh they're not coming coming to take it. But if you replace ones and zeros with -1 and 1, you can do regular multiplication, and you can like do like you can rearrange your your uh computations to extract some multiplications like before parentheses. Um another thing is that like we get to skip like because we do random linear combination, we don't have to like go level by level, but we can have some things on the side and uh sort it into uh our layers when needed.

Um yeah, I'm sure there were like the the the blog post lists all of the sort of fancy tricks we used. Uh there's just a lot of little wins uh that we were able to score for something that I think was I want to say 100 times faster than like a generic uh GKR. Cool. Thank you.