Pinocchio and the Procedural Era: How the First Practical SNARKs Were Built — Article 1 of the ZKP Systems Series

Before 2013, zero-knowledge proofs existed in theory. Goldwasser, Micali, and Rackoff had proven they were possible back in 1985. But “possible in theory” and “runs on a laptop in under a second” are very different things. The gap between them took nearly three decades to close.

Pinocchio closed it.

This article covers the first wave of practical SNARKs — the systems built between 2013 and 2018 that proved the technology could work outside of a whiteboard. They are largely obsolete today, but understanding them is non-negotiable: every modern system is either a direct descendant or a deliberate reaction to what this era built.

The Problem Pinocchio Had to Solve

To build a SNARK, you need to answer a deceptively hard question: how do you encode an arbitrary computation as something a cryptographic proof system can reason about?

A program is a sequence of operations — additions, multiplications, conditionals, memory reads. Cryptographic proof systems, on the other hand, work over mathematical structures: polynomials, elliptic curves, finite fields. Bridging these two worlds required two key ideas that Pinocchio introduced to practice.

Step 1: Arithmetic Circuits

The first idea is to represent computation as an arithmetic circuit — a directed acyclic graph where wires carry field elements and gates perform addition or multiplication.

Take a simple computation: y = x² + x + 1

As an arithmetic circuit:

x ──┬──── [×] ──── x²
            │               │
            └──── [+] ──────┤
                            │
                 1 ──────── [+] ──── y

Every program, no matter how complex, can be flattened into such a circuit. The circuit for SHA-256 has ~28,000 gates. The circuit for a full Ethereum transaction has millions. But the structure is always the same: wires and gates, nothing else.

Step 2: Rank-1 Constraint Systems (R1CS)

An arithmetic circuit can be further reduced to a Rank-1 Constraint System (R1CS) — a set of equations of the form:

(a · s) * (b · s) = (c · s)

where s is the witness vector (all the values in your circuit), and a, b, c are selector vectors that pick which wires participate in each constraint.

For our example y = x² + x + 1, the R1CS constraints are:

Constraint 1: x * x = x²          →  (pick x) * (pick x) = (pick x²)
Constraint 2: x² + x + 1 = y      →  (pick 1) * (pick x²+x+1) = (pick y)

In code, a simple R1CS constraint looks like this:

# R1CS representation for a * b = c
# Each constraint is a triple of vectors (A, B, C)
# The witness s must satisfy: (A·s) * (B·s) = C·s

import numpy as np

# Witness: [1, x, x_squared, y] for x=3, y=x²=9
s = np.array([1, 3, 9, 9])

# Constraint: x * x = x_squared
A = np.array([0, 1, 0, 0])  # picks x
B = np.array([0, 1, 0, 0])  # picks x
C = np.array([0, 0, 1, 0])  # picks x_squared

assert np.dot(A, s) * np.dot(B, s) == np.dot(C, s)
print("Constraint satisfied:", np.dot(A,s), "*", np.dot(B,s), "=", np.dot(C,s))
# Output: Constraint satisfied: 3 * 3 = 9

A full program becomes a list of such constraints. Satisfying all of them simultaneously proves the program executed correctly.

Step 3: From R1CS to QAP

R1CS is the right structure, but it’s not yet something you can build a succinct proof around. Pinocchio’s key insight — following earlier theoretical work by Gennaro, Gentry, Parno, and Raykova — was to convert R1CS into a Quadratic Arithmetic Program (QAP).

The idea: represent each constraint as a polynomial, evaluated at a specific point. If you know the witness, you can construct a polynomial h(x) such that:

A(x) · B(x) - C(x) = h(x) · t(x)

where t(x) is a known target polynomial that has roots at every constraint point. If the prover can produce h(x), the verifier can check this equation — without seeing the witness — using elliptic curve pairings.

This is the mathematical core of Pinocchio, and of every pairing-based SNARK that followed. The prover encodes the witness into elliptic curve points (hiding it via the discrete log), and the verifier checks the QAP equation using pairings without ever seeing the raw values.

Pinocchio in Practice

The Pinocchio paper (Parno, Howell, Gentry, Raykova — IEEE S&P 2013) was the first system to make this practical. Its key numbers:

The bottleneck was the prover — it required expensive elliptic curve exponentiations for every gate in the circuit. A circuit with 10,000 gates took seconds to prove. Not fast, but for the first time, feasible.

The trusted setup was circuit-specific: a new ceremony for every new program. This was accepted as a necessary evil in 2013. It would become the central problem of the next decade.

The Procedural Era Variants (2013–2018)

Pinocchio opened a door. Several systems rushed through it, each solving a specific problem with the original design.

TinyRAM (2013) and vnTinyRAM (2014)

Pinocchio proved computations expressed as arithmetic circuits. But most programs aren’t written as circuits — they’re written as code that runs on a CPU, with memory, branches, and loops.

TinyRAM attacked this directly. Instead of converting programs to circuits, it defined a simple CPU architecture (TinyRAM) and built a SNARK that proved execution of arbitrary programs on that CPU. Memory accesses, branches, loops — all handled natively.

The cost was significant overhead: proving a TinyRAM execution is much more expensive than proving an equivalent arithmetic circuit, because you’re also proving each memory operation is valid. But the programming model was far more natural.

vnTinyRAM (2014) extended this with universality — one setup for any TinyRAM program of bounded size. This was the first attempt at what PLONK and Marlin would later solve properly.

Geppetto (2015)

Pinocchio proved one function at a time. Geppetto asked: what if you want to prove several functions share the same inputs or intermediate values?

The key contribution was multi-function proofs — a single proof that attests to the correct execution of multiple related computations simultaneously. Think proving that a hash was computed correctly AND that the result satisfies some predicate, in one proof.

Geppetto also introduced verification key reuse — a technique where different functions can share parts of the same trusted setup. This reduced ceremony overhead for programs with shared structure.

It was a clever optimization, but the underlying architecture was still circuit-specific and pairing-based. The paper’s ideas would be absorbed into later systems; Geppetto as a standalone system is rarely used today.

Buffet (2015)

Buffet targeted a different inefficiency: Pinocchio’s prover was equally expensive for every gate, whether that gate appeared once or a million times. For programs with highly repetitive structure — like cryptographic hash functions or loops — this was wasteful.

Buffet introduced proof composition for repetitive computations: prove one iteration of a loop correctly, then compose proofs for repeated iterations cheaply. It was an early form of recursive proof composition, a technique that would become central to the field five years later with Halo.

The limitation: Buffet’s composition only worked for a specific class of repetitive programs, not arbitrary recursion. It was a narrow optimization rather than a general solution.

ZoKrates and xJsnark: The Tooling Layer

By 2018, the academic systems had proven the theory. What was missing was usability — something developers could actually pick up and build with.

ZoKrates (2018, Jacob Eberhardt et al.) filled this gap. It’s a high-level programming language and toolchain that compiles down to arithmetic circuits and generates Groth16 proofs. Think of it as the GCC of the SNARK world.

Here’s the same x² = 25 proof from Article 0, written in ZoKrates:

# ZoKrates DSL — proof that we know x where x² = 25
def main(private field x, field y) -> bool {
    assert(x * x == y);
    return true;
}

Compare this to the raw circom version:

// circom — same proof, lower level
pragma circom 2.0.0;

template Square() {
    signal input x;
    signal input y;
    y === x * x;
}
component main {public [y]} = Square();

ZoKrates is more Python-like; circom is more hardware-description-language-like. ZoKrates handles more of the compilation automatically; circom gives you more control over the circuit structure.

The ZoKrates workflow:

# 1. Compile the program to a circuit
zokrates compile -i square.zok

# 2. Run the trusted setup (Groth16)
zokrates setup

# 3. Compute the witness (x=5, y=25)
zokrates compute-witness -a 5 25

# 4. Generate the proof
zokrates generate-proof

# 5. Verify
zokrates verify
# Performing verification...
# PASSED

ZoKrates is still actively maintained and widely used for Ethereum-based ZK applications. Its integration with Solidity verifier contracts makes it practical for production smart contract development.

xJsnark (2018, Jawurek, Kerschbaum, Lagendijk) took a different approach: a Java-based framework targeting developers already familiar with the JVM ecosystem. xJsnark emphasized circuit optimization — automatically applying techniques like common subexpression elimination and gate merging to reduce circuit size.

The performance gains were real but the adoption was limited. The Java ecosystem never became dominant in the ZK space, which gravitated toward Rust and TypeScript tooling. xJsnark’s circuit optimization ideas, however, influenced later compilers.

What the Procedural Era Got Right (and Wrong)

Looking back at 2013–2018 with the benefit of hindsight:

What it got right:

The architecture was correct. R1CS, QAP, pairing-based verification — these concepts are still at the core of Groth16, the most-used SNARK today. Pinocchio’s mathematical framework survived essentially intact.

The separation of concerns between circuit compilation and proof generation was the right abstraction. ZoKrates proved that developer-friendly tooling could sit on top of the cryptographic machinery.

What it got wrong:

Circuit-specific trusted setup was the original sin of the era. Every new program required a new ceremony. In practice this meant ZK applications were nearly impossible to update or iterate on. Zcash’s Powers of Tau ceremony — required every time the Zcash circuit changed — took months to organize.

Prover performance remained a serious obstacle. Proving a SHA-256 hash computation took seconds on 2018 hardware. This limited ZK to use cases where proofs were rare and large, not fast and frequent.

No recursion. Pinocchio-era systems could not compose proofs. You couldn’t prove that a proof was valid. This meant you couldn’t build incrementally verifiable systems — the kind that would later enable zkRollups.

The Bridge to What Came Next

The procedural era established what a SNARK had to be. The next era — starting with Groth16 in 2016, then Sonic, PLONK, and Marlin in 2019 — took that foundation and attacked each of its weaknesses in turn.

Groth16 shrank the proof to 3 group elements. PLONK made the setup universal. Halo eliminated the setup entirely. Nova replaced SNARKs with folding schemes for recursion.

Every one of those breakthroughs was a direct response to a limitation first identified in Pinocchio.

PQ Outlook

All systems in this article are not post-quantum safe.

Pinocchio, TinyRAM, vnTinyRAM, Geppetto, Buffet, ZoKrates, and xJsnark all rely — either directly or via Groth16 — on the hardness of the elliptic curve discrete logarithm problem (ECDLP) and bilinear pairing assumptions. Both are broken by Shor’s algorithm on a sufficiently large quantum computer.

The pairing-based verification equation at the core of every QAP-based system:

e(π_A, π_B) = e(α, β) · e(vk_x, γ) · e(π_C, δ)

…depends entirely on the hardness of computing discrete logs in the pairing groups. A quantum computer would render this check trivially forgeable.

The procedural era systems have no path to post-quantum security without replacing their cryptographic core — which would mean redesigning them from scratch. In practice, this era’s systems will be retired as quantum threats materialize, replaced by hash-based systems like STARKs, Plonky2, and SP1.

What to Remember from This Article

• R1CS is the universal intermediate representation — every SNARK starts here
• QAP converts R1CS into a polynomial divisibility check that pairings can verify
• Trusted setup was accepted as necessary in 2013; the rest of the decade was spent proving it wasn’t
• ZoKrates is the only system from this era still in active production use
• The prover performance problem — too slow for real-time applications — wasn’t solved until Plonky2 in 2022

Next up: the system that took Pinocchio’s architecture and compressed the proof to its theoretical minimum.

Article 2: Groth16 — Why Three Group Elements Is All You Need

References

• Parno, Howell, Gentry, Raykova — “Pinocchio: Nearly Practical Verifiable Computation” (IEEE S&P 2013)
• Ben-Sasson, Chiesa, Genkin, Tromer, Virza — “SNARKs for C: Verifying Program Executions Succinctly and in Zero Knowledge” (2013)
• Gennaro, Gentry, Parno, Raykova — “Quadratic Span Programs and Succinct NIZKs without PCPs” (2013)
• Costello, Fournet, Howell, Kohlweiss, Kreuter, Naehrig, Parno, Zahur — “Geppetto: Versatile Verifiable Computation” (IEEE S&P 2015)
• Eberhardt, Tai — “ZoKrates: Scalable Privacy-Preserving Off-Chain Computations” (IEEE Blockchain 2018)
• Ahmed, Jawurek, Kerschbaum — “xJsnark: A Framework for Efficient Verifiable Computation” (IEEE S&P 2018)