THE SIGNATURE APEX on the betrusted fork: verify_accepts_iff, button-enforced

Third pyramid capped. Identical shape to the risc0 fork (both are sha2-0.10 stacks): the hash oracle is the single monomorphic sha512_hash3(R, A, m) call, extraction runs --no-default-features. - gen/CurveSig: extracted verify glue, definitionally welded to the proven CurveField model (every curve and scalar call resolves to a certified definition; only the hash and wire formats are opaque). - Proofs/SigApexSpec.lean (unchanged from dalek): verify_loop_full with the standard three-axiom cone, and verify_accepts_iff — the verifier accepts IFF compress([s]B - [k]A) = R byte-for-byte. - check.sh Phase 3b enforces the apex cone to be EXACTLY [propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]. - extract.sh gains the reproducible CurveSig stanza (same recipe verified byte-exact on the risc0 fork this session). Full check.sh green: all standard certificates + the apex audit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-09-03 20:13:47 +00:00 · 2026-07-04 22:49:19 +02:00 · 2026-07-04 22:49:19 +02:00 · 9620cf5dd4
commit 9620cf5dd4
parent b408df3765
10 changed files with 830 additions and 1 deletions
--- a/verification/CurveSig.llbc
+++ b/verification/CurveSig.llbc
--- a/verification/Proofs/SigApexSpec.lean
+++ b/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
--- a/verification/check.sh
+++ b/verification/check.sh
@ -29,6 +29,10 @@ GEN_MODULES=(
  CurveField/Types
  CurveField/FunsExternal
  CurveField/Funs
+  CurveSig/TypesExternal
+  CurveSig/Types
+  CurveSig/FunsExternal
+  CurveSig/Funs
 )
 PROOFS=(
  Denote
@ -59,6 +63,7 @@ PROOFS=(
  DsmNafLoopSpec
  DsmNafSpec
  DsmMulSpec
+  SigApexSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
@ -77,6 +82,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=(
@ -87,6 +93,7 @@ AUDIT_IMPORTS=(
  Proofs.DsmLoopSpec
  Proofs.DsmNafSpec
  Proofs.DsmMulSpec
+  Proofs.SigApexSpec
 )

 # ── Phase 0: resource + integrity guards ────────────────────────────────────
@ -166,5 +173,29 @@ lake env bash -c "
    exit 1
  fi
 "
+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, verifying.sha512_hash3, 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."
--- a/verification/extract.sh
+++ b/verification/extract.sh
@ -60,8 +60,30 @@ charon cargo --preset=aeneas \
  --dest-file "$HERE/CurveField.llbc" \
  -- --no-default-features

-echo "[2/2] aeneas: LLBC -> Lean (split files, CurveField.* modules)"
+echo "[2/4] aeneas: LLBC -> Lean (split files, CurveField.* modules)"
 cd "$HERE"
 aeneas -backend lean -split-files -subdir CurveField -dest gen CurveField.llbc

+echo "[3/4] charon: ed25519-dalek verify glue -> LLBC (sha512_hash3 opaque)"
+SIGCRATE="$(dirname "$CRATE")/ed25519-dalek"
+cd "$SIGCRATE"
+charon cargo --preset=aeneas \
+  --start-from 'crate::verifying::verify_sha512' \
+  --start-from 'crate::verifying::recompute_r_sha512' \
+  --opaque 'crate::verifying::sha512_hash3' \
+  --opaque 'crate::signature::compressed_from_bytes' \
+  --opaque 'curve25519_dalek' \
+  --opaque 'sha2' --opaque 'digest' --opaque 'ed25519' \
+  --opaque 'signature' --opaque 'subtle' --opaque 'zeroize' \
+  --opaque 'block_buffer' --opaque 'crypto_common' \
+  --exclude 'generic_array' --exclude 'typenum' \
+  --hide-marker-traits \
+  --dest-file "$HERE/CurveSig.llbc" \
+  -- --no-default-features
+
+echo "[4/4] aeneas: LLBC -> Lean (CurveSig.* modules; hand-maintained"
+echo "        TypesExternal.lean / FunsExternal.lean are NOT overwritten)"
+cd "$HERE"
+aeneas -backend lean -split-files -subdir CurveSig -dest gen CurveSig.llbc
+
 echo "Done. Now run ./check.sh to type-check the regenerated model."
--- a/verification/gen/CurveSig/Funs.lean
+++ b/verification/gen/CurveSig/Funs.lean
@ -0,0 +1,257 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [ed25519_dalek]: function definitions
+import Aeneas
+import CurveSig.Types
+import CurveSig.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 ed25519_dalek
+
+/-- [ed25519_dalek::errors::{impl core::convert::From<ed25519_dalek::errors::InternalError> for signature::error::Error}::from]:
+    Source: 'ed25519-dalek/src/errors.rs', lines 111:4-113:5
+    Visibility: public -/
+def signature.error.Error.Insts.CoreConvertFromInternalError.from
+  (_err : errors.InternalError) : Result signature.error.Error := do
+  signature.error.Error.new
+
+/-- Trait implementation: [ed25519_dalek::errors::{impl core::convert::From<ed25519_dalek::errors::InternalError> for signature::error::Error}]
+    Source: 'ed25519-dalek/src/errors.rs', lines 109:0-119:1 -/
+@[reducible]
+def signature.error.Error.Insts.CoreConvertFromInternalError :
+  core.convert.From signature.error.Error errors.InternalError := {
+  from_ := signature.error.Error.Insts.CoreConvertFromInternalError.from
+}
+
+/-- [ed25519_dalek::signature::check_scalar::L_BYTES]
+    Source: 'ed25519-dalek/src/signature.rs', lines 108:4-111:6 -/
+@[global_simps, irreducible]
+def signature.check_scalar.L_BYTES : Array Std.U8 32#usize :=
+  Array.make 32#usize [
+    237#u8, 211#u8, 245#u8, 92#u8, 26#u8, 99#u8, 18#u8, 88#u8, 214#u8, 156#u8,
+    247#u8, 162#u8, 222#u8, 249#u8, 222#u8, 20#u8, 0#u8, 0#u8, 0#u8, 0#u8,
+    0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 16#u8
+    ]
+
+/-- [ed25519_dalek::signature::check_scalar]: loop body 0:
+    Source: 'ed25519-dalek/src/signature.rs', lines 116:4-127:5 -/
+@[rust_loop_body]
+def signature.check_scalar_loop.body
+  (bytes : Array Std.U8 32#usize) (lt : Bool) (decided : Bool) (i : Std.Usize)
+  :
+  Result (ControlFlow (Bool × Bool × Std.Usize) Bool)
+  := do
+  if i > 0#usize
+  then
+    let j ← i - 1#usize
+    let (lt1, decided1) ←
+      if decided
+      then ok (lt, true)
+      else
+        do
+        let i1 ← Array.index_usize bytes j
+        let i2 ← Array.index_usize signature.check_scalar.L_BYTES j
+        if i1 < i2
+        then ok (true, true)
+        else let b ← if i1 > i2
+                       then ok true
+                       else ok false
+             ok (lt, b)
+    ok (cont (lt1, decided1, j))
+  else ok (done lt)
+
+/-- [ed25519_dalek::signature::check_scalar]: loop 0:
+    Source: 'ed25519-dalek/src/signature.rs', lines 116:4-127:5 -/
+@[rust_loop]
+def signature.check_scalar_loop
+  (bytes : Array Std.U8 32#usize) (lt : Bool) (decided : Bool) (i : Std.Usize)
+  :
+  Result Bool
+  := do
+  loop
+    (fun (lt1, decided1, i1) => signature.check_scalar_loop.body bytes lt1
+      decided1 i1)
+    (lt, decided, i)
+
+/-- [ed25519_dalek::signature::check_scalar]:
+    Source: 'ed25519-dalek/src/signature.rs', lines 106:0-133:1 -/
+def signature.check_scalar
+  (bytes : Array Std.U8 32#usize) :
+  Result (core.result.Result curve25519_dalek.scalar.Scalar
+    signature.error.Error)
+  := do
+  let lt ← signature.check_scalar_loop bytes false false 32#usize
+  if lt
+  then
+    let s ← curve25519_dalek.scalar.Scalar.from_bytes_mod_order bytes
+    ok (core.result.Result.Ok s)
+  else
+    let e ←
+      core.convert.IntoFrom.into
+        signature.error.Error.Insts.CoreConvertFromInternalError
+        errors.InternalError.ScalarFormat
+    ok (core.result.Result.Err e)
+
+/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]: loop body 0:
+    Source: 'ed25519-dalek/src/signature.rs', lines 196:8-200:9
+    Visibility: public -/
+@[rust_loop_body]
+def signature.InternalSignature.from_bytes_loop.body
+  (bytes : Array Std.U8 64#usize) (R_bytes : Array Std.U8 32#usize)
+  (s_bytes : Array Std.U8 32#usize) (i : Std.Usize) :
+  Result (ControlFlow ((Array Std.U8 32#usize) × (Array Std.U8 32#usize) ×
+    Std.Usize) ((Array Std.U8 32#usize) × (Array Std.U8 32#usize)))
+  := do
+  if i < 32#usize
+  then
+    let i1 ← Array.index_usize bytes i
+    let a ← Array.update R_bytes i i1
+    let i2 ← i + 32#usize
+    let i3 ← Array.index_usize bytes i2
+    let a1 ← Array.update s_bytes i i3
+    let i4 ← i + 1#usize
+    ok (cont (a, a1, i4))
+  else ok (done (R_bytes, s_bytes))
+
+/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]: loop 0:
+    Source: 'ed25519-dalek/src/signature.rs', lines 196:8-200:9
+    Visibility: public -/
+@[rust_loop]
+def signature.InternalSignature.from_bytes_loop
+  (bytes : Array Std.U8 64#usize) (R_bytes : Array Std.U8 32#usize)
+  (s_bytes : Array Std.U8 32#usize) (i : Std.Usize) :
+  Result ((Array Std.U8 32#usize) × (Array Std.U8 32#usize))
+  := do
+  loop
+    (fun (R_bytes1, s_bytes1, i1) =>
+      signature.InternalSignature.from_bytes_loop.body bytes R_bytes1 s_bytes1
+      i1)
+    (R_bytes, s_bytes, i)
+
+/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]:
+    Source: 'ed25519-dalek/src/signature.rs', lines 188:4-206:5
+    Visibility: public -/
+def signature.InternalSignature.from_bytes
+  (bytes : Array Std.U8 64#usize) :
+  Result (core.result.Result signature.InternalSignature signature.error.Error)
+  := do
+  let R_bytes := Array.repeat 32#usize 0#u8
+  let s_bytes := Array.repeat 32#usize 0#u8
+  let (R_bytes1, s_bytes1) ←
+    signature.InternalSignature.from_bytes_loop bytes R_bytes s_bytes 0#usize
+  let cey ← signature.compressed_from_bytes R_bytes1
+  let r ← signature.check_scalar s_bytes1
+  let cf ← core.result.Result.Insts.CoreOpsTry_traitTry.branch r
+  match cf with
+  | core.ops.control_flow.ControlFlow.Continue val =>
+    ok (core.result.Result.Ok { R := cey, s := val })
+  | core.ops.control_flow.ControlFlow.Break residual =>
+    core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
+      signature.InternalSignature (core.convert.FromSame signature.error.Error)
+      residual
+
+/-- [ed25519_dalek::signature::{impl core::convert::TryFrom<&'_0 ed25519::Signature, signature::error::Error> for ed25519_dalek::signature::InternalSignature}::try_from]:
+    Source: 'ed25519-dalek/src/signature.rs', lines 212:4-214:5
+    Visibility: public -/
+def
+  signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from
+  (sig : ed25519.Signature) :
+  Result (core.result.Result signature.InternalSignature signature.error.Error)
+  := do
+  let a ← ed25519.Signature.to_bytes sig
+  signature.InternalSignature.from_bytes a
+
+/-- [ed25519_dalek::verifying::recompute_r_sha512]:
+    Source: 'ed25519-dalek/src/verifying.rs', lines 717:0-730:1 -/
+def verifying.recompute_r_sha512
+  (key : verifying.VerifyingKey) (sig : signature.InternalSignature)
+  (message : Slice Std.U8) :
+  Result curve25519_dalek.edwards.CompressedEdwardsY
+  := do
+  let a ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes sig.R
+  let s ← lift (Array.to_slice a)
+  let a1 ←
+    curve25519_dalek.edwards.CompressedEdwardsY.as_bytes key.compressed
+  let s1 ← lift (Array.to_slice a1)
+  let a2 ← verifying.sha512_hash3 s s1 message
+  let k ← curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide a2
+  let minus_A ←
+    curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
+      key.point
+  let ep ←
+    curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint k
+      minus_A sig.s
+  curve25519_dalek.edwards.EdwardsPoint.compress ep
+
+/-- [ed25519_dalek::verifying::verify_sha512]: loop body 0:
+    Source: 'ed25519-dalek/src/verifying.rs', lines 749:4-754:5 -/
+@[rust_loop_body]
+def verifying.verify_sha512_loop.body
+  (e : Array Std.U8 32#usize) (r : Array Std.U8 32#usize) (equal : Bool)
+  (i : Std.Usize) :
+  Result (ControlFlow (Bool × Std.Usize) Bool)
+  := do
+  if i < 32#usize
+  then
+    let i1 ← Array.index_usize e i
+    let i2 ← Array.index_usize r i
+    let equal1 ← if i1 != i2
+                   then ok false
+                   else ok equal
+    let i3 ← i + 1#usize
+    ok (cont (equal1, i3))
+  else ok (done equal)
+
+/-- [ed25519_dalek::verifying::verify_sha512]: loop 0:
+    Source: 'ed25519-dalek/src/verifying.rs', lines 749:4-754:5 -/
+@[rust_loop]
+def verifying.verify_sha512_loop
+  (e : Array Std.U8 32#usize) (r : Array Std.U8 32#usize) (equal : Bool)
+  (i : Std.Usize) :
+  Result Bool
+  := do
+  loop
+    (fun (equal1, i1) => verifying.verify_sha512_loop.body e r equal1 i1)
+    (equal, i)
+
+/-- [ed25519_dalek::verifying::verify_sha512]:
+    Source: 'ed25519-dalek/src/verifying.rs', lines 733:0-760:1 -/
+def verifying.verify_sha512
+  (key : verifying.VerifyingKey) (message : Slice Std.U8)
+  (sig : ed25519.Signature) :
+  Result (core.result.Result Unit signature.error.Error)
+  := do
+  let r ←
+    signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from
+      sig
+  let cf ← core.result.Result.Insts.CoreOpsTry_traitTry.branch r
+  match cf with
+  | core.ops.control_flow.ControlFlow.Continue val =>
+    let expected_R ← verifying.recompute_r_sha512 key val message
+    let e ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes expected_R
+    let r1 ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes val.R
+    let equal ← verifying.verify_sha512_loop e r1 true 0#usize
+    if equal
+    then ok (core.result.Result.Ok ())
+    else
+      let e1 ←
+        core.convert.IntoFrom.into
+          signature.error.Error.Insts.CoreConvertFromInternalError
+          errors.InternalError.Verify
+      ok (core.result.Result.Err e1)
+  | core.ops.control_flow.ControlFlow.Break residual =>
+    core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
+      Unit (core.convert.FromSame signature.error.Error) residual
+
+end ed25519_dalek
--- a/verification/gen/CurveSig/FunsExternal.lean
+++ b/verification/gen/CurveSig/FunsExternal.lean
@ -0,0 +1,69 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   gen/CurveSig/FunsExternal.lean — external functions for the verify glue.
+
+   TIER A/B — REAL DEFINITIONS (no axioms): importing CurveField.Funs makes
+   the curve calls (compress, vartime_double_scalar_mul_basepoint,
+   as_bytes, neg, from_bytes_mod_order, from_bytes_mod_order_wide) resolve to
+   the PROVEN model's definitions by their fully-qualified names. The Result
+   Try/FromResidual plumbing and the compressed_from_bytes constructor are
+   given real definitions below.
+
+   TIER C — THE DELIBERATE OPAQUE BOUNDARY (the only axioms):
+   · verifying.sha512_hash3 — SHA-512 over r ‖ a ‖ m, one call
+   · ed25519.Signature.to_bytes — the wire accessor of an opaque type
+   · signature.error.Error.new  — an opaque error value
+   The apex certificate will carry EXACTLY these axioms beyond the standard
+   three — the documented hash-oracle boundary.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Aeneas
+import CurveSig.TypesExternal
+import CurveField.Funs
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/-! ### Tier A/B: real definitions -/
+
+/-- `Try::branch` for `core::result::Result` — the `?` operator's dispatch. -/
+def core.result.Result.Insts.CoreOpsTry_traitTry.branch
+    {T : Type} {E : Type} (r : core.result.Result T E) :
+    Result (core.ops.control_flow.ControlFlow
+      (core.result.Result core.convert.Infallible E) T) :=
+  match r with
+  | .Ok v => ok (.Continue v)
+  | .Err e => ok (.Break (.Err e))
+
+/-- `FromResidual` for `core::result::Result` — the `?` operator's error
+    conversion. The `Ok Infallible` branch is uninhabited. -/
+def core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
+    (T : Type) {E : Type} {F : Type} (convertFromInst : core.convert.From F E)
+    (r : core.result.Result core.convert.Infallible E) :
+    Result (core.result.Result T F) :=
+  match r with
+  | .Ok v => nomatch v
+  | .Err e => do
+      let f ← convertFromInst.from_ e
+      ok (.Err f)
+
+/-- The compressed-point constructor: `CompressedEdwardsY` is the 32-byte
+    array synonym in the proven model. -/
+def signature.compressed_from_bytes
+    (bytes : Array Std.U8 32#usize) :
+    Result curve25519_dalek.edwards.CompressedEdwardsY :=
+  ok bytes
+
+/-! ### Tier C: the deliberate opaque boundary -/
+
+/-- SHA-512 over r ‖ a ‖ m, as one call (this fork's sha2-0.10 stack; the
+    signature carries no foreign types). OPAQUE BY DESIGN — the hash oracle. -/
+axiom verifying.sha512_hash3
+  : Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result (Array Std.U8 64#usize)
+
+/-- The wire signature's 64 bytes (R ‖ s). Opaque accessor of an opaque
+    type — the verify spec is stated relative to its result. -/
+axiom ed25519.Signature.to_bytes
+  : ed25519.Signature → Result (Array Std.U8 64#usize)
+
+/-- An opaque error value; the spec only distinguishes ok from err. -/
+axiom signature.error.Error.new : Result signature.error.Error
--- a/verification/gen/CurveSig/FunsExternal_Template.lean
+++ b/verification/gen/CurveSig/FunsExternal_Template.lean
@ -0,0 +1,132 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [ed25519_dalek]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Aeneas
+import CurveSig.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 ed25519_dalek
+
+/-- [core::result::{impl core::ops::try_trait::Try for core::result::Result<T, E>}::branch]:
+    Source: '/rustc/library/core/src/result.rs', lines 2177:4-2177:64
+    Name pattern: [core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch]
+    Visibility: public -/
+@[rust_fun
+  "core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch"]
+axiom core.result.Result.Insts.CoreOpsTry_traitTry.branch
+  {T : Type} {E : Type} :
+  core.result.Result T E → Result (core.ops.control_flow.ControlFlow
+    (core.result.Result core.convert.Infallible E) T)
+
+/-- [core::result::{impl core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible, E>> for core::result::Result<T, F>}::from_residual]:
+    Source: '/rustc/library/core/src/result.rs', lines 2192:4-2192:70
+    Name pattern: [core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual]
+    Visibility: public -/
+@[rust_fun
+  "core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual"]
+axiom
+  core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
+  (T : Type) {E : Type} {F : Type} (convertFromInst : core.convert.From F E) :
+  core.result.Result core.convert.Infallible E → Result (core.result.Result T
+    F)
+
+/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]:
+    Source: 'curve25519-dalek/src/edwards.rs', lines 181:4-181:45
+    Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes"]
+axiom curve25519_dalek.edwards.CompressedEdwardsY.as_bytes
+  :
+  curve25519_dalek.edwards.CompressedEdwardsY → Result (Array Std.U8
+    32#usize)
+
+/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]:
+    Source: 'curve25519-dalek/src/edwards.rs', lines 566:4-566:48
+    Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress"]
+axiom curve25519_dalek.edwards.EdwardsPoint.compress
+  :
+  curve25519_dalek.edwards.EdwardsPoint → Result
+    curve25519_dalek.edwards.CompressedEdwardsY
+
+/-- [curve25519_dalek::edwards::{impl core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint> for curve25519_dalek::edwards::EdwardsPoint}::neg]:
+    Source: 'curve25519-dalek/src/edwards.rs', lines 699:4-699:32
+    Name pattern: [curve25519_dalek::edwards::{core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint, curve25519_dalek::edwards::EdwardsPoint>}::neg]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::edwards::{core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint, curve25519_dalek::edwards::EdwardsPoint>}::neg"]
+axiom
+  curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
+  :
+  curve25519_dalek.edwards.EdwardsPoint → Result
+    curve25519_dalek.edwards.EdwardsPoint
+
+/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]:
+    Source: 'curve25519-dalek/src/edwards.rs', lines 902:4-906:21
+    Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint"]
+axiom curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
+  :
+  curve25519_dalek.scalar.Scalar → curve25519_dalek.edwards.EdwardsPoint →
+    curve25519_dalek.scalar.Scalar → Result
+    curve25519_dalek.edwards.EdwardsPoint
+
+/-- [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order]:
+    Source: 'curve25519-dalek/src/scalar.rs', lines 244:4-244:58
+    Name pattern: [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order"]
+axiom curve25519_dalek.scalar.Scalar.from_bytes_mod_order
+  : Array Std.U8 32#usize → Result curve25519_dalek.scalar.Scalar
+
+/-- [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide]:
+    Source: 'curve25519-dalek/src/scalar.rs', lines 257:4-257:64
+    Name pattern: [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide]
+    Visibility: public -/
+@[rust_fun
+  "curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide"]
+axiom curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide
+  : Array Std.U8 64#usize → Result curve25519_dalek.scalar.Scalar
+
+/-- [ed25519::{ed25519::Signature}::to_bytes]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 351:4-351:44
+    Name pattern: [ed25519::{ed25519::Signature}::to_bytes]
+    Visibility: public -/
+@[rust_fun "ed25519::{ed25519::Signature}::to_bytes"]
+axiom ed25519.Signature.to_bytes
+  : ed25519.Signature → Result (Array Std.U8 64#usize)
+
+/-- [signature::error::{signature::error::Error}::new]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/signature-2.2.0/src/error.rs', lines 34:4-34:24
+    Name pattern: [signature::error::{signature::error::Error}::new]
+    Visibility: public -/
+@[rust_fun "signature::error::{signature::error::Error}::new"]
+axiom signature.error.Error.new : Result signature.error.Error
+
+/-- [ed25519_dalek::signature::compressed_from_bytes]:
+    Source: 'ed25519-dalek/src/signature.rs', lines 69:0-71:1 -/
+axiom signature.compressed_from_bytes
+  :
+  Array Std.U8 32#usize → Result curve25519_dalek.edwards.CompressedEdwardsY
+
+/-- [ed25519_dalek::verifying::sha512_hash3]:
+    Source: 'ed25519-dalek/src/verifying.rs', lines 708:0-714:1 -/
+axiom verifying.sha512_hash3
+  :
+  Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result (Array Std.U8
+    64#usize)
+
--- a/verification/gen/CurveSig/Types.lean
+++ b/verification/gen/CurveSig/Types.lean
@ -0,0 +1,41 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [ed25519_dalek]: type definitions
+import Aeneas
+import CurveSig.TypesExternal
+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 ed25519_dalek
+
+/-- [ed25519_dalek::errors::InternalError]
+    Source: 'ed25519-dalek/src/errors.rs', lines 25:0-55:1 -/
+@[discriminant isize]
+inductive errors.InternalError where
+| PointDecompression : errors.InternalError
+| ScalarFormat : errors.InternalError
+| BytesLength : Str → Std.Usize → errors.InternalError
+| Verify : errors.InternalError
+| MismatchedKeypair : errors.InternalError
+
+/-- [ed25519_dalek::signature::InternalSignature]
+    Source: 'ed25519-dalek/src/signature.rs', lines 29:0-51:1 -/
+structure signature.InternalSignature where
+  R : curve25519_dalek.edwards.CompressedEdwardsY
+  s : curve25519_dalek.scalar.Scalar
+
+/-- [ed25519_dalek::verifying::VerifyingKey]
+    Source: 'ed25519-dalek/src/verifying.rs', lines 58:0-64:1
+    Visibility: public -/
+structure verifying.VerifyingKey where
+  compressed : curve25519_dalek.edwards.CompressedEdwardsY
+  point : curve25519_dalek.edwards.EdwardsPoint
+
+end ed25519_dalek
--- a/verification/gen/CurveSig/TypesExternal.lean
+++ b/verification/gen/CurveSig/TypesExternal.lean
@ -0,0 +1,30 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   gen/CurveSig/TypesExternal.lean — external types for the verify glue.
+
+   The three curve types (CompressedEdwardsY, EdwardsPoint, Scalar) are NOT
+   axiomatized: importing CurveField.Types makes every fully-qualified
+   reference in CurveSig/Funs.lean resolve to the PROVEN model's types —
+   the glue and the curve share one universe.
+
+   Only the genuinely foreign types stay opaque — THE deliberate boundary:
+   · ed25519.Signature      — the wire-format signature (only observed
+                              through the opaque `to_bytes`)
+   · signature.error.Error  — the RustCrypto error value (verify's spec only
+                              distinguishes ok from err)
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Aeneas
+import CurveField.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/-- [ed25519::Signature] — opaque: the 64-byte wire signature, observed only
+    through `to_bytes`. -/
+@[rust_type "ed25519::Signature"]
+axiom ed25519.Signature : Type
+
+/-- [signature::error::Error] — opaque: the error value carries no
+    information the verification spec depends on. -/
+@[rust_type "signature::error::Error"]
+axiom signature.error.Error : Type
--- a/verification/gen/CurveSig/TypesExternal_Template.lean
+++ b/verification/gen/CurveSig/TypesExternal_Template.lean
@ -0,0 +1,50 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [ed25519_dalek]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+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
+
+/-- [curve25519_dalek::edwards::CompressedEdwardsY]
+    Source: 'curve25519-dalek/src/edwards.rs', lines 165:0-165:29
+    Name pattern: [curve25519_dalek::edwards::CompressedEdwardsY]
+    Visibility: public -/
+@[rust_type "curve25519_dalek::edwards::CompressedEdwardsY"]
+axiom curve25519_dalek.edwards.CompressedEdwardsY : Type
+
+/-- [curve25519_dalek::edwards::EdwardsPoint]
+    Source: 'curve25519-dalek/src/edwards.rs', lines 371:0-371:23
+    Name pattern: [curve25519_dalek::edwards::EdwardsPoint]
+    Visibility: public -/
+@[rust_type "curve25519_dalek::edwards::EdwardsPoint"]
+axiom curve25519_dalek.edwards.EdwardsPoint : Type
+
+/-- [curve25519_dalek::scalar::Scalar]
+    Source: 'curve25519-dalek/src/scalar.rs', lines 202:0-202:17
+    Name pattern: [curve25519_dalek::scalar::Scalar]
+    Visibility: public -/
+@[rust_type "curve25519_dalek::scalar::Scalar"]
+axiom curve25519_dalek.scalar.Scalar : Type
+
+/-- [ed25519::Signature]
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 303:0-303:20
+    Name pattern: [ed25519::Signature]
+    Visibility: public -/
+@[rust_type "ed25519::Signature"]
+axiom ed25519.Signature : Type
+
+/-- [signature::error::Error]
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/signature-2.2.0/src/error.rs', lines 26:0-26:16
+    Name pattern: [signature::error::Error]
+    Visibility: public -/
+@[rust_type "signature::error::Error"]
+axiom signature.error.Error : Type
+