# 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  ---- ### 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  ([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.  ---- ### Interpreters and abstract machines  See e.g. _Defunctionalized Interpreters for Programming Languages_, Danvy et al. 2014 ---- ### The CEK machine  ---- ### Lurk is a (fancy) iterated CEK abstract machine stepper  ---- ### 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.**