zkLean: A DSL for ZK statement verification

‍Zero-knowledge proofs (ZKPs) are an emerging cryptographic technique on the verge of becoming increasingly useful and important for everyday users in the near future. In a ZKP, one party can prove to another that they know a statement is true without revealing any other information. It ensures trust and verification in cryptographic transactions while maintaining privacy and security.

Recent work by Google has proposed integrating ZKPs into mobile wallets to offer anonymous credentials. Traditionally users need to share their licenses or passports with businesses in order to access age-restricted services, thereby revealing their private information like birthdays and addresses. Anonymous credentials would allow users to provide a cryptographic proof that they have a valid driver’s license issued by their local DMV and that their credential satisfies a policy (e.g., the user is 21 years old). Importantly, the business can check that the policy is satisfied without learning additional information about the user like their birthday or address.

Beyond anonymous credentials, there are multiple use cases for ZKPs that are close to deployment. FAEST is a post-quantum secure digital signature scheme that uses ZKPs in its underlying construction. Blockchains like ZCash and Ethereum are already using or looking to deploy ZKPs in order to provide private transactions and accelerate throughput of their networks.

Are ZKPs secure?

Since ZKPs are close to real world use, it is vital to ensure that they are actually secure. For ZKPs to be theoretically secure, they must satisfy two main properties. The first is confidentiality which guarantees that a verifier does not learn anything about the prover’s secret besides the fact that the secret satisfies the policy. The second property is soundness, ensuring that a prover cannot produce a valid proof unless their secret satisfies the policy. Assuming no implementation bugs, there are multiple ZKP cryptographic algorithms that satisfy these properties. Both of these security properties rely on a correct definition of the intended policy, and unfortunately it is not straightforward to correctly write these policies. If there is a mistake in a policy definition, this would cause soundness bugs where a verifier would accept a ZKP even though the prover’s secret does not satisfy the intended policy. 

ZK policies are difficult to implement correctly since ZK statements operate over field operations like additions and multiplications modulo a large prime number. On the other hand, most statements that developers want to write involve traditional machine word operations like 64-bit additions or shifts. Encoding these machine word operations as prime field arithmetizations requires extensive cryptographic expertise, and the process is tedious and error prone. In practice, it is highly unlikely to manually write a large ZK statement without any soundness issues. 

Formal verification offers one solution to this problem by guaranteeing that a ZK statement conforms to its stated specification. Formal verification tools like interactive theorem provers (ITPs) and SMT solvers verify propositions through machine checked proofs. By applying formal method tools to ZK statements, one can dramatically increase the assurance that a ZK statement is correct.

One such tool we have been developing at Galois to verify ZK statements in the Lean ITP is zkLean. zkLean is a Lean library that defines a DSL for specifying ZK statements as well as formally verifying that ZK statements are correct with respect to their specifications. zkLean makes it easy to define your ZK statement in Lean, and it supports many variants of ZK primitives including arithmetic expressions, equality constraints, R1CS constraints, lookup tables, MLE based lookup tables, and even RAM operations. As a simple example, consider the ZK statement that returns a new variable that is constrained to be zero or one:

def example1 [ ZKField f ] : ZKBuilder f ( ZKExpr f ) := do
  let x <- witness
  constrainEq ( x * ( x - 1)) 0
  return x

‍

The example first creates a new witness variable. Then it constrains this variable to be zero or one, and finally returns the new witness so that it can be used by the caller. Notice that the example function is polymorphic over the underlying prime field f, so it is agnostic to the field that the ZK backend supports.

Case study: SHA-3

To demonstrate the power of zkLean, we have encoded the circuit for the SHA-3 hash function and proven it correct. To do so, we first defined a specification implementation of SHA-3 in Lean. Here’s an excerpt from the specification:

structure StateSpec where
  lanes : Vector (BitVec 64) 25‍

def keccakRoundSpec (s : StateSpec) (round : Fin 24) : StateSpec :=
  s |> thetaSpec |> rho_piSpec |> chiSpec |> (iotaSpec . round)‍

def keccakFSpec (s : StateSpec) : StateSpec :=
  (Array.finRange 24).foldl (fun acc i => keccakRoundSpec acc i) s

‍

Notice that the specification’s state is defined over 64-bit vectors, and the keccakFSpec function runs 24 rounds composed of calls to subroutines like thetaSpec and rho_piSpec. 

Next we implemented the circuit encoding of SHA-3 defined over field arithmetic: 

structure State where
  lanes : Vector (ZKExpr f) 25‍

def keccakRound (s : State) (round : Fin 24) : ZKBuilder f State := do
  theta s >>= rho_pi >>= chi >>= ( iota . round )‍

def keccakF (s : State) : ZKBuilder f State :=
  (Array.finRange 24).foldlM (fun acc i => keccakRound acc i) s

The circuit implementation of SHA-3 in zkLean closely resembles its specification. 

Finally we proved the circuit implementation correct with respect to its bitvector specification. Here is an excerpt from the proof for the keccakRound circuit:

lemma keccakRound.soundness (s0 : State) (s0_bv : StateSpec) (round : Fin 24) :
  { \ _ => eqState s0 s0_bv }
  keccakRound s0 round
  { \ s1 _ => eqState s1 (keccakRoundSpec s0_bv round) }
:= by
  mintro h e
  simp_rw [ keccakRound , bind_assoc , keccakRoundSpec ]
  mspec ( theta.soundness ( s0_bv := s0_bv ) s0 )
  mspec ( rho_pi.soundness ( s0_bv := thetaSpec s0_bv ) _ )
  mspec ( chi.soundness ( s0_bv := rho_piSpec ( thetaSpec s0_bv )) _ )
  mspec ( iota.soundness ( s0_bv := chiSpec ( rho_piSpec ( thetaSpec s0_bv ))) _ round )

‍

zkLean integrates with Lean’s Std.Do notation which allows users to write specifications about circuits using standard Hoare triples. For instance, the postcondition of keccakRound.soundness states that the keccakRound circuit enforces that the resulting field state must be equal to the result of running the specification’s keccakRoundSpec function on the initial bitvector state. Another benefit of integration with Std.Do is that proofs about zkLean circuits are compositional. In the keccakRound.soundness proof, the mspec tactic allows the proof to make use of lemmas on the subcomponents like theta.soundness and rho_pi.soundness.

Integration

Users will often want to verify properties about circuits written in other systems. One option for doing so is to define a custom extraction from the tool into zkLean. For example, we have developed an extractor for the Jolt zkVM that converts all of the frontend constraints in Jolt into a zkLean circuit.

Implementing an extractor for every ZK system is a time intensive process. An alternative approach to implementing custom extractors is to use LLZK. LLZK is an MLIR dialect for ZK circuits. We have defined LLZK frontends and backends, which allow users to convert LLZK circuits to zkLean (or convert zkLean circuits to LLZK). LLZK has integration with other standard circuit languages like Circom, so users can use LLZK to convert their Circom circuits into zkLean (or vice versa).

Automation

Proofs about field operations and their corresponding bitvector operations can be tedious and time consuming. To aid the user, we have developed a Lean tactic to help automate such proofs. The following example demonstrates the usage of our solveMLE automation tactic to prove the soundness of Jolt’s MLE lookup table for bitwise AND with respect to the bitvector operation &&&.

def AND : Subtable f 64 := subtableFromMLE ( fun x => 0 + 2147483648* x [0]* x [1] + ...)‍
lemma and.soundness ( bv1 bv2 : BitVec 32) ( fv1 fv2 : Vector f 32) :
  some bv1 = map_f_to_bv fv1 ->
  some bv2 = map_f_to_bv fv2 ->
  some ( bv1 &&& bv2 ) = f_to_bv ( evalSubtable AND fv1 fv2 )
:= by
  simp [ AND , evalSubtable , Vector.append ]
  solveMLE 32

‍

Note that the user only needs to unfold a few top level definitions with the simp tactic, and then simply calls the solveMLE tactic. The tactic automatically proves the goal, which normally would require a long proof reasoning about modular arithmetic to convert field elements to bitvectors and the constraints enforced by the lookup table. We evaluated our tactic against state-of-the-art ZK solver theories implemented in the cvc5 SMT solver. The following graph shows the comparison results for automatically solving Jolt’s lookup tables. 

‍

As seen in the cactus plot, our tactic (BitModEq) is slower initially, but is able to solve most of the lookup tables while cvc5 times out before solving all of the test cases. Check out Liza’s blog post to learn more about the development of this tactic during her internship.  

Conclusion

zkLean is an expressive DSL for formalizing and verifying ZK statements in the Lean interactive theorem prover. It integrates with existing circuit languages like Circom through the LLZK toolchain and provides automation for automatically verifying bitvector properties. If you have a ZK statement you are looking to deploy, give zkLean a try to verify your circuit and let us know how it goes! 

Acknowledgments

Thank you to the Ethereum Foundation for providing a grant that has funded the development of zkLean.

‍