stark-refined

A STARK prover and verifier, written from scratch in Python, that convinces you u₂₅₅ = C without you ever recomputing the sequence.

Given u₀ = c₀, u₁ = c₁ and the recurrence uₙ = uₙ₋₁ + uₙ₋₂ over a finite field, this project produces a short cryptographic proof that a specific u_{n-1} equals a claimed value C. The verifier checks it in milliseconds, looking at a handful of points, and never runs the recurrence.

Zero runtime dependencies. matplotlib and pytest are needed only for the figures and the test suite.

$ python -m stark_refined demo --n 256

  ==> u_255 = 1717986937

  trace length          n = 256
  LDE domain size       |D| = 2048
  FRI layers                8
  heuristic soundness       ~96 bits

Proving ...     212 ms      196 KiB
Verifying ...   ACCEPT      11.6 ms      (18x faster than proving)

---

Table of contents

• Quick start
• What a STARK actually is
• The protocol, step by step
• Architecture
• Results
• Design decisions
• Testing
• Command reference
• Known simplifications
• References

---

Quick start

git clone https://github.com/GoulvenBonmarchand/stark-fibonacci.git
cd stark-fibonacci
python -m pip install -r requirements.txt      # matplotlib + pytest, optional
PYTHONPATH=src python -m stark_refined         # demo + forgery gallery + benchmarks

That single command proves a claim, verifies it, tries seven forgeries and watches them all get rejected, then runs the full benchmark sweep and writes four figures plus benchmarks/results.json. Expect roughly 90 seconds — most of it spent in the deliberately slow O(n³) baseline.

On Windows PowerShell:

$env:PYTHONPATH="src"; python -m stark_refined

Prefer a proper install? pip install -e . puts a stark-refined command on your PATH and removes the need for PYTHONPATH.

Programmatic use:

from stark_refined import FibonacciClaim, ProofParameters, prove, verify

claim  = FibonacciClaim.from_sequence(c0=1, c1=3141592, trace_length=256)
proof  = prove(claim, ProofParameters(blowup=8, num_queries=32))

open("proof.json", "w").write(proof.to_json())
assert verify(proof)          # ~12 ms, regardless of how long the trace was

---

What a STARK actually is

A STARK (Scalable Transparent ARgument of Knowledge) lets a prover convince a verifier that a computation was performed correctly, where:

• Scalable — verification cost is polylogarithmic in the size of the computation. Proving a 4096-step trace costs the verifier 17 ms; proving a 16-step trace costs 7 ms.
• Transparent — no trusted setup. The only cryptographic assumption is that the hash function behaves like a random oracle. No pairings, no toxic waste, and (unlike pairing-based SNARKs) plausibly post-quantum.
• Argument of Knowledge — soundness holds against computationally bounded provers, and a valid proof implies the prover actually knows a witness.

The single idea underneath everything: turn a claim about a computation into a claim about the degree of a polynomial, then test that degree by random sampling. Degree is a global property, so a local spot-check catches a global lie — that is the whole trick, and everything else is machinery to make it efficient.

---

The protocol, step by step

1. Arithmetisation — computation becomes algebra

Write the execution trace u₀ … u_{n-1} and interpolate it into a single polynomial f of degree < n over the multiplicative subgroup G = ⟨g⟩ of order n, so that f(gⁱ) = uᵢ.

Because G is multiplicative, "the next row" is just "multiply the argument by g". The three-term recurrence collapses into one polynomial identity:

f(g²x) − f(gx) − f(x) = 0    for all x ∈ {g⁰, …, g^{n-3}}

2. Constraints become divisibility

A polynomial vanishes on a set S if and only if it is divisible by Z_S(x) = ∏_{s ∈ S}(x − s). So each constraint becomes a division that succeeds only when the constraint holds:

#	quotient	degree
q₀	(f(x) − c₀) / (x − 1)	n−2
q₁	(f(x) − c₁) / (x − g)	n−2
q₂	(f(g²x) − f(gx) − f(x)) · (x − g^{n-2})(x − g^{n-1}) / (xⁿ − 1)	1
q₃	(f(x) − C) / (x − g^{n-1})	n−2

Note q₂'s denominator. The recurrence must not be enforced on the last two rows — there is no u_n — so the two offending factors of xⁿ − 1 are multiplied back into the numerator. Forgetting this is the single most common bug when implementing a STARK by hand: the division stops being exact and the prover fails with no obvious cause.

The identity Z_G(x) = xⁿ − 1 is why the trace domain is a subgroup: evaluating a product of n linear factors costs O(n), evaluating xⁿ − 1 costs O(log n).

3. Random linear combination with degree adjustment

The verifier does not want to run four separate low-degree tests. It draws α₀…α₃, β₀…β₃ from the transcript and the prover commits to a single composition polynomial:

CP(x) = Σᵢ (αᵢ + βᵢ·x^{eᵢ}) · qᵢ(x)       where eᵢ = (n−1) − deg(qᵢ)

The βᵢ·x^{eᵢ} factors are degree adjustment, and they are not decorative. Without them a cheating prover could hide a too-high-degree q₂ behind a legitimately low-degree q₀: the sum would still look fine. Multiplying every quotient up to the same target degree n − 1 means one FRI run bounds all four at once. (STARK-101 omits this; production systems do not.)

4. Low-degree extension and commitment

CP is evaluated on a coset D = 5·H where |D| = n · blowup and H is the subgroup of order |D|. Two things are happening:

• Redundancy. With blowup = 8 the code rate is 1/8. Two distinct polynomials of degree < n agree on at most n of the 8n points, so they differ on at least 7/8 of the domain. Spot-checking a random point catches a cheat with probability ≥ 7/8.
• Disjointness. 5 generates 𝔽ₚ*, which is strictly larger than H, so 5 ∉ H and D ∩ G = ∅. No quotient denominator can vanish on D — the coset offset exists precisely to prevent a division by zero.

Merkle-root the evaluations. The prover is now bound to a specific vector before it has seen a single query.

5. FRI — proving low degree without reading the polynomial

Split by parity of exponent:

f(x) = f_even(x²) + x·f_odd(x²)

and note both halves are recoverable from two evaluations:

f_even(x²) = (f(x) + f(−x)) / 2
f_odd (x²) = (f(x) − f(−x)) / (2x)

Given a random β, the folded polynomial f′ = f_even + β·f_odd has half the degree and lives on a domain of half the size (because x ↦ x² maps a coset two-to-one onto a coset of half the size). Repeat log₂ n times and what is left is a constant, which the prover sends in the clear.

The verifier picks random indices and, at every layer, checks that the three values it opened satisfy the folding relation. A prover whose word is δ-far from the code survives all of this with probability roughly (1 − δ)^queries.

6. Fiat–Shamir — removing the verifier from the loop

Every "random" challenge is a hash of the entire transcript so far. The prover cannot rewind: changing an earlier commitment changes the hash, which changes every subsequent challenge.

Two rules, both enforced structurally by Channel:

1. Everything the verifier will rely on is absorbed before the challenge that depends on it. You cannot squeeze what you have not absorbed.
2. The statement itself is absorbed first. Omitting this is the classic "weak Fiat–Shamir" bug: a proof for u₂₅₅ = 7 would happily verify against the statement u₂₅₅ = 8. python -m stark_refined tamper demonstrates the attack being rejected.

7. What the verifier actually does

replay the transcript      → same α, β, query indices as the prover
check every Merkle path    → the opened values were committed in advance
recompute CP at each query → from the opened trace values, not from the proof
check FRI folding          → the committed word really is low-degree

That third line is the one people forget. FRI proves low-degreeness, never which polynomial. Without recomputing CP from the trace openings, a prover could commit to any low-degree polynomial at all. tests/test_soundness.py includes exactly that attack — a perfectly valid, perfectly low-degree trace for a different sequence — and asserts it is rejected.

---

Architecture

src/stark_refined/
├── field.py         𝔽ₚ with p = 3·2³⁰+1, roots of unity, batch inversion
├── ntt.py           radix-2 NTT/INTT, coset evaluation, convolution
├── polynomial.py    dense polynomials; BOTH interpolation routines
├── domain.py        power-of-two multiplicative cosets
├── merkle.py        SHA-256 vector commitments, multi-element leaves
├── channel.py       Fiat–Shamir transcript (absorb / squeeze)
├── air.py           the Fibonacci constraint system  ← single source of truth
├── fri.py           the low-degree test, prover and verifier
├── stark.py         assembly, serialisation, prove() / verify()
├── benchmarks.py    the four experiments and their figures
└── cli.py           demo / prove / verify / tamper / bench

Dependencies flow strictly downward — field knows nothing about stark. Each module is independently testable and independently readable.

The constraint system exists exactly once. air.evaluate_composition is called by the prover once per LDE point and by the verifier once per query. There is no "verifier copy" of the constraints that can silently drift out of sync with the prover's — a real class of bugs in hand-rolled proof systems.

---

Results

All numbers below were produced by python -m stark_refined bench on CPython 3.12, x86-64. Re-run it; benchmarks/results.json records your own machine's figures alongside its specs, and python tools/cv_metrics.py reprints them with fitted scaling exponents. Nothing quoted here is a number you cannot point at.

Polynomial layer: O(n³) Lagrange vs O(n log n) NTT

n	Lagrange	NTT	speedup
64	380 ms	189 µs	2 013×
128	2.92 s	393 µs	7 430×
256	23.2 s	872 µs	26 650×

Textbook Lagrange builds each of the n basis polynomials by multiplying out n−1 linear factors, which is O(n²) coefficient operations per basis polynomial and O(n³) overall. The NTT is one inverse transform. The ratio grows as n²/log n, exactly as the asymptotics predict.

End-to-end prover

n	naive backend	NTT backend	speedup	proofs identical
64	477 ms	48.7 ms	9.8×	✓
128	3.21 s	98.0 ms	32.8×	✓
256	23.4 s	199 ms	117×	✓

Both backends produce byte-identical proofs. That equality is asserted in tests/test_backends.py and re-checked by the benchmark itself — the optimisation is behaviour-preserving, not merely fast.

With the naive layer, n = 256 already takes 23 seconds and n = 512 would take over three minutes. With the NTT layer, n = 4096 proves in under four seconds — a 16× longer trace at 1/6 the wall time.

Prover / verifier asymmetry

n	prove	verify	ratio	proof size
256	212 ms	11.6 ms	18×	196 KiB
1024	915 ms	14.2 ms	64×	260 KiB
4096	3.72 s	16.7 ms	223×	333 KiB

Proving is Θ(n log n). Verifying is Θ(queries · log n) and grows by 2.4× while the proved computation grows by 256×. That gap is the entire economic argument for proof systems: do the work once, let everyone check it cheaply and forever.

Soundness

60 random single-element corruptions of an honest proof: 60 rejected, 0 accepted. Seven structured forgeries (python -m stark_refined tamper): all rejected. Five semantic attacks — including a low-degree polynomial encoding a different but perfectly valid sequence — all rejected.

Figures

All four are regenerated by python -m stark_refined bench and land in benchmarks/.

The asymmetry that makes proof systems worth building. Proving is Θ(n log n); verifying is Θ(queries · log n). Measured scaling exponents: 1.03 for the prover, 0.16 for the verifier.

The polynomial layer. Two orders of magnitude of daylight between the textbook route and the NTT, on a log-log axis. Fitted exponent: 2.88 for Lagrange against a predicted 3.00; 0.98 for the NTT.

End-to-end effect on the prover, with the resulting speedup curve. Both backends emit byte-identical proofs at every point on this chart.

Proof size against trace length, on a log x-axis. A 256× longer computation costs 3.6× the proof — the logarithmic term is the FRI layer count.

---

Design decisions

p = 3·2³⁰ + 1. p − 1 = 3·2³⁰, so 𝔽ₚ* contains a cyclic subgroup of order 2ᵏ for every k ≤ 30. A radix-2 NTT only exists when such subgroups exist; a "random" prime would force O(n²) evaluation and O(n³) interpolation. p also fits in 32 bits, so a product of residues fits in 64 — the same code transliterates to uint64 arithmetic in C or Rust unchanged.

Pure Python integers, not NumPy. p² ≈ 1.04 · 10¹⁹ overflows int64 (max 9.22 · 10¹⁸). NumPy would silently wrap and produce a plausible-looking wrong proof. CPython's arbitrary-precision integers are correct by construction; the NTT inner loop drops to raw int residues (no object allocation) for a ~4× win while the public API stays typed.

Exact division raises. In a STARK every polynomial division must be exact — a non-zero remainder is a violated constraint. Polynomial.__truediv__ raises rather than truncating, turning a soundness bug into a stack trace.

Merkle leaves hold pairs. FRI always opens v[j] and v[j + half] together, so each layer commits one leaf per pair: one authentication path instead of two, and one level shallower. Measured effect: proof size at n = 256 fell from 347 KiB to 196 KiB, a 44% reduction, with no change to the security argument (the pairing is a bijection).

Distinct query indices. Sampling with replacement would let repeated queries inflate the apparent security level without adding independent evidence. Channel.challenge_indices rejects duplicates.

Rejection sampling for challenges. Reducing a 256-bit sample mod p biases the distribution by about 2⁻²²³ — negligible, but rejecting the tail is nearly free and removes a footnote from the security argument.

Batch inversion. Montgomery's trick inverts n elements with 3n multiplications and one exponentiation instead of n exponentiations. Used in every FRI fold.

---

Testing

pytest -q                              # 612 tests, ~13 s
python tools/run_tests_nodeps.py       # same suite, zero third-party packages
python tools/run_tests_nodeps.py fri   # only matching files

tools/run_tests_nodeps.py implements the slice of the pytest API the suite uses (mark.parametrize, raises) so the tests run on an air-gapped machine with nothing but CPython. The tests themselves are ordinary pytest.

file	tests	what it pins down
test_field.py	93	field axioms, primality, root orders, batch inversion
test_polynomial.py	70	arithmetic, exact division, both interpolation routines
test_air.py	68	trace, constraint degrees, the index-shift trick
test_domain.py	55	coset structure, disjointness from the trace domain
test_ntt.py	55	NTT against direct evaluation, round trips, convolution
test_stark.py	53	end-to-end across parameters, structural invariants
test_merkle.py	47	path verification, every path-forgery I could think of
test_fri.py	45	folding algebra, acceptance, rejection, tampering
test_soundness.py	37	binding, statement-binding, degree, semantics
test_channel.py	27	transcript ordering, challenge independence
test_serialization.py	23	lossless round trips, language-neutral JSON
test_backends.py	27	naive and NTT paths produce identical proofs
test_cli.py	12	every subcommand, including a tampered proof file

Notable tests rather than notable counts:

• test_air.py::test_quotients_are_polynomials_of_the_expected_degree — interpolates each quotient back from its coset evaluations and checks the degree bound. This is what catches an off-by-one in the transition denominator.
• test_soundness.py::test_a_completely_different_but_valid_trace_is_caught — the attack that FRI alone cannot stop.
• test_backends.py::test_backends_produce_identical_proofs — the optimisation is behaviour-preserving.
• test_channel.py::test_challenge_is_bound_to_everything_absorbed_before_it — the property Fiat–Shamir soundness rests on.

---

Command reference

python -m stark_refined                       # demo + tamper + bench  (default)
python -m stark_refined demo --n 256          # prove and verify, verbosely
python -m stark_refined demo --backend naive  # same, via the O(n³) path
python -m stark_refined prove --n 512 -o proof.json
python -m stark_refined verify -i proof.json
python -m stark_refined tamper                # the forgery gallery
python -m stark_refined bench --quick         # short sweep
python -m stark_refined bench --no-plots      # numbers only

python tools/cv_metrics.py                    # benchmark numbers + fitted exponents
python tools/measure_pair_leaf_gain.py        # proof-size gain from pair leaves

Common flags: --n (trace length, power of two), --c0, --c1, --value (claim a specific final value — use it to watch the prover refuse a false one), --blowup, --queries, --backend {ntt,naive}.

Security scales as queries · log₂(blowup) bits under the standard conjectured bound: --blowup 8 --queries 32 gives ~96 bits, --blowup 16 --queries 32 gives ~128.

---

Known simplifications

Stated plainly, because knowing where a system stops being production-grade is part of understanding it.

1. No zero-knowledge. This is a succinct argument, not a zero-knowledge one. The opened trace values leak information about the witness. Real ZK requires blinding the trace polynomial with random rows and randomising the composition polynomial.
2. Soundness is the conjectured bound. queries · log₂(blowup) assumes FRI is sound up to the list-decoding radius. The provable bound (unique decoding) is roughly half that. Deployed systems use the conjecture; papers do not.
3. No DEEP quotienting. The out-of-domain sampling of DEEP-FRI (Ben-Sasson et al., 2019) tightens soundness meaningfully and is standard in production.
4. Merkle paths are not batched. Queries share tree nodes near the root; deduplicating them (a "batch opening" or Octopus) shrinks proofs by a further 30–40%. The pair-leaf trick here is the easy half of that idea.
5. One AIR, hard-coded. A real system compiles an arbitrary constraint set into an AIR. This project implements one recurrence deliberately, so the protocol stays visible.
6. 32-bit field. Fine for a demonstration; production systems use 64-bit or extension fields so that a single random challenge already carries enough entropy.
7. JSON serialisation. Human-readable and language-neutral, but hex-encoded hashes double the size. A binary encoding would roughly halve it.

---

References

• Ben-Sasson, Bentov, Horesh, Riabzev — Scalable, transparent, and post-quantum secure computational integrity (2018). The STARK paper.
• Ben-Sasson, Bentov, Horesh, Riabzev — Fast Reed–Solomon Interactive Oracle Proofs of Proximity (2018). FRI.
• Ben-Sasson, Goldberg, Kopparty, Saraf — DEEP-FRI (2019).
• StarkWare — STARK 101. The clearest hands-on introduction; this project follows its skeleton and departs from it in the ways listed above.
• Alan Szepieniec — Anatomy of a STARK. The best modular treatment of the algebra.
• Vitalik Buterin — STARKs, Part I–III. Excellent intuition for arithmetisation.

---

Acknowledgements

Built as a bootcamp project supervised by Clément Walter (Zama), co-founder of Kakarot zkEVM. The original brief specified a Fibonacci STARK in Python; the departures from it — degree adjustment, the dual-backend equivalence harness, pair-leaf commitments, the semantic-soundness test suite — are documented above.

MIT licensed.