Proposal: In-circuit Winterfell STARK verifier (R1CS/arkworks) for review and potential upstream inclusion

[sidhujag]

We’ve implemented a full Winterfell-compatible STARK verifier as an R1CS circuit on arkworks (Fr377), using Goldilocks (GL) non‑native “light” gadgets. We’d appreciate your review for correctness and API fit, and are open to adapting it for potential upstream inclusion (as a reference or optional sub-crate).

What this adds

• Winterfell 0.13.1 compatibility
  • Proof parsing (commitments, OOD, queries, FRI)
  • Fiat–Shamir transcript replay and position derivation
  • FRI folding and terminal checks
• Circuit features
  • GL light arithmetic: congruence-only ops inside the circuit; canonicalization only at byte boundaries (Merkle and digests)
  • Batch multiproof for Merkle (RPO-256) and batch inversion (Montgomery’s trick) in FRI to reduce constraints
  • Strict structural checks and soundness guards

Correctness and security highlights

• Transcript replay and query positions (critical)
  • Rebuilds the RandomCoin transcript in-circuit and re-derives LDE query positions, including nonce grinding (leading-zero check).
  • Domain checks, sort/dedup of derived positions, and equality enforcement with witness positions.
  • Prevents adversarial preselected positions slipping through via “only hash positions” binding.
• FRI
  • Binary fold (t=2) folding with batch inversion of denominators.
  • Fixed order-coupling bugs by using position→pair mapping; hi/lo selection derived from the previous non-unique positions.
  • Enforces exact power-of-two domain splits (integer ilog2) and layer count equals AIR’s fri_num_layers.
  • Always runs the FRI verifier; can’t bypass by supplying 0 layers.
• Merkle and RPO
  • RPO-256 implemented in GL light; canonicalize at serialization boundaries into bytes before comparing to proof digests and roots.
  • Batch multiproof verification for trace, composition, and FRI.
• DEEP composition
  • Composition width sourced from AIR (no inference).
  • OOD values allocated once and reused (no duplicate allocs).
• Combiner support
  • RandomRho implemented.
  • DegreeChunks is planned (we can branch on combiner_kind if you prefer the API; code path is scaffolded but currently disabled to avoid complexity creep).

Performance (indicative, varies by backend and machine)

• Constraint counts (approx):
  • 1 FRI layer (steps=64): ~4.0M constraints
  • 2 FRI layers (steps=128): ~5.5M constraints
  • 3 FRI layers (steps=256): ~7.2M constraints
• Notable cuts:
  • Batch inversion in FRI fold loop
  • OOD reuse; byte-boundary canonicalization only
  • Early checks for folding factor, domain, and layer counts avoid wasted constraints
• Potential future reductions:
  • Cheaper in-circuit multiset equality for positions after sort/dedup
  • Tighter integer gadgets for nonce/PRNG masking

Tests

• Positive: 0/1/2/3 FRI layers; different trace sizes.
• Negative/adversarial:
  • Wrong positions commitment
  • Tampered trace/comp/FRI nodes
  • Missing FRI layers (now enforced and rejected)
  • Low PoW nonce violating grinding factor

What we’re asking

• API/compat feedback: Is this the right boundary to integrate (e.g., a “circuit verifier” crate or example) in the Winterfell ecosystem?
• Acceptance criteria: Would you consider including this as a reference R1CS verifier (or a contrib/experimental module)?
• Guidance on:
  • Preferred interface for proof parsing/transcript replay if upstreamed
  • Expectations for DegreeChunks combiner in-circuit (we can complete this path)
  • Any invariants we should assert in-circuit beyond what we already enforce

How to try (high-level)

• Build and run tests in our crate; we mirror Winterfell’s transcript and proof structures.
• Supply a Winterfell proof; parser translates into the circuit’s witness layout; the circuit replays the transcript and verifies commitments, DEEP, and FRI.

We’re happy to provide a PR or a small repo showing the integration points that best align with your design. Thanks for reviewing!

References
https://github.com/sidhujag/PVUGC/tree/main/src/stark
https://github.com/sidhujag/PVUGC/blob/main/docs/STARK_VERIFIER_ARCHITECTURE.md