[ethresear.ch] [Cryptography] GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs
jay-oraclizer
November 7
In October 2025, Vitalik’s GKR tutorial was my first encounter with GKR. Its central observation, that the protocol commits only to a circuit’s input and output and never to the layers in between, made GKR look like the natural tool for proving hash-heavy computation. A year later, that has led to what is, as far as we know, the first machine-checked soundness bound for GKR on general layered circuits, in Isabelle/HOL. The same work produced a soundness proof for sparse-Merkle updates built on that bound, a partial refinement that ties the model to the Rust code, and a sparse prover whose release 1.2 proves 2.41–2.71× faster with byte-identical proofs and unchanged Isabelle theories.
This post follows that work, StateSync-GKR, from the protocol and its field to the update a circuit encodes, the Rust code and the prover arithmetic. Two arXiv papers give the details: Soundness of the GKR Protocol for Sparse-Merkle Updates, with a Machine-Checked Core and StateSync-GKR: Design and Evaluation of a Reusable Sparse GKR Engine, whose appendix plots the measurements in 363 panels. All formal results are proved in the first paper, and Isabelle/HOL also checks the parts marked as machine-checked. The main results:
- The first machine-checked GKR soundness bound for general layered circuits, with a cube gate. For circuits with linear, product and cube gates, Isabelle/HOL checks the bound (s_out + Σᵢ(2sᵢ·db(sᵢ) + 1))/|𝔽| for the whole layer chain and any layer polynomial of total degree at most db(sᵢ), on top of the sumcheck formalization in the Archive of Formal Proofs (dates in Section 1). For the polynomial the verifier evaluates, a paper proof on the mechanized layer lemmas gives (s_out + Σᵢ(8sᵢ + 1))/|𝔽|. The development has 20 theories in six sessions, 11,112 lines and 418 named statements.
- Over the field the challenges come from. The quartic extension \mathbb{F}_p[X]/(X^4 - 3) of the 31-bit KoalaBear field is constructed in the implementation’s coordinates, and the chain bound holds over it with denominator exactly p⁴ ≈ 2¹²⁴; base-field layers carry over by machine-checked lemmas, and the paper completes the whole-chain lift and the cross-field composition.
- From the circuit to the update. In a constraint-level model of the compiler with abstract hash sub-circuits, a verifier that encodes the witness itself accepts exactly the valid sparse-Merkle transitions, and over one field the composition with the chain bound is machine-checked for claims that no witness makes valid. The per-input statement that carries security is proved on paper: with correct hash sub-circuits, any input that matches the claim’s public segments and zeroes every output determines a valid witness.
- Security without a collision-resistant node hash. The node hash, a truncated Poseidon2 permutation, is not collision resistant; that accepted runs for one key and root assert one leaf reduces instead to position binding of the tree, the one cryptographic assumption of these interactive statements, and a machine-checked lemma reduces leaf-hash collisions to sponge collisions.
- A partial refinement down to the Rust code. Creusot contracts with recorded Why3 and SMT proofs relate selected functions of the compiler, the sumcheck engine, the composition facade and the hash-gadget interface to the model, and a mechanized forward theorem derives the chain event from an accepted run and its concrete round checks under an explicit Rust/model value relation; discharging that relation for the compiled verifier is the open last link (Section 5).
- Prover memory and speed, with the Isabelle theories untouched. Libra-style sparse booking keeps peak process memory about 89× below a test-only dense reference at width 4,096, and derived wiring verifies the same proof 10.80–23.68× faster. The round arithmetic of release 1.2 raises proving throughput 2.41–2.71× with all 13,824 compared proof hashes unchanged, and at 1,000 requests per second on one 192-core VM, p99 latency to verified acceptance fell from 440 to 75 ms with a new serving path and to 34 ms with the new arithmetic.
- Reuse. Through a frontend, the sumcheck/GKR core proves any layered circuit of these gate kinds with the field and hash of the shipped entry points, and another application inherits the chain bound and the composition by proving its own arithmetization theorem (Section 7).
Figure 1: Measured gains, each against StateSync-GKR’s own baseline. (a) Peak process memory at width 4,096, sparse prover against a test-only dense reference in the same driver. (b) Under a 3 GiB cap the dense reference is killed at width 8,192, while the sparse prover reaches 65,536. (c) Prepared proving throughput at 192 workers and depth 24, releases 1.1 and 1.2 measured the same day. (d) p99 latency to verified acceptance, timed at the caller with the network included, at 1,000 requests per second on one 192-core VM (median of three 60-second runs).
1. From Sumcheck to GKR
GKR, after Goldwasser, Kalai and Rothblum, runs one sumcheck of Lund, Fortnow, Karloff and Nisan per layer of a layered arithmetic circuit and reduces a claim about the output layer, layer by layer, to a claim about the input, at a soundness cost of degree/|𝔽| per sumcheck round. Thaler made the prover time-optimal for regular wiring, and Libra made it linear-time for general circuits with a two-phase sumcheck. Hashing suits this structure: each round of a Poseidon2 permutation becomes a layer, many hashes run side by side in the same layers, and with a native cube gate for the x³ S-box one layer applies one round.
A system that acts on a verifier’s accept, for example by adopting a new Merkle root, needs a statement about the update the circuit encodes. That rests on three arguments: soundness of the protocol for the gate set and field in use, exactness of the arithmetization that turns the update into a circuit, and position binding of the tree that commits to the state. The second is where deployed proof systems fail most often: under-constrained circuits account for 95 of the 141 vulnerabilities in the systematization of SNARK bugs by Chaliasos et al.
Sumcheck has been formalized in Isabelle/HOL, and the authors’ paper names the analysis of protocols such as GKR as future work; ArkLib develops interactive oracle reductions in Lean 4. Our Isabelle/HOL development takes up that analysis. The first version of the formal paper went to arXiv on 4 October 2026 with, to our knowledge, the first public machine-checked soundness bound for GKR on general layered circuits. In the same days, leanerVM was proving knowledge soundness of a grand-product GKR, the special case of a fixed product tree, in a pull request opened on 2 October and merged on 5 October.
Lean developments covering GKR have appeared since: complexitylib proves perfect completeness and soundness of GKR with addition and multiplication gates; GordieHowe machine-checks a GKR-based argument for ML-DSA-44 from the source program to the non-interactive setting; Longfellow proves conditional extraction and false-statement soundness for a model of its non-interactive verifier; and since 6 November 2026 leanerVM’s main branch proves soundness for a Lean implementation of its non-interactive verifier in the random-oracle model. All four machine-check a bound on the verifier’s acceptance, and the last three reach the non-interactive argument and a committed input. Specific to this work are GKR in Isabelle/HOL, cube gates, the KoalaBear quartic extension in the implementation’s coordinates, an exactness theorem for sparse-Merkle updates of every depth, and a reduction to position binding for a node hash that is not collision resistant.
The second argument has to be proved for each family of circuits, as GordieHowe and leanerVM do for their programs; outside GKR, semaphore-mtb and Zolana have Lean proofs for fixed-depth Merkle circuits, and Coda and Picus consider arbitrary assignments to a circuit’s witness. Sections 2 and 3 settle the first argument for this gate set and field, and Section 4 proves the second for sparse-Merkle updates of every depth.
2. GKR Soundness and Its Layer Chain in Isabelle/HOL
The central machine-checked statement bounds the whole layer chain (gkr_assembly_soundness, Theorem B; this post keeps the development’s letters for its three main theorems). It holds against any prover strategy, with probabilities over the verifier’s uniform and independent public-coin challenges and the verifier holding the circuit input in the clear, as in GKR’s delegation setting. For any layer chain and any false output claim,
\Pr[\mathrm{Bad}_0] \le \frac{s_{\mathrm{out}} + \sum_i \big(2 s_i \cdot \mathrm{db}(s_i) + 1\big)}{|\mathbb{F}|}
where the circuit has 2^(s_out) outputs and layer i reads 2^(sᵢ) wires. The term s_out pays for the random seeding of the output claim, 2sᵢ·db(sᵢ) is the sumcheck bound for a polynomial that represents layer i with degree bound db(sᵢ), and the 1 pays for folding two evaluation points into one claim.
For comparison, the layer identity of the original protocol has addition and multiplication gates:
V_i(z) = \sum_{x,y \in \{0,1\}^{s}} \widetilde{\mathrm{add}}_i(z,x,y)\,\big(V_{i+1}(x) + V_{i+1}(y)\big) + \widetilde{\mathrm{mult}}_i(z,x,y)\,V_{i+1}(x)\,V_{i+1}(y)
The circuits here use weighted linear, product and cube gates, a constants vector per layer, and claims carried as weighted point lists (z_k, c_k), so the sumcheck of layer i runs over
P_i(x,y) = \sum_k c_k \Big[ \widetilde{\mathrm{lin}}(z_k,x)\, V_{i+1}(x)\, \beta(y) + \widetilde{\mathrm{mul}}(z_k,x,y)\, V_{i+1}(x)\, V_{i+1}(y) + \widetilde{\mathrm{pow3}}(z_k,x)\, V_{i+1}(x)^3\, \beta(y) \Big]
with the layer identity
\sum_{(x,y)\in\{0,1\}^{2s}} P_i(x,y) = \sum_k c_k \big( V_i(z_k) - \widetilde{\mathrm{const}}(z_k) \big)
Here Vᵢ is the multilinear extension of layer i’s values, the three wiring predicates and the constants vector are extended the same way, and β is the standard lifting that sums to 1 over the cube. The cube term lets one layer apply Poseidon2’s S-box without stacking two product layers, and it raises the degree of this polynomial to four in each variable of x (two in each variable of y).
Theorem B imports sumcheck soundness from the AFP entry, which bounds by n·d/|𝔽| the chance that an instance in n variables with abstract degree at most d accepts a false sum. The chain bound therefore asks for a representative of each layer: a polynomial in its 2sᵢ variables that agrees with the integrand on the Boolean hypercube and has degree at most db(sᵢ) in the entry’s measure. After a layer’s sumcheck the verifier holds claims about the next layer at two points (x*, y*) and carries them as the claim list [(x*, 1), (y*, r)] with a fresh challenge r, and the chain event recurses over the remaining layers:
\mathrm{Bad}_i = \mathrm{AFPAccept}_i \lor \big(\mathrm{carry}_i\ \text{false} \land \mathrm{Bad}_{i+1}\big)
Here AFPAcceptᵢ is the imported sumcheck’s acceptance event for layer i’s representative, and “carryᵢ false” means a carried evaluation disagrees with the next layer’s true polynomial. A false claim must make some layer’s sumcheck accept a false sum, be hidden by the random combination of the carried values, or reach the input layer, where the verifier rejects it. Theorem B bounds this event for every representative family that meets its premise.
Figure 2: One layer of the GKR reduction and the term each step adds to the bound of gkr_assembly_soundness. The dashed box is the verifier’s own bound, proved on paper by a separate induction.
Which representative is used decides what the theorem says about a verifier. The development discharges the premise with the multilinear interpolation of the layer integrand, of total degree at most 2s, so the theorem applies with db(s) = 2s and a per-layer term 4sᵢ² + 1. The verifier evaluates the Pᵢ above, which agrees with the interpolation on the hypercube and has degree up to four in each variable; its round check bounds that per-variable degree, while the imported round check uses the total degree. The formal paper therefore repeats the induction for Pᵢ and the verifier’s own round check, with the textbook sumcheck bound and the mechanized layer lemmas, and proves on paper
\Pr[\mathcal{V}\ \text{accepts a false output claim}] \le \frac{s_{\mathrm{out}} + \sum_i (8 s_i + 1)}{|\mathbb{F}|}
with 8sᵢ = 2sᵢ·4 for 2sᵢ rounds of degree at most 4, a degree unrelated to the quartic extension field of the next section.
3. Over the Field the Challenges Come From
A bound with denominator p ≈ 2³¹ says little, so small-field provers evaluate circuits over the base field and draw challenges from an extension. StateSync-GKR takes circuit values in KoalaBear, p = 2³¹ − 2²⁴ + 1, and challenges from its quartic extension \mathbb{F}_p[X]/(X^4 - 3). For the bound to speak about that prover, the extension has to exist as a field in the proof assistant, in the coordinates the implementation uses, and the base-field circuit and its false claim have to be carried into it.
The base field is the residues mod p, with primality proved by trial division up to ⌊√p⌋ = 46,159 and discharged by eval, and the extension is a tower of two quadratic extensions in the implementation’s coordinates:
\mathbb{F}_{p^2} = \mathbb{F}_p[\theta]/(\theta^2 - 3), \qquad \mathbb{F}_{p^4} = \mathbb{F}_{p^2}[\alpha]/(\alpha^2 - \theta) \cong \mathbb{F}_p[X]/(X^4 - 3), \qquad |\mathbb{F}_{p^4}| = p^4 \approx 2^{124}
The coordinate map (a₀, a₁, a₂, a₃) ↦ (a₀ + a₂θ) + (a₁ + a₃θ)α is proved bijective, kb_alpha_fourth proves α⁴ = 3, and ext4_denominator_exact proves the cardinality exactly p⁴ for p = 2,130,706,433. Each level is a field by a norm argument with nonsquare certificates, 3 by quadratic reciprocity and −3 from a square root of −1 modulo p checked by evaluation.
The base-field embedding is proved to commute with sums, products and multilinear extensions at base-field points and to preserve layer evaluation, well-formedness and a false output, layer by layer. Theorem B is proved once in a locale over an abstract field and polynomial type, so the extension-field statement (gkr_assembly_soundness_ext4) needed no second probabilistic proof: its locale obligations close by unfold_locales and one call of auto. Four independent uniform base-field coordinates push forward to a uniform extension element (uniform_coeff_tuple_pushforward), the form in which the implementation draws a challenge. On paper are the match with the implementation’s basis 1, X, X², X³, the isomorphism with \mathbb{F}_p[X]/(X^4 - 3), the step from one challenge to many independent ones, and the lift of a whole chain from the per-layer lemmas.
4. From the Circuit to the Update
4.1 Exact Arithmetization
A layer holds 2ˢ wires, a constants vector and a list of Lin, Mul and Pow3 gates. For a transition claim (op, r, r′), the compiler emits a circuit whose outputs are residuals that vanish exactly when a constraint holds: the leaf sponge chain and the compression chain up the authentication path, with key bits selecting sibling order through multiplexers; booleanity residuals b(b − 1); tag residuals such as tag(tag − 2), which force a non-membership leaf to be empty or retired; and boundary residuals that equate recomputed and claimed roots. Acceptance is a zero test on the output layer.
Theorem A relates acceptance to validity in both directions, on the input the verifier itself builds. Soundness (theorem_A_soundness) turns an accepting witness into a canonical valid one, completeness (theorem_A_completeness) shows that every valid transition is accepted, and together they give (theorem_A_compilation_soundness):
\big(\exists\, vd, w.\ \mathsf{accept}(op, r, r', vd, w)\big) \iff \big(\exists w.\ \mathsf{valid}(op, r, r', w)\big)
The verifier model checks the claim’s public parts, encodes the witness as the circuit input and evaluates the compiled checks; on such inputs the hash-chain and booleanity residuals hold by construction, so the theorem rests on the boundary and tag residuals and the public checks. The shipped verifier also rebuilds the input from the witness, and no succinctness in the witness is claimed.
The constraints carry their full weight when the verifier instead receives the input vector from the prover, compares its public segments (key bits, roots, value digest and, for an update, the old leaf’s pre-image) with the claim, and computes no node hash. Then every input that passes these comparisons and zeroes all outputs of the compiled circuit determines a valid witness, assuming that digests are represented by their own field elements and that the hash sub-circuits compute the hash functions on every input. This is proved on paper from a machine-checked characterization of the constraints (A_i_ro, A_i_up: for every input vector of the right length, the circuit accepts exactly when the constraints hold).
4.2 Leaf Binding, and the Defect Behind It
Leaves have three states, empty, occupied and retired, so that a retired slot stays distinguishable from one never used, and a leaf is hashed by a rate-8 sponge over the explicit encoding [tag, len, payload, 0-padding]. That encoding became a lemma after a defect found before the first public release. When an algebraic placeholder hash, documented as having no collision resistance, was replaced with Poseidon2, an internal adversarial review found that folding variable-length leaf records into fixed-width hash input was not injective: two different leaves could reach the same hash input without any break of the hash, and a forged membership proof passed both checking paths. The placeholder’s own caveat had hidden the defect. The fix lays a leaf out losslessly, at a real cost in permutations and proof size, and leaf_fold_inj proves the encoding injective for in-bound lengths, so a leaf-hash collision on distinct encodings yields a sponge collision (h_leaf_collision_to_sponge_collision) with no assumption about the sponge.
4.3 Composition, and the Statement That Carries Security
Theorem C (theorem_C_composition) composes A and B in one locale that identifies the circuit’s field with the challenge field. If the public-side checks pass and no witness makes the claim valid, the chain event of the compiled circuit with the all-zero output claim satisfies
\big(\nexists w.\ \mathsf{valid}(op, r, r', w)\big) \;\Longrightarrow\; \Pr\big[\mathrm{Bad}_0\big] \le \frac{r_{\mathrm{out}} + \sum_i \big(2 s_i \cdot \mathrm{db}(s_i) + 1\big)}{|\mathbb{F}|}
where r_out, the number of residuals (240 to 584; the model gives each its own bit, which overstates this term), takes the place of s_out, and the witness is fixed before the challenges.
For a compressing hash the premise “no witness makes it valid” is strong: a sibling list has far more free field elements than a root, so, heuristically, if the node hash behaves like a random function, most roots are reached from a given leaf by some sibling list and a false claim has a valid witness. The statement that carries security therefore fixes the input. Let x be an input fixed before the challenges, either encoded by the verifier from a witness or received from the prover and checked on its public segments, and let wit(x) be the witness it asserts. Then for every prover strategy
\neg\,\mathsf{valid}\big(op, r, r', \mathrm{wit}(x)\big) \;\Longrightarrow\; \Pr[\mathcal{V}\ \text{accepts}] \le \frac{r_{\mathrm{out}} + \sum_i (8 s_i + 1)}{|\mathbb{F}|}
With p⁴ as the denominator the same holds over KoalaBear with challenges from its quartic extension, and in the constraint-level model at the default depth 24 the bound is below 2⁻¹⁰⁰. These per-input forms are paper proofs on the machine-checked parts: the contrapositive of the arithmetization theorem makes the all-zero claim false, and the verifier bound of Section 2 applies.
A system also relies on accepted runs for one key and root asserting one leaf, and here the hash assumption enters. The node hash is the first half of a Poseidon2 permutation with no feed-forward, so two calls to the inverse permutation give a collision, yet a collision does not give two authentication paths, because a path must start at a leaf hash and its accumulators must connect to that start. What a system needs is position binding of the tree: finding one key, one root and two different leaves with valid paths must be hard. With E the event that two accepted runs with independent challenges assert different leaves for one key and root, and ε the per-input bound, an explicit reduction gives
\Pr[E] \le 2\varepsilon + \mathsf{Adv}^{\mathrm{pb}}(\mathcal{B})
The verifier reads the asserted witness in the clear, so the reduction needs no extractor. Position binding is assumed, not proved, and enters only this bound. Coratger, Khovratovich, Mennink and Wagner prove strong position binding for Merkle trees with a truncated permutation in the ideal-permutation model, with a bound that reaches 1 at about 2¹²³ queries at these parameters; their leaf hash differs from ours and their model idealizes Poseidon2, so the paper cites this as support without applying it.
Figure 3: The status of each result. Machine-checked: Theorems A, B and C. Paper steps over mechanized parts (dashed): the verifier’s own bound, the per-input forms, prover-supplied inputs, the whole-chain lift and the cross-field composition. Position binding is an assumption and enters only the one-leaf bound. On the right, contracts relate code to model clauses (dotted), and the forward theorems carry the value relation that Section 5 calls the last link.
4.4 Nonvacuity as Part of Done
A theorem over a locale has content only if its assumptions can be satisfied, and the proof assistant checks the implication, never the satisfiability. When the model verification first looked finished, with a clean build and no proof left as sorry, requiring a registered concrete instance for every assumption set exposed a compiler-side set that nothing could satisfy: it forced two specification-vector lengths to be powers of two, while they provably satisfy ℓ_ro < ℓ_up < 2ℓ_ro, so both compiler-side headline theorems had been vacuously true. Every locale behind Sections 2 to 4 is now interpreted by a concrete instance over KoalaBear, and the arithmetization and composition theorems are applied, for a tree of depth one with a linear hash pair, to inputs that satisfy their premises (instance_theorem_A_activation, instance_theorem_C_activation). Witnessing the assumptions of every machine-checked theorem we use with a registered concrete instance is now part of what “done” means for this development.
5. A Partial Refinement Down to the Rust Code
A partial refinement connects the model to the implementation in three parts: contracts on the code, verifier bodies that the tool can read, and a forward acceptance theorem in Isabelle/HOL.
Creusot contracts, with recorded Why3 and SMT proofs, relate selected functions to model clauses in four families: the compiler crate to the acceptance definitions of Theorem A; the sumcheck engine and layer reduction to the chain of Theorem B, including the round-step law of the imported sumcheck protocol on the oracle interface; the composition facade to the merged model; and the hash-gadget interface to the model’s hash usage, as interface correspondence only. Recorded proofs also establish the exact public-input equality check and the acceptance classifier, the conjunction of seven named observations from public-input binding to the two final input evaluations. Production wiring-oracle evaluation, transcript operations and the observation helpers stay outside as trusted translation boundaries.
The sumcheck and per-layer verifier bodies are translated around a single foreign-field equality each, exposing round counting, degree checks, rejection paths, transcript order and carry construction to the tool; the records cover their verification conditions, while their stated postconditions are design contracts that the tool does not check. The current tree holds 335 replay records with 2,456 discharged and 182 open solver leaves, none open in the sumcheck records (leaf counts are not a coverage percentage). A source and evidence map names the code, the contract and the recorded evidence for request binding, round checks, carry construction and final input evaluations, and an integrator can reuse it to review a frontend.
The forward theorem production_verifier_acceptance_refines_gkr_chain_bad, a corollary of verifier_acceptance_implies_gkr_chain_bad, derives the chain event of Section 2 from an accepted run and model well-formedness; the per-layer bridge that the first theorem assumes is derived from the concrete round checks and the finish-evaluation part of the value relation rust_hol_value_trace_relation between Rust values and the model, so the acceptance argument can be inspected at the checks it depends on. That relation is the last link, and it is open: with the multilinear representative of Section 2 its finish part fails on honest runs in general, because the verifier compares its last round value with a different polynomial. As it stands the corollary does not apply to the shipped verifier, and the soundness statements of this post are statements about the model. Closing the link takes a mechanized chain bound for the verifier’s own polynomial and round check, the argument Section 2 proves on paper, and a value relation discharged for the compiled verifier body.
The development builds with Isabelle2025-2 against AFP release 2026-08-05; the results were obtained on release 1.1.0, and the theory files are unchanged through release 1.2.1. A hosted workflow rebuilds every session from clean targets on each push to the maintained branch, weekly and on pull requests that change a proof input, and a source check fails on any sorry, oops, axiomatization or oracle command. The two numeric facts discharged by eval in Section 3 also trust the code generator and the ML runtime.
6. Prover Memory and Speed, with the Theories Untouched
Theorem B and its extension-field instance quantify over every prover strategy, and the model contains no prover arithmetic, so a change confined to the prover cannot weaken them. Sparse booking, cube gates and derived wiring were already in release 1.1, on which the formal results were obtained; release 1.2 changes the prover’s arithmetic, adds serving components and keeps the verifier functions, the proof format and the transcript order. A prover change could still break completeness, determinism or the code the contracts describe, and the control for that is the byte comparison: every compared proof of release 1.2 is byte-identical to release 1.1, and the Creusot records of the changed functions were regenerated with no existing contract regressing. So no formal proof had to be redone.
6.1 Sparse Layer Reduction
For a layer with nᵢ input wires, nₒ output wires and m multiplication gates, a dense sumcheck oracle materializes factor tables over all input pairs and owns O(nₒ + nᵢ²) auxiliary memory. The production oracle follows Libra’s two-phase booking, in which multiplication supplies a sparse list of weighted input pairs, so it owns O(nₒ + nᵢ + m) and never builds the input-pair hypercube. The dense method stays in the code as a test-only reference, and differential tests require both oracles to produce the same round polynomials and proofs on every shared case. In the same driver, with field, transcript and circuit fixed, a two-layer mixed circuit of width 4,096 requested 579,584 bytes of additional memory during proving, against 1.88 GB for the dense oracle.
Figure 4: Peak process memory by layer width for the sparse prover and the test-only dense reference in the same driver (release 1.2; release 1.1 is within 0.6 MiB at every width). The sparse prover reaches 65,536 wires in 259.6 MiB.
6.2 Cube Gates and Parallel Path Constraints
Poseidon2 over KoalaBear has an x³ S-box, so the cube and the affine step after it become one round layer of Pow3 and linear taps. The compiler checks every compression on an authentication path against witness-supplied intermediate values as parallel residual constraints, so the number of layers follows the hash’s rounds and does not grow with the tree depth: all nine tested circuits, three operations at depths 24, 28 and 32, have 118 layers, and a membership proof grows from 176,948 bytes at depth 24 to 182,132 bytes at depth 32, about 2.93%. Width and total work still grow with depth.
6.3 Derived Wiring and the Lemma Behind It
Compilation is data-parallel, so each layer’s wiring decomposes into a few arithmetic-progression families plus a sparse residue, and the verifier can evaluate the wiring extension in closed form without iterating the gate list. A lemma in the Isabelle development (derived_mle_eq_table) states when, for well-formed families, the two forms are the same polynomial:
\biguplus_{j} \mathrm{expand}(F_j) \uplus R = G_i \;\Longrightarrow\; \widetilde{W}^{\mathrm{derived}}_i = \widetilde{W}^{\mathrm{table}}_i
At run time the derivation checks each family member’s progression, kind and coefficient and falls back to the exact sparse path on any mismatch, so a wrong layout hint from the compiler is designed to cost time without changing the evaluated polynomial. Against table wiring, itself sparse, derived wiring verified the same proof 10.80–23.68× faster across the nine profiles, the ratio growing with depth for every operation (release 1.1 measurements; release 1.2 changes neither the wiring evaluation nor the proofs).
6.4 Prepared Circuits, Deterministic Transcripts and Serving
Compilation, the commitment to the whole circuit and the derived wiring are the same for every request of one operation kind, so they are prepared once per kind and shared read-only. The commitment dominates: for depth-24 membership in release 1.2 it takes about 104 ms, against 7.8 ms for compilation and 16.4 ms for proving. The transcript absorbs a domain tag, the circuit shape and commitment, the public inputs, the claimed outputs, the round messages and the carried evaluations in a fixed order, so proof bytes depend on neither worker count nor scheduling. Requests run as independent jobs that are never aggregated, and theorem_D_batching_correctness states that a batch of independent jobs verifies exactly when every job verifies on its own.
In the serving path of release 1.2 the verifier checks each received proof against its original request, so a different root, value digest or circuit identifier, or trailing bytes, cause rejection. One connection carried 3,300 requests per second with every request accepted within one second; at 3,400 per second the replies reached the provider’s documented single-flow limit of about 5 Gbit/s.
6.5 The Round Arithmetic of Release 1.2
Release 1.2 keeps the two phases of the sparse oracle and reorganizes each sumcheck round with three standard identities (Figure 5a). The output-line weights c_k·eq(z_k, j) come from one scaled equality table per claim built by doubling, about 2·2ˢ multiplications in place of s·2ˢ. Every table factor is multilinear in the variable being bound, so its values at the round’s five nodes follow from f(0) and f(1) by repeated addition, in one pass over the table. A fixed inverse Vandermonde matrix, built once per layer, then recovers the round polynomial from the five values, removing the per-round inversions and small allocations of Lagrange interpolation.
Each change computes the same field elements by an algebraically equivalent route, and finite-field arithmetic is exact, so the proofs should be identical byte for byte, and they are: across 768 fixtures for each operation at depths 24, 28 and 32, in native and default builds, all 13,824 proof hashes match release 1.1, and the dense and sparse oracles still agree. On a 192-core bare-metal server at depth 24 with batches of 768, prepared proving went from 3,195.50, 2,947.08 and 2,102.02 proofs per second for membership, non-membership and update to 7,713.71, 7,220.36 and 5,390.07, between 2.41× and 2.71× across 1 to 192 workers against release 1.1 measured the same day. On the width-4,096 circuit of Section 6.1, allocation calls per proof fell from 1,282 to 85 with the same requested peak.
Figure 5: (a) The three changes to the sumcheck round arithmetic in release 1.2. (b) Prepared proving throughput at 192 workers, releases 1.1 and 1.2 measured the same day. (c) Allocation calls per proof.
6.6 Summary and Comparison Scope
Mechanism
Baseline
Result
Setting
Sparse layer reduction
test-only dense reference, same driver, field and transcript
3,242.41× less requested allocation; 88.87× lower process memory (89.46× in release 1.1)
two-layer mixed circuit, width 4,096
Sparse reduction under a 3 GiB cap
same
dense killed at width 8,192; sparse proves up to 65,536, the largest tested
same circuit family
Cube gates and parallel path constraints
structural
118 layers at depths 24 to 32; membership proof +2.93% from depth 24 to 32
nine profiles
Derived wiring
table wiring (itself sparse), same proof
10.80–23.68× faster prepared verification
nine profiles, depths 24 to 32
Prepared circuits
fresh preparation per request
7.19–10.13× shorter per-request proving path (3.46–4.45× in release 1.1)
one thread, depth 24
Parallel output handling
serial output handling
14.10–14.64× faster complete prepared local batch (9.71–10.71× in release 1.1)
depth 24, batch 768, 192 workers
Round arithmetic of release 1.2
release 1.1, same day
2.41–2.71× proving throughput; 1,282 → 85 allocation calls per proof; byte-identical proofs
depth 24, 1 to 192 workers; width 4,096
Serving path and prover of release 1.2
release 1.1, same day
p99 433.8–475.1 → 33.7–33.9 ms at 1,000 requests/s; 3,300 requests/s per connection within 1 s
one 192-core VM
Every ratio is an internal comparison with a named baseline and its own workload and timer, so the ratios should not be multiplied with one another or applied to a complete remote service, and same-condition comparisons with other proof systems and production GKR provers are outside this evaluation. The design and evaluation paper carries the full record in over 160 pages, with process repeats, failed attempts and refusals kept in their denominators.
7. Reuse
The engine implements the published GKR construction with Libra’s two-phase sparse sumcheck on Plonky3 primitives and adds no new protocol. Three parts carry over to another application:
- Core. The sumcheck and GKR crates prove and verify layered circuits of the three gate kinds without depending on the sparse-Merkle compiler. A frontend supplies the circuit, witness, output claim and transcript conventions, and must consume both residual input claims.
- Field and hash. The sumcheck crate, the circuit representation and the general model are generic over the field. The single adapter crate that names Plonky3 fixes the field and hash to KoalaBear, its quartic extension and Poseidon2 from Plonky3 v0.4.3; replacing them in the code is a new implementation and verification task.
- Proofs. Another application inherits the chain bound and the composition by proving its own arithmetization theorem in the form of Theorem A’s soundness and repeating the per-input argument on paper. Another challenge field needs a field construction and the lifting lemmas.
Use cases. Any computation written as a layered circuit of these gates runs on the core, and the sparse-Merkle frontend is its first workload: membership, absence and single-leaf updates against a published root, with three-state leaves that keep insertion, update, deletion and restoration distinct and sequentially assigned keys, so the default depth of 24 holds about 16.8 million records.
- AI and custom computation. Machine-learning arithmetic, data pipelines and other layered computations run on the core directly, through a frontend built for them; a guide walks through building one.
- Regulated assets. Proofs that a holder is on a register, that an address is absent from a restricted list, or that a holding changed correctly.
- Blockchains. Membership, absence and single-record updates for rollups, app-chains and synchronization layers that keep their state in the engine’s sparse Merkle tree.
- Data systems. A checkable answer, for a key-value store or registry, to whether a key is present, absent or updated, against a root the client already trusts.
8. Scope
All probabilistic statements concern the interactive public-coin protocol, with challenges drawn uniformly and independently from the field and the input fixed before the challenges, matching the imported sumcheck development. The Fiat–Shamir transformation that makes the running protocol non-interactive is outside the analysis (it is delicate for GKR-based arguments), and we make no claim about the non-interactive protocol. In the running protocol the transcript absorbs the public inputs and the circuit commitment but not the witness-derived input, so that input is not fixed before the challenges there; the independent review records this point and constructs no false acceptance from it. Not treated are a verifier that receives only a commitment to the input, verification of the Poseidon2 sub-circuits against the hash functions (the correspondence between compiled circuits and the model is carried by the contracts of Section 5), and an assembled completeness theorem for a full protocol run. Zero knowledge is not claimed for the inner GKR proof, and no extractor is constructed; hiding is left to an external zkVM wrapper, for which release 1.2.1 attaches, as component evidence, a RISC Zero proof of a fixed depth-24 membership relation checked on an external verification network’s testnet. Release 1.2.1 is source-available under BSL 1.1, which permits non-production research and reproduction; MIT or Apache-2.0 rights already granted for releases up to v1.1.0 remain valid.
9. Open Questions
- Closing the last link to the Rust verifier. Once the verifier’s own integrand and round check have a mechanized bound, should the value relation be discharged through the existing contracts or by validated translation of the specific verifier body?
- A verifier that commits to its input. The verifier here reads the input in the clear, and an argument that commits to the input needs a per-input bound at the input it extracts. Which commitment to the input layer keeps the arithmetization theorem and the composition intact?
- Binary fields. A recent comparison of standard hash candidates for Ethereum models proving costs on a system for binary circuits. Which parts of this chain carry over to GKR over binary towers for Keccak- or BLAKE-based trees? The probabilistic proof is stated over an abstract finite field, while the arithmetization and the cube-gate economics are tied to a prime-field hash.
Approaches to these questions, and corrections to any statement above, are welcome.
A year after that tutorial, the protocol it introduced me to has a soundness proof for these circuits with a machine-checked core, a partial refinement into the Rust code, and a sparse prover that became faster with the same proof bytes. StateSync-GKR was developed for one workload, state synchronization across domains, which is what its name refers to.
Acknowledgments. We thank Bernhard Müller for his independent review of the verifier’s challenge-generation assumptions and the implementation-facing interpretation of the extension-field soundness bound, which clarified the line between the mechanized results and the remaining arguments.
Artifacts
- Formal verification paper and design and evaluation paper
- Source, with REPRODUCING.md and FORMAL_VERIFICATION.md
- Release assets with an SBOM, a provenance attestation, a proof manifest and checksums; a source recipe is expected to reproduce the documented deterministic proof digest
- Engine site and documentation
- Design journey article
- Software DOIs: 10.5281/zenodo.23643505 (v1.2.0, the measured release) and 10.5281/zenodo.23655511 (v1.2.1, current)
Visit Topic to respond.
You are receiving this because you enabled mailing list mode.
ArkLib: Verified-zkEVM/ArkLib
leanerVM: Verified-zkEVM/leanerVM
complexitylib: cslib-community/complexitylib
GordieHowe: cmlsharp/gordiehowe
Longfellow: github.com/longfellow-zk/longfellow-zk/tree/main/…
semaphore-mtb: github.com/worldcoin/semaphore-mtb/tree/master/fo…
Zolana: github.com/helius-labs/zolana/tree/main/prover/se…
Creusot: creusot-rs/creusot
source and evidence map: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
Plonky3 v0.4.3: github.com/Plonky3/Plonky3/releases/tag/v0.4.3
independent review: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
Bernhard Müller: github.com/muellerberndt
Source: Oraclizer/statesync-gkr
REPRODUCING.md: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
FORMAL_VERIFICATION.md: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
source recipe: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
Mentions
[ethresear.ch] [Cryptography] GKR with a Machine-Checked Core, and a Sparse Prover Made Faster with Byte-Identical Proofs jay-oraclizer November 7 In October 2025, Vitalik’s GKR tutorial was my first encounter with GKR. Its central observation, that the protocol commits only to a circuit’s input and output and never to the layers in between, made GKR look like the natural tool for proving hash-heavy computation. A year later, that has led to what is, as far as we know, the first machine-checked soundness bound for GKR on general layered circuits, in Isabelle/HOL. The same work produced a soundness proof for sparse-Merkle updates built on that bound, a partial refinement that ties the model to the Rust code, and a sparse prover whose release 1.2 proves 2.41–2.71× faster with byte-identical proofs and unchanged Isabelle theories. This post follows that work, StateSync-GKR, from the protocol and its field to the update a circuit encodes, the Rust code and the prover arithmetic. Two arXiv papers give the details: Soundness of the GKR Protocol for Sparse-Merkle Updates, with a Machine-Checked Core and StateSync-GKR: Design and Evaluation of a Reusable Sparse GKR Engine, whose appendix plots the measurements in 363 panels. All formal results are proved in the first paper, and Isabelle/HOL also checks the parts marked as machine-checked. The main results: - The first machine-checked GKR soundness bound for general layered circuits, with a cube gate. For circuits with linear, product and cube gates, Isabelle/HOL checks the bound (s_out + Σᵢ(2sᵢ·db(sᵢ) + 1))/|𝔽| for the whole layer chain and any layer polynomial of total degree at most db(sᵢ), on top of the sumcheck formalization in the Archive of Formal Proofs (dates in Section 1). For the polynomial the verifier evaluates, a paper proof on the mechanized layer lemmas gives (s_out + Σᵢ(8sᵢ + 1))/|𝔽|. The development has 20 theories in six sessions, 11,112 lines and 418 named statements. - Over the field the challenges come from. The quartic extension \mathbb{F}_p[X]/(X^4 - 3) of the 31-bit KoalaBear field is constructed in the implementation’s coordinates, and the chain bound holds over it with denominator exactly p⁴ ≈ 2¹²⁴; base-field layers carry over by machine-checked lemmas, and the paper completes the whole-chain lift and the cross-field composition. - From the circuit to the update. In a constraint-level model of the compiler with abstract hash sub-circuits, a verifier that encodes the witness itself accepts exactly the valid sparse-Merkle transitions, and over one field the composition with the chain bound is machine-checked for claims that no witness makes valid. The per-input statement that carries security is proved on paper: with correct hash sub-circuits, any input that matches the claim’s public segments and zeroes every output determines a valid witness. - Security without a collision-resistant node hash. The node hash, a truncated Poseidon2 permutation, is not collision resistant; that accepted runs for one key and root assert one leaf reduces instead to position binding of the tree, the one cryptographic assumption of these interactive statements, and a machine-checked lemma reduces leaf-hash collisions to sponge collisions. - A partial refinement down to the Rust code. Creusot contracts with recorded Why3 and SMT proofs relate selected functions of the compiler, the sumcheck engine, the composition facade and the hash-gadget interface to the model, and a mechanized forward theorem derives the chain event from an accepted run and its concrete round checks under an explicit Rust/model value relation; discharging that relation for the compiled verifier is the open last link (Section 5). - Prover memory and speed, with the Isabelle theories untouched. Libra-style sparse booking keeps peak process memory about 89× below a test-only dense reference at width 4,096, and derived wiring verifies the same proof 10.80–23.68× faster. The round arithmetic of release 1.2 raises proving throughput 2.41–2.71× with all 13,824 compared proof hashes unchanged, and at 1,000 requests per second on one 192-core VM, p99 latency to verified acceptance fell from 440 to 75 ms with a new serving path and to 34 ms with the new arithmetic. - Reuse. Through a frontend, the sumcheck/GKR core proves any layered circuit of these gate kinds with the field and hash of the shipped entry points, and another application inherits the chain bound and the composition by proving its own arithmetization theorem (Section 7). Figure 1: Measured gains, each against StateSync-GKR’s own baseline. (a) Peak process memory at width 4,096, sparse prover against a test-only dense reference in the same driver. (b) Under a 3 GiB cap the dense reference is killed at width 8,192, while the sparse prover reaches 65,536. (c) Prepared proving throughput at 192 workers and depth 24, releases 1.1 and 1.2 measured the same day. (d) p99 latency to verified acceptance, timed at the caller with the network included, at 1,000 requests per second on one 192-core VM (median of three 60-second runs). 1. From Sumcheck to GKR GKR, after Goldwasser, Kalai and Rothblum, runs one sumcheck of Lund, Fortnow, Karloff and Nisan per layer of a layered arithmetic circuit and reduces a claim about the output layer, layer by layer, to a claim about the input, at a soundness cost of degree/|𝔽| per sumcheck round. Thaler made the prover time-optimal for regular wiring, and Libra made it linear-time for general circuits with a two-phase sumcheck. Hashing suits this structure: each round of a Poseidon2 permutation becomes a layer, many hashes run side by side in the same layers, and with a native cube gate for the x³ S-box one layer applies one round. A system that acts on a verifier’s accept, for example by adopting a new Merkle root, needs a statement about the update the circuit encodes. That rests on three arguments: soundness of the protocol for the gate set and field in use, exactness of the arithmetization that turns the update into a circuit, and position binding of the tree that commits to the state. The second is where deployed proof systems fail most often: under-constrained circuits account for 95 of the 141 vulnerabilities in the systematization of SNARK bugs by Chaliasos et al. Sumcheck has been formalized in Isabelle/HOL, and the authors’ paper names the analysis of protocols such as GKR as future work; ArkLib develops interactive oracle reductions in Lean 4. Our Isabelle/HOL development takes up that analysis. The first version of the formal paper went to arXiv on 4 October 2026 with, to our knowledge, the first public machine-checked soundness bound for GKR on general layered circuits. In the same days, leanerVM was proving knowledge soundness of a grand-product GKR, the special case of a fixed product tree, in a pull request opened on 2 October and merged on 5 October. Lean developments covering GKR have appeared since: complexitylib proves perfect completeness and soundness of GKR with addition and multiplication gates; GordieHowe machine-checks a GKR-based argument for ML-DSA-44 from the source program to the non-interactive setting; Longfellow proves conditional extraction and false-statement soundness for a model of its non-interactive verifier; and since 6 November 2026 leanerVM’s main branch proves soundness for a Lean implementation of its non-interactive verifier in the random-oracle model. All four machine-check a bound on the verifier’s acceptance, and the last three reach the non-interactive argument and a committed input. Specific to this work are GKR in Isabelle/HOL, cube gates, the KoalaBear quartic extension in the implementation’s coordinates, an exactness theorem for sparse-Merkle updates of every depth, and a reduction to position binding for a node hash that is not collision resistant. The second argument has to be proved for each family of circuits, as GordieHowe and leanerVM do for their programs; outside GKR, semaphore-mtb and Zolana have Lean proofs for fixed-depth Merkle circuits, and Coda and Picus consider arbitrary assignments to a circuit’s witness. Sections 2 and 3 settle the first argument for this gate set and field, and Section 4 proves the second for sparse-Merkle updates of every depth. 2. GKR Soundness and Its Layer Chain in Isabelle/HOL The central machine-checked statement bounds the whole layer chain (gkr_assembly_soundness, Theorem B; this post keeps the development’s letters for its three main theorems). It holds against any prover strategy, with probabilities over the verifier’s uniform and independent public-coin challenges and the verifier holding the circuit input in the clear, as in GKR’s delegation setting. For any layer chain and any false output claim, \Pr[\mathrm{Bad}_0] \le \frac{s_{\mathrm{out}} + \sum_i \big(2 s_i \cdot \mathrm{db}(s_i) + 1\big)}{|\mathbb{F}|} where the circuit has 2^(s_out) outputs and layer i reads 2^(sᵢ) wires. The term s_out pays for the random seeding of the output claim, 2sᵢ·db(sᵢ) is the sumcheck bound for a polynomial that represents layer i with degree bound db(sᵢ), and the 1 pays for folding two evaluation points into one claim. For comparison, the layer identity of the original protocol has addition and multiplication gates: V_i(z) = \sum_{x,y \in \{0,1\}^{s}} \widetilde{\mathrm{add}}_i(z,x,y)\,\big(V_{i+1}(x) + V_{i+1}(y)\big) + \widetilde{\mathrm{mult}}_i(z,x,y)\,V_{i+1}(x)\,V_{i+1}(y) The circuits here use weighted linear, product and cube gates, a constants vector per layer, and claims carried as weighted point lists (z_k, c_k), so the sumcheck of layer i runs over P_i(x,y) = \sum_k c_k \Big[ \widetilde{\mathrm{lin}}(z_k,x)\, V_{i+1}(x)\, \beta(y) + \widetilde{\mathrm{mul}}(z_k,x,y)\, V_{i+1}(x)\, V_{i+1}(y) + \widetilde{\mathrm{pow3}}(z_k,x)\, V_{i+1}(x)^3\, \beta(y) \Big] with the layer identity \sum_{(x,y)\in\{0,1\}^{2s}} P_i(x,y) = \sum_k c_k \big( V_i(z_k) - \widetilde{\mathrm{const}}(z_k) \big) Here Vᵢ is the multilinear extension of layer i’s values, the three wiring predicates and the constants vector are extended the same way, and β is the standard lifting that sums to 1 over the cube. The cube term lets one layer apply Poseidon2’s S-box without stacking two product layers, and it raises the degree of this polynomial to four in each variable of x (two in each variable of y). Theorem B imports sumcheck soundness from the AFP entry, which bounds by n·d/|𝔽| the chance that an instance in n variables with abstract degree at most d accepts a false sum. The chain bound therefore asks for a representative of each layer: a polynomial in its 2sᵢ variables that agrees with the integrand on the Boolean hypercube and has degree at most db(sᵢ) in the entry’s measure. After a layer’s sumcheck the verifier holds claims about the next layer at two points (x*, y*) and carries them as the claim list [(x*, 1), (y*, r)] with a fresh challenge r, and the chain event recurses over the remaining layers: \mathrm{Bad}_i = \mathrm{AFPAccept}_i \lor \big(\mathrm{carry}_i\ \text{false} \land \mathrm{Bad}_{i+1}\big) Here AFPAcceptᵢ is the imported sumcheck’s acceptance event for layer i’s representative, and “carryᵢ false” means a carried evaluation disagrees with the next layer’s true polynomial. A false claim must make some layer’s sumcheck accept a false sum, be hidden by the random combination of the carried values, or reach the input layer, where the verifier rejects it. Theorem B bounds this event for every representative family that meets its premise. Figure 2: One layer of the GKR reduction and the term each step adds to the bound of gkr_assembly_soundness. The dashed box is the verifier’s own bound, proved on paper by a separate induction. Which representative is used decides what the theorem says about a verifier. The development discharges the premise with the multilinear interpolation of the layer integrand, of total degree at most 2s, so the theorem applies with db(s) = 2s and a per-layer term 4sᵢ² + 1. The verifier evaluates the Pᵢ above, which agrees with the interpolation on the hypercube and has degree up to four in each variable; its round check bounds that per-variable degree, while the imported round check uses the total degree. The formal paper therefore repeats the induction for Pᵢ and the verifier’s own round check, with the textbook sumcheck bound and the mechanized layer lemmas, and proves on paper \Pr[\mathcal{V}\ \text{accepts a false output claim}] \le \frac{s_{\mathrm{out}} + \sum_i (8 s_i + 1)}{|\mathbb{F}|} with 8sᵢ = 2sᵢ·4 for 2sᵢ rounds of degree at most 4, a degree unrelated to the quartic extension field of the next section. 3. Over the Field the Challenges Come From A bound with denominator p ≈ 2³¹ says little, so small-field provers evaluate circuits over the base field and draw challenges from an extension. StateSync-GKR takes circuit values in KoalaBear, p = 2³¹ − 2²⁴ + 1, and challenges from its quartic extension \mathbb{F}_p[X]/(X^4 - 3). For the bound to speak about that prover, the extension has to exist as a field in the proof assistant, in the coordinates the implementation uses, and the base-field circuit and its false claim have to be carried into it. The base field is the residues mod p, with primality proved by trial division up to ⌊√p⌋ = 46,159 and discharged by eval, and the extension is a tower of two quadratic extensions in the implementation’s coordinates: \mathbb{F}_{p^2} = \mathbb{F}_p[\theta]/(\theta^2 - 3), \qquad \mathbb{F}_{p^4} = \mathbb{F}_{p^2}[\alpha]/(\alpha^2 - \theta) \cong \mathbb{F}_p[X]/(X^4 - 3), \qquad |\mathbb{F}_{p^4}| = p^4 \approx 2^{124} The coordinate map (a₀, a₁, a₂, a₃) ↦ (a₀ + a₂θ) + (a₁ + a₃θ)α is proved bijective, kb_alpha_fourth proves α⁴ = 3, and ext4_denominator_exact proves the cardinality exactly p⁴ for p = 2,130,706,433. Each level is a field by a norm argument with nonsquare certificates, 3 by quadratic reciprocity and −3 from a square root of −1 modulo p checked by evaluation. The base-field embedding is proved to commute with sums, products and multilinear extensions at base-field points and to preserve layer evaluation, well-formedness and a false output, layer by layer. Theorem B is proved once in a locale over an abstract field and polynomial type, so the extension-field statement (gkr_assembly_soundness_ext4) needed no second probabilistic proof: its locale obligations close by unfold_locales and one call of auto. Four independent uniform base-field coordinates push forward to a uniform extension element (uniform_coeff_tuple_pushforward), the form in which the implementation draws a challenge. On paper are the match with the implementation’s basis 1, X, X², X³, the isomorphism with \mathbb{F}_p[X]/(X^4 - 3), the step from one challenge to many independent ones, and the lift of a whole chain from the per-layer lemmas. 4. From the Circuit to the Update 4.1 Exact Arithmetization A layer holds 2ˢ wires, a constants vector and a list of Lin, Mul and Pow3 gates. For a transition claim (op, r, r′), the compiler emits a circuit whose outputs are residuals that vanish exactly when a constraint holds: the leaf sponge chain and the compression chain up the authentication path, with key bits selecting sibling order through multiplexers; booleanity residuals b(b − 1); tag residuals such as tag(tag − 2), which force a non-membership leaf to be empty or retired; and boundary residuals that equate recomputed and claimed roots. Acceptance is a zero test on the output layer. Theorem A relates acceptance to validity in both directions, on the input the verifier itself builds. Soundness (theorem_A_soundness) turns an accepting witness into a canonical valid one, completeness (theorem_A_completeness) shows that every valid transition is accepted, and together they give (theorem_A_compilation_soundness): \big(\exists\, vd, w.\ \mathsf{accept}(op, r, r', vd, w)\big) \iff \big(\exists w.\ \mathsf{valid}(op, r, r', w)\big) The verifier model checks the claim’s public parts, encodes the witness as the circuit input and evaluates the compiled checks; on such inputs the hash-chain and booleanity residuals hold by construction, so the theorem rests on the boundary and tag residuals and the public checks. The shipped verifier also rebuilds the input from the witness, and no succinctness in the witness is claimed. The constraints carry their full weight when the verifier instead receives the input vector from the prover, compares its public segments (key bits, roots, value digest and, for an update, the old leaf’s pre-image) with the claim, and computes no node hash. Then every input that passes these comparisons and zeroes all outputs of the compiled circuit determines a valid witness, assuming that digests are represented by their own field elements and that the hash sub-circuits compute the hash functions on every input. This is proved on paper from a machine-checked characterization of the constraints (A_i_ro, A_i_up: for every input vector of the right length, the circuit accepts exactly when the constraints hold). 4.2 Leaf Binding, and the Defect Behind It Leaves have three states, empty, occupied and retired, so that a retired slot stays distinguishable from one never used, and a leaf is hashed by a rate-8 sponge over the explicit encoding [tag, len, payload, 0-padding]. That encoding became a lemma after a defect found before the first public release. When an algebraic placeholder hash, documented as having no collision resistance, was replaced with Poseidon2, an internal adversarial review found that folding variable-length leaf records into fixed-width hash input was not injective: two different leaves could reach the same hash input without any break of the hash, and a forged membership proof passed both checking paths. The placeholder’s own caveat had hidden the defect. The fix lays a leaf out losslessly, at a real cost in permutations and proof size, and leaf_fold_inj proves the encoding injective for in-bound lengths, so a leaf-hash collision on distinct encodings yields a sponge collision (h_leaf_collision_to_sponge_collision) with no assumption about the sponge. 4.3 Composition, and the Statement That Carries Security Theorem C (theorem_C_composition) composes A and B in one locale that identifies the circuit’s field with the challenge field. If the public-side checks pass and no witness makes the claim valid, the chain event of the compiled circuit with the all-zero output claim satisfies \big(\nexists w.\ \mathsf{valid}(op, r, r', w)\big) \;\Longrightarrow\; \Pr\big[\mathrm{Bad}_0\big] \le \frac{r_{\mathrm{out}} + \sum_i \big(2 s_i \cdot \mathrm{db}(s_i) + 1\big)}{|\mathbb{F}|} where r_out, the number of residuals (240 to 584; the model gives each its own bit, which overstates this term), takes the place of s_out, and the witness is fixed before the challenges. For a compressing hash the premise “no witness makes it valid” is strong: a sibling list has far more free field elements than a root, so, heuristically, if the node hash behaves like a random function, most roots are reached from a given leaf by some sibling list and a false claim has a valid witness. The statement that carries security therefore fixes the input. Let x be an input fixed before the challenges, either encoded by the verifier from a witness or received from the prover and checked on its public segments, and let wit(x) be the witness it asserts. Then for every prover strategy \neg\,\mathsf{valid}\big(op, r, r', \mathrm{wit}(x)\big) \;\Longrightarrow\; \Pr[\mathcal{V}\ \text{accepts}] \le \frac{r_{\mathrm{out}} + \sum_i (8 s_i + 1)}{|\mathbb{F}|} With p⁴ as the denominator the same holds over KoalaBear with challenges from its quartic extension, and in the constraint-level model at the default depth 24 the bound is below 2⁻¹⁰⁰. These per-input forms are paper proofs on the machine-checked parts: the contrapositive of the arithmetization theorem makes the all-zero claim false, and the verifier bound of Section 2 applies. A system also relies on accepted runs for one key and root asserting one leaf, and here the hash assumption enters. The node hash is the first half of a Poseidon2 permutation with no feed-forward, so two calls to the inverse permutation give a collision, yet a collision does not give two authentication paths, because a path must start at a leaf hash and its accumulators must connect to that start. What a system needs is position binding of the tree: finding one key, one root and two different leaves with valid paths must be hard. With E the event that two accepted runs with independent challenges assert different leaves for one key and root, and ε the per-input bound, an explicit reduction gives \Pr[E] \le 2\varepsilon + \mathsf{Adv}^{\mathrm{pb}}(\mathcal{B}) The verifier reads the asserted witness in the clear, so the reduction needs no extractor. Position binding is assumed, not proved, and enters only this bound. Coratger, Khovratovich, Mennink and Wagner prove strong position binding for Merkle trees with a truncated permutation in the ideal-permutation model, with a bound that reaches 1 at about 2¹²³ queries at these parameters; their leaf hash differs from ours and their model idealizes Poseidon2, so the paper cites this as support without applying it. Figure 3: The status of each result. Machine-checked: Theorems A, B and C. Paper steps over mechanized parts (dashed): the verifier’s own bound, the per-input forms, prover-supplied inputs, the whole-chain lift and the cross-field composition. Position binding is an assumption and enters only the one-leaf bound. On the right, contracts relate code to model clauses (dotted), and the forward theorems carry the value relation that Section 5 calls the last link. 4.4 Nonvacuity as Part of Done A theorem over a locale has content only if its assumptions can be satisfied, and the proof assistant checks the implication, never the satisfiability. When the model verification first looked finished, with a clean build and no proof left as sorry, requiring a registered concrete instance for every assumption set exposed a compiler-side set that nothing could satisfy: it forced two specification-vector lengths to be powers of two, while they provably satisfy ℓ_ro < ℓ_up < 2ℓ_ro, so both compiler-side headline theorems had been vacuously true. Every locale behind Sections 2 to 4 is now interpreted by a concrete instance over KoalaBear, and the arithmetization and composition theorems are applied, for a tree of depth one with a linear hash pair, to inputs that satisfy their premises (instance_theorem_A_activation, instance_theorem_C_activation). Witnessing the assumptions of every machine-checked theorem we use with a registered concrete instance is now part of what “done” means for this development. 5. A Partial Refinement Down to the Rust Code A partial refinement connects the model to the implementation in three parts: contracts on the code, verifier bodies that the tool can read, and a forward acceptance theorem in Isabelle/HOL. Creusot contracts, with recorded Why3 and SMT proofs, relate selected functions to model clauses in four families: the compiler crate to the acceptance definitions of Theorem A; the sumcheck engine and layer reduction to the chain of Theorem B, including the round-step law of the imported sumcheck protocol on the oracle interface; the composition facade to the merged model; and the hash-gadget interface to the model’s hash usage, as interface correspondence only. Recorded proofs also establish the exact public-input equality check and the acceptance classifier, the conjunction of seven named observations from public-input binding to the two final input evaluations. Production wiring-oracle evaluation, transcript operations and the observation helpers stay outside as trusted translation boundaries. The sumcheck and per-layer verifier bodies are translated around a single foreign-field equality each, exposing round counting, degree checks, rejection paths, transcript order and carry construction to the tool; the records cover their verification conditions, while their stated postconditions are design contracts that the tool does not check. The current tree holds 335 replay records with 2,456 discharged and 182 open solver leaves, none open in the sumcheck records (leaf counts are not a coverage percentage). A source and evidence map names the code, the contract and the recorded evidence for request binding, round checks, carry construction and final input evaluations, and an integrator can reuse it to review a frontend. The forward theorem production_verifier_acceptance_refines_gkr_chain_bad, a corollary of verifier_acceptance_implies_gkr_chain_bad, derives the chain event of Section 2 from an accepted run and model well-formedness; the per-layer bridge that the first theorem assumes is derived from the concrete round checks and the finish-evaluation part of the value relation rust_hol_value_trace_relation between Rust values and the model, so the acceptance argument can be inspected at the checks it depends on. That relation is the last link, and it is open: with the multilinear representative of Section 2 its finish part fails on honest runs in general, because the verifier compares its last round value with a different polynomial. As it stands the corollary does not apply to the shipped verifier, and the soundness statements of this post are statements about the model. Closing the link takes a mechanized chain bound for the verifier’s own polynomial and round check, the argument Section 2 proves on paper, and a value relation discharged for the compiled verifier body. The development builds with Isabelle2025-2 against AFP release 2026-08-05; the results were obtained on release 1.1.0, and the theory files are unchanged through release 1.2.1. A hosted workflow rebuilds every session from clean targets on each push to the maintained branch, weekly and on pull requests that change a proof input, and a source check fails on any sorry, oops, axiomatization or oracle command. The two numeric facts discharged by eval in Section 3 also trust the code generator and the ML runtime. 6. Prover Memory and Speed, with the Theories Untouched Theorem B and its extension-field instance quantify over every prover strategy, and the model contains no prover arithmetic, so a change confined to the prover cannot weaken them. Sparse booking, cube gates and derived wiring were already in release 1.1, on which the formal results were obtained; release 1.2 changes the prover’s arithmetic, adds serving components and keeps the verifier functions, the proof format and the transcript order. A prover change could still break completeness, determinism or the code the contracts describe, and the control for that is the byte comparison: every compared proof of release 1.2 is byte-identical to release 1.1, and the Creusot records of the changed functions were regenerated with no existing contract regressing. So no formal proof had to be redone. 6.1 Sparse Layer Reduction For a layer with nᵢ input wires, nₒ output wires and m multiplication gates, a dense sumcheck oracle materializes factor tables over all input pairs and owns O(nₒ + nᵢ²) auxiliary memory. The production oracle follows Libra’s two-phase booking, in which multiplication supplies a sparse list of weighted input pairs, so it owns O(nₒ + nᵢ + m) and never builds the input-pair hypercube. The dense method stays in the code as a test-only reference, and differential tests require both oracles to produce the same round polynomials and proofs on every shared case. In the same driver, with field, transcript and circuit fixed, a two-layer mixed circuit of width 4,096 requested 579,584 bytes of additional memory during proving, against 1.88 GB for the dense oracle. Figure 4: Peak process memory by layer width for the sparse prover and the test-only dense reference in the same driver (release 1.2; release 1.1 is within 0.6 MiB at every width). The sparse prover reaches 65,536 wires in 259.6 MiB. 6.2 Cube Gates and Parallel Path Constraints Poseidon2 over KoalaBear has an x³ S-box, so the cube and the affine step after it become one round layer of Pow3 and linear taps. The compiler checks every compression on an authentication path against witness-supplied intermediate values as parallel residual constraints, so the number of layers follows the hash’s rounds and does not grow with the tree depth: all nine tested circuits, three operations at depths 24, 28 and 32, have 118 layers, and a membership proof grows from 176,948 bytes at depth 24 to 182,132 bytes at depth 32, about 2.93%. Width and total work still grow with depth. 6.3 Derived Wiring and the Lemma Behind It Compilation is data-parallel, so each layer’s wiring decomposes into a few arithmetic-progression families plus a sparse residue, and the verifier can evaluate the wiring extension in closed form without iterating the gate list. A lemma in the Isabelle development (derived_mle_eq_table) states when, for well-formed families, the two forms are the same polynomial: \biguplus_{j} \mathrm{expand}(F_j) \uplus R = G_i \;\Longrightarrow\; \widetilde{W}^{\mathrm{derived}}_i = \widetilde{W}^{\mathrm{table}}_i At run time the derivation checks each family member’s progression, kind and coefficient and falls back to the exact sparse path on any mismatch, so a wrong layout hint from the compiler is designed to cost time without changing the evaluated polynomial. Against table wiring, itself sparse, derived wiring verified the same proof 10.80–23.68× faster across the nine profiles, the ratio growing with depth for every operation (release 1.1 measurements; release 1.2 changes neither the wiring evaluation nor the proofs). 6.4 Prepared Circuits, Deterministic Transcripts and Serving Compilation, the commitment to the whole circuit and the derived wiring are the same for every request of one operation kind, so they are prepared once per kind and shared read-only. The commitment dominates: for depth-24 membership in release 1.2 it takes about 104 ms, against 7.8 ms for compilation and 16.4 ms for proving. The transcript absorbs a domain tag, the circuit shape and commitment, the public inputs, the claimed outputs, the round messages and the carried evaluations in a fixed order, so proof bytes depend on neither worker count nor scheduling. Requests run as independent jobs that are never aggregated, and theorem_D_batching_correctness states that a batch of independent jobs verifies exactly when every job verifies on its own. In the serving path of release 1.2 the verifier checks each received proof against its original request, so a different root, value digest or circuit identifier, or trailing bytes, cause rejection. One connection carried 3,300 requests per second with every request accepted within one second; at 3,400 per second the replies reached the provider’s documented single-flow limit of about 5 Gbit/s. 6.5 The Round Arithmetic of Release 1.2 Release 1.2 keeps the two phases of the sparse oracle and reorganizes each sumcheck round with three standard identities (Figure 5a). The output-line weights c_k·eq(z_k, j) come from one scaled equality table per claim built by doubling, about 2·2ˢ multiplications in place of s·2ˢ. Every table factor is multilinear in the variable being bound, so its values at the round’s five nodes follow from f(0) and f(1) by repeated addition, in one pass over the table. A fixed inverse Vandermonde matrix, built once per layer, then recovers the round polynomial from the five values, removing the per-round inversions and small allocations of Lagrange interpolation. Each change computes the same field elements by an algebraically equivalent route, and finite-field arithmetic is exact, so the proofs should be identical byte for byte, and they are: across 768 fixtures for each operation at depths 24, 28 and 32, in native and default builds, all 13,824 proof hashes match release 1.1, and the dense and sparse oracles still agree. On a 192-core bare-metal server at depth 24 with batches of 768, prepared proving went from 3,195.50, 2,947.08 and 2,102.02 proofs per second for membership, non-membership and update to 7,713.71, 7,220.36 and 5,390.07, between 2.41× and 2.71× across 1 to 192 workers against release 1.1 measured the same day. On the width-4,096 circuit of Section 6.1, allocation calls per proof fell from 1,282 to 85 with the same requested peak. Figure 5: (a) The three changes to the sumcheck round arithmetic in release 1.2. (b) Prepared proving throughput at 192 workers, releases 1.1 and 1.2 measured the same day. (c) Allocation calls per proof. 6.6 Summary and Comparison Scope Mechanism Baseline Result Setting Sparse layer reduction test-only dense reference, same driver, field and transcript 3,242.41× less requested allocation; 88.87× lower process memory (89.46× in release 1.1) two-layer mixed circuit, width 4,096 Sparse reduction under a 3 GiB cap same dense killed at width 8,192; sparse proves up to 65,536, the largest tested same circuit family Cube gates and parallel path constraints structural 118 layers at depths 24 to 32; membership proof +2.93% from depth 24 to 32 nine profiles Derived wiring table wiring (itself sparse), same proof 10.80–23.68× faster prepared verification nine profiles, depths 24 to 32 Prepared circuits fresh preparation per request 7.19–10.13× shorter per-request proving path (3.46–4.45× in release 1.1) one thread, depth 24 Parallel output handling serial output handling 14.10–14.64× faster complete prepared local batch (9.71–10.71× in release 1.1) depth 24, batch 768, 192 workers Round arithmetic of release 1.2 release 1.1, same day 2.41–2.71× proving throughput; 1,282 → 85 allocation calls per proof; byte-identical proofs depth 24, 1 to 192 workers; width 4,096 Serving path and prover of release 1.2 release 1.1, same day p99 433.8–475.1 → 33.7–33.9 ms at 1,000 requests/s; 3,300 requests/s per connection within 1 s one 192-core VM Every ratio is an internal comparison with a named baseline and its own workload and timer, so the ratios should not be multiplied with one another or applied to a complete remote service, and same-condition comparisons with other proof systems and production GKR provers are outside this evaluation. The design and evaluation paper carries the full record in over 160 pages, with process repeats, failed attempts and refusals kept in their denominators. 7. Reuse The engine implements the published GKR construction with Libra’s two-phase sparse sumcheck on Plonky3 primitives and adds no new protocol. Three parts carry over to another application: - Core. The sumcheck and GKR crates prove and verify layered circuits of the three gate kinds without depending on the sparse-Merkle compiler. A frontend supplies the circuit, witness, output claim and transcript conventions, and must consume both residual input claims. - Field and hash. The sumcheck crate, the circuit representation and the general model are generic over the field. The single adapter crate that names Plonky3 fixes the field and hash to KoalaBear, its quartic extension and Poseidon2 from Plonky3 v0.4.3; replacing them in the code is a new implementation and verification task. - Proofs. Another application inherits the chain bound and the composition by proving its own arithmetization theorem in the form of Theorem A’s soundness and repeating the per-input argument on paper. Another challenge field needs a field construction and the lifting lemmas. Use cases. Any computation written as a layered circuit of these gates runs on the core, and the sparse-Merkle frontend is its first workload: membership, absence and single-leaf updates against a published root, with three-state leaves that keep insertion, update, deletion and restoration distinct and sequentially assigned keys, so the default depth of 24 holds about 16.8 million records. - AI and custom computation. Machine-learning arithmetic, data pipelines and other layered computations run on the core directly, through a frontend built for them; a guide walks through building one. - Regulated assets. Proofs that a holder is on a register, that an address is absent from a restricted list, or that a holding changed correctly. - Blockchains. Membership, absence and single-record updates for rollups, app-chains and synchronization layers that keep their state in the engine’s sparse Merkle tree. - Data systems. A checkable answer, for a key-value store or registry, to whether a key is present, absent or updated, against a root the client already trusts. 8. Scope All probabilistic statements concern the interactive public-coin protocol, with challenges drawn uniformly and independently from the field and the input fixed before the challenges, matching the imported sumcheck development. The Fiat–Shamir transformation that makes the running protocol non-interactive is outside the analysis (it is delicate for GKR-based arguments), and we make no claim about the non-interactive protocol. In the running protocol the transcript absorbs the public inputs and the circuit commitment but not the witness-derived input, so that input is not fixed before the challenges there; the independent review records this point and constructs no false acceptance from it. Not treated are a verifier that receives only a commitment to the input, verification of the Poseidon2 sub-circuits against the hash functions (the correspondence between compiled circuits and the model is carried by the contracts of Section 5), and an assembled completeness theorem for a full protocol run. Zero knowledge is not claimed for the inner GKR proof, and no extractor is constructed; hiding is left to an external zkVM wrapper, for which release 1.2.1 attaches, as component evidence, a RISC Zero proof of a fixed depth-24 membership relation checked on an external verification network’s testnet. Release 1.2.1 is source-available under BSL 1.1, which permits non-production research and reproduction; MIT or Apache-2.0 rights already granted for releases up to v1.1.0 remain valid. 9. Open Questions - Closing the last link to the Rust verifier. Once the verifier’s own integrand and round check have a mechanized bound, should the value relation be discharged through the existing contracts or by validated translation of the specific verifier body? - A verifier that commits to its input. The verifier here reads the input in the clear, and an argument that commits to the input needs a per-input bound at the input it extracts. Which commitment to the input layer keeps the arithmetization theorem and the composition intact? - Binary fields. A recent comparison of standard hash candidates for Ethereum models proving costs on a system for binary circuits. Which parts of this chain carry over to GKR over binary towers for Keccak- or BLAKE-based trees? The probabilistic proof is stated over an abstract finite field, while the arithmetization and the cube-gate economics are tied to a prime-field hash. Approaches to these questions, and corrections to any statement above, are welcome. A year after that tutorial, the protocol it introduced me to has a soundness proof for these circuits with a machine-checked core, a partial refinement into the Rust code, and a sparse prover that became faster with the same proof bytes. StateSync-GKR was developed for one workload, state synchronization across domains, which is what its name refers to. Acknowledgments. We thank Bernhard Müller for his independent review of the verifier’s challenge-generation assumptions and the implementation-facing interpretation of the extension-field soundness bound, which clarified the line between the mechanized results and the remaining arguments. Artifacts - Formal verification paper and design and evaluation paper - Source, with REPRODUCING.md and FORMAL_VERIFICATION.md - Release assets with an SBOM, a provenance attestation, a proof manifest and checksums; a source recipe is expected to reproduce the documented deterministic proof digest - Engine site and documentation - Design journey article - Software DOIs: 10.5281/zenodo.23643505 (v1.2.0, the measured release) and 10.5281/zenodo.23655511 (v1.2.1, current) Visit Topic to respond. You are receiving this because you enabled mailing list mode. ArkLib: Verified-zkEVM/ArkLib leanerVM: Verified-zkEVM/leanerVM complexitylib: cslib-community/complexitylib GordieHowe: cmlsharp/gordiehowe Longfellow: github.com/longfellow-zk/longfellow-zk/tree/main/… semaphore-mtb: github.com/worldcoin/semaphore-mtb/tree/master/fo… Zolana: github.com/helius-labs/zolana/tree/main/prover/se… Creusot: creusot-rs/creusot source and evidence map: github.com/Oraclizer/statesync-gkr/blob/7179c5f53… Plonky3 v0.4.3: github.com/Plonky3/Plonky3/releases/tag/v0.4.3 independent review: github.com/Oraclizer/statesync-gkr/blob/7179c5f53… Bernhard Müller: github.com/muellerberndt Source: Oraclizer/statesync-gkr REPRODUCING.md: github.com/Oraclizer/statesync-gkr/blob/7179c5f53… FORMAL_VERIFICATION.md: github.com/Oraclizer/statesync-gkr/blob/7179c5f53… source recipe: github.com/Oraclizer/statesync-gkr/blob/7179c5f53…
I just want to remind the world, we released the neural architecture that will lead to embodied AGI. It’s open source. Please put Cadence brains in cool things 😄 muellerberndt/cadence
Transformer alternative neural architecture AND its open source (: muellerberndt/cadence
Cadence v0.92 lets builders grow a trained brain with new memory tools and outputs, or graft compatible trained regions into another brain. Build on what you’ve already taught. Give it room to learn more. Combining skills still takes teaching. muellerberndt/cadence
From the same author: Cadence, a brain-like learning system that keeps learning while it acts, with local plasticity in place of backpropagation. pip install cadence-net muellerberndt/cadence Paper: philpapers.org
Cadence is a settling/equilibrium propagation neural net that learns during life. v0.89 adds multi-head attention: The brain can learn to attend to memories keyed by (also learned) compressed representations of meaning. Find the latest release here: github.com/muellerberndt/cadence/releases t.co
New Cadence release just dropped: github.com/muellerberndt/cadence/releases/tag/v0.… Roadmap update: Our strategy is to implement bio-inspired mechanisms for sequence processing, attention and short/long-term memory. These should integrate well with Cadence's local settling dynamics. Symbolic reasoning, language capability and self-reflection are all long-term research goals. A Cadence brain is supposed to be able to form an entire sentence in-brain before saying it.