Skip to content

Generic config#60

Merged
gabriel-barrett merged 15 commits into
mainfrom
generic-config
Jul 10, 2026
Merged

Generic config#60
gabriel-barrett merged 15 commits into
mainfrom
generic-config

Conversation

@gabriel-barrett

@gabriel-barrett gabriel-barrett commented Jul 6, 2026

Copy link
Copy Markdown
Member

Harden the protocol and make it generic over field, hash, and PCS

This PR contains two bodies of work: security/robustness fixes from a code
review, and a refactor that makes the protocol generic over a configuration
trait instead of being hardwired to Goldilocks + Keccak-256.

Security and robustness fixes

  • Panic-free verifier on adversarial proofs. verify_shape now validates
    log_degrees (one entry per circuit, each small enough for the PCS).
    Previously a malformed proof could panic the verifier via an out-of-bounds
    index or a shift overflow — a DoS vector for any service verifying
    untrusted proofs.
  • Fiat-Shamir transcript hardening. The challenger is seeded with a domain
    tag and a digest of all protocol parameters; the circuit shape (widths,
    constraint counts, degrees) is observed before any commitment; claims are
    length-prefixed so [[a, b]] and [[a], [b]] produce distinct
    transcripts; intermediate lookup accumulators are observed before sampling
    the constraint challenge.
  • Witness validation. SystemWitness::from_stage_1 asserts one trace per
    circuit and that main and preprocessed trace heights match, instead of
    silently truncating lookups via zip.
  • Honest docs. The soundness argument now distinguishes conjectured
    (ρ^n, ~2^-100 at the default parameters) from proven Johnson-bound
    (~2^-50) FRI soundness, and states prominently that the protocol is not
    zero-knowledge (no trace blinding; FRI openings reveal witness data).

Genericity refactor

The protocol is now parameterized by StarkGenericConfig (src/config.rs,
modeled on p3-uni-stark): a PCS (which determines the base field), a
challenge field, and a Fiat-Shamir challenger.

  • System<SC, A>, Proof<SC>, ProverKey<SC>, SystemWitness<F>, and the
    builders/folders are generic; GoldilocksKeccakConfig (src/types.rs) is
    the batteries-included reference instantiation.
  • System::new(config, airs) replaces the Committer and its dummy FRI
    parameters; prove/verify no longer take FriParameters — the config
    carries them, so proving and verifying under mismatched parameters is no
    longer expressible.
  • The symbolic builder tags all variables and expressions with the challenge
    field, making Expr and ExprEF the same type. This sidesteps a trait
    coherence conflict that made the old SymbolicExpression<Val>
    SymbolicExpression<ExtVal> conversion impossible to genericize.
  • A second configuration (BabyBear, degree-4 extension, Poseidon2) lives in
    the test suite and differs from the reference config in both the field and
    hash axes, so changes that only compile for the reference config fail CI.

Breaking changes

  • API: System::new takes a config; prove/verify lost their
    FriParameters argument; most public types gained a config parameter.
  • Transcript: proofs generated by earlier versions no longer verify.
  • Toolchain: Rust 1.88 → 1.91. Rust 1.88 miscompiles Plonky3's packed
    BabyBear code under -Ctarget-cpu=native (which this repo enables),
    producing Merkle cap mismatches; Plonky3's own tests fail at the pinned
    rev under 1.88 + native SIMD and pass under 1.91. CI images pinned to
    1.88 need updating.

Testing

  • 19/19 tests pass (including Blake3 integration and the new
    BabyBear/Poseidon2 smoke test), clippy clean, all four examples run, and
    benches compile, with and without the parallel feature.
  • New negative tests: truncated/oversized log_degrees, regrouped claims,
    mismatched preprocessed heights, and tampered proofs under the second
    config.

The verifier never validated the proof's log_degrees field. A proof
with fewer entries than circuits panicked on an out-of-bounds index,
and an oversized entry overflowed the 1 << log_degree shift (debug)
or tripped asserts inside the PCS (release). Both were DoS vectors
for any service verifying untrusted proofs.

verify_shape now checks that log_degrees has one entry per circuit
and that each blown-up quotient domain fits within the two-adic
subgroup of the field.
…mulators

Hardens the Fiat-Shamir transcript in four ways, applied identically
on the prover and verifier sides:

- Seed the challenger with a protocol tag ("multi-stark/v0") for
  domain separation.
- Observe the commitment/FRI parameters and the per-circuit shape
  (widths, constraint counts, degrees) before any commitment, via the
  new System::observe_shape.
- Length-prefix the claims. Previously the claims were observed as a
  bare concatenation, so claim sets like [[a, b]] and [[a], [b]]
  produced identical transcripts; rejection relied on the downstream
  accumulator mismatch rather than on the transcript itself.
- Observe the intermediate lookup accumulators before sampling the
  constraint challenge. They enter the constraints as public values,
  and were previously bound only indirectly through the quotient
  commitment.

This is a breaking change to the proof transcript: proofs generated
by earlier versions no longer verify.
SystemWitness::from_stage_1 zipped main trace rows against
preprocessed rows, so a main trace taller than the preprocessed trace
silently dropped the excess rows' lookups, producing a stage 2 trace
of the wrong height and failing much later with an opaque PCS error.

Both traces are opened on the same domain, so their heights must
match. Assert this (and the trace count) upfront with a clear message.
- ensure! logged every expected verification rejection to stderr via
  eprintln; use tracing::debug instead.
- The quotient degree formula was duplicated between the prover and
  verify_shape; both now use the new Circuit::quotient_degree.
- Remove the unused get_log_quotient_degree (its is_zk parameter was
  aspirational — nothing in the prover implements zero-knowledge) and
  the unused benchmark! macro.
…f ZK

The soundness docs quoted rho^n (~2^-100 at log_blowup = 1 with 100
queries) without saying that this is the conjectured, capacity-style
bound; the proven Johnson bound only gives ~(sqrt(rho))^n (~2^-50 for
the same parameters). State both regimes in the verifier module docs,
the README, and the PCS example.

Also document prominently that the protocol is not zero-knowledge:
traces are committed without blinding and FRI query responses reveal
witness LDE values.
Phase 1 of the genericity refactor. SymbolicAirBuilder<F, EF>,
ProverConstraintFolder<'a, F, EF>, VerifierConstraintFolder<'a, F, EF>
and DebugConstraintBuilder<'a, F, EF> now work over any base field F
and extension EF.

The symbolic builder tags all variables and expressions with EF, even
those referring to base-field columns, so that Expr and ExprEF are the
same type. This sidesteps the coherence problems of converting between
SymbolicExpression<F> and SymbolicExpression<EF>: the old concrete
From<SymbolicExpression<Val>> for SymbolicExpression<ExtVal> impl
could not be made generic (it would overlap with core's reflexive
From<T> for T when EF = F). The base-field embedding is now a single
impl<F: Field, EF: ExtensionField<F>> From<F> for SymbolicExpression<EF>,
which covers the old same-field conversion via the reflexive
ExtensionField<F> for F.

The rest of the crate instantiates the builders concretely at
(Val, ExtVal); later phases make those call sites generic.
Phase 2 of the genericity refactor. LookupAir<A> becomes
LookupAir<A, F>; compute_expr, compute_message and stage_2_traces
work over any base field F and extension EF. The Air impl is bounded
by TwoStagedBuilder<F = F> alone, since the builder's associated EF
already carries the extension.
Phase 3 of the genericity refactor.

- New src/config.rs: the StarkGenericConfig trait (Pcs / Challenge /
  Challenger associated types, modeled on p3-uni-stark) plus type
  aliases (Val, Domain, Com, PcsProof, PcsError, PcsData,
  EvaluationsOnDomain, PackedVal, PackedChallenge). max_log_degree()
  replaces the hardcoded Goldilocks TWO_ADICITY bound in verify_shape.
- types.rs becomes the reference instantiation: GoldilocksKeccakConfig
  (formerly StarkConfig). The protocol parameters are now bound into
  the transcript via the challenger seed (domain tag + parameter
  digest) instead of System::observe_shape, since generic code cannot
  enumerate the parameters of an arbitrary PCS. observe_shape now
  binds only the circuit shape.
- System::new(config, airs) replaces the (commitment_parameters, ...)
  constructor and the Committer with its dummy FRI parameters: the
  preprocessed traces are committed with the real PCS. prove/verify
  no longer take FriParameters — the config carries them, so proving
  and verifying under different parameters is no longer expressible.
- zeta * domain.subgroup_generator() is replaced with the PCS-agnostic
  domain.next_point(zeta) (returns an error on adversarial input in
  the verifier rather than unwrapping).

This changes the transcript again: proofs from earlier versions no
longer verify.
Phase 4 of the genericity refactor. System<SC, A>, Circuit<A, F>,
ProverKey<SC>, SystemWitness<F> and Proof<SC> are now generic over any
StarkGenericConfig; the prover and verifier reference the config
aliases (Val<SC>, Com<SC>, PackedChallenge<SC>, ...) instead of the
concrete Goldilocks/Keccak types. Proof serialization uses
on its commitment and proof types.

SystemWitness::from_stage_1 keeps its call shape via a nested
associated-type bound (Domain: PolynomialSpace<Val = F>) tying the
witness field to the config's base field.

Tests, examples and benches instantiate at GoldilocksKeccakConfig.
Rust 1.88 miscompiles Plonky3's packed BabyBear (monty-31) code when
built with -Ctarget-cpu=native (which this repo enables via
.cargo/config.toml): Plonky3's own uni-stark BabyBear/Poseidon2 tests
fail with Merkle cap mismatches at the pinned rev under 1.88 + native
SIMD, and pass under 1.91+. Goldilocks is unaffected (different
packing code path).

Verified by running Plonky3's no_next_row test at rev e9d7561 under
both toolchains with RUSTFLAGS=-Ctarget-cpu=native: 1.88 fails, 1.91
passes.
Phase 5 of the genericity refactor. BabyBearPoseidon2Config differs
from the reference config in both axes — base field (BabyBear with a
degree-4 extension, vs Goldilocks with degree-2) and hash (Poseidon2
duplex sponge, vs Keccak-256) — so a change that only works for the
reference instantiation now fails this smoke test. The test proves
and verifies a small circuit with a self-canceling lookup pair and
checks that tampered proofs are still rejected.
Phase 6 of the genericity refactor. The README's cryptographic setup
table becomes a "reference configuration" section pointing at
StarkGenericConfig; the prover/verifier module docs stop naming
Goldilocks/Keccak as fixed choices; and the soundness argument states
explicitly that the Schwartz-Zippel terms scale with the configured
challenge field size, with examples of adequate and inadequate
extensions.
@gabriel-barrett
gabriel-barrett marked this pull request as ready for review July 7, 2026 13:46
- crossbeam-epoch 0.9.18 -> 0.9.20 (RUSTSEC-2026-0204, invalid pointer
  dereference in fmt::Pointer; pulled in via criterion)
- rand 0.10.0 -> 0.10.2 (RUSTSEC-2026-0097, unsoundness with a custom
  logger using rand::rng(); pulled in via the new p3-baby-bear dev
  dependency)

cargo deny check now passes all four categories.
The prover obtains trace evaluations on the quotient domain from the
PCS via get_evaluations_on_domain, which for a FRI-based PCS can only
serve domains up to the blowup factor times the trace domain. The
quotient degree is next_power_of_two(max_constraint_degree - 1), so
the constraint degree is implicitly bounded by 2^log_blowup + 1 —
degree 3 at the default log_blowup = 1.

This bound was previously unenforced: a degree-5 circuit at
log_blowup = 1 proved "successfully" and then failed verification
with an unhelpful OodEvaluationMismatch (Plonky3's LDE extrapolation
fallback does not produce usable evaluations here, and upstream's own
tests only exercise quotient_degree <= blowup).

Add StarkGenericConfig::max_quotient_degree (the blowup factor for
the FRI-based configs) and reject offending circuits in System::new
with an actionable message. Regression tests cover both the rejection
at log_blowup = 1 and the same degree-5 circuit proving end-to-end at
log_blowup = 2.
- The prover and verifier module docs described the pre-hardening
  transcript: no mention of the parameter-seeded challenger, the
  system shape observation, the length-prefixing of claims, or the
  intermediate accumulators being observed. Bring the stage-by-stage
  protocol descriptions in line with the code.
- pcs_example claimed to commit 4 polynomials while the code commits
  num_polys = 1.
@gabriel-barrett
gabriel-barrett merged commit e2907d3 into main Jul 10, 2026
4 checks passed
@gabriel-barrett
gabriel-barrett deleted the generic-config branch July 10, 2026 15:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants