TL;DR
- In December 2025 we argued that GKR is not an optimization for a state oracle but a precondition for one to exist. Turning that claim into a running prover showed that a precondition does not make an engine. What else the engine needed was taught one item at a time, by the workload and by failures.
- State synchronization asks a prover narrow questions: is a record under a published root, is it absent, did a leaf change correctly. It asks them again and again, with circuits of the same shape, under a deadline. Three-state leaves, sequential keys, a 118-layer circuit that does not change with tree depth, one preparation and independent per-request proofs all follow from those questions.
- Most of the January plan changed. The memory wall of a dense oracle, a verification cost hidden in the wiring table, a leaf-encoding defect masked by a placeholder hash, and vacuous theorems behind a clean build each changed the engine.
- The published measurements show 89.46x lower peak resident memory than our own dense reference, verification 10.80 to 23.68x faster than table wiring, and a 3.46 to 4.45x shorter proving path from reused preparation. Measured all the way to the caller, the delay piled up in the queue outside proof computation, behind a serial path that returns results.
- We still hold the original claim, and its grounds are now an engine we actually built, measured and machine-checked.
1. Why We Built the StateSync-GKR Prover Ourselves
In December 2025, Why State Oracle Demand a Different Proof Primitive argued that data oracles and state oracles face different proof demands. A data oracle asks whether a value was correct at one moment. A state oracle has to keep asking whether every causally linked state transition is valid. That article held that committing to every intermediate value made continuous synchronization possible in theory but infeasible in computation for existing SNARKs, and it set the GKR protocol, which checks each layer with sumcheck and removes intermediate commitments, as the answer [1]. A month later, GKR Protocol Deep Dive: The Computational Engine Behind OSS laid out a plan to build that engine on gnark, with performance estimated by simulation.
Ten months after the December article, the engine exists. The Rust source of the StateSync-GKR prover is public, and two arXiv papers carry its trust chain and its controlled measurements [5,6]. What we built barely resembles the January plan. We wrote Rust in place of gnark, and in place of another team's GKR library we implemented sumcheck and GKR to their published specifications on open-source field and hash primitives. The decisions we had not planned outnumbered the ones we had. The January estimates were simulations of a gnark design we never built, and the engine we did build asked different things of us.
We built it ourselves for two reasons. The first was to keep the verification boundary inside our own code. We wanted to machine-check in Isabelle/HOL that the engine's acceptance coincides with the intended state transition, and to connect that model to the real code. The tool we chose for that connection, Creusot, works on Rust, and the code the connection relies on had to stay under our control. The second reason was the workload.
Proving for state synchronization means repeating layered circuits of the same shape, without end, inside the deadline of primary finality. That deadline is set by the slowest request more than by the average, and a GKR prover's time is linear in circuit size and, for a fixed shape, the work is the same every time [2]. No general GKR library was built to absorb that repetition and that deadline together.
We also set one prohibition for ourselves: do not invent protocol. GKR and the linear-time techniques built on it are specified precisely, and changing them gains nothing while adding soundness risk [1,2,3]. Our initial design assumed the field library we built on offered a sumcheck component; it did not. When that library added one months later, we kept our own implementation.
The original reason was gone, but that component was evolving together with a higher-level pipeline we do not use, and a new reason had appeared: the code our theorems rest on cannot be left to outside changes. A ready Rust GKR already existed in Polyhedra's Expander, and Libra had shown GKR proving Merkle hashing in 2019 [2]. Our part sits on top of that earlier work, in fitting an engine to the questions of state synchronization.
2. What the Ledger Asked of the Circuit
What state synchronization asks of the StateSync-GKR prover is narrower than one might expect. Against the published root of a sparse Merkle tree that binds asset state, it asks whether a record is present (membership), whether it is absent (non-membership), and whether one leaf changed correctly into a new root (update). The questions are simple, but they repeat without end, and each time the circuit has the same shape. Narrow questions, the same shape repeated, and a deadline: these three properties set most of the engine's decisions.
First, leaves have three states. A leaf is Empty (never written), Occupied (holding a record) or Tombstone (written, then retired). Two states look sufficient, but if a retired slot cannot be told apart from one that was always empty, the historical uniqueness argument fails for whatever once stood there [5]. An absence proof accepts both Empty and Tombstone, yet the circuit encodes them as different values. In a system that carries the life of regulated assets, "deleted" and "never existed" are different facts.
Second, keys are assigned in order. A GKR circuit with a fixed layer structure needs a deterministic bound on tree depth. Keys derived from hashes let an attacker stretch the depth tail, and avoiding collisions would push the depth toward 256 and inflate proof cost. When the asset registry hands out monotonically increasing numbers, the occupied key space packs densely at the front, and the default depth of 24 holds about 16.77 million assets.
Third, hashing is translated into the circuit's own language. Most of what this circuit does is hashing. We first believed BabyBear was a sensible default, and the investigation reversed that. Poseidon2 over KoalaBear has an x³ S-box, cheaper than BabyBear's x⁷ [7,8], and we folded that cube and the affine step after it into native gates of the circuit, which removes intermediate layers. The hash constraints along the path are placed in parallel instead of being stacked layer after layer.
As a result, the nine circuits we tested (three operations at depths 24, 28 and 32) all have the same 118 layers, and raising the depth from 24 to 32 grew the membership proof by only 2.93% [6]. Computation still grows with depth, but the circuit depth that the January article, assuming a depth-32 tree, listed as an implementation challenge turned, in the real engine, into a question of fixing the layer schedule. The code and the formal model are generic over the field and hash, so changing this choice is a re-instantiation and needs no redesign.
Fourth, because the shape repeats, preparation happens once. Circuit compilation, the commitment to the whole circuit, and the wiring data used in verification do not change across requests of the same kind. We first thought this mostly saved compilation. Instrumenting the functions directly showed the main cost was the commitment: at depth-24 membership, compilation took about 7.9 ms, the circuit commitment about 105 ms, and proof generation about 41.5 ms [6]. Reusing the preparation shortened the per-request proving path by 3.46 to 4.45x, depending on the operation [6].
Fifth, each request gets its own proof, bound to the original request. We ruled out aggregate proofs that fold many requests into one from the start. The moment requests are folded together, the statement changes, and it needs a different circuit, a different model and a different audit. Independent jobs that share one preparation run in parallel instead, and the number of workers cannot reach the proof bytes.
The contract is that batched output equals one-by-one output bit for bit, and the model proves the same property as a batch-preservation theorem [5]. The receiver checks the complete proof strictly against the original request and rejects it if the root, the value digest or the circuit identifier differ from the request, or if bytes trail the proof [6].
The December article said a state oracle must prove linked state transitions, while the engine produces an independent proof per request. The two sit on different layers. An update proof binds the previous root and the next root together and states that the transition between them is valid. The order in which those transitions form a chain is decided outside the proof, by whoever adopts roots in sequence: sequencing and state commitment. The causal link did not disappear. It moved into the order of roots outside the proof.
3. Where Our Expectations Broke
Looking back, many of the StateSync-GKR prover's distinctive features were not designed in advance. They arose as responses to places where something went wrong, and the two earlier articles mark where each expectation stood.
3.1 The Memory Problem the December Article Left Open
The December article noted that a GKR prover has to hold the full evaluation of the circuit in memory, so memory management would be a challenge for large batches. When we measured an early build of the StateSync-GKR prover, the bottleneck was the sumcheck oracle. In the dense method, which expands a factor table the size of the input pairs at every layer, auxiliary memory grew fourfold each time the circuit width doubled.
We replaced the oracle with Libra's two-phase sparse booking [2]. The January article had expected sparsity from the many empty leaves; what the engine actually saved on was the sparsity of the multiplication-gate lists. The dense method stayed as a test-only reference, bound to produce bit-identical proofs, so that a faster engine producing a different proof is ruled out by construction.
Comparing the two oracles inside the same prover driver, the sparse oracle's memory grew about twofold per doubling of width against the dense oracle's fourfold, and on a two-layer mixed circuit of width 4096 the sparse oracle used 3,242.41x less additional requested memory during proving and 89.46x less peak resident memory for the whole process [6]. Under a 3 GiB memory cap, the dense oracle was killed at width 8192 before returning a proof, while the sparse oracle returned proofs up to width 65,536, the largest we tested, peaking at about 260 MiB of resident memory [6]. The comparison is with our own dense reference, on a general mixed circuit.
3.2 The Verification Cost Hidden in the Wiring Table
One reason to choose GKR is cheap verification. Once the real Poseidon2 circuit was in place, the cost of that cheap verification had gathered in an unexpected spot: the verifier scanning the wiring table gate by gate. Rewriting the circuit into uniform blocks duplicated node permutations and made proving more expensive, so we dropped it. We read the closed form of the wiring polynomials from the structure of the compiled circuit instead. State synchronization circuits repeat the same shape regularly, which is what makes this derivation possible.
The deriver uses the circuit's markings only as hints, rechecks every gate, and falls back to the exact sparse path when they do not match. A wrong hint costs speed and never soundness. When verifying the same proof with preparation in place, wiring derived from structure was 10.80 to 23.68x faster than table wiring [6], and on the formal side a lemma that the derived and tabulated wiring polynomials are equal supports the substitution [5].
3.3 From Cached Intermediates to Reused Preparation
The January article expected that when consecutive updates share a path, intermediate values of an earlier proof could be cached and reused, and it also sketched proving several updates as one instance or gathering them recursively. Measurement showed that what requests can structurally share is limited to compilation, the commitment and the wiring data. Oracle tables, transcripts and witnesses are tied to each request's challenges and inputs. So reuse settled as reuse of the preparation, and batching settled as independent jobs that share one preparation. A plausible optimization such as a memory pool was rejected by measurement showing that allocation was a negligible share of the profile.
The external layer changed as well. In place of the outer verification that the December article tied to one proof system and one rollup stack, a backend-agnostic external succinct wrapper now carries zero knowledge and external verification (the inner GKR proof is not itself zero-knowledge). The public example runs the GKR verification relation inside a general-purpose zkVM's succinct proof and has that proof checked on an external verification network's testnet. It is component evidence and does not mean the full settlement path is complete.
4. Making Acceptance Mean Validity
In this system, an accepting verdict from the StateSync-GKR prover's verifier becomes an action. An accepted update fixes a new root, and assets move on top of it. So the question we held was one step ahead of GKR's own soundness. GKR soundness speaks only about the circuit's output claim. What we needed to know was whether the circuit expresses the intended state transition exactly.
4.1 How the Leaf Encoding Became a Lemma
Before the public release, early in development, the in-circuit hash position held an algebraic placeholder documented as having no collision resistance. Right after we replaced it with real Poseidon2, our internal adversarial review found a critical defect. The way variable-length leaf records were folded into fixed-width input was not injective, so two different leaves folded into the same hash input. Leaf-hash collisions arose without breaking the hash, and both checking paths accepted a forged membership proof for a record never committed to the tree. What had covered the defect until then was the placeholder's own caveat, "no collision resistance". Swapping a placeholder for the real component also removed the caveat that had been hiding the defect.
The fix was to bind the length into the hash input. A leaf record is laid out as tag, length, payload and zero padding in a lossless fixed-width input, and records over the bound are returned as type-level errors. The leaf hash now runs through more permutations, the circuit and the proof got heavier, and we paid that cost. This was where the rule of choosing soundness when soundness and performance collide became a price actually paid. The public engine contains only the fixed encoding, and the formal verification paper carries a machine-checked lemma that this encoding is injective [5]. The lemma reduces a leaf-hash collision to a collision of the underlying sponge; it does not prove the sponge collision-resistant.
Binding the length into the leaf input made the encoding injective.
4.2 From the Compiler to the GKR Bound
The Isabelle/HOL development proves that acceptance by the compiled circuit coincides, in both directions, with validity of membership, non-membership and update. On top of the sumcheck theorem formalized in the Archive of Formal Proofs (AFP) [4], it builds a GKR assembly model with layer reduction and wiring-polynomial extension, proves an upper bound on the probability that a false output claim passes, and composes the two so that a semantically invalid transition is carried to that bound [5]. The bound holds with denominator p⁴ over the exact degree-4 extension of KoalaBear from which the implementation actually samples challenges, under the stated challenge assumptions [5]. That batched output equals one-by-one output is a theorem inside the same model.
4.3 What a Clean Build Did Not Say
The longest-lasting lesson was that a theorem can be vacuous. When we thought model verification was done, the build was clean and there were zero unfinished proofs (sorry). Then one requirement, to satisfy every assumption with a concrete KoalaBear instance, exposed that the compiler-side assumption set could not be satisfied. It forced both specification-vector lengths to be powers of two while the two lengths provably lay strictly within a factor of two of each other, and no two distinct powers of two do.
The two headline theorems on that assumption set were vacuously true [5]. A theorem prover answers only whether a theorem follows from its assumptions. Whether anything satisfies those assumptions, and whether a file was actually in the build, a person has to ask separately. Several instance files we believed finished had never been registered in the build and so had never been checked; now every theory is registered so that none escapes the build [5]. Since then we count activating every assumption set with a concrete instance as part of being done.
Two distinct powers of two, yet strictly within a factor of two: no such pair.
The connection to the StateSync-GKR prover's Rust implementation is partial. We put Creusot and Why3 contracts on selected Rust functions and machine-checked structure and types, arithmetic and indices, and the development record shows 37 deliberate contract distortions, each rejected by the checker [5]. The connection stopped where the tool cannot yet go, and we did not rewrite the frozen core to fit that wall. A conditional theorem states that the shipped verifier's acceptance record satisfies the model's event, but it takes as an unproved premise that Rust execution values correspond to model values [5].
The mechanized chain runs from transition semantics to the GKR bound under the stated challenge assumptions, and to the shipped verifier under the stated premise. The Fiat-Shamir transform that makes the protocol non-interactive is treated as a cryptographic assumption and is not part of the mechanized chain. Sumcheck itself has an earlier mechanization in Isabelle/HOL [4].
The link our development covers is composing, in one prover, a compiler proven to make circuit acceptance equivalent to state-transition validity with the soundness bound of a GKR assembly model. 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 [5].
5. What the Measurements Taught Us
The ratios in the sections above are all internal comparisons with a named baseline: memory against the dense reference, verification against table wiring, reuse against a path that prepares afresh every time. What the measurements taught us most came after that, in the boundaries of a number.
On a 192-physical-core AWS bare-metal server, measuring proving alone at depth 24 with batches of 768 and 192 workers, the StateSync-GKR prover produced 3,207.74 internal proofs per second for membership, 2,930.85 for non-membership and 2,092.03 for update [6]. Adding parallel witness generation to the same computation gave 2,881.55 per second for membership, and a separate run that added encoding and acceptance of the encoded proof gave 1,593.17 [6]. These numbers come from different hosts and measurement intervals and cannot be subtracted or summed. Side by side, one thing is plain: an engine's speed is a different number depending on where you stop the clock.
What a caller of the StateSync-GKR prover actually receives is none of those numbers. In a test that sends requests from another machine, receives complete proofs back over TCP and accepts them strictly against the original request, one 48-core server took 500 requests per second, evenly mixed across the three operations, for 15 minutes and accepted all 450,000 within 500 ms [6]. A 192-core server, taking 1,150 requests per second for 60 seconds, accepted all 69,000 within 2 seconds.
Of those, 48,553 (70.37%) finished within 1 second; the queue rose from 562 to 1,559 over the input period and drained its remainder in 1.394 seconds after input stopped [6]. The 60 seconds are the input period, and the completion-window rate of that run was about 1,124 per second. The rates of 500, 1,000 and 1,150 are loads we varied in testing; they are not processing limits set for the product.
The observation we held onto longest as researchers came from that test's CPU record. While taking 1,150 requests per second, only about 78 of 192 cores were busy on average, yet the queue grew. Rereading the source showed why. A worker computed one batch of one kind at a time and started the next batch only after finishing hashing, response building, writing and logging for every result.
What accumulated the delay was less the proof computation than the serial path that returns results. Splitting the same total resources into two 48-core servers handled 1,000 per second all within 500 ms, while one 96-core server built a queue and its 99th-percentile latency exceeded 2.5 seconds [6]. Similar CPU usage did not mean similar response latency. Once the prover became fast, the delay moved outside the prover.
We did not run a same-condition comparison with a SNARK or STARK baseline on the same workload, and an attempted comparison with another public GKR implementation did not yield a fair comparison at our sizes, so we report no ranking [6]. The throughput we measured is that of independent inner GKR jobs. Throughput per unit of primary finality, including consensus and state commitment, and the cost of the external wrapper are not in these numbers.
Conclusion
The December claim was that GKR is a precondition for a state oracle to exist. Building the StateSync-GKR prover gave us no reason to withdraw it. What we learned is what has to stand on top of that precondition before there is an engine: a sparse oracle whose memory follows the circuit's width, derived wiring that keeps verification cheap, reuse that never repeats the same preparation, independent proofs the worker count cannot reach, a leaf encoding that sends hash collisions back to the sponge, and a machine-checked chain from acceptance to validity. Failures announced many of these before any plan did. The habit of telling verified from fast may be the most valuable thing this work gave us.
Open questions remain.
- Can the premise that Rust execution values correspond to model values be discharged for the compiled program, or does that correspondence have to take another checkable form?
- The current verifier recomputes leaf and path hashes from the witness [6]. Can a verifier that checks from public inputs alone, without seeing the witness, be obtained on the same circuit structure?
- Compared against SNARK and STARK baselines on the same workload, and as approaches such as folding mature, where does the boundary of the precondition move?
- How does throughput per unit of primary finality, including consensus and state commitment, relate to the inner proof throughput we measured?
References
- [1] Goldwasser, S., Kalai, Y. T., & Rothblum, G. N. (2015). Delegating Computation: Interactive Proofs for Muggles. Journal of the ACM, 62(4). https://doi.org/10.1145/2699436
- [2] Xie, T., Zhang, J., Zhang, Y., Papamanthou, C., & Song, D. (2019). Libra: Succinct Zero-Knowledge Proofs with Optimal Prover Computation. CRYPTO 2019. https://doi.org/10.1007/978-3-030-26954-8_24
- [3] Thaler, J. (2013). Time-Optimal Interactive Proofs for Circuit Evaluation. CRYPTO 2013. https://doi.org/10.1007/978-3-642-40084-1_5
- [4] Garvía Bosshard, A., Bootle, J., & Sprenger, C. (2024). Formal Verification of the Sumcheck Protocol. IEEE CSF 2024. https://doi.org/10.1109/CSF61375.2024.00014
- [5] Kim, J. (2026). StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification. arXiv:2610.05335. https://arxiv.org/abs/2610.05335
- [6] Kim, J. (2026). StateSync-GKR: Design and Evaluation of a Reusable Sparse GKR Engine. arXiv:2610.14849. https://arxiv.org/abs/2610.14849
- [7] Grassi, L., Khovratovich, D., & Schofnegger, M. (2023). Poseidon2: A Faster Version of the Poseidon Hash Function. AFRICACRYPT 2023. https://doi.org/10.1007/978-3-031-37679-5_8
- [8] Plonky3 contributors. (2026). Plonky3 v0.4.3. https://github.com/Plonky3/Plonky3/releases/tag/v0.4.3