[alex]

Part of #4141 (finding 7 of the PPC64LE audit: DSA parameter generation). #4678 has merged, and this branch is restacked onto main (fbc66f8). It changes no Spec/ or TCB/ file and no Rust code outside the generated PPC64LE crate.

What was slow

Each probable-prime test (vg_dsa_probable_prime_{bits}) that gets past trial division sets up Montgomery arithmetic modulo the candidate with Search.montPrep. That computes R² mod c by 128·w modular doublings. #4678 removed the same cost from setupP.

What changed

montPrepFor bits (Impl/Dsa/PPC64LE/ProbablePrime.lean) is Search.montPrepHi when 64 (w − 1) < bits, and Search.montPrep otherwise. montPrepHi is montPrepWith Precompute.r2Hi: 64 + w doublings and six Montgomery squares.

• A candidate of bits bits is above 2^(bits−1), so under that condition its top word cannot be zero, which is what r2Hi needs.
• That holds for the 256-, 1024-, 2048- and 3072-bit tests. The 160-bit test keeps montPrep, because 160 bits use only part of its four words.
• The choice is made when the code is built, so the test has no new branch. vg_dsa_probable_prime_160 is unchanged.

Proofs:

• montPrepFor_ctx (Prime/Body.lean) gets r2Hi's precondition from the candidate's bit length (bitLength_iff_bounds, and the candidate is odd). It goes through prepWith_ctx, which is the old montPrep_ctx generalized over R2Ok r2c P.
• body_ct taints each of the two choices.
• prime_stack covers the stack depth of either choice.

Numbers

Benchmarks run 42521440680: POWER9, dsa_generate_parameters, base = #4678's head (c14404e), one run of each side, measured before the restack.

Benchmark	Base	Head	Change	OpenSSL	Head vs OpenSSL
dsa_generate_parameters/1024	139.55 ms	136.52 ms	2.2% faster	35.15 ms	3.9×
dsa_generate_parameters/2048	977.80 ms	953.67 ms	2.5% faster	397.40 ms	2.4×
dsa_generate_parameters/3072	6930.79 ms	6826.62 ms	1.5% faster	1702.78 ms	4.0×

That is about what the R² setup's share predicted (roughly 5% of parameter generation). The Miller–Rabin rounds, which belong to the bignum work, dominate the rest.

Checks

• After the restack: lake build of the whole project (on main's CI cache) passes, and the full emitter leaves the tree clean. The Static checks pass.
• check_lean_public_imports.py is OK on the edited modules.
• cargo check --target powerpc64le-unknown-linux-gnu --lib builds the crate. CI's ppc64le jobs run the tests.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHEf743DNZVAyToasZ6

[alex]

Closing this: a 1.5–2.5% gain on DSA parameter generation isn't worth a second Montgomery-setup path and its proofs to maintain. Most of the remaining time is in the Miller–Rabin rounds, which the bignum work will speed up for parameter generation too.

---

Generated by Claude Code