Provable has put together a solid compiler team to build a very ambitious circuit compiler language. The core aim of this endeavor is to allow developers to make use of zero-knowledge proofs in their applications in as simple a manner as possible - it achieves this by minimizing cryptographic knowledge requirements. So how exactly does Leo achieve this, and what do you need to know to get started using it? Let’s find out.

Key Concepts

First off, let’s briefly remind ourselves what a zero-knowledge proof is. It is some piece of data that proves that we ran a computation correctly; for example, that we used a private key to send an NFT to somebody, or that we have some attribute that allows us to update the state of an app. Furthermore it allows us to keep some data secret if we wish; for example we don’t have to reveal that private key we used to send the NFT. And the proof data is also far smaller than the whole computation, so it will require a lot less storage space (on chain) and be quicker to communicate.

This is a very abstract idea, so perhaps it will be more relatable if we link it to scalability issues we are seeing across the industry right now. Look at the difficulty different chains are having in getting enough transactions per second, and the clamour for scaling solutions to expand the possibility of on chain gaming. Tools such as state sharding have been helpful, but we need to add in more to support the growth of these use cases (and the future use cases we don’t even know of yet). Moreover, ZKPs also allow us to hide data we don’t want to reveal; of course that is not a possibility for other scaling solutions.

Now, how do you make a ZKP? Well, this is made for us by a proof system and something called a ZK circuit - it’s actually the circuit that we’re going to have to build, and this is what Leo will do for you! The libraries that turn ZK circuits into proofs already exist, so far people have been using these libraries directly.

Think about the device you are using right now, it has circuits inside it that are doing all this computation, right? Well, aren’t those circuits just NAND gates with zeros and ones whizzing through them? ZK circuits are very much similar, except that instead of NAND gates they are made from addition and multiplication gates, and instead of zeros and ones we have numbers between zero and p, where p is a phenomenally large prime number. Are you starting to see that we might be able to do just as much computation in ZK circuits as we can in real circuits?

Now we come to the crux of the issue, the reason why Provable is investing so much into building the circuit compiler Leo - turning high level app ideas into ZK circuits is phenomenally slow because you have to manually put together all the addition and multiplication gates to represent what computations should represent your app. I mean, how long would it take you to write normal apps if you had to put NAND gates together to build up the computation... doesn’t sound fun, right?

Well, that is the current state of ZK circuit creation. You essentially have to work at the circuit construction level because there is not yet enough infrastructure to automate low level, repetitive pieces yet. And actually it’s even worse than that. Not only do we not yet have these automations, but there is a lot of cryptographic knowledge required to even start building ZK circuits. This barrier to entry would in most cases take people several months of full time study to overcome. Doesn’t exactly sound great for product development.

Leo Overview

Leo is a Rust-inspired statically typed programming language built for writing private applications. It is designed for developers to build intuitively on the blockchain, providing the groundwork for a private, decentralized ecosystem. It is the first known programming language to introduce a testing framework, package registry, import resolver, remote compiler, and theorem generator for general-purpose, zero-knowledge applications.

Leo is designed to remove as many cryptographic knowledge requirements as possible. Moreover, it is designed to be reminiscent of Javascript and Typescript so that the army of JS/TS developers out there (around 12 million of them, dwarfing crypto dev numbers) will have a very straightforward learning curve.

Let’s jump forward and say you have written a Leo program, like the bubble sort in the image above - what does Leo actually do when you run the program?

It takes your code, constructs the proof circuit that represents the computation you want to run, populates the input wires with the values you want, runs the circuit, generates proving/verifying keys, and then combines all the relevant data into a ZKP. For example, you could run it on the input data in the image below.

But we said that you don’t need much cryptographic knowledge at all to use Leo, so what is all this proof creation stuff? The summary is that Leo outputs a proof that you ran your computation correctly, meaning if you were to run the above circuit on some array and presented the output array alongside the proof, any observers would be able to confirm that the array was actually sorted by checking the proof rather than the array.

Now that may not sound like much if the array only contains 10 items, but when we start working with data structures that have millions of items, and more complex computations, checking the proof (which is always the same size!) starts to convey a lot more value. But this isn’t a post about how to derive value from ZKPs, this post is to help devs learn Leo so they can make valuable applications themselves.

Leo also does more than just make the circuit for you and generate the proof from it. It is packed with functionality that helps reduce developer times as much as possible. The testing framework, package registry and import resolver all work together to save developers a lot of time ensuring that external functionality is imported easily, and that the code is actually does what it was expected to do.

When you build an ecosystem whose core aim is to allow the development of scalable applications that are private, one of the best ways to nurture the growth is to remove as much friction in application development as possible. This is what Leo is helping to achieve. If you want to learn more, check out the playground or developer docs.