mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
6120f9bb17
Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.
- verification/extract-scalar.sh: function-level Charon/Aeneas extraction
- verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (27 defs).
This fork (v4.1.2) implements Scalar52::sub's constant-time conditional add
with a pure arithmetic mask (constants::L[i] & underflow_mask), so the
extraction pulls in NO external functions or types (unlike v5 dalek, which
routes sub through subtle, and v4.1.3, which uses a local black_box).
- verification/gen/CurveScalar/{TypesExternal,FunsExternal}.lean: decl-free
stub modules kept so the check manifest is uniform across forks.
- verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
constants::L denotes exactly the group order ℓ, kernel-checked).
- verification/check-scalar.sh: guarded compile of the gen modules plus the
denotation foundation.
check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.
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 CurveScalar.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
|