The proof engine for state synchronization
Lighter to prove.
Faster to check.
StateSync-GKR proves that a record is present, absent or correctly changed under a published state root, and its GKR core extends to other layered computations. The path from state semantics to verification is machine-checked in Isabelle/HOL, with a refinement theorem tying the shipped Rust verifier to it under stated conditions.
less memory to generate the same proof
Peak process RAM, 89.46× lower than the engine's own dense reference. Same circuit, field and prover driver; two-layer mixed circuit of width 4,096.
faster to verify the same proof, at the deepest tree tested
The same proof checked with derived instead of table wiring, tree depth 32. Across operations and depths 24 to 32 the gain is 10.80–23.68×. Preparation is outside the timer.
Measured, not projected
Every number comes
from a controlled run.
Each chart is measured against StateSync-GKR's own reference and states the conditions it ran under. The engine paper reports the full method behind every figure.
The wider the circuit, the larger the saving.
Same engine, circuit, field, transcript and prover driver; only the layer representation changes. Two-layer mixed circuit, three processes per point, one job pinned to one core. Below width 256 the two are about the same; the gap opens as layers widen. The dense reference is StateSync-GKR's own implementation of the conventional dense layout.
The advantage grows as the tree gets deeper.
Same proof and request, verified with derived wiring instead of explicit table wiring, which is already sparse. Each bar is the median of five process-level medians of 300 paired calls. The timer covers the whole typed verification call, including path hashing; preparation, proving, encoding and transport are outside it.
Fifteen minutes at a steady 500 requests a second.
One 900-second run on a 48-core server: 48 workers, batch cap 48, a 1:1:1 mix of membership, non-membership and update at depth 24, offered at 500 per second, with a separate 16-core frontend. Latency ends when the complete proof is cryptographically accepted against its original request.
Above 1,000 requests a second, still inside two seconds.
One 60-second window at 1,150 per second on a 192-core server (192 workers, batch cap 192), all 69,000 requests accepted within 2 seconds, slowest 1.598 s, finishing at 1,123.89 per second including the drain. The queue grew during the window and 70.37% met 1 second. Three runs at 1,000 per second met 1 second for all 180,000 requests.
Inside the engine
Sparse where it counts.
Shared where it repeats.
Two design rules explain the memory and repeated-setup results. Store only the gates a circuit actually has, and prepare everything that stays the same once, so each request pays only for its own witness and proof.
Keep the gate list sparse.
The dense reference builds six square tables of input pairs for every layer, and that is where its memory goes. The sparse prover records only the gates that exist, in two passes.
Storage grows with the square of the input width.
Two-phase booking avoids the square tables.
Prepare once. Prove many.
The circuit, its derived wiring and its commitment are built once per operation and configuration. Every request still gets its own witness, transcript and proof.
Own witness
Own transcript
Proof AOwn witness
Own transcript
Proof BOwn witness
Own transcript
Proof CNine mechanisms
Each advantage has
a mechanism behind it.
Some mechanisms are measured directly. Others follow from the source structure, from rejection tests or from the formal model. Each one names the evidence it rests on.
More work fits in the same memory.
The prover books only the gates a layer actually has, instead of six square tables of input pairs. On a two-layer mixed circuit of width 4,096, peak process memory falls 89.46-fold against the engine's dense reference.
Verification skips repeated work.
Regular circuit connections are derived from their structure instead of looked up. Prepared verification of the same proof runs 10.80 to 23.68 times faster, and the formal model states the equivalence to explicit wiring.
Hash rounds stay compact.
Native cube gates and fused affine steps express the supported hash rounds with fewer intermediate wires and layers. This is a structural property of the circuit.
Proofs grow slowly with depth.
Path constraints widen the circuit within the same layer schedule. From tree depth 24 to 32 the inclusion proof grows by about 2.93 percent, while the total work still grows with the path.
Setup is paid once.
Circuit, derived wiring and commitment are prepared once per operation and configuration. At depth 24, per-request proving time is 3.46 to 4.45 times lower than preparing fresh for every request.
Each proof keeps its own lane.
Caller-sized worker pools run independent proof jobs and keep their input order. Parallel encoding and checking make a complete prepared local batch 9.71 to 10.71 times faster than serial output handling.
Deleted and never-written stay distinct.
Empty, occupied and tombstone leaves stay distinct, so a deleted record is never confused with one that never existed, and insert, update, delete and restore keep their meaning. An absence proof accepts either an empty or a deleted slot.
A proof answers only its own request.
The encoded verifier checks the original request, the complete proof and its settings together. Malformed bytes and proofs for a different request are rejected; only a complete proof that checks out against the original request is accepted.
A core you can build on.
The layered-circuit core is separate from the sparse-Merkle compiler. A new frontend supplies its own circuit and inputs, and settles the final input checks the core leaves to it.
Where it fits
Built for systems
that prove state.
Anywhere a record has to be shown present, absent or correctly changed against a committed root, and anywhere a computation can be written as a layered circuit.
Registers and ledgers
Show that a holder is on a register, that an address is absent from a restricted list, or that a holding changed correctly, against a published root.
State commitments
Prove membership, absence and single-record updates for rollups, app-chains and synchronization layers that keep their state in the engine's sparse Merkle tree.
Authenticated data
Give a key-value store or registry a checkable answer to whether a key is present, absent or updated, checked against a root the client already trusts.
Your own circuit
Use the sumcheck and GKR core directly for a computation written as a layered circuit, from machine-learning arithmetic to data pipelines, through a frontend you build.
Formal verification
Machine-checked
from state to proof.
Every link from a state change to an accepted proof is a theorem the Isabelle/HOL proof checker accepts, and a refinement theorem connects the shipped Rust verifier to that model under stated conditions.
- 01
State semantics
Membership, non-membership and updates are given a formal meaning.
- 02
Circuit compiler
The compiled circuit accepts exactly the valid state operations.
- 03
GKR soundness
A false claim survives only within a proved bound, in the exact field the verifier uses.
- 04
Composition
One bound covers the whole path from a state operation to its proof.
- 05
Rust verifier
A refinement theorem ties the shipped verifier's acceptance to the model, under stated conditions.
For developers
Three commands
to your first proof.
The quickstart builds one membership request, proves it, verifies it and then shows a tampered proof being rejected. The last line confirms that nothing is settled on any chain; everything runs locally. The documentation takes you from there to batching, encoding and integration.
$ git clone https://github.com/Oraclizer/statesync-gkr.git
$ cd statesync-gkr
$ cargo run --release --locked --example state_sync_prove_verify
honest-proof=PASS
tampered-proof=REJECTED
secondary-finalized=falseLicensing
Free to build and test.
Commercial for production.
The source is available under the Business Source License 1.1. Research, development and testing are free. Generating proofs in production requires a commercial license; verifying proofs stays free, even in production.
Research and development
Study, modify, test and benchmark the engine in any non-production setting.
Verifying proofs in production
Run, embed or distribute the verifier in production solely to check proofs.
Generating proofs in production
Production proving, embedding the prover in a product or service, or proving for others.