mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-03 19:53:45 +00:00
346 lines
20 KiB
Text
346 lines
20 KiB
Text
/- ───────────────────────────────────────────────────────────────────────────
|
||
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 Hisil–Wong–Carter–Dawson 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 (YY−XX, (X+Y)²−(YY+XX),
|
||
2Z²−(YY−XX)); 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
|
||
Hisil–Wong–Carter–Dawson 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
|
||
-- 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
|
||
-- 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
|
||
-- 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
|