diff --git a/verification/Proofs/DsmLoopSpec.lean b/verification/Proofs/DsmLoopSpec.lean
new file mode 100644
index 0000000..de70a7c
--- /dev/null
+++ b/verification/Proofs/DsmLoopSpec.lean
@@ -0,0 +1,216 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmLoopSpec.lean — double-scalar-mul campaign, brick 3:
+   the 256-iteration Straus/NAF loop, by genuine induction (no unrolling).
+
+   dsm_loop seeds r = identity, j = top+1 and runs
+       while j > 0 { idx = j-1; t = r.double();
+                     t = dsm_step_p(t, table_a, a_naf[idx]);
+                     t = dsm_step_b(t, table_b, b_naf[idx]);
+                     r = t.as_projective(); j = idx; }
+
+   ABSTRACTION: `dsmFold aD bD pA pB P j` — process digits j−1 … 0 onto the
+   accumulator P over the abstract Edwards addition: each iteration doubles
+   and applies the two digits through `edDigit` (DsmStepSpec). The loop
+   invariant is
+       ProjValid r ∧ OnCurve (projPt r) ∧ result = dsmFold … (projPt r) j
+   proven by induction on j.val, one symbolic body-walk per induction step:
+   proj_double_law → dsm_step_p_law → dsm_step_b_law → compl_as_projective_law.
+
+   Digit hypotheses (odd-or-zero, |d| < 16, for all 256 positions of both
+   arrays) are exactly what the NAF spec will provide (layering). Table
+   hypotheses are naf_table_spec's post for both tables.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.DsmStepSpec
+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
+
+/-! ### The abstract double-and-add fold -/
+
+/-- The k-th NAF digit of an extracted digit array, as an integer. -/
+def nafDigit (a : Std.Array Std.I8 256#usize) (k : ℕ) : ℤ := (a.val[k]!).val
+
+/-- `dsmFold aD bD pA pB P j`: apply digits j−1, j−2, …, 0 to accumulator P —
+    per digit: double, add aD's digit-multiple of pA, add bD's digit-multiple
+    of pB (all through `edDigit`, over the abstract `edAdd`). -/
+noncomputable def dsmFold (aD bD : ℕ → ℤ) (pA pB : Fp × Fp) :
+    (Fp × Fp) → ℕ → Fp × Fp
+  | P, 0 => P
+  | P, j + 1 => dsmFold aD bD pA pB
+      (edDigit pB (bD j) (edDigit pA (aD j) (edAdd P P))) j
+
+@[simp] theorem dsmFold_zero (aD bD : ℕ → ℤ) (pA pB P : Fp × Fp) :
+    dsmFold aD bD pA pB P 0 = P := rfl
+
+theorem dsmFold_succ (aD bD : ℕ → ℤ) (pA pB P : Fp × Fp) (j : ℕ) :
+    dsmFold aD bD pA pB P (j + 1) = dsmFold aD bD pA pB
+      (edDigit pB (bD j) (edDigit pA (aD j) (edAdd P P))) j := rfl
+
+/- The neutral point is on the curve: `onCurve_id` (EdCurve.lean). -/
+
+/-- Digit-array contract: every position is a NAF digit — odd or zero,
+    magnitude below 16. (The NAF spec provides this; layering.) -/
+def NafDigits (a : Std.Array Std.I8 256#usize) : Prop :=
+  ∀ k : ℕ, k < 256 →
+    (nafDigit a k = 0 ∨ nafDigit a k % 2 = 1) ∧
+    -16 < nafDigit a k ∧ nafDigit a k < 16
+
+/-- Table contract: the 8 entries are proven caches of the odd multiples
+    of A (naf_table_spec's post, bundled). -/
+def NafTableOf
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (A : EdPoint) : Prop :=
+  ∃ e0 e1 e2 e3 e4 e5 e6 e7,
+    tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
+    NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
+    NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
+    NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7
+
+/-! ### The loop induction -/
+
+/-- **The Straus loop body, by induction on the counter.** From any valid
+    on-curve accumulator r at counter j ≤ 256, the loop returns a valid
+    on-curve point denoting `dsmFold` of the remaining digits applied to
+    (projX r, projY r). One symbolic walk per induction step. -/
+theorem dsm_loop_loop_spec
+    (a_naf b_naf : Std.Array Std.I8 256#usize)
+    (ta tb : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (A B : EdPoint)
+    (hta : NafTableOf ta A) (htb : NafTableOf tb B)
+    (hda : NafDigits a_naf) (hdb : NafDigits b_naf)
+    (n : ℕ) :
+    ∀ (j : Usize) (r : ProjPoint), j.val = n → n ≤ 256 →
+    ProjValid r → OnCurve (projX r) (projY r) →
+    backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
+      a_naf b_naf ta tb r j ⦃ res =>
+        ProjValid res ∧ OnCurve (projX res) (projY res) ∧
+        (projX res, projY res) = dsmFold (nafDigit a_naf) (nafDigit b_naf)
+          (edPt A) (edPt B) (projX r, projY r) n ⦄ := by
+  obtain ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, hlA,
+    hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩ := hta
+  obtain ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, hlB,
+    hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩ := htb
+  induction n with
+  | zero =>
+    intro j r hj hle hv hc
+    unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
+    apply loop_step
+    simp only [backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop.body]
+    have hj0 : ¬ (j > 0#usize) := by clear * - hj; scalar_tac
+    rw [if_neg hj0]
+    try simp only [spec_ok]
+    exact ⟨hv, hc, rfl⟩
+  | succ n ih =>
+    intro j r hj hle hv hc
+    unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
+    apply loop_step
+    simp only [backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop.body]
+    have hjpos : j > 0#usize := by clear * - hj; scalar_tac
+    rw [if_pos hjpos]
+    -- idx ← j − 1
+    step as ⟨idx, hidx⟩
+    have hidxv : idx.val = n := by clear * - hidx hj; scalar_tac
+    -- t0 ← r.double()   (the projective doubling law)
+    step with (proj_double_law r hv hc) as
+      ⟨t0, t0bX, t0bY, t0bZ, t0bT, t0z, t0t, t0x, t0y⟩
+    have hct0 : OnCurve (complX t0) (complY t0) := by
+      rw [t0x, t0y]
+      exact edAdd_closure hc hc
+    -- da ← a_naf[idx]
+    step as ⟨da, hdav⟩
+    have hban : n < (↑a_naf : List Std.I8).length := by
+      clear * - hle; scalar_tac
+    have hdaq : da.val = nafDigit a_naf n := by
+      rw [hdav]
+      simp only [nafDigit, hidxv, getElem!_pos (↑a_naf : List Std.I8) n hban]
+    obtain ⟨hdA1, hdA2, hdA3⟩ := hda n (by omega)
+    -- t1 ← dsm_step_p t0 ta da
+    step with (dsm_step_p_law t0 ta da A eA0 eA1 eA2 eA3 eA4 eA5 eA6 eA7 hlA
+      hA0 hA1 hA2 hA3 hA4 hA5 hA6 hA7 t0bX t0bY t0bZ t0bT t0z t0t hct0
+      (by clear * - hdA1 hdaq; omega)
+      (by clear * - hdA2 hdaq; omega) (by clear * - hdA3 hdaq; omega)) as
+      ⟨t1, t1bX, t1bY, t1bZ, t1bT, t1z, t1t, hct1, ht1⟩
+    -- db ← b_naf[idx]
+    step as ⟨db, hdbv⟩
+    have hbbn : n < (↑b_naf : List Std.I8).length := by
+      clear * - hle; scalar_tac
+    have hdbq : db.val = nafDigit b_naf n := by
+      rw [hdbv]
+      simp only [nafDigit, hidxv, getElem!_pos (↑b_naf : List Std.I8) n hbbn]
+    obtain ⟨hdB1, hdB2, hdB3⟩ := hdb n (by omega)
+    -- t2 ← dsm_step_b t1 tb db
+    step with (dsm_step_b_law t1 tb db B eB0 eB1 eB2 eB3 eB4 eB5 eB6 eB7 hlB
+      hB0 hB1 hB2 hB3 hB4 hB5 hB6 hB7 t1bX t1bY t1bZ t1bT t1z t1t hct1
+      (by clear * - hdB1 hdbq; omega) (by clear * - hdB2 hdbq; omega)
+      (by clear * - hdB3 hdbq; omega)) as
+      ⟨t2, t2bX, t2bY, t2bZ, t2bT, t2z, t2t, hct2, ht2⟩
+    -- r1 ← t2.as_projective()
+    step with (compl_as_projective_law t2 t2bX t2bY t2bZ t2bT t2z t2t) as
+      ⟨r1, hr1v, hr1x, hr1y⟩
+    have hcr1 : OnCurve (projX r1) (projY r1) := by
+      rw [hr1x, hr1y]; exact hct2
+    -- the digit chain: (projPt r1) = edDigit_B (edDigit_A (edAdd P P))
+    have hchain : (projX r1, projY r1)
+        = edDigit (edPt B) (nafDigit b_naf n)
+            (edDigit (edPt A) (nafDigit a_naf n)
+              (edAdd (projX r, projY r) (projX r, projY r))) := by
+      have e1 : (complX t0, complY t0)
+          = edAdd (projX r, projY r) (projX r, projY r) := by
+        rw [Prod.ext_iff]; exact ⟨t0x, t0y⟩
+      have e2 : (projX r1, projY r1) = (complX t2, complY t2) := by
+        rw [Prod.ext_iff]; exact ⟨hr1x, hr1y⟩
+      rw [e2, ht2, hdbq, ht1, hdaq, e1]
+    try simp only [spec_ok]
+    -- close with the induction hypothesis at counter idx (= n)
+    apply spec_mono (ih idx r1 hidxv (by omega) hr1v hcr1)
+    intro res ⟨hv', hc', heq⟩
+    refine ⟨hv', hc', ?_⟩
+    rw [heq, hchain, dsmFold_succ]
+
+/-! ### The top-index constant and the public loop wrapper -/
+
+/-- `dsm_top_index` is the constant 255 (leading zero digits are identity
+    doublings — the source patch starts every walk at bit 255). -/
+theorem dsm_top_index_spec (a b : Std.Array Std.I8 256#usize) :
+    backend.serial.scalar_mul.vartime_double_base.dsm_top_index a b
+      ⦃ r => r = 255#usize ⦄ := by
+  unfold backend.serial.scalar_mul.vartime_double_base.dsm_top_index
+  simp [spec_ok]
+
+/-- **The full Straus loop**: from the identity, process all 256 digit
+    positions — the result denotes `dsmFold … edId 256`. -/
+theorem dsm_loop_spec (i : Usize) (hi : i.val = 255)
+    (a_naf b_naf : Std.Array Std.I8 256#usize)
+    (ta tb : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (A B : EdPoint)
+    (hta : NafTableOf ta A) (htb : NafTableOf tb B)
+    (hda : NafDigits a_naf) (hdb : NafDigits b_naf) :
+    backend.serial.scalar_mul.vartime_double_base.dsm_loop
+      i a_naf b_naf ta tb ⦃ res =>
+        ProjValid res ∧ OnCurve (projX res) (projY res) ∧
+        (projX res, projY res) = dsmFold (nafDigit a_naf) (nafDigit b_naf)
+          (edPt A) (edPt B) edId 256 ⦄ := by
+  obtain ⟨P0, hP0ok, hP0v, hP0x, hP0y⟩ := run_projective_identity
+  unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop
+  rw [hP0ok]
+  simp only [bind_tc_ok]
+  have hcP0 : OnCurve (projX P0) (projY P0) := by
+    rw [hP0x, hP0y]; exact onCurve_id
+  -- j ← i + 1  (= 256)
+  step as ⟨j, hj⟩
+  have hjv : j.val = 256 := by clear * - hj hi; scalar_tac
+  apply spec_mono (dsm_loop_loop_spec a_naf b_naf ta tb A B hta htb hda hdb
+    256 j P0 hjv (by omega) hP0v hcP0)
+  intro res ⟨hv, hc, heq⟩
+  refine ⟨hv, hc, ?_⟩
+  rw [heq, hP0x, hP0y]
+  rfl
+
+end CurveFieldProofs
diff --git a/verification/Proofs/DsmStepSpec.lean b/verification/Proofs/DsmStepSpec.lean
new file mode 100644
index 0000000..edb1a9a
--- /dev/null
+++ b/verification/Proofs/DsmStepSpec.lean
@@ -0,0 +1,315 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmStepSpec.lean — double-scalar-mul campaign, brick 2:
+   the per-digit step of the Straus/NAF loop.
+
+   vartime_double_base's loop body is
+       t = r.double();  t = dsm_step_p(t, table_a, a_naf[i]);
+       t = dsm_step_b(t, table_b, b_naf[i]);  r = t.as_projective();
+   This file proves the three non-loop ingredients as LAWS over the abstract
+   Edwards addition (computational layering, no associativity):
+
+   · `proj_double_law`      — ProjectivePoint::double denotes edAdd P P
+                              (lift of the coordinate-level proj_double_spec,
+                              same Z²-scaled linear_combination discipline as
+                              edwards_double_law's Z⁴ one).
+   · `compl_as_projective_law` — CompletedPoint::as_projective preserves the
+                              denoted affine point ((X:Z),(Y:T)) ↦ (XT:YZ:ZT).
+   · `naf_select_entry`     — select on a table with proven entries returns
+                              THE entry for the digit: NafEntryOf r A ((x−1)/2).
+   · `dsm_step_p_law`/`dsm_step_b_law` — the three-way digit step denotes
+                              `edDigit`: add the (+d)-th odd multiple, add the
+                              negation of the (−d)-th, or pass through.
+
+   The digit hypotheses (odd-or-zero, |d| < 16) are exactly what the NAF
+   digit spec will provide; they are taken as hypotheses here (layering).
+   ────────────────────────────────────────────────────────────────────────────── -/
+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
+
+/-! ### Projective coordinate plumbing -/
+
+/-- ⟪X⟫ = x·⟪Z⟫ for a projective point with ⟪Z⟫ ≠ 0 (x := projX). -/
+theorem proj_X_eq (p : ProjPoint) (hZ0 : ⟪p.Z⟫ ≠ 0) : ⟪p.X⟫ = projX p * ⟪p.Z⟫ := by
+  unfold projX
+  field_simp
+
+/-- ⟪Y⟫ = y·⟪Z⟫ for a projective point with ⟪Z⟫ ≠ 0 (y := projY). -/
+theorem proj_Y_eq (p : ProjPoint) (hZ0 : ⟪p.Z⟫ ≠ 0) : ⟪p.Y⟫ = projY p * ⟪p.Z⟫ := by
+  unfold projY
+  field_simp
+
+/-- **ProjectivePoint::double denotes the Edwards doubling law.**
+
+    MATH: for a valid projective point P on the curve, `double` returns a
+    completed point t with 2⁵⁴-bounded limbs, unit denominators, and
+        (complX t, complY t) = edAdd (projX P, projY P) (projX P, projY P).
+    Same derivation as `edwards_double_law` with Z² in place of Z⁴:
+    the curve equation turns Y²−X² into Z²·(1+D) and 2Z²−(Y²−X²) into
+    Z²·(1−D), both nonzero by completeness at the diagonal. -/
+theorem proj_double_law (p : ProjPoint) (hp : ProjValid p)
+    (hcp : OnCurve (projX p) (projY p)) :
+    backend.serial.curve_models.ProjectivePoint.double p ⦃ t =>
+      Bnd t.X (2^54) ∧ Bnd t.Y (2^54) ∧ Bnd t.Z (2^54) ∧ Bnd t.T (2^54) ∧
+      ⟪t.Z⟫ ≠ 0 ∧ ⟪t.T⟫ ≠ 0 ∧
+      complX t = (edAdd (projX p, projY p) (projX p, projY p)).1 ∧
+      complY t = (edAdd (projX p, projY p) (projX p, projY p)).2 ⦄ := by
+  apply spec_mono (proj_double_spec p hp)
+  rintro t ⟨hbX, hbY, hbZ, hbT, hvX, hvY, hvZ, hvT⟩
+  obtain ⟨-, -, -, hZ0⟩ := hp
+  obtain ⟨hp1, hm1⟩ := completeness hcp hcp
+  have hX := proj_X_eq p hZ0
+  have hY := proj_Y_eq p hZ0
+  have hZ2 : ⟪p.Z⟫^2 ≠ 0 := pow_ne_zero 2 hZ0
+  -- the curve equation in doubling-friendly form
+  have hcur : projY p ^ 2 - projX p ^ 2
+      = 1 + edD * projX p * projX p * projY p * projY p := by
+    have h := hcp
+    unfold OnCurve at h
+    linear_combination h
+  -- the four coordinates, Z²-scaled
+  have eX : ⟪t.X⟫ = ⟪p.Z⟫^2 * (projX p * projY p + projX p * projY p) := by
+    rw [hvX, hX, hY]; ring
+  have eY : ⟪t.Y⟫ = ⟪p.Z⟫^2 * (projY p * projY p + projX p * projX p) := by
+    rw [hvY, hX, hY]; ring
+  have eZ : ⟪t.Z⟫ = ⟪p.Z⟫^2 *
+      (1 + edD * projX p * projX p * projY p * projY p) := by
+    rw [hvZ, hX, hY]
+    linear_combination ⟪p.Z⟫^2 * hcur
+  have eT : ⟪t.T⟫ = ⟪p.Z⟫^2 *
+      (1 - edD * projX p * projX p * projY p * projY p) := by
+    rw [hvT, hX, hY]
+    linear_combination (-(⟪p.Z⟫^2)) * hcur
+  have hZne : ⟪t.Z⟫ ≠ 0 := by rw [eZ]; exact mul_ne_zero hZ2 hp1
+  have hTne : ⟪t.T⟫ ≠ 0 := by rw [eT]; exact mul_ne_zero hZ2 hm1
+  refine ⟨hbX.mono (by norm_num), hbY.mono (by norm_num),
+          hbZ.mono (by norm_num), hbT.mono (by norm_num), hZne, hTne, ?_, ?_⟩
+  · show ⟪t.X⟫ / ⟪t.Z⟫ = (projX p * projY p + projX p * projY p) /
+      (1 + edD * projX p * projX p * projY p * projY p)
+    rw [fp_div_eq_div_iff hZne hp1, eX, eZ]
+    ring
+  · show ⟪t.Y⟫ / ⟪t.T⟫ = (projY p * projY p + projX p * projX p) /
+      (1 - edD * projX p * projX p * projY p * projY p)
+    rw [fp_div_eq_div_iff hTne hm1, eY, eT]
+    ring
+
+/-- **CompletedPoint::as_projective preserves the denoted point.**
+
+    MATH: ((X:Z),(Y:T)) ↦ (XT : YZ : ZT) — with ⟪Z⟫,⟪T⟫ ≠ 0 the new
+    denominator ZT is a unit and XT/ZT = X/Z, YZ/ZT = Y/T. -/
+theorem compl_as_projective_law (p : ComplPoint)
+    (hbX : Bnd p.X (2^54)) (hbY : Bnd p.Y (2^54))
+    (hbZ : Bnd p.Z (2^54)) (hbT : Bnd p.T (2^54))
+    (hZ0 : ⟪p.Z⟫ ≠ 0) (hT0 : ⟪p.T⟫ ≠ 0) :
+    backend.serial.curve_models.CompletedPoint.as_projective p ⦃ r =>
+      ProjValid r ∧ projX r = complX p ∧ projY r = complY p ⦄ := by
+  unfold backend.serial.curve_models.CompletedPoint.as_projective
+  step with (mul_spec' _ _ hbX hbT) as ⟨fe, feb, fev⟩
+  step with (mul_spec' _ _ hbY hbZ) as ⟨fe1, fe1b, fe1v⟩
+  step with (mul_spec' _ _ hbZ hbT) as ⟨fe2, fe2b, fe2v⟩
+  try simp only [spec_ok]
+  refine ⟨⟨feb.mono (by norm_num), fe1b.mono (by norm_num),
+           fe2b.mono (by norm_num), ?_⟩, ?_, ?_⟩
+  · show ⟪fe2⟫ ≠ 0
+    rw [fe2v]; exact mul_ne_zero hZ0 hT0
+  · show ⟪fe⟫ / ⟪fe2⟫ = ⟪p.X⟫ / ⟪p.Z⟫
+    rw [fev, fe2v, mul_div_mul_right _ _ hT0]
+  · show ⟪fe1⟫ / ⟪fe2⟫ = ⟪p.Y⟫ / ⟪p.T⟫
+    rw [fe1v, fe2v, mul_comm ⟪p.Z⟫ ⟪p.T⟫, mul_div_mul_right _ _ hZ0]
+
+/-! ### Digit-indexed table lookup -/
+
+/-- select on a table with proven entries returns THE entry for the digit:
+    for odd x < 16, the result is a valid cache of the ((x−1)/2)-th odd
+    multiple of A. -/
+theorem naf_select_entry
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (x : Usize) (A : EdPoint)
+    (e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
+    (hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
+    (h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
+    (h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
+    (h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
+    (hodd : x.val % 2 = 1) (hlt : x.val < 16) :
+    window.NafLookupTable5.select
+      backend.serial.curve_models.ProjectiveNielsPoint.Insts.CoreMarkerCopy tbl x
+      ⦃ r => NafEntryOf r A ((x.val - 1) / 2) ⦄ := by
+  apply spec_mono (naf_select_spec tbl x e0 e1 e2 e3 e4 e5 e6 e7 hl hodd hlt)
+  rintro r ⟨i1, i3, i5, i7, i9, i11, i13, i15⟩
+  have hx : x.val = 1 ∨ x.val = 3 ∨ x.val = 5 ∨ x.val = 7 ∨ x.val = 9 ∨
+      x.val = 11 ∨ x.val = 13 ∨ x.val = 15 := by omega
+  rcases hx with hx | hx | hx | hx | hx | hx | hx | hx
+  · rw [i1 hx, hx]; exact h0
+  · rw [i3 hx, hx]; exact h1
+  · rw [i5 hx, hx]; exact h2
+  · rw [i7 hx, hx]; exact h3
+  · rw [i9 hx, hx]; exact h4
+  · rw [i11 hx, hx]; exact h5
+  · rw [i13 hx, hx]; exact h6
+  · rw [i15 hx, hx]; exact h7
+
+/-! ### The abstract digit step -/
+
+/-- One NAF digit's action on the accumulator: add the d-th odd multiple of
+    the base (d > 0), add its negation (d < 0), or pass through (d = 0) —
+    over the abstract `edAdd`, no associativity. -/
+noncomputable def edDigit (aPt : Fp × Fp) (d : ℤ) (P : Fp × Fp) : Fp × Fp :=
+  if 0 < d then edAdd P (edOdd ((d.toNat - 1) / 2) aPt)
+  else if d < 0 then edAdd P (edNeg (edOdd (((-d).toNat - 1) / 2) aPt))
+  else P
+
+/-- **The digit step denotes `edDigit`.**
+
+    Given a bounded, unit-denominator completed accumulator t denoting an
+    on-curve point, a table whose entries are proven caches of odd multiples
+    of A, and a NAF digit (odd or zero, |d| < 16): `dsm_step_p` returns a
+    completed point with the same validity shape denoting
+    `edDigit (edPt A) d.val (complX t, complY t)`. The `select` masserts
+    (panic freedom) are discharged, not assumed. -/
+theorem dsm_step_p_law (t : ComplPoint)
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (d : Std.I8) (A : EdPoint)
+    (e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
+    (hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
+    (h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
+    (h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
+    (h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
+    (hbX : Bnd t.X (2^54)) (hbY : Bnd t.Y (2^54))
+    (hbZ : Bnd t.Z (2^54)) (hbT : Bnd t.T (2^54))
+    (hZ0 : ⟪t.Z⟫ ≠ 0) (hT0 : ⟪t.T⟫ ≠ 0)
+    (hct : OnCurve (complX t) (complY t))
+    (hd : d.val = 0 ∨ d.val % 2 = 1) (hdlo : -16 < d.val) (hdhi : d.val < 16) :
+    backend.serial.scalar_mul.vartime_double_base.dsm_step_p t tbl d ⦃ r =>
+      Bnd r.X (2^54) ∧ Bnd r.Y (2^54) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^54) ∧
+      ⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
+      OnCurve (complX r) (complY r) ∧
+      (complX r, complY r) = edDigit (edPt A) d.val (complX t, complY t) ⦄ := by
+  unfold backend.serial.scalar_mul.vartime_double_base.dsm_step_p
+  split
+  · -- d > 0: add the d-th odd multiple
+    rename_i hdpos
+    have hdposv : (0:ℤ) < d.val := by clear * - hdpos; scalar_tac
+    -- ep ← t.as_extended
+    step with (compl_as_extended_law t hbX hbY hbZ hbT hZ0 hT0) as ⟨ep, hepv, hepx, hepy⟩
+    have hepc : OnCurveExt ep := by
+      show OnCurve (edX ep) (edY ep)
+      rw [hepx, hepy]; exact hct
+    have hept : edPt ep = (complX t, complY t) := by
+      calc edPt ep = (edX ep, edY ep) := rfl
+        _ = (complX t, complY t) := by rw [hepx, hepy]
+    -- i ← d as usize  (in-bounds: 0 < d < 16)
+    step with (IScalar.hcast_inBounds_spec .Usize d
+      (by clear * - hdposv hdhi; scalar_tac)) as ⟨i, hi⟩
+    have hiv : i.val = d.val.toNat := by clear * - hi hdposv; omega
+    have hiodd : i.val % 2 = 1 := by clear * - hiv hd hdposv; omega
+    have hilt : i.val < 16 := by clear * - hiv hdhi hdposv; omega
+    -- pnp ← select tbl i  (the ((i−1)/2)-th odd multiple's cache)
+    step with (naf_select_entry tbl i A e0 e1 e2 e3 e4 e5 e6 e7 hl
+      h0 h1 h2 h3 h4 h5 h6 h7 hiodd hilt) as ⟨pnp, hpnp⟩
+    obtain ⟨hpv, Q, hpn, hQv, hQc, hQpt⟩ := hpnp
+    -- r ← ep + pnp  (the mixed-add kernel law)
+    apply spec_mono (add_projniels_law ep pnp hpn hepv hQv hepc hQc hpv)
+    rintro r ⟨rbX, rbY, rbZ, rbT, rz, rt, rx, ry⟩
+    have hcr : OnCurve (complX r) (complY r) := by
+      rw [rx, ry]
+      exact edAdd_closure (show OnCurve (edX ep) (edY ep) from hepc)
+        (show OnCurve (edX Q) (edY Q) from hQc)
+    refine ⟨rbX.mono (by norm_num), rbY.mono (by norm_num), rbZ,
+            rbT.mono (by norm_num), rz, rt, hcr, ?_⟩
+    have hk : (i.val - 1) / 2 = (d.val.toNat - 1) / 2 := by
+      clear * - hiv; omega
+    simp only [edDigit, if_pos hdposv]
+    calc (complX r, complY r)
+        = ((edAdd (edPt ep) (edPt Q)).1, (edAdd (edPt ep) (edPt Q)).2) := by
+          rw [rx, ry]
+      _ = edAdd (edPt ep) (edPt Q) := rfl
+      _ = edAdd (complX t, complY t) (edOdd ((d.val.toNat - 1) / 2) (edPt A)) := by
+          rw [hept, hQpt, hk]
+  · -- d < 0 or d = 0
+    split
+    · -- d < 0: add the negation of the (−d)-th odd multiple
+      rename_i hdneg
+      have hdnegv : d.val < 0 := by clear * - hdneg; scalar_tac
+      -- ep ← t.as_extended
+      step with (compl_as_extended_law t hbX hbY hbZ hbT hZ0 hT0) as ⟨ep, hepv, hepx, hepy⟩
+      have hepc : OnCurveExt ep := by
+        show OnCurve (edX ep) (edY ep)
+        rw [hepx, hepy]; exact hct
+      have hept : edPt ep = (complX t, complY t) := by
+        calc edPt ep = (edX ep, edY ep) := rfl
+          _ = (complX t, complY t) := by rw [hepx, hepy]
+      -- i ← −d;  i1 ← i as usize
+      step as ⟨i, hi⟩
+      have hiv : i.val = -d.val := by clear * - hi hdnegv hdlo; scalar_tac
+      step with (IScalar.hcast_inBounds_spec .Usize i
+        (by clear * - hiv hdnegv hdlo; scalar_tac)) as ⟨i1, hi1⟩
+      have hi1v : i1.val = (-d.val).toNat := by clear * - hi1 hiv hdnegv; omega
+      have hiodd : i1.val % 2 = 1 := by clear * - hi1v hd hdnegv; omega
+      have hilt : i1.val < 16 := by clear * - hi1v hdlo hdnegv; omega
+      -- pnp ← select tbl i1
+      step with (naf_select_entry tbl i1 A e0 e1 e2 e3 e4 e5 e6 e7 hl
+        h0 h1 h2 h3 h4 h5 h6 h7 hiodd hilt) as ⟨pnp, hpnp⟩
+      obtain ⟨hpv, Q, hpn, hQv, hQc, hQpt⟩ := hpnp
+      -- r ← ep − pnp  (the mixed-sub kernel law)
+      apply spec_mono (sub_projniels_law ep pnp hpn hepv hQv hepc hQc hpv)
+      rintro r ⟨rbX, rbY, rbZ, rbT, rz, rt, rx, ry⟩
+      have hcr : OnCurve (complX r) (complY r) := by
+        rw [rx, ry]
+        exact edAdd_closure (show OnCurve (edX ep) (edY ep) from hepc)
+          (onCurve_neg (show OnCurve (edX Q) (edY Q) from hQc))
+      refine ⟨rbX.mono (by norm_num), rbY.mono (by norm_num),
+              rbZ.mono (by norm_num), rbT, rz, rt, hcr, ?_⟩
+      have hk : (i1.val - 1) / 2 = ((-d.val).toNat - 1) / 2 := by
+        clear * - hi1v; omega
+      have hnpos : ¬ ((0:ℤ) < d.val) := by clear * - hdnegv; omega
+      simp only [edDigit, if_neg hnpos, if_pos hdnegv]
+      calc (complX r, complY r)
+          = ((edAdd (edPt ep) (edNeg (edPt Q))).1,
+             (edAdd (edPt ep) (edNeg (edPt Q))).2) := by
+            rw [rx, ry]
+        _ = edAdd (edPt ep) (edNeg (edPt Q)) := rfl
+        _ = edAdd (complX t, complY t)
+              (edNeg (edOdd (((-d.val).toNat - 1) / 2) (edPt A))) := by
+            rw [hept, hQpt, hk]
+    · -- d = 0: pass through
+      rename_i hnpos hnneg
+      have h0v : d.val = 0 := by clear * - hnpos hnneg; scalar_tac
+      try simp only [spec_ok]
+      have hzero : ¬ ((0:ℤ) < d.val) ∧ ¬ (d.val < 0) := by
+        clear * - h0v; omega
+      refine ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hct, ?_⟩
+      simp only [edDigit, if_neg hzero.1, if_neg hzero.2]
+
+/-- `dsm_step_b` delegates to `dsm_step_p` (both tables are runtime
+    `NafLookupTable5<ProjectiveNielsPoint>` in this extraction). -/
+theorem dsm_step_b_law (t : ComplPoint)
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (d : Std.I8) (A : EdPoint)
+    (e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
+    (hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
+    (h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
+    (h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
+    (h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
+    (hbX : Bnd t.X (2^54)) (hbY : Bnd t.Y (2^54))
+    (hbZ : Bnd t.Z (2^54)) (hbT : Bnd t.T (2^54))
+    (hZ0 : ⟪t.Z⟫ ≠ 0) (hT0 : ⟪t.T⟫ ≠ 0)
+    (hct : OnCurve (complX t) (complY t))
+    (hd : d.val = 0 ∨ d.val % 2 = 1) (hdlo : -16 < d.val) (hdhi : d.val < 16) :
+    backend.serial.scalar_mul.vartime_double_base.dsm_step_b t tbl d ⦃ r =>
+      Bnd r.X (2^54) ∧ Bnd r.Y (2^54) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^54) ∧
+      ⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
+      OnCurve (complX r) (complY r) ∧
+      (complX r, complY r) = edDigit (edPt A) d.val (complX t, complY t) ⦄ := by
+  unfold backend.serial.scalar_mul.vartime_double_base.dsm_step_b
+  exact dsm_step_p_law t tbl d A e0 e1 e2 e3 e4 e5 e6 e7 hl
+    h0 h1 h2 h3 h4 h5 h6 h7 hbX hbY hbZ hbT hZ0 hT0 hct hd hdlo hdhi
+
+end CurveFieldProofs
diff --git a/verification/Proofs/DsmTableSpec.lean b/verification/Proofs/DsmTableSpec.lean
new file mode 100644
index 0000000..2b940b3
--- /dev/null
+++ b/verification/Proofs/DsmTableSpec.lean
@@ -0,0 +1,485 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/DsmTableSpec.lean — double-scalar-mul campaign, brick 1:
+   the NAF lookup-table construction  `NafLookupTable5::from(&A)`.
+
+   window.rs builds the odd-multiples table  [A, 3A, 5A, 7A, 9A, 11A, 13A, 15A]
+   (as ProjectiveNielsPoint caches):
+       Ai[0] = A.as_projective_niels();  A2 = A.double();
+       for i in 0..7 { Ai[i+1] = (A2 + Ai[i]).as_extended().as_projective_niels() }
+
+   SPEC (relational, computational layering — no associativity assumed):
+   entry k is a VALID niels cache of a valid on-curve point Q_k with
+       edPt Q_k = edOdd k (edPt A)
+   where `edOdd` is the abstract double-and-add recursion
+       edOdd 0 p = p,   edOdd (k+1) p = edAdd (edAdd p p) (edOdd k p)
+   — i.e. exactly the (2k+1)-fold sum the code computes, expressed over the
+   proven abstract Edwards addition `edAdd` (EdCurve). Composes the proven
+   group-layer laws: edwards_as_projective_niels_spec, edwards_double_law,
+   add_projniels_law, compl_as_extended_law (EdMain / EdConvert).
+
+   Loop-peel machinery (loop_step / range_next_*_spec) is the field layer's
+   (AddSpec.lean, same namespace) — this file imports only the CurveField
+   extraction tree.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.EdMain
+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
+
+/- Loop-peel machinery (loop_step / range_next_*_spec) comes from the
+   field layer's AddSpec.lean — already in this namespace via Proofs.EdMain. -/
+
+/-! ### The abstract odd-multiple recursion -/
+
+/-- `edOdd k p` is the double-and-add recursion the table loop computes:
+    p, then 2p+p, 2p+(3p), … — abstractly, the (2k+1)-th odd multiple,
+    expressed over `edAdd` WITHOUT assuming associativity (computational
+    layering; the group-semantics reading is phase 2 of the campaign). -/
+noncomputable def edOdd : ℕ → Fp × Fp → Fp × Fp
+  | 0, p => p
+  | k + 1, p => edAdd (edAdd p p) (edOdd k p)
+
+@[simp] theorem edOdd_zero (p : Fp × Fp) : edOdd 0 p = p := rfl
+
+theorem edOdd_succ (k : ℕ) (p : Fp × Fp) :
+    edOdd (k + 1) p = edAdd (edAdd p p) (edOdd k p) := rfl
+
+/-- Entry contract of the NAF table: a valid niels cache of a valid,
+    on-curve point denoting the k-th odd multiple of A. -/
+def NafEntryOf (e : backend.serial.curve_models.ProjectiveNielsPoint) (A : EdPoint) (k : ℕ) : Prop :=
+  ProjNielsValid e ∧ ∃ Q : EdPoint, IsNielsOf e Q ∧ ExtValid Q ∧
+    OnCurveExt Q ∧ edPt Q = edOdd k (edPt A)
+
+/-- The entry list of a `NafLookupTable5` (the type is a transparent
+    synonym for `Array ProjectiveNielsPoint 8`). -/
+def tblEntries
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint) : List backend.serial.curve_models.ProjectiveNielsPoint :=
+  Subtype.val (tbl : Std.Array backend.serial.curve_models.ProjectiveNielsPoint 8#usize)
+
+/-! ### The table-construction loop: 7 concrete peels -/
+
+/-- The `from` loop: starting from `[cache(A)]*8`, after 7 iterations entry k
+    holds a valid cache of the k-th odd multiple, for every k ≤ 7. -/
+theorem naf_table_loop_spec (A A2 : EdPoint)
+    (Ai : Std.Array backend.serial.curve_models.ProjectiveNielsPoint 8#usize) (n0 : backend.serial.curve_models.ProjectiveNielsPoint)
+    (hl0 : (↑Ai : List backend.serial.curve_models.ProjectiveNielsPoint) = [n0, n0, n0, n0, n0, n0, n0, n0])
+    (hn0v : ProjNielsValid n0) (hn0n : IsNielsOf n0 A)
+    (hAv : ExtValid A) (hAc : OnCurveExt A)
+    (hA2v : ExtValid A2) (hA2c : OnCurveExt A2)
+    (hA2pt : edPt A2 = edAdd (edPt A) (edPt A)) :
+    window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop
+      { start := 0#usize, «end» := 7#usize } Ai A2
+      ⦃ arr => ∃ e0 e1 e2 e3 e4 e5 e6 e7,
+          (↑arr : List backend.serial.curve_models.ProjectiveNielsPoint) = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
+          NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
+          NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
+          NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7 ⦄ := by
+  have hq0pt : edPt A = edOdd 0 (edPt A) := rfl
+  unfold window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop
+  -- ── iteration 0: read entry 0 (cache of q0), write entry 1 = cache of 2A + q0
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with range_next_lt_spec as ⟨o0, iter0, ho0, hs0, he0⟩
+  simp only [ho0]
+  have hsv0 : iter0.start.val = 1 := by clear * - hs0; omega
+  have hev0 : iter0.«end».val = 7 := by clear * - he0; scalar_tac
+  -- entry 0 out of the array
+  step as ⟨e0x, he0x⟩
+  simp [hl0] at he0x
+  rw [he0x]
+  -- cp ← A2 + n0   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n0 hn0n hA2v hAv hA2c hAc hn0v) as
+    ⟨cp0, cb0X, cb0Y, cb0Z, cb0T, cz0, ct0, cx0, cy0⟩
+  -- q1 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp0 (cb0X.mono (by norm_num))
+    (cb0Y.mono (by norm_num)) cb0Z (cb0T.mono (by norm_num)) cz0 ct0) as
+    ⟨q1, hq1v, hq1x, hq1y⟩
+  have hq1c : OnCurveExt q1 := by
+    show OnCurve (edX q1) (edY q1)
+    rw [hq1x, cx0, hq1y, cy0]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX A) (edY A) from hAc)
+  have hq1pt : edPt q1 = edOdd 1 (edPt A) := by
+    have h : edPt q1 = edAdd (edPt A2) (edPt A) := by
+      calc edPt q1 = (edX q1, edY q1) := rfl
+        _ = ((edAdd (edPt A2) (edPt A)).1, (edAdd (edPt A2) (edPt A)).2) := by
+            rw [hq1x, cx0, hq1y, cy0]
+        _ = edAdd (edPt A2) (edPt A) := rfl
+    rw [h, hA2pt, hq0pt]
+    rfl
+  -- n1 ← q1.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q1 hq1v) as ⟨n1, hn1v, hn1n⟩
+  -- write it at index 1
+  step as ⟨j0, hj0⟩
+  have hj0v : j0 = 1#usize := by clear * - hj0; scalar_tac
+  rw [hj0v]
+  step as ⟨Ai1, hA1⟩
+  have hl1 : (↑Ai1 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n0, n0, n0, n0, n0, n0] := by
+    simp only [hA1, Array.set_val_eq, hl0]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 1: read entry 1 (cache of q1), write entry 2 = cache of 2A + q1
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter0 (by clear * - hsv0 hev0; scalar_tac)) as ⟨o1, iter1, ho1, hs1, he1⟩
+  simp only [ho1]
+  have hsv1 : iter1.start.val = 2 := by clear * - hs1 hsv0; omega
+  have hev1 : iter1.«end».val = 7 := by clear * - he1 hev0; scalar_tac
+  have hidx1 : iter0.start = 1#usize := by clear * - hsv0; scalar_tac
+  rw [hidx1]
+  -- entry 1 out of the array
+  step as ⟨e1x, he1x⟩
+  simp [hl1] at he1x
+  rw [he1x]
+  -- cp ← A2 + n1   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n1 hn1n hA2v hq1v hA2c hq1c hn1v) as
+    ⟨cp1, cb1X, cb1Y, cb1Z, cb1T, cz1, ct1, cx1, cy1⟩
+  -- q2 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp1 (cb1X.mono (by norm_num))
+    (cb1Y.mono (by norm_num)) cb1Z (cb1T.mono (by norm_num)) cz1 ct1) as
+    ⟨q2, hq2v, hq2x, hq2y⟩
+  have hq2c : OnCurveExt q2 := by
+    show OnCurve (edX q2) (edY q2)
+    rw [hq2x, cx1, hq2y, cy1]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q1) (edY q1) from hq1c)
+  have hq2pt : edPt q2 = edOdd 2 (edPt A) := by
+    have h : edPt q2 = edAdd (edPt A2) (edPt q1) := by
+      calc edPt q2 = (edX q2, edY q2) := rfl
+        _ = ((edAdd (edPt A2) (edPt q1)).1, (edAdd (edPt A2) (edPt q1)).2) := by
+            rw [hq2x, cx1, hq2y, cy1]
+        _ = edAdd (edPt A2) (edPt q1) := rfl
+    rw [h, hA2pt, hq1pt]
+    rfl
+  -- n2 ← q2.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q2 hq2v) as ⟨n2, hn2v, hn2n⟩
+  -- write it at index 2
+  step as ⟨j1, hj1⟩
+  have hj1v : j1 = 2#usize := by clear * - hj1; scalar_tac
+  rw [hj1v]
+  step as ⟨Ai2, hA2⟩
+  have hl2 : (↑Ai2 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n0, n0, n0, n0, n0] := by
+    simp only [hA2, Array.set_val_eq, hl1]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 2: read entry 2 (cache of q2), write entry 3 = cache of 2A + q2
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter1 (by clear * - hsv1 hev1; scalar_tac)) as ⟨o2, iter2, ho2, hs2, he2⟩
+  simp only [ho2]
+  have hsv2 : iter2.start.val = 3 := by clear * - hs2 hsv1; omega
+  have hev2 : iter2.«end».val = 7 := by clear * - he2 hev1; scalar_tac
+  have hidx2 : iter1.start = 2#usize := by clear * - hsv1; scalar_tac
+  rw [hidx2]
+  -- entry 2 out of the array
+  step as ⟨e2x, he2x⟩
+  simp [hl2] at he2x
+  rw [he2x]
+  -- cp ← A2 + n2   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n2 hn2n hA2v hq2v hA2c hq2c hn2v) as
+    ⟨cp2, cb2X, cb2Y, cb2Z, cb2T, cz2, ct2, cx2, cy2⟩
+  -- q3 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp2 (cb2X.mono (by norm_num))
+    (cb2Y.mono (by norm_num)) cb2Z (cb2T.mono (by norm_num)) cz2 ct2) as
+    ⟨q3, hq3v, hq3x, hq3y⟩
+  have hq3c : OnCurveExt q3 := by
+    show OnCurve (edX q3) (edY q3)
+    rw [hq3x, cx2, hq3y, cy2]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q2) (edY q2) from hq2c)
+  have hq3pt : edPt q3 = edOdd 3 (edPt A) := by
+    have h : edPt q3 = edAdd (edPt A2) (edPt q2) := by
+      calc edPt q3 = (edX q3, edY q3) := rfl
+        _ = ((edAdd (edPt A2) (edPt q2)).1, (edAdd (edPt A2) (edPt q2)).2) := by
+            rw [hq3x, cx2, hq3y, cy2]
+        _ = edAdd (edPt A2) (edPt q2) := rfl
+    rw [h, hA2pt, hq2pt]
+    rfl
+  -- n3 ← q3.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q3 hq3v) as ⟨n3, hn3v, hn3n⟩
+  -- write it at index 3
+  step as ⟨j2, hj2⟩
+  have hj2v : j2 = 3#usize := by clear * - hj2; scalar_tac
+  rw [hj2v]
+  step as ⟨Ai3, hA3⟩
+  have hl3 : (↑Ai3 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n3, n0, n0, n0, n0] := by
+    simp only [hA3, Array.set_val_eq, hl2]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 3: read entry 3 (cache of q3), write entry 4 = cache of 2A + q3
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter2 (by clear * - hsv2 hev2; scalar_tac)) as ⟨o3, iter3, ho3, hs3, he3⟩
+  simp only [ho3]
+  have hsv3 : iter3.start.val = 4 := by clear * - hs3 hsv2; omega
+  have hev3 : iter3.«end».val = 7 := by clear * - he3 hev2; scalar_tac
+  have hidx3 : iter2.start = 3#usize := by clear * - hsv2; scalar_tac
+  rw [hidx3]
+  -- entry 3 out of the array
+  step as ⟨e3x, he3x⟩
+  simp [hl3] at he3x
+  rw [he3x]
+  -- cp ← A2 + n3   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n3 hn3n hA2v hq3v hA2c hq3c hn3v) as
+    ⟨cp3, cb3X, cb3Y, cb3Z, cb3T, cz3, ct3, cx3, cy3⟩
+  -- q4 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp3 (cb3X.mono (by norm_num))
+    (cb3Y.mono (by norm_num)) cb3Z (cb3T.mono (by norm_num)) cz3 ct3) as
+    ⟨q4, hq4v, hq4x, hq4y⟩
+  have hq4c : OnCurveExt q4 := by
+    show OnCurve (edX q4) (edY q4)
+    rw [hq4x, cx3, hq4y, cy3]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q3) (edY q3) from hq3c)
+  have hq4pt : edPt q4 = edOdd 4 (edPt A) := by
+    have h : edPt q4 = edAdd (edPt A2) (edPt q3) := by
+      calc edPt q4 = (edX q4, edY q4) := rfl
+        _ = ((edAdd (edPt A2) (edPt q3)).1, (edAdd (edPt A2) (edPt q3)).2) := by
+            rw [hq4x, cx3, hq4y, cy3]
+        _ = edAdd (edPt A2) (edPt q3) := rfl
+    rw [h, hA2pt, hq3pt]
+    rfl
+  -- n4 ← q4.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q4 hq4v) as ⟨n4, hn4v, hn4n⟩
+  -- write it at index 4
+  step as ⟨j3, hj3⟩
+  have hj3v : j3 = 4#usize := by clear * - hj3; scalar_tac
+  rw [hj3v]
+  step as ⟨Ai4, hA4⟩
+  have hl4 : (↑Ai4 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n3, n4, n0, n0, n0] := by
+    simp only [hA4, Array.set_val_eq, hl3]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 4: read entry 4 (cache of q4), write entry 5 = cache of 2A + q4
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter3 (by clear * - hsv3 hev3; scalar_tac)) as ⟨o4, iter4, ho4, hs4, he4⟩
+  simp only [ho4]
+  have hsv4 : iter4.start.val = 5 := by clear * - hs4 hsv3; omega
+  have hev4 : iter4.«end».val = 7 := by clear * - he4 hev3; scalar_tac
+  have hidx4 : iter3.start = 4#usize := by clear * - hsv3; scalar_tac
+  rw [hidx4]
+  -- entry 4 out of the array
+  step as ⟨e4x, he4x⟩
+  simp [hl4] at he4x
+  rw [he4x]
+  -- cp ← A2 + n4   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n4 hn4n hA2v hq4v hA2c hq4c hn4v) as
+    ⟨cp4, cb4X, cb4Y, cb4Z, cb4T, cz4, ct4, cx4, cy4⟩
+  -- q5 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp4 (cb4X.mono (by norm_num))
+    (cb4Y.mono (by norm_num)) cb4Z (cb4T.mono (by norm_num)) cz4 ct4) as
+    ⟨q5, hq5v, hq5x, hq5y⟩
+  have hq5c : OnCurveExt q5 := by
+    show OnCurve (edX q5) (edY q5)
+    rw [hq5x, cx4, hq5y, cy4]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q4) (edY q4) from hq4c)
+  have hq5pt : edPt q5 = edOdd 5 (edPt A) := by
+    have h : edPt q5 = edAdd (edPt A2) (edPt q4) := by
+      calc edPt q5 = (edX q5, edY q5) := rfl
+        _ = ((edAdd (edPt A2) (edPt q4)).1, (edAdd (edPt A2) (edPt q4)).2) := by
+            rw [hq5x, cx4, hq5y, cy4]
+        _ = edAdd (edPt A2) (edPt q4) := rfl
+    rw [h, hA2pt, hq4pt]
+    rfl
+  -- n5 ← q5.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q5 hq5v) as ⟨n5, hn5v, hn5n⟩
+  -- write it at index 5
+  step as ⟨j4, hj4⟩
+  have hj4v : j4 = 5#usize := by clear * - hj4; scalar_tac
+  rw [hj4v]
+  step as ⟨Ai5, hA5⟩
+  have hl5 : (↑Ai5 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n3, n4, n5, n0, n0] := by
+    simp only [hA5, Array.set_val_eq, hl4]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 5: read entry 5 (cache of q5), write entry 6 = cache of 2A + q5
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter4 (by clear * - hsv4 hev4; scalar_tac)) as ⟨o5, iter5, ho5, hs5, he5⟩
+  simp only [ho5]
+  have hsv5 : iter5.start.val = 6 := by clear * - hs5 hsv4; omega
+  have hev5 : iter5.«end».val = 7 := by clear * - he5 hev4; scalar_tac
+  have hidx5 : iter4.start = 5#usize := by clear * - hsv4; scalar_tac
+  rw [hidx5]
+  -- entry 5 out of the array
+  step as ⟨e5x, he5x⟩
+  simp [hl5] at he5x
+  rw [he5x]
+  -- cp ← A2 + n5   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n5 hn5n hA2v hq5v hA2c hq5c hn5v) as
+    ⟨cp5, cb5X, cb5Y, cb5Z, cb5T, cz5, ct5, cx5, cy5⟩
+  -- q6 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp5 (cb5X.mono (by norm_num))
+    (cb5Y.mono (by norm_num)) cb5Z (cb5T.mono (by norm_num)) cz5 ct5) as
+    ⟨q6, hq6v, hq6x, hq6y⟩
+  have hq6c : OnCurveExt q6 := by
+    show OnCurve (edX q6) (edY q6)
+    rw [hq6x, cx5, hq6y, cy5]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q5) (edY q5) from hq5c)
+  have hq6pt : edPt q6 = edOdd 6 (edPt A) := by
+    have h : edPt q6 = edAdd (edPt A2) (edPt q5) := by
+      calc edPt q6 = (edX q6, edY q6) := rfl
+        _ = ((edAdd (edPt A2) (edPt q5)).1, (edAdd (edPt A2) (edPt q5)).2) := by
+            rw [hq6x, cx5, hq6y, cy5]
+        _ = edAdd (edPt A2) (edPt q5) := rfl
+    rw [h, hA2pt, hq5pt]
+    rfl
+  -- n6 ← q6.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q6 hq6v) as ⟨n6, hn6v, hn6n⟩
+  -- write it at index 6
+  step as ⟨j5, hj5⟩
+  have hj5v : j5 = 6#usize := by clear * - hj5; scalar_tac
+  rw [hj5v]
+  step as ⟨Ai6, hA6⟩
+  have hl6 : (↑Ai6 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n3, n4, n5, n6, n0] := by
+    simp only [hA6, Array.set_val_eq, hl5]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 6: read entry 6 (cache of q6), write entry 7 = cache of 2A + q6
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_lt_spec iter5 (by clear * - hsv5 hev5; scalar_tac)) as ⟨o6, iter6, ho6, hs6, he6⟩
+  simp only [ho6]
+  have hsv6 : iter6.start.val = 7 := by clear * - hs6 hsv5; omega
+  have hev6 : iter6.«end».val = 7 := by clear * - he6 hev5; scalar_tac
+  have hidx6 : iter5.start = 6#usize := by clear * - hsv5; scalar_tac
+  rw [hidx6]
+  -- entry 6 out of the array
+  step as ⟨e6x, he6x⟩
+  simp [hl6] at he6x
+  rw [he6x]
+  -- cp ← A2 + n6   (the mixed-add kernel law)
+  step with (add_projniels_law A2 n6 hn6n hA2v hq6v hA2c hq6c hn6v) as
+    ⟨cp6, cb6X, cb6Y, cb6Z, cb6T, cz6, ct6, cx6, cy6⟩
+  -- q7 ← cp.as_extended   (valid extended point denoting the sum)
+  step with (compl_as_extended_law cp6 (cb6X.mono (by norm_num))
+    (cb6Y.mono (by norm_num)) cb6Z (cb6T.mono (by norm_num)) cz6 ct6) as
+    ⟨q7, hq7v, hq7x, hq7y⟩
+  have hq7c : OnCurveExt q7 := by
+    show OnCurve (edX q7) (edY q7)
+    rw [hq7x, cx6, hq7y, cy6]
+    exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
+      (show OnCurve (edX q6) (edY q6) from hq6c)
+  have hq7pt : edPt q7 = edOdd 7 (edPt A) := by
+    have h : edPt q7 = edAdd (edPt A2) (edPt q6) := by
+      calc edPt q7 = (edX q7, edY q7) := rfl
+        _ = ((edAdd (edPt A2) (edPt q6)).1, (edAdd (edPt A2) (edPt q6)).2) := by
+            rw [hq7x, cx6, hq7y, cy6]
+        _ = edAdd (edPt A2) (edPt q6) := rfl
+    rw [h, hA2pt, hq6pt]
+    rfl
+  -- n7 ← q7.as_projective_niels   (the new table entry)
+  step with (edwards_as_projective_niels_spec q7 hq7v) as ⟨n7, hn7v, hn7n⟩
+  -- write it at index 7
+  step as ⟨j6, hj6⟩
+  have hj6v : j6 = 7#usize := by clear * - hj6; scalar_tac
+  rw [hj6v]
+  step as ⟨Ai7, hA7⟩
+  have hl7 : (↑Ai7 : List backend.serial.curve_models.ProjectiveNielsPoint)
+      = [n0, n1, n2, n3, n4, n5, n6, n7] := by
+    simp only [hA7, Array.set_val_eq, hl6]
+    rfl
+  try simp only [spec_ok]
+  -- ── iteration 7: range exhausted (start = end = 7) — done
+  apply loop_step
+  simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
+  step with (range_next_ge_spec iter6 (by clear * - hsv6 hev6; scalar_tac)) as ⟨o7, iter7, ho7, hr7⟩
+  simp only [ho7]
+  try simp only [spec_ok]
+  refine ⟨n0, n1, n2, n3, n4, n5, n6, n7, hl7, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · exact ⟨hn0v, A, hn0n, hAv, hAc, hq0pt⟩
+  · exact ⟨hn1v, q1, hn1n, hq1v, hq1c, hq1pt⟩
+  · exact ⟨hn2v, q2, hn2n, hq2v, hq2c, hq2pt⟩
+  · exact ⟨hn3v, q3, hn3n, hq3v, hq3c, hq3pt⟩
+  · exact ⟨hn4v, q4, hn4n, hq4v, hq4c, hq4pt⟩
+  · exact ⟨hn5v, q5, hn5n, hq5v, hq5c, hq5pt⟩
+  · exact ⟨hn6v, q6, hn6n, hq6v, hq6c, hq6pt⟩
+  · exact ⟨hn7v, q7, hn7n, hq7v, hq7c, hq7pt⟩
+
+/-! ### The public table-construction spec -/
+
+/-- **NafLookupTable5::from(&A)**: for a valid on-curve A, the table's 8
+    entries are valid niels caches of valid on-curve points denoting
+    A, 3A, 5A, …, 15A — the odd multiples as `edOdd` values over the
+    proven abstract Edwards addition. -/
+theorem naf_table_spec (A : EdPoint) (hA : ExtValid A) (hcA : OnCurveExt A) :
+    window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from A
+      ⦃ tbl => ∃ e0 e1 e2 e3 e4 e5 e6 e7,
+          tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
+          NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
+          NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
+          NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7 ⦄ := by
+  unfold window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from
+  step with (edwards_as_projective_niels_spec A hA) as ⟨pnp, hpv, hpn⟩
+  step with (edwards_double_law A hA hcA) as ⟨A2, hA2v, hA2c, hA2pt⟩
+  step with (naf_table_loop_spec A A2 (Array.repeat 8#usize pnp) pnp
+      (by simp [List.replicate]) hpv hpn hA hcA hA2v hA2c hA2pt) as
+    ⟨e0, e1, e2, e3, e4, e5, e6, e7, tblA, hl, h0, h1, h2, h3, h4, h5, h6, h7⟩
+  try simp only [spec_ok]
+  exact ⟨e0, e1, e2, e3, e4, e5, e6, e7, hl, h0, h1, h2, h3, h4, h5, h6, h7⟩
+
+
+/-! ### The table lookup -/
+
+/-- **NafLookupTable5::select(x)** for odd x < 16: returns entry x/2 —
+    enumerated per digit so downstream digit case-splits use it directly.
+    The two `massert`s (x odd, x < 16) are DISCHARGED, certifying the
+    absence of the lookup panic paths. -/
+theorem naf_select_spec
+    (tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
+    (x : Usize)
+    (e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
+    (hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
+    (hodd : x.val % 2 = 1) (hlt : x.val < 16) :
+    window.NafLookupTable5.select
+      backend.serial.curve_models.ProjectiveNielsPoint.Insts.CoreMarkerCopy tbl x
+      ⦃ r => (x.val = 1 → r = e0) ∧ (x.val = 3 → r = e1) ∧ (x.val = 5 → r = e2) ∧
+             (x.val = 7 → r = e3) ∧ (x.val = 9 → r = e4) ∧ (x.val = 11 → r = e5) ∧
+             (x.val = 13 → r = e6) ∧ (x.val = 15 → r = e7) ⦄ := by
+  unfold window.NafLookupTable5.select
+  step as ⟨lv, hlv⟩
+  have hlv1 : lv = 1#usize := by
+    clear * - hlv hodd
+    have h1 : x.val &&& 1 = 1 := by rw [Nat.and_one_is_mod, hodd]
+    scalar_tac
+  step with (massert_spec _ hlv1) as ⟨hu1⟩
+  step with (massert_spec (x < 16#usize) (by clear * - hlt; scalar_tac)) as ⟨hu2⟩
+  step as ⟨i, hi⟩
+  step as ⟨r, hr⟩
+  simp only [tblEntries] at hl
+  simp [hl] at hr
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> intro hx
+  · have hik : i.val = 0 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 1 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 2 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 3 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 4 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 5 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 6 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+  · have hik : i.val = 7 := by clear * - hi hx; omega
+    rw [hr]; simp [hik]
+
+end CurveFieldProofs
diff --git a/verification/check.sh b/verification/check.sh
index b8e1b35..9630f08 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -52,16 +52,29 @@ PROOFS=(
   EdAddAffNiels
   EdConvert
   EdMain
+  DsmTableSpec
+  DsmStepSpec
+  DsmLoopSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
   CurveFieldProofs.fieldImplementation
   CurveFieldProofs.edwardsImplementation
+  CurveFieldProofs.naf_table_spec
+  CurveFieldProofs.naf_select_spec
+  CurveFieldProofs.proj_double_law
+  CurveFieldProofs.compl_as_projective_law
+  CurveFieldProofs.dsm_step_p_law
+  CurveFieldProofs.dsm_step_b_law
+  CurveFieldProofs.dsm_loop_spec
 )
 # Imports needed so every certificate in CERTS is in scope for the audit.
 AUDIT_IMPORTS=(
   Proofs.FieldMain
   Proofs.EdMain
+  Proofs.DsmTableSpec
+  Proofs.DsmStepSpec
+  Proofs.DsmLoopSpec
 )
 
 # ── Phase 0: resource + integrity guards ────────────────────────────────────