zkPi+

In many fields, including computer science and mathematics, when we want to convince someone that a certain statement is true, we often do so via a proof. For example, to demonstrate that a particular sorting algorithm is correct, one can present arguments to establish invariants and properties about components of the algorithm. Then use these sub-properties to show that all outputs of the algorithm are guaranteed to be sorted.

However, these types of proofs inevitably reveal information about how the algorithm works. While this is perfectly fine in most cases, for closed-source software it is not, since such proofs are not possible without access to the algorithm's code. Because of this, many users are often reluctant to run closed-source software, since they have no way of knowing how it may behave, and what it may do with their data.

In this post, we will describe a system that attempts to address these issues by allowing proofs of arbitrary statements about programs, mathematics, and more to be encoded in zero-knowledge proofs. Which can be verified without revealing the arguments used to establish the statement in question. We will start by explaining the system used to write these proofs, and then we'll describe how they can be converted to the zero-knowledge representation.

Introduction to Lean

The foundation of this system is the Lean 4 programming language and theorem prover. As this description suggests, Lean has a variety of uses. Since it is a programming language, it can be used to create executable programs for general-purpose programming tasks. Its second use-case, as a theorem prover, complements the first. Lean allows a wide variety of statements about programs, mathematics, and more to be described and proven in a structured way, such that the compiler can verify whether a proof is correct. These two features can be used together to create extremely reliable software which is guaranteed to conform to the desired specifications (as long as one trusts the Lean compiler).

Lean implements these features by building on ideas from the field of programming languages, in particular that of dependent types, using the presentation from the calculus of inductive constructions. While providing a complete explanation of Lean along with the necessary background is far beyond the scope of this post, a quick example will help provide some intuition for how the system as a whole will work. The following code defines the $\le$ relation on natural numbers, and proves that $2 \le 4$:

inductive Nat.le (n : Nat) : Nat → Prop where
  | refl : Nat.le n n
  | step : Nat.le n m → Nat.le n (m + 1)

theorem Nat.two_le_four : Nat.le 2 4 :=
  Nat.le.step (Nat.le.step Nat.le.refl)

In the above, line 1 begins the definition of $\le$ by stating that it will be a property which relates two Nats (the type for natural numbers in Lean). Lines 2 and 3 define constructors for Nat.le. They are called constructors since they can be used to construct terms of type Nat.le n m, for certain choices of n and m (we will see an example of this on the last line of the second statement). Since we are trying to use Nat.le to model the $\le$ relation on natural numbers, we want it to be possible to construct a term of the corresponding type whenever the mathematical relationship between $n$ and $m$ holds, and impossible otherwise. To accomplish this, the refl constructor is restricted so it can only prove that a natural number is less than or equal to itself, and the step constructor can only prove that $n \le m$ implies $n \le m + 1$.

With this definition in hand, the second statement proves the theorem that $2 \le 4$. Line 5 gives a name to the theorem (so it can be reused as a sub-argument of future theorems) and states the type of the theorem as Nat.le 2 4, since this corresponds to the $2 \le 4$ mathematical statement which is being encoded. In the last line, the constructors of Nat.le are used to create a term of the required type, which proves that the theorem is true. Reading the term from right-to-left, the n variable in the definition of Nat.le.refl will be instantiated as 2 so that its use in our theorem has type Nat.le 2 2. The first application of the step constructor extends this type to Nat.le 2 3, and the second results in the required Nat.le 2 4.

If you are interested in learning more about Lean, various resources are available on the project's website.

The zkSNARK Primitive

In short, a zkSNARK is a type of zero-knowledge proof. The parts of the acronym stand for the following properties:

• zero-knowledge: A proof is zero-knowledge if it reveals nothing about the private information used to construct the proof. In our case, this private information will be the Lean term used to prove the theorem.
• Succinct: A proof is succinct when its size is constant, and it can be verified in constant time. (Depending on how you look at things, our system may not completely satisfy this property, as the size of the proof will scale based on the size of the underlying Lean proof.)
• Non-interactive: A proof is noninteractive when only a single prover message is required to convince a verifier (instead of a longer protocol).
• Argument of Knowledge: This description encompasses two sub-properties:
  • Completeness: It must be possible to construct the zkSNARK given any valid underlying proof.
  • Computational Knowledge Soundness: It should be computationally infeasible to construct a valid zkSNARK without a valid underlying proof.

Overview of zkPi

Now that we have established the necessary background, the system for encoding Lean proofs in zero-knowledge can finally be described. Our work, which we have named zkPi+, is an updated version of a prior work called zkPi by Laufer, Ozdemir, and Boneh. In this section, we will describe the architecture of zkPi, and explain the aspects of it that we aimed to improve.

The following table gives a brief summary of zkPi's architecture:

flowchart TD
    A(Lean.Expr) -->|lean4export| B(Lean 4
Export Format) -->|LeanEncoding::parse| C(Theorem) -->|Evaluator::eval| D(Theorem) -->|export_ty_term| E("ZkInput
(Typing Derivation)") -->|ZkInput::serialize| F(Circ Input Term)

Recall that in a prior section, we explained that a proof in Lean consists of a term whose type corresponds to the statement being shown. zkPi uses this idea to create zero-knowledge proofs of Lean statements by embedding the proof term and type-checking it in a zkSNARK, thus demonstrating that the statement is provable. To accomplish this, the pipeline above starts with a Lean.Expr representation of the proof term. The Lean.Expr datatype is a low-level IR in Lean which corresponds closely to the calculus of inductive constructions. This data is exported from Lean with lean4export, and parsed by the zkpi binary. zkPi then attempts to evaluate the proof down to a simpler form (in order to reduce the amount of work required in the zkSNARK). Next, the zkpi binary performs type-checking on the proof term, and constructs a "typing derivation", which is a recursive datatype that demonstrates why the proof term has the expected type. This typing derivation is then serialized to a format which can be accepted as input by the "circ" circuit compiler. At this point, the zkSNARK can finally be constructed by using this data as input to a ZoKrates program which verifies that the private typing derivation encoded in the input is well-formed.

This architecture works well, however, there is still some room to improve on zkPi. First, since the paper was published in 2024, the existing codebase was about 2 years old and thus incompatible with current versions of Lean. Updating things was mostly straightforward. The only complication was that lean4export's file format changed, so we replaced zkPi's parser with a call to the parser from nanoda_lib (another external type checker for Lean), along with some glue code to convert between representations. Second, as shown by the following diagram from the paper, efficiency issues and missing features of Lean's type theory prevent zkPi from compiling all theorems from mathlib and the Lean standard library.

We decided to focus on adding support for the highlighted features. In the next few sections, we'll explain what these features are, and how we added support for them.

Adding Strings

Lean's representation of the AST (Expr) stores strings as literals (.lit "string"), but to use them in proofs we need them to be an inductive type. The definition of strings in Stdlib is:

structure String where ofByteArray ::
  toByteArray : ByteArray
  isValidUTF8 : ByteArray.IsValidUTF8 toByteArray

However, this poses some issues. While converting to a byte array is easy, producing a proof of validity for one is not. It's easier to just let Lean do this. One way to do this is to construct the string using String.ofList. This only requires us to convert each char in the string to its numerical representation:

String.ofList [Char.ofNat ${str[0]}, ..., Char.ofNat ${str[n]}]

Unfortunately, this is not good enough. We found in practice that any theorem involving strings was extremely slow to verify. To get a good result, more optimizations implemented in the Lean kernel would likely need to be implemented in our type checker.

Adding Quotients

A quotient type is a type based on an underlying type $\alpha$ and an equivalence relation $R$. All inhabitants of $\alpha$ can be converted to inhabitants of the quotient, and quotient terms whose underlying values are related by $R$ are considered propositionally equal. A common notation for a quotient type is $\alpha/R$.

You can think of a quotient type as a copy of a type with equality redefined.

For example:

def Multiset : Type := Quotient ⟨List.Perm, _⟩
structure Real : Type where cauchy : Quotient (CauSeq.equiv (abv := (abs : ℚ → ℚ)))

To add quotients, we need to add the following to zkPi:

$$ \begin{aligned} \text{sound}_{R}& : \forall x ~ y : \alpha. ~ R ~ x ~ y \to \text{mk}_{R} ~ x = \text{mk}_{R} ~ y \\ \text{lift}_{R}& : \forall \beta : U_v. ~ \forall f : \alpha \to \beta. ~ (\forall x ~ y : \alpha. ~ R ~ x ~ y \to f ~ x = f ~ y) \to \alpha/R \to \beta \\ \text{ind}_{R}& : \forall \beta : \alpha / R \to U_0. ~ \forall \text{mk} : (\forall x. ~ \beta ~ \text{mk}_{R} ~ x) \to y \to \beta ~ y \end{aligned} $$

Adding Quot.sound is the easiest, as it's an axiom: we simply have to define it. Then we must add the reduction rules for Quot.lift and Quot.ind. To do this, we add a check to our evaluation function that looks for applications of either rule. If it finds one, it checks that the structure matches what is expected, then returns the result (an element of $\beta$ for Quot.lift or $\beta ~ y$ for Quot.ind).

After adding these, we found we were able to check new theorems involving quotients. It was also fast enough to be usable.

Inductive Families

Inductive families are inductive types that have a function return type:

inductive Nat.le (n : Nat) : Nat → Prop where
  | refl : Nat.le n n
  | step : Nat.le n m → Nat.le n (m + 1)

In this example, Nat $\to$ Prop is our function. This means that for every Nat passed in, we get back a new inductive type. Hence, our definition defines an entire family of inductives. This is the trickiest change to implement, as it requires changes to the existing recursor logic.

In particular, zkPi didn't support recursive inductive families. When an inductive type is indexed, like Nat.le is indexed by its second Nat argument, the recursor needs to track how those indices change at each recursive step. zkPi's original implementation assumed the indices stayed fixed, which meant it couldn't handle these cases. The fix was three steps:

1. Finding out which constructor arguments are the indices for recursive sub-terms.
2. Substituting bound variables to get concrete index values during evaluation.
3. Rebuilding the recursor application with correct indices in the circuit.

We found this also worked correctly for our test cases.

Summary

Unfortunately, we were unable to evaluate the performance after our changes given computational limitations. However, we can speculate about the changes. It is clear that no examples with strings would succeed, even though they are now supported, as they are simply too slow. In effect, the failures previously caused by missing string support would instead become timeouts. For quotient types and inductive families, we have no reason to believe these would not work. We could expect to see the failure rates drop due to this, insofar as the newly supported theorems don't time out.

Our code is available on Codeberg.

Future Work

The obvious improvement is optimization. After these changes, it's clear the main limitation left is speed. There are a few possible directions to pursue on this end. Namely, taking more from the Lean type checker itself, things like lazy expansion of literals, more efficient representations, better reduction, etc. would certainly help to gain back some time.

A second area of optimization would be on the circuit end. We can try to use later versions of the compiler, different proof systems, try to shrink the amount of work the circuit does, or maybe use an entirely different approach.

Finally, there are still missing features: we did not add eta-expansion or any of the features from the other category of failures. While these do not account for a large share of failures, they would be necessary for zkPi to be fully compatible with Lean.

Conclusion

Returning to the project's goals, having the ability to verify Lean proofs in zero-knowledge would be a fantastic addition to the ecosystem. It could potentially enable a more decentralized untrusted environment for theorem searching, one where you do not have to execute unknown code locally. zkPi demonstrates that this is possible, and this extension brings us even closer. It seems that just a bit more effort could make this usable in real-world applications. We hope to see this line of work continued.