Research

Proofs

Proving GKR Soundness for Sparse Merkle Updates

4 Nov 2026 · 28 min read

A GKR verifier's acceptance is a statement about a circuit, and a system that applies sparse Merkle updates needs a statement about the update. We prove GKR soundness for membership, non-membership and update claims on trees of every depth, with challenges from KoalaBear's quartic extension, and mark which steps Isabelle/HOL re-checks and which are paper proofs.

arXiv: formal verification GitHub v1.1.1 arXiv: design and evaluation
Empty cleanroom hall with one floor tile lifted to show the pedestals beneath; GKR soundness

TL;DR

  • We prove GKR soundness for sparse Merkle updates. For membership, non-membership and update claims on trees of every depth, an accepted run certifies, except with a small and exact probability, that the siblings in the witness form a valid authentication path from the claimed leaf to the claimed root.
  • If the witness read from an input fixed before the challenges is not valid, the verifier accepts with probability at most \(\bigl(s_{\mathrm{out}} + \sum_i (8s_i + 1)\bigr)/|\mathbb{F}|\). With challenges drawn from the quartic extension of the 31-bit KoalaBear field, our update circuits stay below \(2^{-100}\) at the default parameters for up to 1,024 layers.
  • Isabelle/HOL re-checks the core: the layer-chain bound, its instance over the quartic extension, the arithmetization theorem for encoded witnesses and, over one field, the composition. The remaining steps are paper proofs, and every bound concerns the interactive public-coin protocol.
  • The implemented node hash is a truncated permutation and is not collision resistant, so position binding is our one cryptographic assumption. Only the statement that accepted runs for one key and root assert one leaf depends on it.
  • On the way to the proof we corrected four of our earlier claims, and the places where they broke are where tests and audits of a verifier without a code-level proof should aim first.

What an Accepted GKR Proof Says About an Update

When a GKR verifier accepts, what it has checked is a statement about a circuit. The prover claims that every output of a layered arithmetic circuit is zero, and the verifier pushes that claim down one layer at a time, running one sumcheck per layer under random challenges, until it reaches the input. A state synchronization system that accepts a sparse Merkle update on the strength of that verdict needs a statement about the update instead: an invalid update is accepted only with small probability. This article follows the route from the first statement to the second.

StateSync-GKR accepts sparse Merkle state transitions (membership of a key, non-membership of a key, an update of a key's leaf) on the strength of a GKR verifier's verdict. The GKR soundness theorem fixes a circuit and an input and bounds the probability that a false output claim is accepted. It does not say what the outputs of the compiled circuit mean for that input, and that meaning has to be proved for each family of circuits.

Sparse Merkle trees add a further point. Over a compressing hash, an authentication path carries far more free field elements than a root, so heuristically almost every root admits some valid path for almost any leaf. The existential statement, that a claim no witness can make valid is rarely accepted, is therefore weak. The statement that carries security fixes the witness.

An accepted run certifies, except with a small and exact probability, that the path the witness opens, the sibling list from the claimed leaf to the claimed root, is valid. It says nothing about paths nobody opened, and the system needs nothing more, because it acts on that one update. Every result is proved in our paper [1], and Isabelle/HOL re-checks its core. Along the way, this article marks each step as machine-checked, proved on paper, assumed, or out of scope.

The article builds on our earlier post What State Synchronization Asked of a GKR Prover, which told how the leaf encoding became a lemma and what a clean build did not say. Its trust-chain figure connected the shipped Rust verifier to the model's event under one unproved premise. We have since found that the premise fails on honest runs in general, so this article corrects that link: no result here reaches the shipped Rust verifier.

In exchange, the article leaves the next piece of work a precise handoff. The bound and the composition do not depend on the workload, so another application inherits the composition by proving its own arithmetization theorem, and another challenge field needs only a field construction and the lifting lemmas, with no second probabilistic proof.

Three Arguments and One Field Change

Turning acceptance into the validity of an update takes three arguments. Protocol soundness is the GKR bound for the gate set and the field that the system actually uses. Exact arithmetization says that the compiled checks accept exactly the valid updates: a missing check lets the protocol prove a weaker statement than intended with probability one, and a superfluous check makes honest updates unprovable. Commitment binding says that the root binds the state. Our node hash is a truncated permutation and is not collision resistant, so the binding we need is position binding of the tree.

A small-field prover adds one more step. It evaluates circuits over a 31-bit prime field and draws the verifier's challenges from an extension field, so the bound has to hold over the field the challenges come from, and the circuit has to be carried into that field.

The development is written in Isabelle/HOL (Isabelle2025-2) on top of the sumcheck entry of the Archive of Formal Proofs, release afp-2026-08-05. It has six sessions with twenty theories, 11,112 lines and 418 named statements, and no theory contains sorry, oops, axiomatization or an oracle. The statements below are quoted from the signed release v1.1.0; the archived v1.1.1 changes the package license metadata and keeps the theory files. A clean build of the six sessions reproduces the check:

isabelle build -c -d /path/to/afp/thys -d formal/isabelle SESSION
From acceptance to a valid update Three arguments and one field change lead from an accepted run to a valid update; each step is checked in Isabelle/HOL, proved on paper or assumed.
From an accepted run to a valid update, step by step Inside a dashed boundary named interactive public-coin protocol, four argument boxes stand in a column. Protocol soundness: chain bound, checked in Isabelle/HOL; bound for the verifier, proved on paper. Small-field instance: chain bound with field size p to the fourth, checked in Isabelle/HOL; one layer lifted from the base field, checked in Isabelle/HOL; whole chain lifted, proved on paper. Exact arithmetization: encoded witnesses sound and complete, checked in Isabelle/HOL; inputs sent by the prover, proved on paper. Leaf binding: injective leaf encoding and the reduction of leaf collisions to sponge collisions, checked in Isabelle/HOL; two leaves at one key give a collision, proved on paper; position binding, an assumption. The first three join into Composition: no valid witness over one field, checked in Isabelle/HOL, an existential form that is not per witness; per witness over the base field and the quartic extension, proved on paper; per input vector in the delegation setting, proved on paper. The per-witness composition, which carries security, and leaf binding lead to what an accepted update certifies: its leaves are authenticated to the roots with error at most the bound, and one leaf per key and root under position binding, both proved on paper. Outside the boundary: the Fiat-Shamir transform, the Poseidon2 sub-circuits (abstract in the model) and the commitment to the input; and the shipped Rust verifier, which holds the witness and builds the input, replaces no hash work and claims no succinctness. A crossed-out dashed path shows that no result reaches its code. Interactive public-coin protocol Protocol soundness chain bound bound for the verifier Small-field instance chain bound with |F| = p4 one layer lifted from Fp whole chain lifted Exact arithmetization encoded witnesses: sound, complete inputs sent by the prover Leaf binding injective leaf encoding leaf collisions to sponge collisions two leaves at one key: a collision position bindingassumption Composition no valid witness, one field existential form, not per witness per witness, Fp and Fp4 per input vector (delegation) An accepted update certifies leaves authenticated to the roots, error ≤ the bound one leaf per key and root under position binding per witness carries security Outside the analysis Fiat-Shamir transform (non-interactive) Poseidon2 sub-circuits (abstract in the model) Commitment to the input Shipped Rust verifier holds the witness, builds the input no hash work replaced, no succinctness no result reaches the code
Interactive public-coin protocol
Protocol soundness
Checked in Isabelle/HOL: chain boundProved on paper: bound for the verifier
Small-field instance
Checked in Isabelle/HOL: chain bound with |F| = p4Checked in Isabelle/HOL: one layer lifted from FpProved on paper: whole chain lifted
Exact arithmetization
Checked in Isabelle/HOL: encoded witnesses: sound, completeProved on paper: inputs sent by the prover
joined in
Composition
Checked in Isabelle/HOL: no valid witness, one field
existential form, not per witness
Proved on paper: per witness, Fp and Fp4Proved on paper: per input vector (delegation)
per witnesscarries security
An accepted update certifies
Proved on paper: leaves authenticated to the roots, error ≤ the boundProved on paper: one leaf per key and root, under position binding
binds the leaves
Leaf binding
Checked in Isabelle/HOL: injective leaf encodingChecked in Isabelle/HOL: leaf collisions to sponge collisionsProved on paper: two leaves at one key: a collision
position bindingassumption
Blocked: no result reaches the code
Outside the analysisShipped Rust verifierholds the witness, builds the input · no hash work replaced, no succinctnessFiat-Shamir transform (non-interactive)Poseidon2 sub-circuits (abstract in the model)Commitment to the input
checked in Isabelle/HOL proved on paper assumption
Figure 1What an accepted run certifies, and what each step rests on

GKR Soundness with a Cube Gate

Interactive proofs in the GKR family [2] reduce a claim about the output of a layered arithmetic circuit, one sumcheck per layer, to a claim about the next layer, until they reach the input. Our circuits use linear, product and cube gates, and the cube gate serves the \(x^3\) S-box of Poseidon2. If the circuit has \(2^{s_{\mathrm{out}}}\) outputs and the sumcheck of layer \(i\) runs over \(2s_i\) variables with round polynomials of degree at most \(d_i\), a false output claim survives the layer chain with probability at most

$$\frac{s_{\mathrm{out}} + \sum_i \left(2 s_i d_i + 1\right)}{|\mathbb{F}|}.$$

The Isabelle statement of this GKR soundness bound reads:

theorem gkr_assembly_soundness:
  fixes P :: "'a layer ⇒ nat ⇒ ('a list × 'a) list ⇒ 'a list ⇒ 'p"
    and A :: "nat ⇒ 'a list ⇒ ('p, 'a, 'a, nat, 's) prover × 's × 'a × 'a × 'a"
    and outs :: "nat ⇒ 'a"
    and dbnd :: "nat ⇒ nat"
  assumes wf: "gkr_chain_wf (s0 # ss) (L0 # Ls) (b0 # bs)"
    and repr: "⋀L s claims b. layer_poly_repr (P L s claims b) L s claims b (dbnd s)"
    and outs_ne: "∃idx < 2 ^ layer_width_bits L0. outs idx ≠ layer_eval L0 b0 ! idx"
  shows "measure_pmf.prob
           (pmf_of_set (tuples (UNIV :: 'a set)
              (layer_width_bits L0 + chain_rlen (s0 # ss))))
           {rs. gkr_chain_bad P (λj pfx. A j (take (layer_width_bits L0) rs @ pfx))
                  (s0 # ss) (L0 # Ls) (b0 # bs)
                  [(take (layer_width_bits L0) rs, 1)]
                  (mle (layer_width_bits L0) outs (take (layer_width_bits L0) rs)
                   - const_mle L0 (take (layer_width_bits L0) rs))
                  (drop (layer_width_bits L0) rs)}
       ≤ (real (layer_width_bits L0)
           + (∑s←s0 # ss. real (2 * s) * real (dbnd s) + 1)) / real CARD('a)"

Over a finite field 'a, suppose the layer chain L0 # Ls is well formed (wf: widths and wiring fit), the polynomial P used at each layer represents that layer's sumcheck instance (repr, defined below), and the claimed outputs outs differ from the real outputs in at least one position (outs_ne). Then, when the output seed and every chain challenge are drawn uniformly, whatever strategy the prover A follows, the probability of the bad event gkr_chain_bad, in which the false claim survives every round check to the end of the chain, is at most the length of the output seed plus \(\sum_s \bigl(2s \cdot \mathit{dbnd}(s) + 1\bigr)\), divided by \(|\mathbb{F}|\).

The theorem lives in the locale gkr_layer_sumcheck, whose only assumptions are those of the multivariate-polynomial interface (variables, degree, evaluation, substitution) of the Isabelle sumcheck development [3]. That development is our per-round foundation, and its authors named the analysis of protocols such as GKR, which rely directly on sumcheck, as future work. This bound takes up that analysis.

From the Chain Bound to the Verifier's Polynomial

At layer \(i\), the claim equals the sum of the layer integrand over the Boolean cube \(\{0,1\}^{2s}\). Sumcheck reduces that sum to a single value at a random point \((\xi, \eta)\), and after the last round the verifier computes that value with its own formula and compares. The machine-checked chain bound does not ask for the integrand itself. It accepts any representative that meets this definition:

definition layer_poly_repr ::
  "'p ⇒ 'a layer ⇒ nat ⇒ ('a list × 'a) list ⇒ 'a list ⇒ nat ⇒ bool" where
  "layer_poly_repr p L s claims below dbnd ⟷
     vars p ⊆ set (upt 0 (2 * s)) ∧ deg p ≤ dbnd ∧
     (∀x<2^s. ∀y<2^s. eval p (idx_subst s x y) = layer_integrand L s claims below x y)"

A polynomial p represents layer L when its variables lie among the first \(2s\), its degree (total degree, in this interface) is at most dbnd, and it agrees with the layer integrand at every point of the cube. Agreement on the cube is enough for the sum, since the sumcheck sum ranges over Boolean substitutions and the round machinery never inspects non-Boolean values of p.

The Isabelle development instantiates the bound with \(\mathrm{ML}(I)\), the multilinear interpolation of the integrand. Its total degree is at most \(2s\), so \(\mathit{dbnd} = 2s\) and each layer contributes \(4s_i^2 + 1\) to the numerator.

The verifier's final check, however, does not evaluate \(\mathrm{ML}(I)\). It evaluates the integrand polynomial \(\hat P\), the natural extension of the integrand built from the multilinear extensions of the wiring predicates and of the next layer's values, at \((\xi, \eta)\). Its degree is at most 4 in each variable of the first block, at most 2 in each variable of the second, and at most \(5s\) in total. The two polynomials agree on the cube and in general differ at the random point, and when they differ they coincide there with probability at most \(5s/|\mathbb{F}|\). The mechanized bound, instantiated with \(\mathrm{ML}(I)\), therefore does not by itself bound the verifier's acceptance.

Two polynomials, one cube The mechanized chain bound uses ML(I), but the verifier checks P̂  at a random point where the two part, so its bound is proved on paper.
The representative and the integrand on the cube and at the random point A schematic slice along one variable X sub j, with the other variables on the Boolean cube. The multilinear representative ML(I), degree at most 1 in X sub j, is a straight line; the integrand polynomial P-hat, degree at most 4 in X sub j, is a curve. Both pass through the same values at the cube points 0 and 1. At a random coordinate xi sub j drawn from the field, the two values differ; when the polynomials differ, they agree at a random point (xi, eta) with probability at most 5s over the field size. Below, ML(I), the multilinear representative with degree at most 1 in each variable and total degree at most 2s, instantiates the chain bound checked in Isabelle/HOL, with per-layer term 4 s sub i squared plus 1, which holds for events about ML(I). That chain bound does not bound the verifier's acceptance. P-hat, the integrand polynomial with degree at most 4 in each X sub j, at most 2 in each Y sub j and total degree at most 5s, goes through the verifier's checks: degree of g sub t at most 4 in every round, then P-hat at (xi, eta) from the carried values. That gives the bound for the verifier, proved on paper: s out plus the sum over layers of 8 s sub i plus 1, over the field size; per layer 8 s sub i from the sumcheck and 1 from the carry, and s out from the output seed. 0 1 cube points ξj, random in F differ slice along Xj, the others on the cube schematic at a random point (ξ, η), when the two differ Pr[ ML(I) = P̂ ] ≤ 5s / |F| P̂: degree ≤ 4 in Xj ML(I): degree ≤ 1 in Xj ML(I) multilinear representative degree ≤ 1 in each variable total degree ≤ 2s P̂ integrand polynomial degree ≤ 4 in each Xj, ≤ 2 in each Yj total degree ≤ 5s Checked in Isabelle/HOL Chain bound per layer 4si2 + 1 holds for events about ML(I) Proved on paper Bound for the verifier (sout + Σi (8si + 1)) / |F| per layer: 8si sumcheck + 1 carry output seed: sout instantiates verifier's checks deg gt ≤ 4 in every round then P̂(ξ, η) from carried values does not boundacceptance The representative and the integrand on the cube and at the random point A schematic slice along one variable X sub j, with the other variables on the Boolean cube. The multilinear representative ML(I), degree at most 1 in X sub j, is a straight line; the integrand polynomial P-hat, degree at most 4 in X sub j, is a curve. Both pass through the same values at the cube points 0 and 1. At a random coordinate xi sub j drawn from the field, the two values differ; when the polynomials differ, they agree at a random point (xi, eta) with probability at most 5s over the field size. Below, ML(I), the multilinear representative with degree at most 1 in each variable and total degree at most 2s, instantiates the chain bound checked in Isabelle/HOL, with per-layer term 4 s sub i squared plus 1, which holds for events about ML(I). That chain bound does not bound the verifier's acceptance. P-hat, the integrand polynomial with degree at most 4 in each X sub j, at most 2 in each Y sub j and total degree at most 5s, goes through the verifier's checks: degree of g sub t at most 4 in every round, then P-hat at (xi, eta) from the carried values. That gives the bound for the verifier, proved on paper: s out plus the sum over layers of 8 s sub i plus 1, over the field size; per layer 8 s sub i from the sumcheck and 1 from the carry, and s out from the output seed. 0 1 cube points ξj, random in F slice along Xj, schematic P̂: degree ≤ 4 in Xj ML(I): degree ≤ 1 in Xj at a random point (ξ, η), when the two differ Pr[ ML(I) = P̂ ] ≤ 5s / |F| ML(I) multilinear representative degree ≤ 1 in each variable total degree ≤ 2s P̂ integrand polynomial degree ≤ 4 in each Xj, ≤ 2 in each Yj total degree ≤ 5s Checked in Isabelle/HOL Chain bound per layer 4si2 + 1 holds for events about ML(I) Proved on paper Bound for the verifier (sout + Σi (8si + 1)) / |F| per layer: 8si sumcheck + 1 carry output seed: sout verifier's checks deg gt ≤ 4 in every round then P̂(ξ, η) from carried values does not boundacceptance instantiates
Figure 2The representative and the integrand agree on the cube and part at the verifier's point

The paper closes this gap with two paper proofs. First, if the verifier accepts, the bad event of the chain occurs for \(\hat P\), because the round checks of the verifier receive round polynomials of \(\hat P\) of degree at most 4 per variable. Second, the same chain argument applied to \(\hat P\) gives \(8s_i/|\mathbb{F}| + 1/|\mathbb{F}|\) per layer (\(2s_i\) rounds of degree 4) and \(s_{\mathrm{out}}/|\mathbb{F}|\) for the output seed. The bound for the verifier is

$$\varepsilon = \frac{s_{\mathrm{out}} + \sum_i \left(8 s_i + 1\right)}{|\mathbb{F}|},$$

the same shape as the mechanized bound, applied to the verifier by a paper step.

Carrying the Bound into the Quartic Extension

StateSync-GKR evaluates its circuits over the 31-bit KoalaBear prime \(p = 2^{31} - 2^{24} + 1 = 2{,}130{,}706{,}433\). Over that field alone the bound is of little use. With 1,024 layers of \(2^{32}\) wires each (\(s_i = 32\)), the numerator is about \(2^{18}\) and the denominator about \(2^{31}\), which leaves roughly \(2^{-13}\). The challenges therefore come from the quartic extension \(\mathbb{F}_p[X]/(X^4 - 3)\). Here "quartic" is the degree of the field extension, a different four from the degree bound of the round polynomials in the previous section.

The Isabelle development builds the extension as a tower of two quadratic extensions, proves that it is a field with exactly \(p^4\) elements, and instantiates the chain bound over it:

lemma gkr_layer_sumcheck_mpoly_ext4:
  "gkr_layer_sumcheck
     (vars :: koala_bear_ext4 mpoly ⇒ nat set) total_degree
     (λp σ. insertion (the ∘ σ) p) inst"

lemmas gkr_assembly_soundness_ext4 =
  gkr_layer_sumcheck.gkr_assembly_soundness[
    OF gkr_layer_sumcheck_mpoly_ext4]

lemma ext4_denominator_exact:
  "real CARD(koala_bear_ext4) = real (2130706433 ^ 4)"

The first lemma shows that multivariate polynomials with coefficients in the extension satisfy every assumption of the locale above. The chain bound then holds over the extension as stated (gkr_assembly_soundness_ext4), with the exact denominator \(2130706433^4\) (ext4_denominator_exact) in place of an estimate.

The circuit also has to move into the extension. The embedding of the base field preserves layer evaluation, well-formedness and false outputs one layer at a time, and that per-layer lifting is machine-checked; lifting a whole chain and composing across the two fields are paper proofs. In the same way, the fact that four uniform base-field coordinates give one uniform extension challenge is machine-checked, while its extension to several independent challenges is a paper step.

Since \(\log_2 p^4 > 123.95\), the GKR soundness bound is small at practical sizes. For at most \(2^{10}\) layers with \(s_i \le 32\) and \(s_{\mathrm{out}} \le 2^{10}\), as for circuits whose layers have at most \(2^{32}\) wires, the numerator is below \(2^{18.02}\) and the bound is below \(2^{-105}\).

The circuits of our constraint-level model give every entry its own width bit, so they are wider. At the default parameters (tree depth \(d = 24\), leaf encodings of at most \(m = 31\) elements, digests of \(W = 8\) elements), the input and the output of the hash stack have fewer than \(2^{10}\) width bits, and for at most \(2^{10}\) layers the numerator is below \(2^{23.01}\) and the bound stays below \(2^{-100}\). All of these figures concern the interactive protocol over the extension.

Size of the bound At 1,024 layers the 31-bit field alone leaves a bound near 2−13; challenges from the quartic extension bring it to 2−105.9 and 2−101.0.
The bound against the number of layers, base field and quartic extension A chart of the soundness bound on a base-2 log scale, from 2 to the 0 down to 2 to the minus 140, against the number of layers n from 1 to 4,096 on a log scale. Three curves. Over the 31-bit base field, field size p, with s_i = s_out = 32, the bound is log2(32 + 257n) minus 30.99 and stays near the top: 2 to the minus 13.0 at 1,024 layers. Over the quartic extension, field size p to the fourth, the same numerator gives a bound 93 bits lower (a factor p to the minus 3): log2(32 + 257n) minus 123.95, which is 2 to the minus 105.9 at 1,024 layers, for layers of at most 2 to the 32 wires. For the update circuit over the quartic extension, s_out = 448 and every s_i = 1023: log2(448 + 8185n) minus 123.95, which is 2 to the minus 101.0 at 1,024 layers. A dashed reference line marks 1,024 layers. 20 2−20 2−40 2−60 2−80 2−100 2−120 2−140 1 4 16 64 256 1,024 4,096 Upper bound, log scale Layers in the circuit, n (log scale) 1,024 layers 2−13.0 2−101.0 2−105.9 same numerator, |F| from p to p4 bound × p−3 ≈ 2−93 31-bit base field, |F| = p update circuit, |F| = p4 quartic extension, |F| = p4 The bound against the number of layers, base field and quartic extension A chart of the soundness bound on a base-2 log scale, from 2 to the 0 down to 2 to the minus 140, against the number of layers n from 1 to 4,096 on a log scale. Three curves. Over the 31-bit base field, field size p, with s_i = s_out = 32, the bound is log2(32 + 257n) minus 30.99 and stays near the top: 2 to the minus 13.0 at 1,024 layers. Over the quartic extension, field size p to the fourth, the same numerator gives a bound 93 bits lower (a factor p to the minus 3): log2(32 + 257n) minus 123.95, which is 2 to the minus 105.9 at 1,024 layers, for layers of at most 2 to the 32 wires. For the update circuit over the quartic extension, s_out = 448 and every s_i = 1023: log2(448 + 8185n) minus 123.95, which is 2 to the minus 101.0 at 1,024 layers. A dashed reference line marks 1,024 layers. 20 2−40 2−80 2−120 1 16 256 4,096 Upper bound, log scale Layers n, log scale 1,024 layers 2−13.0 2−101.0 2−105.9 same numerator bound × p−3 ≈ 2−93 31-bit base field, |F| = p update circuit quartic extension, |F| = p4
Bound (sout + Σi (8si + 1)) / |F| for the interactive public-coin protocol · an upper bound, not an estimate of attack success · not the level after Fiat-Shamir Base field and quartic extension curves: si = sout = 32 (layers of at most 232 wires) · update circuit: sout = 448, every si = 1023 Below 2−105 for at most 210 layers with si ≤ 32 and sout ≤ 210 · below 2−100 for the model circuits at d = 24, m = 31, W = 8 with at most 210 layers and si, sout < 210
Figure 3The bound over the 31-bit field and over its quartic extension, by number of layers

Exact Arithmetization of Sparse Merkle Checks

Start with the semantics. A key is a number \(k < 2^d\), read as its \(d\) bits. A leaf is in one of three states: Empty (never populated), Occ(v) (populated with payload \(v\)) or Tomb (populated, then retired), encoded as \((0)\), \((1) \,\|\, \mathrm{penc}(v)\) and \((2)\).

The leaf hash folds that encoding into a sponge input (a tag lane, a length lane, the entries, then zeros), and an authentication path computes the root through an accumulator chain that follows the bits of the key. Validity of a membership \(\mathrm{Mem}(k, v)\), a non-membership \(\mathrm{Non}(k)\) and an update \(\mathrm{Upd}(k, \ell_o, \ell_n)\) is defined with one sibling list. For an update, the same siblings give the old root with the old leaf and the new root with the new leaf.

The constraint-level model of our compiler emits six kinds of check: C1 the leaf hash, C2 the accumulator chain through a multiplexer, C3 the root, C4 and C4′ the value digest, C5 the key bits \(\beta(\beta - 1) = 0\), and C6 the leaf tag \(x_0(x_0 - 2) = 0\). The hash sub-circuits stay abstract functions. The mechanized arithmetization theorem is a pair:

theorem theorem_A_soundness:
  assumes acc: "verifier_accept op root root' vd w"
  shows "smt_valid op root root' (canon_witness op w)"

theorem theorem_A_completeness:
  assumes valid: "smt_valid op root root' w"
  shows "verifier_accept op root root' (wit_vd op w) w"

If the verifier model accepts, meaning the public checks on the claim and the witness echo hold and the compiled checks pass on the encoding of the witness, then the canonical form of the witness makes the transition valid. Conversely, every valid witness is accepted together with its canonical value digest. Both theorems sit inside the following two locales, and their assumptions are everything the result depends on:

locale compiler_model_base = smt_semantics params h_leaf h_node
  for params :: smt_params
  and h_leaf :: "'v leaf_state ⇒ 'd"
  and h_node :: "'d ⇒ 'd ⇒ 'd" +
  fixes W :: nat and L :: nat
    and digest_repr :: "'d ⇒ 'f::idom list"
    and leaf_repr :: "'v leaf_state ⇒ 'f list"
    and hl :: "'f list ⇒ 'f list"
    and hn :: "'f list ⇒ 'f list ⇒ 'f list"
  assumes L_pos: "0 < L"
    and digest_len [simp]: "⋀x. length (digest_repr x) = W"
    and digest_inj: "⋀x y. digest_repr x = digest_repr y ⟹ x = y"
    and leaf_len [simp]: "⋀lf. length (leaf_repr lf) = L"
    and leaf_tag: "⋀lf. leaf_repr lf ! 0 = leaf_tag_val lf"
    and hl_len [simp]: "⋀xs. length (hl xs) = W"
    and hn_len [simp]: "⋀a b. length (hn a b) = W"
    and hl_correct: "⋀lf. hl (leaf_repr lf) = digest_repr (h_leaf lf)"
    and hn_correct: "⋀a b. hn (digest_repr a) (digest_repr b) = digest_repr (h_node a b)"

locale compiler_model = compiler_model_base params h_leaf h_node W L digest_repr leaf_repr hl hn
  for params :: smt_params
  and h_leaf :: "'v leaf_state ⇒ 'd"
  and h_node :: "'d ⇒ 'd ⇒ 'd"
  and W L :: nat
  and digest_repr :: "'d ⇒ 'f::idom list"
  and leaf_repr :: "'v leaf_state ⇒ 'f list"
  and hl hn +
  fixes stack :: "op_kind ⇒ 'f layer list"
  assumes stack_spec_ro:
    "⋀k xs. k ≠ KUpdate ⟹ length xs = ivlen k ⟹
       foldr layer_eval (stack k) xs = ev_ro xs"
    and stack_spec_up:
    "⋀xs. length xs = ivlen KUpdate ⟹
       foldr layer_eval (stack KUpdate) xs = ev_up xs"

Taken one at a time, the assumptions say this. Digests are represented injectively as lists of \(W\) field elements (digest_len, digest_inj). A leaf representation has length \(L > 0\) and starts with the leaf tag (L_pos, leaf_len, leaf_tag). The hash sub-circuits hl and hn output \(W\) elements (hl_len, hn_len) and compute the leaf and node hashes exactly on representations (hl_correct, hn_correct). The layer stack computes the residual functions of read-only operations and of updates exactly (stack_spec_ro, stack_spec_up). That the hash sub-circuits implement Poseidon2 lies outside these assumptions and is not verified.

The characterization of acceptance itself is not restricted to honestly encoded inputs:

theorem A_i_ro:
  assumes k: "k ≠ KUpdate" and len: "length xs = ivlen k"
  shows "circuit_accept (compile k) xs ⟷ cons_ro k xs"

theorem A_i_up:
  assumes len: "length xs = ivlen KUpdate"
  shows "circuit_accept (compile KUpdate) xs ⟷ cons_up xs"

For every input vector xs of the right length, the compiled circuit accepts if and only if the constraint list holds. The paper proof for the delegation setting below builds on this characterization. A theorem inside a locale is an implication from the locale's assumptions, so every locale used here is interpreted by a concrete instance over the KoalaBear field, and the arithmetization and composition theorems are applied, for a tree of depth one with a linear hash pair, to inputs that meet their premises (instance_theorem_A_activation, instance_theorem_C_activation).

Per-Input GKR Soundness for Two Verifiers

The composition is machine-checked inside the locale statesync_gkr_v01, which combines the two locales above. We omit two comment lines of the original:

theorem theorem_C_composition:
  fixes P :: "'a layer ⇒ nat ⇒ ('a list × 'a) list ⇒ 'a list ⇒ 'p"
    and A :: "nat ⇒ 'a list ⇒ ('p, 'a, 'a, nat, 's) prover × 's × 'a × 'a × 'a"
    and w :: "'v leaf_state × 'd list"
    and root root' vd :: 'd
    and dbnd :: "nat ⇒ nat"
  assumes bels: "bels = tl (circuit_values (mk_res_layer (descs (kind_of op)) # stack (kind_of op))
                             (encode_witness op root root' vd w))"
    and wf: "gkr_chain_wf (s0 # ss) (mk_res_layer (descs (kind_of op)) # stack (kind_of op)) bels"
    and repr: "⋀Ly s claims b. layer_poly_repr (P Ly s claims b) Ly s claims b (dbnd s)"
    and pub: "pub_ok op root root' vd"
    and wlen: "length (snd w) = depth params"
    and echo: "echo_ok op w"
    and nosem: "¬ (∃w'. smt_valid op root root' w')"
  shows "measure_pmf.prob
           (pmf_of_set (tuples (UNIV :: 'a set)
              (length (descs (kind_of op)) + chain_rlen (s0 # ss))))
           {rs. gkr_chain_bad P (λj pfx. A j (take (length (descs (kind_of op))) rs @ pfx))
                  (s0 # ss) (mk_res_layer (descs (kind_of op)) # stack (kind_of op)) bels
                  [(take (length (descs (kind_of op))) rs, 1)]
                  (mle (length (descs (kind_of op))) (λ_. 0)
                     (take (length (descs (kind_of op))) rs)
                   - const_mle (mk_res_layer (descs (kind_of op)))
                       (take (length (descs (kind_of op))) rs))
                  (drop (length (descs (kind_of op))) rs)}
       ≤ (real (length (descs (kind_of op)))
           + (∑s←s0 # ss. real (2 * s) * real (dbnd s) + 1)) / real CARD('a)"

Suppose the layer values of the circuit, evaluated on the encoding of the witness w, form a well-formed chain (bels, wf), a representative exists (repr), the public checks, the path length and the witness echo hold (pub, wlen, echo), and no witness w' makes the transition valid (nosem). Then the claim that every output is zero is accepted with probability at most the chain bound. The last premise is existential. As noted above, a false claim over a compressing hash almost always has such a witness, so this form is the machine-checked backbone of the composition, and the statement that carries security is the per-witness one.

The paper proves the per-witness statement in two verifier settings. In the first, the verifier receives the witness, computes the circuit input from it before any challenge is drawn, and holds that input in the clear. For every witness whose canonical form does not make the transition valid, this verifier accepts with probability at most \(\varepsilon\), over the base field and over the extension. The verifier that ships with StateSync-GKR is of this kind. Such a verifier could check the authentication path by hashing it directly, so in this setting the protocol replaces no hash computation of the verifier, and no succinctness in the witness is claimed.

The second is the delegation setting of GKR. The verifier receives the circuit input from the prover, checks its public entries and computes no node hash, so the protocol checks the hash chains, and this is where GKR carries the hashing.

Every accepted input, honestly encoded or not, determines a valid witness under three conditions: a digest is represented by its own field elements, the node sub-circuit computes the compression function on every pair of inputs and, for updates, the leaf sub-circuit computes the leaf hash of the old leaf. Checks on public segments of the input bind the key bits, the roots, the value digest and, for updates, the pre-image of the old leaf. If the witness read from the prover's first message, sent before any challenge, is not valid, the verifier accepts with probability at most \(\varepsilon\).

That proof uses the chain constraint, and the chain constraint cannot be dropped. Without it, an input that puts the pre-image of Occ(v) in the leaf segment, the value digest in the first accumulator, the claimed root in every later accumulator and zeros in the sibling entries passes every other check, and a false membership claim is accepted with probability one. The check on the pre-image of the old leaf is needed for the same reason.

An accepted run therefore certifies, except with probability \(\varepsilon\), that the siblings of the witness form a valid authentication path for the leaf the claim determines and for the claimed roots.

Position Binding and One Leaf per Key

The remaining question is whether the root binds the leaf. The leaf side is machine-checked:

corollary encoded_state_collision_to_sponge_collision:
  fixes encp :: "'v ⇒ 'f list"
  assumes encp_bound: "⋀v. 1 + length (encp v) ≤ max_fields"
      and max_pos: "1 ≤ max_fields"
      and neq: "encode encp l1 ≠ encode encp l2"
      and collide: "h_leaf (encode encp l1) = h_leaf (encode encp l2)"
  shows "∃p1 p2. p1 ≠ p2 ∧ sponge p1 = sponge p2"

When payload encodings stay within the length bound (encp_bound, max_pos), two leaf states with different encodings and the same leaf hash yield two different sponge inputs with the same output; we omit the explanatory comment of the original. The reduction needs the length lane, because without it the encodings \((1, 7)\) and \((1, 7, 0)\) pad to the same sponge input. The leaf encoding fix described in our earlier post survives as this lemma.

The node side is a paper step plus an assumption. Two different leaves with valid paths at the same key under one root yield a collision of the leaf hash or of the node hash. The implemented node hash has cheap collisions, though (see the last correction below), so the paper defines position binding. An algorithm breaks it by giving two different leaves valid paths at the same key under one root, and its advantage is the probability that it does. For a fixed, unkeyed hash such an algorithm exists in principle, as for any compressing hash, so the assumption is read through an explicit reduction.

Position binding is the one cryptographic assumption of the paper, and it enters only the one-leaf corollary. The probability that two accepted runs for one key and root assert different leaves is at most \(2\varepsilon + \mathrm{Adv}^{\mathrm{pb}}(B)\), where \(\varepsilon\) is the single-run bound above and \(B\) simulates both runs and outputs the two asserted witnesses.

Coratger, Khovratovich, Mennink and Wagner [9] analyze Merkle trees with a truncated permutation as compression function and prove strong position binding in the ideal-permutation model. Their leaf hash starts with a public key block, which ours does not, and their model idealizes Poseidon2, so we cite their theorem as support and do not apply it. The single-run bounds use no cryptographic property of the hashes at all.

Four Corrections on the Way to the Proof

While we turned this proof into a paper, four claims in our earlier drafts turned out to be larger than what the code or the formalization supported. For each one, we give the reason it was larger and what remained after we stepped back, with stepped back meaning that the claim was narrowed to what is proved.

Writing these four down was the least comfortable part of the work. Each took back a sentence we had been glad to write, and one had already reached readers in a published figure. We keep them in full because the places where our own claims broke taught us more about checking a GKR verifier than the places where they held.

The Bound Was Stated for a Polynomial the Verifier Does Not Compute

Our earlier draft drew the verifier-level \(2^{-105}\) from a degree-four specialization of the chain bound, one that fixes dbnd to the constant 4, and that specialization holds only vacuously because no representative meets its premises. The four there is a degree bound and has nothing to do with the degree of the field extension. What remained machine-checked was the bound for the multilinear representative \(\mathrm{ML}(I)\), and \(\mathrm{ML}(I)\) agrees with the verifier's \(\hat P\) on the cube but in general not at the random point \((\xi, \eta)\) where the verifier checks the value.

Isabelle theory on a laptop, sticky note: agrees on the cube, not at (ξ, η); GKR soundness

A sticky note on the laptop: the representative agrees on the cube, not at (ξ, η)

The build was clean and the theorem was true, yet the polynomial inside the theorem was not the one the verifier computes. In hindsight, we had checked that the theorem holds and skipped the plainer question of which polynomial it is about. After we stepped back, the machine-checked bound still stands for the representative, and a paper proof establishes a bound of the same shape for the verifier. The figure stands, and its basis is now a paper proof.

The development contains two conditional theorems about the verifier that ships with the artifact. verifier_acceptance_implies_gkr_chain_bad and its corollary production_verifier_acceptance_refines_gkr_chain_bad state that the acceptance record of the shipped verifier satisfies the bad event of the model. Their premises, a per-layer bridge in the theorem and the relation rust_hol_value_trace_relation between Rust values and the model in the corollary, are not discharged.

With the multilinear representative, they fail on honest runs in general. The bridge asks the wiring reconstruction to match the value of the representative whenever the carried values are correct, while the verifier computes \(\hat P\) and the representative is \(\mathrm{ML}(I)\). The trust-chain figure in our earlier post used these theorems to attach the shipped verifier to the chain.

After we stepped back, no result reaches the shipped Rust verifier, and the two theorems stay in the development unused. Contracts checked with Creusot and Why3 relate parts of the Rust code to model clauses; that relation is partial, and nothing in this article depends on it.

This is the correction we regret most, because the figure that drew the link had already been published. The chain that replaces it is shorter, and every step on it is marked for what it is: machine-checked, proved on paper or assumed.

Encoded Inputs Satisfy the Chain Constraint by Construction

Our earlier draft said the compiled circuit was not under-constrained. The mechanized arithmetization theorem, however, concerns the input that the verifier model builds from the witness, and on such inputs the hash-chain residuals (C1, C2) and the bit residuals (C5) hold by construction. Its proof therefore uses only C3, C4 and C4′, C6 and the public checks, and the theorem stays true for a circuit without the chain constraint. "Not under-constrained" is a claim about arbitrary inputs a prover might choose, and the formalization covered honest encodings only. Every input we had tested was honestly encoded too, so nothing we ran could have shown us the gap.

After we stepped back, we state the mechanized theorem for encoded inputs, and a paper proof now covers inputs the prover chooses: in the delegation setting, every accepted input determines a valid witness. The characterization it rests on, acceptance for every input vector (A_i_ro, A_i_up), is machine-checked. Because that proof uses the chain constraint, the counterexample input above goes through once the constraint is removed.

The Node Hash Is a Truncated Permutation

The digests of the implementation are 8 field elements. The node hash \(h_{\mathrm{node}}(a, b)\) is the first half of the Poseidon2 permutation \(\mathsf{Perm}(a \,\|\, b)\), with no feed-forward, and the leaf hash is an overwrite sponge of rate 8. The permutation is public, so anyone can run it backwards. Pick a target node hash \(z\) and two different second halves \(u\) and \(u'\); then \(\mathsf{Perm}^{-1}(z \,\|\, u)\) and \(\mathsf{Perm}^{-1}(z \,\|\, u')\) are two different inputs with node hash \(z\), found with two inverse calls.

Handwritten note on a printed page: Perm⁻¹(z‖u), Perm⁻¹(z‖u′) → same node hash z; GKR soundness

A handwritten note on a printed page: two inverse calls give the same node hash

Such a collision does not give two authentication paths for one key, because a path must start at a leaf hash and its accumulators must connect to that start, and two paths for one key are exactly what a system must rule out.

Our earlier draft derived the binding of leaves by the root from collision resistance, which this hash does not have. Nothing about this was hidden: the permutation is public, and we had not run it backwards against our own node hash. The reduction (two leaves yield a collision) is still proved, but for this hash it is no security argument. After we stepped back, the property the system needs, position binding, became the one cryptographic assumption, and it enters only the one-leaf corollary.

Set side by side, the four corrections share a pattern. The objects a proof handled were never matched one by one against the objects that run, even though they went by the same names. Every mismatch also sat where the adversary or the randomness picks a value: the random point off the cube, the input the prover chooses, the inverse permutation anyone can call.

Honest runs and honest inputs never pass through those places, so a fully green test suite does not reveal the mismatch. The lesson is to match each proof object against its running counterpart, starting where the adversary and the randomness choose. We would make the same trade again: each correction left a smaller claim, and each smaller claim is one we can defend.

What Remains for a Verifier Without a Code-Level Proof

Our shipped Rust verifier is itself a verifier without a code-level proof, since no result in this article reaches its code. This section starts from it and lists, from our records only, what remains for any GKR verifier whose theorems do not reach the code. It does not follow that such a verifier is unsafe. What follows is a precise list of what has to be checked separately, and four threats head that list.

  • Missing constraints that honest inputs cannot reveal. Honestly built inputs satisfy the hash chain by construction, so tests and theorems that use such inputs pass even when the chain constraint is missing. Where the prover supplies the input, the same gap is a direct route to accepting a false transition. In the systematization of Chaliasos et al. [8], under-constrained circuits are the most prevalent vulnerability class within ZK circuits.
  • Security figures that rest on a formula the verifier does not compute. A bound from a correct theorem still does not bound the verifier's acceptance when the polynomial in the theorem differs from the verifier's.
  • Binding arguments that assume a property the hash lacks. A binding argument built on collision resistance does not stand for a node hash that is a truncated permutation.
  • Trust that stays on the code side. Mismatches between code and model remain, along with trust in the field arithmetic, the challenger and the Poseidon2 implementation of the underlying library, the Rust compiler and the operating system. The non-interactive transformation remains as well. The Fiat-Shamir transformation is outside our analysis, and it is delicate for GKR-based arguments: for every choice of the Fiat-Shamir hash, Khovratovich, Rothblum and Soukhanov construct a circuit, depending on that hash, for which the compiled argument accepts a false statement [10]. Whether the challenges the implementation derives from its transcript are uniform and independent, conditioned on earlier messages and on the input, is a property of its Fiat-Shamir construction and is not established here.

Even before a proof reaches the code, it gives a verifier three things.

  • An exact list of the checks a verifier must make. The theorem that the compiled checks accept exactly the valid transitions, together with the counterexample that goes through once the chain constraint is dropped, is a reference that implementations, tests and audits can compare against.
  • Targets for tests and audits. The places where these mismatches gathered (the random point off the cube, the input the prover chooses, collisions built with the inverse permutation) form a ready list of targets.
  • A basis for design decisions. At the same circuit size, the base field alone gives about \(2^{-13}\) and the quartic extension gives less than \(2^{-105}\), and that calculation is the reason the challenges come from the extension.

How This Relates to Other Machine-Checked GKR Work

The Isabelle sumcheck development [3] is the foundation of our per-round bound and, as noted above, left the analysis of GKR open. Lean developments covering GKR have since appeared. The complexitylib library [4] proves perfect completeness and soundness of the GKR protocol for layered circuits with addition and multiplication gates over an arbitrary finite field, composing round-by-round soundness of its stages, with error \(\bigl(w_{\mathrm{out}} + \sum_i 5 w_i\bigr)/|\mathbb{F}|\) for layers of \(2^{w_i}\) gates. Round-by-round soundness is stronger than the GKR soundness bounds we prove.

The Lean library of the GordieHowe proof system [5] machine-checks the security theorems of a GKR-based argument, from round-by-round knowledge soundness to the non-interactive argument. For ML-DSA-44 it proves the source program complete and round-by-round knowledge sound for the FIPS 204 verification relation and carries this to the non-interactive argument. Its applications do not take as hypotheses that each compiled circuit enforces the checks assigned to it; those facts are proved from certificates over the exported circuits, and the Lean kernel checks the certificates.

Longfellow [6] proves in Lean, for a model of its version-7 verifier, conditional extraction and false-statement soundness with error \((1 + N + t_A)/2^{116}\). Its chain runs from a trusted circuit through a padded layer-by-layer sumcheck, Ligero, Fiat-Shamir, a two-field MAC and a Merkle extraction reduction, and it is stronger than ours in reaching the non-interactive verifier and the commitment.

The leanerVM development [7] proves round-by-round knowledge soundness of the oracle protocol of leanVM, in which a grand-product GKR checks the table bus. At the time of writing, open pull requests add knowledge soundness of a Lean implementation of the non-interactive verifier in the random-oracle model. Once merged, that end-to-end statement is stronger than ours, for a virtual machine and with GKR in a different role.

Our part of this picture is the proof that the checks of the compiled circuit are exact. The GKR development of complexitylib does not include that step, the main chain of Longfellow replaces it with a trusted circuit, and the GordieHowe library machine-checks certificates for the fixed circuits of its applications. Our proof covers sparse Merkle circuits of every depth, in a constraint-level model where only the hash sub-circuits are abstract, and it stops at the interactive protocol. It also differs in its gate set, which includes the cube gate, and in carrying base-field circuits into the exact extension field from which a small-field prover draws its challenges.

Conclusion

A GKR verifier's acceptance is a statement about a circuit, and a system that acts on it needs a statement about an update. For sparse Merkle membership, non-membership and update, we have proved the route between the two: a GKR soundness bound with a cube gate, its instance over the exact quartic extension of a 31-bit field, the exactness of a verifier model that encodes the witness together with soundness for inputs supplied by the prover, and their composition into a per-input bound. Position binding then adds that accepted runs for one key and root assert one leaf.

Isabelle/HOL checks the chain bound, its extension-field instance, the arithmetization theorem and, over one field, the existential composition, and the remaining steps are proved on paper. The results do not depend on the workload. Another application inherits the composition by proving its own arithmetization theorem, and another challenge field needs a field construction and the lifting lemmas, with no second probabilistic proof.

The four corrections changed how we read our own theorems. We now read each one beside the objects that run, starting where an adversary or the randomness chooses.

The per-input bound reads the witness from the first message of the prover. An argument that sends only a commitment to the input needs a bound of the same form at the input it extracts. How tight can that bound be?

References

Subscribe

New research, by email.

  • One email when a new article is published
  • Confirm once, leave with one click
  • Privacy