LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)

NADA AMIN, Harvard University, USA
JOHN BURNHAM, Lurk Lab, USA
FRANÇOIS GARILLOT, Lurk Lab, USA
ROSARIO GENNARO, Protocol Labs, USA
CHHI’MÈD KÜNZANG, Lurk Lab, USA
DANIEL ROGOZIN, University College London, United Kingdom
CAMERON WONG, Harvard University, USA

We introduce Lurk, a new LISP-based programming language for zk-SNARKs. Traditional approaches to programming over zero-knowledge proofs require compiling the desired computation into a flat circuit, imposing serious constraints on the size and complexity of computations that can be achieved in practice. Lurk programs are instead provided as data to the universal Lurk interpreter circuit, allowing the resulting language to be Turing-complete without compromising the size of the resulting proof artifacts. Our work describes the design and theory behind Lurk, along with detailing how its implementation of content addressing can be used to sidestep many of the usual concerns of programming zero-knowledge proofs.

Additional Key Words and Phrases: Lisp, Rust

1 INTRODUCTION

Assume that you query a remote database 𝑤 with key 𝑥, and want a guarantee that the remote database server is answering the query correctly; or that you need to prove that you have a sufficiently high balance 𝑤 in your financial account in order to participate in a given transaction 𝑥, but don’t want to reveal how much money you have. These are examples of “proofs” that a (potentially secret) value 𝑤 and a public input 𝑥 satisfy a given relationship, and play an important role in many secure applications where computations are performed by untrusted servers, including blockchain systems.

Succinct Non-Interactive Arguments of Knowledge (or SNARKs) [Ben-Sasson et al. 2014b] have been a very exciting area of research in the last decade: a SNARK allows one party (the prover) to prove to another party (the verifier) that a certain computation 𝐹 has been performed correctly. Specifically, it allows the verifier to prove the existence of a witness 𝑤 such that 𝑦 = 𝐹 (𝑥,𝑤) for a publicly known input 𝑥. It is easy to see that the above examples can be cast in this framework.

One such proof is the witness 𝑤 itself, with the verification procedure being to simply recompute the function 𝐹. The crucial property of SNARKs, however, is that they produce a proof 𝜋 which is shorter than 𝑤 and can be verified faster than recomputing 𝐹 (particularly, sublinear in either). An additional important property of SNARKs is that they can be zero-knowledge (zk-SNARKs), revealing no information about 𝑤 to the verifier.

This paper introduces Lurk¹, a new LISP-based programming language which automatically constructs zk-SNARKs for arbitrary programs, avoiding ad-hoc compilation of programs into flat circuits – a process which imposes serious constraints on the size and complexity of computations that can be achieved in practice. Although zk-SNARKs theoretically enable applications like those described above, the possibility of deploying them has so far been impeded by the lack of a practical and general language stack. One author conceived of Lurk after his experience implementing the Filecoin proofs [Fisch et al. 2018], which consist largely of Merkle-inclusion proofs at scale.

Lurk emerged through a design effort to generalize such proofs of knowledge, to exploit recent cryptographic proving-system breakthroughs, and to solve software-engineering usability problems still unaddressed by new cryptography. Claims about computation provable in arithmetic circuits (the implementation language of SNARK statements) generally end with the observation that such circuits are Turing-complete. This theoretical equivalence might lead prospective proof implementers to wrongly believe that proofs of execution of programs written in conventional programming languages can be easily represented in SNARK circuits, but this is not the case. In fact, non-trivial programs expressed in R1CS require that control structures be unrolled and recursive programs be translated into a witnessed form which is unintuitive to audit or author by hand and penalizes performance of general-purpose programs.

Lurk solves this problem by integrating a concise interpreter with its cryptographic backend, to express proofs over the evaluation of a high-level Turing-complete source programming language. In other words, the Lurk interpreter sequentially reduces Lurk programs until a terminal result remains, with no intermediate representation required: the (content-addressed) human-readable program is the input to the arithmetic circuit proving its reduction; and the final result of evaluation is similarly legible.

2 CRYPTOGRAPHIC BACKGROUND

2.1 Arithmetization

The first step in the construction of a SNARK is to arithmetize the computation 𝑓, which for the purpose of this paper, can be thought as expressing a computation into a format that makes easier to prove its correctness. Following the work on Quadratic Span Programs (QSP) [Gennaro et al. 2013], a very popular arithmetization for SNARKs is Rank 1 Constrained Systems (R1CS) which are a universal model that can encode any computation 𝑓.

Let 𝑓 be a function defined over a field F. We want to show that ∃𝑤 : 𝑓 (𝑥,𝑤) = 𝑦 or equivalently via a satisfiability predicate 𝑓, that ∃𝑤 : 𝑓 (𝑥,𝑦,𝑤)=1. We call 𝑥,𝑦 public input and let 𝑚 = |𝑥|+|𝑦|+|𝑤|+ 1. We can associate to 𝑓 three 𝑚 × 𝑚 matrices 𝐴,𝐵,𝐶 defined over F.

R1CS are closely related to arithmetic circuits (indeed those matrices can be thought as encoding addition and multiplication gates).

Mapping a computation 𝑓 to an R1CS system of constraints can be a tedious effort, but it is also one of the main computational bottlenecks in SNARKs, requiring large overhead for the prover in terms of both computation time and memory. Indeed a circuit verifying the computation of 𝑓 must basically "write down" the entire computation trace as a witness to prove its correctness.

2.2 Incrementally Verifiable Computation

Starting with the work of Valiant [2008], researchers have been studying alternative ways to construct SNARKs that would not require construction of a circuit for the entire computation 𝑓. One approach involves verifying that each step of the computation has been performed correctly and then use recursion to fold the correctness proofs of the first 𝑖 − 1 steps and the correctness proof of the 𝑖 step into a proof of correctness of all 𝑖 steps.

The reason this is appealing is that it allows verifying a computation as it is executed: in this case the cryptographic verification engine is only applied to the transition function of the machine executing a program. This gives rise to the notion of Incrementally Verifiable Computation (IVC) where the function 𝐹 is executed as the repeated composition of a smaller function 𝑓 that at the 𝑖 step takes as input the result of the previous step (the input and output of the computation 𝑓 is the state of the machine over which the big computation 𝐹 is run).

2.3 Cryptographic Commitments

A cryptographic commitment is a protocol that can be thought of as the equivalent of an opaque envelope. A sender who has a value 𝑣, produces a commitment 𝐶 = 𝐶𝑜𝑚(𝑣) to 𝑣, and later can open the commitment 𝐶 to 𝑣. A commitment must be binding, i.e. can only be opened to a unique value 𝑣; it is usually compressing in the sense that |𝐶 | < |𝑣| and can be hiding, i.e. the value 𝐶 reveals no information about 𝑣. In practice commitments are built from collision-resistant hash functions 𝐶 = 𝐻 (𝑣,𝑟) for some randomness 𝑟. The collision-resistant property guarantees binding, the range of 𝐻 is usually smaller than its domain, and under some reasonable assumptions the randomness 𝑟 protects the secrecy of 𝑣.

Commitments are a crucial tool in SNARKs. For example, note that the efficiency requirement on the SNARK verifier prevents them from even reading a description of the function 𝐹. One way to deal with this is to assume some preprocessing phase where the function is committed to a short string that can be handled by the verifier (preprocessing SNARKs). In IVC schemes like Nova, the intermediate computation steps are compressed in order for the state of the recursion not to grow too much.

4 A BRIEF OVERVIEW OF LURK

In this section, we describe the surface language and novel features of Lurk, along with providing examples motivating those features’ utility.

4.1 Lurk is a Lisp

Inheriting from typical Lisp tradition, Lurk has no syntax of note. Everything is an expression. Some expressions are self-evaluating; for example, the number 3 evaluates to itself.

4.2 Looping and branching

Lurk supports evaluating only some branches of a program, as well as unbounded loops and recursion. This is a strict improvement on the direct compilation approach.

4.3 Commitments

Lurk has built-in support for cryptographic commitments.

4.4 Functional Commitments

Because Lurk allows commitments to any Lurk expression, we can also commit to functions.

5 EXAMPLE APPLICATIONS

5.1 Credit-Score

Consider a credit bureau, who wants to preserve the secrecy of its proprietary rating algorithm while also proving that it applies its algorithm fairly to all parties.

5.2 Zero-Knowledge Type-Certificates (zk-TCs)

Another interesting program to implement in Lurk is a type checker.

6 DISCUSSION

So far, we have described the insights that led to the development of Lurk, and demonstrated that its architecture is adequate to serve real-world programming use cases. In this section, we compare our project to related work, and explore upcoming work.