diff --git a/verification/Proofs/DsmMulSpec.lean b/verification/Proofs/DsmMulSpec.lean
new file mode 100644
index 0000000..3506152
--- /dev/null
+++ b/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
+
+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
diff --git a/verification/Proofs/DsmNafLoadSpec.lean b/verification/Proofs/DsmNafLoadSpec.lean
new file mode 100644
index 0000000..1db9e62
--- /dev/null
+++ b/verification/Proofs/DsmNafLoadSpec.lean
@@ -0,0 +1,1473 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmNafLoadSpec.lean — NAF campaign, stage 1: the little-endian
+   byte→word load of `non_adjacent_form` (scalar.rs: read_le_u64_into
+   refactored to the nested index loop for extraction).
+
+   Four inner walks (one per word: t |= bytes[8k+bi] << 8bi, bi = 0..7) and
+   the outer 4-peel filling x_u64[0..3]; x_u64[4] stays 0 — the pad word the
+   digit loop's cross-word window reads at positions ≥ 251.
+
+   GENERATED by dsm_naf_load_gen.py — proven fbw idioms: or-accumulation via
+   Nat.two_pow_add_eq_or_of_lt with the explicit calc bridge (default simp
+   literalizes 2^8; simp only keeps pow form), hypothesis-side index
+   evaluation, minimal-context value haves.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmTableSpec
+open Aeneas Aeneas.Std Result ControlFlow
+open curve25519
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- Inner LE-load loop for word 0: t accumulates bytes 0..7
+    little-endian. The scalar struct passes through unchanged. -/
+theorem naf_word_loop_spec_0 (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]) :
+    scalar.Scalar.non_adjacent_form_loop0_loop0 self 0#usize 0#u64 0#usize
+      ⦃ p => p.1 = self ∧ p.2.val = 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 ⦄ := by
+  have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
+  have hbb0 : b0.val < 2^8 := by scalar_tac
+  have hbb1 : b1.val < 2^8 := by scalar_tac
+  have hbb2 : b2.val < 2^8 := by scalar_tac
+  have hbb3 : b3.val < 2^8 := by scalar_tac
+  have hbb4 : b4.val < 2^8 := by scalar_tac
+  have hbb5 : b5.val < 2^8 := by scalar_tac
+  have hbb6 : b6.val < 2^8 := by scalar_tac
+  have hbb7 : b7.val < 2^8 := by scalar_tac
+  unfold scalar.Scalar.non_adjacent_form_loop0_loop0
+  -- bi = 0: byte 0
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (0#usize < 8#usize) by scalar_tac)]
+  step as ⟨i0, hi0⟩
+  have hi0v : i0 = 0#usize := by clear * - hi0; scalar_tac
+  rw [hi0v]
+  step as ⟨i10, hi10⟩
+  have hi10v : i10 = 0#usize := by clear * - hi10; scalar_tac
+  rw [hi10v]
+  step as ⟨x0, hx0⟩
+  simp [hb] at hx0
+  step with UScalar.cast.step_spec as ⟨c0, hc0⟩
+  have hc0v : c0.val = b0.val := by
+    rw [hc0, UScalar.cast_val_eq, hx0]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s0, hsh0⟩
+  have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac
+  step as ⟨t0, ht0⟩
+  have ht0v : t0.val = b0.val * 2^0 := by
+    rw [ht0]
+    simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y0, hy0⟩
+  have hy0v : y0.val = b0.val := by
+    simp [hy0, UScalar.val_or, ht0v]
+  step as ⟨bi0, hbi0⟩
+  have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac
+  rw [hbi0v]
+  try simp only [spec_ok]
+  -- bi = 1: byte 1
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (1#usize < 8#usize) by scalar_tac)]
+  step as ⟨i1, hi1⟩
+  have hi1v : i1 = 0#usize := by clear * - hi1; scalar_tac
+  rw [hi1v]
+  step as ⟨i11, hi11⟩
+  have hi11v : i11 = 1#usize := by clear * - hi11; scalar_tac
+  rw [hi11v]
+  step as ⟨x1, hx1⟩
+  simp [hb] at hx1
+  step with UScalar.cast.step_spec as ⟨c1, hc1⟩
+  have hc1v : c1.val = b1.val := by
+    rw [hc1, UScalar.cast_val_eq, hx1]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s1, hsh1⟩
+  have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac
+  step as ⟨t1, ht1⟩
+  have ht1v : t1.val = b1.val * 2^8 := by
+    rw [ht1]
+    simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y1, hy1⟩
+  have hy1v : y1.val = b0.val + b1.val * 2^8 := by
+    have hult : y0.val < 2^8 := by rw [hy0v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b1.val
+    have hadd : y0.val ||| b1.val * 2^8 = y0.val + b1.val * 2^8 := by
+      calc y0.val ||| b1.val * 2^8
+          = y0.val ||| 2^8 * b1.val := by rw [Nat.mul_comm]
+        _ = 2^8 * b1.val ||| y0.val := Nat.lor_comm _ _
+        _ = 2^8 * b1.val + y0.val := hor.symm
+        _ = y0.val + b1.val * 2^8 := by ring
+    simp only [hy1, UScalar.val_or, ht1v]
+    rw [hadd, hy0v]
+    try ring
+  step as ⟨bi1, hbi1⟩
+  have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac
+  rw [hbi1v]
+  try simp only [spec_ok]
+  -- bi = 2: byte 2
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (2#usize < 8#usize) by scalar_tac)]
+  step as ⟨i2, hi2⟩
+  have hi2v : i2 = 0#usize := by clear * - hi2; scalar_tac
+  rw [hi2v]
+  step as ⟨i12, hi12⟩
+  have hi12v : i12 = 2#usize := by clear * - hi12; scalar_tac
+  rw [hi12v]
+  step as ⟨x2, hx2⟩
+  simp [hb] at hx2
+  step with UScalar.cast.step_spec as ⟨c2, hc2⟩
+  have hc2v : c2.val = b2.val := by
+    rw [hc2, UScalar.cast_val_eq, hx2]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s2, hsh2⟩
+  have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac
+  step as ⟨t2, ht2⟩
+  have ht2v : t2.val = b2.val * 2^16 := by
+    rw [ht2]
+    simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y2, hy2⟩
+  have hy2v : y2.val = b0.val + b1.val * 2^8 + b2.val * 2^16 := by
+    have hult : y1.val < 2^16 := by rw [hy1v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b2.val
+    have hadd : y1.val ||| b2.val * 2^16 = y1.val + b2.val * 2^16 := by
+      calc y1.val ||| b2.val * 2^16
+          = y1.val ||| 2^16 * b2.val := by rw [Nat.mul_comm]
+        _ = 2^16 * b2.val ||| y1.val := Nat.lor_comm _ _
+        _ = 2^16 * b2.val + y1.val := hor.symm
+        _ = y1.val + b2.val * 2^16 := by ring
+    simp only [hy2, UScalar.val_or, ht2v]
+    rw [hadd, hy1v]
+    try ring
+  step as ⟨bi2, hbi2⟩
+  have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac
+  rw [hbi2v]
+  try simp only [spec_ok]
+  -- bi = 3: byte 3
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (3#usize < 8#usize) by scalar_tac)]
+  step as ⟨i3, hi3⟩
+  have hi3v : i3 = 0#usize := by clear * - hi3; scalar_tac
+  rw [hi3v]
+  step as ⟨i13, hi13⟩
+  have hi13v : i13 = 3#usize := by clear * - hi13; scalar_tac
+  rw [hi13v]
+  step as ⟨x3, hx3⟩
+  simp [hb] at hx3
+  step with UScalar.cast.step_spec as ⟨c3, hc3⟩
+  have hc3v : c3.val = b3.val := by
+    rw [hc3, UScalar.cast_val_eq, hx3]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s3, hsh3⟩
+  have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac
+  step as ⟨t3, ht3⟩
+  have ht3v : t3.val = b3.val * 2^24 := by
+    rw [ht3]
+    simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y3, hy3⟩
+  have hy3v : y3.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 := by
+    have hult : y2.val < 2^24 := by rw [hy2v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b3.val
+    have hadd : y2.val ||| b3.val * 2^24 = y2.val + b3.val * 2^24 := by
+      calc y2.val ||| b3.val * 2^24
+          = y2.val ||| 2^24 * b3.val := by rw [Nat.mul_comm]
+        _ = 2^24 * b3.val ||| y2.val := Nat.lor_comm _ _
+        _ = 2^24 * b3.val + y2.val := hor.symm
+        _ = y2.val + b3.val * 2^24 := by ring
+    simp only [hy3, UScalar.val_or, ht3v]
+    rw [hadd, hy2v]
+    try ring
+  step as ⟨bi3, hbi3⟩
+  have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac
+  rw [hbi3v]
+  try simp only [spec_ok]
+  -- bi = 4: byte 4
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (4#usize < 8#usize) by scalar_tac)]
+  step as ⟨i4, hi4⟩
+  have hi4v : i4 = 0#usize := by clear * - hi4; scalar_tac
+  rw [hi4v]
+  step as ⟨i14, hi14⟩
+  have hi14v : i14 = 4#usize := by clear * - hi14; scalar_tac
+  rw [hi14v]
+  step as ⟨x4, hx4⟩
+  simp [hb] at hx4
+  step with UScalar.cast.step_spec as ⟨c4, hc4⟩
+  have hc4v : c4.val = b4.val := by
+    rw [hc4, UScalar.cast_val_eq, hx4]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s4, hsh4⟩
+  have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac
+  step as ⟨t4, ht4⟩
+  have ht4v : t4.val = b4.val * 2^32 := by
+    rw [ht4]
+    simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y4, hy4⟩
+  have hy4v : y4.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 := by
+    have hult : y3.val < 2^32 := by rw [hy3v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b4.val
+    have hadd : y3.val ||| b4.val * 2^32 = y3.val + b4.val * 2^32 := by
+      calc y3.val ||| b4.val * 2^32
+          = y3.val ||| 2^32 * b4.val := by rw [Nat.mul_comm]
+        _ = 2^32 * b4.val ||| y3.val := Nat.lor_comm _ _
+        _ = 2^32 * b4.val + y3.val := hor.symm
+        _ = y3.val + b4.val * 2^32 := by ring
+    simp only [hy4, UScalar.val_or, ht4v]
+    rw [hadd, hy3v]
+    try ring
+  step as ⟨bi4, hbi4⟩
+  have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac
+  rw [hbi4v]
+  try simp only [spec_ok]
+  -- bi = 5: byte 5
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (5#usize < 8#usize) by scalar_tac)]
+  step as ⟨i5, hi5⟩
+  have hi5v : i5 = 0#usize := by clear * - hi5; scalar_tac
+  rw [hi5v]
+  step as ⟨i15, hi15⟩
+  have hi15v : i15 = 5#usize := by clear * - hi15; scalar_tac
+  rw [hi15v]
+  step as ⟨x5, hx5⟩
+  simp [hb] at hx5
+  step with UScalar.cast.step_spec as ⟨c5, hc5⟩
+  have hc5v : c5.val = b5.val := by
+    rw [hc5, UScalar.cast_val_eq, hx5]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s5, hsh5⟩
+  have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac
+  step as ⟨t5, ht5⟩
+  have ht5v : t5.val = b5.val * 2^40 := by
+    rw [ht5]
+    simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y5, hy5⟩
+  have hy5v : y5.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 := by
+    have hult : y4.val < 2^40 := by rw [hy4v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b5.val
+    have hadd : y4.val ||| b5.val * 2^40 = y4.val + b5.val * 2^40 := by
+      calc y4.val ||| b5.val * 2^40
+          = y4.val ||| 2^40 * b5.val := by rw [Nat.mul_comm]
+        _ = 2^40 * b5.val ||| y4.val := Nat.lor_comm _ _
+        _ = 2^40 * b5.val + y4.val := hor.symm
+        _ = y4.val + b5.val * 2^40 := by ring
+    simp only [hy5, UScalar.val_or, ht5v]
+    rw [hadd, hy4v]
+    try ring
+  step as ⟨bi5, hbi5⟩
+  have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac
+  rw [hbi5v]
+  try simp only [spec_ok]
+  -- bi = 6: byte 6
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (6#usize < 8#usize) by scalar_tac)]
+  step as ⟨i6, hi6⟩
+  have hi6v : i6 = 0#usize := by clear * - hi6; scalar_tac
+  rw [hi6v]
+  step as ⟨i16, hi16⟩
+  have hi16v : i16 = 6#usize := by clear * - hi16; scalar_tac
+  rw [hi16v]
+  step as ⟨x6, hx6⟩
+  simp [hb] at hx6
+  step with UScalar.cast.step_spec as ⟨c6, hc6⟩
+  have hc6v : c6.val = b6.val := by
+    rw [hc6, UScalar.cast_val_eq, hx6]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s6, hsh6⟩
+  have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac
+  step as ⟨t6, ht6⟩
+  have ht6v : t6.val = b6.val * 2^48 := by
+    rw [ht6]
+    simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y6, hy6⟩
+  have hy6v : y6.val = 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 := by
+    have hult : y5.val < 2^48 := by rw [hy5v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b6.val
+    have hadd : y5.val ||| b6.val * 2^48 = y5.val + b6.val * 2^48 := by
+      calc y5.val ||| b6.val * 2^48
+          = y5.val ||| 2^48 * b6.val := by rw [Nat.mul_comm]
+        _ = 2^48 * b6.val ||| y5.val := Nat.lor_comm _ _
+        _ = 2^48 * b6.val + y5.val := hor.symm
+        _ = y5.val + b6.val * 2^48 := by ring
+    simp only [hy6, UScalar.val_or, ht6v]
+    rw [hadd, hy5v]
+    try ring
+  step as ⟨bi6, hbi6⟩
+  have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac
+  rw [hbi6v]
+  try simp only [spec_ok]
+  -- bi = 7: byte 7
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (7#usize < 8#usize) by scalar_tac)]
+  step as ⟨i7, hi7⟩
+  have hi7v : i7 = 0#usize := by clear * - hi7; scalar_tac
+  rw [hi7v]
+  step as ⟨i17, hi17⟩
+  have hi17v : i17 = 7#usize := by clear * - hi17; scalar_tac
+  rw [hi17v]
+  step as ⟨x7, hx7⟩
+  simp [hb] at hx7
+  step with UScalar.cast.step_spec as ⟨c7, hc7⟩
+  have hc7v : c7.val = b7.val := by
+    rw [hc7, UScalar.cast_val_eq, hx7]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s7, hsh7⟩
+  have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac
+  step as ⟨t7, ht7⟩
+  have ht7v : t7.val = b7.val * 2^56 := by
+    rw [ht7]
+    simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y7, hy7⟩
+  have hy7v : y7.val = 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 := by
+    have hult : y6.val < 2^56 := by rw [hy6v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b7.val
+    have hadd : y6.val ||| b7.val * 2^56 = y6.val + b7.val * 2^56 := by
+      calc y6.val ||| b7.val * 2^56
+          = y6.val ||| 2^56 * b7.val := by rw [Nat.mul_comm]
+        _ = 2^56 * b7.val ||| y6.val := Nat.lor_comm _ _
+        _ = 2^56 * b7.val + y6.val := hor.symm
+        _ = y6.val + b7.val * 2^56 := by ring
+    simp only [hy7, UScalar.val_or, ht7v]
+    rw [hadd, hy6v]
+    try ring
+  step as ⟨bi7, hbi7⟩
+  have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac
+  rw [hbi7v]
+  try simp only [spec_ok]
+  -- exit: bi = 8, done (self, t)
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)]
+  try simp only [spec_ok]
+  exact ⟨True.intro, hy7v⟩
+
+/-- Inner LE-load loop for word 1: t accumulates bytes 8..15
+    little-endian. The scalar struct passes through unchanged. -/
+theorem naf_word_loop_spec_1 (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]) :
+    scalar.Scalar.non_adjacent_form_loop0_loop0 self 1#usize 0#u64 0#usize
+      ⦃ p => p.1 = self ∧ p.2.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 ⦄ := by
+  have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
+  have hbb8 : b8.val < 2^8 := by scalar_tac
+  have hbb9 : b9.val < 2^8 := by scalar_tac
+  have hbb10 : b10.val < 2^8 := by scalar_tac
+  have hbb11 : b11.val < 2^8 := by scalar_tac
+  have hbb12 : b12.val < 2^8 := by scalar_tac
+  have hbb13 : b13.val < 2^8 := by scalar_tac
+  have hbb14 : b14.val < 2^8 := by scalar_tac
+  have hbb15 : b15.val < 2^8 := by scalar_tac
+  unfold scalar.Scalar.non_adjacent_form_loop0_loop0
+  -- bi = 0: byte 8
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (0#usize < 8#usize) by scalar_tac)]
+  step as ⟨i0, hi0⟩
+  have hi0v : i0 = 8#usize := by clear * - hi0; scalar_tac
+  rw [hi0v]
+  step as ⟨i10, hi10⟩
+  have hi10v : i10 = 8#usize := by clear * - hi10; scalar_tac
+  rw [hi10v]
+  step as ⟨x0, hx0⟩
+  simp [hb] at hx0
+  step with UScalar.cast.step_spec as ⟨c0, hc0⟩
+  have hc0v : c0.val = b8.val := by
+    rw [hc0, UScalar.cast_val_eq, hx0]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s0, hsh0⟩
+  have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac
+  step as ⟨t0, ht0⟩
+  have ht0v : t0.val = b8.val * 2^0 := by
+    rw [ht0]
+    simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y0, hy0⟩
+  have hy0v : y0.val = b8.val := by
+    simp [hy0, UScalar.val_or, ht0v]
+  step as ⟨bi0, hbi0⟩
+  have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac
+  rw [hbi0v]
+  try simp only [spec_ok]
+  -- bi = 1: byte 9
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (1#usize < 8#usize) by scalar_tac)]
+  step as ⟨i1, hi1⟩
+  have hi1v : i1 = 8#usize := by clear * - hi1; scalar_tac
+  rw [hi1v]
+  step as ⟨i11, hi11⟩
+  have hi11v : i11 = 9#usize := by clear * - hi11; scalar_tac
+  rw [hi11v]
+  step as ⟨x1, hx1⟩
+  simp [hb] at hx1
+  step with UScalar.cast.step_spec as ⟨c1, hc1⟩
+  have hc1v : c1.val = b9.val := by
+    rw [hc1, UScalar.cast_val_eq, hx1]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s1, hsh1⟩
+  have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac
+  step as ⟨t1, ht1⟩
+  have ht1v : t1.val = b9.val * 2^8 := by
+    rw [ht1]
+    simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y1, hy1⟩
+  have hy1v : y1.val = b8.val + b9.val * 2^8 := by
+    have hult : y0.val < 2^8 := by rw [hy0v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b9.val
+    have hadd : y0.val ||| b9.val * 2^8 = y0.val + b9.val * 2^8 := by
+      calc y0.val ||| b9.val * 2^8
+          = y0.val ||| 2^8 * b9.val := by rw [Nat.mul_comm]
+        _ = 2^8 * b9.val ||| y0.val := Nat.lor_comm _ _
+        _ = 2^8 * b9.val + y0.val := hor.symm
+        _ = y0.val + b9.val * 2^8 := by ring
+    simp only [hy1, UScalar.val_or, ht1v]
+    rw [hadd, hy0v]
+    try ring
+  step as ⟨bi1, hbi1⟩
+  have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac
+  rw [hbi1v]
+  try simp only [spec_ok]
+  -- bi = 2: byte 10
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (2#usize < 8#usize) by scalar_tac)]
+  step as ⟨i2, hi2⟩
+  have hi2v : i2 = 8#usize := by clear * - hi2; scalar_tac
+  rw [hi2v]
+  step as ⟨i12, hi12⟩
+  have hi12v : i12 = 10#usize := by clear * - hi12; scalar_tac
+  rw [hi12v]
+  step as ⟨x2, hx2⟩
+  simp [hb] at hx2
+  step with UScalar.cast.step_spec as ⟨c2, hc2⟩
+  have hc2v : c2.val = b10.val := by
+    rw [hc2, UScalar.cast_val_eq, hx2]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s2, hsh2⟩
+  have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac
+  step as ⟨t2, ht2⟩
+  have ht2v : t2.val = b10.val * 2^16 := by
+    rw [ht2]
+    simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y2, hy2⟩
+  have hy2v : y2.val = b8.val + b9.val * 2^8 + b10.val * 2^16 := by
+    have hult : y1.val < 2^16 := by rw [hy1v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b10.val
+    have hadd : y1.val ||| b10.val * 2^16 = y1.val + b10.val * 2^16 := by
+      calc y1.val ||| b10.val * 2^16
+          = y1.val ||| 2^16 * b10.val := by rw [Nat.mul_comm]
+        _ = 2^16 * b10.val ||| y1.val := Nat.lor_comm _ _
+        _ = 2^16 * b10.val + y1.val := hor.symm
+        _ = y1.val + b10.val * 2^16 := by ring
+    simp only [hy2, UScalar.val_or, ht2v]
+    rw [hadd, hy1v]
+    try ring
+  step as ⟨bi2, hbi2⟩
+  have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac
+  rw [hbi2v]
+  try simp only [spec_ok]
+  -- bi = 3: byte 11
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (3#usize < 8#usize) by scalar_tac)]
+  step as ⟨i3, hi3⟩
+  have hi3v : i3 = 8#usize := by clear * - hi3; scalar_tac
+  rw [hi3v]
+  step as ⟨i13, hi13⟩
+  have hi13v : i13 = 11#usize := by clear * - hi13; scalar_tac
+  rw [hi13v]
+  step as ⟨x3, hx3⟩
+  simp [hb] at hx3
+  step with UScalar.cast.step_spec as ⟨c3, hc3⟩
+  have hc3v : c3.val = b11.val := by
+    rw [hc3, UScalar.cast_val_eq, hx3]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s3, hsh3⟩
+  have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac
+  step as ⟨t3, ht3⟩
+  have ht3v : t3.val = b11.val * 2^24 := by
+    rw [ht3]
+    simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y3, hy3⟩
+  have hy3v : y3.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 := by
+    have hult : y2.val < 2^24 := by rw [hy2v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b11.val
+    have hadd : y2.val ||| b11.val * 2^24 = y2.val + b11.val * 2^24 := by
+      calc y2.val ||| b11.val * 2^24
+          = y2.val ||| 2^24 * b11.val := by rw [Nat.mul_comm]
+        _ = 2^24 * b11.val ||| y2.val := Nat.lor_comm _ _
+        _ = 2^24 * b11.val + y2.val := hor.symm
+        _ = y2.val + b11.val * 2^24 := by ring
+    simp only [hy3, UScalar.val_or, ht3v]
+    rw [hadd, hy2v]
+    try ring
+  step as ⟨bi3, hbi3⟩
+  have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac
+  rw [hbi3v]
+  try simp only [spec_ok]
+  -- bi = 4: byte 12
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (4#usize < 8#usize) by scalar_tac)]
+  step as ⟨i4, hi4⟩
+  have hi4v : i4 = 8#usize := by clear * - hi4; scalar_tac
+  rw [hi4v]
+  step as ⟨i14, hi14⟩
+  have hi14v : i14 = 12#usize := by clear * - hi14; scalar_tac
+  rw [hi14v]
+  step as ⟨x4, hx4⟩
+  simp [hb] at hx4
+  step with UScalar.cast.step_spec as ⟨c4, hc4⟩
+  have hc4v : c4.val = b12.val := by
+    rw [hc4, UScalar.cast_val_eq, hx4]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s4, hsh4⟩
+  have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac
+  step as ⟨t4, ht4⟩
+  have ht4v : t4.val = b12.val * 2^32 := by
+    rw [ht4]
+    simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y4, hy4⟩
+  have hy4v : y4.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 := by
+    have hult : y3.val < 2^32 := by rw [hy3v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b12.val
+    have hadd : y3.val ||| b12.val * 2^32 = y3.val + b12.val * 2^32 := by
+      calc y3.val ||| b12.val * 2^32
+          = y3.val ||| 2^32 * b12.val := by rw [Nat.mul_comm]
+        _ = 2^32 * b12.val ||| y3.val := Nat.lor_comm _ _
+        _ = 2^32 * b12.val + y3.val := hor.symm
+        _ = y3.val + b12.val * 2^32 := by ring
+    simp only [hy4, UScalar.val_or, ht4v]
+    rw [hadd, hy3v]
+    try ring
+  step as ⟨bi4, hbi4⟩
+  have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac
+  rw [hbi4v]
+  try simp only [spec_ok]
+  -- bi = 5: byte 13
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (5#usize < 8#usize) by scalar_tac)]
+  step as ⟨i5, hi5⟩
+  have hi5v : i5 = 8#usize := by clear * - hi5; scalar_tac
+  rw [hi5v]
+  step as ⟨i15, hi15⟩
+  have hi15v : i15 = 13#usize := by clear * - hi15; scalar_tac
+  rw [hi15v]
+  step as ⟨x5, hx5⟩
+  simp [hb] at hx5
+  step with UScalar.cast.step_spec as ⟨c5, hc5⟩
+  have hc5v : c5.val = b13.val := by
+    rw [hc5, UScalar.cast_val_eq, hx5]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s5, hsh5⟩
+  have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac
+  step as ⟨t5, ht5⟩
+  have ht5v : t5.val = b13.val * 2^40 := by
+    rw [ht5]
+    simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y5, hy5⟩
+  have hy5v : y5.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 := by
+    have hult : y4.val < 2^40 := by rw [hy4v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b13.val
+    have hadd : y4.val ||| b13.val * 2^40 = y4.val + b13.val * 2^40 := by
+      calc y4.val ||| b13.val * 2^40
+          = y4.val ||| 2^40 * b13.val := by rw [Nat.mul_comm]
+        _ = 2^40 * b13.val ||| y4.val := Nat.lor_comm _ _
+        _ = 2^40 * b13.val + y4.val := hor.symm
+        _ = y4.val + b13.val * 2^40 := by ring
+    simp only [hy5, UScalar.val_or, ht5v]
+    rw [hadd, hy4v]
+    try ring
+  step as ⟨bi5, hbi5⟩
+  have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac
+  rw [hbi5v]
+  try simp only [spec_ok]
+  -- bi = 6: byte 14
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (6#usize < 8#usize) by scalar_tac)]
+  step as ⟨i6, hi6⟩
+  have hi6v : i6 = 8#usize := by clear * - hi6; scalar_tac
+  rw [hi6v]
+  step as ⟨i16, hi16⟩
+  have hi16v : i16 = 14#usize := by clear * - hi16; scalar_tac
+  rw [hi16v]
+  step as ⟨x6, hx6⟩
+  simp [hb] at hx6
+  step with UScalar.cast.step_spec as ⟨c6, hc6⟩
+  have hc6v : c6.val = b14.val := by
+    rw [hc6, UScalar.cast_val_eq, hx6]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s6, hsh6⟩
+  have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac
+  step as ⟨t6, ht6⟩
+  have ht6v : t6.val = b14.val * 2^48 := by
+    rw [ht6]
+    simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y6, hy6⟩
+  have hy6v : y6.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 := by
+    have hult : y5.val < 2^48 := by rw [hy5v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b14.val
+    have hadd : y5.val ||| b14.val * 2^48 = y5.val + b14.val * 2^48 := by
+      calc y5.val ||| b14.val * 2^48
+          = y5.val ||| 2^48 * b14.val := by rw [Nat.mul_comm]
+        _ = 2^48 * b14.val ||| y5.val := Nat.lor_comm _ _
+        _ = 2^48 * b14.val + y5.val := hor.symm
+        _ = y5.val + b14.val * 2^48 := by ring
+    simp only [hy6, UScalar.val_or, ht6v]
+    rw [hadd, hy5v]
+    try ring
+  step as ⟨bi6, hbi6⟩
+  have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac
+  rw [hbi6v]
+  try simp only [spec_ok]
+  -- bi = 7: byte 15
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (7#usize < 8#usize) by scalar_tac)]
+  step as ⟨i7, hi7⟩
+  have hi7v : i7 = 8#usize := by clear * - hi7; scalar_tac
+  rw [hi7v]
+  step as ⟨i17, hi17⟩
+  have hi17v : i17 = 15#usize := by clear * - hi17; scalar_tac
+  rw [hi17v]
+  step as ⟨x7, hx7⟩
+  simp [hb] at hx7
+  step with UScalar.cast.step_spec as ⟨c7, hc7⟩
+  have hc7v : c7.val = b15.val := by
+    rw [hc7, UScalar.cast_val_eq, hx7]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s7, hsh7⟩
+  have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac
+  step as ⟨t7, ht7⟩
+  have ht7v : t7.val = b15.val * 2^56 := by
+    rw [ht7]
+    simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y7, hy7⟩
+  have hy7v : y7.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 := by
+    have hult : y6.val < 2^56 := by rw [hy6v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b15.val
+    have hadd : y6.val ||| b15.val * 2^56 = y6.val + b15.val * 2^56 := by
+      calc y6.val ||| b15.val * 2^56
+          = y6.val ||| 2^56 * b15.val := by rw [Nat.mul_comm]
+        _ = 2^56 * b15.val ||| y6.val := Nat.lor_comm _ _
+        _ = 2^56 * b15.val + y6.val := hor.symm
+        _ = y6.val + b15.val * 2^56 := by ring
+    simp only [hy7, UScalar.val_or, ht7v]
+    rw [hadd, hy6v]
+    try ring
+  step as ⟨bi7, hbi7⟩
+  have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac
+  rw [hbi7v]
+  try simp only [spec_ok]
+  -- exit: bi = 8, done (self, t)
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)]
+  try simp only [spec_ok]
+  exact ⟨True.intro, hy7v⟩
+
+/-- Inner LE-load loop for word 2: t accumulates bytes 16..23
+    little-endian. The scalar struct passes through unchanged. -/
+theorem naf_word_loop_spec_2 (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]) :
+    scalar.Scalar.non_adjacent_form_loop0_loop0 self 2#usize 0#u64 0#usize
+      ⦃ p => p.1 = self ∧ p.2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 ⦄ := by
+  have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
+  have hbb16 : b16.val < 2^8 := by scalar_tac
+  have hbb17 : b17.val < 2^8 := by scalar_tac
+  have hbb18 : b18.val < 2^8 := by scalar_tac
+  have hbb19 : b19.val < 2^8 := by scalar_tac
+  have hbb20 : b20.val < 2^8 := by scalar_tac
+  have hbb21 : b21.val < 2^8 := by scalar_tac
+  have hbb22 : b22.val < 2^8 := by scalar_tac
+  have hbb23 : b23.val < 2^8 := by scalar_tac
+  unfold scalar.Scalar.non_adjacent_form_loop0_loop0
+  -- bi = 0: byte 16
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (0#usize < 8#usize) by scalar_tac)]
+  step as ⟨i0, hi0⟩
+  have hi0v : i0 = 16#usize := by clear * - hi0; scalar_tac
+  rw [hi0v]
+  step as ⟨i10, hi10⟩
+  have hi10v : i10 = 16#usize := by clear * - hi10; scalar_tac
+  rw [hi10v]
+  step as ⟨x0, hx0⟩
+  simp [hb] at hx0
+  step with UScalar.cast.step_spec as ⟨c0, hc0⟩
+  have hc0v : c0.val = b16.val := by
+    rw [hc0, UScalar.cast_val_eq, hx0]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s0, hsh0⟩
+  have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac
+  step as ⟨t0, ht0⟩
+  have ht0v : t0.val = b16.val * 2^0 := by
+    rw [ht0]
+    simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y0, hy0⟩
+  have hy0v : y0.val = b16.val := by
+    simp [hy0, UScalar.val_or, ht0v]
+  step as ⟨bi0, hbi0⟩
+  have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac
+  rw [hbi0v]
+  try simp only [spec_ok]
+  -- bi = 1: byte 17
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (1#usize < 8#usize) by scalar_tac)]
+  step as ⟨i1, hi1⟩
+  have hi1v : i1 = 16#usize := by clear * - hi1; scalar_tac
+  rw [hi1v]
+  step as ⟨i11, hi11⟩
+  have hi11v : i11 = 17#usize := by clear * - hi11; scalar_tac
+  rw [hi11v]
+  step as ⟨x1, hx1⟩
+  simp [hb] at hx1
+  step with UScalar.cast.step_spec as ⟨c1, hc1⟩
+  have hc1v : c1.val = b17.val := by
+    rw [hc1, UScalar.cast_val_eq, hx1]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s1, hsh1⟩
+  have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac
+  step as ⟨t1, ht1⟩
+  have ht1v : t1.val = b17.val * 2^8 := by
+    rw [ht1]
+    simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y1, hy1⟩
+  have hy1v : y1.val = b16.val + b17.val * 2^8 := by
+    have hult : y0.val < 2^8 := by rw [hy0v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b17.val
+    have hadd : y0.val ||| b17.val * 2^8 = y0.val + b17.val * 2^8 := by
+      calc y0.val ||| b17.val * 2^8
+          = y0.val ||| 2^8 * b17.val := by rw [Nat.mul_comm]
+        _ = 2^8 * b17.val ||| y0.val := Nat.lor_comm _ _
+        _ = 2^8 * b17.val + y0.val := hor.symm
+        _ = y0.val + b17.val * 2^8 := by ring
+    simp only [hy1, UScalar.val_or, ht1v]
+    rw [hadd, hy0v]
+    try ring
+  step as ⟨bi1, hbi1⟩
+  have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac
+  rw [hbi1v]
+  try simp only [spec_ok]
+  -- bi = 2: byte 18
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (2#usize < 8#usize) by scalar_tac)]
+  step as ⟨i2, hi2⟩
+  have hi2v : i2 = 16#usize := by clear * - hi2; scalar_tac
+  rw [hi2v]
+  step as ⟨i12, hi12⟩
+  have hi12v : i12 = 18#usize := by clear * - hi12; scalar_tac
+  rw [hi12v]
+  step as ⟨x2, hx2⟩
+  simp [hb] at hx2
+  step with UScalar.cast.step_spec as ⟨c2, hc2⟩
+  have hc2v : c2.val = b18.val := by
+    rw [hc2, UScalar.cast_val_eq, hx2]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s2, hsh2⟩
+  have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac
+  step as ⟨t2, ht2⟩
+  have ht2v : t2.val = b18.val * 2^16 := by
+    rw [ht2]
+    simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y2, hy2⟩
+  have hy2v : y2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 := by
+    have hult : y1.val < 2^16 := by rw [hy1v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b18.val
+    have hadd : y1.val ||| b18.val * 2^16 = y1.val + b18.val * 2^16 := by
+      calc y1.val ||| b18.val * 2^16
+          = y1.val ||| 2^16 * b18.val := by rw [Nat.mul_comm]
+        _ = 2^16 * b18.val ||| y1.val := Nat.lor_comm _ _
+        _ = 2^16 * b18.val + y1.val := hor.symm
+        _ = y1.val + b18.val * 2^16 := by ring
+    simp only [hy2, UScalar.val_or, ht2v]
+    rw [hadd, hy1v]
+    try ring
+  step as ⟨bi2, hbi2⟩
+  have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac
+  rw [hbi2v]
+  try simp only [spec_ok]
+  -- bi = 3: byte 19
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (3#usize < 8#usize) by scalar_tac)]
+  step as ⟨i3, hi3⟩
+  have hi3v : i3 = 16#usize := by clear * - hi3; scalar_tac
+  rw [hi3v]
+  step as ⟨i13, hi13⟩
+  have hi13v : i13 = 19#usize := by clear * - hi13; scalar_tac
+  rw [hi13v]
+  step as ⟨x3, hx3⟩
+  simp [hb] at hx3
+  step with UScalar.cast.step_spec as ⟨c3, hc3⟩
+  have hc3v : c3.val = b19.val := by
+    rw [hc3, UScalar.cast_val_eq, hx3]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s3, hsh3⟩
+  have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac
+  step as ⟨t3, ht3⟩
+  have ht3v : t3.val = b19.val * 2^24 := by
+    rw [ht3]
+    simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y3, hy3⟩
+  have hy3v : y3.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 := by
+    have hult : y2.val < 2^24 := by rw [hy2v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b19.val
+    have hadd : y2.val ||| b19.val * 2^24 = y2.val + b19.val * 2^24 := by
+      calc y2.val ||| b19.val * 2^24
+          = y2.val ||| 2^24 * b19.val := by rw [Nat.mul_comm]
+        _ = 2^24 * b19.val ||| y2.val := Nat.lor_comm _ _
+        _ = 2^24 * b19.val + y2.val := hor.symm
+        _ = y2.val + b19.val * 2^24 := by ring
+    simp only [hy3, UScalar.val_or, ht3v]
+    rw [hadd, hy2v]
+    try ring
+  step as ⟨bi3, hbi3⟩
+  have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac
+  rw [hbi3v]
+  try simp only [spec_ok]
+  -- bi = 4: byte 20
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (4#usize < 8#usize) by scalar_tac)]
+  step as ⟨i4, hi4⟩
+  have hi4v : i4 = 16#usize := by clear * - hi4; scalar_tac
+  rw [hi4v]
+  step as ⟨i14, hi14⟩
+  have hi14v : i14 = 20#usize := by clear * - hi14; scalar_tac
+  rw [hi14v]
+  step as ⟨x4, hx4⟩
+  simp [hb] at hx4
+  step with UScalar.cast.step_spec as ⟨c4, hc4⟩
+  have hc4v : c4.val = b20.val := by
+    rw [hc4, UScalar.cast_val_eq, hx4]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s4, hsh4⟩
+  have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac
+  step as ⟨t4, ht4⟩
+  have ht4v : t4.val = b20.val * 2^32 := by
+    rw [ht4]
+    simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y4, hy4⟩
+  have hy4v : y4.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 := by
+    have hult : y3.val < 2^32 := by rw [hy3v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b20.val
+    have hadd : y3.val ||| b20.val * 2^32 = y3.val + b20.val * 2^32 := by
+      calc y3.val ||| b20.val * 2^32
+          = y3.val ||| 2^32 * b20.val := by rw [Nat.mul_comm]
+        _ = 2^32 * b20.val ||| y3.val := Nat.lor_comm _ _
+        _ = 2^32 * b20.val + y3.val := hor.symm
+        _ = y3.val + b20.val * 2^32 := by ring
+    simp only [hy4, UScalar.val_or, ht4v]
+    rw [hadd, hy3v]
+    try ring
+  step as ⟨bi4, hbi4⟩
+  have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac
+  rw [hbi4v]
+  try simp only [spec_ok]
+  -- bi = 5: byte 21
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (5#usize < 8#usize) by scalar_tac)]
+  step as ⟨i5, hi5⟩
+  have hi5v : i5 = 16#usize := by clear * - hi5; scalar_tac
+  rw [hi5v]
+  step as ⟨i15, hi15⟩
+  have hi15v : i15 = 21#usize := by clear * - hi15; scalar_tac
+  rw [hi15v]
+  step as ⟨x5, hx5⟩
+  simp [hb] at hx5
+  step with UScalar.cast.step_spec as ⟨c5, hc5⟩
+  have hc5v : c5.val = b21.val := by
+    rw [hc5, UScalar.cast_val_eq, hx5]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s5, hsh5⟩
+  have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac
+  step as ⟨t5, ht5⟩
+  have ht5v : t5.val = b21.val * 2^40 := by
+    rw [ht5]
+    simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y5, hy5⟩
+  have hy5v : y5.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 := by
+    have hult : y4.val < 2^40 := by rw [hy4v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b21.val
+    have hadd : y4.val ||| b21.val * 2^40 = y4.val + b21.val * 2^40 := by
+      calc y4.val ||| b21.val * 2^40
+          = y4.val ||| 2^40 * b21.val := by rw [Nat.mul_comm]
+        _ = 2^40 * b21.val ||| y4.val := Nat.lor_comm _ _
+        _ = 2^40 * b21.val + y4.val := hor.symm
+        _ = y4.val + b21.val * 2^40 := by ring
+    simp only [hy5, UScalar.val_or, ht5v]
+    rw [hadd, hy4v]
+    try ring
+  step as ⟨bi5, hbi5⟩
+  have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac
+  rw [hbi5v]
+  try simp only [spec_ok]
+  -- bi = 6: byte 22
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (6#usize < 8#usize) by scalar_tac)]
+  step as ⟨i6, hi6⟩
+  have hi6v : i6 = 16#usize := by clear * - hi6; scalar_tac
+  rw [hi6v]
+  step as ⟨i16, hi16⟩
+  have hi16v : i16 = 22#usize := by clear * - hi16; scalar_tac
+  rw [hi16v]
+  step as ⟨x6, hx6⟩
+  simp [hb] at hx6
+  step with UScalar.cast.step_spec as ⟨c6, hc6⟩
+  have hc6v : c6.val = b22.val := by
+    rw [hc6, UScalar.cast_val_eq, hx6]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s6, hsh6⟩
+  have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac
+  step as ⟨t6, ht6⟩
+  have ht6v : t6.val = b22.val * 2^48 := by
+    rw [ht6]
+    simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y6, hy6⟩
+  have hy6v : y6.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 := by
+    have hult : y5.val < 2^48 := by rw [hy5v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b22.val
+    have hadd : y5.val ||| b22.val * 2^48 = y5.val + b22.val * 2^48 := by
+      calc y5.val ||| b22.val * 2^48
+          = y5.val ||| 2^48 * b22.val := by rw [Nat.mul_comm]
+        _ = 2^48 * b22.val ||| y5.val := Nat.lor_comm _ _
+        _ = 2^48 * b22.val + y5.val := hor.symm
+        _ = y5.val + b22.val * 2^48 := by ring
+    simp only [hy6, UScalar.val_or, ht6v]
+    rw [hadd, hy5v]
+    try ring
+  step as ⟨bi6, hbi6⟩
+  have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac
+  rw [hbi6v]
+  try simp only [spec_ok]
+  -- bi = 7: byte 23
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (7#usize < 8#usize) by scalar_tac)]
+  step as ⟨i7, hi7⟩
+  have hi7v : i7 = 16#usize := by clear * - hi7; scalar_tac
+  rw [hi7v]
+  step as ⟨i17, hi17⟩
+  have hi17v : i17 = 23#usize := by clear * - hi17; scalar_tac
+  rw [hi17v]
+  step as ⟨x7, hx7⟩
+  simp [hb] at hx7
+  step with UScalar.cast.step_spec as ⟨c7, hc7⟩
+  have hc7v : c7.val = b23.val := by
+    rw [hc7, UScalar.cast_val_eq, hx7]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s7, hsh7⟩
+  have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac
+  step as ⟨t7, ht7⟩
+  have ht7v : t7.val = b23.val * 2^56 := by
+    rw [ht7]
+    simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y7, hy7⟩
+  have hy7v : y7.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 := by
+    have hult : y6.val < 2^56 := by rw [hy6v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b23.val
+    have hadd : y6.val ||| b23.val * 2^56 = y6.val + b23.val * 2^56 := by
+      calc y6.val ||| b23.val * 2^56
+          = y6.val ||| 2^56 * b23.val := by rw [Nat.mul_comm]
+        _ = 2^56 * b23.val ||| y6.val := Nat.lor_comm _ _
+        _ = 2^56 * b23.val + y6.val := hor.symm
+        _ = y6.val + b23.val * 2^56 := by ring
+    simp only [hy7, UScalar.val_or, ht7v]
+    rw [hadd, hy6v]
+    try ring
+  step as ⟨bi7, hbi7⟩
+  have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac
+  rw [hbi7v]
+  try simp only [spec_ok]
+  -- exit: bi = 8, done (self, t)
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)]
+  try simp only [spec_ok]
+  exact ⟨True.intro, hy7v⟩
+
+/-- Inner LE-load loop for word 3: t accumulates bytes 24..31
+    little-endian. The scalar struct passes through unchanged. -/
+theorem naf_word_loop_spec_3 (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]) :
+    scalar.Scalar.non_adjacent_form_loop0_loop0 self 3#usize 0#u64 0#usize
+      ⦃ p => p.1 = self ∧ p.2.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 ⦄ := by
+  have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
+  have hbb24 : b24.val < 2^8 := by scalar_tac
+  have hbb25 : b25.val < 2^8 := by scalar_tac
+  have hbb26 : b26.val < 2^8 := by scalar_tac
+  have hbb27 : b27.val < 2^8 := by scalar_tac
+  have hbb28 : b28.val < 2^8 := by scalar_tac
+  have hbb29 : b29.val < 2^8 := by scalar_tac
+  have hbb30 : b30.val < 2^8 := by scalar_tac
+  have hbb31 : b31.val < 2^8 := by scalar_tac
+  unfold scalar.Scalar.non_adjacent_form_loop0_loop0
+  -- bi = 0: byte 24
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (0#usize < 8#usize) by scalar_tac)]
+  step as ⟨i0, hi0⟩
+  have hi0v : i0 = 24#usize := by clear * - hi0; scalar_tac
+  rw [hi0v]
+  step as ⟨i10, hi10⟩
+  have hi10v : i10 = 24#usize := by clear * - hi10; scalar_tac
+  rw [hi10v]
+  step as ⟨x0, hx0⟩
+  simp [hb] at hx0
+  step with UScalar.cast.step_spec as ⟨c0, hc0⟩
+  have hc0v : c0.val = b24.val := by
+    rw [hc0, UScalar.cast_val_eq, hx0]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s0, hsh0⟩
+  have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac
+  step as ⟨t0, ht0⟩
+  have ht0v : t0.val = b24.val * 2^0 := by
+    rw [ht0]
+    simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y0, hy0⟩
+  have hy0v : y0.val = b24.val := by
+    simp [hy0, UScalar.val_or, ht0v]
+  step as ⟨bi0, hbi0⟩
+  have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac
+  rw [hbi0v]
+  try simp only [spec_ok]
+  -- bi = 1: byte 25
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (1#usize < 8#usize) by scalar_tac)]
+  step as ⟨i1, hi1⟩
+  have hi1v : i1 = 24#usize := by clear * - hi1; scalar_tac
+  rw [hi1v]
+  step as ⟨i11, hi11⟩
+  have hi11v : i11 = 25#usize := by clear * - hi11; scalar_tac
+  rw [hi11v]
+  step as ⟨x1, hx1⟩
+  simp [hb] at hx1
+  step with UScalar.cast.step_spec as ⟨c1, hc1⟩
+  have hc1v : c1.val = b25.val := by
+    rw [hc1, UScalar.cast_val_eq, hx1]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s1, hsh1⟩
+  have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac
+  step as ⟨t1, ht1⟩
+  have ht1v : t1.val = b25.val * 2^8 := by
+    rw [ht1]
+    simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y1, hy1⟩
+  have hy1v : y1.val = b24.val + b25.val * 2^8 := by
+    have hult : y0.val < 2^8 := by rw [hy0v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b25.val
+    have hadd : y0.val ||| b25.val * 2^8 = y0.val + b25.val * 2^8 := by
+      calc y0.val ||| b25.val * 2^8
+          = y0.val ||| 2^8 * b25.val := by rw [Nat.mul_comm]
+        _ = 2^8 * b25.val ||| y0.val := Nat.lor_comm _ _
+        _ = 2^8 * b25.val + y0.val := hor.symm
+        _ = y0.val + b25.val * 2^8 := by ring
+    simp only [hy1, UScalar.val_or, ht1v]
+    rw [hadd, hy0v]
+    try ring
+  step as ⟨bi1, hbi1⟩
+  have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac
+  rw [hbi1v]
+  try simp only [spec_ok]
+  -- bi = 2: byte 26
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (2#usize < 8#usize) by scalar_tac)]
+  step as ⟨i2, hi2⟩
+  have hi2v : i2 = 24#usize := by clear * - hi2; scalar_tac
+  rw [hi2v]
+  step as ⟨i12, hi12⟩
+  have hi12v : i12 = 26#usize := by clear * - hi12; scalar_tac
+  rw [hi12v]
+  step as ⟨x2, hx2⟩
+  simp [hb] at hx2
+  step with UScalar.cast.step_spec as ⟨c2, hc2⟩
+  have hc2v : c2.val = b26.val := by
+    rw [hc2, UScalar.cast_val_eq, hx2]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s2, hsh2⟩
+  have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac
+  step as ⟨t2, ht2⟩
+  have ht2v : t2.val = b26.val * 2^16 := by
+    rw [ht2]
+    simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y2, hy2⟩
+  have hy2v : y2.val = b24.val + b25.val * 2^8 + b26.val * 2^16 := by
+    have hult : y1.val < 2^16 := by rw [hy1v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b26.val
+    have hadd : y1.val ||| b26.val * 2^16 = y1.val + b26.val * 2^16 := by
+      calc y1.val ||| b26.val * 2^16
+          = y1.val ||| 2^16 * b26.val := by rw [Nat.mul_comm]
+        _ = 2^16 * b26.val ||| y1.val := Nat.lor_comm _ _
+        _ = 2^16 * b26.val + y1.val := hor.symm
+        _ = y1.val + b26.val * 2^16 := by ring
+    simp only [hy2, UScalar.val_or, ht2v]
+    rw [hadd, hy1v]
+    try ring
+  step as ⟨bi2, hbi2⟩
+  have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac
+  rw [hbi2v]
+  try simp only [spec_ok]
+  -- bi = 3: byte 27
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (3#usize < 8#usize) by scalar_tac)]
+  step as ⟨i3, hi3⟩
+  have hi3v : i3 = 24#usize := by clear * - hi3; scalar_tac
+  rw [hi3v]
+  step as ⟨i13, hi13⟩
+  have hi13v : i13 = 27#usize := by clear * - hi13; scalar_tac
+  rw [hi13v]
+  step as ⟨x3, hx3⟩
+  simp [hb] at hx3
+  step with UScalar.cast.step_spec as ⟨c3, hc3⟩
+  have hc3v : c3.val = b27.val := by
+    rw [hc3, UScalar.cast_val_eq, hx3]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s3, hsh3⟩
+  have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac
+  step as ⟨t3, ht3⟩
+  have ht3v : t3.val = b27.val * 2^24 := by
+    rw [ht3]
+    simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y3, hy3⟩
+  have hy3v : y3.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 := by
+    have hult : y2.val < 2^24 := by rw [hy2v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b27.val
+    have hadd : y2.val ||| b27.val * 2^24 = y2.val + b27.val * 2^24 := by
+      calc y2.val ||| b27.val * 2^24
+          = y2.val ||| 2^24 * b27.val := by rw [Nat.mul_comm]
+        _ = 2^24 * b27.val ||| y2.val := Nat.lor_comm _ _
+        _ = 2^24 * b27.val + y2.val := hor.symm
+        _ = y2.val + b27.val * 2^24 := by ring
+    simp only [hy3, UScalar.val_or, ht3v]
+    rw [hadd, hy2v]
+    try ring
+  step as ⟨bi3, hbi3⟩
+  have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac
+  rw [hbi3v]
+  try simp only [spec_ok]
+  -- bi = 4: byte 28
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (4#usize < 8#usize) by scalar_tac)]
+  step as ⟨i4, hi4⟩
+  have hi4v : i4 = 24#usize := by clear * - hi4; scalar_tac
+  rw [hi4v]
+  step as ⟨i14, hi14⟩
+  have hi14v : i14 = 28#usize := by clear * - hi14; scalar_tac
+  rw [hi14v]
+  step as ⟨x4, hx4⟩
+  simp [hb] at hx4
+  step with UScalar.cast.step_spec as ⟨c4, hc4⟩
+  have hc4v : c4.val = b28.val := by
+    rw [hc4, UScalar.cast_val_eq, hx4]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s4, hsh4⟩
+  have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac
+  step as ⟨t4, ht4⟩
+  have ht4v : t4.val = b28.val * 2^32 := by
+    rw [ht4]
+    simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y4, hy4⟩
+  have hy4v : y4.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 := by
+    have hult : y3.val < 2^32 := by rw [hy3v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b28.val
+    have hadd : y3.val ||| b28.val * 2^32 = y3.val + b28.val * 2^32 := by
+      calc y3.val ||| b28.val * 2^32
+          = y3.val ||| 2^32 * b28.val := by rw [Nat.mul_comm]
+        _ = 2^32 * b28.val ||| y3.val := Nat.lor_comm _ _
+        _ = 2^32 * b28.val + y3.val := hor.symm
+        _ = y3.val + b28.val * 2^32 := by ring
+    simp only [hy4, UScalar.val_or, ht4v]
+    rw [hadd, hy3v]
+    try ring
+  step as ⟨bi4, hbi4⟩
+  have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac
+  rw [hbi4v]
+  try simp only [spec_ok]
+  -- bi = 5: byte 29
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (5#usize < 8#usize) by scalar_tac)]
+  step as ⟨i5, hi5⟩
+  have hi5v : i5 = 24#usize := by clear * - hi5; scalar_tac
+  rw [hi5v]
+  step as ⟨i15, hi15⟩
+  have hi15v : i15 = 29#usize := by clear * - hi15; scalar_tac
+  rw [hi15v]
+  step as ⟨x5, hx5⟩
+  simp [hb] at hx5
+  step with UScalar.cast.step_spec as ⟨c5, hc5⟩
+  have hc5v : c5.val = b29.val := by
+    rw [hc5, UScalar.cast_val_eq, hx5]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s5, hsh5⟩
+  have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac
+  step as ⟨t5, ht5⟩
+  have ht5v : t5.val = b29.val * 2^40 := by
+    rw [ht5]
+    simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y5, hy5⟩
+  have hy5v : y5.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 := by
+    have hult : y4.val < 2^40 := by rw [hy4v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b29.val
+    have hadd : y4.val ||| b29.val * 2^40 = y4.val + b29.val * 2^40 := by
+      calc y4.val ||| b29.val * 2^40
+          = y4.val ||| 2^40 * b29.val := by rw [Nat.mul_comm]
+        _ = 2^40 * b29.val ||| y4.val := Nat.lor_comm _ _
+        _ = 2^40 * b29.val + y4.val := hor.symm
+        _ = y4.val + b29.val * 2^40 := by ring
+    simp only [hy5, UScalar.val_or, ht5v]
+    rw [hadd, hy4v]
+    try ring
+  step as ⟨bi5, hbi5⟩
+  have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac
+  rw [hbi5v]
+  try simp only [spec_ok]
+  -- bi = 6: byte 30
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (6#usize < 8#usize) by scalar_tac)]
+  step as ⟨i6, hi6⟩
+  have hi6v : i6 = 24#usize := by clear * - hi6; scalar_tac
+  rw [hi6v]
+  step as ⟨i16, hi16⟩
+  have hi16v : i16 = 30#usize := by clear * - hi16; scalar_tac
+  rw [hi16v]
+  step as ⟨x6, hx6⟩
+  simp [hb] at hx6
+  step with UScalar.cast.step_spec as ⟨c6, hc6⟩
+  have hc6v : c6.val = b30.val := by
+    rw [hc6, UScalar.cast_val_eq, hx6]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s6, hsh6⟩
+  have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac
+  step as ⟨t6, ht6⟩
+  have ht6v : t6.val = b30.val * 2^48 := by
+    rw [ht6]
+    simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y6, hy6⟩
+  have hy6v : y6.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 := by
+    have hult : y5.val < 2^48 := by rw [hy5v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b30.val
+    have hadd : y5.val ||| b30.val * 2^48 = y5.val + b30.val * 2^48 := by
+      calc y5.val ||| b30.val * 2^48
+          = y5.val ||| 2^48 * b30.val := by rw [Nat.mul_comm]
+        _ = 2^48 * b30.val ||| y5.val := Nat.lor_comm _ _
+        _ = 2^48 * b30.val + y5.val := hor.symm
+        _ = y5.val + b30.val * 2^48 := by ring
+    simp only [hy6, UScalar.val_or, ht6v]
+    rw [hadd, hy5v]
+    try ring
+  step as ⟨bi6, hbi6⟩
+  have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac
+  rw [hbi6v]
+  try simp only [spec_ok]
+  -- bi = 7: byte 31
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_pos (show (7#usize < 8#usize) by scalar_tac)]
+  step as ⟨i7, hi7⟩
+  have hi7v : i7 = 24#usize := by clear * - hi7; scalar_tac
+  rw [hi7v]
+  step as ⟨i17, hi17⟩
+  have hi17v : i17 = 31#usize := by clear * - hi17; scalar_tac
+  rw [hi17v]
+  step as ⟨x7, hx7⟩
+  simp [hb] at hx7
+  step with UScalar.cast.step_spec as ⟨c7, hc7⟩
+  have hc7v : c7.val = b31.val := by
+    rw [hc7, UScalar.cast_val_eq, hx7]
+    simp only [UScalarTy.U64, UScalarTy.numBits]
+    omega
+  step as ⟨s7, hsh7⟩
+  have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac
+  step as ⟨t7, ht7⟩
+  have ht7v : t7.val = b31.val * 2^56 := by
+    rw [ht7]
+    simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64]
+    omega
+  step as ⟨y7, hy7⟩
+  have hy7v : y7.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 := by
+    have hult : y6.val < 2^56 := by rw [hy6v]; omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b31.val
+    have hadd : y6.val ||| b31.val * 2^56 = y6.val + b31.val * 2^56 := by
+      calc y6.val ||| b31.val * 2^56
+          = y6.val ||| 2^56 * b31.val := by rw [Nat.mul_comm]
+        _ = 2^56 * b31.val ||| y6.val := Nat.lor_comm _ _
+        _ = 2^56 * b31.val + y6.val := hor.symm
+        _ = y6.val + b31.val * 2^56 := by ring
+    simp only [hy7, UScalar.val_or, ht7v]
+    rw [hadd, hy6v]
+    try ring
+  step as ⟨bi7, hbi7⟩
+  have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac
+  rw [hbi7v]
+  try simp only [spec_ok]
+  -- exit: bi = 8, done (self, t)
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body]
+  rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)]
+  try simp only [spec_ok]
+  exact ⟨True.intro, hy7v⟩
+
+/-- Outer LE-load loop: fills x_u64[0..3] with the four little-endian
+    words of the 32 scalar bytes; x_u64[4] stays 0 (the carry pad). -/
+theorem naf_load_spec (self : scalar.Scalar)
+    (x_u64 : Std.Array Std.U64 5#usize)
+    (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])
+    (hx : (↑x_u64 : List Std.U64) = [0#u64, 0#u64, 0#u64, 0#u64, 0#u64]) :
+    scalar.Scalar.non_adjacent_form_loop0 self x_u64 0#usize
+      ⦃ ws => ∃ v0 v1 v2 v3 : U64,
+          (↑ws : List Std.U64) = [v0, v1, v2, v3, 0#u64] ∧
+          v0.val = 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 ∧
+          v1.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 ∧
+          v2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 ∧
+          v3.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 ⦄ := by
+  unfold scalar.Scalar.non_adjacent_form_loop0
+  -- k = 0: word 0
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0.body]
+  rw [if_pos (show (0#usize < 4#usize) by scalar_tac)]
+  step with (naf_word_loop_spec_0 self 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) as ⟨s0, t0, hs0, ht0⟩
+  rw [hs0]
+  step as ⟨a0, ha0⟩
+  have hl0 : (↑a0 : List Std.U64) = [t0, 0#u64, 0#u64, 0#u64, 0#u64] := by
+    simp only [ha0, Array.set_val_eq, hx]
+    rfl
+  step as ⟨k0, hk0⟩
+  have hk0v : k0 = 1#usize := by clear * - hk0; scalar_tac
+  rw [hk0v]
+  try simp only [spec_ok]
+  -- k = 1: word 1
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0.body]
+  rw [if_pos (show (1#usize < 4#usize) by scalar_tac)]
+  step with (naf_word_loop_spec_1 self 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) as ⟨s1, t1, hs1, ht1⟩
+  rw [hs1]
+  step as ⟨a1, ha1⟩
+  have hl1 : (↑a1 : List Std.U64) = [t0, t1, 0#u64, 0#u64, 0#u64] := by
+    simp only [ha1, Array.set_val_eq, hl0]
+    rfl
+  step as ⟨k1, hk1⟩
+  have hk1v : k1 = 2#usize := by clear * - hk1; scalar_tac
+  rw [hk1v]
+  try simp only [spec_ok]
+  -- k = 2: word 2
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0.body]
+  rw [if_pos (show (2#usize < 4#usize) by scalar_tac)]
+  step with (naf_word_loop_spec_2 self 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) as ⟨s2, t2, hs2, ht2⟩
+  rw [hs2]
+  step as ⟨a2, ha2⟩
+  have hl2 : (↑a2 : List Std.U64) = [t0, t1, t2, 0#u64, 0#u64] := by
+    simp only [ha2, Array.set_val_eq, hl1]
+    rfl
+  step as ⟨k2, hk2⟩
+  have hk2v : k2 = 3#usize := by clear * - hk2; scalar_tac
+  rw [hk2v]
+  try simp only [spec_ok]
+  -- k = 3: word 3
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0.body]
+  rw [if_pos (show (3#usize < 4#usize) by scalar_tac)]
+  step with (naf_word_loop_spec_3 self 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) as ⟨s3, t3, hs3, ht3⟩
+  rw [hs3]
+  step as ⟨a3, ha3⟩
+  have hl3 : (↑a3 : List Std.U64) = [t0, t1, t2, t3, 0#u64] := by
+    simp only [ha3, Array.set_val_eq, hl2]
+    rfl
+  step as ⟨k3, hk3⟩
+  have hk3v : k3 = 4#usize := by clear * - hk3; scalar_tac
+  rw [hk3v]
+  try simp only [spec_ok]
+  -- exit: k = 4, done x_u64
+  apply loop_step
+  simp only [scalar.Scalar.non_adjacent_form_loop0.body]
+  rw [if_neg (show ¬ (4#usize < 4#usize) by scalar_tac)]
+  try simp only [spec_ok]
+  exact ⟨t0, t1, t2, t3, hl3, ht0, ht1, ht2, ht3⟩
+
+end CurveFieldProofs
diff --git a/verification/Proofs/DsmNafLoopSpec.lean b/verification/Proofs/DsmNafLoopSpec.lean
new file mode 100644
index 0000000..bdd7c03
--- /dev/null
+++ b/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
+
+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
diff --git a/verification/Proofs/DsmNafMath.lean b/verification/Proofs/DsmNafMath.lean
new file mode 100644
index 0000000..f600c56
--- /dev/null
+++ b/verification/Proofs/DsmNafMath.lean
@@ -0,0 +1,239 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmNafMath.lean — NAF campaign, stage 2: the pure arithmetic core
+   of the w=5 NAF digit loop (no extraction dependence beyond `nafDigit`).
+
+   The digit loop's state is (naf, pos, carry) with the exact ℤ invariant
+       nafSum naf 256 + carry·2^pos = V mod 2^pos
+   (digits at k ≥ pos all zero, carry ≤ 1, and carry = 1 → pos ≤ 254 given
+   V < 2^253 — the component that kills the carry at exit).
+
+   Step theorems the monadic walk plugs in:
+   · `nafSum_set`          — writing a fresh digit adds d·2^pos to the sum.
+   · `div_pow_shift` / `mod32_absorb` / `naf_window_single` / `naf_window_cross`
+     — the 64-bit buffer read at bit position p+b sees (V >> (p+b)) mod 32
+     (single word when b + 5 ≤ 64; cross-word via disjoint-OR otherwise).
+   · `naf_even_step`       — even window ⇒ pos+1, carry preserved (the parity
+     of V >> pos matches carry, so both sides absorb carry·2^(pos+1)).
+   · `naf_odd_step`        — odd window ⇒ digit (window − 32·carry'), pos+5:
+     the digit plus the new carry reconstruct the 5 consumed bits
+     (Nat.mod_mul telescoping).
+   · `naf_carry_even` / `naf_carry_odd` — carry = 1 → pos ≤ 254 propagation
+     from V < 2^253.
+   · `naf_exit`            — pos ≥ 256 kills the carry: nafSum = V exactly.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmLoopSpec
+open Aeneas Aeneas.Std
+open curve25519
+
+set_option maxHeartbeats 4000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+/-! ### The signed digit sum -/
+
+/-- Σ_{k<m} naf[k]·2^k over ℤ — the value a digit array denotes. -/
+def nafSum (naf : Std.Array Std.I8 256#usize) (m : ℕ) : ℤ :=
+  ∑ k ∈ Finset.range m, nafDigit naf k * 2^k
+
+/-- Setting entry `pos` (previously 0) adds d·2^pos to the full sum. -/
+theorem nafSum_set (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ) (d : Std.I8)
+    (hpos : pos < 256) (hold : nafDigit naf pos = 0)
+    (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) :
+    nafSum naf' 256 = nafSum naf 256 + d.val * 2^pos := by
+  have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
+  have hlen' : ((↑naf : List Std.I8).set pos d).length = 256 := by
+    rw [List.length_set]; exact hlen
+  have hdig : ∀ k, k < 256 → nafDigit naf' k =
+      if k = pos then d.val else nafDigit naf k := by
+    intro k hk
+    unfold nafDigit
+    rw [hset]
+    by_cases h : k = pos
+    · subst h
+      rw [getElem!_pos ((↑naf : List Std.I8).set k d) k (by omega),
+          List.getElem_set_self]
+      simp
+    · rw [getElem!_pos ((↑naf : List Std.I8).set pos d) k (by omega),
+          List.getElem_set_ne (by omega),
+          ← getElem!_pos (↑naf : List Std.I8) k (by omega)]
+      rw [if_neg h]
+  unfold nafSum
+  have hmem : pos ∈ Finset.range 256 := Finset.mem_range.mpr hpos
+  rw [← Finset.sum_erase_add _ _ hmem, ← Finset.sum_erase_add _ _ hmem]
+  have hcongr : ∑ k ∈ (Finset.range 256).erase pos, nafDigit naf' k * 2^k
+      = ∑ k ∈ (Finset.range 256).erase pos, nafDigit naf k * 2^k := by
+    apply Finset.sum_congr rfl
+    intro k hk
+    rw [hdig k (Finset.mem_range.mp (Finset.mem_of_mem_erase hk)),
+        if_neg (Finset.ne_of_mem_erase hk)]
+  rw [hcongr, hdig pos hpos, if_pos rfl, hold]
+  ring
+
+/-! ### Window-read arithmetic -/
+
+/-- Dividing the three-part value lo + 2^p·(w + 2^64·rest) by 2^(p+b)
+    (b ≤ 64, lo < 2^p) yields w >> b plus the rest shifted down. -/
+theorem div_pow_shift (lo w rest p b : ℕ) (hlo : lo < 2^p) (hb : b ≤ 64) :
+    (lo + 2^p * (w + 2^64 * rest)) / 2^(p+b) = w / 2^b + 2^(64-b) * rest := by
+  have hp : (0:ℕ) < 2^p := Nat.two_pow_pos p
+  have hbp : (0:ℕ) < 2^b := Nat.two_pow_pos b
+  rw [pow_add, ← Nat.div_div_eq_div_mul]
+  have h1 : (lo + 2^p * (w + 2^64 * rest)) / 2^p = w + 2^64 * rest := by
+    rw [Nat.add_mul_div_left _ _ hp, Nat.div_eq_of_lt hlo, Nat.zero_add]
+  rw [h1]
+  have h2 : (2:ℕ)^64 = 2^b * 2^(64-b) := by
+    rw [← pow_add]; congr 1; omega
+  rw [h2, Nat.mul_assoc, Nat.add_mul_div_left _ _ hbp]
+
+/-- Multiples of 2^m (m ≥ 5) vanish mod 32. -/
+theorem mod32_absorb (x y m : ℕ) (hm : 5 ≤ m) :
+    (x + 2^m * y) % 32 = x % 32 := by
+  have h : (2:ℕ)^m = 32 * 2^(m-5) := by
+    rw [show (32:ℕ) = 2^5 by norm_num, ← pow_add]; congr 1; omega
+  rw [h, Nat.mul_assoc, Nat.add_mul_mod_self_left]
+
+/-- Single-word window read: when the 5-bit window at bit b fits inside
+    word w (b + 5 ≤ 64), (w >> b) mod 32 is the value's window at p+b. -/
+theorem naf_window_single (V lo w rest p b : ℕ)
+    (hV : V = lo + 2^p * (w + 2^64 * rest)) (hlo : lo < 2^p) (hb : b + 5 ≤ 64) :
+    (w / 2^b) % 32 = (V / 2^(p+b)) % 32 := by
+  rw [hV, div_pow_shift lo w rest p b hlo (by omega)]
+  exact (mod32_absorb _ _ _ (by omega)).symm
+
+/-- Cross-word window read: when the window at bit b straddles into the next
+    word w' (b ≥ 60), the extracted read (w >> b) ||| ((w' << (64−b)) mod 2^64)
+    still sees the value's window at p+b, mod 32. -/
+theorem naf_window_cross (V lo w w' rest p b : ℕ)
+    (hV : V = lo + 2^p * (w + 2^64 * (w' + 2^64 * rest)))
+    (hlo : lo < 2^p) (hw : w < 2^64) (hb : b < 64) :
+    ((w / 2^b) ||| (w' <<< (64 - b)) % 2^64) % 32 = (V / 2^(p+b)) % 32 := by
+  have hp64 : (2:ℕ)^(64-b) * 2^b = 2^64 := by
+    rw [← pow_add]; congr 1; omega
+  have hp128 : (2:ℕ)^(64-b) * 2^64 = 2^(128-b) := by
+    rw [← pow_add]; congr 1; omega
+  -- the truncated shift: (w' << (64−b)) mod 2^64 = 2^(64−b)·(w' mod 2^b)
+  have hsh : (w' <<< (64 - b)) % 2^64 = 2^(64-b) * (w' % 2^b) := by
+    rw [Nat.shiftLeft_eq, Nat.mul_comm w' _, ← hp64, Nat.mul_mod_mul_left]
+  -- the OR is disjoint: w >> b < 2^(64−b)
+  have hdl : w / 2^b < 2^(64-b) := by
+    rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos b)]
+    calc w < 2^64 := hw
+      _ = 2^(64-b) * 2^b := hp64.symm
+  have hor := Nat.two_pow_add_eq_or_of_lt (b := w / 2^b) (i := 64-b) hdl (w' % 2^b)
+  rw [hsh, Nat.lor_comm, ← hor]
+  -- the value side
+  rw [hV, div_pow_shift lo w _ p b hlo (by omega)]
+  -- both sides are (w/2^b + 2^(64−b)·(w' mod 2^b)) mod 32 after absorbing
+  -- the 2^64-multiples: w' = w' mod 2^b + 2^b·(w'/2^b)
+  have hw' : w' = w' % 2^b + 2^b * (w' / 2^b) := (Nat.mod_add_div _ _).symm
+  have e1 : w / 2^b + 2^(64-b) * (w' + 2^64 * rest)
+      = (2^(64-b) * (w' % 2^b) + w / 2^b)
+        + 2^64 * (w' / 2^b + 2^(64-b) * rest) := by
+    conv_lhs => rw [hw']
+    rw [Nat.mul_add, Nat.mul_add, Nat.mul_add, ← Nat.mul_assoc, hp64,
+        ← Nat.mul_assoc, hp128]
+    have hp128' : (2:ℕ)^(128-b) = 2^64 * 2^(64-b) := by
+      rw [← pow_add]; congr 1; omega
+    rw [hp128']
+    ring
+  rw [e1]
+  have := mod32_absorb (2^(64-b) * (w' % 2^b) + w / 2^b)
+    (w' / 2^b + 2^(64-b) * rest) 64 (by omega)
+  rw [this]
+
+/-! ### Invariant step theorems -/
+
+/-- Even window: digit 0, position advances by 1, carry preserved.
+    The parity of V >> pos equals the carry, so the invariant extends. -/
+theorem naf_even_step (V pos : ℕ) (carry : ℕ) (S : ℤ)
+    (hc : carry ≤ 1)
+    (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ))
+    (heven : (carry + (V / 2^pos) % 32) % 2 = 0) :
+    S + carry * 2^(pos+1) = ((V % 2^(pos+1) : ℕ) : ℤ) := by
+  have hmm : V % 2^(pos+1) = V % 2^pos + 2^pos * ((V / 2^pos) % 2) := by
+    rw [pow_succ, Nat.mod_mul]
+  have hpar : (V / 2^pos) % 2 = carry := by omega
+  rw [hmm, hpar]
+  push_cast at hinv ⊢
+  linear_combination hinv
+
+/-- Odd window: digit window − 32·carry', position advances by 5.
+    The digit plus the promoted carry reconstruct the 5 consumed bits. -/
+theorem naf_odd_step (V pos : ℕ) (carry carry' : ℕ) (S d : ℤ)
+    (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ))
+    (hd : d = (carry : ℤ) + ((V / 2^pos) % 32 : ℕ) - 32 * carry') :
+    (S + d * 2^pos) + carry' * 2^(pos+5) = ((V % 2^(pos+5) : ℕ) : ℤ) := by
+  have hmm : V % 2^(pos+5) = V % 2^pos + 2^pos * ((V / 2^pos) % 32) := by
+    have h : (2:ℕ)^(pos+5) = 2^pos * 32 := by rw [pow_add]; norm_num
+    rw [h, Nat.mod_mul]
+  rw [hmm, hd]
+  push_cast at hinv ⊢
+  linear_combination hinv
+
+/-- Carry propagation, even step: with V < 2^253, an even step that keeps
+    carry = 1 must be reading a set bit, so pos ≤ 252 and pos+1 ≤ 254. -/
+theorem naf_carry_even (V pos : ℕ) (carry : ℕ) (hV : V < 2^253)
+    (hc : carry ≤ 1)
+    (heven : (carry + (V / 2^pos) % 32) % 2 = 0) :
+    carry = 1 → pos + 1 ≤ 254 := by
+  intro h1
+  subst h1
+  have h3 : 1 ≤ (V / 2^pos) % 32 := by
+    generalize (V / 2^pos) % 32 = r at heven ⊢
+    omega
+  have hge : 1 ≤ V / 2^pos := le_trans h3 (Nat.mod_le _ _)
+  have hle : 2^pos ≤ V := by
+    have h5 := (Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge
+    simpa using h5
+  have hpb : pos ≤ 252 := by
+    by_contra h
+    have h253 : (2:ℕ)^253 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
+    exact absurd (lt_of_le_of_lt (le_trans h253 hle) hV) (lt_irrefl _)
+  omega
+
+/-- Carry propagation, odd step: producing carry' = 1 needs window ≥ 16, so
+    V >> pos ≥ 15, forcing pos ≤ 249 (V < 2^253) and pos+5 ≤ 254. -/
+theorem naf_carry_odd (V pos : ℕ) (carry carry' : ℕ) (hV : V < 2^253)
+    (hc : carry ≤ 1)
+    (hcw : (carry + (V / 2^pos) % 32 < 16 ∧ carry' = 0) ∨
+           (16 ≤ carry + (V / 2^pos) % 32 ∧ carry' = 1)) :
+    carry' = 1 → pos + 5 ≤ 254 := by
+  intro h1
+  rcases hcw with ⟨-, h0⟩ | ⟨hge, -⟩
+  · omega
+  · have h15 : 15 ≤ (V / 2^pos) % 32 := by
+      generalize (V / 2^pos) % 32 = r at hge ⊢
+      omega
+    have hge15 : 15 ≤ V / 2^pos := le_trans h15 (Nat.mod_le _ _)
+    have hmul : 15 * 2^pos ≤ V :=
+      (Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge15
+    have hpb : pos ≤ 249 := by
+      by_contra h
+      have h250 : (2:ℕ)^250 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
+      have hbig : (2:ℕ)^253 < 15 * 2^250 := by norm_num
+      have hmono : 15 * 2^250 ≤ 15 * 2^pos := Nat.mul_le_mul_left 15 h250
+      exact absurd (lt_of_le_of_lt (le_trans hmono hmul) hV) (not_lt.mpr hbig.le)
+    omega
+
+/-- Exit: at pos ≥ 256 the carry must be dead (carry = 1 forces pos ≤ 254),
+    and V mod 2^pos = V, so the digit sum equals V exactly. -/
+theorem naf_exit (V pos : ℕ) (carry : ℕ) (S : ℤ) (hV : V < 2^253)
+    (hpos : 256 ≤ pos) (hc : carry ≤ 1) (hcp : carry = 1 → pos ≤ 254)
+    (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ)) : S = V := by
+  have hc0 : carry = 0 := by
+    by_contra h
+    have h1 : carry = 1 := by omega
+    have := hcp h1
+    omega
+  subst hc0
+  have hmod : V % 2^pos = V := by
+    apply Nat.mod_eq_of_lt
+    calc V < 2^253 := hV
+      _ ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
+  rw [hmod] at hinv
+  push_cast at hinv
+  linarith
+
+end CurveFieldProofs
diff --git a/verification/Proofs/DsmNafSpec.lean b/verification/Proofs/DsmNafSpec.lean
new file mode 100644
index 0000000..6dcea72
--- /dev/null
+++ b/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
+
+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
diff --git a/verification/check.sh b/verification/check.sh
index 9630f08..4ab554e 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -55,6 +55,11 @@ PROOFS=(
   DsmTableSpec
   DsmStepSpec
   DsmLoopSpec
+  DsmNafLoadSpec
+  DsmNafMath
+  DsmNafLoopSpec
+  DsmNafSpec
+  DsmMulSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
@@ -67,6 +72,12 @@ CERTS=(
   CurveFieldProofs.dsm_step_p_law
   CurveFieldProofs.dsm_step_b_law
   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=(
@@ -75,6 +86,8 @@ AUDIT_IMPORTS=(
   Proofs.DsmTableSpec
   Proofs.DsmStepSpec
   Proofs.DsmLoopSpec
+  Proofs.DsmNafSpec
+  Proofs.DsmMulSpec
 )
 
 # ── Phase 0: resource + integrity guards ────────────────────────────────────
diff --git a/verification/gen/CurveField/FunsExternal.lean b/verification/gen/CurveField/FunsExternal.lean
index f87bdc2..3051596 100644
--- a/verification/gen/CurveField/FunsExternal.lean
+++ b/verification/gen/CurveField/FunsExternal.lean
@@ -330,14 +330,6 @@ axiom
 axiom backend.serial.scalar_mul.variable_base.mul
   : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
 
-/-- [curve25519::backend::serial::scalar_mul::vartime_double_base::mul]:
-    Source: 'curve25519/solana-ed25519/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::backend::serial::scalar_mul::vartime_triple_base::mul_128_128_256_prechecked]:
     Source: 'curve25519/solana-ed25519/src/backend/serial/scalar_mul/vartime_triple_base.rs', lines 68:0-168:1 -/
 axiom backend.serial.scalar_mul.vartime_triple_base.mul_128_128_256_prechecked