Inside a modern prover: sumcheck, lookups and Binius

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

Part 2 listed what makes Ethereum hard to prove. Among them were bit operations and Keccak, the hash that holds Ethereum’s state together, costing by one estimate a thousand times as much as a proof-friendly hash. Most provers of that time worked in a prime field of about 2²⁵⁴ elements, and paid for every bit as if it were a 254-bit number.

Since last autumn I have been working part-time with KOI Foundation as a zero-knowledge protocol engineer, alongside my final-year project in the lab. The job is mostly reading papers and the code that implements them. The provers I have been reading rest on three ideas: the sumcheck protocol, lookup arguments and, in Binius, binary fields.

Everything is a sum over a cube

The sumcheck protocol is older than blockchains. Lund, Fortnow, Karloff and Nisan introduced it in 1990 [1], and Justin Thaler’s textbook, my main reference, calls it the single most important “hammer” for efficient interactive proofs [2]. It proves that a polynomial, summed over every corner of the Boolean hypercube {0, 1}ⁿ, gives some value H.

A list of 2ⁿ numbers is a function on the hypercube, each index in binary being a corner, and exactly one polynomial of degree at most one in each variable takes those values, the list’s multilinear extension. A claim such as “every constraint holds” can be rewritten as a sum over the cube of polynomials built from such extensions [2].

Take eight numbers, 3, 1, 4, 1, 5, 9, 2, 6, on the corners 000 to 111, with multilinear extension f. Their sum is 31. The prover splits the sum on the first variable and sends both halves: g₁(0) = 3 + 1 + 4 + 1 = 9 and g₁(1) = 5 + 9 + 2 + 6 = 22. The verifier checks that 9 + 22 = 31 and replies with a random r₁. The prover must now defend a smaller claim: that g₁(r₁) is the sum of f(r₁, x₂, x₃) over the four remaining corners. Each round removes a variable, until one claim about f at a random point is left, for the commitment to settle.

Round	g(0), g(1)	Check	r	g(r)
1	9, 22	9 + 22 = 31	2	35
2	24, 11	24 + 11 = 35	3	82
3	83, 96	83 + 96 ≡ 82	5	51
end	the commitment gives f(2, 3, 5) = 51

Two properties make it the workhorse of current provers. The first is soundness: a false sum forces at least one false polynomial, and a false polynomial of degree d agrees with the true one at no more than d points, so a cheat survives all n rounds with probability at most n·d/|F| [2], negligible over a field of about 2¹²⁸ elements. The second is prover speed. After each challenge r, the prover folds its table in half, each pair (a, b) that differs only in the variable just fixed becoming (1 − r)·a + r·b: the eight numbers become 7, 17, 0 and 11, then two, then one. The work is linear in the size of the data, with no fast Fourier transform over the whole computation.

Opening one corner

The first concrete problem I worked on at KOI was a small version of a question Ethereum also faces: can a commitment to a long list, say of hashes standing for some state, be opened at one position cheaply and provably?

A plain sum cannot do it. Addition is commutative, so a sum is blind to position: it cannot tell a value at corner 101 from the same value at 011. The fix is the equality polynomial,

eq(k, x) = ∏ᵢ (kᵢxᵢ + (1 − kᵢ)(1 − xᵢ)),

which is 1 at x = k and 0 at every other corner, so summing eq(k, x)·f(x) over the cube gives exactly f(k); for the list above and k = 101, it picks out 9. Proving that sum is one more sumcheck, at the end of which the verifier computes eq(k, r) itself and asks the commitment for f(r). The same polynomial runs all through the Jolt paper [3].

It took me several passes, on paper and in Python, to see why this works, and a hint about dynamic programming to see why it is fast. The prover needs eq(r, x) at all 2ⁿ corners, and builds the table one variable at a time: start from [1] and replace every entry v by the pair (1 − rᵢ)·v and rᵢ·v. Each entry costs one multiplication instead of n. This tensor product returns in the Binius commitment below.

Lookups: proving that you read from a table

Part 2 introduced lookup arguments: the prover shows that an operation’s inputs and outputs sit in a table of correct results. With Plookup, the prover’s work grows with the table [4].

Lasso, by Srinath Setty, Justin Thaler and Riad Wahby, lifts that limit for tables with structure [5], and its companion Jolt uses it to prove a RISC-V processor [3]. For an instruction on two 64-bit inputs, the table of all results has 2¹²⁸ entries. But the result of, say, a bitwise AND can be assembled from results on small chunks of the inputs, so one lookup into the huge table becomes a few into small subtables, and the prover pays for the number of lookups rather than the size of the table. Barry WhiteHat called the end point, circuits made of nothing but lookups, the lookup singularity [6].

The part of Lasso I spent longest on checks the lookups themselves, by offline memory checking, an idea of Blum, Evans, Gemmell, Kannan and Naor [7]. The table is treated as a memory whose entries start with an access counter of 0. Each lookup reads a triple (address, value, counter) and writes it back with the counter plus one. The prover then shows that the initial entries plus the writes form the same multiset as the reads plus the final entries.

	Tuples (address, value, counter)
Initial	(0, 0, 0), (1, 1, 0), (2, 4, 0), (3, 9, 0)
Reads	(2, 4, 0), (3, 9, 0), (2, 4, 1)
Writes	(2, 4, 1), (3, 9, 1), (2, 4, 2)
Final	(0, 0, 0), (1, 1, 0), (2, 4, 2), (3, 9, 1)

In January the team spent an evening on one question: what are the counters for? Lasso compresses each tuple into one field element, a·γ² + v·γ + t − τ, with the same random γ and τ throughout, and compares the products of the two sides [5]. Rereading the paper settled it: the counters are what make the check mean anything. Without them, every write copies its read exactly, the two sides agree whatever was read, and a prover could read 2² = 5 and pass. With them, the accesses to each address must form an unbroken chain from the initial entry to the final one. The products themselves are checked layer by layer as a binary tree, in the style of Goldwasser, Kalai and Rothblum: sumcheck again [8].

I then mapped all this onto the memory-checking and Surge modules of Jolt’s Rust code [9]. That became the pattern of the job: one line of mathematics can be a whole file of code, and the quickest test of whether I understood the line was to find it in the file.

Binius: stop paying for bits you do not use

Vitalik Buterin’s introduction to Binius starts from the waste [10]: over a 256-bit prime field, every value costs a whole field element, even a single bit. Binius, by Benjamin Diamond and Jim Posen of Irreducible, works over binary fields instead [11]. Data stays as bits, and a large field is used only where security needs it, for the verifier’s random challenges.

The fields form a tower, a construction of Wiedemann’s [12]. Adjoin to the bits {0, 1} an element x₀ with x₀² = x₀ + 1 to get four elements, then x₁ with x₁² = x₁x₀ + 1 to get sixteen, and so on up to 128 bits [10], [11]. Each field sits inside the next with the same bits, so a 4-bit value is also a 128-bit value with zeros on top, and multiplying a small element by a large one is cheap.

In January the team began a small Python version of the Binius commitment, to be checked against Vitalik’s reference code [13]; my part was the Reed–Solomon step. We used the galois library, which builds the 16-element field the textbook way, as polynomials modulo x⁴ + x + 1, and the numbers stopped matching: same field, different coordinates, so the same bit patterns multiply differently.

In the 16-element field	Tower (Binius)	Textbook, mod x⁴ + x + 1
2 × 2	3	4
2 × 3	1	6
3 × 3	2	5
four-element subfield	{0, 1, 2, 3}	{0, 1, 6, 7}

The commitment itself works like this [10], [11]. Arrange the 2ⁿ bits as a grid, pack each row into larger field elements and extend it with a Reed–Solomon code, reading it as a polynomial’s values and appending more of them, and commit to the columns with a Merkle tree. To prove f(r), split r into a row part and a column part. The prover sends one row, t′, the sum of all rows weighted by the tensor product of the row part. The verifier extends t′ itself and compares it with a few sampled columns, weighted the same way; because the code is linear, a false t′ would disagree in many places. Weighting t′ by the tensor product of the column part then gives f(r). This is the “square root” idea of Ligero and Brakedown [14], [15]: for N values, the proof carries on the order of √N field elements.

Two details cost me the most time. First, Reed–Solomon codes over prime fields use a fast Fourier transform on a subgroup of size 2ᵏ, but the nonzero elements of a binary field form a group of odd order, 2ᵏ − 1, with no such subgroups; Binius uses the additive FFT of Lin, Chung and Han instead [16]. My update to the team on 6 March put it this way:

For additive FFT, the novel polynomial basis built from subspace polynomials allows recursive odd–even splits similar to the multiplicative FFT, and it reduces the FFT complexity to O(N log N).

Second, the step I was stuck on in November: ring switching, from Diamond and Posen’s follow-up paper [17]. It lets small-field data, packed into large-field elements, be committed and opened with a large-field scheme, which is where the tower’s nesting pays off. Paired with FRI-style folding in place of the grid, it cuts proofs from √N to polylogarithmic size.

Where it is heading, and why Ethereum cares

The field has moved while I learnt it. Irreducible’s new Binius documentation is built around an arithmetization called M3, multi-multiset matching [18]: a computation is a set of tables whose rows push and pull tuples through channels, and the proof shows that every channel balances. The memory check above is one instance, and Lasso is re-expressed this way.

One worked example there is inclusion in a Merkle Patricia trie, the structure in which Ethereum keeps its state, with its nodes linked by Keccak-256 hashes [18], [19]. Keccak is XOR, AND, NOT and rotations of 64-bit words, all native to a binary field. That matters because Ethereum wants stateless clients, which check each block against a proof of the state it touches. One plan replaces the trie with a Verkle tree, John Kuszmaul’s 2018 idea of a Merkle tree with vector commitments in place of hashes [20]. Another moves to a binary hash tree and proves its branches with a STARK, which would also survive a quantum computer [21]. That plan needs fast proofs of hashing, which is what binary-field provers are built for.

My final-year project is in its last weeks, so I am stepping back from this work for now. What I take away is less any one protocol than a habit: read the paper, find the code, and work a small example by hand until the two agree. Every confusion in this post, from the counters to the field that was not a tower, gave way to that.

References

1. Carsten Lund, Lance Fortnow, Howard Karloff and Noam Nisan. Algebraic methods for interactive proof systems. Journal of the ACM 39(4), pp. 859–868, 1992; conference version in FOCS 1990. doi:10.1145/146585.146605.
2. Justin Thaler. Proofs, Arguments, and Zero-Knowledge. Foundations and Trends in Privacy and Security 4(2–4), pp. 117–660, 2022. doi:10.1561/3300000030. Author's copy, version of 18 July 2023.
3. Arasu Arun, Srinath Setty and Justin Thaler. Jolt: SNARKs for virtual machines via lookups. In EUROCRYPT 2024. IACR ePrint 2023/1217.
4. Ariel Gabizon and Zachary J. Williamson. plookup: a simplified polynomial protocol for lookup tables. 2020. IACR ePrint 2020/315.
5. Srinath Setty, Justin Thaler and Riad Wahby. Unlocking the lookup singularity with Lasso. In EUROCRYPT 2024. IACR ePrint 2023/1216.
6. Barry WhiteHat. Lookup singularity. zkresear.ch, 23 November 2022. zkresear.ch/t/lookup-singularity/65.
7. Manuel Blum, Will Evans, Peter Gemmell, Sampath Kannan and Moni Naor. Checking the correctness of memories. Algorithmica 12, pp. 225–244, 1994. doi:10.1007/BF01185212.
8. Shafi Goldwasser, Yael Tauman Kalai and Guy N. Rothblum. Delegating computation: interactive proofs for muggles. Journal of the ACM 62(4), 27, 2015. doi:10.1145/2699436.
9. a16z crypto. Jolt. GitHub repository, files jolt-core/src/lasso/memory_checking.rs and surge.rs, as of 13 March 2025.
10. Vitalik Buterin. Binius: highly efficient proofs over binary fields. 29 April 2024. vitalik.eth.limo.
11. Benjamin E. Diamond and Jim Posen. Succinct arguments over towers of binary fields. 2023. IACR ePrint 2023/1784.
12. Doug Wiedemann. An iterated quadratic extension of GF(2). The Fibonacci Quarterly 26(4), pp. 290–295, 1988. fq.math.ca.
13. Vitalik Buterin. Binius reference code, in the ethereum/research repository, April–May 2024. github.com/ethereum/research/tree/master/binius.
14. Scott Ames, Carmit Hazay, Yuval Ishai and Muthuramakrishnan Venkitasubramaniam. Ligero: lightweight sublinear arguments without a trusted setup. In ACM CCS 2017, pp. 2087–2104. doi:10.1145/3133956.3134104.
15. Alexander Golovnev, Jonathan Lee, Srinath Setty, Justin Thaler and Riad S. Wahby. Brakedown: linear-time and field-agnostic SNARKs for R1CS. In CRYPTO 2023. IACR ePrint 2021/1043.
16. Sian-Jheng Lin, Wei-Ho Chung and Yunghsiang S. Han. Novel polynomial basis and its application to Reed–Solomon erasure codes. In FOCS 2014, pp. 316–325. doi:10.1109/FOCS.2014.41.
17. Benjamin E. Diamond and Jim Posen. Polylogarithmic proofs for multilinears over binary towers. 2024. IACR ePrint 2024/504.
18. Irreducible. Binius documentation, binius.xyz, archived 17 February 2025: pages on M3, Lasso and Merkle–Patricia inclusion.
19. ethereum.org. Merkle Patricia Trie. Developer documentation. ethereum.org.
20. John Kuszmaul. Verkle trees. MIT PRIMES, 2018. math.mit.edu.
21. Vitalik Buterin. Possible futures of the Ethereum protocol, part 4: The Verge. 23 October 2024. vitalik.eth.limo.