Lecture 3: Programming ZKPs
Guest Lecturers: Pratyush Mishra and Alex Ozdemir

Zero Knowledge Proofs
Instructors: Dan Boneh, Shafi Goldwasser, Dawn Song, Justin Thaler, Yupeng Zhang

Using a ZKP

Idea

Program

Programmer

R1CSCompiler*Params
Setup

ZKP
Prove

This Lecture2

ZKP MOOC

This Lecture
1. Big Picture: ZKP programmability
2. Using an HDL (+ tutorial)
3. Using a library (+ tutorial)
4. Using a compiler (+ tutorial)
5. An overview of prominent ZKP toolchains

3

ZKP MOOCZKP Programmability

4

ZKP MOOC
Credit: Faithie/ShutterstockRecap: ZKPs for a predicate 𝜙§ Prover knows 𝜙, 𝑥, 𝑤
§ Verifier knows 𝜙, 𝑥
§ Proof 𝜋 shows that 𝜙(𝑥, 𝑤) holds§ but does not reveal 𝑤§ Key Question: what can 𝜙 be?

5ZKP MOOC

What is 𝜙?
𝜙 in theory
𝜙 in practice§ 𝑤 is a factorization of§ 𝜙 is an “arithmetic circuit”
integer 𝑥
over inputs 𝑥, 𝑤
§ 𝑤 is the secret key for public
key 𝑥§ 𝑤 is the credential foraccount 𝑥§ 𝑤 is a valid transaction
6ZKP MOOC

Arithmetic Circuits (ACs), Part I§ Domain: “prime field”§ ACs as systems of field
equations:§ 𝑝: a large (~255 bit) prime§ ℤ! : the integers, mod 𝑝§ Example:§ 𝑤! ×𝑤! ×𝑤! = 𝑥§ 𝑤" ×𝑤" = 𝑥§ Addition is also OK§ operations: +,×, = (mod 𝑝)§ Example in ℤ":§ 4+5=9=4§ 4×4 = 16 = 1

7

ZKP MOOC

Arithmetic Circuits (ACs), Part II§ ACs as circuits§ Example:§ Directed, acyclic graph§ Nodes: inputs, gates,
constants§ Edges: wires/connections§ 𝑤#×𝑤#×𝑤# = 𝑥§ 𝑤$×𝑤$ = 𝑥§ As a circuit:

8ZKP MOOC

R1CS: a common Arithmetic Circuit format§ R1CS: format for ZKP ACs§ Definition:§ Examples:§ 𝑤(× 𝑤) − 𝑤( − 1 = 𝑥$
§ 𝑤(×𝑤( = 𝑤(§ 𝑤(×𝑤(×𝑤( = 𝑥$

§ 𝑥: field elements 𝑥$, … , 𝑥_ℓ§ 𝑤: 𝑤$, … , 𝑤%&ℓ&$§ 𝜙: 𝑛 equations of form

§ 𝑤# ×𝑤# = 𝑤$
§ 𝑤$ ×𝑤# = 𝑥"

§ 𝛼×𝛽 = 𝛾
§ where 𝛼, 𝛽, 𝛾 are affine
combinations of variables
9ZKP MOOC

R1CS: Matrix Definition§ 𝑥: vector of ℓ field elements§ 𝑤: vector of 𝑚 − ℓ − 1 field elements§ 𝜙: matrices 𝐴, 𝐵, 𝐶 ∈ ℤ"×$!
§ 𝑧 = 1 ∥ 𝑥 ∥ 𝑤 ∈ ℤ"!
§ Holds when 𝐴𝑧 ∘ 𝐵𝑧 = 𝐶𝑧

10ZKP MOOC

Writing an AC as R1CS (Example)§ Step 1: intermediate 𝑤s§ Step 2: write equations§ 𝑤#×𝑤$ = 𝑤(§ 𝑤) = 𝑤( + 𝑥#
§ 𝑤$×𝑥# = 𝑤*§ 𝑤) = 𝑤*

11

ZKP MOOC

Zooming out: a Programming Languages problem
High-levelspecification for 𝜙

Program in highlevel language

Using:• Libraries• Compilers• Programming Langs.
• Domain Specific Langs.
• …

12R1CS

Assembly

ZKP MOOC

The Idea
High-level code•••••Compiler/Library

R1CS

ZK Proof System

Booleans
Structures
Modules
Functions…

13

ZKP MOOC

An Example
Zcash Circuit•••••

Bellman Library

R1CS

Groth16

Merkle tree
Pedersen
HashSignatures
Spend logic…

14

ZKP MOOCAn HDL for R1CS

15

ZKP MOOC
Credit: Faithie/ShutterstockProgramming Languages (PLs) vs.
Hardware Description Languages (HDLs)
PL objects§ Variables§ Operations§ Program/Functions

HDL objects§ Wires§ Gates§ Circuit/Sub-circuits

PL actions§ Mutate variables§ Call functions

HDL actions§ Connect wires§ Create sub-circuits
16

ZKP MOOC

HDLs: From Digital to Arithmetic
An HDL for R1CS
§ circom

HDLs for Digital Circuits§ Verilog§ SystemVerilog§ VHDL§ Chisel§…

§ wires: R1CS variables§ gates: R1CS constraints§ a circom circuit does 2things:§ sets variable values§ creates R1CS constraints

17

ZKP MOOC

Circom: Base Language§ A “template” is a (sub)circuit§ A “signal” is a wire

template Multiply() {signal input x;
signal input y;signal output z;§ “input” or “output”§ “<--” sets signal values§ “===” creates constraints

z <-- x * y;z === x * y;// ERROR: z === x * x * y// OR: z <== x * y;

§ Must be rank-1:§ one side: linear§ other side: quadratic}
component main {public [x]} =Multiply();§ “<==” does both18

ZKP MOOC

Circom: Metaprogramming Language§ Template arguments§ Signal arrays§ Variables

template RepeatedSquaring(n) {signal input x;
signal output y;§ Mutable§ Not signals§ Evaluated at compile-time

signal xs[n];xs[0] <== x;
for (var i = 0; i <= n; i++) {xs[i+1] <== xs[i] * xs[i];}y <== xs[n];§ Loops§ If statements§ Array accesses}
component main {public [x]} =RepeatedSquaring(1000);19ZKP MOOC

Circom: Witness Computation & Sub-circuits§ Witness computation:
more general than R1CS
§ “<--” is more generalthan “===”

template NonZero() {signal input in;signal inverse;
inverse <-- 1 / in; // not R1CS
1 == in * signal;// is R1CS}§ Access inputs/outputs
with dot-notation

template Main() {signal input a; signal input b;
component nz = NonZero();nz.in <== a;0 == a * b;}§ “component”s hold subcircuits

20

ZKP MOOC

Circom Tutorial

21

ZKP MOOC
Credit: Faithie/ShutterstockTutorial Example: Sudoku§ 9 by 9 grid
§ Some cells have #s§ Goal: fill all cells with 1…9§ Rule: no duplicates in any:
§ Column§ Row§ 3x3 sub-gridPuzzle22

Solution

ZKP MOOC

A Library for R1CS

23

ZKP MOOC
Credit: Faithie/ShutterstockCircom: Recap§ An HDL for R1CS
§ Key features:§ Direct control over constraints§ Custom language§ Can be good
§ Can be bad24

ZKP MOOC

R1CS Libraries§ A library in a host language (Eg: Rust, OCaml, C++, Go, …)§ Key type: constraint system§ Maintains state about R1CS constraints
Constraint System
and variables§ Key operations:§ create variableABC§ create linear combinations of variables§ add constraintvariables

25

ZKP MOOC

ConstraintSystem Operations
Variable creation

Adding constraints

cs.add_var(p, v) → id
• cs: constraint system• p: visibility of variable• v: assigned value• id: variable handlecs.constrain(lcA, lcB, lcC)
• Adds a constraint lcA × lcB = lcC

Constraint System

Linear Combination creation

cs.zero() : returns the empty LC
lc.add(c, id) → lc'• id: variable• c: coefficient• lc' := lc + c * id

A

BClcA

lcB

lcC

variables

26id(p, v)

ZKP MOOCExample: Boolean AND
Create resultvariable
fn and(cs: ConstraintSystem, a: Var, b: Var) → Var {let result = cs.new_witness_var(|| a.value() & b.value());
self.cs.enforce_constraint(lc!() + a,lc!() + b,
Enforce constraintlc!() + result,);
resultCreate linear combinations}27

ZKP MOOCExample: Boolean AND
Create result
variablefn and(cs: ConstraintSystem, a: Var, b: Var) → Var {is unpleasant, tedious, and error-prone!
let result This= cs.new_witness_var(||a.value() & b.value());
self.cs.enforce_constraint(lc!()Can+ a,
you imagine writing a complex algorithm likelc!() + b, signature verification in this style?
Enforce constraintlc!() + result,);
resultCreate linear combinations}28

ZKP MOOC

Idea: Leverage Language Abstractions!
We can use language abstractions like structs, operator
Wrap variable inoverloading,dedicated type
methods, etc. to allow better developer UX:struct Boolean { var: Var };impl BitAnd for Boolean {fn and(self: Boolean, other: Boolean) → Boolean {Implement// Same as before
interface for
Boolean { var: result }operatoroverloading }}29

ZKP MOOC

Does it work? Yes!
Can use abstractions like normal code:
let a = Boolean::new_witness(|| true);let b = Boolean::new_witness(|| false);(a & b).enforce_equal(Boolean::FALSE);

Many different gadget libraries:• libsnark: gadgetlib (C++)• arkworks: r1cs-std + crypto-primitives (Rust)• Snarky (Ocaml)• Gnark (Go)30

ZKP MOOC

What about Witness Computation?
§ Can perform arbitrary computations to generate
witnesses
Closure (lambda) executed only during proving!

let a = Boolean::new_witness(|| (4 == 5) & (x < y));let b = Boolean::new_witness(|| false);(a & b).enforce_equal(Boolean::FALSE);

31

ZKP MOOC

Arkworks Tutorial

32

ZKP MOOC
Credit: Faithie/ShutterstockCompiling a
Programming Language
to R1CS33

ZKP MOOC
Credit: Faithie/ShutterstockHDLs & Circuit Libraries§ Difference:§ Host language v. custom language§ Similarities:§ explicit wire creation (explicitly wire values)§ explicit constraint creation§ Do we need to explicitly build a circuit?
§ No!
34

ZKP MOOC

Compiling PLs to Circuits (Idea)
ProgramCompilerR1CS• Wires• Constraints• Variables• Mutation• Functions• Arrays35

ZKP MOOC

ZoKrates: Syntax§ Struct syntax for customtypes§ Variables contain values
during execution/proving§ Can annotate privacy§ “assert” creates
constraints

type F = field;

def main(public F x, private
F[2] ys) {field y0 = y[0];field y1 = y[1];assert(x = y0 * y1);}

36

ZKP MOOC

Zokrates: Language features§ Integer generics§ Arrays§ Variables§ Mutable§ Fixed-length loops§ If expressions§ Array accesses

def repeated_squaring<N>(field x) -> field {field[N] mut xs;
xs[0] = x;
for u32 i in 0..n {xs[i + 1] = xs[i] * xs[i];}return xs[N];}def main (public field x) -> field {repeated_squaring::<1000>(x)}37

ZKP MOOC

What about Witness Computation?
§ No way to compute witnesses§ All witnesses must be provided as input
def main(private field a, publicfield b) {assert(a * b == 1)}38

ZKP MOOC

ZoKrates Tutorial

39

ZKP MOOC
Credit: Faithie/ShutterstockZKP Toolchains:
A Quick Tour40

ZKP MOOC
Credit: Faithie/ShutterstockToolchain TypeHDLa language fordescribing circuit
synthesis

Librarya library for describing
circuit synthesis

41

PL + Compiler
a language,
compiled to a circuit

ZKP MOOC

Toolchain Types, OrganizedStandalone Language?

CircuitNo

Yes

Library(arkworks)

HDL(circom)

Language TypePL(noir)

Program42

ZKP MOOC

circom===

Pros:§ Clear constraints§ Elegant syntax
Cons:
HDL
§ Hard to learn§ Limited abstraction
types?

arkworks

ZoKrates

Pros:§ Clear constraints§ As expressive as Rust
Cons:§ Need to know Rust
§ Few optimizations

Pros:§ Easiest to learn§ Elegant syntax
Cons:§ Limited witness
computation

manual opts

43

just a PL

always implicit

ZKP MOOC

Other toolchains
HDL• Circom

Library• Arkworks (Rust)• Gadgetlib (C++)• Bellman (Rust)• Snarky (OCaml)• PLONKish (Rust)

44

PL + Compiler• ZoKrates• Noir• Leo• CairoZKP MOOC

Timeline

BellmanGadgetlib

2015

Arkworks
Noir

SnarkyCircom ZoKrates

45

PLONKish2020

Cairo
Leo?
ZKP MOOC

Shared Compiler Infrastructure?
SourceCairo
ZoKrates
CircomPLONKishNoir
SnarkyBellmanGadgetlib
Leo

Common Techniques
RAM-checking CirC

Structures

TargetMutation
A library for
Fixed-Width
Variables
ZKPInt.languages

R1CS

Booleansgithub.com/circify/circOptimization
Control-Flow

46

Plonk
AIR

ZKP MOOC

Summary
HDL

Library(circom)

(ark)

R1CS

Idea
PL

ZKP(noir)47

ZKP MOOC

End of Lecture48

ZKP MOOC
Credit: Faithie/Shutterstock