← Writing

Only adds and multiplies: why proving the EVM looks impossible

Part 2 of Zero Knowledge, Full Proof. A proof system understands two operations, addition and multiplication. What it takes to turn a program into polynomials, why the Ethereum Virtual Machine resists, and the two routes the teams racing to prove it are taking.

The GitHub page of the appliedzkp zkevm-specs repository in November 2021: a recent commit titled Bitwise opcode spec (AND, OR, XOR), and a README that says the project aims to define a validity snark proof for Ethereum transactions.

Part 2 of Zero Knowledge, Full Proof, a series on zero-knowledge proofs and privacy on-chain.

Part 1 ended on a question: how does one prove something about an arbitrary program, rather than about two balls? The honest answer is “with great difficulty”. Most zk-rollups running on Ethereum today can do payments and swaps, and little else [1]. Vitalik Buterin’s guide to rollups from January 2021 put the problem in one line of its comparison table: proving general-purpose EVM execution with a zk-SNARK “is much harder than proving simple computations” [2]. In the same guide, he predicted that ZK rollups would nonetheless “win out in all use cases” in the medium to long term. This post is about the gap between those two sentences, and about why it is starting to close.

A program with two operations

A zero-knowledge proof does not see code. It sees a circuit: a fixed network of additions and multiplications over the integers modulo a large prime. Ye Zhang of Scroll noted last year that the standard constraint format, R1CS, supports only addition and multiplication [1]. Every other operation a program performs has to be rebuilt out of those two.

Vitalik’s classic example makes this concrete [3]. Suppose I want to prove that I know a number x satisfying x³ + x + 5 = 35, without revealing that x = 3. The first step is to flatten the equation into a sequence of single operations, each of which becomes one gate and one constraint:

The equation x cubed plus x plus 5 equals 35 as a circuit The input x feeds four gates in turn: a multiplication x times x gives s1, a multiplication s1 times x gives y, an addition y plus x gives s2, and an addition s2 plus 5 gives the output, which must equal 35. With x equal to 3 the wires carry 9, 27 and 30, and the output is 35. x × × + + 5 35 s1 = 9 y = 27 s2 = 30 x = 3 s1 = x · x s2 = y + x y = s1 · x 35 = s2 + 5
Four gates, four constraints. The prover's secret is the value on every wire (the witness): with x = 3, each constraint checks out. After Vitalik Buterin's example [3].

The second step is the one that makes large programs feasible. The constraints are rewritten as a rank-1 constraint system, and then as a single statement about polynomials: the witness satisfies every constraint if and only if one polynomial built from it is divisible by another polynomial that is zero at every constraint’s index [3], [4]. A million constraints become one polynomial identity.

Checking that identity is cheap because of a result from 1979 and 1980. Two different polynomials of degree d can agree on at most d points, so a nonzero polynomial of degree d vanishes at a uniformly random point of a finite field F with probability at most d/|F|. This is the Schwartz–Zippel lemma [5], [6]. On the curve that Ethereum’s precompiles support, the field has about 2²⁵⁴ elements. For a circuit with a million constraints, a false claim survives a check at one random point with a probability of around 10⁻⁷⁰. The random point is either derived by the Fiat–Shamir transform from part 1, or hidden inside a trusted setup, which is the subject of part 4.

What ordinary code does that circuits cannot

The difficulty is everything that happens before the polynomials: rewriting a real program as additions and multiplications. Four habits of ordinary code are expensive in a circuit.

The first is branching. A circuit is fixed in advance, so it cannot take one path or the other. It computes both branches and selects the result with a bit b, as b·u + (1 − b)·v, plus a constraint b·(b − 1) = 0 that forces b to be 0 or 1.

The second is looping. A loop whose length depends on the input cannot exist in a fixed circuit; it must be unrolled up to a maximum number of iterations, and the circuit pays for the maximum every time [1].

The third is bit manipulation. A CPU computes the AND or XOR of two 256-bit words in one instruction. A circuit sees numbers only as field elements, never as bits, and a 256-bit word does not even fit in one element of a field of about 2²⁵⁴ elements, so it is held in pieces, such as two 128-bit halves. To take an AND or XOR, the circuit must first split the word into 256 bits, constrain every bit with b·(b − 1) = 0, and prove that the bits recombine into those pieces. One instruction becomes hundreds of constraints.

The fourth is hashing. Standard hash functions such as SHA-256 and Keccak are built from exactly those bit operations. Hash functions designed for proofs, such as Poseidon, work natively with field elements instead [7]. By Zhang’s estimate, a Keccak hash costs about a thousand times as much as a Poseidon hash inside a circuit [1].

In ordinary codeIn a circuit
if / elseboth branches, plus a selector bit
a loop of any lengthunrolled to a fixed maximum
AND, XOR on 256-bit wordssplit into bits, hundreds of constraints
SHA-256, Keccakvery expensive; Poseidon is cheap

Two ways to put an application in a circuit

Zhang described two strategies [1]. The first is to design a dedicated circuit for each application, the equivalent of building an ASIC. This is what most of today’s zk-rollups do: a circuit for transfers, a circuit for swaps. It is efficient, but every new application needs a new circuit written by a specialist, and applications in different circuits cannot call each other.

The second is to build one circuit for a whole processor, and prove the execution of any program on it. For Ethereum, the processor is the EVM. The catch is the fixed-circuit rule again. The circuit cannot know in advance which instruction comes next, so every step of the execution must contain the logic for every instruction, with selectors switching on the one actually used. Even to prove a single addition, one pays for all of it. Zhang estimated that the EVM circuit for one step is about 10,000 times larger than a circuit for addition alone [1].

Three steps of a processor circuit Three columns, one per execution step. Each column contains the same six instruction blocks: ADD, MUL, AND, SLOAD, CALL and KECCAK. In step 1 only ADD is switched on, in step 2 only MUL, and in step 3 only SLOAD, but every block is present in every step. step 1: ADDstep 2: MULstep 3: SLOAD ADDMULANDSLOADCALLKECCAK ADDMULANDSLOADCALLKECCAK ADDMULANDSLOADCALLKECCAK … and the rest of the instruction set, every step
A circuit for a processor cannot know which instruction comes next, so every step contains all of them and a selector switches one on. The proof pays for every box, not only the highlighted ones.

Why the EVM in particular

A processor circuit is expensive for any machine. The EVM, designed in 2014 to be executed by ordinary computers rather than proven, makes it harder in six specific ways, which Zhang listed last year [1].

Diagram of the Ethereum Virtual Machine: inside the machine state sit the program counter, the gas available, the stack and the memory; outside it, the EVM code in a virtual ROM and the account storage in the persistent world state.
The EVM as ethereum.org draws it [8]: a program counter, gas, a stack and memory that vanish after each transaction, and storage that persists. Diagram from ethereum.org, adapted from Ethereum EVM illustrated, © 2018 Takenobu Tani, BSD 3-Clause licence.

First, the EVM supports very few elliptic curves. Its precompiled contracts offer pairings on only one curve, alt_bn128, now usually called BN254 [9]. That makes it hard to verify one proof inside another, a technique called recursion.

Second, the EVM works on 256-bit words, held on a stack up to 1,024 items deep [8], while proof systems work natively in a prime field of a different size. Every mismatched operation needs extra range checks; by Zhang’s estimate, around 100 more constraints for every EVM step.

Third, the EVM has many special instructions, such as CALL, and error conditions tied to gas, each of which needs its own careful circuit.

Fourth, the EVM is a stack machine [8]. zkSync and StarkWare avoid this by defining their own register-based instruction sets and compiling contracts into them, which makes them compatible with Ethereum’s languages but not with its bytecode.

Fifth, Ethereum’s state is stored in a Merkle Patricia trie hashed with Keccak, which is far from zk-friendly: by Zhang’s estimate, a Keccak hash costs about a thousand times as much as a Poseidon hash to prove [1].

Sixth, all of the above is multiplied by the processor-circuit overhead: every step pays for the whole EVM.

Why it is becoming possible anyway

Zhang’s note argues that the cost is no longer a barrier, because of four advances [1].

First, polynomial commitments. A scheme such as KZG lets a prover commit to a polynomial and later open it at any point with a constant-size proof [10]. Proof systems built on it, such as PLONK, need only one universal setup for all circuits up to a chosen size instead of one per circuit [11], and their constraints are no longer limited to one multiplication each, which is what lets later variants of PLONK add custom gates that express more in a single constraint [1].

Second, lookup arguments. Instead of proving a bitwise operation gate by gate, the prover shows that each input and output appears in a precomputed table of correct results. Plookup made this efficient [12], and it is exactly what bit operations and hash functions need.

Third, recursion without a trusted setup. Earlier recursive schemes needed a trusted setup and cycles of expensive pairing-friendly curves; Halo replaced them with ordinary curves and an argument whose cost is amortised across many proofs [13]. Checking the final result on Ethereum still needs an extra “wrapping” step [1].

Fourth, hardware. Provers are moving to GPUs, FPGAs and ASICs. Zhang wrote that his team’s paper on an ASIC prover had been accepted at ISCA, the leading computer-architecture conference, and that their GPU prover was about five to ten times faster than Filecoin’s implementation [1]. PipeZK, a pipelined accelerator presented at ISCA in 2021, shows what this line of work looks like [14].

The architecture Scroll is building on was specified by the Ethereum Foundation, whose team Scroll works with closely, and it is being written down in the open, in the repository shown at the top of this post [1], [15]. It splits the proof in two: a state proof that every read and write to storage, memory and the stack is consistent, and an EVM proof that each instruction computed the right thing from the values it read.

Two routes, four teams

The teams racing to build a zkEVM are splitting along one line: whether to prove the EVM itself, or a different machine that runs the same programs.

Two routes from a Solidity contract to a proof A Solidity contract can take two routes. On the left, it is compiled to a virtual machine designed for proofs, and that machine is proven: zkSync 2.0, and StarkNet with its own language, Cairo. This is easier to prove but the bytecode differs from Ethereum's. On the right, it is compiled to EVM bytecode as today, and the EVM itself is proven: Scroll with the Ethereum Foundation, and Polygon Hermez. This is fully compatible but harder to prove. Solidity contract compile to aproof-friendly VM compile to EVMbytecode, as today prove that VM prove the EVM itself zkSync 2.0;StarkNet (Cairo) Scroll with the EF;Polygon Hermez easier to prove,bytecode differs fully compatible,harder to prove
The two routes, and who is on each as of February 2022.

The first route keeps the language and changes the machine. zkSync and StarkWare compile contracts into instruction sets of their own design, register-based and built to be proven [1]. StarkNet, whose alpha has been running on Ethereum mainnet since November 2021, uses its own language, Cairo [16]. zkSync 2.0 compiles Solidity, and this week Matter Labs opened its public testnet [17]. Proving is easier on this route, but the compatibility is at the level of the language, not the bytecode: tools and contracts that depend on the EVM’s exact behaviour do not automatically carry over.

The second route proves the EVM’s own bytecode, so that every existing contract and tool works unchanged, and the prover pays for every one of the six problems above. Scroll is building the Ethereum Foundation’s design with the Foundation’s own team [1], [15]. Polygon, which merged with Hermez Network in August 2021 in a deal worth about $250 million [18], is building a zkEVM of its own; this month its team published a new consensus design, written for that zkEVM, on the Ethereum research forum [19].

None of the EVM-compatible systems is on Ethereum mainnet yet. But the question has changed. A year ago it was whether the EVM could be proven at all; now it is which compromises to make, and how quickly the provers can be made fast.

What comes next

Every system in this post rests on a proof system underneath, and the choice of proof system brings its own trade-offs: how large the proof is, how long it takes to produce, whether it needs a trusted setup ceremony, and whether it would survive a large quantum computer. Part 4 looks at that choice.

References

  1. Ye Zhang. zkEVM. HackMD, 2021. hackmd.io/@yezhang/S1_KMMbGt.
  2. Vitalik Buterin. An incomplete guide to rollups. 5 January 2021. vitalik.eth.limo.
  3. Vitalik Buterin. Quadratic arithmetic programs: from zero to hero. December 2016. vitalik.eth.limo; first published on Medium.
  4. Maksym Petkus. Why and how zk-SNARK works. 2019. arXiv:1906.07221.
  5. Jacob T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM 27(4), pp. 701–717, 1980. doi:10.1145/322217.322225.
  6. Richard Zippel. Probabilistic algorithms for sparse polynomials. In Symbolic and Algebraic Computation (EUROSAM '79), pp. 216–226, 1979. doi:10.1007/3-540-09519-5_73.
  7. Lorenzo Grassi, Dmitry Khovratovich, Christian Rechberger, Arnab Roy and Markus Schofnegger. Poseidon: a new hash function for zero-knowledge proof systems. In 30th USENIX Security Symposium, pp. 519–535, 2021. usenix.org. Preprint: IACR ePrint 2019/458.
  8. ethereum.org. Ethereum Virtual Machine (EVM). Developer documentation. ethereum.org/developers/docs/evm. Archived copy: 21 February 2022.
  9. Vitalik Buterin and Christian Reitwiessner. EIP-197: precompiled contracts for optimal ate pairing check on the elliptic curve alt_bn128. 2017. eips.ethereum.org/EIPS/eip-197.
  10. Aniket Kate, Gregory M. Zaverucha and Ian Goldberg. Constant-size commitments to polynomials and their applications. In Advances in Cryptology: ASIACRYPT 2010, pp. 177–194, 2010. doi:10.1007/978-3-642-17373-8_11.
  11. Ariel Gabizon, Zachary J. Williamson and Oana Ciobotaru. PLONK: permutations over Lagrange-bases for oecumenical noninteractive arguments of knowledge. 2019. IACR ePrint 2019/953.
  12. Ariel Gabizon and Zachary J. Williamson. plookup: a simplified polynomial protocol for lookup tables. 2020. IACR ePrint 2020/315.
  13. Sean Bowe, Jack Grigg and Daira Hopwood. Recursive proof composition without a trusted setup. 2019. IACR ePrint 2019/1021.
  14. Ye Zhang, Shuo Wang, Xian Zhang, Jiangbin Dong, Xingzhong Mao, Fan Long, Cong Wang, Dong Zhou, Mingyu Gao and Guangyu Sun. PipeZK: accelerating zero-knowledge proof with a pipelined architecture. In 2021 ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA), pp. 416–428, 2021. doi:10.1109/ISCA52012.2021.00040.
  15. Ethereum Foundation, Applied ZKP team. Zkevm specifications. GitHub repository appliedzkp/zkevm-specs, 2021. github.com/appliedzkp/zkevm-specs.
  16. StarkWare. StarkNet Alpha, now on mainnet! 29 November 2021. medium.com/starkware. Archived copy: 29 November 2021.
  17. Matter Labs. zkSync 2.0: public testnet is live! 22 February 2022. blog.matter-labs.io.
  18. Polygon. Hermez Network is joining Polygon and becoming Polygon Hermez, via the first full-blown merger of two blockchain networks. 13 August 2021. polygon.technology. Archived copy of the original announcement: 8 September 2021.
  19. David Schwartz and Jordi Baylina. Proof of Efficiency: a new consensus mechanism for zk-rollups. Ethereum Research, 10 February 2022. ethresear.ch.

More writing →