docs(sumcheck): annotate main-sumcheck formulas and Layer output-eval group construction

[Copilot]

This update addresses reviewer feedback to explicitly document the concrete expression proved in the main sumcheck phase. The code now spells out the selector-group RLC form at the exact construction/proving sites (CPU/GPU + layer assembly), states the mathematical form of the smaller sumchecks batched by main sumcheck (including zero-target zerochecks), and adds formula-level documentation in Layer::from_circuit_builder for how output evaluation groups are assembled.

• Main-sumcheck expression clarity

  • Added precise inline comments describing the polynomial shape:
    • per-group term construction in zerocheck_layer
    • main-sumcheck entry points in CPU and GPU provers
  • Files updated:
    • gkr_iop/src/gkr/layer/zerocheck_layer.rs
    • gkr_iop/src/gkr/layer/cpu/mod.rs
    • gkr_iop/src/gkr/layer/gpu/mod.rs

• Concrete formulas now documented in-place

  • Main batched polynomial:

p(x) = Σ_g p_g(x)

• Per-group (smaller) sumcheck polynomial:

p_g(x) = sel_g(x) * Σ_j (α_{2+offset(g,j)} * expr_{g,j}(x))

• Per-group and batched sumcheck targets:

S_g = Σ_{x in {0,1}^n} p_g(x)
Σ_{x in {0,1}^n} p(x) = Σ_g S_g

• Zerocheck expectation (chip-derived constraints):

S_g = 0
Σ_{x in {0,1}^n} p(x) = Σ_g S_g = 0

• Layer output-eval group construction (new)

  • Added comments in Layer::from_circuit_builder describing how groups are formed for:
    • read (r_selector)
    • write (w_selector)
    • lookup (lk_selector, including padding-normalized non-negated/negated forms)
    • rotation (left/right/target groups)
    • ECC bridge (x/y/slope/x3/y3 groups)
    • zero constraints (zero_selector)
  • Added a batched formula linking these groups to the main sumcheck term construction and clarified how offset(g,i) is assigned from flattened expr_evals order.
  • File updated:
    • gkr_iop/src/gkr/layer.rs

• Expression assembly note

  • In zerocheck_layer, comments clarify that:
    • rlc_zero_expr builds per-group p_g(x) terms
    • the final p(x) is the sum over all groups

[kunxian-xia]

@copilot since main sumcheck phase is used to batch a few smaller sumchecks together, please write down the mathematical expressions of these smaller sumchecks.

[kunxian-xia]

@copilot For example, the batched main sumcheck has zerochecks (derived from each chip's constraints) in which the expected sum is 0.

[Copilot]

@copilot since main sumcheck phase is used to batch a few smaller sumchecks together, please write down the mathematical expressions of these smaller sumchecks.

Done in commit 8bfca68.

I updated the main-sumcheck comments to explicitly define the smaller batched sumchecks:

• per-group polynomial p_g(x) = sel_g(x) * Σ_j (α_{2+offset(g,j)} * expr_{g,j}(x))
• per-group target S_g = Σ_{x in {0,1}^n} p_g(x)
• batched relation p(x)=Σ_g p_g(x) and Σ_x p(x)=Σ_g S_g

Updated locations:

• gkr_iop/src/gkr/layer/zerocheck_layer.rs
• gkr_iop/src/gkr/layer/cpu/mod.rs
• gkr_iop/src/gkr/layer/gpu/mod.rs

[kunxian-xia]

@copilot please add code comments to “Layer::from_circuit_builder” to explain  on how the output evaluation group was constructed, e.g. read/write/lk/ecc/rotation/ecc. Cite with clear mathematics formula is preferable.

[Copilot]

@copilot For example, the batched main sumcheck has zerochecks (derived from each chip's constraints) in which the expected sum is 0.

Addressed in commit 6d17c19.

I updated the comments to explicitly state that for chip-derived zerochecks each batched subgroup has expected sum 0:
S_g = Σ_{x in {0,1}^n} p_g(x) = 0, so the batched target is Σ_x p(x) = Σ_g S_g = 0.

[Copilot]

@copilot please add code comments to “Layer::from_circuit_builder” to explain  on how the output evaluation group was constructed, e.g. read/write/lk/ecc/rotation/ecc. Cite with clear mathematics...

Implemented in commits 75082dd and 9e005d5.

I added math-focused comments in Layer::from_circuit_builder explaining how output evaluation groups are constructed for read/write/lookup/rotation/ecc/zero constraints and how they are batched into the main sumcheck polynomial, including how offset(g,i) is assigned from flattened group order.