[alex]

Part of #991.

Divstep.invert, the inversion modulo p = 2²⁵⁵ − 19 that vg_x25519, vg_x25519_base and Ed25519's key generation, signing and verification share on AArch64, now follows the structure of s2n-bignum's bignum_inv_p25519. It replaces the generic memory-resident InvCfg.inv that it used before; the short Weierstrass curves' inversion is untouched. invert_ok keeps its statement, so no caller changes.

There are no TCB or Spec changes. No contract or Rust API changes.

Benchmarks

The Benchmarks workflow compares this branch (7df2a50) with main (4e93b6c) on the x25519 and ed25519 modules. Below are three N2 runs (one run of each side) and the two clean Apple runs (the fastest of five).

Benchmark	N2 run 1	N2 run 2	N2 run 3	Apple run 3	Apple run 5
x25519/32	−1.6%	−1.7%	−1.8% (27.46 → 26.97 µs)	−0.1%	−2.2%
x25519_raw/32	−1.7%	−1.7%	−1.7%	−1.8%	−2.4%
x25519_public_key/32	−4.5%	−4.5%	−4.5%	−10.6%	−3.9%
x25519_generate/32	−4.5%	−4.5%	−4.5%	−7.6%	−4.9%
ed25519_keygen/32	−4.5%	−4.5%	−4.4%	−5.6%	−4.5%
ed25519_sign/64	−4.2%	−4.2%	−4.2%	−5.4%	−3.8%
ed25519_sign/1024	−3.7%	−3.7%	−3.7%	−4.9%	−1.8%
ed25519_sign/16384	−1.2%	−1.2%	−1.2%	−0.5%	−0.7%
ed25519_verify/64	−0.5%	0.0%	−0.1%	+0.5%	−2.1%
ed25519_verify/1024	−0.4%	0.0%	−0.2%	0.0%	+0.2%
ed25519_verify/16384	−0.4%	0.0%	−0.1%	−1.4%	+2.0%

Runs:

• N2: 39010141870, 39011399949 and 39011960834.
• Apple: 39011960834 (run 3) and 39013127743 (run 5).

Every inversion is about 0.44 µs faster on N2. On N2, x25519 is now 26.97 µs, against s2n-bignum's own 26.6 µs.

Which Apple runs count: x25519 and x25519_raw run the same ladder and inversion, so an Apple run counts only when the two agree within 3%.

• Runs 1, 2 and 4 failed that check. For example, run 4's base x25519 was 22.84 µs against x25519_raw's 25.70 µs.
• In runs 3 and 5 the two agree within 1.2%.
• Verification is mostly hashing and inverts only once. Its ±2% on Apple goes in opposite directions in the two runs and does not show on N2.

Impl

Impl/Ed25519/AArch64/Divstep.lean replaces the code in place.

• Batches: ten batches of 59 divsteps each, using the packed divsteps the short Weierstrass curves already use (Weierstrass.AArch64.pwords).
• Matrix: stored as magnitudes and sign masks (mat).
• Rows: four, each producing five words in a staging area, with the words of the multiplicand complemented for a negative entry and the magnitude added back, as s2n-bignum does.
• After the rows: f and g are shifted right by 59. u and v are reduced modulo p by q = ⌊W/2²⁵⁵⌋ − [W < 0], a fold of 19q.
• Start: u = 0 and v = 2⁻⁵⁹⁰ mod p, so that 2^(59i) f ≡ x 2⁵⁹⁰ u after i batches.
• End: u is folded once at bit 255. The result is u, or 2p − u when f < 0, chosen with an eor/and select rather than a branch.

All of it is in registers except the numbers f, g, u and v, the staging rows, and d. The batch counter is in x20 and the output pointer in x19: the taint analysis treats memory as secret, so a counter or pointer reloaded from memory would fail callers' taint_decide. To free x19, the matrix's second carry is computed into x11. The registers written are still within x19 :: clob 4 ++ [x2, x20], which invert_ok promises.

Proofs

Proof/Ed25519/AArch64/Inv/:

• Half, Row: a row: (W + 2²⁵⁶ (k_a + k_b)) mod 2³²⁰ = (c + X' a + Y' b) mod 2³²⁰ (row_ok).
• Mat: the matrix's magnitudes, masks and carries (mat_ok).
• Conn: the rows as integers, signed for f and g, unsigned for u and v.
• Out: the shift and the reduction (shift_ok, reduce_ok). Math.redV_cong shows the reduction is W mod p for W ≡ R (mod 2³²⁰) with |R| < 2³¹⁷.
• Step: the batches' invariant RInv and step_inv, mirroring x86-64's Proof/X25519/X86_64/Divstep/Sound.lean.
• Batch, Ends: the tail of a batch (outs_ok), and init_ok and finish_ok.

The two ends reduce with the same word lemmas as Freeze.lean (fold_top, add19_top), in this code's registers. Divstep.lean states the result as the class Sound, whose field is invert_ok itself. Its proof is in DivstepSound.lean, which only the registration files import, as before:

• batch_ok and the loop;
• after 590 divsteps, f = ±1 (divsteps_590, p prime);
• Fermat.

Keeping the proof behind the class keeps callers free of the algebra, and Divstep/Packed under check_lean_speed's 40-importer limit. Constant time is unchanged: the callers' taint_decide covers the new code.

Speed:

• The slowest new declarations are row_ok (3.0 s), batch_ok (2.3 s) and red_arith (2.2 s).
• red_arith calls omega_using with the facts each step needs; the whole-context omega took 11 s.
• Moduli above 2²⁵⁶ are written 2 ^ 256 * 2 ^ 64, so that unifying core's and Mathlib's Nat powers never evaluates 2³²⁰.

Checks

• Full lake build passes, and Emit.lean regenerated src/asm/aarch64/x25519.rs and ed25519.rs.
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt and cpu_tests.py lint pass, as does cargo fmt --check.
• Under qemu on AArch64, from the proven build: the x25519 and ed25519 unit tests, the RFC 7748 and RFC 8032 vectors, and Wycheproof's x25519 and ed25519 tests pass.
• ci/algorithms_table.py leaves the README unchanged: the docs don't describe the inversion.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw