NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex

The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
  lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
  telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
  remaining-bits measure: per-step 64-bit window read (4-way word split),
  digit write via hcast/wrapping_sub (exact value window - 32*carry',
  oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
  DISCHARGED; the digits satisfy the NAF conditions and
      sum naf[k]*2^k = V   EXACTLY (integers, no modular slack)
  for any scalar whose LE byte value V is below 2^253.

And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
  base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
  kernel-checked via denominator-free 121666-scaled witnesses. Includes the
  generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
  vartime_double_base::mul: for canonical scalars and a valid on-curve A,
  the result is valid, on-curve, and denotes
      dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
  with both digit arrays proven exact NAF encodings. Phase 2 (group
  semantics [a]A + [b]B) requires Edwards associativity — deferred and
  documented; nothing assumes it.

Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.

CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

verification/Proofs/DsmMulSpec.lean

@@ -0,0 +1,200 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmMulSpec.lean — double-scalar-mul campaign, brick 4:
+   the basepoint constant and the public `vartime_double_base::mul` spec.
+
+   · `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is a VALID
+     extended point ON THE CURVE denoting the standard base point
+         B = (x_B, y_B),  x_B = 15112…202,  y_B = 46316…960
+     — kernel-checked literal arithmetic: the extended coherence X·Y = Z·T
+     and the (121666-scaled, denominator-free) curve equation
+         121666·y² + 121665·x²y² ≡ 121666 + 121666·x²  (mod p).
+     A corrupted basepoint constant would be caught here.
+
+   · `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC:
+     for canonical scalars (byte values < 2^253) and a valid on-curve A,
+     `mul a A b` returns a valid on-curve R with
+         edPt R = dsmFold (digits of a) (digits of b) (edPt A) edBasePt edId 256
+     where both digit arrays are proven NAF encodings of the scalars' exact
+     byte values (existentially exposed with their NafDigits + nafSum facts).
+     Composes non_adjacent_form_spec ×2, dsm_top_index_spec, naf_table_spec
+     ×2 (A and the basepoint), dsm_loop_spec, proj_as_extended_spec.
+     Phase 2 (reading dsmFold as [a]A + [b]B in the group) requires Edwards
+     associativity — deliberately deferred and documented; nothing here
+     assumes it.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmNafSpec
+open Aeneas Aeneas.Std Result ControlFlow
+open curve25519_dalek
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+set_option exponentiation.threshold 600
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- Generic mod-p witness → Fp product identity (abstract, no literal
+    crunching during cast distribution). -/
+theorem fp_mul_eq_of_witness (a b c : ℕ) (hmod : (a * b) % P = c % P) :
+    (a : Fp) * (b : Fp) = (c : Fp) := by
+  have h1 : ((a * b : ℕ) : Fp) = ((c : ℕ) : Fp) := by
+    rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod]
+  push_cast at h1
+  exact h1
+
+/-- Generic 121666-scaled curve-equation witness → OnCurve (abstract x, y). -/
+theorem onCurve_of_witness (x y : ℕ)
+    (hmod : (121666 * (y * y) + 121665 * (x * x) * (y * y)) % P
+          = (121666 + 121666 * (x * x)) % P) :
+    OnCurve (x : Fp) (y : Fp) := by
+  have h1 : ((121666 * (y * y) + 121665 * (x * x) * (y * y) : ℕ) : Fp)
+      = ((121666 + 121666 * (x * x) : ℕ) : Fp) := by
+    rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod]
+  push_cast at h1
+  have h6 : (121666 : Fp) ≠ 0 := by
+    have h : ((121666 : ℕ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
+    simpa using h
+  have hd := edD_char
+  unfold OnCurve
+  apply mul_left_cancel₀ h6
+  linear_combination h1 - (x : Fp)^2 * (y : Fp)^2 * hd
+
+/-- The standard Ed25519 base point, as ZMod literals. -/
+noncomputable def edBasePt : Fp × Fp :=
+  ((15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp),
+   (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp))
+
+/-- **The transpiled basepoint constant is the standard base point** —
+    valid, on-curve, kernel-audited literal arithmetic. -/
+theorem run_basepoint :
+    ∃ B : EdPoint,
+      backend.serial.u64.constants.ED25519_BASEPOINT_POINT = ok B ∧
+      ExtValid B ∧ OnCurveExt B ∧ edPt B = edBasePt := by
+  -- the four coordinate denotations
+  have hXv : ⟪(Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64,
+      2070867633025821#u64, 562264141797630#u64, 587772402128613#u64] :
+      backend.serial.u64.field.FieldElement51)⟫ =
+      (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) := by
+    simp [denote, feVal, limbsVal, Array.make]
+  have hYv : ⟪(Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64,
+      450359962737049#u64, 900719925474099#u64, 1801439850948198#u64] :
+      backend.serial.u64.field.FieldElement51)⟫ =
+      (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by
+    simp [denote, feVal, limbsVal, Array.make]
+  have hZv : ⟪(Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64] :
+      backend.serial.u64.field.FieldElement51)⟫ = (1 : Fp) := by
+    simp [denote, feVal, limbsVal, Array.make]
+  have hTv : ⟪(Array.make 5#usize [1841354044333475#u64, 16398895984059#u64,
+      755974180946558#u64, 900171276175154#u64, 1821297809914039#u64] :
+      backend.serial.u64.field.FieldElement51)⟫ =
+      (46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by
+    simp [denote, feVal, limbsVal, Array.make]
+  -- coherence of the affine literals: x·y = t (z = 1)
+  have hco : (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) *
+      (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) =
+      (46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by
+    apply fp_mul_eq_of_witness
+    norm_num [P]
+  -- the curve equation for the affine literals (121666-scaled witness)
+  have hcv : OnCurve
+      (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp)
+      (46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by
+    have h := onCurve_of_witness
+      15112221349535400772501151409588531511454012693041857206046113283949847762202
+      46316835694926478169428394003475163141307993866256225615783033603165251855960
+      (by norm_num [P])
+    push_cast at h
+    exact h
+  refine ⟨⟨Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64,
+             2070867633025821#u64, 562264141797630#u64, 587772402128613#u64],
+           Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64,
+             450359962737049#u64, 900719925474099#u64, 1801439850948198#u64],
+           Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64],
+           Array.make 5#usize [1841354044333475#u64, 16398895984059#u64,
+             755974180946558#u64, 900171276175154#u64, 1821297809914039#u64]⟩,
+         ?_, ⟨?_, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩
+  · unfold backend.serial.u64.constants.ED25519_BASEPOINT_POINT
+      backend.serial.u64.field.FieldElement51.from_limbs
+    rfl
+  · simp [Bnd, Array.make]
+  · simp [Bnd, Array.make]
+  · simp [Bnd, Array.make]
+  · simp [Bnd, Array.make]
+  · show ⟪_⟫ ≠ 0
+    rw [hZv]; exact one_ne_zero
+  · show ⟪_⟫ * ⟪_⟫ = ⟪_⟫ * ⟪_⟫
+    rw [hXv, hYv, hZv, hTv, one_mul]
+    exact hco
+  · show OnCurve (edX _) (edY _)
+    unfold edX edY
+    simp only
+    rw [hXv, hYv, hZv, div_one, div_one]
+    exact hcv
+  · show (edX _, edY _) = edBasePt
+    unfold edX edY edBasePt
+    simp only
+    rw [hXv, hYv, hZv, div_one, div_one]
+
+/-- **vartime_double_base::mul — the phase-1 computational specification.**
+    For canonical scalars a, b (LE byte values Va, Vb < 2^253) and a valid
+    on-curve A: the result is a valid on-curve point denoting the abstract
+    double-and-add fold of the two proven NAF encodings over A and the
+    standard base point. -/
+theorem vartime_double_base_mul_spec
+    (a b : scalar.Scalar) (A : EdPoint)
+    (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 : Std.U8)
+    (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8)
+    (hab : (↑a.bytes : List Std.U8) = [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31])
+    (hbb : (↑b.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31])
+    (Va Vb : ℕ)
+    (hVa : Va = a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248)
+    (hVb : Vb = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248)
+    (hValt : Va < 2^253) (hVblt : Vb < 2^253)
+    (hAv : ExtValid A) (hAc : OnCurveExt A) :
+    backend.serial.scalar_mul.vartime_double_base.mul a A b ⦃ R =>
+      ExtValid R ∧ OnCurveExt R ∧
+      ∃ (na nb : Std.Array Std.I8 256#usize),
+        NafDigits na ∧ NafDigits nb ∧
+        nafSum na 256 = (Va : ℤ) ∧ nafSum nb 256 = (Vb : ℤ) ∧
+        edPt R = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 ⦄ := by
+  obtain ⟨B, hBok, hBv, hBc, hBpt⟩ := run_basepoint
+  unfold backend.serial.scalar_mul.vartime_double_base.mul
+  -- the two NAF encodings
+  step with (non_adjacent_form_spec a
+    a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31
+    hab Va hVa hValt) as ⟨na, hnaD, hnaS⟩
+  step with (non_adjacent_form_spec b
+    b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31
+    hbb Vb hVb hVblt) as ⟨nb, hnbD, hnbS⟩
+  -- the top index (constant 255)
+  step with (dsm_top_index_spec na nb) as ⟨i, hi⟩
+  -- table over A
+  step with (naf_table_spec A hAv hAc) as
+    ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, ta, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩
+  -- the basepoint constant
+  rw [hBok]
+  simp only [bind_tc_ok]
+  -- table over B
+  step with (naf_table_spec B hBv hBc) as
+    ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, tb, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩
+  -- the 256-step Straus loop
+  step with (dsm_loop_spec i (by rw [hi]; scalar_tac : i.val = 255) na nb ta tb A B
+    ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩
+    ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩
+    hnaD hnbD) as ⟨r, hrv, hrc, hrfold⟩
+  -- the final projective → extended conversion
+  apply spec_mono (proj_as_extended_spec r hrv)
+  rintro R ⟨hRv, -, -, -, -, hRx, hRy⟩
+  refine ⟨hRv, ?_, na, nb, hnaD, hnbD, hnaS, hnbS, ?_⟩
+  · show OnCurve (edX R) (edY R)
+    rw [hRx, hRy]
+    exact hrc
+  · calc edPt R = (edX R, edY R) := rfl
+      _ = (projX r, projY r) := by rw [hRx, hRy]
+      _ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) (edPt B) edId 256 := hrfold
+      _ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 := by
+          rw [hBpt]
+
+end CurveFieldProofs

verification/Proofs/DsmNafLoopSpec.lean

@@ -0,0 +1,418 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmNafLoopSpec.lean — NAF campaign, stage 3: the w=5 digit loop,
+   by induction on the remaining-bits measure (no unrolling).
+
+   State (naf, pos, carry); exact ℤ invariant (DsmNafMath):
+       carry ≤ 1 ∧ (carry = 1 → pos ≤ 254) ∧ digits ≥ pos all zero ∧
+       digit conditions ∧ nafSum naf 256 + carry·2^pos = V mod 2^pos.
+   One symbolic body-walk per induction step:
+   · `naf_bitbuf_spec`  — the (single|cross)-word 64-bit read at bit pos,
+     4-way split on the word index, closed by naf_window_single/cross.
+   · `naf_update_spec`  — the odd-digit write: hcast / wrapping_sub digit,
+     new carry ∈ {0,1}, exact digit value window − 32·carry′, oddness and
+     |d| < 16 (the strict lower bound needs the window's oddness).
+   · even step: pos+1 via naf_even_step / naf_carry_even;
+     odd step: pos+5 via nafSum_set / naf_odd_step / naf_carry_odd.
+   Exit (pos ≥ 256): naf_exit — the carry is provably dead and
+       nafSum naf 256 = V  exactly (V < 2^253: canonical scalars, which is
+   what the mul call sites provide).
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmNafMath
+open Aeneas Aeneas.Std Result ControlFlow
+open curve25519_dalek
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-! ### Digit-array set plumbing -/
+
+/-- Entries away from the written index are unchanged. -/
+theorem nafDigit_set_ne (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ)
+    (d : Std.I8) (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d)
+    (k : ℕ) (hk : k < 256) (hne : k ≠ pos) :
+    nafDigit naf' k = nafDigit naf k := by
+  have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
+  unfold nafDigit
+  rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) k
+        (by rw [List.length_set]; omega),
+      List.getElem_set_ne (by omega),
+      ← getElem!_pos (↑naf : List Std.I8) k (by omega)]
+
+/-- The written entry holds the new digit. -/
+theorem nafDigit_set_eq (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ)
+    (d : Std.I8) (hpos : pos < 256)
+    (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) :
+    nafDigit naf' pos = d.val := by
+  have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
+  unfold nafDigit
+  rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) pos
+        (by rw [List.length_set]; omega),
+      List.getElem_set_self]
+
+/-! ### The 64-bit window read and the digit write -/
+
+/-- The 64-bit buffer read of the digit loop at bit position pos: its masked
+    value is the 5-bit window of V at pos. Four word cases (the fifth word is
+    the zero pad), each closed by naf_window_single (bit_idx < 59) or
+    naf_window_cross. -/
+theorem naf_bitbuf_spec
+    (x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ)
+    (hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64])
+    (hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))))
+    (u bidx : Usize) (pos : ℕ) (hposv : pos < 256)
+    (hu : u.val = pos / 64) (hbidx : bidx.val = pos % 64) :
+    (if bidx < 59#usize
+     then do
+          let i1 ← Array.index_usize x_u64 u
+          i1 >>> bidx
+     else
+       do
+       let i1 ← Array.index_usize x_u64 u
+       let i2 ← i1 >>> bidx
+       let i3 ← 1#usize + u
+       let i4 ← Array.index_usize x_u64 i3
+       let i5 ← 64#usize - bidx
+       let i6 ← i4 <<< i5
+       ok (i2 ||| i6))
+    ⦃ buf => buf.val % 32 = (V / 2^pos) % 32 ⦄ := by
+  have hb0 : v0.val < 2^64 := by scalar_tac
+  have hb1 : v1.val < 2^64 := by scalar_tac
+  have hb2 : v2.val < 2^64 := by scalar_tac
+  have hb3 : v3.val < 2^64 := by scalar_tac
+  have hulen : u.val < 4 := by clear * - hu hposv; omega
+  have hsz : (U64.size : ℕ) = 2^64 := by scalar_tac
+  split
+  · -- single-word read
+    rename_i hblt
+    have hbv : pos % 64 < 59 := by
+      have h := hbidx ▸ (show bidx.val < 59 by clear * - hblt; scalar_tac)
+      omega
+    step as ⟨w, hw⟩
+    step as ⟨buf, hbuf⟩
+    rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega)
+      with hc | hc | hc | hc
+    · have huv : u.val = 0 := by omega
+      simp only [hx, huv] at hw
+      simp at hw
+      rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
+      have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by
+        rw [hVdef]; try ring
+      have h := naf_window_single V (0) v0.val (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) 0 (pos % 64)
+        hd (by norm_num) (by omega)
+      rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 1 := by omega
+      simp only [hx, huv] at hw
+      simp at hw
+      rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
+        rw [hVdef]; try ring
+      have h := naf_window_single V (v0.val) v1.val (v2.val + 2^64 * (v3.val + 2^64 * 0)) 64 (pos % 64)
+        hd (by omega) (by omega)
+      rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 2 := by omega
+      simp only [hx, huv] at hw
+      simp at hw
+      rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * 0)) := by
+        rw [hVdef]; try ring
+      have h := naf_window_single V (v0.val + 2^64 * v1.val) v2.val (v3.val + 2^64 * 0) 128 (pos % 64)
+        hd (by omega) (by omega)
+      rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 3 := by omega
+      simp only [hx, huv] at hw
+      simp at hw
+      rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * (0)) := by
+        rw [hVdef]; try ring
+      have h := naf_window_single V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val (0) 192 (pos % 64)
+        hd (by omega) (by omega)
+      rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+  · -- cross-word read
+    rename_i hbge
+    have hbv : 59 ≤ pos % 64 := by
+      have h : ¬ (bidx.val < 59) := by clear * - hbge; scalar_tac
+      omega
+    step as ⟨w, hw⟩
+    step as ⟨i2, hi2⟩
+    step as ⟨i3, hi3⟩
+    step as ⟨w', hw'⟩
+    step as ⟨i5, hi5⟩
+    step as ⟨i6, hi6⟩
+    try simp only [spec_ok]
+    rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega)
+      with hc | hc | hc | hc
+    · have huv : u.val = 0 := by omega
+      have hi3v : i3.val = 1 := by clear * - hi3 huv; omega
+      simp only [hx, huv] at hw
+      simp at hw
+      simp only [hx, hi3v] at hw'
+      simp at hw'
+      rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
+          Nat.shiftRight_eq_div_pow]
+      have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by
+        rw [hVdef]; try simp; try ring
+      have h := naf_window_cross V (0) v0.val (v1.val) (v2.val + 2^64 * (v3.val + 2^64 * 0)) 0 (pos % 64)
+        hd (by norm_num) (by omega) (by omega)
+      rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 1 := by omega
+      have hi3v : i3.val = 2 := by clear * - hi3 huv; omega
+      simp only [hx, huv] at hw
+      simp at hw
+      simp only [hx, hi3v] at hw'
+      simp at hw'
+      rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
+          Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
+        rw [hVdef]; try simp; try ring
+      have h := naf_window_cross V (v0.val) v1.val (v2.val) (v3.val + 2^64 * 0) 64 (pos % 64)
+        hd (by omega) (by omega) (by omega)
+      rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 2 := by omega
+      have hi3v : i3.val = 3 := by clear * - hi3 huv; omega
+      simp only [hx, huv] at hw
+      simp at hw
+      simp only [hx, hi3v] at hw'
+      simp at hw'
+      rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
+          Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * (0))) := by
+        rw [hVdef]; try simp; try ring
+      have h := naf_window_cross V (v0.val + 2^64 * v1.val) v2.val (v3.val) (0) 128 (pos % 64)
+        hd (by omega) (by omega) (by omega)
+      rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+    · have huv : u.val = 3 := by omega
+      have hi3v : i3.val = 4 := by clear * - hi3 huv; omega
+      simp only [hx, huv] at hw
+      simp at hw
+      simp only [hx, hi3v] at hw'
+      simp at hw'
+      rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
+          Nat.shiftRight_eq_div_pow]
+      have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * ((0#u64).val + 2^64 * (0))) := by
+        rw [hVdef]; try simp; try ring
+      have h := naf_window_cross V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val ((0#u64).val) (0) 192 (pos % 64)
+        hd (by omega) (by omega) (by omega)
+      rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h
+      exact h
+
+/-- The odd-digit write: hcast (or hcast + wrapping_sub) produces the digit
+    window − 32·carry′ with carry′ the ≥16 indicator; the digit is odd with
+    |d| < 16, and the entry is written at pos. -/
+theorem naf_update_spec (naf : Std.Array Std.I8 256#usize) (pos : Usize) (window : Std.U64)
+    (hpos : pos.val < 256) (hwle : window.val ≤ 32) (hwodd : window.val % 2 = 1) :
+    (if window < 16#u64
+     then do
+          let i4 ← lift (UScalar.hcast .I8 window)
+          let a ← Array.update naf pos i4
+          ok (a, 0#u64)
+     else
+       do
+       let i4 ← lift (UScalar.hcast .I8 window)
+       let i5 ← lift (UScalar.hcast .I8 32#u64)
+       let i6 ← lift (core.num.I8.wrapping_sub i4 i5)
+       let a ← Array.update naf pos i6
+       ok (a, 1#u64))
+    ⦃ p => ∃ d : Std.I8, (↑p.1 : List Std.I8) = (↑naf : List Std.I8).set pos.val d ∧
+        p.2.val ≤ 1 ∧
+        (d.val : ℤ) = (window.val : ℤ) - 32 * (p.2.val : ℤ) ∧
+        d.val % 2 = 1 ∧ -16 < d.val ∧ d.val < 16 ∧
+        ((window.val < 16 ∧ p.2.val = 0) ∨ (16 ≤ window.val ∧ p.2.val = 1)) ⦄ := by
+  split
+  · rename_i hlt
+    have hltv : window.val < 16 := by clear * - hlt; scalar_tac
+    step with (UScalar.hcast_inBounds_spec .I8 window
+      (by clear * - hltv; scalar_tac)) as ⟨d, hd⟩
+    step as ⟨a, ha⟩
+    try simp only [spec_ok]
+    refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hd], ?_, ?_, ?_,
+      Or.inl ⟨hltv, by simp⟩⟩
+    · rw [hd]; clear * - hwodd; omega
+    · rw [hd]; push_cast; omega
+    · rw [hd]; clear * - hltv; omega
+  · rename_i hge
+    have hgev : 16 ≤ window.val := by clear * - hge; scalar_tac
+    step with (UScalar.hcast_inBounds_spec .I8 window
+      (by clear * - hwle; scalar_tac)) as ⟨d0, hd0⟩
+    step with (UScalar.hcast_inBounds_spec .I8 32#u64
+      (by scalar_tac)) as ⟨t32, ht32⟩
+    step as ⟨d, hd⟩
+    step as ⟨a, ha⟩
+    try simp only [spec_ok]
+    have hdv : (d.val : ℤ) = (window.val : ℤ) - 32 := by
+      rw [hd]
+      simp only [core.num.I8.wrapping_sub_val_eq, hd0, ht32]
+      have hb := Aeneas.Arith.Int.bmod_pow2_eq_of_inBounds' 8 ((window.val : ℤ) - 32)
+        (by norm_num) (by clear * - ; push_cast; omega)
+        (by clear * - hwle; push_cast; omega)
+      push_cast at hb ⊢
+      convert hb using 2 <;> norm_num
+    refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hdv], ?_, ?_, ?_,
+      Or.inr ⟨hgev, by simp⟩⟩
+    · rw [hdv]; clear * - hwodd hgev; omega
+    · rw [hdv]; clear * - hgev hwodd; push_cast; omega
+    · rw [hdv]; clear * - hwle; omega
+
+
+/-! ### The digit loop -/
+
+/-- **The w=5 NAF digit loop**, by induction on the remaining-bits measure.
+    From any state satisfying the invariant, the loop returns a digit array
+    with the NAF digit conditions and exact value V. -/
+theorem naf_digit_loop_spec
+    (x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ)
+    (hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64])
+    (hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))))
+    (hV : V < 2^253) (m : ℕ) :
+    ∀ (naf : Std.Array Std.I8 256#usize) (pos : Usize) (carry : Std.U64),
+    256 - pos.val ≤ m →
+    carry.val ≤ 1 →
+    (carry.val = 1 → pos.val ≤ 254) →
+    (∀ k, pos.val ≤ k → k < 256 → nafDigit naf k = 0) →
+    (∀ k, k < 256 → (nafDigit naf k = 0 ∨ nafDigit naf k % 2 = 1) ∧
+        -16 < nafDigit naf k ∧ nafDigit naf k < 16) →
+    nafSum naf 256 + carry.val * 2^pos.val = ((V % 2^pos.val : ℕ) : ℤ) →
+    scalar.Scalar.non_adjacent_form_loop1 5#usize naf x_u64 32#u64 31#u64 pos carry
+      ⦃ res => NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by
+  induction m with
+  | zero =>
+    intro naf pos carry hm hc hcp hzero hdig hinv
+    unfold scalar.Scalar.non_adjacent_form_loop1
+    apply loop_step
+    simp only [scalar.Scalar.non_adjacent_form_loop1.body]
+    have hguard : ¬ (pos < 256#usize) := by clear * - hm; scalar_tac
+    rw [if_neg hguard]
+    try simp only [spec_ok]
+    exact ⟨hdig, naf_exit V pos.val carry.val _ hV (by clear * - hm; omega) hc hcp hinv⟩
+  | succ m ih =>
+    intro naf pos carry hm hc hcp hzero hdig hinv
+    unfold scalar.Scalar.non_adjacent_form_loop1
+    apply loop_step
+    simp only [scalar.Scalar.non_adjacent_form_loop1.body]
+    by_cases hguard : pos < 256#usize
+    swap
+    · -- exit branch (measure slack)
+      rw [if_neg hguard]
+      try simp only [spec_ok]
+      have hge : 256 ≤ pos.val := by clear * - hguard; scalar_tac
+      exact ⟨hdig, naf_exit V pos.val carry.val _ hV hge hc hcp hinv⟩
+    · rw [if_pos hguard]
+      have hposv : pos.val < 256 := by clear * - hguard; scalar_tac
+      -- u64_idx ← pos / 64 ; bit_idx ← pos % 64 ; i ← 64 − 5
+      step as ⟨u, hu⟩
+      step as ⟨bidx, hbidx⟩
+      step as ⟨i59, hi59⟩
+      have hi59v : i59 = 59#usize := by clear * - hi59; scalar_tac
+      rw [hi59v]
+      -- bit_buf: the 5-bit window of V at pos
+      step with (naf_bitbuf_spec x_u64 v0 v1 v2 v3 V hx hVdef u bidx pos.val
+        hposv hu hbidx) as ⟨buf, hbuf⟩
+      -- i1 ← buf &&& 31 : the masked window
+      step as ⟨msk, hmsk⟩
+      have hmskv : msk.val = (V / 2^pos.val) % 32 := by
+        rw [hmsk, UScalar.val_and]
+        rw [show (31#u64).val = 2^5 - 1 by scalar_tac,
+            Nat.and_two_pow_sub_one_eq_mod]
+        rw [show (2:ℕ)^5 = 32 from by norm_num]
+        exact hbuf
+      -- window ← carry + msk
+      step as ⟨win, hwin⟩
+      have hwinv : win.val = carry.val + (V / 2^pos.val) % 32 := by
+        rw [hwin, hmskv]
+      have hwle : win.val ≤ 32 := by clear * - hwinv hc; omega
+      -- i2 ← win &&& 1 : the parity bit
+      step as ⟨par, hpar⟩
+      have hparv : par.val = win.val % 2 := by
+        rw [hpar, UScalar.val_and]
+        rw [show (1#u64).val = 2^1 - 1 by scalar_tac,
+            Nat.and_two_pow_sub_one_eq_mod]
+        try norm_num
+      split
+      · -- EVEN window: digit 0, pos+1, carry unchanged
+        rename_i hz
+        have heven : (carry.val + (V / 2^pos.val) % 32) % 2 = 0 := by
+          have h : par.val = 0 := by rw [hz]; simp
+          rw [← hwinv, ← hparv]
+          exact h
+        step as ⟨pos1, hpos1⟩
+        have hpos1v : pos1.val = pos.val + 1 := by clear * - hpos1; omega
+        try simp only [spec_ok]
+        apply ih naf pos1 carry (by clear * - hm hpos1v; omega) hc
+          (fun h1 => by have := naf_carry_even V pos.val carry.val hV hc heven h1
+                        clear * - this hpos1v; omega)
+          (fun k hk1 hk2 => hzero k (by clear * - hk1 hpos1v; omega) hk2)
+          hdig
+          (by rw [hpos1v]
+              exact naf_even_step V pos.val carry.val _ hc hinv heven)
+      · -- ODD window: write digit, pos+5, carry from the ≥16 test
+        rename_i hnz
+        have hwodd : win.val % 2 = 1 := by
+          have h : par.val ≠ 0 := by
+            clear * - hnz
+            intro h
+            exact hnz (by scalar_tac)
+          clear * - h hparv
+          omega
+        -- i3 ← 32 / 2 (= 16)
+        step as ⟨h16, hh16⟩
+        have hh16v : h16 = 16#u64 := by clear * - hh16; scalar_tac
+        rw [hh16v]
+        -- the digit write (both branches of the < 16 test)
+        step with (naf_update_spec naf pos win hposv hwle hwodd) as
+          ⟨d, naf1, carry1, hset, hc1, hdval, hdodd, hdlo, hdhi, hcase⟩
+        -- pos1 ← pos + 5
+        step as ⟨pos1, hpos1⟩
+        have hpos1v : pos1.val = pos.val + 5 := by clear * - hpos1; scalar_tac
+        try simp only [spec_ok]
+        -- the digit facts at the written index and away from it
+        have holdz : nafDigit naf pos.val = 0 :=
+          hzero pos.val (le_refl _) hposv
+        have hsum1 : nafSum naf1 256 = nafSum naf 256 + d.val * 2^pos.val :=
+          nafSum_set naf naf1 pos.val d hposv holdz hset
+        have hdig1 : ∀ k, k < 256 → nafDigit naf1 k =
+            if k = pos.val then d.val else nafDigit naf k := by
+          intro k hk
+          by_cases h : k = pos.val
+          · subst h
+            rw [nafDigit_set_eq naf naf1 pos.val d hk hset, if_pos rfl]
+          · rw [nafDigit_set_ne naf naf1 pos.val d hset k hk h, if_neg h]
+        -- the window as a ℕ fact for the step lemmas
+        have hwcase : (carry.val + (V / 2^pos.val) % 32 < 16 ∧ carry1.val = 0) ∨
+            (16 ≤ carry.val + (V / 2^pos.val) % 32 ∧ carry1.val = 1) := by
+          rw [← hwinv]
+          exact hcase
+        apply ih naf1 pos1 carry1 (by clear * - hm hpos1v; omega) hc1
+          (fun h1 => by
+            have := naf_carry_odd V pos.val carry.val carry1.val hV hc hwcase h1
+            clear * - this hpos1v; omega)
+          (fun k hk1 hk2 => by
+            rw [hdig1 k hk2, if_neg (by clear * - hk1 hpos1v hposv; omega)]
+            exact hzero k (by clear * - hk1 hpos1v; omega) hk2)
+          (fun k hk => by
+            rw [hdig1 k hk]
+            by_cases h : k = pos.val
+            · rw [if_pos h]
+              exact ⟨Or.inr hdodd, hdlo, hdhi⟩
+            · rw [if_neg h]
+              exact hdig k hk)
+          (by rw [hpos1v, hsum1]
+              have hd' : (d.val : ℤ) = (carry.val : ℤ) +
+                  ((V / 2^pos.val) % 32 : ℕ) - 32 * carry1.val := by
+                rw [hdval, hwinv]
+                push_cast
+                ring
+              exact naf_odd_step V pos.val carry.val carry1.val _ d.val hinv hd')
+
+
+end CurveFieldProofs

verification/Proofs/DsmNafSpec.lean

@@ -0,0 +1,84 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmNafSpec.lean — NAF campaign, stage 4: the public spec of
+   `Scalar::non_adjacent_form(5)`.
+
+   Composes the proven stages: both entry masserts DISCHARGED (w = 5 is in
+   [2,8]), the LE byte→word load (DsmNafLoadSpec), width = 1<<<5 = 32 and
+   window_mask = 31 computed, and the digit loop (DsmNafLoopSpec) seeded
+   with the all-zeros state whose invariant is trivial.
+
+   POST: the 256 digits satisfy the NAF conditions (odd-or-zero, |d| < 16 —
+   exactly `NafDigits`, what dsm_loop_spec consumes) and their signed sum
+   reconstructs the scalar's little-endian byte value EXACTLY:
+       nafSum res 256 = V   (as integers, no modular slack).
+   Requires V < 2^253 — canonical scalars, which the mul call sites provide.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmNafLoadSpec
+import Proofs.DsmNafLoopSpec
+open Aeneas Aeneas.Std Result ControlFlow
+open curve25519_dalek
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- **Scalar::non_adjacent_form(5)**: for a scalar whose 32-byte LE value V
+    is below 2^253, the result is a 256-entry NAF digit array — every digit
+    odd or zero with |d| < 16, and Σ naf[k]·2^k = V exactly. Both entry
+    masserts are discharged. -/
+theorem non_adjacent_form_spec (self : scalar.Scalar)
+    (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8)
+    (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31])
+    (V : ℕ)
+    (hVbytes : V = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248)
+    (hV : V < 2^253) :
+    scalar.Scalar.non_adjacent_form self 5#usize ⦃ res =>
+      NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by
+  unfold scalar.Scalar.non_adjacent_form
+  step with (massert_spec (5#usize ≥ 2#usize) (by scalar_tac)) as ⟨h2⟩
+  step with (massert_spec (5#usize ≤ 8#usize) (by scalar_tac)) as ⟨h8⟩
+  -- the LE load fills x_u64[0..3]; word 4 stays 0
+  step with (naf_load_spec self (Array.repeat 5#usize 0#u64)
+    b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31
+    hb (by simp [List.replicate])) as ⟨v0, v1, v2, v3, ws, hws, hv0, hv1, hv2, hv3⟩
+  -- width ← 1 <<< 5 (= 32), window_mask ← width − 1 (= 31)
+  step as ⟨wd, hwd⟩
+  have hwdv : wd = 32#u64 := by clear * - hwd; scalar_tac
+  rw [hwdv]
+  step as ⟨mk, hmk⟩
+  have hmkv : mk = 31#u64 := by clear * - hmk; scalar_tac
+  rw [hmkv]
+  -- the initial all-zeros digit state
+  have hz : ∀ k, k < 256 → nafDigit (Array.repeat 256#usize 0#i8) k = 0 := by
+    intro k hk
+    unfold nafDigit
+    rw [getElem!_pos (↑(Array.repeat 256#usize 0#i8) : List Std.I8) k
+        (by simp; omega)]
+    simp only [Array.repeat_val, List.getElem_replicate]
+    simp
+  have hsum0 : nafSum (Array.repeat 256#usize 0#i8) 256 = 0 := by
+    unfold nafSum
+    apply Finset.sum_eq_zero
+    intro k hk
+    rw [hz k (Finset.mem_range.mp hk)]
+    ring
+  -- the word-form value
+  have hVw : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
+    rw [hVbytes, hv0, hv1, hv2, hv3]
+    ring
+  -- the digit loop from the trivial invariant
+  apply naf_digit_loop_spec ws v0 v1 v2 v3 V hws hVw hV 256
+    (Array.repeat 256#usize 0#i8) 0#usize 0#u64
+    (by scalar_tac)
+    (by scalar_tac)
+    (by intro h; simp at h)
+    (fun k _ hk => hz k hk)
+    (fun k hk => ⟨Or.inl (hz k hk), by rw [hz k hk]; norm_num,
+                  by rw [hz k hk]; norm_num⟩)
+    (by simp [hsum0])
+
+end CurveFieldProofs

verification/check.sh

@@ -57,6 +57,9 @@ PROOFS=(
   DsmLoopSpec
   DsmNafLoadSpec
   DsmNafMath
+  DsmNafLoopSpec
+  DsmNafSpec
+  DsmMulSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
@@ -71,6 +74,10 @@ CERTS=(
   CurveFieldProofs.dsm_loop_spec
   CurveFieldProofs.naf_load_spec
   CurveFieldProofs.naf_exit
+  CurveFieldProofs.naf_digit_loop_spec
+  CurveFieldProofs.non_adjacent_form_spec
+  CurveFieldProofs.run_basepoint
+  CurveFieldProofs.vartime_double_base_mul_spec
 )
 # Imports needed so every certificate in CERTS is in scope for the audit.
 AUDIT_IMPORTS=(
@@ -81,6 +88,8 @@ AUDIT_IMPORTS=(
   Proofs.DsmLoopSpec
   Proofs.DsmNafLoadSpec
   Proofs.DsmNafMath
+  Proofs.DsmNafSpec
+  Proofs.DsmMulSpec
 )
 
 # ── Phase 0: resource + integrity guards ────────────────────────────────────

verification/gen/CurveField/FunsExternal.lean

@@ -340,14 +340,6 @@ axiom
 axiom backend.serial.scalar_mul.variable_base.mul
   : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
 
-/-- [curve25519_dalek::backend::serial::scalar_mul::vartime_double_base::mul]:
-    Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1
-    Visibility: public -/
-axiom backend.serial.scalar_mul.vartime_double_base.mul
-  :
-  scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
-    edwards.EdwardsPoint
-
 /-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx2::mul]:
     Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2
     Visibility: public -/