THE SIGNATURE APEX: the EdDSA verification equation, proven and audited

`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
  the byte-equality of the two arrays (induction; axiom cone = exactly
  [propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
  extracted RustCrypto verifier accepts IFF the recomputed compressed point
      compress( [s]·B − [k]·A )
  equals the signature's R byte-for-byte. The recomputation is grounded in
  the PROVEN curve model (every curve and scalar call is a certified
  definition); k is whatever scalar the SHA-512 oracle produces — the
  honest EdDSA acceptance criterion with the hash opaque.

Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
  vector-backend axiom into the apex cone. Fixed at the build level:
  extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
  SIMD arm compiles out; BackendKind has only Serial and
  get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
  definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
  path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).

check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
  [propext, Classical.choice, Quot.sound,
   ed25519.Signature, sha2.Sha512,
   sha512_new, sha512_update, sha512_finalize_bytes,
   ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.

Full check.sh green: 16 standard certificates + the apex audit.

Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.

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

verification/.apex-LS0V.lean

@@ -0,0 +1 @@
+import Proofs.SigApexSpec

verification/Proofs/SigApexSpec.lean

@@ -0,0 +1,196 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/SigApexSpec.lean — the signature-layer apex, phase 1:
+   the EdDSA verification equation, SHA-512 opaque.
+
+   `verify_sha512 key msg sig` is the extracted RustCrypto verifier
+   (gen/CurveSig): parse the signature, recompute
+       R' = compress( [s]·B − [k]·A )              (k from the SHA-512 hash)
+   and accept iff R' equals the signature's R, byte-for-byte.
+
+   This file proves the verifier's control flow reduces EXACTLY to that
+   recompute-and-compare — the literal EdDSA check — over the PROVEN curve
+   model. SHA-512 stays an opaque oracle: the statement holds for whatever
+   bytes the hash produces, so the theorem is the honest
+       "accept  ↔  the recomputed compressed point equals R".
+
+   Phase 2 (the point-level equation  [s]B − [k]A = decompress R,  which
+   additionally needs `to_bytes` canonicity and `decompress`) is deliberately
+   deferred and documented — mirroring the dsm layer's phase split.
+
+   The load-bearing lemma is `verify_loop_eq`: the 32-byte comparison loop
+   returns precisely the byte-equality of the two arrays.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.ScalarDenote
+import Proofs.AddSpec
+import CurveSig.Funs
+open Aeneas Aeneas.Std Result ControlFlow
+open curve25519_dalek
+
+set_option maxHeartbeats 4000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- Byte-equality of two 32-byte arrays over the tail `[n, 32)`. -/
+def rangeEq (e r : Array Std.U8 32#usize) (n : ℕ) : Prop :=
+  ∀ j, n ≤ j → j < 32 → e.val[j]! = r.val[j]!
+
+instance (e r : Array Std.U8 32#usize) (n : ℕ) : Decidable (rangeEq e r n) := by
+  have : rangeEq e r n ↔ ∀ j, j < 32 → n ≤ j → e.val[j]! = r.val[j]! := by
+    unfold rangeEq; exact ⟨fun h j hj hn => h j hn hj, fun h j hn hj => h j hj hn⟩
+  exact decidable_of_iff _ this.symm
+
+/-- **The comparison loop returns byte-equality.** From accumulator `b` at
+    index `i ≤ 32`, `verify_sha512_loop` returns `b ∧ (all bytes in [i,32)
+    agree)`. Proven as a Hoare triple (the codebase's loop idiom); since the
+    loop always returns `ok`, this pins its value exactly. -/
+theorem verify_loop_spec (e r : Array Std.U8 32#usize) :
+    ∀ (n : ℕ) (b : Bool) (i : Usize), i.val = 32 - n → n ≤ 32 →
+    ed25519_dalek.verifying.verify_sha512_loop e r b i
+      ⦃ res => res = (b && decide (rangeEq e r (32 - n))) ⦄ := by
+  intro n
+  induction n with
+  | zero =>
+    intro b i hi _
+    unfold ed25519_dalek.verifying.verify_sha512_loop
+    apply loop_step
+    simp only [ed25519_dalek.verifying.verify_sha512_loop.body]
+    have hge : ¬ (i < 32#usize) := by clear * - hi; scalar_tac
+    rw [if_neg hge]
+    try simp only [spec_ok]
+    have hemp : decide (rangeEq e r (32 - 0)) = true := by
+      simp only [decide_eq_true_eq]; intro j hj1 hj2; omega
+    rw [hemp, Bool.and_true]
+  | succ n ih =>
+    intro b i hi hle
+    unfold ed25519_dalek.verifying.verify_sha512_loop
+    apply loop_step
+    simp only [ed25519_dalek.verifying.verify_sha512_loop.body]
+    have hlt : i < 32#usize := by clear * - hi hle; scalar_tac
+    rw [if_pos hlt]
+    have hiv : i.val = 32 - (n + 1) := hi
+    have hb1 : i.val < (e.val).length := by clear * - hle hiv; scalar_tac
+    have hb2 : i.val < (r.val).length := by clear * - hle hiv; scalar_tac
+    -- e[i], r[i]
+    step as ⟨x, hx⟩
+    step as ⟨y, hy⟩
+    -- the accumulator update: reduce the `if` to a plain `ok`
+    have hite : (if (x != y) = true then (ok false : Result Bool) else ok b)
+        = ok (if (x != y) = true then false else b) := by
+      by_cases hc : (x != y) = true
+      · rw [if_pos hc, if_pos hc]
+      · rw [if_neg hc, if_neg hc]
+    rw [hite]
+    -- name the reduced accumulator, then reduce the trivial `ok` bind
+    generalize heq1 : (if (x != y) = true then false else b) = eq1
+    simp only [bind_tc_ok]
+    -- i + 1
+    step as ⟨i3, hi3⟩
+    have hnext : i3.val = 32 - n := by clear * - hi3 hiv hle; scalar_tac
+    try simp only [spec_ok]
+    -- close with the IH at (eq1, i3); rewrite the range split
+    apply spec_mono (ih eq1 i3 hnext (by omega))
+    intro res hres
+    rw [hres]
+    -- eq1 = (b && e[i]=r[i]); the [i,32) range = byte i ∧ [i+1,32)
+    have hxv : x = e.val[i.val]'hb1 := by rw [hx]
+    have hyv : y = r.val[i.val]'hb2 := by rw [hy]
+    have heq1v : eq1 = (b && decide (e.val[i.val]! = r.val[i.val]!)) := by
+      rw [← heq1, hxv, hyv]
+      rw [getElem!_pos e.val i.val hb1, getElem!_pos r.val i.val hb2]
+      by_cases h : e.val[i.val]'hb1 = r.val[i.val]'hb2
+      · have hb : ¬ ((e.val[i.val]'hb1 != r.val[i.val]'hb2) = true) := by
+          simp [bne_iff_ne, h]
+        rw [if_neg hb]; simp [h]
+      · have hb : (e.val[i.val]'hb1 != r.val[i.val]'hb2) = true := by
+          simp [bne_iff_ne, h]
+        rw [if_pos hb]; simp [h]
+    rw [heq1v, Bool.and_assoc]
+    congr 1
+    -- decide(byte i) && decide(tail [i+1,32)) = decide(rangeEq [i,32))
+    have hiff : rangeEq e r (32 - (n + 1)) ↔
+        (e.val[i.val]! = r.val[i.val]!) ∧ rangeEq e r (32 - n) := by
+      have h32 : i.val < 32 := by clear * - hlt; scalar_tac
+      constructor
+      · intro h
+        refine ⟨h i.val (by clear * - hiv; omega) h32, ?_⟩
+        intro j hj1 hj2; exact h j (by omega) hj2
+      · rintro ⟨hbyte, htail⟩ j hj1 hj2
+        rcases Nat.lt_or_ge j (32 - n) with hj | hj
+        · have hji : j = i.val := by clear * - hj1 hj hiv; omega
+          rw [hji]; exact hbyte
+        · exact htail j hj hj2
+    have hda : (decide (e.val[i.val]! = r.val[i.val]!) && decide (rangeEq e r (32 - n)))
+        = decide ((e.val[i.val]! = r.val[i.val]!) ∧ rangeEq e r (32 - n)) := by
+      by_cases hp : (e.val[i.val]! = r.val[i.val]!) <;>
+        by_cases hq : rangeEq e r (32 - n) <;> simp [hp, hq]
+    rw [hda, decide_eq_decide]
+    exact hiff.symm
+
+/-- The comparison loop from the verifier's entry state (`b = true`,
+    `i = 0`): the result equals the full 32-byte equality. -/
+theorem verify_loop_full (e r : Array Std.U8 32#usize) :
+    ed25519_dalek.verifying.verify_sha512_loop e r true 0#usize
+      ⦃ res => res = decide (rangeEq e r 0) ⦄ := by
+  have h := verify_loop_spec e r 32 true 0#usize (by scalar_tac) (le_refl _)
+  apply spec_mono h
+  intro res hres; rw [hres]; simp
+
+/-! ### The apex: the EdDSA verification equation -/
+
+open ed25519_dalek in
+/-- **The EdDSA verification equation, SHA-512 opaque.** For a signature that
+    parses (`try_from` succeeds with internal signature `val`), and with the
+    recomputation and byte extractions total, the extracted RustCrypto
+    verifier accepts **iff** the recomputed compressed point `expected_R`
+    equals the signature's `R`, byte-for-byte:
+        verify_sha512 key msg sig = ok (Ok ())   ↔   e = R  (all 32 bytes).
+
+    `expected_R` (via `recompute_r_sha512`) is the PROVEN composition
+    `compress( [s]·B − [k]·A )` over the certified curve model; `k` is the
+    scalar the SHA-512 oracle produces — the hash stays opaque, so this is
+    exactly the honest EdDSA acceptance criterion. -/
+theorem verify_accepts_iff
+    (key : verifying.VerifyingKey) (msg : Slice Std.U8) (sig : ed25519.Signature)
+    (val : signature.InternalSignature)
+    (er : curve25519_dalek.edwards.CompressedEdwardsY)
+    (e r1 : Array Std.U8 32#usize)
+    (hparse : signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from sig
+        = ok (core.result.Result.Ok val))
+    (hrec : verifying.recompute_r_sha512 key val msg = ok er)
+    (he : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes er = ok e)
+    (hr1 : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes val.R = ok r1) :
+    verifying.verify_sha512 key msg sig = ok (core.result.Result.Ok ())
+      ↔ rangeEq e r1 0 := by
+  unfold verifying.verify_sha512
+  rw [hparse]
+  simp only [core.result.Result.Insts.CoreOpsTry_traitTry.branch, bind_tc_ok]
+  rw [hrec]
+  simp only [bind_tc_ok]
+  rw [he]
+  simp only [bind_tc_ok]
+  rw [hr1]
+  simp only [bind_tc_ok]
+  have hloop := verify_loop_full e r1
+  obtain ⟨v, hv, hpost⟩ := spec_imp_exists hloop
+  rw [hv]
+  simp only [bind_tc_ok]
+  rw [hpost]
+  by_cases hb : rangeEq e r1 0
+  · rw [decide_eq_true hb, if_pos rfl]
+    simp only [hb, iff_true]
+  · rw [decide_eq_false hb, if_neg (by simp)]
+    constructor
+    · intro hcontra
+      exfalso
+      -- the else-branch binds an opaque error value; whatever it is, binding
+      -- with `Err` can only yield `fail`/`div`/`ok (Err _)` — never `ok (Ok ())`
+      generalize hz : signature.error.Error.Insts.CoreConvertFromInternalError.from
+        errors.InternalError.Verify = z at hcontra
+      cases z <;> simp_all
+    · intro hc; exact absurd hc hb
+
+end CurveFieldProofs

verification/check.sh

@@ -29,6 +29,10 @@ GEN_MODULES=(
   CurveField/Types
   CurveField/FunsExternal
   CurveField/Funs
+  CurveSig/TypesExternal
+  CurveSig/Types
+  CurveSig/FunsExternal
+  CurveSig/Funs
 )
 PROOFS=(
   Basic
@@ -60,6 +64,7 @@ PROOFS=(
   DsmNafLoopSpec
   DsmNafSpec
   DsmMulSpec
+  SigApexSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
@@ -78,6 +83,7 @@ CERTS=(
   CurveFieldProofs.non_adjacent_form_spec
   CurveFieldProofs.run_basepoint
   CurveFieldProofs.vartime_double_base_mul_spec
+  CurveFieldProofs.verify_loop_full
 )
 # Imports needed so every certificate in CERTS is in scope for the audit.
 AUDIT_IMPORTS=(
@@ -90,6 +96,7 @@ AUDIT_IMPORTS=(
   Proofs.DsmNafMath
   Proofs.DsmNafSpec
   Proofs.DsmMulSpec
+  Proofs.SigApexSpec
 )
 
 # ── Phase 0: resource + integrity guards ────────────────────────────────────
@@ -169,5 +176,30 @@ lake env bash -c "
     exit 1
   fi
 "
+echo ""
+echo "=== Phase 3b: signature-apex audit (SHA-512 + wire-format boundary) ==="
+# The verification-equation apex is grounded in the PROVEN curve model; its
+# only axioms beyond the standard three are the deliberate, documented
+# boundary: the SHA-512 hash oracle and the opaque wire-format types.
+# NO curve axioms, NO scalar axioms, NO backend-dispatch axioms.
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -euo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  cd '$HERE'
+  ALLOWED='[propext, Classical.choice, Quot.sound, ed25519.Signature, sha2.Sha512, verifying.sha512_finalize_bytes, verifying.sha512_new, verifying.sha512_update, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]'
+  AUD=\$(mktemp '$HERE/.apex-XXXX.lean')
+  { echo 'import Proofs.SigApexSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; } > \"\$AUD\"
+  OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
+  echo \"\$OUT\"
+  rm -f \"\$AUD\"
+  FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
+  if echo \"\$FLAT\" | grep -qF \"depends on axioms: \$ALLOWED\"; then
+    echo '  apex axiom cone = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)'
+  else
+    echo 'APEX AUDIT FAILED: verify_accepts_iff cone is not the documented boundary'; exit 1
+  fi
+"
+
 echo ""
 echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."

verification/extract.sh

@@ -25,6 +25,10 @@ CRATE=~/GitClone/FormalVerification/sources/curve25519-dalek-source/curve25519-d
 
 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 \

verification/gen/CurveField/Funs.lean

@@ -3747,12 +3747,8 @@ def backend.variable_base_mul
   (point : edwards.EdwardsPoint) (scalar : scalar.Scalar) :
   Result edwards.EdwardsPoint
   := do
-  let bk ← backend.get_selected_backend
-  match bk with
-  | backend.BackendKind.Avx2 =>
-    backend.vector.scalar_mul.variable_base.spec_avx2.mul point scalar
-  | backend.BackendKind.Serial =>
-    backend.serial.scalar_mul.variable_base.mul point scalar
+  let _ ← backend.get_selected_backend
+  backend.serial.scalar_mul.variable_base.mul point scalar
 
 /-- [curve25519_dalek::backend::vartime_double_base_mul]:
     Source: 'curve25519-dalek/src/backend.rs', lines 267:0-277:1
@@ -3761,12 +3757,8 @@ def backend.vartime_double_base_mul
   (a : scalar.Scalar) (A : edwards.EdwardsPoint) (b : scalar.Scalar) :
   Result edwards.EdwardsPoint
   := do
-  let bk ← backend.get_selected_backend
-  match bk with
-  | backend.BackendKind.Avx2 =>
-    backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul a A b
-  | backend.BackendKind.Serial =>
-    backend.serial.scalar_mul.vartime_double_base.mul a A b
+  let _ ← backend.get_selected_backend
+  backend.serial.scalar_mul.vartime_double_base.mul a A b
 
 /-- [curve25519_dalek::constants::BASEPOINT_ORDER]
     Source: 'curve25519-dalek/src/constants.rs', lines 72:0-78:2 -/

verification/gen/CurveField/FunsExternal.lean

@@ -183,7 +183,10 @@ 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 (`subtle.Choice := Std.U8`,
+  -- TypesExternal); `unwrap_u8` is upstream's `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
@@ -355,8 +358,14 @@ axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul
     edwards.EdwardsPoint
 
 /-- [curve25519_dalek::backend::get_selected_backend]:
-    Source: 'curve25519-dalek/src/backend.rs', lines 55:0-75:1 -/
-axiom backend.get_selected_backend : Result backend.BackendKind
+    Source: 'curve25519-dalek/src/backend.rs', lines 55:0-75:1
+
+    REAL DEFINITION (not an axiom): under the verified build configuration
+    (`curve25519_dalek_backend = "serial"`) the only backend is `Serial`, so
+    the runtime selector returns it unconditionally. Faithful to the extracted
+    config; keeps the verifier's axiom cone free of backend-dispatch axioms. -/
+def backend.get_selected_backend : Result backend.BackendKind :=
+  ok backend.BackendKind.Serial
 
 /-- [curve25519_dalek::edwards::affine::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::affine::AffinePoint}::conditional_swap]:
     Source: 'curve25519-dalek/src/edwards/affine.rs', lines 23:0-30:1

verification/gen/CurveField/FunsExternal_Template.lean

@@ -286,20 +286,6 @@ axiom
 axiom backend.serial.scalar_mul.variable_base.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::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::get_selected_backend]:
     Source: 'curve25519-dalek/src/backend.rs', lines 55:0-75:1 -/
 axiom backend.get_selected_backend : Result backend.BackendKind

verification/gen/CurveField/Types.lean

@@ -190,7 +190,6 @@ def backend.serial.u64.scalar.Scalar52 := Array Std.U64 5#usize
     Source: 'curve25519-dalek/src/backend.rs', lines 46:0-52:1 -/
 @[discriminant isize]
 inductive backend.BackendKind where
-| Avx2 : backend.BackendKind
 | Serial : backend.BackendKind
 
 /-- [curve25519_dalek::edwards::affine::AffinePoint]