ML-DSA x86-64 sign: each row of w with one fused dot-inverse call

lean/VerifiedGarbage/Artifacts/MlDsaArith/X86_64.lean

@@ -9,13 +9,30 @@ public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Ntt
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.NttInv
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.YMontgomery
 public import VerifiedGarbage.Proof.Framework.Registration
+public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Dot
+public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.YDot
 
 /-! # ML-DSA (FIPS 204) on x86-64: the arithmetic of polynomials -/
 
 @[expose] public section
 
 namespace VG.Artifacts.MlDsaArith.X86_64
 
+/-- Notes on `vg_mldsa_dot_inverse{c}`. -/
+def dotNotes : List String :=
+  ["The function computes on four coefficients at a time in SSE2 registers: it sums the products in \
+      64-bit lanes, reduces each sum once, then runs `vg_mldsa_inv_ntt`'s code, with a table of the 256 \
+      zetas that it stores in `scratch`. It sets MXCSR to `0x1FBF` around its multiplications (Intel's \
+      mitigation of MXCSR-configuration-dependent timing) and loads the caller's MXCSR back before returning."]
+
+/-- Notes on `vg_mldsa_dot_inverse{c}_avx2`. -/
+def dotNotesAvx2 : List String :=
+  ["The function computes on eight coefficients at a time in AVX2 registers: it sums the products in \
+      64-bit lanes, reduces each sum once to the sum times `2⁻³²`, then runs \
+      `vg_mldsa_montgomery_inv_ntt_avx2`'s code, which cancels the factor, with a table of the 256 zetas \
+      that it stores in `scratch`. It sets MXCSR to `0x1FBF` around its multiplications (Intel's \
+      mitigation of MXCSR-configuration-dependent timing) and loads the caller's MXCSR back before returning."]
+
 def artifacts : List Artifact := [
   Spec.MlDsa.nttApi.artifact X86_64.target {
     notes := ["The function computes on four coefficients at a time in SSE2 registers, with a table of \
@@ -101,6 +118,36 @@ def artifacts : List Artifact := [
     notes := ["The function computes on eight coefficients at a time in AVX2 registers."]
     code := Impl.MlDsa.X86_64.Arith.subAvx2
     verified := Proof.MlDsa.X86_64.Arith.subY_verified
+    features := ["avx", "avx2"] },
+  (Spec.MlDsa.dotInverseApi 4).artifact X86_64.target {
+    notes := dotNotes
+    code := Impl.MlDsa.X86_64.Arith.dotInvSse2 4
+    verified := Proof.MlDsa.X86_64.Arith.DotS.verified4 },
+  (Spec.MlDsa.dotInverseApi 5).artifact X86_64.target {
+    notes := dotNotes
+    code := Impl.MlDsa.X86_64.Arith.dotInvSse2 5
+    verified := Proof.MlDsa.X86_64.Arith.DotS.verified5 },
+  (Spec.MlDsa.dotInverseApi 7).artifact X86_64.target {
+    notes := dotNotes
+    code := Impl.MlDsa.X86_64.Arith.dotInvSse2 7
+    verified := Proof.MlDsa.X86_64.Arith.DotS.verified7 },
+  (Spec.MlDsa.dotInverseApi 4).artifact X86_64.target {
+    suffix := "_avx2"
+    notes := dotNotesAvx2
+    code := Impl.MlDsa.X86_64.Arith.dotInvAvx2 4
+    verified := Proof.MlDsa.X86_64.Arith.YDot.verified4
+    features := ["avx", "avx2"] },
+  (Spec.MlDsa.dotInverseApi 5).artifact X86_64.target {
+    suffix := "_avx2"
+    notes := dotNotesAvx2
+    code := Impl.MlDsa.X86_64.Arith.dotInvAvx2 5
+    verified := Proof.MlDsa.X86_64.Arith.YDot.verified5
+    features := ["avx", "avx2"] },
+  (Spec.MlDsa.dotInverseApi 7).artifact X86_64.target {
+    suffix := "_avx2"
+    notes := dotNotesAvx2
+    code := Impl.MlDsa.X86_64.Arith.dotInvAvx2 7
+    verified := Proof.MlDsa.X86_64.Arith.YDot.verified7
     features := ["avx", "avx2"] }]
 
 end VG.Artifacts.MlDsaArith.X86_64

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Arith/Avx2.lean

@@ -206,6 +206,6 @@ def subAvx2 : Prog isa :=
 def Backend.avx2 : Backend :=
   ⟨nttAvx2, nttInvAvx2, mulAvx2, mulAddAvx2, addAvx2, subAvx2, Round.highBitsAvx2,
     Round.lowBitsAvx2, Round.normLtAvx2, Round.makeHintAvx2, Round.useHintAvx2, Sample.Rej5.rejNTT4Avx2,
-    Sample.Mask4.expandMask4Avx2, "_avx2", false⟩
+    Sample.Mask4.expandMask4Avx2, "_avx2", false, .block [], .block [], .block []⟩
 
 end VG.Impl.MlDsa.X86_64.Arith

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Arith/Backend.lean

@@ -2,6 +2,7 @@ module
 
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Ntt
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Mul
+public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Dot
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.AddSub
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Round.Round
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Sample.RejNtt4
@@ -47,18 +48,27 @@ structure Backend where
   sfx : String
   /-- Whether products and the inverse transform use Montgomery scaling. -/
   montgomery : Bool := false
+  /-- `vg_mldsa_dot_inverse4`, `5` and `7`: the inverse NTT of a row's sum of products. -/
+  dotInv4 : Prog isa
+  dotInv5 : Prog isa
+  dotInv7 : Prog isa
 
 /-- The SSE2 code. -/
 def Backend.sse2 : Backend :=
   ⟨Arith.ntt, Arith.nttInv, Arith.mul, Arith.mulAdd, Arith.add, Arith.sub, Round.highBits,
     Round.lowBits, Round.normLt, Round.makeHint, Round.useHint, Sample.Rej4.rejNTT4,
-    Sample.Mask4.expandMask4, "", false⟩
+    Sample.Mask4.expandMask4, "", false, dotInvSse2 4, dotInvSse2 5,
+    dotInvSse2 7⟩
+
+/-- `vg_mldsa_dot_inverse{c}`, for `c` of 4, 5 and 7. -/
+abbrev Backend.dotInv (B : Backend) (c : Nat) : Prog isa :=
+  if c = 4 then B.dotInv4 else if c = 5 then B.dotInv5 else B.dotInv7
 
 /-- Every function empty, which the proofs that the functions calling a
 backend never write `rsp` (and load MXCSR only to restore it) evaluate in
 its place. -/
 def Backend.empty : Backend :=
   ⟨.block [], .block [], .block [], .block [], .block [], .block [], .block [], .block [], .block [],
-    .block [], .block [], .block [], .block [], "", false⟩
+    .block [], .block [], .block [], .block [], "", false, .block [], .block [], .block []⟩
 
 end VG.Impl.MlDsa.X86_64.Arith

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Arith/Dot.lean

@@ -0,0 +1,63 @@
+module
+
+public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Mul
+public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Ntt
+
+/-!
+# ML-DSA on x86-64: a row's sum of products, four coefficients at a time
+
+`vg_mldsa_dot_inverse{c}` sums the products of the coefficients of `c` pairs
+of polynomials `a[j]`, `b[j]` (each below `3 q`) in quadwords: `pmuludq`
+multiplies the even doublewords of its operands, and those shifted down by
+32 bits are the odd ones, so `xmm5` accumulates the products of the even
+coefficients and `xmm6` those of the odd ones (`dotMac`). A sum of at most
+seven products is below `63 q² < 2³² q`, so one Montgomery reduction of each
+quadword (`vredc`), merged as in `vmont`, leaves the sum times `2⁻³²` below
+`2 q`, which `vcsub` reduces (`dotRed`).
+
+The SSE2 code (`dotInvSse2`), whose inverse NTT is not scaled, multiplies
+each sum by `2⁶⁴ mod q` (in `xmm11`, `mulPro`) with `vmont` (`dotPlain`), which
+cancels the `2⁻³²`.
+-/
+
+@[expose] public section
+
+namespace VG.Impl.MlDsa.X86_64.Arith
+
+open VG.X86_64
+open VG.Impl.MlKem.X86_64 (xb xmov withMxcsr rcxLoop)
+
+/-- The sums, zero. -/
+def dotZero : List Instr := [xb .pxor .xmm5 .xmm5, xb .pxor .xmm6 .xmm6]
+
+/-- The products of the doublewords of `xmm0` and `xmm1` added to the
+quadwords of `xmm5` (even doublewords) and `xmm6` (odd ones). -/
+def dotMac : List Instr :=
+  [xmov .xmm2 .xmm0, .xop (.shift .psrlq .xmm2 32), xmov .xmm3 .xmm1, .xop (.shift .psrlq .xmm3 32),
+    xb .pmuludq .xmm2 .xmm3, xb .pmuludq .xmm0 .xmm1, xb .paddq .xmm5 .xmm0, xb .paddq .xmm6 .xmm2]
+
+/-- The sums, reduced: `(P + m q) / 2³²` of each quadword, merged into the
+doublewords of `xmm5`, then reduced to `[0, q)`. -/
+def dotRed : List Instr :=
+  vredc .xmm5 .xmm2 ++ [.xop (.shift .psrlq .xmm5 32)] ++ vredc .xmm6 .xmm2 ++ [xb .por .xmm5 .xmm6] ++
+    vcsub .xmm5 .xmm2
+
+/-- The sum times `2⁻³²`, times `2⁶⁴ mod q` (in `xmm11`) times `2⁻³²`: the sum
+modulo `q`. -/
+def dotPlain : List Instr := vmont .xmm5 .xmm11 .xmm11 .xmm2 .xmm4 ++ vcsub .xmm5 .xmm2
+
+/-- The coefficients of `a[j]` and `b[j]`. -/
+def dotLoadsS (j : Nat) : List Instr := [.movdquLoad .xmm0 (at_ .r10 (1024 * j)), .movdquLoad .xmm1 (at_ .rdx (1024 * j))]
+
+/-- Four coefficients of the sum of the `c` products. -/
+def dotBodyS (c : Nat) : List Instr :=
+  dotZero ++ (List.range c).flatMap (fun j => dotLoadsS j ++ dotMac) ++ dotRed ++ dotPlain ++
+    [.movdquStore (at_ .r8 0) .xmm5, .alu .add .r8 (.imm 16), .alu .add .r10 (.imm 16), .alu .add .rdx (.imm 16)]
+
+/-- `vg_mldsa_dot_inverse{c}`: the sum of the `c` products, then `NTT⁻¹`, in
+one MXCSR region. -/
+def dotInvSse2 (c : Nat) : Prog isa :=
+  .seq (.block [.mov .r10 (.reg .rsi), .mov .rsi (.reg .rcx)]) <| withMxcsr .rsi 768 <|
+    .seq (.block (mulPro ++ [.mov .r8 (.reg .rdi)])) (.seq (rcxLoop 64 (dotBodyS c)) nttInvBody)
+
+end VG.Impl.MlDsa.X86_64.Arith

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Arith/Montgomery.lean

@@ -1,6 +1,7 @@
 module
 
 public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Lazy
+public import VerifiedGarbage.Impl.MlDsa.X86_64.Arith.Dot
 
 /-! # Montgomery-scaled AVX2 products for ML-DSA -/
 
@@ -65,19 +66,42 @@ def ylast : Prog isa :=
 /-- `NTT⁻¹` with Montgomery scaling: the eight layers with `vibflyLazy`, whose
 coefficients stay below `256 q < 2^32`, the last two of them with the
 reducing multiplication by `R/256`, which accepts any doubleword (`ylast`). -/
-def montNttInvAvx2 : Prog isa := VG.Impl.MlKem.X86_64.withMxcsr .rsi 768 <|
+def montInvBody : Prog isa :=
   .seq (.block ypro) (.seq (.block (yconst .xmm11 1072693376)) (.seq (ylay1 vibflyLazy 248 yzeta8R (-32))
     (.seq (ylay2 vibflyLazy 124 0x5F 0x0A (-16)) (.seq (ylay4 vibflyLazy 62 0x55 0x00 (-8))
       (.seq (ylay vibflyLazy 8 31 (-4)) (.seq (ylay vibflyLazy 16 15 (-4)) (.seq (ylay vibflyLazy 32 7 (-4))
         (.seq ylast (.block yepi)))))))))
 
+def montNttInvAvx2 : Prog isa := VG.Impl.MlKem.X86_64.withMxcsr .rsi 768 montInvBody
+
+/-! ## A row's sum of products, then `NTT⁻¹` -/
+
+/-- The coefficients of `a[j]` and `b[j]`. -/
+def dotLoads (j : Nat) : List Instr :=
+  [.vmovdquLoad .l256 .xmm0 (at_ .r10 (1024 * j)), .vmovdquLoad .l256 .xmm1 (at_ .rdx (1024 * j))]
+
+/-- Eight coefficients of the sum of the `c` products, scaled by `2⁻³²`. -/
+def dotBody (c : Nat) : List Instr :=
+  toY dotZero ++ (List.range c).flatMap (fun j => dotLoads j ++ toY dotMac) ++
+    toY dotRed ++ [.vmovdquStore .l256 (at_ .r8 0) .xmm5, .alu .add .r8 (.imm 32), .alu .add .r10 (.imm 32),
+      .alu .add .rdx (.imm 32)]
+
+/-- `vg_mldsa_dot_inverse{c}_avx2`: the sum of the `c` products scaled by
+`2⁻³²`, then `NTT⁻¹` with Montgomery scaling, in one MXCSR region. -/
+def dotInvAvx2 (c : Nat) : Prog isa :=
+  .seq (.block [.mov .r10 (.reg .rsi), .mov .rsi (.reg .rcx)]) <| VG.Impl.MlKem.X86_64.withMxcsr .rsi 768 <|
+    .seq (.block (yconsts ++ [.mov .r8 (.reg .rdi)])) (.seq (rcxLoop 32 (dotBody c)) montInvBody)
+
 /-- AVX2 arithmetic with lazy forward NTT, scaled products and a compensating inverse NTT. -/
 def Backend.avx2Combined : Backend :=
   { Backend.avx2 with
     ntt := lazyNtt
     invNtt := montNttInvAvx2
     mul := montMulAvx2
     mulAdd := montMulAddAvx2
-    montgomery := true }
+    montgomery := true
+    dotInv4 := dotInvAvx2 4
+    dotInv5 := dotInvAvx2 5
+    dotInv7 := dotInvAvx2 7 }
 
 end VG.Impl.MlDsa.X86_64.Arith

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Arith/Ntt.lean

@@ -99,10 +99,13 @@ def ntt : Prog isa := withMxcsr .rsi 768 <|
     (.seq (vlay vbfly 16 8 4) (.seq (vlay vbfly 8 16 4) (.seq (vlay vbfly 4 32 4)
       (.seq (vlay2 vbfly 64 0x50 8) (vlay1 vbfly 128 0xE4 16))))))))
 
-def nttInv : Prog isa := withMxcsr .rsi 768 <|
+/-- `NTT⁻¹` but for `withMxcsr`. -/
+def nttInvBody : Prog isa :=
   .seq (.block vpro) (.seq (vlay1 vibfly 252 0x1B (-16)) (.seq (vlay2 vibfly 126 0x05 (-8))
     (.seq (vlay vibfly 4 63 (-4)) (.seq (vlay vibfly 8 31 (-4)) (.seq (vlay vibfly 16 15 (-4))
       (.seq (vlay vibfly 32 7 (-4)) (.seq (vlay vibfly 64 3 (-4)) (.seq (vlay vibfly 128 1 (-4))
         vscale))))))))
 
+def nttInv : Prog isa := withMxcsr .rsi 768 nttInvBody
+
 end VG.Impl.MlDsa.X86_64.Arith

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Frag.lean

@@ -34,7 +34,6 @@ structure Prims where
   ntt : Prog isa
   invNtt : Prog isa
   mul : Prog isa
-  mulAdd : Prog isa
   add : Prog isa
   sub : Prog isa
   rejNTT : Prog isa
@@ -55,6 +54,10 @@ structure Prims where
   /-- What the names of the polynomial arithmetic's functions end with (`Arith.Backend`). -/
   sfx : String := ""
   montgomery : Bool := false
+  /-- `vg_mldsa_dot_inverse4`, `5` and `7` -/
+  dotInv4 : Prog isa := .block []
+  dotInv5 : Prog isa := .block []
+  dotInv7 : Prog isa := .block []
 
 /-! ## The layout of the working space (in bytes)
 
@@ -184,9 +187,19 @@ def nttAt (f : Ptr) : Prog isa := callP ("vg_mldsa_ntt" ++ P.sfx) P.ntt [.ptr f,
 
 def invNttAt (f : Ptr) : Prog isa := callP ((if P.montgomery then "vg_mldsa_montgomery_inv_ntt" else "vg_mldsa_inv_ntt") ++ P.sfx) P.invNtt [.ptr f, .ptr (sc oPS)]
 
+/-- `vg_mldsa_dot_inverse{c}`, for `c` of 4, 5 and 7. -/
+abbrev Prims.dotInv (P : Prims) (c : Nat) : Prog isa := if c = 4 then P.dotInv4 else if c = 5 then P.dotInv5 else P.dotInv7
+
+/-- The name of `vg_mldsa_dot_inverse{c}`, written out (the kernel evaluates
+code, and `toString` on `Nat` is well-founded recursion). -/
+abbrev dotInvName (c : Nat) : String :=
+  if c = 4 then "vg_mldsa_dot_inverse4" else if c = 5 then "vg_mldsa_dot_inverse5" else "vg_mldsa_dot_inverse7"
+
+def dotInvAt (count : Nat) (h f g : Ptr) : Prog isa :=
+  callP (dotInvName count ++ P.sfx) (P.dotInv count) [.ptr h, .ptr f, .ptr g, .ptr (sc oPS)]
+
 def mulAt (h f g : Ptr) : Prog isa := callP ((if P.montgomery then "vg_mldsa_montgomery_multiply_ntt" else "vg_mldsa_multiply_ntt") ++ P.sfx) P.mul [.ptr h, .ptr f, .ptr g]
 
-def mulAddAt (h f g : Ptr) : Prog isa := callP ((if P.montgomery then "vg_mldsa_montgomery_multiply_add_ntt" else "vg_mldsa_multiply_add_ntt") ++ P.sfx) P.mulAdd [.ptr h, .ptr f, .ptr g]
 
 def addAt (f g : Ptr) : Prog isa := callP ("vg_mldsa_add" ++ P.sfx) P.add [.ptr f, .ptr g]
 

lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Sign.lean

@@ -177,9 +177,7 @@ def mask4 (g : Nat) : Prog isa :=
   .seq (seqR (cpM4 g) 0 4) (.seq (mask4At P p.γ₁ (yP p (4 * g)) (r4P p)) (seqR (yhR P p) (4 * g) 4))
 
 /-- `w[i] = NTT⁻¹(∑_j Â[i, j] ŷ[j])`. -/
-def rowW (i : Nat) : Prog isa :=
-  .seq (mulAt P (wP p i) (aP p i 0) (yhP p 0))
-    (.seq (seqR (fun j => mulAddAt P (wP p i) (aP p i j) (yhP p j)) 1 (p.ℓ - 1)) (invNttAt P (wP p i)))
+def rowW (i : Nat) : Prog isa := dotInvAt P p.ℓ (wP p i) (aP p i 0) (yhP p 0)
 
 /-- `w1Encode(HighBits(w[i]))` to `W1 + i · w1Len`. -/
 def w1R (i : Nat) : Prog isa :=

lean/VerifiedGarbage/Proof/MlDsa/Arith/DotSum.lean

@@ -0,0 +1,54 @@
+module
+
+public import VerifiedGarbage.Spec.MlDsa.FusedInverse
+import VerifiedGarbage.Proof.MlDsa.Arith.Zq
+public import VerifiedGarbage.Proof.Framework.PowLit
+public import VerifiedGarbage.Spec.MlDsa
+
+/-! # ML-DSA: a coefficient of a row's sum of products
+
+Coefficient `i` of `dotNTT f g c` is the sum `dsum` of the products of the
+natural numbers that the coefficients `i` of `f j` and `g j` reduce from. -/
+
+@[expose] public section
+
+namespace VG.Proof.MlDsa.Arith
+open VG.Spec.MlDsa
+
+/-- `∑_{j < c} A j · B j`. -/
+def dsum (A B : Nat → Nat) : Nat → Nat
+  | 0 => 0
+  | c + 1 => dsum A B c + A c * B c
+
+theorem dsum_le {A B : Nat → Nat} {b : Nat} : ∀ {c}, (∀ j < c, A j * B j ≤ b) → dsum A B c ≤ c * b
+  | 0, _ => by simp [dsum]
+  | c + 1, h => by
+    rw [Nat.succ_mul]; exact Nat.add_le_add (dsum_le fun j hj => h j (by omega)) (h c (by omega))
+
+theorem dotNTT_succ (f g : Nat → Poly) (c : Nat) :
+    dotNTT f g (c + 1) = add (dotNTT f g c) (multiplyNTT (f c) (g c)) := by
+  simp only [dotNTT, List.range_succ, List.map_append, List.map_cons, List.map_nil, List.foldl_append,
+    List.foldl_cons, List.foldl_nil]
+
+theorem dotNTT_get {f g : Nat → Poly} {A B : Nat → Nat} {i : Nat} (hi : i < n) :
+    ∀ {c : Nat}, (∀ j < c, (f j)[i]! = Fin.ofNat q (A j)) → (∀ j < c, (g j)[i]! = Fin.ofNat q (B j)) →
+      (dotNTT f g c)[i]! = Fin.ofNat q (dsum A B c)
+  | 0, _, _ => by
+    show zero[i]! = _
+    rw [getElem!_eq zero hi]
+    simp only [zero, Vector.getElem_replicate]
+    rfl
+  | c + 1, hf, hg => by
+    rw [dotNTT_succ, add_get _ _ hi, mul_get _ _ hi, dotNTT_get hi (fun j hj => hf j (by omega))
+      (fun j hj => hg j (by omega)), hf c (by omega), hg c (by omega)]
+    apply Fin.ext
+    simp only [dsum, Fin.val_add, Fin.val_mul, Fin.val_ofNat, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
+
+theorem dotNTT_congr {f g f' g' : Nat → Poly} {c : Nat} (hf : ∀ j < c, f j = f' j) (hg : ∀ j < c, g j = g' j) :
+    dotNTT f g c = dotNTT f' g' c := by
+  unfold dotNTT
+  congr 1
+  exact List.map_congr_left fun j hj => by
+    rw [hf j (List.mem_range.mp hj), hg j (List.mem_range.mp hj)]
+
+end VG.Proof.MlDsa.Arith

lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Avx2Lit.lean

@@ -31,6 +31,7 @@ namespace VG
 open Impl.MlDsa.X86_64
 
 materialize_code Arith.lazyNtt
+materialize_code Arith.montInvBody
 materialize_code Arith.montNttInvAvx2
 materialize_code Arith.montMulAvx2
 materialize_code Arith.montMulAddAvx2

lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Backend.lean

@@ -9,6 +9,7 @@ public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.AddSub
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Mul
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Ntt
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.NttInv
+public import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Dot
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Round.Bits
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Round.MakeHint
 public import VerifiedGarbage.Proof.MlDsa.X86_64.Round.NormLt
@@ -81,6 +82,7 @@ structure BackendOk (B : Backend) : Prop where
   useHint : FnOk (fun S => Spec.MlDsa.useHintContract X86_64.abi S) B.useHint
   rej4 : Rej4Ok B.rej4
   expandMask4 : Mask4Ok B.expandMask4
+  dotInv : ∀ c, c = 4 ∨ c = 5 ∨ c = 7 → FnOk (fun S => Spec.MlDsa.dotInverseContract c X86_64.abi S) (B.dotInv c)
 
 /-- An implementation of the polynomial arithmetic on x86-64. -/
 structure ArithImpl where
@@ -124,7 +126,15 @@ def ArithImpl.sse2 : ArithImpl where
       rej4 := ⟨Rej4.rejNTT4_verified, Proof.MlKem.X86_64.nosp_of (by decide +kernel), by decide +kernel,
         by decide +kernel, Code.all_of_allInstrs (by decide +kernel), fun _ _ _ => Rej4.rejNTT4_ret⟩
       expandMask4 := ⟨Mask4.expandMask4_verified, Proof.MlKem.X86_64.nosp_of (by decide +kernel), by decide +kernel,
-        by decide +kernel, Code.all_of_allInstrs (by decide +kernel)⟩ }
+        by decide +kernel, Code.all_of_allInstrs (by decide +kernel)⟩
+      dotInv := fun c hc => by
+        rcases hc with rfl | rfl | rfl
+        · exact FnOk.of Arith.DotS.verified4 (by decide +kernel) (by decide +kernel) (by decide +kernel)
+            (by decide +kernel)
+        · exact FnOk.of Arith.DotS.verified5 (by decide +kernel) (by decide +kernel) (by decide +kernel)
+            (by decide +kernel)
+        · exact FnOk.of Arith.DotS.verified7 (by decide +kernel) (by decide +kernel) (by decide +kernel)
+            (by decide +kernel) }
   features := []
 
 end VG.Proof.MlDsa.X86_64