feat(multilinear): the sumcheck, and the two arguments built on it - #998
Draft
ColoCarletti wants to merge 1 commit into
Draft
ColoCarletti wants to merge 1 commit into
ColoCarletti wants to merge 1 commit into
Conversation
One brick and two uses. The sumcheck reduces a sum over `2^n` points to a single evaluation: round by round the prover sends a one-variable polynomial, the verifier draws, and the cube halves. The form here does not send `g(0)` — it is recovered from the claim the round entered with, since `g(0) + g(1)` is that claim — which saves a whole pass over the cube and one element per round, and has a consequence worth stating plainly: **a round never rejects.** Verification recovers `g(0)`, absorbs, draws and interpolates; the only rejection a sumcheck has is its final claim, and discharging that is the caller's. On top of it, two arguments. The zerocheck says a polynomial vanishes on the whole cube, by weighting it with `eq(r, ·)` at the cost of one degree. LogUp-GKR says a bus balances, by reducing a tree of fractions layer by layer. Neither is a separate protocol: both are a weight and a claim handed to the same rounds. `claim_reduce` ties the shifted views a table reads back to the columns they read, so a shifted read is not a second commitment. `batch` is what makes that one pass instead of several: statements over one cube share their factors and their rounds, combined with powers of a challenge. The claims are absorbed **before** that challenge is drawn — which is the only thing stopping a prover from picking a statement after seeing it. `gpu` is the seam to the device, and this is the half that declines: every entry point returns `None`, so the whole path is host-only and can be read without a card. The half that does the work lands last. `zerocheck` is the reference and says so: a real table's constraints go in as a compiled `batch::Rule` beside its two bus claims, so all three share one pass over one factor list. Nothing outside tests calls it. It stays because the tests that do call it are `stark`'s, they run the production polynomial through it, and three of them are negative. What pinches it: 128 tests, in debug and parallel. The one to know about is `batch::the_claims_are_bound_to_the_batching_challenge`, which is not a test of a proof — pull the three claim absorptions out of both sides and every other test still passes, because the two sides still agree and the proof still verifies. What is lost is soundness, and the only thing that sees it is the transcript: two different claims have to give different challenges. Checked that it is the one test that fails. Not wired to anything. Nothing in the tree calls this crate yet.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
New crate. Nothing in the tree calls it yet.
The sumcheck reduces a sum over
2^npoints to one evaluation: each roundthe prover sends a one-variable polynomial, the verifier draws, the cube
halves. It does not send
g(0)— that comes from the claim the roundentered with — which saves a pass over the cube and one element per round,
and has a consequence worth knowing: a round never rejects. The only
rejection is the final claim, and discharging it is the caller's. All four
callers here do.
Two uses on top:
zerochecksays a polynomial vanishes on the whole cube,logupsays a bus balances. Neither is a separate protocol — both are aweight and a claim handed to the same rounds.
batchruns severalstatements over one cube in one pass;
claim_reduceties shifted readsback to the columns they read.
zerocheckis the reference, not the path, and says so: a real table'sconstraints go in as a compiled
batch::Rule.gpuis only the half that declines — every entry point returnsNone, sothe whole thing is host-only and reads without a card.
One test is worth pointing at:
the_claims_are_bound_to_the_batching_challenge.Pull the claim absorptions out of both sides and every proof still verifies
and every other test passes; what is lost is soundness, and only the
transcript sees it. Checked that it is the one test that fails.