Get started
Introduction
StateSync-GKR is a GKR and sumcheck proof engine in Rust, built for state synchronization and machine-checked from state semantics to verification. Start here to see what it does, who it is for and how these docs are organized.
StateSync-GKR is a Rust implementation of the GKR protocol and multilinear sumcheck, developed by Oraclizer Labs. It was built for state synchronization, where one system has to prove to another that a record is present, absent or correctly changed, and its name comes from that origin. Its sparse-Merkle frontend compiles those state operations into layered arithmetic circuits, so you can prove and verify that an authenticated state tree contains a record, does not contain a record, or changed one leaf from an old root to a new root. The protocol and sumcheck layers do not depend on that frontend, so the same engine can prove other computations written as layered circuits.
The path from state semantics to GKR verification is machine-checked in Isabelle/HOL, and a refinement theorem connects the shipped Rust verifier to that model under stated conditions. Formal verification explains what is proved and what is not.
What you can do with it#
| Task | Entry point | Guide |
|---|---|---|
| Prove and verify membership, non-membership or a single-leaf update | StateSyncProver with a SyncRequest | Proving state operations |
| Prepare a circuit once and reuse it for every request of the same kind | prepare, prove_sync_op_prepared, verify_sync_op_prepared | Prepared execution |
| Run independent proof jobs across CPU cores, one proof per job | make_job_prepared, prove_batch_parallel | Batching and parallelism |
| Send a proof to another process and verify the received bytes | encode_sync_result, verify_encoded_sync_op | Encoding and transport |
| Build a frontend for a different arithmetic circuit | The sumcheck and gkr modules | Custom frontends |
| Check a supplied sparse-Merkle path without creating a GKR proof | compiler::smt_valid_native | API reference |
In separate controlled comparisons against its own internal references, StateSync-GKR used about 89 times less peak process memory on a generic two-layer test circuit and verified the same proof up to 23.68 times faster with derived instead of table wiring. Each figure has its own reference, workload and timer boundary. See Benchmark results before you reuse a number.
Who it is for#
- Blockchain and infrastructure developers who need to prove or verify the contents of a sparse Merkle tree and single-leaf changes to it.
- Engineers who want a reusable GKR and sumcheck core for their own circuit frontend.
- Reviewers, auditors and researchers who need to see what is machine-checked, what is measured and what is assumed.
Version and status#
- Docs version line: 1.1. These pages describe the 1.1 component line.
- Current version: 1.1.1, the licensing revision of 1.1.0. Release history is in the changelog.
- Packages: The Cargo packages carry version
0.1.0-devand are not published to crates.io. Integrate by pinning an exact source revision. See Versioning. - License: The current official distribution is licensed under the Business Source License 1.1. Non-production use, such as research, development and testing, is free. Production use that generates proofs, embeds or redistributes the proving functionality in a product or service, or offers proof generation to third parties requires a commercial license; production use solely to verify proofs stays free. See Licensing.
- Formal verification: The compiler and protocol models are machine-checked in Isabelle/HOL, and a refinement theorem connects the shipped Rust verifier to them under stated conditions. See Formal verification, and read Trust boundaries before you deploy.
Fastest path to a first proof#
- Install the pinned Rust toolchain: Installation.
- Run the bundled example: Quickstart.
- Build requests from your own state: Proving state operations.
- Reuse preparation for repeated requests: Prepared execution.
The Quickstart example builds one synthetic membership request, proves it, verifies the honest proof and checks that a tampered copy is rejected. A successful run prints:
honest-proof=PASS
tampered-proof=REJECTED
secondary-finalized=falseThe last line records that the local example makes no finality claim on any destination chain.
How these docs are organized#
| Section | What it covers | Pages |
|---|---|---|
| Get started | Toolchain setup, a first proof and the repository layout | Installation, Quickstart, Project layout |
| Concepts | How GKR reduces a circuit, how sparse-Merkle state is represented, how circuits are layered and how a proof moves from request to acceptance | How GKR works, Sparse-Merkle state, Circuits and layers, Proof lifecycle |
| Guides | Task-oriented instructions for proving, reuse, parallel jobs, transport, custom frontends, integration, tuning and diagnosis | Proving state operations, Prepared execution, Batching and parallelism, Encoding and transport, Custom frontends, Production integration, Performance tuning, Troubleshooting |
| Reference | Public API, configuration values, the encoded proof format, error types and terminology | API, Configuration, Wire format, Errors, Glossary |
| Benchmarks | Measured memory, verification, batch and serving results, and how they were measured | Results, Methodology |
| Security and assurance | What the component checks and assumes, what the formal proofs cover and how to report a vulnerability | Trust boundaries, Formal verification, Security policy |
| Project | License terms, release history, version numbers, citation and common questions | Licensing, Changelog, Versioning, Citing, FAQ |
Get help#
- Reproducible defects, documentation errors and focused design proposals go to issues (opens in a new tab) in the source repository.
- Suspected vulnerabilities must be reported privately. Follow the Security policy.
- For a commercial license, contact us through StateSync-GKR licensing.
- For a product overview, see the StateSync-GKR home page.