instruction: generate witness for multilinear eval by tcoratger · Pull Request #12 · leanEthereum/leanVM

tcoratger · 2025-08-17T18:13:23Z

No description provided.

# This is the 1st commit message: wip: issue/88 # This is the commit message leanEthereum#2: wip: issue/88 # This is the commit message leanEthereum#3: wip: issue/88 # This is the commit message leanEthereum#4: wip: issue/88 # This is the commit message leanEthereum#5: wip: issue/88 # This is the commit message leanEthereum#6: shrink test_match # This is the commit message leanEthereum#7: wip: issue/88 # This is the commit message leanEthereum#8: remove mark_vars_as_declared # This is the commit message leanEthereum#9: wip: issue/88 # This is the commit message leanEthereum#10: wip: issue/88 # This is the commit message leanEthereum#11: wip: issue/88 # This is the commit message leanEthereum#12: reverse stack trace order # This is the commit message leanEthereum#13: add failing test case from shrinking WHIR recursion # This is the commit message leanEthereum#14: wip: issue/88: bugfix: eliminate name shadowing # This is the commit message leanEthereum#15: refactor: remove declared_vars # This is the commit message leanEthereum#16: wip: issue/88

…ERVE Three fixes from upstream zk-alloc (Barnadrot/zk-alloc PRs leanEthereum#10, leanEthereum#11, leanEthereum#12): 1. realloc: ptr::copy instead of copy_nonoverlapping — prevents UB when arena realloc hands back overlapping src/dst across phase boundaries (upstream hunt-2-fix, commit 23004b5) 2. begin_phase: swap+assert instead of unconditional store — panics if called while a phase is already active, catching nested-phase bugs early instead of silently corrupting (upstream PR leanEthereum#12) 3. syscall: add aarch64 Linux raw-syscall module with MAP_NORESERVE — prevents SIGABRT on aarch64 Linux with vm.overcommit_memory=0 (upstream PR leanEthereum#11). macOS path unchanged. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* Defer the bus forms' reductions to one per constraint row A table's constraint summand is its AIR identity plus three bus forms, and every term of every form reduced on its own: a dense dot product, then one reduction per quadratic product, then a reduced add between the forms. MUL paid 33 reductions per node per row, each six CLMULs, against 102 CLMULs of actual dot product. Both the y-fold and the base reduction are GF(2)-linear, so they commute with XOR. `ColVal` gains an `Unreduced` accumulator (`F192BaseUnreduced` for a K round, `F192Unreduced` for an E one) and every product now lands there, so a table's whole summand reduces once. xmss 900 r1 2.934 s -> 2.911 s (-0.8%) xmss 900 r2 3.689 s -> 3.672 s (-0.5%) rec 2 r1 1.732 s -> 1.702 s (-1.7%) rec 2 r2 1.570 s -> 1.545 s (-1.6%) Prove constraints stage 395 ms -> 368 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Size the extension NTT's deep sub-group for a 24-byte row The two additive NTTs shared a 2 MiB sub-group target, but the target is spent against `log2_ceil` of the row size, and that rounding is not the same on both sides: the base encode's 37 F64 lanes round 296 bytes up to 512, while the extension encode's 8 F192 lanes are exactly 192 and round to 256. The same budget therefore bought the extension NTT a sub-group twice as large in real bytes, past a worker's share of L3, and its deep layers streamed. xmss 900 r1 2.911 s -> 2.903 s (-0.3%) xmss 900 r2 3.672 s -> 3.611 s (-1.7%) rec 2 r1 1.702 s -> 1.687 s (-0.9%) rec 2 r2 1.545 s -> 1.538 s (-0.5%) L1 recursive commit NTT 178 ms -> 154 ms The base encode measures best where it is; 18, 19, 20 and 22 all cost it 8% or more. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fuse three layers per pass in the extension NTT The base encode has fused three layers per pass since it was written; the extension encode, copied from it, stopped at two. That cost the recursive commits a third more passes over an 800 MB codeword, and, because the AVX-512 kernel transposes each row out of AoS on load and back on store, a third more transposes per butterfly: a fused-2 group paid 96 permutes for 72 CLMULs, a fused-3 group pays 96 for 216. The layer ladder is now `run_layers_ext`, the shape of the F64 twin's `run_layers`, and both fused widths share one kernel driven by a table of (top, bot, twiddle) triples, so the AVX-512 path holds all four or eight rows in registers for the whole pass with one body rather than two. xmss 900 r1 2.903 s -> 2.826 s (-2.7%) xmss 900 r2 3.611 s -> 3.486 s (-3.5%) rec 2 r1 1.687 s -> 1.654 s (-2.0%) rec 2 r2 1.538 s -> 1.511 s (-1.8%) L1 recursive commit NTT 154 ms -> 111 ms, L2 55 ms -> 39 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Publish two write-once buffers with streaming stores An ordinary store fetches the cache line it is about to overwrite, so a buffer written once and not read back until a later pass costs its own size twice in memory traffic. On this box that is the difference between 28 GB/s and 62 GB/s of useful writes on a 16-thread gigabyte fill, and the prover is bandwidth bound: going from four cores to eight buys only 1.44x. `primitives::stream::Stream` is the region those stores belong to. Streaming stores are weakly ordered, so the `sfence` lands on drop, once per region rather than once per copy, which is what makes a fold kernel's 192-byte publishes worth streaming; the type is neither `Send` nor `Sync`, so a region cannot outlive the thread whose stores it fences. Two destinations qualify today. The zerocheck's fused fold builds its round message from the folded values while they are still in registers, so nothing reads its output until the next round. The recursive commits' replica fill is a pure copy that the transform's first pass reads much later. Both are far larger than any cache. Elsewhere a consumer follows in the same pass, and there the fetch a streaming store avoids just becomes that consumer's miss. xmss 900 r1 2.826 s -> 2.755 s (-2.5%) xmss 900 r2 3.486 s -> 3.412 s (-2.1%) rec 2 r1 1.654 s -> 1.629 s (-1.5%) rec 2 r2 1.511 s -> 1.500 s (-0.7%) zerocheck tail 177 ms -> 171 ms, recursive commits 290 ms -> 271 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Stage the lane fold in L1 so its output can stream The lane rounds fold the committed witness and its basis, then read both back to build the next round's message. The read back is an L2 hit, so it was free, but it is what forced the fold's output to be written normally: an ordinary store fetches every line it overwrites, and at the L0 shape that is 1.6 GB of read-for-ownership traffic in a round that is already bandwidth bound. Folding into a 12 KiB stage first moves the message's read into L1 and leaves nothing reading `nf`/`nb` until the next round, so the stage publishes with streaming stores and the fetch disappears. 64, 256 and 512-element stages all measure slightly worse. xmss 900 r1 2.755 s -> 2.716 s (-1.4%) xmss 900 r2 3.412 s -> 3.341 s (-2.1%) rec 2 r1 1.629 s -> 1.601 s (-1.7%) rec 2 r2 1.500 s -> 1.469 s (-2.1%) initial sumcheck 300 ms -> 230 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Issue the zerocheck folds' products four at a time A tower product is a chain of carry-less multiplies and a reduction, and a scalar one leaves most of the multiplier idle waiting on it; four independent products fill the 128-bit lanes of one AVX-512 register and measure twice the throughput. The GKR layer already had that dispatcher hidden inside it, so it moves to `primitives::field` as `mul2`/`mul4`/`mul_unreduced4` and the four zerocheck fold kernels, all of them scalar, now use it. The pair kernel had been hand-unrolled four ways for the same reason, in 130 lines of longhand naming sixteen fold products and eight message products; the vector form says the same thing in thirty and hands the sixteen to four instructions. The two round-2 kernels gain the unrolling they never had, and with it the eight-output streaming publish, a padding hole folding to zero rather than branching around its stores. xmss 900 r1 2.716 s -> 2.660 s (-2.1%) xmss 900 r2 3.341 s -> 3.275 s (-2.0%) rec 2 r1 1.601 s -> 1.597 s (-0.2%) rec 2 r2 1.469 s -> 1.460 s (-0.6%) zerocheck round 2 158 ms -> 131 ms, tail 171 ms -> 136 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Publish the GKR layer fold with streaming stores Each radix-four layer folds into a buffer only the next round reads, and the top layer of the bus product tree is tens of megabytes, so by then it is long evicted: an ordinary store's fetch of every line it overwrites is pure waste. Two output rows are eight elements, 192 bytes, three whole cache lines, which is exactly the grain to publish. xmss 900 r1 2.660 s -> 2.633 s (-1.0%) xmss 900 r2 3.275 s -> 3.251 s (-0.7%) rec 2 r1 1.597 s -> 1.579 s (-1.1%) rec 2 r2 1.460 s -> 1.453 s (-0.5%) Bus GKR stage 230 ms -> 213 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Sum a table's three bus forms into one before evaluating it The constraint batch adds the three sides' evaluations, so the row loop was running three dot products over the same column values, and for MUL three product lists that largely name the same pairs. Summing the scaled forms once at setup gives one dot and one merged list: XOR's linear part goes from 34 terms to 15, MUL's quadratic part from 30 products to 15, and each is read once per node rather than three times. Exact by linearity of the form in its coefficients, and both prover and verifier build their airs through the same function, so neither can see a different total. xmss 900 r1 2.633 s -> 2.516 s (-4.4%) xmss 900 r2 3.251 s -> 3.134 s (-3.6%) rec 2 r1 1.579 s -> 1.473 s (-6.7%) rec 2 r2 1.453 s -> 1.388 s (-4.5%) Prove constraints stage 366 ms -> 246 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Run the zerocheck's round-one kernels a register wide Two 128-bit loops in the univariate-skip round, on a machine whose registers are four times that. The inverse-NTT table apply held its accumulator as four 128-bit chunks and round-tripped every one of them through memory once per input chunk. At the protocol's `ell = 64` the whole accumulator is a single ZMM, and the `i' + 8b` permutation collapses to one `vpermq`: an XOR of `8b` on a byte index is an XOR of `b` on a qword index, which is the narrow arm's chunk swap and half-swap in one shuffle. The GFNI combine then multiplies and folds the same 64 bytes in one register rather than four. Byte unpacking and `packus` are exact inverses within a 128-bit lane, so the wide accumulators sit in a different order and narrow back to the same bytes. Machines without AVX-512 keep both 128-bit arms, which the oracle test now reaches through the dispatcher rather than by naming one. xmss 900 r1 2.516 s -> 2.478 s (-1.5%) xmss 900 r2 3.134 s -> 3.130 s (-0.1%) rec 2 r1 1.473 s -> 1.473 s (0.0%) rec 2 r2 1.388 s -> 1.380 s (-0.6%) zerocheck round 1 132 ms -> 108 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the base encode's butterfly an AVX2 arm The kernel was AVX-512 or scalar, so a machine with VPCLMULQDQ and no AVX-512 ran the innermost loop of the largest NTT one element at a time. The 256-bit form is the same three steps at half the width; only the odd-lane blend changes, from a mask to a 32-bit immediate. Unchanged on AVX-512 (the arm is compiled out). With AVX-512 disabled at `-C target-feature`: base encode NTT 417 ms -> 291 ms xmss 900 r1 2.948 s -> 2.831 s (-4.0%) rec 2 r2 1.578 s -> 1.506 s (-4.6%) The extension encode's butterfly is still AVX-512 or scalar and is the larger remaining gap there: 251 ms against 111 ms with AVX-512. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the two measured facts the last campaign turned on The prover's bandwidth ceiling and Zen 4's half-rate 512-bit shuffles decided most of what was worth doing and most of what was not, and neither is guessable from the code. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fan out the round a constraint table joins the batch Every later fold of a table's columns is dispatched across the pool, but the one in the round it joins ran as a serial `map().collect()` on the dispatcher. That is the largest fold the table ever does: it reads all `2^tau` of each column and writes half that many lifted values, half of everything that table will ever fold, with fifteen threads idle. Prove constraints stage 249 ms -> 156 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fan the replica fill out over replicas as well as message chunks The fill chunked the message alone, but down the recursion the message shrinks by 2^3 a level while the codeword shrinks by only 2^1, so from the third level on there was exactly one chunk and a couple of hundred megabytes went to one thread. Ordering the (chunk, replica) grid replica-innermost keeps the property the chunking was there for, since a worker's run of tasks still copies one message chunk into every replica while it is in cache. xmss 900 r1 2.418 s -> 2.397 s (-0.9%) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Run the encode's whole-buffer layers as one gathered wide-radix pass Up in the top phase a pass over the codeword is 2.5 GB, and the fused kernels capped at three layers, so the six layers between the seeded first pass and the cache-resident phase cost two of them. They cannot simply be widened in place. A group of `j` layers touches `2^j` rows spaced `block_size >> j` apart, and at 37 lanes any stride of 512 rows or more is an exact multiple of 4 KiB, so the rows of a wide group land in a handful of L1 sets. Gathering the group into one contiguous 32 KiB scratch removes the aliasing; the copy is L1 traffic against a DRAM pass. `twiddles_radix` generalizes the radix-8 twiddle set to any width by the same F2-linearity, and `radix_butterflies` is the radix-8 schedule with its distance and twiddle stride parameterized, so `j = 3` is the old kernel with its rows gathered. xmss 900 r1 2.426 s -> 2.376 s (-2.1%) rec 2 r2 1.349 s -> 1.310 s (-2.9%) base encode NTT 273 ms -> 244 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the univariate-skip row fold an x86 kernel The fold is one table lookup and one XOR per byte, run once per post-URM row, which is a hundred million times a proof and the innermost operation of both round-two kernels. aarch64 had a hand-unrolled kernel for it; x86 fell through to the scalar table lookup, whose trip count is a struct field the compiler cannot see and whose every lookup is bounds-checked. The x86 twin is the same shape: each 24-byte entry folds as one 128-bit load over `(c0, c1)` with `c2` in a scalar register, unrolled for the protocol's eight chunks. The oracle test that pinned the NEON kernel was gated on aarch64 and so tested nothing here; it now goes through the dispatcher and covers whichever arm the target reaches. xmss 900 r1 2.376 s -> 2.350 s (-1.1%) rec 2 r2 1.310 s -> 1.304 s (-0.5%) zerocheck round 2 133 ms -> 110 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Publish the packed flock witness into q_flock with streaming stores The lift into the committed column is a word-for-word copy of a quarter of a gigabyte, and nothing reads that window until the commitment encodes it. The read-for-ownership an ordinary store pays is therefore pure waste, and most of it does not even show in this stage: the dirty lines are written back later, during the commit. xmss 900 r1 2.350 s -> 2.331 s (-0.8%) rec 2 r2 1.304 s -> 1.291 s (-1.0%) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Take every table's column and pair evaluations from one eq table `tables_at` and `prod_sums_at` evaluate the same table at the same point, and each ran a fold ladder per column and per pair: a ladder rebuilds the equality weights implicitly every time, and lifts every K word it reads into an E it writes and reads again, where a dot against materialised weights moves the column's own eight bytes. It also allocated a fresh system vector per ladder level, on pool workers, which is where most of the prover's remaining per-proof page faults were coming from. One eq table per table now streams past every column and every pair at once, with an unreduced accumulator each. Exact by construction: `fill_eq_table` is the same LSB-first weight the ladder binds in, and the field is exact. xmss 900 r1 2.334 s -> 2.318 s (-0.7%) Prove bus stage 450 ms -> 410 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the extension NTT's butterflies a NEON arm The base encode's butterfly has had an eight-lane NEON kernel for a while; the extension NTT's had only the AVX-512 one, so on Apple silicon both the per-row butterfly and the fused radix-4/radix-8 passes ran the portable lane-at-a-time loop. That is 12% of a fibonacci proof spent scalar. `mul_base` scales all three coefficients of an F192 by the same twiddle and the adds are elementwise, so a butterfly over n interleaved F192 lanes is exactly the base field's over 3n u64. The AoS layout therefore needs no transpose here, which is the one thing the AVX-512 arm has to pay for per pass: its register holds one coefficient of eight lanes, so it gathers them. Both arms reduce through the existing all-PMULL lane-pair fold. fibonacci 2M r1 0.5044 s -> 0.4988 s (-1.1%) rec 2 r2 0.5386 s -> 0.5316 s (-1.3%) extension NTT 55.4 ms -> 49.2 ms (-11%) Measured on an M4 Max MacBook Pro, five interleaved A/B rounds at cooldown 6. x86 is untouched: the new kernels are gated on aarch64 with `aes`, and the portable arm's condition only grows the case it already excluded. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hold two vectors of every row in the extension NTT's fused pass The NEON fused pass took one 128-bit vector of each row at a time, which leaves a radix-8 schedule holding eight vectors against the 32 the register file has, too few in flight to cover the reduction's dependent PMULL folds. Two vectors a row doubles the independent work without spilling: sixteen live, and the schedule's twelve butterflies each have two products to interleave. Three and four vectors a row measure the same to within the noise, and four puts a radix-8 pass at exactly 32 live vectors, so two is where the headroom is. extension NTT 54.2 ms -> 41.4 ms (-24%) PCS open 174 ms -> 152 ms (-12.5%) fibonacci 2M r1 0.5044 s -> 0.4942 s (-2.0%, cumulative with the NEON arm) rec 2 r2 0.5372 s -> 0.5270 s (-1.9%, cumulative) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Run the extension NTT's fused pass a butterfly at a time on NEON The NEON fused pass held a tile of every row in registers for the whole schedule, the shape the AVX-512 arm takes because it has to transpose the rows anyway and wants to pay for that once per pass. NEON transposes nothing, so it was buying only the saved reloads, and paying for them: a tile leaves just its own width of independent work to cover the reduction's dependent PMULL folds, while a whole row leaves the entire lane count. The rows never leave L1 either way. Running it a butterfly at a time over whole rows, as the F64 twin's `radix8_butterflies` already does, is 26% better. The same restructure in the other direction confirms it from the other side: giving the base encode's radix-8 group the register-resident tile costs its `Commit` 14%. extension NTT 42.3 ms -> 30.8 ms (-26%) PCS open 155 ms -> 148 ms extension NTT, against the branch tip before this NEON work: 59.5 -> 30.8 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record what the NEON campaign measured Two facts worth not re-deriving, in the shape the last campaign's note took. Apple silicon has no read-for-ownership to elide, so `Stream` is correctly a copy there and wants no `STNP` arm: a store-only fill sustains 289 GB/s, exactly what a read-only pass over the same buffer reaches, and `STNP` measures identical to `STP` at every thread count. The L1 stage in the lane fold still earns its keep there, for the read locality alone. And NEON is the width ceiling (no SVE; SME2 is matrix-only), so an AVX-512 win that is purely width has no counterpart. What ports is shape, sometimes inverted: the register-resident tile the AVX-512 fused passes use costs NEON 26% on the extension NTT and 14% on the base encode. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keep measurements out of comments A timing, a throughput or a percentage in a comment is true on one host with one compiler on one day, and nothing ever rechecks it. Several in here were already describing a prover that has since been rewritten around them: the arena's figures predate the walks replacing the materialized matrices, and the flock fold's predate the current kernel. So they come out, everywhere, and the rule goes in next to the one about comments being sparse. What each comment kept is the direction and the reason, which is the part that stays true and the part a reader needs. The numbers are in the commit messages that introduced them, which are dated and do not rot. The statistics themselves stay: a "95% confidence half-width" is what the estimator computes, not a claim about how fast anything ran. README.md keeps its benchmark output too, which is the point of it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keep the zerocheck folds' quads out of memory on NEON `Issue the zerocheck folds' products four at a time` rewrote the four kernels around `[F192; 4]`, which is free on AVX-512, where the quad IS the register. On NEON a quad is four separate PMULL chains, and the array is not free: it spills, and the whole rewrite came out 17% down on the zerocheck and 5% down on `blake2s_batch` against main. Three things it was not: the products themselves measure the same either way, destructuring the results changes nothing, and forcing `mul4` to inline recovers almost none of it. Reverting the arrays recovers all of it. So the quad becomes a tuple, and the arrays appear only inside `mul_quad` / `mul_quad_unreduced`, on the one target whose multiply is wide enough to want them. There the four operands are gathered exactly as before and go to one instruction group; everywhere else they stay four ordinary products and never reach memory. Both arms keep all four kernels unrolled four ways and keep the eight-output streaming publish, so nothing that commit added is given up. blake2s_batch n_log=18, zerocheck 288 ms -> 251 ms (main: 248 ms) blake2s_batch n_log=18, prove 639 ms -> 605 ms (main: 607 ms) xmss 900 r1 0.9445 s -> 0.9268 s (-1.9%) rec 2 r2 0.5088 s -> 0.5080 s (neutral) Found by BENCH_REPEAT=3 BENCH_COOLDOWN=2 FLOCK_N_LOG=18 on the flock bench, which loads the zerocheck far harder than the VM benchmarks do. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record why a quad wants to be a tuple on NEON The shape lesson from the zerocheck fix, next to the width one. Worth writing down because the symptom points away from the cause: the products measure the same either way, so the arithmetic looks innocent and the array does not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Note how to compile the arm this machine never builds Every vector kernel here has an x86 arm and an aarch64 one, and on an Apple dev machine the x86 one is not compiled at all, so nothing catches a typo in it before it reaches the server. A cross `cargo check` does, needs no linker, and takes a couple of seconds. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the pool more claims than it has workers, and stop marshalling GKR's quads Two independent things, both of which come from the pool being 11 performance workers and 4 efficiency ones rather than 16 equal ones. `recommended_chunk_size` and `window_rows` both aimed at four claims per worker. That is right on a homogeneous host, where every worker finishes its share together; here an efficiency core takes about three times as long, so with four claims each the whole dispatch waits on an E core holding a P core's share, and the reserved worker made the count odd so no power-of-two shape divided it evenly either. Both now aim far higher, with a floor so the small end is no finer than it was, and guided self-scheduling hands out smaller first claims for the same reason. `Slot` joins `Line` at 128-byte alignment, which is the line. Separately, `mul4` was not inlining on aarch64: it expands to four Karatsuba chains there, well past the inliner's budget, so its two `[F192; 4]` arguments and its result went through the stack on every call, and `quartic_summand` carried a 432-byte frame and a ten-register spill to feed it. Forcing it inline removes the symbol from the binary entirely. The GKR layer fold then no longer needs its staging array: on a target whose stores already avoid the fetch it bought nothing, and the `slot.len()` the compiler could not fold made the publish a libc `memcpy` call per output pair. xmss 900 r1 0.9128 s -> 0.8906 s (products and fold) -> 0.8800 s (pool) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fold the tower reduction's overflow with a second PMULL, not on the scalar side `base_reduce` folded the first product's ≤4-bit overflow with a shift-XOR chain in a general register, on the premise that the vector pipes were PMULL-saturated and the scalar ports were free. On Apple silicon they are not: PMULL retires at about the rate `eor` does, so the second product is nearly free while the three lane extractions the scalar form needs are not, and they are on the critical path of every F192 multiply in the prover. This is the same all-PMULL fold `reduce_pair_pmull4` already uses for the base field, which records the same conclusion in its own comment. Cheaper reduction also brings `mul4` back under the inliner's budget on its own, so the two reinforce. xmss 900 r1 0.8876 s -> 0.8674 s (-2.3%, five of five rounds) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Slice the multilinear folds, and reduce F64 the way F192 now does `fold_high_inplace` and its two `eq` siblings indexed the container twice per element. Nothing proves a `Vec`'s data pointer does not alias its own elements, so each iteration reloaded the pointer and the length and paid a bounds check for them; splitting once hoists all of it. These run one column per pool task out of the constraint fold, so it is 11 workers' worth. `mul_shift_tail` gets the same all-PMULL fold as `base_reduce`, for the same reason, and its doc no longer claims the vector pipes are PMULL-saturated. xmss 900 r1 0.8562 s -> 0.8430 s (-1.5%, five of five rounds) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Let auto-deref do the splitting clippy, no behaviour change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Interleave four BLAKE2s groups on NEON, not two Four lanes is narrow enough that the G function's dependency chain bounds this backend rather than the four SIMD pipes, which is why the rounds are `inline(never)` and why two groups were already interleaved. Two is not the plateau though: the instruction count that justified it only measures the round's ALU work and ignores the store-to-load round trip at each round boundary, and the reordering window is wide enough to cover several of those. Four measures best; six and eight fall back slightly. `PAIR: bool` becomes `GROUPS: usize` and the pair kernels become const-generic over it, so x86 keeps exactly one group and its own path. The shared transposed block buffer already had room for four NEON groups. batched BLAKE2s, LEN=256 about a fifth faster xmss 900 r1 0.8408 s -> 0.8284 s (-1.5%, five of five rounds) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Batch Merkle leaves by what the hasher actually consumes `BATCH_LEAVES` was 32 because the widest backend is 16 lanes paired, and 32 is a multiple of every narrower backend's paired batch too. It is also what the staging tile is rounded down to, and on a 4-lane backend the real batch unit is 8, so at the low end of the lane range a tile ran at under two thirds capacity and the hasher was called half again as often as it needed to be, each call paying its own setup. Deriving it from the backend's own interleave keeps every target correct without a second magic number, and the existing `HASH_GROUP` multiple assertion still holds. xmss 900 r1, PCS open 283 ms -> 279 ms, reproduced across two runs Also measured and reverted, none of them better here: the leaf fold's rows per task at 1024 rather than 4096, the zerocheck's hi-half cap at 9 rather than 7, and lincheck's NEON tile at 16 rather than 8. The first is slightly worse and the other two are a wash on this workload. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the ring-switch byte table its shape `fold_one_slot_ext` took the 24x256 table as a flat slice with a runtime length, so every one of its 24 lookups per output slot carried a bounds check and a multiply by the 24-byte element stride, and LLVM hoisted all 24 addresses ahead of the loads to do the checks, which forced a register shuffle it had no registers for. That is most of the instructions in a kernel that runs once per committed word. A `u8` cannot index a 256-entry row out of bounds and the row index is a constant of the unrolled loop, so typing the table as `[[F192; 256]; 24]` deletes all of it and folds the row stride into the address. xmss 900 r1 0.8290 s -> 0.8084 s (-2.5%, five of five rounds) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Swap the univariate-skip accumulators once, not once per odd position `π_b(i') = i' ⊕ 8b` is a chunk-index XOR by `b >> 1`, which is a free load offset, and for odd `b` a swap of each chunk's two 8-byte halves. That swap was applied to all eight registers at each of the four odd positions, which made `ext` the largest single share of this body's vector work, and the body is vector-ALU bound rather than load bound. The swap is an involution, it distributes over XOR, and it commutes with the chunk reindexing, so accumulating the odd positions plainly, swapping once, then adding the even positions gives the same `E ⊕ S(O)` with a quarter of the permutes. The register footprint is unchanged, so the body's handful of spills does not grow. `ODD` leaves the byte kernel, which now only reindexes chunks. blake2s_batch n_log=18, zerocheck -3% xmss 900 r1, Flock reduction 132.5 ms -> 129.7 ms xmss 900 r1 end to end: inside the noise, this stage being a seventh of it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the convert table its shape too The same flat-slice cost the ring-switch byte table had: two lookups per lane per medium position, each paying a bounds check, a branch and a multiply by the 24-byte element stride, and the branches making the body multi-block so the constant-trip loop around them never unrolled. A `u8` cannot index a 256-entry row out of bounds, so typing it removes all of that. xmss 900 r1, Flock reduction 130.3 ms -> 128.3 ms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * benchmarks --------- Co-authored-by: Tom Wambsgans <TomWambsgans@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

tcoratger and others added 4 commits August 16, 2025 19:17

instructions: update the precompiles

c83fef8

instruction: generate witness for multilinear eval

8aaf0a9

Merge branch 'main' into new-precompiles

eeab6a3

some fixes

60a5714

tcoratger merged commit 72ab579 into main Aug 17, 2025
3 checks passed

TomWambsgans deleted the new-precompiles branch August 29, 2025 23:10

Barnadrot mentioned this pull request May 11, 2026

zk-alloc: M2 Asahi aarch64 perf fixes (cherry-picked from zkam experiment) #220

Closed

6 tasks

Barnadrot mentioned this pull request May 20, 2026

fix(zk-alloc): realloc UB fix + flat-phase assert + aarch64 MAP_NORESERVE #227

Closed

Navigation Menu

Uh oh!

instruction: generate witness for multilinear eval - #12

instruction: generate witness for multilinear eval#12
tcoratger merged 4 commits into
mainfrom
new-precompiles

tcoratger commented Aug 17, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

tcoratger commented Aug 17, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant