[reaperhulk]

This is the P-384 counterpart of #3741 (P-256). It is independent of that PR, and both branch from main.

On ARMv7, P-384 signing, public-key derivation and verification's [u]G multiplied the generator with vg_p384_mul, a double-and-add ladder over all 384 bits. On main, signing took 7.97 ms (OpenSSL: 2.76 ms; aws-lc-rs: 638 µs) and key derivation took 7.57 ms (OpenSSL: 2.60 ms) (run).

This PR switches them to the fixed-base comb secp256k1 uses on ARMv7 (Impl/Weierstrass/Arm/TComb.lean), with P-384's verified seven-bit tables (Impl/P384/CombTable7.lean). The comb does 55 complete Renes–Costello–Batina additions, and each one takes its entry from a masked scan of all 64 entries in a public row of the 337,920-byte table VG_P384_COMB. Verification's [v]Q is still a call of vg_p384_mul.

As for P-256, verification copies u as words into K's slot for vg_p384_mul. So its generator (verifyGeneratorP384) first expands that slot into the table of bits the comb reads.

Proofs

These mirror #3741's, in P-384's sub-namespaces:

• Proof/P384/Arm/Comb.lean: layout, Config and the satisfiable memory.
• Proof/Ecdsa/Arm/P384/CombGenerator.lean: the generator lemmas.
• Proof/{Ecdsa,EcKey,Ecdsa/Verify}/Arm/P384/Comb.lean: each function's contract with its table, constant time and Verified.
• Proof/Ecdsa/Rfc6979/Arm/P384Sha384Comb.lean: the RFC 6979 signer.
• Proof/Ecdsa/Arm/P384/Verified.lean gains wf₀_pre and agree₀. sign_ct keeps its statement.

The comb's Config and the generator lemmas unify terms containing 2^384, which is above Lean's default exponentiation threshold. They raise it to 512, as other P-384 proofs do (e.g. Proof/Weierstrass/AArch64/MontFn384.lean).

There are no changes to TCB/ or Spec/. The only Rust changes are the regenerated src/asm/arm/{ec_p384,ecdsa_p384}.rs and the new src/asm/arm/consts/vg_p384_comb.rs.

P-224 and P-521 cannot follow yet. P-224's 37-row table covers 256-bit scalars, but its ladder covers 224 bits, so the comb's startBits condition fails. P-521 has nine words, and the comb's Layout allows at most six. Each would need a new table or a wider layout.

Speed

Benchmarks run on ARMv7, comparing against main (run):

Benchmark	Base	Head	Change
ec_p384_public_key/97	7.56 ms	941.43 µs	87.6% faster
ecdh_p384/48	7.57 ms	7.57 ms	0.1%
ecdsa_p384_sha384_sign/64	7.96 ms	1.34 ms	83.2% faster
ecdsa_p384_sha384_sign/16384	8.05 ms	1.42 ms	82.3% faster
ecdsa_p384_sha384_verify/64	15.15 ms	8.51 ms	43.8% faster

Checks run locally

• Full lake build and Emit.lean --check.
• check_lean_imports, check_lean_modules, check_lean_single_importer, check_lean_public_imports (on the changed modules), check_registrations, check_lean_speed, check_variants, check_arch_gates and check_vectors; cargo fmt --check; and cargo clippy --target armv7-unknown-linux-gnueabihf --all-targets -D warnings.
• cargo test --target armv7-unknown-linux-gnueabihf -- p384 under qemu-arm with Wycheproof: 18 tests pass, including RFC 6979 P-384 (keys, public key, SHA-384 signing, verify), CAVP ECDH, Wycheproof ECDSA and ECDH P-384, and compressed points.

---

Generated by Claude Code