diff --git a/gkr/bls12-377/gkr.go b/gkr/bls12-377/gkr.go index 0744747e7a..74152eee38 100644 --- a/gkr/bls12-377/gkr.go +++ b/gkr/bls12-377/gkr.go @@ -82,6 +82,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // identityGate is the identity gate LevelCircuit and consolidationView use to build level 0's @@ -131,11 +132,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -147,7 +148,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -170,22 +171,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -225,7 +224,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]fr.Element, r.nbVars) @@ -239,7 +238,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss for i, w := range outputs { outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []fr.Element for i, w := range outputs { if r.consolidated[w] { @@ -250,24 +249,24 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -275,8 +274,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -295,6 +294,7 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -343,12 +343,12 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -414,8 +414,8 @@ func iterateElems(elems []fr.Element, counter *int, yield func(int, *fr.Element) } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *fr.Element] { return func(yield func(int, *fr.Element) bool) { diff --git a/gkr/bls12-377/sumcheck.go b/gkr/bls12-377/sumcheck.go index bda61904aa..578700dae0 100644 --- a/gkr/bls12-377/sumcheck.go +++ b/gkr/bls12-377/sumcheck.go @@ -24,10 +24,11 @@ type transcript = gkrcore.Transcript[fr.Element] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial // compute gⱼ polynomial for current round - roundFold(r fr.Element) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.Polynomial // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne fr.Element) fr.Element // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r fr.Element) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -39,49 +40,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial - finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum fr.Element, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]fr.Element, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum fr.Element, degree int, t transcript) error { r := make([]fr.Element, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*fr.Vector)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -248,6 +258,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial { return p } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r fr.Element) { @@ -354,15 +371,13 @@ func (c *zeroCheckBase) proveFinalEval(r []fr.Element, extraPolys []polynomial.M return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff fr.Element) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin, len(uniqueInputs)) @@ -387,8 +402,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -436,15 +453,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum fr.Element) { level := r.schedule[levelI] - var foldingCoeff fr.Element if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -453,43 +470,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zero for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin // contiguous buffer; second half is the current round's eq segment + q []fr.Element // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne fr.Element) fr.Element { + var res, oneMinusQj fr.Element + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomial computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomial computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { @@ -535,7 +563,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -605,7 +633,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []fr.Element) []fr.Elemen // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -628,7 +656,7 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -652,20 +680,27 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -673,44 +708,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]fr.Element, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 fr.Element - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*fr.Vector)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/bls12-377/sumcheck_test.go b/gkr/bls12-377/sumcheck_test.go index 8a2ab0567f..b6bb8cdb3a 100644 --- a/gkr/bls12-377/sumcheck_test.go +++ b/gkr/bls12-377/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewNativeTranscript(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r fr.Element) { c.g.Fold(r) } diff --git a/gkr/bls12-381/gkr.go b/gkr/bls12-381/gkr.go index a663b033f1..785d9c9911 100644 --- a/gkr/bls12-381/gkr.go +++ b/gkr/bls12-381/gkr.go @@ -82,6 +82,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // identityGate is the identity gate LevelCircuit and consolidationView use to build level 0's @@ -131,11 +132,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -147,7 +148,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -170,22 +171,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -225,7 +224,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]fr.Element, r.nbVars) @@ -239,7 +238,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss for i, w := range outputs { outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []fr.Element for i, w := range outputs { if r.consolidated[w] { @@ -250,24 +249,24 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -275,8 +274,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -295,6 +294,7 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -343,12 +343,12 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -414,8 +414,8 @@ func iterateElems(elems []fr.Element, counter *int, yield func(int, *fr.Element) } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *fr.Element] { return func(yield func(int, *fr.Element) bool) { diff --git a/gkr/bls12-381/sumcheck.go b/gkr/bls12-381/sumcheck.go index 9009535d92..792f642802 100644 --- a/gkr/bls12-381/sumcheck.go +++ b/gkr/bls12-381/sumcheck.go @@ -24,10 +24,11 @@ type transcript = gkrcore.Transcript[fr.Element] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial // compute gⱼ polynomial for current round - roundFold(r fr.Element) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.Polynomial // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne fr.Element) fr.Element // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r fr.Element) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -39,49 +40,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial - finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum fr.Element, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]fr.Element, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum fr.Element, degree int, t transcript) error { r := make([]fr.Element, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*fr.Vector)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -248,6 +258,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial { return p } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r fr.Element) { @@ -354,15 +371,13 @@ func (c *zeroCheckBase) proveFinalEval(r []fr.Element, extraPolys []polynomial.M return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff fr.Element) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin, len(uniqueInputs)) @@ -387,8 +402,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -436,15 +453,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum fr.Element) { level := r.schedule[levelI] - var foldingCoeff fr.Element if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -453,43 +470,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zero for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin // contiguous buffer; second half is the current round's eq segment + q []fr.Element // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne fr.Element) fr.Element { + var res, oneMinusQj fr.Element + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomial computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomial computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { @@ -535,7 +563,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -605,7 +633,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []fr.Element) []fr.Elemen // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -628,7 +656,7 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -652,20 +680,27 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -673,44 +708,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]fr.Element, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 fr.Element - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*fr.Vector)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/bls12-381/sumcheck_test.go b/gkr/bls12-381/sumcheck_test.go index 0f663e48bc..2ae834b5de 100644 --- a/gkr/bls12-381/sumcheck_test.go +++ b/gkr/bls12-381/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewNativeTranscript(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r fr.Element) { c.g.Fold(r) } diff --git a/gkr/bn254/gkr.go b/gkr/bn254/gkr.go index ab771c4545..8f0d7419fb 100644 --- a/gkr/bn254/gkr.go +++ b/gkr/bn254/gkr.go @@ -82,6 +82,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // identityGate is the identity gate LevelCircuit and consolidationView use to build level 0's @@ -131,11 +132,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -147,7 +148,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -170,22 +171,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -225,7 +224,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]fr.Element, r.nbVars) @@ -239,7 +238,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss for i, w := range outputs { outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []fr.Element for i, w := range outputs { if r.consolidated[w] { @@ -250,24 +249,24 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -275,8 +274,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -295,6 +294,7 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -343,12 +343,12 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -414,8 +414,8 @@ func iterateElems(elems []fr.Element, counter *int, yield func(int, *fr.Element) } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *fr.Element] { return func(yield func(int, *fr.Element) bool) { diff --git a/gkr/bn254/sumcheck.go b/gkr/bn254/sumcheck.go index deaea4086c..2675eab655 100644 --- a/gkr/bn254/sumcheck.go +++ b/gkr/bn254/sumcheck.go @@ -24,10 +24,11 @@ type transcript = gkrcore.Transcript[fr.Element] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial // compute gⱼ polynomial for current round - roundFold(r fr.Element) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.Polynomial // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne fr.Element) fr.Element // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r fr.Element) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -39,49 +40,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial - finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum fr.Element, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]fr.Element, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum fr.Element, degree int, t transcript) error { r := make([]fr.Element, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*fr.Vector)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -248,6 +258,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial { return p } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r fr.Element) { @@ -354,15 +371,13 @@ func (c *zeroCheckBase) proveFinalEval(r []fr.Element, extraPolys []polynomial.M return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff fr.Element) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin, len(uniqueInputs)) @@ -387,8 +402,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -436,15 +453,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum fr.Element) { level := r.schedule[levelI] - var foldingCoeff fr.Element if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -453,43 +470,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zero for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin // contiguous buffer; second half is the current round's eq segment + q []fr.Element // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne fr.Element) fr.Element { + var res, oneMinusQj fr.Element + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomial computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomial computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { @@ -535,7 +563,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -605,7 +633,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []fr.Element) []fr.Elemen // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -628,7 +656,7 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -652,20 +680,27 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -673,44 +708,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]fr.Element, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 fr.Element - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*fr.Vector)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/bn254/sumcheck_test.go b/gkr/bn254/sumcheck_test.go index f4bc769139..c16259ad27 100644 --- a/gkr/bn254/sumcheck_test.go +++ b/gkr/bn254/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewNativeTranscript(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r fr.Element) { c.g.Fold(r) } diff --git a/gkr/bw6-761/gkr.go b/gkr/bw6-761/gkr.go index d13d6524c7..70b32847f5 100644 --- a/gkr/bw6-761/gkr.go +++ b/gkr/bw6-761/gkr.go @@ -82,6 +82,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // identityGate is the identity gate LevelCircuit and consolidationView use to build level 0's @@ -131,11 +132,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -147,7 +148,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -170,22 +171,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -225,7 +224,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]fr.Element, r.nbVars) @@ -239,7 +238,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss for i, w := range outputs { outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []fr.Element for i, w := range outputs { if r.consolidated[w] { @@ -250,24 +249,24 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -275,8 +274,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -295,6 +294,7 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -343,12 +343,12 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -414,8 +414,8 @@ func iterateElems(elems []fr.Element, counter *int, yield func(int, *fr.Element) } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *fr.Element] { return func(yield func(int, *fr.Element) bool) { diff --git a/gkr/bw6-761/sumcheck.go b/gkr/bw6-761/sumcheck.go index 94bf8c4fa0..8e62a94486 100644 --- a/gkr/bw6-761/sumcheck.go +++ b/gkr/bw6-761/sumcheck.go @@ -24,10 +24,11 @@ type transcript = gkrcore.Transcript[fr.Element] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial // compute gⱼ polynomial for current round - roundFold(r fr.Element) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.Polynomial // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne fr.Element) fr.Element // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r fr.Element) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []fr.Element) []fr.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -39,49 +40,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial - finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []fr.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum fr.Element, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]fr.Element, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum fr.Element, degree int, t transcript) error { r := make([]fr.Element, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*fr.Vector)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -248,6 +258,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial { return p } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r fr.Element) { @@ -354,15 +371,13 @@ func (c *zeroCheckBase) proveFinalEval(r []fr.Element, extraPolys []polynomial.M return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff fr.Element) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin, len(uniqueInputs)) @@ -387,8 +402,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -436,15 +453,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum fr.Element) { level := r.schedule[levelI] - var foldingCoeff fr.Element if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -453,43 +470,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (fr.Element, *zero for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin // contiguous buffer; second half is the current round's eq segment + q []fr.Element // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne fr.Element) fr.Element { + var res, oneMinusQj fr.Element + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomial computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomial computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { @@ -535,7 +563,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -605,7 +633,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []fr.Element) []fr.Elemen // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -628,7 +656,7 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -652,20 +680,27 @@ func (r *resources) buildSuffixEq(q []fr.Element) polynomial.MultiLin { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -673,44 +708,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]fr.Element, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 fr.Element - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*fr.Vector)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/bw6-761/sumcheck_test.go b/gkr/bw6-761/sumcheck_test.go index a91592524a..1afea0185f 100644 --- a/gkr/bw6-761/sumcheck_test.go +++ b/gkr/bw6-761/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewNativeTranscript(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne fr.Element) fr.Element { + var res fr.Element + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r fr.Element) { c.g.Fold(r) } diff --git a/gkr/bytecode.go b/gkr/bytecode.go index 326abe1247..154014ee13 100644 --- a/gkr/bytecode.go +++ b/gkr/bytecode.go @@ -11,7 +11,7 @@ const ( OpMul // result = src1 * src2 * ... OpNeg // result = -src1 _ // retired: the multiply-accumulate that read its addend first - OpSumExp17 // result = (src1 + src2 + src3)^17 + OpSumExp17 // result = (src1 + src2 + src3)¹⁷ OpMulAcc // result = (src1 * src2) + src3 ) diff --git a/gkr/field.go b/gkr/field.go index ad7e709731..5fa3ad8a65 100644 --- a/gkr/field.go +++ b/gkr/field.go @@ -2,20 +2,20 @@ package gkr import "math/big" -// Field describes F_p[X]/(f), with f = Xⁿ + MinPoly[n-1]·Xⁿ⁻¹ + … + MinPoly[0] monic and -// irreducible over F_p, n = len(MinPoly). Coefficients are in increasing degree: X is [0], +// Field describes Fₚ[X]/(f), with f = Xⁿ + MinPoly[n-1]·Xⁿ⁻¹ + … + MinPoly[0] monic and +// irreducible over Fₚ, n = len(MinPoly). Coefficients are in increasing degree: X is [0], // X² + 1 is [1, 0]. type Field struct { Modulus *big.Int MinPoly []*big.Int } -// PrimeField describes F_p itself, as F_p[X]/(X). +// PrimeField describes Fₚ itself, as Fₚ[X]/(X). func PrimeField(p *big.Int) Field { return Field{Modulus: p, MinPoly: []*big.Int{big.NewInt(0)}} } -// Degree returns n, the extension degree of the field over F_p. +// Degree returns n, the extension degree of the field over Fₚ. func (f Field) Degree() int { return len(f.MinPoly) } diff --git a/gkr/gkrapi/api.go b/gkr/gkrapi/api.go index f559f943e2..4a98599c52 100644 --- a/gkr/gkrapi/api.go +++ b/gkr/gkrapi/api.go @@ -10,7 +10,7 @@ import ( // Circuit is a circuit compiled by API.Compile, ready to prove and verify with gkr/. type Circuit = gkr.SerializableCircuit -// PrimeField describes F_p itself. +// PrimeField describes Fₚ itself. var PrimeField = gkr.PrimeField // KoalaBearE6 describes KoalaBear's degree-6 extension E6. diff --git a/gkr/koalabear/gkr.go b/gkr/koalabear/gkr.go index 321c98ca9c..01ea44010d 100644 --- a/gkr/koalabear/gkr.go +++ b/gkr/koalabear/gkr.go @@ -85,6 +85,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // evaluateBase returns the evaluation of the multilinear extension of the base field column col at @@ -139,11 +140,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -155,7 +156,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -178,22 +179,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -233,7 +232,7 @@ func Prove[D hash.ArrayBlock[koalabear.Element]](c Circuit, schedule constraint. } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]extensions.E6, r.nbVars) @@ -247,7 +246,7 @@ func Prove[D hash.ArrayBlock[koalabear.Element]](c Circuit, schedule constraint. for i, w := range outputs { outputEvals[i] = r.evaluateBase(r.assignment[w], firstChallenge) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []extensions.E6 for i, w := range outputs { if r.consolidated[w] { @@ -258,24 +257,24 @@ func Prove[D hash.ArrayBlock[koalabear.Element]](c Circuit, schedule constraint. gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -283,8 +282,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -303,6 +302,7 @@ func Verify[D hash.ArrayBlock[koalabear.Element]](c Circuit, schedule constraint return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -351,12 +351,12 @@ func Verify[D hash.ArrayBlock[koalabear.Element]](c Circuit, schedule constraint gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -422,8 +422,8 @@ func iterateElems(elems []extensions.E6, counter *int, yield func(int, *extensio } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *extensions.E6] { return func(yield func(int, *extensions.E6) bool) { diff --git a/gkr/koalabear/sumcheck.go b/gkr/koalabear/sumcheck.go index 862fc07cc1..ee19ac0afb 100644 --- a/gkr/koalabear/sumcheck.go +++ b/gkr/koalabear/sumcheck.go @@ -26,10 +26,11 @@ type transcript = gkrcore.Transcript[extensions.E6] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.PolynomialE6 // compute gⱼ polynomial for current round - roundFold(r extensions.E6) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []extensions.E6) []extensions.E6 // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.PolynomialE6 // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne extensions.E6) extensions.E6 // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r extensions.E6) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []extensions.E6) []extensions.E6 // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -41,49 +42,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.PolynomialE6 - finalEvalProof []extensions.E6 //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.PolynomialE6 // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []extensions.E6 //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum extensions.E6, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.PolynomialE6, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]extensions.E6, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.PolynomialE6, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRangeE6(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum extensions.E6, degree int, t transcript) error { r := make([]extensions.E6, claims.varsNum()) - gJ := make(polynomial.PolynomialE6, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*extensions.VectorE6)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRangeE6(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -349,6 +359,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.PolynomialE6 { return c.roundPolynomialExt() } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne extensions.E6) extensions.E6 { + var res extensions.E6 + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r extensions.E6) { @@ -491,15 +508,13 @@ func (c *zeroCheckBase) proveFinalEval(r []extensions.E6, extraPolys []polynomia return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff extensions.E6) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLinE6, len(uniqueInputs)) @@ -527,8 +542,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -576,15 +593,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (extensions.E6, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum extensions.E6) { level := r.schedule[levelI] - var foldingCoeff extensions.E6 if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -593,43 +610,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (extensions.E6, *z for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLinE6 // contiguous buffer; second half is the current round's eq segment + q []extensions.E6 // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne extensions.E6) extensions.E6 { + var res, oneMinusQj extensions.E6 + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomialExt computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomialExt computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. // It is used for every round after the first, which runs entirely over the extension. @@ -676,7 +704,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialExt() polynomial.Polynomial iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -712,8 +740,8 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialExt() polynomial.Polynomial return p } -// roundPolynomialBaseInputs computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomialBaseInputs computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. // It is used for the first round, whose input tables are base field columns. @@ -760,7 +788,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialBaseInputs() polynomial.Pol iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -840,7 +868,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []extensions.E6) []extens // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -863,7 +891,7 @@ func (r *resources) buildSuffixEq(q []extensions.E6) polynomial.MultiLinE6 { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -887,20 +915,27 @@ func (r *resources) buildSuffixEq(q []extensions.E6) polynomial.MultiLinE6 { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -908,44 +943,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]extensions.E6, r.nbVars) - gPrime := make(polynomial.PolynomialE6, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 extensions.E6 - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*extensions.VectorE6)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRangeE6(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEqE6(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/koalabear/sumcheck_test.go b/gkr/koalabear/sumcheck_test.go index b95511a169..e36c19eafb 100644 --- a/gkr/koalabear/sumcheck_test.go +++ b/gkr/koalabear/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewExtensionTranscript[extensions.E6](hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.PolynomialE6 { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne extensions.E6) extensions.E6 { + var res extensions.E6 + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r extensions.E6) { c.g.Fold(r) } diff --git a/gkr/mamabear/gkr.go b/gkr/mamabear/gkr.go index cf53d0424c..5c74f6f746 100644 --- a/gkr/mamabear/gkr.go +++ b/gkr/mamabear/gkr.go @@ -85,6 +85,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // evaluateBase returns the evaluation of the multilinear extension of the base field column col at @@ -139,11 +140,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -155,7 +156,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -178,22 +179,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -233,7 +232,7 @@ func Prove[D hash.ArrayBlock[mamabear.Element]](c Circuit, schedule constraint.G } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]extensions.E3, r.nbVars) @@ -247,7 +246,7 @@ func Prove[D hash.ArrayBlock[mamabear.Element]](c Circuit, schedule constraint.G for i, w := range outputs { outputEvals[i] = r.evaluateBase(r.assignment[w], firstChallenge) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []extensions.E3 for i, w := range outputs { if r.consolidated[w] { @@ -258,24 +257,24 @@ func Prove[D hash.ArrayBlock[mamabear.Element]](c Circuit, schedule constraint.G gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -283,8 +282,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -303,6 +302,7 @@ func Verify[D hash.ArrayBlock[mamabear.Element]](c Circuit, schedule constraint. return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -351,12 +351,12 @@ func Verify[D hash.ArrayBlock[mamabear.Element]](c Circuit, schedule constraint. gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -422,8 +422,8 @@ func iterateElems(elems []extensions.E3, counter *int, yield func(int, *extensio } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *extensions.E3] { return func(yield func(int, *extensions.E3) bool) { diff --git a/gkr/mamabear/sumcheck.go b/gkr/mamabear/sumcheck.go index 578a3a890d..59b7280d50 100644 --- a/gkr/mamabear/sumcheck.go +++ b/gkr/mamabear/sumcheck.go @@ -26,10 +26,11 @@ type transcript = gkrcore.Transcript[extensions.E3] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.PolynomialE3 // compute gⱼ polynomial for current round - roundFold(r extensions.E3) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []extensions.E3) []extensions.E3 // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.PolynomialE3 // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne extensions.E3) extensions.E3 // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r extensions.E3) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []extensions.E3) []extensions.E3 // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -41,49 +42,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.PolynomialE3 - finalEvalProof []extensions.E3 //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.PolynomialE3 // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []extensions.E3 //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum extensions.E3, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.PolynomialE3, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]extensions.E3, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.PolynomialE3, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRangeE3(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum extensions.E3, degree int, t transcript) error { r := make([]extensions.E3, claims.varsNum()) - gJ := make(polynomial.PolynomialE3, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*extensions.VectorE3)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRangeE3(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -349,6 +359,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.PolynomialE3 { return c.roundPolynomialExt() } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne extensions.E3) extensions.E3 { + var res extensions.E3 + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r extensions.E3) { @@ -491,15 +508,13 @@ func (c *zeroCheckBase) proveFinalEval(r []extensions.E3, extraPolys []polynomia return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff extensions.E3) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLinE3, len(uniqueInputs)) @@ -527,8 +542,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -576,15 +593,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (extensions.E3, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum extensions.E3) { level := r.schedule[levelI] - var foldingCoeff extensions.E3 if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -593,43 +610,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (extensions.E3, *z for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLinE3 // contiguous buffer; second half is the current round's eq segment + q []extensions.E3 // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne extensions.E3) extensions.E3 { + var res, oneMinusQj extensions.E3 + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomialExt computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomialExt computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. // It is used for every round after the first, which runs entirely over the extension. @@ -676,7 +704,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialExt() polynomial.Polynomial iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -712,8 +740,8 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialExt() polynomial.Polynomial return p } -// roundPolynomialBaseInputs computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomialBaseInputs computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. // It is used for the first round, whose input tables are base field columns. @@ -760,7 +788,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomialBaseInputs() polynomial.Pol iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -840,7 +868,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []extensions.E3) []extens // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -863,7 +891,7 @@ func (r *resources) buildSuffixEq(q []extensions.E3) polynomial.MultiLinE3 { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -887,20 +915,27 @@ func (r *resources) buildSuffixEq(q []extensions.E3) polynomial.MultiLinE3 { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -908,44 +943,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]extensions.E3, r.nbVars) - gPrime := make(polynomial.PolynomialE3, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 extensions.E3 - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*extensions.VectorE3)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRangeE3(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEqE3(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/gkr/mamabear/sumcheck_test.go b/gkr/mamabear/sumcheck_test.go index 17f5b0545f..d43c6ea409 100644 --- a/gkr/mamabear/sumcheck_test.go +++ b/gkr/mamabear/sumcheck_test.go @@ -30,7 +30,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewExtensionTranscript[extensions.E3](hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { @@ -113,6 +113,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.PolynomialE3 { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne extensions.E3) extensions.E3 { + var res extensions.E3 + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r extensions.E3) { c.g.Fold(r) } diff --git a/go.mod b/go.mod index 9ae9a1ecb5..fe03298a77 100644 --- a/go.mod +++ b/go.mod @@ -7,7 +7,7 @@ require ( github.com/blang/semver/v4 v4.0.0 github.com/consensys/bavard v0.2.2-0.20260118153501-cba9f5475432 github.com/consensys/compress v0.3.0 - github.com/consensys/gnark-crypto v0.22.1-0.20261103155519-1a9aede5b1c3 + github.com/consensys/gnark-crypto v0.22.1-0.20261105032453-23c660cd7688 github.com/fxamacker/cbor/v2 v2.9.2 github.com/google/go-cmp v0.7.0 github.com/google/pprof v0.0.0-20260802141513-ef3492d7dac3 diff --git a/go.sum b/go.sum index 2018272ca0..f1ff2777db 100644 --- a/go.sum +++ b/go.sum @@ -61,8 +61,8 @@ github.com/consensys/bavard v0.2.2-0.20260118153501-cba9f5475432 h1:4ACburMEVC+u github.com/consensys/bavard v0.2.2-0.20260118153501-cba9f5475432/go.mod h1:k/zVjHHC4B+PQy1Pg7fgvG3ALicQw540Crag8qx+dZs= github.com/consensys/compress v0.3.0 h1:HRIcHvWkW9C9req0ZWg7mhYHzBarohXhcszIwHONVkM= github.com/consensys/compress v0.3.0/go.mod h1:pyM+ZXiNUh7/0+AUjUf9RKUM6vSH7T/fsn5LLS0j1Tk= -github.com/consensys/gnark-crypto v0.22.1-0.20261103155519-1a9aede5b1c3 h1:XYMiyi5Qn8+4QBQE9UzmFw1hwNPMkJaYtExUexWkDak= -github.com/consensys/gnark-crypto v0.22.1-0.20261103155519-1a9aede5b1c3/go.mod h1:+GBvEPnGIwDMfw6RJdxtImW8wHcBDaveR3s8URlDAc0= +github.com/consensys/gnark-crypto v0.22.1-0.20261105032453-23c660cd7688 h1:CotLmoIaf2CkrtTS4p05ewaYlqI/iZHJiQbI0URIT7M= +github.com/consensys/gnark-crypto v0.22.1-0.20261105032453-23c660cd7688/go.mod h1:+GBvEPnGIwDMfw6RJdxtImW8wHcBDaveR3s8URlDAc0= github.com/coreos/go-semver v0.3.0/go.mod h1:nnelYz7RCh+5ahJtPPxZlU+153eP4D4r3EedlOD2RNk= github.com/coreos/go-systemd/v22 v22.3.2/go.mod h1:Y58oyj3AT4RCenI/lSvhwexgC+NSVTIJ3seZv2GcEnc= github.com/cpuguy83/go-md2man/v2 v2.0.0/go.mod h1:maD7wRr/U5Z6m/iR4s+kqSMx2CaBsrgA7czyZG/E6dU= diff --git a/internal/generator/backend/template/gkr/evaluator.go.tmpl b/internal/generator/backend/template/gkr/evaluator.go.tmpl index 14df9afcaa..f1e3b1a2c6 100644 --- a/internal/generator/backend/template/gkr/evaluator.go.tmpl +++ b/internal/generator/backend/template/gkr/evaluator.go.tmpl @@ -163,7 +163,7 @@ func (e *{{ $ge }}) Evaluate(top ...{{ $elem }}) *{{ $elem }} { {{- end }} dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum {{ $elem }} {{- if .Mixed }} if e.isInputConstant(inst, 0) { diff --git a/internal/generator/backend/template/gkr/gkr.go.tmpl b/internal/generator/backend/template/gkr/gkr.go.tmpl index 256c6f60c5..6cfdba71d4 100644 --- a/internal/generator/backend/template/gkr/gkr.go.tmpl +++ b/internal/generator/backend/template/gkr/gkr.go.tmpl @@ -91,6 +91,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } {{ if .Mixed -}} @@ -155,11 +156,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -171,7 +172,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -194,22 +195,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -253,7 +252,7 @@ func Prove{{ $typeParams }}(c Circuit, schedule constraint.GkrProvingSchedule, a } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]{{ .ElementType }}, r.nbVars) @@ -271,7 +270,7 @@ func Prove{{ $typeParams }}(c Circuit, schedule constraint.GkrProvingSchedule, a outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) {{- end }} } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []{{ .ElementType }} for i, w := range outputs { if r.consolidated[w] { @@ -282,24 +281,24 @@ func Prove{{ $typeParams }}(c Circuit, schedule constraint.GkrProvingSchedule, a gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -307,8 +306,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -327,6 +326,7 @@ func Verify{{ $typeParams }}(c Circuit, schedule constraint.GkrProvingSchedule, return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -375,12 +375,12 @@ func Verify{{ $typeParams }}(c Circuit, schedule constraint.GkrProvingSchedule, gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -446,8 +446,8 @@ func iterateElems(elems []{{ .ElementType }}, counter *int, yield func(int, *{{ } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *{{ .ElementType }}] { return func(yield func(int, *{{ .ElementType }}) bool) { diff --git a/internal/generator/backend/template/gkr/sumcheck.go.tmpl b/internal/generator/backend/template/gkr/sumcheck.go.tmpl index 2de01c695d..fcebca322e 100644 --- a/internal/generator/backend/template/gkr/sumcheck.go.tmpl +++ b/internal/generator/backend/template/gkr/sumcheck.go.tmpl @@ -24,7 +24,8 @@ type transcript = gkrcore.Transcript[{{ .ElementType }}] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial{{ .ExtensionSuffix }} // compute gⱼ polynomial for current round + roundPolynomial() polynomial.Polynomial{{ .ExtensionSuffix }} // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne {{ .ElementType }}) {{ .ElementType }} // recover gⱼ(0) from the current claim and gⱼ(1) roundFold(r {{ .ElementType }}) // fold inputs and eq at challenge r varsNum() int // number of variables proveFinalEval(r []{{ .ElementType }}) []{{ .ElementType }} // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof @@ -39,49 +40,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial{{ .ExtensionSuffix }} + partialSumPolys []polynomial.Polynomial{{ .ExtensionSuffix }} // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier finalEvalProof []{{ .ElementType }} //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum {{ .ElementType }}, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial{{ .ExtensionSuffix }}, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]{{ .ElementType }}, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial{{ .ExtensionSuffix }}, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange{{ .ExtensionSuffix }}(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum {{ .ElementType }}, degree int, t transcript) error { r := make([]{{ .ElementType }}, claims.varsNum()) - gJ := make(polynomial.Polynomial{{ .ExtensionSuffix }}, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*{{ .FieldPackageName }}.Vector{{ .ExtensionSuffix }})(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange{{ .ExtensionSuffix }}(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -175,6 +185,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial{{ .ExtensionSu } {{- end }} +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne {{ .ElementType }}) {{ .ElementType }} { + var res {{ .ElementType }} + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r {{ .ElementType }}) { @@ -337,15 +354,13 @@ func (c *zeroCheckBase) proveFinalEval(r []{{ .ElementType }}, extraPolys []poly return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff {{ .ElementType }}) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin{{ .ExtensionSuffix }}, len(uniqueInputs)) @@ -383,8 +398,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -432,15 +449,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) ({{ .ElementType }}, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum {{ .ElementType }}) { level := r.schedule[levelI] - var foldingCoeff {{ .ElementType }} if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -449,39 +466,50 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) ({{ .ElementType } for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin{{ .ExtensionSuffix }} // contiguous buffer; second half is the current round's eq segment + q []{{ .ElementType }} // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne {{ .ElementType }}) {{ .ElementType }} { + var res, oneMinusQj {{ .ElementType }} + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } {{ template "singleSourceRoundPolynomial" dict "Config" . "Base" false }} @@ -548,7 +576,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []{{ .ElementType }}) []{ // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -571,7 +599,7 @@ func (r *resources) buildSuffixEq(q []{{ .ElementType }}) polynomial.MultiLin{{ buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -595,20 +623,27 @@ func (r *resources) buildSuffixEq(q []{{ .ElementType }}) polynomial.MultiLin{{ func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -616,46 +651,41 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]{{ .ElementType }}, r.nbVars) - gPrime := make(polynomial.Polynomial{{ .ExtensionSuffix }}, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 {{ .ElementType }} - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*{{ .FieldPackageName }}.Vector{{ .ExtensionSuffix }})(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange{{ .ExtensionSuffix }}(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq{{ .ExtensionSuffix }}(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } {{ define "zeroCheckRoundPolynomial" -}} @@ -789,8 +819,8 @@ func (c *zeroCheckClaims) {{ $name }}() polynomial.Polynomial{{ .Config.Extensio {{- $use = "\n// It is used for every round after the first, which runs entirely over the extension." }} {{- $ge = "GateEvaluatorMixed" }} {{- end }} -// {{ $name }} computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// {{ $name }} computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0.{{ $use }} func (c *singleSourceZeroCheckClaims) {{ $name }}() polynomial.Polynomial{{ .Config.ExtensionSuffix }} { @@ -836,7 +866,7 @@ func (c *singleSourceZeroCheckClaims) {{ $name }}() polynomial.Polynomial{{ .Con iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } diff --git a/internal/generator/backend/template/gkr/sumcheck.test.defs.go.tmpl b/internal/generator/backend/template/gkr/sumcheck.test.defs.go.tmpl index 06b06c13ee..3236750fd9 100644 --- a/internal/generator/backend/template/gkr/sumcheck.test.defs.go.tmpl +++ b/internal/generator/backend/template/gkr/sumcheck.test.defs.go.tmpl @@ -24,6 +24,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial{{ .Extensi return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne {{ .ElementType }}) {{ .ElementType }} { + var res {{ .ElementType }} + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r {{ .ElementType }}) { c.g.Fold(r) } diff --git a/internal/generator/backend/template/gkr/sumcheck.test.go.tmpl b/internal/generator/backend/template/gkr/sumcheck.test.go.tmpl index e2d6fb2826..78dae7b397 100644 --- a/internal/generator/backend/template/gkr/sumcheck.test.go.tmpl +++ b/internal/generator/backend/template/gkr/sumcheck.test.go.tmpl @@ -21,7 +21,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := {{ .NewTranscript }}(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { diff --git a/internal/generator/backend/template/gkr/sumcheck.test.vectors.gen.go.tmpl b/internal/generator/backend/template/gkr/sumcheck.test.vectors.gen.go.tmpl index 342d03aefe..3b81b27417 100644 --- a/internal/generator/backend/template/gkr/sumcheck.test.vectors.gen.go.tmpl +++ b/internal/generator/backend/template/gkr/sumcheck.test.vectors.gen.go.tmpl @@ -29,9 +29,14 @@ func runMultilin(testCaseInfo *sumcheckTestCaseInfo) error { return err } + var claimedSum rational.Element + if _, err = claimedSum.SetInterface(testCaseInfo.ClaimedSum); err != nil { + return err + } + claim := singleMultilinClaim{poly} t := gkrcore.NewNativeTranscript(hsh) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, claimedSum, t) testCaseInfo.Proof = sumcheckToPrintableProof(proof) // Verification @@ -40,11 +45,6 @@ func runMultilin(testCaseInfo *sumcheckTestCaseInfo) error { } else { return _err } - var claimedSum rational.Element - if _, err = claimedSum.SetInterface(testCaseInfo.ClaimedSum); err != nil { - return err - } - if hsh, err = hashFromDescription(testCaseInfo.Hash); err != nil { return err } diff --git a/internal/gkr/bls12-377/evaluator.go b/internal/gkr/bls12-377/evaluator.go index f232d443c3..050e362eb0 100644 --- a/internal/gkr/bls12-377/evaluator.go +++ b/internal/gkr/bls12-377/evaluator.go @@ -102,7 +102,7 @@ func (e *GateEvaluator) Evaluate(top ...fr.Element) *fr.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum fr.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) diff --git a/internal/gkr/bls12-381/evaluator.go b/internal/gkr/bls12-381/evaluator.go index 3a27deb35f..d0a7fd71ae 100644 --- a/internal/gkr/bls12-381/evaluator.go +++ b/internal/gkr/bls12-381/evaluator.go @@ -102,7 +102,7 @@ func (e *GateEvaluator) Evaluate(top ...fr.Element) *fr.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum fr.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) diff --git a/internal/gkr/bn254/evaluator.go b/internal/gkr/bn254/evaluator.go index 4be82328ee..07c5aeea4b 100644 --- a/internal/gkr/bn254/evaluator.go +++ b/internal/gkr/bn254/evaluator.go @@ -102,7 +102,7 @@ func (e *GateEvaluator) Evaluate(top ...fr.Element) *fr.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum fr.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) diff --git a/internal/gkr/bw6-761/evaluator.go b/internal/gkr/bw6-761/evaluator.go index a56ef53036..2f318a1481 100644 --- a/internal/gkr/bw6-761/evaluator.go +++ b/internal/gkr/bw6-761/evaluator.go @@ -102,7 +102,7 @@ func (e *GateEvaluator) Evaluate(top ...fr.Element) *fr.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum fr.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) diff --git a/internal/gkr/gkr.go b/internal/gkr/gkr.go index 4701073e6a..e164014273 100644 --- a/internal/gkr/gkr.go +++ b/internal/gkr/gkr.go @@ -210,7 +210,6 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]frontend.Variable, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) for j := range r.nbVars { partialSumPoly := proof[levelI].PartialSumPolys[j] @@ -218,21 +217,16 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er return errors.New("malformed proof") } - // Recover g'(0) from (1-q_j)*g'(0) + q_j*g'(1) = claimedSum - // g'(0) = (claimedSum - q_j * g'(1)) / (1 - q_j) - qjTimesGPrime1 := r.api.Mul(q[j], partialSumPoly[0]) // partialSumPoly[0] = g'(1) - numerator := r.api.Sub(claimedSum, qjTimesGPrime1) - oneMinusQj := r.api.Sub(1, q[j]) - gPrime[0] = r.api.Div(numerator, oneMinusQj) - - copy(gPrime[1:], partialSumPoly) + // (1-qⱼ)·g'(0) + qⱼ·g'(1) = claimedSum, with g'(0) = c₀ and g'(1) = ∑ᵢ₌₀ cᵢ, + // gives c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ + c0 := r.api.Sub(claimedSum, r.api.Mul(q[j], partialSumPoly.Eval(r.api, 1))) challenges[j] = r.t.Squeeze(proof[levelI].PartialSumPolys[j]...) - claimedSum = polynomial.InterpolateLDE(r.api, challenges[j], gPrime[:(degree+1)]) + claimedSum = r.api.Add(r.api.Mul(partialSumPoly.Eval(r.api, challenges[j]), challenges[j]), c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(r.api, q, challenges) claimedSum = r.api.Mul(eqAtQR, claimedSum) diff --git a/internal/gkr/gkrcore/gate.go b/internal/gkr/gkrcore/gate.go index 43d144b3f1..5c8b124419 100644 --- a/internal/gkr/gkrcore/gate.go +++ b/internal/gkr/gkrcore/gate.go @@ -140,7 +140,7 @@ func (gc *gateCompiler) recordCommutative(op gkr.GateOp, identity *big.Int, comb return gc.addInstruction(op, vars...) } -// SumExp17 records (a + b + c)^17 as a single instruction. If any of a, b, c is a constant, the +// SumExp17 records (a + b + c)¹⁷ as a single instruction. If any of a, b, c is a constant, the // first one found is read first. Constants are not merged. func (gc *gateCompiler) SumExp17(a, b, c frontend.Variable) frontend.Variable { operands := []frontend.Variable{a, b, c} @@ -301,10 +301,10 @@ func CompileGateFunction(f gkr.GateFunction, nbInputs int, field Field) (gkr.Ser }, nil } -// Field describes F_p[X]/(f); see gkr.Field. +// Field describes Fₚ[X]/(f); see gkr.Field. type Field = gkr.Field -// gateTester evaluates gate bytecode over a field F_p[X]/(f), to discover a gate's degree and +// gateTester evaluates gate bytecode over a field Fₚ[X]/(f), to discover a gate's degree and // solvable variable. An element is a []*big.Int of length field.Degree(), coefficient i the // coefficient of Xⁱ, each reduced mod p. For gkr.PrimeField, Degree() is 1, and every operation below // reduces to arithmetic mod p. @@ -511,7 +511,7 @@ func (t *gateTester) evaluate(inputs ...[]*big.Int) []*big.Int { case gkr.OpMulAcc: // a*b + c dst = t.mul(t.vars[inst.Inputs[0]], t.vars[inst.Inputs[1]]) dst = t.add(dst, t.vars[inst.Inputs[2]]) - case gkr.OpSumExp17: // (a + b + c)^17 + case gkr.OpSumExp17: // (a + b + c)¹⁷ dst = t.add(t.vars[inst.Inputs[0]], t.vars[inst.Inputs[1]]) dst = t.add(dst, t.vars[inst.Inputs[2]]) dst = t.pow(dst, big.NewInt(17)) diff --git a/internal/gkr/koalabear/evaluator.go b/internal/gkr/koalabear/evaluator.go index d030c6c18f..c5699f025b 100644 --- a/internal/gkr/koalabear/evaluator.go +++ b/internal/gkr/koalabear/evaluator.go @@ -104,7 +104,7 @@ func (e *GateEvaluator) Evaluate(top ...koalabear.Element) *koalabear.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum koalabear.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) @@ -288,7 +288,7 @@ func (e *GateEvaluatorMixed) Evaluate(top ...extensions.E6) *extensions.E6 { } dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum extensions.E6 if e.isInputConstant(inst, 0) { sum.AddElement(&e.vars[inst.Inputs[1]], &e.consts[inst.Inputs[0]]) diff --git a/internal/gkr/mamabear/evaluator.go b/internal/gkr/mamabear/evaluator.go index 3d1d4e9932..27beb2210d 100644 --- a/internal/gkr/mamabear/evaluator.go +++ b/internal/gkr/mamabear/evaluator.go @@ -104,7 +104,7 @@ func (e *GateEvaluator) Evaluate(top ...mamabear.Element) *mamabear.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum mamabear.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) @@ -288,7 +288,7 @@ func (e *GateEvaluatorMixed) Evaluate(top ...extensions.E3) *extensions.E3 { } dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum extensions.E3 if e.isInputConstant(inst, 0) { sum.AddElement(&e.vars[inst.Inputs[1]], &e.consts[inst.Inputs[0]]) diff --git a/internal/gkr/rational/evaluator.go b/internal/gkr/rational/evaluator.go index 43a7f0c5b9..c86c273ed9 100644 --- a/internal/gkr/rational/evaluator.go +++ b/internal/gkr/rational/evaluator.go @@ -102,7 +102,7 @@ func (e *GateEvaluator) Evaluate(top ...rational.Element) *rational.Element { prod.Mul(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) dst.Add(&prod, &e.vars[inst.Inputs[2]]) case gkr.OpSumExp17: - // result = (x[0] + x[1] + x[2])^17 + // result = (x[0] + x[1] + x[2])¹⁷ var sum rational.Element sum.Add(&e.vars[inst.Inputs[0]], &e.vars[inst.Inputs[1]]) sum.Add(&sum, &e.vars[inst.Inputs[2]]) diff --git a/internal/gkr/rational/gkr.go b/internal/gkr/rational/gkr.go index 2ee6c45d14..722d08656a 100644 --- a/internal/gkr/rational/gkr.go +++ b/internal/gkr/rational/gkr.go @@ -81,6 +81,7 @@ type resources struct { claimValueIndices [][]int // claimValueIndices[wI][claimI]: index of w's claimI-th claimed value in its source level's finalEvalProof claims Claims consolidated []bool // the wires of schedule[0], indexed by wire + proof Proof // the proof being built by Prove or checked by Verify } // identityGate is the identity gate LevelCircuit and consolidationView use to build level 0's @@ -130,11 +131,11 @@ func (r *resources) proveSkipLevel(levelI int) sumcheckProof { // verifySkipLevel verifies a SkipSumcheck level: checks that the finalEvalProof is consistent with // the gate evaluations, and records outgoing eval points. -func (r *resources) verifySkipLevel(levelI int, proof Proof) error { +func (r *resources) verifySkipLevel(levelI int) error { level := r.schedule[levelI].(*constraint.GkrSkipLevel) gkrcore.CollectOutgoingEvalPoints(level, levelI, r.outgoingEvalPoints) - finalEval := proof[levelI].finalEvalProof + finalEval := r.proof[levelI].finalEvalProof _, inputIndices := r.circuit.InputMapping(level) group := constraint.GkrClaimGroup(*level) @@ -146,7 +147,7 @@ func (r *resources) verifySkipLevel(levelI int, proof Proof) error { evaluator.PushInput(finalEval[level.FinalEvalProofIndex(inI, claimI)]) } gateEval := evaluator.Evaluate() - claimedEval := proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] + claimedEval := r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]] if !claimedEval.Equal(gateEval) { return fmt.Errorf("level %d wire %d claim %d: claimed eval %v disagrees with gate eval %v", levelI, wI, claimI, &claimedEval, gateEval) } @@ -169,22 +170,20 @@ func (r *resources) levelPredicates(levelI int) (absorb, include func(wI int) bo } // proveLevel proves level levelI: computes its proof entry, absorbs its values, and appends its claims. -func (r *resources) proveLevel(levelI int) sumcheckProof { - var entry sumcheckProof +func (r *resources) proveLevel(levelI int) { switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - entry = r.proveSkipLevel(levelI) + r.proof[levelI] = r.proveSkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - entry = r.proveSingleSourceZeroCheckLevel(levelI) + r.proof[levelI] = r.proveSingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - entry = r.proveSumcheckLevel(levelI) + r.proof[levelI] = r.proveSumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, entry.finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], entry.finalEvalProof, r.outgoingEvalPoints[levelI], include) - return entry + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) } // Prove consistency of the claimed assignment. It returns the evaluation claims on the circuit's @@ -224,7 +223,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss } } - proof := make(Proof, len(schedule)+1) + r.proof = make(Proof, len(schedule)+1) // Derive the initial challenge point firstChallenge := make([]rational.Element, r.nbVars) @@ -238,7 +237,7 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss for i, w := range outputs { outputEvals[i] = r.assignment[w].Evaluate(firstChallenge, &r.memPool) } - proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} + r.proof[len(schedule)] = sumcheckProof{finalEvalProof: outputEvals} var absorbedOutputEvals []rational.Element for i, w := range outputs { if r.consolidated[w] { @@ -249,24 +248,24 @@ func Prove(c Circuit, schedule constraint.GkrProvingSchedule, assignment WireAss gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputEvals, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - proof[levelI] = r.proveLevel(levelI) + r.proveLevel(levelI) } r.circuit = r.circuit.LevelCircuit(r.schedule, 0, identityGate()) - proof[0] = r.proveLevel(0) + r.proveLevel(0) - return proof, r.claims, nil + return r.proof, r.claims, nil } // verifyLevel verifies level levelI: checks its proof entry, absorbs its values, and appends its claims. -func (r *resources) verifyLevel(levelI int, proof Proof) error { +func (r *resources) verifyLevel(levelI int) error { var err error switch r.schedule[levelI].(type) { case *constraint.GkrSkipLevel: - err = r.verifySkipLevel(levelI, proof) + err = r.verifySkipLevel(levelI) case *constraint.GkrSingleSourceZeroCheckLevel: - err = r.verifySingleSourceZeroCheckLevel(levelI, proof) + err = r.verifySingleSourceZeroCheckLevel(levelI) case *constraint.GkrSumcheckLevel: - err = r.verifySumcheckLevel(levelI, proof) + err = r.verifySumcheckLevel(levelI) default: panic(fmt.Sprintf("level %d: unknown proving level type %T", levelI, r.schedule[levelI])) } @@ -274,8 +273,8 @@ func (r *resources) verifyLevel(levelI int, proof Proof) error { return fmt.Errorf("level %d: %v", levelI, err) } absorb, include := r.levelPredicates(levelI) - constraint.AbsorbGkrFinalEvalProof(r.transcript, proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) - gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) + constraint.AbsorbGkrFinalEvalProof(r.transcript, r.proof[levelI].finalEvalProof, gkrcore.UniqueGateInputs(r.circuit, r.schedule[levelI]), absorb, r.schedule[levelI]) + gkrcore.AppendLevelClaims(r.claims, r.circuit, r.schedule[levelI], r.proof[levelI].finalEvalProof, r.outgoingEvalPoints[levelI], include) return nil } @@ -294,6 +293,7 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in return nil, errors.New("number of variables must be positive") } r := newResources(c, schedule, logNbInstances, hasher) + r.proof = proof if len(proof) != len(schedule)+1 { return nil, fmt.Errorf("proof has %d levels, expected %d", len(proof), len(schedule)+1) @@ -342,12 +342,12 @@ func Verify(c Circuit, schedule constraint.GkrProvingSchedule, logNbInstances in gkrcore.AppendOutputClaims(r.claims, c, firstChallenge, outputLevel.finalEvalProof, func(wI int) bool { return !r.consolidated[wI] }) for levelI := len(schedule) - 1; levelI >= 1; levelI-- { - if err := r.verifyLevel(levelI, proof); err != nil { + if err := r.verifyLevel(levelI); err != nil { return nil, err } } r.circuit = view - if err := r.verifyLevel(0, proof); err != nil { + if err := r.verifyLevel(0); err != nil { return nil, err } return r.claims, nil @@ -413,8 +413,8 @@ func iterateElems(elems []rational.Element, counter *int, yield func(int, *ratio } // Flatten yields the proof's elements by position. For each entry of the proof, in order, it -// yields the evaluations at 1, …, d of its partial sum polynomials, d being their degree, then its -// final evaluations. +// yields the coefficients of degree 1 to d of its partial sum polynomials, d being their degree, +// then its final evaluations. // DeserializeProof reads the same order. func (p Proof) Flatten() iter.Seq2[int, *rational.Element] { return func(yield func(int, *rational.Element) bool) { diff --git a/internal/gkr/rational/sumcheck.go b/internal/gkr/rational/sumcheck.go index 2cb7029e63..b9f52c544b 100644 --- a/internal/gkr/rational/sumcheck.go +++ b/internal/gkr/rational/sumcheck.go @@ -23,10 +23,11 @@ type transcript = gkrcore.Transcript[rational.Element] // sumcheckClaims to a multi-sumcheck statement. i.e. one of the form ∑_{0≤i<2ⁿ} fⱼ(i) = cⱼ for 1 ≤ j ≤ m. // Later evolving into a claim of the form gⱼ = ∑_{0≤i<2ⁿ⁻ʲ} g(r₁, r₂, ..., rⱼ₋₁, Xⱼ, i...) type sumcheckClaims interface { - roundPolynomial() polynomial.Polynomial // compute gⱼ polynomial for current round - roundFold(r rational.Element) // fold inputs and eq at challenge r - varsNum() int // number of variables - proveFinalEval(r []rational.Element) []rational.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + roundPolynomial() polynomial.Polynomial // compute the evaluations gⱼ(1), ..., gⱼ(d) of the polynomial of the current round + evaluationAtZero(round int, claim, atOne rational.Element) rational.Element // recover gⱼ(0) from the current claim and gⱼ(1) + roundFold(r rational.Element) // fold inputs and eq at challenge r + varsNum() int // number of variables + proveFinalEval(r []rational.Element) []rational.Element // in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } // sumcheckLazyClaims is the sumcheckClaims data structure on the verifier side. It is "lazy" in that it has to compute fewer things. @@ -38,49 +39,58 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-statement. type sumcheckProof struct { - partialSumPolys []polynomial.Polynomial - finalEvalProof []rational.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof + partialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier + finalEvalProof []rational.Element //in case it is difficult for the verifier to compute g(r₁, ..., rₙ) on its own, the prover can provide the value and a proof } -// sumcheckProve creates a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (proveLevel). -// Pattern: roundPolynomial, [roundFold, roundPolynomial]*, proveFinalEval. -func sumcheckProve(claims sumcheckClaims, t transcript) sumcheckProof { +// sumcheckProve creates a non-interactive sumcheck proof. claimedSum is the sum being proved. +// The fold challenge is derived by the caller (foldClaims). +// Pattern: [roundPolynomial, evaluationAtZero, roundFold]*, proveFinalEval. +func sumcheckProve(claims sumcheckClaims, claimedSum rational.Element, t transcript) sumcheckProof { varsNum := claims.varsNum() proof := sumcheckProof{partialSumPolys: make([]polynomial.Polynomial, varsNum)} - proof.partialSumPolys[0] = claims.roundPolynomial() challenges := make([]rational.Element, varsNum) - for j := range varsNum - 1 { + for j := range varsNum { + evals := claims.roundPolynomial() + gJ := make(polynomial.Polynomial, len(evals)+1) + copy(gJ[1:], evals) + gJ[0] = claims.evaluationAtZero(j, claimedSum, evals[0]) + + gJCoeffs := polynomial.InterpolateOnRange(gJ) + proof.partialSumPolys[j] = gJCoeffs[1:] challenges[j] = t.Squeeze(proof.partialSumPolys[j]...) - claims.roundFold(challenges[j]) - proof.partialSumPolys[j+1] = claims.roundPolynomial() + claimedSum = gJCoeffs.Eval(&challenges[j]) + if j+1 < varsNum { + claims.roundFold(challenges[j]) + } } - challenges[varsNum-1] = t.Squeeze(proof.partialSumPolys[varsNum-1]...) proof.finalEvalProof = claims.proveFinalEval(challenges) return proof } // sumcheckVerify verifies a non-interactive sumcheck proof. -// The fold challenge is derived by the caller (verifyLevel). +// The fold challenge is derived by the caller (foldClaims). // claimedSum is the expected sum; degree is the polynomial's degree in each variable. func sumcheckVerify(claims sumcheckLazyClaims, proof sumcheckProof, claimedSum rational.Element, degree int, t transcript) error { r := make([]rational.Element, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum - + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { if len(proof.partialSumPolys[j]) != degree { return errors.New("malformed proof") } - copy(gJ[1:], proof.partialSumPolys[j]) - gJ[0].Sub(&gJR, &proof.partialSumPolys[j][0]) + + c0 := (*rational.Vector)(&proof.partialSumPolys[j]).Sum() + c0.Sub(&gJR, &c0) + c0.Halve() r[j] = t.Squeeze(proof.partialSumPolys[j]...) - gJCoeffs := polynomial.InterpolateOnRange(gJ[:(degree + 1)]) - gJR = gJCoeffs.Eval(&r[j]) + gJR = proof.partialSumPolys[j].Eval(&r[j]) + gJR.Mul(&gJR, &r[j]) + gJR.Add(&gJR, &c0) } return claims.verifyFinalEval(r, gJR, proof.finalEvalProof) @@ -247,6 +257,13 @@ func (c *zeroCheckClaims) roundPolynomial() polynomial.Polynomial { return p } +// evaluationAtZero returns gⱼ(0) = claim - gⱼ(1), as gⱼ(0) + gⱼ(1) = claim. +func (c *zeroCheckClaims) evaluationAtZero(_ int, claim, atOne rational.Element) rational.Element { + var res rational.Element + res.Sub(&claim, &atOne) + return res +} + // roundFold folds all input and eq polynomials at the verifier challenge r. // After this call, j ← j+1 and rⱼ = r. func (c *zeroCheckClaims) roundFold(r rational.Element) { @@ -353,15 +370,13 @@ func (c *zeroCheckBase) proveFinalEval(r []rational.Element, extraPolys []polyno return evaluations } -// init derives the folding coefficient, sets up the input multilinears, +// init sets the folding coefficient, sets up the input multilinears, // and builds gate evaluator pools — the steps common to all sumcheck-family provers. -func (c *zeroCheckBase) init(r *resources, levelI int) { +func (c *zeroCheckBase) init(r *resources, levelI int, foldingCoeff rational.Element) { c.levelI = levelI c.resources = r + c.foldingCoeff = foldingCoeff level := r.schedule[levelI] - if level.NbClaims() >= 2 { - c.foldingCoeff = r.transcript.Squeeze() - } uniqueInputs, inputIndices := r.circuit.InputMapping(level) c.input = make([]polynomial.MultiLin, len(uniqueInputs)) @@ -386,8 +401,10 @@ func (c *zeroCheckBase) init(r *resources, levelI int) { } func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { + foldingCoeff, claimedSum := r.foldClaims(levelI) + var claims zeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) level := r.schedule[levelI] eqLength := 1 << r.nbVars @@ -435,15 +452,15 @@ func (r *resources) proveSumcheckLevel(levelI int) sumcheckProof { } } - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -// verifyLevelSetup derives the folding coefficient, collects all claimed wire -// evaluations from the proof or the initial assignment, computes the batched -// claimed sum, and builds the lazy-claims object shared by both verifiers. -func (r *resources) verifyLevelSetup(levelI int, proof Proof) (rational.Element, *zeroCheckLazyClaims) { +// foldClaims squeezes the folding coefficient of level levelI if it has at least two claims, and +// returns it with the sum the level's sumcheck proves: the claimed values of the level's wires, +// folded by the coefficient. The values are read from r.proof, which must hold the entries of the +// levels the claims come from. +func (r *resources) foldClaims(levelI int) (foldingCoeff, claimedSum rational.Element) { level := r.schedule[levelI] - var foldingCoeff rational.Element if level.NbClaims() >= 2 { foldingCoeff = r.transcript.Squeeze() } @@ -452,43 +469,54 @@ func (r *resources) verifyLevelSetup(levelI int, proof Proof) (rational.Element, for _, group := range level.ClaimGroups() { for _, wI := range group.Wires { for claimI, src := range group.ClaimSources { - claimedEvals = append(claimedEvals, proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) + claimedEvals = append(claimedEvals, r.proof[src.Level].finalEvalProof[r.claimValueIndices[wI][claimI]]) } } } + return foldingCoeff, claimedEvals.Eval(&foldingCoeff) +} - return claimedEvals.Eval(&foldingCoeff), &zeroCheckLazyClaims{ +func (r *resources) verifySumcheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ foldingCoeff: foldingCoeff, resources: r, levelI: levelI, } -} - -func (r *resources) verifySumcheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) level := r.schedule[levelI].(*constraint.GkrSumcheckLevel) - return sumcheckVerify(lazyClaims, proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) + return sumcheckVerify(lazyClaims, r.proof[levelI], claimedSum, r.circuit.ZeroCheckDegree(level), r.transcript) } // singleSourceZeroCheckClaims is the prover-side claim for a single-source // zerocheck with the eq polynomial factored out (Section 3.2 of ePrint 2024/108). // // When a level has exactly one claim source with evaluation point q, the standard -// round polynomial g_j(X) = Σ_h eq(q, (r₀…r_{j-1}, X, h)) · G(r₀…r_{j-1}, X, h) +// round polynomial gⱼ(X) = Σₕ eq(q, (r₀…rⱼ₋₁, X, h)) · G(r₀…rⱼ₋₁, X, h) // has degree d+1 (one from eq, d from the gate). Factoring out the per-variable eq -// gives g_j(X) = eq(q_j, X) · g'_j(X) where g'_j has degree d. The prover sends +// gives gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X) where g'ⱼ has degree d. The prover sends // d evaluations per round instead of d+1, saving one field element per variable and // reducing the number of gate evaluations per hypercube point from d+1 to d. // -// The suffix eq tables eq(q_{j+1}…q_{N-1}; ·) are precomputed bottom-up and used +// The suffix eq tables eq(qⱼ₊₁…q_{N-1}; ·) are precomputed bottom-up and used // read-only as weights in each round; only the input multilinears are folded. type singleSourceZeroCheckClaims struct { zeroCheckBase suffixEq polynomial.MultiLin // contiguous buffer; second half is the current round's eq segment + q []rational.Element // the evaluation point of the claim source +} + +// evaluationAtZero returns g'ⱼ(0) = (claim - qⱼ·g'ⱼ(1)) / (1 - qⱼ), from (1 - qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) = claim. +func (c *singleSourceZeroCheckClaims) evaluationAtZero(round int, claim, atOne rational.Element) rational.Element { + var res, oneMinusQj rational.Element + res.Mul(&c.q[round], &atOne) + res.Sub(&claim, &res) + oneMinusQj.SetOne() + oneMinusQj.Sub(&oneMinusQj, &c.q[round]) + return *res.Div(&res, &oneMinusQj) } -// roundPolynomial computes g'_j(1), ..., g'_j(d) where d is the gate degree. -// g'_j(m) = ∑_h suffixEq[j+1][h] · ∑_w α^w · gate_w(inputs at (m, h)) +// roundPolynomial computes g'ⱼ(1), ..., g'ⱼ(d) where d is the gate degree. +// g'ⱼ(m) = ∑ₕ suffixEq[j+1][h] · ∑_w αʷ · gate_w(inputs at (m, h)) // The wire contributions are accumulated via Horner's method in α (= foldingCoeff), // eliminating precomputed batchCoeffs and the multiply-by-one for wire 0. func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { @@ -534,7 +562,7 @@ func (c *singleSourceZeroCheckClaims) roundPolynomial() polynomial.Polynomial { iIndex := 0 nextIIndex := nbUniqueInputs for d := range degree { - // Horner accumulation: gate_0 + α·(gate_1 + α·(... + α·gate_{W-1})) + // Horner accumulation: gate₀ + α·(gate₁ + α·(... + α·gate_{W-1})) for _, inputI := range c.inputIndices[nbWires-1] { evaluators[nbWires-1].PushInput(inputEvals[iIndex+inputI]) } @@ -604,7 +632,7 @@ func (c *singleSourceZeroCheckClaims) proveFinalEval(r []rational.Element) []rat // buf[2:4] = suffixEq[N-1] = eq(q_{N-1}; ·) (length 2) // buf[4:8] = suffixEq[N-2] = eq(q_{N-2}, q_{N-1}; ·) (length 4) // ... -// buf[2^(N-1):2^N] = suffixEq[1] = eq(q_1, ..., q_{N-1}; ·) (length 2^(N-1)) +// buf[2^(N-1):2^N] = suffixEq[1] = eq(q₁, ..., q_{N-1}; ·) (length 2^(N-1)) // // The first two positions are unused padding so that the buffer halves cleanly: // in round j the eq segment is buf[len(buf)/2:] and buf is trimmed to buf[:len(buf)/2]. @@ -627,7 +655,7 @@ func (r *resources) buildSuffixEq(q []rational.Element) polynomial.MultiLin { buf[2].Sub(&buf[2], &q[n-1]) buf[3].Set(&q[n-1]) - // Each suffixEq[j] is built by tensoring [1-q_j, q_j] with suffixEq[j+1]. + // Each suffixEq[j] is built by tensoring [1-qⱼ, qⱼ] with suffixEq[j+1]. // suffixEq[j+1] sits at buf[srcStart : srcStart+prevLen], // suffixEq[j] goes to buf[dstStart : dstStart+2*prevLen]. for j := n - 2; j >= 1; j-- { @@ -651,20 +679,27 @@ func (r *resources) buildSuffixEq(q []rational.Element) polynomial.MultiLin { func (r *resources) proveSingleSourceZeroCheckLevel(levelI int) sumcheckProof { level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) + foldingCoeff, claimedSum := r.foldClaims(levelI) var claims singleSourceZeroCheckClaims - claims.init(r, levelI) + claims.init(r, levelI, foldingCoeff) // Build suffix eq table from the single claim source's eval point src := level.ClaimSources[0] q := r.outgoingEvalPoints[src.Level][src.OutgoingClaimIndex] claims.suffixEq = r.buildSuffixEq(q) + claims.q = q - return sumcheckProve(&claims, r.transcript) + return sumcheckProve(&claims, claimedSum, r.transcript) } -func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) error { - claimedSum, lazyClaims := r.verifyLevelSetup(levelI, proof) +func (r *resources) verifySingleSourceZeroCheckLevel(levelI int) error { + foldingCoeff, claimedSum := r.foldClaims(levelI) + lazyClaims := &zeroCheckLazyClaims{ + foldingCoeff: foldingCoeff, + resources: r, + levelI: levelI, + } level := r.schedule[levelI].(*constraint.GkrSingleSourceZeroCheckLevel) src := level.ClaimSources[0] @@ -672,44 +707,39 @@ func (r *resources) verifySingleSourceZeroCheckLevel(levelI int, proof Proof) er degree := r.circuit.ZeroCheckDegree(level) challenges := make([]rational.Element, r.nbVars) - gPrime := make(polynomial.Polynomial, degree+1) - // The verifier tracks claimedSum = g'_{j-1}(r_{j-1}), the "primed" value with + // The verifier tracks claimedSum = g'ⱼ₋₁(rⱼ₋₁), the "primed" value with // the per-variable eq factors already absent. This is correct because the - // full round polynomial is g_j(X) = eq(q_j, X) · g'_j(X), where - // g'_j(X) = Σ_h suffixEq[j+1](h) · G(r₀…r_{j-1}, X, h), and + // full round polynomial is gⱼ(X) = eq(qⱼ, X) · g'ⱼ(X), where + // g'ⱼ(X) = Σₕ suffixEq[j+1](h) · G(r₀…rⱼ₋₁, X, h), and // - // g'_{j-1}(r_{j-1}) = Σ_{h_j ∈ {0,1}} eq(q_j, h_j) · g'_j(h_j) - // = (1-q_j)·g'_j(0) + q_j·g'_j(1) + // g'ⱼ₋₁(rⱼ₋₁) = Σ_{hⱼ ∈ {0,1}} eq(qⱼ, hⱼ) · g'ⱼ(hⱼ) + // = (1-qⱼ)·g'ⱼ(0) + qⱼ·g'ⱼ(1) // - // so the recovery formula g'_j(0) = (claimedSum - q_j·g'_j(1)) / (1-q_j) - // applies directly without dividing out accumulated prefix eq factors. - // After interpolating and evaluating g'_j(r_j), the update is simply - // claimedSum ← g'_j(r_j), carrying no eq baggage into the next round. + // With the coefficients cᵢ of g'ⱼ, g'ⱼ(0) = c₀ and g'ⱼ(1) = ∑ᵢ₌₀ cᵢ, so + // c₀ = claimedSum - qⱼ · ∑ᵢ₌₁ cᵢ, and g'ⱼ(rⱼ) = c₀ + rⱼ · ∑ᵢ₌₁ cᵢ · rⱼⁱ⁻¹. + // After evaluating g'ⱼ(rⱼ), the update is simply claimedSum ← g'ⱼ(rⱼ), + // carrying no eq baggage into the next round. for j := range r.nbVars { - partialPoly := proof[levelI].partialSumPolys[j] + partialPoly := r.proof[levelI].partialSumPolys[j] if len(partialPoly) != degree { return errors.New("malformed proof") } - var oneMinusQj, qjTimesGPrime1 rational.Element - oneMinusQj.SetOne() - oneMinusQj.Sub(&oneMinusQj, &q[j]) - qjTimesGPrime1.Mul(&q[j], &partialPoly[0]) // partialPoly[0] = g'(1) - gPrime[0].Sub(&claimedSum, &qjTimesGPrime1) - gPrime[0].Div(&gPrime[0], &oneMinusQj) - - copy(gPrime[1:], partialPoly) + c0 := (*rational.Vector)(&partialPoly).Sum() + c0.Mul(&c0, &q[j]) + c0.Sub(&claimedSum, &c0) challenges[j] = r.transcript.Squeeze(partialPoly...) - gPrimeCoeffs := polynomial.InterpolateOnRange(gPrime[:(degree + 1)]) - claimedSum = gPrimeCoeffs.Eval(&challenges[j]) + claimedSum = partialPoly.Eval(&challenges[j]) + claimedSum.Mul(&claimedSum, &challenges[j]) + claimedSum.Add(&claimedSum, &c0) } - // claimedSum is now Σ_w c^w · gate_w(inputs(r)), without the eq factor. - // verifyFinalEval expects Σ_w c^w · eq(q, r) · gate_w(inputs(r)), so multiply. + // claimedSum is now Σ_w cʷ · gate_w(inputs(r)), without the eq factor. + // verifyFinalEval expects Σ_w cʷ · eq(q, r) · gate_w(inputs(r)), so multiply. eqAtQR := polynomial.EvalEq(q, challenges) claimedSum.Mul(&claimedSum, &eqAtQR) - return lazyClaims.verifyFinalEval(challenges, claimedSum, proof[levelI].finalEvalProof) + return lazyClaims.verifyFinalEval(challenges, claimedSum, r.proof[levelI].finalEvalProof) } diff --git a/internal/gkr/rational/sumcheck_test.go b/internal/gkr/rational/sumcheck_test.go index 892913b36f..1422a0fee9 100644 --- a/internal/gkr/rational/sumcheck_test.go +++ b/internal/gkr/rational/sumcheck_test.go @@ -27,7 +27,7 @@ func testSumcheckSingleClaimMultilin(polyInt []uint64, hashGenerator func() fiel claim := singleMultilinClaim{g: poly.Clone()} t := gkrcore.NewNativeTranscript(hashGenerator()) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, poly.Sum(), t) var sb strings.Builder for _, p := range proof.partialSumPolys { diff --git a/internal/gkr/rational/sumcheck_test_vector_gen.go b/internal/gkr/rational/sumcheck_test_vector_gen.go index b8de5093d2..ad263d5cc4 100644 --- a/internal/gkr/rational/sumcheck_test_vector_gen.go +++ b/internal/gkr/rational/sumcheck_test_vector_gen.go @@ -37,9 +37,14 @@ func runMultilin(testCaseInfo *sumcheckTestCaseInfo) error { return err } + var claimedSum rational.Element + if _, err = claimedSum.SetInterface(testCaseInfo.ClaimedSum); err != nil { + return err + } + claim := singleMultilinClaim{poly} t := gkrcore.NewNativeTranscript(hsh) - proof := sumcheckProve(&claim, t) + proof := sumcheckProve(&claim, claimedSum, t) testCaseInfo.Proof = sumcheckToPrintableProof(proof) // Verification @@ -48,11 +53,6 @@ func runMultilin(testCaseInfo *sumcheckTestCaseInfo) error { } else { return _err } - var claimedSum rational.Element - if _, err = claimedSum.SetInterface(testCaseInfo.ClaimedSum); err != nil { - return err - } - if hsh, err = hashFromDescription(testCaseInfo.Hash); err != nil { return err } @@ -175,6 +175,12 @@ func (c *singleMultilinClaim) roundPolynomial() polynomial.Polynomial { return sumForX1One(c.g) } +func (c *singleMultilinClaim) evaluationAtZero(_ int, claim, atOne rational.Element) rational.Element { + var res rational.Element + res.Sub(&claim, &atOne) + return res +} + func (c *singleMultilinClaim) roundFold(r rational.Element) { c.g.Fold(r) } diff --git a/internal/gkr/sumcheck.go b/internal/gkr/sumcheck.go index b87c6fb9a5..adc36a8178 100644 --- a/internal/gkr/sumcheck.go +++ b/internal/gkr/sumcheck.go @@ -19,7 +19,7 @@ type sumcheckLazyClaims interface { // sumcheckProof of a multi-sumcheck statement. type sumcheckProof struct { - PartialSumPolys []polynomial.Polynomial + PartialSumPolys []polynomial.Polynomial // for each round j, the coefficients c₁, ..., c_d of gⱼ(X) = ∑ᵢ cᵢXⁱ; c₀ is derived by the verifier FinalEvalProof []frontend.Variable } @@ -51,20 +51,19 @@ func (t *transcript) Squeeze(elements ...frontend.Variable) frontend.Variable { func verifySumcheck(api frontend.API, claims sumcheckLazyClaims, proof sumcheckProof, claimedSum frontend.Variable, degree int, t *transcript) error { r := make([]frontend.Variable, claims.varsNum()) - gJ := make(polynomial.Polynomial, degree+1) gJR := claimedSum + // gⱼ(0) + gⱼ(1) = gⱼ₋₁(rⱼ₋₁) and gⱼ(1) = ∑ᵢ₌₀ cᵢ give c₀ = (gⱼ₋₁(rⱼ₋₁) - ∑ᵢ₌₁ cᵢ) / 2. for j := range claims.varsNum() { partialSumPoly := proof.PartialSumPolys[j] if len(partialSumPoly) != degree { return errors.New("malformed proof") } - copy(gJ[1:], partialSumPoly) - gJ[0] = api.Sub(gJR, partialSumPoly[0]) // Requirement that gⱼ(0) + gⱼ(1) = gⱼ₋₁(r) + c0 := api.Div(api.Sub(gJR, partialSumPoly.Eval(api, 1)), 2) r[j] = t.Squeeze(proof.PartialSumPolys[j]...) - gJR = polynomial.InterpolateLDE(api, r[j], gJ[:(degree+1)]) + gJR = api.Add(api.Mul(partialSumPoly.Eval(api, r[j]), r[j]), c0) } return claims.verifyFinalEval(api, r, gJR, proof.FinalEvalProof) diff --git a/internal/gkr/test_vectors/single_input_two_outs_two_instances.json b/internal/gkr/test_vectors/single_input_two_outs_two_instances.json index 705c1003e3..9abfebfa21 100644 --- a/internal/gkr/test_vectors/single_input_two_outs_two_instances.json +++ b/internal/gkr/test_vectors/single_input_two_outs_two_instances.json @@ -38,8 +38,8 @@ ], "partialSumPolys": [ [ - 4, - 9 + 2, + 1 ] ] }, diff --git a/internal/gkr/test_vectors/single_mimc_gate_four_instances.json b/internal/gkr/test_vectors/single_mimc_gate_four_instances.json index 8b76f5c5d7..867a6f4022 100644 --- a/internal/gkr/test_vectors/single_mimc_gate_four_instances.json +++ b/internal/gkr/test_vectors/single_mimc_gate_four_instances.json @@ -38,22 +38,22 @@ ], "partialSumPolys": [ [ - 32640, - 559871, - 4194304, - 20000001, - 71663744, - 210829195, - 536887296 + 6895, + 273, + 11795, + 8015, + 5565, + 1771, + 257 ], [ - 16384, - 2097152, - 35831808, - 268435456, - 1280000000, - 4586471424, - 13492928512 + 0, + 0, + 0, + 0, + 0, + 0, + 16384 ] ] }, diff --git a/internal/gkr/test_vectors/single_mimc_gate_two_instances.json b/internal/gkr/test_vectors/single_mimc_gate_two_instances.json index a916251982..5ec1128757 100644 --- a/internal/gkr/test_vectors/single_mimc_gate_two_instances.json +++ b/internal/gkr/test_vectors/single_mimc_gate_two_instances.json @@ -32,13 +32,13 @@ ], "partialSumPolys": [ [ - 2187, - 16384, - 78125, - 279936, - 823543, - 2097152, - 4782969 + 448, + 672, + 560, + 280, + 84, + 14, + 1 ] ] }, diff --git a/internal/gkr/test_vectors/single_mul_gate_two_instances.json b/internal/gkr/test_vectors/single_mul_gate_two_instances.json index 3762b8ccb7..8cec46df78 100644 --- a/internal/gkr/test_vectors/single_mul_gate_two_instances.json +++ b/internal/gkr/test_vectors/single_mul_gate_two_instances.json @@ -32,8 +32,8 @@ ], "partialSumPolys": [ [ - 9, - 8 + 2, + -1 ] ] }, diff --git a/internal/gkr/test_vectors/sumcheck/vectors.json b/internal/gkr/test_vectors/sumcheck/vectors.json index 64b8e3fb2d..551e5efbf7 100644 --- a/internal/gkr/test_vectors/sumcheck/vectors.json +++ b/internal/gkr/test_vectors/sumcheck/vectors.json @@ -13,7 +13,7 @@ "proof": { "partialSumPolys": [ [ - 3 + 2 ] ], "finalEvalProof": {} @@ -40,13 +40,13 @@ "proof": { "partialSumPolys": [ [ - 26 + 16 ], [ - -1 + 4 ], [ - -4 + 1 ] ], "finalEvalProof": {} diff --git a/internal/rational/vector.go b/internal/rational/vector.go index aa557aad5d..31df766921 100644 --- a/internal/rational/vector.go +++ b/internal/rational/vector.go @@ -7,3 +7,11 @@ func (v Vector) MustSetRandom() { v[i].MustSetRandom() } } + +// Sum returns the sum of the elements of v. +func (v *Vector) Sum() (res Element) { + for i := range *v { + res.Add(&res, &(*v)[i]) + } + return +}