x86 X448/Ed448: field arithmetic by calls of verified functions

[alex]

Implements #1252's spec of vg_gf448_r16_* on x86.

Why

On x86 (32-bit), X448 and Ed448 inlined every field operation: each multiplication was a fully unrolled 28×28 product. That made src/asm/x86/x448.rs about 46k instructions and ed448.rs about 179k. This PR implements #1252's curve448 field functions on x86 and makes the callers call them.

What

• The field functions (Impl/X448/X86.lean, Artifacts/Gf448R16/X86.lean): vg_gf448_r16_mul, _add, _sub and _mul_a24.
  • The multiplication is the fully unrolled 28×28 product, as the inline code had it: each row reads its a limb and the b limbs at fixed offsets, with a carry pass. It exists once, so its size barely matters. (A first version ran the rows as a loop through a row pointer; CI measured it about 6% slower, from the dependent load at each row.)
  • Each function saves the callee-saved registers in its own part of the working space (bytes 4080–4095, inside the 3584–4095 the spec gives it). They use no stack.
  • Correctness and constant time are proven against the shared contracts (Proof/X448/X86/Fn*.lean).
• The callers: X448's vg_x448, and Ed448's vg_ed448_scalar_base and vg_ed448_verify_equation. Each field operation pushes its arguments (ws, o, a, b) and calls a field function, which uses the 20 bytes of stack below the return address. Their contracts become …Contract X86.abi 20 with stack := 20.
• Correctness of the callers:
  • Memory frames now include the call stack. Facts about memory outside the working space are recovered per piece with Exec.frameSp.
  • X448's Main.lean and Ed448's BaseMain.lean are split into stage lemmas.
• Constant time of the callers (Proof/X448/X86/{CallCT,Runs,CT}.lean, Proof/Ed448/X86/{BaseCT,VerifyCT}.lean):
  • The calls are related run by run (RelCT.callWith), using the callee's own constant time, rather than by one taint analysis through the callees' bodies.
  • The blocks between calls are proven by the taint analysis, from what each run's correctness says of its own state.
  • The loops (ladder, squarings, Ed448's loops) use RelCT.loop with the correctness invariants.
  • Ed448's RestCT.lean, the old single taint check of everything after the entry block, is deleted.
• Ed448's complete operations (public key, signing, verification): the only change is that their call sites now show the callee's 20 bytes of stack are apart from its buffers (Kit.callee_stk, Kit.callee_in). They already reserved those bytes (CalleeOk.stack ≤ 20).
• No Spec/ or TCB/ changes.

The registration file for the multiplication, addition and subtraction states ofSig explicitly. The default rfl proof does not see through binContract's extra definition in #1252's spec. This is harmless, but it may be worth inlining binContract there.

Size

Instruction lines in the generated x86 code:

file	before	after
x448.rs	46,474	5,239
ed448.rs	179,479	24,712
gf448_r16.rs (new)	—	8,934
total	225,953	38,885

Only src/asm/x86/{x448,ed448,mod}.rs and the new gf448_r16.rs change under src/.

Performance

CI's Benchmarks check ("Compare with base (x86)", i686, on the unrolled multiplication) shows every X448 and Ed448 benchmark faster than base:

Benchmark	Base	Head	Change
ed448_keygen/57	6.74 ms	6.50 ms	3.5% faster
ed448_sign/64	6.77 ms	6.54 ms	3.4% faster
ed448_sign/1024	6.78 ms	6.55 ms	3.4% faster
ed448_sign/16384	7.15 ms	6.92 ms	3.1% faster
ed448_verify/64	11.12 ms	10.72 ms	3.5% faster
ed448_verify/1024	11.13 ms	10.75 ms	3.4% faster
ed448_verify/16384	11.32 ms	10.91 ms	3.6% faster
x448/56	3.39 ms	3.28 ms	3.3% faster
x448_generate/56	3.39 ms	3.28 ms	3.3% faster
x448_public_key/56	3.39 ms	3.28 ms	3.4% faster
x448_raw/56	3.39 ms	3.28 ms	3.2% faster

Local i686 measurements (a small harness over the public API, since the bench crate needs a 32-bit OpenSSL) were too noisy on this machine to resolve a few percent either way.

Checks

• lake build (all jobs) and lake env lean --run Emit.lean --check pass. The emitter's audits pass: standard axioms only, every VG.Spec definition in Spec/.
• ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py, cpu_tests.py lint and algorithms_table.py all pass.
• cargo fmt --check passes, and cargo clippy --all-targets -- -D warnings passes on x86-64 and i686-unknown-linux-gnu.
• cargo test with Wycheproof passes natively and on i686-unknown-linux-gnu, in debug and release. That includes the RFC 7748/8032 and Wycheproof X448/Ed448 tests.
• The costliest new declaration is verifyEquation_ct, at about 4.6 s, mostly kernel time for the entry block's taint check.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AiLjb1MZn17fRtREr4t9q9

---

Generated by Claude Code

[alex]

Rebased onto main (9feca45, after #1252 and #1254 merged; no conflicts, no files shared with #1254). CI is green on d6047fd, including the x86 Benchmarks comparison, and a clean local lake build plus Emit.lean --check pass. Ready to be queued.

---

Generated by Claude Code