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:

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

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
3. Cryptographic verification applied to transition function of executing program
4. IVC: Repeated composition of smaller function \(f\) over machine state
5. Most efficient IVC candidate: Nova (Kothapalli et al., 2022)

IVC

(slide source: Kothapalli 2022)

Nova

• cheap folding argument rather than recursion
• plus a final SNARK

• but we need a "natural" iterative form

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

Opening commitments

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

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