Generate linear and quadratic constraints from padded sumcheck proof #39

tgeoghegan · 2025-10-22T19:02:35Z

We can't be certain that this works yet, because we don't yet have the Ligero prover set up which would produce a serialized proof we could compare against a test vector. Still, we can start code review. In parallel, I'm going to work on:

making sumcheck::Proof::new also emit the actual witness vector, so that we can extend the test on sumcheck::constraints::ProofConstraints to check that the constraints it generated are consistent with witness values
see if I can modify longfellow-zk to spit out a test vector of constraints (a vector of (c, j, k) triples for linear LHS, the b vector for linear RHS and a vector of (x, y, z) triples for the quad constraints) so we can test against that

I also suspect that in the near future, we'll want to move some modules or items out of the sumcheck module, because things like constraints and the witness layout will also be used by the Ligero prover and verifier. longfellow-zk has some of this stuff in a zk-common module, which could work for us.

src/sumcheck/mod.rs

tgeoghegan · 2025-10-22T19:23:12Z

src/sumcheck/constraints.rs

+        );
+
+        // Transcripts should have received the same sequence of writes.
+        assert!(proof_transcript.compare_state(&constraint_transcript));


This assertion is failing, so I must be missing a write to the transcript somewhere in the constraint generator. Or perhaps I'm wrong to expect the two transcripts to be in the same state.

Ah, I see why this assertion fails: on the sumcheck prover side, we write all inputs (public and private) to the transcript after doing the 3.1.3 transcript stuff. If I remove that write from Proof::new, then the transcript states sync up as expected.

So this means we have to resolve the inconsistency between sumcheck/prover.h and zk/zk_prover.h so that the proof test vector won't incorporate private inputs.

For now I refactored the sumcheck prover so we can toggle whether it runs in zk_test.cc compat mode, enabling both tests to pass.

tgeoghegan · 2025-10-22T19:34:26Z

src/sumcheck/constraints.rs

+        for (layer_index, (circuit_layer, proof_layer)) in
+            circuit.layers.iter().zip(proof.layers.iter()).enumerate()
+        {
+            // Choose alpha and beta for this layer


A bunch of this is exactly the same as in Proof::new, and could be factored out into something akin go longfellow-zk's begin_layer and end_layer methods. But then again it's nice to surface everything that's going on, and enable readers to compare it to the specification.

src/sumcheck/constraints.rs

src/sumcheck/bind.rs

src/sumcheck/mod.rs

src/sumcheck/constraints.rs

src/fields/mod.rs

src/sumcheck/bind.rs

jcjones

src/sumcheck/witness.rs

src/sumcheck/constraints.rs

src/sumcheck/witness.rs

src/sumcheck/constraints.rs

src/fields/fieldp256/mod.rs

src/sumcheck/constraints.rs

src/fields/mod.rs

src/sumcheck/constraints.rs

src/fields/mod.rs

src/fields/field2_128/mod.rs

src/sumcheck/witness.rs

src/sumcheck/constraints.rs

divergentdave · 2025-10-27T18:30:01Z

src/sumcheck/constraints.rs

+                    for term in &mut constraints.linear_constraint_lhs {
+                        if term.constraint_number == layer_index {
+                            term.constant_factor *=
+                                FE::lagrange_basis_polynomial_i(FE::ONE, challenge[0]);
+                        }
+                    }


I think mutating constraints after adding their constituent parts to the data structure makes this harder to follow and line up with the spec. What if we accumulated all the coefficients we need in a temporary data structure, and then only added the constraint after we had looped through all sumcheck rounds, so that we have computed all the known parts?

The per-layer constraint is claim = Q * VL * VR, where claim depends on all the polynomial evaluation pad values for this layer, plus the VL and VR pad values from the last layer, if applicable. Likewise, VL and VR depend on the VL and VR pad values from this layer, since they are the sum of the respective fields of the proof and pad. So, we could build up a representation of the symbolic claim expression as a dense list of 4*logw coefficients for polynomial evaluation pad values, plus 2 coefficients for VL/VR pad values, plus a constant term, to track the claim through the two nested loops. Then, we could combine that, along with a few more expressions for the VL and VR of the current layer, and add the whole layer constraint in one go. Note that we'd only need to compute and use the witness index values at the end as well, when adding to constraints. Does this sound like a useful refactoring?

src/sumcheck/constraints.rs

divergentdave · 2025-10-29T13:16:28Z

src/sumcheck/symbolic.rs

+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct SymbolicExpression<FieldElement> {
+    constraint_number: usize,
+    terms: Vec<SymbolicTerm<FieldElement>>,
+}


FYI, a potential footgun: the derived equality comparisons would say that two SymbolicExpression values are different, even if the mathematical expressions they represent are equal, if they distribute the constant term differently between the known fields of different SymbolicTerms. I assume we're only using the PartialEq implementation in tests, and they're passing, so this may not matter in practice. (Putting my optimization hat on, having only one FieldElement for the constant term in an expression would save memory)

Actually, we could say the same about how PartialEq is sensitive to the ordering of symbolic terms too.

Actually, I only derived PartialEq, Eq here out of reflex, because I generally find that I want all four of these traits on every struct I define. But nothing breaks if we remove PartialEq, Eq: the tests check the result of the lhs_terms() and known() methods. So I removed the derived traits to avoid the semantic ambiguity you pointed out.

Putting my optimization hat on, having only one FieldElement for the constant term in an expression would save memory

Good call. I was able to achieve this by refactoring a bit more. SymbolicExpression now sums known parts into a single field element, and represents the symbolic parts using a new Symbolic struct, private to the symbolic module, so there's no change to the users.

divergentdave · 2025-10-29T14:06:19Z

src/sumcheck/witness.rs

+///   - polynomials at each layer (2 * 2 * logw elements per circuit layer)
+///   - vl, vr and vl * vr for each layer of the circuit (three elements per circuit layer)


Clarification:

Suggested change

/// - polynomials at each layer (2 * 2 * logw elements per circuit layer)

/// - vl, vr and vl * vr for each layer of the circuit (three elements per circuit layer)

/// - one-time-pad for polynomials at each layer (2 * 2 * logw elements per circuit layer)

/// - one-time-pad for vl, vr and vl * vr for each layer of the circuit (three elements per circuit layer)

divergentdave · 2025-10-29T15:12:57Z

src/sumcheck/constraints.rs

+        final_claim += SymbolicTerm::from_known(
+            claims[0] + gamma * claims[1]
+                - public_inputs
+                    .iter()
+                    .zip(eq2.iter())
+                    .fold(FE::ZERO, |sum, (public_input_i, eq2_i)| {
+                        sum + *public_input_i * eq2_i
+                    }),
+        );
+
+        constraints
+            .linear_constraint_lhs
+            .extend(final_claim.lhs_terms());
+        constraints.linear_constraint_rhs.push(final_claim.known());


I think it could be misleading to put this field element in the final_claim known part, then put it in the constraint RHS. While the end result is correct, the semantics of final_claim just before we destructure it don't match up with what the protocol is actually doing. The SymbolicExpression represents some $ax+b$, and if we require the expression to equal zero, then the resulting constraint would be $ax=-b$. We could either flip the sign of the constant term we add up front, and then negate final_claim.known() before adding it to the RHS, or we could just track the RHS separately, giving it its own name.

Suggested change

final_claim += SymbolicTerm::from_known(

claims[0] + gamma * claims[1]

- public_inputs

.iter()

.zip(eq2.iter())

.fold(FE::ZERO, |sum, (public_input_i, eq2_i)| {

sum + *public_input_i * eq2_i

}),

);

constraints

.linear_constraint_lhs

.extend(final_claim.lhs_terms());

constraints.linear_constraint_rhs.push(final_claim.known());

let rhs = (

claims[0] + gamma * claims[1]

- public_inputs

.iter()

.zip(eq2.iter())

.fold(FE::ZERO, |sum, (public_input_i, eq2_i)| {

sum + *public_input_i * eq2_i

}),

);

constraints

.linear_constraint_lhs

.extend(final_claim.lhs_terms());

constraints.linear_constraint_rhs.push(rhs);

Yeah, this is because here we're computing the final claim:

SUM_{i} (eq2[i + npub] * sym_private_inputs[i]) - sym_layer_pad.vl - gamma * sym_layer_pad.vr = - SUM_{i} (eq2[i] * public_inputs[i]) + claims[0] + gamma * claims[1]

...and the spec has already done the work for us of rearranging everything into an LHS of purely symbolic parts and an RHS of purely known parts. I think it'd fit more neatly into the SymbolicExpression abstraction if it were expressed as

SUM_{i} (eq2[i + npub] * sym_private_inputs[i]) - SUM_{i} (eq2[i] * public_inputs[i]) + claims[0] - sym_layer_pad.vl + gamma * claims[1] - gamma * sym_layer_pad.vr = 0

...but then it'd be harder to line up our implementation with the specification, and I think that has a lot of value. It's possible that we could change the spec's descriptions of the per-layer and final constraints so that there's consistency across how they're specified and how we implement them. For now I'll go with your suggestion.

jcjones

The SymbolicExpression refactoring is great, well done. Feels way more maintainable, too.

The new outstanding issues look fine.

I think this is is good to go. Thanks for letting us tear into it so thoroughly, I'm pleased with the result!

Implements generation of linear and quadratic constraints from a padded sumcheck proof, specified in 6.6 [1] and 4.4 [2]. - `fields`: for efficient computation of Lagrange basis polynomials, we add trait `LagrangePolynomialFieldElement`, which defines methods for the basis polynomial denomimators and methods for evaluating basis polynomials 0, 1, and 2. - `sumcheck/witness`: computes the layout of the witness vector, needed for symbolic manipulation of quantities in constraints and eventually for construction of Ligero commitment and proof. - `sumcheck/symbolic`: allows computing symbolic expressions consisting of terms of the form `a + bx`, where `a` is a known quantity, `x` is some unknown element of the witness vector and `b` is a constant scale factor. - `sumcheck/bind`: implements the `bindeq` function of 6.2 [3]. - `sumcheck/mod`: sumcheck prover now emits the witness vector and Fiat-Shamir transcript so they may be used to validate constraints. - `sumcheck/constraints`: implements the constraint generation of 6.6. In order to valiate the correctness of all this, we also modify `longfellow-zk` to emit a Ligero commitment and constraints when running `zk_test.cc` [4]. More work on test vector generation from C++ is needed. [1]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-4.4 [2]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.6 [3]: https://datatracker.ietf.org/doc/html/draft-google-cfrg-libzk-01#section-6.2 [4]: https://github.com/tgeoghegan/longfellow-zk/tree/constraint-test-vector

tgeoghegan requested a review from a team as a code owner October 22, 2025 19:02

divergentdave reviewed Oct 22, 2025

View reviewed changes

src/sumcheck/mod.rs Outdated Show resolved Hide resolved

tgeoghegan commented Oct 22, 2025

View reviewed changes

src/sumcheck/constraints.rs Show resolved Hide resolved

divergentdave reviewed Oct 24, 2025

View reviewed changes

src/sumcheck/bind.rs Outdated Show resolved Hide resolved

src/sumcheck/mod.rs Outdated Show resolved Hide resolved

src/sumcheck/constraints.rs Outdated Show resolved Hide resolved

src/fields/mod.rs Outdated Show resolved Hide resolved

src/fields/mod.rs Show resolved Hide resolved

tgeoghegan commented Oct 25, 2025

View reviewed changes

src/fields/mod.rs Outdated Show resolved Hide resolved

This was referenced Oct 27, 2025

const evaluation of Lagrange basis polynomial denominators #40

Open

Iterative version of bindeq #41

Open

tgeoghegan commented Oct 27, 2025

View reviewed changes

src/sumcheck/bind.rs Outdated Show resolved Hide resolved

tgeoghegan force-pushed the timg/sumcheck-constraints branch from d6c6f7f to 6defa7e Compare October 27, 2025 14:33

tgeoghegan requested review from a team and divergentdave October 27, 2025 14:33

jcjones reviewed Oct 27, 2025

View reviewed changes

divergentdave reviewed Oct 27, 2025

View reviewed changes

tgeoghegan requested review from divergentdave and jcjones October 28, 2025 15:30

divergentdave approved these changes Oct 29, 2025

View reviewed changes

jcjones approved these changes Oct 29, 2025

View reviewed changes

tgeoghegan force-pushed the timg/sumcheck-constraints branch from f2c1da5 to 4be42ea Compare October 29, 2025 16:41

tgeoghegan force-pushed the timg/sumcheck-constraints branch from 4be42ea to 61bb982 Compare October 29, 2025 16:48

tgeoghegan merged commit 6530ff5 into main Oct 29, 2025
3 checks passed

tgeoghegan deleted the timg/sumcheck-constraints branch October 29, 2025 16:50

		/// - polynomials at each layer (2 * 2 * logw elements per circuit layer)
		/// - vl, vr and vl * vr for each layer of the circuit (three elements per circuit layer)

Generate linear and quadratic constraints from padded sumcheck proof #39

Generate linear and quadratic constraints from padded sumcheck proof #39

Uh oh!

Conversation

tgeoghegan commented Oct 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcjones left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcjones left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tgeoghegan commented Oct 22, 2025 •

edited

Loading