# Lurk: Lambda the Ultimate Recursive Knowledge (Experience Report)
Nada Amin, John Burnham, François Garillot , Rosario Gennaro, Chhi’mèd Künzang, Daniel Rogozin, Cameron Wong
ICFP 2023
---
## Introduction
![](https://hackmd.io/_uploads/SksFgDw0n.png)
----
### Wouldn't it be nice?
- to create a proof artefact that's asymptotically faster to verify than redoing the type-checking,
- to demonstrate that you have a valid proof of a theorem ... while witholding the proof (*Like Fermat !*)
----
### This talk
- NOT how we built e.g. a Lean type-checker in a Zero-knowledge proof system (see paper),
- at the *cheap* cost of writing it in Lisp,
- why this involved building a general-purpose FPL (Lisp-ish) interpreter,
- how interpreters work in the cryptographic context, and where we'd like your help.
----
### Warning : the word "proof" is overloaded
Proofs of type-checking are an example, this isn't a talk about theorem proving.
----
### Zero-knowledge proofs:
- a protocol involving a *prover*, and a *verifier*,
- the prover creates a proof of satisfiability, which is a piece of data,
- For $x, y, f$ fixed publicly (known to all) the proof demonstrates:
$$ \exists w, f(x, w) = y$$
- the protocol for verifying the proof is *sound* & *complete*,
- $f$ must be expressed as an *arithmetic circuit*.
----
### Other key properties
- succintness: verifying the proof is at most a polylog in the size of $f$,
- zero-knowledge: if the witness w is present.
Hence the name SNARKs: Succint Non-interactive Arguments of Knowledge (SNARKs)
----
### Arithmetic Circuits
```mermaid
graph LR
A[ ] -->|a| Add
B[ ] -->|b| Add
Add(+) --> |a+b| Mul
C[ ] --> |c| Mul
Mul(*) -->| c*a + c*b| Output[ ]
```
- and equality constraints,
- input wires contain field elements.
---
### Expressing Computation as Arithmetic circuits
Some ZK-proof DSLs compiling to circuits
- circom,
- Zokrates,
- snarkyJS / snarky,
- Leo,
- Noir
----
### Expressing Computation as Arithmetic circuits
1. Direct compilation approach: stepwise translation & ad-hoc combinators
2. Arithmetic circuits are a flat structure, requires flattening control and unrolling loops,
3. a *non-uniform model of computation* that really represents traces.
----
### Loop unrolling
When we don't know the iteration count, it's harder to produce the circuit:
```scheme
(let ((collatz (lambda (n)
(letrec ((aux (lambda (acc n)
(if (= n 1)
acc
(let ((x (/ n 2)))
(if (< x 0) ; odd
(aux (+ 1 acc) (+ 1 (* 3 n)))
(aux (+ 1 acc) x)))))))
(aux 0 n))))
(collatz 27))
```
----
### Branching
```scheme
(let (f n)
(if (= n 0)
1
(/ 5 n)))
```
---
## IVC
----
### Incrementally Verifiable Computation for SNARKs
(IVC, Valiant 2008)
1. Assume you can break $f$ down as repeated $f_1\ldots f_n$ steps and verify correctness step-by-step,
4. *Traditionally*, you'd create at each step a proof of $\Pi_n$ s.t.:
$$ \exists w_n, \textrm{verif}(\Pi_{n-1}) = true \wedge f_n(y_{n-1}, w_n) = y_n$$
5. Should look like a Y combinator to you,
----
### IVC
![](https://hackmd.io/_uploads/By8n9QuZ3.png)
([slide source: Kothapalli & al. 2022](https://www.youtube.com/watch?v=Jj19k2AXH2k))
----
## Nova: a most efficient IVC candidate
(Kothapalli, Setty, Tzianna 2022)
- cheap folding argument rather than recursion,
- finish with a final SNARK over *a smaller proof statement*,
- but we need a "natural" iterative form of the computation.
---
## Language definitions to the rescue!
- interpreters are natively expressed as recursive applications of a step function,
- the cryptographic $f$ becomes the interpreter of our language,
- the user's Lisp program becomes "just" an input (e.g. $x$ n prior notation)
----
## Definitional language interpreters
A common way of defining a language : giving it an interpreter.
![](https://hackmd.io/_uploads/r1BWftV-2.png)
----
### Interpreters and abstract machines
![](https://hackmd.io/_uploads/SkpTlKEbh.png)
See e.g. _Defunctionalized Interpreters for Programming Languages_, Danvy et al. 2014
----
### The CEK machine
![](https://hackmd.io/_uploads/rk7BamO-h.png)
----
### Lurk is a (fancy) iterated CEK abstract machine stepper
![](https://hackmd.io/_uploads/H1AAVKN-3.png)
----
### Some Lurk characteristics
- 12k constraints for the CEK step machine,
- for comparison, a sha-256 hash function is 44k constraints,
- the sha256 compression function is 27K constraints.
Lurk is really small!
(and *when we figure out how to do way fewer steps*, that wil mean really fast!)
---
## Writing an interpreter in the cryptographic context
- state management is adversarial,
- rather than passing large inputs for the state of the abstract machine, pass $commitments$ to it,
- the program and its inputs/output can be arbitrarily large, or hidden,
- Concretely, $H(C), H(E), H(K)$ rather than $C, E, K$.
----
## Commitments
```scheme!
> (commit 123)
Iterations: 2
Result: (comm 0x2937881e)
```
----
### Opening commitments
```scheme!
((open 0x1aec2d8c) 9); here 9 is a salt
Iterations: 12
Result: 88
```
----
### Hashing all the things!
- hash-consing: a classic functional programming technique to share structurally equal values,
- we hash each value rigorously, and compare using hash equality,
- concretely, this holds the prover accountable to a unique program, while focusing on a fragment in a given step.
---
## A taste of Lurk
----
### Lurk is a Lisp
```scheme
> (let ((collatz (lambda (n)
(letrec ((aux (lambda (acc n)
(if (= n 1)
acc
(let ((x (/ n 2)))
(if (< x 0) ; odd
(aux (+ 1 acc) (+ 1 (* 3 n)))
(aux (+ 1 acc) x)))))))
(aux 0 n))))
(collatz 27))
Iterations: 4016
Result: 111
```
----
### Functional commitments
```scheme!
(commit (lambda (x) (+ 7 (* x x))))
Iterations: 2
Result: (comm 0x1aec2d8c)
```
----
### Higher-order functional commitments
```scheme!
> (let ((secret-data 555)
(data-interface (lambda (f) (f secret-data))))
(commit data-interface))
Iterations: 7
Result: (comm 0x03836e2e)
> ((open 0x03836e2e) (lambda (data) (+ data 111)))
Iterations: 14
Result: 666
```
---
## Lurk release 1.0 alpha
- [the blog post](https://blog.lurk-lang.org/posts/announcing-lurk-alpha/)
- [the pre-print](https://eprint.iacr.org/2023/369)
- and more! Specification, audit report, tutorial etc.
---
## Future work
- in the cryptographic context, book-keeping steps are more expensive than abstract machines assume,
- this is ripe for *formal verification*,
- abstract machines (for functional PLs) are very similar : is there a general discipline for encoding them to circuits?
- importantly: **if you think we are being dunces, your feedback would be a gift.**

{"title":"Lurk: Lambda the Ultimate Recursive Knowledge","slideOptions":"{\"transition\":\"slide\",\"tags\":\"Lurk, talk, crypto\"}","description":"circom,","contributors":"[{\"id\":\"dbd3a2cc-6969-479a-9e28-e36eca77e32e\",\"add\":9386,\"del\":2487}]"}