ML-DSA on x86-64: key generation, signing and verification generic over the polynomial arithmetic

README.md

@@ -827,7 +827,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>✅ SSE2 NTT</td>
+<td>✅ SSE2 polynomial arithmetic</td>
 
 <td>✅ SHA extensions</td>
 
@@ -843,7 +843,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>✅ SSE2 NTT</td>
+<td>✅ SSE2 polynomial arithmetic</td>
 
 <td>✅ SHA extensions</td>
 
@@ -859,7 +859,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>✅ SSE2 NTT</td>
+<td>✅ SSE2 polynomial arithmetic</td>
 
 <td>✅ SHA extensions</td>
 

docs/algorithms/ml-dsa-44.toml

@@ -3,4 +3,4 @@ family = "Signatures"
 specs = ["MlDsa"]
 modules = ["src/mldsa44.rs"]
 asm = ["mldsa44", "mldsa"]
-optimized = { x86_64 = "SSE2 NTT" }
+optimized = { x86_64 = "SSE2 polynomial arithmetic" }

docs/algorithms/ml-dsa-65.toml

@@ -3,4 +3,4 @@ family = "Signatures"
 specs = ["MlDsa"]
 modules = ["src/mldsa65.rs"]
 asm = ["mldsa65", "mldsa"]
-optimized = { x86_64 = "SSE2 NTT" }
+optimized = { x86_64 = "SSE2 polynomial arithmetic" }

docs/algorithms/ml-dsa-87.toml

@@ -3,4 +3,4 @@ family = "Signatures"
 specs = ["MlDsa"]
 modules = ["src/mldsa87.rs"]
 asm = ["mldsa87", "mldsa"]
-optimized = { x86_64 = "SSE2 NTT" }
+optimized = { x86_64 = "SSE2 polynomial arithmetic" }

lean/VerifiedGarbage/Artifacts/MlDsaArith/X86_64.lean

@@ -46,27 +46,37 @@ def artifacts : List Artifact := [
   { Spec.MlDsa.mulApi with
     target := X86_64.target
     doc := Spec.MlDsa.mulApi.doc
+      (notes := ["The function computes on four coefficients at a time in SSE2 registers. It sets MXCSR to \
+        `0x1FBF` around its multiplications (Intel's mitigation of MXCSR-configuration-dependent timing), \
+        through the last 8 bytes of `h`, which it stores last, and loads the caller's MXCSR back before \
+        returning."])
     code := Impl.MlDsa.X86_64.Arith.mul
     contract := Spec.MlDsa.mulContract X86_64.abi
     verified := Proof.MlDsa.X86_64.Arith.mul_verified
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.MlDsa.mulAddApi with
     target := X86_64.target
     doc := Spec.MlDsa.mulAddApi.doc
+      (notes := ["The function computes on four coefficients at a time in SSE2 registers. It sets MXCSR to \
+        `0x1FBF` around its multiplications (Intel's mitigation of MXCSR-configuration-dependent timing), \
+        through the last 8 bytes of `h`, which it stores last, and loads the caller's MXCSR back before \
+        returning."])
     code := Impl.MlDsa.X86_64.Arith.mulAdd
     contract := Spec.MlDsa.mulAddContract X86_64.abi
     verified := Proof.MlDsa.X86_64.Arith.mulAdd_verified
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.MlDsa.addApi with
     target := X86_64.target
     doc := Spec.MlDsa.addApi.doc
+      (notes := ["The function computes on four coefficients at a time in SSE2 registers."])
     code := Impl.MlDsa.X86_64.Arith.add
     contract := Spec.MlDsa.addContract X86_64.abi
     verified := Proof.MlDsa.X86_64.Arith.add_verified
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.MlDsa.subApi with
     target := X86_64.target
     doc := Spec.MlDsa.subApi.doc
+      (notes := ["The function computes on four coefficients at a time in SSE2 registers."])
     code := Impl.MlDsa.X86_64.Arith.sub
     contract := Spec.MlDsa.subContract X86_64.abi
     verified := Proof.MlDsa.X86_64.Arith.sub_verified

lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaKeyGen.lean

@@ -0,0 +1,65 @@
+import VerifiedGarbage.TCB.X86_64.Target
+import VerifiedGarbage.Proof.MlDsa.X86_64.KeyGen.Inst
+
+/-!
+# ML-DSA (FIPS 204) on x86-64: key generation
+
+A generic file (see `TCB/Emit.lean`): the artifacts it lists, which call an
+implementation `v` of the polynomial arithmetic (`vg_mldsa_ntt`, …), are
+emitted once for each implementation (`Variants/MlDsaArith/X86_64/`), named
+with its suffix (e.g. `vg_mldsa44_keygen_avx2`), and need its CPU features.
+**Review note**: `sig` and `doc` are trusted, as they tie the Rust caller to
+the contract; check them against the contract's `pre`/`post`. Each artifact
+is made from its function's `Api` (in `Spec/MlDsa/Contract.lean`, reviewed
+with the contract), and this file adds only notes on the implementation. The
+emitter adds the `# Safety` items that depend on the target
+(`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+-/
+
+namespace VG.Generic.MlDsaArith.X86_64.MlDsaKeyGen
+
+open VG.Proof.MlDsa.X86_64 (ArithImpl)
+open VG.Impl.MlDsa.X86_64.KeyGen (keyGen primsWith)
+
+/-- Notes on the implementation, the same for every parameter set. -/
+def notes : List String :=
+  ["The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 \
+    bytes of stack below its return address.",
+   "It samples every polynomial of `A` and of `s1` and `s2` whatever the samplers return, and \
+    zeroes the polynomial of a sampler that fails rather than branching on it: its timing does not \
+    depend on whether key generation fails."]
+
+def artifacts (v : ArithImpl) : List Artifact := [
+  { Spec.MlDsa.keyGen44Api with
+    name := Spec.MlDsa.keyGen44Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.keyGen44Api.doc (notes := notes)
+    code := keyGen (primsWith v.code) Spec.MlDsa.mlDsa44
+    contract := Spec.MlDsa.keyGenContract Spec.MlDsa.mlDsa44 X86_64.abi 32
+    stack := 32
+    verified := Proof.MlDsa.X86_64.KeyGen.keyGen_verifiedWith v (.inl rfl)
+    spSafe := Proof.MlDsa.X86_64.KeyGen.keyGen_spSafe v (.inl rfl) },
+  { Spec.MlDsa.keyGen65Api with
+    name := Spec.MlDsa.keyGen65Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.keyGen65Api.doc (notes := notes)
+    code := keyGen (primsWith v.code) Spec.MlDsa.mlDsa65
+    contract := Spec.MlDsa.keyGenContract Spec.MlDsa.mlDsa65 X86_64.abi 32
+    stack := 32
+    verified := Proof.MlDsa.X86_64.KeyGen.keyGen_verifiedWith v (.inr (.inl rfl))
+    spSafe := Proof.MlDsa.X86_64.KeyGen.keyGen_spSafe v (.inr (.inl rfl)) },
+  { Spec.MlDsa.keyGen87Api with
+    name := Spec.MlDsa.keyGen87Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.keyGen87Api.doc (notes := notes)
+    code := keyGen (primsWith v.code) Spec.MlDsa.mlDsa87
+    contract := Spec.MlDsa.keyGenContract Spec.MlDsa.mlDsa87 X86_64.abi 32
+    stack := 32
+    verified := Proof.MlDsa.X86_64.KeyGen.keyGen_verifiedWith v (.inr (.inr rfl))
+    spSafe := Proof.MlDsa.X86_64.KeyGen.keyGen_spSafe v (.inr (.inr rfl)) }]
+
+end VG.Generic.MlDsaArith.X86_64.MlDsaKeyGen

lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaSign.lean

@@ -0,0 +1,65 @@
+import VerifiedGarbage.TCB.X86_64.Target
+import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.Verified
+
+/-!
+# ML-DSA (FIPS 204) on x86-64: signing
+
+A generic file (see `TCB/Emit.lean`): the artifacts it lists, which call an
+implementation `v` of the polynomial arithmetic (`vg_mldsa_ntt`, …), are
+emitted once for each implementation (`Variants/MlDsaArith/X86_64/`), named
+with its suffix (e.g. `vg_mldsa44_sign_avx2`), and need its CPU features.
+**Review note**: `sig` and `doc` are trusted, as they tie the Rust caller to
+the contract; check them against the contract's `pre`/`post`. Each artifact
+is made from its function's `Api` (in `Spec/MlDsa/Contract.lean`, reviewed
+with the contract), and this file adds only notes on the implementation. The
+emitter adds the `# Safety` items that depend on the target
+(`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+-/
+
+namespace VG.Generic.MlDsaArith.X86_64.MlDsaSign
+
+open VG.Proof.MlDsa.X86_64 (ArithImpl)
+open VG.Proof.MlDsa.X86_64.Sign (primsWith)
+
+/-- Notes on the implementation, the same for every parameter set. -/
+def notes : List String :=
+  ["The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 \
+    bytes of stack below its return address.",
+   "The signing loop runs at most 814 iterations (FIPS 204 Appendix C). Each iteration computes \
+    every validity check and combines them without branching: the one branch on their result \
+    is the only place an iteration's outcome affects timing."]
+
+def artifacts (v : ArithImpl) : List Artifact := [
+  { Spec.MlDsa.sign44Api with
+    name := Spec.MlDsa.sign44Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.sign44Api.doc (notes := notes)
+    code := Impl.MlDsa.X86_64.Sign.sign (primsWith v.code) Spec.MlDsa.mlDsa44
+    contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa44 X86_64.abi 24
+    stack := 24
+    verified := Proof.MlDsa.X86_64.Sign.sign_verified' v (.inl rfl)
+    spSafe := Proof.MlDsa.X86_64.Sign.sign_spSafe v (.inl rfl) },
+  { Spec.MlDsa.sign65Api with
+    name := Spec.MlDsa.sign65Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.sign65Api.doc (notes := notes)
+    code := Impl.MlDsa.X86_64.Sign.sign (primsWith v.code) Spec.MlDsa.mlDsa65
+    contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa65 X86_64.abi 24
+    stack := 24
+    verified := Proof.MlDsa.X86_64.Sign.sign_verified' v (.inr (.inl rfl))
+    spSafe := Proof.MlDsa.X86_64.Sign.sign_spSafe v (.inr (.inl rfl)) },
+  { Spec.MlDsa.sign87Api with
+    name := Spec.MlDsa.sign87Api.name ++ v.code.sfx
+    features := v.features
+    target := X86_64.target
+    doc := Spec.MlDsa.sign87Api.doc (notes := notes)
+    code := Impl.MlDsa.X86_64.Sign.sign (primsWith v.code) Spec.MlDsa.mlDsa87
+    contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa87 X86_64.abi 24
+    stack := 24
+    verified := Proof.MlDsa.X86_64.Sign.sign_verified' v (.inr (.inr rfl))
+    spSafe := Proof.MlDsa.X86_64.Sign.sign_spSafe v (.inr (.inr rfl)) }]
+
+end VG.Generic.MlDsaArith.X86_64.MlDsaSign