[Japabu]

Builds on #990 (merged). Its commits: round 0, 4c3c94a (rebased unchanged from 55005b1); round 1, 41e89b9; round 2, d633558.

Problem

The 2^255 - 19 field behind X25519 and Ed25519 cost about 91–100 ns per multiplication on the T14 against ring's 13–17 ns (spec section 1.2, derived from #932). It multiplied each of its 25 products by a runtime 1 or 19 as u128, squared by multiplying, carried in three full passes, inverted with a square and a multiply per exponent bit, and erased every element and workspace with volatile stores and a fence, which kept the arithmetic in memory.

What changes

• A 5x51 field with typed bounds (parity items 1 and 5: X1, X2, X4). Tight is what a multiplication or carry leaves (limbs 0, 2, 3, 4 below 2^51, limb 1 below 2^51 + 2^19); Loose is the sum or difference of two tight elements (every limb below 2^53). Multiplication takes either, addition and subtraction take only Tight, so a missing carry does not compile. Multiplication premultiplies b's four wrapping limbs by 19, squaring takes 15 products, mul_small is one row, the carry is one pass with the top carry folded by 19 plus one short carry. Every product and carry uses wrapping operations whose bounds the types establish, so the shipped profile's overflow checks add nothing. Inversion and the square root's power use the curve25519 addition chain: 254 squarings and 11 multiplications.
• X25519's ladder swaps by one XOR mask per coordinate pair (2 swaps per step instead of 6 selects) and multiplies by 121665 with mul_small.
• Ed25519 runs on the typed field and doubles with RFC 8032's dedicated doubling (section 5.1.4) in its fixed-schedule multiplication and in the small-order check. Its algorithms are otherwise unchanged; the comb, joint verify and scalar reduction are later PRs.
• Erasure at the boundary, per the owner's conditional approval of item 26. Field elements, NIST residues and both curves' points are Copy intermediates. Secret owners still erase on drop. Each key agreement erases its shared value before it becomes bytes: X25519's x2 / z2, and P-256/P-384's product point and affine coordinates (one erase per agreement, restored as the orchestrator decided under the owner's rule that key cleanup is kept). The X25519 ladder's (x2, z2, x3, z3) is a secret::Workspace.

The erasure contract

The contract lives in lib/crypto/src/secret.rs's header, and lib.rs points to it:

• Erased: owners. A Secret, and every type that owns a key, seed, expanded key, key schedule, scalar or shared secret, erases its own storage when it drops. So do the hash, HMAC, Keccak, SHA-1 and Poly1305 states. This is unchanged.
• Erased: key-agreement values. Each key agreement writes its output bytes into a Secret it owns, then erases the values they came from: X25519's x2 / z2, and P-256/P-384's product point and affine coordinates, each held in a Workspace. The output Secret is moved into the returned SharedSecret, an owner. Not erased: the copies of the output bytes that this move leaves in the agreement's finished frame, and the computation's arithmetic intermediates.
• Erased: workspaces. A secret operation's explicitly managed state is a Workspace, dropped when the operation returns, on every path out of it, early returns and ? included. The X25519 ladder's (x2, z2, x3, z3) is one. A workspace erases its own storage; the copies the computation works on, in registers and other slots, are not erased.
• Erased per value, for now. Ed25519 scalars (scalar25519::S, until its reduction is rewritten) and ML-KEM polynomials (mlkem::Poly) still erase every temporary on drop.
• How. Volatile stores of zero over the value's own storage, then a sequentially consistent compiler fence. They erase that location and no other.
• Not erased. Other arithmetic intermediates: 2^255 - 19 field elements, NIST residues and both curves' points are Copy values. Also not erased: registers; spill slots and every other copy the compiler makes, by-value moves and returns included; a moved value's earlier location; finished stack frames; the caller's buffers and public outputs. These remain until something overwrites them. The contract does not claim that any stack frame is wiped.
• Panics. An unwinding panic drops, and so erases, every owner and workspace on the unwound frames. Under panic = "abort", nothing runs after the panic.

Zeroable, which erase relies on to write zero bytes over a value, is now an unsafe trait. Each impl states why zero is a valid value.

What the generated code shows. This inspection replaces round 0's claim, which was wrong.

• Round 0 said the ladder state was written to its own slot on every step. The x86-64 listing shows the opposite: the loop works on registers and other stack slots, and the workspace slot is written only before the loop and by the final swap. The contract therefore claims only what holds regardless of code generation.
• At 41e89b9, in [profile.toyos] with the ToyOS toolchain (rustc 1.99.0-dev), I emitted the crate for x86_64-unknown-toyos and aarch64-unknown-toyos. A script walked each secret path's call graph and listed every conditional branch. The paths are P-256 and P-384 agree and public_key, Ed25519 sign and from_seed, and X25519 agree and public_key.
• Every branch reached is one of four kinds: a loop counter or the hash's round index; a check on a public length; a bit of the public inversion exponent; or a result check whose outcome cannot vary for validated inputs (affine's infinity check, and X25519's disclosed all-zero refusal). No branch in the point operations, the residue arithmetic or the 2^255 - 19 field operations depends on anything but a loop counter. Masks come from the register barrier.
• Erasure in the shipped agreements, at round 2 (d633558's code), [profile.toyos], both targets. NIST's affine now writes into the caller's coordinate Workspace, and X25519's multiply into the caller's Secret, so the returned-coordinate copies round 1 left are gone. On the success path, what remains is the copies of the output bytes that the move into SharedSecret leaves:
  • P-256, x86-64: the output Secret local at −160..−129(%rbp), copied into the return slot. The product (−256..−161), the coordinates (−128..−65), the to_be staging word (−48) and the consumed scalar are zeroed, each group followed by the fence.
  • P-256, aarch64: the output local at [sp, sp+32). The product, coordinates, staging slot and scalar are zeroed. On the unwind path the output local is erased too, because the Secret drops.
  • X25519, x86-64: the 32-byte result at −48..−17(%rbp) is moved into the return slot. Erasing the consumed key uses −48..−33 as its staging slot, so the upper 16 bytes, −32..−17, remain.
  • X25519, aarch64: the same at [sp+16, sp+32).
  • Round 1's listing was of the earlier code. There, P-256 also left affine's returned x[1..3] and y in agree's frame. That is now removed.
• The inspection covers the shipped profile on these two targets. The UEFI loader target and the fixed-versus-random harness remain stage 4's.

Checks

Round 2, at d633558. Host CI ran on #997's head cd7960d, which contains this commit unchanged (result in #997). cargo clippy and cargo test -p toyos-crypto --release in the three CI forms: exit 0 each. The shipped agreements' code extracts: https://github.com/ToyOSOrg/evidence/tree/f3a54df6253a32c4ff3e3236ebe81b7a01664e1e/pr-997/r2/agree-code

Round 1, at 41e89b9. Logs: https://github.com/ToyOSOrg/evidence/tree/7c1d744ca3ee34eeda72bc1d301ba3451783227b/pr-992/r2

• 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.
• Generated-code inspection of every secret scalar-multiplication path on x86_64-unknown-toyos and aarch64-unknown-toyos in [profile.toyos]: see "What the generated code shows" above, and inspection/ in the logs. Correction (review round 2): the subq; cmovb; testq; je branches in Tight::bytes and to_be are copy_nonoverlapping's debug overlap check on two stack addresses, which is on in [profile.toyos], not length checks. The addresses are public, so the conclusion stands.
• Rosetta reproduction (requested in review): rosetta-adx-sigill.log. CPUID through Rosetta reports BMI2 and ADX. mulx runs, while adcx and adox exit 132 (SIGILL). No code here dispatches on ADX.
• Round 0's controls (below) were not rerun. Round 1 changed none of the patched lines. It adds erasure, removes two accumulator workspaces, and changes doc comments, Zeroable's safety and one debug assertion; none of that can change which test a field or ladder mutation reds.

Round 0, at 55005b1 unless stated. Logs: https://github.com/ToyOSOrg/evidence/tree/e52b6c4658ed56e2719da2f8defd24d396d370d6/pr-992/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.
• cargo test --test toyos-build -- crypto_instrument_prints_its_table (QEMU, x86_64) on the probe head fb93764, which carries this PR's crate unchanged: exit 0, 88 rows in each build.
• New tests: field25519_carries_and_noncanonical_inputs_match_integer_oracle (rewritten for the typed field: squaring, mul_small, negation, inversion, the (p-5)/8 power, loose operands into every multiplication) and field25519_limb_bounds_hold_at_their_extremes (the largest limbs each type admits through every operation, and the tight bound of a product).
• 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
carry folds by 18 instead of 19	red: field oracles, constants, X25519 and Ed25519 vectors, Wycheproof
2p's low limb one short	red: as above
one square product with 2a1 replaced by a1	red: as above
canonical encoding's q computed from h + 18	red: field oracles, RFC 7748/8032, Wycheproof
one addition-chain step a squaring short	red: field oracles, constants, vectors
the short carry into limb 1 dropped	red: as above
Ed25519 doubling's G = A - B made B - A	red: Ed25519 differential, RFC 8032, Wycheproof
ladder swap by the bit instead of bit XOR previous bit	red: X25519 differential, RFC 7748, Wycheproof
final ladder swap removed	green: an equivalent mutant. SecretKey::from_bytes clamps bit 0 to zero, so that swap's mask is always zero. It stays as RFC 7748's ladder states it.

Measurements

• M1 on the T14 (probe fb93764 = round 0 of this PR plus additive rows; judge exit 0). Boundary over per-temporary erasure, same arithmetic:

  row	ratio	spread
  x25519/ecdh	0.796	0.0013
  ed25519/verify/64	0.801	0.0026
  ed25519/sign/64	0.812	0.0059
  p-256/ecdh	0.936	0.0054

• M1 on the AMD bench (the same probe, judge exit 0): x25519/ecdh 0.795, ed25519/verify 0.794, ed25519/sign 0.808, p-256/ecdh 0.882.

• Rounds 1 and 2 add one erase per agreement and remove two accumulator workspaces; I expect no visible change against rows of 83 to 517 us, but that is an inference, not a measurement.

• This PR's parity rows on the T14 (same boot): x25519/ecdh 83.2 us against ring's 42.2 (1.97x; The ring comparator: toyos-crypto beside ring in a guest, on metal rows (crypto stage 2) #932 measured 13.3x). ed25519/sign 95.0 us against 12.9 (7.34x; was 71.1x). ed25519/verify 179.7 us against 53.1 (3.38x; was 34.5x). The NIST and RSA rows beneath it come from crypto: RSA R^2 by squarings, NIST curves as compile-time types, Ed25519 constants, a register barrier (parity items 1-4) #990: p-256/ecdh 8.56x (was 21.2x), ecdsa-p-256 verify 9.33x, p-384/ecdh 2.49x, rsa-2048-pkcs1 2.15x (was 38.1x). None passes yet.

• Exploratory runs on the development Mac are superseded by the T14 numbers.

Risks

• Every-return-path erasure rests on Workspace and the owners being drop guards. Under panic = "abort" nothing is erased after a panic.
• Ed25519's secret scalars (scalar25519::S) are owners and keep erasing on drop; crypto: Ed25519 verify by one joint multiplication, scalars by Barrett (parity items 6, E3, E4) #997 rewrites their reduction and settles that wording.

🤖 Generated with Claude Code

[Japabu]

Review of #992, round 1 (head 55005b1, top commit only)

I read the commit, the full diff against f5fbc03, each changed file at the head, every caller of multiply, Point::mul, agree and Workspace, the owner types elsewhere in the crate (scalar25519, mlkem, hash, aes), the evidence README, the x86-64 listing, the controls, the wiped probe crate's diff and readback-probe/rows-t14.txt. I did not read the analysis notes or any ring or BoringSSL source. I ran nothing.

Architecture

• Field types. Tight/Loose with Multiply over either bound is the right shape. A missing carry does not compile, and the bounds replace overflow checks rather than suppressing them. The field is self-contained and stays portable for the soft-float loader.
• Erasure model. Owners erase themselves, and named workspaces erase at operation end. This is the model the owner conditionally approved (item 26).
• M1. Measured on the T14 at probe fb93764, boundary over per-temporary: x25519/ecdh 0.796, ed25519/verify 0.801, ed25519/sign 0.812, p-256/ecdh 0.936. Spreads are ≤ 0.6% (rows-t14.txt:79–82; judge exit 0, 1 passed). The control crate lib/crypto-wiped differs from this PR only in Drop wipes on Tight/Loose and on the multiply and canonicalise workspaces. It is a fair A/B. The owner's measured-benefit condition is met on the T14.
• Size. Net +499/−232 lines. Most of it is the explicit 5×51 kernels and the two bound tests.

Arithmetic, checked by hand

• Bounds. Tight inputs give add < 2^52 + 2^20. TWO_P[0] = 2^52 − 38 and TWO_P[i] = 2^52 − 2 both exceed every tight limb, so sub never borrows and stays below 2^53. In mul, the products are below 2^53 · 19 · 2^53 < 2^110.3, so five-term columns stay below 2^113 < 2^115. In square, three-term columns stay below 2^113.
• Carry. After the pass, v4 >> 51 < 2^64.1, and ×19 fits u128. r0 >> 51 < 2^17.3, so limb 1 < 2^51 + 2^19, as Tight states.
• mul_small. k < 2^17 on a Loose operand gives < 2^70. Correct.
• Formulas. I checked the square's 15 products and the mul's 25 columns term by term.
• from_bytes/bytes. The shifts are 13, 38/26, 25/39 and 12. q is the exact carry of h + 19, and h < 2p, so q ∈ {0, 1} and the masked h4 drops bit 255. Correct.
• Inversion chain. 254 S + 11 M yields 2^255 − 21. pow_p58 yields 2^252 − 3, so q·q^((p−5)/8) = q^((p+3)/8), the same exponent as the old bytes.
• Ladder. The swap mask is ct::mask(swap ^ bit), which goes through the barrier. The step is RFC 7748's (a24 = 121665 with AA).
• Ed25519 doubling. It is RFC 8032 §5.1.4 term by term. The identity doubles to (0 : −1 : −1 : 0), which is the identity.
• Equivalent mutant. Confirmed. multiply is private. Its two callers pass SecretKey's bytes, and from_bytes clears bit 0 (&= 248), so the final swap's mask is always zero.

Erasure contract against the code

Every error and early-return path drops its owners. I checked x25519::agree's zero refusal, ecc from_bytes/generate/first_valid, and Ed25519 sign's ?s. Secret, Scalar, S and the hashers all erase on drop. The bullets on registers, spills, moves and panics are accurate. The following do not hold.

BLOCKER

1. The PR body's generated-code claim is false. The body says multiply "keeps its ladder state in its own stack slot and writes it on every step".

   • The listing you cite shows the opposite. The Workspace slot is [rbp−736, rbp−576). It is written by rep movsq before the loop (.s:71–74) and by the final swap after it (.s:1989–2069). The loop body LBB111_3 (.s:107–1976) never stores to it.
   • During the loop the state lives in registers and other slots ([rbp−112], [rbp−72], [rbp−48], [rbp−56], [rbp−64], [rbp−80], [rbp−192], …).
   • The final swap writes x2's limbs to both places (.s:1991, 2001, 2008, 2017), and only the workspace copy is erased (.s:2340–2386).
   • So the erasure removes the copy LLVM materialises for the workspace at loop exit. The ladder's working copies remain in the dead frame. Later code partly overwrites them with the final multiplication's own unerased temporaries.
   • This is consistent with the contract's "spill slots… not erased", but the body tells the owner the opposite of what the code does, and the owner is judging exactly that. Correct the body to describe the actual listing (orchestrator).

2. The accumulator workspaces erase only the value the function returns.

   • In nist.rs:155–163 and ed25519.rs:148–156, each step overwrites r.0 in place. After the loop the slot holds exactly the result, which r.0 then copies out to the caller.
   • For keygen, sign and verify that result is public. For ECDH agree it is the secret product, and agree keeps it unerased (item 3).
   • These two Workspaces therefore remove nothing that is not still held elsewhere. Their doc comments and the contract's example ("a scalar multiplication's accumulator") suggest protection that does not exist.
   • Delete them and correct secret.rs:6–9 and the PR body's list. If the secret product must be erased, erase it where it is owned (item 3).

3. ECDH's shared secret, in integer form, is no longer erased.

   • nist.rs:214–222 dropped main's wipe64(&mut x); wipe64(&mut y). x is the shared secret before it becomes bytes, and the product point it came from is also left behind.
   • These are not per-intermediate field wipes. They are explicit cleanup of a key-equivalent value, and the owner's ruling preserves key cleanup.
   • Either restore it, or say so in the contract and get the owner's agreement:
     • Restoring means holding self.mul(scalar) in a Workspace inside agree and wiping x and y. That is one erase per agreement, which is invisible against M1's 516 µs row.
     • Otherwise the contract must state that a secret scalar multiplication's result and its affine and limb forms are not erased. That covers NIST's product, x and y, and X25519's x2·z2⁻¹ at x25519.rs:75. Whether that relaxation is acceptable is the owner's decision, not ours.
   • encode's removed wipes were of public coordinates and are fine.

4. The contract misstates which intermediates are erased (secret.rs:13–17).

   • It says arithmetic intermediates are not erased and names only field elements and residues.
   • But scalar25519::S (scalar25519.rs:11) and ML-KEM's Poly (mlkem.rs:17) still erase every temporary on drop, and so do Poly1305 and the hash states as owners.
   • A contract the owner must review should list the types that still erase per value. Note S as pending the Barrett PR.

5. Zeroable must be an unsafe trait (secret.rs:50).

   • erase<T: Zeroable> (:59) is safe. Its unsafe block justifies writing zero bytes over any T with "zero bytes are a valid T".
   • Before this PR it was only reached through arrays of primitives. Now it covers arbitrary structs (Tight, Residue, both Points).
   • A safe impl Zeroable for a type with a reference, NonZero or an enum would make safe code undefined behaviour. The invariant belongs to the implementer, so the trait must say unsafe trait, and each impl should carry a one-line safety note.

6. The constant-time evidence is overclaimed.

   • The body says "the generated code is the evidence for both here". In fact one function, x25519::multiply, was inspected, on x86_64-apple-darwin under --release (overflow checks off), not [profile.toyos].
   • The other secret paths this PR changes were not inspected: nist::Point::mul (now Copy residues in registers) and Ed25519's fixed-schedule mul with the new doubling (sign, keygen). Neither was aarch64.
   • Either narrow the sentence to what was inspected, or extend the check. The cheapest extension is --emit asm of nist::Point::<P256,4>::mul and ed25519::Point::mul for x86_64-unknown-toyos in the shipped profile, grepping for conditional branches on non-counter registers. It needs no machine.
   • The stage-4 inspection on all three shipped targets remains the track's exit.

7. The crypto track's weakness record is stale.

   • issues/toyos-crypto-is-in-the-tree-on-par-with-ring-and-secure.md:426–428 says "Owned secret storage is wiped on drop…".
   • This PR deliberately stops erasing field elements, residues and points. Under "no silent debt" the record should point to secret.rs's contract and state the weakening and its owner condition, in the same change.

SUGGESTION

8. field25519.rs:132: square_times(0) squares once, which contradicts its doc. Every caller passes k ≥ 2. Document k ≥ 1 or assert it in debug builds.
9. test_arithmetic.rs:78: the test is named for "the largest limbs each bound admits", but it exercises the largest reachable limbs. That is the useful claim, so rename it rather than widen it.

Tests and evidence

• The CI host log is at 55005b1 and exits 0 with 87 green.
• Nine controls turn their tests red. They hit the fold constant, 2p, a square product, canonicalisation at h = p, the chain length, the short carry, the doubling and the step swap. The tenth is the explained equivalent mutant.
• The two new oracle tests are hermetic and focused, and loose operands reach every multiplication.
• The Mac M1 figures are correctly labelled exploratory. The T14 numbers above supersede them.

Rosetta and ADX

• No code in crypto: RSA R^2 by squarings, NIST curves as compile-time types, Ed25519 constants, a register barrier (parity items 1-4) #990 or crypto: a 5x51 field with typed bounds and erasure at the boundary (parity items 1 and 5) #992 dispatches on CPUID ADX, and LLVM emitted no adcx/adox.
• The only check is is_x86_feature_detected!("bmi2") && …("adx") in the unlanded probe's guest binary (crypto_parity.rs:973), which runs on ToyOS, not under Rosetta.
• The SIGILL observation has no saved log in the evidence. Record it with a minimal reproduction before any X5/N6/R5 ADX kernel lands, because host tests of such a kernel on x86_64-apple-darwin would then need a reason not to trust Rosetta's CPUID. The fix belongs in that test environment. Capable metal should not be degraded because of it.

Verdict: SEND BACK. Items 1–7 are required. Item 3 may instead go to the owner as an explicit contract relaxation. Once they are resolved, the erasure contract is in a reviewable state for the owner's landing condition.

[Japabu]

Review of #992, round 2 (head 41e89b9)

I read the round-1 commit 41e89b9 against 4c3c94a, every changed file at the head, secret.rs and ecc.rs in full, the updated body, the track record's hunk and the inspection evidence (inspection/README.md, the per-path branch listings and the two .s extracts). I also spot-checked the emitted [profile.toyos] assembly for both targets.

I did not rebuild: this role runs no builds. The spot-check used the implementer's own --emit asm output in the scratch target-asm/. Its mangled crate hashes match the inspection files (Cs4U4sOGKWW3b on x86-64, Cs8xBsXJZo7Hy on aarch64), and it was written at the commit's time. The orchestrator may delete that 108 MB directory once this review is settled.

I did not read the analysis notes or any ring or BoringSSL source.

Round-1 items

1. Body's generated-code claim: fixed. The body now states that the ladder works in registers and other slots, and that only the workspace slot is erased.
2. Accumulator workspaces: fixed. Both are deleted, with their comments. Ed25519's impl Zeroable for Point is removed with them.
3. ECDH shared value: restored as the orchestrator decided.
   • nist::Point::agree holds the product in a Workspace and wipes x and y.
   • x25519::multiply holds x2·z2⁻¹ in a Workspace.
   • In the shipped code on both targets, the named locations are zeroed, each group followed by the fence. I checked p256::SecretKey::agree on x86-64 and aarch64.
   • What remains is in item A below.
4. Per-value types listed: fixed. The contract names S and Poly, and the hash, HMAC, Keccak, SHA-1 and Poly1305 states.
5. Zeroable: fixed, and sound.
   • It is pub(crate) unsafe trait Zeroable: Copy, with a # Safety section.
   • The impls are integers, arrays of zeroable elements, Tight([u64; 5]), Residue([u64; N], PhantomData<M>) and NIST Point { x, y, z: Residue }. Every one is valid at all-zero bytes.
   • Copy excludes Drop types, erase writes only inside the exclusively borrowed value, and padding may be written.
   • Nit, not required: "Every bit pattern of zero bytes" reads better as "The all-zero bit pattern".
6. Constant-time evidence: fixed.
   • Scope: the shipped profile on x86_64-unknown-toyos and aarch64-unknown-toyos, from every secret entry point: P-256 and P-384 agree/public_key, Ed25519 sign/from_seed, X25519 agree/public_key.
   • Spot-checks:
     • The X25519 ladder's branches are cmpq $32 (decode) and addq $-1, %r12; jb (the 255-step counter).
     • aarch64's ladder b.ne takes its flags from cmn x7, #1 on the loop index.
     • The masks are the empty InlineAsm followed by neg.
   • The conclusion holds: no branch in the point, residue or field operations depends on anything but a counter.
   • One classification is wrong, without changing the conclusion (suggestion C).
7. Track record: fixed. It points to the contract and states the weakening, the owner's condition and the T14 M1 range.
8. square_times and test name: taken. Both suggestions.

M1

M1 now holds on both benches. The coordinator relayed the AMD boot of probe fb93764 (judge exit 0): x25519 0.795, Ed25519 verify 0.794, sign 0.808, P-256 ECDH 0.882 (readback-probe-amd/rows-amd.txt). The T14 gave 0.796–0.936. The owner's measured-benefit condition is met on the T14 and on the AMD machine.

Findings

BLOCKER

A. lib/crypto/src/secret.rs:7–10 — the key-agreement bullet overstates what the shipped code erases. The owner is judging exactly this bullet.

• The word "before" is false. It says each agreement erases its shared value "before it becomes the returned bytes". Both implementations erase after the bytes exist:
  • X25519 drops the shared workspace after Secret(shared.0.bytes()).
  • NIST wipes x after to_be(&x, output).
• Same-frame copies survive on both shipped targets. After agree returns, its dead frame still holds the shared secret through by-value returns and moves:
  • P-256 x86-64 (x86-4p256…agree.s):
    • affine's returned Result<(x, y)> sits at −176..−112(%rbp). The workspace erase uses −176..−161 as its 16-byte staging slot, so the tag and x[0] are zeroed.
    • x[1..3] (−160, −152, −144) and all of y (−136..−112) remain.
    • The output Secret<32> at −96..−65, the whole shared secret as bytes, is moved into SharedSecret and not erased. The body states this one copy.
  • P-256 aarch64: the same layout at x29−88. stp xzr, xzr, [x29, #-88] zeroes the tag and x[0]. x[1..3] (−72..−56) and y (−48..−24) remain, and so does the output local at [sp, sp+32).
  • X25519 x86-64: SecretKey::agree holds multiply's 32-byte result at −48..−17. On the success path only −48..−33 is zeroed, as the staging slot for erasing the consumed key. The upper 16 bytes of the shared secret remain at −32..−17.
• Why it matters. The general "Not erased: by-value moves and returns, a moved value's earlier location" clause makes the contract's lists logically complete. But the key-agreement bullet, read on its own, tells the owner the shared value is gone once the bytes belong to SharedSecret. In the shipped code the full shared secret remains in the dead agree frame on both targets. This is not a regression: main had the same pattern. But the contract is new here and must not promise more.
• Fix (one of):
  • (a) State it in the bullet, in one sentence: the named values (X25519's x2/z2, NIST's product point and affine coordinates) are erased once the bytes are written, and copies left by returns and moves on the way out are not erased, including the output bytes before they move into SharedSecret.
  • (b) Remove the copies that code can remove, then state the rest. For example, affine could write into the caller's &mut [u64; N] arrays. The move into SharedSecret and Result cannot be prevented in Rust's value model, so (a) is needed either way.
• PR body (orchestrator). It should list these copies next to the output-Secret one, for both targets and for X25519.

B. lib/crypto/src/secret.rs:13–15 — "Its slot is what LLVM writes at the ladder's end" is a codegen observation stated as contract.

• It was established on x86_64-apple-darwin --release in round 0. The shipped-target inspection does not re-establish it for the ladder slot.
• It can change with any compiler or profile.
• Fix: keep the codegen-independent part ("the workspace erases its own slot; copies the loop works on in registers and other slots are not erased"). Leave the observation to evidence.

SUGGESTION

C. inspection/README.md (evidence) — one branch classification is wrong.

• The README classes the subq; cmovb; testq; je → panic_nounwind_fmt branches as slice bounds in Tight::bytes and as output-length checks in to_be.
• They are copy_nonoverlapping's debug overlap check, which is on in [profile.toyos]. It compares the absolute difference of two stack addresses (−8(%rbp) against −48/−40(%rbp) in bytes).
• Its operands are addresses, which are public, so the conclusion stands. A future reader should not be told they are length checks.

D. issues/toyos-crypto-is-in-the-tree-on-par-with-ring-and-secure.md:426–432 — the AMD M1 range (0.79–0.88) could join the T14's, now that it exists.

Statement for the owner's condition

• Accurate as written? No, because of A.
• What is accurate. The contract's lists of what is erased and what is not are complete:
  • Erased: owners, hash and MAC states, the named key-agreement values, the workspaces, and per-value S and Poly.
  • Not erased: every other field element, residue and point; registers, spills, by-value moves and returns, earlier locations of moved values, finished frames, and caller buffers.
  • These lists match the code and the shipped assembly I checked.
• What must change. The key-agreement bullet claims more than the shipped code delivers ("before", and silence about same-frame copies of the shared secret), and one sentence is a codegen observation (B).
• After A and B. I would consider the contract accurate and complete enough for the owner's "precise, reviewed contract" condition. M1 holds on both benches.
• Remaining P-256 by-value-move gap. The body states it honestly but incompletely. It names the output Secret and omits affine's returned coordinates and X25519's result (A).

Verdict: SEND BACK (A, B; each a short wording change).

[Japabu]

Review of #992, round 3 (head d633558, base main)

I read the round-2 commit d633558 against 41e89b9, secret.rs, nist.rs and x25519.rs at the head, and the updated body. I also read the shipped-profile code extracts in evidence f3a54df (pr-997/r2/agree-code/) for p256::SecretKey::agree and x25519::SecretKey::agree on x86_64-unknown-toyos and aarch64-unknown-toyos, and checked them instruction by instruction. I ran no builds; the extracts are the implementer's emitted [profile.toyos] code of this source. I did not read the analysis notes or any ring or BoringSSL source.

Round-2 items

A. Key-agreement bullet: fixed, and the code fix is correct.

• The order is now true. The bullet says each agreement "writes its output bytes into a Secret it owns, then erases the values they came from".
• The remaining copies are named in the contract:
  • the output bytes left in the agreement's finished frame by the move into SharedSecret;
  • the arithmetic intermediates, under "Not erased".
• NIST. affine(&self, x, y) writes into a Workspace<[[u64; N]; 2]> that agree owns. encode and ECDSA verify pass plain arrays, which is correct because their coordinates are public.
• X25519. multiply writes into the caller's &mut [u8; 32]. agree passes a Secret, which is also erased on the zero-refusal path. public_key passes a plain array, which is public.
• I checked the shipped code against the body's per-target list:
  • P-256, x86-64.
    • Zeroed, each group followed by the fence: the coordinates' workspace (−128..−65, in four 16-byte stores), the to_be staging word at −48 (the erase's staging slot), the product (−256..−161) and the consumed scalar.
    • Remaining: the output local at −160..−129, copied to the return slot.
  • P-256, aarch64.
    • Zeroed: the coordinates at x29−96..−33, the staging word at x29−16, the product at sp+32..sp+127 and the scalar.
    • Remaining: the output at [sp, sp+32).
  • X25519, x86-64. The result at −48..−17 is copied to the return slot. Only −48..−33 is zeroed, as the staging slot for erasing the consumed key, so −32..−17 remains.
  • X25519, aarch64. The same, with [sp+16, sp+32) remaining.
  • Round 1's affine return-slot copies are gone on both targets. The body is accurate.

B. Codegen sentence: fixed. The workspace bullet now says only what holds regardless of code generation.

Suggestions C and D and the Zeroable nit are taken. The evidence correction (copy_nonoverlapping's overlap check) is in the body.

Statement for the owner's condition

The erasure contract in lib/crypto/src/secret.rs is now accurate and complete enough for the owner's condition.

• It states what is erased:
  • owners and the hash and MAC states;
  • the named key-agreement values, once the output is written;
  • workspaces, on every return path, through their own storage only;
  • S and Poly per value.
• It states what is not erased:
  • the other field elements, residues and points;
  • registers, spills, by-value moves and returns, and moved values' earlier locations;
  • finished frames, including the output bytes' copy in the agreement's frame;
  • the caller's buffers.
• Every claim I checked matches the source and the shipped code on both ToyOS targets.
• The remaining P-256 by-value-move gap, and the X25519 one, are stated honestly and exactly, per target, in the body.
• M1 is met on both benches: T14 0.796–0.936, AMD 0.795–0.882.

For the orchestrator

• Stale body header. The first line still says "Stacked on crypto: RSA R^2 by squarings, NIST curves as compile-time types, Ed25519 constants, a register barrier (parity items 1-4) #990 (base branch wt/toyos-crypto-perf)". crypto: RSA R^2 by squarings, NIST curves as compile-time types, Ed25519 constants, a register barrier (parity items 1-4) #990 has merged and the base is main.
• Stale ladder bullet. The "What the generated code shows" bullet says of the round-0 ladder finding that "The contract above now says so". The contract deliberately no longer describes the ladder's code generation, so "the contract above now says so" should go.
• Note, not a defect. S's per-value line here still reads "for now … until its reduction is rewritten". That is true at this head, and crypto: Ed25519 verify by one joint multiplication, scalars by Barrett (parity items 6, E3, E4) #997 settles it.

No findings.

Verdict: LAND.