[david415]

Prepares the Signature interface for ML-DSA, following what KEM.lean did for ML-KEM.

FIPS 204 signing rejects candidate signatures until one passes its norm checks, so a total signer can only try a bounded number of times, and the old law (verify (pub sk) m (sign sk m s).1 = true for every key and state) cannot hold for it. Now:

• sign : PrivateKey → ByteArray → EStateM SignError State Sig, with SignError.aborted, as encap/decap already return EStateM KEMError.
• verify_sign : ∀ sk m s σ s', sign sk m s = .ok σ s' → verify (pub sk) m σ = true: partial correctness, so an abort is reported instead of returning a signature that does not verify. No Reliable predicate is needed, because unlike a KEM's decryption failure, an abort is observable.
• sign_ok, the @[spec] Hoare triple, as generate_ok is for KEMs. The two EStateM triple lemmas move from KEM.lean to Cryptlib/Util/Triple.lean so both interfaces share them.
• Ed25519 never aborts: Ed25519Verify.nativeSignature_sign and Ed25519Blinded.signature_sign state sign sk m s = .ok (signNative sk m) s.
• Combiner (via EStateM versions of sliftL/sliftR, with sliftL_ok/sliftR_ok), Blindable.verify_blinded and the Check.lean examples follow.

make test (all suites pass), make axioms.