[Japabu]

Status: draft; review r1 LAND pending the AMD boots. T14 and AMD judges passed, and both benches' X25519 constant-time boots; the AMD Ed25519 constant-time boot is staged at 23840e4 and not yet run.

Problem

X25519 and Ed25519 ran on five 51-bit limbs on every target. On the T14 (main 40e5286's cryptocase, ours over ring) X25519 was 1.39, Ed25519 sign 1.37 and verify 1.04. ring's X25519 ladder on x86-64 runs four 64-bit words on MULX/ADCX/ADOX; our x86-64 machine code for the five-limb ladder spills heavily (1,368 stack references in agree), because each mul pins RAX and RDX.

Result

T14 judge (cryptocase, ours over ring, shipped build), main 40e5286 → this branch at 6ea5923:

row	main	branch
x25519/ecdh	1.391	1.276
ed25519/sign/64	1.365	1.088
ed25519/verify/64	1.038	0.819 (pass)

AMD bench judge at 23840e4 (the same crate tree): x25519/ecdh 1.225, ed25519/sign/64 1.116, ed25519/verify/64 0.743 (pass). No recent AMD judge of main's 25519 rows exists to compare with.

X25519 and sign remain above ring on both benches: our agreement ladder is still slower than ring's.

Constant time on the T14 (1,000,000 measurements a routine, threshold 4.5): X25519 agreement max |t| 2.30, X25519 public key 1.83, Ed25519 derivation and signature 2.58; leaky controls 1,258 to 1,309, null 1.25 to 2.29. On the AMD bench at 23840e4: X25519 agreement 3.32, public key 2.65; null controls 1.82 and 1.04, leaky 210.6 and 194.7. Recorded in the track issue.

Change

• x86-64: four 64-bit words (field25519/radix64.rs). Any value below 2^256 is an element; whatever passes 2^256 folds back as 38, and only the encoding reduces below p. Multiplication and squaring are BMI2/ADX inline assembly (arch/x86_64/f25519.rs, Intel SDM Vol. 2A MULX/ADCX/ADOX) where CPUID admits them, dispatched per operation as P-256's kernels are (crypto: P-256 field multiplication and squaring on BMI2 and ADX, inline in the point formulas #1036) and inlined into the ladder and the point formulas; otherwise a portable u128 form computes the same words. The kernels use general registers alone, so the UEFI loader takes them too.
• AArch64 keeps five 51-bit limbs (field25519/radix51.rs, moved unchanged). On the development Mac (exploratory, under load) a portable four-word ladder took 30.7 µs against the limbs' 16.0 µs.
• One interface over both. On four words a sum is already a multiplication operand, so Loose is Tight and carry is the identity; the curve code in x25519.rs and ed25519.rs is unchanged. The inversion and square-root chains move to field25519.rs and run on the dispatched operations; compile-time tables invert by square-and-multiply over the portable form (Tight::inverted).
• Edwards doubling forms 2Z^2 by an addition rather than a small multiplication.
• Ed25519 verification's rules (toyos-crypto: Ed25519 verification's rules are explicit, and each disagreement has a verdict #1044) are untouched: no change to decoding, the small-order lists, S < L or k's reduction.

Decisions

• Method. The Linux probes on both benches decide it (main against the branch, same probe): Ed25519 sign 0.797 (T14) and 0.789 (AMD), verify 0.795 and 0.811, the X25519 public key 0.782 and 0.768, X25519 agreement 0.979 and 0.934. ring's own X25519 ladder runs four words on ADX on x86-64, which is the reason to expect it. Against it, crypto: ChaCha20 short messages in one register set, rows from the key (parity item 9, part) #1022's dependent-chain rows put one five-limb multiplication at 0.80 of a four-word MULX one on the T14 (pr-1022/r1/baseline-m11/t14-rows.txt); a chain measures latency, while the ladder and the point formulas keep independent multiplications in flight, and the five-limb x86-64 code spills (1,368 stack references in agree against 726 now). The probes time whole operations.
• Representation per target, not per CPU. Both benches and every modern x86-64 have BMI2 and ADX; a CPU without them (QEMU's qemu64) runs the portable four words, slower than five limbs would be there. Dispatching between two representations at run time would carry both through every curve routine.
• Fermat inversion stays. On ADX the chain and crypto: NIST inversion by Bernstein and Yang's divsteps #1043's divsteps modulo 2^255 − 19 are comparable on the T14: 2.81 against 2.89 µs, from two runs about 3% apart.
• No dual-flag-chain squaring. Running the doubling and the diagonal squares on CF and OF at once changed nothing on either bench (probe25519-1).
• AVX-512 IFMA is not in this PR. The T14 has it; the AMD bench and Intel's client cores since Alder Lake do not. A vectorised ladder is a separate design.

Checks

check	revision	result
cargo run -- --ci host	6ea5923	exit 0, 102 steps
crate tests, [profile.toyos], aarch64-apple-darwin (five limbs)	6ea5923	pass
crate tests, [profile.toyos], x86_64-apple-darwin under Rosetta (portable four words; Rosetta has no BMI2/ADX; the SHA-NI block test skipped, Rosetta has no SHA)	6ea5923	pass
clippy, three forms × two Mac targets, both UEFI targets	6ea5923	clean
kernels in an emulator against integers (scratch, not committed)	6ea5923	22,400 products, 22,020 squares
portable negative controls m4–m6 under Rosetta	6ea5923	each red by its test
kernel negative controls m1–m3	6ea5923	red in the emulator; exit 101 on both benches
Linux on the T14 and the AMD bench: unit tests on the ADX kernels	6ea5923	every 25519 test passes on both; the one failure is ML-KEM's NIST vector file, absent on a bench (ENOENT)
Linux probes, main against the branch	6ea5923	table in evidence r2
T14 cryptocase (judge), cryptoctcase (X25519), cryptoctcurvescase (Ed25519)	6ea5923	all passed, judge exit 0
AMD cryptocase, cryptoctcase	23840e4	both passed, judge exit 0
AMD cryptoctcurvescase (Ed25519)	23840e4	staged, not run
cargo run -- --ci host after the rebase	3be4d6b	exit 0, 102 steps (23840e4 adds only the issue record)
machine code: the staged x86_64-unknown-toyos guests and loader, an aarch64 rlib	6ea5923	no branch on secret data; the setb of carries and of the ladder's scalar bit and the cmov of copy_from_slice's precondition are data-independent; kernels inlined (inspection/README.md)

Evidence

Round 4 (AMD boots): https://github.com/ToyOSOrg/evidence/tree/6488b4fbb6785e65332d03fb504fe3849d89810a/pr-1046/r4

Round 3 (T14 boots): https://github.com/ToyOSOrg/evidence/tree/430684ceb7e0a9af6f1048cdfdfa937eef45d03e/pr-1046/r3

Round 2 (the Linux runs): https://github.com/ToyOSOrg/evidence/tree/f87c7472e440550c4871f155c92b378b9acff10c/pr-1046/r2

Round 1 (host checks, controls, machine code, the staged runs' recipe): https://github.com/ToyOSOrg/evidence/tree/343d2f3453d7f180cf96847ff105c243c18a5f7b/pr-1046/r1

Risks

• The AMD Ed25519 constant-time verdict is open until its staged boot runs.
• No AArch64 bench: the five-limb path is unchanged in representation, and its Mac timings are exploratory.
• Without BMI2/ADX (QEMU TCG's qemu64) X25519 and Ed25519 run the portable four words, slower than five limbs there: as a dependent chain, a four-word multiplication even with MULX intrinsics took 21.4 ns against the limbs' 17.2 ns on the T14 (row m2/f25519-mul/5x51-over-4x64-mulx, crypto: ChaCha20 short messages in one register set, rows from the key (parity item 9, part) #1022's evidence pr-1022/r1/baseline-m11/t14-rows.txt). QEMU's clock is a hang ceiling only.

🤖 Generated with Claude Code

[Japabu]

Review r1: #1046 at 23840e4

I read both commits, the whole diff, every changed file, and the callers in x25519.rs, ed25519.rs (decode, double, encode, verify), arch/mod.rs and arch/x86_64.rs (features(), the portable override). I also read the evidence for r1 (inspection README, mutant patches, Rosetta log), r2 (both Linux runs) and r3 (T14 judge log, README). I ran nothing.

Architecture

The design is sound and has the right owners. Choosing the representation per target is a selector cfg in field25519.rs. Both representations sit behind one Tight/Loose/Multiply interface, so the curve code stays shared. The kernels live in the architecture module and are dispatched through arch::f25519_* with the same public CPUID check that P-256 uses (#1036), and portable still turns them off. Making Loose a type alias of Tight on four words is the right simplification: every [u64; 4] is a valid element, every operation accepts any value below 2^256, and bytes() alone reduces. Nothing has to be enforced on x86-64. On AArch64, where the bounds do matter, Loose stays a distinct type, so curve code that adds two loose values still fails to compile there. The const square-and-multiply inverted is a second, deliberately small inversion. It exists because const fns cannot reach the dispatched trait, and the new const-form test checks it. That is acceptable. Hardware selection is correct: every 2020+ x86-64 has BMI2/ADX, and only a featureless QEMU CPU takes the slower portable four words, which does not cost metal anything.

Size: about +548 production lines (229 of kernel assembly, about 250 of portable four-word arithmetic, about 40 of dispatch glue and the const inversion), and about +115 test lines (the four-word words test, the const-form check, and the radix-51 bound test moved to its module). The asymmetric parity gains on both benches justify the size.

Correctness: what I verified

• ADX mul. In each row, xor clears CF and OF; mulx and mov leave the flags alone; the low halves chain on CF through adcx, the high halves on OF through adox, and both chains close into the row's new top word (adox T, 0; adcx T, 0). The eight-word product cannot overflow. In the fold, the top word is at most 37 + 2 = 39, then 38 × 39 = 1482 is added. If that addition carries out, the low word is below 1482 < 2^11, so the final + 38 cannot carry, as the comment says. Every temporary is out rather than lateout, so no output shares a register with a or b, which are read after the first write. That is 12 reg operands plus rdx, which fits the 13 allocatable GPRs.
• ADX square. The cross products' adc T4, hi carry is taken by adc T5, 0 after the mulx that writes T5. The partial sums stay below 2^384, so nothing is lost. The doubling, the diagonal squares and the fold are the same as mul's.
• Portable form. product/square → reduce → fold computes the same integer t_lo + 38·t_hi and then the same final fold, so its words are identical to the kernels'. The words test asserts exactly this on ADX hardware, and m2 shows it is the only test that can tell the two paths apart.
• sub. The second borrow leaves word 0 at 2^64 − 38 or above, so the second 38 cannot borrow.
• bytes. Folding bit 255 gives v < 2^255 + 19 < 2p, so one conditional subtraction is enough. The selection uses ct::mask.
• Secret independence. The only branches are the public feature check and loop counters. mulx, adcx, adox, imul, sbb and and take no data-dependent time. setb on carries and the scalar bit is a register-only set, not a transfer. The inline asm reads only through readonly pointers.
• Verification verdicts. decode still refuses a non-canonical y by b != y.bytes(). from_bytes masks bit 255 exactly as before. eq, is_negative, encode and the R comparison all go through the canonical bytes, so verdicts depend only on correct arithmetic mod p, not on the representation. toyos-crypto: Ed25519 verification's rules are explicit, and each disagreement has a verdict #1044's rules are not touched.
• Evidence on the ADX kernels. On both benches, the r2 Linux runs printed f25519 path: the BMI2/ADX kernels. The words test, the_comb_agrees_with_straus and public_keys_by_the_comb_are_the_ladders passed, and m1–m3 went red. The one failure is ML-KEM's tests/acvp file being absent on the bench, which is independent of this change. Under Rosetta, the portable form passed 74 tests, and m4–m6 went red there.

Findings

No blockers.

Before landing (orchestrator's gate, not a code defect):

• AMD boots. The AMD judge and X25519 constant-time boots are still open. The kernels are the same instructions on Zen 2, but secret independence on the second bench is a material claim, and a leak there would block.
• Ed25519 constant time on AMD. The AMD request (readback-r2-amd/request.txt) stages only cryptocase and cryptoctcase. The new field also runs Ed25519 key derivation and signing. An AMD X25519 pass does exercise the same kernels, and the track issue already records that the AMD bench has not run the curves program. The cheapest fix is to add cryptoctcurvescase to the AMD batch. Otherwise, the PR's Risks should say that Ed25519 constant time on AMD is not run and that X25519 stands in for the kernels.
• toyos-crypto: Ed25519 verification takes an R of order dividing 8 where the equation holds #1047 is not in the branch's base. Main 4dc75f5 carries toyos-crypto: Ed25519 verification takes an R of order dividing 8 where the equation holds #1047, which changes verify and tests/ed25519_verdicts.rs, and crypto: ChaCha20 short messages in one register set, rows from the key (parity item 9, part) #1022, which touches arch/{mod,x86_64}.rs. The branch is based on 69727e3. git merge-tree merges cleanly. No measured run has paired this field with toyos-crypto: Ed25519 verification takes an R of order dividing 8 where the equation holds #1047's verdict corpus. The merge queue's required host job (ubuntu x86-64, the dispatched form) runs that corpus on the merged tree, so I do not require a separate run. The owner's verdict constraint is established when that job is green, not before.

SUGGESTION

• PR "Checks" row on machine code. It says "no transfer, cmov or set on secret data". The inspection README's own table lists setb after the portable additions' carries and bt eax,edx; setb sil on the ladder's scalar bit. These are constant-time register sets, so secret independence holds, but the sentence is literally false. Suggested wording: "no transfer or cmov on secret data; setb only materialises carries and the scalar bit". The README's summary line has the same wording. The PR text is the orchestrator's to correct.
• PR "Decisions: Fermat inversion stays". The 2.81 µs (Fermat on ADX, this probe) and 2.89 µs (crypto: NIST inversion by Bernstein and Yang's divsteps #1043's divsteps) come from different runs, about 3% apart, and the AMD has no divsteps figure. The decision is sound because nothing measured gains and keeping Fermat adds no code, but the figures do not show that Fermat is faster. They should be presented as "comparable".
• lib/crypto/src/arch/x86_64.rs:207-208. "The kernels use general registers alone, so UEFI takes them too" repeats the module header's new sentence (lines 2–3). Deleting it from the f25519_mul doc leaves one statement of that contract.
• Machine-code inspection on AArch64. It used an aarch64-apple-darwin rlib, not aarch64-unknown-toyos. The radix-51 arithmetic is unchanged, but double and the dispatched chains changed on AArch64 too. When the next AArch64 image is built, disassembling its crypto_constant_time* would cover the shipped target. This is low risk and not required here.

LAND

[Japabu]

Landing at 2840639. Review r1 returned LAND, pending the AMD boots, which have now all run at 23840e4. The later commits change only comments and the issue record.

• AMD judge: crypto_instrument PASS. Against ring: x25519 1.225, ed25519 sign 1.116, verify 0.743.
• AMD constant time: crypto_secret_timing (X25519 agreement 3.32, public key 2.65) and crypto_secret_timing_curves (Ed25519 2.95; P-256 1.94 and 2.15; P-384 3.19 and 2.23) PASS, with the leaky and null controls holding.
• T14: all three boots passed at 6ea5923, whose crate is byte-identical.
  The merge queue's host job runs toyos-crypto: Ed25519 verification takes an R of order dividing 8 where the equation holds #1047's verdict tests against this field.