zheng's IOP through zippel — 2026-10-24

The question: does this IOP prove what it claims? The way to answer it, tried here: write the IOP of rs/src/spartan + rs/src/sumcheck as a zippel choreography (specs/proto/), let zippel derive the transcript and run its completeness and special-soundness analyses. zippel at f207f68c (2026-10-24), nightly-2026-09-13, arkworks 0.6 over BLS12-381's scalar field (the field only enters the analyses through algebra; Goldilocks is not a backend yet), ark-gb and Singular 4.4.1 as Gröbner backends, M4 Max.

what ran

Sizes are the smallest that exercise both the base case and the recursive case of every size-overloaded round function, the paper's own rule for bounded checking.

what it says

1. The IOP is complete as written. Every honest run of zheng's protocol — outer sumcheck over eq(τ,·)·(a·b − c) with degree-3 round polynomials on four points, the matrix_evals check, γ-batching, the inner product sumcheck with degree-2 round polynomials on three points, the closing check against ẑ(ry) — is accepted by the verifier, as an algebraic identity, not as a test on random inputs.
2. The analysis catches a real bug class. Sending a degree-3 round polynomial as three evaluations type-checks and even passes a run on a degenerate instance; completeness fails in 4.5 s. This is exactly the mistake OuterSumcheckProver::round_poly avoids with num_pts = degree + 2, now checked rather than trusted.
3. The transcript order is the same. zippel absorbs every <- message and squeezes every challenge in program order; zheng's order (commitment, τ, [round polynomial, r] × log m, the three evaluations, γ, [round polynomial, r] × log n, eval_value, the lens seed) is the same sequence. Two differences, neither a discrepancy: zheng tags each absorb with a domain byte, round index and degree (transcript.rs), zippel binds the session and the instance bytes once in the domain separator; and the commitment has no counterpart in the oracle model — z is bound as an instance instead. The statement is bound above Spartan (rs/src/lib.rs:266, absorb_statement), so the CCS reaches the transcript through the program hash, not through SpartanVerifier::verify itself.
4. Special soundness does not apply in the oracle model. With the lens as an oracle nothing is witness, so there is nothing to extract: the outer and full protocols are rejected as "verifier has 0 challenges" (τ is drawn before any prover message, which breaks the Σ-shape the analysis expects), the inner one yields a unit search ideal. zippel's special soundness is an extractor property for protocols with a witness and a commitment; sumcheck's soundness is a probabilistic bound per round, which the paper's own Figure 6 does not claim for sumcheck either. To get a soundness verdict from zippel, z must be a witness and the commitment inside the protocol — the hash-based lens is not expressible there, and Spartan with Hyrax was already too large for the analysis in the paper.
5. Size. ark-gb stops at 1,023 variables (their generic sumcheck at four variables, degree 3, needs 1,285); Singular lifts the limit and costs about 20× at these sizes. Everything above fits ark-gb.

what to keep

• specs/proto/ is the executable spec of the IOP. A change to the protocol in rs/ without the matching change here is a review finding.
• the gate: zippel-check on every file, completeness at the sizes above, and zheng_bug must keep failing (a passing bug variant means the analysis is not looking). Run recipe in specs/proto/README.md; it is a separate nightly toolchain, never a dependency of the workspace.
• next: the HyperNova fold step and the decider's algebraic part as protocols — the two "asserted, not yet proven" properties of the settlement lottery live there; and an analysis-only Goldilocks backend upstream so the sized-type checks run in our field.