Skip to content

protocol.md

Latest commit

 

History

History
127 lines (90 loc) · 3.69 KB

protocol.md

File metadata and controls

127 lines (90 loc) · 3.69 KB
Raw

Tiny STARK Protocol

This document describes the generic protocol implemented in this repository. It does not define a concrete proving statement by itself. Instead, statement code supplies a StarkStatement containing:

  • a statement id
  • a witness trace
  • public input labels and values
  • expression-based AIR constraints

The protocol turns that statement into commitments, transcript challenges, query openings, a composition codeword, and a toy FRI proof.

For a visual map, see the STARK Protocol Flow Diagram. For a higher-level theory overview, see STARK Layers Theory.

Domains

The trace domain H is a power-of-two multiplicative subgroup of the Goldilocks field. The composition domain is a larger power-of-two subgroup:

|D| = |H| * blowupFactor

The implementation samples query points from D \ H, because quotient denominators vanish on the original trace domain.

Commitments

The prover commits to:

  1. Trace low-degree-extension rows.
  2. Composition codeword values.
  3. Each FRI folded codeword.

All commitments are binary Merkle trees with SHA-256. Field elements are encoded as canonical little-endian 64-bit Goldilocks values.

Composition Polynomial

Each AIR boundary or transition expression becomes one quotient term. If a statement has m quotient terms, Fiat-Shamir samples m random coefficients and the prover combines them into one composition polynomial:

C(x) = alpha_0 * q_0(x)
     + alpha_1 * q_1(x)
     + ...
     + alpha_{m-1} * q_{m-1}(x)

The verifier checks sampled values of C(x) by recomputing them from opened trace LDE rows at x and g * x.

Generic AIR Programs

The air/program package contains a tiny expression language for AIR constraints. A statement can define formulas over current-row and next-row trace registers:

boundary:   current.column - public_value
transition: next.column - current.column

ProgramAir evaluates those formulas on trace rows, while ProgramComposition converts the same formulas into quotient polynomials.

The separation is:

  • io.tinystark.protocol owns proof generation, verification, transcript order, proof bytes, and query openings.
  • Future statement packages own traces, public input labels, and AIR formulas.

Fiat-Shamir Order

The transcript order is:

  1. protocol label and public inputs
  2. trace root
  3. composition challenges
  4. composition root
  5. FRI folding challenges and folded roots
  6. query indices

This means query indices are sampled only after all codeword commitments are fixed.

Query Checks

For each sampled query index, the proof opens:

  • trace row at x
  • shifted trace row at g * x
  • composition value at x
  • FRI folding path for the composition codeword

The verifier checks:

  • every Merkle opening matches its root
  • opened trace rows have the right width
  • the composition value matches the AIR quotient formula
  • each FRI folding step is locally consistent
  • the final FRI layer is constant

Proof Bytes

StarkProofCodec encodes generic proof objects into a deterministic binary format. The format is versioned with a magic header, rejects trailing bytes, and rebuilds Merkle proofs through normal validation.

What "Finished" Means Here

For this repository, the reusable educational STARK protocol is complete enough to:

  • generate a proof for a supplied StarkStatement
  • serialize it
  • read it back
  • verify it against statement AIR
  • reject malformed or tampered proofs in tests

It is not a production STARK. A production system would need careful parameter selection, optimized polynomial evaluation, audited domain separation, stronger FRI variants, broader AIR support, side-channel review, and a security analysis.