x86-64 P-256 ECDH by 5-bit windows in Jacobian coordinates (−18%)

lean/VerifiedGarbage/Generic/MdHash/P256/X86_64/EcdsaP256Sha256.lean

@@ -1,5 +1,6 @@
 import VerifiedGarbage.TCB.X86_64.Target
 import VerifiedGarbage.Proof.Weierstrass.Law
+import VerifiedGarbage.Proof.Weierstrass.X86_64.InvInterface
 import VerifiedGarbage.Proof.P256.Comb7
 import VerifiedGarbage.Proof.Ecdsa.Rfc6979.X86_64.Sha256
 
@@ -17,7 +18,7 @@ The stack is 240 bytes: a 216-byte frame, and the 24 bytes below it that the
 calls use (`vg_ecdsa_p256_sign` only its return address).
 
 It reads the comb's tables of `vg_ecdsa_p256_sign`, the static `VG_P256_COMB`.
-It is generic over P-256's group law and inversions `h` too, the variant
+It is generic over P-256's group law, inversions and prime order `h` too, the variant
 `Variants/P256/X86_64/Law.lean`; and is emitted for each multiplication of
 `vg_ecdsa_p256_sign`: the baseline's, and BMI2's and ADX's
 (`vg_ecdsa_p256_sign_adx`, which the instance with the suffix `_adx` calls).
@@ -31,7 +32,7 @@ open VG.Proof.Ecdsa.Rfc6979.X86_64.Sha256 (pack sign_verified)
 /-- The signature with the hash's compression function `c`, and P-256's
 multiplication with BMI2 and ADX (`adx`, `_adx`, calling `vg_ecdsa_p256_sign_adx`)
 or not. -/
-def withMul (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) (c : Proof.Sha256.X86_64.Compress)
+def withMul (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) (c : Proof.Sha256.X86_64.Compress)
     (adx : Bool) :
     Artifact :=
   { Spec.Ecdsa.Rfc6979.P256Sha256.signApi with
@@ -49,7 +50,7 @@ def withMul (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) (c : Proof.
     spSafe := sign_spSafe (pack adx h.law (Proof.P256.combOk7 h.law) h.inv c)
     features := c.features ++ (if adx then ["bmi2", "adx", "avx", "avx2"] else []).filter (!c.features.contains ·) }
 
-def artifacts (v : Proof.Pbkdf2.Md.X86_64.MdHash) (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) :
+def artifacts (v : Proof.Pbkdf2.Md.X86_64.MdHash) (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) :
     List Artifact :=
   match v.sha256 with
   | none => []

lean/VerifiedGarbage/Generic/MdHash/P256/X86_64/EcdsaP256Sha384.lean

@@ -1,5 +1,6 @@
 import VerifiedGarbage.TCB.X86_64.Target
 import VerifiedGarbage.Proof.Weierstrass.Law
+import VerifiedGarbage.Proof.Weierstrass.X86_64.InvInterface
 import VerifiedGarbage.Proof.P256.Comb7
 import VerifiedGarbage.Proof.Ecdsa.Rfc6979.X86_64.Sha384
 
@@ -17,7 +18,7 @@ The stack is 240 bytes: a 216-byte frame, and the 24 bytes below it that the
 calls use (`vg_ecdsa_p256_sign` only its return address).
 
 It reads the comb's tables of `vg_ecdsa_p256_sign`, the static `VG_P256_COMB`.
-It is generic over P-256's group law and inversions `h` too, the variant
+It is generic over P-256's group law, inversions and prime order `h` too, the variant
 `Variants/P256/X86_64/Law.lean`; and is emitted for each multiplication of
 `vg_ecdsa_p256_sign`: the baseline's, and BMI2's and ADX's
 (`vg_ecdsa_p256_sign_adx`, which the instance with the suffix `_adx` calls).
@@ -31,7 +32,7 @@ open VG.Proof.Ecdsa.Rfc6979.X86_64.Sha384 (pack sign_verified)
 /-- The signature with the hash's compression function `c`, and P-256's
 multiplication with BMI2 and ADX (`adx`, `_adx`, calling `vg_ecdsa_p256_sign_adx`)
 or not. -/
-def withMul (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) (c : Proof.Sha512.X86_64.Compress)
+def withMul (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) (c : Proof.Sha512.X86_64.Compress)
     (adx : Bool) :
     Artifact :=
   { Spec.Ecdsa.Rfc6979.P256Sha384.signApi with
@@ -49,7 +50,7 @@ def withMul (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) (c : Proof.
     spSafe := sign_spSafe (pack adx h.law (Proof.P256.combOk7 h.law) h.inv c)
     features := c.features ++ (if adx then ["bmi2", "adx", "avx", "avx2"] else []).filter (!c.features.contains ·) }
 
-def artifacts (v : Proof.Pbkdf2.Md.X86_64.MdHash) (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) :
+def artifacts (v : Proof.Pbkdf2.Md.X86_64.MdHash) (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) :
     List Artifact :=
   match v.sha384 with
   | none => []

lean/VerifiedGarbage/Generic/P256/X86_64/EcP256.lean

@@ -1,5 +1,6 @@
 import VerifiedGarbage.TCB.X86_64.Target
 import VerifiedGarbage.Proof.Weierstrass.Law
+import VerifiedGarbage.Proof.Weierstrass.X86_64.InvInterface
 import VerifiedGarbage.Proof.P256.Comb7
 import VerifiedGarbage.Impl.EcKey.P256.X86_64
 import VerifiedGarbage.Proof.EcKey.X86_64.Verified
@@ -10,8 +11,8 @@ import VerifiedGarbage.Proof.EcKey.X86_64.LitAdx
 /-!
 # P-256 public keys (FIPS 186-5 §A.2) on x86-64
 
-A generic file (see `TCB/Emit.lean`) over P-256's group law and
-inversions `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
+A generic file (see `TCB/Emit.lean`) over P-256's group law,
+inversions and prime order `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
 multiplication: the baseline's, and BMI2's and ADX's, with the comb's
 selection by AVX2 (`_adx`).
 -/
@@ -42,7 +43,7 @@ def publicKey (adx : Bool) (code : Prog X86_64.isa)
     spSafe := hsp
     features := if adx then ["bmi2", "adx", "avx", "avx2"] else [] }
 
-def artifacts (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) : List Artifact := [
+def artifacts (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) : List Artifact := [
   publicKey false Impl.EcKey.X86_64.publicKeyP256
     (Proof.EcKey.X86_64.pk_verified h.law (Proof.P256.combOk7 h.law) h.inv) (Code.all_of_allInstrs (by lit_decide)),
   publicKey true Impl.EcKey.X86_64.publicKeyP256Adx

lean/VerifiedGarbage/Generic/P256/X86_64/EcdhP256.lean

@@ -1,5 +1,6 @@
 import VerifiedGarbage.TCB.X86_64.Target
 import VerifiedGarbage.Proof.Weierstrass.Law
+import VerifiedGarbage.Proof.Weierstrass.X86_64.InvInterface
 import VerifiedGarbage.Impl.Ecdh.P256.X86_64
 import VerifiedGarbage.Proof.Ecdh.X86_64.Verified
 import VerifiedGarbage.Proof.Ecdh.X86_64.Lit
@@ -9,8 +10,8 @@ import VerifiedGarbage.Proof.Ecdh.X86_64.LitAdx
 /-!
 # ECDH over P-256 (SP 800-56A) on x86-64
 
-A generic file (see `TCB/Emit.lean`) over P-256's group law and
-inversions `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
+A generic file (see `TCB/Emit.lean`) over P-256's group law,
+inversions and prime order `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
 multiplication: the baseline's, and BMI2's and ADX's (`_adx`).
 -/
 
@@ -32,25 +33,30 @@ def exchange (adx : Bool) (code : Prog X86_64.isa)
       Montgomery form, " ++ Proof.Ecdsa.X86_64.mulNote adx ++ ". The peer's key is checked without branches (its first byte, both \
       coordinates below `p`, and the curve's equation), and `[d]P` is computed for the peer's \
       point if it is valid, else `G`, so it always runs on a point of the curve. `[d]P` is by \
-      signed 4-bit windows: `d` is recoded as `d + 8 Σ_{j<65} 16^j`, whose 65 nibbles less 8 \
-      are digits in `[-8, 7]`; a table of `[1 … 8]P` is built in `scratch` by complete \
-      additions; then, from the point at infinity, for each digit from the top, four doublings \
-      in Jacobian coordinates (dbl-2001-b, for `a = -3`) and the addition of the digit's entry, \
-      selected in constant time by loading all eight entries, 16 bytes at a time, and keeping \
-      (`pand`, `por`) the one of the digit's magnitude, and negated by a mask of its sign, by \
-      the complete addition formulas of Renes, Costello and Batina for `a = -3` (Algorithm 4); \
+      signed 5-bit windows in Jacobian coordinates, P-256 having prime order: `d` is recoded as \
+      `d + 16 Σ_{j<52} 32^j`, whose 52 5-bit windows less 16 are digits in `[-16, 15]`; a table \
+      of `[1 … 16]P`, each entry with its `Z²` and `Z³`, is built in `scratch` by a doubling and \
+      mixed additions; then, from the point at infinity, for each digit from the top, five \
+      doublings in Jacobian coordinates for `a = -3` (with a halving modulo `p` in place of \
+      multiplications by small constants) and the addition of the digit's entry, selected in \
+      constant time by loading all sixteen entries, " ++
+      (if adx then "32 bytes at a time with AVX2" else "16 bytes at a time") ++
+      ", and keeping (by masks) the one of the digit's magnitude, its `y` negated by a mask of its \
+      sign, by Jacobian addition with the entry's `Z²` and `Z³`, whose exceptional cases (equal \
+      or opposite points) do not arise for `d < n`; the sum is kept, by masks, unless the digit \
+      is zero, and the entry in its place where the accumulator is the point at infinity; \
       `Z⁻¹` is by the signature's divsteps. The result (or zeros) is selected by a mask of the \
       checks, `d` in `[1, n-1]` and `Z ≠ 0`, so the time depends only on the pointers."])
     code
     contract := Spec.Ecdh.Instance.exchangeContract Spec.EcKey.P256.inst X86_64.abi
     verified := hv
     spSafe := hsp
-    features := if adx then ["bmi2", "adx"] else [] }
+    features := if adx then ["bmi2", "adx", "avx", "avx2"] else [] }
 
-def artifacts (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) : List Artifact := [
+def artifacts (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) : List Artifact := [
   exchange false Impl.Ecdh.X86_64.exchangeP256
-    (Proof.Ecdh.X86_64.ecdh_verified h.law h.inv) (Code.all_of_allInstrs (by lit_decide)),
+    (Proof.Ecdh.X86_64.ecdh_verified h.law h.inv h.prime) (Code.all_of_allInstrs (by lit_decide)),
   exchange true Impl.Ecdh.X86_64.exchangeP256Adx
-    (Proof.Ecdh.X86_64.ecdh_verified_adx h.law h.inv) (Code.all_of_allInstrs (by lit_decide))]
+    (Proof.Ecdh.X86_64.ecdh_verified_adx h.law h.inv h.prime) (Code.all_of_allInstrs (by lit_decide))]
 
 end VG.Generic.P256.X86_64.EcdhP256

lean/VerifiedGarbage/Generic/P256/X86_64/EcdsaP256.lean

@@ -1,5 +1,6 @@
 import VerifiedGarbage.TCB.X86_64.Target
 import VerifiedGarbage.Proof.Weierstrass.Law
+import VerifiedGarbage.Proof.Weierstrass.X86_64.InvInterface
 import VerifiedGarbage.Proof.P256.Comb7
 import VerifiedGarbage.Impl.Ecdsa.P256.X86_64
 import VerifiedGarbage.Proof.Ecdsa.X86_64.Verified
@@ -15,8 +16,8 @@ import VerifiedGarbage.Proof.Ecdsa.Verify.X86_64.LitAdx
 /-!
 # ECDSA over P-256 (FIPS 186-5) on x86-64
 
-A generic file (see `TCB/Emit.lean`) over P-256's group law and
-inversions `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
+A generic file (see `TCB/Emit.lean`) over P-256's group law,
+inversions and prime order `h`, the variant `Variants/P256/X86_64/Law.lean`, for each
 multiplication: the baseline's, and BMI2's and ADX's, with the comb's
 selection by AVX2 (`_adx`).
 -/
@@ -102,7 +103,7 @@ def verify (adx : Bool) (code : Prog X86_64.isa)
     spSafe := hsp
     features := if adx then ["bmi2", "adx"] else [] }
 
-def artifacts (h : Proof.Weierstrass.X86_64.HasLawInv Spec.P256.curve) : List Artifact := [
+def artifacts (h : Proof.Weierstrass.X86_64.HasLawInvOrd Spec.P256.curve) : List Artifact := [
   sign false Impl.Ecdsa.X86_64.signP256
     (Proof.Ecdsa.X86_64.sign_verified h.law (Proof.P256.combOk7 h.law) h.inv) (Code.all_of_allInstrs (by lit_decide)),
   verify false Impl.Ecdsa.Verify.X86_64.jointVerifyP256

lean/VerifiedGarbage/Impl/Ecdh/P256/X86_64.lean

@@ -1,16 +1,23 @@
 import VerifiedGarbage.Impl.Ecdh.X86_64
 import VerifiedGarbage.Impl.Ecdsa.P256.X86_64
+import VerifiedGarbage.Impl.P256.X86_64.DoubleHalfPublic
 
-/-! # ECDH over P-256 on x86-64: four-word field elements and scalars -/
+/-! # ECDH over P-256 on x86-64: four-word field elements and scalars, by the
+Jacobian window method (`Cfg.exchangeJ`, P-256 having prime order) with the
+doubling by halving (`Impl/P256/X86_64/DoubleHalfPublic.lean`) -/
 
 namespace VG.Impl.Ecdh.X86_64
 
 open VG.X86_64
 
 /-- `vg_ecdh_p256`. -/
-def exchangeP256 : Prog isa := Cfg.exchange Impl.Ecdsa.X86_64.p256
+def exchangeP256 : Prog isa :=
+  Cfg.exchangeJ Impl.Ecdsa.X86_64.p256
+    (Impl.P256.X86_64.doubleHalfPublic Impl.Ecdsa.X86_64.p256.MP' Impl.Ecdsa.X86_64.p256.rcbSlots)
 
 /-- `vg_ecdh_p256_adx`. -/
-def exchangeP256Adx : Prog isa := Cfg.exchange Impl.Ecdsa.X86_64.p256x
+def exchangeP256Adx : Prog isa :=
+  Cfg.exchangeJ Impl.Ecdsa.X86_64.p256x
+    (Impl.P256.X86_64.doubleHalfPublic Impl.Ecdsa.X86_64.p256x.MP' Impl.Ecdsa.X86_64.p256x.rcbSlots)
 
 end VG.Impl.Ecdh.X86_64

lean/VerifiedGarbage/Impl/Ecdh/X86_64.lean

@@ -1,4 +1,5 @@
 import VerifiedGarbage.Impl.Ecdsa.X86_64
+import VerifiedGarbage.Impl.Weierstrass.X86_64.WinJac
 
 /-!
 # ECDH on x86-64
@@ -160,10 +161,51 @@ def middle : Prog isa :=
     Mont.X86_64.mul c.MP' (c.sl X) (c.sl XM) (c.sl ONE),
     c.checkRange (c.sl D) ++ c.checkNonzero (c.sl RZ) ++ finish c]
 
-/-- `vg_ecdh_<curve>`. -/
-def exchange : Prog isa :=
+/-! ## Windows of 5 bits in Jacobian coordinates, for a curve of prime order -/
+
+/-- The digits of the Jacobian window method, for scalars below `2^nbits`:
+`⌈(nbits + 2) / 5⌉`, enough for the recoding's carry. -/
+def jwinJ : Nat := (c.nbits + 6) / 5
+
+/-- The Jacobian window method's areas: its scalar and bits where the other
+window method's are, its table where that one's starts (16 entries of five
+coordinates), and the selected entry past it. -/
+def jwinCfg : JacWinCfg where
+  M := c.MP'
+  S := c.rcbSlots
+  P := c.pt PX PY ONEP
+  R := c.pt RX RY RZ
+  D := c.pt DX DY DZ
+  T := c.winTbl + 16 * (40 * c.n)
+  neg := c.sl PT
+  zero := c.sl ZERO
+  bits := c.winBits
+  tbl := c.winTbl
+  J := jwinJ c
+  one := c.mont 1
+  avx2 := c.MP'.adx
+
+/-- `d + offset J` and its bits, from the slot of `d`. -/
+def jwinPrep : Prog isa :=
+  .seq (.block (WinCfg.addConst c.n (c.sl K) c.winK (JacWinCfg.offset (jwinJ c))))
+    (bits c.winK c.winBits (8 * (c.n + 1)))
+
+/-- `[d]P` into `R` by the Jacobian window method, `dbl` doubling a point in
+place. -/
+def mulQJ (dbl : Pt → Prog isa) : Prog isa :=
+  .seq (.block (maskK c)) (.seq (jwinPrep c) ((jwinCfg c).window dbl))
+
+/-- `vg_ecdh_<curve>`, with `mq` computing `[d]P` into `R`. -/
+def exchangeWith (mq : Prog isa) : Prog isa :=
   .seq (.block (args)) <| .seq (prefix' c none) <| .seq (.block (peer c)) <| .seq (validate c) <|
-  .seq (mulQ c) <| .seq c.pPow (middle c)
+  .seq mq <| .seq c.pPow (middle c)
+
+/-- `vg_ecdh_<curve>` by the Jacobian window method, for a curve of prime
+order. -/
+def exchangeJ (dbl : Pt → Prog isa) : Prog isa := exchangeWith c (mulQJ c dbl)
+
+/-- `vg_ecdh_<curve>`. -/
+def exchange : Prog isa := exchangeWith c (mulQ c)
 
 end Cfg