starlib

A Lean 4 library for formally verifying succinct non-interactive arguments of knowledge (SNARKs), with a focus on modular and composable specifications and security proofs.

This project is derived from ArkLib and continues development under a new name.

• 🌐 Site & docs: https://nktkt.github.io/starlib/
• 📘 Blueprint (web): https://nktkt.github.io/starlib/blueprint/
• 📄 Blueprint (PDF): https://nktkt.github.io/starlib/blueprint.pdf
• 🚀 Quickstart: docs/getting-started.md
• 🔱 Fork notes: docs/FORK.md

Overview

starlib aims to formalize the information-theoretic core of modern SNARKs — Interactive Oracle Reductions (IORs) — and to provide:

• Executable specifications of proof-system protocols, built modularly via composition and lifting interfaces.
• Proofs of completeness and round-by-round knowledge soundness via generic theorems about composition and lifting.
• A pathway from IORs to non-interactive arguments via the (interactive) BCS transform and the Fiat-Shamir transform (duplex-sponge variant).

In the longer term, the goal is to verify functional equivalence between executable specifications and extracted code from production Rust implementations of the same protocols.

Library Structure

The core is a mechanized theory of Interactive Oracle Reductions, located under Starlib/OracleReduction/:

1. An IOR (OracleReduction in the formalization) is an interactive protocol between a prover and a verifier that reduces a relation R₁ on public statement and private witness to another relation R₂.
2. The verifier does not see prover messages in the clear, but can make oracle queries against a specified oracle interface (e.g. vector entries, polynomial evaluations).
3. IORs can be sequentially composed when relations are compatible (R₁ ⇒ R₂, R₂ ⇒ R₃) and can be lifted from a simple context into a larger virtual context. These operations let us construct protocols such as Plonk from sub-routines (zero-check, permutation check, quotienting) and derive end-to-end security from component security.
4. After specifying an IOR, we obtain a non-interactive argument via the BCS transform (replacing oracle messages with commitments plus opening arguments) followed by Fiat-Shamir.

Proof systems built on top of this theory live under Starlib/ProofSystem/, with commitment schemes under Starlib/CommitmentScheme/.

Repository Layout

• Starlib/Data/ — reusable mathematics, coding theory, polynomials, supporting definitions.
• Starlib/OracleReduction/ — core IOR abstractions and security theory.
• Starlib/ProofSystem/ — protocol formalizations built on the core.
• Starlib/CommitmentScheme/ — commitments and opening arguments.
• Starlib/ToMathlib/ — local extensions intended for upstreaming.
• blueprint/ — design documents and bibliography.
• scripts/ — repository utilities (build, lint, validation).

Active Areas

Components currently under active development include:

• The Sum-Check Protocol
• Spartan
• Merkle Trees
• FRI and coding-theory prerequisites
• STIR and WHIR
• Binius

Getting Started

Prerequisites: a working Lean 4 / Lake toolchain via elan. The pinned version lives in lean-toolchain and is picked up automatically.

git clone https://github.com/nktkt/starlib.git
cd starlib

# Fetch precompiled Mathlib / dependency caches (saves ~30 min on first build)
lake exe cache get

# Build the whole library
lake build

# Routine local validation (mirrors what CI runs)
./scripts/validate.sh

Optional checks:

./scripts/validate.sh --lint    # Lean style linting
./scripts/validate.sh --docs    # Build doc-gen4 API docs
./scripts/validate.sh --site    # Build blueprint + website output

See docs/getting-started.md for the full on-ramp.

Using starlib as a dependency

Add the library to another Lean 4 project's lakefile.toml:

[[require]]
name = "Starlib"
git = "https://github.com/nktkt/starlib"
rev = "main"   # pin to a specific commit SHA in production

Then import the modules you need:

import Starlib.OracleReduction.Composition
import Starlib.ProofSystem.Sumcheck.Basic

The Lean toolchain version of your project must match the one pinned in lean-toolchain.

Dependencies

• Mathlib — Lean 4 mathematical library.
• VCV-io — verified computation framework.
• CompPoly — computational polynomial primitives.
• doc-gen4, checkdecls — documentation and declaration linting.

Contributing

Contributions are very welcome. Before opening a pull request, please:

1. Read CONTRIBUTING.md for style, naming, and citation conventions.
2. Make sure ./scripts/validate.sh passes locally.
3. If you added or removed .lean files under Starlib/, regenerate the umbrella import file with ./scripts/update-lib.sh.

Issue and pull request templates live under .github/.

License

See LICENSE for license terms. Upstream attribution and authors are listed in AUTHORS.

Acknowledgements

starlib builds directly on the work of the ArkLib project by the verified-zkEVM effort. Many thanks to the original authors and contributors.