Skip to content

feat(ppsnark): Batch the Logup-GKR last layer with the Inner sumcheck batch - #502

Open
Sun-Jc wants to merge 5 commits into
microsoft:mainfrom
Sun-Jc:feat/ppsnark/gkr-inner-batched
Open

feat(ppsnark): Batch the Logup-GKR last layer with the Inner sumcheck batch#502
Sun-Jc wants to merge 5 commits into
microsoft:mainfrom
Sun-Jc:feat/ppsnark/gkr-inner-batched

Conversation

@Sun-Jc

@Sun-Jc Sun-Jc commented Jul 23, 2026

Copy link
Copy Markdown
Contributor

Dependency: Should merge after #501

Summary

The default GKR memory-check currently runs the Logup-GKR fractional-sum argument to its own evaluation point, then a seven-column rerandomize sumcheck carries the reconcile columns into the Inner batched sumcheck's point — two independent O(N) opening-point reductions of the same length. This PR fuses them: the GKR argument runs only to its input layer (the prefix), and its last layer shares the n-1 suffix rounds and the final MSB fold f with the Inner sumcheck's three relations (ABC / E / W), landing both on one shared point r_shared = f ∥ s. The seven-column rerandomize is deleted and a single PCS opening remains.

  • A fresh beta (sampled after the four initial claims C_G/C_A/C_E/C_W are bound) batches the GKR last layer with the three Inner relations.
  • n-1 shared suffix rounds send one fused cubic; the boundary uses h_sum = e_suffix − G_end, with G_end reconstructed by the verifier from the input splits (never absorbed), then a single fold f closes both protocols.
  • The verifier checks the Inner endpoint h(f) == inner_expected and the GKR input-layer reconcile + balance separately (no RLC merge); component-wise exact fraction equality with four root-denominator ≠ 0 guards; a forged GKR depth is rejected with Err. n = 1 keeps the exact component-wise root gate.

Two memory-check implementations remain mutually exclusive behind a cargo feature: default = fused Logup-GKR, logup-no-gkr = the original inverse-logup path. Both build and test.

What this is (and is not)

  • Proof size: a guaranteed −(3d+4) field-element win over the un-fused GKR path — drop the standalone inner-batched sumcheck (3d coefficients) plus the four rerandomize columns.
  • Prover time: the fused memory-check region measures ~105 ms faster than un-fused (region wall smem_region 1 127 → 1 022 ms). The gains are borrowing the memory-check columns instead of cloning six length-N ones, the Derive more traits. #7Add support for using bellperson to generate R1CS. #8 fusion itself, and getting ts_row/ts_col free from the GKR splits; part of that is given back by the fused path's serial inner-prep, which the un-fused path overlaps with its GKR. This is real but small: it is dwarfed by the shared MSM stages (commit L + PCS ≈ 8 s ≈ 85% of e2e), so end-to-end wall time is a wash inside MSM run-to-run noise. The durable wins are proof size + prover memory (one fewer resident/committed column set), now with a small measurable field-time gain.
  • Choosing GKR over inverse-logup at all is a size↔time trade: GKR removes ~3 s of inverse-oracle MSM from the prover, at the cost of a larger, O(d²), field-only (0 G) memory-check payload.

Benchmark 1 — prover time, canonical 11-stage breakdown (3-way)

num_cons = 2²⁰ (N_mem = 2²²), BN254 / HyperKZG, test-utils, DirectSNARK::prove on NonTrivialCircuit. 35 reps per config, PPS_STAGE probe; every cell is that config's own 35-rep median (ms) — not pooled. ① and ③ are on this branch (the logup-no-gkr feature and the default respectively); ② was measured in a feat/ppsnark/gkr worktree, instrumented inside mem_check_logup_gkr::prove_step and its monolithic GKR loop (split at j == 1) so every memory-check sub-stage is measured like-for-like against ③, not folded. Stages 0/1/2/9/10 are config-independent by construction (identical z+SpMV, outer sumcheck, commit L_row/L_col, extra evals, single-poly EE::prove open); their cross-config differences are pure MSM run-to-run noise (quantified in the third bullet). The memory-check region wall (smem_region, defined below the table) is the noise-free measure of the only real 3-way difference. Taxonomy from jcbase/bench/2026-07-23-ppsnark-breakdown.md.

# stage ① baseline (logup-no-gkr) ② un-fused GKR (feat/ppsnark/gkr) ③ fused (this PR) cost
0 prepare (z + SpMV) 112 117 110 field
1 outer sum-check 84 82 76 field
2 commit L 2 343 2 648 2 527 MSM (noise)
3 prepare mem-check (build + commit 4 inv oracles) 3 773 field + MSM
4a mem-check witness assembly (6 × length-N column clone) 52 0 (borrows) field (memcpy)
4b gkr prepare (build_input_layers) 123 107 field
4c inner-instance prep (val, masked_eq, slot build) (in #3 join) ‖ concurrent 77 field
5 gkr build tree 110 110 field
6 gkr first layers (j = d…2) 293 292 field
7 gkr last layer (j = 1) 257 445 (fused ⊕ inner) field
8 inner-sc-batch 378 225 0 (merged into #7) field
8b extra ts_row/ts_col re-open 15 0 (free from splits) field
mem-check region wall (smem_region) 4 216 1 127 1 022 field (②③)
9 evals 36 38 37 field
10 pcs open 5 506 5 681 5 964 MSM (noise)
e2e total 12 446 9 589 9 700

What smem_region is. It is the wall-clock of the whole memory-check + inner-sumcheck region of prove: from the moment the L_row/L_col commitments are absorbed (end of #2) to the start of the extra evals (#9). It therefore covers the c/gamma/r squeezes, the entire memory-check (#3 for ①; #4a–#7 for ②③), the batched inner sumcheck (#8), ②'s extra ts re-open (#8b), and the transcript glue between them. It is the honest apples-to-apples number because all three configs enter it with the same state and leave it having produced the same thing — r_inner_batched plus every evaluation the batch opening needs. It is measured as one span, so unlike the per-stage medians it needs no summing assumption.

Do not sum the sub-stage rows — compare at the region wall. The individual spans are disjoint and correctly measured (checked per-rep: in 35/35 reps the sub-stage sum is below the region wall, residual ≈ 47 ms, so there is no double counting), but a column sum is not comparable across ② and ③ for two reasons. (1) Concurrency asymmetry: ③ runs the inner-instance prep (#4c) serially for 77 ms, while ② runs the same O(N) work as build_inner inside a rayon::join with its GKR, so ②'s equivalent cost never appears as a serial span. (2) Unattributed region glue: ②'s spans leave ≈51 ms of the wall unmeasured (openings/proof-struct assembly, transcript, and freeing the extra 7-column rerandomize set), versus ≈−9 ms for ③. Summing the measured rows alone would put the gap at −121 ms; the honest, single-span measurement is −105 ms.

Reading the table

  • The mem-check wall is the whole 3-way story. ① pays Make traits public. #3 ≈ 3.77 s — building the four inverse oracles (batch_invert) and committing them (4 × length-N MSM, pure group work) — plus Add support for using bellperson to generate R1CS. #8 ≈ 0.38 s for the six-route inverse-logup sumcheck → wall ≈ 4.22 s. ②/③ commit nothing for the memory-check (Make traits public. #3 empty): every sub-stage is field arithmetic (0 G). So switching inverse-logup → GKR removes ~3 s of MSM and makes the prover field-bound there: wall 4.22 s → 1.13 / 1.02 s. This is the large, robust 3-way difference and the reason to prefer GKR.
  • Fusion measurably beats un-fused; the sub-stages show the direction, the wall gives the size. The result is ③'s region wall 1 022 ms vs ②'s 1 127 ms = −105 ms. Per-stage, ③ wins on: −52 ms borrowing its memory-check columns where ② clones six length-N ones (#4a — cross-checked two ways: ②'s clone span measures 52 ms, and re-cloning them inside ③ costs 52 ms); −37 ms net on the fusion proper (Derive more traits. #7 + Add support for using bellperson to generate R1CS. #8: ② 257 + 225 = 482 → ③ 445 + 0, i.e. the last layer grows +188 ms as it takes on the Inner ABC/E/W relations, but the standalone inner sumcheck's 225 ms disappears); −15 ms reading ts_row/ts_col free from the folded GKR splits instead of re-opening them (#8b); −16 ms on build_input_layers (#4b). Against those, ③ pays +77 ms for its serial inner-prep (#4c), which ② overlaps with its GKR. The shared GKR work matches to within a millisecond (Input checks #5 110 vs 110, Add InputOutputMismatch error. #6 293 vs 292) — a useful sanity check that the two independent instrumentations agree.
  • e2e's ③ > ② (9 700 vs 9 589 ms) is MSM measurement noise, not a memcheck regression. The only real prover difference is the memory-check region, where ③ is faster. The e2e ordering is set by the config-independent MSM stages Make Nova generic over the group #2 and Add a test case that uses the bellperson adapter to generate R1CS #10, whose jitter dwarfs the effect: opening the same batched polynomial at the same point 30 times back-to-back inside one run gives EE::prove = median 5 562 ms, min 4 941, max 6 423 — a 1 482 ms spread on identical work. The ③−② pcs median gap (283 ms) is 19 % of that pure single-poly jitter, and ②/③ swap places across passes (an earlier 35-rep pass put ②'s pcs at 5 479 and its commit L at 2 356, this one at 5 681 / 2 648 — the same config moving ~300 ms). smem_region strips that noise and ranks ③ fastest.
  • pcs (Add a test case that uses the bellperson adapter to generate R1CS #10) is identical across all three by constructionEE::prove opens one length-N RLC polynomial, independent of column count or memory-check; do not attribute any Add a test case that uses the bellperson adapter to generate R1CS #10 difference to fusion.

Benchmark 2 — proof size (3-way, theoretical + measured)

Engine Bn256EngineKZG + HyperKZG (BN254); G = compressed G1 = 32 B, F = BN254 scalar = 32 B. c = outer rounds = log₂(num_cons)+1; d = inner / memory-check rounds = log₂(num_cons)+2. "Proof" = the ppSNARK RelaxedR1CSSNARK object; actual = bincode (legacy) serialized length in bytes of a real prove output. Proof structure is byte-identical on this branch — the post-squash quality refactors are transcript-equivalent and touch no serialized type.

Measured total bytes

log₂ num_cons (c, d) ① baseline ② un-fused GKR ③ fused (this PR) ③ − ② ③ / ①
10 (11,12) 4 824 18 264 16 880 −1 384 (−7.6%) 3.5×
12 (13,14) 5 496 22 592 21 000 −1 592 (−7.0%) 3.8×
14 (15,16) 6 168 27 336 25 536 −1 800 (−6.6%) 4.1×
16 (17,18) 6 840 32 496 30 488 −2 008 (−6.2%) 4.5×
18 (19,20) 7 512 38 072 35 856 −2 216 (−5.8%) 4.8×

Theoretical composition (crypto elements, then closed-form bytes incl. bincode framing)

config crypto elements closed-form bytes matches measured?
① baseline total (d+8) G + (3c+6d+19) F memcheck flat 4 G + 4 F = 256 B yes
② un-fused GKR memcheck (1.5·d(d−1) + 16d + 15) F, 0 G 52 d² + 476 d + 496 yes (every row)
③ fused GKR memcheck (1.5·d(d−1) + 16d + 11) F, 0 G 52 d² + 476 d + 368 yes (every row)
③ fused total 52 d² + 708 d + 896 yes (every row)
Δ (③ − ②) −(3d + 4) F −(104 d + 136) (incl. framing) yes

Theory-vs-measured (fused total, closed form 52 d² + 708 d + 896):

log₂ num_cons (c, d) theoretical measured
10 (11,12) 16 880 16 880
14 (15,16) 25 536 25 536
18 (19,20) 35 856 35 856

Where the win comes from. The memory-check field itself shrinks by a flat 128 B (= 4 F) (drop the 7 rerandomize columns, net against the fused suffix's extra split/MSB data). The growing part of the win is the removed standalone sc_inner_batched (d cubic rounds = 3d F), so the total delta is −(3d+4) F — reproducing the hand-derived bound exactly. Fusing shaves ~6–8 % off the GKR proof but does not close the gap to the flat 4 G + 4 F inverse-logup baseline: the GKR memory-check is an O(d²), field-only payload that keeps config ③ 3.5×–4.8× larger than baseline, widening with size.


Soundness & tests

  • Two independent audits (manual protocol replay + crypto-security-reviewer) confirm no false-accept path: the fused MSB-fold boundary red-lines R1–R7 hold (G_end recomputed from splits, endpoint/reconcile checked separately, splits+h bound before f, component-wise exact equality + root-den ≠ 0, beta fresh after the four initial claims, h_sum = e_suffix − G_end, exact n=1 root gate). Net added soundness error vs the un-fused path is the fresh beta's 3/|F|.
  • New negative tests: forged-GKR-depth rejection (Err, not panic), reconcile_and_balance reject paths (mismatched column / unbalanced roots / zero root denominator), and a differential lock tying the fused last-layer gate algebra to the standalone GKR reconstruction.
  • Gates green: fmt / clippy -D warnings / doc --document-private-items; logup_gkr (28 tests) + fused module (8 tests); test_ivc_nontrivial_with_compression on both the default (fused) and logup-no-gkr features.

CI note

Both feature configs must build + test — the matrix needs --features logup-no-gkr (and --features "logup-no-gkr,test-utils") alongside the default (which covers fused Logup-GKR).

Sun-Jc added 5 commits July 14, 2026 13:33
Replace the ppSNARK inverse-logup memory-check with a Logup-GKR fractional-sum
argument, selectable by cargo feature.

- Default: Logup-GKR. A fractional-sum GKR argument (src/spartan/logup_gkr/)
  folds the four row/col x table/access sub-instances into per-instance trees,
  with Horner lambda-batching (distinct powers per num/den) and MSB-first fold.
- logup-no-gkr: the original inverse-logup memory-check (main's behaviour).
  The two paths are mutually exclusive and each compiles only its own code, so
  the GKR default drops the four inverse-oracle commitments and the six-route
  sumcheck.
- Host bridge (src/spartan/mem_check_logup_gkr.rs) reconciles the claimed
  fingerprint columns against the GKR-reduced input claims (component-wise
  equality), runs the row/col balance check with a nonzero-denominator guard,
  and carries the seven reconcile columns into the inner batched sumcheck via a
  RerandomizeSumcheckInstance landing at r_inner_batched.
- Verifier binds GKR depth to log N (rejects mismatched depth with NovaError
  instead of panicking) and uses exact fraction equality at the root gate and
  host reconcile to close the (0,0) projective-claim bypass.

test_ivc_nontrivial_with_compression passes on both feature paths.
clippy 1.97 adds `useless_borrows_in_formatting` and `manual_clear`:
- drop redundant `&` in write!/writeln! args (test_shape_cs pretty_print)
- use Vec::clear() instead of truncate(0) (num gadget)
Reuse preceding-layer left final claims as the first sumcheck round's t(0), so the cached-delta pass only evaluates t(inf). The verifier and proof format are unchanged.

At 20 variables, paired GKR prove benchmarks reduce median time by about 15 ms (~8%).
Build the outer sum-check third input uCz_E = u*Cz + E with a parallel
iterator instead of a serial one. The map is memory-parallel and was
needlessly serial: it shows a 4.2x-8.9x speedup on the construction itself
(1.06ms -> 0.26ms at 2^16, 15.6ms -> 1.75ms at 2^20). The outer sum-check
and all downstream logic are unchanged, so this is a zero-risk net win.
End-to-end prover impact is ~0.1% (below the benchmark noise floor).
Replace the default GKR memory-check's independent opening-point reduction
(the Logup-GKR argument to its own point, then a seven-column rerandomize
sumcheck carrying the reconcile columns into the Inner sumcheck) with a
single fused reduction: the GKR argument runs only to its input layer (the
prefix), and its last layer shares the n-1 suffix rounds and the final MSB
fold f with the Inner sumcheck's three relations, landing both on one
shared point r_shared = f || s. This drops the seven-column rerandomize
entirely and keeps a single PCS opening.

Protocol:
- Stage the Logup-GKR argument into prefix + last layer (shared per-round
  reduction body; standalone byte-equal to the prior monolithic loop).
- A fresh beta (sampled after the four initial claims C_G/C_A/C_E/C_W are
  bound) batches the GKR last layer with the ABC / E / W Inner relations.
  n-1 shared suffix rounds send one fused cubic; the boundary uses
  h_sum = e_suffix - G_end (G_end reconstructed by the verifier from the
  input splits, never absorbed), then one shared fold f closes both.
- Verifier checks the Inner endpoint h(f) == inner_expected and the GKR
  input-layer reconcile + balance separately (no RLC merge); component-wise
  exact fraction equality with four root-den != 0 guards; a forged GKR
  depth is rejected with Err.
- n = 1 keeps the exact component-wise root-gate check.

Proof size: -(3d+4) field elements vs the un-fused GKR path (drop the
standalone inner-batched sumcheck's 3d coefficients + the 4 rerandomize
columns). Prover time is neutral (memory-check is field-bound and dwarfed
by the shared MSM stages); the fusion's win is proof size + memory.

The fused driver borrows its memory-check columns: MemCheckWitness holds
slices (build_input_layers only reads them to derive the fraction layers),
so assembling it costs no per-column clone of the padded row/col columns.

Two memory-check implementations remain mutually exclusive behind a cargo
feature: default = fused Logup-GKR; logup-no-gkr = the original
inverse-logup path. Both build and test.
@Sun-Jc
Sun-Jc force-pushed the feat/ppsnark/gkr-inner-batched branch from 274b1e5 to c2a1c02 Compare July 26, 2026 07:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant