diff --git a/README.md b/README.md index 5327870bd..e56aba7d0 100644 --- a/README.md +++ b/README.md @@ -923,7 +923,7 @@ yours to keep: ✅ -✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2) +✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2) ✅ SHA extensions @@ -939,7 +939,7 @@ yours to keep: ✅ -✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2) +✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2) ✅ SHA extensions @@ -955,7 +955,7 @@ yours to keep: ✅ -✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2) +✅ AVX2; SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2) ✅ SHA extensions diff --git a/docs/algorithms/ml-dsa-44.toml b/docs/algorithms/ml-dsa-44.toml index 77df162de..cfe6fa086 100644 --- a/docs/algorithms/ml-dsa-44.toml +++ b/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 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2)" } +optimized = { x86_64 = "SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2)" } diff --git a/docs/algorithms/ml-dsa-65.toml b/docs/algorithms/ml-dsa-65.toml index 3d5f174db..b66d35e1a 100644 --- a/docs/algorithms/ml-dsa-65.toml +++ b/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 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2)" } +optimized = { x86_64 = "SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2)" } diff --git a/docs/algorithms/ml-dsa-87.toml b/docs/algorithms/ml-dsa-87.toml index 75d9dc3d0..6b8399adc 100644 --- a/docs/algorithms/ml-dsa-87.toml +++ b/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 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time in key generation and verification (four SHAKE128 instances at once with AVX2)" } +optimized = { x86_64 = "SSE2 and AVX2 polynomial arithmetic; HighBits, LowBits, MakeHint and the norm check with AVX2; matrix sampled four entries at a time (four SHAKE128 instances at once with AVX2)" } diff --git a/lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaSign.lean b/lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaSign.lean index 2a231e969..9eb6721bd 100644 --- a/lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaSign.lean +++ b/lean/VerifiedGarbage/Generic/MlDsaArith/X86_64/MlDsaSign.lean @@ -24,7 +24,7 @@ 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 \ + ["The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 \ 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 \ @@ -37,8 +37,8 @@ def artifacts (v : ArithImpl) : List Artifact := [ 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 + contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa44 X86_64.abi 32 + stack := 32 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 @@ -47,8 +47,8 @@ def artifacts (v : ArithImpl) : List Artifact := [ 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 + contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa65 X86_64.abi 32 + stack := 32 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 @@ -57,8 +57,8 @@ def artifacts (v : ArithImpl) : List Artifact := [ 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 + contract := Spec.MlDsa.signContract Spec.MlDsa.mlDsa87 X86_64.abi 32 + stack := 32 verified := Proof.MlDsa.X86_64.Sign.sign_verified' v (.inr (.inr rfl)) spSafe := Proof.MlDsa.X86_64.Sign.sign_spSafe v (.inr (.inr rfl)) }] diff --git a/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Frag.lean b/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Frag.lean index a8a164427..066d7b621 100644 --- a/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Frag.lean +++ b/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Frag.lean @@ -44,6 +44,8 @@ structure Prims where bitPack : Prog isa bitUnpack : Prog isa hintBitPack : Prog isa + /-- `vg_mldsa_rej_ntt_poly4` -/ + rej4 : Prog isa /-- What the names of the polynomial arithmetic's functions end with (`Arith.Backend`). -/ sfx : String := "" @@ -54,7 +56,8 @@ at 200 (640 bytes); the caller's callee-saved registers at 840 (48 bytes); the iterations left (`CNT`), the counter `κ` (`KAP`) and the number of 1s of the hint (`ONES`) at 888, 896 and 904 (8 bytes each); the seed of `RejNTTPoly` (`RS`, 34 bytes) at 912; the seed of `ExpandMask` (`MS`, -`ρ″` and two bytes) at 960; `c̃` (`CT`, up to 64 bytes) at 1040; the +`ρ″` and two bytes) at 960; `c̃` (`CT`, up to 64 bytes) at 1040; the four +seeds of `vg_mldsa_rej_ntt_poly4` (`RS4`, 136 bytes) at 1152; the encoding of `w₁` (`W1`, up to 1024 bytes) at 2048; the working space of the primitives (`PS`, 2048 bytes) at 3072; and polynomials of 1024 bytes from 5120 (`P i`). -/ @@ -66,6 +69,7 @@ def oONES : Nat := 904 def oRS : Nat := 912 def oMS : Nat := 960 def oCT : Nat := 1040 +def oRS4 : Nat := 1152 def oW1 : Nat := 2048 def oPS : Nat := 3072 /-- Polynomial `i`. -/ @@ -184,6 +188,12 @@ def rejAt (a : Ptr) : Prog isa := .seq (callP "vg_mldsa_rej_ntt_poly" P.rejNTT [.ptr (sc oRS), .ptr a, .ptr (sc oPS)]) (.block [.alu32 .and .r15 (.reg .rax)]) +/-- `RejNTTPoly` of the four seeds at `RS4` to the four polynomials from `a`, with the working +space `w`, and `r15 ← r15 ∧ result`. -/ +def rej4At (a w : Ptr) : Prog isa := + .seq (callP ("vg_mldsa_rej_ntt_poly4" ++ P.sfx) P.rej4 [.ptr (sc oRS4), .ptr a, .ptr w]) + (.block [.alu32 .and .r15 (.reg .rax)]) + /-- A polynomial of `ExpandMask` from the seed at `MS` to `a`. -/ def maskAt (gamma1 : Nat) (a : Ptr) : Prog isa := callP "vg_mldsa_expand_mask_poly" P.expandMask [.ptr (sc oMS), .imm gamma1, .ptr a, .ptr (sc oPS)] diff --git a/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Sign.lean b/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Sign.lean index f31cf96e5..3f09192a2 100644 --- a/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Sign.lean +++ b/lean/VerifiedGarbage/Impl/MlDsa/X86_64/Sign/Sign.lean @@ -13,8 +13,11 @@ keeps `scratch` in `rbx`, `sk` in `rbp`, `mu` in `r12`, `rnd` in `r13` and `scratch`. 1. `ρ` (the first 32 bytes of `sk`) to `RS`, the seed of `RejNTTPoly`, and - `Â[r, s] = RejNTTPoly(ρ ‖ s ‖ r)` for the `kℓ` entries, with `r15` the - AND of the results. If one failed (`r15 = 0`), it returns 0 at once. + to each of the four seeds at `RS4`, and `Â[r, s] = RejNTTPoly(ρ ‖ s ‖ r)` + for the `kℓ` entries: four consecutive entries at a time + (`vg_mldsa_rej_ntt_poly4`, each seed at `RS4` with its entry's indices), + then the last `kℓ mod 4` one at a time, with `r15` the AND of the + results. If one failed (`r15 = 0`), it returns 0 at once. 2. `ŝ₁`, `ŝ₂` and `t̂₀`: the `NTT` of the `BitUnpack` of their pieces of `sk`; and `ρ″ = H(K ‖ rnd ‖ μ, 64)` to `MS`. 3. The rejection sampling loop, at most 814 iterations (`minBounds.sign`), @@ -29,8 +32,8 @@ keeps `scratch` in `rbx`, `sk` in `rbp`, `mu` in `r12`, `rnd` in `r13` and iterations. 4. If `r15 = 1`: `c̃`, the `BitPack` of `z` and `HintBitPack(h)` to `sig`. -Only the calls of `vg_mldsa_rej_ntt_poly` (whose seeds are `ρ` and two -indices), and the branch on their results, depend on `ρ`; only the calls of +Only the calls of `vg_mldsa_rej_ntt_poly` and `vg_mldsa_rej_ntt_poly4` +(whose seeds are `ρ` and two indices), and the branch on their results, depend on `ρ`; only the calls of `vg_mldsa_sample_in_ball`, and the branch on their results, on `c̃`; only the branch on the validity checks on whether they passed, and only the call of `vg_mldsa_hint_bit_pack` on the hint of the signature. Every other @@ -71,7 +74,8 @@ abbrev sigH : Nat := cLen p + zLen p * p.ℓ /-! ## The polynomials of the working space `ĉ` (0), four temporaries (1–4), then `h` (`k`), `y` (`ℓ`), `ŷ` (`ℓ`), -`w` (`k`), `ŝ₁` (`ℓ`), `ŝ₂` (`k`), `t̂₀` (`k`) and `Â` (`kℓ`, row by row). -/ +`w` (`k`), `ŝ₁` (`ℓ`), `ŝ₂` (`k`), `t̂₀` (`k`) and `Â` (`kℓ`, row by row), then the +working space of `vg_mldsa_rej_ntt_poly4` (8 KiB). -/ abbrev pS (i : Nat) : Ptr := sc (oP i) abbrev cP : Ptr := pS 0 @@ -87,6 +91,10 @@ abbrev s1P (r : Nat) : Ptr := pS (5 + 2 * p.k + 2 * p.ℓ + r) abbrev s2P (i : Nat) : Ptr := pS (5 + 2 * p.k + 3 * p.ℓ + i) abbrev t0P (i : Nat) : Ptr := pS (5 + 3 * p.k + 3 * p.ℓ + i) abbrev aP (i j : Nat) : Ptr := pS (5 + 4 * p.k + 3 * p.ℓ + p.ℓ * i + j) +/-- Entry `e = ℓi + j` of `Â`. -/ +abbrev aE (e : Nat) : Ptr := pS (5 + 4 * p.k + 3 * p.ℓ + e) +/-- The working space of `vg_mldsa_rej_ntt_poly4`. -/ +abbrev r4P : Ptr := pS (5 + 4 * p.k + 3 * p.ℓ + p.k * p.ℓ) end @@ -99,8 +107,23 @@ variable (P : Prims) (p : Params) def sampleE (e : Nat) : Prog isa := .seq (.block (setB (sc (oRS + 32)) (e % p.ℓ) ++ setB (sc (oRS + 33)) (e / p.ℓ))) (rejAt P (aP p (e / p.ℓ) (e % p.ℓ))) -/-- `ρ` to `RS`, and the `kℓ` entries of `Â`. -/ -def expandA : Prog isa := .seq (copy (sc oRS) (.rbp, 0) 32) (seqR (sampleE P p) 0 (p.k * p.ℓ)) +/-- `ρ` to seed `k` of `RS4`. -/ +def cpR4 (k : Nat) : Prog isa := copy (sc (oRS4 + 34 * k)) (.rbp, 0) 32 + +/-- The indices of entry `e + k` of `Â` to seed `k` of `RS4`. -/ +def setSR (e k : Nat) : List Instr := + setB (sc (oRS4 + 34 * k + 32)) ((e + k) % p.ℓ) ++ setB (sc (oRS4 + 34 * k + 33)) ((e + k) / p.ℓ) + +/-- Entries `4g, …, 4g + 3` of `Â`. -/ +def sample4 (g : Nat) : Prog isa := + .seq (.block (setSR p (4 * g) 0)) (.seq (.block (setSR p (4 * g) 1)) (.seq (.block (setSR p (4 * g) 2)) + (.seq (.block (setSR p (4 * g) 3)) (rej4At P (aE p (4 * g)) (r4P p))))) + +/-- `ρ` to `RS` and to the four seeds of `RS4`, and the `kℓ` entries of `Â`: four at a time, then +the last `kℓ mod 4` one at a time. -/ +def expandA : Prog isa := + .seq (copy (sc oRS) (.rbp, 0) 32) (.seq (seqR cpR4 0 4) + (.seq (seqR (sample4 P p) 0 (p.k * p.ℓ / 4)) (seqR (sampleE P p) (4 * (p.k * p.ℓ / 4)) (p.k * p.ℓ % 4)))) /-- `ŝ₁[r]`. -/ def decS1 (r : Nat) : Prog isa := diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Backend.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Backend.lean index 759bdcb13..ec62cfd5b 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Backend.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/Backend.lean @@ -43,6 +43,10 @@ structure Rej4Ok (c : Prog isa) : Prop where depth : c.depth ≤ 3 ctl : ctlOk c = true sp : c.all (fun i => !isa.writesSp i) = true + /-- Its result is whether each seed has 256 coefficients in its first 1008 bytes of output, as + both implementations', which signing branches on. -/ + ret : ∀ s t s', (Spec.MlDsa.rejNTT4Contract X86_64.abi 24).pre s → Exec isa c s t s' → + (s'.gpr .rax).setWidth 32 = Rej4.rej4Res s.mem (s.gpr .rdi) /-- Each function of the backend `B` meets its contract, and is safe to call. -/ structure BackendOk (B : Backend) : Prop where @@ -96,7 +100,7 @@ def ArithImpl.sse2 : ArithImpl where makeHint := FnOk.of Round.makeHint_verified (by decide +kernel) (by decide +kernel) (by decide +kernel) (by decide +kernel) 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)⟩ } + by decide +kernel, Code.all_of_allInstrs (by decide +kernel), fun _ _ _ => Rej4.rejNTT4_ret⟩ } features := [] end VG.Proof.MlDsa.X86_64 diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/BackendAvx2.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/BackendAvx2.lean index f91cfc25f..ec836ecc4 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/BackendAvx2.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Arith/BackendAvx2.lean @@ -41,7 +41,7 @@ def ArithImpl.avx2 : ArithImpl where makeHint := FnOk.of Round.makeHintY_verified (by decide +kernel) (by decide +kernel) (by decide +kernel) (by decide +kernel) rej4 := ⟨Rej4.rejNTT4Avx2_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), fun _ _ _ => Rej4.rejNTT4Avx2_ret⟩ } features := ["avx", "avx2"] end VG.Proof.MlDsa.X86_64 diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sample/Rej4Verified.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sample/Rej4Verified.lean index ddb0be67b..99763f2ba 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sample/Rej4Verified.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sample/Rej4Verified.lean @@ -1,5 +1,6 @@ import VerifiedGarbage.Proof.MlDsa.X86_64.Sample.Rej4Scalar import VerifiedGarbage.Proof.MlKem.X86_64.S4Verified +import VerifiedGarbage.Proof.MlDsa.KeyGen.Mono /-! # ML-DSA on x86-64: `vg_mldsa_rej_ntt_poly4` and `vg_mldsa_rej_ntt_poly4_avx2`, verified @@ -17,6 +18,7 @@ open VG VG.X86_64 open VG.Proof.MlDsa.Sample (rnFold rejNTT_some rejNTT_none) open VG.Proof.MlDsa.X86_64.Sample (leakBytes_inj) open VG.Spec.MlDsa (G) +open VG.Spec.Sha3 (bytesAt) theorem seed4_eq : Spec.MlDsa.seed4 = Spec.MlKem.seed4 := rfl theorem poly4_eq : Spec.MlDsa.poly4 = Spec.MlKem.poly4 := rfl @@ -45,11 +47,62 @@ theorem r4_post {s s' : State} (h : r4K.post s s') : obtain ⟨k, hk, hk'⟩ := hall exact ⟨k, hk, rejNTT_none (B := 1008) (by decide) (by decide) hk'⟩ +theorem r4_pre (s : State) (h : (Spec.MlDsa.rejNTT4Contract X86_64.abi 24).pre s) : r4K.pre s := by + revert s h + sig_implies_pre [Spec.MlDsa.rejNTT4Contract, Spec.MlDsa.rejNTT4Sig, r4K, MlKem.X86_64.sample4K, X86_64.abi, + X86_64.argRegs] + +/-- The result of either implementation: whether each seed has 256 coefficients in its first 1008 +bytes of output. -/ +def rej4Res (m : Mem) (a : Addr) : BitVec 32 := + if (List.range 4).all (fun k => (rnFold [] (G (Spec.MlDsa.seed4 m a k) 1008)).length == 256) then 1 else 0 + +theorem seed4_of136 {m m' : Mem} {a a' : Addr} (h : bytesAt m a 136 = bytesAt m' a' 136) {k : Nat} (hk : k < 4) : + Spec.MlDsa.seed4 m a k = Spec.MlDsa.seed4 m' a' k := by + unfold Spec.MlDsa.seed4 + rw [← Proof.MlKem.bytesAt_slice m a (show 34 * k + 34 ≤ 136 by omega), + ← Proof.MlKem.bytesAt_slice m' a' (show 34 * k + 34 ≤ 136 by omega), h] + +/-- The result depends only on the 136 bytes of the seeds. -/ +theorem rej4Res_congr {m m' : Mem} {a a' : Addr} (h : bytesAt m a 136 = bytesAt m' a' 136) : + rej4Res m a = rej4Res m' a' := by + have e : ((List.range 4).all fun k => (rnFold [] (G (Spec.MlDsa.seed4 m a k) 1008)).length == 256) = + ((List.range 4).all fun k => (rnFold [] (G (Spec.MlDsa.seed4 m' a' k) 1008)).length == 256) := by + rw [Bool.eq_iff_iff, List.all_eq_true, List.all_eq_true] + exact ⟨fun H k hk => by rw [← seed4_of136 h (List.mem_range.mp hk)]; exact H k hk, + fun H k hk => by rw [seed4_of136 h (List.mem_range.mp hk)]; exact H k hk⟩ + simp only [rej4Res, e] + +/-- The public data of two calls include their seeds. -/ +theorem r4_pub {S : Nat} (s₁ s₂ : State) (h : (Spec.MlDsa.rejNTT4Contract X86_64.abi S).pub s₁ s₂) : + bytesAt s₁.mem (s₁.gpr .rdi) 136 = bytesAt s₂.mem (s₂.gpr .rdi) 136 := by + sig_pub [Spec.MlDsa.rejNTT4Contract, Spec.MlDsa.rejNTT4Sig, X86_64.abi, X86_64.argRegs] at h + obtain ⟨_, hb, _⟩ := h + exact leakBytes_inj hb + +/-- Within the bound both implementations sample to, so within `maxBounds`'s. -/ +theorem rej4Res_max {m : Mem} {a : Addr} (h : rej4Res m a = 1) {k : Nat} (hk : k < 4) {B : Nat} (hB : 1008 ≤ B) : + (Spec.MlDsa.rejNTTPoly B (Spec.MlDsa.seed4 m a k)).isSome := by + unfold rej4Res at h + by_cases hall : ((List.range 4).all fun k => (rnFold [] (G (Spec.MlDsa.seed4 m a k) 1008)).length == 256) = true + · have hs : (rnFold [] (G (Spec.MlDsa.seed4 m a k) 1008)).length = 256 := by + simpa using List.all_eq_true.mp hall k (List.mem_range.mpr hk) + rw [Proof.MlDsa.KeyGen.rejNTTPoly_mono hB (rejNTT_some hs)]; rfl + · rw [ite_eq_right hall] at h; exact absurd h (by decide) + +/-- The result of code that meets `r4K`. -/ +theorem rej4_ret {c : Prog isa} + (hc : ∀ σ, r4K.pre σ → ∃ t s', Exec isa c σ t s' ∧ abiPreserved σ s' ∧ r4K.post σ s') {s s' : State} + {t : List Leak} (h : (Spec.MlDsa.rejNTT4Contract X86_64.abi 24).pre s) (e : Exec isa c s t s') : + (s'.gpr .rax).setWidth 32 = rej4Res s.mem (s.gpr .rdi) := by + obtain ⟨_, _, e', _, hq⟩ := hc s (r4_pre s h) + obtain ⟨-, rfl⟩ := Exec.det e e' + exact hq.1 + theorem rej4_verified (c : Prog isa) (hc : ∀ σ, r4K.pre σ → ∃ t s', Exec isa c σ t s' ∧ abiPreserved σ s' ∧ r4K.post σ s') (ht : ConstantTime isa r4K.pre r4K.pub c) : Verified X86_64.target c (Spec.MlDsa.rejNTT4Contract X86_64.abi 24) := Verified.of_correct hc ht - { pre := by sig_implies_pre [Spec.MlDsa.rejNTT4Contract, Spec.MlDsa.rejNTT4Sig, r4K, MlKem.X86_64.sample4K, - X86_64.abi, X86_64.argRegs] + { pre := r4_pre post := by intro s s' _ h sig_post [Spec.MlDsa.rejNTT4Contract, Spec.MlDsa.rejNTT4Sig, r4K, X86_64.abi, X86_64.argRegs] @@ -76,4 +129,12 @@ theorem rejNTT4Avx2_verified : Verified X86_64.target Impl.MlDsa.X86_64.Sample.R theorem rejNTT4_verified : Verified X86_64.target Impl.MlDsa.X86_64.Sample.Rej4.rejNTT4 (Spec.MlDsa.rejNTT4Contract X86_64.abi 24) := rej4_verified _ correct_scalar ct_scalar +theorem rejNTT4Avx2_ret {s s' : State} {t : List Leak} (h : (Spec.MlDsa.rejNTT4Contract X86_64.abi 24).pre s) + (e : Exec isa Impl.MlDsa.X86_64.Sample.Rej4.rejNTT4Avx2 s t s') : + (s'.gpr .rax).setWidth 32 = rej4Res s.mem (s.gpr .rdi) := rej4_ret correct h e + +theorem rejNTT4_ret {s s' : State} {t : List Leak} (h : (Spec.MlDsa.rejNTT4Contract X86_64.abi 24).pre s) + (e : Exec isa Impl.MlDsa.X86_64.Sample.Rej4.rejNTT4 s t s') : + (s'.gpr .rax).setWidth 32 = rej4Res s.mem (s.gpr .rdi) := rej4_ret correct_scalar h e + end VG.Proof.MlDsa.X86_64.Rej4 diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Inst.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Inst.lean index 938cf8fa4..87bab372b 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Inst.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Inst.lean @@ -19,8 +19,8 @@ import VerifiedGarbage.Proof.MlDsa.X86_64.Arith.Backend Untrusted: everything here is checked by Lean. The verified x86-64 implementations of the primitives (`prims`), and what the proofs of signing need of them, with any implementation `v` of the polynomial arithmetic -(`prims_okWith`), with 24 bytes of stack for each call: their -contracts, and, of the two samplers whose result signing branches on, that +(`prims_okWith`), with 32 bytes of stack for each call: their +contracts, and, of the samplers whose result signing branches on, that it depends only on their public data and that they succeed only if the algorithm finishes within `maxBounds` (from what their own proofs say they return, `rejNTT_correct` and `sampleInBall_correct`). @@ -53,6 +53,7 @@ def prims : Prims where bitPack := Impl.MlDsa.X86_64.Pack.bitPack bitUnpack := Impl.MlDsa.X86_64.Pack.bitUnpack hintBitPack := Impl.MlDsa.X86_64.Pack.hintBitPack + rej4 := Impl.MlDsa.X86_64.Sample.Rej4.rejNTT4 /-- The primitives, with the polynomial arithmetic of `B`. -/ def primsWith (B : Impl.MlDsa.X86_64.Arith.Backend) : Prims := @@ -63,6 +64,7 @@ def primsWith (B : Impl.MlDsa.X86_64.Arith.Backend) : Prims := mulAdd := B.mulAdd add := B.add sub := B.sub + rej4 := B.rej4 highBits := B.highBits lowBits := B.lowBits normLt := B.normLt @@ -75,7 +77,7 @@ theorem nosp_of {c : Prog isa} (h : c.allInstrs (fun i => !Taint.clobbers i .rsp simpa using List.all_eq_true.mp h i hi /-- The stack signing gives each call. -/ -abbrev signStack : Nat := 24 +abbrev signStack : Nat := 32 /-! ## The samplers' results -/ @@ -168,6 +170,18 @@ def prims_okWith (v : ArithImpl) : PrimsOk (primsWith v.code) signStack where by_cases hf : (VG.Proof.MlDsa.Sample.rnFold [] (G (bytesAt s.mem (s.gpr .rdi) 34) 1008)).length = 256 · rw [rejNTTPoly_mono (show 1008 ≤ maxBounds.rejNTT by decide) (VG.Proof.MlDsa.Sample.rejNTT_some hf)]; rfl · rw [ifn hf] at h1; exact absurd h1.symm one_ne_zero32 + rej4 := ⟨24, by decide, v.ok.rej4.ver, v.ok.rej4.nosp, by + have := v.ok.rej4.depth + show 8 * (v.code.rej4.depth + 1) ≤ signStack + unfold signStack; omega⟩ + rej4Ret := fun s₁ s₂ t₁ t₂ s₁' s₂' ⟨h₁, h₂, hp⟩ e₁ e₂ => + ⟨v.ok.rej4.ver.2.1 s₁ s₂ t₁ t₂ s₁' s₂' h₁ h₂ hp e₁ e₂, + show _ = _ by + rw [v.ok.rej4.ret _ _ _ h₁ e₁, v.ok.rej4.ret _ _ _ h₂ e₂] + exact Proof.MlDsa.X86_64.Rej4.rej4Res_congr (Proof.MlDsa.X86_64.Rej4.r4_pub s₁ s₂ hp)⟩ + rej4Max := fun s t s' h e h1 k hk => by + rw [v.ok.rej4.ret _ _ _ h e] at h1 + exact Proof.MlDsa.X86_64.Rej4.rej4Res_max h1 hk (by decide) ballRet := fun s₁ s₂ t₁ t₂ s₁' s₂' ⟨h₁, h₂, hp⟩ e₁ e₂ => ⟨Proof.MlDsa.X86_64.Sample.sampleInBall_verified.2.1 s₁ s₂ t₁ t₂ s₁' s₂' h₁ h₂ hp e₁ e₂, show _ = _ by rw [sb_ret h₁ e₁, sb_ret h₂ e₂, (sb_pub s₁ s₂ hp).1, (sb_pub s₁ s₂ hp).2]⟩ diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA.lean index 76def5f74..5e9c8b5b1 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA.lean @@ -9,7 +9,7 @@ Untrusted: everything here is checked by Lean. `ρ` to `RS`, then entry `e = ℓi + j` of `Â` by `vg_mldsa_rej_ntt_poly` from the seed `ρ ‖ j ‖ i`, with `r15` the AND of the results (`IA`): if it is 1, every entry so far is `RejNTTPoly`'s within `maxBounds`; if it is 0, one entry's -`RejNTTPoly` does not finish within `minBounds` (`expandA_ok`). +`RejNTTPoly` does not finish within `minBounds` (`sampleE_ok`). -/ namespace VG.Proof.MlDsa.X86_64.Sign @@ -213,29 +213,4 @@ theorem sampleE_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {σ : S exact WP.seq (WP.mono (blkE_ok he h) fun s1 ⟨⟨h1, hs1⟩, _⟩ => WP.seq (WP.mono (callE_ok hP he h1 hs1) fun s2 h2 => andE_ok he h2)) -/-! ## The matrix -/ - -/-- What `ExpandA` needs of the layout. -/ -def aChk (p : Params) : Bool := - (List.range (p.k * p.ℓ)).all (eChk p) && copyChk (sgB p) (sgW p) (sc oRS) (.rbp, 0) 32 && - stChk p [(sc oRS, 32)] && decide (32 ≤ p.skLen) - -theorem aChk_ok {p : Params} (h : Ok3 p) : aChk p = true := by - rcases h with rfl | rfl | rfl <;> decide - -theorem expandA_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} (hc : aChk p = true) {σ s : State} - (hs : St p D σ s) (h15 : s.gpr .r15 = 1) : WP isa (Impl.MlDsa.X86_64.Sign.expandA P p) s (IA p D σ (p.k * p.ℓ)) := by - simp only [aChk, Bool.and_eq_true, List.all_eq_true, List.mem_range, decide_eq_true_eq] at hc - obtain ⟨⟨⟨he, hcp⟩, hst⟩, hsk⟩ := hc - unfold Impl.MlDsa.X86_64.Sign.expandA - refine WP.seq (WP.mono (copy_okB hs.lay hcp) fun s1 ⟨hP1, hcs1, hb⟩ => ?_) - have S1 := hs.step hP1 hst - have e15 : s1.gpr .r15 = 1 := by rw [hcs1 _ (by decide), h15] - have I0 : IA p D σ 0 s1 := ⟨S1, by rw [hP1.pa (by decide), hb, rhoOf, ← hs.sk, VG.Proof.MlKem.bytesAt_take _ _ hsk], - .inr e15, fun _ => ⟨fun _ h => absurd h (Nat.not_lt_zero _), fun _ h => absurd h (Nat.not_lt_zero _)⟩, - fun h0 => absurd (h0.symm.trans e15) (by decide)⟩ - have := seqR_ok (f := sampleE P p) (I := IA p D σ) (p.k * p.ℓ) 0 - (fun k _ hk s h => sampleE_ok hP (he k (by omega)) h) s1 I0 - rwa [Nat.zero_add] at this - end VG.Proof.MlDsa.X86_64.Sign diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA4.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA4.lean new file mode 100644 index 000000000..a1620ee68 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseA4.lean @@ -0,0 +1,284 @@ +import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PhaseA + +/-! +# ML-DSA signing on x86-64: `ExpandA`, four entries at a time + +Untrusted: everything here is checked by Lean. `ρ` to `RS` and to each of +the four seeds at `RS4` (`IA4`); then, for each group of four entries +`4g, …, 4g + 3`, their indices to the seeds (`GS`, `slot_ok`) and one call +of `vg_mldsa_rej_ntt_poly4`, ANDed into `r15` (`call4_ok`); then the last +`kℓ mod 4` entries one at a time (`sampleE_ok`). Each step keeps `IA` +(`expandA_ok`). +-/ + +namespace VG.Proof.MlDsa.X86_64.Sign + +open VG VG.X86_64 VG.Impl.MlDsa.X86_64.Sign +open VG.Proof.MlKem.X86_64 (Keep Keep.gpr WP.keep) +open VG.Proof.MlDsa.Sign +open VG.Spec.MlDsa +open VG.Spec.Sha3 (bytesAt) + +/-- `ExpandA` after `e` entries, with `ρ` in each seed of `RS4`. -/ +structure IA4 (p : Params) (D : Nat) (σ : State) (e : Nat) (s : State) : Prop where + ia : IA p D σ e s + rs4 : ∀ k < 4, bytesAt s.mem (pa s (sc (oRS4 + 34 * k))) 32 = rhoOf p σ + +/-- … and the seeds of entries `e, …, e + j - 1` in the first `j` seeds. -/ +structure GS (p : Params) (D : Nat) (σ : State) (e j : Nat) (s : State) : Prop where + ia4 : IA4 p D σ e s + done : ∀ k < j, bytesAt s.mem (pa s (sc (oRS4 + 34 * k))) 34 = seedE p σ (e + k) + +/-! ## Pieces that keep `IA` -/ + +theorem IA.step {p : Params} {D : Nat} {σ : State} {e : Nat} {s s' : State} (h : IA p D σ e s) + {ws : List (Ptr × Nat)} (hP : PPostB D s s' ws) (hst : stChk p ws = true) (hk : keepB (sgB p) ws (sc oRS) 32 = true) + (hf : famChk (sgB p) ws (aBase p) e = true) (e15 : s'.gpr .r15 = s.gpr .r15) : IA p D σ e s' := by + refine ⟨h.st.step hP hst, (h.st.lay.keepBytes hP hk).trans h.rs, by rw [e15]; exact h.r01, fun h1 => ?_, + fun h0 => h.bad (by rw [← e15]; exact h0)⟩ + obtain ⟨ok, fam⟩ := h.ok (by rw [← e15]; exact h1) + exact ⟨ok, Fam.keep h.st.lay hP hf fam⟩ + +/-- The seeds of `RS4` apart from `ws`. -/ +def rs4Chk (p : Params) (ws : List (Ptr × Nat)) (n : Nat) : Bool := + (List.range 4).all fun k => keepB (sgB p) ws (sc (oRS4 + 34 * k)) n + +theorem rs4Chk_spec {p : Params} {ws : List (Ptr × Nat)} {n : Nat} (h : rs4Chk p ws n = true) {k : Nat} + (hk : k < 4) : keepB (sgB p) ws (sc (oRS4 + 34 * k)) n = true := + List.all_eq_true.mp h k (List.mem_range.mpr hk) + +theorem IA4.step {p : Params} {D : Nat} {σ : State} {e : Nat} {s s' : State} (h : IA4 p D σ e s) + {ws : List (Ptr × Nat)} (hP : PPostB D s s' ws) (hst : stChk p ws = true) (hk : keepB (sgB p) ws (sc oRS) 32 = true) + (hf : famChk (sgB p) ws (aBase p) e = true) (h4 : rs4Chk p ws 32 = true) (e15 : s'.gpr .r15 = s.gpr .r15) : + IA4 p D σ e s' := + ⟨h.ia.step hP hst hk hf e15, fun k hk => (h.ia.st.lay.keepBytes hP (rs4Chk_spec h4 hk)).trans (h.rs4 k hk)⟩ + +/-! ## The seeds of a group -/ + +/-- What seed `j` of entry `e + j` needs of the layout. -/ +def slotChk (p : Params) (e j : Nat) : Bool := + let w1 : List (Ptr × Nat) := [(sc (oRS4 + 34 * j + 32), 1)] + let w2 : List (Ptr × Nat) := [(sc (oRS4 + 34 * j + 33), 1)] + stChk p w1 && stChk p w2 && inB (sgW p) (sc (oRS4 + 34 * j + 32)) 1 && inB (sgW p) (sc (oRS4 + 34 * j + 33)) 1 && + keepB (sgB p) w1 (sc oRS) 32 && keepB (sgB p) w2 (sc oRS) 32 && famChk (sgB p) w1 (aBase p) e && + famChk (sgB p) w2 (aBase p) e && rs4Chk p w1 32 && rs4Chk p w2 32 && + keepB (sgB p) w2 (sc (oRS4 + 34 * j + 32)) 1 && + (List.range j).all (fun k => keepB (sgB p) w1 (sc (oRS4 + 34 * k)) 34 && keepB (sgB p) w2 (sc (oRS4 + 34 * k)) 34) && + decide ((e + j) % p.ℓ < 256) && decide ((e + j) / p.ℓ < 256) + +theorem slot_ok {p : Params} {D : Nat} {σ : State} {e j : Nat} (hj4 : j < 4) (hc : slotChk p e j = true) {s : State} + (h : GS p D σ e j s) : WP isa (.block (setSR p e j)) s fun s' => GS p D σ e (j + 1) s' ∧ s'.gpr .r15 = s.gpr .r15 := by + simp only [slotChk, Bool.and_eq_true, decide_eq_true_eq] at hc + obtain ⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨c1, c2⟩, w1⟩, w2⟩, k1⟩, k2⟩, f1⟩, f2⟩, r1⟩, r2⟩, k12⟩, kd⟩, hj⟩, hi⟩ := hc + have L := h.ia4.ia.st.lay + unfold setSR + rw [WP.block_append_iff] + refine WP.mono (setB_okB L (show Reg.rbx ≠ .rax by decide) hj w1) fun s1 ⟨hP1, hcs1, hm1⟩ => ?_ + have e1 : s1.gpr .r15 = s.gpr .r15 := hcs1 _ (by decide) + have I1 := h.ia4.step hP1 c1 k1 f1 r1 e1 + refine WP.mono (setB_okB I1.ia.st.lay (show Reg.rbx ≠ .rax by decide) hi w2) fun s2 ⟨hP2, hcs2, hm2⟩ => ?_ + have e2 : s2.gpr .r15 = s1.gpr .r15 := hcs2 _ (by decide) + have I2 := I1.step hP2 c2 k2 f2 r2 e2 + refine ⟨⟨I2, fun k hk => ?_⟩, e2.trans e1⟩ + rcases (by omega : k < j ∨ k = j) with hk' | rfl + · have kk := List.all_eq_true.mp kd k (List.mem_range.mpr hk') + simp only [Bool.and_eq_true] at kk + rw [I1.ia.st.lay.keepBytes hP2 kk.2, L.keepBytes hP1 kk.1] + exact h.done k hk' + · refine seed34 (I2.rs4 k (by omega)) ?_ ?_ + · rw [pa_sc_add, I1.ia.st.lay.keepBytes hP2 k12, hm1, hP1.pa (show Reg.rbx ∈ bases by decide)]; exact bytes1_write _ _ _ + · rw [pa_sc_add, hm2, hP2.pa (show Reg.rbx ∈ bases by decide)]; exact bytes1_write _ _ _ + +/-! ## The call -/ + +theorem pa_poly4 (s : State) (i k : Nat) : poly4 (pa s (pS i)) k = pa s (pS (i + k)) := by + unfold poly4 + rw [pa_sc_add, show oP i + 1024 * k = oP (i + k) by simp only [oP]; omega] + +theorem seed4_eq {p : Params} {D : Nat} {σ : State} {e : Nat} {s : State} (h : GS p D σ e 4 s) {k : Nat} + (hk : k < 4) : seed4 s.mem (pa s (sc oRS4)) k = seedE p σ (e + k) := by + unfold seed4 + rw [pa_sc_add]; exact h.done k hk + +/-- What the call of a group needs of the layout. -/ +def callChk (p : Params) (e : Nat) : Bool := + let w3 : List (Ptr × Nat) := [(pS (aBase p + e), 4096), (r4P p, 8192)] + stChk p w3 && stChk p [] && keepB (sgB p) w3 (sc oRS) 32 && rs4Chk p w3 32 && famChk (sgB p) w3 (aBase p) e && + rej4Chk (sgB p) (sgW p) (pS (aBase p + e)) (r4P p) + +/-- What the call of group `e` leaves. -/ +abbrev R4Post (D : Nat) (a w : Ptr) (s s' : State) : Prop := + PPostB D s s' [(a, 4096), (w, 8192)] ∧ (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) ∧ + ((s'.gpr .rax).setWidth 32 = 1 → ∀ k < 4, Reduced s'.mem (poly4 (pa s a) k)) ∧ + (((s'.gpr .rax).setWidth 32 = 1 ∧ ∀ k < 4, ∃ b : Bounds, + rejNTTPoly b.rejNTT (seed4 s.mem (pa s (sc oRS4)) k) = some (polyAt s'.mem (poly4 (pa s a) k))) ∨ + ((s'.gpr .rax).setWidth 32 = 0 ∧ ∃ k < 4, + rejNTTPoly minBounds.rejNTT (seed4 s.mem (pa s (sc oRS4)) k) = none)) ∧ + ((s'.gpr .rax).setWidth 32 = 1 → ∀ k < 4, + (rejNTTPoly maxBounds.rejNTT (seed4 s.mem (pa s (sc oRS4)) k)).isSome) + +/-- The call of group `e` is done. -/ +def J4 (p : Params) (D e : Nat) (σ s : State) : Prop := + ∃ s₀, GS p D σ e 4 s₀ ∧ R4Post D (pS (aBase p + e)) (r4P p) s₀ s + +theorem callG_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {σ : State} {e : Nat} + (hc : callChk p e = true) {s : State} (h : GS p D σ e 4 s) : + WP isa (callP ("vg_mldsa_rej_ntt_poly4" ++ P.sfx) P.rej4 [.ptr (sc oRS4), .ptr (pS (aBase p + e)), .ptr (r4P p)]) s + fun s' => J4 p D e σ s' ∧ s'.gpr .r15 = s.gpr .r15 := by + simp only [callChk, Bool.and_eq_true] at hc + exact WP.mono (rej4Call_ok hP h.ia4.ia.st.lay hc.2) fun s' h' => ⟨⟨s, h, h'⟩, h'.2.1 _ (by decide)⟩ + +theorem and4_ok {p : Params} {D : Nat} {σ : State} {e : Nat} (hc : callChk p e = true) {s : State} + (hJ : J4 p D e σ s) : WP isa (.block [.alu32 .and .r15 (.reg .rax)]) s (IA4 p D σ (e + 4)) := by + simp only [callChk, Bool.and_eq_true] at hc + obtain ⟨⟨⟨⟨⟨c3, c0⟩, k3⟩, r3⟩, f3⟩, _⟩ := hc + obtain ⟨s₀, h, hP3, hcs3, hred, hout, hmax⟩ := hJ + have L := h.ia4.ia.st.lay + have I1 := h.ia4.step hP3 c3 k3 f3 r3 (hcs3 _ (by decide)) + refine WP.mono (and15_ok s) fun s4 ⟨h15, hm4, k4⟩ => ?_ + have hP4 : PPostB D s s4 [] := (postB15 k4 hm4 _).1 + rw [hcs3 _ (by decide)] at h15 + have hr : (s.gpr .rax).setWidth 32 = 1 ∨ (s.gpr .rax).setWidth 32 = 0 := by + rcases hout with ⟨h1, _⟩ | ⟨h0, _⟩ + exacts [.inl h1, .inr h0] + have hb4 : s4.gpr .rbx = s₀.gpr .rbx := by rw [hP4.bs _ (by decide), hP3.bs _ (by decide)] + have epa : ∀ q : Ptr, q.1 = .rbx → pa s4 q = pa s₀ q := fun q hq => by simp only [pa, hq, hb4] + have hia := h.ia4.ia + refine ⟨⟨I1.ia.st.step hP4 c0, ?_, ?_, fun h1 => ?_, fun h0 => ?_⟩, fun k hk => ?_⟩ + · rw [hm4, epa _ rfl, ← hP3.pa (by decide), I1.ia.rs] + · rw [h15] + rcases hia.r01 with e0 | e0 <;> rcases hr with e1 | e1 <;> rw [e0, e1] <;> decide + · have hs : s₀.gpr .r15 = 1 ∧ (s.gpr .rax).setWidth 32 = 1 := by + rw [h15] at h1 + rcases hia.r01 with e0 | e0 <;> rcases hr with e1 | e1 <;> rw [e0, e1] at h1 <;> + first | exact ⟨e0, e1⟩ | exact absurd h1 (by decide) + obtain ⟨ok1, fam⟩ := hia.ok hs.1 + have hm := hmax hs.2 + refine ⟨fun e' he' => ?_, fun j hj => ?_⟩ + · by_cases he'' : e' < e + · exact ok1 e' he'' + · obtain ⟨k, hk, rfl⟩ : ∃ k, k < 4 ∧ e' = e + k := ⟨e' - e, by omega, by omega⟩ + rw [← seed4_eq h hk]; exact hm k hk + · by_cases hj' : j < e + · exact Fam.of_eq hm4 (hP4.bs _ (by decide)) (Fam.keep L hP3 f3 fam) j hj' + · obtain ⟨k, hk, rfl⟩ : ∃ k, k < 4 ∧ j = e + k := ⟨j - e, by omega, by omega⟩ + show PolyIs s4.mem (pa s4 (pS (aBase p + (e + k)))) (aVal p σ (e + k)) + rw [hm4, epa _ rfl, ← Nat.add_assoc, ← pa_poly4] + rcases hout with ⟨_, hb⟩ | ⟨h0, _⟩ + · refine ⟨hred hs.2 k hk, ?_⟩ + have := rej_val (x := seed4 s₀.mem (pa s₀ (sc oRS4)) k) (.inl ⟨hs.2, hb k hk⟩) hs.2 (hm k hk) + rw [this, seed4_eq h hk]; rfl + · rw [hs.2] at h0; cases h0 + · rw [h15] at h0 + rcases hia.r01 with e0 | e0 + · obtain ⟨e', he', hn⟩ := hia.bad e0 + exact ⟨e', by omega, hn⟩ + · rcases hr with e1 | e1 + · rw [e0, e1] at h0; exact absurd h0 (by decide) + · rcases hout with ⟨h1, _⟩ | ⟨_, k, hk, hn⟩ + · rw [e1] at h1; cases h1 + · exact ⟨e + k, by omega, by rw [← seed4_eq h hk]; exact hn⟩ + · rw [hm4, epa _ rfl, ← hP3.pa (show Reg.rbx ∈ bases by decide)]; exact I1.rs4 k hk + +theorem call4_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {σ : State} {e : Nat} + (hc : callChk p e = true) {s : State} (h : GS p D σ e 4 s) : + WP isa (rej4At P (pS (aBase p + e)) (r4P p)) s (IA4 p D σ (e + 4)) := by + unfold rej4At + exact WP.seq (WP.mono (callG_ok hP hc h) fun _ h' => and4_ok hc h'.1) + +theorem bytes136 (m : Mem) (P : Addr) : bytesAt m P 136 = bytesAt m P 34 ++ bytesAt m (P + BitVec.ofNat 64 34) 34 ++ + bytesAt m (P + BitVec.ofNat 64 68) 34 ++ bytesAt m (P + BitVec.ofNat 64 102) 34 := by + rw [show 136 = 34 + 102 from rfl, VG.Proof.MlKem.bytesAt_add, show 102 = 34 + 68 from rfl, + VG.Proof.MlKem.bytesAt_add, show 68 = 34 + 34 from rfl, VG.Proof.MlKem.bytesAt_add] + simp only [BitVec.add_assoc, ← BitVec.ofNat_add, List.append_assoc, Nat.reduceAdd] + +/-- The four seeds of a group, from `ρ`. -/ +theorem GS.seeds {p : Params} {D : Nat} {σ : State} {e : Nat} {s : State} (h : GS p D σ e 4 s) : + bytesAt s.mem (pa s (sc oRS4)) 136 = aSeed (rhoOf p σ) ((e + 0) / p.ℓ) ((e + 0) % p.ℓ) ++ + aSeed (rhoOf p σ) ((e + 1) / p.ℓ) ((e + 1) % p.ℓ) ++ aSeed (rhoOf p σ) ((e + 2) / p.ℓ) ((e + 2) % p.ℓ) ++ + aSeed (rhoOf p σ) ((e + 3) / p.ℓ) ((e + 3) % p.ℓ) := by + have b : ∀ k < 4, bytesAt s.mem (pa s (sc oRS4) + BitVec.ofNat 64 (34 * k)) 34 = seedE p σ (e + k) := + fun k hk => seed4_eq h hk + have b0 := b 0 (by decide) + rw [show 34 * 0 = 0 from rfl, BitVec.add_zero] at b0 + rw [bytes136, b0, b 1 (by decide), b 2 (by decide), b 3 (by decide)] + +/-- What a group needs of the layout. -/ +def g4Chk (p : Params) (e : Nat) : Bool := + slotChk p e 0 && slotChk p e 1 && slotChk p e 2 && slotChk p e 3 && callChk p e + +theorem sample4_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {σ : State} {g : Nat} + (hc : g4Chk p (4 * g) = true) {s : State} (h : IA4 p D σ (4 * g) s) : + WP isa (sample4 P p g) s (IA4 p D σ (4 * g + 4)) := by + simp only [g4Chk, Bool.and_eq_true] at hc + obtain ⟨⟨⟨⟨s0, s1⟩, s2⟩, s3⟩, cc⟩ := hc + unfold sample4 + refine WP.seq (WP.mono (slot_ok (by decide) s0 (j := 0) ⟨h, fun _ h => absurd h (Nat.not_lt_zero _)⟩) fun x0 h0 => ?_) + refine WP.seq (WP.mono (slot_ok (by decide) s1 h0.1) fun x1 h1 => ?_) + refine WP.seq (WP.mono (slot_ok (by decide) s2 h1.1) fun x2 h2 => ?_) + refine WP.seq (WP.mono (slot_ok (by decide) s3 h2.1) fun x3 h3 => ?_) + exact call4_ok hP cc h3.1 + +/-! ## The matrix -/ + +/-- `ρ` to `sc o`. -/ +theorem copyRho_ok {p : Params} {D : Nat} {σ : State} {o : Nat} + (hc : copyChk (sgB p) (sgW p) (sc o) (.rbp, 0) 32 = true) (hst : stChk p [(sc o, 32)] = true) (hsk : 32 ≤ p.skLen) + {s : State} (hs : St p D σ s) : + WP isa (copy (sc o) (.rbp, 0) 32) s fun s' => St p D σ s' ∧ PPostB D s s' [(sc o, 32)] ∧ + bytesAt s'.mem (pa s' (sc o)) 32 = rhoOf p σ ∧ s'.gpr .r15 = s.gpr .r15 := + WP.mono (copy_okB hs.lay hc) fun _ ⟨hP1, hcs1, hb⟩ => ⟨hs.step hP1 hst, hP1, + by rw [hP1.pa (show Reg.rbx ∈ bases by decide), hb, rhoOf, ← hs.sk, VG.Proof.MlKem.bytesAt_take _ _ hsk], hcs1 _ (by decide)⟩ + +/-- After `ρ` to `RS` and to the first `j` seeds of `RS4`. -/ +structure ICopy (p : Params) (D : Nat) (σ : State) (j : Nat) (s : State) : Prop where + st : St p D σ s + rs : bytesAt s.mem (pa s (sc oRS)) 32 = rhoOf p σ + rs4 : ∀ k < j, bytesAt s.mem (pa s (sc (oRS4 + 34 * k))) 32 = rhoOf p σ + r15 : s.gpr .r15 = 1 + +/-- What the copy of `ρ` to seed `j` of `RS4` needs of the layout. -/ +def cpChk (p : Params) (j : Nat) : Bool := + copyChk (sgB p) (sgW p) (sc (oRS4 + 34 * j)) (.rbp, 0) 32 && stChk p [(sc (oRS4 + 34 * j), 32)] && + keepB (sgB p) [(sc (oRS4 + 34 * j), 32)] (sc oRS) 32 && + (List.range j).all fun k => keepB (sgB p) [(sc (oRS4 + 34 * j), 32)] (sc (oRS4 + 34 * k)) 32 + +theorem cpR4_ok {p : Params} {D : Nat} {σ : State} {j : Nat} (hc : cpChk p j = true) (hsk : 32 ≤ p.skLen) {s : State} + (h : ICopy p D σ j s) : WP isa (cpR4 j) s (ICopy p D σ (j + 1)) := by + simp only [cpChk, Bool.and_eq_true] at hc + obtain ⟨⟨⟨hcp, hst⟩, k0⟩, kk⟩ := hc + refine WP.mono (copyRho_ok hcp hst hsk h.st) fun s1 ⟨S1, hP1, hb, e15⟩ => + ⟨S1, (h.st.lay.keepBytes hP1 k0).trans h.rs, fun k hk => ?_, e15.trans h.r15⟩ + rcases (by omega : k < j ∨ k = j) with hk' | rfl + · exact (h.st.lay.keepBytes hP1 (List.all_eq_true.mp kk k (List.mem_range.mpr hk'))).trans (h.rs4 k hk') + · exact hb + +/-- What `ExpandA` needs of the layout. -/ +def aChk (p : Params) : Bool := + (List.range (p.k * p.ℓ)).all (eChk p) && copyChk (sgB p) (sgW p) (sc oRS) (.rbp, 0) 32 && + stChk p [(sc oRS, 32)] && decide (32 ≤ p.skLen) && (List.range 4).all (cpChk p) && + (List.range (p.k * p.ℓ / 4)).all fun g => g4Chk p (4 * g) + +theorem aChk_ok {p : Params} (h : Ok3 p) : aChk p = true := by + rcases h with rfl | rfl | rfl <;> decide + +theorem ICopy.ia4 {p : Params} {D : Nat} {σ s : State} (h : ICopy p D σ 4 s) : IA4 p D σ 0 s := + ⟨⟨h.st, h.rs, .inr h.r15, fun _ => ⟨fun _ h => absurd h (Nat.not_lt_zero _), fun _ h => absurd h (Nat.not_lt_zero _)⟩, + fun h0 => absurd (h0.symm.trans h.r15) (by decide)⟩, h.rs4⟩ + +theorem expandA_ok {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} (hc : aChk p = true) {σ s : State} + (hs : St p D σ s) (h15 : s.gpr .r15 = 1) : WP isa (Impl.MlDsa.X86_64.Sign.expandA P p) s (IA p D σ (p.k * p.ℓ)) := by + simp only [aChk, Bool.and_eq_true, List.all_eq_true, List.mem_range, decide_eq_true_eq] at hc + obtain ⟨⟨⟨⟨⟨he, hcp⟩, hst⟩, hsk⟩, hc4⟩, hg⟩ := hc + unfold Impl.MlDsa.X86_64.Sign.expandA + refine WP.seq (WP.mono (copyRho_ok hcp hst hsk hs) fun s1 ⟨S1, _, hb, e15⟩ => ?_) + have I0 : ICopy p D σ 0 s1 := ⟨S1, hb, fun _ h => absurd h (Nat.not_lt_zero _), e15.trans h15⟩ + refine WP.seq (WP.mono (seqR_ok (f := cpR4) (I := ICopy p D σ) 4 0 + (fun k _ hk s h => cpR4_ok (hc4 k (by omega)) hsk h) s1 I0) fun s2 h2 => ?_) + refine WP.seq (WP.mono (seqR_ok (f := sample4 P p) (I := fun g => IA4 p D σ (4 * g)) (p.k * p.ℓ / 4) 0 + (fun g _ hg' s h => sample4_ok hP (hg g (by omega)) h) s2 h2.ia4) fun s3 h3 => ?_) + have := seqR_ok (f := sampleE P p) (I := IA p D σ) (p.k * p.ℓ % 4) (4 * (p.k * p.ℓ / 4)) + (fun k h1 hk s h => sampleE_ok hP (he k (by omega)) h) s3 (by rw [Nat.zero_add] at h3; exact h3.ia) + rwa [show 4 * (p.k * p.ℓ / 4) + p.k * p.ℓ % 4 = p.k * p.ℓ by omega] at this + +end VG.Proof.MlDsa.X86_64.Sign diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseACT.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseACT.lean index b18950110..3969c33db 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseACT.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseACT.lean @@ -4,8 +4,9 @@ import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.Rel # ML-DSA signing on x86-64: `ExpandA` leaks only `ρ` Untrusted: everything here is checked by Lean. Two runs of `ExpandA` with -the same `ρ` compute the same results of `vg_mldsa_rej_ntt_poly`, so they -agree on `r15` (`RA`), and leak the same (`expandA_tr`). +the same `ρ` compute the same results of `vg_mldsa_rej_ntt_poly` and +`vg_mldsa_rej_ntt_poly4`, so they agree on `r15` (`RA`), and leak the same +(`expandA_tr`). -/ namespace VG.Proof.MlDsa.X86_64.Sign @@ -51,29 +52,87 @@ theorem sampleE_tr {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {e : Na (block_nomem_tr (fun i hi s => by simp only [List.mem_singleton] at hi; subst hi; rfl)) fun x y x' y' h fx fy _ => by rw [fx, fy, h.2.1, h.2.2] +/-! ## Four entries at a time -/ + +/-- Two runs in a group, after the seeds of its first `j` entries, with the same `r15`. -/ +abbrev RG (p : Params) (D e j : Nat) : State → State → Prop := + RR p D (fun σ s => GS p D σ e j s) fun x y => x.gpr .r15 = y.gpr .r15 + +theorem slot_tr {p : Params} {D e j : Nat} (hj4 : j < 4) (hc : slotChk p e j = true) : + RelCT isa (RG p D e j) (.block (setSR p e j)) (RG p D e (j + 1)) := + stepRR (F := fun s s' => s'.gpr .r15 = s.gpr .r15) (fun σ s _ h => slot_ok hj4 hc h) + (block_tr (rs := [.rbx]) rfl fun x y h r hr => by + simp only [List.mem_singleton] at hr; subst hr + exact (h.lrel fun _ _ h => h.ia4.ia.st).regs (.rbx, scrLen p) (by simp [sgR, sgW])) + fun x y x' y' h fx fy _ => by rw [fx, fy, h.2] + +theorem call4_tr {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {e : Nat} (hc : callChk p e = true) : + RelCT isa (RG p D e 4) (rej4At P (pS (aBase p + e)) (r4P p)) + (RR p D (fun σ s => IA4 p D σ (e + 4) s) fun x y => x.gpr .r15 = y.gpr .r15) := by + have hc' := hc + simp only [callChk, Bool.and_eq_true] at hc' + unfold rej4At + refine RelCT.seq (R := RR p D (J4 p D e) + fun x y => x.gpr .r15 = y.gpr .r15 ∧ (x.gpr .rax).setWidth 32 = (y.gpr .rax).setWidth 32) ?_ ?_ + · refine stepRR (F := fun s s' => s'.gpr .r15 = s.gpr .r15) (fun σ s _ h => callG_ok hP hc h) + ((rej4Call_tr hP hc'.2).mono (fun x y h => ⟨h.lrel fun _ _ h => h.ia4.ia.st, ?_⟩) fun _ _ h => h) + fun x y x' y' h fx fy q => ⟨by rw [fx, fy, h.2], q⟩ + obtain ⟨⟨σ₁, σ₂, _, _, hpub, g₁, g₂⟩, _⟩ := h + rw [g₁.seeds, g₂.seeds, pub_rho hpub] + · refine stepRR (F := fun s s' => s'.gpr .r15 = + BitVec.setWidth 64 ((s.gpr .r15).setWidth 32 &&& (s.gpr .rax).setWidth 32)) + (fun σ s _ h => WP.conj (and4_ok hc h) (WP.mono (and15_ok s) fun _ h => h.1)) + (block_nomem_tr (fun i hi s => by simp only [List.mem_singleton] at hi; subst hi; rfl)) + fun x y x' y' h fx fy _ => by rw [fx, fy, h.2.1, h.2.2] + +theorem sample4_tr {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} {g : Nat} (hc : g4Chk p (4 * g) = true) : + RelCT isa (RR p D (fun σ s => IA4 p D σ (4 * g) s) fun x y => x.gpr .r15 = y.gpr .r15) (sample4 P p g) + (RR p D (fun σ s => IA4 p D σ (4 * g + 4) s) fun x y => x.gpr .r15 = y.gpr .r15) := by + simp only [g4Chk, Bool.and_eq_true] at hc + obtain ⟨⟨⟨⟨s0, s1⟩, s2⟩, s3⟩, cc⟩ := hc + unfold sample4 + refine RelCT.seq (RelCT.mono (slot_tr (by decide) s0) (fun x y h => RR.mono h + (fun σ s h => ⟨h, fun _ h => absurd h (Nat.not_lt_zero _)⟩) id) fun _ _ h => h) ?_ + refine RelCT.seq (slot_tr (by decide) s1) (RelCT.seq (slot_tr (by decide) s2) (RelCT.seq (slot_tr (by decide) s3) ?_)) + exact call4_tr hP cc + +/-! ## The matrix -/ + +theorem cpR4_tr {p : Params} {D j : Nat} (hj : j < 4) (hc : cpChk p j = true) (hsk : 32 ≤ p.skLen) : + RelCT isa (RR p D (fun σ s => ICopy p D σ j s) fun _ _ => True) (cpR4 j) + (RR p D (fun σ s => ICopy p D σ (j + 1) s) fun _ _ => True) := + stepRR (F := fun _ _ => True) (fun σ s _ h => WP.mono (cpR4_ok hc hsk h) fun _ h => ⟨h, trivial⟩) + (copy_tr (by decide) (by decide) (show oRS4 + 34 * j < 2 ^ 31 by simp only [oRS4]; omega) (by decide) (by decide) + fun x y h => ⟨(h.lrel fun _ _ h => h.st).regs (.rbx, scrLen p) (by simp [sgR, sgW]), + (h.lrel fun _ _ h => h.st).regs (.rbp, p.skLen) (by simp [sgR, sgW])⟩) + fun _ _ _ _ _ _ _ _ => trivial + theorem expandA_tr {P : Prims} {D : Nat} (hP : PrimsOk P D) {p : Params} (hc : aChk p = true) : RelCT isa (RR p D (fun σ s => St p D σ s ∧ s.gpr .r15 = 1) fun _ _ => True) (Impl.MlDsa.X86_64.Sign.expandA P p) (RA p D (p.k * p.ℓ)) := by simp only [aChk, Bool.and_eq_true, List.all_eq_true, List.mem_range, decide_eq_true_eq] at hc - obtain ⟨⟨⟨he, hcp⟩, hst⟩, hsk⟩ := hc - obtain ⟨_, _, _, _, _, _, _, _⟩ := copyChk_spec hcp + obtain ⟨⟨⟨⟨⟨he, hcp⟩, hst⟩, hsk⟩, hc4⟩, hg⟩ := hc unfold Impl.MlDsa.X86_64.Sign.expandA - refine RelCT.seq (R := RA p D 0) (stepRR (F := fun s s' => s'.gpr .r15 = s.gpr .r15) (J := fun σ s => IA p D σ 0 s) - (E' := fun x y => x.gpr .r15 = y.gpr .r15) - (fun σ s _ h => ?_) (copy_tr (by decide) (by decide) (by decide) (by decide) (by decide) fun x y h => ?_) - fun x y x' y' h fx fy _ => ?_) ?_ - · refine WP.mono (copy_okB h.1.lay hcp) fun s1 ⟨hP1, hcs1, hb⟩ => ⟨?_, hcs1 _ (by decide)⟩ - have S1 := h.1.step hP1 hst - have e15 : s1.gpr .r15 = 1 := by rw [hcs1 _ (by decide), h.2] - exact ⟨S1, by rw [hP1.pa (by decide), hb, rhoOf, ← h.1.sk, VG.Proof.MlKem.bytesAt_take _ _ hsk], - .inr e15, fun _ => ⟨fun _ h => absurd h (Nat.not_lt_zero _), fun _ h => absurd h (Nat.not_lt_zero _)⟩, - fun h0 => absurd (h0.symm.trans e15) (by decide)⟩ - · have L := h.lrel fun _ _ h => h.1 - exact ⟨L.regs (.rbx, scrLen p) (by simp [sgR, sgW]), L.regs (.rbp, p.skLen) (by simp [sgR, sgW])⟩ - · obtain ⟨⟨σ₁, σ₂, _, _, _, ⟨_, h₁⟩, ⟨_, h₂⟩⟩, _⟩ := h - rw [fx, fy, h₁, h₂] - · have := seqR_tr (f := sampleE P p) (R := fun k => RA p D k) (p.k * p.ℓ) 0 - fun k _ hk => sampleE_tr hP (he k (by omega)) - rwa [Nat.zero_add] at this + refine RelCT.seq (R := RR p D (fun σ s => ICopy p D σ 0 s) fun _ _ => True) (stepRR (F := fun _ _ => True) + (fun σ s _ h => WP.mono (copyRho_ok hcp hst hsk h.1) fun s1 ⟨S1, _, hb, e15⟩ => + ⟨⟨S1, hb, fun _ h => absurd h (Nat.not_lt_zero _), e15.trans h.2⟩, trivial⟩) + (copy_tr (by decide) (by decide) (by decide) (by decide) (by decide) fun x y h => + ⟨(h.lrel fun _ _ h => h.1).regs (.rbx, scrLen p) (by simp [sgR, sgW]), + (h.lrel fun _ _ h => h.1).regs (.rbp, p.skLen) (by simp [sgR, sgW])⟩) + fun _ _ _ _ _ _ _ _ => trivial) ?_ + have hC := seqR_tr (f := cpR4) (R := fun j => RR p D (fun σ s => ICopy p D σ j s) fun _ _ => True) 4 0 + fun j _ hj => cpR4_tr (by omega) (hc4 j (by omega)) hsk + refine RelCT.seq (R := RR p D (fun σ s => ICopy p D σ 4 s) fun _ _ => True) hC ?_ + have hG := seqR_tr (f := sample4 P p) + (R := fun g => RR p D (fun σ s => IA4 p D σ (4 * g) s) fun x y => x.gpr .r15 = y.gpr .r15) (p.k * p.ℓ / 4) 0 + fun g _ hg' => sample4_tr hP (hg g (by omega)) + rw [Nat.zero_add] at hG + refine RelCT.seq (RelCT.mono hG (fun x y h => ?_) fun _ _ h => h) ?_ + · obtain ⟨⟨σ₁, σ₂, p₁, p₂, hpub, i₁, i₂⟩, _⟩ := h + exact ⟨⟨σ₁, σ₂, p₁, p₂, hpub, i₁.ia4, i₂.ia4⟩, i₁.r15.trans i₂.r15.symm⟩ + have hE := seqR_tr (f := sampleE P p) (R := fun k => RA p D k) (p.k * p.ℓ % 4) (4 * (p.k * p.ℓ / 4)) + fun k h1 hk => sampleE_tr hP (he k (by omega)) + rw [show 4 * (p.k * p.ℓ / 4) + p.k * p.ℓ % 4 = p.k * p.ℓ by omega] at hE + exact RelCT.mono hE (fun x y h => RR.mono h (fun σ s h => h.ia) id) fun _ _ h => h end VG.Proof.MlDsa.X86_64.Sign diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseD.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseD.lean index bb2c02b8d..f112d7319 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseD.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PhaseD.lean @@ -1,4 +1,4 @@ -import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PhaseA +import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PhaseA4 import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PrimsD import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.Hash diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Prims.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Prims.lean index f44f8a638..c099490a0 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Prims.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Prims.lean @@ -6,7 +6,7 @@ import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.Glue Untrusted: everything here is checked by Lean. What the proofs need of the implementations of the primitives (`PrimsOk`): each is verified against its shared contract (`Spec/MlDsa/Poly.lean`) for a stack that fits in the `D` -bytes the function gives its calls (`Callee`); and, of the two samplers +bytes the function gives its calls (`Callee`); and, of the samplers whose result the function branches on, that the result is public in their own runs (`RetPub`) and that they succeed only when the algorithm finishes within `maxBounds`, the bounds the leakage of signing is stated for. @@ -43,11 +43,17 @@ structure PrimsOk (P : Prims) (D : Nat) where bitPack : Callee (fun S => bitPackContract X86_64.abi S) D P.bitPack bitUnpack : Callee (fun S => bitUnpackContract X86_64.abi S) D P.bitUnpack hintBitPack : Callee (fun S => hintBitPackContract X86_64.abi S) D P.hintBitPack + rej4 : Callee (fun S => rejNTT4Contract X86_64.abi S) D P.rej4 /-- `vg_mldsa_rej_ntt_poly`'s result depends only on its public data (its seed). -/ rejRet : RetPub (rejNTTContract X86_64.abi rejNTT.S) P.rejNTT /-- `vg_mldsa_rej_ntt_poly` succeeds only if `RejNTTPoly` finishes within `maxBounds`. -/ rejMax : ∀ s t s', (rejNTTContract X86_64.abi rejNTT.S).pre s → Exec isa P.rejNTT s t s' → (s'.gpr .rax).setWidth 32 = 1 → (rejNTTPoly maxBounds.rejNTT (bytesAt s.mem (s.gpr .rdi) 34)).isSome + /-- `vg_mldsa_rej_ntt_poly4`'s result depends only on its public data (its seeds). -/ + rej4Ret : RetPub (rejNTT4Contract X86_64.abi rej4.S) P.rej4 + /-- `vg_mldsa_rej_ntt_poly4` succeeds only if `RejNTTPoly` finishes within `maxBounds` on each seed. -/ + rej4Max : ∀ s t s', (rejNTT4Contract X86_64.abi rej4.S).pre s → Exec isa P.rej4 s t s' → + (s'.gpr .rax).setWidth 32 = 1 → ∀ k < 4, (rejNTTPoly maxBounds.rejNTT (seed4 s.mem (s.gpr .rdi) k)).isSome /-- `vg_mldsa_sample_in_ball`'s result depends only on its public data (`c̃`). -/ ballRet : RetPub (sampleInBallContract X86_64.abi ball.S) P.ball /-- `vg_mldsa_sample_in_ball` succeeds only if `SampleInBall` finishes within `maxBounds`. -/ diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PrimsB.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PrimsB.lean index 83c1741a4..2ca655b89 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PrimsB.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/PrimsB.lean @@ -211,6 +211,105 @@ theorem rejCall_tr {P : Prims} (hP : PrimsOk P D) {a : Ptr} (hc : rejChk (rbs ++ simp only [hx1, hx2, hx3, hy1, hy2, hy3, Arg.val, Ax.bytes' i1 hD, Ay.bytes' i1 hD, hb] simp only [Ax.rsp, Ay.rsp, R.rsp, R.pa i1, R.pa i2, R.pa i3, and_self] +/-! ## `RejNTTPoly` four times -/ + +/-- What the call of `vg_mldsa_rej_ntt_poly4` from the seeds at `RS4` to the four polynomials from `a`, +with the working space `w`, needs of the layout. -/ +def rej4Chk (bs wbs : List (Reg × Nat)) (a w : Ptr) : Bool := + inB wbs a 4096 && inB wbs w 8192 && inB bs (sc oRS4) 136 && inB bs a 4096 && inB bs w 8192 && + sepB bs (sc oRS4) 136 a 4096 && sepB bs (sc oRS4) 136 w 8192 && sepB bs a 4096 w 8192 && + decide (a.1 ∈ bases) && decide (a.2 < 2 ^ 31) && decide (w.1 ∈ bases) && decide (w.2 < 2 ^ 31) + +theorem rej4Chk_spec {bs wbs : List (Reg × Nat)} {a w : Ptr} (hc : rej4Chk bs wbs a w = true) : + inB wbs a 4096 = true ∧ inB wbs w 8192 = true ∧ inB bs (sc oRS4) 136 = true ∧ inB bs a 4096 = true ∧ + inB bs w 8192 = true ∧ sepB bs (sc oRS4) 136 a 4096 = true ∧ sepB bs (sc oRS4) 136 w 8192 = true ∧ + sepB bs a 4096 w 8192 = true ∧ ([Arg.ptr (sc oRS4), .ptr a, .ptr w].all Arg.ok) = true := by + simp only [rej4Chk, Bool.and_eq_true, decide_eq_true_eq] at hc + obtain ⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨⟨h1, h2⟩, h3⟩, h4⟩, h5⟩, h6⟩, h7⟩, h8⟩, h9⟩, h10⟩, h11⟩, h12⟩ := hc + refine ⟨h1, h2, h3, h4, h5, h6, h7, h8, ?_⟩ + simp only [List.all_cons, List.all_nil, Arg.ok, h9, h10, h11, h12, decide_true, Bool.and_true] + decide + +theorem rej4Pre {S : Nat} (hS : S + 8 ≤ D) {s s1 : State} (A : At D rbs wbs s s1) {a w : Ptr} + (hc : rej4Chk (rbs ++ wbs) wbs a w = true) (hA : ArgsIn [.ptr (sc oRS4), .ptr a, .ptr w] s s1) : + (rejNTT4Contract X86_64.abi S).pre + (s1.callEntry.withRegions [⟨pa s (sc oRS4), 136⟩] [⟨pa s a, 4096⟩, ⟨pa s w, 8192⟩]) := by + obtain ⟨_, _, i1, i2, i3, d12, d13, d23, _⟩ := rej4Chk_spec hc + obtain ⟨e1, e2, e3⟩ := argsIn3 hA + have hD : 8 ≤ D := by omega + have hwf := ce_wfS (ws := [64, 64, 64]) (by decide) hS (A.rsp ▸ A.L.sp) [⟨pa s (sc oRS4), 136⟩] + [⟨pa s a, 4096⟩, ⟨pa s w, 8192⟩] + sig_pre [rejNTT4Contract, rejNTT4Sig, X86_64.abi, VG.X86_64.argRegs] + simp only [e1, e2, e3, Arg.val] + refine ⟨hwf, trivial, trivial, A.L.disj d12, A.L.disj d13, A.L.disj d23, A.ret i1 hD, A.ret i2 hD, ?_, + A.L.nwp i1, A.L.nwp i2, A.L.nwp i3⟩ + refine Sig.conj_cons.mpr ⟨A.ret i3 hD, conj_stk [⟨pa s (sc oRS4), 136⟩, ⟨pa s a, 4096⟩, ⟨pa s w, 8192⟩] ?_⟩ + simp only [List.mem_cons, List.mem_nil_iff, or_false, forall_eq_or_imp, forall_eq] + exact ⟨A.stk hS i1, A.stk hS i2, A.stk hS i3⟩ + +/-- The seeds on entry to the call are those before it. -/ +theorem At.seeds4 {s s1 : State} (A : At D rbs wbs s s1) (hi : inB (rbs ++ wbs) (sc oRS4) 136 = true) (hD : 8 ≤ D) + {k : Nat} (hk : k < 4) : + seed4 (s1.mem.writeW (s1.gpr .rsp - 8) (s1.unknowns 0)) (pa s (sc oRS4)) k = seed4 s.mem (pa s (sc oRS4)) k := by + unfold seed4 + rw [← VG.Proof.MlKem.bytesAt_slice _ _ (show 34 * k + 34 ≤ 136 by omega), + ← VG.Proof.MlKem.bytesAt_slice s.mem _ (show 34 * k + 34 ≤ 136 by omega), A.bytes' hi hD] + +/-- The call of `vg_mldsa_rej_ntt_poly4`: its outcome, and that it succeeds +only if `RejNTTPoly` finishes within `maxBounds` on each seed. -/ +theorem rej4Call_ok {P : Prims} (hP : PrimsOk P D) {s : State} (L : Lay D rbs wbs s) {a w : Ptr} + (hc : rej4Chk (rbs ++ wbs) wbs a w = true) : + WP isa (callP ("vg_mldsa_rej_ntt_poly4" ++ P.sfx) P.rej4 [.ptr (sc oRS4), .ptr a, .ptr w]) s fun s' => + PPostB D s s' [(a, 4096), (w, 8192)] ∧ (∀ r ∈ calleeSaved, s'.gpr r = s.gpr r) ∧ + ((s'.gpr .rax).setWidth 32 = 1 → ∀ k < 4, Reduced s'.mem (poly4 (pa s a) k)) ∧ + (((s'.gpr .rax).setWidth 32 = 1 ∧ ∀ k < 4, ∃ b : Bounds, + rejNTTPoly b.rejNTT (seed4 s.mem (pa s (sc oRS4)) k) = some (polyAt s'.mem (poly4 (pa s a) k))) ∨ + ((s'.gpr .rax).setWidth 32 = 0 ∧ ∃ k < 4, + rejNTTPoly minBounds.rejNTT (seed4 s.mem (pa s (sc oRS4)) k) = none)) ∧ + ((s'.gpr .rax).setWidth 32 = 1 → ∀ k < 4, + (rejNTTPoly maxBounds.rejNTT (seed4 s.mem (pa s (sc oRS4)) k)).isSome) := by + obtain ⟨w1, w2, i1, i2, i3, _, _, _, ok⟩ := rej4Chk_spec hc + have hD : 8 ≤ D := by have := hP.rej4.hS; omega + refine WP.mono (callP_ok (hv_with hP.rej4.ver.1 hP.rej4Max) hP.rej4.nosp hP.rej4.depth L.dsm ok + (fun s1 hA hm k => rej4Pre hP.rej4.hS (At.of L hm k) hc hA) + (covers_append (L.cR i1) (covers_wr (covers_cons (L.cW w1) (L.cW w2)))) (covers_cons (L.cW w1) (L.cW w2))) + fun s' ⟨hpost, hcs, s1, hA, hm, k, s₂, hm₂, hg₂, hq, hx⟩ => ⟨hpost, hcs, ?_⟩ + have A := At.of L hm k + obtain ⟨e1, e2, e3⟩ := argsIn3 hA + have er : s₂.gpr .rax = s'.gpr .rax := hg₂ .rax (by decide) + sig_post [rejNTT4Contract, rejNTT4Sig, X86_64.abi, VG.X86_64.argRegs] at hq + simp only [e1, e2, Arg.val, hm₂, er] at hq + simp only [State.withRegions_gpr, State.withRegions_mem, State.callEntry_gpr _ (by decide : Reg.rdi ≠ .rsp), + e1, Arg.val, er] at hx + obtain ⟨hr, ho⟩ := hq + refine ⟨hr, ?_, fun h1 k hk => by rw [← A.seeds4 i1 hD hk]; exact hx h1 k hk⟩ + rcases ho with ⟨h1, hb⟩ | ⟨h0, k, hk, hn⟩ + · exact .inl ⟨h1, fun k hk => by rw [← A.seeds4 i1 hD hk]; exact hb k hk⟩ + · exact .inr ⟨h0, k, hk, by rw [← A.seeds4 i1 hD hk]; exact hn⟩ + +theorem rej4Call_tr {P : Prims} (hP : PrimsOk P D) {a w : Ptr} (hc : rej4Chk (rbs ++ wbs) wbs a w = true) : + RelCT isa (fun x y => LRel D rbs wbs x y ∧ + bytesAt x.mem (pa x (sc oRS4)) 136 = bytesAt y.mem (pa y (sc oRS4)) 136) + (callP ("vg_mldsa_rej_ntt_poly4" ++ P.sfx) P.rej4 [.ptr (sc oRS4), .ptr a, .ptr w]) + fun x y => (x.gpr .rax).setWidth 32 = (y.gpr .rax).setWidth 32 := by + obtain ⟨w1, w2, i1, i2, i3, _, _, _, ok⟩ := rej4Chk_spec hc + have hD : 8 ≤ D := by have := hP.rej4.hS; omega + refine callPRet_tr hP.rej4.ver.1 hP.rej4Ret ok + fun x y x1 y1 ⟨R, hb⟩ ⟨⟨hAx, hmx⟩, kx⟩ ⟨⟨hAy, hmy⟩, ky⟩ => + ⟨_, _, _, _, rej4Pre hP.rej4.hS (At.of R.lx hmx kx) hc hAx, rej4Pre hP.rej4.hS (At.of R.ly hmy ky) hc hAy, ?_, + by rw [kx.2.1, kx.2.2]; exact covers_append (R.lx.cR i1) (covers_wr (covers_cons (R.lx.cW w1) (R.lx.cW w2))), + by rw [kx.2.2]; exact covers_cons (R.lx.cW w1) (R.lx.cW w2), + by rw [ky.2.1, ky.2.2]; exact covers_append (R.ly.cR i1) (covers_wr (covers_cons (R.ly.cW w1) (R.ly.cW w2))), + by rw [ky.2.2]; exact covers_cons (R.ly.cW w1) (R.ly.cW w2), + by rw [(At.of R.lx hmx kx).rsp, (At.of R.ly hmy ky).rsp, R.rsp]⟩ + obtain ⟨hx1, hx2, hx3⟩ := argsIn3 hAx + obtain ⟨hy1, hy2, hy3⟩ := argsIn3 hAy + have Ax := At.of R.lx hmx kx + have Ay := At.of R.ly hmy ky + sig_pub [rejNTT4Contract, rejNTT4Sig, X86_64.abi, VG.X86_64.argRegs] + simp only [hx1, hx2, hx3, hy1, hy2, hy3, Arg.val, Ax.bytes' i1 hD, Ay.bytes' i1 hD, hb] + simp only [Ax.rsp, Ay.rsp, R.rsp, R.pa i1, R.pa i2, R.pa i3, and_self] + /-! ## `ExpandMask` -/ /-- What a call of `vg_mldsa_expand_mask_poly` to `a` needs of the layout. -/ diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Rel.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Rel.lean index bb0316c64..9fa493a61 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Rel.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Rel.lean @@ -1,4 +1,4 @@ -import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PhaseA +import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.PhaseA4 import VerifiedGarbage.Proof.MlDsa.X86_64.Sign.BlockTr /-! diff --git a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Verified.lean b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Verified.lean index 8d11355f3..627b81982 100644 --- a/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Verified.lean +++ b/lean/VerifiedGarbage/Proof/MlDsa/X86_64/Sign/Verified.lean @@ -76,7 +76,7 @@ with no implementation of it. -/ theorem sign_same {m mc : Prog isa → Bool} (hm : Comp m mc) {B : Backend} (h1 : mc B.ntt = true) (h2 : mc B.invNtt = true) (h3 : mc B.mul = true) (h4 : mc B.mulAdd = true) (h5 : mc B.add = true) - (h6 : mc B.sub = true) (h8 : mc B.highBits = true) (h9 : mc B.lowBits = true) + (h6 : mc B.sub = true) (h7 : mc B.rej4 = true) (h8 : mc B.highBits = true) (h9 : mc B.lowBits = true) (h10 : mc B.normLt = true) (h11 : mc B.makeHint = true) (p : Params) : Same m (Impl.MlDsa.X86_64.Sign.sign (primsWith B) p) (Impl.MlDsa.X86_64.Sign.sign (primsWith .empty) p) := by unfold Impl.MlDsa.X86_64.Sign.sign @@ -94,13 +94,14 @@ include h3 theorem sign_ctl : ctlOk (Impl.MlDsa.X86_64.Sign.sign (primsWith v.code) p) = true := ctlOk_of_ctlC (Same.ok (sign_same Comp.ctlC v.ok.ntt.ctl v.ok.invNtt.ctl v.ok.mul.ctl v.ok.mulAdd.ctl - v.ok.add.ctl v.ok.sub.ctl v.ok.highBits.ctl v.ok.lowBits.ctl v.ok.normLt.ctl v.ok.makeHint.ctl p) (sign0_ctlC h3)) + v.ok.add.ctl v.ok.sub.ctl v.ok.rej4.ctl v.ok.highBits.ctl v.ok.lowBits.ctl v.ok.normLt.ctl v.ok.makeHint.ctl p) + (sign0_ctlC h3)) theorem sign_spSafe : (Impl.MlDsa.X86_64.Sign.sign (primsWith v.code) p).all (fun i => !isa.writesSp i) = true := Code.all_of_allInstrs (Same.ok (sign_same (Comp.all _) (Code.allInstrs_of_all v.ok.ntt.sp) (Code.allInstrs_of_all v.ok.invNtt.sp) (Code.allInstrs_of_all v.ok.mul.sp) (Code.allInstrs_of_all v.ok.mulAdd.sp) (Code.allInstrs_of_all v.ok.add.sp) - (Code.allInstrs_of_all v.ok.sub.sp) + (Code.allInstrs_of_all v.ok.sub.sp) (Code.allInstrs_of_all v.ok.rej4.sp) (Code.allInstrs_of_all v.ok.highBits.sp) (Code.allInstrs_of_all v.ok.lowBits.sp) (Code.allInstrs_of_all v.ok.normLt.sp) (Code.allInstrs_of_all v.ok.makeHint.sp) p) (sign0_sp h3)) diff --git a/src/asm/x86_64/mldsa44.rs b/src/asm/x86_64/mldsa44.rs index ce51e5fa5..c62980516 100644 --- a/src/asm/x86_64/mldsa44.rs +++ b/src/asm/x86_64/mldsa44.rs @@ -953,7 +953,7 @@ pub(crate) const VG_MLDSA44_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -968,7 +968,7 @@ pub(crate) const VG_MLDSA44_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). /// * The CPU must support the `avx` and `avx2` target features. #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 2420], scratch: *mut [u64; 9728]) -> u32 { @@ -997,202 +997,154 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "add rsi, 8", "sub rcx, 1", "jne 20b", + "mov rdi, rbx", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", + "mov rdi, rbx", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", + "mov rdi, rbx", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", + "mov rdi, rbx", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 38912", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 39936", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 40960", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 41984", + "add rsi, 38912", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 43008", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 44032", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 45056", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 46080", + "add rsi, 43008", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 47104", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 48128", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 49152", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 50176", + "add rsi, 47104", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 51200", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 52224", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 53248", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 54272", + "add rsi, 51200", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 96", @@ -1427,7 +1379,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -1446,13 +1398,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 14336", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 18432", "mov rsi, rbx", @@ -1476,13 +1428,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 15360", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 19456", "mov rsi, rbx", @@ -1506,13 +1458,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 16384", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 20480", "mov rsi, rbx", @@ -1536,13 +1488,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 17408", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 21504", "mov rsi, rbx", @@ -1806,12 +1758,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 28f", + "jne 212f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 29f", - "28:", + "jmp 213f", + "212:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -2042,13 +1994,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 22528", "mov ecx, 128", - "210:", + "214:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 210b", + "jne 214b", "mov rdi, rbx", "add rdi, 22528", "mov rsi, rbx", @@ -2092,13 +2044,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 23552", "mov ecx, 128", - "211:", + "215:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 211b", + "jne 215b", "mov rdi, rbx", "add rdi, 23552", "mov rsi, rbx", @@ -2142,13 +2094,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 24576", "mov ecx, 128", - "212:", + "216:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 212b", + "jne 216b", "mov rdi, rbx", "add rdi, 24576", "mov rsi, rbx", @@ -2192,13 +2144,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rsi, rbx", "add rsi, 25600", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -2225,36 +2177,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 214f", + "jne 218f", "mov rax, QWORD PTR [rbx+896]", "add rax, 4", "mov QWORD PTR [rbx+896], rax", - "jmp 215f", - "214:", + "jmp 219f", + "218:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "215:", - "29:", + "219:", + "213:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 216f", - "jmp 217f", - "216:", + "jne 220f", + "jmp 221f", + "220:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 4", - "218:", + "222:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 218b", + "jne 222b", "mov rdi, rbx", "add rdi, 14336", "mov esi, 131071", @@ -2295,8 +2247,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "add rcx, 2336", "mov r8d, 84", "call {vg_mldsa_hint_bit_pack}", - "217:", - "22:", + "221:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -2305,7 +2257,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign_avx2(sk: *const [u8; 2560], "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", - vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, + vg_mldsa_rej_ntt_poly4_avx2 = sym super::mldsa::vg_mldsa_rej_ntt_poly4_avx2, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt_avx2 = sym super::mldsa::vg_mldsa_ntt_avx2, vg_keccak_absorb = sym super::sha3::vg_keccak_absorb, @@ -4016,7 +3968,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_keygen(seed: *const [u8; 32], pk /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -4031,7 +3983,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_keygen(seed: *const [u8; 32], pk /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 2420], scratch: *mut [u64; 9728]) -> u32 { core::arch::naked_asm!( @@ -4059,202 +4011,154 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "add rsi, 8", "sub rcx, 1", "jne 20b", + "mov rdi, rbx", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", + "mov rdi, rbx", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", + "mov rdi, rbx", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", + "mov rdi, rbx", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 38912", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 39936", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 40960", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 41984", + "add rsi, 38912", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 43008", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 44032", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 45056", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 46080", + "add rsi, 43008", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 47104", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 48128", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 49152", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 50176", + "add rsi, 47104", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 51200", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 52224", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 53248", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 54272", + "add rsi, 51200", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 55296", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 96", @@ -4489,7 +4393,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -4508,13 +4412,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 14336", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 18432", "mov rsi, rbx", @@ -4538,13 +4442,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 15360", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 19456", "mov rsi, rbx", @@ -4568,13 +4472,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 16384", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 20480", "mov rsi, rbx", @@ -4598,13 +4502,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 17408", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 21504", "mov rsi, rbx", @@ -4868,12 +4772,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 28f", + "jne 212f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 29f", - "28:", + "jmp 213f", + "212:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -5104,13 +5008,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 22528", "mov ecx, 128", - "210:", + "214:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 210b", + "jne 214b", "mov rdi, rbx", "add rdi, 22528", "mov rsi, rbx", @@ -5154,13 +5058,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 23552", "mov ecx, 128", - "211:", + "215:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 211b", + "jne 215b", "mov rdi, rbx", "add rdi, 23552", "mov rsi, rbx", @@ -5204,13 +5108,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 24576", "mov ecx, 128", - "212:", + "216:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 212b", + "jne 216b", "mov rdi, rbx", "add rdi, 24576", "mov rsi, rbx", @@ -5254,13 +5158,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rsi, rbx", "add rsi, 25600", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -5287,36 +5191,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 214f", + "jne 218f", "mov rax, QWORD PTR [rbx+896]", "add rax, 4", "mov QWORD PTR [rbx+896], rax", - "jmp 215f", - "214:", + "jmp 219f", + "218:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "215:", - "29:", + "219:", + "213:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 216f", - "jmp 217f", - "216:", + "jne 220f", + "jmp 221f", + "220:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 4", - "218:", + "222:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 218b", + "jne 222b", "mov rdi, rbx", "add rdi, 14336", "mov esi, 131071", @@ -5357,8 +5261,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "add rcx, 2336", "mov r8d, 84", "call {vg_mldsa_hint_bit_pack}", - "217:", - "22:", + "221:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -5367,7 +5271,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa44_sign(sk: *const [u8; 2560], mu: "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", - vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, + vg_mldsa_rej_ntt_poly4 = sym super::mldsa::vg_mldsa_rej_ntt_poly4, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt = sym super::mldsa::vg_mldsa_ntt, vg_keccak_absorb = sym super::sha3::vg_keccak_absorb, diff --git a/src/asm/x86_64/mldsa65.rs b/src/asm/x86_64/mldsa65.rs index 74e2b8cb2..e83f0160d 100644 --- a/src/asm/x86_64/mldsa65.rs +++ b/src/asm/x86_64/mldsa65.rs @@ -1370,7 +1370,7 @@ pub(crate) const VG_MLDSA65_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -1385,7 +1385,7 @@ pub(crate) const VG_MLDSA65_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). /// * The CPU must support the `avx` and `avx2` target features. #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 3309], scratch: *mut [u64; 12928]) -> u32 { @@ -1414,341 +1414,221 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "add rsi, 8", "sub rcx, 1", "jne 20b", + "mov rdi, rbx", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", + "mov rdi, rbx", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", + "mov rdi, rbx", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", + "mov rdi, rbx", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 50176", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 51200", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 52224", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 53248", + "add rsi, 50176", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 54272", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 55296", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 56320", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 57344", + "add rsi, 54272", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 58368", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 59392", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 60416", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 61440", + "add rsi, 58368", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 62464", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 63488", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 64512", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 65536", + "add rsi, 62464", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 66560", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 67584", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 68608", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 69632", + "add rsi, 66560", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 70656", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 71680", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 72704", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 73728", + "add rsi, 70656", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 74752", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 75776", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 76800", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 77824", + "add rsi, 74752", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 3", "mov BYTE PTR [rbx+944], al", @@ -1775,9 +1655,9 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "call {vg_mldsa_rej_ntt_poly}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 128", @@ -2077,7 +1957,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -2096,13 +1976,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 16384", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 21504", "mov rsi, rbx", @@ -2126,13 +2006,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 17408", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 22528", "mov rsi, rbx", @@ -2156,13 +2036,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 18432", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 23552", "mov rsi, rbx", @@ -2186,13 +2066,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 19456", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 24576", "mov rsi, rbx", @@ -2216,13 +2096,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 20480", "mov ecx, 128", - "28:", + "212:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 28b", + "jne 212b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -2620,12 +2500,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 29f", + "jne 213f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 210f", - "29:", + "jmp 214f", + "213:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -2934,13 +2814,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 26624", "mov ecx, 128", - "211:", + "215:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 211b", + "jne 215b", "mov rdi, rbx", "add rdi, 26624", "mov rsi, rbx", @@ -2984,13 +2864,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 27648", "mov ecx, 128", - "212:", + "216:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 212b", + "jne 216b", "mov rdi, rbx", "add rdi, 27648", "mov rsi, rbx", @@ -3034,13 +2914,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 28672", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 28672", "mov rsi, rbx", @@ -3084,13 +2964,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 29696", "mov ecx, 128", - "214:", + "218:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 214b", + "jne 218b", "mov rdi, rbx", "add rdi, 29696", "mov rsi, rbx", @@ -3134,13 +3014,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 30720", "mov ecx, 128", - "215:", + "219:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 215b", + "jne 219b", "mov rdi, rbx", "add rdi, 30720", "mov rsi, rbx", @@ -3184,13 +3064,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rsi, rbx", "add rsi, 31744", "mov ecx, 128", - "216:", + "220:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 216b", + "jne 220b", "mov rdi, rbx", "add rdi, 31744", "mov rsi, rbx", @@ -3217,36 +3097,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 217f", + "jne 221f", "mov rax, QWORD PTR [rbx+896]", "add rax, 5", "mov QWORD PTR [rbx+896], rax", - "jmp 218f", - "217:", + "jmp 222f", + "221:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "218:", - "210:", + "222:", + "214:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 219f", - "jmp 220f", - "219:", + "jne 223f", + "jmp 224f", + "223:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 6", - "221:", + "225:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 221b", + "jne 225b", "mov rdi, rbx", "add rdi, 16384", "mov esi, 524287", @@ -3295,8 +3175,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "add rcx, 3248", "mov r8d, 61", "call {vg_mldsa_hint_bit_pack}", - "220:", - "22:", + "224:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -3305,6 +3185,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign_avx2(sk: *const [u8; 4032], "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", + vg_mldsa_rej_ntt_poly4_avx2 = sym super::mldsa::vg_mldsa_rej_ntt_poly4_avx2, vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt_avx2 = sym super::mldsa::vg_mldsa_ntt_avx2, @@ -5850,7 +5731,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_keygen(seed: *const [u8; 32], pk /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -5865,7 +5746,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_keygen(seed: *const [u8; 32], pk /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 3309], scratch: *mut [u64; 12928]) -> u32 { core::arch::naked_asm!( @@ -5893,341 +5774,221 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "add rsi, 8", "sub rcx, 1", "jne 20b", - "mov eax, 0", - "mov BYTE PTR [rbx+944], al", - "mov eax, 0", - "mov BYTE PTR [rbx+945], al", "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 50176", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 1", - "mov BYTE PTR [rbx+944], al", - "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 51200", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 2", - "mov BYTE PTR [rbx+944], al", - "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 52224", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 3", - "mov BYTE PTR [rbx+944], al", - "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 53248", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 54272", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", - "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 55296", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 1", - "mov BYTE PTR [rbx+944], al", - "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 56320", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 2", - "mov BYTE PTR [rbx+944], al", - "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 57344", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 3", - "mov BYTE PTR [rbx+944], al", - "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 58368", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 59392", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", - "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 60416", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 1", - "mov BYTE PTR [rbx+944], al", - "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 61440", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1252], al", + "mov eax, 0", + "mov BYTE PTR [rbx+1253], al", + "mov eax, 3", + "mov BYTE PTR [rbx+1286], al", + "mov eax, 0", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 62464", + "add rsi, 50176", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", - "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov eax, 4", + "mov BYTE PTR [rbx+1184], al", + "mov eax, 0", + "mov BYTE PTR [rbx+1185], al", + "mov eax, 0", + "mov BYTE PTR [rbx+1218], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1219], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1252], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1286], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 63488", + "add rsi, 54272", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", + "mov eax, 3", + "mov BYTE PTR [rbx+1184], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1185], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1219], al", + "mov eax, 0", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1253], al", + "mov eax, 1", + "mov BYTE PTR [rbx+1286], al", + "mov eax, 2", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 64512", + "add rsi, 58368", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", + "mov eax, 2", + "mov BYTE PTR [rbx+1184], al", + "mov eax, 2", + "mov BYTE PTR [rbx+1185], al", + "mov eax, 3", + "mov BYTE PTR [rbx+1218], al", + "mov eax, 2", + "mov BYTE PTR [rbx+1219], al", + "mov eax, 4", + "mov BYTE PTR [rbx+1252], al", + "mov eax, 2", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 65536", + "add rsi, 62464", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 66560", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 67584", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 68608", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 69632", + "add rsi, 66560", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 70656", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 71680", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 72704", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 73728", + "add rsi, 70656", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 74752", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 75776", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 76800", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 77824", + "add rsi, 74752", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 80896", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 3", "mov BYTE PTR [rbx+944], al", @@ -6254,9 +6015,9 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "call {vg_mldsa_rej_ntt_poly}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 128", @@ -6556,7 +6317,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -6575,13 +6336,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 16384", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 21504", "mov rsi, rbx", @@ -6605,13 +6366,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 17408", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 22528", "mov rsi, rbx", @@ -6635,13 +6396,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 18432", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 23552", "mov rsi, rbx", @@ -6665,13 +6426,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 19456", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 24576", "mov rsi, rbx", @@ -6695,13 +6456,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 20480", "mov ecx, 128", - "28:", + "212:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 28b", + "jne 212b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -7099,12 +6860,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 29f", + "jne 213f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 210f", - "29:", + "jmp 214f", + "213:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -7413,13 +7174,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 26624", "mov ecx, 128", - "211:", + "215:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 211b", + "jne 215b", "mov rdi, rbx", "add rdi, 26624", "mov rsi, rbx", @@ -7463,13 +7224,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 27648", "mov ecx, 128", - "212:", + "216:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 212b", + "jne 216b", "mov rdi, rbx", "add rdi, 27648", "mov rsi, rbx", @@ -7513,13 +7274,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 28672", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 28672", "mov rsi, rbx", @@ -7563,13 +7324,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 29696", "mov ecx, 128", - "214:", + "218:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 214b", + "jne 218b", "mov rdi, rbx", "add rdi, 29696", "mov rsi, rbx", @@ -7613,13 +7374,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 30720", "mov ecx, 128", - "215:", + "219:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 215b", + "jne 219b", "mov rdi, rbx", "add rdi, 30720", "mov rsi, rbx", @@ -7663,13 +7424,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rsi, rbx", "add rsi, 31744", "mov ecx, 128", - "216:", + "220:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 216b", + "jne 220b", "mov rdi, rbx", "add rdi, 31744", "mov rsi, rbx", @@ -7696,36 +7457,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 217f", + "jne 221f", "mov rax, QWORD PTR [rbx+896]", "add rax, 5", "mov QWORD PTR [rbx+896], rax", - "jmp 218f", - "217:", + "jmp 222f", + "221:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "218:", - "210:", + "222:", + "214:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 219f", - "jmp 220f", - "219:", + "jne 223f", + "jmp 224f", + "223:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 6", - "221:", + "225:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 221b", + "jne 225b", "mov rdi, rbx", "add rdi, 16384", "mov esi, 524287", @@ -7774,8 +7535,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "add rcx, 3248", "mov r8d, 61", "call {vg_mldsa_hint_bit_pack}", - "220:", - "22:", + "224:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -7784,6 +7545,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa65_sign(sk: *const [u8; 4032], mu: "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", + vg_mldsa_rej_ntt_poly4 = sym super::mldsa::vg_mldsa_rej_ntt_poly4, vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt = sym super::mldsa::vg_mldsa_ntt, diff --git a/src/asm/x86_64/mldsa87.rs b/src/asm/x86_64/mldsa87.rs index 2b5d50687..ed91837d4 100644 --- a/src/asm/x86_64/mldsa87.rs +++ b/src/asm/x86_64/mldsa87.rs @@ -1953,7 +1953,7 @@ pub(crate) const VG_MLDSA87_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -1968,7 +1968,7 @@ pub(crate) const VG_MLDSA87_SIGN_AVX2_FEATURES: &[&str] = &["avx", "avx2"]; /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). /// * The CPU must support the `avx` and `avx2` target features. #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 4627], scratch: *mut [u64; 18048]) -> u32 { @@ -1997,682 +1997,394 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "add rsi, 8", "sub rcx, 1", "jne 20b", + "mov rdi, rbx", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", + "mov rdi, rbx", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", + "mov rdi, rbx", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", + "mov rdi, rbx", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 64512", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 65536", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 66560", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 67584", + "add rsi, 64512", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 68608", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 69632", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 70656", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 71680", + "add rsi, 68608", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 72704", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 73728", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 74752", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 75776", + "add rsi, 72704", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 76800", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 77824", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 78848", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 79872", + "add rsi, 76800", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 80896", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 81920", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 82944", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 83968", + "add rsi, 80896", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 84992", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 86016", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 87040", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 88064", + "add rsi, 84992", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 89088", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 90112", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 91136", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 92160", + "add rsi, 89088", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 93184", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 94208", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 95232", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 96256", + "add rsi, 93184", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 97280", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 98304", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 99328", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 100352", + "add rsi, 97280", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 101376", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 102400", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 103424", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 104448", + "add rsi, 101376", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 105472", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 106496", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 107520", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 108544", + "add rsi, 105472", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 109568", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 110592", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 111616", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 112640", + "add rsi, 109568", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 113664", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 114688", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 115712", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 116736", + "add rsi, 113664", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 117760", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 118784", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 119808", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 120832", + "add rsi, 117760", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4_avx2}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 96", @@ -3050,7 +2762,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -3069,13 +2781,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 18432", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -3099,13 +2811,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 19456", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 26624", "mov rsi, rbx", @@ -3129,13 +2841,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 20480", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 27648", "mov rsi, rbx", @@ -3159,13 +2871,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 21504", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 28672", "mov rsi, rbx", @@ -3189,13 +2901,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 22528", "mov ecx, 128", - "28:", + "212:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 28b", + "jne 212b", "mov rdi, rbx", "add rdi, 29696", "mov rsi, rbx", @@ -3219,13 +2931,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 23552", "mov ecx, 128", - "29:", + "213:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 29b", + "jne 213b", "mov rdi, rbx", "add rdi, 30720", "mov rsi, rbx", @@ -3249,13 +2961,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 24576", "mov ecx, 128", - "210:", + "214:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 210b", + "jne 214b", "mov rdi, rbx", "add rdi, 31744", "mov rsi, rbx", @@ -3871,12 +3583,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 211f", + "jne 215f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 212f", - "211:", + "jmp 216f", + "215:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -4285,13 +3997,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 32768", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 32768", "mov rsi, rbx", @@ -4335,13 +4047,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 33792", "mov ecx, 128", - "214:", + "218:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 214b", + "jne 218b", "mov rdi, rbx", "add rdi, 33792", "mov rsi, rbx", @@ -4385,13 +4097,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 34816", "mov ecx, 128", - "215:", + "219:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 215b", + "jne 219b", "mov rdi, rbx", "add rdi, 34816", "mov rsi, rbx", @@ -4435,13 +4147,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 35840", "mov ecx, 128", - "216:", + "220:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 216b", + "jne 220b", "mov rdi, rbx", "add rdi, 35840", "mov rsi, rbx", @@ -4485,13 +4197,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 36864", "mov ecx, 128", - "217:", + "221:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 217b", + "jne 221b", "mov rdi, rbx", "add rdi, 36864", "mov rsi, rbx", @@ -4535,13 +4247,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 37888", "mov ecx, 128", - "218:", + "222:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 218b", + "jne 222b", "mov rdi, rbx", "add rdi, 37888", "mov rsi, rbx", @@ -4585,13 +4297,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 38912", "mov ecx, 128", - "219:", + "223:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 219b", + "jne 223b", "mov rdi, rbx", "add rdi, 38912", "mov rsi, rbx", @@ -4635,13 +4347,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rsi, rbx", "add rsi, 39936", "mov ecx, 128", - "220:", + "224:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 220b", + "jne 224b", "mov rdi, rbx", "add rdi, 39936", "mov rsi, rbx", @@ -4668,36 +4380,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 221f", + "jne 225f", "mov rax, QWORD PTR [rbx+896]", "add rax, 7", "mov QWORD PTR [rbx+896], rax", - "jmp 222f", - "221:", + "jmp 226f", + "225:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "222:", - "212:", + "226:", + "216:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 223f", - "jmp 224f", - "223:", + "jne 227f", + "jmp 228f", + "227:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 8", - "225:", + "229:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 225b", + "jne 229b", "mov rdi, rbx", "add rdi, 18432", "mov esi, 524287", @@ -4762,8 +4474,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "add rcx, 4544", "mov r8d, 83", "call {vg_mldsa_hint_bit_pack}", - "224:", - "22:", + "228:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -4772,7 +4484,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign_avx2(sk: *const [u8; 4896], "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", - vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, + vg_mldsa_rej_ntt_poly4_avx2 = sym super::mldsa::vg_mldsa_rej_ntt_poly4_avx2, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt_avx2 = sym super::mldsa::vg_mldsa_ntt_avx2, vg_keccak_absorb = sym super::sha3::vg_keccak_absorb, @@ -8417,7 +8129,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_keygen(seed: *const [u8; 32], pk /// /// Contract: `VG.Spec.MlDsa.signContract`. Constant time but for `ρ` and the rejection sampling: timing may depend on the pointers, on `ρ` (the first 32 bytes of `*sk`), on the number of iterations of the signing loop and the commitment hash of each, and on the hint of the signature (`signLeak`), but not on anything else of the key, the message representative or the randomness. /// -/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 24 bytes of stack below its return address. +/// The function saves its caller's callee-saved registers in `scratch`; its calls use the 32 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. /// @@ -8432,7 +8144,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_keygen(seed: *const [u8; 32], pk /// * `rnd` must be fresh random bytes (FIPS 204 §3.6.1), or 32 zero bytes for deterministic signing. /// * `scratch` is working space: on return it holds intermediate values, which the caller must destroy (FIPS 204 §3.6.3). /// * `sig` and `scratch` must not overlap each other, `sk`, `mu` or `rnd` (distinct Rust objects never do). -/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 24 bytes of stack below it, or wrap around the end of the address space (no Rust object does). +/// * None of `sk`, `mu`, `rnd`, `sig` and `scratch` may overlap the return address on the stack or the 32 bytes of stack below it, or wrap around the end of the address space (no Rust object does). #[unsafe(naked)] pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: *const [u8; 64], rnd: *const [u8; 32], sig: *mut [u8; 4627], scratch: *mut [u64; 18048]) -> u32 { core::arch::naked_asm!( @@ -8460,682 +8172,394 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "add rsi, 8", "sub rcx, 1", "jne 20b", + "mov rdi, rbx", + "add rdi, 1152", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "21:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 21b", + "mov rdi, rbx", + "add rdi, 1186", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "22:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 22b", + "mov rdi, rbx", + "add rdi, 1220", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "23:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 23b", + "mov rdi, rbx", + "add rdi, 1254", + "mov rsi, rbp", + "add rsi, 0", + "mov ecx, 4", + "24:", + "mov rax, QWORD PTR [rsi]", + "mov QWORD PTR [rdi], rax", + "add rdi, 8", + "add rsi, 8", + "sub rcx, 1", + "jne 24b", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 64512", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 65536", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 66560", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 67584", + "add rsi, 64512", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 68608", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 69632", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 0", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 70656", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 71680", + "add rsi, 68608", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 72704", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 73728", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 74752", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 75776", + "add rsi, 72704", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 76800", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 1", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 77824", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 78848", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 79872", + "add rsi, 76800", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 80896", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 81920", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 82944", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 83968", + "add rsi, 80896", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 2", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 84992", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 86016", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 87040", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", - "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 88064", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 3", - "mov BYTE PTR [rbx+944], al", - "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 89088", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", - "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 90112", + "add rsi, 84992", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", - "mov eax, 5", - "mov BYTE PTR [rbx+944], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 91136", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1184], al", + "mov eax, 3", + "mov BYTE PTR [rbx+1185], al", + "mov eax, 4", + "mov BYTE PTR [rbx+1218], al", + "mov eax, 3", + "mov BYTE PTR [rbx+1219], al", + "mov eax, 5", + "mov BYTE PTR [rbx+1252], al", + "mov eax, 3", + "mov BYTE PTR [rbx+1253], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 3", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 92160", + "add rsi, 89088", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 93184", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 94208", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 95232", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 96256", + "add rsi, 93184", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 97280", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 98304", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 4", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 99328", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 100352", + "add rsi, 97280", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 101376", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 102400", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 103424", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 104448", + "add rsi, 101376", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 105472", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 5", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 106496", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 107520", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 108544", + "add rsi, 105472", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 109568", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 110592", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 111616", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 112640", + "add rsi, 109568", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 6", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 113664", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 0", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 114688", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 1", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 115712", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 2", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 116736", + "add rsi, 113664", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "mov eax, 3", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1184], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 117760", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1185], al", "mov eax, 4", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1218], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 118784", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1219], al", "mov eax, 5", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1252], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", - "mov rdi, rbx", - "add rdi, 912", - "mov rsi, rbx", - "add rsi, 119808", - "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", - "and r15d, eax", + "mov BYTE PTR [rbx+1253], al", "mov eax, 6", - "mov BYTE PTR [rbx+944], al", + "mov BYTE PTR [rbx+1286], al", "mov eax, 7", - "mov BYTE PTR [rbx+945], al", + "mov BYTE PTR [rbx+1287], al", "mov rdi, rbx", - "add rdi, 912", + "add rdi, 1152", "mov rsi, rbx", - "add rsi, 120832", + "add rsi, 117760", "mov rdx, rbx", - "add rdx, 3072", - "call {vg_mldsa_rej_ntt_poly}", + "add rdx, 121856", + "call {vg_mldsa_rej_ntt_poly4}", "and r15d, eax", "test r15d, r15d", - "jne 21f", - "jmp 22f", - "21:", + "jne 25f", + "jmp 26f", + "25:", "mov rdi, rbp", "add rdi, 128", "mov esi, 96", @@ -9513,7 +8937,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov QWORD PTR [rbx+896], rax", "mov eax, 814", "mov QWORD PTR [rbx+888], rax", - "23:", + "27:", "mov rax, QWORD PTR [rbx+896]", "add rax, 0", "mov BYTE PTR [rbx+1024], al", @@ -9532,13 +8956,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 18432", "mov ecx, 128", - "24:", + "28:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 24b", + "jne 28b", "mov rdi, rbx", "add rdi, 25600", "mov rsi, rbx", @@ -9562,13 +8986,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 19456", "mov ecx, 128", - "25:", + "29:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 25b", + "jne 29b", "mov rdi, rbx", "add rdi, 26624", "mov rsi, rbx", @@ -9592,13 +9016,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 20480", "mov ecx, 128", - "26:", + "210:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 26b", + "jne 210b", "mov rdi, rbx", "add rdi, 27648", "mov rsi, rbx", @@ -9622,13 +9046,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 21504", "mov ecx, 128", - "27:", + "211:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 27b", + "jne 211b", "mov rdi, rbx", "add rdi, 28672", "mov rsi, rbx", @@ -9652,13 +9076,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 22528", "mov ecx, 128", - "28:", + "212:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 28b", + "jne 212b", "mov rdi, rbx", "add rdi, 29696", "mov rsi, rbx", @@ -9682,13 +9106,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 23552", "mov ecx, 128", - "29:", + "213:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 29b", + "jne 213b", "mov rdi, rbx", "add rdi, 30720", "mov rsi, rbx", @@ -9712,13 +9136,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 24576", "mov ecx, 128", - "210:", + "214:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 210b", + "jne 214b", "mov rdi, rbx", "add rdi, 31744", "mov rsi, rbx", @@ -10334,12 +9758,12 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "add r8, 3072", "call {vg_mldsa_sample_in_ball}", "test eax, eax", - "jne 211f", + "jne 215f", "mov r15d, 0", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "jmp 212f", - "211:", + "jmp 216f", + "215:", "mov rdi, rbx", "add rdi, 5120", "mov rsi, rbx", @@ -10748,13 +10172,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 32768", "mov ecx, 128", - "213:", + "217:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 213b", + "jne 217b", "mov rdi, rbx", "add rdi, 32768", "mov rsi, rbx", @@ -10798,13 +10222,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 33792", "mov ecx, 128", - "214:", + "218:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 214b", + "jne 218b", "mov rdi, rbx", "add rdi, 33792", "mov rsi, rbx", @@ -10848,13 +10272,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 34816", "mov ecx, 128", - "215:", + "219:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 215b", + "jne 219b", "mov rdi, rbx", "add rdi, 34816", "mov rsi, rbx", @@ -10898,13 +10322,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 35840", "mov ecx, 128", - "216:", + "220:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 216b", + "jne 220b", "mov rdi, rbx", "add rdi, 35840", "mov rsi, rbx", @@ -10948,13 +10372,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 36864", "mov ecx, 128", - "217:", + "221:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 217b", + "jne 221b", "mov rdi, rbx", "add rdi, 36864", "mov rsi, rbx", @@ -10998,13 +10422,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 37888", "mov ecx, 128", - "218:", + "222:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 218b", + "jne 222b", "mov rdi, rbx", "add rdi, 37888", "mov rsi, rbx", @@ -11048,13 +10472,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 38912", "mov ecx, 128", - "219:", + "223:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 219b", + "jne 223b", "mov rdi, rbx", "add rdi, 38912", "mov rsi, rbx", @@ -11098,13 +10522,13 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rsi, rbx", "add rsi, 39936", "mov ecx, 128", - "220:", + "224:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 220b", + "jne 224b", "mov rdi, rbx", "add rdi, 39936", "mov rsi, rbx", @@ -11131,36 +10555,36 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "shr rax, 63", "and r15d, eax", "test r15d, r15d", - "jne 221f", + "jne 225f", "mov rax, QWORD PTR [rbx+896]", "add rax, 7", "mov QWORD PTR [rbx+896], rax", - "jmp 222f", - "221:", + "jmp 226f", + "225:", "mov eax, 1", "mov QWORD PTR [rbx+888], rax", - "222:", - "212:", + "226:", + "216:", "mov rax, QWORD PTR [rbx+888]", "sub rax, 1", "mov QWORD PTR [rbx+888], rax", - "jne 23b", + "jne 27b", "test r15d, r15d", - "jne 223f", - "jmp 224f", - "223:", + "jne 227f", + "jmp 228f", + "227:", "mov rdi, r14", "add rdi, 0", "mov rsi, rbx", "add rsi, 1040", "mov ecx, 8", - "225:", + "229:", "mov rax, QWORD PTR [rsi]", "mov QWORD PTR [rdi], rax", "add rdi, 8", "add rsi, 8", "sub rcx, 1", - "jne 225b", + "jne 229b", "mov rdi, rbx", "add rdi, 18432", "mov esi, 524287", @@ -11225,8 +10649,8 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "add rcx, 4544", "mov r8d, 83", "call {vg_mldsa_hint_bit_pack}", - "224:", - "22:", + "228:", + "26:", "mov eax, r15d", "mov r15, QWORD PTR [rbx+880]", "mov r14, QWORD PTR [rbx+872]", @@ -11235,7 +10659,7 @@ pub(crate) unsafe extern "sysv64" fn vg_mldsa87_sign(sk: *const [u8; 4896], mu: "mov rbp, QWORD PTR [rbx+848]", "mov rbx, QWORD PTR [rbx+840]", "ret", - vg_mldsa_rej_ntt_poly = sym super::mldsa::vg_mldsa_rej_ntt_poly, + vg_mldsa_rej_ntt_poly4 = sym super::mldsa::vg_mldsa_rej_ntt_poly4, vg_mldsa_bit_unpack = sym super::mldsa::vg_mldsa_bit_unpack, vg_mldsa_ntt = sym super::mldsa::vg_mldsa_ntt, vg_keccak_absorb = sym super::sha3::vg_keccak_absorb,