lean-guard: disable core dumps (no more apport popups on capped aborts)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-02 16:23:31 +02:00
parent 41ce8998d2
commit f4687c3eb3
16 changed files with 7300 additions and 735 deletions

View file

@ -26,7 +26,7 @@ in this repository.
| Layer | Certificate | Status | Axioms of certificate |
|-------|-------------|--------|-----------------------|
| Field 𝔽_p | `fieldImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
| Group law (Edwards) | `edwardsImplementation` | ⏳ in progress | — |
| Group law (Edwards) | `edwardsImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
| Scalar mod | `scalarImplementation` | ⏳ in progress | — |
| Signature (EdDSA) | `verifyEquation` | ⏳ in progress | — |

File diff suppressed because one or more lines are too long

View file

@ -0,0 +1,376 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdAddAffNiels.lean — coordinate-level specs for the MIXED addition
kernels EdwardsPoint ± AffineNielsPoint -> CompletedPoint and for the
negation of an AffineNielsPoint.
CONTEXT. The Rust crate curve25519/solana-ed25519 adds an extended point
P = (X₁:Y₁:Z₁:T₁) and a PRECOMPUTED affine cache N = (y+x, yx, 2dxy)
(an `AffineNielsPoint`, implicit Z = 1 — see Proofs/EdDenote.lean) with
the HisilWongCarterDawson mixed formulas
(src/backend/serial/curve_models.rs:458-472 for `add`, 479-493 for `sub`):
PP = (Y₁+X₁)·(y+x) MM = (Y₁X₁)·(yx)
Txy2d = T₁·(2dxy) Z2 = Z₁+Z₁
add: (X, Y, Z, T) = (PPMM, PP+MM, Z2+Txy2d, Z2Txy2d)
sub: mirrored — multiply CROSSWISE (PM = (Y₁+X₁)(yx),
MP = (Y₁X₁)(y+x)) and FLIP the sign of Txy2d in Z/T:
(X, Y, Z, T) = (PMMP, PM+MP, Z2Txy2d, Z2+Txy2d)
(3 muls, 3 unreduced adds, 3 reduced subs each — one mul fewer than the
projective-Niels kernels because the affine cache has no Z field).
`neg` (curve_models.rs:516-522) negates the cached point by SWAPPING the
y+x / yx fields and negating 2dxy: (x, y) = (x, y), so
y+(x) = yx, y(x) = y+x, 2d(x)y = 2dxy.
THIS FILE proves, in the STATEMENT POLICY of the point-spec phase
(coordinate level ONLY — no curve constants, no division, no OnCurve;
the algebra-law packaging happens in a later file):
* `add_affniels_spec` / `sub_affniels_spec` — under `ExtValid Pt` and
`AffNielsValid N` (the limb-bound + Z ≠ 0 validity predicates of
Proofs/EdDenote.lean) the kernels run PANIC-FREE, every output field
carries the exact bound its producing field op guarantees
(sub: 2⁵², single unreduced add of two reduced/mul outputs: 2⁵³,
unreduced add consuming another unreduced add: 2⁵⁴), and the four
coordinates satisfy the formulas above, stated STRICTLY in terms of
the input struct-field denotations ⟪Pt.X⟫ … ⟪N.xy2d⟫;
* `affniels_neg_spec` — negation runs, preserves `AffNielsValid`, and
denotes the field swap + negation.
BOUND BOOKKEEPING (the entire panic-freedom argument). Inputs carry
Bnd 2⁵² (ExtValid) resp. Bnd 2⁵³/2⁵² (AffNielsValid); the field ops
require Bnd 2⁵⁴ (mul/sub, MulSpec/SubNegSpec) resp. pairwise limb sums
< 2⁶⁴ (the unreduced add, AddSpec). Chasing the chain:
Y₁+X₁, Z2 : add of two 2⁵² values -> 2⁵³ (< 2⁵⁴ ✓)
Y₁X₁ : sub -> 2⁵²
PP/MM/PM/MP/Txy2d : mul of ≤ 2⁵³/2⁵³ inputs -> 2⁵¹+2¹³
X-output : sub of two mul outputs -> 2⁵²
Y-output : add of two mul outputs -> 2⁵³
Z2 ± Txy2d: sub -> 2⁵²; add of 2⁵³ + (2⁵¹+2¹³) values -> 2⁵⁴
so every intermediate is a legal input for its consumer, and the output
bounds exposed below (X: 2⁵², Y: 2⁵³, then add: Z 2⁵⁴ / T 2⁵²,
sub: Z 2⁵² / T 2⁵⁴) are the TRUE per-field bounds of the chain.
PROOF TECHNIQUE: the InvertSpec playbook — unfold the transpiled body,
walk it with `let* ⟨x, posts…⟩ ← spec by edis` (one field op per line;
`edis` discharges each op's Bnd side condition by hypothesis weakening;
where the needed bound is verbatim in context the `let*` machinery
discharges it itself and no `by` block is given). The final `let*`
also reduces the trailing `ok {…}` and collapses the constructor
projections, so the four coordinate equations close by rewriting the
recorded postconditions (plus `ring` where 2·Z appears as Z+Z).
The three `aff_*`-prefixed wrappers re-state AddSpec's `add_spec` (whose
hypotheses name all 10 limbs, so the `let*` machinery cannot apply it
directly) and SubNegSpec's `sub_spec`/`neg_spec` in hypothesis-light form,
exactly like `mul_spec'` (InvertSpec.lean); prefixed `aff_` to avoid name
collisions with the sibling point-op spec files, which declare their own.
Nothing in gen/ is modified; we only run the transpiled code.
Imports: Proofs/EdDenote (validity predicates, mk_* lemmas, ⟪·⟫/Bnd via
FieldMain) and Proofs/Square2Spec (uniform field-op spec environment of
the point-op phase). Imported by: the forthcoming Edwards algebra layer.
─────────────────────────────────────────────────────────────────────── -/
import Proofs.EdDenote
import Proofs.Square2Spec
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
namespace CurveFieldProofs
-- the weakest-precondition layer: spec_mono / spec_ok used below
open Aeneas.Std.WP
/-- Discharge: linear arithmetic, or a `Bnd` weakening from any hypothesis.
Every field op consumed below needs its inputs bounded (mul/sub: 2⁵⁴,
the add wrappers: 2⁵²/2⁵³), while the producing step only recorded a
tighter bound (2⁵², 2⁵³ or 2⁵¹+2¹³); this side-condition tactic closes
such goals either by `scalar_tac` or by weakening an existing `Bnd _ c`
hypothesis with `Bnd.mono` and `c ≤ c'` by `norm_num`. Passed as the
discharger to every `let*` step. (Local re-declaration of InvertSpec's
`bnd` macro — macros are kept file-local in this development.)
(`name :=` disambiguates the generated syntax-kind declaration from the
sibling files' `edis` macros so they can all be imported together.) -/
macro (name := edisAffNiels) "edis" : tactic =>
`(tactic| (first
| scalar_tac
| exact Bnd.mono (by assumption) (by norm_num)))
/-! ## Hypothesis-light wrappers for the unreduced add, sub and negate
The base specs take the 5 limbs of every argument as explicit variables
(their proofs compute limb by limb), so the `let*` machinery cannot
apply them directly; each wrapper repackages the limbs existentially via
`Fe.exists_limbs` — the `mul_spec'` pattern of Proofs/InvertSpec.lean.
The unreduced `fe_add` needs TWO instances because its output bound is
input-relative (`∀ c, Bnd a c → Bnd b c → Bnd r (2·c)`, AddSpec.lean):
the kernels below add reduced values (2⁵² → 2⁵³) but also feed one add
output into another add (2⁵³ → 2⁵⁴). -/
/-- RUST ANALOG: `impl Add for FieldElement51` (the `+` operator),
curve25519/solana-ed25519/src/backend/serial/u64/field.rs:68-72 (limbwise
`a[i] + b[i]`, no carry, no reduction) — verified in AddSpec.lean.
MATH: Bnd(a, 2⁵²) and Bnd(b, 2⁵²) ==> fe_add a b = ok r with
Bnd(r, 2⁵³) and ⟪r⟫ = ⟪a⟫ + ⟪b⟫.
LaTeX: $\mathrm{Bnd}(a,2^{52}) \wedge \mathrm{Bnd}(b,2^{52}) \Rightarrow
\llbracket r\rrbracket = \llbracket a\rrbracket+\llbracket b\rrbracket$.
Totality: each limb sum is < 2⁵² + 2⁵² = 2⁵³ < 2⁶⁴ — no u64 overflow.
WHY NEEDED: the Y₁+X₁ / Z₁+Z₁ / PP+MM additions below consume REDUCED
(2⁵², or 2⁵¹+2¹³ mul-output) values; this instance records the tight
2⁵³ output bound those sums actually satisfy. -/
theorem aff_add_spec53 (a b : Fe) (ha : Bnd a (2^52)) (hb : Bnd b (2^52)) :
fe_add a b ⦃ r => Bnd r (2^53) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
obtain ⟨x0, x1, x2, x3, x4, hA⟩ := Fe.exists_limbs a -- materialize a's limbs
obtain ⟨y0, y1, y2, y3, y4, hB⟩ := Fe.exists_limbs b -- materialize b's limbs
-- per-limb inequalities for the pairwise-sum < 2⁶⁴ side condition
have ha' := (Bnd_eq a x0 x1 x2 x3 x4 _ hA).mp ha
have hb' := (Bnd_eq b y0 y1 y2 y3 y4 _ hB).mp hb
apply spec_mono (add_spec a b x0 x1 x2 x3 x4 y0 y1 y2 y3 y4 hA hB
⟨by omega, by omega, by omega, by omega, by omega⟩)
rintro r ⟨-, hval, hbnd⟩
-- bound: instantiate AddSpec's relative law at c = 2⁵², weaken 2·2⁵² ≤ 2⁵³
refine ⟨(hbnd (2^52) ha hb).mono (by norm_num), ?_⟩
-- value: feVal r = feVal a + feVal b over , cast once into 𝔽_p
simp only [denote, hval, Nat.cast_add]
/-- RUST ANALOG: same operator as `aff_add_spec53`, at the next bound level.
MATH: Bnd(a, 2⁵³) and Bnd(b, 2⁵³) ==> fe_add a b = ok r with
Bnd(r, 2⁵⁴) and ⟪r⟫ = ⟪a⟫ + ⟪b⟫.
Totality: limb sums < 2⁵³ + 2⁵³ = 2⁵⁴ < 2⁶⁴.
WHY NEEDED: the Z-coordinate of the `add` kernel (resp. T of `sub`) is
Z2 + Txy2d where Z2 = Z₁+Z₁ is itself an UNREDUCED add output (2⁵³) —
one level above what `aff_add_spec53` admits. Output 2⁵⁴ is still a
legal input for every downstream field op (their invariant is < 2⁵⁴…
consumers weaken via `Bnd.mono` where they need ≤). -/
@[step]
theorem aff_add_spec54 (a b : Fe) (ha : Bnd a (2^53)) (hb : Bnd b (2^53)) :
fe_add a b ⦃ r => Bnd r (2^54) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
obtain ⟨x0, x1, x2, x3, x4, hA⟩ := Fe.exists_limbs a
obtain ⟨y0, y1, y2, y3, y4, hB⟩ := Fe.exists_limbs b
have ha' := (Bnd_eq a x0 x1 x2 x3 x4 _ hA).mp ha
have hb' := (Bnd_eq b y0 y1 y2 y3 y4 _ hB).mp hb
apply spec_mono (add_spec a b x0 x1 x2 x3 x4 y0 y1 y2 y3 y4 hA hB
⟨by omega, by omega, by omega, by omega, by omega⟩)
rintro r ⟨-, hval, hbnd⟩
refine ⟨(hbnd (2^53) ha hb).mono (by norm_num), ?_⟩
simp only [denote, hval, Nat.cast_add]
/-- RUST ANALOG: `impl Sub for FieldElement51` (the 16p-trick subtraction),
field.rs:84-101 — verified in SubNegSpec.lean.
MATH: Bnd(a, 2⁵⁴) and Bnd(b, 2⁵⁴) ==> fe_sub a b = ok r with
Bnd(r, 2⁵²) and ⟪r⟫ = ⟪a⟫ ⟪b⟫.
WHY NEEDED: hypothesis-light restatement of `sub_spec` (which names all
10 limbs) for the `let*` machinery — the Y₁X₁, PPMM and Z2Txy2d
steps below. -/
@[step]
theorem aff_sub_spec (a b : Fe) (ha : Bnd a (2^54)) (hb : Bnd b (2^54)) :
fe_sub a b ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = ⟪a⟫ - ⟪b⟫ ⦄ := by
obtain ⟨x0, x1, x2, x3, x4, hA⟩ := Fe.exists_limbs a
obtain ⟨y0, y1, y2, y3, y4, hB⟩ := Fe.exists_limbs b
exact sub_spec a b x0 x1 x2 x3 x4 y0 y1 y2 y3 y4 hA hB ha hb
/-- RUST ANALOG: `FieldElement51::negate` (16p a, then reduce),
field.rs:276-286 — verified in SubNegSpec.lean.
MATH: Bnd(a, 2⁵⁴) ==> fe_neg a = ok r with Bnd(r, 2⁵²) and
⟪r⟫ = ⟪a⟫.
WHY NEEDED: hypothesis-light restatement of `neg_spec` for the single
negate step of `affniels_neg_spec`. -/
@[step]
theorem aff_neg_spec (a : Fe) (ha : Bnd a (2^54)) :
fe_neg a ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = -⟪a⟫ ⦄ := by
obtain ⟨x0, x1, x2, x3, x4, hA⟩ := Fe.exists_limbs a
exact neg_spec a x0 x1 x2 x3 x4 hA ha
/-! ## The two mixed-addition kernels -/
/-- Rust: `impl Add<&AffineNielsPoint, CompletedPoint> for &EdwardsPoint`,
src/backend/serial/curve_models.rs:458-472; transpiled at
gen/CurveField/Funs.lean:1604-1640 as
`SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBAffineNielsPointCompletedPoint.add`.
MATH (coordinate level; writing X₁ = ⟪Pt.X⟫ etc., y±x = ⟪N.y_plus_x⟫ /
⟪N.y_minus_x⟫, 2dxy = ⟪N.xy2d⟫): under ExtValid Pt and AffNielsValid N
the kernel runs panic-free and returns the completed point
X = (Y₁+X₁)(y+x) (Y₁X₁)(yx) [= PP MM]
Y = (Y₁+X₁)(y+x) + (Y₁X₁)(yx) [= PP + MM]
Z = 2Z₁ + T₁·2dxy [= Z2 + Txy2d]
T = 2Z₁ T₁·2dxy [= Z2 Txy2d]
with the exact per-field bounds of the producing ops: X,T from `sub`
(2⁵²), Y a single unreduced add of two mul outputs (2⁵³), Z an
unreduced add consuming the unreduced Z2 (2⁵⁴) — all < 2⁵⁴+1, i.e.
consumable by every field op. NO curve constant and NO division
appears: the equations are stated strictly over the input struct-field
denotations; the later algebra layer combines them with `IsAffNielsOf`
(which characterizes ⟪N.xy2d⟫ via 121666·⟪N.xy2d⟫ = 243330·(x·y)) and
the curve equation to obtain the Edwards addition law.
WHY NEEDED: this is THE workhorse of fixed-base scalar multiplication —
`mul_base` adds table entries (AffineNielsPoint) to the accumulator with
exactly this kernel. -/
theorem add_affniels_spec (Pt : EdPoint) (N : AffNiels)
(hPt : ExtValid Pt) (hN : AffNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBAffineNielsPointCompletedPoint.add
Pt N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^52) ∧
⟪r.X⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.y_plus_x⟫
- (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.y_minus_x⟫ ∧
⟪r.Y⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.y_plus_x⟫
+ (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.y_minus_x⟫ ∧
⟪r.Z⟫ = 2 * ⟪Pt.Z⟫ + ⟪Pt.T⟫ * ⟪N.xy2d⟫ ∧
⟪r.T⟫ = 2 * ⟪Pt.Z⟫ - ⟪Pt.T⟫ * ⟪N.xy2d⟫ ⦄ := by
-- unpack the validity predicates (Z≠0 and the Segre coherence are not
-- needed at coordinate level — they ride along for the algebra layer)
obtain ⟨hPX, hPY, hPZ, hPT, -, -⟩ := hPt
obtain ⟨hNyp, hNym, hNxy⟩ := hN
-- expose the transpiled 10-step monadic body
unfold SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBAffineNielsPointCompletedPoint.add
-- Y_plus_X = Y₁+X₁ (unreduced add of two 2⁵² coords -> 2⁵³;
-- the 2⁵² side conditions are hypotheses verbatim — no discharger needed)
let* ⟨ YpX, YpX_bnd, YpX_val ⟩ ← aff_add_spec53
-- Y_minus_X = Y₁X₁ (reduced sub -> 2⁵²)
let* ⟨ YmX, YmX_bnd, YmX_val ⟩ ← aff_sub_spec by edis
-- PP = (Y₁+X₁)·(y+x); inputs 2⁵³ ≤ 2⁵⁴ -> 2⁵¹+2¹³
let* ⟨ PP, PP_bnd, PP_val ⟩ ← mul_spec' by edis
-- MM = (Y₁X₁)·(yx)
let* ⟨ MM, MM_bnd, MM_val ⟩ ← mul_spec' by edis
-- Txy2d = T₁·(2dxy)
let* ⟨ Txy, Txy_bnd, Txy_val ⟩ ← mul_spec' by edis
-- Z2 = Z₁+Z₁ (unreduced -> 2⁵³; side conditions verbatim in context)
let* ⟨ Z2, Z2_bnd, Z2_val ⟩ ← aff_add_spec53
-- X = PP MM (sub -> 2⁵²)
let* ⟨ rX, rX_bnd, rX_val ⟩ ← aff_sub_spec by edis
-- Y = PP + MM (mul outputs ≤ 2⁵² -> 2⁵³)
let* ⟨ rY, rY_bnd, rY_val ⟩ ← aff_add_spec53 by edis
-- Z = Z2 + Txy2d (2⁵³ + mul output -> 2⁵⁴)
let* ⟨ rZ, rZ_bnd, rZ_val ⟩ ← aff_add_spec54 by edis
-- T = Z2 Txy2d (sub -> 2⁵²)
let* ⟨ rT, rT_bnd, rT_val ⟩ ← aff_sub_spec by edis
-- the tail `ok { X := rX, Y := rY, Z := rZ, T := rT }` was already reduced
-- by the final `let*` (it also collapsed the constructor projections);
-- left: the four bounds + four coordinate equations. Substitute the
-- recorded step posts; X/Y close by rewriting alone, Z/T need `ring`
-- for Z₁+Z₁ = 2·Z₁
refine ⟨rX_bnd, rY_bnd, rZ_bnd, rT_bnd, ?_, ?_, ?_, ?_⟩
· rw [rX_val, PP_val, MM_val, YpX_val, YmX_val]
· rw [rY_val, PP_val, MM_val, YpX_val, YmX_val]
· rw [rZ_val, Z2_val, Txy_val]; ring
· rw [rT_val, Z2_val, Txy_val]; ring
/-- Rust: `impl Sub<&AffineNielsPoint, CompletedPoint> for &EdwardsPoint`,
src/backend/serial/curve_models.rs:479-493; transpiled at
gen/CurveField/Funs.lean:1657-1693 as
`SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBAffineNielsPointCompletedPoint.sub`.
MATH: the mirror image of `add_affniels_spec` — subtraction of the
cached point is addition of its negation (x, y), whose cache swaps
y+x ↔ yx and negates 2dxy (cf. `affniels_neg_spec` below); the Rust
code inlines that swap by multiplying CROSSWISE and flipping the sign
of Txy2d in the Z/T outputs. Under ExtValid Pt and AffNielsValid N:
X = (Y₁+X₁)(yx) (Y₁X₁)(y+x) [= PM MP]
Y = (Y₁+X₁)(yx) + (Y₁X₁)(y+x) [= PM + MP]
Z = 2Z₁ T₁·2dxy [= Z2 Txy2d]
T = 2Z₁ + T₁·2dxy [= Z2 + Txy2d]
with the per-field bounds of the producing ops — note Z/T trade places
with `add`'s: here Z comes from `sub` (2⁵²) and T from the unreduced
add (2⁵⁴).
WHY NEEDED: scalar multiplication with signed digit recodings (NAF)
subtracts table entries as often as it adds them. -/
theorem sub_affniels_spec (Pt : EdPoint) (N : AffNiels)
(hPt : ExtValid Pt) (hN : AffNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBAffineNielsPointCompletedPoint.sub
Pt N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^54) ∧
⟪r.X⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.y_minus_x⟫
- (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.y_plus_x⟫ ∧
⟪r.Y⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.y_minus_x⟫
+ (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.y_plus_x⟫ ∧
⟪r.Z⟫ = 2 * ⟪Pt.Z⟫ - ⟪Pt.T⟫ * ⟪N.xy2d⟫ ∧
⟪r.T⟫ = 2 * ⟪Pt.Z⟫ + ⟪Pt.T⟫ * ⟪N.xy2d⟫ ⦄ := by
obtain ⟨hPX, hPY, hPZ, hPT, -, -⟩ := hPt
obtain ⟨hNyp, hNym, hNxy⟩ := hN
unfold SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBAffineNielsPointCompletedPoint.sub
-- Y_plus_X = Y₁+X₁ -> 2⁵³ (side conditions verbatim in context);
-- Y_minus_X = Y₁X₁ -> 2⁵²
let* ⟨ YpX, YpX_bnd, YpX_val ⟩ ← aff_add_spec53
let* ⟨ YmX, YmX_bnd, YmX_val ⟩ ← aff_sub_spec by edis
-- the crosswise products: PM = (Y₁+X₁)(yx), MP = (Y₁X₁)(y+x)
let* ⟨ PM, PM_bnd, PM_val ⟩ ← mul_spec' by edis
let* ⟨ MP, MP_bnd, MP_val ⟩ ← mul_spec' by edis
-- Txy2d = T₁·(2dxy); Z2 = Z₁+Z₁ (side conditions verbatim in context)
let* ⟨ Txy, Txy_bnd, Txy_val ⟩ ← mul_spec' by edis
let* ⟨ Z2, Z2_bnd, Z2_val ⟩ ← aff_add_spec53
-- X = PM MP; Y = PM + MP; Z = Z2 Txy2d; T = Z2 + Txy2d
let* ⟨ rX, rX_bnd, rX_val ⟩ ← aff_sub_spec by edis
let* ⟨ rY, rY_bnd, rY_val ⟩ ← aff_add_spec53 by edis
let* ⟨ rZ, rZ_bnd, rZ_val ⟩ ← aff_sub_spec by edis
let* ⟨ rT, rT_bnd, rT_val ⟩ ← aff_add_spec54 by edis
-- bounds + equations (the final `let*` reduced the trailing `ok {…}`)
refine ⟨rX_bnd, rY_bnd, rZ_bnd, rT_bnd, ?_, ?_, ?_, ?_⟩
· rw [rX_val, PM_val, MP_val, YpX_val, YmX_val]
· rw [rY_val, PM_val, MP_val, YpX_val, YmX_val]
· rw [rZ_val, Z2_val, Txy_val]; ring
· rw [rT_val, Z2_val, Txy_val]; ring
/-! ## Negation of an affine-Niels cache point -/
/-- Rust: `impl Neg for &AffineNielsPoint`,
src/backend/serial/curve_models.rs:516-522; transpiled at
gen/CurveField/Funs.lean:1767-1773 as
`SharedAAffineNielsPoint.Insts.CoreOpsArithNegAffineNielsPoint.neg`
(the single field negation goes through the operator wrapper
`SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg`,
Funs.lean:1732, which is definitionally `FieldElement51::negate`).
MATH: AffNielsValid N ==> neg N = ok r with AffNielsValid r and
⟪r.y_plus_x⟫ = ⟪N.y_minus_x⟫,
⟪r.y_minus_x⟫ = ⟪N.y_plus_x⟫,
⟪r.xy2d⟫ = ⟪N.xy2d⟫.
On denotations this IS the cache of the negated affine point: if N
caches (x, y) then r caches (x, y), since y+(x) = yx, y(x) = y+x
and 2d(x)y = (2dxy) — the algebra layer derives
`IsAffNielsOf N x y → IsAffNielsOf r (x) y` from these three equations
by ring reasoning on the 121666-characterization of `IsAffNielsOf`.
Validity is PRESERVED (not just some bound): the swapped fields keep
their 2⁵³ bounds verbatim, and `negate` REDUCES, returning 2⁵² — so r
can re-enter the add/sub kernels above. (The y±x swap is pure data
movement — the two equations hold by `rfl`; only xy2d runs code.)
WHY NEEDED: signed-digit lookup tables (`NafLookupTable`/`select`)
produce N for negative digits with exactly this function. -/
theorem affniels_neg_spec (N : AffNiels) (hN : AffNielsValid N) :
SharedAAffineNielsPoint.Insts.CoreOpsArithNegAffineNielsPoint.neg N ⦃ r =>
AffNielsValid r ∧
⟪r.y_plus_x⟫ = ⟪N.y_minus_x⟫ ∧
⟪r.y_minus_x⟫ = ⟪N.y_plus_x⟫ ∧
⟪r.xy2d⟫ = -⟪N.xy2d⟫ ⦄ := by
obtain ⟨hNyp, hNym, hNxy⟩ := hN
-- expose the body and the operator wrapper around `negate`
unfold SharedAAffineNielsPoint.Insts.CoreOpsArithNegAffineNielsPoint.neg
SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
-- the one field op: xy2d' = xy2d (input 2⁵² ≤ 2⁵⁴, output reduced 2⁵²)
let* ⟨ nx, nx_bnd, nx_val ⟩ ← aff_neg_spec by edis
-- the final `let*` reduced the tail `ok { y_plus_x := N.y_minus_x,
-- y_minus_x := N.y_plus_x, xy2d := nx }` and already closed the two
-- pure-data-movement equations (they are `rfl` after the projections
-- collapse); left: validity — the swap preserves the 2⁵³ bounds and
-- negate's reduced output is the required 2⁵² — and the xy2d equation
exact ⟨⟨hNym, hNyp, nx_bnd⟩, nx_val⟩
end CurveFieldProofs

View file

@ -0,0 +1,362 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdAddProjNiels.lean — coordinate-level specs for the MIXED
addition/subtraction kernels EdwardsPoint ± ProjectiveNielsPoint →
CompletedPoint, and for projective-niels negation.
CONTEXT. The Rust crate curve25519/solana-ed25519 adds points in
extended coordinates against a precomputed "niels" cache
(Y+X, YX, Z, T·2d) using the HisilWongCarterDawson mixed-addition
formulas (src/backend/serial/curve_models.rs:411-452):
add: PP = (Y₁+X₁)·(Y₂+X₂) sub: PM = (Y₁+X₁)·(Y₂X₂)
MM = (Y₁X₁)·(Y₂X₂) MP = (Y₁X₁)·(Y₂+X₂)
TT2d = T₁·(T₂·2d) TT2d = T₁·(T₂·2d)
ZZ = Z₁·Z₂, ZZ2 = ZZ+ZZ ZZ = Z₁·Z₂, ZZ2 = ZZ+ZZ
X' = PPMM Y' = PP+MM X' = PMMP Y' = PM+MP
Z' = ZZ2+TT2d T' = ZZ2TT2d Z' = ZZ2TT2d T' = ZZ2+TT2d
The result lives in the ℙ¹×ℙ¹ "completed" model ((X':Z'), (Y':T')).
Charon+Aeneas transpiled both bodies (and the `Neg` impl for the niels
cache, curve_models.rs:500-511) into gen/CurveField/Funs.lean.
THIS FILE proves, for each of the three kernels, TOTAL correctness at the
COORDINATE level (the statement policy of the point-op phase):
* hypotheses — only the EdDenote validity predicates (`ExtValid`,
`ProjNielsValid`), which carry the limb bounds making the field ops
panic-free, plus ⟪Z⟫ ≠ 0 side facts;
* conclusions — per-output-field `Bnd` bounds (exactly what the field-op
chain yields: `fe_sub`/`fe_mul` outputs are reduced ≤ 2⁵², a single
unreduced `fe_add` of reduced inputs gives 2⁵³, and the stacked add
ZZ2 + TT2d gives 2⁵⁴) AND the four coordinate equations over 𝔽_p,
phrased STRICTLY in the input struct-field denotations, e.g.
⟪r.Z⟫ = 2·⟪P.Z⟫·⟪N.Z⟫ + ⟪P.T⟫·⟪N.T2d⟫.
No curve constants, no division, no `OnCurve` here — identifying these
limb-level equations with the Edwards group law (via `IsNielsOf` and
the d-characterization of EdDenote.lean) happens in a later file.
PROOF TECHNIQUE. Identical to Proofs/InvertSpec.lean: `unfold` the
transpiled monadic body, then walk it with `let* ⟨x, post…⟩ ← spec by edis`
— one field operation per line, the named postconditions accumulating in
the context — and close the four coordinate equations by `rw`+`ring`.
The `edis` side-condition macro (re-declared here; macros do not travel
across files) discharges every `Bnd _ (2⁵²/2⁵³/2⁵⁴)` obligation by
`assumption` or by weakening an existing bound (`Bnd.mono`). Because the
base specs `sub_spec`/`neg_spec`/`add_spec` (SubNegSpec.lean/AddSpec.lean)
take explicit limb variables, this file first re-packages them limb-free
(`sub_spec'`, `neg_spec'`, `add52_spec`, `add53_spec`) via
`Fe.exists_limbs`, mirroring `mul_spec'` (InvertSpec.lean).
Imports: Proofs/EdDenote.lean (point predicates + mk-projection simps)
and Proofs/Square2Spec.lean (the point-op phase's common field-op stock).
Imported by: the forthcoming algebra-law packaging file (EdCurve phase).
─────────────────────────────────────────────────────────────────────── -/
import Proofs.EdDenote
import Proofs.Square2Spec
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
namespace CurveFieldProofs
-- the weakest-precondition layer: spec_mono / spec_ok used below
open Aeneas.Std.WP
/-! ## Limb-free wrappers for the unreduced add, sub, and negate
The base specs (AddSpec.lean / SubNegSpec.lean) name all five limbs of
every argument explicitly because their proofs compute limb by limb; the
`let*` automation cannot invent those variables. As with `mul_spec'`
(InvertSpec.lean), we re-state each spec with the limbs repackaged via
`Fe.exists_limbs`. `fe_add` performs NO reduction (limbwise `aᵢ+bᵢ`), so
its output bound genuinely doubles the input bound — we expose the two
instances this file needs (2⁵²→2⁵³ and 2⁵³→2⁵⁴) of one parametric lemma. -/
/-- Parametric limb-free `fe_add` spec.
Rust: `impl Add<&FieldElement51> for &FieldElement51`, u64/field.rs:68-72
(limbwise sum, no carry, no reduction) — verified in Proofs/AddSpec.lean.
MATH: c ≤ 2⁶³, Bnd(a,c), Bnd(b,c) ==> fe_add a b = ok r with
Bnd(r, 2c) and ⟪r⟫ = ⟪a⟫ + ⟪b⟫.
The hypothesis c ≤ 2⁶³ makes every limbwise sum aᵢ + bᵢ < 2c ≤ 2⁶⁴ —
exactly the u64 no-overflow side condition of `add_spec`, i.e. the
panic-freedom of the unreduced add. The value clause is `add_spec`'s
exact equation `feVal r = feVal a + feVal b` pushed through the mod-p
cast (additions commute with 𝔽_p).
WHY NEEDED: parent of the two fixed-bound instances below; stated
parametrically so the bound bookkeeping is proved once.
(`private`: Proofs/EdConvert.lean exports a different `add_spec''` under
the same name; this one is only consumed in-file, so privacy avoids the
duplicate-declaration clash without changing any statement.) -/
private theorem add_spec'' (c : ) (hc : c ≤ 2^63) (a b : Fe)
(hba : Bnd a c) (hbb : Bnd b c) :
fe_add a b ⦃ r => Bnd r (2*c) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
-- materialize the limbs of both arguments and their per-limb bounds
obtain ⟨a0, a1, a2, a3, a4, hA⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hB⟩ := Fe.exists_limbs b
have hA' := (Bnd_eq a a0 a1 a2 a3 a4 c hA).mp hba
have hB' := (Bnd_eq b b0 b1 b2 b3 b4 c hB).mp hbb
-- run the base spec; each pairwise sum < 2c ≤ 2⁶⁴ closes by omega
apply spec_mono (add_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hA hB
⟨by omega, by omega, by omega, by omega, by omega⟩)
rintro r ⟨-, hval, hbnd⟩
-- bound: the "doubles any common bound" law at c; value: one cast to 𝔽_p
exact ⟨hbnd c hba hbb, by simp [denote, hval]⟩
/-- `fe_add` on two REDUCED (2⁵²) inputs: output bound 2⁵³.
MATH: Bnd(a,2⁵²), Bnd(b,2⁵²) ==> fe_add a b = ok r, Bnd(r,2⁵³),
⟪r⟫ = ⟪a⟫ + ⟪b⟫.
WHY NEEDED: the three "first-generation" adds of the kernels below
(Y₁+X₁ on the 2⁵²-bounded extended coordinates, ZZ+ZZ and PP+MM on
2⁵²-bounded mul outputs) all fit this instance. -/
theorem add52_spec (a b : Fe) (hba : Bnd a (2^52)) (hbb : Bnd b (2^52)) :
fe_add a b ⦃ r => Bnd r (2^53) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
apply spec_mono (add_spec'' (2^52) (by norm_num) a b hba hbb)
rintro r ⟨h1, h2⟩
exact ⟨h1.mono (by norm_num), h2⟩ -- 2·2⁵² = 2⁵³
/-- `fe_add` on two 2⁵³-bounded inputs: output bound 2⁵⁴ (still a legal
input for every field op — the dalek 2⁵⁴ discipline's outer edge).
MATH: Bnd(a,2⁵³), Bnd(b,2⁵³) ==> fe_add a b = ok r, Bnd(r,2⁵⁴),
⟪r⟫ = ⟪a⟫ + ⟪b⟫.
WHY NEEDED: the "second-generation" add ZZ2 + TT2d stacks on top of the
unreduced ZZ2 (Bnd 2⁵³), so it needs this wider instance. -/
theorem add53_spec (a b : Fe) (hba : Bnd a (2^53)) (hbb : Bnd b (2^53)) :
fe_add a b ⦃ r => Bnd r (2^54) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
apply spec_mono (add_spec'' (2^53) (by norm_num) a b hba hbb)
rintro r ⟨h1, h2⟩
exact ⟨h1.mono (by norm_num), h2⟩ -- 2·2⁵³ = 2⁵⁴
/-- Limb-free `fe_sub` spec (the "+16p then subtract, then reduce" trick).
Rust: `impl Sub<&FieldElement51> for &FieldElement51`,
u64/field.rs:84-101 — verified in Proofs/SubNegSpec.lean.
MATH: Bnd(a,2⁵⁴), Bnd(b,2⁵⁴) ==> fe_sub a b = ok r, Bnd(r,2⁵²),
⟪r⟫ = ⟪a⟫ ⟪b⟫.
WHY NEEDED: the kernels below subtract four times each (Y₁X₁, PPMM /
PMMP, ZZ2TT2d); this is `sub_spec` with the limbs repackaged so `let*`
can apply it. -/
theorem sub_spec' (a b : Fe) (hba : Bnd a (2^54)) (hbb : Bnd b (2^54)) :
fe_sub a b ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = ⟪a⟫ - ⟪b⟫ ⦄ := by
obtain ⟨a0, a1, a2, a3, a4, hA⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hB⟩ := Fe.exists_limbs b
exact sub_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hA hB hba hbb
/-- Limb-free `fe_neg` spec (16p a, then reduce).
Rust: `FieldElement51::negate`, u64/field.rs:276-286 — verified in
Proofs/SubNegSpec.lean.
MATH: Bnd(a,2⁵⁴) ==> fe_neg a = ok r, Bnd(r,2⁵²), ⟪r⟫ = ⟪a⟫.
WHY NEEDED: `ProjectiveNielsPoint::neg` (below) negates the T2d field. -/
theorem neg_spec' (a : Fe) (hba : Bnd a (2^54)) :
fe_neg a ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = -⟪a⟫ ⦄ := by
obtain ⟨a0, a1, a2, a3, a4, hA⟩ := Fe.exists_limbs a
exact neg_spec a a0 a1 a2 a3 a4 hA hba
/-- Discharge macro for the `let*` side conditions of this file (the `bnd`
pattern of InvertSpec.lean, re-declared because macros are local to
their file): every obligation is a `Bnd _ c` goal, closed either by an
exact hypothesis (`assumption`) or by weakening a tighter bound from the
context (`Bnd.mono` + `norm_num` on the ≤ between the two numerals);
`scalar_tac` mops up any residual linear-arithmetic goal.
(`name :=` disambiguates the generated syntax-kind declaration from the
sibling files' `edis` macros so they can all be imported together.) -/
macro (name := edisProjNiels) "edis" : tactic =>
`(tactic| (first
| assumption
| exact Bnd.mono (by assumption) (by norm_num)
| scalar_tac))
/-! ## 1. Mixed addition: EdwardsPoint + &ProjectiveNielsPoint → CompletedPoint -/
/-- Rust: `impl Add<&ProjectiveNielsPoint> for &EdwardsPoint`,
src/backend/serial/curve_models.rs:411-430; transpiled at
gen/CurveField/Funs.lean (`SharedAEdwardsPoint.Insts.
CoreOpsArithAddSharedBProjectiveNielsPointCompletedPoint.add`).
MATH (HWCD08 mixed addition, ℙ¹×ℙ¹ output): for an extended point P
(ExtValid: all coords Bnd 2⁵², ⟪Z⟫ ≠ 0, X·Y = Z·T) and a niels cache N
(ProjNielsValid: Y±X Bnd 2⁵³, Z/T2d Bnd 2⁵², ⟪Z⟫ ≠ 0), the kernel is
TOTAL (every intermediate field op stays inside the 2⁵⁴ discipline:
the 20 + … machine-op side conditions are discharged step by step) and
the completed-point output r satisfies
Bnd r.X 2⁵² (PP MM: reduced sub output)
Bnd r.Y 2⁵³ (PP + MM: one unreduced add of two ≤2⁵² mul outputs)
Bnd r.Z 2⁵⁴ (ZZ2 + TT2d: add stacked on the unreduced ZZ2 ≤ 2⁵³)
Bnd r.T 2⁵² (ZZ2 TT2d: reduced sub output)
⟪r.X⟫ = (⟪P.Y⟫+⟪P.X⟫)·⟪N.Y_plus_X⟫ (⟪P.Y⟫⟪P.X⟫)·⟪N.Y_minus_X⟫
⟪r.Y⟫ = (⟪P.Y⟫+⟪P.X⟫)·⟪N.Y_plus_X⟫ + (⟪P.Y⟫⟪P.X⟫)·⟪N.Y_minus_X⟫
⟪r.Z⟫ = 2·⟪P.Z⟫·⟪N.Z⟫ + ⟪P.T⟫·⟪N.T2d⟫
⟪r.T⟫ = 2·⟪P.Z⟫·⟪N.Z⟫ ⟪P.T⟫·⟪N.T2d⟫
— the computation order of the Rust source (PP, MM, TT2d, ZZ, ZZ2 = ZZ+ZZ,
then X' = PPMM, Y' = PP+MM, Z' = ZZ2+TT2d, T' = ZZ2TT2d) verbatim, with
each intermediate eliminated. Deliberately NO curve constant, division
or group-law claim here: combined with `IsNielsOf N Q` (EdDenote.lean)
the right-hand sides become the HWCD08 addition formulas for P + Q, which
the algebra-law packaging file exploits.
WHY NEEDED: this is the workhorse of scalar multiplication — every
table-lookup addition in the double-and-add ladder goes through it. -/
theorem add_projniels_spec (Pt : EdPoint) (N : ProjNiels)
(hPt : ExtValid Pt) (hN : ProjNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBProjectiveNielsPointCompletedPoint.add
Pt N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^52) ∧
⟪r.X⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.Y_plus_X⟫
- (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.Y_minus_X⟫ ∧
⟪r.Y⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.Y_plus_X⟫
+ (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.Y_minus_X⟫ ∧
⟪r.Z⟫ = 2 * ⟪Pt.Z⟫ * ⟪N.Z⟫ + ⟪Pt.T⟫ * ⟪N.T2d⟫ ∧
⟪r.T⟫ = 2 * ⟪Pt.Z⟫ * ⟪N.Z⟫ - ⟪Pt.T⟫ * ⟪N.T2d⟫ ⦄ := by
-- unpack the validity predicates into named Bnd facts for `edis`
obtain ⟨hPX, hPY, hPZ, hPT, _hPZ0, _hPcoh⟩ := hPt
obtain ⟨hNyp, hNym, hNZ, hNT, _hNZ0⟩ := hN
-- expose the transpiled 11-step monadic body
unfold SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBProjectiveNielsPointCompletedPoint.add
-- Y₁+X₁ : unreduced add of two reduced coordinates (Bnd 2⁵³);
-- preconditions are verbatim hypotheses, found by `let*` itself
let* ⟨ Y_plus_X, Ypx_bnd, Ypx_val ⟩ ← add52_spec
-- Y₁X₁ : reduced sub (Bnd 2⁵²)
let* ⟨ Y_minus_X, Ymx_bnd, Ymx_val ⟩ ← sub_spec' by edis
-- PP = (Y₁+X₁)·N.Y_plus_X
let* ⟨ PP, PP_bnd, PP_val ⟩ ← mul_spec' by edis
-- MM = (Y₁X₁)·N.Y_minus_X
let* ⟨ MM, MM_bnd, MM_val ⟩ ← mul_spec' by edis
-- TT2d = T₁·N.T2d
let* ⟨ TT2d, TT_bnd, TT_val ⟩ ← mul_spec' by edis
-- ZZ = Z₁·N.Z
let* ⟨ ZZ, ZZ_bnd, ZZ_val ⟩ ← mul_spec' by edis
-- ZZ2 = ZZ + ZZ (unreduced doubling, Bnd 2⁵³)
let* ⟨ ZZ2, ZZ2_bnd, ZZ2_val ⟩ ← add52_spec by edis
-- X' = PP MM
let* ⟨ rX, rX_bnd, rX_val ⟩ ← sub_spec' by edis
-- Y' = PP + MM
let* ⟨ rY, rY_bnd, rY_val ⟩ ← add52_spec by edis
-- Z' = ZZ2 + TT2d (the stacked add, Bnd 2⁵⁴)
let* ⟨ rZ, rZ_bnd, rZ_val ⟩ ← add53_spec by edis
-- T' = ZZ2 TT2d
let* ⟨ rT, rT_bnd, rT_val ⟩ ← sub_spec' by edis
-- `let*` already collapsed the final `ok {…}` constructor's projections;
-- bounds are the recorded step posts; equations close by rewriting the
-- chain of step values and (for Z/T) merging ZZ+ZZ into 2·ZZ by ring
refine ⟨rX_bnd, rY_bnd, rZ_bnd, rT_bnd, ?_, ?_, ?_, ?_⟩
· rw [rX_val, PP_val, MM_val, Ypx_val, Ymx_val]
· rw [rY_val, PP_val, MM_val, Ypx_val, Ymx_val]
· rw [rZ_val, ZZ2_val, ZZ_val, TT_val]; ring
· rw [rT_val, ZZ2_val, ZZ_val, TT_val]; ring
/-! ## 2. Mixed subtraction: EdwardsPoint &ProjectiveNielsPoint → CompletedPoint -/
/-- Rust: `impl Sub<&ProjectiveNielsPoint> for &EdwardsPoint`,
src/backend/serial/curve_models.rs:433-452; transpiled at
gen/CurveField/Funs.lean (`…SubSharedBProjectiveNielsPointCompletedPoint.sub`).
MATH: same hypotheses and totality as `add_projniels_spec`; the body is
the addition kernel with the cache's Y_plus_X/Y_minus_X CROSSED
(PM = (Y₁+X₁)·(Y₂X₂), MP = (Y₁X₁)·(Y₂+X₂)) and the Z'/T' roles of
ZZ2 ± TT2d swapped — algebraically, addition of the NEGATED niels point
(cf. `projniels_neg_spec` below: negation swaps Y±X and flips T2d):
Bnd r.X 2⁵², Bnd r.Y 2⁵³, Bnd r.Z 2⁵², Bnd r.T 2⁵⁴
(Z' is now the reduced SUB ZZ2TT2d and T' the stacked ADD ZZ2+TT2d,
so the 2⁵²/2⁵⁴ bounds trade places relative to `add_projniels_spec`)
⟪r.X⟫ = (⟪P.Y⟫+⟪P.X⟫)·⟪N.Y_minus_X⟫ (⟪P.Y⟫⟪P.X⟫)·⟪N.Y_plus_X⟫
⟪r.Y⟫ = (⟪P.Y⟫+⟪P.X⟫)·⟪N.Y_minus_X⟫ + (⟪P.Y⟫⟪P.X⟫)·⟪N.Y_plus_X⟫
⟪r.Z⟫ = 2·⟪P.Z⟫·⟪N.Z⟫ ⟪P.T⟫·⟪N.T2d⟫
⟪r.T⟫ = 2·⟪P.Z⟫·⟪N.Z⟫ + ⟪P.T⟫·⟪N.T2d⟫
WHY NEEDED: the signed-digit (NAF) scalar-multiplication ladder
subtracts table entries as often as it adds them. -/
theorem sub_projniels_spec (Pt : EdPoint) (N : ProjNiels)
(hPt : ExtValid Pt) (hN : ProjNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBProjectiveNielsPointCompletedPoint.sub
Pt N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^54) ∧
⟪r.X⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.Y_minus_X⟫
- (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.Y_plus_X⟫ ∧
⟪r.Y⟫ = (⟪Pt.Y⟫ + ⟪Pt.X⟫) * ⟪N.Y_minus_X⟫
+ (⟪Pt.Y⟫ - ⟪Pt.X⟫) * ⟪N.Y_plus_X⟫ ∧
⟪r.Z⟫ = 2 * ⟪Pt.Z⟫ * ⟪N.Z⟫ - ⟪Pt.T⟫ * ⟪N.T2d⟫ ∧
⟪r.T⟫ = 2 * ⟪Pt.Z⟫ * ⟪N.Z⟫ + ⟪Pt.T⟫ * ⟪N.T2d⟫ ⦄ := by
obtain ⟨hPX, hPY, hPZ, hPT, _hPZ0, _hPcoh⟩ := hPt
obtain ⟨hNyp, hNym, hNZ, hNT, _hNZ0⟩ := hN
unfold SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBProjectiveNielsPointCompletedPoint.sub
-- Y₁+X₁, Y₁X₁ — same prologue as the addition kernel
let* ⟨ Y_plus_X, Ypx_bnd, Ypx_val ⟩ ← add52_spec
let* ⟨ Y_minus_X, Ymx_bnd, Ymx_val ⟩ ← sub_spec' by edis
-- PM = (Y₁+X₁)·N.Y_minus_X (crossed relative to `add`)
let* ⟨ PM, PM_bnd, PM_val ⟩ ← mul_spec' by edis
-- MP = (Y₁X₁)·N.Y_plus_X
let* ⟨ MP, MP_bnd, MP_val ⟩ ← mul_spec' by edis
-- TT2d = T₁·N.T2d, ZZ = Z₁·N.Z, ZZ2 = ZZ+ZZ
let* ⟨ TT2d, TT_bnd, TT_val ⟩ ← mul_spec' by edis
let* ⟨ ZZ, ZZ_bnd, ZZ_val ⟩ ← mul_spec' by edis
let* ⟨ ZZ2, ZZ2_bnd, ZZ2_val ⟩ ← add52_spec by edis
-- X' = PM MP, Y' = PM + MP
let* ⟨ rX, rX_bnd, rX_val ⟩ ← sub_spec' by edis
let* ⟨ rY, rY_bnd, rY_val ⟩ ← add52_spec by edis
-- Z' = ZZ2 TT2d, T' = ZZ2 + TT2d (roles swapped relative to `add`)
let* ⟨ rZ, rZ_bnd, rZ_val ⟩ ← sub_spec' by edis
let* ⟨ rT, rT_bnd, rT_val ⟩ ← add53_spec by edis
refine ⟨rX_bnd, rY_bnd, rZ_bnd, rT_bnd, ?_, ?_, ?_, ?_⟩
· rw [rX_val, PM_val, MP_val, Ypx_val, Ymx_val]
· rw [rY_val, PM_val, MP_val, Ypx_val, Ymx_val]
· rw [rZ_val, ZZ2_val, ZZ_val, TT_val]; ring
· rw [rT_val, ZZ2_val, ZZ_val, TT_val]; ring
/-! ## 3. Negation of a projective-niels cache point -/
/-- Rust: `impl Neg for &ProjectiveNielsPoint`,
src/backend/serial/curve_models.rs:500-511; transpiled at
gen/CurveField/Funs.lean (`SharedAProjectiveNielsPoint.Insts.
CoreOpsArithNegProjectiveNielsPoint.neg`).
MATH: negating an Edwards point (x,y) ↦ (x,y) sends the cache
(Y+X, YX, Z, T·2d) to (YX, Y+X, Z, T·2d): the two sum/difference
fields SWAP, Z is untouched, and T2d is negated through the (total,
`neg_spec'`) field negation. Hence for ProjNielsValid N:
neg N = ok r, ProjNielsValid r (swap preserves the 2⁵³/2⁵³ bounds,
⟪r.Z⟫ = ⟪N.Z⟫ ≠ 0, and fe_neg outputs a reduced 2⁵² T2d), and
⟪r.Y_plus_X⟫ = ⟪N.Y_minus_X⟫, ⟪r.Y_minus_X⟫ = ⟪N.Y_plus_X⟫,
⟪r.Z⟫ = ⟪N.Z⟫, ⟪r.T2d⟫ = ⟪N.T2d⟫.
(Field-wise relational form, matching the statement policy: combined
with `IsNielsOf N Q` these four equations say exactly `IsNielsOf r (Q)`
— e.g. 121666·⟪r.T2d⟫ = 121666·⟪N.T2d⟫ = 243330·⟪Q.T⟫ = 243330·(⟪Q.T⟫)
— which the packaging file derives.)
WHY NEEDED: the NAF ladder materializes negative table digits through
this kernel; it also explains `sub_projniels_spec` as
"add the negation". -/
theorem projniels_neg_spec (N : ProjNiels) (hN : ProjNielsValid N) :
SharedAProjectiveNielsPoint.Insts.CoreOpsArithNegProjectiveNielsPoint.neg
N ⦃ r =>
ProjNielsValid r ∧
⟪r.Y_plus_X⟫ = ⟪N.Y_minus_X⟫ ∧ ⟪r.Y_minus_X⟫ = ⟪N.Y_plus_X⟫ ∧
⟪r.Z⟫ = ⟪N.Z⟫ ∧ ⟪r.T2d⟫ = -⟪N.T2d⟫ ⦄ := by
obtain ⟨hNyp, hNym, hNZ, hNT, hNZ0⟩ := hN
-- expose the body; the inner `…NegFieldElement51.neg` is a direct call to
-- `FieldElement51::negate` (= fe_neg), so unfold both layers
unfold SharedAProjectiveNielsPoint.Insts.CoreOpsArithNegProjectiveNielsPoint.neg
SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
-- t2d = N.T2d (total: Bnd 2⁵² ≤ 2⁵⁴; output reduced to 2⁵²)
let* ⟨ t2d, t2d_bnd, t2d_val ⟩ ← neg_spec' by edis
-- `let*` collapsed the `{ N with … }` constructor's projections and already
-- closed the three definitional field equations (Y±X swap, Z untouched);
-- remaining: validity (swapped bounds + Z ≠ 0 + reduced new T2d) and the
-- T2d value clause (= neg's post)
exact ⟨⟨hNym, hNyp, hNZ, t2d_bnd, hNZ0⟩, t2d_val⟩
end CurveFieldProofs

View file

@ -0,0 +1,453 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdConvert.lean — coordinate-level specs for the REPRESENTATION
CONVERSIONS between the four point models of curve25519/solana-ed25519.
CONTEXT. The Rust crate keeps Edwards points in four internal models
(see the header of Proofs/EdDenote.lean): extended ℙ³ (`EdwardsPoint`,
x = X/Z, y = Y/Z, Segre coherence X·Y = Z·T), projective ℙ²
(`ProjectivePoint`, x = X/Z, y = Y/Z), completed ℙ¹×ℙ¹
(`CompletedPoint`, x = X/Z, y = Y/T) and the readily-addable niels
caches (`ProjectiveNielsPoint` = (Y+X, YX, Z, T·2d),
`AffineNielsPoint`). The add/double kernels produce COMPLETED points;
the conversion methods specified here move the result back into the
model the next operation wants — each one is a handful of field
mul/square/add/sub calls and NOTHING else (no division ever happens at
runtime; the affine value is preserved because numerator and denominator
are multiplied by the same nonzero factor).
THIS FILE proves one spec per conversion, coordinate-level ONLY:
* `proj_as_extended_spec` — ProjectivePoint.as_extended
(X:Y:Z) ↦ (XZ : YZ : Z² : XY) [curve_models.rs:338-345]
* `compl_as_projective_spec` — CompletedPoint.as_projective
((X:Z),(Y:T)) ↦ (XT : YZ : ZT) [curve_models.rs:353-359]
* `compl_as_extended_spec` — CompletedPoint.as_extended
((X:Z),(Y:T)) ↦ (XT : YZ : ZT : XY) [curve_models.rs:365-372]
* `edwards_as_projective_niels_spec`— EdwardsPoint.as_projective_niels
(X:Y:Z:T) ↦ (Y+X, YX, Z, T·2d) [edwards.rs:528-535]
* `edwards_neg_spec` — Neg for &EdwardsPoint
(X:Y:Z:T) ↦ (X : Y : Z : T) [edwards.rs:844-851]
Each spec asserts, under the input validity predicate of EdDenote:
TOTALITY (the triple — every limb stays inside the dalek 2⁵²/2⁵⁴
discipline, so no u64/u128 overflow, no panic), the output VALIDITY
predicate (limb bounds + the Z ≠ 0 obligation that the Rust code never
states + Segre coherence where applicable), the per-field COORDINATE
EQUATIONS over 𝔽_p strictly in terms of the input struct-field
denotations (e.g. ⟪r.X⟫ = ⟪p.X⟫·⟪p.Z⟫ — no curve constants, no
division), and the resulting DENOTATION identities (edX/edY/projX/
projY/complX/complY agree across the conversion, resp. `IsNielsOf`).
The algebra-law packaging (group laws, OnCurve preservation) happens in
a later file (EdMain), which composes exactly these posts.
FUTURE WORK (deliberately skipped here):
* `EdwardsPoint.as_affine_niels` (edwards.rs:551-561) and
`to_affine`-style code — both run `invert` (a 254-squaring Fermat
chain); their specs belong next to the scalar-mul layer and need
`invert_spec` composition with the validity predicates.
PROOF TECHNIQUE. Identical to Proofs/InvertSpec.lean: unfold the
transpiled body, walk every field-op bind with `let* ⟨x, posts⟩ ← spec`
(the Aeneas step machinery), discharging each 2⁵⁴-bound side condition
with the `edis` macro below, then close the terminal `ok {…}` with
`spec_ok` and prove the conjunction — bound goals by `Bnd.mono`/
`norm_num`, value goals by rewriting the step posts and `ring`, and the
division identities by cross-multiplying with `fp_div_eq_div_iff`
(EdDenote) over the nonzero denominators.
Imports: Proofs/EdDenote.lean (validity predicates, denotations, the
EDWARDS_D2 characterization, division helpers) and Proofs/Square2Spec
(square2_spec' — not used by the conversions themselves, but imported
here so this file sits at the same layer as the doubling specs that
need it, keeping the downstream import graph linear).
Imported by: the forthcoming point-operation files (EdMain).
─────────────────────────────────────────────────────────────────────── -/
import Proofs.EdDenote
import Proofs.Square2Spec
open Aeneas Aeneas.Std Result
open Aeneas.Std.WP
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
namespace CurveFieldProofs
/-! ## Step-friendly wrappers for the remaining field ops
`mul_spec'`/`square_spec'`/`pow2k_spec'` (InvertSpec.lean) and
`square2_spec'` (Square2Spec.lean) are already `@[step]`-registered.
The point bodies additionally call `fe_add`, `fe_sub` and the
borrowed-`Neg` wrapper; their base specs (AddSpec.lean, SubNegSpec.lean)
take explicit limb lists, which the step machinery cannot invent, so —
exactly as in InvertSpec — we re-state them with the limbs repackaged
via `Fe.exists_limbs` and register the wrappers with `@[step]`. -/
/-- Step-friendly `fe_add` spec at the REDUCED input level.
Rust: `impl Add<&FieldElement51> for &FieldElement51`, u64/field.rs:58-73
(limbwise `a[i] + b[i]`, NO carry, NO reduction — Proofs/AddSpec.lean).
MATH: Bnd(a,2⁵²) and Bnd(b,2⁵²) ==> fe_add a b = ok r with
Bnd(r, 2⁵³) and ⟪r⟫ = ⟪a⟫ + ⟪b⟫ in 𝔽_p.
The 2⁵² → 2⁵³ instantiation is the one the point code lives on: every
`Y + X` in a niels-cache construction adds two REDUCED coordinates, and
the doubled bound 2⁵³ < 2⁵⁴ keeps the sum a legal input for any
subsequent mul/sub. Derived from `add_spec` (AddSpec.lean): its
pairwise-overflow hypothesis holds since a_i + b_i < 2⁵² + 2⁵² = 2⁵³
< 2⁶⁴; its generic bound law `∀ c, Bnd a c → Bnd b c → Bnd r (2c)` is
instantiated at c = 2⁵²; its EXACT value equation
`feVal r = feVal a + feVal b` is cast into 𝔽_p by `push_cast`.
WHY NEEDED: `as_projective_niels` below computes Y_plus_X with this
unreduced add; the addition/doubling kernels of the next file do too. -/
@[step]
theorem add_spec'' (a b : Fe) (hba : Bnd a (2^52)) (hbb : Bnd b (2^52)) :
fe_add a b ⦃ r => Bnd r (2^53) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
-- materialize the limbs of both inputs and restate the bounds limbwise
obtain ⟨a0, a1, a2, a3, a4, ha⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hb⟩ := Fe.exists_limbs b
have hba' := hba
have hbb' := hbb
rw [Bnd_eq a a0 a1 a2 a3 a4 _ ha] at hba'
rw [Bnd_eq b b0 b1 b2 b3 b4 _ hb] at hbb'
-- run the base spec; the 5 pairwise sums are < 2⁵³ < 2⁶⁴ (omega)
apply spec_mono (add_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 ha hb
⟨by omega, by omega, by omega, by omega, by omega⟩)
rintro r ⟨-, hval, hbnd⟩
constructor
· -- bound: the generic law at c = 2⁵² gives 2·2⁵² = 2⁵³
exact (hbnd _ hba hbb).mono (by norm_num)
· -- value: cast the exact equation feVal r = feVal a + feVal b to 𝔽_p
simp only [denote]
rw [hval]
push_cast
ring
/-- Step-friendly `fe_sub` spec (limbs hidden, `@[step]`-registered).
Rust: `impl Sub<&FieldElement51> for &FieldElement51`,
u64/field.rs:84-101 (adds the constant 16p limbwise before subtracting
so u64 subtraction cannot underflow, then reduces —
Proofs/SubNegSpec.lean).
MATH: Bnd(a,2⁵⁴) and Bnd(b,2⁵⁴) ==> fe_sub a b = ok r with
Bnd(r, 2⁵²) and ⟪r⟫ = ⟪a⟫ ⟪b⟫ in 𝔽_p.
WHY NEEDED: `Y X` in the niels-cache construction below; the
addition/doubling kernels of the next file subtract throughout. -/
@[step]
theorem sub_spec'' (a b : Fe) (hba : Bnd a (2^54)) (hbb : Bnd b (2^54)) :
fe_sub a b ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = ⟪a⟫ - ⟪b⟫ ⦄ := by
obtain ⟨a0, a1, a2, a3, a4, ha⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hb⟩ := Fe.exists_limbs b
exact sub_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 ha hb hba hbb
/-- Step-friendly spec for the borrowed-`Neg` wrapper.
Rust: `impl Neg for &FieldElement51 { fn neg }`, u64/field.rs:218-222 —
literally `self.negate()`; transpiled at gen/CurveField/Funs.lean:1732
as a one-line `do`-wrapper around `FieldElement51.negate`
(= `fe_neg`, verified in Proofs/SubNegSpec.lean).
MATH: Bnd(a,2⁵⁴) ==> neg a = ok r with Bnd(r, 2⁵²) and
⟪r⟫ = ⟪a⟫ in 𝔽_p.
Stated about the WRAPPER (the name the point bodies actually call) so
the step machinery matches it syntactically.
WHY NEEDED: `EdwardsPoint::neg` below negates X and T through it. -/
@[step]
theorem neg_spec'' (a : Fe) (hba : Bnd a (2^54)) :
SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg a
⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = -⟪a⟫ ⦄ := by
-- the wrapper body is exactly `negate self`
unfold SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
obtain ⟨a0, a1, a2, a3, a4, ha⟩ := Fe.exists_limbs a
exact neg_spec a a0 a1 a2 a3 a4 ha hba
/-- Discharge macro for the step side conditions of this file (local copy of
InvertSpec's `bnd` — tactic macros do not travel across files): every
field-op step demands `Bnd · (2⁵⁴)` (or 2⁵² for `add_spec''`) on its
inputs while the context holds the tighter validity bounds (2⁵²/2⁵³
from the predicates, 2⁵¹+2¹³ from previous steps); close such goals by
direct assumption, by `scalar_tac`, or by weakening any `Bnd`
hypothesis with `Bnd.mono` + `norm_num`.
(`name :=` disambiguates the generated syntax-kind declaration from the
sibling files' `edis` macros so they can all be imported together.) -/
macro (name := edisConvert) "edis" : tactic =>
`(tactic| (first
| assumption
| scalar_tac
| exact Bnd.mono (by assumption) (by norm_num)))
/-! ## 1. ProjectivePoint → EdwardsPoint -/
/-- Rust: `ProjectivePoint::as_extended`, curve_models.rs:338-345 —
"Convert this point from the ℙ² model to the ℙ³ model. This costs
3M + 1S."; transpiled at gen/CurveField/Funs.lean:1360.
CODE: X' = X·Z, Y' = Y·Z, Z' = Z², T' = X·Y.
MATH: ProjValid p ==> as_extended p = ok r with
* ExtValid r — all four outputs are mul/square outputs (bound
2⁵¹+2¹³ ≤ 2⁵²); ⟪r.Z⟫ = ⟪p.Z⟫² ≠ 0 since ⟪p.Z⟫ ≠ 0; Segre holds
BY CONSTRUCTION: (XZ)·(YZ) = (Z²)·(XY) — pure `ring`;
* the four coordinate equations
⟪r.X⟫ = ⟪p.X⟫·⟪p.Z⟫, ⟪r.Y⟫ = ⟪p.Y⟫·⟪p.Z⟫,
⟪r.Z⟫ = ⟪p.Z⟫·⟪p.Z⟫, ⟪r.T⟫ = ⟪p.X⟫·⟪p.Y⟫;
* the affine point is UNCHANGED: edX r = projX p, edY r = projY p
(numerator and denominator both gained the factor ⟪p.Z⟫ ≠ 0:
(XZ)/(Z²) = X/Z, cross-multiplied via `fp_div_eq_div_iff`).
WHY NEEDED: `double_and_add`-style chains re-extend the running
projective point before each extended-coordinates addition. -/
theorem proj_as_extended_spec (p : ProjPoint) (hp : ProjValid p) :
backend.serial.curve_models.ProjectivePoint.as_extended p ⦃ r =>
ExtValid r ∧
⟪r.X⟫ = ⟪p.X⟫ * ⟪p.Z⟫ ∧ ⟪r.Y⟫ = ⟪p.Y⟫ * ⟪p.Z⟫ ∧
⟪r.Z⟫ = ⟪p.Z⟫ * ⟪p.Z⟫ ∧ ⟪r.T⟫ = ⟪p.X⟫ * ⟪p.Y⟫ ∧
edX r = projX p ∧ edY r = projY p ⦄ := by
obtain ⟨hX, hY, hZ, hZ0⟩ := hp
-- expose the 4-step transpiled body
unfold backend.serial.curve_models.ProjectivePoint.as_extended
-- fe ← mul X Z with ⟪fe⟫ = ⟪p.X⟫·⟪p.Z⟫
let* ⟨ fe, fe_post1, fe_post2 ⟩ ← mul_spec' by edis
-- fe1 ← mul Y Z with ⟪fe1⟫ = ⟪p.Y⟫·⟪p.Z⟫
let* ⟨ fe1, fe1_post1, fe1_post2 ⟩ ← mul_spec' by edis
-- fe2 ← square Z with ⟪fe2⟫ = ⟪p.Z⟫·⟪p.Z⟫
let* ⟨ fe2, fe2_post1, fe2_post2 ⟩ ← square_spec' by edis
-- fe3 ← mul X Y with ⟪fe3⟫ = ⟪p.X⟫·⟪p.Y⟫
let* ⟨ fe3, fe3_post1, fe3_post2 ⟩ ← mul_spec' by edis
-- the terminal `ok {X := fe, Y := fe1, Z := fe2, T := fe3}` was already
-- consumed by the step machinery (projections collapsed); unfold the
-- predicate and the four denotations to expose the conjunction
simp only [ExtValid, edX, edY, projX, projY]
-- the new denominator ⟪fe2⟫ = ⟪p.Z⟫² is nonzero
have hrZ : ⟪fe2⟫ ≠ 0 := by
rw [fe2_post2]; exact mul_ne_zero hZ0 hZ0
refine ⟨⟨fe_post1.mono (by norm_num), fe1_post1.mono (by norm_num),
fe2_post1.mono (by norm_num), fe3_post1.mono (by norm_num),
hrZ, ?_⟩,
fe_post2, fe1_post2, fe2_post2, fe3_post2, ?_, ?_⟩
· -- Segre coherence: (XZ)·(YZ) = (Z²)·(XY)
rw [fe_post2, fe1_post2, fe2_post2, fe3_post2]; ring
· -- x preserved: (XZ)/(Z²) = X/Z ⟺ (XZ)·Z = X·Z²
rw [fp_div_eq_div_iff hrZ hZ0, fe_post2, fe2_post2]; ring
· -- y preserved: (YZ)/(Z²) = Y/Z ⟺ (YZ)·Z = Y·Z²
rw [fp_div_eq_div_iff hrZ hZ0, fe1_post2, fe2_post2]; ring
/-! ## 2. CompletedPoint → ProjectivePoint -/
/-- Rust: `CompletedPoint::as_projective`, curve_models.rs:353-359 —
"Convert this point from the ℙ¹×ℙ¹ model to the ℙ² model. This costs
3M."; transpiled at gen/CurveField/Funs.lean:1379.
CODE: X' = X·T, Y' = Y·Z, Z' = Z·T.
MATH: ComplValid p ==> as_projective p = ok r with
* ProjValid r — three mul outputs (≤ 2⁵²), and
⟪r.Z⟫ = ⟪p.Z⟫·⟪p.T⟫ ≠ 0 because BOTH completed denominators are
nonzero (`mul_ne_zero`);
* the coordinate equations ⟪r.X⟫ = ⟪p.X⟫·⟪p.T⟫,
⟪r.Y⟫ = ⟪p.Y⟫·⟪p.Z⟫, ⟪r.Z⟫ = ⟪p.Z⟫·⟪p.T⟫;
* the affine point is UNCHANGED: projX r = complX p (the x-fraction
X/Z was multiplied through by T) and projY r = complY p (the
y-fraction Y/T was multiplied through by Z) — the two ℙ¹ lines are
put over the COMMON denominator Z·T.
WHY NEEDED: every doubling step of a scalar-mul ladder feeds the
completed output back as a projective point through this conversion. -/
theorem compl_as_projective_spec (p : ComplPoint) (hp : ComplValid p) :
backend.serial.curve_models.CompletedPoint.as_projective p ⦃ r =>
ProjValid r ∧
⟪r.X⟫ = ⟪p.X⟫ * ⟪p.T⟫ ∧ ⟪r.Y⟫ = ⟪p.Y⟫ * ⟪p.Z⟫ ∧
⟪r.Z⟫ = ⟪p.Z⟫ * ⟪p.T⟫ ∧
projX r = complX p ∧ projY r = complY p ⦄ := by
obtain ⟨hX, hY, hZ, hT, hZ0, hT0⟩ := hp
-- expose the 3-step transpiled body
unfold backend.serial.curve_models.CompletedPoint.as_projective
-- fe ← mul X T with ⟪fe⟫ = ⟪p.X⟫·⟪p.T⟫
let* ⟨ fe, fe_post1, fe_post2 ⟩ ← mul_spec' by edis
-- fe1 ← mul Y Z with ⟪fe1⟫ = ⟪p.Y⟫·⟪p.Z⟫
let* ⟨ fe1, fe1_post1, fe1_post2 ⟩ ← mul_spec' by edis
-- fe2 ← mul Z T with ⟪fe2⟫ = ⟪p.Z⟫·⟪p.T⟫
let* ⟨ fe2, fe2_post1, fe2_post2 ⟩ ← mul_spec' by edis
-- the terminal `ok {X := fe, Y := fe1, Z := fe2}` was already consumed by
-- the step machinery (projections collapsed); unfold predicate/denotations
simp only [ProjValid, projX, projY, complX, complY]
-- the common denominator ⟪fe2⟫ = ⟪p.Z⟫·⟪p.T⟫ is nonzero
have hrZ : ⟪fe2⟫ ≠ 0 := by
rw [fe2_post2]; exact mul_ne_zero hZ0 hT0
refine ⟨⟨fe_post1.mono (by norm_num), fe1_post1.mono (by norm_num),
fe2_post1.mono (by norm_num), hrZ⟩,
fe_post2, fe1_post2, fe2_post2, ?_, ?_⟩
· -- x preserved: (XT)/(ZT) = X/Z ⟺ (XT)·Z = X·(ZT)
rw [fp_div_eq_div_iff hrZ hZ0, fe_post2, fe2_post2]; ring
· -- y preserved: (YZ)/(ZT) = Y/T ⟺ (YZ)·T = Y·(ZT)
rw [fp_div_eq_div_iff hrZ hT0, fe1_post2, fe2_post2]; ring
/-! ## 3. CompletedPoint → EdwardsPoint -/
/-- Rust: `CompletedPoint::as_extended`, curve_models.rs:365-372 —
"Convert this point from the ℙ¹×ℙ¹ model to the ℙ³ model. This costs
4M."; transpiled at gen/CurveField/Funs.lean:1397.
CODE: X' = X·T, Y' = Y·Z, Z' = Z·T, T' = X·Y.
MATH: ComplValid p ==> as_extended p = ok r with
* ExtValid r — four mul outputs (≤ 2⁵²); ⟪r.Z⟫ = ⟪p.Z⟫·⟪p.T⟫ ≠ 0
(`mul_ne_zero` on the two completed denominators); Segre BY
CONSTRUCTION: (XT)·(YZ) = (ZT)·(XY) — pure `ring` (this is
exactly why the extended T-cache is computed as X·Y here:
T'/Z' = (X/Z)·(Y/T) = x·y);
* the coordinate equations ⟪r.X⟫ = ⟪p.X⟫·⟪p.T⟫,
⟪r.Y⟫ = ⟪p.Y⟫·⟪p.Z⟫, ⟪r.Z⟫ = ⟪p.Z⟫·⟪p.T⟫, ⟪r.T⟫ = ⟪p.X⟫·⟪p.Y⟫;
* the affine point is UNCHANGED: edX r = complX p,
edY r = complY p (same common-denominator argument as
`compl_as_projective_spec`).
WHY NEEDED: the result of a point addition (a completed point) is
re-extended through this conversion whenever the next operation needs
the T-cache (e.g. another addition or a niels-cache build). -/
theorem compl_as_extended_spec (p : ComplPoint) (hp : ComplValid p) :
backend.serial.curve_models.CompletedPoint.as_extended p ⦃ r =>
ExtValid r ∧
⟪r.X⟫ = ⟪p.X⟫ * ⟪p.T⟫ ∧ ⟪r.Y⟫ = ⟪p.Y⟫ * ⟪p.Z⟫ ∧
⟪r.Z⟫ = ⟪p.Z⟫ * ⟪p.T⟫ ∧ ⟪r.T⟫ = ⟪p.X⟫ * ⟪p.Y⟫ ∧
edX r = complX p ∧ edY r = complY p ⦄ := by
obtain ⟨hX, hY, hZ, hT, hZ0, hT0⟩ := hp
-- expose the 4-step transpiled body
unfold backend.serial.curve_models.CompletedPoint.as_extended
-- fe ← mul X T with ⟪fe⟫ = ⟪p.X⟫·⟪p.T⟫
let* ⟨ fe, fe_post1, fe_post2 ⟩ ← mul_spec' by edis
-- fe1 ← mul Y Z with ⟪fe1⟫ = ⟪p.Y⟫·⟪p.Z⟫
let* ⟨ fe1, fe1_post1, fe1_post2 ⟩ ← mul_spec' by edis
-- fe2 ← mul Z T with ⟪fe2⟫ = ⟪p.Z⟫·⟪p.T⟫
let* ⟨ fe2, fe2_post1, fe2_post2 ⟩ ← mul_spec' by edis
-- fe3 ← mul X Y with ⟪fe3⟫ = ⟪p.X⟫·⟪p.Y⟫
let* ⟨ fe3, fe3_post1, fe3_post2 ⟩ ← mul_spec' by edis
-- the terminal `ok {X := fe, Y := fe1, Z := fe2, T := fe3}` was already
-- consumed by the step machinery (projections collapsed); unfold
-- predicate/denotations
simp only [ExtValid, edX, edY, complX, complY]
-- the common denominator ⟪fe2⟫ = ⟪p.Z⟫·⟪p.T⟫ is nonzero
have hrZ : ⟪fe2⟫ ≠ 0 := by
rw [fe2_post2]; exact mul_ne_zero hZ0 hT0
refine ⟨⟨fe_post1.mono (by norm_num), fe1_post1.mono (by norm_num),
fe2_post1.mono (by norm_num), fe3_post1.mono (by norm_num),
hrZ, ?_⟩,
fe_post2, fe1_post2, fe2_post2, fe3_post2, ?_, ?_⟩
· -- Segre coherence: (XT)·(YZ) = (ZT)·(XY)
rw [fe_post2, fe1_post2, fe2_post2, fe3_post2]; ring
· -- x preserved: (XT)/(ZT) = X/Z ⟺ (XT)·Z = X·(ZT)
rw [fp_div_eq_div_iff hrZ hZ0, fe_post2, fe2_post2]; ring
· -- y preserved: (YZ)/(ZT) = Y/T ⟺ (YZ)·T = Y·(ZT)
rw [fp_div_eq_div_iff hrZ hT0, fe1_post2, fe2_post2]; ring
/-! ## 4. EdwardsPoint → ProjectiveNielsPoint -/
/-- Rust: `EdwardsPoint::as_projective_niels`, edwards.rs:528-535 —
"Convert to a ProjectiveNielsPoint"; transpiled at
gen/CurveField/Funs.lean:3165.
CODE: Y_plus_X = Y + X, Y_minus_X = Y X, Z = Z,
T2d = T · EDWARDS_D2.
MATH: ExtValid P ==> as_projective_niels P = ok r with
* ProjNielsValid r — Y_plus_X is the single UNREDUCED add of two
reduced coordinates (bound 2⁵³, `add_spec''`), Y_minus_X a reduced
sub output (2⁵² ≤ 2⁵³), Z is P.Z verbatim (2⁵²), T2d a mul output
(≤ 2⁵²); ⟪r.Z⟫ = ⟪P.Z⟫ ≠ 0 carries over;
* IsNielsOf r P — the cache really derives from P (the EXACT shape
EdDenote fixed):
⟪r.Y_plus_X⟫ = ⟪P.Y⟫ + ⟪P.X⟫,
⟪r.Y_minus_X⟫ = ⟪P.Y⟫ ⟪P.X⟫,
⟪r.Z⟫ = ⟪P.Z⟫,
121666·⟪r.T2d⟫ = 243330·⟪P.T⟫
(the last is the denominator-free characterization of
⟪r.T2d⟫ = ⟪P.T⟫·2d: the EDWARDS_D2 step yields the table entry D2
with 121666·⟪D2⟫ = 243330 (`edwards_d2_spec`, EdDenote) and the
mul step yields ⟪r.T2d⟫ = ⟪P.T⟫·⟪D2⟫; multiply the latter by
121666 and substitute).
WHY NEEDED: every extended-coordinates point addition `P + Q` first
caches Q in this form; the next file's add/sub specs consume exactly
`ProjNielsValid` + `IsNielsOf`. -/
theorem edwards_as_projective_niels_spec (P : EdPoint) (hP : ExtValid P) :
edwards.EdwardsPoint.as_projective_niels P ⦃ r =>
ProjNielsValid r ∧ IsNielsOf r P ⦄ := by
obtain ⟨hX, hY, hZ, hT, hZ0, -⟩ := hP
-- expose the 4-step transpiled body
unfold edwards.EdwardsPoint.as_projective_niels
-- fe ← add Y X with ⟪fe⟫ = ⟪P.Y⟫ + ⟪P.X⟫, Bnd 2⁵³
-- (no discharge needed: the 2⁵² preconditions are hypotheses verbatim)
let* ⟨ fe, fe_post1, fe_post2 ⟩ ← add_spec''
-- fe1 ← sub Y X with ⟪fe1⟫ = ⟪P.Y⟫ ⟪P.X⟫, Bnd 2⁵²
let* ⟨ fe1, fe1_post1, fe1_post2 ⟩ ← sub_spec'' by edis
-- fe2 ← EDWARDS_D2 with 121666·⟪fe2⟫ = 243330 (the 2d table
-- entry; a closed constant — no preconditions to discharge)
let* ⟨ fe2, fe2_post1, fe2_post2 ⟩ ← edwards_d2_spec
-- fe3 ← mul T fe2 with ⟪fe3⟫ = ⟪P.T⟫·⟪fe2⟫
let* ⟨ fe3, fe3_post1, fe3_post2 ⟩ ← mul_spec' by edis
-- the terminal `ok {…}` was already consumed by the step machinery (which
-- also collapsed the constructor projections, so the ⟪r.Z⟫ = ⟪P.Z⟫
-- conjunct is already `True`); unfold the two predicates to expose the
-- conjunction
simp only [ProjNielsValid, IsNielsOf]
refine ⟨⟨fe_post1, fe1_post1.mono (by norm_num), hZ,
fe3_post1.mono (by norm_num), hZ0⟩,
fe_post2, fe1_post2, trivial, ?_⟩
-- T2d characterization: 121666·(⟪P.T⟫·⟪fe2⟫) = ⟪P.T⟫·(121666·⟪fe2⟫)
-- = ⟪P.T⟫·(243330) = 243330·⟪P.T⟫
calc (121666 : Fp) * ⟪fe3⟫
= ⟪P.T⟫ * ((121666 : Fp) * ⟪fe2⟫) := by rw [fe3_post2]; ring
_ = -243330 * ⟪P.T⟫ := by rw [fe2_post2]; ring
/-! ## 5. Negation of an EdwardsPoint -/
/-- Rust: `impl Neg for &EdwardsPoint { fn neg }`, edwards.rs:844-851 —
negate X and T, keep Y and Z; transpiled at
gen/CurveField/Funs.lean:3371.
CODE: r = (X : Y : Z : T).
MATH: ExtValid P ==> neg P = ok r with
* ExtValid r — the two negate outputs are reduced (2⁵²,
`neg_spec''`), Y/Z are P's verbatim; ⟪r.Z⟫ = ⟪P.Z⟫ ≠ 0 carries
over; Segre is PRESERVED: (X)·Y = Z·(T) follows from
X·Y = Z·T by negating both sides;
* the coordinate equations ⟪r.X⟫ = ⟪P.X⟫, ⟪r.Y⟫ = ⟪P.Y⟫,
⟪r.Z⟫ = ⟪P.Z⟫, ⟪r.T⟫ = ⟪P.T⟫;
* the denoted affine point is the EDWARDS NEGATIVE:
edX r = (edX P) (X/Z = (X/Z), `neg_div`) and edY r = edY P
— on a twisted Edwards curve (x, y) = (x, y).
WHY NEEDED: subtraction `P Q` is implemented as `P + (Q)`; the
group-law layer (EdMain) packages this spec as the implementation of
`edNeg` (EdCurve.lean). -/
theorem edwards_neg_spec (P : EdPoint) (hP : ExtValid P) :
SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg P ⦃ r =>
ExtValid r ∧
⟪r.X⟫ = -⟪P.X⟫ ∧ ⟪r.Y⟫ = ⟪P.Y⟫ ∧ ⟪r.Z⟫ = ⟪P.Z⟫ ∧ ⟪r.T⟫ = -⟪P.T⟫ ∧
edX r = -(edX P) ∧ edY r = edY P ⦄ := by
obtain ⟨hX, hY, hZ, hT, hZ0, hSeg⟩ := hP
-- expose the 2-step transpiled body
unfold SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
-- fe ← neg X with ⟪fe⟫ = ⟪P.X⟫, Bnd 2⁵²
let* ⟨ fe, fe_post1, fe_post2 ⟩ ← neg_spec'' by edis
-- fe1 ← neg T with ⟪fe1⟫ = ⟪P.T⟫, Bnd 2⁵²
let* ⟨ fe1, fe1_post1, fe1_post2 ⟩ ← neg_spec'' by edis
-- the terminal `ok { P with X := fe, T := fe1 }` (= ok (mk fe P.Y P.Z fe1))
-- was already consumed by the step machinery, which also collapsed the
-- projections: the Y/Z coordinate equations and `edY r = edY P` are
-- already `True`; unfold the predicate/denotation defs to expose the rest
simp only [ExtValid, edX, edY]
refine ⟨⟨fe_post1, hY, hZ, fe1_post1, hZ0, ?_⟩,
fe_post2, fe1_post2, ?_, trivial⟩
· -- Segre preserved: (X)·Y = (X·Y) = (Z·T) = Z·(T)
rw [fe_post2, fe1_post2, neg_mul, hSeg, mul_neg]
· -- x negated: ⟪fe⟫/⟪P.Z⟫ = (⟪P.X⟫)/⟪P.Z⟫ = (⟪P.X⟫/⟪P.Z⟫)
rw [fe_post2, neg_div]
end CurveFieldProofs

View file

@ -0,0 +1,588 @@
/-
═══════════════════════════════════════════════════════════════════════════════
Proofs/EdCurve.lean — pure mathematics of the curve25519 twisted Edwards curve
(curve constant d, completeness of the addition law,
and the basic point-arithmetic laws over 𝔽_p)
═══════════════════════════════════════════════════════════════════════════════
WHAT THIS FILE PROVES (all in 𝔽_p, p = 2²⁵⁵ 19, over `Fp := ZMod P` from
Proofs/Field.lean — no transpiled code appears here):
* `edD` — the Ed25519 curve constant d = 121665/121666 ∈ 𝔽_p,
with its decode-friendly characterization `edD_char`.
* `OnCurve x y` — the twisted Edwards curve equation with a = 1:
x² + y² = 1 + d·x²·y² (the Ed25519 curve x²+y² =
1 + d x² y², RFC 8032 §5.1).
* `edAdd/edNeg/edId`— the complete twisted Edwards addition law, negation
and neutral element on coordinate pairs.
* `edD_not_square` — d is a quadratic NON-residue mod p. This is the
number-theoretic heart of the file: by Euler's
criterion it reduces to the 255-bit exponentiation
d^((p1)/2) ≡ 1 (mod p), which the Lean KERNEL
checks via a fuel-based `powMod` (the technique of
Proofs/P25519.lean — no `native_decide`, no axioms).
* `completeness` — THE BernsteinLange completeness theorem (BBJLP,
"Twisted Edwards curves" / BernsteinLange "Faster
addition and doubling on elliptic curves", Thm 3.3):
because d is not a square (and 1 IS a square), the
denominators 1 ± d·x₁x₂y₁y₂ of the addition law NEVER
vanish on curve points. Hence `edAdd` is total: no
case distinctions, no exceptional pairs — the property
that makes Edwards form attractive for constant-time
cryptography in the first place.
* `onCurve_id`, `onCurve_neg`, `edAdd_id`, `edAdd_comm`, `edAdd_neg`,
`edAdd_closure` — the mechanical group-operation laws: (0,1) is neutral,
negation stays on the curve, p + (p) = identity,
addition is commutative and CLOSED on the curve.
(Associativity is deliberately out of scope — Tier 2.)
RUST ANALOG (indirect — this file is meta-level mathematics):
curve25519/solana-ed25519/src/backend/serial/u64/constants.rs defines
`EDWARDS_D` (the limb encoding of d = 121665/121666) and `SQRT_M1`;
src/edwards.rs implements point addition in extended coordinates whose
projective denominators are exactly the 1 ± d·x₁x₂y₁y₂ treated here. The
Rust code never checks for exceptional cases — `completeness` is the
mathematical fact that justifies this.
PLACE IN THE IMPORT GRAPH
Imports Proofs.Field (for `P`, `Fp := ZMod P`, the `Fact (Nat.Prime P)` and
`NeZero P` instances) plus mathlib (Euler's criterion). Nothing imports it
yet: it is the Tier-1 pure-mathematics layer for the upcoming verification
of the transpiled twisted Edwards point arithmetic.
PROOF TECHNIQUE, FOR THE LAY READER
1. Big-number facts (d^((p1)/2) = 1, sqrt(1)² = 1, the canonical
residue of d) are stated as closed equations between `Nat` literals and
checked by the KERNEL with `decide`, through the same fuel-based
square-and-multiply `powMod` used by Proofs/P25519.lean. GMP-backed
kernel `Nat` arithmetic makes each check milliseconds.
2. Algebraic identities on the curve are proved with `linear_combination`:
every identity is exhibited as an EXPLICIT polynomial combination of the
two curve equations (the cofactor polynomials below were computed and
verified offline with an exact Gröbner-basis computation; the Lean
`ring` normalizer re-verifies them from scratch, so they are trusted
only as HINTS, not as facts).
3. The completeness argument follows BernsteinLange: if a denominator
1 ± d·x₁x₂y₁y₂ vanished, d = (…/…)² would be a square — contradiction
with `edD_not_square`. The a = 1 twist is handled directly using
i = √1 ∈ 𝔽_p (p ≡ 1 mod 4): the role (x₁ ± y₁)² plays for a = 1 is
played by (i·x₁ ± ε·y₁)² here.
-/
import Proofs.Field
import Mathlib.NumberTheory.LegendreSymbol.Basic
import Mathlib.FieldTheory.Finite.Basic
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.FieldSimp
-- Big decimal literals (255-bit numbers) build deep numeral terms during
-- elaboration; same limits as Proofs/P25519.lean and Proofs/Field.lean.
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
namespace CurveFieldProofs
/-! ## Kernel-checkable modular exponentiation
The technique of Proofs/P25519.lean, recreated here so this file depends only
on the MATHEMATICAL interface of Proofs/Field.lean (`P`, `Fp`, the instances)
and not on the primality certificate's internal helpers: a fuel-based
square-and-multiply on raw `Nat`, with a once-proved correctness lemma. Each
255-bit exponentiation below then becomes a single closed `Nat` equation that
the kernel `decide`s with GMP big-integer arithmetic in milliseconds — no
`native_decide`, no axioms. -/
/-- Fuel-based binary modular exponentiation, kernel-reducible.
MATH (for sufficient fuel; made precise by `powModAux_eq`):
`powModAux fuel a k n = a^k mod n`.
Algorithm: square-and-multiply along the binary digits of `k`, every
intermediate reduced mod n (so nothing exceeds n² ≈ 510 bits here).
WHY THE `fuel` ARGUMENT: structural recursion on `fuel` is what the kernel
can unfold step by step during `decide`; recursion on `k/2 < k` would compile
to `WellFounded.fix`, which the kernel cannot evaluate. -/
def powModAux : Nat → Nat → Nat → Nat → Nat
| 0, _, _, n => 1 % n
| fuel + 1, a, k, n =>
if k = 0 then 1 % n
else if k % 2 = 1 then powModAux fuel (a * a % n) (k / 2) n * a % n
else powModAux fuel (a * a % n) (k / 2) n
/- Correctness of `powModAux`.
MATH (ASCII): forall fuel a k n, k < 2^fuel ==>
powModAux fuel a k n = a^k mod n
The hypothesis `k < 2^fuel` says the fuel covers every binary digit of the
exponent, so the recursion never runs dry.
WHY NEEDED: turns each kernel computation `powMod a k n = …` into the
mathematical statement `a^k % n = …` consumed by the bridge lemmas below.
Proof: induction on `fuel`, mirroring the recursion of `powModAux`. -/
theorem powModAux_eq : ∀ (fuel a k n : ), k < 2 ^ fuel → powModAux fuel a k n = a ^ k % n := by
intro fuel
induction fuel with
| zero =>
-- base case: k < 2^0 = 1 forces k = 0, and both sides reduce to 1 % n
intro a k n hk
rw [pow_zero] at hk
have hk0 : k = 0 := by omega
subst hk0
simp [powModAux]
| succ f ih =>
intro a k n hk
by_cases hk0 : k = 0
-- k = 0: both sides are 1 % n by definition
· subst hk0; simp [powModAux]
-- k ≠ 0: the recursive call gets exponent k/2, which fits in f bits…
· have hk2 : k / 2 < 2 ^ f := by
rw [pow_succ] at hk
omega
-- …so the induction hypothesis describes it: (a²%n)^(k/2) % n
have hrec := ih (a * a % n) (k / 2) n hk2
have haa : a * a = a ^ 2 := (pow_two a).symm
simp only [powModAux, if_neg hk0]
-- split on the lowest bit of k and reassemble the exponent:
by_cases hodd : k % 2 = 1
-- odd k: (a²)^(k/2) · a = a^(2·(k/2)+1) = a^k (mods commute via Nat.pow_mod)
· rw [if_pos hodd, hrec, ← Nat.pow_mod, Nat.mod_mul_mod, haa, ← pow_mul, ← pow_succ,
show 2 * (k / 2) + 1 = k by omega]
-- even k: (a²)^(k/2) = a^(2·(k/2)) = a^k
· rw [if_neg hodd, hrec, ← Nat.pow_mod, haa, ← pow_mul,
show 2 * (k / 2) = k by omega]
/-- `powMod a k n = a ^ k % n` for all `k < 2 ^ 256` — fuel fixed at 256,
enough for every exponent below 2²⁵⁶, in particular for `P / 2` (< 2²⁵⁴).
WHY NEEDED: the single entry point of all kernel computations below. -/
def powMod (a k n : ) : := powModAux 256 a k n
/- Bridge from the `Nat` computation into `ZMod n`.
MATH: k < 2^256 ==> (a : ZMod n)^k = (powMod a k n : ZMod n).
Casting `a` into Z/n and exponentiating there agrees with computing
`a^k mod n` over the naturals and casting the result (the cast is a ring
homomorphism that kills `% n`).
WHY NEEDED: this is how the kernel-checked equation
`powMod dNum (P/2) P = P 1` becomes the field equation
`edD^(P/2) = 1` in `edD_pow_eq_neg_one`. -/
theorem cast_pow_eq (a k n : ) (hk : k < 2 ^ 256) :
(a : ZMod n) ^ k = ((powMod a k n : ) : ZMod n) := by
rw [powMod, powModAux_eq 256 a k n hk, ZMod.natCast_mod, Nat.cast_pow]
/-! ## Casting `Nat` residues into 𝔽_p
Two tiny workhorses: a natural number is 0 in 𝔽_p iff p divides it. Every
kernel-checked congruence below enters the field through these. -/
/- MATH: n % P = 0 ==> (n : F_p) = 0 — multiples of p vanish in 𝔽_p.
WHY NEEDED: imports each kernel-checked `Nat` congruence (a closed `% P`
equation, checked by `decide`) into the field 𝔽_p. -/
theorem natCast_eq_zero_of_mod {n : } (h : n % P = 0) : (n : Fp) = 0 := by
rw [← ZMod.natCast_mod n P, h, Nat.cast_zero]
/- MATH: n % P ≠ 0 ==> (n : F_p) ≠ 0 — non-multiples of p survive in 𝔽_p.
Distinct naturals can collide in Z/p, so the cast-level inequality needs
the residues compared mod p (`ZMod.natCast_eq_natCast_iff'`).
WHY NEEDED: gives the nonvanishing of the small constants 2, 121665,
121666 (each `% P` check is a kernel `decide`: P is huge, they are tiny). -/
theorem natCast_ne_zero_of_mod {n : } (h : n % P ≠ 0) : (n : Fp) ≠ 0 := by
intro hc
apply h
have h0 : ((n : ) : Fp) = ((0 : ) : Fp) := by rw [Nat.cast_zero]; exact hc
have h1 := (ZMod.natCast_eq_natCast_iff' n 0 P).mp h0
rwa [Nat.zero_mod] at h1
/- MATH: (121666 : F_p) ≠ 0. True because 0 < 121666 < P, i.e. P ∤ 121666.
WHY NEEDED: 121666 is the denominator of d — without this, `edD` would be
division by zero and `edD_char`/`dNum_cast` would be vacuous.
(`private`: Proofs/EdDenote.lean exports an identical public lemma of the
same name; importers that need both files use that one. Privacy here
avoids a duplicate-declaration clash without changing any statement.) -/
private theorem c121666_ne_zero : (121666 : Fp) ≠ 0 := by
have h : ((121666 : ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
exact_mod_cast h
/- MATH: (121665 : F_p) ≠ 0 (numerator of d). WHY NEEDED: `edD_ne_zero`. -/
theorem c121665_ne_zero : (121665 : Fp) ≠ 0 := by
have h : ((121665 : ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
exact_mod_cast h
/- MATH: (2 : F_p) ≠ 0 — the field has characteristic ≠ 2 (p is odd).
WHY NEEDED: the completeness proof at one point divides the curve world
into i·x₂ = ±y₂ and needs "both" to force x₂ = 0 via 2·i·x₂ = 0. -/
theorem two_ne_zero_Fp : (2 : Fp) ≠ 0 := by
have h : ((2 : ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
exact_mod_cast h
/-! ## The curve constant d = 121665/121666 -/
/-- The Ed25519 twisted Edwards curve constant
MATH: d := 121665/121666 ∈ 𝔽_p (RFC 8032 §5.1; BBJLP "Twisted Edwards
curves" parameters a = 1, d).
Rust analog: `constants::EDWARDS_D` in curve25519/solana-ed25519/src/
backend/serial/u64/constants.rs — the limb vector denoting exactly this
field element.
WHY NEEDED: parametrizes the curve equation `OnCurve` and the addition
law `edAdd`; its NON-squareness (`edD_not_square`) is what makes the
addition law complete. -/
noncomputable def edD : Fp := -(121665 : Fp) / 121666
/- MATH: 121666 · d = 121665 — the denominator-free characterization.
This is the form a DECODER of the constant can check by pure limb
arithmetic (multiply by 121666, compare with 121665), with no inversion.
Proof: cancel the nonzero denominator 121666.
WHY NEEDED: the bridge between the abstract fraction and any concrete
representation of d — used right below to certify the canonical residue
`dNum`, and intended as the spec hook for the transpiled `EDWARDS_D`. -/
theorem edD_char : (121666 : Fp) * edD = -121665 := by
unfold edD
rw [mul_comm, div_mul_cancel₀ _ c121666_ne_zero]
/- MATH: d ≠ 0 — numerator 121665 and denominator 121666 are both nonzero.
WHY NEEDED: Euler's criterion (`ZMod.euler_criterion`) only speaks about
nonzero elements; also gives x,y ≠ 0 extraction in the completeness proof. -/
theorem edD_ne_zero : edD ≠ 0 := by
unfold edD
exact div_ne_zero (neg_ne_zero.mpr c121665_ne_zero) c121666_ne_zero
/-! ## d as a canonical residue, and d^((p1)/2) = 1
To exponentiate d with the kernel we need d as a NATURAL number. `dNum` is
the canonical representative (computed offline as
(p 121665)·121666⁻¹ mod p; the kernel re-certifies it below, so the
literal is trusted only as a hint). -/
/-- The unique n < P with (n : 𝔽_p) = d, as a decimal literal.
MATH: dNum := (p 121665) · (121666⁻¹ mod p) mod p.
WHY NEEDED: `powMod` computes on `Nat`, not on `ZMod P`; this literal is
the entry ticket for the kernel computation of d^((p1)/2). -/
def dNum : := 37095705934669439343138083508754565189542113879843219016388785533085940283555
/- MATH: (dNum : F_p) = d.
Proof: by `edD_char`-style cancellation it suffices that
121666·dNum + 121665 ≡ 0 (mod p) — a closed `Nat` congruence the kernel
`decide`s (one big multiplication and one division by P).
WHY NEEDED: transports the kernel-checked power of `dNum` to a statement
about `edD` itself. -/
theorem dNum_cast : (dNum : Fp) = edD := by
unfold edD
rw [eq_div_iff c121666_ne_zero]
-- the kernel certifies: p | dNum·121666 + 121665
have key : ((dNum * 121666 + 121665 : ) : Fp) = 0 := natCast_eq_zero_of_mod (by decide)
push_cast at key
linear_combination key
/- MATH: d^((p1)/2) = 1 in 𝔽_p (stated with `P / 2`, which equals
(p1)/2 since p is odd — this is the exact exponent in mathlib's
`ZMod.euler_criterion`).
Proof: the kernel computes powMod dNum (P/2) P = P 1 (≈255 squarings of
255-bit numbers — milliseconds via GMP), and (P 1 : 𝔽_p) = 1 because
(P1) + 1 = P ≡ 0.
WHY NEEDED: with Euler's criterion this IS the non-squareness of d. -/
theorem edD_pow_eq_neg_one : edD ^ (P / 2) = -1 := by
rw [← dNum_cast, cast_pow_eq dNum (P / 2) P (by decide),
show powMod dNum (P / 2) P = P - 1 from by decide]
-- (P 1 : 𝔽_p) = 1, i.e. ↑(P1) + 1 = 0, i.e. ↑P = 0
have hP1 : 1 ≤ P := by norm_num [P]
have h : ((P - 1 : ) : Fp) + ((1 : ) : Fp) = 0 := by
rw [← Nat.cast_add, Nat.sub_add_cancel hP1]
exact natCast_eq_zero_of_mod (by simp)
rw [Nat.cast_one] at h
linear_combination h
/- MATH: 1 ≠ 1 in 𝔽_p (characteristic ≠ 2: their difference is 2 ≠ 0).
WHY NEEDED: turns `edD^(P/2) = 1` into `edD^(P/2) ≠ 1` for Euler. -/
theorem neg_one_ne_one_Fp : (-1 : Fp) ≠ 1 := by
intro hc
exact two_ne_zero_Fp (by linear_combination -hc)
/-- d is a quadratic NON-residue modulo p.
MATH (ASCII): ¬ exists r in F_p, d = r·r.
LaTeX: $\left(\frac{d}{p}\right) = -1$.
Proof: Euler's criterion (`ZMod.euler_criterion`, d ≠ 0) reduces
squareness to d^(p/2) = 1; but d^(p/2) = 1 ≠ 1 by the kernel
computation above.
WHY NEEDED: THE hypothesis of the BernsteinLange completeness theorem.
A square d would admit exceptional point pairs where the addition law's
denominators vanish; non-square d (this theorem) rules them ALL out. -/
theorem edD_not_square : ¬ IsSquare edD := by
intro hsq
have h := (ZMod.euler_criterion P edD_ne_zero).mp hsq
rw [edD_pow_eq_neg_one] at h
exact neg_one_ne_one_Fp h
/-! ## √1 in 𝔽_p
p ≡ 1 (mod 4), so 1 is a square mod p. A concrete square root (the same
distinguished one the Rust constant `SQRT_M1` denotes, namely
2^((p1)/4) mod p) lets the a = 1 completeness proof run DIRECTLY on the
twisted curve: wherever the classical a = 1 proof squares (x₁ ± y₁), we
square (i·x₁ ± ε·y₁) instead. -/
/-- The canonical √1 of 𝔽_p as a decimal literal: 2^((p1)/4) mod p
(computed offline; the kernel re-certifies the defining equation below).
Rust analog: `constants::SQRT_M1`.
WHY NEEDED: makes 1 an EXPLICIT square, which is what lets the a = 1
twisted curve reuse the BernsteinLange square-exhibition argument. -/
def sNum : := 19681161376707505956807079304988542015446066515923890162744021073123829784752
/-- √1 as a field element. -/
noncomputable def sqrtM1 : Fp := (sNum : Fp)
/- MATH: sqrtM1² = 1. Proof: the kernel certifies p | sNum·sNum + 1 (one
255×255-bit multiplication), and a multiple of p vanishes in 𝔽_p.
WHY NEEDED: the only property of `sqrtM1` the completeness proof uses. -/
theorem sqrtM1_sq : sqrtM1 ^ 2 = -1 := by
have key : ((sNum * sNum + 1 : ) : Fp) = 0 := natCast_eq_zero_of_mod (by decide)
push_cast at key
unfold sqrtM1
linear_combination key
/- MATH: sqrtM1 ≠ 0 (its square is 1 ≠ 0).
WHY NEEDED: cancellation in the `i·x₂ = ±y₂ ⇒ x₂ = 0` step. -/
theorem sqrtM1_ne_zero : sqrtM1 ≠ 0 := by
intro h0
have h := sqrtM1_sq
rw [h0] at h
exact one_ne_zero (by linear_combination h)
/-! ## The curve, its addition law, negation, neutral element -/
/-- The twisted Edwards curve equation with a = 1 (Ed25519, RFC 8032 §5.1):
MATH (ASCII): OnCurve x y :<=> -x^2 + y^2 = 1 + d·x^2·y^2.
LaTeX: $-x^2 + y^2 = 1 + d x^2 y^2$.
Rust analog: the (implicit) invariant of `EdwardsPoint` in
curve25519/solana-ed25519/src/edwards.rs — affine coordinates here,
extended coordinates there. -/
def OnCurve (x y : Fp) : Prop := -(x^2) + y^2 = 1 + edD * x^2 * y^2
/-- The COMPLETE twisted Edwards addition law (BBJLP "Twisted Edwards
curves", §6, a = 1):
MATH: (x₁,y₁) + (x₂,y₂) =
( (x₁y₂ + x₂y₁) / (1 + d·x₁x₂y₁y₂), (y₁y₂ + x₁x₂) / (1 d·x₁x₂y₁y₂) ).
By `completeness` the denominators never vanish on curve points, so the
division is honest field division everywhere we ever apply it. (On the
pair type `Fp × Fp` at large, mathlib's junk-value convention x/0 = 0
applies — all theorems below restrict to curve points.)
Rust analog: `EdwardsPoint: Add` (extended-coordinate version) in
src/edwards.rs — the projective P³ formulas compute exactly these two
fractions. -/
noncomputable def edAdd (p q : Fp × Fp) : Fp × Fp :=
( (p.1*q.2 + q.1*p.2) / (1 + edD*p.1*q.1*p.2*q.2),
(p.2*q.2 + p.1*q.1) / (1 - edD*p.1*q.1*p.2*q.2) )
/-- Point negation: (x, y) = (x, y) (Edwards curves negate the
x-coordinate). Rust analog: `EdwardsPoint: Neg` in src/edwards.rs. -/
def edNeg (p : Fp × Fp) : Fp × Fp := (-p.1, p.2)
/-- The neutral element (0, 1).
Rust analog: `EdwardsPoint::identity()` (X=0, Y=Z=1, T=0). -/
def edId : Fp × Fp := (0, 1)
/-! ## Completeness of the addition law (BernsteinLange)
The mathematical heart of the file. Shape of the argument (BBJLP Thm 3.3 /
BernsteinLange "Faster addition and doubling", adapted to a = 1):
Suppose some denominator vanished, i.e. ε := d·x₁x₂y₁y₂ ∈ {1, +1}. Then
x₁, x₂, y₁, y₂ are all nonzero (their product is ±1/d ≠ 0), and with
i := √1 the two curve equations combine into the EXPLICIT square identities
(i·x₁ + ε·y₁)² = d · x₁²y₁² · (i·x₂ + y₂)²
(i·x₁ ε·y₁)² = d · x₁²y₁² · (i·x₂ y₂)²
(kernel-of-the-proof: ε² = 1 turns d²·(x₁x₂y₁y₂)² into 1, which is what
collapses everything). At least one of i·x₂ ± y₂ is nonzero — otherwise
2·i·x₂ = 0 forces x₂ = 0 — so dividing the corresponding identity by the
nonzero square (x₁y₁·(i·x₂ ± y₂))² exhibits d as a SQUARE in 𝔽_p,
contradicting `edD_not_square`. ∎ -/
/- The shared core: NO curve points make d·x₁x₂y₁y₂ a square root of 1.
MATH (ASCII): OnCurve x1 y1 ∧ OnCurve x2 y2 ∧ ε² = 1 ∧
d·x1·x2·y1·y2 = ε ==> False.
Instantiated with ε = 1 (resp. ε = +1) this kills the "+" (resp. "")
denominator of `edAdd`. The two `linear_combination` certificates are the
polynomial cofactors of the square identities above w.r.t. the ideal
generated by the two curve equations, heq, i² = 1 and ε² = 1 (computed
and verified offline; `ring` re-verifies them here).
WHY NEEDED: the engine behind both halves of `completeness`. -/
theorem denominator_core {x1 y1 x2 y2 : Fp} (h1 : OnCurve x1 y1) (h2 : OnCurve x2 y2)
(ε : Fp) (hε : ε ^ 2 = 1) (heq : edD * x1 * x2 * y1 * y2 = ε) : False := by
-- ε is a unit, hence so is the product d·x₁x₂y₁y₂: all factors are nonzero
have hε0 : ε ≠ 0 := by
intro h0
rw [h0] at hε
exact one_ne_zero (by linear_combination -hε)
have hne : edD * x1 * x2 * y1 * y2 ≠ 0 := by rw [heq]; exact hε0
have hy2 : y2 ≠ 0 := right_ne_zero_of_mul hne
have hy1 : y1 ≠ 0 := right_ne_zero_of_mul (left_ne_zero_of_mul hne)
have hx2 : x2 ≠ 0 := right_ne_zero_of_mul (left_ne_zero_of_mul (left_ne_zero_of_mul hne))
have hx1 : x1 ≠ 0 :=
right_ne_zero_of_mul (left_ne_zero_of_mul (left_ne_zero_of_mul (left_ne_zero_of_mul hne)))
have hi := sqrtM1_sq
unfold OnCurve at h1 h2
-- the two BernsteinLange square identities (cofactors verified offline)
have key₁ : (sqrtM1*x1 + ε*y1)^2 = edD * x1^2*y1^2 * (sqrtM1*x2 + y2)^2 := by
linear_combination h1 - edD*x1^2*y1^2 * h2
- (edD*x1*x2*y1*y2 + ε + 2*sqrtM1*x1*y1) * heq
+ (x1^2 - edD*x1^2*y1^2*x2^2) * hi + (y1^2 - 1) * hε
have key₂ : (sqrtM1*x1 - ε*y1)^2 = edD * x1^2*y1^2 * (sqrtM1*x2 - y2)^2 := by
linear_combination h1 - edD*x1^2*y1^2 * h2
- (edD*x1*x2*y1*y2 + ε - 2*sqrtM1*x1*y1) * heq
+ (x1^2 - edD*x1^2*y1^2*x2^2) * hi + (y1^2 - 1) * hε
-- at least one of i·x₂ ± y₂ is a unit; divide the matching identity by it
by_cases hc : sqrtM1*x2 + y2 = 0
· -- i·x₂ + y₂ = 0, so i·x₂ y₂ ≠ 0 (else 2·i·x₂ = 0 forces x₂ = 0)
have hc2 : sqrtM1*x2 - y2 ≠ 0 := by
intro hc2
apply hx2
have h2x : (2 * sqrtM1) * x2 = 0 := by linear_combination hc + hc2
rcases mul_eq_zero.mp h2x with h | h
· rcases mul_eq_zero.mp h with h' | h'
· exact absurd h' two_ne_zero_Fp
· exact absurd h' sqrtM1_ne_zero
· exact h
-- d = ((i·x₁ ε·y₁)/(x₁y₁(i·x₂ y₂)))² — a square, contradiction
apply edD_not_square
refine ⟨(sqrtM1*x1 - ε*y1) / (x1*y1*(sqrtM1*x2 - y2)), ?_⟩
have hden : x1*y1*(sqrtM1*x2 - y2) ≠ 0 := mul_ne_zero (mul_ne_zero hx1 hy1) hc2
rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hden hden)]
linear_combination -key₂
· -- i·x₂ + y₂ ≠ 0: same square exhibition with the "+" identity
apply edD_not_square
refine ⟨(sqrtM1*x1 + ε*y1) / (x1*y1*(sqrtM1*x2 + y2)), ?_⟩
have hden : x1*y1*(sqrtM1*x2 + y2) ≠ 0 := mul_ne_zero (mul_ne_zero hx1 hy1) hc
rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hden hden)]
linear_combination -key₁
/-- THE COMPLETENESS THEOREM (BernsteinLange, a = 1 twisted case).
MATH (ASCII): for all curve points (x1,y1), (x2,y2):
1 + d·x1·x2·y1·y2 ≠ 0 and 1 d·x1·x2·y1·y2 ≠ 0.
LaTeX: $1 \pm d\,x_1x_2y_1y_2 \neq 0$ on $E \times E$.
Both denominators of `edAdd` are units at EVERY pair of curve points —
the addition law is complete: one formula, no exceptions, defined even
for doubling (p = q). This is precisely why the Rust implementation can
be branch-free (constant-time) without an exceptional-case audit.
Proof: if a denominator vanished, d·x₁x₂y₁y₂ would be ∓1, which
`denominator_core` (using ¬IsSquare d) refutes. -/
theorem completeness {x1 y1 x2 y2 : Fp} (h1 : OnCurve x1 y1) (h2 : OnCurve x2 y2) :
1 + edD * x1 * x2 * y1 * y2 ≠ 0 ∧ 1 - edD * x1 * x2 * y1 * y2 ≠ 0 := by
constructor
· intro hbad
exact denominator_core h1 h2 (-1) (by norm_num) (by linear_combination hbad)
· intro hbad
exact denominator_core h1 h2 1 (by norm_num) (by linear_combination -hbad)
/-! ## The mechanical laws -/
/- MATH: (0, 1) lies on the curve: 0² + 1² = 1 = 1 + d·0²·1².
WHY NEEDED: the neutral element must be a point for `edAdd_id`/`edAdd_neg`
to be statements about curve points. -/
theorem onCurve_id : OnCurve 0 1 := by
unfold OnCurve
norm_num
/- MATH: (x, y) on the curve ⇒ (x, y) on the curve ((x)² = x²).
WHY NEEDED: `edNeg` maps points to points; feeds `edAdd_neg`. -/
theorem onCurve_neg {x y : Fp} (h : OnCurve x y) : OnCurve (-x) y := by
unfold OnCurve at h ⊢
linear_combination h
/- MATH: (x,y) + (0,1) = (x,y) — right identity. At q = (0,1) the
denominators are LITERALLY 1 (no completeness needed): the components
reduce to (x·1 + 0·y)/1 and (y·1 + x·0)/1. -/
theorem edAdd_id {x y : Fp} (_h : OnCurve x y) : edAdd (x, y) edId = (x, y) := by
unfold edAdd edId
simp
/- MATH: p + q = q + p — the formula is literally symmetric in p, q (both
numerators and both denominators are, up to commuting products/sums).
WHY NEEDED: with `edAdd_id` it gives the LEFT identity for free, and it
is half of the abelian-group structure (Tier 2). -/
theorem edAdd_comm (p q : Fp × Fp) : edAdd p q = edAdd q p := by
unfold edAdd
rw [Prod.mk.injEq]
constructor
· rw [show q.1*p.2 + p.1*q.2 = p.1*q.2 + q.1*p.2 from by ring,
show edD*q.1*p.1*q.2*p.2 = edD*p.1*q.1*p.2*q.2 from by ring]
· rw [show q.2*p.2 + q.1*p.1 = p.2*q.2 + p.1*q.1 from by ring,
show edD*q.1*p.1*q.2*p.2 = edD*p.1*q.1*p.2*q.2 from by ring]
/- MATH: (x,y) + (x,y) = (0,1) — every point has an inverse.
The x-component's numerator is x·y + (x)·y = 0 (no completeness needed:
0/z = 0 for ANY z). The y-component is (y² x²)/(1 + d·x²y²); the curve
equation says numerator = denominator, and completeness (at the point and
its negation, where the "" denominator of `edAdd` is 1 + d·x²y²)
guarantees the denominator is a unit, so the quotient is 1.
WHY NEEDED: inverses — another quarter of the group structure. -/
theorem edAdd_neg {x y : Fp} (h : OnCurve x y) : edAdd (x, y) (edNeg (x, y)) = edId := by
-- the "" denominator at ((x,y), (x,y)) is 1 d·x·(x)·y·y = 1 + d·x²y² ≠ 0
have hm := (completeness h (onCurve_neg h)).2
unfold OnCurve at h
show ( (x*y + -x*y) / (1 + edD * x * -x * y * y),
(y*y + x * -x) / (1 - edD * x * -x * y * y) ) = (0, 1)
rw [Prod.mk.injEq]
constructor
· rw [show x*y + -x*y = (0 : Fp) from by ring, zero_div]
· rw [div_eq_iff hm, one_mul]
linear_combination h
/- MATH: the sum of two curve points is a curve point — `edAdd` is CLOSED on
the curve. With x₃ = T/(1+D), y₃ = N/(1D) (T = x₁y₂+x₂y₁, N = y₁y₂+x₁x₂,
D = d·x₁x₂y₁y₂), multiplying the target curve equation by the unit
(1+D)²(1D)² turns it into the polynomial identity
T²(1D)² + N²(1+D)² = (1+D)²(1D)² + d·T²·N²,
which is an explicit combination of the two input curve equations: the
two big cofactor polynomials in the `linear_combination` below were
computed offline by a Gröbner-basis reduction of the identity modulo the
curve ideal, and are re-verified from scratch by `ring` here (the `hT`/
`hN` summands merely re-relate u = x₃, v = y₃ to their numerators).
WHY NEEDED: well-definedness of the group operation — the final quarter
of the Tier-1 group-law package (associativity is Tier 2). -/
theorem edAdd_closure {x1 y1 x2 y2 : Fp} (h1 : OnCurve x1 y1) (h2 : OnCurve x2 y2) :
OnCurve (edAdd (x1, y1) (x2, y2)).1 (edAdd (x1, y1) (x2, y2)).2 := by
obtain ⟨hp, hm⟩ := completeness h1 h2
unfold OnCurve at h1 h2
show -(((x1*y2 + x2*y1) / (1 + edD*x1*x2*y1*y2))^2)
+ ((y1*y2 + x1*x2) / (1 - edD*x1*x2*y1*y2))^2
= 1 + edD * ((x1*y2 + x2*y1) / (1 + edD*x1*x2*y1*y2))^2
* ((y1*y2 + x1*x2) / (1 - edD*x1*x2*y1*y2))^2
-- name the two components and recover their defining equations
have hT : (x1*y2 + x2*y1) / (1 + edD*x1*x2*y1*y2) * (1 + edD*x1*x2*y1*y2)
= x1*y2 + x2*y1 := div_mul_cancel₀ _ hp
have hN : (y1*y2 + x1*x2) / (1 - edD*x1*x2*y1*y2) * (1 - edD*x1*x2*y1*y2)
= y1*y2 + x1*x2 := div_mul_cancel₀ _ hm
set u := (x1*y2 + x2*y1) / (1 + edD*x1*x2*y1*y2) with hu
set v := (y1*y2 + x1*x2) / (1 - edD*x1*x2*y1*y2) with hv
-- clear the (unit) denominators: multiply both sides by (1+D)²(1D)²
apply mul_right_cancel₀ (mul_ne_zero (pow_ne_zero 2 hp) (pow_ne_zero 2 hm))
-- …and certify the resulting polynomial identity from the curve equations
linear_combination
(edD^3*x1^2*y1^2*x2^4*y2^4 - edD^2*x1^2*x2^4*y2^4 + edD^2*y1^2*x2^4*y2^4
- edD^2*x2^4*y2^4 - edD*x1^2*x2^4*y2^2 + edD*y1^2*x2^4*y2^2
+ edD*x1^2*x2^2*y2^4 - edD*y1^2*x2^2*y2^4 - 2*edD*x2^4*y2^4
- 2*x2^4*y2^2 + 2*x2^2*y2^4 - 2*edD*x2^2*y2^2 + x2^4 - 4*x2^2*y2^2
+ y2^4) * h1
+ (edD*x1^4*x2^2*y2^2 + edD*y1^4*x2^2*y2^2 + 2*edD*x1^2*x2^2*y2^2
- 2*edD*y1^2*x2^2*y2^2 + 2*x1^2*x2^2*y2^2 - 2*y1^2*x2^2*y2^2
+ edD*x2^2*y2^2 - x1^2*x2^2 + y1^2*x2^2 + x1^2*y2^2 - y1^2*y2^2
+ 2*x2^2*y2^2 - x2^2 + y2^2 + 1) * h2
+ (-(1 - edD*x1*x2*y1*y2)^2 * (u*(1 + edD*x1*x2*y1*y2) + (x1*y2 + x2*y1))
- edD*(y1*y2 + x1*x2)
* (u*v*(1 + edD*x1*x2*y1*y2)*(1 - edD*x1*x2*y1*y2)
+ (x1*y2 + x2*y1)*(y1*y2 + x1*x2))) * hT
+ ((1 + edD*x1*x2*y1*y2)^2 * (v*(1 - edD*x1*x2*y1*y2) + (y1*y2 + x1*x2))
- edD*u*(1 + edD*x1*x2*y1*y2)
* (u*v*(1 + edD*x1*x2*y1*y2)*(1 - edD*x1*x2*y1*y2)
+ (x1*y2 + x2*y1)*(y1*y2 + x1*x2))) * hN
end CurveFieldProofs

View file

@ -0,0 +1,655 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdDenote.lean — POINT DENOTATION layer: from transpiled limb
structures to coordinates in 𝔽_p, p = 2²⁵⁵ 19.
CONTEXT. The Rust crate curve25519/solana-ed25519 represents points of
the twisted Edwards curve x² + y² = 1 + d·x²y² (d = 121665/121666)
in four internal models (src/backend/serial/curve_models.rs module docs,
following HisilWongCarterDawson 2008 and the ℙ¹×ℙ¹ picture of
CostelloSmith 2017):
* `EdwardsPoint` (X:Y:Z:T) — "extended" ℙ³ coordinates with
x = X/Z, y = Y/Z and the Segre coherence
X·Y = Z·T (equivalently T = XY/Z);
* `ProjectivePoint` (X:Y:Z) — ℙ² coordinates, x = X/Z, y = Y/Z;
* `CompletedPoint` ((X:Z),(Y:T)) ∈ ℙ¹×ℙ¹ — x = X/Z, y = Y/T
(NOTE: here T is the SECOND DENOMINATOR, a
completely different role from the extended T);
* `ProjectiveNielsPoint` (Y+X, YX, Z, T·2d) — a CACHE of readily-added
combinations of an extended point;
* `AffineNielsPoint` (y+x, yx, 2d·x·y) — the same cache for an
affine point (Z = 1).
All coordinates are `FieldElement51` (= `Fe`) limb vectors; Charon+Aeneas
transpiled the structures to gen/CurveField/Types.lean and the code to
gen/CurveField/Funs.lean. Proofs/FieldMain.lean already established that
the FIELD layer is correct: the denotation ⟪·⟫ : Fe → 𝔽_p, the limb-bound
invariant `Bnd`, and one `run_*` theorem per field operation.
THIS FILE builds the corresponding layer for POINTS, in four parts:
1. VALIDITY PREDICATES + DENOTATIONS for each representation
(`ExtValid`/`edX`/`edY`, `ProjValid`/`projX`/`projY`,
`ComplValid`/`complX`/`complY`, `ProjNielsValid`/`IsNielsOf`,
`AffNielsValid`/`IsAffNielsOf`).
⚠ The Z ≠ 0 (resp. Z ≠ 0 ∧ T ≠ 0) side conditions are carried
EXPLICITLY: the Rust code NEVER checks them (projective division by
zero cannot panic — it is simply never performed; the code only
manipulates numerators/denominators), so they must live in the
specification layer. Every honest production of a point (identity,
decompression, the add/double formulas on valid inputs) maintains
them, and the op-spec phase will thread them through.
2. CONSTANT SPECS for the precomputed curve constants `EDWARDS_D` and
`EDWARDS_D2` (gen/CurveField/Funs.lean). To keep this file
independent of the (not-yet-existing) math layer Proofs/EdCurve.lean
— which will define the canonical `edD : Fp := -(121665:Fp)/121666` —
the d-constant is specified in CHARACTERIZATION FORM:
121666 · ⟪D⟫ = 121665 (d = 121665/121666)
121666 · ⟪D2⟫ = 243330 (2d = 243330/121666),
which pins the same field element without naming any quotient.
`edwards_d2_eq_two_d` then proves ⟪D2⟫ = 2·⟪D⟫ outright.
3. IDENTITY-CONSTANT SPECS: the generated `Identity` trait
implementations for `ProjectivePoint` (0:1:1), `AffineNielsPoint`
(1,1,0), `ProjectiveNielsPoint` (1,1,1,0) and `EdwardsPoint`
(0:1:1:0) all RUN (no panic), are valid, and denote the neutral
affine point (0, 1).
4. SMALL FIELD HELPERS the op-spec phase needs: 2 ≠ 0 and 121666 ≠ 0
in 𝔽_p, division-equation rewrites (`fp_div_eq_iff` etc.), the
determinism extractor `ok_ext`, and the constructor-projection
(`mk_*`) conveniences for the point structures.
PROOF TECHNIQUE for the constants: identical to `sqrt_m1_spec`
(Proofs/ConstSpecs.lean). Each constant is `from_limbs` of 5 literal
limbs; `simp` evaluates the denotation to a concrete ~255-bit natural
number N, and the characterization becomes the -congruence
(121666·N) mod p = p 121665, which `norm_num` checks by kernel-verified
literal arithmetic. (Sanity-checked externally:
N_d = 37095705934669439343138083508754565189542113879843219016388785533085940283555,
N_d2 = 16295367250680780974490674513165176452449235426866156013048779062215315747161,
121666·N_d ≡ 121665 and 121666·N_d2 ≡ 243330 (mod p), N_d2 ≡ 2·N_d.)
Nothing in gen/ (the transpiled code) is modified; we only define
predicates ABOUT it and run it.
Imports: Proofs/FieldMain.lean (denotation, Bnd, run_* runners, Field 𝔽_p).
Imported by: the forthcoming point-operation spec files.
─────────────────────────────────────────────────────────────────────── -/
import Proofs.FieldMain
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 4000000
namespace CurveFieldProofs
/-! ## Short aliases for the transpiled point types
Definitionally the generated structures (`rfl`-equal), mirroring the
`Fe`/`fe_*` aliases of Proofs/Denote.lean. The Rust source lines cited
are from the generated docstrings in gen/CurveField/Types.lean. -/
/-- Rust: `pub struct EdwardsPoint { X, Y, Z, T: FieldElement51 }`,
src/edwards.rs:390-395 — extended (ℙ³ / "extended twisted Edwards")
coordinates. -/
abbrev EdPoint := edwards.EdwardsPoint
/-- Rust: `pub(crate) struct ProjectivePoint { X, Y, Z }`,
src/backend/serial/curve_models.rs:154-158 — ℙ² coordinates. -/
abbrev ProjPoint := backend.serial.curve_models.ProjectivePoint
/-- Rust: `pub(crate) struct CompletedPoint { X, Y, Z, T }`,
src/backend/serial/curve_models.rs:169-174 — ℙ¹×ℙ¹ coordinates
((X:Z),(Y:T)); the output type of the add/double kernels. -/
abbrev ComplPoint := backend.serial.curve_models.CompletedPoint
/-- Rust: `pub struct ProjectiveNielsPoint { Y_plus_X, Y_minus_X, Z, T2d }`,
src/backend/serial/curve_models.rs:206-211 — readily-addable cache of an
`EdwardsPoint`. -/
abbrev ProjNiels := backend.serial.curve_models.ProjectiveNielsPoint
/-- Rust: `pub(crate) struct AffineNielsPoint { y_plus_x, y_minus_x, xy2d }`,
src/backend/serial/curve_models.rs:184-188 — readily-addable cache of an
affine point (Z = 1). -/
abbrev AffNiels := backend.serial.curve_models.AffineNielsPoint
/-! ## Small 𝔽_p facts the point layer relies on
The point denotations divide by Z (and T), and the d-constant
characterization divides (conceptually) by 121666 and 2; these lemmas
make those denominators usable. -/
/-- No Rust analog — arithmetic helper generalizing `natCast_P_sub_one`
(Proofs/ConstSpecs.lean) from k = 1 to arbitrary k ≤ p.
MATH: ((p k : ) : 𝔽_p) = (k : 𝔽_p) (since p ≡ 0 in 𝔽_p).
WHY NEEDED: the constant specs below compute (121666·N) mod p to the
literal p 121665 (resp. p 243330); this lemma converts that natural
number into the field element 121665 (resp. 243330). -/
theorem natCast_P_sub (k : ) (hk : k ≤ P) : ((P - k : ) : Fp) = -(k : Fp) := by
-- k ≤ p lets Nat.cast_sub distribute the truncated subtraction
rw [Nat.cast_sub hk, ZMod.natCast_self]
ring
/-- No Rust analog — arithmetic helper.
MATH: 0 < k < p ==> (k : 𝔽_p) ≠ 0.
A positive natural number below the modulus does not vanish mod p:
(k : 𝔽_p) = 0 would mean p k, forcing p ≤ k.
WHY NEEDED: the two specific instances below (k = 2 and k = 121666);
stated generally so the op-spec phase can produce further nonzero
numerals (e.g. 121665, 486664) without repeating the argument. -/
theorem natCast_ne_zero_of_lt_P {k : } (h0 : 0 < k) (hk : k < P) :
((k : ) : Fp) ≠ 0 := by
intro h
-- (k : ZMod p) = 0 ↔ p k, and a divisor of a positive number is ≤ it
have hdvd : P k := (ZMod.natCast_eq_zero_iff k P).mp h
have := Nat.le_of_dvd h0 hdvd
omega
/-- MATH: (2 : 𝔽_p) ≠ 0 — p = 2²⁵⁵ 19 is an ODD prime, so the field has
characteristic ≠ 2.
WHY NEEDED: the projective-niels denominator is 2·Z (the cache stores
Y+X and YX, whose sum/difference is 2Y/2X), so recovering coordinates
divides by 2; also doubling formulas. Primed to avoid clashing with
mathlib's `two_ne_zero`. -/
theorem two_ne_zero' : (2 : Fp) ≠ 0 := by
have h := natCast_ne_zero_of_lt_P (k := 2) (by norm_num) (by norm_num [P])
exact_mod_cast h
/-- MATH: (121666 : 𝔽_p) ≠ 0 (121666 = 1 a·d⁻¹-free spelling: it is just
a small positive integer < p).
WHY NEEDED: the curve constant d is characterized below as the solution
of 121666·d = 121665; this lemma makes that characterization UNIQUE
(121666 is invertible), which `edwards_d2_eq_two_d` and the future
EdCurve.lean bridge (d = 121665/121666) exploit. -/
theorem c121666_ne_zero : (121666 : Fp) ≠ 0 := by
have h := natCast_ne_zero_of_lt_P (k := 121666) (by norm_num) (by norm_num [P])
exact_mod_cast h
/-! ## 1. Validity predicates and denotations
Each representation gets
* a VALIDITY predicate: the limb bounds under which the transpiled
field ops run panic-free (the dalek 2⁵²/2⁵⁴ discipline of
Proofs/FieldMain.lean), PLUS the nonzero-denominator conditions; and
* a DENOTATION: the affine coordinates (x, y) ∈ 𝔽_p × 𝔽_p it
represents.
⚠ Z ≠ 0 IS NOT CHECKED BY THE RUST CODE. The implementation never
divides — it works with fractions symbolically — so nothing at runtime
enforces a nonzero denominator, and a "point" with Z = 0 would
silently denote garbage (0/0). The predicate layer here is where that
obligation lives; every constructor of points we specify (identity
below, decompression and the arithmetic kernels in the op-spec phase)
PROVES it, and every consumer ASSUMES it. -/
/-- Validity of an extended ("ℙ³") point P = (X : Y : Z : T).
MATH: all four coordinates obey the reduced limb bound 2⁵²
(so any field op may consume them), Z ≢ 0 (mod p), and the
Segre/extended coherence X·Y ≡ Z·T (mod p)
(i.e. T carries the product x·y: T/Z = (X/Z)·(Y/Z)).
Rust: the *intended* invariant of `EdwardsPoint` per
curve_models.rs module docs ("the curve is given by the pair of
equations W₁² + W₂² = W₃² + dW₀², W₀W₃ = W₁W₂"); the curve equation
itself is deliberately NOT part of this predicate — it belongs to the
math layer (Proofs/EdCurve.lean) on the denoted pair (edX, edY).
WHY NEEDED: precondition and postcondition of every extended-point
operation in the op-spec phase. -/
def ExtValid (Pt : EdPoint) : Prop :=
Bnd Pt.X (2^52) ∧ Bnd Pt.Y (2^52) ∧ Bnd Pt.Z (2^52) ∧ Bnd Pt.T (2^52) ∧
⟪Pt.Z⟫ ≠ 0 ∧ ⟪Pt.X⟫ * ⟪Pt.Y⟫ = ⟪Pt.Z⟫ * ⟪Pt.T⟫
/-- Affine x-coordinate denoted by an extended point: x = ⟪X⟫ / ⟪Z⟫.
(Meaningful under `ExtValid` — division by ⟪Z⟫ ≠ 0; on Z ≡ 0 it would
be mathlib's junk value 0.) `noncomputable` because 𝔽_p division goes
through the classical field instance — irrelevant, never executed. -/
noncomputable def edX (Pt : EdPoint) : Fp := ⟪Pt.X⟫ / ⟪Pt.Z⟫
/-- Affine y-coordinate denoted by an extended point: y = ⟪Y⟫ / ⟪Z⟫. -/
noncomputable def edY (Pt : EdPoint) : Fp := ⟪Pt.Y⟫ / ⟪Pt.Z⟫
/-- Validity of a projective ("ℙ²") point P = (X : Y : Z).
MATH: limb bounds 2⁵² on X, Y, Z and Z ≢ 0 (mod p).
No coherence equation — ℙ² has no redundant coordinate. -/
def ProjValid (Pt : ProjPoint) : Prop :=
Bnd Pt.X (2^52) ∧ Bnd Pt.Y (2^52) ∧ Bnd Pt.Z (2^52) ∧ ⟪Pt.Z⟫ ≠ 0
/-- Affine x-coordinate denoted by a projective point: x = ⟪X⟫ / ⟪Z⟫. -/
noncomputable def projX (Pt : ProjPoint) : Fp := ⟪Pt.X⟫ / ⟪Pt.Z⟫
/-- Affine y-coordinate denoted by a projective point: y = ⟪Y⟫ / ⟪Z⟫. -/
noncomputable def projY (Pt : ProjPoint) : Fp := ⟪Pt.Y⟫ / ⟪Pt.Z⟫
/-- Validity of a completed ("ℙ¹×ℙ¹") point P = ((X : Z), (Y : T)).
MATH: limb bounds 2⁵² on all four coordinates, Z ≢ 0 AND T ≢ 0.
⚠ TWO denominators: the completed model is a product of two projective
lines, x = X/Z on the first and y = Y/T on the second — the field T here
plays the role of a DENOMINATOR for y, entirely unlike the extended
model's T (which is a cached numerator product). Both must be nonzero
for the point to denote affine coordinates. -/
def ComplValid (Pt : ComplPoint) : Prop :=
Bnd Pt.X (2^52) ∧ Bnd Pt.Y (2^52) ∧ Bnd Pt.Z (2^52) ∧ Bnd Pt.T (2^52) ∧
⟪Pt.Z⟫ ≠ 0 ∧ ⟪Pt.T⟫ ≠ 0
/-- Affine x-coordinate denoted by a completed point: x = ⟪X⟫ / ⟪Z⟫. -/
noncomputable def complX (Pt : ComplPoint) : Fp := ⟪Pt.X⟫ / ⟪Pt.Z⟫
/-- Affine y-coordinate denoted by a completed point: y = ⟪Y⟫ / ⟪T⟫
(T, not Z — see `ComplValid`). -/
noncomputable def complY (Pt : ComplPoint) : Fp := ⟪Pt.Y⟫ / ⟪Pt.T⟫
/-- Limb-bound + denominator validity of a projective-niels cache point.
MATH: Bnd(Y_plus_X, 2⁵³), Bnd(Y_minus_X, 2⁵³), Bnd(Z, 2⁵²),
Bnd(T2d, 2⁵²), and ⟪Z⟫ ≠ 0.
The 2⁵³ bound on the two sum/difference fields is the natural one:
`to_projective_niels` computes Y_plus_X with the UNREDUCED `fe_add`
(output bound 2⁵³ — `run_add`, FieldMain.lean) from two reduced (2⁵²)
coordinates, while Y_minus_X, Z, T2d come from `fe_sub`/`fe_mul`
(output bound 2⁵²; stated as ≤ 2⁵³ resp. 2⁵² accordingly). All four
are < 2⁵⁴, so every field op may consume them directly. -/
def ProjNielsValid (N : ProjNiels) : Prop :=
Bnd N.Y_plus_X (2^53) ∧ Bnd N.Y_minus_X (2^53) ∧ Bnd N.Z (2^52) ∧
Bnd N.T2d (2^52) ∧ ⟪N.Z⟫ ≠ 0
/-- RELATIONAL denotation of a projective-niels point: `IsNielsOf N Pt`
says the cache N was correctly derived from the extended point Pt.
MATH: ⟪Y_plus_X⟫ = ⟪Pt.Y⟫ + ⟪Pt.X⟫,
⟪Y_minus_X⟫ = ⟪Pt.Y⟫ ⟪Pt.X⟫,
⟪Z⟫ = ⟪Pt.Z⟫,
121666 · ⟪T2d⟫ = 243330 · ⟪Pt.T⟫ (i.e. ⟪T2d⟫ = ⟪Pt.T⟫ · 2d,
with 2d = 243330/121666 expressed denominator-free — the same
characterization trick as `edwards_d_spec` below, so no `edD`
definition is needed in this file).
DESIGN. We deliberately specify the niels cache RELATIONALLY rather
than giving it standalone coordinates (which would be
x = (⟪Y_plus_X⟫ ⟪Y_minus_X⟫)/(2⟪Z⟫), y = (⟪Y_plus_X⟫ + ⟪Y_minus_X⟫)/(2⟪Z⟫)
plus a cache-coherence equation for T2d): every niels point the code
ever creates comes from `to_projective_niels` on a concrete extended
point, and every consumer (`add`/`sub` of EdwardsPoint + ProjNiels)
immediately recombines the fields, so the derivation facts are exactly
the shape the op-spec proofs use. The standalone coordinates are
recoverable from this relation by field algebra (divide by 2⟪Z⟫ ≠ 0,
using `two_ne_zero'` and `fp_div_eq_iff`). -/
def IsNielsOf (N : ProjNiels) (Pt : EdPoint) : Prop :=
⟪N.Y_plus_X⟫ = ⟪Pt.Y⟫ + ⟪Pt.X⟫ ∧
⟪N.Y_minus_X⟫ = ⟪Pt.Y⟫ - ⟪Pt.X⟫ ∧
⟪N.Z⟫ = ⟪Pt.Z⟫ ∧
(121666 : Fp) * ⟪N.T2d⟫ = -243330 * ⟪Pt.T⟫
/-- Limb-bound validity of an affine-niels cache point.
MATH: Bnd(y_plus_x, 2⁵³), Bnd(y_minus_x, 2⁵³), Bnd(xy2d, 2⁵²).
No denominator condition — the affine cache has implicit Z = 1.
(2⁵³ on the sum/difference fields for the same `fe_add` reason as in
`ProjNielsValid`; the precomputed basepoint tables actually store
reduced values, which satisfy this a fortiori.) -/
def AffNielsValid (N : AffNiels) : Prop :=
Bnd N.y_plus_x (2^53) ∧ Bnd N.y_minus_x (2^53) ∧ Bnd N.xy2d (2^52)
/-- RELATIONAL denotation of an affine-niels point: `IsAffNielsOf N x y`
says N caches the affine point (x, y) (implicit Z = 1).
MATH: ⟪y_plus_x⟫ = y + x, ⟪y_minus_x⟫ = y x,
121666 · ⟪xy2d⟫ = 243330 · (x · y) (i.e. ⟪xy2d⟫ = 2d·x·y,
denominator-free as in `IsNielsOf`). -/
def IsAffNielsOf (N : AffNiels) (x y : Fp) : Prop :=
⟪N.y_plus_x⟫ = y + x ∧
⟪N.y_minus_x⟫ = y - x ∧
(121666 : Fp) * ⟪N.xy2d⟫ = -243330 * (x * y)
/-! ## 2. The curve constants EDWARDS_D and EDWARDS_D2
Rust: `constants::EDWARDS_D` ("Edwards d value, equal to
121665/121666 mod p") and `constants::EDWARDS_D2` (= 2·d),
curve25519/solana-ed25519/src/backend/serial/u64/constants.rs:45-60;
transpiled at gen/CurveField/Funs.lean:1121 and :1977 as `from_limbs`
of 5 literal limbs each.
The specs use the denominator-free CHARACTERIZATION
121666 · d = 121665,
which determines d uniquely in 𝔽_p (121666 is invertible —
`c121666_ne_zero`), so this file needs no division and no dependence on
the future canonical definition `edD := -(121665 : Fp)/121666` in
Proofs/EdCurve.lean (the bridge there is one `fp_div_eq_iff` away). -/
/-- Rust: `constants::EDWARDS_D`, u64/constants.rs:45-51.
MATH: EDWARDS_D = ok D with Bnd(D, 2⁵²) and 121666·⟪D⟫ = 121665
in 𝔽_p — i.e. ⟪D⟫ is THE Edwards curve constant d = 121665/121666.
The limbs [929955233495203, 466365720129213, 1662059464998953,
2033849074728123, 1442794654840575] denote the 255-bit number
N_d = 37095705934669439343138083508754565189542113879843219016388785533085940283555
and the spec certifies 121666·N_d ≡ 121665 (mod p) by kernel-verified
literal arithmetic (the `sqrt_m1_spec` technique, ConstSpecs.lean).
(Each limb is < 2⁵¹; stated at the uniform reduced bound 2⁵².)
WHY NEEDED: a corrupted table entry here would change the curve being
implemented — `is_valid`, point addition (via T2d/xy2d caches) and
decompression all multiply by this constant. -/
theorem edwards_d_spec :
backend.serial.u64.constants.EDWARDS_D ⦃ dfe =>
Bnd dfe (2^52) ∧ (121666 : Fp) * ⟪dfe⟫ = -121665 ⦄ := by
unfold backend.serial.u64.constants.EDWARDS_D
backend.serial.u64.field.FieldElement51.from_limbs
-- simp discharges the Bnd conjunct and evaluates `feVal` to the literal
-- N_d; the remaining goal is `(121666 : 𝔽_p) * (N_d : 𝔽_p) = -121665`.
simp [Bnd, denote, feVal, limbsVal, Array.make]
-- 121666·N_d ≡ p 121665 (mod p), checked by literal arithmetic on
-- (norm_num evaluates the ~272-bit product and the division by p in-kernel)
have hmod :
((121666 *
37095705934669439343138083508754565189542113879843219016388785533085940283555 : ))
% P = P - 121665 := by
norm_num [P]
-- assemble: 121666·(N_d:𝔽_p) = ((121666·N_d) mod p : 𝔽_p) = ((p121665) : 𝔽_p) = 121665
have key :
((121666 : ) : Fp) *
((37095705934669439343138083508754565189542113879843219016388785533085940283555 : ) : Fp)
= -121665 := by
rw [← Nat.cast_mul, ← ZMod.natCast_mod, hmod,
natCast_P_sub 121665 (by norm_num [P])]
norm_num
exact_mod_cast key
/-- Rust: `constants::EDWARDS_D2` ("Edwards 2*d value, equal to
2*(121665/121666) mod p"), u64/constants.rs:54-60.
MATH: EDWARDS_D2 = ok D2 with Bnd(D2, 2⁵²) and
121666·⟪D2⟫ = 243330 in 𝔽_p — the SAME characterization shape
as `edwards_d_spec`, with 243330 = 2·(121665), so ⟪D2⟫ = 2d
(made explicit by `edwards_d2_eq_two_d` below).
The limbs [1859910466990425, 932731440258426, 1072319116312658,
1815898335770999, 633789495995903] denote
N_d2 = 16295367250680780974490674513165176452449235426866156013048779062215315747161,
and the spec certifies 121666·N_d2 ≡ 243330 (mod p).
WHY NEEDED: `T2d`/`xy2d` caches are built by multiplying with this
constant; the extended-coordinates addition formulas bake "2d" in. -/
theorem edwards_d2_spec :
backend.serial.u64.constants.EDWARDS_D2 ⦃ d2 =>
Bnd d2 (2^52) ∧ (121666 : Fp) * ⟪d2⟫ = -243330 ⦄ := by
unfold backend.serial.u64.constants.EDWARDS_D2
backend.serial.u64.field.FieldElement51.from_limbs
simp [Bnd, denote, feVal, limbsVal, Array.make]
-- 121666·N_d2 ≡ p 243330 (mod p), literal arithmetic on
have hmod :
((121666 *
16295367250680780974490674513165176452449235426866156013048779062215315747161 : ))
% P = P - 243330 := by
norm_num [P]
have key :
((121666 : ) : Fp) *
((16295367250680780974490674513165176452449235426866156013048779062215315747161 : ) : Fp)
= -243330 := by
rw [← Nat.cast_mul, ← ZMod.natCast_mod, hmod,
natCast_P_sub 243330 (by norm_num [P])]
norm_num
exact_mod_cast key
/-- The two table constants are coherent: ⟪D2⟫ = 2 · ⟪D⟫.
MATH: EDWARDS_D = ok D and EDWARDS_D2 = ok D2 ==> ⟪D2⟫ = 2·⟪D⟫.
Phrased over ANY successful evaluations (the constants are
deterministic, so D/D2 are forced to the spec witnesses).
PROOF: both characterizations live over the invertible scalar 121666:
121666·⟪D2⟫ = 243330 = 2·(121665) = 2·(121666·⟪D⟫) = 121666·(2⟪D⟫),
cancel 121666 (`c121666_ne_zero`).
WHY NEEDED: the op-spec phase proves `to_projective_niels` (which
multiplies by EDWARDS_D2) produces `IsNielsOf` facts; this lemma is the
glue identifying the D2 table entry with "2·d" wherever the math layer
speaks in terms of d alone. -/
theorem edwards_d2_eq_two_d {dfe d2 : Fe}
(hd : backend.serial.u64.constants.EDWARDS_D = ok dfe)
(hd2 : backend.serial.u64.constants.EDWARDS_D2 = ok d2) :
⟪d2⟫ = 2 * ⟪dfe⟫ := by
-- materialize the spec witnesses and identify them with dfe/d2 (determinism)
obtain ⟨d', hd', _, hdv⟩ := spec_exists edwards_d_spec
obtain ⟨d2', hd2', _, hd2v⟩ := spec_exists edwards_d2_spec
rw [hd'] at hd; cases hd
rw [hd2'] at hd2; cases hd2
-- compare the two characterizations over the common factor 121666
have h : (121666 : Fp) * ⟪d2⟫ = (121666 : Fp) * (2 * ⟪dfe⟫) := by
rw [hd2v, mul_left_comm, hdv]
norm_num
exact mul_left_cancel₀ c121666_ne_zero h
/-! ## 3. The identity constants
Rust implements `traits::Identity` for each representation
(curve_models.rs:229-264, edwards.rs:428-437); under Aeneas a Rust
`fn identity()` becomes a 0-argument fallible computation built from the
`ZERO`/`ONE` field constants, so each spec asserts TOTALITY (`= ok _`),
VALIDITY (the predicates of §1 — in particular the Z ≠ 0 obligation the
Rust code never states), and the DENOTATION: the neutral element of the
Edwards group is the affine point (0, 1).
The proofs run the constants via `run_zero`/`run_one` (FieldMain.lean)
and evaluate the transpiled do-blocks on the resulting `ok` values. -/
/-- Rust: `impl Identity for ProjectivePoint` — (X:Y:Z) = (0:1:1),
curve_models.rs:229-237; transpiled at gen/CurveField/Funs.lean:580.
MATH: identity = ok Pt, ProjValid Pt, (projX Pt, projY Pt) = (0, 1).
(x = 0/1 = 0, y = 1/1 = 1 — the Edwards neutral point.) -/
theorem run_projective_identity :
∃ Pt : ProjPoint,
backend.serial.curve_models.ProjectivePoint.Insts.Curve25519_dalekTraitsIdentity.identity
= ok Pt ∧
ProjValid Pt ∧ projX Pt = 0 ∧ projY Pt = 1 := by
-- run the two field constants the do-block binds
obtain ⟨z, hz, hzb, hz0⟩ := run_zero
obtain ⟨o, ho, hob, ho1⟩ := run_one
-- restate at the generated names (fe_zero/fe_one are reducible aliases)
have hz' : backend.serial.u64.field.FieldElement51.ZERO = ok z := hz
have ho' : backend.serial.u64.field.FieldElement51.ONE = ok o := ho
refine ⟨⟨z, o, o⟩, ?_, ⟨hzb, hob, hob, ?_⟩, ?_, ?_⟩
· -- totality: substitute the ok-values, the do-block reduces definitionally
unfold backend.serial.curve_models.ProjectivePoint.Insts.Curve25519_dalekTraitsIdentity.identity
rw [hz', ho']; rfl
· -- Z ≠ 0: ⟪Z⟫ = ⟪o⟫ = 1 ≠ 0
show ⟪o⟫ ≠ 0
rw [ho1]; exact one_ne_zero
· -- x = ⟪z⟫/⟪o⟫ = 0/⟪o⟫ = 0
show ⟪z⟫ / ⟪o⟫ = 0
rw [hz0, zero_div]
· -- y = ⟪o⟫/⟪o⟫ = 1/1 = 1
show ⟪o⟫ / ⟪o⟫ = 1
rw [ho1, div_one]
/-- Rust: `impl Identity for EdwardsPoint` — (X:Y:Z:T) = (0:1:1:0),
edwards.rs:428-437; transpiled at gen/CurveField/Funs.lean:2998.
MATH: identity = ok E, ExtValid E (in particular the extended
coherence X·Y = Z·T holds: 0·1 = 1·0), (edX E, edY E) = (0, 1). -/
theorem run_edwards_identity :
∃ E : EdPoint,
edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity = ok E ∧
ExtValid E ∧ edX E = 0 ∧ edY E = 1 := by
obtain ⟨z, hz, hzb, hz0⟩ := run_zero
obtain ⟨o, ho, hob, ho1⟩ := run_one
have hz' : backend.serial.u64.field.FieldElement51.ZERO = ok z := hz
have ho' : backend.serial.u64.field.FieldElement51.ONE = ok o := ho
refine ⟨⟨z, o, o, z⟩, ?_, ⟨hzb, hob, hob, hzb, ?_, ?_⟩, ?_, ?_⟩
· unfold edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
rw [hz', ho']; rfl
· -- Z ≠ 0
show ⟪o⟫ ≠ 0
rw [ho1]; exact one_ne_zero
· -- coherence X·Y = Z·T: ⟪z⟫·⟪o⟫ = ⟪o⟫·⟪z⟫ (commutativity, value-free)
show ⟪z⟫ * ⟪o⟫ = ⟪o⟫ * ⟪z⟫
ring
· show ⟪z⟫ / ⟪o⟫ = 0
rw [hz0, zero_div]
· show ⟪o⟫ / ⟪o⟫ = 1
rw [ho1, div_one]
/-- Rust: `impl Identity for AffineNielsPoint` — (y+x, yx, 2dxy) = (1,1,0),
curve_models.rs:256-264; transpiled at gen/CurveField/Funs.lean:636.
MATH: identity = ok N, AffNielsValid N, IsAffNielsOf N 0 1 —
the cache of the neutral affine point (x,y) = (0,1):
y+x = 1, yx = 1, 2d·x·y = 0. -/
theorem run_affine_niels_identity :
∃ N : AffNiels,
backend.serial.curve_models.AffineNielsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
= ok N ∧
AffNielsValid N ∧ IsAffNielsOf N 0 1 := by
obtain ⟨z, hz, hzb, hz0⟩ := run_zero
obtain ⟨o, ho, hob, ho1⟩ := run_one
have hz' : backend.serial.u64.field.FieldElement51.ZERO = ok z := hz
have ho' : backend.serial.u64.field.FieldElement51.ONE = ok o := ho
refine ⟨⟨o, o, z⟩, ?_,
⟨hob.mono (by norm_num), hob.mono (by norm_num), hzb⟩, ?_, ?_, ?_⟩
· unfold backend.serial.curve_models.AffineNielsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
rw [ho', hz']; rfl
· -- ⟪y_plus_x⟫ = 1 + 0
show ⟪o⟫ = 1 + 0
rw [ho1]; norm_num
· -- ⟪y_minus_x⟫ = 1 0
show ⟪o⟫ = 1 - 0
rw [ho1]; norm_num
· -- 121666·⟪xy2d⟫ = 243330·(0·1): both sides 0
show (121666 : Fp) * ⟪z⟫ = -243330 * (0 * 1)
rw [hz0]; ring
/-- Rust: `impl Identity for ProjectiveNielsPoint` —
(Y+X, YX, Z, T2d) = (1, 1, 1, 0), curve_models.rs:239-248; transpiled
at gen/CurveField/Funs.lean:599.
MATH: both identities run, ProjNielsValid N, and N IS the niels cache
of the extended identity: IsNielsOf N E
(Y+X = 1+0, YX = 10, Z = 1, 121666·0 = 243330·0).
Stated jointly with the EdwardsPoint identity so the relational
denotation `IsNielsOf` has its reference point in hand. -/
theorem run_projective_niels_identity :
∃ (N : ProjNiels) (E : EdPoint),
backend.serial.curve_models.ProjectiveNielsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
= ok N ∧
edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity = ok E ∧
ProjNielsValid N ∧ IsNielsOf N E := by
obtain ⟨z, hz, hzb, hz0⟩ := run_zero
obtain ⟨o, ho, hob, ho1⟩ := run_one
have hz' : backend.serial.u64.field.FieldElement51.ZERO = ok z := hz
have ho' : backend.serial.u64.field.FieldElement51.ONE = ok o := ho
refine ⟨⟨o, o, o, z⟩, ⟨z, o, o, z⟩, ?_, ?_,
⟨hob.mono (by norm_num), hob.mono (by norm_num), hob, hzb, ?_⟩,
?_, ?_, ?_, ?_⟩
· unfold backend.serial.curve_models.ProjectiveNielsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
rw [ho', hz']; rfl
· unfold edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity
rw [hz', ho']; rfl
· -- ⟪Z⟫ = 1 ≠ 0
show ⟪o⟫ ≠ 0
rw [ho1]; exact one_ne_zero
· -- ⟪Y_plus_X⟫ = ⟪E.Y⟫ + ⟪E.X⟫: 1 = 1 + 0
show ⟪o⟫ = ⟪o⟫ + ⟪z⟫
rw [hz0]; ring
· -- ⟪Y_minus_X⟫ = ⟪E.Y⟫ ⟪E.X⟫: 1 = 1 0
show ⟪o⟫ = ⟪o⟫ - ⟪z⟫
rw [hz0]; ring
· -- ⟪Z⟫ = ⟪E.Z⟫
show ⟪o⟫ = ⟪o⟫
rfl
· -- 121666·⟪T2d⟫ = 243330·⟪E.T⟫: both sides 0 (⟪z⟫ = 0)
show (121666 : Fp) * ⟪z⟫ = -243330 * ⟪z⟫
rw [hz0]; ring
/-! ## 4. Helpers for the op-spec phase
Division-equation rewrites for the coordinate algebra (every point
equation lives over the denominators Z, T, 2Z), a determinism
extractor, and constructor-projection conveniences. All thin wrappers,
named and collected here so the op-spec files read uniformly. -/
/-- MATH: b ≠ 0 ==> (a / b = c ↔ a = c·b) in 𝔽_p.
WHY NEEDED: turns coordinate goals like `edX P = x` (a division) into
denominator-free multiplications that `ring` can chew on — the standard
`field_simp` step, packaged for one denominator. -/
theorem fp_div_eq_iff {a b c : Fp} (hb : b ≠ 0) : a / b = c ↔ a = c * b :=
div_eq_iff hb
/-- MATH: b ≠ 0 ==> (c = a / b ↔ c·b = a) in 𝔽_p (mirror image). -/
theorem fp_eq_div_iff {a b c : Fp} (hb : b ≠ 0) : c = a / b ↔ c * b = a :=
eq_div_iff hb
/-- MATH: b ≠ 0, d ≠ 0 ==> (a/b = c/d ↔ a·d = c·b) in 𝔽_p.
WHY NEEDED: comparing two projective representations of the same affine
coordinate (e.g. output of `to_extended` against the input point)
cross-multiplies exactly like this. -/
theorem fp_div_eq_div_iff {a b c d : Fp} (hb : b ≠ 0) (hd : d ≠ 0) :
a / b = c / d ↔ a * d = c * b :=
div_eq_div_iff hb hd
/-- MATH: a ≠ 0 ==> 2·a ≠ 0 in 𝔽_p (char 𝔽_p ≠ 2, `two_ne_zero'`).
WHY NEEDED: the niels recombination denominator is 2·⟪Z⟫. -/
theorem two_mul_ne_zero {a : Fp} (ha : a ≠ 0) : 2 * a ≠ 0 :=
mul_ne_zero two_ne_zero' ha
/-- Determinism extractor.
MATH: x = ok a and x = ok b ==> a = b (a `Result` computation is
a value, not a relation — two successful runs agree).
WHY NEEDED: op-spec proofs constantly match a hypothesis `f p = ok r`
(from an unfolded caller) against a `run_*`/spec witness `f p = ok r'`
to transport facts about r' to r. (The `rw …; cases …` idiom of
FieldMain.lean, packaged.) -/
theorem ok_ext {α} {x : Result α} {a b : α} (h1 : x = ok a) (h2 : x = ok b) :
a = b := by
rw [h1] at h2
cases h2
rfl
/-! Constructor-projection ("denote-of-pair") conveniences: once a point is
exhibited as a literal `⟨…⟩`, its fields are the components — `rfl`, but
naming them lets op-spec proofs rewrite without `show`-blocks. Marked
`@[simp]` so `simp` collapses projections of freshly built points. -/
@[simp] theorem EdPoint.mk_X (x y z t : Fe) : (edwards.EdwardsPoint.mk x y z t).X = x := rfl
@[simp] theorem EdPoint.mk_Y (x y z t : Fe) : (edwards.EdwardsPoint.mk x y z t).Y = y := rfl
@[simp] theorem EdPoint.mk_Z (x y z t : Fe) : (edwards.EdwardsPoint.mk x y z t).Z = z := rfl
@[simp] theorem EdPoint.mk_T (x y z t : Fe) : (edwards.EdwardsPoint.mk x y z t).T = t := rfl
@[simp] theorem ProjPoint.mk_X (x y z : Fe) :
(backend.serial.curve_models.ProjectivePoint.mk x y z).X = x := rfl
@[simp] theorem ProjPoint.mk_Y (x y z : Fe) :
(backend.serial.curve_models.ProjectivePoint.mk x y z).Y = y := rfl
@[simp] theorem ProjPoint.mk_Z (x y z : Fe) :
(backend.serial.curve_models.ProjectivePoint.mk x y z).Z = z := rfl
@[simp] theorem ComplPoint.mk_X (x y z t : Fe) :
(backend.serial.curve_models.CompletedPoint.mk x y z t).X = x := rfl
@[simp] theorem ComplPoint.mk_Y (x y z t : Fe) :
(backend.serial.curve_models.CompletedPoint.mk x y z t).Y = y := rfl
@[simp] theorem ComplPoint.mk_Z (x y z t : Fe) :
(backend.serial.curve_models.CompletedPoint.mk x y z t).Z = z := rfl
@[simp] theorem ComplPoint.mk_T (x y z t : Fe) :
(backend.serial.curve_models.CompletedPoint.mk x y z t).T = t := rfl
@[simp] theorem ProjNiels.mk_Y_plus_X (a b c d : Fe) :
(backend.serial.curve_models.ProjectiveNielsPoint.mk a b c d).Y_plus_X = a := rfl
@[simp] theorem ProjNiels.mk_Y_minus_X (a b c d : Fe) :
(backend.serial.curve_models.ProjectiveNielsPoint.mk a b c d).Y_minus_X = b := rfl
@[simp] theorem ProjNiels.mk_Z (a b c d : Fe) :
(backend.serial.curve_models.ProjectiveNielsPoint.mk a b c d).Z = c := rfl
@[simp] theorem ProjNiels.mk_T2d (a b c d : Fe) :
(backend.serial.curve_models.ProjectiveNielsPoint.mk a b c d).T2d = d := rfl
@[simp] theorem AffNiels.mk_y_plus_x (a b c : Fe) :
(backend.serial.curve_models.AffineNielsPoint.mk a b c).y_plus_x = a := rfl
@[simp] theorem AffNiels.mk_y_minus_x (a b c : Fe) :
(backend.serial.curve_models.AffineNielsPoint.mk a b c).y_minus_x = b := rfl
@[simp] theorem AffNiels.mk_xy2d (a b c : Fe) :
(backend.serial.curve_models.AffineNielsPoint.mk a b c).xy2d = c := rfl
end CurveFieldProofs

View file

@ -0,0 +1,346 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdDouble.lean — coordinate-level specs for POINT DOUBLING:
`ProjectivePoint::double` (the ℙ² → ℙ¹×ℙ¹ doubling kernel) and
`EdwardsPoint::double` (the extended-coordinates wrapper around it).
WHAT THIS FILE PROVES
* `as_projective_spec` — `EdwardsPoint::as_projective` is a plain
struct rebuild: it copies X, Y, Z (dropping T), is total, and its
output is `ProjValid` whenever the input is `ExtValid`.
* `proj_double_spec` — for ProjValid p, `ProjectivePoint::double p`
is total (no panic/overflow anywhere in the 9 field ops) and returns
the completed point r with the per-field limb bounds
Bnd r.X 2⁵², Bnd r.Y 2⁵³, Bnd r.Z 2⁵², Bnd r.T 2⁵²
and the four COORDINATE EQUATIONS over 𝔽_p (p = 2²⁵⁵ 19)
⟪r.X⟫ = 2·⟪p.X⟫·⟪p.Y⟫
⟪r.Y⟫ = ⟪p.Y⟫² + ⟪p.X⟫²
⟪r.Z⟫ = ⟪p.Y⟫² ⟪p.X⟫²
⟪r.T⟫ = 2·⟪p.Z⟫² (⟪p.Y⟫² ⟪p.X⟫²)
(the X equation is stated in the ring-normal form 2XY; the code
literally computes (X+Y)² (Y²+X²), which `ring` identifies with it).
* `edwards_double_spec` — for ExtValid P, `EdwardsPoint::double P`
(= as_projective ∘ ProjectivePoint::double ∘ CompletedPoint::
as_extended) is total, all four output coordinates are reduced
(Bnd · 2⁵²), and, writing X' Y' Z' T' for the four completed-point
polynomials above evaluated at ⟪P.X⟫ ⟪P.Y⟫ ⟪P.Z⟫, the output denotes
⟪r.X⟫ = X'·T', ⟪r.Y⟫ = Y'·Z', ⟪r.Z⟫ = Z'·T', ⟪r.T⟫ = X'·Y'
— the ℙ¹×ℙ¹ → ℙ³ Segre re-embedding of the doubled point.
STATEMENT POLICY (deliberate). Everything here is COORDINATE-LEVEL: the
hypotheses are the validity predicates of Proofs/EdDenote.lean (limb
bounds + ⟪Z⟫ ≠ 0), and the postconditions are limb bounds plus polynomial
identities over 𝔽_p in the INPUT struct-field denotations. No curve
constant, no division, no `OnCurve` appears: that r really doubles the
denoted affine point (and that ⟪r.Z⟫ ≠ 0, which needs the curve equation)
is the job of the algebra layer (Proofs/EdCurve.lean and the op-law
files), which will consume these specs and `fp_div_*`/`two_ne_zero'`.
RUST ANALOG
`ProjectivePoint::double`, curve25519/solana-ed25519/src/backend/serial/
curve_models.rs:381-397 (transpiled at gen/CurveField/Funs.lean:1464-1487):
let XX = self.X.square();
let YY = self.Y.square();
let ZZ2 = self.Z.square2();
let X_plus_Y = &self.X + &self.Y;
let X_plus_Y_sq = X_plus_Y.square();
let YY_plus_XX = &YY + &XX;
let YY_minus_XX = &YY - &XX;
CompletedPoint { X: &X_plus_Y_sq - &YY_plus_XX, // = 2XY
Y: YY_plus_XX,
Z: YY_minus_XX,
T: &ZZ2 - &YY_minus_XX }
— the "dbl-2008-hwcd" doubling of HisilWongCarterDawson 2008 §3.3
(a = 1 twisted Edwards), with 2·Z² computed by the dedicated `square2`
(verified in Proofs/Square2Spec.lean).
`EdwardsPoint::double`, src/edwards.rs:774-776 (Funs.lean:3261-3265):
self.as_projective().double().as_extended()
with `as_projective` (edwards.rs:541-547, Funs.lean:3029-3033) the X,Y,Z
copy and `CompletedPoint::as_extended` (curve_models.rs:365-372,
Funs.lean:1397-1413) the four cross-multiplications
(X·T, Y·Z, Z·T, X·Y) landing back in extended coordinates.
PANIC-FREEDOM / BOUND BOOKKEEPING (the entire totality argument)
square/square2 inputs need Bnd · 2⁵⁴ — satisfied by ProjValid's 2⁵²;
fe_add on two reduced (2⁵²) inputs: limbwise sums < 2⁵³ < 2⁶⁴, output
Bnd 2⁵³ (the one unreduced value in the body, also fine as a square /
sub input since 2⁵³ < 2⁵⁴);
fe_sub/fe_mul inputs need 2⁵⁴ — all arguments are ≤ 2⁵³ here;
outputs: square/mul 2⁵¹+2¹³ (≤ 2⁵²), square2 2⁵³, sub 2⁵², add 2⁵³.
The `edis` discharge macro below closes every such side condition.
PROOF ARCHITECTURE — the InvertSpec playbook
Each body is walked with the `let*` symbolic-execution steps, consuming
one field op per line via the registered specs (`square_spec'`,
`square2_spec'`, `mul_spec'` and the two LOCAL wrappers `add_spec''`/
`sub_spec''` below, derived from AddSpec/SubNegSpec); the final `ok`
struct is collapsed by `spec_ok` + the `mk_*` projection lemmas of
EdDenote, the bound conjuncts are the step posts (weakened by Bnd.mono),
and each coordinate equation closes by rewriting the chain of value
posts and `ring`.
Imports: Proofs/EdDenote (point predicates, mk_* lemmas),
Proofs/Square2Spec (square2_spec'; transitively SquareSpec /
MulSpec / SubNegSpec / AddSpec and the WP layer).
Imported by: the forthcoming doubling-law file (EdCurve algebra phase).
─────────────────────────────────────────────────────────────────────── -/
import Proofs.EdDenote
import Proofs.Square2Spec
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
-- The step machinery sometimes discharges a side condition before the
-- attached `by edis` block runs (e.g. when an exact hypothesis is already
-- in context); keeping the uniform `by edis` on every step is clearer than
-- special-casing those, so the two "unused tactic" lints are disabled.
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
namespace CurveFieldProofs
-- the weakest-precondition layer: spec_mono / spec_ok used by the wrappers
open Aeneas.Std.WP
/-- Discharge tactic for the side conditions of the doubling bodies: either
a hypothesis verbatim (validity predicates), linear arithmetic
(`scalar_tac`), or a `Bnd _ c ≤ Bnd _ c'` weakening from any hypothesis
via `Bnd.mono` (e.g. a 2⁵¹+2¹³ square output fed to a 2⁵⁴-input op).
Same pattern as `bnd` in Proofs/InvertSpec.lean (macros are file-local,
so it is re-declared here under a fresh name).
(`name :=` disambiguates the generated syntax-kind declaration from the
sibling files' `edis` macros so they can all be imported together.) -/
macro (name := edisDouble) "edis" : tactic =>
`(tactic| (first
| assumption
| scalar_tac
| exact Bnd.mono (by assumption) (by norm_num)))
/-! ## Local step-friendly wrappers for `+` and `-`
The base `add_spec` (Proofs/AddSpec.lean) needs explicit limb lists and
per-limb no-overflow hypotheses, and `sub_spec` (Proofs/SubNegSpec.lean)
needs explicit limb lists; the `let*` machinery cannot invent those. The two
wrappers below repackage them with the limbs hidden (via `Fe.exists_limbs`),
exactly like `mul_spec'`/`square_spec'` in InvertSpec. They are `private`
(file-local): other op-spec files declare their own copies, and privacy
prevents name clashes when several such files are imported together. -/
/-- Rust: `impl Add for FieldElement51` (limbwise `+`, NO reduction),
curve25519/solana-ed25519/src/backend/serial/u64/field.rs:58-73.
MATH: Bnd(a,2⁵²) and Bnd(b,2⁵²) ==> fe_add a b = ok r with
Bnd(r, 2⁵³) and ⟪r⟫ = ⟪a⟫ + ⟪b⟫.
The 2⁵² input bound is the reduced-operand discipline: limbwise sums are
< 2⁵³ < 2⁶⁴ (no u64 overflow), and the output bound doubles — the
generic law `∀ c, Bnd a c → Bnd b c → Bnd r (2c)` of `add_spec`
instantiated at c = 2⁵². The value is exact over , so it adds in 𝔽_p.
WHY NEEDED: `double` adds X+Y and YY+XX; both arguments are reduced
(≤ 2⁵²), and the 2⁵³ output is exactly the bound the postcondition of
`proj_double_spec` exposes for r.Y. -/
private theorem add_spec'' (a b : Fe) (ha : Bnd a (2^52)) (hb : Bnd b (2^52)) :
fe_add a b ⦃ r => Bnd r (2^53) ∧ ⟪r⟫ = ⟪a⟫ + ⟪b⟫ ⦄ := by
-- name the limbs and turn the two Bnd's into per-limb inequalities
obtain ⟨a0, a1, a2, a3, a4, hla⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hlb⟩ := Fe.exists_limbs b
have hba := (Bnd_eq a a0 a1 a2 a3 a4 _ hla).mp ha
have hbb := (Bnd_eq b b0 b1 b2 b3 b4 _ hlb).mp hb
-- run add_spec; each pairwise sum < 2⁵² + 2⁵² = 2⁵³ < 2⁶⁴ is closed by omega
apply spec_mono (add_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hla hlb
⟨by omega, by omega, by omega, by omega, by omega⟩)
rintro r ⟨-, hval, hbnd⟩
-- bound: instantiate the "doubles any common bound" law at 2⁵² (2·2⁵² = 2⁵³)
refine ⟨by simpa using hbnd (2^52) ha hb, ?_⟩
-- value: feVal r = feVal a + feVal b over , then push through the cast
simp [denote, hval]
/-- Rust: `impl Sub for FieldElement51` (add 16p limbwise, subtract, reduce),
curve25519/solana-ed25519/src/backend/serial/u64/field.rs.
MATH: Bnd(a,2⁵⁴) and Bnd(b,2⁵⁴) ==> fe_sub a b = ok r with
Bnd(r, 2⁵²) and ⟪r⟫ = ⟪a⟫ ⟪b⟫
— `sub_spec` (Proofs/SubNegSpec.lean) verbatim, with the limb lists
destructured internally so `let*` can apply it.
WHY NEEDED: `double` subtracts three times (YYXX, (X+Y)²−(YY+XX),
2Z²(YYXX)); all six arguments are ≤ 2⁵³ < 2⁵⁴ here. -/
private theorem sub_spec'' (a b : Fe) (ha : Bnd a (2^54)) (hb : Bnd b (2^54)) :
fe_sub a b ⦃ r => Bnd r (2^52) ∧ ⟪r⟫ = ⟪a⟫ - ⟪b⟫ ⦄ := by
obtain ⟨a0, a1, a2, a3, a4, hla⟩ := Fe.exists_limbs a
obtain ⟨b0, b1, b2, b3, b4, hlb⟩ := Fe.exists_limbs b
exact sub_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hla hlb ha hb
/-! ## The doubling kernel on ℙ² -/
/-- Coordinate-level spec for `ProjectivePoint::double`.
Rust: curve25519/solana-ed25519/src/backend/serial/curve_models.rs:
381-397, transpiled at gen/CurveField/Funs.lean:1464-1487 — the
HisilWongCarterDawson doubling producing a COMPLETED (ℙ¹×ℙ¹) point.
MATH: ProjValid p ==> double p = ok r with
Bnd r.X 2⁵², Bnd r.Y 2⁵³, Bnd r.Z 2⁵², Bnd r.T 2⁵² and, in 𝔽_p,
⟪r.X⟫ = 2·⟪p.X⟫·⟪p.Y⟫ (computed as (X+Y)² (Y²+X²))
⟪r.Y⟫ = ⟪p.Y⟫² + ⟪p.X⟫²
⟪r.Z⟫ = ⟪p.Y⟫² ⟪p.X⟫²
⟪r.T⟫ = 2·⟪p.Z⟫² (⟪p.Y⟫² ⟪p.X⟫²).
LaTeX: $(X':Z') = (2XY : Y^2 - X^2)$, $(Y':T') = (Y^2+X^2 : 2Z^2-(Y^2-X^2))$,
i.e. the doubled point in ℙ¹×ℙ¹ — writing x = X/Z, y = Y/Z, this encodes
x' = 2xy/(2(Z/Z)²−(y²x²))-style fractions whose algebra (and the
nonvanishing of the denominators) is established in the law layer, NOT
here.
Bounds: r.Y is the single unreduced addition of the body (two ≤ 2⁵²
summands ⇒ 2⁵³); the other three fields are `sub` outputs (2⁵²). All
four are < 2⁵⁴, so the completed point can feed any field op directly
(`as_extended`/`as_projective` consume it below / in the add file).
WHY NEEDED: the computational core of point doubling; consumed by
`edwards_double_spec` below and by the scalar-multiplication ladder
specs later. -/
theorem proj_double_spec (p : ProjPoint) (hp : ProjValid p) :
backend.serial.curve_models.ProjectivePoint.double p ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^52) ∧
⟪r.X⟫ = 2 * ⟪p.X⟫ * ⟪p.Y⟫ ∧
⟪r.Y⟫ = ⟪p.Y⟫^2 + ⟪p.X⟫^2 ∧
⟪r.Z⟫ = ⟪p.Y⟫^2 - ⟪p.X⟫^2 ∧
⟪r.T⟫ = 2 * ⟪p.Z⟫^2 - (⟪p.Y⟫^2 - ⟪p.X⟫^2) ⦄ := by
-- the limb bounds of the validity predicate (⟪Z⟫ ≠ 0 is not needed here:
-- doubling never divides — it is carried for the law layer only)
obtain ⟨hpX, hpY, hpZ, -⟩ := hp
-- expose the transpiled 9-op monadic body
unfold backend.serial.curve_models.ProjectivePoint.double
-- XX ← square p.X ⟪XX⟫ = ⟪p.X⟫·⟪p.X⟫, Bnd 2⁵¹+2¹³
let* ⟨ XX, XX_post1, XX_post2 ⟩ ← square_spec' by edis
-- YY ← square p.Y ⟪YY⟫ = ⟪p.Y⟫·⟪p.Y⟫
let* ⟨ YY, YY_post1, YY_post2 ⟩ ← square_spec' by edis
-- ZZ2 ← square2 p.Z ⟪ZZ2⟫ = 2·(⟪p.Z⟫·⟪p.Z⟫), Bnd 2⁵³
let* ⟨ ZZ2, ZZ2_post1, ZZ2_post2 ⟩ ← square2_spec' by edis
-- X_plus_Y ← p.X + p.Y (unreduced add of two reduced values, Bnd 2⁵³)
let* ⟨ XpY, XpY_post1, XpY_post2 ⟩ ← add_spec'' by edis
-- X_plus_Y_sq ← square X_plus_Y
let* ⟨ XpYsq, XpYsq_post1, XpYsq_post2 ⟩ ← square_spec' by edis
-- YY_plus_XX ← YY + XX (both ≤ 2⁵¹+2¹³ ≤ 2⁵², output Bnd 2⁵³ = r.Y)
let* ⟨ YpX, YpX_post1, YpX_post2 ⟩ ← add_spec'' by edis
-- YY_minus_XX ← YY XX (sub reduces: Bnd 2⁵² = r.Z)
let* ⟨ YmX, YmX_post1, YmX_post2 ⟩ ← sub_spec'' by edis
-- fe ← X_plus_Y_sq YY_plus_XX (= 2XY, the r.X numerator)
let* ⟨ feX, feX_post1, feX_post2 ⟩ ← sub_spec'' by edis
-- fe1 ← ZZ2 YY_minus_XX (= 2Z² (Y²X²), the r.T field)
let* ⟨ feT, feT_post1, feT_post2 ⟩ ← sub_spec'' by edis
-- the body returns `ok { X := feX, Y := YpX, Z := YmX, T := feT }`; the
-- `let*` machinery already collapsed the triple on the literal and reduced
-- the struct projections, so the goal is the bare conjunction.
-- Bounds are the step posts verbatim; each equation is the chain of value
-- posts followed by polynomial normalization.
refine ⟨feX_post1, YpX_post1, YmX_post1, feT_post1, ?_, ?_, ?_, ?_⟩
· -- ⟪r.X⟫ = (⟪p.X⟫+⟪p.Y⟫)² (⟪p.Y⟫²+⟪p.X⟫²) = 2·⟪p.X⟫·⟪p.Y⟫
rw [feX_post2, XpYsq_post2, XpY_post2, YpX_post2, YY_post2, XX_post2]; ring
· -- ⟪r.Y⟫ = ⟪p.Y⟫² + ⟪p.X⟫²
rw [YpX_post2, YY_post2, XX_post2]; ring
· -- ⟪r.Z⟫ = ⟪p.Y⟫² ⟪p.X⟫²
rw [YmX_post2, YY_post2, XX_post2]; ring
· -- ⟪r.T⟫ = 2·⟪p.Z⟫² (⟪p.Y⟫² ⟪p.X⟫²)
rw [feT_post2, ZZ2_post2, YmX_post2, YY_post2, XX_post2]; ring
/-! ## The extended-coordinates wrapper -/
/-- Spec for `EdwardsPoint::as_projective`: the ℙ³ → ℙ² forgetful map is a
plain struct rebuild copying X, Y, Z (and dropping the cached T).
Rust: curve25519/solana-ed25519/src/edwards.rs:541-547, transpiled at
gen/CurveField/Funs.lean:3029-3033 (a single `ok { … }`, no field op).
MATH: ExtValid P ==> as_projective P = ok pp with ProjValid pp and
pp.X = P.X, pp.Y = P.Y, pp.Z = P.Z (Fe-level equality of the
limb vectors — strictly stronger than denotation equality, which is what
downstream rewriting uses). ProjValid is inherited: the three copied
fields keep their 2⁵² bounds and ⟪Z⟫ ≠ 0 is ExtValid's own clause; the
extended coherence X·Y = Z·T is simply forgotten.
WHY NEEDED: first step of `EdwardsPoint::double` (and of `is_valid`);
proving it once keeps `edwards_double_spec` a three-step composition. -/
theorem as_projective_spec (P : EdPoint) (hP : ExtValid P) :
edwards.EdwardsPoint.as_projective P ⦃ pp =>
ProjValid pp ∧ pp.X = P.X ∧ pp.Y = P.Y ∧ pp.Z = P.Z ⦄ := by
obtain ⟨hX, hY, hZ, -, hZ0, -⟩ := hP
-- the body is literally `ok { X := P.X, Y := P.Y, Z := P.Z }`
unfold edwards.EdwardsPoint.as_projective
-- collapse the triple on the `ok` literal; the three copy equations reduce
-- to `True` (definitional projections of the literal)
simp only [spec_ok]
-- validity: bounds and ⟪Z⟫ ≠ 0 are ExtValid clauses
exact ⟨⟨hX, hY, hZ, hZ0⟩, trivial, trivial, trivial⟩
/-- Coordinate-level spec for `EdwardsPoint::double`.
Rust: curve25519/solana-ed25519/src/edwards.rs:774-776, transpiled at
gen/CurveField/Funs.lean:3261-3265:
self.as_projective().double().as_extended()
— drop to ℙ², run the doubling kernel (`proj_double_spec`), then re-embed
the completed ℙ¹×ℙ¹ result into extended ℙ³ coordinates via
`CompletedPoint::as_extended` (curve_models.rs:365-372, Funs.lean:
1397-1413), which cross-multiplies (X,Y,Z,T) ↦ (X·T, Y·Z, Z·T, X·Y).
MATH: ExtValid P ==> double P = ok r with all four fields reduced
(Bnd · 2⁵², they are mul outputs) and, abbreviating in 𝔽_p
X' := 2·⟪P.X⟫·⟪P.Y⟫, Y' := ⟪P.Y⟫² + ⟪P.X⟫²,
Z' := ⟪P.Y⟫² ⟪P.X⟫², T' := 2·⟪P.Z⟫² (⟪P.Y⟫² ⟪P.X⟫²),
the four SEGRE-PRODUCT equations
⟪r.X⟫ = X'·T', ⟪r.Y⟫ = Y'·Z', ⟪r.Z⟫ = Z'·T', ⟪r.T⟫ = X'·Y'
(spelled out below with the primed names inlined — the postcondition is
STRICTLY a polynomial identity in ⟪P.X⟫, ⟪P.Y⟫, ⟪P.Z⟫).
⚠ The output is stated coordinate-only, deliberately WITHOUT ⟪r.Z⟫ ≠ 0
and without the extended coherence ⟪r.X⟫·⟪r.Y⟫ = ⟪r.Z⟫·⟪r.T⟫ (so not as
`ExtValid r`): the coherence is a one-line `ring` consequence of the
four equations (X'T'·Y'Z' = Z'T'·X'Y'), and Z'·T' ≠ 0 genuinely needs
the curve equation on (edX P, edY P) — both belong to the algebra layer
that packages doubling as a group law. Note the cached T of the INPUT
is not consumed by doubling at all (as_projective drops it), so the
equations mention only ⟪P.X⟫, ⟪P.Y⟫, ⟪P.Z⟫.
WHY NEEDED: the public doubling entry point of the crate; the scalar
multiplication ladder and the group-law file build directly on it. -/
theorem edwards_double_spec (P : EdPoint) (hP : ExtValid P) :
edwards.EdwardsPoint.double P ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^52) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^52) ∧
⟪r.X⟫ = (2 * ⟪P.X⟫ * ⟪P.Y⟫) *
(2 * ⟪P.Z⟫^2 - (⟪P.Y⟫^2 - ⟪P.X⟫^2)) ∧
⟪r.Y⟫ = (⟪P.Y⟫^2 + ⟪P.X⟫^2) * (⟪P.Y⟫^2 - ⟪P.X⟫^2) ∧
⟪r.Z⟫ = (⟪P.Y⟫^2 - ⟪P.X⟫^2) *
(2 * ⟪P.Z⟫^2 - (⟪P.Y⟫^2 - ⟪P.X⟫^2)) ∧
⟪r.T⟫ = (2 * ⟪P.X⟫ * ⟪P.Y⟫) * (⟪P.Y⟫^2 + ⟪P.X⟫^2) ⦄ := by
-- expose the 3-step transpiled body
unfold edwards.EdwardsPoint.double
-- pp ← as_projective P (copies X, Y, Z; ProjValid from ExtValid)
let* ⟨ pp, pp_valid, ppX, ppY, ppZ ⟩ ← as_projective_spec by edis
-- cp ← ProjectivePoint.double pp (the kernel, spec above)
let* ⟨ cp, cpX_b, cpY_b, cpZ_b, cpT_b, cpX_v, cpY_v, cpZ_v, cpT_v ⟩ ←
proj_double_spec by edis
-- the tail call: as_extended cp — four cross-multiplications
unfold backend.serial.curve_models.CompletedPoint.as_extended
-- rX ← cp.X * cp.T, rY ← cp.Y * cp.Z, rZ ← cp.Z * cp.T, rT ← cp.X * cp.Y
-- (every factor is ≤ 2⁵³ < 2⁵⁴ by the kernel's bounds — edis weakens)
let* ⟨ rX, rX_post1, rX_post2 ⟩ ← mul_spec' by edis
let* ⟨ rY, rY_post1, rY_post2 ⟩ ← mul_spec' by edis
let* ⟨ rZ, rZ_post1, rZ_post2 ⟩ ← mul_spec' by edis
let* ⟨ rT, rT_post1, rT_post2 ⟩ ← mul_spec' by edis
-- final struct literal: the `let*` machinery already collapsed the triple
-- and reduced the projections, leaving the bare conjunction.
-- bounds: mul outputs are 2⁵¹+2¹³ ≤ 2⁵²; equations: substitute the mul
-- posts, the kernel's coordinate equations, and the as_projective copies,
-- then normalize
refine ⟨rX_post1.mono (by norm_num), rY_post1.mono (by norm_num),
rZ_post1.mono (by norm_num), rT_post1.mono (by norm_num),
?_, ?_, ?_, ?_⟩
-- (after the rewrites both sides are syntactically identical, so the `rfl`
-- built into `rw` closes each goal — no `ring` needed)
· -- ⟪r.X⟫ = ⟪cp.X⟫·⟪cp.T⟫ = X'·T'
rw [rX_post2, cpX_v, cpT_v, ppX, ppY, ppZ]
· -- ⟪r.Y⟫ = ⟪cp.Y⟫·⟪cp.Z⟫ = Y'·Z'
rw [rY_post2, cpY_v, cpZ_v, ppX, ppY]
· -- ⟪r.Z⟫ = ⟪cp.Z⟫·⟪cp.T⟫ = Z'·T'
rw [rZ_post2, cpZ_v, cpT_v, ppX, ppY, ppZ]
· -- ⟪r.T⟫ = ⟪cp.X⟫·⟪cp.Y⟫ = X'·Y'
rw [rT_post2, cpX_v, cpY_v, ppX, ppY]
end CurveFieldProofs

View file

@ -0,0 +1,911 @@
/- ───────────────────────────────────────────────────────────────────────────
Proofs/EdMain.lean — TIER-1 MAIN THEOREM: the transpiled curve25519 point
operations implement the COMPLETE twisted Edwards addition law on the
curve x² + y² = 1 + d·x²·y² over 𝔽_p, p = 2²⁵⁵ 19.
WHAT THIS FILE PROVES. Proofs/FieldMain.lean established that the
transpiled `FieldElement51` code implements the field 𝔽_p; the Ed* files
established, coordinate by coordinate, what every transpiled POINT
operation computes (EdDouble/EdAddProjNiels/EdAddAffNiels/EdConvert) and
what the pure MATHEMATICS of the curve says (EdCurve: the curve constant
d, the BernsteinLange completeness theorem, the group-operation laws).
This file welds the two layers together. Writing `edPt P` for the affine
point (edX P, edY P) ∈ 𝔽_p × 𝔽_p denoted by an extended point P and
`OnCurveExt P` for "edPt P satisfies the curve equation", we prove that
for valid on-curve inputs each public `EdwardsPoint` operation
* RUNS (returns `ok` — every limb stays inside the dalek 2⁵²/2⁵⁴
discipline, no u64/u128 overflow, no panic),
* PRESERVES the representation invariant (`ExtValid`: limb bounds,
Z ≢ 0, the Segre coherence X·Y = Z·T) and the curve membership
(`OnCurveExt` — via the mathematical closure theorem), and
* DENOTES the mathematical operation:
identity ↦ edId neg P ↦ edNeg (edPt P)
add P Q ↦ edAdd (edPt P) (edPt Q)
sub P Q ↦ edAdd (edPt P) (edNeg (edPt Q))
double P ↦ edAdd (edPt P) (edPt P)
where `edAdd` is THE complete twisted Edwards addition law of
Proofs/EdCurve.lean — one branch-free formula, total on the curve
because d is not a square (`completeness`).
The results are packaged as the certificate `IsEdwardsImplementation`
and THE MAIN THEOREM `edwardsImplementation`, mirroring the
`IsFieldImplementation`/`fieldImplementation` pair of FieldMain.lean,
followed by implementation-level corollaries (`impl_add_comm_ed`,
`impl_add_id_ed`, `impl_add_neg_ed`) deriving the group-ish laws by
actually RUNNING the transpiled code.
PROOF ARCHITECTURE (bottom-up):
1. DENOTATION BRIDGES. `ext_X_eq`/`ext_Y_eq`/`ext_T_eq` recover the
projective coordinates from the affine ones (X = x·Z, Y = y·Z,
T = x·y·Z — the last from the Segre coherence), `ext_oncurve_poly`
clears the denominators of the curve equation once and for all, and
`niels_T2d_eq`/`affniels_xy2d_eq` convert the denominator-free
121666-characterizations of the cached T·2d / 2d·x·y fields into
honest equations over the canonical curve constant `edD` (cancelling
the unit 121666 against `edD_char`).
2. THE CENTRAL ALGEBRA LEMMA `add_law_fractions`. Every HWCD08 mixed
addition kernel produces a completed point whose four fields are a
COMMON NONZERO FACTOR s times the four canonical quantities
x₁y₂ + x₂y₁, y₁y₂ + x₁x₂, 1 + d·x₁x₂y₁y₂, 1 d·x₁x₂y₁y₂.
Given those factorizations the lemma concludes: both denominators
are nonzero (BernsteinLange `completeness` kills the parenthesized
factors, s ≠ 0 the rest) and the two quotients are EXACTLY the two
components of `edAdd (x₁,y₁) (x₂,y₂)`.
3. KERNEL LAWS. For each of the four mixed kernels (add/sub against a
projective or affine niels cache) a triple `*_law` composes the
coordinate spec with the bridges of step 1 — substituting X = x·Z
etc. turns each coordinate post into the s-factorization required by
step 2, with `ring` doing the bookkeeping — and concludes that the
completed output denotes the edAdd of the inputs (negated second
argument for the sub kernels, since the crossed cache fields are
precisely the cache of the negated point).
4. TOP-LEVEL LAWS. The public `EdwardsPoint` API is run end to end:
`add`/`sub` = as_projective_niels ∘ kernel ∘ as_extended (composed
with `spec_bind`, the re-extension handled by a relaxed-bound
version of EdConvert's `compl_as_extended_spec`, since the kernel
outputs carry 2⁵³/2⁵⁴ bounds); `double` consumes EdDouble's already-
composed Segre products, where the curve equation rewrites the
doubling denominators y² x² and 2 (y² x²) into 1 ± d·x²y²;
`neg` and `identity` are direct. Curve membership of every output
is `edAdd_closure`/`onCurve_neg`/`onCurve_id` — pure mathematics.
5. PACKAGING + COROLLARIES, as described above.
AXIOM HYGIENE: `#print axioms edwardsImplementation` (kept live at the
bottom of this file) reports exactly [propext, Classical.choice,
Quot.sound] — Lean's standard axioms; no sorry, no native_decide, no
custom axiom. Nothing in gen/ (the transpiled code) is modified.
Imports: Proofs/EdCurve (mathematics), Proofs/EdDenote (denotations),
Proofs/EdDouble + EdAddProjNiels + EdAddAffNiels + EdConvert (coordinate
specs); these pull in FieldMain and the whole field layer transitively.
Imported by: nothing — this is the root of the point-law development.
─────────────────────────────────────────────────────────────────────── -/
import Proofs.EdCurve
import Proofs.EdDenote
import Proofs.EdDouble
import Proofs.EdAddProjNiels
import Proofs.EdAddAffNiels
import Proofs.EdConvert
open Aeneas Aeneas.Std Aeneas.Std.WP Result
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option maxRecDepth 8000
namespace CurveFieldProofs
/-! ## 0. The denoted affine point and the curve-membership predicate -/
/-- The affine point denoted by an extended (ℙ³) point:
`edPt P = (edX P, edY P) = (⟪P.X⟫/⟪P.Z⟫, ⟪P.Y⟫/⟪P.Z⟫) ∈ 𝔽_p × 𝔽_p`.
This is the object the MATHEMATICAL layer (Proofs/EdCurve.lean) speaks
about: `edAdd`/`edNeg`/`edId` act on such pairs. Meaningful under
`ExtValid P` (division by ⟪Z⟫ ≠ 0). `noncomputable` because 𝔽_p
division goes through the classical field instance — never executed. -/
noncomputable def edPt (P : EdPoint) : Fp × Fp := (edX P, edY P)
/-- Curve membership of an extended point, stated on its DENOTATION:
MATH: OnCurveExt P :<=> (edX P)² + (edY P)² = 1 + d·(edX P)²·(edY P)².
This is the semantic invariant the Rust `EdwardsPoint` type maintains
implicitly (every constructor — identity, decompression, the arithmetic
proved below — establishes it; no run-time check exists). Deliberately
NOT part of `ExtValid`: representation validity (limb bounds, Z ≠ 0,
Segre) and curve membership are independent concerns, threaded as two
separate hypotheses throughout. -/
def OnCurveExt (P : EdPoint) : Prop := OnCurve (edX P) (edY P)
/-! ## 1. Denotation bridges: projective coordinates from affine ones
The coordinate specs of the Ed* files speak in the struct-field
denotations ⟪P.X⟫, ⟪P.Y⟫, ⟪P.Z⟫, ⟪P.T⟫; the mathematics speaks in the
affine pair (edX P, edY P). These lemmas translate: every field is the
corresponding affine coordinate times ⟪P.Z⟫ (T carrying the PRODUCT
x·y, by the Segre coherence). -/
/-- MATH: ⟪P.Z⟫ ≠ 0 ==> ⟪P.X⟫ = edX P · ⟪P.Z⟫ (clear the denominator
of edX P = ⟪P.X⟫/⟪P.Z⟫).
WHY NEEDED: the kernel-law proofs substitute this everywhere to turn
the coordinate posts into polynomials in (edX, edY, ⟪Z⟫). -/
theorem ext_X_eq (P : EdPoint) (hZ0 : ⟪P.Z⟫ ≠ 0) : ⟪P.X⟫ = edX P * ⟪P.Z⟫ := by
unfold edX
rw [div_mul_cancel₀ _ hZ0]
/-- MATH: ⟪P.Z⟫ ≠ 0 ==> ⟪P.Y⟫ = edY P · ⟪P.Z⟫. Mirror of `ext_X_eq`. -/
theorem ext_Y_eq (P : EdPoint) (hZ0 : ⟪P.Z⟫ ≠ 0) : ⟪P.Y⟫ = edY P * ⟪P.Z⟫ := by
unfold edY
rw [div_mul_cancel₀ _ hZ0]
/-- The T-denotation lemma.
MATH: ⟪P.Z⟫ ≠ 0 and ⟪P.X⟫·⟪P.Y⟫ = ⟪P.Z⟫·⟪P.T⟫ (the Segre/extended
coherence carried by `ExtValid`) ==> ⟪P.T⟫ = edX P · edY P · ⟪P.Z⟫.
I.e. the cached fourth coordinate T really carries the PRODUCT of the
affine coordinates (T/Z = x·y) — the property that lets the mixed
addition kernels charge the d·x₁x₂y₁y₂ term to a single multiplication
T₁·(T₂·2d). Proof: substitute X = x·Z, Y = y·Z into Segre and cancel
one ⟪P.Z⟫ ≠ 0. -/
theorem ext_T_eq (P : EdPoint) (hZ0 : ⟪P.Z⟫ ≠ 0)
(hSeg : ⟪P.X⟫ * ⟪P.Y⟫ = ⟪P.Z⟫ * ⟪P.T⟫) :
⟪P.T⟫ = edX P * edY P * ⟪P.Z⟫ := by
apply mul_left_cancel₀ hZ0
rw [← hSeg, ext_X_eq P hZ0, ext_Y_eq P hZ0]
ring
/-- Quotient form of `ext_T_eq`: ⟪P.T⟫ / ⟪P.Z⟫ = edX P · edY P.
WHY NEEDED: the reader-friendly statement of "T caches x·y"; not used
by the proofs below (they prefer the denominator-free `ext_T_eq`). -/
theorem ext_T_div (P : EdPoint) (hZ0 : ⟪P.Z⟫ ≠ 0)
(hSeg : ⟪P.X⟫ * ⟪P.Y⟫ = ⟪P.Z⟫ * ⟪P.T⟫) :
⟪P.T⟫ / ⟪P.Z⟫ = edX P * edY P := by
rw [fp_div_eq_iff hZ0, ext_T_eq P hZ0 hSeg]
/-- The curve equation with the denominators cleared ONCE.
MATH: for ⟪P.Z⟫ ≠ 0,
OnCurveExt P <=> (⟪P.X⟫² + ⟪P.Y⟫²)·⟪P.Z⟫² = ⟪P.Z⟫⁴ + d·⟪P.X⟫²·⟪P.Y⟫²
— the PROJECTIVE (homogeneous-degree-4) form of x² + y² = 1 + d·x²y²
under x = X/Z, y = Y/Z. Both directions are a single `linear_combination`
over the nonzero scalar ⟪P.Z⟫⁴.
WHY NEEDED: the limb-level bridge for curve membership — e.g. a future
`is_valid`/decompression spec checks exactly this polynomial; the law
proofs below mostly use the affine form directly. -/
theorem ext_oncurve_poly (P : EdPoint) (hZ0 : ⟪P.Z⟫ ≠ 0) :
OnCurveExt P ↔
(-(⟪P.X⟫^2) + ⟪P.Y⟫^2) * ⟪P.Z⟫^2 = ⟪P.Z⟫^4 + edD * ⟪P.X⟫^2 * ⟪P.Y⟫^2 := by
have hX := ext_X_eq P hZ0
have hY := ext_Y_eq P hZ0
have hZ4 : ⟪P.Z⟫^4 ≠ 0 := pow_ne_zero 4 hZ0
unfold OnCurveExt OnCurve
constructor
· -- affine ⇒ projective: multiply the affine equation by ⟪P.Z⟫⁴
intro h
rw [hX, hY]
linear_combination ⟪P.Z⟫^4 * h
· -- projective ⇒ affine: both sides are ⟪P.Z⟫⁴ times the affine sides
intro h
rw [hX, hY] at h
apply mul_left_cancel₀ hZ4
linear_combination h
/-- The T2d-cache conversion.
MATH: IsNielsOf N Q ==> ⟪N.T2d⟫ = 2·d·⟪Q.T⟫.
`IsNielsOf` (Proofs/EdDenote.lean) characterizes the cached field
denominator-free as 121666·⟪N.T2d⟫ = 243330·⟪Q.T⟫ (so that file needs
no `edD`); combined with the canonical characterization
121666·d = 121665 (`edD_char`, Proofs/EdCurve.lean) and the
invertibility of 121666 (`c121666_ne_zero`) this pins the cache to the
honest field element 2·d·⟪Q.T⟫.
WHY NEEDED: lets the projective-niels kernel laws name the d-term of
the addition formulas through the canonical constant `edD`. -/
theorem niels_T2d_eq {N : ProjNiels} {Q : EdPoint} (hN : IsNielsOf N Q) :
⟪N.T2d⟫ = 2 * edD * ⟪Q.T⟫ := by
obtain ⟨-, -, -, h⟩ := hN
-- cancel the unit 121666 on both sides
apply mul_left_cancel₀ c121666_ne_zero
rw [h]
-- 243330·T = 121666·(2·d·T) because 121666·d = 121665 (edD_char)
linear_combination (-2 * ⟪Q.T⟫) * edD_char
/-- The xy2d-cache conversion (affine analogue of `niels_T2d_eq`).
MATH: IsAffNielsOf N x y ==> ⟪N.xy2d⟫ = 2·d·(x·y).
Same 121666-cancellation against `edD_char`. -/
theorem affniels_xy2d_eq {N : AffNiels} {x y : Fp} (hN : IsAffNielsOf N x y) :
⟪N.xy2d⟫ = 2 * edD * (x * y) := by
obtain ⟨-, -, h⟩ := hN
apply mul_left_cancel₀ c121666_ne_zero
rw [h]
linear_combination (-2 * (x * y)) * edD_char
/-! ## 2. The central algebra lemma
Each HWCD08 mixed-addition kernel returns a completed (ℙ¹×ℙ¹) point
whose four fields share a common nonzero factor s (s = 2·Z₁·Z₂ for the
projective-niels kernels, s = 2·Z₁ for the affine ones, the second
input negated for the sub kernels). Everything that is specific to a
kernel is establishing those four factorizations; everything they have
in COMMON — completeness of the denominators and the identification
with `edAdd` — is this one lemma. -/
/-- CENTRAL ALGEBRA LEMMA. If the four fields of a completed point are a
common nonzero factor s times the four canonical addition-law
quantities of the curve points (x₁,y₁), (x₂,y₂), then the point's two
denominators are NONZERO and its two quotients are EXACTLY the complete
twisted Edwards sum `edAdd (x₁,y₁) (x₂,y₂)`.
MATH: s ≠ 0, OnCurve x₁ y₁, OnCurve x₂ y₂,
rX = s·(x₁y₂ + x₂y₁), rY = s·(y₁y₂ + x₁x₂),
rZ = s·(1 + d·x₁x₂y₁y₂), rT = s·(1 d·x₁x₂y₁y₂)
==> rZ ≠ 0 ∧ rT ≠ 0 ∧ rX/rZ = (edAdd (x₁,y₁) (x₂,y₂)).1
∧ rY/rT = (edAdd (x₁,y₁) (x₂,y₂)).2.
The nonvanishing is the BernsteinLange COMPLETENESS theorem
(Proofs/EdCurve.lean): d is not a square, hence 1 ± d·x₁x₂y₁y₂ ≠ 0 at
EVERY pair of curve points — no exceptional cases, which is precisely
why the branch-free Rust code is correct as written. The quotient
identities are then division-cancellation of s (cross-multiplication
+ `ring`). -/
theorem add_law_fractions {x1 y1 x2 y2 s rX rY rZ rT : Fp}
(hs : s ≠ 0) (hc1 : OnCurve x1 y1) (hc2 : OnCurve x2 y2)
(hX : rX = s * (x1 * y2 + x2 * y1))
(hY : rY = s * (y1 * y2 + x1 * x2))
(hZ : rZ = s * (1 + edD * x1 * x2 * y1 * y2))
(hT : rT = s * (1 - edD * x1 * x2 * y1 * y2)) :
rZ ≠ 0 ∧ rT ≠ 0 ∧
rX / rZ = (edAdd (x1, y1) (x2, y2)).1 ∧
rY / rT = (edAdd (x1, y1) (x2, y2)).2 := by
-- BernsteinLange: both parenthesized denominators are units on the curve
obtain ⟨hp, hm⟩ := completeness hc1 hc2
have hZ0 : rZ ≠ 0 := by rw [hZ]; exact mul_ne_zero hs hp
have hT0 : rT ≠ 0 := by rw [hT]; exact mul_ne_zero hs hm
refine ⟨hZ0, hT0, ?_, ?_⟩
· -- x-component: cancel s from numerator and denominator
show rX / rZ = (x1 * y2 + x2 * y1) / (1 + edD * x1 * x2 * y1 * y2)
rw [fp_div_eq_div_iff hZ0 hp, hX, hZ]
ring
· -- y-component: same cancellation against the "" denominator
show rY / rT = (y1 * y2 + x1 * x2) / (1 - edD * x1 * x2 * y1 * y2)
rw [fp_div_eq_div_iff hT0 hm, hY, hT]
ring
/-! ## 3. Kernel laws: the four mixed add/sub kernels denote `edAdd`
Each law upgrades the corresponding coordinate spec (EdAddProjNiels /
EdAddAffNiels) from "these polynomials in the struct fields" to "the
completed output DENOTES the Edwards sum", threading the nonzero
denominators that the conversion back to ℙ³ will need. The bounds in
the postconditions are those of the coordinate specs, verbatim. -/
/-- LAW for the projective-niels mixed ADDITION kernel
(`EdwardsPoint + &ProjectiveNielsPoint → CompletedPoint`,
curve_models.rs:411-430).
MATH: for an extended point P₁ and the niels cache N of an extended
point P₂ — both valid, both ON THE CURVE — the kernel runs and its
completed output r satisfies, beyond the limb bounds of
`add_projniels_spec`:
⟪r.Z⟫ ≠ 0, ⟪r.T⟫ ≠ 0 (completeness — the ℙ¹×ℙ¹ point is honest),
(complX r, complY r) = edAdd (edPt P₁) (edPt P₂).
Proof: substitute Xᵢ = xᵢZᵢ, Yᵢ = yᵢZᵢ, Tᵢ = xᵢyᵢZᵢ (the §1 bridges)
into the four coordinate posts; `ring` reshapes them into the common
factorization s = 2·Z₁·Z₂ required by `add_law_fractions`. -/
theorem add_projniels_law (P1 : EdPoint) (N : ProjNiels) {P2 : EdPoint}
(hN : IsNielsOf N P2) (h1 : ExtValid P1) (h2 : ExtValid P2)
(hc1 : OnCurveExt P1) (hc2 : OnCurveExt P2) (hNv : ProjNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBProjectiveNielsPointCompletedPoint.add
P1 N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^52) ∧
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
complX r = (edAdd (edPt P1) (edPt P2)).1 ∧
complY r = (edAdd (edPt P1) (edPt P2)).2 ⦄ := by
-- run the coordinate-level spec and strengthen its post
apply spec_mono (add_projniels_spec P1 N h1 hNv)
rintro r ⟨hbX, hbY, hbZ, hbT, hrX, hrY, hrZ, hrT⟩
-- the cache fields in terms of P2's coordinates (incl. the d-term)
have hN2d := niels_T2d_eq hN
obtain ⟨hNyp, hNym, hNZ, -⟩ := hN
-- the §1 bridges for both inputs
obtain ⟨-, -, -, -, hZ1, hSeg1⟩ := h1
obtain ⟨-, -, -, -, hZ2, hSeg2⟩ := h2
have hX1 := ext_X_eq P1 hZ1
have hY1 := ext_Y_eq P1 hZ1
have hT1 := ext_T_eq P1 hZ1 hSeg1
have hX2 := ext_X_eq P2 hZ2
have hY2 := ext_Y_eq P2 hZ2
have hT2 := ext_T_eq P2 hZ2 hSeg2
have hc1' : OnCurve (edX P1) (edY P1) := hc1
have hc2' : OnCurve (edX P2) (edY P2) := hc2
-- the common factor s = 2·Z₁·Z₂ is a unit
have hs : (2 : Fp) * ⟪P1.Z⟫ * ⟪P2.Z⟫ ≠ 0 :=
mul_ne_zero (mul_ne_zero two_ne_zero' hZ1) hZ2
-- the four s-factorizations (HWCD08 algebra, certified by `ring`)
have eX : ⟪r.X⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(edX P1 * edY P2 + edX P2 * edY P1) := by
rw [hrX, hNyp, hNym, hX1, hY1, hX2, hY2]; ring
have eY : ⟪r.Y⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(edY P1 * edY P2 + edX P1 * edX P2) := by
rw [hrY, hNyp, hNym, hX1, hY1, hX2, hY2]; ring
have eZ : ⟪r.Z⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(1 + edD * edX P1 * edX P2 * edY P1 * edY P2) := by
rw [hrZ, hNZ, hN2d, hT1, hT2]; ring
have eT : ⟪r.T⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(1 - edD * edX P1 * edX P2 * edY P1 * edY P2) := by
rw [hrT, hNZ, hN2d, hT1, hT2]; ring
-- the central lemma does the rest
obtain ⟨hZ0, hT0, hxd, hyd⟩ := add_law_fractions hs hc1' hc2' eX eY eZ eT
exact ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hxd, hyd⟩
/-- LAW for the projective-niels mixed SUBTRACTION kernel
(`EdwardsPoint &ProjectiveNielsPoint → CompletedPoint`,
curve_models.rs:433-452).
MATH: under the same hypotheses as `add_projniels_law`, the sub kernel
computes edAdd (edPt P₁) (edNeg (edPt P₂)) — subtraction IS addition
of the negated point. The crossed cache fields (Y₂∓X₂ in place of
Y₂±X₂) and the flipped sign of the T·2d term are exactly the cache of
(x₂, y₂): the SAME factorizations as the add law emerge, with the
central lemma instantiated at (edX P₂, edY P₂), whose curve membership
is `onCurve_neg`. -/
theorem sub_projniels_law (P1 : EdPoint) (N : ProjNiels) {P2 : EdPoint}
(hN : IsNielsOf N P2) (h1 : ExtValid P1) (h2 : ExtValid P2)
(hc1 : OnCurveExt P1) (hc2 : OnCurveExt P2) (hNv : ProjNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBProjectiveNielsPointCompletedPoint.sub
P1 N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^54) ∧
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
complX r = (edAdd (edPt P1) (edNeg (edPt P2))).1 ∧
complY r = (edAdd (edPt P1) (edNeg (edPt P2))).2 ⦄ := by
apply spec_mono (sub_projniels_spec P1 N h1 hNv)
rintro r ⟨hbX, hbY, hbZ, hbT, hrX, hrY, hrZ, hrT⟩
have hN2d := niels_T2d_eq hN
obtain ⟨hNyp, hNym, hNZ, -⟩ := hN
obtain ⟨-, -, -, -, hZ1, hSeg1⟩ := h1
obtain ⟨-, -, -, -, hZ2, hSeg2⟩ := h2
have hX1 := ext_X_eq P1 hZ1
have hY1 := ext_Y_eq P1 hZ1
have hT1 := ext_T_eq P1 hZ1 hSeg1
have hX2 := ext_X_eq P2 hZ2
have hY2 := ext_Y_eq P2 hZ2
have hT2 := ext_T_eq P2 hZ2 hSeg2
have hc1' : OnCurve (edX P1) (edY P1) := hc1
-- the second point of the addition is the NEGATION (x₂, y₂)
have hc2' : OnCurve (-(edX P2)) (edY P2) := onCurve_neg hc2
have hs : (2 : Fp) * ⟪P1.Z⟫ * ⟪P2.Z⟫ ≠ 0 :=
mul_ne_zero (mul_ne_zero two_ne_zero' hZ1) hZ2
-- factorizations at (x₁,y₁), (x₂,y₂): the crossed products supply the
-- sign flips, `ring` checks them
have eX : ⟪r.X⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(edX P1 * edY P2 + -(edX P2) * edY P1) := by
rw [hrX, hNyp, hNym, hX1, hY1, hX2, hY2]; ring
have eY : ⟪r.Y⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(edY P1 * edY P2 + edX P1 * -(edX P2)) := by
rw [hrY, hNyp, hNym, hX1, hY1, hX2, hY2]; ring
have eZ : ⟪r.Z⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(1 + edD * edX P1 * -(edX P2) * edY P1 * edY P2) := by
rw [hrZ, hNZ, hN2d, hT1, hT2]; ring
have eT : ⟪r.T⟫ = 2 * ⟪P1.Z⟫ * ⟪P2.Z⟫ *
(1 - edD * edX P1 * -(edX P2) * edY P1 * edY P2) := by
rw [hrT, hNZ, hN2d, hT1, hT2]; ring
obtain ⟨hZ0, hT0, hxd, hyd⟩ := add_law_fractions hs hc1' hc2' eX eY eZ eT
exact ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hxd, hyd⟩
/-- LAW for the affine-niels mixed ADDITION kernel
(`EdwardsPoint + &AffineNielsPoint → CompletedPoint`,
curve_models.rs:458-472).
MATH: for valid on-curve P₁ and the affine cache N of a curve point
(x₂, y₂) (implicit Z₂ = 1), the kernel's completed output denotes
edAdd (edPt P₁) (x₂, y₂). Identical algebra to `add_projniels_law`
with Z₂ := 1, common factor s = 2·Z₁. -/
theorem add_affniels_law (P1 : EdPoint) (N : AffNiels) {x2 y2 : Fp}
(hN : IsAffNielsOf N x2 y2) (h1 : ExtValid P1)
(hc1 : OnCurveExt P1) (hc2 : OnCurve x2 y2) (hNv : AffNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBAffineNielsPointCompletedPoint.add
P1 N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^52) ∧
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
complX r = (edAdd (edPt P1) (x2, y2)).1 ∧
complY r = (edAdd (edPt P1) (x2, y2)).2 ⦄ := by
apply spec_mono (add_affniels_spec P1 N h1 hNv)
rintro r ⟨hbX, hbY, hbZ, hbT, hrX, hrY, hrZ, hrT⟩
have hxy2d := affniels_xy2d_eq hN
obtain ⟨hNyp, hNym, -⟩ := hN
obtain ⟨-, -, -, -, hZ1, hSeg1⟩ := h1
have hX1 := ext_X_eq P1 hZ1
have hY1 := ext_Y_eq P1 hZ1
have hT1 := ext_T_eq P1 hZ1 hSeg1
have hc1' : OnCurve (edX P1) (edY P1) := hc1
-- common factor s = 2·Z₁ (the affine cache has implicit Z₂ = 1)
have hs : (2 : Fp) * ⟪P1.Z⟫ ≠ 0 := mul_ne_zero two_ne_zero' hZ1
have eX : ⟪r.X⟫ = 2 * ⟪P1.Z⟫ * (edX P1 * y2 + x2 * edY P1) := by
rw [hrX, hNyp, hNym, hX1, hY1]; ring
have eY : ⟪r.Y⟫ = 2 * ⟪P1.Z⟫ * (edY P1 * y2 + edX P1 * x2) := by
rw [hrY, hNyp, hNym, hX1, hY1]; ring
have eZ : ⟪r.Z⟫ = 2 * ⟪P1.Z⟫ * (1 + edD * edX P1 * x2 * edY P1 * y2) := by
rw [hrZ, hxy2d, hT1]; ring
have eT : ⟪r.T⟫ = 2 * ⟪P1.Z⟫ * (1 - edD * edX P1 * x2 * edY P1 * y2) := by
rw [hrT, hxy2d, hT1]; ring
obtain ⟨hZ0, hT0, hxd, hyd⟩ := add_law_fractions hs hc1' hc2 eX eY eZ eT
exact ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hxd, hyd⟩
/-- LAW for the affine-niels mixed SUBTRACTION kernel
(`EdwardsPoint &AffineNielsPoint → CompletedPoint`,
curve_models.rs:479-493).
MATH: the sub kernel denotes edAdd (edPt P₁) (x₂, y₂) — addition of
the negated cached point, exactly as in `sub_projniels_law` (crossed
products + flipped Txy2d sign), at Z₂ = 1. -/
theorem sub_affniels_law (P1 : EdPoint) (N : AffNiels) {x2 y2 : Fp}
(hN : IsAffNielsOf N x2 y2) (h1 : ExtValid P1)
(hc1 : OnCurveExt P1) (hc2 : OnCurve x2 y2) (hNv : AffNielsValid N) :
SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBAffineNielsPointCompletedPoint.sub
P1 N ⦃ r =>
Bnd r.X (2^52) ∧ Bnd r.Y (2^53) ∧ Bnd r.Z (2^52) ∧ Bnd r.T (2^54) ∧
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
complX r = (edAdd (edPt P1) (-x2, y2)).1 ∧
complY r = (edAdd (edPt P1) (-x2, y2)).2 ⦄ := by
apply spec_mono (sub_affniels_spec P1 N h1 hNv)
rintro r ⟨hbX, hbY, hbZ, hbT, hrX, hrY, hrZ, hrT⟩
have hxy2d := affniels_xy2d_eq hN
obtain ⟨hNyp, hNym, -⟩ := hN
obtain ⟨-, -, -, -, hZ1, hSeg1⟩ := h1
have hX1 := ext_X_eq P1 hZ1
have hY1 := ext_Y_eq P1 hZ1
have hT1 := ext_T_eq P1 hZ1 hSeg1
have hc1' : OnCurve (edX P1) (edY P1) := hc1
have hc2' : OnCurve (-x2) y2 := onCurve_neg hc2
have hs : (2 : Fp) * ⟪P1.Z⟫ ≠ 0 := mul_ne_zero two_ne_zero' hZ1
have eX : ⟪r.X⟫ = 2 * ⟪P1.Z⟫ * (edX P1 * y2 + -x2 * edY P1) := by
rw [hrX, hNyp, hNym, hX1, hY1]; ring
have eY : ⟪r.Y⟫ = 2 * ⟪P1.Z⟫ * (edY P1 * y2 + edX P1 * -x2) := by
rw [hrY, hNyp, hNym, hX1, hY1]; ring
have eZ : ⟪r.Z⟫ = 2 * ⟪P1.Z⟫ * (1 + edD * edX P1 * -x2 * edY P1 * y2) := by
rw [hrZ, hxy2d, hT1]; ring
have eT : ⟪r.T⟫ = 2 * ⟪P1.Z⟫ * (1 - edD * edX P1 * -x2 * edY P1 * y2) := by
rw [hrT, hxy2d, hT1]; ring
obtain ⟨hZ0, hT0, hxd, hyd⟩ := add_law_fractions hs hc1' hc2' eX eY eZ eT
exact ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hxd, hyd⟩
/-! ## 4. The ℙ¹×ℙ¹ → ℙ³ re-embedding at the kernels' true bounds
EdConvert's `compl_as_extended_spec` requires `ComplValid` (all fields
≤ 2⁵²), but the add/sub kernels output Y at 2⁵³ and one of Z/T at 2⁵⁴
(the stacked unreduced add). All four are still legal `fe_mul` inputs
(≤ 2⁵⁴), so the conversion runs fine — we re-prove its spec at the
relaxed bounds, walking the 4-multiplication body with `spec_bind`. -/
/-- Relaxed-bound spec for `CompletedPoint::as_extended`
(curve_models.rs:365-372 — X' = X·T, Y' = Y·Z, Z' = Z·T, T' = X·Y).
MATH: for any completed point with all fields ≤ 2⁵⁴ and BOTH
denominators nonzero, the conversion runs and returns an `ExtValid`
extended point denoting the SAME affine point (numerators and
denominators are multiplied through by the same nonzero factors;
Segre holds by construction: (XT)(YZ) = (ZT)(XY)). -/
theorem compl_as_extended_law (p : ComplPoint)
(hbX : Bnd p.X (2^54)) (hbY : Bnd p.Y (2^54))
(hbZ : Bnd p.Z (2^54)) (hbT : Bnd p.T (2^54))
(hZ0 : ⟪p.Z⟫ ≠ 0) (hT0 : ⟪p.T⟫ ≠ 0) :
backend.serial.curve_models.CompletedPoint.as_extended p ⦃ r =>
ExtValid r ∧ edX r = complX p ∧ edY r = complY p ⦄ := by
-- expose the 4-multiplication body and walk it with spec_bind
unfold backend.serial.curve_models.CompletedPoint.as_extended
-- fe ← X·T
apply spec_bind (mul_spec' _ _ hbX hbT)
rintro fe ⟨fe_b, fe_v⟩
-- fe1 ← Y·Z
apply spec_bind (mul_spec' _ _ hbY hbZ)
rintro fe1 ⟨fe1_b, fe1_v⟩
-- fe2 ← Z·T (the new common denominator — a product of two units)
apply spec_bind (mul_spec' _ _ hbZ hbT)
rintro fe2 ⟨fe2_b, fe2_v⟩
-- fe3 ← X·Y (the new T-cache)
apply spec_bind (mul_spec' _ _ hbX hbY)
rintro fe3 ⟨fe3_b, fe3_v⟩
-- terminal `ok {X := fe, Y := fe1, Z := fe2, T := fe3}`: collapse the
-- triple with `spec_ok` and unfold the predicate/denotations (the
-- constructor projections reduce definitionally during the unfolding)
simp only [spec_ok, ExtValid, edX, edY, complX, complY]
have hrZ : ⟪fe2⟫ ≠ 0 := by
rw [fe2_v]; exact mul_ne_zero hZ0 hT0
refine ⟨⟨fe_b.mono (by norm_num), fe1_b.mono (by norm_num),
fe2_b.mono (by norm_num), fe3_b.mono (by norm_num), hrZ, ?_⟩,
?_, ?_⟩
· -- Segre by construction: (XT)·(YZ) = (ZT)·(XY)
rw [fe_v, fe1_v, fe2_v, fe3_v]; ring
· -- x preserved: (XT)/(ZT) = X/Z ⟺ (XT)·Z = X·(ZT)
rw [fp_div_eq_div_iff hrZ hZ0, fe_v, fe2_v]; ring
· -- y preserved: (YZ)/(ZT) = Y/T ⟺ (YZ)·T = Y·(ZT)
rw [fp_div_eq_div_iff hrZ hT0, fe1_v, fe2_v]; ring
/-! ## 5. Top-level laws: the public `EdwardsPoint` API -/
/-- THE ADDITION LAW for the public operator
`impl Add<&EdwardsPoint> for &EdwardsPoint` (edwards.rs:785-787,
transpiled at gen/CurveField/Funs.lean:3271-3283), whose body is
let pnp ← as_projective_niels(Q); -- cache Q
let cp ← P + pnp; -- HWCD08 mixed addition
cp.as_extended() -- back to ℙ³
MATH: ExtValid P, ExtValid Q, OnCurveExt P, OnCurveExt Q ==>
add P Q = ok R with ExtValid R, OnCurveExt R, and
edPt R = edAdd (edPt P) (edPt Q)
— the transpiled addition IS the complete twisted Edwards addition law,
with the representation invariant and curve membership preserved
(the latter by the mathematical closure theorem `edAdd_closure`). -/
theorem edwards_add_law (P Q : EdPoint)
(hP : ExtValid P) (hQ : ExtValid Q)
(hcP : OnCurveExt P) (hcQ : OnCurveExt Q) :
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P Q ⦃ R =>
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt Q) ⦄ := by
unfold SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
-- pnp ← as_projective_niels Q (EdConvert: valid cache, IsNielsOf pnp Q)
apply spec_bind (edwards_as_projective_niels_spec Q hQ)
rintro pnp ⟨hpnpv, hpnpn⟩
-- cp ← P + pnp (the kernel law: completed point denoting the edAdd)
apply spec_bind (add_projniels_law P pnp hpnpn hP hQ hcP hcQ hpnpv)
rintro cp ⟨cbX, cbY, cbZ, cbT, cZ0, cT0, cx, cy⟩
-- tail: as_extended cp (relaxed-bound conversion, §4)
apply spec_mono (compl_as_extended_law cp (cbX.mono (by norm_num))
(cbY.mono (by norm_num)) cbZ (cbT.mono (by norm_num)) cZ0 cT0)
rintro R ⟨hRv, hRx, hRy⟩
refine ⟨hRv, ?_, ?_⟩
· -- curve membership: the denoted point IS an edAdd value, and edAdd is
-- closed on the curve (Proofs/EdCurve.lean)
show OnCurve (edX R) (edY R)
rw [hRx, cx, hRy, cy]
exact edAdd_closure (show OnCurve (edX P) (edY P) from hcP)
(show OnCurve (edX Q) (edY Q) from hcQ)
· -- the denotation equation, assembled componentwise
calc edPt R = (edX R, edY R) := rfl
_ = ((edAdd (edPt P) (edPt Q)).1, (edAdd (edPt P) (edPt Q)).2) := by
rw [hRx, cx, hRy, cy]
_ = edAdd (edPt P) (edPt Q) := rfl
/-- THE SUBTRACTION LAW for the public operator
`impl Sub<&EdwardsPoint> for &EdwardsPoint` (edwards.rs:806-808,
Funs.lean:3328-3340): same pipeline as `add` with the mixed SUB kernel.
MATH: on valid on-curve inputs, sub P Q = ok R with ExtValid R,
OnCurveExt R, and edPt R = edAdd (edPt P) (edNeg (edPt Q)) — i.e.
P Q is P + (Q), the group subtraction. -/
theorem edwards_sub_law (P Q : EdPoint)
(hP : ExtValid P) (hQ : ExtValid Q)
(hcP : OnCurveExt P) (hcQ : OnCurveExt Q) :
SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBEdwardsPointEdwardsPoint.sub
P Q ⦃ R =>
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edNeg (edPt Q)) ⦄ := by
unfold SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBEdwardsPointEdwardsPoint.sub
-- pnp ← as_projective_niels Q
apply spec_bind (edwards_as_projective_niels_spec Q hQ)
rintro pnp ⟨hpnpv, hpnpn⟩
-- cp ← P pnp (kernel law: denotes edAdd with the NEGATED point)
apply spec_bind (sub_projniels_law P pnp hpnpn hP hQ hcP hcQ hpnpv)
rintro cp ⟨cbX, cbY, cbZ, cbT, cZ0, cT0, cx, cy⟩
-- tail: as_extended cp (Z here is 2⁵², T 2⁵⁴ — roles swapped vs add)
apply spec_mono (compl_as_extended_law cp (cbX.mono (by norm_num))
(cbY.mono (by norm_num)) (cbZ.mono (by norm_num)) cbT cZ0 cT0)
rintro R ⟨hRv, hRx, hRy⟩
refine ⟨hRv, ?_, ?_⟩
· -- closure at (edPt P, edNeg (edPt Q)) — the negation stays on the curve
show OnCurve (edX R) (edY R)
rw [hRx, cx, hRy, cy]
exact edAdd_closure (show OnCurve (edX P) (edY P) from hcP)
(onCurve_neg (show OnCurve (edX Q) (edY Q) from hcQ))
· calc edPt R = (edX R, edY R) := rfl
_ = ((edAdd (edPt P) (edNeg (edPt Q))).1,
(edAdd (edPt P) (edNeg (edPt Q))).2) := by
rw [hRx, cx, hRy, cy]
_ = edAdd (edPt P) (edNeg (edPt Q)) := rfl
/-- THE DOUBLING LAW for `EdwardsPoint::double` (edwards.rs:774-776):
doubling denotes adding the point to itself with the COMPLETE law —
no special doubling case distinction exists, because none is needed.
MATH: ExtValid P, OnCurveExt P ==> double P = ok R with
ExtValid R, OnCurveExt R, edPt R = edAdd (edPt P) (edPt P).
PROOF. `edwards_double_spec` (EdDouble.lean) already gives the four
composed Segre products of the dbl-2008-hwcd kernel; substituting
X = x·Z, Y = y·Z and writing u := y² x², the curve equation
x² + y² = 1 + d·x²y² rewrites the doubling denominators
u = 1 + d·x²y² and 2 u = 1 d·x²y²,
turning the products into
⟪R.X⟫ = Z⁴·2xy·(1 D), ⟪R.Y⟫ = Z⁴·(y²+x²)·(1 + D),
⟪R.Z⟫ = Z⁴·(1 + D)(1 D), (D := d·x²y²)
whence edX R = 2xy/(1 + D) and edY R = (y²+x²)/(1 D) — exactly
`edAdd (x,y) (x,y)` — with ⟪R.Z⟫ ≠ 0 by completeness at ((x,y),(x,y)). -/
theorem edwards_double_law (P : EdPoint) (hP : ExtValid P) (hcP : OnCurveExt P) :
edwards.EdwardsPoint.double P ⦃ R =>
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt P) ⦄ := by
apply spec_mono (edwards_double_spec P hP)
rintro R ⟨hbX, hbY, hbZ, hbT, hvX, hvY, hvZ, hvT⟩
obtain ⟨-, -, -, -, hZ0, -⟩ := hP
have hc : OnCurve (edX P) (edY P) := hcP
-- completeness at the DIAGONAL pair ((x,y),(x,y)) — the doubling case
obtain ⟨hp, hm⟩ := completeness hc hc
have hX := ext_X_eq P hZ0
have hY := ext_Y_eq P hZ0
have hZ4 : ⟪P.Z⟫^4 ≠ 0 := pow_ne_zero 4 hZ0
-- the curve equation in the doubling-friendly form y² x² = 1 + D
have hcur : edY P ^ 2 - edX P ^ 2
= 1 + edD * edX P * edX P * edY P * edY P := by
have h := hc
unfold OnCurve at h
linear_combination h
-- the three composed products, rewritten through the curve equation into
-- Z⁴ times the canonical addition-law quantities at (x,y),(x,y)
have eX : ⟪R.X⟫ = ⟪P.Z⟫^4 * ((edX P * edY P + edX P * edY P) *
(1 - edD * edX P * edX P * edY P * edY P)) := by
rw [hvX, hX, hY]
linear_combination (-(2 * edX P * edY P * ⟪P.Z⟫^4)) * hcur
have eY : ⟪R.Y⟫ = ⟪P.Z⟫^4 * ((edY P * edY P + edX P * edX P) *
(1 + edD * edX P * edX P * edY P * edY P)) := by
rw [hvY, hX, hY]
linear_combination (⟪P.Z⟫^4 * (edY P * edY P + edX P * edX P)) * hcur
have eZ : ⟪R.Z⟫ = ⟪P.Z⟫^4 * ((1 + edD * edX P * edX P * edY P * edY P) *
(1 - edD * edX P * edX P * edY P * edY P)) := by
rw [hvZ, hX, hY]
linear_combination (⟪P.Z⟫^4 *
(1 - edD * edX P * edX P * edY P * edY P - (edY P ^ 2 - edX P ^ 2))) * hcur
-- the output denominator is a product of units (Z⁴ and the two complete
-- denominators)
have hRZ : ⟪R.Z⟫ ≠ 0 := by
rw [eZ]
exact mul_ne_zero hZ4 (mul_ne_zero hp hm)
-- the two affine coordinates of the double
have hxR : edX R = (edAdd (edPt P) (edPt P)).1 := by
show ⟪R.X⟫ / ⟪R.Z⟫ = (edX P * edY P + edX P * edY P) /
(1 + edD * edX P * edX P * edY P * edY P)
rw [fp_div_eq_div_iff hRZ hp, eX, eZ]
ring
have hyR : edY R = (edAdd (edPt P) (edPt P)).2 := by
show ⟪R.Y⟫ / ⟪R.Z⟫ = (edY P * edY P + edX P * edX P) /
(1 - edD * edX P * edX P * edY P * edY P)
rw [fp_div_eq_div_iff hRZ hm, eY, eZ]
ring
refine ⟨⟨hbX, hbY, hbZ, hbT, hRZ, ?_⟩, ?_, ?_⟩
· -- Segre: (X'T')·(Y'Z') = (Z'T')·(X'Y') — pure ring on the products
rw [hvX, hvY, hvZ, hvT]; ring
· -- curve membership via closure at the diagonal
show OnCurve (edX R) (edY R)
rw [hxR, hyR]
exact edAdd_closure hc hc
· calc edPt R = (edX R, edY R) := rfl
_ = ((edAdd (edPt P) (edPt P)).1, (edAdd (edPt P) (edPt P)).2) := by
rw [hxR, hyR]
_ = edAdd (edPt P) (edPt P) := rfl
/-- THE NEGATION LAW for `impl Neg for &EdwardsPoint` (edwards.rs:844-851):
negation denotes the mathematical Edwards negation (x, y) ↦ (x, y).
MATH: ExtValid P, OnCurveExt P ==> neg P = ok R with ExtValid R,
OnCurveExt R (negation stays on the curve: `onCurve_neg`), and
edPt R = edNeg (edPt P). Direct from EdConvert's `edwards_neg_spec`. -/
theorem edwards_neg_law (P : EdPoint) (hP : ExtValid P) (hcP : OnCurveExt P) :
SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg P ⦃ R =>
ExtValid R ∧ OnCurveExt R ∧ edPt R = edNeg (edPt P) ⦄ := by
apply spec_mono (edwards_neg_spec P hP)
rintro R ⟨hRv, -, -, -, -, hx, hy⟩
refine ⟨hRv, ?_, ?_⟩
· show OnCurve (edX R) (edY R)
rw [hx, hy]
exact onCurve_neg (show OnCurve (edX P) (edY P) from hcP)
· calc edPt R = (edX R, edY R) := rfl
_ = (-(edX P), edY P) := by rw [hx, hy]
_ = edNeg (edPt P) := rfl
/-- THE IDENTITY LAW: the transpiled `EdwardsPoint::identity()` constant
(0 : 1 : 1 : 0) runs, is valid, LIES ON THE CURVE (`onCurve_id`), and
denotes the neutral element edId = (0, 1). Packaging of EdDenote's
`run_edwards_identity` runner with the math-layer facts. -/
theorem run_edwards_identity_law :
∃ I : EdPoint,
edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity = ok I ∧
ExtValid I ∧ OnCurveExt I ∧ edPt I = edId := by
obtain ⟨I, hI, hIv, hx, hy⟩ := run_edwards_identity
refine ⟨I, hI, hIv, ?_, ?_⟩
· show OnCurve (edX I) (edY I)
rw [hx, hy]
exact onCurve_id
· calc edPt I = (edX I, edY I) := rfl
_ = (0, 1) := by rw [hx, hy]
_ = edId := rfl
/-! ## 6. Runners: triple → existential, FieldMain style
One `run_*` per operation, converting the law triples into plain
existentials `∃ R, op = ok R ∧ …` ("the machine code RUNS without
panicking and returns R with these properties") via `spec_exists`
(Proofs/Field.lean) — the exact shape the certificate fields use. -/
/-- Runner for the addition law (see `edwards_add_law`). -/
theorem run_edwards_add (P Q : EdPoint)
(hP : ExtValid P) (hQ : ExtValid Q)
(hcP : OnCurveExt P) (hcQ : OnCurveExt Q) :
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P Q = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt Q) :=
spec_exists (edwards_add_law P Q hP hQ hcP hcQ)
/-- Runner for the subtraction law (see `edwards_sub_law`). -/
theorem run_edwards_sub (P Q : EdPoint)
(hP : ExtValid P) (hQ : ExtValid Q)
(hcP : OnCurveExt P) (hcQ : OnCurveExt Q) :
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBEdwardsPointEdwardsPoint.sub
P Q = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edNeg (edPt Q)) :=
spec_exists (edwards_sub_law P Q hP hQ hcP hcQ)
/-- Runner for the doubling law (see `edwards_double_law`). -/
theorem run_edwards_double (P : EdPoint)
(hP : ExtValid P) (hcP : OnCurveExt P) :
∃ R, edwards.EdwardsPoint.double P = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt P) :=
spec_exists (edwards_double_law P hP hcP)
/-- Runner for the negation law (see `edwards_neg_law`). -/
theorem run_edwards_neg (P : EdPoint)
(hP : ExtValid P) (hcP : OnCurveExt P) :
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg P = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edNeg (edPt P) :=
spec_exists (edwards_neg_law P hP hcP)
/-! ## 7. The Edwards-implementation certificate -/
/-- The transpiled curve25519 point code implements the complete twisted
Edwards addition law on x² + y² = 1 + d·x²·y² over 𝔽_p, through the
denotation `edPt` on valid on-curve extended points.
This `structure … : Prop` is a named conjunction of five claims — a
CERTIFICATE, mirroring `IsFieldImplementation` (FieldMain.lean).
Field by field: each transpiled operation, on inputs satisfying the
representation invariant (`ExtValid`) and the curve equation
(`OnCurveExt`), (1) RETURNS `ok` — no panic, every machine-arithmetic
side condition holds; (2) re-establishes BOTH invariants on its output;
and (3) denotes the corresponding operation of the mathematical layer
(Proofs/EdCurve.lean): the neutral element `edId`, the negation
`edNeg`, and the COMPLETE addition law `edAdd` (with subtraction as
addition of the negation and doubling as self-addition — the same
branch-free formula, total by BernsteinLange completeness).
WHY THIS SHAPE: as with the field layer, a literal group instance on
the struct is impossible (redundant projective representation, partial
machine ops), so the laws transfer through the denotation. -/
structure IsEdwardsImplementation : Prop where
/-- `EdwardsPoint::identity()` runs, is valid, on-curve, denotes (0,1). -/
id_ok : ∃ I : EdPoint,
edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity = ok I ∧
ExtValid I ∧ OnCurveExt I ∧ edPt I = edId
/-- `P` runs and denotes the Edwards negation (x, y) ↦ (x, y). -/
neg_ok : ∀ P : EdPoint, ExtValid P → OnCurveExt P →
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg P = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edNeg (edPt P)
/-- `P + Q` runs and denotes the complete addition law `edAdd`. -/
add_ok : ∀ P Q : EdPoint, ExtValid P → ExtValid Q →
OnCurveExt P → OnCurveExt Q →
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P Q = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt Q)
/-- `P Q` runs and denotes addition of the negation: P + (Q). -/
sub_ok : ∀ P Q : EdPoint, ExtValid P → ExtValid Q →
OnCurveExt P → OnCurveExt Q →
∃ R, SharedAEdwardsPoint.Insts.CoreOpsArithSubSharedBEdwardsPointEdwardsPoint.sub
P Q = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edNeg (edPt Q))
/-- `P.double()` runs and denotes self-addition with the SAME complete
formula — no exceptional doubling case. -/
double_ok : ∀ P : EdPoint, ExtValid P → OnCurveExt P →
∃ R, edwards.EdwardsPoint.double P = ok R ∧
ExtValid R ∧ OnCurveExt R ∧ edPt R = edAdd (edPt P) (edPt P)
/-- **The transpiled code implements the complete twisted Edwards addition
law.**
THE TIER-1 MAIN THEOREM of the point-arithmetic development. Every
clause of the certificate is discharged by the corresponding runner of
§6, which in turn packages: the per-machine-op proofs of the *Spec
files (panic-freedom and exact field arithmetic), the coordinate-level
kernel specs (EdDouble/EdAddProjNiels/EdConvert), the denotation
bridges of this file, and the pure mathematics of Proofs/EdCurve.lean
(d non-square ⇒ completeness; closure; the group identities).
`#print axioms CurveFieldProofs.edwardsImplementation` yields exactly
[propext, Classical.choice, Quot.sound] — Lean's standard axioms only
(checked live at the end of this file). -/
theorem edwardsImplementation : IsEdwardsImplementation where
id_ok := run_edwards_identity_law
neg_ok := fun P hP hcP => run_edwards_neg P hP hcP
add_ok := fun P Q hP hQ hcP hcQ => run_edwards_add P Q hP hQ hcP hcQ
sub_ok := fun P Q hP hQ hcP hcQ => run_edwards_sub P Q hP hQ hcP hcQ
double_ok := fun P hP hcP => run_edwards_double P hP hcP
/-! ## 8. Group-ish laws THROUGH the implementation
Each corollary runs the actual transpiled operations and states the
corresponding mathematical law up to denotation — the implementation-
level mirror of `edAdd_comm`/`edAdd_id`/`edAdd_neg` (EdCurve.lean),
in the style of FieldMain's `impl_*` corollaries. As there, the limb
vectors of the two sides generally DIFFER; only the denoted affine
points agree, which is why the laws are stated through `edPt`. -/
/-- Commutativity at the implementation level.
MATH: for valid on-curve P, Q both `P + Q` and `Q + P` RUN, and their
results denote the same affine point (edAdd is symmetric —
`edAdd_comm`). -/
theorem impl_add_comm_ed (P Q : EdPoint)
(hP : ExtValid P) (hQ : ExtValid Q)
(hcP : OnCurveExt P) (hcQ : OnCurveExt Q) :
∃ R1 R2,
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P Q = ok R1 ∧
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
Q P = ok R2 ∧
edPt R1 = edPt R2 := by
obtain ⟨R1, h1, -, -, e1⟩ := run_edwards_add P Q hP hQ hcP hcQ
obtain ⟨R2, h2, -, -, e2⟩ := run_edwards_add Q P hQ hP hcQ hcP
exact ⟨R1, R2, h1, h2, by rw [e1, e2, edAdd_comm]⟩
/-- Right identity at the implementation level.
MATH: for valid on-curve P, running the identity constant and then
`P + identity` yields a point denoting edPt P itself (`edAdd_id`). -/
theorem impl_add_id_ed (P : EdPoint) (hP : ExtValid P) (hcP : OnCurveExt P) :
∃ I R,
edwards.EdwardsPoint.Insts.Curve25519_dalekTraitsIdentity.identity = ok I ∧
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P I = ok R ∧
edPt R = edPt P := by
obtain ⟨I, hI, hIv, hIc, hIe⟩ := run_edwards_identity_law
obtain ⟨R, hR, -, -, hRe⟩ := run_edwards_add P I hP hIv hcP hIc
refine ⟨I, R, hI, hR, ?_⟩
rw [hRe, hIe]
exact edAdd_id (show OnCurve (edX P) (edY P) from hcP)
/-- Inverses at the implementation level.
MATH: for valid on-curve P, running `P` and then `P + (P)` yields a
point denoting the neutral element edId = (0, 1) (`edAdd_neg`). -/
theorem impl_add_neg_ed (P : EdPoint) (hP : ExtValid P) (hcP : OnCurveExt P) :
∃ N R,
SharedAEdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg P = ok N ∧
SharedAEdwardsPoint.Insts.CoreOpsArithAddSharedBEdwardsPointEdwardsPoint.add
P N = ok R ∧
edPt R = edId := by
obtain ⟨N, hN, hNv, hNc, hNe⟩ := run_edwards_neg P hP hcP
obtain ⟨R, hR, -, -, hRe⟩ := run_edwards_add P N hP hNv hcP hNc
refine ⟨N, R, hN, hR, ?_⟩
rw [hRe, hNe]
exact edAdd_neg (show OnCurve (edX P) (edY P) from hcP)
/- AXIOM AUDIT (live). Expected (and verified) output:
'CurveFieldProofs.edwardsImplementation' depends on axioms:
[propext, Classical.choice, Quot.sound]
— Lean's three standard axioms only: no sorry, no native_decide, no
custom axiom. (The 4 axioms modeling external functions in
gen/CurveField/FunsExternal.lean are outside the dependency cone of the
point operations verified here.) The command's output is informational
and does not affect the build. -/
#print axioms edwardsImplementation
end CurveFieldProofs

View file

@ -20,6 +20,7 @@ source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-300}"
export LEAN_MEM_MB="${LEAN_MEM_MB:-6144}"
CORES="${LEAN_MAX_CORES:-0-3}"
# Layer manifests (extended as the pyramid grows; ORDER = import order).
@ -43,14 +44,23 @@ PROOFS=(
InvertSpec
FieldMain
FeQ
EdCurve
EdDenote
EdDouble
EdAddProjNiels
EdAddAffNiels
EdConvert
EdMain
)
# Fully-qualified certificate names; each must be axiom-clean.
CERTS=(
CurveFieldProofs.fieldImplementation
CurveFieldProofs.edwardsImplementation
)
# Imports needed so every certificate in CERTS is in scope for the audit.
AUDIT_IMPORTS=(
Proofs.FieldMain
Proofs.EdMain
)
# ── Phase 0: resource + integrity guards ────────────────────────────────────
@ -88,7 +98,7 @@ lake env bash -c "
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
compile() {
echo \" · \$1\"
taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -o \"\${1}.olean\" \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; }
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; }
}
for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done
cd '$HERE'
@ -120,7 +130,7 @@ lake env bash -c "
for i in ${AUDIT_IMPORTS[*]}; do echo \"import \$i\"; done
for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done
} > \"\$AUD\"
OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean \"\$AUD\" 2>&1)
OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -M \${LEAN_MEM_MB:-4096} \"\$AUD\" 2>&1)
echo \"\$OUT\"
rm -f \"\$AUD\"
N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true)

47
verification/extract.sh Executable file
View file

@ -0,0 +1,47 @@
#!/usr/bin/env bash
# Regenerate the Lean model in gen/ from the Rust sources.
#
# SCOPE: field arithmetic + Edwards point arithmetic
# roots: crate::field, crate::backend::serial::u64::field,
# crate::backend::serial::curve_models, crate::edwards
# (same widening the reference solution used for its Tier-1 addition-law
# theorem; scalar-mul backends and decompress internals stay opaque —
# upstream Aeneas cannot translate them; they are modeled/axiomatized in
# gen/CurveField/FunsExternal.lean OUTSIDE every certificate's cone).
#
# Rust --charon--> CurveField.llbc --aeneas--> gen/CurveField/*.lean
#
# The hand-written gen/CurveField/{TypesExternal,FunsExternal}.lean are NOT
# touched by regeneration (Aeneas only rewrites the *_Template variants).
# After regenerating, diff the templates against the hand-written files:
# diff gen/CurveField/FunsExternal_Template.lean gen/CurveField/FunsExternal.lean
#
# Usage: ./extract.sh
set -euo pipefail
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)"
cd "$CRATE"
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 \
--opaque 'crate::field::_::internal_invert_batch' \
--opaque 'crate::backend::serial::scalar_mul' \
--opaque 'crate::backend::vector' \
--opaque 'crate::backend::get_selected_backend' \
--opaque 'crate::edwards::decompress' \
--opaque 'crate::edwards::_::sum' \
--opaque 'crate::edwards::_::from_slice' \
--dest-file "$HERE/CurveField.llbc" \
-- --no-default-features
echo "[2/2] aeneas: LLBC -> Lean (split files, CurveField.* modules)"
cd "$HERE"
aeneas -backend lean -split-files -subdir CurveField -dest gen CurveField.llbc
echo "Done. Now run ./check.sh to type-check the regenerated model."

File diff suppressed because it is too large Load diff

View file

@ -24,6 +24,16 @@ set_option maxHeartbeats 1000000
set_option maxRecDepth 2048
open curve25519_dalek
/-- [core::array::{impl core::hash::Hash for [T; N]}::hash]:
Source: '/rustc/library/core/src/array/mod.rs', lines 349:4-349:50
Name pattern: [core::array::{core::hash::Hash<[@T; @N]>}::hash]
Visibility: public -/
@[rust_fun "core::array::{core::hash::Hash<[@T; @N]>}::hash"]
axiom Array.Insts.CoreHashHash.hash
{T : Type} {H : Type} {N : Std.Usize} (hashHashInst : core.hash.Hash T)
(hashHasherInst : core.hash.Hasher H) :
Array T N → H → Result H
/-- [core::fmt::{impl core::fmt::Debug for [T]}::fmt]:
Source: '/rustc/library/core/src/fmt/mod.rs', lines 3122:4-3122:50
Name pattern: [core::fmt::{core::fmt::Debug<[@T]>}::fmt]
@ -36,6 +46,40 @@ axiom Slice.Insts.CoreFmtDebug.fmt
Slice T → core.fmt.Formatter → Result ((core.result.Result Unit
core.fmt.Error) × core.fmt.Formatter)
/-- [core::hash::impls::{impl core::hash::Hash for u8}::hash]:
Source: '/rustc/library/core/src/hash/mod.rs', lines 812:16-812:56
Name pattern: [core::hash::impls::{core::hash::Hash<u8>}::hash]
Visibility: public -/
@[rust_fun "core::hash::impls::{core::hash::Hash<u8>}::hash"]
axiom U8.Insts.CoreHashHash.hash
{H : Type} (HasherInst : core.hash.Hasher H) : Std.U8 → H → Result H
/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
axiom U32.Insts.CoreIterRangeStep.backward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
axiom U32.Insts.CoreIterRangeStep.forward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
Visibility: public -/
@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
axiom U32.Insts.CoreIterRangeStep.steps_between
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::index_mut]:
Source: '/rustc/library/core/src/slice/index.rs', lines 660:4-660:51
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index_mut]
@ -113,6 +157,13 @@ def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
Result (Option (Slice T)) :=
ok (some s)
/-- [subtle::{subtle::Choice}::unwrap_u8]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 133:4-133:33
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
/-- [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
Name pattern: [subtle::{core::convert::From<bool, subtle::Choice>}::from]
@ -122,6 +173,15 @@ def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
def Bool.Insts.CoreConvertFromChoice.from (c : subtle.Choice) : Result Bool :=
ok (c.val != 0)
/-- [subtle::{impl core::ops::bit::BitAnd<subtle::Choice, subtle::Choice> for subtle::Choice}::bitand]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 162:4-162:42
Name pattern: [subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand]
Visibility: public -/
@[rust_fun
"subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand"]
axiom subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand
: subtle.Choice → subtle.Choice → Result subtle.Choice
/-- [subtle::{impl core::ops::bit::BitOr<subtle::Choice, subtle::Choice> for subtle::Choice}::bitor]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 177:4-177:41
Name pattern: [subtle::{core::ops::bit::BitOr<subtle::Choice, subtle::Choice, subtle::Choice>}::bitor]
@ -232,16 +292,135 @@ def U64.Insts.SubtleConditionallySelectable.conditional_swap
(a b : Std.U64) (choice : subtle.Choice) : Result (Std.U64 × Std.U64) :=
ok (if choice.val = 0 then (a, b) else (b, a))
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::internal_invert_batch]:
Source: 'curve25519/solana-ed25519/src/field.rs', lines 195:4-229:5
/-- [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
AXIOM (deliberate): extracted opaque via charon `--opaque`. Dead code under
the extraction feature set (its only caller `invert_batch_alloc` is
alloc-gated); its iterator `rev/zip` loops have no Aeneas model. Give it a
model here if batch inversion ever becomes a verification target. -/
axiom field.FieldElement51.internal_invert_batch
/-- [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
:
Slice backend.serial.u64.field.FieldElement51 → Slice
backend.serial.u64.field.FieldElement51 → Result ((Slice
backend.serial.u64.field.FieldElement51) × (Slice
backend.serial.u64.field.FieldElement51))
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::scalar_mul::vartime_double_base::mul]:
Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1
Visibility: public -/
axiom backend.serial.scalar_mul.vartime_double_base.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 -/
axiom
backend.serial.curve_models.ProjectiveNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.ProjectiveNielsPoint →
backend.serial.curve_models.ProjectiveNielsPoint → subtle.Choice →
Result (backend.serial.curve_models.ProjectiveNielsPoint ×
backend.serial.curve_models.ProjectiveNielsPoint)
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::AffineNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 313:0-327:1
Visibility: public -/
axiom
backend.serial.curve_models.AffineNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.AffineNielsPoint →
backend.serial.curve_models.AffineNielsPoint → subtle.Choice → Result
(backend.serial.curve_models.AffineNielsPoint ×
backend.serial.curve_models.AffineNielsPoint)
/-- [curve25519_dalek::edwards::decompress::step_2]:
Source: 'curve25519-dalek/src/edwards.rs', lines 223:4-240:5 -/
axiom edwards.decompress.step_2
:
edwards.CompressedEdwardsY → backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 → Result edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::decompress::step_1]:
Source: 'curve25519-dalek/src/edwards.rs', lines 209:4-220:5 -/
axiom edwards.decompress.step_1
:
edwards.CompressedEdwardsY → Result (subtle.Choice ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51)
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::from_slice]:
Source: 'curve25519-dalek/src/edwards.rs', lines 404:4-406:5
Visibility: public -/
axiom edwards.CompressedEdwardsY.from_slice
:
Slice Std.U8 → Result (core.result.Result edwards.CompressedEdwardsY
core.array.TryFromSliceError)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
(edwards.EdwardsPoint × edwards.EdwardsPoint)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_assign]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom
edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::{impl core::cmp::Eq for curve25519_dalek::edwards::EdwardsPoint}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/edwards.rs', lines 501:0-501:27
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.EdwardsPoint → Result Unit
/-- [curve25519_dalek::edwards::{impl core::iter::traits::accum::Sum<T> for curve25519_dalek::edwards::EdwardsPoint}::sum]:
Source: 'curve25519-dalek/src/edwards.rs', lines 671:4-676:5
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum
{T : Type} {I : Type} (coreborrowBorrowTEdwardsPointInst : core.borrow.Borrow
T edwards.EdwardsPoint) (coreitertraitsiteratorIteratorInst :
core.iter.traits.iterator.Iterator I T) :
I → Result edwards.EdwardsPoint
/-- [curve25519_dalek::field::{impl core::cmp::Eq for curve25519_dalek::backend::serial::u64::field::FieldElement51}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/field.rs', lines 84:0-84:27
Visibility: public -/
axiom
backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq.assert_fields_are_eq
: backend.serial.u64.field.FieldElement51 → Result Unit

View file

@ -15,6 +15,16 @@ set_option maxHeartbeats 1000000
set_option maxRecDepth 2048
open curve25519_dalek
/-- [core::array::{impl core::hash::Hash for [T; N]}::hash]:
Source: '/rustc/library/core/src/array/mod.rs', lines 349:4-349:50
Name pattern: [core::array::{core::hash::Hash<[@T; @N]>}::hash]
Visibility: public -/
@[rust_fun "core::array::{core::hash::Hash<[@T; @N]>}::hash"]
axiom Array.Insts.CoreHashHash.hash
{T : Type} {H : Type} {N : Std.Usize} (hashHashInst : core.hash.Hash T)
(hashHasherInst : core.hash.Hasher H) :
Array T N → H → Result H
/-- [core::fmt::{impl core::fmt::Debug for [T]}::fmt]:
Source: '/rustc/library/core/src/fmt/mod.rs', lines 3122:4-3122:50
Name pattern: [core::fmt::{core::fmt::Debug<[@T]>}::fmt]
@ -25,6 +35,40 @@ axiom Slice.Insts.CoreFmtDebug.fmt
Slice T → core.fmt.Formatter → Result ((core.result.Result Unit
core.fmt.Error) × core.fmt.Formatter)
/-- [core::hash::impls::{impl core::hash::Hash for u8}::hash]:
Source: '/rustc/library/core/src/hash/mod.rs', lines 812:16-812:56
Name pattern: [core::hash::impls::{core::hash::Hash<u8>}::hash]
Visibility: public -/
@[rust_fun "core::hash::impls::{core::hash::Hash<u8>}::hash"]
axiom U8.Insts.CoreHashHash.hash
{H : Type} (HasherInst : core.hash.Hasher H) : Std.U8 → H → Result H
/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
axiom U32.Insts.CoreIterRangeStep.backward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
axiom U32.Insts.CoreIterRangeStep.forward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
Visibility: public -/
@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
axiom U32.Insts.CoreIterRangeStep.steps_between
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::index_mut]:
Source: '/rustc/library/core/src/slice/index.rs', lines 660:4-660:51
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index_mut]
@ -91,6 +135,13 @@ axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
{T : Type} :
core.ops.range.RangeFull → Slice T → Result (Option (Slice T))
/-- [subtle::{subtle::Choice}::unwrap_u8]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 133:4-133:33
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
/-- [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
Name pattern: [subtle::{core::convert::From<bool, subtle::Choice>}::from]
@ -98,6 +149,15 @@ axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
@[rust_fun "subtle::{core::convert::From<bool, subtle::Choice>}::from"]
axiom Bool.Insts.CoreConvertFromChoice.from : subtle.Choice → Result Bool
/-- [subtle::{impl core::ops::bit::BitAnd<subtle::Choice, subtle::Choice> for subtle::Choice}::bitand]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 162:4-162:42
Name pattern: [subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand]
Visibility: public -/
@[rust_fun
"subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand"]
axiom subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand
: subtle.Choice → subtle.Choice → Result subtle.Choice
/-- [subtle::{impl core::ops::bit::BitOr<subtle::Choice, subtle::Choice> for subtle::Choice}::bitor]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 177:4-177:41
Name pattern: [subtle::{core::ops::bit::BitOr<subtle::Choice, subtle::Choice, subtle::Choice>}::bitor]
@ -178,3 +238,135 @@ axiom U64.Insts.SubtleConditionallySelectable.conditional_assign
axiom U64.Insts.SubtleConditionallySelectable.conditional_swap
: Std.U64 → Std.U64 → subtle.Choice → Result (Std.U64 × Std.U64)
/-- [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
/-- [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::scalar_mul::vartime_double_base::mul]:
Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1
Visibility: public -/
axiom backend.serial.scalar_mul.vartime_double_base.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 -/
axiom
backend.serial.curve_models.ProjectiveNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.ProjectiveNielsPoint →
backend.serial.curve_models.ProjectiveNielsPoint → subtle.Choice →
Result (backend.serial.curve_models.ProjectiveNielsPoint ×
backend.serial.curve_models.ProjectiveNielsPoint)
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::AffineNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 313:0-327:1
Visibility: public -/
axiom
backend.serial.curve_models.AffineNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.AffineNielsPoint →
backend.serial.curve_models.AffineNielsPoint → subtle.Choice → Result
(backend.serial.curve_models.AffineNielsPoint ×
backend.serial.curve_models.AffineNielsPoint)
/-- [curve25519_dalek::edwards::decompress::step_2]:
Source: 'curve25519-dalek/src/edwards.rs', lines 223:4-240:5 -/
axiom edwards.decompress.step_2
:
edwards.CompressedEdwardsY → backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 → Result edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::decompress::step_1]:
Source: 'curve25519-dalek/src/edwards.rs', lines 209:4-220:5 -/
axiom edwards.decompress.step_1
:
edwards.CompressedEdwardsY → Result (subtle.Choice ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51)
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::from_slice]:
Source: 'curve25519-dalek/src/edwards.rs', lines 404:4-406:5
Visibility: public -/
axiom edwards.CompressedEdwardsY.from_slice
:
Slice Std.U8 → Result (core.result.Result edwards.CompressedEdwardsY
core.array.TryFromSliceError)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
(edwards.EdwardsPoint × edwards.EdwardsPoint)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_assign]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom
edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::{impl core::cmp::Eq for curve25519_dalek::edwards::EdwardsPoint}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/edwards.rs', lines 501:0-501:27
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.EdwardsPoint → Result Unit
/-- [curve25519_dalek::edwards::{impl core::iter::traits::accum::Sum<T> for curve25519_dalek::edwards::EdwardsPoint}::sum]:
Source: 'curve25519-dalek/src/edwards.rs', lines 671:4-676:5
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum
{T : Type} {I : Type} (coreborrowBorrowTEdwardsPointInst : core.borrow.Borrow
T edwards.EdwardsPoint) (coreitertraitsiteratorIteratorInst :
core.iter.traits.iterator.Iterator I T) :
I → Result edwards.EdwardsPoint
/-- [curve25519_dalek::field::{impl core::cmp::Eq for curve25519_dalek::backend::serial::u64::field::FieldElement51}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/field.rs', lines 84:0-84:27
Visibility: public -/
axiom
backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq.assert_fields_are_eq
: backend.serial.u64.field.FieldElement51 → Result Unit

View file

@ -15,6 +15,14 @@ set_option maxRecDepth 2048
namespace curve25519_dalek
/-- Trait declaration: [core::borrow::Borrow]
Source: '/rustc/library/core/src/borrow.rs', lines 158:0-158:40
Name pattern: [core::borrow::Borrow]
Visibility: public -/
@[rust_trait "core::borrow::Borrow"]
structure core.borrow.Borrow (Self : Type) (Borrowed : Type) where
borrow : Self → Result Borrowed
/-- Trait declaration: [core::ops::arith::Add]
Source: '/rustc/library/core/src/ops/arith.rs', lines 76:0-76:31
Name pattern: [core::ops::arith::Add]
@ -101,15 +109,95 @@ structure subtle.ConditionallySelectable (Self : Type) where
conditional_assign : Self → Self → subtle.Choice → Result Self
conditional_swap : Self → Self → subtle.Choice → Result (Self × Self)
/-- [curve25519_dalek::backend::BackendKind]
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]
Source: 'curve25519-dalek/src/scalar.rs', lines 202:0-239:1
Visibility: public -/
structure scalar.Scalar where
bytes : Array Std.U8 32#usize
/-- [curve25519_dalek::backend::serial::u64::field::FieldElement51]
Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 43:0-43:47
Visibility: public -/
@[reducible]
def backend.serial.u64.field.FieldElement51 := Array Std.U64 5#usize
/-- [curve25519_dalek::edwards::EdwardsPoint]
Source: 'curve25519-dalek/src/edwards.rs', lines 371:0-376:1
Visibility: public -/
structure edwards.EdwardsPoint where
X : backend.serial.u64.field.FieldElement51
Y : backend.serial.u64.field.FieldElement51
Z : backend.serial.u64.field.FieldElement51
T : backend.serial.u64.field.FieldElement51
/-- [curve25519_dalek::backend::serial::curve_models::ProjectivePoint]
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 154:0-158:1
Visibility: public -/
structure backend.serial.curve_models.ProjectivePoint where
X : backend.serial.u64.field.FieldElement51
Y : backend.serial.u64.field.FieldElement51
Z : backend.serial.u64.field.FieldElement51
/-- [curve25519_dalek::backend::serial::curve_models::CompletedPoint]
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 169:0-174:1
Visibility: public -/
structure backend.serial.curve_models.CompletedPoint where
X : backend.serial.u64.field.FieldElement51
Y : backend.serial.u64.field.FieldElement51
Z : backend.serial.u64.field.FieldElement51
T : backend.serial.u64.field.FieldElement51
/-- [curve25519_dalek::backend::serial::curve_models::AffineNielsPoint]
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 184:0-188:1
Visibility: public -/
structure backend.serial.curve_models.AffineNielsPoint where
y_plus_x : backend.serial.u64.field.FieldElement51
y_minus_x : backend.serial.u64.field.FieldElement51
xy2d : backend.serial.u64.field.FieldElement51
/-- [curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint]
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 206:0-211:1
Visibility: public -/
structure backend.serial.curve_models.ProjectiveNielsPoint where
Y_plus_X : backend.serial.u64.field.FieldElement51
Y_minus_X : backend.serial.u64.field.FieldElement51
Z : backend.serial.u64.field.FieldElement51
T2d : backend.serial.u64.field.FieldElement51
/-- Trait declaration: [curve25519_dalek::traits::Identity]
Source: 'curve25519-dalek/src/traits.rs', lines 26:0-30:1
Visibility: public -/
structure traits.Identity (Self : Type) where
identity : Result Self
/-- Trait declaration: [curve25519_dalek::traits::ValidityCheck]
Source: 'curve25519-dalek/src/traits.rs', lines 412:0-415:1 -/
structure traits.ValidityCheck (Self : Type) where
is_valid : Self → Result Bool
/-- [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]
def backend.serial.u64.field.FieldElement51.from_bytes.closure := Unit
/-- [curve25519_dalek::edwards::CompressedEdwardsY]
Source: 'curve25519-dalek/src/edwards.rs', lines 165:0-165:44
Visibility: public -/
@[reducible]
def edwards.CompressedEdwardsY := Array Std.U8 32#usize
/-- [curve25519_dalek::montgomery::MontgomeryPoint]
Source: 'curve25519-dalek/src/montgomery.rs', lines 76:0-76:41
Visibility: public -/
@[reducible]
def montgomery.MontgomeryPoint := Array Std.U8 32#usize
end curve25519_dalek

130
verification/lean-guard Executable file
View file

@ -0,0 +1,130 @@
#!/usr/bin/env bash
# ────────────────────────────────────────────────────────────────────────────
# lean-guard — HARD-CAPPED Lean compiler wrapper.
#
# Successor to lean-safe after the 2026-07-02 OOM incident: a single `lean`
# elaboration (tactic-search blowup: simp[*]/scalar_tac over a ~60-hypothesis
# context with 2^256-scale literals) grew to 12.2GB RSS and was killed by the
# GLOBAL kernel OOM killer, taking the driving session down with it.
# lean-safe's guards (timeout + affinity + PREFLIGHT headroom) cannot stop
# that: the process passes preflight, then balloons inside its timeout.
#
# NEW GUARDS (in addition to all lean-safe guards):
# A. lean -M <MB> — Lean's internal cap: elaboration aborts
# with a clean "maximum memory exceeded"
# error. First line of defense; graceful.
# B. systemd-run --user --scope
# -p MemoryMax / MemorySwapMax — kernel cgroup cap around the process:
# if Lean's own accounting misses (C-level
# allocations), the cgroup kills ONLY this
# lean, never the session, never the box.
# C. flock on /tmp/lean-guard.lock — machine-wide single-flight: at most ONE
# lean compile at a time, regardless of
# how many agents/scripts are active.
#
# Env knobs (defaults for this 14GB / 8-core ThinkPad):
# LEAN_TIMEOUT per-file wall clock seconds (default 400)
# LEAN_MEM_MB lean -M internal cap, MB (default 4096)
# LEAN_CGROUP_MB cgroup MemoryMax, MB (default LEAN_MEM_MB+1024)
# LEAN_MAX_CORES taskset core range (default 0-3)
# LEAN_MIN_FREE_MB preflight available-RAM floor (default 3072)
# LEAN_LOCK_WAIT max seconds to wait for the lock (default 7200)
#
# Usage: lean-guard <file.lean> [extra lean args...]
# The .olean output path is always computed as ${file%.lean}.olean.
# Requires: lean on PATH (caller sources the toolchain env; typically run
# inside `lake env` so LEAN_PATH is set — this wrapper does NOT clobber env).
# ────────────────────────────────────────────────────────────────────────────
set -uo pipefail
# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort;
# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport
# popups and fill /var/crash. ulimit applies to this shell and every child.
ulimit -c 0 2>/dev/null || true
TIMEOUT_SEC=${LEAN_TIMEOUT:-400}
MEM_MB=${LEAN_MEM_MB:-4096}
CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))}
CORES=${LEAN_MAX_CORES:-0-3}
MIN_FREE_MB=${LEAN_MIN_FREE_MB:-3072}
LOCK_WAIT=${LEAN_LOCK_WAIT:-7200}
LOCK_FILE=/tmp/lean-guard.lock
LOG_FILE="${HOME}/.lean-guard.log"
if ! command -v lean &>/dev/null; then
echo "FATAL: lean not on PATH — source ~/aeneas-toolchain/env.sh (and run inside lake env)"
exit 1
fi
if [ $# -eq 0 ]; then
echo "Usage: lean-guard <file.lean> [lean args...]"
exit 1
fi
LEAN_FILE="$1"; shift || true
# ── Guard 1: source integrity (anti olean-clobber) ──────────────────────────
if [ ! -f "$LEAN_FILE" ]; then
echo "MISSING: $LEAN_FILE"; exit 1
fi
if ! grep -qE '^[[:space:]]*(/-|import |namespace |theorem |def |open |set_option |--)' "$LEAN_FILE" 2>/dev/null; then
echo "FATAL: $LEAN_FILE is not Lean source (binary/olean data?)."
echo " Restore: git checkout HEAD -- $LEAN_FILE"
exit 1
fi
# ── Guard 2: output path ─────────────────────────────────────────────────────
case "$LEAN_FILE" in
*.lean) ;;
*) echo "FATAL: input lacks .lean extension"; exit 1 ;;
esac
OLEAN_FILE="${LEAN_FILE%.lean}.olean"
[ "$OLEAN_FILE" = "$LEAN_FILE" ] && { echo "FATAL: output would clobber source"; exit 1; }
# ── Guard C: machine-wide single-flight ─────────────────────────────────────
exec 9>"$LOCK_FILE"
if ! flock -w "$LOCK_WAIT" 9; then
echo "FATAL: could not acquire lean-guard lock within ${LOCK_WAIT}s (another compile stuck?)"
exit 1
fi
# ── Guard 3: preflight headroom (after lock: serialized measurement) ────────
AVAIL_MB=$(free -m | awk '/Mem:/{print $7}')
if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then
echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile"
exit 1
fi
echo "[$(date -u +%F' '%T)] $LEAN_FILE (t=${TIMEOUT_SEC}s M=${MEM_MB}MB cg=${CGROUP_MB}MB cores=$CORES avail=${AVAIL_MB}MB)" >> "$LOG_FILE"
# ── Compile under both caps ──────────────────────────────────────────────────
run_leancmd() {
taskset -c "$CORES" \
timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
}
if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then
# --scope runs the command as a child of THIS shell (env inherited),
# merely placing it in a fresh cgroup with the hard caps below.
systemd-run --user --scope --quiet \
-p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \
-- taskset -c "$CORES" \
timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
EXIT_CODE=$?
else
echo " (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE"
run_leancmd "$@"
EXIT_CODE=$?
fi
case $EXIT_CODE in
0) echo " OK" >> "$LOG_FILE" ;;
124) echo " TIMEOUT ${TIMEOUT_SEC}s" >> "$LOG_FILE"
echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" ;;
137) echo " KILLED (cgroup MemoryMax ${CGROUP_MB}MB hit)" >> "$LOG_FILE"
echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" ;;
*) echo " FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE" ;;
esac
# stale partial olean from a failed compile must not poison later imports
[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE"
exit $EXIT_CODE