perf(ed25519): verify without ADX through curve25519-dalek's AVX2 backend

ALGORITHMS.md

@@ -19,7 +19,8 @@ x86_64 runs every feature. Each column to its right denies more, as
 and VPCLMULQDQ (Sandy Bridge); no AVX also AVX (Westmere); no AES-NI also
 AES-NI, PCLMULQDQ, and SSE4.1 (Core 2); and SSE2 also SSSE3. Without ADX
 alone (Haswell), rind runs the same sources as x86_64, through s2n-bignum's
-routines that don't use it.
+routines that don't use it, except that Ed25519 verification runs
+curve25519-dalek ⚡ (see below).
 CPUs with AVX2 but without SHA-NI run [OpenSSL]'s AVX2 SHA-256, and CPUs
 with the SHA512 instructions its SHA-384 and SHA-512 for them. Intel CPUs
 without AVX2 run [aws-lc]'s AVX SHA-1, SHA-256, and verified ✓ SHA-384 and
@@ -70,6 +71,12 @@ SHA-512.
   key or 32 B seal.
 - P-256 without ADX: verification runs s2n-bignum's verified routines rather
   than aws-lc's `ecp_nistz256`.
+- Ed25519 verification without ADX: on CPUs with AVX2, `[S]B - [k]A` runs a
+  port of curve25519-dalek's AVX2 backend, variable-time over public inputs,
+  rather than s2n-bignum's verified `edwards25519_scalarmuldouble_alt`, a
+  constant-time fixed-window loop. Verification fell from 1.31× to 1.09×
+  curve25519-dalek's time on an i7-8700 with ADX denied, and from 1.30× to
+  1.08× on an OVH VPS whose virtual CPU hides ADX.
 - ChaCha20-Poly1305 without AES-NI and on SSE2, which lack SSE4.1: rind runs
   Graviola's scalar Poly1305 there, and aws-lc BoringSSL's SSE2
   `poly1305_vec.c`, which rind doesn't port for CPUs older than Westmere.
@@ -124,7 +131,7 @@ tests use [Wycheproof]'s vectors.
 | [aws-lc] | copied, by `admin/import-aws-lc`: its SHA-384/512 assembly for x86_64 and aarch64, its x86_64 AVX SHA-256 routine and its aarch64 one for the SHA-256 instructions, Montgomery multiplication and the x86_64 exponentiation's `bn_power5` (with one deliberate change: rind's `bn_sqr8x_mont` and `bn_powerx5` zero two scratch words their `mulx` squaring reads unwritten, which valgrind reports though results and timing do not depend on them), AVX2 and dual AVX-512 RSAZ exponentiation, AES-NI AES-CTR, P-256's generator multiplication (its row scan and mixed addition), and SSE4.1 and AVX2 ChaCha20-Poly1305 (with one deliberate change: rind's copy reads the choice of AVX2 from the block rind passes it rather than aws-lc's `OPENSSL_ia32cap_P`), its aarch64 NEON ChaCha20-Poly1305, its x86_64 assembly for CPUs without AVX2 (SSSE3 ChaCha20, SSSE3 and AVX SHA-1, and SSSE3 SHA-256) without AES-NI (SSSE3 AES and GHASH), and without SSSE3 (integer SHA-1 and SHA-256), its aarch64 Montgomery multiplication, and its aarch64 assembly for CPUs without the crypto extension (NEON AES, NEON GHASH, and scalar SHA-1 and SHA-256), as Rust naked functions; its 32-bit ARM assembly for ChaCha20, SHA-384/512, Montgomery multiplication, the ARMv8 crypto extension (AES, GHASH, SHA-1, SHA-256), and NEON Poly1305, in Rust `global_asm!`; and the C that drives that Poly1305, RSAZ, and `bn_power5`, that sets up its x86_64 SSSE3 GHASH table, and that computes its constant-time SSE2 AES and integer GHASH for x86_64 CPUs without SSSE3, ported to Rust, the GHASH also for armv7 without the crypto extension. aws-lc takes its Poly1305, ChaCha20-Poly1305, SSSE3 GHASH, and constant-time AES and GHASH from BoringSSL and the rest from OpenSSL | Apache-2.0; Poly1305, ChaCha20-Poly1305, SSSE3 and integer GHASH, and constant-time AES ISC | [SAW and NSym proofs](https://github.com/awslabs/aws-lc-verification/tree/797302470c1703cbb1a3a6fa98daffef0bfd3d80) that its x86_64 AVX and aarch64 scalar SHA-384/512 routines compute their specified result for all inputs. The proof of its aarch64 routine for the SHA-512 instructions ends with the result in registers, before the routine stores it, so earns no ✓. They check aws-lc's own build, not rind's copy, and do not cover its 32-bit ARM code. [`proofs/`](proofs/README.md) proves rind's SHA-384/512 around the AVX and aarch64 scalar routines. |
 | [BoringSSL] | copied, by `admin/import-boringssl`: its x86_64 VAES AES-GCM assembly, `aes-gcm-avx2-x86_64` and `aes-gcm-avx512-x86_64`, as Rust naked functions; its 32-bit ARM NEON X25519 assembly, in Rust `global_asm!`, which BoringSSL takes from [SUPERCOP]'s `neon2`, public domain | Apache-2.0 | nothing |
 | [OpenSSL] | copied, by `admin/import-openssl`: its x86_64 AVX2 SHA-256 and SHA-512 assembly and its SHA-512 assembly for the SHA512 instructions, from `sha512-x86_64`, as Rust naked functions; its 32-bit ARM Keccak-f assembly, integer and NEON, `keccak1600-armv4`, in Rust `global_asm!` | Apache-2.0 | nothing |
-| [curve25519-dalek] | dependency, with its serial 32-bit backend | BSD-3-Clause | nothing: that backend's field arithmetic is hand-written. Its `fiat` backend would run [fiat-crypto]'s verified field arithmetic instead, but only a `--cfg` flag for the whole build selects it, so rind refuses it rather than let the build pick. |
+| [curve25519-dalek] | dependency, with its serial 32-bit backend, for armv7; ported: its AVX2 backend's field arithmetic, point formulas, and base point table, and its scalars' non-adjacent forms, to Rust intrinsics, for Ed25519 verification on x86_64 CPUs with AVX2 but without ADX | BSD-3-Clause | nothing: that backend's field arithmetic is hand-written, as is the AVX2 backend's. Its `fiat` backend would run [fiat-crypto]'s verified field arithmetic instead, but only a `--cfg` flag for the whole build selects it, so rind refuses it rather than let the build pick. |
 | [fiat-crypto] | dependency | MIT OR Apache-2.0 OR BSD-1-Clause | [Coq proofs](https://github.com/mit-plv/fiat-crypto/tree/67316f05d771f7f2db62beede59e9b56406a9efd) that each generated field operation is correct. rind's point formulas, inversion, and table lookup over them are not covered. |
 
 rind's own code is licensed under Apache-2.0 OR ISC OR MIT-0. Copied code
@@ -133,8 +140,9 @@ texts they require; dependencies ship their own. Every file under
 `rind/src` names its license in a `SPDX-License-Identifier` comment, and
 files Graviola wrote keep their `Written for Graviola by ...` header. The
 `rind` crate as a whole is therefore `(Apache-2.0 OR ISC OR MIT-0) AND
-(Apache-2.0 OR ISC OR MIT) AND Apache-2.0 AND ISC`. The adapter crates copy
-nothing under another license, so they stay `Apache-2.0 OR ISC OR MIT-0`.
+(Apache-2.0 OR ISC OR MIT) AND Apache-2.0 AND ISC AND BSD-3-Clause`. The
+adapter crates copy nothing under another license, so they stay
+`Apache-2.0 OR ISC OR MIT-0`.
 rind-ring runs ring's own tests, which keep ring's licenses and stay out of
 the published crate.
 
@@ -204,8 +212,11 @@ only which candidates it discards.
 
 ### ECC
 On x86_64 and aarch64, all ECC field and scalar arithmetic are provided by
-s2n-bignum, except P256's on x86_64 where aws-lc's is named below, and the
-rest of this section describes those backends.
+s2n-bignum, except P256's on x86_64 where aws-lc's is named below, and
+Ed25519 verification's on x86_64 CPUs with AVX2 but without ADX, which runs
+curve25519-dalek's AVX2 backend over width-5 and width-8 non-adjacent forms
+of its two scalars, the latter over a 10 KiB table of the base point's odd
+multiples. The rest of this section describes those backends.
 
 P256 base point multiplication on x86_64 is aws-lc's: 7-bit Booth windows over
 37 rows of 64 affine points (a 152KB constant table), each row scanned whole

BENCHMARKS.md

@@ -709,9 +709,9 @@ Each operation where another library is more than 10% faster than rind, on a hos
 | SHA-256, 64 B | `nixos` | 1.17× (RustCrypto + dalek) | Narrowed by [#352](https://github.com/moq-dev/rind/pull/352): on the SHA extensions the last block is padded and the digest written in registers, and `digest::Context::finish` takes `&mut self`, so it no longer copies the context. Closed by [#394](https://github.com/moq-dev/rind/pull/394), after this data, which drops the context's wipe on drop: on GitHub's AMD EPYC 9V45 runner it measured rind at 0.84× main's time at 64 B and 0.86× RustCrypto's. The next refresh drops this entry. |
 | RSA-2048 PKCS#1 sign | `nixos` | 1.10× (graviola) | Noise: other work kept 5 CPUs busy during this run, in which PSS signing, the same exponentiation, measured 0.95× graviola's time. Interleaved runs on `nixos` the same morning measured rind's PKCS#1 signing at 436 to 446 µs against graviola's 432 to 542 µs and ring's 459 to 568 µs. The next refresh rechecks it. |
 | 1 MB transfer, AES-128-GCM, XChaCha20-Poly1305 seal, 1350 B | `desktop` | 1.11× to 1.22× (aws-lc-rs, ring) | Noise: other work kept 5 CPUs busy during this run. The run before it measured 0.99× ring's and 0.97× aws-lc-rs's time, and neither shows on another host. The next refresh rechecks both. |
-| Ed25519 verify | `ovh-iad`, `ovh-sea` | 1.29× to 1.30× (RustCrypto + dalek) | These VPSes' virtual CPUs hide ADX, as CPUs older than Broadwell and Zen lack it, and there rind runs s2n-bignum's verified `_alt` routines, which RustCrypto's AVX2 backend beats. |
+| Ed25519 verify | `ovh-iad`, `ovh-sea` | 1.29× to 1.30× (RustCrypto + dalek) | These VPSes' virtual CPUs hide ADX, and there rind ran s2n-bignum's verified `_alt` routines, which RustCrypto's AVX2 backend beats. Closed by [#415](https://github.com/moq-dev/rind/pull/415), after this data, which runs a port of that backend there: its collection measured rind at 1.08× RustCrypto's time on both VPSes. The next refresh drops this entry. |
 | Ed25519 sign | `ovh-iad` | 1.13× (aws-lc-rs) | Noise from the VPS's other tenants: `ovh-sea`, the same virtual CPU, measured 0.92× aws-lc-rs's time, and no dedicated host shows it. The next refresh rechecks it. |
-| `p256-ecdsa-verify/*` | no ADX tier | 1.14× (aws-lc-rs) | Only CPUs older than Broadwell and Zen lack ADX, and there rind runs s2n-bignum's verified `_alt` routines. |
+| `p256-ecdsa-verify/*` | no ADX tier | 1.14× (aws-lc-rs) | CPUs older than Broadwell and Zen lack ADX, and so do virtual CPUs that hide it, as `ovh-iad`'s and `ovh-sea`'s do. There rind runs s2n-bignum's verified `_alt` routines, which trail by more than 10% only on the nightly runners: on the VPSes P-256 verification measured 1.05× aws-lc-rs's time. |
 | `chacha20poly1305/*/16KB`, `xchacha20poly1305/*/16KB` | no AES-NI tier | 1.17× (aws-lc-rs) | Without SSE4.1 rind runs Graviola's scalar Poly1305 rather than port BoringSSL's SSE2 `poly1305_vec.c` for CPUs older than Westmere, as ALGORITHMS.md records. |
 
 ## Verified code

LICENSE

@@ -214,6 +214,17 @@ OpenSSL <https://github.com/openssl/openssl>
   Copyright 2017-2026 The OpenSSL Project Authors. All Rights Reserved.
   License: Apache-2.0. OpenSSL has no NOTICE file.
 
+curve25519-dalek <https://github.com/dalek-cryptography/curve25519-dalek>
+
+  What: rind/src/low/x86_64/edwards25519_scalarmuldouble_avx2.rs, a port
+  of curve25519-dalek 5.0.0's AVX2 backend (its field arithmetic, point
+  formulas, and table of the base point's odd multiples) and its scalars'
+  non-adjacent forms, for Ed25519 verification on x86_64 CPUs with AVX2 but
+  without ADX.
+  Copyright (c) 2016-2021 isis agora lovecruft. All rights reserved.
+  Copyright (c) 2016-2021 Henry de Valence. All rights reserved.
+  License: BSD-3-Clause.
+
 --
 
 SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
@@ -476,3 +487,37 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
+
+
+BSD 3-Clause license
+-------------------------------------
+
+Copyright (c) 2016-2021 isis agora lovecruft. All rights reserved.
+Copyright (c) 2016-2021 Henry de Valence. All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+contributors may be used to endorse or promote products derived from
+this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

PLATFORMS.md

@@ -31,12 +31,14 @@ Android are untested.
   Bobcat and Bulldozer, and QEMU's default `qemu64` model, AES and GHASH run
   Rust ports of [aws-lc]'s constant-time SSE2 and integer C, SHA1 and SHA256
   its integer assembly, and ChaCha20 [HACL\*]'s verified rounds.
-  Without `adx`, as on Haswell and AMD's cores before Zen, [s2n-bignum]'s
-  `_alt` routines replace those that use it, and [aws-lc]'s Montgomery
-  multiplication replaces its Karatsuba routines for RSA; with `avx2` there,
-  as on Haswell, RSA-2048 signing runs aws-lc's RSAZ exponentiation. With
-  `avx512ifma`, as on Ice Lake, Sapphire Rapids, and AMD's Zen 4 and 5,
-  RSA-2048, 3072, and 4096 signing runs aws-lc's dual AVX-512 RSAZ.
+  Without `adx`, as on Haswell, AMD's cores before Zen, and virtual CPUs
+  that hide it, [s2n-bignum]'s `_alt` routines replace those that use it,
+  and [aws-lc]'s Montgomery multiplication replaces its Karatsuba routines
+  for RSA; with `avx2` there, as on Haswell, RSA-2048 signing runs aws-lc's
+  RSAZ exponentiation, and Ed25519 verification a port of
+  [curve25519-dalek]'s AVX2 backend. With `avx512ifma`, as on Ice Lake,
+  Sapphire Rapids, and AMD's Zen 4 and 5, RSA-2048, 3072, and 4096 signing
+  runs aws-lc's dual AVX-512 RSAZ.
 - 32-bit `arm` (tested on `armv7-unknown-linux-gnueabihf`, and built for
   `armv7-linux-androideabi`) runs portable Rust instead, mostly from
   [libcrux] (see [ALGORITHMS.md](ALGORITHMS.md)), and needs no CPU features. RSA's
@@ -59,6 +61,7 @@ at startup to get an error naming the missing feature instead.
 family since 2004, and of some AMD cores.
 
 [s2n-bignum]: https://github.com/awslabs/s2n-bignum
+[curve25519-dalek]: https://github.com/dalek-cryptography/curve25519-dalek
 [HACL\*]: https://github.com/hacl-star/hacl-star
 [mlkem-native]: https://github.com/pq-code-package/mlkem-native
 [libcrux]: https://github.com/cryspen/libcrux

admin/parse-asm/driver.ed25519.py

@@ -201,6 +201,39 @@
         )
         parse_file(input, d)
 
+    # bignum_inv_p25519 (x86_64)
+    with (
+        open("../../thirdparty/s2n-bignum/x86/curve25519/bignum_inv_p25519.S") as input,
+        generated("../../rind/src/low/x86_64/bignum_inv_p25519.rs") as output,
+    ):
+        d = RustDriver(output, Architecture_amd64)
+        d.emit_rust_function(
+            "bignum_inv_p25519",
+            parameter_map=[
+                ("inout", "z.as_mut_ptr() => _"),
+                ("inout", "x.as_ptr() => _"),
+            ],
+            rust_decl="fn bignum_inv_p25519(z: &mut [u64; 4], x: &[u64; 4])",
+        )
+        parse_file(input, d)
+
+    # bignum_mul_p25519_alt (x86_64)
+    with (
+        open("../../thirdparty/s2n-bignum/x86/curve25519/bignum_mul_p25519_alt.S") as input,
+        generated("../../rind/src/low/x86_64/bignum_mul_p25519_alt.rs") as output,
+    ):
+        d = RustDriver(output, Architecture_amd64)
+        d.emit_rust_function(
+            "bignum_mul_p25519_alt",
+            parameter_map=[
+                ("inout", "z.as_mut_ptr() => _"),
+                ("inout", "x.as_ptr() => _"),
+                ("inout", "y.as_ptr() => _"),
+            ],
+            rust_decl="fn bignum_mul_p25519_alt(z: &mut [u64; 4], x: &[u64; 4], y: &[u64; 4])",
+        )
+        parse_file(input, d)
+
     # bignum_neg_p25519 (x86_64)
     with (
         open("../../thirdparty/s2n-bignum/x86/curve25519/bignum_neg_p25519.S") as input,

benchmarks/gaps.toml

@@ -31,7 +31,7 @@ reason = "Noise: other work kept 5 CPUs busy during this run. The run before it
 [[gap]]
 operations = ["ed25519-verify"]
 on = ["ovh-iad", "ovh-sea"]
-reason = "These VPSes' virtual CPUs hide ADX, as CPUs older than Broadwell and Zen lack it, and there rind runs s2n-bignum's verified `_alt` routines, which RustCrypto's AVX2 backend beats."
+reason = "These VPSes' virtual CPUs hide ADX, and there rind ran s2n-bignum's verified `_alt` routines, which RustCrypto's AVX2 backend beats. Closed by [#415](https://github.com/moq-dev/rind/pull/415), after this data, which runs a port of that backend there: its collection measured rind at 1.08× RustCrypto's time on both VPSes. The next refresh drops this entry."
 
 [[gap]]
 operations = ["ed25519-sign"]
@@ -41,7 +41,7 @@ reason = "Noise from the VPS's other tenants: `ovh-sea`, the same virtual CPU, m
 [[gap]]
 operations = ["p256-ecdsa-verify/*"]
 on = ["no ADX"]
-reason = "Only CPUs older than Broadwell and Zen lack ADX, and there rind runs s2n-bignum's verified `_alt` routines."
+reason = "CPUs older than Broadwell and Zen lack ADX, and so do virtual CPUs that hide it, as `ovh-iad`'s and `ovh-sea`'s do. There rind runs s2n-bignum's verified `_alt` routines, which trail by more than 10% only on the nightly runners: on the VPSes P-256 verification measured 1.05× aws-lc-rs's time."
 
 [[gap]]
 operations = ["chacha20poly1305/*/16KB", "xchacha20poly1305/*/16KB"]

proofs/README.md

@@ -201,7 +201,10 @@ The spec, in `Rind/Ed25519.lean`, is RFC 8032 over HOL Light's
 `edwards25519_group`, whose multiplication and power stay opaque, with
 s2n-bignum's `ed25519_encode` and `ed25519_decode` of its points. Each theorem
 assumes `Runs` and `RunsSha512`, and each with a message bounds it at
-2^64 - 64 bytes. That a multiple of the base point is a point of the group,
+2^64 - 64 bytes. The two that verify also assume `RunsDouble`: on x86_64
+that a CPU without ADX lacks AVX2 too, since with it rind runs a port of
+curve25519-dalek's AVX2 backend, which nothing proves, and on aarch64
+nothing. That a multiple of the base point is a point of the group,
 which `ed25519_key_pair_verify` assumes, is the group's theory, which these
 theorems do not import. `PublicKey` reaches each algorithm's key parser, and
 each parsed key its verification, through function pointers, which

proofs/Rind/Aarch64/S2nBignum.lean

@@ -328,6 +328,10 @@ reads an input. -/
 def Runs : Prop :=
   (∃ e, low.entry.Entry.new_secret = ok e) ∧ (∃ e, low.entry.Entry.new_public = ok e)
 
+/-- Ed25519 verification's double scalar multiplication runs s2n-bignum's
+routine, as it does on every aarch64 CPU. -/
+def RunsDouble : Prop := True
+
 @[step]
 theorem new_secret_spec (h : Runs) : low.entry.Entry.new_secret ⦃ _ => True ⦄ := by
   obtain ⟨⟨e, he⟩, -⟩ := h