[Japabu]

Based on main 18a3873 (after #993 and #1015). Two commits: 652b3d0 (round 0, 04e784c rebased) and 9b76272 (round 1).

Problem

On the T14 at #1000, RSA verify was 2.0–2.4x ring: RSA-2048 PKCS#1 52.5 us against 24.5. M9 put key construction at 13.7 us and the exponentiation at 38.7 us; both are Montgomery multiplications, 6 and 18 of them.

M2 measured this kernel's shape, mulx with two carry chains, at 0.40x (T14) and 0.43x (AMD bench) of the mulx + _addcarry_u64 intrinsics form for a 2048-bit modulus. LLVM emits no adcx/adox from Rust, so this is the one place the analysis named where asm! is justified (R5).

What changes

• arch/x86_64/montgomery.rs. One asm! block per word of b: a product row and a reduction row over the modulus's words, four words per loop step.
  • mulx forms the products. Their low and high halves add on two independent chains, CF through adcx and OF through adox (Intel SDM Vol. 2A).
  • The loops count with lea and jrcxz, which leave both flags alone.
  • Rust keeps the outer loop and the final subtraction. All RSA data is public; the kernel has no data-dependent branch or address in any case.
• Dispatch. CPUID leaf 7 EBX bit 19 now admits ADX beside BMI2. The hosted x86-64 dispatch takes the kernel where both are present, after checking its length precondition. Elsewhere the portable CIOS multiplication runs, now named mul_portable.
• Key size. Keys use whole groups of four words; the zero words above a modulus only enlarge R. 2048- and 4096-bit keys are unchanged (32 and 64 words).

Metal

The combined T14 boot (ec01b15, which carries this kernel unchanged) passed with judge exit 0. crypto_parity verified ring's RSA signatures through the kernel before timing them. Ours over ring:

row	PKCS#1	PSS
RSA-2048 verify	1.16	1.10
RSA-4096 verify	1.18	1.14

At #1000 these were 2.14 / 1.99 and 2.41 / 2.30.

Review round 1 (9b76272)

• The kernel's contract and both dispatchers' now state the return: out and the returned top word are a·b/2^(64n) mod m plus at most one m, below 2m and unreduced. The caller subtracts.
• The equivalence test's doc names the padded word counts it covers: 32 to 64 in steps of 8.
• Checks at 9b76272: cargo run -- --ci host exit 0, 93 green; crate clippy (host and --target x86_64-apple-darwin) and crate tests in the three forms, exit 0. Log: https://github.com/ToyOSOrg/evidence/tree/847d357932fe05252d2d4a39f8c507bcd3c5580d/pr-1014/r2

Round 2 (79fbb43)

• instruction_path_matches_the_portable_multiplication prints whether rsa_mul answered, that is whether the instruction path ran. A --nocapture run then shows that it compared the kernel, not the portable code with itself. Under Rosetta it prints the portable path. The test reads no CPUID; its probe uses zero operands, inside the kernel's contract.
• For the AMD bench's Linux: a static x86_64-unknown-linux-musl build of the library test binary at 79fbb43.
  • The development Mac has no Linux C toolchain, so ring, rcgen and rustls's ring backend (dev-dependencies) are dropped from that build, and with them the rustls-provider tests. The library, the kernel and this test are unchanged.
  • Filter: rsa::tests::instruction_path --nocapture.

Checks (round 0)

All at 04e784c. Logs: https://github.com/ToyOSOrg/evidence/tree/ce88e7308dadb4e4909cdad09cf839d4832d2d3c/pr-1014/r1

• cargo run -- --ci host: exit 0, 93 steps green. The development Mac is aarch64, so these runs test the portable path.
• Crate clippy (adopted lints, -D warnings): exit 0 in the three CI forms for the host and for --target x86_64-apple-darwin, and for x86_64-unknown-uefi. Crate tests: exit 0 in the three forms.
• crypto_instrument_prints_its_table (QEMU x86_64): exit 0. QEMU's qemu64 model has no BMI2, so it runs the portable path.
• The kernel's arithmetic, emulated (emulate.py in the evidence; scratch, never lands). It interprets the exact asm! template from the source file, with the SDM's semantics for mov, xor, mulx, adcx, adox, imul, lea, jrcxz and jmp. Over whole multiplications it checks a·b/R mod m, below 2m:
  • for n = 4, 8, 32, 36 and 64 words;
  • on random moduli and the all-ones modulus;
  • at the largest residues.
  • It passes. Two mutations fail it: one adox turned into adcx, and the OF carry into t[n + 1] dropped. So does a misplaced store.
• The assembled kernel (x86_64-unknown-toyos, [profile.toyos]): 163 lines, 12 mulx, no call. The register allocation preserves rbx, which it chose for lo.
• New test instruction_path_matches_the_portable_multiplication: five modulus lengths (2048 to 4096 bits, three of them not multiples of 256), 64 cases each, the largest residues included. It runs the kernel only on x86-64 hosts with ADX.

Measurements

Readback staged at 04e784c (crypto_instrument, cryptocase; exit 2 = Staged). The RSA rows run the kernel on both benches. Before timing, crypto_parity checks that each row's verification succeeds on ring's signatures.

• From M2's single-multiplication rows, I expect the 18 exponentiation and 6 key multiplications to fall to about 0.45x their present time, which would put RSA-2048 verify near 25 us against ring's 24.5. That is an inference, not a measurement.

Risks

• The kernel has run only on metal. The development Mac cannot execute it: Rosetta raises SIGILL on adcx/adox. The T14 boot above is its first execution. On an ADX host, instruction_path_matches_the_portable_multiplication passed on Linux on an AMD Ryzen 7 4800U (run, binary hash and build recipe). It printed bmi2 1 adx 1 and the kernel path. The binary is the musl unit-test build at 79fbb43, with three C-backed dev-dependencies removed so that it builds on the Mac (musl-devdeps.patch). The library and test source are unchanged. That test covers 64 cases per word count, including the largest residues; it is the check that would catch a carry error on rare inputs. The run predates 720756f, which removed the test's CPUID print and changed only its probe's operands.
• No x86_64-apple-darwin run takes the kernel path. Rosetta's CPUID reports no leaf-7 feature: no BMI2, ADX or AVX2 (cpuid-rosetta.log). So --target x86_64-apple-darwin tests take the portable path, and no Rosetta run exercises this kernel. This corrects my earlier finding, recorded in crypto: a 5x51 field with typed bounds and erasure at the boundary (parity items 1 and 5) #992's evidence, that Rosetta reports ADX. That probe was built with -C target-feature=+bmi2,+adx, which makes is_x86_feature_detected! a compile-time constant.
• No dedicated squaring kernel (R4). 22 of the 24 multiplications are squarings, so an asm squaring is the next lever if the rows still fall short.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PXEk8BBMDT8tXu4AnENB9Q

[Japabu]

Review of #1014, round 1 (head 04e784c, R5)

What I read and did not run

• Read:
  • the commit;
  • arch/x86_64/montgomery.rs and the asm! template, instruction by instruction;
  • the dispatch in arch/mod.rs and arch/x86_64.rs;
  • rsa.rs's mul, montgomery_r2, the padding and the exponentiation's uses of words;
  • the new test;
  • the scratch emulator (inspection-pr7/emulate.py) and the assembled listing.
• Not run: nothing.

Architecture

• Where the asm sits. The asm! stays in the architecture module, behind the existing hosted! selector and CPUID cache. This is the one place M2 justified asm, because LLVM emits no adcx/adox.
• What Rust keeps. Rust keeps the outer loop and the final subtraction, so the kernel is one row pair.
• Machines without ADX. Padding keys to four-word groups costs non-ADX machines nothing for 2048-, 3072- and 4096-bit keys. Other sizes pay a few extra words.
• Size. Net +235 lines.

The kernel, checked

• Flags at loop entry. Each row's loop is entered after xor {hi:e}, {hi:e}, which clears both CF and OF.
  • Between that xor and the loop come only mov, mulx, lea and jrcxz, none of which writes a flag.
  • In the reduction row, the imul that forms q (and leaves CF and OF defined by overflow) comes before that row's xor.
  • So both chains start at zero in both rows.
• Flags across iterations. Inside the loops, CF is written only by adcx and OF only by adox. lea, mov, jrcxz and jmp preserve both (SDM Vol. 2A). So each chain carries across words and iterations.
• Product row.
  • t[j] gets t[j] + lo(a_j·b_i) on CF, and hi(a_{j−1}·b_i) on OF.
  • The h0/hi alternation is consistent: the first word of each quad adds hi, the last mulx of the quad writes hi, and the closing adox adds h0.
  • The tail folds the pending hi and both carries into t[n]. It writes t[n+1] as the two chains' carry-outs.
  • Overwriting t[n+1] is correct. After the previous reduction the value lives in t[0..=n], and t[n+1] is stale.
• Reduction row.
  • q = t₀·n0. Word 0's sum is computed only for its CF, with OF still clear, and is not stored.
  • Words 1..n−1 shift down by one through the same alternation. The tail writes t[n−1] = t[n] + h0 + CF + OF, and t[n] = t[n+1] + carries.
• Bounds. With a, b < m, the CIOS bound t < 2m holds after each row pair. This includes zero-padded moduli, since m < R.
  • So t[n] ≤ 1, and the n + 2 words never overflow.
  • mul returns t[n], and the caller subtracts once when top != 0 || out ≥ m.
• Operands.
  • Intel syntax: mulx hi, lo, src writes the high word first, which matches.
  • Every scratch register is out(reg), not a late output, so none shares a register with an input that is read after it is written. {t}, {m}, {n0}, {quads} and {zero} are all read late.
  • rdx and rcx are declared. Flags are not preserved, and memory is assumed read and written. nostack is correct because nothing is pushed.
  • The listing allocates 11 general registers plus rdx and rcx, saving rbx.
• Memory.
  • Reads cover a[0..n] and m[0..n].
  • Writes cover t[0..n+2] within [u64; 66], which suffices for n ≤ 64.
  • rsa_mul asserts the length precondition before the unsafe call.
  • n = 0 never reaches row, because the outer loop runs zero times.
• Emulator. It interprets the source template's actual lines and models flags per the SDM.
  • It sets CF and OF to undefined after imul, so any use before the xor would raise.
  • It holds whole multiplications to bigints for n = 4 to 64, with the all-ones modulus and maximal residues.
  • That is good evidence for the template's logic. It is not evidence of real-CPU behaviour, which only the first metal and CI runs give.

Dispatch

• CPUID bit. ADX is CPUID leaf 7, sub-leaf 0, EBX bit 19, and BMI2 is bit 8 (SDM Vol. 2A, CPUID). Neither needs XCR0 state.
  • bmi2_adx() requires both bits.
  • The decode test removes bit 19 and checks that the feature goes.
  • The hosted test compares the result with is_x86_feature_detected!.
• Fallbacks.
  • UEFI and non-x86 targets get None through hosted!.
  • The portable feature yields Features(READ), so they get None there too.
• Padding.
  • words = len.div_ceil(32)·4, at most 64.
  • montgomery_r2 works for any word count: 64w − (bits − 1) + w doublings, then six squarings, give 2^(64w)·R.
  • n0 depends only on m₀.
  • Every comparison and subtraction runs over self.words, and the zero words above m are harmless.
  • The test covers 32, 40, 48, 56 and 64 words.

Findings

BLOCKER

1. Three contract comments are wrong or garbled. These are the contracts of an unsafe kernel and its dispatcher, so they must be exact.
   • arch/x86_64/montgomery.rs:8 says "out = a b / 2^(64n) mod m". The kernel does not reduce: out with t[n] is the value below 2m, and the caller subtracts.
   • arch/mod.rs:57–59 says "with the top word of the unreduced result below 2m". It is the result, not its top word, that is below 2m, and the function returns that top word.
   • arch/x86_64.rs:155 has the same ambiguity.
   • Suggested wording: "out and the returned top word are a·b/2^(64n) mod m plus at most one m: below 2m, unreduced".
2. rsa.rs:349 — the test's doc says "for every word count". It covers five padded counts, 32 to 64 in steps of 8. Say that instead.

Before landing (orchestrator)

• The kernel has never executed.
• The metal boot must run crypto_parity's RSA rows, which verify ring's signatures before timing.
• An x86-64 host run must have ADX, so that instruction_path_matches_the_portable_multiplication exercises the kernel. That run is a CI runner in the merge queue, or the metal guest.
• Gap. The guest check compares only a verify result, so a carry bug on rare inputs would not show there. The host test with 64 cases per length, including the maximal residues, is the one that would catch it. Confirm that the merge-queue runner reports ADX, or run that test once on an ADX machine.

SUGGESTION

3. Each multiplication calls the out-of-line features(), 24 times per verify. crypto: no out-of-line calls on ChaCha20's per-message path (parity item 9, part) #1015 inlines it. If crypto: no out-of-line calls on ChaCha20's per-message path (parity item 9, part) #1015 lands first, nothing is needed.

PR body (orchestrator)

• The base is d7f269d, not 81c1386 as the body says.
• The body says Rosetta raises SIGILL on adcx/adox while mulx runs, and also that Rosetta's CPUID reports no BMI2. These statements are consistent, but say plainly that no x86_64-apple-darwin run takes this path.

Verdict: SEND BACK (items 1–2, wording). After those, this PR is fit to LAND once the metal run and an ADX host test pass.

[Japabu]

Review of #1014, round 2 (head 79fbb43, R5)

What I read and did not run

• Read:
  • 9b76272 (round 1) and 79fbb43 (the test's path report);
  • the whole diff against 18a3873 again: the kernel, both dispatchers, the padding and the test.
• Evidence read:
  • adx-binary/ (README, SHA256SUMS, amd-linux-run.txt, musl-devdeps.patch); the binary's hash matches;
  • evidence/pr-1014/r1 and r2.
• Not run: nothing. I read no other implementation's source. The only citations are the SDM and Koç–Acar–Kaliski.

Architecture

Unchanged from round 1, where it was accepted. The one asm! kernel stays in arch/x86_64/montgomery.rs, behind hosted! and the CPUID cache. Rust keeps the outer loop and the final subtraction, and keys are padded to four-word groups. Net +256/−7: 146 lines are the kernel, about 60 are tests, and the rest is dispatch.

Round-1 blockers

1. Contracts. Resolved. arch/x86_64/montgomery.rs:8–9, arch/mod.rs:57–59 and arch/x86_64.rs:163–164 now say that out and the returned top word are the unreduced result below 2m. rsa.rs mul subtracts when top != 0 || out ≥ m, which matches.
2. Test doc. Resolved. It says "32 to 64 in steps of 8", which matches 256, 300, 384, 448 and 512 bytes after div_ceil(32)·4.

The ADX evidence

• The run. toyos_crypto-tests-79fbb43af ran rsa::tests::instruction_path --nocapture on the AMD bench under Linux, a Ryzen 7 4800U, as a host test only. It printed bmi2 1 adx 1 and instruction path: the BMI2/ADX kernel. The test passed, with EXIT=0.
• The build. The binary is the crate's library tests at 79fbb43 for x86_64-unknown-linux-musl. Only the ring, rcgen and rustls-ring dev-dependencies were removed (the patch shows exactly that). The kernel, the dispatch and this test are byte-identical, and --lib with those features does not need the removed crates.
• What it shows. The kernel executed on a real ADX CPU and agreed with mul_portable on 320 multiplications: five word counts with 64 cases each, the maximal residues (n − 1)² among them.
• The portable oracle. mul_portable is held independently by the RSA differential against ring and by Wycheproof, so the comparison has an independent anchor.
• Intel. The combined T14 boot (ec01b15) ran the same kernel on Intel and verified ring's signatures through it before timing.
• Sufficiency. The template's emulation (r1 evidence) covers its logic. This run covers its execution on Zen 2, and the T14 boot covers Intel with a verify result. Together they suffice for this PR. Nothing more is needed for the AMD bench's guest: its rows would run the identical code, and the host run already holds the arithmetic.
• What the record must show. Publish amd-linux-run.txt with the binary's SHA-256 and build recipe in pr-1014's evidence, and cite it in the PR body. The run must show adx 1, the kernel line and the pass. After finding 1 below it is the kernel line that carries the claim; the CPUID line becomes redundant. Deleting the print does not invalidate this run.

Findings

BLOCKER

1. lib/crypto/src/rsa.rs:353–360 — the test reads CPUID with #[cfg(target_arch = "x86_64")] and core::arch::x86_64::__cpuid_count in rsa.rs.
   • Root's rule keeps architecture intrinsics and target_arch in architecture modules, selectors, build/arch.rs or the licence evaluator. rsa.rs is generic code.
   • The block is also redundant. The next line's crate::arch::rsa_mul(...).is_some() reports which path ran, and that is the claim a reader needs. arch/x86_64.rs's hosted test already ties bmi2_adx() to is_x86_feature_detected!("bmi2") and ("adx").
   • Fix: delete the block, including its #[allow(unused_unsafe)] and the Rust 1.89 comment. A recompile and the crate's clippy suffice; the ADX run stays valid.

SUGGESTION

2. rsa.rs — the probe calls rsa_mul with a = b = m = all ones and n0 = 1, outside the documented a, b < m.
   • It is memory-safe, and the result is discarded.
   • Zero operands, for example a = b = 0 with that m, would stay within the contract at no cost.
3. arch/mod.rs:57 — the doc says what Some holds but not when the function returns None. "None where the CPU has no such path" would complete the contract.
4. Round 1's suggestion 3 (inlining features()) is settled by crypto: no out-of-line calls on ChaCha20's per-message path (parity item 9, part) #1015.

PR body (orchestrator)

• Risks. "has not yet run on an ADX host" and "This is open for the orchestrator" are now stale. Replace them with the AMD Linux run and its evidence link.
• Round 2. After finding 1, it should no longer say that the test prints the CPUID bits.

Verdict: SEND BACK (finding 1, a deletion of eight lines; everything else is ready to land).