Skip to content

Sumcheck over the infinity hypercube - #2520

Merged
jimpo merged 2 commits into
mainfrom
aj/binius-702-sumcheck-over-the-infinity-hypercube
Oct 30, 2026
Merged

jimpo merged 2 commits into
mainfrom
aj/binius-702-sumcheck-over-the-infinity-hypercube

Conversation

@benji-potamus

@benji-potamus benji-potamus commented Oct 29, 2026 •

Copy link
Copy Markdown
Collaborator

Resolves BINIUS-702 (sub-issue 6 of BINIUS-696; groundwork for Phase A / A′).

A sumcheck over {0, ∞}^n: the ordinary sumcheck with round check R(0) + R(∞) = s. For monomial-coefficient tables u, w, Σ_x u^∞(x) w^∞(x) = <u, w>, and the sumcheck reduces to u^∞(r), w^∞(r) at the challenge point r.

Commits

  1. Add sumcheck verifier over the infinity hypercube (binius_ip::sumcheck::infinity)
    • verify and batch_verify, mirroring sumcheck::{verify, batch_verify}.
    • RoundProof::recover_infinity: a_d = s - a_0. The wire format is unchanged (the top coefficient is still the one dropped).
  2. Add product prover for the infinity-hypercube sumcheck (binius_ip_prover::sumcheck::infinity::batch_prove)
    • Takes pairs [u, w] of mixed variable counts and binds the top variable each round. It computes R(∞) = <u_1, w_1> and the middle coefficient from the cross terms, and takes R(0) from the claim. The fold is u' = u_0 + r u_1.
    • A claim that is smaller than the current round count contributes its constant claim as R, so there is no padding factor. It closes at the low k coordinates of the point.

Tests

  • Round trip over five pairs with mixed sizes (5, 0, 3, 5, 1 vars). Each eval equals the monomial-basis evaluation <u, eq_ind_partial_eval::<InfCube>(r)>, and the batched eval matches.
  • A tampered round-0 coefficient is rejected (the final eval mismatches).
  • recover_infinity round-trips.

The prover is a standalone function and does not implement SumcheckProver. That way it can't be paired with the boolean-cube batch_verify by mistake.

🤖 Generated with Claude Code

@benji-potamus
benji-potamus requested a review from a team October 29, 2026 14:12
@linear-code

linear-code Bot commented Oct 29, 2026

Copy link
Copy Markdown

BINIUS-702

@benji-potamus
benji-potamus force-pushed the aj/binius-702-sumcheck-over-the-infinity-hypercube branch from 03d9810 to f2f6c2c Compare October 29, 2026 15:31
jimpo and others added 2 commits October 30, 2026 21:32
Verify a sumcheck whose round check is R(0) + R(inf) = s, batched over
claims of mixed variable counts.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Prove a batch of claims <u, w> over pairs of monomial-coefficient
tables, binding the top variable each round with u' = u_0 + rho * u_1.
Smaller claims contribute their constant claim until their variables
come up, so no padding factor is needed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@benji-potamus
benji-potamus force-pushed the aj/binius-702-sumcheck-over-the-infinity-hypercube branch from f2f6c2c to 11ae1ad Compare October 30, 2026 21:33
@jimpo
jimpo added this pull request to the merge queue Oct 30, 2026
Merged via the queue into main with commit 292a377 Oct 30, 2026
10 checks passed
@jimpo
jimpo deleted the aj/binius-702-sumcheck-over-the-infinity-hypercube branch October 30, 2026 22:04
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