Research: seven-component aggregation performance stack by latifkasuli · Pull Request #5 · leanEthereum/leanVM-b

latifkasuli · 2026-08-07T05:51:02Z

Summary

This draft preserves an evidence-backed aggregation-performance research stack, integrates upstream main at 4982d7eb9972c6ea9fdeba52787c6af0401c4824, and adds a production-only extraction of the validated public-MLE shared-owner path.

It remains a research handoff, not a merge-ready production patch. The older measured mechanisms retain replay selectors and measurement seams for reproducibility. The new shared-owner extraction itself has no runtime research selector or legacy duplication path.

Source and evidence boundary

The six-component all-off/on campaign binds to b61a0ee64a9e5f41c368f937c56cdbb74fd3908b on the older 84fbd3e freeze.
The incremental L0/seven-component campaign binds to 256928f9127c812749e40b08b4cf9744185c6b61 on that same freeze.
The two-kernel campaign binds to a5477b369ee44ef7aea91b0799f7b920b349632f on the earlier e9cd16d integration.
The public-MLE shared-owner system campaign binds to composed experimental commit e5d33ab1e756166daa88c283cd5e089bc1668693, tree 25175fd1b1edfbeb8c94cb4c0768d367ad9a9c2d, with upstream 4982d7e as an ancestor.
The production extraction begins at 7ed548795bc9f04a65010d9705f2a5c980828c61, integrates upstream through 72f2a77574ddd9dad62518c554d4a5a9830e7e2f, and is finalized by 04ba272b14f406b5b629b58de4476983dd8d824b.
Current PR head b7625ef55d40c3dd9150fd4f1e2727bf8c94ce4f records the result and evidence boundary without rewriting any measured commit.

Historical proof hashes, fixtures, geometry, and timings remain evidence only for their named source commits. Wire version 2 identifies the artifact encoding, not protocol compatibility; fixtures and proofs must be regenerated after transcript or recursion-guest changes.

Earlier seven-component result

On the older measured freeze:

Six components versus all off at N2: outer proving -30.91%, process wall -20.72%, peak physical memory -22.98%.
Six components versus all off at N8: outer proving -31.87%, process wall -26.85%, peak physical memory -32.44%.
Incremental L0 NTT at N2: L0 induction -78.02%, PCS opening -25.66%, outer proving -7.07%, process wall -3.51%, peak physical memory -2.48%.
Incremental L0 NTT at N8: L0 induction -74.10%, PCS opening -24.32%, outer proving -6.51%, process wall -4.46%, peak physical memory -3.27%.
All 142 retained proofs were byte-identical within topology and passed the unchanged inspection path.

After seven components, the N2 phase cluster was Bus 0.687050 s, PCS opening 0.527055 s, constraints 0.518037 s, and Flock reduction 0.336672 s. This moved the previous PCS bottleneck; it did not establish that aggregation meets a production budget.

Two-kernel result on `e9cd16d`

Two default-off, fail-closed experiments were measured on the earlier integrated stack:

LEANVM_CONSTRAINT_NODE_SKIP=1 derives one Boolean constraints-sumcheck endpoint from the running claim, including the exact zeta == 1 branch.
FLOCK_PACKED_128_PARALLEL=1 serializes the three live packed witnesses concurrently into disjoint, completely initialized outputs.

The canonical N2 campaign used one AMD EPYC 9354 NUMA domain, CPUs 8–15, four pilots, and 32 measured fresh processes in a repeated 2×2 Williams-square design.

Effect	Paired-block median	Favorable blocks
Node skip on constraints	-62.897 ms	8/8
Parallel path on packed copy	-118.250 ms	8/8
Parallel path on Flock reduction	-124.799 ms	8/8
Combined versus control on outer proving	-189.041 ms (-6.31%)	8/8
Combined versus control on process wall	-175.106 ms (-3.02%)	8/8
Combined versus control on peak physical memory	-3.781 MB	5/8

All 36 proofs were byte-identical and passed inspection. The direct mechanisms were repeatedly favorable, but the stated -350 ms system-materiality gate failed. The system deltas are descriptive rather than a confirmatory production-acceptance result.

Current upstream integration

The branch now incorporates upstream through 4982d7e, including the changes that:

replaced the earlier PCS batching challenges;
replaced the Bus tuple's univariate fingerprint with multilinear equality weights;
deduplicated the Flock ring-switch message;
transported and checked all three public-input limbs;
removed redundant skip challenges and reconstructed-AB checking; and
updated the native, Python, and recursive verifier paths consistently.

The integration retains upstream transcript and pre-bound ring-switch semantics while preserving the research timing spans, direct-fold path, and hardened L0 induction policy. Proofs and fixtures predating these protocol changes remain historical artifacts only.

Production shared-owner extraction

The production path builds the nine public bytecode columns once as immutable Arc<[F64]> owners and shares them across the Bus push and pull layouts.

Reuse is authorized only when all relevant invariants agree:

push and pull contain the same public coordinates;
block index, tuple slot, and bytecode dimension match;
all shared coordinates have one common dimension;
the public table has the exact required length;
push and pull have identical allocation identity; and
no public coordinate appears on the count side.

If authorization fails, proving falls back to the original scalar public-MLE evaluations. The verifier, transcript, and proof format are unchanged. The experimental ownership selector, legacy-owner duplication, diagnostics, CLI option, and campaign plumbing are absent from this production extraction.

Current-head public-MLE shared-owner result

A current-protocol N2 system campaign measured the mechanism on composed experimental commit e5d33ab. The shared arm reused nine public-column evaluations across both Bus decompositions and the bytecode claim; the control arm performed 27 evaluations.

The canonical workload was two children, eight BLAKE3 hashes per child, 64,000 iterations per child, and inverse-rate log 2. It ran on an AMD EPYC 9534 with CPUs 8–15 pinned to NUMA node 0 under inherited memory policy.

One excluded CH pilot preceded the fixed measured order (CHHC HCCH) × 5, giving 40 fresh measured processes and 20 adjacent pairs. There were no retries, replacements, adaptive extensions, or outlier deletions.

Preregistered endpoint	Result
Favorable complete-boundary pairs	20/20
Paired median complete-boundary reduction	69.5405 ms (1.689693%)
Paired median Bus reduction	52.5209925 ms
Boundary-delta MAD	25.7795 ms
Material non-Bus regression	None
Median sampled cgroup footprint, shared minus control	-29,503,488 B (-28.14 MiB; -0.3520%)
Proof exactness and verification	44/44 byte-identical at 229,124 B; accepted

All eight preregistered promotion gates passed. The final campaign seal covers 1,110 entries with SHA-256 aa36dc23b4a0812cf8436bd800188dc54aec2aa89a4128012eb3fcdcb2c3b668.

The original post-run validator exposed a projection bug after validating a new PATH-binding field. An immutable repaired validator and a separate raw reconstruction both reproduced source identity, proof checks, sampler evidence, pair statistics, decision gates, and seals without changing campaign data, ordering, thresholds, or rules.

Evidence boundary and limits

The timing result belongs to experimental commit e5d33ab, not bare upstream 4982d7e and not automatically to the selector-free extraction at this PR head.

The experiment's flag-absent arm exercised the intended production shared-owner path, making the campaign strong mechanism-transfer evidence. Removing the A/B harness nevertheless changes the built source, so the EPYC numbers above are not presented as a direct benchmark of b7625ef. No separate production-head performance rerun has been performed.

This is a single-process N2 result on one EPYC 9534 placement. It does not establish N4/N8 scaling, concurrent-prover admission, cross-host portability, or completion of the broader aggregation objective. The memory endpoint is a 25 ms whole-cgroup sample rather than an exact per-process physical peak, and CPU placement was pinned without a hard memory bind.

Local validation on `b7625ef`

The following passed locally on the final code tree; b7625ef is documentation-only relative to that tree:

cargo fmt --all -- --check.
cargo check -p lean_vm --tests.
cargo test --release -p lean_vm: 31 passed, 0 failed.
cargo testall: zero failures, including the ordinary recursion_2to1 and recursion_2to1_mixed tests.
cargo clippyall.
cargo docall.
ruff check python-verifier/verifier.py.
latexmk -pdf -interaction=nonstopmode main.tex from doc/: successful 43-page build.
Git diff, whitespace, and conflict-marker checks.

These are unsealed compatibility and regression checks, not a replacement performance campaign.

The ignored soundness oracle and a separate --all-features suite were not run in this final validation pass. ruff format --check is also not claimed: the merged python-verifier/verifier.py would currently be reformatted, and this patch deliberately does not include an unrelated whole-file formatting change.

Hosted CI

GitHub created Rust and Documentation PDF workflow runs for prior pushes, but they stopped with action_required before starting any jobs. A leanEthereum maintainer must approve workflow execution for this fork PR. No hosted CI result is claimed until those jobs are approved and complete.

Fast-upstream procedure

Immediately before review, fetch origin/main and inspect:

git rev-list --left-right --count HEAD...origin/main

If the branch is behind, inspect the changed files, integrate the exact new upstream head, and rerun the applicable validation commands. Do not rewrite evidence-bound commits 256928f, 7be45de, a2c1024, a5477b3, or e5d33ab.

Feedback requested

What N2 latency, peak-memory, proof-size, and concurrency budgets should define acceptance?
Is current main the intended architecture for splitting and productionizing the retained research mechanisms?
Should the selector-free public-MLE shared-owner extraction be reviewed first?
Which retained mechanism should be split next: direct fold-6, allocation/capacity changes, AVX-512 Bus MLE, the narrow L0 induction policy, constraints node skip, or packed serialization?

# Conflicts: # crates/pcs/src/stack_open.rs

latifkasuli · 2026-08-09T07:55:56Z

@TomWambsgans We’re pausing new optimization work and would appreciate a decision-level review rather than a line-by-line review of this research stack.

Could you please help with four decisions?

Approve the pending Rust and Documentation workflow runs.
Confirm whether the fail-closed Arc<[F64]> public-MLE shared-owner design fits the intended Bus architecture.
Provide the N2/N8 latency, memory, proof-size, hardware, and concurrent-prover budgets that should define acceptance.
Indicate which mechanism you would like split first into a clean, merge-sized PR, and which current-source reruns you require.

The latest current-protocol shared-owner campaign was favorable in 20/20 pairs: median 69.54 ms reduction at the complete N2 boundary and 52.52 ms in Bus, with 44/44 byte-identical verified proofs. The timing evidence binds to experimental commit e5d33ab; PR #5 documents the selector-free production extraction and that evidence boundary.

If the design is acceptable, we’ll submit only the shared-owner extraction as a fresh small PR and leave this draft as the research/evidence index.

TomWambsgans · 2026-08-09T10:41:42Z

Hi, looking into it

The L0 induction picks between a dense per-query basis expansion and a sparse transposed NTT. Both return bit-identical output, verified by running them side by side on every call site of both benchmarks, so the choice is only ever about speed and cannot affect a proof's validity. The model charged the NTT log_block passes over the codeword domain and dispatched on n_queries > 4 * 2^rate * log_block. That factor is not there in wall time. Timing both paths on AVX512 at the shapes this repository proves: cols=20 rate=1 q=226 dense 643 ms NTT 25 ms 25.2x cols=19 rate=2 q=113 dense 167 ms NTT 26 ms 6.4x cols=20 rate=2 q=113 dense 344 ms NTT 80 ms 4.3x cols=19 rate=3 q=75 dense 120 ms NTT 66 ms 1.8x cols=20 rate=3 q=75 dense 248 ms NTT 127 ms 2.0x Each row implies a crossover at queries / ratio, and dividing by the blowup gives 4.5, 4.4, 6.5, 5.1 and 4.7 queries per unit of 2^rate: one constant, holding across three blowups, with no size term. Both paths scale with the message, so the ratio between them cannot depend on it, which is what the log_block factor was asserting. Its thresholds ran from 168 to 736, an order of magnitude high, and every rate-2 and rate-3 shape was on the slow path because of it. So the fix is the model, not an exception list for the shapes someone measured. The threshold becomes n_queries > 8 * 2^rate. Since a threshold above the true crossover can only forgo a win and can never mis-pick the NTT, 8 is the safe side of every measurement below. Query counts are set by the rate, so the tested quantity only ever takes the values 112, 28 and 9.4, and rate 3 clears the threshold by the least. It was measured rather than left to the margin: faster at cols 16, 19 and 20 in a real proof and at 12 and 14 standalone. pcs_throughput disagrees at exactly one shape, cols 16 rate 3, by +2.6% over 5 paired rounds. That benchmark opens no arena phase, so ArenaVec falls back to the system allocator and the NTT's scratch is charged an allocation it never pays inside cpu::prove. Driving the same shape through the prover (xmss --n-signatures 30 --log-inv-rate 3) puts the NTT 3.9% ahead over 6 rounds, so the benchmark is what is unrepresentative there, not the dispatch. The >= 12 floor is the original's and stays: the ratio argument is size-free, but nothing here measured a smaller message, and the floor is what keeps the log_n = 16 roundtrip on the dense path. Re-measured on Apple M4 Max (NEON, 12P + 4E), an arena phase open per call so the allocator behaves as it does inside cpu::prove, minimum of 3: cols=19 rate=1 q=226 dense 43.7 ms NTT 1.8 ms 24.0x crossover 4.7 cols=19 rate=2 q=113 dense 23.7 ms NTT 3.2 ms 7.5x crossover 3.8 cols=19 rate=3 q=75 dense 17.8 ms NTT 7.9 ms 2.3x crossover 4.2 cols=20 rate=1 q=226 dense 89.4 ms NTT 3.9 ms 23.0x crossover 4.9 cols=20 rate=2 q=113 dense 49.5 ms NTT 8.0 ms 6.2x crossover 4.6 cols=20 rate=3 q=75 dense 35.9 ms NTT 19.0 ms 1.9x crossover 5.0 3.8 to 5.0 against AVX512's 4.4 to 6.5: the size-free ratio holds on a second microarchitecture, and the NTT wins at every shape the change moves. Neither arm has an architecture-specific kernel here, transpose_layers_ext is scalar on both and the AVX512 butterflies serve the commit and fold NTT instead, so what differs between the machines is the balance of bandwidth against cores. On a single cold-page call the crossover rises to between 4.6 and 7.8, still under 8 but leaving rate 3 a margin of 1.3x rather than the 2x the warm numbers imply. Below the floor the expansion is the right call by a wide margin: at cols 10 it is 2x to 8x faster than the NTT. End to end, interleaved, the baseline arm reproducing the old dispatch through a temporary threshold override so both arms are one binary: AVX512, 3 passes per arm per round, measured against 6203daf recursion --n 2 --log-inv-rate 2 1.590 s -> 1.452 s -138 ms (-8.68%), 5/5 rounds favorable recursion --n 2 --log-inv-rate 3 1.883 s -> 1.829 s -54 ms (-2.87%), 4/4 rounds favorable xmss --n-signatures 890 ... unchanged, 2/4 rounds favorable, no consistent sign M4 Max, --repeat 5 --cooldown 6, 5 rounds per arm recursion --n 2 --log-inv-rate 2 0.5412 s -> 0.5224 s -18.8 ms (-3.47%), 5/5 rounds favorable recursion --n 2 --log-inv-rate 3 0.6468 s -> 0.6448 s -2.0 ms (-0.31%), 3/5 rounds favorable Rate 3 on the M4 sits inside the run-to-run band of +-2%, so that machine's recursion benchmark does not resolve it either way. The arithmetic says why: the outer L0 saves about 5 ms of 645 ms and the two inner proofs about 9 ms of a 4.5 s command. It is not a regression, and the microbenchmark is unambiguous at 1.9x to 2.3x, but the -2.87% above is an AVX512 result and does not generalize. Rate 2 does: -8.68% there, -3.47% here, every round favorable on both. Peak memory drops with it, 14.19 GiB -> 13.89 GiB at rate 2, since the dense path holds two 2^cols F192 buffers per thread and the NTT path does not. xmss is untouched because at rate 1 it already cleared the old threshold, so both arms take the same path and the two are the same binary. The benchmark reports outer proving only, which understates the rate-2 result: the whole recursion --n 2 --log-inv-rate 2 command goes 13.41 s -> 12.59 s on AVX512, the two inner proofs each dropping an L0 call from 344 ms to about 70 ms. The idea of moving these shapes onto the NTT path is from #5, which allowlisted rate 2 with 113 queries at columns 19 to 21. This generalizes it to the model, which is what also reaches rate 3. Co-Authored-By: Adam Mohammed A Latif <latifkasuli@gmail.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The leaf vector is the largest buffer a proof allocates, one E element per bus row, and it was built with `ArenaVec::filled(ONE, explicit)` before any leaf was computed. Nothing reads those identities. `stack_offsets` packs the blocks contiguously from zero, so the blocks tile `0..explicit` and every slot is written by exactly one block fill; the implicit identity padding that GKR does rely on lives beyond `explicit`, up to `2^mu`, and was never materialized in the first place. The `covered == explicit` test is what licenses skipping the fill, rather than an appeal to how `stack_offsets` currently packs. If a layout ever left a hole, the sum of the block sizes falls short of `explicit` and the identity fill comes back, so the uninitialized path cannot outlive the invariant that justifies it. Capacity is also rounded up to whole four-tuples: `gkr::QuaternaryLayerState` pads whatever level it is handed to a multiple of four before the sumcheck reads it, and for level zero that level is this vector, so without the reservation the pad reallocates and copies all of it. Measured against f3f4f7d, interleaved A/B, 3 passes per arm per round: xmss --n-signatures 890 --log-inv-rate 1 3.700 s -> 3.646 s -54 ms (-1.46%), 5/5 rounds favorable recursion --n 2 --log-inv-rate 2 1.445 s -> 1.418 s -22 ms (-1.5%), 8/9 rounds favorable Picked first out of the remaining candidates on saving per line added: 76 ms across the two benchmarks for 19 lines, about four times the ratio of anything else measured, and the only one needing no new API and no new test. Idea from #5. Co-Authored-By: Adam Mohammed A Latif <latifkasuli@gmail.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

TomWambsgans · 2026-08-09T20:26:59Z

Hi, thanks for your contribution. I like to keep 1 commit = 1 optimisation, so I did:

f3f4f7d
4edd923
And I have put another one on a PR for later constraints: derive one sumcheck endpoint from the running claim #6

I have included what seemed the best ROI in terms of perf / LoC. Feel free to keep this PR open, will come back to remaining optimisations later. For now my focus is cleaning / doc / soundness etc

latifkasuli · 2026-08-09T20:41:32Z

Thanks, that approach makes sense. We’ll keep #5 open as the research and evidence reference, and pause further optimization work while you focus on cleanup, documentation, and soundness. It’s great to see the L0 dispatch and Bus leaf work upstream, and the constraints endpoint optimization isolated in #6. When you return to the remaining items, we can extract whichever mechanism you select onto current main and run only the validation you need.

latifkasuli added 29 commits August 6, 2026 12:32

research: add 84f Gate 0 measurement seam

b5b9c30

experiment: rederive direct fold6 on c091b04

4892eee

research: add opt-in GKR phase attribution

cd11645

experiment: skip redundant GKR fold zero fill

12dce36

experiment: skip redundant Bus leaf initialization

974740f

experiment: reserve quaternary Bus leaf padding

ee2449d

experiment: preallocate GKR layer tails

efefb23

experiment: preserve quaternary GKR layer headroom

ae54122

experiment: screen AVX-512 MLE fold lanes

eb6f460

experiment: trace Bus post-GKR phases

14f5b60

experiment: gate AVX-512 Bus MLE folds

b61a0ee

experiment: gate L0 induce NTT selection

256928f

perf: select L0 induce NTT for measured shapes

7be45de

test: cover L0 induce policy boundaries

a2c1024

merge: integrate upstream e9cd16d into aggregation stack

ae08017

docs: add aggregation research handoff

3b15970

experiment: derive one constraints sumcheck node

0e36615

experiment: parallelize packed Flock serialization

79c9523

experiment: separate packed copy timing

a5477b3

docs: record current-source kernel pair result

067268f

docs: clarify node skip mechanism

c02f301

test: harden two-kernel exactness boundaries

c4b8348

docs: correct two-kernel evidence boundary

e8e873f

merge: integrate upstream f7b4330

5b7dc20

merge: integrate upstream ffc1a6a

f338bd3

perf: reuse shared public MLE evaluations

7ed5487

merge: integrate upstream 4982d7e

72f2a77

# Conflicts: # crates/pcs/src/stack_open.rs

perf: make public MLE reuse production-only

04ba272

docs: record shared-owner system result

b7625ef

TomWambsgans mentioned this pull request Aug 9, 2026

constraints: derive one sumcheck endpoint from the running claim #6

Open

TomWambsgans marked this pull request as ready for review August 9, 2026 20:27

Navigation Menu

Uh oh!

Research: seven-component aggregation performance stack - #5

Research: seven-component aggregation performance stack#5
latifkasuli wants to merge 29 commits into
leanEthereum:mainfrom
latifkasuli:research/aggregation-stack-20260807

latifkasuli commented Aug 7, 2026 •

edited

Loading

Uh oh!

latifkasuli commented Aug 9, 2026

Uh oh!

TomWambsgans commented Aug 9, 2026

Uh oh!

TomWambsgans commented Aug 9, 2026

Uh oh!

latifkasuli commented Aug 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

latifkasuli commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Source and evidence boundary

Earlier seven-component result

Two-kernel result on e9cd16d

Current upstream integration

Production shared-owner extraction

Current-head public-MLE shared-owner result

Evidence boundary and limits

Local validation on b7625ef

Hosted CI

Fast-upstream procedure

Feedback requested

Uh oh!

latifkasuli commented Aug 9, 2026

Uh oh!

TomWambsgans commented Aug 9, 2026

Uh oh!

TomWambsgans commented Aug 9, 2026

Uh oh!

latifkasuli commented Aug 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

latifkasuli commented Aug 7, 2026 •

edited

Loading

Two-kernel result on `e9cd16d`

Local validation on `b7625ef`