Univariate skip for the batched AIR sumcheck (+ finite-difference kernel)#251

Closed

Barnadrot wants to merge 9 commits into

leanEthereum:mainfrom

Barnadrot:pw13-clean

Commits on Jun 11, 2026

pw13-1 T1: backend primitives for univariate skip (skip domain, tensor-tail eq/next expansion)
Barnadrot
committed
pw13-1 T2: univariate skip-round kernel for AirSumcheckSession (+ go/no-go timing gate)

Barnadrot
and
claude
committed
pw13-1 T3: front-loaded uniskip batched AIR sumcheck orchestration (prove+verify)
Barnadrot
committed
pw13-1 T4: WHIR tensor-tail statements (Lagrange ⊗ eq weights for uniskip openings)
Barnadrot
committed
pw13-1 T5: wire uniskip AIR sumcheck into production prover/verifier

Barnadrot
and
claude
committed
pw13-1 T6: python verifier mirrors uniskip protocol (executable spec)
Barnadrot
committed
pw13-1 T7: recursion circuit verifies uniskip protocol (zkDSL + recompilation)
Barnadrot
committed
pw13-2 U1: finite-difference extension for uniskip kernel (+bench gate)
Barnadrot
committed
style: cargo fmt
Barnadrot
committed