This repository was archived by the owner on Sep 12, 2026. It is now read-only.
(almost) free PCS padding at commitment - #11
Merged
Merged
Conversation
The L0 interleaving now takes the committed witness's TOP
INITIAL_FOLDING_FACTOR coordinates, so lane l is the contiguous stack block
q[l * 2^(mu-k) ..) and the stack's zero tail is whole lanes. `whir::commit`
encodes only the n_lanes = ceil(P / 2^(mu-k)) lanes that carry data, and the
opening's dense weight, its first k sumcheck rounds, the stack allocation and
its zero fill all shrink with them. The absent lanes encode to zero codewords,
which is exactly what the leaf image and an opened row carry for them, so a
verifier sees the same 2^mu-word commitment either way and never learns
n_lanes: the whole change is prover-side except for one thing.
That one thing: the fold challenges arrive in round order while every
transparent weight is written in witness coordinates, so all three verifiers
rotate the terminal point left by k before evaluating it. Rust does it before
`eval_b_at`, Python before `evaluate_basis`, and in the guest `open_stacked`
returns a rotated buffer pair built where the level shape is still a
compile-time constant, which keeps the two-buffer split point and every
overlap pin downstream untouched.
Soundness rests on the weight vanishing at every boolean point past P, which
holds because each weight family is supported on a placed column. A prover
filling the uncommitted lanes with anything commits q + delta supported there
and proves the same claims; committing fewer lanes than n_lanes can only make
its own proof fail. `ood_samples[0] == 0` is now load-bearing for this: an
out-of-domain weight is a full tensor that would not vanish out there.
The Merkle half is deliberately unchanged. A leaf is still 2^k words, with the
absent lanes' zeros supplied from a staging tile, because the recursion guest
cannot hash a run-time-length leaf: BLAKE2s's byte counter and final flag are
compile-time bytecode immediates. Shrinking it needs an 8-way match_range on
ceil(n_lanes/8) inside the guest's L0 query loop, and buys the Merkle third of
the commit stage plus proof size and guest cycles.
The encode keeps the tuned interleaved driver and only its first pass changes,
since that is the pass that turns lane-major message blocks into interleaved
codeword rows. It transposes in row tiles rather than gathering in the fused
radix-8 pass's order: the fused order reads n_lanes streams 2^(mu-k) words
apart and measured 28% on top of the whole encode, while tiling reads every
stream in bursts and costs 3%. Two lane-major codeword layouts were tried and
rejected on measurement, the first because its deep layers fall to scalar
butterfly widths (3x slower).
Measured against the parent, M4 Max, 5 repeats:
xmss --n-signatures 900 --log-inv-rate 1
1.135 s -> 1.049 s, 793 -> 858 XMSS/s, peak 20.84 -> 15.99 GiB
recursion --n 2 --xmss-per-leaf 900 --log-inv-rate 2
0.596 s -> 0.585 s, peak 24.95 -> 20.77 GiB
The recursion node's fill is 0.909, so it has almost nothing to skip; its
leaves are the 0.573 case. Since mu = log2_ceil(P), n_lanes always exceeds
2^(k-1), which caps the encode saving near half.
Doc: Annex B gains its coordinate-order convention and a paragraph on the rows
a prover may omit; the stacking section gains the concrete choice, both
soundness conditions and the rotation.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two savings the previous commit left on the table, both from the same change of
leaf-image order: an L0 leaf now reads its lanes from the top interleaving index
downwards, so codeword lane t is stack block n_lanes-1-t and the lanes a
padding-free commitment leaves out are the image's LEADING words.
That order is forced by BLAKE2s. A zero SUFFIX cannot be shared, since its
compressions take whatever state the real data left; a zero PREFIX can, because
its compressions depend on nothing after them. So the whole 64-byte blocks of
absent lanes are one chaining value every leaf shares, computed once per commit
(`blake2s::zero_prefix_state`) and continued per leaf
(`hash_many_dyn_from_state`, the batched kernels now taking a state and a
counter offset; `hash_many_dyn` is that with the IV). The digest is
bit-for-bit the standard BLAKE2s of the whole image.
The same order lets the image's tail alone travel: `PrunedMerklePaths` stores
`n_lanes` words per L0 row, and `open` restores the prefix into
`RawMerklePath`, which the recursion guest and the Python verifier read. So the
Rust and Python verifiers derive `n_lanes` from the announced layout to parse a
row and supply the zeros themselves, while the guest keeps receiving full-width
images and is unchanged in everything that costs it: 798,651 cycles and 323,181
bytecode instructions, both identical. Its only edit is a compile-time slot flip
in the level-0 row weights, since the image it folds is lane-descending.
Both savings are quantised to whole blocks of 8 lanes, so a witness whose
`n_lanes` is just under `2^k` gains nothing from either; the proof-size saving
is not quantised.
Measured against the parent, M4 Max, 5 repeats:
xmss --n-signatures 900 --log-inv-rate 1
proof 352.5 -> 305.8 KiB, commit's Merkle stage 87 -> 64 ms,
1.049 -> 1.038 s
recursion --n 2 --xmss-per-leaf 900 --log-inv-rate 2
proof 218.6 -> 213.6 KiB, 0.589 -> 0.596 s (n_lanes = 59 leaves no whole
block to skip), peak memory 20.77 -> 20.04 GiB
Against main the branch now stands at 1.135 -> 1.038 s (793 -> 867 XMSS/s),
proof 352.4 -> 305.8 KiB, peak 20.84 -> 15.98 GiB.
The equivalence test drops its byte-identical-transcript claim, which the proof
change makes false on purpose, for the sharper one: same root, same scalar
stream, and the stored row is exactly the full image with its leading zeros
dropped, with a wrong-width row rejected.
Doc: every place that said the Merkle work was untouched or that no verifier
learns the lane count now says what is actually true, in AGENTS.md,
`lean_vm::pcs`, `whir::commit`, `stack_open` and the stacking section.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A commitment with nothing to skip (`n_lanes == 2^k`, which is what
`FLOCK_N_LOG=18 blake2s_batch` commits) was about 1% slower than before the
padding-free layout. Two causes, one of them removed entirely.
The opening was 1.1% slower because the lane fold's inner loop indexed
`f[src0 + t]` and `f[src1 + t]` instead of taking four equal-length slices, so
it kept its bounds checks and did not vectorise the way the adjacent-pair kernel
it replaced does. Sliced, the stage measures 225.8 and 228.9 ms against main's
226.7 and 229.1 ms, i.e. parity.
The commit stage was 8% slower because the encode replicated the transposed
message into all `2^rate` replicas and only then transformed, which gives up the
fused first pass and costs an extra sweep of the whole codeword. It now
transposes into the codeword's OWN message region and runs the fused pass in
place from there, blocks descending so replica 0, which is the message, is
transformed last once every other replica has read it. That leaves 4%.
The remaining 4% is one blocked transpose of the message, which a row-major
message does not need, and it is the cheapest structure I could measure:
fuse the transpose into the fused pass (8 * n_lanes streams) +28% encode
stage those eight row windows in cache, one slice at a time +21% encode
lane-major codeword, no transpose at all +240% encode
(a single lane's last three layers fall to scalar butterfly width)
transpose into the message region, then fuse in place +5% encode
At 15% of that benchmark's prove time this is ~0.6% overall, inside its own
run-to-run spread (main measured 594 to 622 ms across these runs). Reaching
exact parity needs the transpose moved into the deep phase's cache-resident
sub-blocks, which wants either a second codeword buffer or a lane-major final
layout with a gathering leaf hash.
The headline workloads are unchanged by this: xmss 1.031 s at 872.9 XMSS/s and
305.8 KiB, recursion 0.594 s and 213.6 KiB.
Also one encode path instead of two: `encode_interleaved_in_place` is the
primitive, `encode_interleaved` a copying wrapper for the test oracle, and
`replicate_in_place` is shared with it. `transpose_lane_major` scatters straight
into its destination run rather than filling a stack tile and copying it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review of the three padding-free commits. Nothing changes what is proved; one change makes the L0 leaf hashing faster. The staging tile now hands the batched BLAKE2s whole batches. It sized itself in bytes, so the production shape gave it 51 leaves per tile and the hasher sent 3 of them down its scalar path, 60 of every 1024 leaves. Rounding the tile's leaf count to a multiple of the widest paired batch takes the L0 Merkle stage from 67 ms to 59 ms on the 900-signature XMSS aggregation. The rest is the code saying what it does: - `zero_prefix_state` had inherited `hash_many_dyn`'s doc line, and `hash_many_dyn` had been left with none. It also re-asserted the three preconditions its delegate asserts, under a SAFETY comment for arms it no longer has. - `transpose_lane_major` took a `&self` it never read, advertising a dependence on the transform's domain that it does not have. It is a free function next to the encoder now. - `encode_interleaved`, the copying wrapper, had one caller left, a test. Deleted; the test writes its message and calls the primitive. - The L0 row decode was duplicated verbatim in both verifiers, comment included; it is `l0_row_ascending`. - `hash_row` and `leaf_image` each derived the zero prefix and built the image separately. One `leaf_image`, one `hash_words` over it, so the raw path stops cloning its row too. - The dense verifier's `basis_ris_starts[0]` was a never-read `usize::MAX`. Slot 0 leaves the loop, and the two side vectors zip. - The padded-rows test had a duplicated case and no case where the zero prefix is whole blocks exactly, or where it is shorter than one block at the production leaf width. It has both, and the list names its regimes. - One LaTeX paragraph was hard-wrapped mid-sentence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
TomWambsgans
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
How it works? Just pick a nice variable folding ordering in WHIR. For more details: see end of Annex B, subsection "Optimizations", in doc