Skip to content

feat(stark): opt-in LogUp-GKR mode — batch GKR replaces committed LogUp columns (port of #485)#857

Draft
MauroToscano wants to merge 20 commits into
mainfrom
feat/logup-gkr-v3
Draft

feat(stark): opt-in LogUp-GKR mode — batch GKR replaces committed LogUp columns (port of #485)#857
MauroToscano wants to merge 20 commits into
mainfrom
feat/logup-gkr-v3

Conversation

@MauroToscano

@MauroToscano MauroToscano commented Jul 21, 2026

Copy link
Copy Markdown
Contributor

Reimplementation of the LogUp-GKR experiment (#485) on the current prover, as an opt-in mode (LogUpMode::Gkr, default Standard).

#485 could not be rebased: its 22 commits target a prover from before the single-source constraint migration (#764/#772), forward accumulation (#823), the rkyv in-place verifier (#769), and the GPU residency stack (#748/#798/#799) — every wiring file conflicts against rewritten code. This PR ports the three self-contained protocol modules from the branch tip verbatim (they carry all of #485's soundness-fix commits and the SVO sumcheck optimizations) and re-implements the integration from scratch against today's architecture. Analysis and the execution plan live in thoughts/logup-gkr/.

What GKR mode does

Standard LogUp commits ⌈K/2⌉ batched term columns + 1 accumulated column per table. GKR mode replaces them with 2 aux columns regardless of interaction count:

  • a batch GKR over per-table fraction-summation trees proves every table's total LogUp contribution on the shared transcript (before forking); the bus balance is checked on the transcript-bound root claims (external targets like the COMMIT bus work unchanged);
  • a Lagrange kernel column l = eq(·, r) at the GKR random point and a bridge running-sum column σ with one degree-2 circular constraint (σ_next − σ_curr − l·batched + Δ) tie the GKR column claims back to the committed trace (Schwartz–Zippel over γ, plus a γ^K·l² kernel self-check);
  • σ is the sole next-row OOD read, so the pruned 1-column g·z block from refactor(logup): forward accumulation so acc is the sole next-row OOD read #823 carries over.

On #485 this measured peak heap −70 % (221 GB → 66 GB) at +2.6 % prove time (fib 8M) — the aux LDE/Merkle/OOD/opening footprint for bus-heavy tables (CPU: 21 aux cols → 2) collapses, and the GKR trees are transient, freed before the LDE phases.

Design decisions

  • Opt-in and wire-preserving. With GKR off nothing changes: same transcript, same MultiProof/VmProof rkyv layout (GKR proofs use separate wrapper types GkrMultiProof/GkrVmProof), so cross-version verification of standard mode stays meaningful. Mode mismatches fail closed in both directions, on both prover and verifier.
  • The bridge constraint is single-source. One emit body (emit_logup_gkr_constraints) serves the prover folder, the verifier/recursion folder, IR capture, and derived metadata, like every other constraint post-feat(stark): single-source constraints — one definition per constraint, verified cross-version [stacked on #763] #764. γ powers and Δ are read as challenge leaves from an extended per-table rap-challenges layout — no new context plumbing.
  • All GKR randomness is transcript-derived. The verifier ignores everything proof-carried except the batch proof and column claims; random points and instance claims come from gkr_verify_batch's replay (preserving Feat/gkr logup #485's fix for its review finding Initial vm implementation #1).
  • Guest-friendly verify paths. No hash maps anywhere on verify-reachable code (sorted-slice lookups); untrusted-proof shape guards reject malformed round polynomials / layer lists as errors, never panics (closes Feat/gkr logup #485's residual DoS vector).
  • GPU paths are gated to standard mode (device_only_for, resident aux build, fused composition): GKR v1 runs the CPU composition/aux paths, matching the conditions of Feat/gkr logup #485's original bench. GPU support for GKR mode is follow-up work.

⚠️ Known soundness gap (inherited from #485, documented, NOT fixed here)

reconstruct_and_verify_gkr_claims is fail-open for multi-interaction tables (every production table): nothing binds the batch-GKR leaf claims (n̂, d̂) to the committed columns, because the leaf fraction is a nonlinear (cross-multiplied) function of the columns and MLE does not commute with products. A malicious prover can run an honest GKR over fabricated leaves and fake the bus balance. The Codex review of #485 flagged this (finding #2) and the branch never closed it.

It is deliberately not fixed in this PR — the fix is a protocol change to the GKR input layer (a linear input layer or an input-layer sumcheck, à la Winterfell/Stwo LogUp-GKR), and mixing it into the port would have destroyed the only correctness reference. An #[ignore]d test (reconstruct_multi_interaction_rejects_fabricated_leaf_claims) asserts the desired fail-closed behavior and becomes the acceptance test for the follow-up. GKR mode must not be treated as production-sound until that lands. Full analysis: thoughts/logup-gkr/port-plan.md §6.

Test coverage

  • Ported module tests (61: GKR prove/verify roundtrips incl. SVO paths, sumcheck, Lagrange kernel).
  • Bridge constraint folder==IR parity (prover + verifier, 1000 random frames × 2 layouts) — the GPU-contract gate every constraint gets.
  • Cross-mode oracle: the GKR tree root equals the standard-mode table contribution L computed by the standard aux path.
  • 12 e2e GKR tests at the stark layer: multi-table + single-table roundtrips (mixed instance sizes), rkyv wrapper roundtrip, tampered root claim / column claim / child claims / σ-OOD / kernel-OOD / smuggled bus inputs / wrong balance all rejected, mode mismatches fail closed.
  • Wire-format tests: rkyv + cbor roundtrips; malformed round polynomials and truncated layer lists rejected as errors.
  • VM-level e2e: the full table set (incl. preprocessed DECODE/PAGE/REGISTER, 1-row tables) proves+verifies in GKR mode; library-path e2e on a committing program exercises the nonzero verifier-computed COMMIT bus target and rejects tampered public output.
  • Standard mode: full stark (288) + prover suites green; make lint clean in all four feature configs.

Remaining before un-draft

  • Cross-version verification of standard mode against an origin/main binary (examples + VM programs) — expected to pass byte-for-byte; standard-mode paths are transcriptions.
  • Memory/time bench: comment /bench on this PR — the CLI's prove defaults to GKR mode on this branch (--logup-mode standard for the production path), so the standard PR-vs-main bench IS the GKR-vs-standard A/B on the same workload. Early local data point: proof bundle 20.8 MB (GKR) vs 33.7 MB (standard) on a small commit program (−38 %).
  • Decision on the leaf-binding fix (input-layer sumcheck vs per-interaction linear leaves) — required before any production use.
  • Continuation support: the full continuation pipeline (epoch proofs, the cross-epoch global-memory proof, host + archived verify, the recursion guest, CLI --continuations) is mode-parametrized — prove_continuation_gkr/verify_continuation_gkr, GkrContinuationProof (standard bundle + KB-scale per-proof GKR artifacts; standard wire format untouched), recursion-gkr-cont-{min,blowup2}.elf guests, RECURSION_DUMP_GKR=1 dump mode. Multi-epoch host roundtrip (prove → verify owned+archived → attest → consumer program_id check) green.
  • Recursion-guest support: verify_gkr_recursion_blob reads the archive in place (only the KB-scale GKR artifacts are deserialized), recursion-gkr-{min,blowup2}.elf guests + RECURSION_DUMP_GKR=1 dump mode, same program_id attestation as the standard path. Measured (blowup2/219q, identical ethrex-5tx inner): 5.060B guest cycles vs 5.234B standard = −3.3 % cycles (−3.7 % keccak), blob 102 MB vs 116 MB = −12 % — the smaller openings outweigh the added sumcheck replay.
  • GPU support for GKR mode (aux build, bridge in the fused composition kernel, GKR sumcheck kernels).

…t/gkr-logup

Verbatim from the branch tip (78be304), which includes the batch GKR
protocol with SVO sumcheck, all soundness-fix commits, and in-module
tests (61 passing). Not yet wired into the prover/verifier.
…bridge constraint

Opt-in per-AIR mode (default Standard, wire-identical). GKR mode:
- aux trace = 2 columns (Lagrange kernel l, bridge running sum sigma)
  regardless of interaction count
- one degree-2 bridge constraint sigma_next - sigma_curr - l*batched + delta,
  emitted through the generic ConstraintBuilder (all four interpretations:
  prover/verifier folders, IR capture, derived meta) with gamma powers and
  delta read as challenge leaves from the extended rap_challenges layout
- boundary constraints l[0] = prod(1 - r_j) and sigma[0] = 0
- sigma is the sole next-row OOD read (preserves g*z pruning)
- logup_gkr module: leaf fractions, layer trees, column-claim finalize,
  bridge params, aux-column build, and verifier-side claim reconstruction
  (sorted-slice lookups, no hashing on verify paths; the multi-interaction
  leaf-binding gap is documented fail-open pending the input-layer fix)
- AIR trait: bus_interactions() and logup_mode() accessors

Gates: bridge folder==IR parity (prover+verifier, 1000 random frames),
GKR tree root == standard-mode table contribution (cross-mode oracle),
aux-column recurrence/boundary tests; 275 stark tests green.
…pper

- rkyv Archive/Serialize/Deserialize on RoundPoly, SumcheckProof,
  BatchGkrLayerProof, BatchGkrProof (rkyv is the authoritative format)
- GkrMultiProof = MultiProof + batch GKR proof + per-table column claims,
  a SEPARATE top-level type so standard-mode proofs stay byte-identical
  (cross-version verification remains meaningful with GKR off)
- untrusted-proof shape guards in gkr_verify_batch: round polynomials must
  have exactly 4 evals (deserialization bypasses RoundPoly::new's assert),
  max_layers bounded before the 2^n_unused shift
- tests: rkyv + cbor roundtrip verifies; malformed round poly and truncated
  layer list rejected as errors, not panics
Prover (multi_prove_gkr -> GkrMultiProof): after the shared z/alpha
sampling, a new Phase B'/B'' on the SHARED transcript — parallel leaf
fractions + summation trees per interacting table, one gkr_prove_batch,
parallel per-table column-claim finalize, claims absorbed then gamma
sampled, per-table challenge vectors extended with the bridge params.
Aux build receives the extended vector (kernel + sigma columns); layer
trees are freed before the LDE phases (the memory win). The fork-time L
absorb vanishes with bus_public_inputs. Standard mode is untouched:
multi_prove fails closed on GKR-mode AIRs and vice versa.

Verifier (multi_verify_gkr): mirrors the phase order exactly — batch GKR
replay (random point and instance claims derived from the transcript,
never the proof), exact column-claim index-set check + reconstruction,
claims absorbed then gamma sampled, per-table extended challenges into
the unchanged rounds 2-4, and the bus balance checked on the batch
proof's root claims (zero denominators rejected). GKR proofs must not
carry bus_public_inputs (fail-closed).

GPU paths are explicitly gated to standard mode (device_only_for and the
fused composition): GKR v1 runs the CPU composition/aux paths.

Tests: 12 e2e GKR-mode tests — multi-table and single-table roundtrips
(mixed instance sizes), rkyv wrapper roundtrip, tampered root claim /
column claim / child claims / sigma OOD / kernel OOD rejected, smuggled
bus_public_inputs rejected, mode mismatches fail closed both ways, wrong
expected balance rejected. Plus an #[ignore]d test documenting the known
multi-interaction leaf-binding gap (port-plan §6).
…ntry points

- VmAirs::new_with_logup_mode: every table constructor takes the mode
  (new delegates with Standard; no env magic, prover and verifier must
  construct with the same mode)
- prove_gkr_with_options_and_inputs -> GkrVmProof (GkrMultiProof + the
  usual verifier metadata; the standard VmProof wire format is untouched)
- verify_gkr_with_options: same statement absorption and verifier-computed
  COMMIT bus target as the standard path, checked against the GKR root
  claims via multi_verify_gkr
- fix single-row tables (n_vars = 0): the extended challenge vector ends
  exactly at the empty random point; kernel boundary is l[0] = 1

Tests: full VM table set (CPU..PAGE/REGISTER/DECODE incl. preprocessed,
1-row tables) proves+verifies in GKR mode (sub_neg_result minimal);
library-path e2e on a committing program exercises the NONZERO COMMIT
bus target and rejects tampered public output.
@MauroToscano

Copy link
Copy Markdown
Contributor Author

/bench-prove

@github-actions

github-actions Bot commented Jul 21, 2026

Copy link
Copy Markdown

Benchmark — ethrex 20 transfers (median of 3)

Table parallelism: auto (cores / 3)

Metric main PR Δ
Peak heap 73028 MB 53945 MB -19083 MB (-26.1%) 🟢
Prove time 37.771s 33.095s -4.676s (-12.4%) 🟢

🎉 Improvement detected — heap or time decreased by more than 5%.

✅ Low variance (time: 0.6%, heap: 0.6%)

Commit: d4ceb2e · Baseline: cached · Runner: self-hosted bench

A plain `cli prove` — exactly what the /bench workflow runs — now proves
with the batch-GKR LogUp path, so the PR-vs-main bench comparison is the
GKR-vs-standard A/B on the same workload. `--logup-mode standard` keeps
the production path reachable; `verify` takes the matching flag (the two
modes have different proof bundle types). Timing still covers proof
generation only, identically in both modes.

Smoke-tested both modes end-to-end (prove + verify) on test_commit_4;
GKR proof bundle is 20.8 MB vs 33.7 MB standard on that program.
@MauroToscano

Copy link
Copy Markdown
Contributor Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The recursion-guest cycle comparison adds guest builds on top of the verifier bench, longer on a cold runner. The bench server is occupied until it finishes.

@MauroToscano

Copy link
Copy Markdown
Contributor Author

/bench-prove

@github-actions

Copy link
Copy Markdown

Verifier benchmark — ebbba689e2 vs main (20 pairs)

=== Verify ABBA result ===

Metric main PR Δ
Verify time (per-side) 3.483s 3.637s +4.43% 🔴
Proof size 204.30 MiB 188.07 MiB -7.94% 🟢

Per-side (PR can't deserialize the baseline's proof — proof-format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.

  pairs: 20   mean A (PR): 3.637s   mean B (main): 3.483s
  [parametric] paired-t   mean +4.43%   sd 0.72%   se 0.16%
               95% CI: [+4.10%, +4.77%]   (t df=19 = 2.093)
  [robust]     median +4.53%   Wilcoxon W+=210 W-=0  p(exact)=1.9e-06  (z=+3.90)

  run-to-run jitter:    A CV 0.40%   B CV 0.44%        (lower = steadier)
  within-session drift: +0.32% over the run, 1st->2nd half +0.18%

🔴 REAL REGRESSION — PR verifies ~4.43% slower (paired-t and Wilcoxon agree).

Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.


Recursion guest cycles (main vs PR)

=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main 528a841 guest=recursion-min.elf
REF_A (PR) ebbba68 ebbba68 guest=recursion-min.elf

Metric REF_B (baseline) REF_A (PR) Δ (A-B)
Guest cycles 41.7M 42.1M +0.4M (+0.88%)
Keccak calls 3025 3025 0

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)
ref_b_sha=528a8411bb641a1290c0794cdd79c76eba76c739 ref_b_elf=recursion-min.elf ref_b_cycles=41749851 ref_b_keccak=3025 ref_b_execute_wall_s=2
ref_a_sha=ebbba689e2db06b64793b185d4e6f6239fffeaad ref_a_elf=recursion-min.elf ref_a_cycles=42117336 ref_a_keccak=3025 ref_a_execute_wall_s=2
delta_cycles=367485 delta_keccak=0

(blowup2 regime unavailable for these refs — see the workflow log.)

=== Recursion-guest cycle comparison — 128-bit (blowup=4, 110 queries — realistic base-layer) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main 528a841 guest=recursion-blowup4.elf
REF_A (PR) ebbba68 ebbba68 guest=recursion-blowup4.elf

Metric REF_B (baseline) REF_A (PR) Δ (A-B)
Guest cycles 364.5M 365.7M +1.2M (+0.32%)
Keccak calls 189337 189337 0

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)
ref_b_sha=528a8411bb641a1290c0794cdd79c76eba76c739 ref_b_elf=recursion-blowup4.elf ref_b_cycles=364530729 ref_b_keccak=189337 ref_b_execute_wall_s=5
ref_a_sha=ebbba689e2db06b64793b185d4e6f6239fffeaad ref_a_elf=recursion-blowup4.elf ref_a_cycles=365693700 ref_a_keccak=189337 ref_a_execute_wall_s=6
delta_cycles=1162971 delta_keccak=0

=== Recursion-guest cycle comparison — 128-bit (blowup=4, 110 queries) — real ethrex block, 4 transfers — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main 528a841 guest=recursion-cont-blowup4.elf
REF_A (PR) ebbba68 ebbba68 guest=recursion-cont-blowup4.elf

Metric REF_B (baseline) REF_A (PR) Δ (A-B)
Guest cycles 1470.1M 1521.5M +51.4M (+3.50%)
Keccak calls 1755694 1780570 +24876

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)
ref_b_sha=528a8411bb641a1290c0794cdd79c76eba76c739 ref_b_elf=recursion-cont-blowup4.elf ref_b_cycles=1470095496 ref_b_keccak=1755694 ref_b_execute_wall_s=22
ref_a_sha=ebbba689e2db06b64793b185d4e6f6239fffeaad ref_a_elf=recursion-cont-blowup4.elf ref_a_cycles=1521506092 ref_a_keccak=1780570 ref_a_execute_wall_s=24
delta_cycles=51410596 delta_keccak=24876

The +28.5% prove-time regression on the ethrex-20tx bench was dominated
by serial work in the GKR phase (which runs between multi_prove's
parallel phases and inherits none of their table parallelism):

- batch sumcheck round loop: per-instance round evals now run in
  parallel across instances, the per-round gate/eq sums use parallel
  reductions above 2^10 pairs, and the post-challenge claim/fold updates
  run in parallel across instances (field ops are exact, so any
  reduction order is value-identical; the transcript sequence is
  untouched). Previously only fold_table was parallel.
- PerInstanceTables leaf-layer even/odd splits parallelized.
- compute_lagrange_kernel: doubling algorithm (1 mul + 1 sub per output
  pair, O(N)) replacing the per-bit full-table passes (O(n*N) ext mults,
  ~20x the necessary work at production sizes); values are identical
  (regression test vs the per-bit product definition).
- the GKR path no longer materializes column-major clones of the main
  segment (previously 3x per table): leaf fractions, the column-claim
  inner products (now ONE row-major pass computing all K claims with
  per-chunk partial sums), and the aux batched column all read borrowed
  row-major rows in place via a new BusValue::accumulate_fingerprint_row.
- hoisted the per-instance-per-round inversion of 2; instruments spans
  for the GKR phases (r1_gkr_trees / r1_gkr_batch_prove / r1_gkr_finalize).

Local ethrex-5tx phase timings (10-core M-series): trees 3.13s -> 2.12s,
batch prove 4.63s -> 2.26s, finalize 1.39s -> 0.25s, GKR aux build
1.90s -> 0.38s. The wins should be larger on the many-core bench box,
where the serial batch phase was the Amdahl bottleneck.
@MauroToscano

Copy link
Copy Markdown
Contributor Author

/bench

1 similar comment
@MauroToscano

Copy link
Copy Markdown
Contributor Author

/bench

The recursion pipeline could not consume GkrVmProof at all (host-side,
owned-deserialize only). Now:

- Verifier::multi_verify_gkr_views: the GKR verify entry over proof
  VIEWS — per-table STARK proofs owned or rkyv-archived (read in place,
  #769-style), batch GKR proof + column claims borrowed.
- verify_gkr_proof_parts: single GKR VM-proof verification impl (the
  analogue of verify_proof_parts), taking supplied DECODE/page roots;
  verify_gkr_with_options funnels into it.
- GkrGuestInput + recursion::encode_gkr_guest_input: the guest blob on
  the same magic-prefixed wire format; verify_gkr_recursion_blob reads
  the archive in place and materializes only small metadata plus the
  KB-scale GKR artifacts (batch proof, column claims) — the MB-scale
  per-table data stays zero-copy.
- recursion::verify_and_attest_gkr_blob: attests the SAME
  program_id(elf, roots) || public_output as the standard path (LogUp
  mode changes bus-sum proving, not program identity), so
  check_attestation needs no GKR variant.
- guest: 'gkr' feature (mutually exclusive with 'continuation') +
  recursion-gkr-{min,blowup2}-bench bins; Makefile builds
  recursion-gkr-{min,blowup2}.elf.
- dump mode: RECURSION_DUMP_GKR=1 on test_dump_recursion_input proves
  the inner in GKR mode and encodes the GkrGuestInput blob.
- host roundtrip test mirrors the guest path end-to-end and pins the
  cross-format rejects (standard blob vs GKR verifier and vice versa).
Every multi_prove/multi_verify site in the continuation path is now
mode-parametrized: epoch proofs (VM tables + the epoch-local L2G
bookend), the cross-epoch global-memory proof (per-epoch L2G airs + one
GLOBAL_MEMORY air per touched page), and their verifiers all thread a
LogUpMode through the AIR builders (with_logup_mode) and dispatch to the
standard or GKR prove/verify entry points.

- GkrContinuationProof = the standard ContinuationProof (unchanged wire
  format) + per-epoch and global GkrProofExtras (batch proof + column
  claims, KB-scale). Containing the standard bundle as `base` keeps
  every view, L2G binding check, and root precompute working unchanged.
- prove_continuation_gkr / verify_continuation_gkr (host, owned) and
  verify_gkr_continuation_archived (guest: per-table proofs read in
  place off the archived base bundle, only the GKR extras deserialized).
- recursion: GkrContinuationGuestInput + encode_gkr_continuation_guest_input
  + verify_gkr_continuation_and_attest -- same program_id attestation as
  the standard continuation path (consumer flow unchanged).
- guest: the gkr and continuation features now compose (fourth input
  layout); recursion-gkr-cont-{min,blowup2}.elf Makefile targets.
- CLI: --logup-mode now applies to --continuations on prove and verify.
- dump mode: RECURSION_DUMP_GKR=1 + RECURSION_DUMP_EPOCH_LOG2 dumps a
  GKR continuation blob.
- host roundtrip test: multi-epoch GKR continuation proves, verifies
  owned + archived, attests, and passes the consumer program_id check.
The empty guest finishes inside a 2^6-cycle epoch, so the multi-epoch
assert fired; 2^3 matches the standard continuation tests' fixture size.
…oundtrip

The empty guest finishes inside even a 2^3-cycle epoch; fibonacci(10) at
2^4-cycle epochs splits into multiple epochs (the same fixture the
standard continuation roundtrip test uses).
Implements thoughts/logup-gkr/input-layer-design.md: each table's GKR
instance now extends log2(K-hat) layers below the per-row fractions, to
K-hat*N leaves indexed i*K-hat + k (interaction bits LOW) with leaf
(i,k) = (sign_k*m_k(i), fp_k(i)) for k < K and the fraction identity
(0,1) for padding. Leaves are LINEAR in the trace columns.

By pair-level associativity of fraction addition, the extended tree's
layer at size N equals the cross-multiplied per-row fractions
bit-for-bit (regression-tested against compute_logup_leaf_fractions),
so every layer from N up, the root, the batch sumcheck code, the
bridge/kernel columns, the rap-challenge layout, and the wire format
are all unchanged. The instance point splits (kappa, rho): rho (the row
part, same length as before) feeds the column claims and kernel/bridge;
kappa only weights the verifier's reconstruction.

The verifier's reconstruct_and_verify_gkr_claims becomes an EXACT
check for every table and size:

  n = sum_k eq(kappa,k) * sign_k * m_k(claims)
  d = sum_k eq(kappa,k) * fp_k(claims) + (1 - sum_k eq(kappa,k))

replacing the three-way branch whose multi-interaction arm was
FAIL-OPEN (the known soundness gap, port-plan.md section 6): a prover
can no longer run an honest GKR over fabricated leaves. n_layers on the
verifier side = log2(N) + log2(K-hat) with K-hat derived from the AIR's
interactions, never the proof.

The forgery test is un-ignored and extended (honest claims accepted,
fabricated claims rejected, wrong-length kappa rejected). Single-row
multi-interaction tables now run a real GKR over interactions (the old
0-layer special case dissolves).

Stage 1 materializes the deep layers (transient O(K-hat*N) on the
biggest tables) — correctness first; stage 2 (virtual deep layers per
the design doc) restores today's memory profile.

Gates: 291 stark tests green including all GKR e2e roundtrip/tamper
tests, the cross-mode oracle (root unchanged), and the Fact-1
bit-equality test; VM-level GKR e2e + library-path tests green.
The batch prover's instances become GkrInstance { upper_layers (the
materialized >=N tree, exactly the pre-extension shape), input_num_vars,
deep_oracle }. For the below-N layers of an extended-input instance, the
four split tables (nl/nr/dl/dr) are materialized ONE LAYER AT A TIME
directly from the oracle — per-row streaming that rebuilds the K-hat
leaf pairs and folds them c levels — and dropped when that batch layer's
sumcheck completes. The K-hat*N input layer and the intermediate deep
layers are never resident: peak transient is the deepest layer's split
tables (2x child size) instead of the whole extended tree, which OOM'd
a 62 GiB box on ethrex-10tx with stage 1.

Layer values are the balanced partial fraction sums either way
(pair-level associativity), so the transcript is byte-identical to a
fully materialized extended tree. Gated by a differential test: same
seed over mixed-size padded instances => identical proof bytes, points,
claims, and transcript states between GkrInstance::materialized(full
extended tree) and the oracle-backed instance.

A fully materialized tree is the degenerate case (input_num_vars = 0),
which keeps all in-module tests and single-interaction tables on the
old path unchanged. compute_logup_layers (the stage-1 builder) stays as
the differential/test oracle; the prover now uses build_gkr_instance.

292 stark tests green (incl. the differential gate and all GKR e2e
roundtrips, which now exercise the streamed path end-to-end).
…ized

The per-layer materialization of the previous commit still held one deep
layer's split tables (2x child size — up to ~13 GB per big table) and
cost ~30 s of huge-table sumcheck on ethrex-10tx. Now the k-bit rounds
of a deep layer materialize NOTHING: gate sums stream per row through
the oracle (rebuild the K-hat leaves, fold c tree levels + the bound
challenges, apply gate_generic's exact formulas), with eq factored as a
tiny k-part (pre-halved per round) times the untouched row-part. Once
every k-bit is bound, the four tables materialize at N size — absorbing
the folded k-eq into eq_correction and handing the row rounds to the
unchanged fold path. kp == 0 layers materialize directly (already
N-sized).

Peak transient per deep layer drops from O(K-hat*N) to O(N) (the
handoff tables + eq_row), the same order as the resident >=N tree.

Transcript-identical by construction; the stage-2 differential test
(byte-identical proofs vs the materialized extended tree) now pins the
streamed rounds, the kp == 0 path, and the handoff. 292 stark tests
green.
The streamed k-bit rounds recomputed every leaf fingerprint on every
round (21 full passes on the biggest table), pushing the batch prove to
62s on ethrex-10tx. Now each oracle caches its K*N fingerprints once
(row-major, built in parallel on first deep round, freed with the
instance; the padded tail is the constant 1 and never stored) — the one
expensive leaf component. Numerators stay recomputed (1-2 column reads).
Rounds also reuse per-thread scratch buffers (rayon for_each_init /
fold) instead of allocating six vectors per row, and the c-level
fraction folds are padding-aware (identity tail costs nothing).

Same values, same transcript; the byte-identical differential test
still pins the streamed path against the materialized extended tree.
292 stark tests green.
Streaming every deep layer rebuilds a per-row sub-tree of ~K-hat
fraction-adds on EVERY k-round — dominant for the high-c layers whose
tables are small anyway. Split by slot count: layers with > 8 per-row
slots stream (shallow per-row rebuild, big tables that must not
materialize); layers with <= 8 slots materialize whole (bounded
transient <= 8N pairs, decaying per round) and run the ordinary fold
path. The differential test gains a K = 20 (K-hat = 32) instance so the
streamed branch stays pinned byte-identical alongside the materialized
ones.
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