Repository navigation
x86-64 Ed25519: fold sums of products once in every field program - #1472
Merged
Merged
Conversation
fieldCode now folds the carry of a sum, or the borrow of a difference, once (addL, subL) wherever one operand of the sum, or the subtrahend, is bounded by 2p, as products and constants are: it tracks, through the program, which slots it last wrote with one (bndStep), and chooses each operation's code by it (fieldCodeFrom). The doublings of verification and of the comb, and four of the six sums and differences of verification's cached addition, read products of the same block. The proofs: the tracking and the per-operation lemmas move from FieldLazy.lean to Field.lean, where fieldCodeFrom_ok proves the program under any initial bounds; fieldCode_ok follows, so its users are unchanged. From the analysis of the rustls provider in #991. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RLVbycsRXKPfaW1swVZejG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#1398 folded the comb's additions' sums and differences once (
addL,subL) where an operand is at most2p, as every product is. This applies the same rule to every x86-64 Ed25519 field program, automatically:fieldCodenow tracks, through the program, which slots it last wrote with a product or a constant (bndStep), and folds each sum once if one of its operands is such a slot, and each difference once if its subtrahend is (fieldCodeFrom,opOk). Programs read nothing about earlier blocks, so a slot written before the program counts as unbounded.That covers the doublings of verification and of the comb (
dblOps:B - AandA + B, withA,Bsquares) and four of the six sums and differences of verification's cached addition (pointAddCachedOps, whose last four read its products). The two that read the accumulator, andC - (B - A)in the doubling, keep both folds.Proof
No change to
Spec/orTCB/.Impl/Ed25519/X86_64/Field.lean:FieldOp.out,FieldOp.bnd,bndStep,opOkandbndOut(moved fromProof/.../FieldLazy.lean, since code generation now uses them;bndStepis anif, not Mathlib'sFunction.update),fieldCodeFrom, andfieldCodeasfieldCodeFromfrom no bounded slot.Proof/Ed25519/X86_64/Field.lean:Bnd,EdArith.mulBnd/sqrBnd,bnd_afterandfieldOpB_ok(moved fromFieldLazy.lean),opOk_self, andfieldCodeFrom_ok, the program under any initial bounds, with the bounds after it.fieldCode_okkeeps its statement and follows from it, sofieldCodeWide_okand every user are unchanged.Proof/Ed25519/X86_64/FieldLazy.lean:fieldCodeFromWide_oklifts it to the wide scratch;fieldCodeWide_accandfieldCodeWide_accKeep(the comb's accumulator bounds from x86-64 Ed25519/X25519: the comb's sums and differences folded once #1398) use it.Measurements
On a Sapphire Rapids Xeon, against main, fastest of eleven interleaved runs of each side (
ci/bench_compare.py --rounds 11 --measurement-time 2),VG_CPU_FEATURES=avx,avx2,bmi1,bmi2,adx:ed25519_keygen/32ed25519_sign/64ed25519_verify/64ed25519_verify/1024ed25519_verify/16384With the baseline and with all of this CPU's features (the
_ifmavariants, whose verification multiplies in vector lanes), fastest of five, everything moved by under 2% either way except baselineed25519_verify/16384(3.8% slower in one run of five, which SHA-512 over 16 KiB dominates; the code it runs there is unchanged). X25519's key generation uses the comb's doublings too.Why
From the analysis of the rustls provider in #991: after the signing work (#1360, #1377, #1398, #1421), verification without AVX512_IFMA was next.
🤖 Generated with Claude Code
https://claude.ai/code/session_01RLVbycsRXKPfaW1swVZejG
Generated by Claude Code