Lurk: Lambda the Ultimate Recursive Knowledge (Experience Report)

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

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

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:

(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

(let (f n)
  (if (= n 0)
      1
      (/ 5 n)))

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,
2. 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\]
3. Should look like a Y combinator to you,

IVC

(slide source: Kothapalli & al. 2022)

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.

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!)

Commitments

> (commit 123)
Iterations: 2
  Result: (comm 0x2937881e)

Opening commitments

((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.

Lurk is a Lisp

> (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

(commit (lambda (x) (+ 7 (* x x))))

Iterations: 2
Result: (comm 0x1aec2d8c)

Higher-order functional commitments

> (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