[david415]

ML-DSA-65 (FIPS 204) as a Signature, stacked on #54 (signatures that can abort).

Construction (Cryptlib/Primitives/Sign/MLDSA/)

• Sampling.lean: VCVio's Extern/MLDSA/Sampling.lean (Apache-2.0, attributed) with the native SHAKE bindings replaced by VCVio's pure-Lean Keccak, the same swap ML-KEM's primitives make. The sampler bounds (sampleInBall_norm, sampleInBall_l1Norm, expandS_bound, expandMask_get_cInfNorm_le) carry over unchanged, since they hold for any stream.
• MLDSA.lean: prims p, VCVio's concrete rounding, NTT and encodings with those samplers, and scheme p hp : Signature; mldsa65Signature is ML-DSA-65.

Correctness: FIPS204.correct: for keys from any seed, a signature the signing loop returns verifies. It instantiates VCVio's fipsSign_fipsVerify_correct' with

• VCVio's concrete rounding laws (useHint_makeHint, hide_low);
• wApprox_eq, re-proved from only t = A·s₁ + s₂, Power2Round and the NTT laws. VCVio's version takes the whole Primitives.Laws, including the random-oracle field keyVector_t0_determined, which no concrete instance can satisfy;
• cs2_bound, from SampleInBall's ℓ₁ count and ExpandS's range.

It depends on propext, Classical.choice and Quot.sound only, pinned in Sign/Check.lean.

As a Signature

• The private key is the 32-byte seed ξ, so every private key is honestly generated.
• Signing is external-mode with an empty context (M' = 0 ‖ 0 ‖ M), hedged with 32 bytes per signature from the signing state.
• Public keys and signatures are their FIPS 204 byte encodings (1952 and 3309 bytes).
• sign aborts after 1000 rejected attempts (ML-DSA-65 needs about five on average), or if the key or signature encoding would not decode back to itself. That check is run, not proved: VCVio has no encoding round-trip lemmas. With it, verify_sign follows from correct. Proving the round trips would let the check go.

Tests: mldsa_test against NIST ACVP-Server vectors for ML-DSA-65, extracted by scripts/extract_acvp_mldsa.py with .sha256 sidecars:

• 25 key generations;
• 90 signatures (deterministic and hedged, through the external interface, the internal one, and with μ given);
• 30 verifications, including the "modified signature" rejections.

All pass. So do sign/verify round trips through mldsa65Signature, which reject another message and a changed signature; signing takes about 90 ms. HashML-DSA (pre-hash) is not implemented. Added to make test, make test-mldsa and CI.

make test (all suites), make axioms.