In the three years since Mina launched on mainnet, a lot has changed in the proof system that powers Mina’s succinct blockchain, bringing us at last to the goal of Mina as a Proof of Everything. A combination of old techniques and new, high-powered research have come together to make a proof system optimized for recursion – designed to bring proofs together from anywhere to create a single, succinct, universal proof. With the recent Berkeley Upgrade on Mina’s mainnet, we’re proud that Mina is powered by Kimchi, the proof system that makes the magic happen. As we thought about the future of the proof system, we knew that we’d only just begun to unlock its potential.
What’s old is new
We started by upgrading the fundamental pieces of the foundation of the proof system. On v1 of Mina’s mainnet, we had a PLONK-based proof system, powered by 3 ‘columns’ that each operation could use, the PLONK permutation argument, and some extra operations that made Pickles – our recursion layer – efficient enough to use in production. However, 3 ‘columns’ were not enough; `a`, `b`, and `c` could handily describe addition (`a + b = c`), multiplication (`a * b = c`), and even Mina’s Poseidon hash function, but getting the most out of the cryptography required us to think bigger.
Today, Kimchi has 15 columns, unlocking much more flexibility. The Pickles recursion layer spent a lot of time and constraints dealing with elliptic curve points (EC points) to make the recursion sing. With clever design and careful tweaking, we could make those operations over 10x faster, giving a nice power-up to Pickles and Kimchi. Additionally, Mina’s signatures use the same kinds of Elliptic Curve point operations, so Mina’s protocol circuits benefited for free. Nice!
With zkApps coming online, application developers would need more power too. Using this newfound flexibility, the o1Labs cryptography team researched and built optimized operations for ‘foreign fields’, so that Mina’s proof system can talk about EVM signatures, bn128/bn254 proofs, and much more cryptography that was previously out of reach. Knowing that such operations are important, Kimchi was designed to be extremely flexible, making it easy to add new operations whenever needed.
New is new too
The entire zero knowledge research space has simultaneously been moving ahead at a lightning pace. It used to be very expensive and difficult to prove that a number was in a certain range or that your data came from a particular set. Not so with Plookup! As an elegant solution to these problems and more, we couldn’t resist adding lookups to Kimchi and Pickles, allowing us to support random-access arrays natively, efficient range checks, and many other neat tricks for optimizing circuits.
In the same way that Kimchi is designed to make introducing new operations easy, linking them to lookups is now easy too. We’ve already used these to support the ‘foreign field’ operations and to create important primitives like `XOR` and other logical operations used extensively for traditional hash functions like SHA256. All of this together means it’s never been easier or faster to create an application on top of Kimchi and Pickles, exactly what we need to make world-class zkApps a reality. Read how our zk Typescript framework, o1js, incorporates Ethereum signatures.
In addition to these optimizations, we also realized that fixed-size circuits weren’t enough for what we wanted to build. Pickles can always help by breaking computations up with recursion, but we wanted to do away with the limit altogether. Kimchi can now ‘chunk’ a circuit, so that you can prove circuits much bigger than used to be possible, and Pickles can use recursion to make those ‘chunks’ disappear back into a single, tiny proof. We’ll share more on “chunking” in a future blog post!
Faster is better
Changing how circuits work for Kimchi and Pickles is impactful, but we wanted even more performance. We know how critical it is for users that proving and verification is fast, so we researched and redesigned core parts of the proof system to squeeze more out of Kimchi.
Evaluations presented such an opportunity. We were converting back and forth between two different formats so that we could calculate with field elements (numbers) on one side, and create EC points as ‘commitments’ on the other. But why bother? We found that we could use the Lagrange basis to give us ‘commitments’ that work perfectly with the format for field elements and skip that whole expensive step. Win!
We went deeper on this: we were storing both formats for every circuit in memory in the ‘proving key’, using extra RAM and CPU that could be avoided. We realized that, with a few small tweaks to the proof system, we could eliminate one format completely and make Kimchi more efficient in speed and memory. We pushed this to its logical conclusion, so generating the proving key itself is now far more efficient than it used to be.
Then, we turned our eye to PLONK itself: it turns out that an optimization in PLONK called linearization, which makes perfect sense for the paper’s use case, is an anti-optimization when you’re doing recursion. As a result of this change alone, many Kimchi and Pickles circuits more than doubled in performance.
Flexibility is the future
Tying this all together, we’ve ended up with Kimchi - a flexible, configurable proof system designed to work efficiently with recursion. After all the painstaking design work and code refactorings, it’s now easy to build a version of Kimchi for completely different use cases. Using this flexibility, the cryptography team at o1Labs has been developing o1VM to prove the execution of normal programs that run against the MIPS instruction set. The goals when designing such a system are very different, and it’s a testament to Kimchi’s design that the first prototype was up and running in a matter of weeks.
We believe that combining and composing proofs that are lightweight and succinct is essential to get the most out of zk. The cryptography team has also been working on a system to take any custom Kimchi proof and seamlessly plug it into Mina through o1js or any other Kimchi and Pickles system. As o1VM enters its next step of development, we’re excited to see this bringing the full power of zero knowledge VMs to Mina and o1js for zkApp developers and users alike.
We also know that recursion isn’t always the right answer: sometimes your circuit runs a lot of times, and you have so much shared structure that you can be even more efficient. Alongside the o1VM effort, Kimchi now comes with a prototype of ‘folding’: a recent technique to squash many proof inputs together and still get to a single proof.
Why not another proving backend too? Kimchi now supports outputting bn254 KZG proofs, different hashing backends, and of course, the choice to work with folding or with Pickles for recursion. We’re firm believers in using the right tool for the job, and Kimchi is the Swiss army knife that achieves that today.
What’s next
Exciting things are on the horizon for Kimchi! We've only scratched the surface in this post, with much more to share soon. Keep an eye out for updates as we're gearing up to integrate this flexibility natively into o1js to enhance the power of the Mina protocol with cutting-edge optimizations. In the meantime, dive into the Mina Book, which houses documentation and specifications for Kimchi and other cryptographic algorithms used in Mina.