[Japabu]

Based on main (27ab916, after #990 and #992 merged; rebased unchanged). Three commits: round 0, a488389; round 1, b47ac40; round 2, b824d27.

Problem

Ed25519 verify was 3.38x ring on the T14 after #992 (179.7 us against 53.1), and sign 7.34x. Verification ran two separate 256-step double-and-add multiplications and decoded R and the public key with an inversion plus a power each. It checked small order by three doublings and a projective compare, and reduced k with a 512-step shift-and-subtract loop. Signing reduced three times bit by bit, multiplied mod L by 256 conditional additions, and re-reduced the static secret scalar on every signature.

This is the analysis's item 6 (V1–V4) with E3 and E4. Item 7's comb, which signing needs, is a later PR.

What changes

• Joint multiplication (V1). [s]B − [k]A in one doubling chain (Straus) over width-7 and width-5 NAFs of s and k (Hankerson, Menezes and Vanstone, Guide to ECC, algorithm 3.35).
  • B's 32 odd multiples are a static affine table, built at compile time by const fn with one simultaneous inversion.
  • A's 8 odd multiples are built per verification.
  • Doublings run from projective coordinates through completed points (Hisil, Wong, Carter and Dawson 2008).
  • Additions take cached (A) or affine (B) operands.
• No decode of R; same strict policy (V4).
  • Verification accepts when [s]B − [k]A encodes to R's bytes. A noncanonical R, one off the curve or a negative zero can never equal a canonical encoding.
  • R and the public key are refused when their encoding is one of the eight points of order dividing 8. A decoded key's encoding is canonical, so the list is complete.
  • Visible change: an R that does not decode is now refused as InvalidSignature instead of InvalidPoint. No caller in the tree matches on the variant.
• Single-exponentiation decode (V2). RFC 8032 section 5.1.3: x = u v³ (u v⁷)^((p−5)/8).
• Typed public scalars. The variable-time recoding accepts only PublicScalar, which comes only from canonical (S) and reduce (k). The signing path's secret S does not convert to it.
• Scalars mod L (E3, E4).
  • 512-bit reduction is Barrett's (HAC 14.42, b = 2^64, k = 4) with one masked subtraction. For x < 2^512 the estimate is at most one short, because 2^512/L − μ < 1/4 and the truncation of x / 2^192 adds under 2^−60. A test asserts the bound. HAC's general bound allows a second subtraction. That bound shows it never runs here, and a scratch search over 300,000 structured inputs found none needing it, so it is not written.
  • Signing computes s = k·a + r with one 4x4 product and one reduction.
  • The signing key keeps its clamped scalar reduced once, plus its prefix as a Secret. Both are erased on drop.
• The field's core is const fn. product, square and carry are const fn. The run-time Multiply methods call them, so the table is built from the same code that runs.

Constant time: the sign path (Point::mul and the scalar arithmetic) keeps its fixed schedule and masked selects. All of verify's inputs are public, and its module contract says so.

Review round 2 (b824d27)

• barrett now also wipes q1, the top five words of the secret input, and q3, the quotient, so the contract's "its reduction erases its workspaces" holds.
• Checks: clippy and crate tests in the three CI forms exit 0. cargo run -- --ci host ran on the rebased stack's head 2594dd3, which contains this commit unchanged; exit 0, 87 green: https://github.com/ToyOSOrg/evidence/tree/fca6eb8e7a4dc943b985d3b79eaeb263f704accb/pr-1000/r1-rebased

Review round 1 (cd7960d)

• secret.rs states the settled erasure of S: secret scalars are owners, and their reduction erases its workspaces.
• The scalar oracle's edge values are now multiples of L and their predecessors below 2^512, as its comment says. The false "short by up to two" is gone.
• Tight::times is documented as the const form of Multiply::mul, tight by tight.
• Suggestions declined:
  • 4, five columns of q₃L: the gain is small.
  • 5: PublicScalar::reduce shares barrett with the secret path and so wipes public temporaries. One reduction is simpler, and the wipes cost a few stores.
• Suggestion 6 taken: QEMU logs from here on start with their revision.
• Checks at cd7960d:
  • cargo run -- --ci host: exit 0, 87 steps green. Logs: https://github.com/ToyOSOrg/evidence/tree/f3a54df6253a32c4ff3e3236ebe81b7a01664e1e/pr-997/r2
  • Clippy and crate tests in the three CI forms: exit 0 each.
  • The Barrett subtraction control, rerun on the new edge values: red (scalar25519_reduction_and_signing_arithmetic_match_integer_oracle).

Checks (round 0)

All at 1d0f66a. Logs: https://github.com/ToyOSOrg/evidence/tree/b76a3e5d3e80dff169164774dd61753ac77bf894/pr-997/r1

• cargo run -- --ci host: exit 0, 87 steps green.
• cargo clippy -p toyos-crypto --all-targets with the adopted lints and -D warnings, and cargo test -p toyos-crypto --release, in the three CI forms: exit 0 each. Rosetta x86_64 tests with sign: exit 0. x86_64-unknown-uefi and aarch64-unknown-uefi builds: exit 0.
• cargo test --test toyos-build -- crypto_instrument_prints_its_table (QEMU x86_64): exit 0.
• The existing ring and ed25519-dalek differentials, RFC 8032 and Wycheproof's ed25519 all pass on the new verify and sign.
• New tests: Barrett's constant and its one-subtraction bound; NAF digits recomposing the scalar for widths 2 to 8; the eight small-order encodings; the static table against repeated addition; noncanonical and negative-zero encodings refused; a small-order R that satisfies the cofactorless equation refused; Barrett's edge values against num-bigint.
• Negative controls, each a checked patch applied, built (exit 0), tested with --features sign --release --no-fail-fast, and reverted in the same run:

control	result
μ's low word one less	red: barretts_constant_is_floor_of_2_512_over_l
Barrett's subtraction removed	red: the scalar integer oracle
mul_add squares a instead of multiplying by b	red: the scalar oracle, the Ed25519 differential, RFC 8032
S accepted at or above L	red: RFC 8032 strict rejection, Wycheproof
small-order R check removed	red: a_small_order_r_satisfying_the_equation_is_refused (green before that test existed)
small-order key check removed	red: RFC 8032 strict rejection
decode's multiplication by sqrt(-1) removed	red: small-order test, differential, RFC 8032, Wycheproof
decode's canonical-y check removed	red: noncanonical_encodings_and_negative_zero_are_refused (green before it existed)
decode's negative-zero check removed	red: the same (green before it existed)
a negative B digit added instead of subtracted	red: differential, RFC 8032, Wycheproof
A's table built by steps of A instead of 2A	red: differential, RFC 8032, Wycheproof
verification accepts without comparing	red: RFC 8032, Wycheproof
NAF window sign test >= made >	green: an equivalent mutant. The window is taken only when k is odd, so it never equals 2^(w-1).

The first run also had "Barrett's second subtraction removed" green. The bound in "What changes" shows it unreachable; it is deleted, and the control above removes the one that remains.

Measurements

T14 (readback at 1d0f66a, judge exit 0): ed25519/verify/64 55.3 us against ring's 53.1, 1.041x (was 3.38x after #992, 34.5x at #932). ed25519/sign/64 86.4 us, 6.66x (was 7.34x); the comb is item 7. No other row moved materially.

Readback staged at 1d0f66a (crypto_instrument, cryptocase; exit 2 = Staged, no machine touched). Its rows are this PR's full table; the Ed25519 rows are the ones this PR moves.

• Exploratory, development Mac under other agents' load, a profile like the shipped one, best of 7 batches of 200: verify 41.9 us against ring's 48.3 (0.87); sign 88.3 us against 16.0 (5.53, until the comb). Not a bench measurement.

Risks

• W_B = 7 (32 entries, 3.75 KiB) is the analysis's middle choice. M6 (widths 5, 7 and 8) is not measured. Verify is 1.04x on the T14, so the wider table (M6) is the first lever if it does not pass.
• The UEFI loader target builds but has never run this code.

🤖 Generated with Claude Code

[Japabu]

Review of #997, round 1 (head 1d0f66a, stacked on #992)

I read the commit against 41e89b9 and each changed file in full at the head (ed25519.rs, scalar25519.rs, field25519.rs, test_arithmetic.rs). I also read the module contracts in secret.rs and lib.rs, every caller of PublicScalar and of Ed25519 verify in the tree, spec §3.2 and §4, the evidence at b76a3e5 (CI log, QEMU log, controls with patches and results) and the T14 rows. I ran nothing. I did not read the analysis notes or any ring or BoringSSL source.

Architecture

This is V1–V4 plus E3/E4 as the spec states them.

• Verify. It is variable time over public inputs. That variable time is confined to PublicScalar::naf and verification_point, and its contract is in the module header.
• Sign. It keeps its fixed schedule.
• The base table. It is built at compile time by the same field code that runs, without build.rs or a generated file.
• Size. Net +739/−194. Roughly 200 of the added lines are tests. The rest is mostly the coordinate forms (Projective, Completed, Cached, Niels), Straus and Barrett.
• Metal. The coordinator relayed the T14 result at 1d0f66a, judge exit 0 (readback-pr3/rows-t14.txt):
  • Ed25519 verify is 55.3 µs against ring's 53.1, 1.041× (was 3.38×).
  • Sign is 86.4 µs, 6.66× (was 7.34×; the comb is the next PR).
  • No other row moved materially.
  • The body still shows only the Mac number. The orchestrator should add these.

Correctness, checked by hand

• Formulas.
  • Completed::from_abcd and point follow RFC 8032 §5.1.4's addition (E = B−A, F = D−C, G = D+C, H = B+A; X = EF, Y = GH, Z = FG, T = EH).
  • Projective::double follows its doubling, reading no T.
  • add_cached and add_niels are correct with 2Z and 2dT folded in: Niels has Z₂ = 1, so D = 2Z₁.
  • The sub_* forms are correct negations: they swap y±x and negate the T term, as −Q = (−X, Y, Z, −T) requires.
  • The const add in the table builder is the same formula. The types bound every addition (Tight + Tight → Loose, carry before each product), so #992's bound proof covers these chains.
• Joint multiplication.
  • It computes s·B + k·(−A) = [s]B − [k]A, which is R exactly when [S]B = R + [k]A.
  • A's table is [−A, 3(−A), …, 15(−A)], indexed by |d|/2 for |d| ≤ 15 (W_A = 5).
  • B_ODD has 32 entries, indexed by |d|/2 for |d| ≤ 63 (W_B = 7).
  • The chain runs from the top nonzero digit. Doubling the initial identity is harmless. t.point() is taken only where an addition needs T, and projective() drops T only before a doubling.
  • When s = k = 0 it returns the identity, whose encoding is in SMALL_ORDER, so verify has already refused that R.
  • The extended formulas are complete on the curve: a = −1 is a square and d is not. Every operand is on the curve, including a mixed-order A.
• The static table.
  • points[i] = (2i+1)B by repeated complete addition of 2B.
  • Montgomery's simultaneous inversion is correct. prefix[i] = z₀…zᵢ. Walking down, z_inverse = inverse·prefix[i−1], then inverse ← inverse·zᵢ, and i = 0 takes the remaining inverse.
  • Each Niels entry is (y+x, y−x, 2dxy) of the affine point.
  • base_table_holds_the_odd_multiples_of_b checks all 32 entries against run-time repeated addition through a different doubling and addition path. The ring, dalek, RFC 8032 and Wycheproof differentials close the remaining common-mode risk.
• Comparing R's encoding. This is equivalent to the old strict decode-then-compare.
  • Strict decoding is a bijection between canonical encodings and curve points, and encode always yields the canonical one: y < p, and the sign bit is x's parity, so it is 0 when x = 0.
  • So encode(P) == R holds exactly when R is canonical and decodes to P.
  • A noncanonical y, a negative zero, or an off-curve R can never match.
  • The only change is the refusal's variant, InvalidPoint becoming InvalidSignature. Nothing outside the crate matches on it: I searched the tree, including lib/update (which still uses dalek), build/ssh, crypto_parity and ring_kat.
• Small order.
  • The eight encodings are the y = 1, y = −1 and y = 0 points (x = ±√−1, both signs) and the four order-8 points (26e8…05/85 and c717…7a/fa).
  • The test establishes the set independently. The eight encodings are distinct, each decodes (so is canonical), and each satisfies [8]P = O. The cofactor is 8 and E(F_p) ≅ ℤ/8 × ℤ/L, so these are all the torsion points.
  • For A: the key is decoded first, so its encoding is canonical and list membership is exactly "small order".
  • For R: any accepted R is canonical (previous point), so a noncanonical small-order R is refused by the compare.
  • The policy is the old one. Small-order R and A are refused; mixed-order points are not, as before.
• Decode.
  • RFC 8032 §5.1.3 steps 1–4, in order:
    • canonical y by re-encoding;
    • u = y² − 1 and v = dy² + 1;
    • x = uv³(uv⁷)^((p−5)/8);
    • the checks vx² = u, vx² = −u (then ×√−1), otherwise refuse;
    • x = 0 with the sign bit set refused;
    • the sign chosen.
  • v ≠ 0 always holds, because −1/d is a nonsquare.
  • It takes one pow_p58 and no inversion.
• Barrett.
  • With q₁ = ⌊x/2^192⌋ < 2^320, x/L − q₁μ/2^320 = (q₁/2^320)(2^512/L − μ) + (x mod 2^192)/L. This is below ε + 2^−60.
  • So ⌊x/L⌋ − q₃ ≤ 1 whenever ε + 2^−60 < 1, and q₃ ≤ x/L because μ ≤ 2^512/L. Hence 0 ≤ r < 2L, and one masked subtraction suffices.
  • The test asserts μ = ⌊2^512/L⌋ and 4(2^512 − μL) < L, that is, ε < 1/4, which is more than needed.
  • subtract_l's sign test is valid. r < 2^254, so r − L mod 2^320 has bit 319 set exactly when r < L.
  • mul_add: t = ab < 2^506, and adding c < L stays below 2^512. s = k·a + r matches RFC 8032.
  • reduce32 places the clamped scalar in the low half. [a mod L]B = [a]B because B has order L.
  • PublicScalar::canonical's borrow chain is correct.
• wNAF.
  • Algorithm 3.35 as written. Digits are odd with |d| ≤ 2^(w−1) − 1, which fits i8 for w ≤ 8.
  • The length is at most 254 for k < L, so [i8; 256] never overflows.
  • The test recomposes 201 scalars at every width and checks oddness, magnitude and spacing.
• Equivalent mutant. Confirmed. The window is taken only when k is odd, so it is odd and cannot equal the even 2^(w−1).

PublicScalar and the secret path

• The type has no conversion from S. Its only constructors are reduce (verify's k) and canonical (verify's S).
• Its only uses outside its module are PublicKey::verify and one test.
• The variable-time functions are naf, verification_point and Point::decode, and each is reached only from verify or PublicKey::from_bytes.
• Sign and from_seed reach Point::mul, Projective::double/encode, invert, barrett, subtract_l and mul_add. All are fixed schedule, and subtract_l selects through ct::mask.
• The type keeps S out. It does not stop a future caller passing secret bytes to PublicScalar::reduce, but that call would say "public" at the site. That is what spec §4.5 asks for.

Findings

BLOCKER

1. lib/crypto/src/secret.rs:16–18 (unchanged here, now stale) — the contract says S erases per value "for now… until its reduction is rewritten".
   • This PR is that rewrite, and S still erases on drop. barrett, reduce, reduce32, mul_add and subtract_l also wipe their temporaries.
   • Fix: state the settled behaviour (S and its reduction temporaries are erased) and drop "for now" and "until". Or, if per-value erasure of S is meant to go, do that and move S to "Not erased".
   • crypto: a 5x51 field with typed bounds and erasure at the boundary (parity items 1 and 5) #992's Risks line about S needs the same update (orchestrator).
2. lib/crypto/src/test_arithmetic.rs:108–111 — the new comment is false here, and the edge values are not what it says.
   • "Barrett's quotient estimate is short by up to two" contradicts barrett's own comment and the bound this PR proves. For x < 2^512 it is short by at most one. HAC's general bound is two.
   • For k ≥ 2, ⌊2^512/L⌋·k·L − 1 exceeds 2^512 and is then reduced mod 2^512. Those values are not "just below a multiple of L".
   • The test still holds the reduction against num-bigint, and the control shows it reds when the subtraction is removed.
   • Fix: state the true purpose in one line (inputs where the one subtraction is and is not taken). Either keep only k = 1 or generate k·L − 1 below 2^512.
3. lib/crypto/src/field25519.rs:136 — "self * b, for constants" is false.
   • invert, pow_p58 and pow_2_250_1 run at run time on every verify and sign through times and squared.
   • Fix: say what distinguishes times from Multiply::mul: it is the const form, Tight by Tight. Or delete the comment.

SUGGESTION

4. scalar25519.rs:95 — HAC 14.42 needs only q₃·L mod b^(k+1). Five columns of the 5×4 product would do instead of all nine words. The gain is small; leave it if you prefer.
5. scalar25519.rs:165 — PublicScalar::reduce goes through barrett, which wipes q₂, q₃L and r for a public value. The cost is negligible, and sharing one reduction is reasonable. Mentioned only so that it is a decision.
6. Evidence: qemu-crypto-instrument.log does not record its revision, unlike ci-host.log. One header line would make it self-identifying.

Tests and evidence

• --ci host at 1d0f66a: the log header gives the revision, and it exits 0 with 87 green. QEMU crypto_instrument_prints_its_table exits 0 (78 rows; timings not judged there, correctly).
• The 12 controls are real patches, built and run. Each red names the claimed test.
• Three controls were green in the first block: the small-order R check, the canonical-y check and the negative-zero check. Each exposed a missing test. The new tests turned them red in the second block. That is the intended use of negative controls.
  • a_small_order_r_satisfying_the_equation_is_refused is the one that matters. It builds an R = O signature that satisfies the cofactorless equation, confirms that it does, and shows the refusal comes from the small-order check. Without the check, the encoding compare would accept it.
• "Barrett's second subtraction removed" was green, so the step was proved unreachable and deleted, and the remaining subtraction's control is red. That is correct handling.
• The first-block controls ran on 41e89b9ec + pr3-tree.patch. The second block ran after the gap tests. Between them the tree gained tests and lost the unreachable subtraction, and neither change can turn a first-block red green.
• The new tests are hermetic and seeded, each with one claim.
• Missing: no control perturbs the table builder (for example, an off-by-one in the simultaneous-inversion index). base_table_holds_the_odd_multiples_of_b and the differentials would catch it, so this is not required.

Verdict: SEND BACK (items 1–3, each a comment or one-line change; no arithmetic or design change is needed).

[Japabu]

Review of #997, round 2 (head cd7960d)

I read the round-1 commit cd7960d. A range-diff confirms that cd2d860 is 1d0f66a rebased unchanged onto d633558. I also read scalar25519.rs, the changed test, the new contract line and the PR's replies, and checked the evidence at f3a54df (pr-997/r2: ci-host.log, the Barrett control rerun and controls-results.txt). I ran nothing.

Round-1 items

1. S's erasure in the contract: reworded, but the new wording overstates. See item R1.
2. Test comment and edge values: fixed.
   • The comment now reads "multiples of L and their predecessors, small and near 2^512: where the one subtraction is taken and where it is not". It is true.
   • The values (μ − j)·L and (μ − j)·L − 1 for j = 0..3 lie below 2^512, since μL ≤ 2^512, so the reduction mod 2^512 no longer changes them.
   • The Barrett control was rerun on them and is red.
3. times doc: fixed. It now reads "The const form of [Multiply::mul], tight by tight".

Suggestions

• 4 and 5 declined. Both reasons are fine and the matter is settled.
• 6 taken. QEMU logs now record their revision.

Finding

BLOCKER

R1. lib/crypto/src/secret.rs:19–21 — "their reduction erases its workspaces" claims more than barrett does.

• barrett (scalar25519.rs:88–104) wipes q₂, q₃L and r, and subtract_l wipes d. The callers wipe their input x or t.
• But q1 = [x[3..8]], the top five words of the secret input, is a named local and is never wiped. The same goes for q3, the secret-dependent quotient.
• These are explicit locals, not compiler copies, so the contract's "Not erased" list does not cover them. A reader of "erases its workspaces" would take them as erased.
• Fix: either wipe64(&mut q1); wipe64(&mut q3) (two more wipes of five words; q1 and q3 need mut), or name what is erased ("its products and remainder"). The first keeps the sentence true and is cheaper to reason about.

Evidence

• --ci host at cd7960d exits 0 with 87 steps green.
• Round 1 changed only comments, test inputs and one contract line, so the earlier controls still stand. The one control those test inputs affect, Barrett, was rerun and is red.
• The T14 figures (verify 1.041×, sign 6.66×) are now in the body.

Verdict: SEND BACK (R1 only, a two-line change or one reworded clause).

[Japabu]

Review of #997, round 3 (head b824d27, base main)

I read the round-2 commit and checked the rebase. I ran nothing.

Rebase

• The base matches the old one. crypto: a 5x51 field with typed bounds and erasure at the boundary (parity items 1 and 5) #992 merged as squash 27ab916. git diff d63355844 27ab916b7 -- lib/crypto is empty, so the crate under this PR is byte-identical to the base I reviewed.
• The rebased commits are unchanged. git range-diff shows a488389 = cd2d860 and b47ac40 = cd7960d, both marked = (no content change).

R1

Fixed. barrett now declares q1 and q3 mut and wipes both, alongside q₂, q₃L and r. Every named array in the reduction is now erased, so secret.rs's "their reduction erases its workspaces" is true. The two extra wipes do not touch the arithmetic.

Evidence

• Clippy and the crate tests in the three forms exit 0 at b824d27.
• --ci host exits 0 on the rebased stack head 2594dd3, which contains this commit unchanged.
• Adding wipes cannot turn any control's red green, so no control needs a rerun.

Verdict: LAND.