/- ─────────────────────────────────────────────────────────────────────────── 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 Bernstein–Lange 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 (Bernstein–Lange `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 Bernstein–Lange 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 -- Bernstein–Lange: 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 Bernstein–Lange 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