Skip to content

ML-DSA on x86-64: ExpandMask four polynomials at a time in signing (sign −5 to −11% instructions with AVX2) - #537

Merged
alex merged 80 commits into
mainfrom
claude/fervent-einstein-ukl7t7-em4
Oct 2, 2026
Merged

ML-DSA on x86-64: ExpandMask four polynomials at a time in signing (sign −5 to −11% instructions with AVX2)#537
alex merged 80 commits into
mainfrom
claude/fervent-einstein-ukl7t7-em4

Conversation

@alex

@alex alex commented Oct 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This implements vg_mldsa_expand_mask_poly4, whose spec and contract were reviewed in #508.

The branch also carries #544, which was reviewed and squash-merged into it: verification samples  as one run of kℓ entries, four at a time. That change is summarized in the last section below.

What

vg_mldsa_expand_mask_poly4 writes four polynomials of ExpandMask from four 66-byte seeds (Impl/MlDsa/X86_64/Sample/ExpandMask4.lean). There are two implementations:

  • _avx2. It runs the four SHAKE256 instances at once, one in each 64-bit element of the ymm registers. It uses vg_mldsa_rej_ntt_poly4_avx2's absorb and squeeze code at SHAKE256's rate: 17 lanes per block, with the 66-byte seed and padding in the first block. It squeezes five blocks of each instance, then unpacks each seed's output with vg_mldsa_expand_mask_poly's loop, for 18 or 20 bits per coefficient. It branches only on γ₁, which is public.
  • Baseline. It calls vg_mldsa_expand_mask_poly on each seed, saving its caller's callee-saved registers in scratch.

Both are proven against expandMask4Contract with 24 bytes of stack. They are a new function of the MlDsaArith backend.

Signing. The commitment now writes y[4g], …, y[4g + 3] with one call per group of four:

  • it copies ρ″ to the four seeds at MS4 (oMS4 = 1296), each followed by the two bytes of κ + 4g + k;
  • it calls vg_mldsa_expand_mask_poly4, with the rej4 working space as scratch;
  • it copies each y[r] to ŷ[r] and runs the NTT on it.

The last ℓ mod 4 polynomials are written one at a time, as before.

Proofs (untrusted)

  • Sample/M4Base, M4Absorb, M4Squeeze, M4Top: correctness of the AVX2 variant (absorbing, squeezing, unpacking).
  • M4CT: constant time. The taint analysis covers the absorbing and squeezing. For the branch on γ₁, both runs take the same side because their γ₁ agree (cmp_ok, sel_ct).
  • M4Scalar: correctness of the baseline (four calls).
  • M4Verified: Verified against the shared contract.
  • Sign/PhaseC: the seeds of a group (ms4_ok), the call (m4call_ok), the NTTs (yhR_ok), and commit_ok with both loops.
  • PhaseCCT: their leakage (mask4_tr).
  • PrimsB: mask4Call_ok/_tr.
  • ExpandMaskLoop's GPre.wr now asks only that each coefficient written lies in the writable regions, so a call can write a polynomial inside a larger region.

There are no TCB or Spec changes.

Performance

Instructions for 20 deterministic signatures (callgrind, AVX2; base is #536's head):

before after
ML-DSA-44 53.6M 47.6M −11.3%
ML-DSA-65 73.8M 68.0M −7.9%
ML-DSA-87 93.5M 88.6M −5.3%

The baseline changes by +0.1 to +0.2%. ML-DSA-65 and -87 gain less because ℓ = 5 and 7 leave one and three polynomials to the single-seed path. docs/algorithms/ml-dsa-*.toml and the README tables are updated.

Also included: #544 (verification's  as one run of entries)

Â[r, s] is entry e = ℓr + s, at polynomial 20 + e. Verification samples kℓ/4 groups of four (aGrp) and then the last kℓ mod 4 entries one at a time (aOne), so no group repeats an entry and none is cut short at the end of a row. Per verification with AVX2, ML-DSA-65 needs 7.9% fewer instructions and ML-DSA-87 8.1% fewer. The baseline ML-DSA-87 needs 9.3% fewer. Its proofs are in Verify/StageA, CTSample, StageC, Correct, CTCompute and Instrs, with no TCB or Spec changes.

Checks run

  • lake build and the emitter
  • check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, algorithms_table
  • cargo fmt --check and cargo clippy --all-targets -D warnings
  • cargo test --release with Wycheproof, both on the default path and with VG_CPU_FEATURES=none --features cpu-features-env

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

Generated by Claude Code

claude added 30 commits October 1, 2026 13:33
@claude
ML-DSA on x86-64: NTT and NTT⁻¹ in SSE2
c8a8986 
vg_mldsa_ntt and vg_mldsa_inv_ntt now compute on four coefficients at a
time in SSE2 registers, as ML-KEM's x86-64 NTT does: a Montgomery
multiplication with pmuludq (the even doublewords, then the odd ones moved
down by pshufd), conditional additions of q with psrad masks, and for the
layers with len 2 and 1 the coefficients of two or four blocks gathered with
punpck{l,h}qdq (and pshufd) and interleaved back. The zetas are a table in
Montgomery form that the prologue stores in scratch; the multiplications run
inside ML-KEM's withMxcsr, so Intel's MCDT mitigation holds.

Proofs: the lanes' arithmetic (VArith), the butterflies on registers
(VLanes), the loads and stores of four coefficients and the zetas (VMem),
the layers (VLay, VLay21), and the functions (Ntt, NttInv). Signing and
verification now check that their code loads MXCSR only to restore it
(ctlOk, through a compositional ctlC for verification) rather than never,
since their primitives now do.

ML-DSA-65 on this machine: sign 1.53 ms -> 0.81 ms, verify 281 us ->
181 us, keygen 276 us -> 248 us.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge remote-tracking branch 'origin/main' into pr1-merge
e49e9bb
@claude
ML-DSA on x86-64: polynomial arithmetic in SSE2
ae7eb79 
vg_mldsa_multiply_ntt, vg_mldsa_multiply_add_ntt, vg_mldsa_add and
vg_mldsa_sub now compute on four coefficients at a time in SSE2 registers,
with the vector helpers of the NTT (Vec.lean).

The products are two Montgomery multiplications: f·g·2⁻³², then by
2⁶⁴ mod q, which is f·g in [0, 2q), reduced with vcsub (for
multiply_add, h is then added and the sum reduced). They use pmuludq, so
they run inside ML-KEM's withMxcsr. These functions have no working space
and use no stack, so MXCSR goes through the last 8 bytes of h, addressed
through r8 = h. The last four coefficients of h are loaded into xmm6
first. The loop stores the first 252 coefficients. The last four are
computed from registers before MXCSR is loaded back, and stored after it.
Their callers' proofs are unchanged: the functions still need no stack
and never write rsp.

add and sub use paddd/psubd and vcsub/vcadd.

Proofs: the lanes of a product (mul_lane, mulAdd_lane), the loop
(Mul.step, Mul.loop_ok), the last block (Mul.last), the function
(Mul.fn_ok), and withMxcsr through the end of a polynomial
(withMxcsrH_ok). AddSub is reproven the same way.

ML-DSA-65 instructions executed (callgrind, PR #464 -> this): sign
-19%, verify -11%, keygen -2%.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge remote-tracking branch 'origin/claude/fervent-einstein-ukl7t7' …
04e1ac6 
…into claude/fervent-einstein-ukl7t7-mul
@claude
ML-DSA on x86-64: key generation, signing and verification generic ov…
6703c7a 
…er the arithmetic

Key generation, signing and verification on x86-64 now call the
polynomial arithmetic of an implementation given as a variant of the new
interface MlDsaArith (Variants/MlDsaArith/X86_64/). They are registered
in Generic/MlDsaArith/X86_64/ and emitted once for each implementation,
so a faster arithmetic (e.g. AVX2) reaches them without editing them. The
only variant is the existing SSE2 code (Sse2), and the generated code is
unchanged.

- Impl: Arith.Backend holds the six functions' code and a name suffix.
  Each Prims gets a sfx field, and the arithmetic calls are named
  "vg_mldsa_ntt" ++ sfx and so on. primsWith B swaps in B's arithmetic.
- Proof: ArithImpl is a backend with FnOk for each function: verified
  without stack, no rsp writes, depth <= 2, ctlOk, spSafe. prims_okWith
  builds each caller's PrimsOk from it.
- ctlOk and spSafe of signing and key generation are no longer evaluated
  on the whole code with a concrete backend. Same/same_tac
  (Proof/MlDsa/X86_64/Arith/Same.lean) shows that a check composing over
  the code's structure (ctlC, Code.allInstrs) gives the same result as
  on the code with every arithmetic function empty, which the kernel
  evaluates once per parameter set. Verification already did this by
  hand; its call lemmas now allow the names to differ.
- The registration files Artifacts/MlDsa{KeyGen,Sign,Verify}/X86_64.lean
  move to Generic/MlDsaArith/X86_64/.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge origin/main into claude/fervent-einstein-ukl7t7-mul
3e2aa65 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge claude/fervent-einstein-ukl7t7-mul (with origin/main) into clau…
55761ef 
…de/fervent-einstein-ukl7t7-generic

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: polynomial arithmetic in AVX2
791054f 
Add an AVX2 variant of MlDsaArith on x86-64: vg_mldsa_ntt_avx2,
vg_mldsa_inv_ntt_avx2, vg_mldsa_multiply_ntt_avx2,
vg_mldsa_multiply_add_ntt_avx2, vg_mldsa_add_avx2 and vg_mldsa_sub_avx2
compute on eight coefficients at a time, four in each 128-bit lane of an
AVX2 register. In each lane the VEX.256 form of the SSE2 code does what the
SSE2 code does to an xmm register, so the proofs lift the SSE2 lemmas to
each lane (ML-KEM's ylanes). The NTT layers with len >= 8 load eight
coefficients of each half of a block; len = 4 regroups two blocks with
vperm2i128; len = 2 and 1 run the SSE2 gatherings in each lane, with the
zetas of each lane arranged by vpshufd/vpblendd or vpermq.

Key generation, signing and verification are generic over MlDsaArith, so
the emitter generates their _avx2 instances; the Rust API selects them on
CPUs with AVX and AVX2 (mldsa_common::Backend).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Spec: ML-DSA's RejNTTPoly four times (vg_mldsa_rej_ntt_poly4)
b818911 
The contract of a function that samples four elements of the matrix A at
once, as ML-KEM's vg_mlkem_sample_ntt4 does: for each of the four 34-byte
seeds, RejNTTPoly (FIPS 204 Algorithm 30) of it, reduced, or 0 if the loop
does not finish within Appendix C's least bound for one of them. Its
scratch is that of vg_mldsa_rej_ntt_poly (256 u64s), so callers can pass
the same working space. No implementation yet: an x86-64 one, with four
SHAKE128 instances in AVX2 registers, follows in its own PR.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Spec: give vg_mldsa_rej_ntt_poly4 8 KiB of scratch
779ca16 
Four interleaved Keccak states, the second buffer of the 4-way permutation
and its table of round constants already take 2368 bytes, before the
squeezed output; ML-KEM's vg_mlkem_sample_ntt4 has 1024 u64s for the same.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
CI: test ML-DSA on the CPUs of the x86-64 feature matrix
e365dde 
ML-DSA now chooses between its SSE2 and AVX2 polynomial arithmetic by CPU
feature, so test it end to end where the choice differs: under SDE's
Pentium 4 (the SSE2 code, and the line that chooses it) and Haswell.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-rej4spec' into claude/fe…
e04e23b 
…rvent-einstein-ukl7t7-rej4
@claude
ML-DSA on x86-64: sample  four entries at a time in verification
be2f80c 
vg_mldsa_rej_ntt_poly4 runs RejNTTPoly on four seeds. Its AVX2 variant
runs the four SHAKE128 instances at once in the 64-bit elements of ymm
registers, with the absorb and squeeze code of vg_mlkem_sample_ntt4_avx2,
and runs vg_mldsa_rej_ntt_poly's loop over the same 1008 bytes of each
seed's output (squeezed in two rounds of three blocks). The baseline calls
vg_mldsa_rej_ntt_poly on each seed. Both are proven against
rejNTT4Contract with 24 bytes of stack, and are a new function of the
MlDsaArith backend.

Verification now samples each row of  four entries at a time from SB4
(four copies of ρ with the row's indices): the entries from 0, then for
ℓ = 7 the last four (sampling entry 3 again), or for ℓ = 5 the last one
alone. Its rej4 working space is the 8 KiB after the last row of Â, which
the scratch size already allows. Its stack grows from 24 to 32 bytes, as
its baseline callee calls three deep.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: sample  four entries at a time in key generation
9a8bde9 
Key generation calls vg_mldsa_rej_ntt_poly4 (four SHAKE128 instances at
once with AVX2, four calls of vg_mldsa_rej_ntt_poly without) for each
group of four consecutive entries of Â, from four seeds at oSA4 that each
hold ρ and the indices of their entry, with its 8 KiB of working space
after the polynomials; the last kℓ mod 4 entries are sampled one at a
time as before. Each call's result is ANDed into r15 and masks the four
polynomials it sampled, as for one entry.

Its calls now use 24 bytes of stack, within the 32 its contract already
allows. Instructions per key generation (callgrind, AVX2): ML-DSA-44
23.5M → 16.8M (−29%), ML-DSA-65 38.4M → 26.7M (−31%), ML-DSA-87
64.4M → 40.8M (−37%); the baseline is unchanged (+0.06%).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: sample  four entries at a time in signing
f8a40e9 
Signing copies ρ to four seeds at RS4 and, for each group of four
consecutive entries of Â, sets their indices and calls
vg_mldsa_rej_ntt_poly4 (four SHAKE128 instances at once with AVX2), with
8 KiB of working space after the polynomials, ANDing its result into r15;
the last kℓ mod 4 entries are sampled one at a time as before.

Signing branches on r15, so the proofs need, as of
vg_mldsa_rej_ntt_poly, that the result depends only on the seeds and
that it is 1 only if RejNTTPoly finishes within maxBounds: both
implementations return whether each seed has 256 coefficients in 1008
bytes of output (Rej4Ok.ret, from their proofs' contract r4K).

Its calls now use 32 bytes of stack (24 for vg_mldsa_rej_ntt_poly4 and
the return address), as key generation's and verification's.
Instructions for 20 deterministic signatures (callgrind, AVX2):
ML-DSA-44 60.4M → 53.6M (−11%), ML-DSA-65 85.6M → 73.8M (−14%),
ML-DSA-87 117.1M → 93.5M (−20%); the baseline is unchanged (+0.02%).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Spec: ML-DSA's ExpandMask four polynomials at a time (vg_mldsa_expand…
c125d98 
…_mask_poly4)

vg_mldsa_expand_mask_poly4(seeds, gamma1, a, scratch) writes the four
polynomials of ExpandMask of the four 66-byte seeds at seeds (seed66) to
the four polynomials from a (poly4): for each, what expandMaskContract
says. The four are independent, so an implementation may run four
SHAKE256 instances at once, as vg_mldsa_rej_ntt_poly4 does SHAKE128.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: HighBits and LowBits with AVX2
856f4bb 
vg_mldsa_high_bits_avx2 and vg_mldsa_low_bits_avx2 compute on eight
coefficients at a time: in each 128-bit lane, the VEX.256 form of SSE2
code on four doublewords (hbX, lbX). Decompose is the reference
implementation's, in 32 bits, with the multiplications by M and by 2γ₂
sums of shifts (no multiplication instructions, so nothing MCDT
affects), r₁ = f mod m as f ANDed with the sign of f - m, and r₀ plus q
if negative. They branch once on the public γ₂.

They join the polynomial arithmetic's backend, as variants of
vg_mldsa_high_bits and vg_mldsa_low_bits, so signing with AVX2 calls
them. The proofs: what the SSE2 code computes in a doubleword is r₁ and
r₀ of Decompose (YLane), each lane does it (YBlock, ylanes), and the loop
stores all 256 (YBits).

Instructions for 20 deterministic signatures (callgrind, AVX2):
ML-DSA-44 60.7M → 58.2M (−4.1%), ML-DSA-65 86.2M → 82.2M (−4.6%),
ML-DSA-87 118.3M → 113.8M (−3.8%); the baseline is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: the norm check and MakeHint with AVX2
49840a5 
vg_mldsa_norm_lt_avx2 and vg_mldsa_make_hint_avx2 compute on eight
coefficients at a time, in the VEX.256 form of SSE2 code on the four
doublewords of each 128-bit lane, as HighBits and LowBits do.

norm_lt clamps the public bound to q (which changes no result), so that
a - b and (q - b) - a fit in 32 bits and one of them is negative exactly
when a coefficient is out of bounds; it ANDs their ORs into an
accumulator, spreads its sign bits and returns (vpmovmskb + 1) >> 32.
There is no branch on data.

make_hint computes r₁ of r and of (r + z) mod q with hbX, the hint as
(r₁ ^ r₁' + 63) >> 6, and counts the eight hints of an iteration from
the byte mask of the hints shifted to bit 7 (vpmovmskb), summing its
nibbles with three shifts and additions.

Both join the polynomial arithmetic's backend, as variants of
vg_mldsa_norm_lt and vg_mldsa_make_hint, so signing (both) and
verification (norm_lt) with AVX2 call them. The proofs: YNorm (the
differences, the mask and the result) and YHint (the hint in a
doubleword, the count, the loop, and the count is hintOnes).

Instructions (callgrind, AVX2), 20 deterministic signatures:
ML-DSA-44 58.2M → 53.5M (−8.0%), ML-DSA-65 82.2M → 75.5M (−8.2%),
ML-DSA-87 113.8M → 106.1M (−6.8%); 20 verifications: 23.5M → 23.0M
(−2.0%), 35.7M → 35.4M (−0.8%), 72.0M → 70.2M (−2.4%). The baseline is
unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: copy 8 bytes at a time in signing
b33f8a0 
Signing's copies (y to ŷ, 1024 bytes in every iteration, and the
32-byte seed and c̃) moved one byte per iteration: 6 instructions a byte,
about 8% of the instructions of a signature with AVX2. All of them are
of a multiple of 8 bytes, so `copy` now moves a quadword per iteration,
and `copyChk` checks that the length is one.

copy_ok and copy_tr are the byte copy's proofs with the quadword
loop: each iteration writes the 8 bytes it read (copy_byte, by
writeW_byte and byte_readW).

Instructions for 20 deterministic signatures (callgrind):
AVX2: ML-DSA-44 53.5M → 49.7M (−7.2%), ML-DSA-65 75.5M → 70.4M (−6.7%),
ML-DSA-87 106.1M → 100.2M (−5.6%); baseline ISA: 78.3M → 74.5M (−5.0%),
110.9M → 105.8M (−4.6%), 148.9M → 143.0M (−4.0%).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: UseHint with AVX2
309a7dd 
vg_mldsa_use_hint_avx2 computes UseHint on eight coefficients at a time,
in the VEX.256 form of SSE2 code on the four doublewords of each 128-bit
lane (uhX), as the other AVX2 rounding functions do: f of r (hfX, the
part of hbX before the reduction modulo m), the sign P of f · 2γ₂ - r
(set exactly when r₀ > 0), and the sign H of h | -h (set exactly when
the hint is not 0); then δ = ¬(P + P) ∧ H (pandn) is 1, -1 or 0, and
the result is (f + δ + m) mod m, by two conditional subtractions of m,
as vg_mldsa_use_hint computes it. There is no branch on data.

It joins the polynomial arithmetic's backend as a variant of
vg_mldsa_use_hint, which verification with AVX2 calls. The proofs
(YUse): the value in a doubleword is uhS's (uhL_toNat), and the loop
stores all 256.

Instructions for one key generation, one signature and 20
verifications (callgrind, AVX2): ML-DSA-44 22.8M → 22.2M (−2.4%),
ML-DSA-65 35.3M → 34.5M (−2.5%), ML-DSA-87 69.1M → 67.9M (−1.7%); the
baseline is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-em4spec' into claude/fer…
0c99395 
…vent-einstein-ukl7t7-em4
@claude
Merge main into claude/fervent-einstein-ukl7t7-avx2
4563920 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
ML-DSA on x86-64: ExpandMask four polynomials at a time in signing
fca09e7 
vg_mldsa_expand_mask_poly4 writes four polynomials of ExpandMask from four
66-byte seeds. Its AVX2 variant runs the four SHAKE256 instances at once
in the 64-bit elements of ymm registers (the absorb and squeeze code of
vg_mldsa_rej_ntt_poly4_avx2, at SHAKE256's rate), squeezes five blocks of
each, and unpacks each seed's output with vg_mldsa_expand_mask_poly's
loop. The baseline calls vg_mldsa_expand_mask_poly on each seed. Both are
proven against expandMask4Contract with 24 bytes of stack, and are a new
function of the MlDsaArith backend.

Signing's commitment now writes y[4g], ..., y[4g + 3] with one call for
each group of four: it copies ρ″ to four seeds at MS4 with κ + 4g + k,
calls vg_mldsa_expand_mask_poly4 with the rej4 working space, and then
copies each y[r] to ŷ[r] and runs the NTT on it; the last ℓ mod 4 are
written one at a time as before.

Instructions for 20 deterministic signatures (callgrind, AVX2):
ML-DSA-44 53.6M → 47.6M (−11.3%), ML-DSA-65 73.8M → 68.0M (−7.9%),
ML-DSA-87 93.5M → 88.6M (−5.3%); the baseline changes by +0.1 to +0.2%.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-avx2' into claude/ferven…
11c34b1 
…t-einstein-ukl7t7-ybits2

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-ybits2' into claude/ferv…
2d4b324 
…ent-einstein-ukl7t7-ynorm

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-ynorm' into claude/ferve…
ba3af81 
…nt-einstein-ukl7t7-copy8

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-copy8' into claude/ferve…
5bd087c 
…nt-einstein-ukl7t7-yuse

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-avx2' into claude/ferven…
8160f69 
…t-einstein-ukl7t7-rej4

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-rej4' into claude/ferven…
2c38b92 
…t-einstein-ukl7t7-rej4kg

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-rej4kg' into claude/ferv…
1c58e17 
…ent-einstein-ukl7t7-rej4sg

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
claude added 3 commits October 2, 2026 03:59
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-rej4sg' into claude/ferv…
b1d1773 
…ent-einstein-ukl7t7-em4

The Backend has highBits, lowBits, normLt, makeHint, rej4 and expandMask4,
and sign_same takes all of them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge main into claude/fervent-einstein-ukl7t7-yuse
d2b4c83 
Main has #513, #519 and #523, which this branch already has.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge main into claude/fervent-einstein-ukl7t7-rej4sg
80ac2dc 
Regenerates the ML-DSA asm, which conflicted with the 8-byte copy.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
Base automatically changed from claude/fervent-einstein-ukl7t7-rej4sg to main October 2, 2026 04:36
claude added 3 commits October 2, 2026 04:38
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-rej4sg' into claude/ferv…
ef29a45 
…ent-einstein-ukl7t7-em4

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge main into claude/fervent-einstein-ukl7t7-yuse
1b8b07f 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge main into claude/fervent-einstein-ukl7t7-em4
533acff 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@alex
alex enabled auto-merge October 2, 2026 04:57
@alex
alex added this pull request to the merge queue Oct 2, 2026
claude added 2 commits October 2, 2026 05:16
@claude
Merge main into claude/fervent-einstein-ukl7t7-yuse
6c0278c 
Takes main's shorter optimized notes, whose "rounding" covers UseHint.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge main into claude/fervent-einstein-ukl7t7-em4
6aead95 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Oct 2, 2026
@claude
Merge main into claude/fervent-einstein-ukl7t7-em4
01dd40c 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@reaperhulk
reaperhulk added this pull request to the merge queue Oct 2, 2026
@reaperhulk
reaperhulk removed this pull request from the merge queue due to a manual request Oct 2, 2026
@alex @claude
ML-DSA on x86-64: sample verification's  as one run of entries (#544)
551c0ef 
Verification kept Â[r, s] at polynomial 20 + 8r + s, so a group of four
entries of vg_mldsa_rej_ntt_poly4 could not cross a row: for ℓ = 7 the
second group of each row sampled entry 3 again, and for ℓ = 5 the last
entry of each row was sampled alone. Â[r, s] is now entry e = ℓr + s at
polynomial 20 + e, and verification samples the kℓ entries as key
generation and signing do: kℓ/4 groups of four (each seed's indices are
e mod ℓ and e / ℓ), then the last kℓ mod 4 one at a time. ML-DSA-87
(56 entries) has no duplicate, and ML-DSA-65 makes 7 four-way calls and
2 single ones instead of 6 and 6.

The proofs of the samplers (StageA, CTSample) now count sampled entries
by their number, Done ℓ e r' c' := ℓr' + c' < e; the rest only pass ℓ
to pA. The working space of vg_mldsa_rej_ntt_poly4 stays at polynomial
20 + 8k, after  for every ℓ.

Instructions per verification (callgrind, 20 verifications less key
generation and one signature): AVX2 ML-DSA-65 1.061M → 0.977M (−7.9%),
ML-DSA-87 1.677M → 1.540M (−8.1%); baseline ML-DSA-87 3.276M → 2.971M
(−9.3%, undoing the duplicate's cost); ML-DSA-44 and the ML-DSA-65
baseline are unchanged.


Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

Co-authored-by: Claude <noreply@anthropic.com>
@reaperhulk
reaperhulk enabled auto-merge October 2, 2026 10:22
claude added 2 commits October 2, 2026 10:36
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-yuse' into claude/ferven…
f837e06 
…t-einstein-ukl7t7-em4

Takes both new MlDsaArith backend functions: useHint and expandMask4.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@claude
Merge branch 'claude/fervent-einstein-ukl7t7-em4' (with #544) into th…
1abf1d5 
…e merge of #526

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@reaperhulk
reaperhulk added this pull request to the merge queue Oct 2, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Oct 2, 2026
@claude
Merge main into claude/fervent-einstein-ukl7t7-em4
9a9b508 
Keeps both new MlDsaArith backend functions: useHint (#526) and expandMask4.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@alex
alex enabled auto-merge October 2, 2026 12:07
@claude
Merge main into claude/fervent-einstein-ukl7t7-em4
9fedec4 
#576's sign_message and verify_message proofs list signing's backend
functions and verification's sampling steps: SignFn now passes
expandMask4 to sign_same, and VerifyFn follows the entries of  sampled
as one run (aGrp, then aOne).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr
@alex
alex added this pull request to the merge queue Oct 2, 2026
Merged via the queue into main with commit 8c99952 Oct 2, 2026
49 checks passed
@alex
alex deleted the claude/fervent-einstein-ukl7t7-em4 branch October 2, 2026 13:10
alex pushed a commit that referenced this pull request Oct 2, 2026
@claude
Merge origin/main
d5b3432 
#583 is now on main; this branch already carries it and builds on it, so
its side is kept in every file both changed. The merge adds only #537.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn
@alex alex mentioned this pull request Oct 2, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@alex @claude