[alex]

Part of #991.

Stacked on #2635 (base claude/a64-comb-alt).

The AArch64 comb behind vg_ed25519_scalar_base and vg_x25519_base selected each digit's entry with NEON masks: per-magnitude masks in registers, copied into vector lanes, and each candidate inserted with BIT. Afterwards it negated the entry with a vector swap. This PR selects in general-purpose registers instead, as s2n-bignum's edwards25519_scalarmulbase_alt does.

• Every entry of the digit's table is loaded with ldp, at addresses from the static's address and the loop's public counter only.
• Each word is kept with csel where the digit's magnitude equals the entry's index, starting from the identity.
• 2dT is negated and Y - X / Y + X are exchanged under the sign, with csel, and the entry is stored once.

There is no early exit and no secret-indexed address; the artifacts' constant-time proofs (taint_decide) cover the new selection.

• Impl/Ed25519/AArch64/Comb.lean: combDigitS (the digit without masks), tblAddrS, scanInit, scanCand, scanNeg, scanSign, combEntry; combStep uses combEntry. The vector selection (magRegs, combMasks, combDigit, tblAddr, combNeg) is removed.
• Proof/Ed25519/AArch64/CombEntry.lean (new), combEntry_ok: slots 4–6 hold the selected entry, with the sign applied (Y - X and Y + X exchanged, 2dT negated). The rest of the workspace and the saved registers are kept.
• CombLoop.lean, CombDigit.lean, CombSelect.lean: the loop's invariant uses combEntry_ok; the proofs of the vector selection are removed (−578 lines), and the tables' lemmas (TblAt, combWord_eq) stay.
• src/asm/aarch64/{ed25519,x25519}.rs regenerated.

Not trust changes: nothing under TCB/ or Spec/.

Benchmarks

N2 (aarch64), three runs, base eb6885e (#2635's code)

Benchmark	39018538619¹	39018936660	39021027574
ed25519_keygen/32	8.39 → 7.98 µs (−4.8%)	8.39 → 7.99 (−4.8%)	8.39 → 7.99 (−4.8%)
ed25519_sign/64	8.91 → 8.51 (−4.5%)	8.91 → 8.51 (−4.5%)	8.92 → 8.52 (−4.5%)
ed25519_sign/1024	10.33 → 9.95 (−3.7%)	10.33 → 9.93 (−3.9%)	10.33 → 9.92 (−3.9%)
ed25519_sign/16384	32.88 → 32.53 (−1.1%)	32.87 → 32.55 (−1.0%)	32.87 → 32.53 (−1.0%)
ed25519_verify/64	−0.3%	−0.5%	−0.1%
ed25519_verify/1024	−0.4%	−0.6%	+0.1%
ed25519_verify/16384	−0.3%	−0.5%	0.0%
x25519/32	0.0%	0.0%	0.0%
x25519_generate/32	8.24 → 7.84 (−4.9%)	8.24 → 7.84 (−4.8%)	8.24 → 7.85 (−4.7%)
x25519_public_key/32	8.10 → 7.69 (−5.0%)	8.10 → 7.69 (−5.0%)	8.10 → 7.69 (−5.0%)
x25519_raw/32	0.0%	0.0%	0.0%

¹ At 82bae89, before the commit that removes the dead vector selection; the generated code (src/) is identical to this PR's.

Apple M1 (aarch64-apple)

Rule: a job counts only if every row this PR does not touch (x25519, x25519_raw and the three ed25519_verify rows) moved by at most ±3% base → head. Pass: at least two clean runs, no row's mean more than 3% slower, and no row more than 3% slower in every clean run. If two clean runs could not be had within about 3 hours, the evidence is N2 plus llvm-mca's M1 model. That is the case here: of six Apple runs, one is clean, and no further Apple runs were dispatched while the macOS runners were starving the repository's CI. An A/A run (identical code on both sides, run 39031471393) moved the control rows by up to 13% on macos-latest.

The clean run, 39018936660 (default configuration):

Benchmark	Base → head
ed25519_keygen/32	6.55 → 6.41 µs (−2.2%)
ed25519_sign/64	7.13 → 7.12 (−0.1%)
ed25519_sign/1024	8.34 → 8.39 (+0.7%)
ed25519_sign/16384	28.65 → 28.42 (−0.8%)
x25519_generate/32	6.95 → 6.97 (+0.3%)
x25519_public_key/32	6.28 → 6.30 (+0.3%)
controls: x25519 / x25519_raw	+2.3% / +1.5%
controls: ed25519_verify 64 / 1024 / 16384	+0.4 / +2.9 / +1.8%

llvm-mca on the comb loop as emitted (from 21: to cbnz x8, 21b in vg_ed25519_scalar_base, 64 iterations a call):

	apple-m1	neoverse-n2
#2635 (983 instructions a step)	376.4 cycles a step	247.2
this PR (1012 instructions a step)	362.4 (−3.7%)	222.2 (−10.1%)

All Apple runs, including those whose controls failed (default configuration, unless marked none for VG_CPU_FEATURES=none, which counts only for the X25519 rows because Ed25519 uses a SHA-512 variant there):

Run	Controls (x25519, x25519_raw, ed25519_verify 64/1024/16384)	Verdict
39018936660	+2.3, +1.5, +0.4/+2.9/+1.8	clean; none: x25519_raw −3.8, ed25519_verify/64 +23.6, rejected
39021027574	x25519 +18.1	rejected
39024857872	x25519 −7.1; none: ed25519_verify/1024 −3.4	rejected
39025932793	ed25519_verify/64 +3.2; none: x25519 +9.0	rejected
39028339309	x25519 +13.4; none: ed25519_verify/1024 −8.9	rejected
39031497110²	x25519_raw +6.9	rejected

² From the fastest of 8 fresh copies of each binary (claude/tmp-comb-sel-copies, this PR plus a measurement-only change to ci/bench_compare.py).

Checks

lake build, the emitter (with its audits) regenerating src/asm to exactly this PR's files, every ci/check_*.py, and the X25519 and Ed25519 Wycheproof tests (aarch64, under qemu) pass.

---

Generated by Claude Code