# Lurk: Lambda the Ultimate Recursive Knowledge --- ## About me ### François Garillot (@huitseeker) ### Team work from [Lurk Lab](https://twitter.com/LurkLab), #### Team previously at Protocol Labs, #### (led by [Chhi'mèd Künzang](https://twitter.com/porcuquine2)). --- ## ZK-proof languages ---- # Writing a ZK-proof language in 2023 - circom, - Zokrates, - snarkyJS / snarky, - Leo, - Noir ---- ### SNARKs and Rank 1 Constrained Systems (R1CS) 1. Arithmetize computation $f$ for SNARKs using arithmetic circuit, 2. Express computation as $\exists w: f'(x,y,w)=1$ 3. Map to three $m \times m$ matrices $A,B,C$ over $\mathbb{F}$ 4. Satisfiability is equivalent to $(A \cdot z) \circ (B \cdot z) = C \cdot z$ ---- ### Expressing Computation as R1CS Instance 1. Direct compilation approach: stepwise translation and ad-hoc combinators 2. Drawbacks: R1CS is a flat structure, requires flattening and unrolling loops - Increased R1CS size negatively affects proving time, - Prover memory can become a practical bottleneck due to space complexity. ---- ### Branch 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)) ``` --- ## IVC ---- ### Incrementally Verifiable Computation (IVC) for SNARKs 1. Alternative to constructing a circuit for entire computation $f$ 2. Verify correctness step-by-step, then recursively fold correctness proofs 4. Cryptographic verification applied to transition function of executing program 5. IVC: Repeated composition of smaller function $f$ over machine state 6. Most efficient IVC candidate: Nova (Kothapalli et al., 2022) ---- ### IVC  ([slide source: Kothapalli 2022](https://www.youtube.com/watch?v=Jj19k2AXH2k)) ---- ## Nova - cheap folding argument rather than recursion - plus a final SNARK  - but we need a "natural" iterative form --- ## Language definitions --- ## 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 as an iterated abstract machine stepper  --- ## Commitments ```scheme! > (commit 123) Iterations: 2 Result: (comm 0x2937881e) ``` ---- ### Opening commitments ```scheme! ((open 0x1aec2d8c) 9) Iterations: 12 Result: 88 ``` ---- ### Hashing all the things! - hash-consing is a classic functional programming technique to share structurally equal values, - we hash each value rigorously, and compare using hash equality, - translating this to Poseidon in proof gives program equality semantics in proofs. --- ## 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. --- ## Lurk - on Twitter @LurkLab - on [Zulip](https://zulip.lurk-lab.com/): https://zulip.lurk-lab.com/