[alex]

The AArch64 ML-KEM NTTs and inverse NTTs are now proven by an abstract interpreter that the kernel runs over the code:

• forward: vg_mlkem_ntt, Readonly.fwd and Readonly.fwdW;
• inverse: vg_mlkem_ntt_inv, Readonly.inv and Readonly.invW.

This replaces the hand proofs of their passes, about 3,000 lines. This change is proof only: src/asm/ is unchanged (Emit.lean --check), and so are the TCB, the Spec, the contracts and the statements of Ntt16.correct, Ntt16.correctInv, Readonly.fwd_ok, Readonly.inv_ok, W.fwdW_ok and W.invW_ok.

The machine (Proof/MlKem/AArch64/NttR/)

• Sym.lean: the interpreter.
  • Each halfword lane holds a term:
    • the coefficient p after st levels;
    • a constant;
    • a product by a zeta or its tw;
    • a product modulo q;
    • a Gentleman–Sande difference and its products;
    • a step of a reduction;
    • not followed.
  • Terms, vectors, general registers (pointers into regions, or numbers) and the 16-byte chunks of the regions the code touches are all packed into Nats. The kernel evaluates them natively.
  • For NTT (fwdRules), a butterfly is accepted only when its two terms are the pair the Cooley–Tukey layer st combines, with that block's zeta (bflyOk).
  • For NTT⁻¹ (invRules), the levels are the Gentleman–Sande layers (gsPair, gsZeta), the reductions between them and the multiplication by 3303. The final reduction to [0, q) is collapsed too.
• Sound.lean, Step.lean: soundness.
  • What a term means: Hd, given the coefficients after each number of levels (L) and their reductions (O).
  • Every instruction the NTTs use keeps the relation Rel between the machine's state and the real one (step_ok).
  • So do blocks, counted loops and programs (run_ok, loop_ok, runP_ok).
  • Region separation is stated once in Ctx and built by Ctx.of.
• Model.lean: the coefficients the butterflies compute (Lf) obey bflyOk (model). They represent NTT's within (st + 1) q (Lf_rep), and their reductions are NTT's coefficients (Of_ntt).
• ModelI.lean: the same for NTT⁻¹. Its levels (Li) obey the inverse's operations (modelI) and represent nttInvL's coefficients within their bounds (Li_rep). Their reductions are nttInv's coefficients (Oi_nttInv).
• RunW.lean, RunU.lean, RunI.lean: the regions and starting terms of each transform, and the kernel's runs.
  • Forward: checkW_ok, checkU_ok, checkN_ok.
  • Inverse: checkIW_ok, checkIU_ok, checkIN_ok, the last for the end of nttInv.
  • The polynomial is stored with 16 bits (fwdW, invW) or as u32s (fwd, ntt, inv, nttInv). For u32s the high halfwords are junk on input and zero on output.
  • Each table is a Nat literal (tabT, itabT). Its lanes are read by a general lemma (slot_foldr), not evaluated.
• FwdW.lean, FwdU.lean, Inv.lean: the top proofs.
  • The starting state holds of the caller's (initW_rel, initU_rel).
  • The regions are apart (ctxW, ctxU, ctxN).
  • These take the table's symbol, the table and the model, so forward and inverse share them.
  • The run leaves NTT (fwdW_run, fwd_run, ntt_run) or NTT⁻¹ (invW_run, inv_run, nttInv_run) of the input in the polynomial.
  • ntt and nttInv first store their table into the working space with the existing halves_ok. Then the machine runs the rest (nttTail, nttInvTail).

Deleted

• Whole modules: Ntt16/W/Pass2.lean, Pass2.lean, Last.lean, InvPass1.lean, InvPass2.lean, InvIdx.lean, InvRows.lean, W/InvPass1.lean and W/InvPass2.lean.
• The forward-only parts of Ntt16/Pass1.lean, W/Pass1.lean and Fwd.lean:
  • the pass invariants;
  • p1_body and its loads and arithmetic;
  • the table lemmas;
  • the constants' lemmas.
• All of Gs.lean but the lane lemma gs_lane.
• CoeffsIn moves to Widen16.lean, its only remaining user.

Build time

The first version of this PR (forward NTTs only) made CI's build about 25 s slower: 48.4 s of new machine modules against 22.9 s of forward proofs saved (CI run 39649160162).

The inverse on the machine adds ModelI, RunI, LitI and Inv. It deletes:

• the inverse's hand proofs, about 40 s on that run (InvPass1, InvPass2, InvIdx, InvRows, W.InvPass1, W.InvPass2);
• Pass2 and Last.

I'll post the module times from this PR's own CI run as a comment.

No maxHeartbeats or other limits.

Checks

• Full lake build and Emit.lean --check (no change to src/asm/).
• The Python checks:
  • check_lean_imports, check_lean_modules and check_lean_public_imports;
  • check_registrations and check_lean_speed;
  • check_vectors and check_arch_gates;
  • check_variants and check_mcdt.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

[alex]

Build-time numbers from this PR's own CI (run 39649160162, the assembly step's Built lines), compared like for like with main's CI.

New machine modules (48.4 s):

Module	s
RunU	11
Step	9.9
RunW	7.5
Sound	4.4
FwdU	3.6
Model	3.2
Lit	2.8
FwdW	2.4
Ctx	1.9
Sym	1.7

Trimmed forward modules (was → now):

Module	Was	Now
Pass1	4.8	2.3
Pass2	11.0	1.8
Last	5.3	1.5
W.Pass1	2.0	1.1
W.Pass2 (deleted)	3.4	—
Fwd	3.5	2.3
Readonly.Fwd	1.7	1.3
W.Fwd	2.7	1.2
Total	34.4	11.5

On CI this PR costs about 60 s, against 34 s for the hand proofs it replaces: +25 s. My local profile sums had suggested the opposite. They undercounted, because they leave out the time a module spends waiting on its imports under 6 workers.

Of the 60 s, about 24 s is fixed cost of the machine:

• Sym, Sound, Step, Model, Ctx and Lit.
• These are paid once and shared by the transforms that follow, starting with the out-of-line NTT stacked on this PR.

The other 24.5 s is the per-transform runs and top proofs:

• RunU and RunW: the kernel's lit_decide over the 4 + 2 passes.
• FwdU and FwdW.

Moving the inverse NTT onto the machine would delete InvPass1, InvPass2, InvIdx and W.InvPass* (about 40 s on this run). That would more than repay the fixed cost, but it is not in this PR.

---

Generated by Claude Code

[reaperhulk]

Let's not regress on proof perf if we can avoid it.

[alex]

Agreed. As it stands this PR costs about 25 s of CI build. The forward NTTs are the only thing on the machine so far, and its fixed cost (about 24 s: Sym, Sound, Step, Model, Ctx, Lit) is paid with nothing yet to amortize it.

The kernel's runs themselves are cheap: checkU_ok 4.2 s, checkN_ok 3.2 s and checkW_ok 3.0 s (local profile). The cost is in the machine's modules.

So I'll make this PR a net win rather than wait for the follow-ups. I'll move the three inverse NTTs (nttInv, Readonly.inv, Readonly.invW) onto the same machine here, which is the same kind of change and also proof only. That deletes InvPass1 (17 s), InvIdx (10 s), InvPass2 (6.6 s), the W.InvPass* modules and what remains of Pass1, Pass2 and Last (about 45 s on this PR's CI run). It adds three more kernel runs of about 3 s each, plus a Gentleman–Sande rule in Sym, Step and Model.

I'll update this PR with the new CI module times once it's done. Until then, please hold off merging.

---

Generated by Claude Code

[alex]

Build times from this PR's CI run at 926300f (run 39678153997, the Lean assembly job's per-module times):

Machine (NttR), forward and inverse:

Module	s
RunI	6.7
Step	6.3
RunU	4.6
Sound	3.7
RunW	3.7
Lit	2.1
Sym	1.8
Model	1.5
FwdU	1.2
LitI, ModelI	1.0 each
FwdW	1.0
Ctx	0.8
Inv	0.6
Total	35.9

What is left of Ntt16: Gs 2.4, Widen16 1.7, Pass1 1.4, W.Pass1 1.1, Fwd 0.9, Readonly.Pre 0.9, Inv 0.7, Readonly.Fwd 0.5, W.Fwd 0.5, Readonly.Inv 0.5, W.Inv 0.5. That is about 11 s.

So the NTT proofs, forward and inverse, now take about 47 s of module time.

Before this PR, from run 39649160162 and main's numbers in the description:

• the forward hand proofs took 34.4 s;
• the inverse hand proofs this deletes took about 40 s (InvPass1, InvPass2, InvIdx, InvRows, W.InvPass1, W.InvPass2).

So the PR now saves roughly 25–30 s, where the forward-only version cost about 25 s.

These come from two runs, and module times on CI vary between runs: RunU took 11 s on the earlier run and 4.6 s on this one. The direction is clear, but treat the exact size as approximate.

---

Generated by Claude Code