[alex]

Part of #991.

What

AArch64 Montgomery products of 4-word moduli (mulR, Impl/Mont/AArch64.lean) no longer clear the accumulator words that their first row writes anyway.

• The first row, rowInit, writes words 0 to n - 1 by mul. The setup now clears only the top two words (accClear), not all six: 4 fewer movz per multiplication.
• Curves it reaches: mulR is shared, so this reaches P-192, P-224, P-256, secp256k1 and brainpoolP256r1 alike. In all, 1832 movz go from the generated code.
• Three loads become moves: in three places, a load of the multiplier becomes orr x1, x8, x8, because x8 is no longer cleared and the existing forwarding pass can reuse it.

rowInit now takes the register its chain reads through as a parameter; mulR passes x0, so its code is otherwise unchanged.

No TCB/ or Spec/ changes.

Proof

• RowInit.lean: mulsLo_ok and rowInit_ok need only the words past the multiplicand's cleared, i.e. the top one. rowInit_ok takes any Ptr register.
• Round.lean:
  • accV, the accumulator's value entering round i (zero entering the first);
  • AccInit, what the first round needs: the top two words cleared, and all of them unless the first row is rowInit.
  • prodRow_ok and round_ok are stated with them.
• Rounds.lean: rounds_ok's invariant uses accV from AccInit.
• Ops.lean: setup_ok proves AccInit (wins_zero_lt, accClear_sub). mulR_okW and the P-256 verifier's mul_ok (VerifySparse/Ops.lean) read accV at n > 0 as the window's value.

Performance

Benchmarks run 39103992124: aarch64, cpu_features='-', against main (e3794cde7), with modules=ecdh_p256 ecdsa_p256 ec_p256 ecdh_p384 ecdsa_p384 ec_p384 ecdh_secp256k1 (secp256k1 as a canary for the other 4-word curves). The other 4-word curves (P-192, P-224, brainpoolP256r1) share mulR and were not benchmarked.

Benchmark	main	this PR	Change
ec_p256_public_key/65	11.46 µs	11.42 µs	0.3% faster
ecdh_p256/32	45.43 µs	45.45 µs	0.0%
ecdh_secp256k1/32	217.02 µs	215.57 µs	0.7% faster
ecdsa_p256_sha256_sign/64	14.16 µs	14.11 µs	0.3% faster
ecdsa_p256_sha256_sign/1024	14.61 µs	14.56 µs	0.3% faster
ecdsa_p256_sha256_sign/16384	21.75 µs	21.68 µs	0.3% faster
ecdsa_p256_sha256_verify/64	46.31 µs	46.25 µs	0.1% faster
ecdsa_p256_sha256_verify/1024	46.86 µs	46.80 µs	0.1% faster
ecdsa_p256_sha256_verify/16384	53.93 µs	53.84 µs	0.2% faster
ecdsa_p256_sha384_sign/64	15.90 µs	15.84 µs	0.4% faster
ecdsa_p256_sha384_sign/1024	16.65 µs	16.59 µs	0.3% faster
ecdsa_p256_sha384_sign/16384	27.89 µs	27.82 µs	0.2% faster
ecdsa_p256_sha384_verify/64	46.59 µs	46.52 µs	0.1% faster
ecdsa_p256_sha384_verify/1024	47.49 µs	47.47 µs	0.1% faster
ecdsa_p256_sha384_verify/16384	58.60 µs	58.50 µs	0.2% faster

The cleared registers' movz (zero idioms) are nearly free on Neoverse N2, hence the small change.

P-384, measured and dropped. That run's head also gave P-384's product and square the same first row (rowInit straight into the words, then the chain of high words), dropping 6 movz and 6 adds per product and 5 of each per square. It was slower on N2:

• ecdh_p384/48: 189.42 → 191.54 µs (1.1% slower);
• ecdsa_p384_sha384_sign/16384: 63.08 → 63.95 µs (1.4% slower).

The interleaved mul/adds row, as in s2n-bignum's _alt, schedules better there. So this PR leaves P-384 as it is: src/asm/aarch64/p384_mont.rs is byte-identical to main's, and its rows above don't apply.

Tests

• lake build, Emit.lean --check and the ci/check_*.py scripts pass.
• Wycheproof for P-192, P-224, P-256, P-384, secp256k1 and brainpoolP256r1 passes under qemu (cargo test --release --target aarch64-unknown-linux-gnu), both by default and with VG_CPU_FEATURES=none.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw