Merge scalar into CurveField: one type universe, serial-only backend

Replicates dalek's gen merge: extract.sh co-extracts the Scalar52 backend
and scalar::from_bytes_mod_order[_wide] into the CurveField model, pins
RUSTFLAGS --cfg curve25519_dalek_backend="serial" (SIMD dispatch compiles
out; get_selected_backend becomes a real definition), and upgrades
unwrap_u8 to the documented Choice-model definition. ScalarDenote repoints
by one import line; both buttons green over the merged gen.

Prepares the verify-glue integration (CurveSig) on this fork.

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

verification/Proofs/ScalarDenote.lean

@@ -23,7 +23,7 @@
 
    Imports: gen/CurveScalar (the transpiled Scalar52 arithmetic).
    ────────────────────────────────────────────────────────────────────────────── -/
-import CurveScalar.Funs
+import CurveField.Funs
 open Aeneas Aeneas.Std Result
 open curve25519_dalek
 

verification/check-scalar.sh

@@ -6,7 +6,7 @@ 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)
+GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs)  # MERGED GEN: scalar module now lives in CurveField
 PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec)
 
 echo "=== stub/axiom audit ==="

verification/extract.sh

@@ -23,13 +23,30 @@ source ~/aeneas-toolchain/env.sh
 HERE="$(cd "$(dirname "$0")" && pwd)"
 CRATE=~/GitClone/FormalVerification/sources/betrusted-curve25519-dalek-source/curve25519-dalek
 
-echo "[1/2] charon: Rust -> LLBC (field + curve_models + edwards)"
+echo "[1/2] charon: Rust -> LLBC (field + curve_models + edwards + scalar [MERGED GEN])"
 cd "$CRATE"
+# Force the portable SERIAL backend (the one we verify): the SIMD dispatch
+# arm is `#[cfg(curve25519_dalek_backend = "simd")]`, so pinning the cfg to
+# "serial" removes it from the extraction — no vector-backend axiom leaks in.
+export RUSTFLAGS='--cfg curve25519_dalek_backend="serial"'
 charon cargo --preset=aeneas \
   --start-from crate::field \
   --start-from crate::backend::serial::u64::field \
   --start-from crate::backend::serial::curve_models \
   --start-from crate::edwards \
+  --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' \
+  --start-from 'crate::backend::serial::u64::scalar::_::from_bytes_wide' \
+  --start-from 'crate::scalar::_::from_bytes_mod_order' \
+  --start-from 'crate::scalar::_::from_bytes_mod_order_wide' \
   --opaque 'crate::field::_::internal_invert_batch' \
   --opaque 'crate::backend::serial::scalar_mul::variable_base' \
   --opaque 'crate::backend::serial::scalar_mul::straus' \

verification/gen/CurveField/FunsExternal.lean

@@ -162,7 +162,9 @@ def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
     Name pattern: [subtle::{subtle::Choice}::unwrap_u8]
     Visibility: public -/
 @[rust_fun "subtle::{subtle::Choice}::unwrap_u8"]
-axiom subtle.Choice.unwrap_u8 : subtle.Choice → Result Std.U8
+def subtle.Choice.unwrap_u8 (c : subtle.Choice) : Result Std.U8 :=
+  -- MODEL (faithful): `Choice` is the u8 wrapper; `unwrap_u8` is `self.0`.
+  ok c
 
 /-- [subtle::{impl core::convert::From<subtle::Choice> for bool}::from]:
     Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 153:4-153:35
@@ -294,7 +296,10 @@ def U64.Insts.SubtleConditionallySelectable.conditional_swap
 
 /-- [curve25519_dalek::backend::get_selected_backend]:
     Source: 'curve25519-dalek/src/backend/mod.rs', lines 55:0-75:1 -/
-axiom backend.get_selected_backend : Result backend.BackendKind
+-- REAL DEFINITION (not an axiom): under the verified build configuration
+-- (curve25519_dalek_backend = "serial") the only backend is Serial.
+def backend.get_selected_backend : Result backend.BackendKind :=
+  ok backend.BackendKind.Serial
 
 /-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx512ifma_avx512vl::mul]:
     Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2

verification/gen/CurveField/FunsExternal_Template.lean

@@ -242,40 +242,11 @@ axiom U64.Insts.SubtleConditionallySelectable.conditional_swap
     Source: 'curve25519-dalek/src/backend/mod.rs', lines 55:0-75:1 -/
 axiom backend.get_selected_backend : Result backend.BackendKind
 
-/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx512ifma_avx512vl::mul]:
-    Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2
-    Visibility: public -/
-axiom backend.vector.scalar_mul.variable_base.spec_avx512ifma_avx512vl.mul
-  : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
-
-/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx2::mul]:
-    Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2
-    Visibility: public -/
-axiom backend.vector.scalar_mul.variable_base.spec_avx2.mul
-  : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
-
 /-- [curve25519_dalek::backend::serial::scalar_mul::variable_base::mul]:
     Source: 'curve25519-dalek/src/backend/serial/scalar_mul/variable_base.rs', lines 11:0-48:1 -/
 axiom backend.serial.scalar_mul.variable_base.mul
   : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
 
-/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx512ifma_avx512vl::mul]:
-    Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2
-    Visibility: public -/
-axiom
-  backend.vector.scalar_mul.vartime_double_base.spec_avx512ifma_avx512vl.mul
-  :
-  scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
-    edwards.EdwardsPoint
-
-/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx2::mul]:
-    Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2
-    Visibility: public -/
-axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.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

@@ -113,8 +113,6 @@ structure subtle.ConditionallySelectable (Self : Type) where
     Source: 'curve25519-dalek/src/backend/mod.rs', lines 46:0-52:1 -/
 @[discriminant isize]
 inductive backend.BackendKind where
-| Avx2 : backend.BackendKind
-| Avx512 : backend.BackendKind
 | Serial : backend.BackendKind
 
 /-- [curve25519_dalek::scalar::Scalar]
@@ -188,6 +186,12 @@ structure traits.Identity (Self : Type) where
 structure traits.ValidityCheck (Self : Type) where
   is_valid : Self → Result Bool
 
+/-- [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
+
 /-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure]
     Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
 @[reducible]