Double-scalar-mul enters the verified model: vartime_double_base extracted transparently

extract.sh now opens crate::backend::serial::scalar_mul::vartime_double_base
(the other scalar_mul strategies stay opaque): non_adjacent_form (with its
loops), NafLookupTable5 (from/select), the curve-model helpers and
vartime_double_base::mul itself land in gen/CurveField - the same
namespace as the proven edwards operations, so the coming double-and-add
induction can consume EdDouble/EdAddProjNiels/EdConvert directly.
Zero sorries, zero external axioms (the pinned sources carry documented
compat refactors: single-assignment loop helpers, param-rooted while,
always-256-iterations, index-based LE load).

Full check.sh pressed fresh over the regenerated model: every existing
field and group-law certificate still green and axiom-clean - the scope
extension is purely additive.

verification/extract.sh

@@ -31,7 +31,10 @@ charon cargo --preset=aeneas \
   --start-from crate::backend::serial::curve_models \
   --start-from crate::edwards \
   --opaque 'crate::field::_::internal_invert_batch' \
-  --opaque 'crate::backend::serial::scalar_mul' \
+  --opaque 'crate::backend::serial::scalar_mul::variable_base' \
+  --opaque 'crate::backend::serial::scalar_mul::straus' \
+  --opaque 'crate::backend::serial::scalar_mul::precomputed_straus' \
+  --opaque 'crate::backend::serial::scalar_mul::pippenger' \
   --opaque 'crate::backend::vector' \
   --opaque 'crate::backend::get_selected_backend' \
   --opaque 'crate::edwards::decompress' \

verification/gen/CurveField/FunsExternal_Template.lean

@@ -276,14 +276,6 @@ axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul
   scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
     edwards.EdwardsPoint
 
-/-- [curve25519_dalek::backend::serial::scalar_mul::vartime_double_base::mul]:
-    Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1
-    Visibility: public -/
-axiom backend.serial.scalar_mul.vartime_double_base.mul
-  :
-  scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
-    edwards.EdwardsPoint
-
 /-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]:
     Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1
     Visibility: public -/

verification/gen/CurveField/Types.lean

@@ -138,6 +138,11 @@ structure edwards.EdwardsPoint where
   Z : backend.serial.u64.field.FieldElement51
   T : backend.serial.u64.field.FieldElement51
 
+/-- [curve25519_dalek::window::NafLookupTable5]
+    Source: 'curve25519-dalek/src/window.rs', lines 183:0-183:56 -/
+@[reducible]
+def window.NafLookupTable5 (T : Type) := Array T 8#usize
+
 /-- [curve25519_dalek::backend::serial::curve_models::ProjectivePoint]
     Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 154:0-158:1
     Visibility: public -/
@@ -155,14 +160,6 @@ structure backend.serial.curve_models.CompletedPoint where
   Z : backend.serial.u64.field.FieldElement51
   T : backend.serial.u64.field.FieldElement51
 
-/-- [curve25519_dalek::backend::serial::curve_models::AffineNielsPoint]
-    Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 184:0-188:1
-    Visibility: public -/
-structure backend.serial.curve_models.AffineNielsPoint where
-  y_plus_x : backend.serial.u64.field.FieldElement51
-  y_minus_x : backend.serial.u64.field.FieldElement51
-  xy2d : backend.serial.u64.field.FieldElement51
-
 /-- [curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint]
     Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 206:0-211:1
     Visibility: public -/
@@ -172,6 +169,14 @@ structure backend.serial.curve_models.ProjectiveNielsPoint where
   Z : backend.serial.u64.field.FieldElement51
   T2d : backend.serial.u64.field.FieldElement51
 
+/-- [curve25519_dalek::backend::serial::curve_models::AffineNielsPoint]
+    Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 184:0-188:1
+    Visibility: public -/
+structure backend.serial.curve_models.AffineNielsPoint where
+  y_plus_x : backend.serial.u64.field.FieldElement51
+  y_minus_x : backend.serial.u64.field.FieldElement51
+  xy2d : backend.serial.u64.field.FieldElement51
+
 /-- Trait declaration: [curve25519_dalek::traits::Identity]
     Source: 'curve25519-dalek/src/traits.rs', lines 26:0-30:1
     Visibility: public -/