Add scalar-layer foundation (Scalar52 arithmetic mod ℓ)

Transpile the Scalar52 limb backend (backend::serial::u64::scalar add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas, scoped at the function level to the iterator-free arithmetic core. - verification/extract-scalar.sh: function-level Charon/Aeneas extraction. This fork (v4.1.3) inlines a local `black_box` (a volatile read used as an optimization barrier) inside Scalar52::sub; charon cannot translate the `&raw const` it lowers to, so it is marked --opaque and modeled below. - verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (27 defs) - verification/gen/CurveScalar/FunsExternal.lean: hand-written model of Scalar52::sub::black_box as the identity on u64 (a volatile read returns the value written; the qualifier is only an optimization barrier). TypesExternal.lean is decl-free — this fork pulls in no external types (unlike v5 dalek, which routes sub through subtle::Choice). - verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52 denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled constants::L denotes exactly the group order ℓ, kernel-checked). - verification/check-scalar.sh: guarded compile of the gen modules plus the denotation foundation. check-scalar.sh passes: gen compiles; denotation + L = ℓ proven. add/sub/mul remain in progress. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-09-03 19:53:45 +00:00 · 2026-07-02 21:24:39 +02:00 · 2026-07-02 21:24:39 +02:00 · 6fe31be80d
commit 6fe31be80d
parent d3f7359832
10 changed files with 877 additions and 1 deletions
--- a/README.md
+++ b/README.md
@ -27,7 +27,7 @@ in this repository.
 |-------|-------------|--------|-----------------------|
 | Field 𝔽_p          | `fieldImplementation`    | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Group law (Edwards) | `edwardsImplementation`  | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
-| Scalar mod ℓ        | `scalarImplementation`   | ⏳ in progress | — |
+| Scalar mod ℓ        | `scalarImplementation`   | 🔨 foundation | denotation + L=ℓ proven; add/sub/mul in progress |
 | Signature (EdDSA)   | `verifyEquation`          | ⏳ in progress | — |

 Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
--- a/verification/CurveScalar.llbc
+++ b/verification/CurveScalar.llbc
--- a/verification/Proofs/ScalarDenote.lean
+++ b/verification/Proofs/ScalarDenote.lean
@ -0,0 +1,90 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/ScalarDenote.lean — SEMANTIC FOUNDATION for the scalar layer:
+   from Scalar52 machine limbs to ℤ/ℓℤ, ℓ the ed25519 group order.
+
+   WHAT THIS FILE PROVIDES
+   * `Ell` — the group order ℓ = 2²⁵² + 27742317777372353535851937790883648493
+     (a prime; the order of the ed25519 basepoint).
+   * `Sc := Scalar52` — the transpiled type: 5 little-endian 52-bit-limbed u64s
+     (`Array U64 5`; each limb < 2⁵² by the crate's representation invariant).
+   * `scVal`/`scLimbs` — the exact ℕ value Σ lᵢ·2^(52i).
+   * `ScBnd` — the limb-bound invariant (all limbs < 2⁵²).
+   * `scDenote` (⟦·⟧) — the denotation Scalar52 → ZMod ℓ.
+   * `L_val` — the transpiled `constants::L` denotes exactly ℓ (kernel-checked).
+
+   RUST ANALOG: `src/backend/serial/u64/scalar.rs` — `pub struct Scalar52(pub [u64; 5])`,
+   invariant "5 limbs of 52 bits each, value < ℓ after reduction".
+
+   SCOPE NOTE. This file + the add/sub specs are the tractable core. The
+   Montgomery multiplication path (`mul_internal` → `montgomery_reduce`) shares
+   the 4×64-Montgomery big-coefficient structure that overflows the Lean kernel
+   in the pasta field layer (documented in that repo's POSTMORTEM); it is built
+   the same isolated-lemma way but is not yet complete.
+
+   Imports: gen/CurveScalar (the transpiled Scalar52 arithmetic).
+   ────────────────────────────────────────────────────────────────────────────── -/
+import CurveScalar.Funs
+open Aeneas Aeneas.Std Result
+open curve25519_dalek
+
+namespace ScalarProofs
+
+/-- The ed25519 group order ℓ = 2²⁵² + 27742317777372353535851937790883648493. -/
+def Ell : ℕ := 7237005577332262213973186563042994240857116359379907606001950938285454250989
+
+/-- The transpiled Scalar52 element type (5 little-endian 52-bit limbs). -/
+abbrev Sc := backend.serial.u64.scalar.Scalar52
+
+/-- Exact ℕ value of five little-endian 52-bit limbs. -/
+def scLimbs (a0 a1 a2 a3 a4 : U64) : ℕ :=
+  a0.val + 2^52 * a1.val + 2^104 * a2.val + 2^156 * a3.val + 2^208 * a4.val
+
+/-- Exact ℕ value of a `Scalar52`. -/
+def scVal (a : Sc) : ℕ :=
+  match (↑a : List U64) with
+  | [a0, a1, a2, a3, a4] => scLimbs a0 a1 a2 a3 a4
+  | _ => 0
+
+/-- Every `Scalar52` IS five named u64 limbs. -/
+theorem Sc.exists_limbs (a : Sc) :
+    ∃ a0 a1 a2 a3 a4 : U64, (↑a : List U64) = [a0, a1, a2, a3, a4] := by
+  obtain ⟨l, hl⟩ := a
+  match l, hl with
+  | [a0, a1, a2, a3, a4], _ => exact ⟨a0, a1, a2, a3, a4, rfl⟩
+
+@[simp]
+theorem scVal_eq (a : Sc) (a0 a1 a2 a3 a4 : U64)
+    (h : (↑a : List U64) = [a0, a1, a2, a3, a4]) :
+    scVal a = scLimbs a0 a1 a2 a3 a4 := by
+  unfold scVal; rw [h]
+
+/-- The limb discipline: every limb below 2⁵² (52-bit limbs). -/
+def ScBnd (a : Sc) : Prop :=
+  ∃ a0 a1 a2 a3 a4 : U64, (↑a : List U64) = [a0, a1, a2, a3, a4] ∧
+    a0.val < 2^52 ∧ a1.val < 2^52 ∧ a2.val < 2^52 ∧ a3.val < 2^52 ∧ a4.val < 2^52
+
+/-- The denotation: machine limbs ↦ ℤ/ℓℤ. -/
+def scDenote (a : Sc) : ZMod Ell := (scVal a : ZMod Ell)
+
+notation "⟦" a "⟧" => scDenote a
+
+/-- The transpiled `constants::L` as a limb list. -/
+theorem L_limbs :
+    (↑backend.serial.u64.constants.L : List U64) =
+      [671914833335277#u64, 3916664325105025#u64, 1367801#u64, 0#u64,
+       17592186044416#u64] := by
+  unfold backend.serial.u64.constants.L
+  rfl
+
+/-- **The transpiled modulus constant denotes exactly the group order ℓ.**
+    Kernel-checked literal arithmetic (no native_decide). -/
+theorem L_val : scVal backend.serial.u64.constants.L = Ell := by
+  rw [scVal_eq _ _ _ _ _ _ L_limbs]
+  unfold scLimbs Ell
+  norm_num
+
+/-- The limbs of L are each below 2⁵² (needed by the add/sub reductions). -/
+theorem L_bnd : ScBnd backend.serial.u64.constants.L := by
+  refine ⟨_, _, _, _, _, L_limbs, ?_, ?_, ?_, ?_, ?_⟩ <;> norm_num
+
+end ScalarProofs
--- a/verification/check-scalar.sh
+++ b/verification/check-scalar.sh
@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+# Scalar-layer check (Scalar52 arithmetic mod ℓ). Compiles the gen model + the
+# proven foundation. add/sub (Range-loop reductions) and the Montgomery mul
+# path are in progress — see README. Guarded compiles throughout.
+set -uo pipefail
+source ~/aeneas-toolchain/env.sh
+HERE="$(cd "$(dirname "$0")" && pwd)"
+AENEAS_LEAN="$AENEAS_HOME/backends/lean"
+GEN=(CurveScalar/TypesExternal CurveScalar/Types CurveScalar/FunsExternal CurveScalar/Funs)
+PROOFS=(ScalarDenote)
+
+echo "=== stub/axiom audit ==="
+grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }
+echo "  clean"
+echo "=== compile (guarded) ==="
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -uo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  for m in ${GEN[*]}; do echo \"  · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
+  cd '$HERE'
+  for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
+" || { echo FAIL; exit 1; }
+echo ""
+echo "SCALAR FOUNDATION: gen compiles; denotation + group-order constant (L = ℓ) proven."
--- a/verification/extract-scalar.sh
+++ b/verification/extract-scalar.sh
@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+# Regenerate the SCALAR-layer Lean model (gen/CurveScalar) from Rust.
+#
+# SCOPE: the Scalar52 limb backend (backend::serial::u64::scalar) — the
+#   iterator-free ARITHMETIC core: add/sub/mul/square/montgomery_reduce/
+#   from_bytes/to_bytes mod ℓ = 2²⁵² + 27742317777372353535851937790883648493.
+#   The high-level crate::scalar wrapper (Sum/Product/NAF/radix/byte-parsing,
+#   all iterator-heavy) is brought in only for the signature layer.
+set -euo pipefail
+source ~/aeneas-toolchain/env.sh
+HERE="$(cd "$(dirname "$0")" && pwd)"
+CRATE=~/GitClone/FormalVerification/sources/risc0-curve25519-dalek-source/curve25519-dalek
+
+echo "[1/2] charon: Rust -> LLBC (scalar + Scalar52)"
+cd "$CRATE"
+charon cargo --preset=aeneas \
+  --start-from 'crate::backend::serial::u64::scalar::_::add' \
+  --start-from 'crate::backend::serial::u64::scalar::_::sub' \
+  --start-from 'crate::backend::serial::u64::scalar::_::mul' \
+  --start-from 'crate::backend::serial::u64::scalar::_::square' \
+  --start-from 'crate::backend::serial::u64::scalar::_::montgomery_mul' \
+  --start-from 'crate::backend::serial::u64::scalar::_::montgomery_square' \
+  --start-from 'crate::backend::serial::u64::scalar::_::montgomery_reduce' \
+  --start-from 'crate::backend::serial::u64::scalar::_::montgomery_invert' \
+  --start-from 'crate::backend::serial::u64::scalar::_::as_montgomery' \
+  --start-from 'crate::backend::serial::u64::scalar::_::from_montgomery' \
+  --opaque 'crate::backend::serial::u64::scalar::_::sub::black_box' \
+  --dest-file "$HERE/CurveScalar.llbc" \
+  -- --no-default-features
+
+echo "[2/2] aeneas: LLBC -> Lean (split files, CurveScalar.* modules)"
+cd "$HERE"
+aeneas -backend lean -split-files -subdir CurveScalar -dest gen CurveScalar.llbc
+echo "Done."
--- a/verification/gen/CurveScalar/Funs.lean
+++ b/verification/gen/CurveScalar/Funs.lean
@ -0,0 +1,641 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [curve25519_dalek]: function definitions
+import Aeneas
+import CurveScalar.Types
+import CurveScalar.FunsExternal
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
+namespace curve25519_dalek
+
+/-- [curve25519_dalek::backend::serial::u64::constants::L]
+    Source: 'curve25519-dalek/src/backend/serial/u64/constants.rs', lines 117:0-123:3 -/
+@[global_simps, irreducible]
+def backend.serial.u64.constants.L : backend.serial.u64.scalar.Scalar52 :=
+  Array.make 5#usize [
+    671914833335277#u64, 3916664325105025#u64, 1367801#u64, 0#u64,
+    17592186044416#u64
+    ]
+
+/-- [curve25519_dalek::backend::serial::u64::constants::LFACTOR]
+    Source: 'curve25519-dalek/src/backend/serial/u64/constants.rs', lines 126:0-126:48 -/
+@[global_simps, irreducible]
+def backend.serial.u64.constants.LFACTOR : Std.U64 := 1439961107955227#u64
+
+/-- [curve25519_dalek::backend::serial::u64::constants::RR]
+    Source: 'curve25519-dalek/src/backend/serial/u64/constants.rs', lines 138:0-144:3 -/
+@[global_simps, irreducible]
+def backend.serial.u64.constants.RR : backend.serial.u64.scalar.Scalar52 :=
+  Array.make 5#usize [
+    2764609938444603#u64, 3768881411696287#u64, 1616719297148420#u64,
+    1087343033131391#u64, 10175238647962#u64
+    ]
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{impl core::ops::index::Index<usize, u64> for curve25519_dalek::backend::serial::u64::scalar::Scalar52}::index]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 42:4-44:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+  (self : backend.serial.u64.scalar.Scalar52) (_index : Std.Usize) :
+  Result Std.U64
+  := do
+  Array.index_usize self _index
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{impl core::ops::index::IndexMut<usize, u64> for curve25519_dalek::backend::serial::u64::scalar::Scalar52}::index_mut]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 48:4-50:5
+    Visibility: public -/
+def
+  backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
+  (self : backend.serial.u64.scalar.Scalar52) (_index : Std.Usize) :
+  Result (Std.U64 × (Std.U64 → backend.serial.u64.scalar.Scalar52))
+  := do
+  let (i, index_mut_back) ← Array.index_mut_usize self _index
+  let back := fun i1 => let a := index_mut_back i1
+                        a
+  ok (i, back)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::m]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 55:0-57:1 -/
+def backend.serial.u64.scalar.m
+  (x : Std.U64) (y : Std.U64) : Result Std.U128 := do
+  let i ← lift (UScalar.cast .U128 x)
+  let i1 ← lift (UScalar.cast .U128 y)
+  i * i1
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::ZERO]
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 61:4-61:57
+    Visibility: public -/
+@[global_simps, irreducible]
+def backend.serial.u64.scalar.Scalar52.ZERO
+  : backend.serial.u64.scalar.Scalar52 :=
+  let a := Array.repeat 5#usize 0#u64
+  a
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop body 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 190:8-193:9
+    Visibility: public -/
+@[rust_loop_body]
+def backend.serial.u64.scalar.Scalar52.sub_loop0.body
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
+  (iter : core.ops.range.Range Std.Usize)
+  (difference : backend.serial.u64.scalar.Scalar52) (borrow : Std.U64) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
+    backend.serial.u64.scalar.Scalar52 × Std.U64)
+    (backend.serial.u64.scalar.Scalar52 × Std.U64))
+  := do
+  let (o, iter1) ←
+    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
+  match o with
+  | none => ok (done (difference, borrow))
+  | some i =>
+    let i1 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        a i
+    let i2 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        b i
+    let i3 ← borrow >>> 63#i32
+    let i4 ← i2 + i3
+    let borrow1 ← lift (core.num.U64.wrapping_sub i1 i4)
+    let (_, index_mut_back) ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
+        difference i
+    let i5 ← lift (borrow1 &&& mask)
+    let difference1 := index_mut_back i5
+    ok (cont (iter1, difference1, borrow1))
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 190:8-193:9
+    Visibility: public -/
+@[rust_loop]
+def backend.serial.u64.scalar.Scalar52.sub_loop0
+  (iter : core.ops.range.Range Std.Usize)
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52)
+  (difference : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
+  (borrow : Std.U64) :
+  Result (backend.serial.u64.scalar.Scalar52 × Std.U64)
+  := do
+  loop
+    (fun (iter1, difference1, borrow1) =>
+      backend.serial.u64.scalar.Scalar52.sub_loop0.body a b mask iter1
+      difference1 borrow1)
+    (iter, difference, borrow)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop body 1:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 0:0-203:9
+    Visibility: public -/
+@[rust_loop_body]
+def backend.serial.u64.scalar.Scalar52.sub_loop1.body
+  (mask : Std.U64) (underflow_mask : Std.U64)
+  (iter : core.ops.range.Range Std.Usize)
+  (difference : backend.serial.u64.scalar.Scalar52) (carry : Std.U64) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
+    backend.serial.u64.scalar.Scalar52 × Std.U64)
+    backend.serial.u64.scalar.Scalar52)
+  := do
+  let (o, iter1) ←
+    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
+  match o with
+  | none => ok (done difference)
+  | some i =>
+    let i1 ← carry >>> 52#i32
+    let i2 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        difference i
+    let i3 ← i1 + i2
+    let i4 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        backend.serial.u64.constants.L i
+    let i5 ← backend.serial.u64.scalar.Scalar52.sub.black_box underflow_mask
+    let i6 ← lift (i4 &&& i5)
+    let carry1 ← i3 + i6
+    let (_, index_mut_back) ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
+        difference i
+    let i7 ← lift (carry1 &&& mask)
+    let difference1 := index_mut_back i7
+    ok (cont (iter1, difference1, carry1))
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop 1:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 0:0-203:9
+    Visibility: public -/
+@[rust_loop]
+def backend.serial.u64.scalar.Scalar52.sub_loop1
+  (iter : core.ops.range.Range Std.Usize)
+  (difference : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
+  (underflow_mask : Std.U64) (carry : Std.U64) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  loop
+    (fun (iter1, difference1, carry1) =>
+      backend.serial.u64.scalar.Scalar52.sub_loop1.body mask underflow_mask
+      iter1 difference1 carry1)
+    (iter, difference, carry)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 176:4-206:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.sub
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let i ← 1#u64 <<< 52#i32
+  let mask ← i - 1#u64
+  let (difference, borrow) ←
+    backend.serial.u64.scalar.Scalar52.sub_loop0
+      { start := 0#usize, «end» := 5#usize } a b
+      backend.serial.u64.scalar.Scalar52.ZERO mask 0#u64
+  let i1 ← borrow >>> 63#i32
+  let i2 ← lift (i1 ^^^ 1#u64)
+  let underflow_mask ← lift (core.num.U64.wrapping_sub i2 1#u64)
+  backend.serial.u64.scalar.Scalar52.sub_loop1
+    { start := 0#usize, «end» := 5#usize } difference mask underflow_mask
+    0#u64
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]: loop body 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 166:8-169:9
+    Visibility: public -/
+@[rust_loop_body]
+def backend.serial.u64.scalar.Scalar52.add_loop.body
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
+  (iter : core.ops.range.Range Std.Usize)
+  (sum : backend.serial.u64.scalar.Scalar52) (carry : Std.U64) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
+    backend.serial.u64.scalar.Scalar52 × Std.U64)
+    backend.serial.u64.scalar.Scalar52)
+  := do
+  let (o, iter1) ←
+    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
+  match o with
+  | none => ok (done sum)
+  | some i =>
+    let i1 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        a i
+    let i2 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        b i
+    let i3 ← i1 + i2
+    let i4 ← carry >>> 52#i32
+    let carry1 ← i3 + i4
+    let (_, index_mut_back) ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
+        sum i
+    let i5 ← lift (carry1 &&& mask)
+    let sum1 := index_mut_back i5
+    ok (cont (iter1, sum1, carry1))
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]: loop 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 166:8-169:9
+    Visibility: public -/
+@[rust_loop]
+def backend.serial.u64.scalar.Scalar52.add_loop
+  (iter : core.ops.range.Range Std.Usize)
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52)
+  (sum : backend.serial.u64.scalar.Scalar52) (mask : Std.U64) (carry : Std.U64)
+  :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  loop
+    (fun (iter1, sum1, carry1) =>
+      backend.serial.u64.scalar.Scalar52.add_loop.body a b mask iter1 sum1
+      carry1)
+    (iter, sum, carry)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 160:4-173:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.add
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let i ← 1#u64 <<< 52#i32
+  let mask ← i - 1#u64
+  let sum ←
+    backend.serial.u64.scalar.Scalar52.add_loop
+      { start := 0#usize, «end» := 5#usize } a b
+      backend.serial.u64.scalar.Scalar52.ZERO mask 0#u64
+  backend.serial.u64.scalar.Scalar52.sub sum backend.serial.u64.constants.L
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::mul_internal]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 211:4-225:5 -/
+def backend.serial.u64.scalar.Scalar52.mul_internal
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) :
+  Result (Array Std.U128 9#usize)
+  := do
+  let z := Array.repeat 9#usize 0#u128
+  let i ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      0#usize
+  let i1 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
+      0#usize
+  let i2 ← backend.serial.u64.scalar.m i i1
+  let z1 ← Array.update z 0#usize i2
+  let i3 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
+      1#usize
+  let i4 ← backend.serial.u64.scalar.m i i3
+  let i5 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      1#usize
+  let i6 ← backend.serial.u64.scalar.m i5 i1
+  let i7 ← i4 + i6
+  let z2 ← Array.update z1 1#usize i7
+  let i8 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
+      2#usize
+  let i9 ← backend.serial.u64.scalar.m i i8
+  let i10 ← backend.serial.u64.scalar.m i5 i3
+  let i11 ← i9 + i10
+  let i12 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      2#usize
+  let i13 ← backend.serial.u64.scalar.m i12 i1
+  let i14 ← i11 + i13
+  let z3 ← Array.update z2 2#usize i14
+  let i15 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
+      3#usize
+  let i16 ← backend.serial.u64.scalar.m i i15
+  let i17 ← backend.serial.u64.scalar.m i5 i8
+  let i18 ← i16 + i17
+  let i19 ← backend.serial.u64.scalar.m i12 i3
+  let i20 ← i18 + i19
+  let i21 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      3#usize
+  let i22 ← backend.serial.u64.scalar.m i21 i1
+  let i23 ← i20 + i22
+  let z4 ← Array.update z3 3#usize i23
+  let i24 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
+      4#usize
+  let i25 ← backend.serial.u64.scalar.m i i24
+  let i26 ← backend.serial.u64.scalar.m i5 i15
+  let i27 ← i25 + i26
+  let i28 ← backend.serial.u64.scalar.m i12 i8
+  let i29 ← i27 + i28
+  let i30 ← backend.serial.u64.scalar.m i21 i3
+  let i31 ← i29 + i30
+  let i32 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      4#usize
+  let i33 ← backend.serial.u64.scalar.m i32 i1
+  let i34 ← i31 + i33
+  let z5 ← Array.update z4 4#usize i34
+  let i35 ← backend.serial.u64.scalar.m i5 i24
+  let i36 ← backend.serial.u64.scalar.m i12 i15
+  let i37 ← i35 + i36
+  let i38 ← backend.serial.u64.scalar.m i21 i8
+  let i39 ← i37 + i38
+  let i40 ← backend.serial.u64.scalar.m i32 i3
+  let i41 ← i39 + i40
+  let z6 ← Array.update z5 5#usize i41
+  let i42 ← backend.serial.u64.scalar.m i12 i24
+  let i43 ← backend.serial.u64.scalar.m i21 i15
+  let i44 ← i42 + i43
+  let i45 ← backend.serial.u64.scalar.m i32 i8
+  let i46 ← i44 + i45
+  let z7 ← Array.update z6 6#usize i46
+  let i47 ← backend.serial.u64.scalar.m i21 i24
+  let i48 ← backend.serial.u64.scalar.m i32 i15
+  let i49 ← i47 + i48
+  let z8 ← Array.update z7 7#usize i49
+  let i50 ← backend.serial.u64.scalar.m i32 i24
+  Array.update z8 8#usize i50
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::square_internal]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 230:4-249:5 -/
+def backend.serial.u64.scalar.Scalar52.square_internal
+  (a : backend.serial.u64.scalar.Scalar52) :
+  Result (Array Std.U128 9#usize)
+  := do
+  let i ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      0#usize
+  let i1 ← i * 2#u64
+  let i2 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      1#usize
+  let i3 ← i2 * 2#u64
+  let i4 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      2#usize
+  let i5 ← i4 * 2#u64
+  let i6 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      3#usize
+  let i7 ← i6 * 2#u64
+  let i8 ← backend.serial.u64.scalar.m i i
+  let i9 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 0#usize
+  let i10 ← backend.serial.u64.scalar.m i9 i2
+  let i11 ← backend.serial.u64.scalar.m i9 i4
+  let i12 ← backend.serial.u64.scalar.m i2 i2
+  let i13 ← i11 + i12
+  let i14 ← backend.serial.u64.scalar.m i9 i6
+  let i15 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 1#usize
+  let i16 ← backend.serial.u64.scalar.m i15 i4
+  let i17 ← i14 + i16
+  let i18 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
+      4#usize
+  let i19 ← backend.serial.u64.scalar.m i9 i18
+  let i20 ← backend.serial.u64.scalar.m i15 i6
+  let i21 ← i19 + i20
+  let i22 ← backend.serial.u64.scalar.m i4 i4
+  let i23 ← i21 + i22
+  let i24 ← backend.serial.u64.scalar.m i15 i18
+  let i25 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 2#usize
+  let i26 ← backend.serial.u64.scalar.m i25 i6
+  let i27 ← i24 + i26
+  let i28 ← backend.serial.u64.scalar.m i25 i18
+  let i29 ← backend.serial.u64.scalar.m i6 i6
+  let i30 ← i28 + i29
+  let i31 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 3#usize
+  let i32 ← backend.serial.u64.scalar.m i31 i18
+  let i33 ← backend.serial.u64.scalar.m i18 i18
+  ok (Array.make 9#usize [ i8, i10, i13, i17, i23, i27, i30, i32, i33 ])
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part2]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 263:8-266:9 -/
+def backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2
+  (sum : Std.U128) : Result (Std.U128 × Std.U64) := do
+  let i ← lift (UScalar.cast .U64 sum)
+  let i1 ← 1#u64 <<< 52#i32
+  let i2 ← i1 - 1#u64
+  let w ← lift (i &&& i2)
+  let i3 ← sum >>> 52#i32
+  ok (i3, w)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part1]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 257:8-260:9 -/
+def backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1
+  (sum : Std.U128) : Result (Std.U128 × Std.U64) := do
+  let i ← lift (UScalar.cast .U64 sum)
+  let i1 ←
+    lift (core.num.U64.wrapping_mul i backend.serial.u64.constants.LFACTOR)
+  let i2 ← 1#u64 <<< 52#i32
+  let i3 ← i2 - 1#u64
+  let p ← lift (i1 &&& i3)
+  let i4 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+      backend.serial.u64.constants.L 0#usize
+  let i5 ← backend.serial.u64.scalar.m p i4
+  let i6 ← sum + i5
+  let i7 ← i6 >>> 52#i32
+  ok (i7, p)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 254:4-287:5 -/
+def backend.serial.u64.scalar.Scalar52.montgomery_reduce
+  (limbs : Array Std.U128 9#usize) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let i ← Array.index_usize limbs 0#usize
+  let (carry, n0) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i
+  let i1 ← Array.index_usize limbs 1#usize
+  let i2 ← carry + i1
+  let i3 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+      backend.serial.u64.constants.L 1#usize
+  let i4 ← backend.serial.u64.scalar.m n0 i3
+  let i5 ← i2 + i4
+  let (carry1, n1) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i5
+  let i6 ← Array.index_usize limbs 2#usize
+  let i7 ← carry1 + i6
+  let i8 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+      backend.serial.u64.constants.L 2#usize
+  let i9 ← backend.serial.u64.scalar.m n0 i8
+  let i10 ← i7 + i9
+  let i11 ← backend.serial.u64.scalar.m n1 i3
+  let i12 ← i10 + i11
+  let (carry2, n2) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i12
+  let i13 ← Array.index_usize limbs 3#usize
+  let i14 ← carry2 + i13
+  let i15 ← backend.serial.u64.scalar.m n1 i8
+  let i16 ← i14 + i15
+  let i17 ← backend.serial.u64.scalar.m n2 i3
+  let i18 ← i16 + i17
+  let (carry3, n3) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i18
+  let i19 ← Array.index_usize limbs 4#usize
+  let i20 ← carry3 + i19
+  let i21 ←
+    backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+      backend.serial.u64.constants.L 4#usize
+  let i22 ← backend.serial.u64.scalar.m n0 i21
+  let i23 ← i20 + i22
+  let i24 ← backend.serial.u64.scalar.m n2 i8
+  let i25 ← i23 + i24
+  let i26 ← backend.serial.u64.scalar.m n3 i3
+  let i27 ← i25 + i26
+  let (carry4, n4) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i27
+  let i28 ← Array.index_usize limbs 5#usize
+  let i29 ← carry4 + i28
+  let i30 ← backend.serial.u64.scalar.m n1 i21
+  let i31 ← i29 + i30
+  let i32 ← backend.serial.u64.scalar.m n3 i8
+  let i33 ← i31 + i32
+  let i34 ← backend.serial.u64.scalar.m n4 i3
+  let i35 ← i33 + i34
+  let (carry5, r0) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i35
+  let i36 ← Array.index_usize limbs 6#usize
+  let i37 ← carry5 + i36
+  let i38 ← backend.serial.u64.scalar.m n2 i21
+  let i39 ← i37 + i38
+  let i40 ← backend.serial.u64.scalar.m n4 i8
+  let i41 ← i39 + i40
+  let (carry6, r1) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i41
+  let i42 ← Array.index_usize limbs 7#usize
+  let i43 ← carry6 + i42
+  let i44 ← backend.serial.u64.scalar.m n3 i21
+  let i45 ← i43 + i44
+  let (carry7, r2) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i45
+  let i46 ← Array.index_usize limbs 8#usize
+  let i47 ← carry7 + i46
+  let i48 ← backend.serial.u64.scalar.m n4 i21
+  let i49 ← i47 + i48
+  let (carry8, r3) ←
+    backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i49
+  let r4 ← lift (UScalar.cast .U64 carry8)
+  backend.serial.u64.scalar.Scalar52.sub
+    (Array.make 5#usize [ r0, r1, r2, r3, r4 ]) backend.serial.u64.constants.L
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::mul]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 291:4-294:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.mul
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let a1 ← backend.serial.u64.scalar.Scalar52.mul_internal a b
+  let ab ← backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
+  let a2 ←
+    backend.serial.u64.scalar.Scalar52.mul_internal ab
+      backend.serial.u64.constants.RR
+  backend.serial.u64.scalar.Scalar52.montgomery_reduce a2
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::square]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 299:4-302:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.square
+  (self : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let a ← backend.serial.u64.scalar.Scalar52.square_internal self
+  let aa ← backend.serial.u64.scalar.Scalar52.montgomery_reduce a
+  let a1 ←
+    backend.serial.u64.scalar.Scalar52.mul_internal aa
+      backend.serial.u64.constants.RR
+  backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_mul]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 306:4-308:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.montgomery_mul
+  (a : backend.serial.u64.scalar.Scalar52)
+  (b : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let a1 ← backend.serial.u64.scalar.Scalar52.mul_internal a b
+  backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_square]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 312:4-314:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.montgomery_square
+  (self : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let a ← backend.serial.u64.scalar.Scalar52.square_internal self
+  backend.serial.u64.scalar.Scalar52.montgomery_reduce a
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::as_montgomery]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 318:4-320:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.as_montgomery
+  (self : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  backend.serial.u64.scalar.Scalar52.montgomery_mul self
+    backend.serial.u64.constants.RR
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop body 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 327:8-329:9
+    Visibility: public -/
+@[rust_loop_body]
+def backend.serial.u64.scalar.Scalar52.from_montgomery_loop.body
+  (self : backend.serial.u64.scalar.Scalar52)
+  (iter : core.ops.range.Range Std.Usize) (limbs : Array Std.U128 9#usize) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U128
+    9#usize)) (Array Std.U128 9#usize))
+  := do
+  let (o, iter1) ←
+    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
+  match o with
+  | none => ok (done limbs)
+  | some i =>
+    let i1 ←
+      backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
+        self i
+    let i2 ← lift (UScalar.cast .U128 i1)
+    let a ← Array.update limbs i i2
+    ok (cont (iter1, a))
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop 0:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 327:8-329:9
+    Visibility: public -/
+@[rust_loop]
+def backend.serial.u64.scalar.Scalar52.from_montgomery_loop
+  (iter : core.ops.range.Range Std.Usize)
+  (self : backend.serial.u64.scalar.Scalar52) (limbs : Array Std.U128 9#usize)
+  :
+  Result (Array Std.U128 9#usize)
+  := do
+  loop
+    (fun (iter1, limbs1) =>
+      backend.serial.u64.scalar.Scalar52.from_montgomery_loop.body self iter1
+      limbs1)
+    (iter, limbs)
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 325:4-331:5
+    Visibility: public -/
+def backend.serial.u64.scalar.Scalar52.from_montgomery
+  (self : backend.serial.u64.scalar.Scalar52) :
+  Result backend.serial.u64.scalar.Scalar52
+  := do
+  let limbs := Array.repeat 9#usize 0#u128
+  let limbs1 ←
+    backend.serial.u64.scalar.Scalar52.from_montgomery_loop
+      { start := 0#usize, «end» := 5#usize } self limbs
+  backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs1
+
+end curve25519_dalek
--- a/verification/gen/CurveScalar/FunsExternal.lean
+++ b/verification/gen/CurveScalar/FunsExternal.lean
@ -0,0 +1,28 @@
+-- Hand-written external function models for the Scalar52 arithmetic extraction.
+-- This fork (curve25519-dalek v4.1.3) implements Scalar52::sub's constant-time
+-- conditional add directly with a local `black_box` optimization barrier rather
+-- than routing through subtle::ConditionallySelectable (as the v5 dalek does).
+-- The sole external item is that `black_box`.
+import Aeneas
+import CurveScalar.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+set_option maxHeartbeats 1000000
+set_option maxRecDepth 2048
+open curve25519_dalek
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub::black_box]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 179:8-183:9
+
+    MODEL (faithful): the Rust body is
+      `unsafe { core::ptr::read_volatile(&value) }`
+    — a volatile read of the `u64` `value` living on the stack. The `volatile`
+    qualifier only forbids the compiler from eliding/reordering the read (an
+    optimization barrier to keep the constant-time path branch-free); the VALUE
+    read back is exactly the value written, so semantically this is the identity
+    on `u64`. -/
+def backend.serial.u64.scalar.Scalar52.sub.black_box
+  (value : Std.U64) : Result Std.U64 :=
+  ok value
--- a/verification/gen/CurveScalar/FunsExternal_Template.lean
+++ b/verification/gen/CurveScalar/FunsExternal_Template.lean
@ -0,0 +1,22 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [curve25519_dalek]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Aeneas
+import CurveScalar.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+open curve25519_dalek
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub::black_box]:
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 179:8-183:9 -/
+axiom backend.serial.u64.scalar.Scalar52.sub.black_box
+  : Std.U64 → Result Std.U64
+
--- a/verification/gen/CurveScalar/Types.lean
+++ b/verification/gen/CurveScalar/Types.lean
@ -0,0 +1,23 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [curve25519_dalek]: type definitions
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+namespace curve25519_dalek
+
+/-- [curve25519_dalek::backend::serial::u64::scalar::Scalar52]
+    Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 25:0-25:34
+    Visibility: public -/
+@[reducible]
+def backend.serial.u64.scalar.Scalar52 := Array Std.U64 5#usize
+
+end curve25519_dalek
--- a/verification/gen/CurveScalar/TypesExternal.lean
+++ b/verification/gen/CurveScalar/TypesExternal.lean
@ -0,0 +1,12 @@
+-- Hand-written external types for the Scalar52 arithmetic extraction.
+-- This fork's function-level scalar extraction pulls in NO external types
+-- (unlike the v5 dalek template, whose sub/conditional_select route through
+-- subtle::Choice). Kept as a (decl-free) module so the check manifest is
+-- uniform across forks.
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+set_option maxHeartbeats 1000000
+set_option maxRecDepth 2048