mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
5bf9ed5176
Gen merge: extract.sh now co-extracts the Scalar52 backend and the public scalar::from_bytes_mod_order[_wide] conversions into the SAME CurveField model, so the whole library — field, curve_models, edwards, scalar — shares one type universe (Scalar is a single structure, not two). The scalar proof chain repoints by one import line (ScalarDenote: CurveScalar.Funs -> CurveField.Funs); check-scalar.sh's gen list follows. Both buttons — the scalar certificates and the field/group/dsm certificates — pass fresh over the merged gen, so the merge is proven-safe, not merely hoped-safe. Verify glue (gen/CurveSig): the extracted ed25519-dalek verify_sha512 path, integrated against the proven model: - TypesExternal.lean imports CurveField.Types, so CompressedEdwardsY / EdwardsPoint / Scalar in the glue ARE the proven model's types. Only the genuinely foreign types stay opaque: sha2.Sha512, ed25519.Signature, signature.error.Error. - FunsExternal.lean imports CurveField.Funs, so every curve/scalar call (compress, vartime_double_scalar_mul_basepoint, as_bytes, neg, from_bytes_mod_order[_wide]) resolves to a proven definition — no axioms. The `?`-operator plumbing (Try::branch, FromResidual::from_residual) and compressed_from_bytes get real definitions. Only the SHA-512 hasher (sha512_new/update/finalize_bytes) and two opaque wire accessors (Signature.to_bytes, Error.new) remain axiomatized — the deliberate, documented hash-oracle boundary. Audited: `verify_sha512`'s entire axiom cone is [propext, Classical.choice, Quot.sound, sha2.Sha512, sha512_new, sha512_update, sha512_finalize_bytes, ed25519.Signature.to_bytes, signature.error.Error.new] — zero curve axioms, zero scalar axioms. The verify path is definitionally grounded in the certified model; the only trust boundary is SHA-512. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
90 lines
4.1 KiB
Text
90 lines
4.1 KiB
Text
/- ──────────────────────────────────────────────────────────────────────────────
|
||
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 CurveField.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
|