From 40c0da0bb90f1b648c40d5cd5da8697f1e331bd6 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 09:22:09 -0700 Subject: [PATCH 1/2] Fast/Projective: generalize the RCB projective arithmetic over the base field MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `PVes` gains a type parameter (`PVes F`), and every operation and lemma is stated over an arbitrary `[Field F]` in place, under its original name. The completeness arguments take the single hypothesis `hy0 : ∀ x, ¬ OnCurve 0 5 (x, 0)` (no 2-torsion), from which `2 ≠ 0` and `5 ≠ 0` are derived; the bridge to the affine group takes the curve `E` with `E.A = 0`, `E.B = 5`. `[DecidableEq F]` is assumed only by the computable declarations that branch on field equality. `paddFast` stays Vesta-only. Vesta call sites in `MsmProj` and `ProjectiveMontEquiv` pass `Vesta.curve rfl rfl` and `Vesta.no_onCurve_y_zero`; `TrustBoundary`'s census is unchanged. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01TUVBzWdyPZ8AWYoGVYADs6 --- CompElliptic/Curves/Pasta/Fast/MsmProj.lean | 136 ++++---- .../Curves/Pasta/Fast/Projective.lean | 318 +++++++++++------- .../Pasta/Fast/ProjectiveMontEquiv.lean | 61 ++-- 3 files changed, 292 insertions(+), 223 deletions(-) diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean index 0fd0481..768e8f7 100644 --- a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean +++ b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean @@ -41,32 +41,32 @@ local instance : Inhabited Projective.G := ⟨0⟩ /-! ## Projective bucket sum (`foldr padd pid`), mirroring `Fast.Msm.bucketOf` -/ /-- The `padd`-fold sum of a list of projective points, from the projective identity `pid`. -/ -def psum (L : List PVes) : PVes := L.foldr padd pid +def psum (L : List (PVes Fq)) : PVes Fq := L.foldr padd pid -theorem psum_cons (a : PVes) (xs : List PVes) : psum (a :: xs) = padd a (psum xs) := rfl +theorem psum_cons (a : PVes Fq) (xs : List (PVes Fq)) : psum (a :: xs) = padd a (psum xs) := rfl /-- A projective `padd`-sum of valid points is valid, and `toAffine` carries it to the affine sum. -/ -theorem psum_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : - Valid (psum L) ∧ toAffine (psum L) = (L.map toAffine).sum := by +theorem psum_spec (L : List (PVes Fq)) (h : ∀ P ∈ L, Valid P) : + Valid (psum L) ∧ toAffine Vesta.curve rfl rfl (psum L) = (L.map (toAffine Vesta.curve rfl rfl)).sum := by induction L with - | nil => exact ⟨valid_pid, by simp [psum, toAffine_pid]⟩ + | nil => exact ⟨valid_pid, by simp [psum, toAffine_pid Vesta.curve rfl rfl]⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) obtain ⟨hvxs, hxseq⟩ := ih hxs rw [psum_cons] - exact ⟨valid_padd ha hvxs, by rw [toAffine_padd ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ + exact ⟨valid_padd Vesta.no_onCurve_y_zero ha hvxs, by rw [toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ /-- The projective bucket-`b` sum: `padd`-fold the points whose digit tag is `b`. -/ -def pbucketOf (dp : List (ℕ × PVes)) (b : ℕ) : PVes := +def pbucketOf (dp : List (ℕ × PVes Fq)) (b : ℕ) : PVes Fq := psum (dp.filterMap fun p => if p.1 = b then some p.2 else none) /-- The projective bucket sum is valid and matches `Fast.Msm.bucketOf` of the `toAffine`-mapped digit-tagged list. -/ -theorem pbucketOf_spec (dp : List (ℕ × PVes)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : +theorem pbucketOf_spec (dp : List (ℕ × PVes Fq)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : Valid (pbucketOf dp b) - ∧ toAffine (pbucketOf dp b) - = Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) b := by + ∧ toAffine Vesta.curve rfl rfl (pbucketOf dp b) + = Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) b := by have hval : ∀ P ∈ dp.filterMap (fun p => if p.1 = b then some p.2 else none), Valid P := by intro P hP rw [List.mem_filterMap] at hP @@ -85,17 +85,17 @@ theorem pbucketOf_spec (dp : List (ℕ × PVes)) (b : ℕ) (h : ∀ p ∈ dp, Va /-- One step of the projective suffix-sum accumulator: carry `(running, total)`, `padd` the next bucket into `running`, then `padd` `running` into `total`. -/ -def paccStep (a : PVes) (p : PVes × PVes) : PVes × PVes := +def paccStep (a : PVes Fq) (p : PVes Fq × PVes Fq) : PVes Fq × PVes Fq := (padd p.1 a, padd p.2 (padd p.1 a)) /-- Folding `paccStep` over valid points keeps both accumulator components valid, and `toAffine` carries the whole fold (componentwise) to the affine `Fast.Msm.accStep` fold. -/ -theorem foldr_paccStep_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : +theorem foldr_paccStep_spec (L : List (PVes Fq)) (h : ∀ P ∈ L, Valid P) : Valid (L.foldr paccStep (pid, pid)).1 ∧ Valid (L.foldr paccStep (pid, pid)).2 - ∧ (toAffine (L.foldr paccStep (pid, pid)).1, toAffine (L.foldr paccStep (pid, pid)).2) - = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map toAffine) := by + ∧ (toAffine Vesta.curve rfl rfl (L.foldr paccStep (pid, pid)).1, toAffine Vesta.curve rfl rfl (L.foldr paccStep (pid, pid)).2) + = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map (toAffine Vesta.curve rfl rfl)) := by induction L with - | nil => exact ⟨valid_pid, valid_pid, by simp [toAffine_pid]⟩ + | nil => exact ⟨valid_pid, valid_pid, by simp [toAffine_pid Vesta.curve rfl rfl]⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -103,30 +103,30 @@ theorem foldr_paccStep_spec (L : List PVes) (h : ∀ P ∈ L, Valid P) : have hstep : (a :: xs).foldr paccStep (pid, pid) = paccStep a (xs.foldr paccStep (pid, pid)) := rfl rw [hstep] - have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd hv1 ha - refine ⟨hv1', valid_padd hv2 hv1', ?_⟩ + have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd Vesta.no_onCurve_y_zero hv1 ha + refine ⟨hv1', valid_padd Vesta.no_onCurve_y_zero hv2 hv1', ?_⟩ rw [List.map_cons, List.foldr_cons, ← heq, Msm.accStep] - simp only [paccStep, toAffine_padd hv1 ha, toAffine_padd hv2 hv1'] + simp only [paccStep, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hv1 ha, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hv2 hv1'] /-! ## Projective window value, mirroring `Fast.Msm.windowValue` -/ /-- The digit-tagged projective term list for window `i`. -/ -def pdpOf (base i : ℕ) (pterms : List (ℕ × PVes)) : List (ℕ × PVes) := +def pdpOf (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : List (ℕ × PVes Fq) := pterms.map fun t => (Msm.digit base i t.1, t.2) /-- The projective window value: build the `base − 1` projective buckets, then run the projective suffix-sum accumulation. -/ -def pwindowValue (base i : ℕ) (pterms : List (ℕ × PVes)) : PVes := +def pwindowValue (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : PVes Fq := (List.foldr paccStep (pid, pid) ((List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1))).2 /-- The projective window value is valid and matches `Fast.Msm.windowValue` of the `toAffine`-mapped terms. -/ -theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes)) +theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValue base i pterms) - ∧ toAffine (pwindowValue base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := by + ∧ toAffine Vesta.curve rfl rfl (pwindowValue base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by intro p hp rw [pdpOf, List.mem_map] at hp @@ -142,9 +142,9 @@ theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes)) exact (pbucketOf_spec _ _ hdp).1 obtain ⟨_, hv2, heq⟩ := foldr_paccStep_spec buckets hbval refine ⟨hv2, ?_⟩ - have hmap : buckets.map toAffine + have hmap : buckets.map (toAffine Vesta.curve rfl rfl) = (List.range (base - 1)).map fun k => - Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine t.2))) (k + 1) := by + Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2))) (k + 1) := by rw [hbuck, List.map_map] apply List.map_congr_left intro k _ @@ -157,16 +157,16 @@ theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes)) /-- Horner across windows in projective coordinates: each `base •` doubling is the fast binary scalar multiplication `pnsmulFast base`, and the window value is folded in with `padd`. -/ -def phornerList (base : ℕ) (vals : List PVes) : PVes := +def phornerList (base : ℕ) (vals : List (PVes Fq)) : PVes Fq := List.foldr (fun v acc => padd (pnsmulFast base acc) v) pid vals /-- The projective Horner fold is valid and matches `Fast.Msm.hornerList` of the `toAffine`-mapped window values; each `2^c`-fold doubling transports via `pnsmulFast_spec`. -/ -theorem phornerList_spec (base : ℕ) (vals : List PVes) (h : ∀ P ∈ vals, Valid P) : +theorem phornerList_spec (base : ℕ) (vals : List (PVes Fq)) (h : ∀ P ∈ vals, Valid P) : Valid (phornerList base vals) - ∧ toAffine (phornerList base vals) = Msm.hornerList base (vals.map toAffine) := by + ∧ toAffine Vesta.curve rfl rfl (phornerList base vals) = Msm.hornerList base (vals.map (toAffine Vesta.curve rfl rfl)) := by induction vals with - | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList, toAffine_pid]⟩ + | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList, toAffine_pid Vesta.curve rfl rfl]⟩ | cons v xs ih => have hv : Valid v := h v (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -174,8 +174,8 @@ theorem phornerList_spec (base : ℕ) (vals : List PVes) (h : ∀ P ∈ vals, Va have hstep : phornerList base (v :: xs) = padd (pnsmulFast base (phornerList base xs)) v := rfl rw [hstep] - refine ⟨valid_padd (pnsmulFast_spec hvacc base).1 hv, ?_⟩ - rw [toAffine_padd (pnsmulFast_spec hvacc base).1 hv, (pnsmulFast_spec hvacc base).2, heq, + refine ⟨valid_padd Vesta.no_onCurve_y_zero (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).1 hv, ?_⟩ + rw [toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).1 hv, (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).2, heq, List.map_cons] simp only [Msm.hornerList, List.foldr_cons] @@ -186,9 +186,9 @@ theorem phornerList_spec (base : ℕ) (vals : List PVes) (h : ∀ P ∈ vals, Va `PVes` with `padd`/`pnsmulFast`; a single `toAffine` (one field inversion) is taken at the end. Proven equal to the affine `Fast.Msm.pippenger` (`pippengerProj_eq`). -/ def pippengerProj (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) + toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2)))) + pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2)))) /-- **The projective Pippenger equals the affine Pippenger.** Lifting by `ofAffine` and reading back by `toAffine` is the identity on terms (`toAffine_ofAffine`); each window and the Horner fold commute @@ -197,20 +197,20 @@ to the affine `Fast.Msm.pippenger`. -/ theorem pippengerProj_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : pippengerProj c terms = Msm.pippenger c terms := by rw [pippengerProj] - set pterms := terms.map (fun t => (t.1, ofAffine t.2)) with hpterms + set pterms := terms.map (fun t => (t.1, ofAffine Vesta.curve t.2)) with hpterms set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValue (2 ^ c) i pterms with hwin have hval : ∀ p ∈ pterms, Valid p.2 := by intro p hp rw [hpterms, List.mem_map] at hp obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine t.2 - have hf : pterms.map (fun t => (t.1, toAffine t.2)) = terms := by + exact valid_ofAffine Vesta.curve rfl rfl t.2 + have hf : pterms.map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) = terms := by rw [hpterms, List.map_map] conv_rhs => rw [← List.map_id terms] apply List.map_congr_left intro t _ - simp only [Function.comp_apply, toAffine_ofAffine, id_eq] + simp only [Function.comp_apply, toAffine_ofAffine Vesta.curve rfl rfl, id_eq] have hwval : ∀ P ∈ windows, Valid P := by intro P hP rw [hwin, List.mem_map] at hP @@ -237,18 +237,18 @@ nose), so it too is transported through `toAffine` (`foldl_pscatterStep_spec`). /-- One projective scatter step: drop digit-`0` terms, otherwise `padd` the point into bucket slot `d − 1` (slot `k` holds bucket `k + 1`). -/ -def pscatterStep (a : Array PVes) (p : ℕ × PVes) : Array PVes := +def pscatterStep (a : Array (PVes Fq)) (p : ℕ × PVes Fq) : Array (PVes Fq) := if p.1 = 0 then a else a.modify (p.1 - 1) (fun v => padd v p.2) /-- Scatter a digit-tagged projective point list into its `base − 1` buckets in one pass. -/ -def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes)) : Array PVes := +def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes Fq)) : Array (PVes Fq) := dp.foldl pscatterStep (Array.replicate (base - 1) pid) -@[simp] theorem size_pscatterStep (a : Array PVes) (p : ℕ × PVes) : +@[simp] theorem size_pscatterStep (a : Array (PVes Fq)) (p : ℕ × PVes Fq) : (pscatterStep a p).size = a.size := by unfold pscatterStep; split <;> simp -@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PVes)) (a : Array PVes) : +@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PVes Fq)) (a : Array (PVes Fq)) : (dp.foldl pscatterStep a).size = a.size := by induction dp generalizing a with | nil => rfl @@ -256,7 +256,7 @@ def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes)) : Array PVes := /-- A single projective scatter step through `getElem?`: slot `k` gains a right-`padd` of `x` exactly when the digit is `k + 1`. -/ -theorem getElem?_pscatterStep (a : Array PVes) (d : ℕ) (x : PVes) (k : ℕ) : +theorem getElem?_pscatterStep (a : Array (PVes Fq)) (d : ℕ) (x : PVes Fq) (k : ℕ) : (pscatterStep a (d, x))[k]? = if d = k + 1 then a[k]?.map (fun v => padd v x) else a[k]? := by unfold pscatterStep @@ -271,11 +271,11 @@ theorem getElem?_pscatterStep (a : Array PVes) (d : ℕ) (x : PVes) (k : ℕ) : /-- **The scatter fold invariant, transported through `toAffine`.** Starting from a valid slot value `v`, slot `k` ends valid and reads — in `G` — as `toAffine v` plus the affine bucket sum of the processed digit-tagged list. -/ -private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes)) (hdp : ∀ p ∈ dp, Valid p.2) : - ∀ (a : Array PVes) (k : ℕ) (v : PVes), a[k]? = some v → Valid v → +private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes Fq)) (hdp : ∀ p ∈ dp, Valid p.2) : + ∀ (a : Array (PVes Fq)) (k : ℕ) (v : PVes Fq), a[k]? = some v → Valid v → ∃ w, (dp.foldl pscatterStep a)[k]? = some w ∧ Valid w ∧ - toAffine w = toAffine v - + Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by + toAffine Vesta.curve rfl rfl w = toAffine Vesta.curve rfl rfl v + + Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by induction dp with | nil => intro a k v hv hval @@ -290,9 +290,9 @@ private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes)) (hdp : ∀ p · have hv' : (pscatterStep a (d, x))[k]? = some (padd v x) := by rw [getElem?_pscatterStep, if_pos hdk, hv, Option.map_some] obtain ⟨w, hw, hwval, hweq⟩ := - ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd hval hx) + ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd Vesta.no_onCurve_y_zero hval hx) refine ⟨w, hw, hwval, ?_⟩ - rw [hweq, toAffine_padd hval hx, List.map_cons, Msm.bucketOf_cons, if_pos hdk, _root_.add_assoc] + rw [hweq, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hval hx, List.map_cons, Msm.bucketOf_cons, if_pos hdk, _root_.add_assoc] · have hv' : (pscatterStep a (d, x))[k]? = some v := by rw [getElem?_pscatterStep, if_neg hdk, hv] obtain ⟨w, hw, hwval, hweq⟩ := ih hdp' (pscatterStep a (d, x)) k v hv' hval @@ -301,22 +301,22 @@ private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes)) (hdp : ∀ p /-- **The scattered buckets are the affine bucket list, slotwise.** Every slot is valid, and `toAffine` maps the slot list to exactly the bucket list `Msm.windowValue` folds over. -/ -theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes)) (hdp : ∀ p ∈ dp, Valid p.2) : +theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes Fq)) (hdp : ∀ p ∈ dp, Valid p.2) : (∀ P ∈ (pbucketScatter base dp).toList, Valid P) - ∧ (pbucketScatter base dp).toList.map toAffine + ∧ (pbucketScatter base dp).toList.map (toAffine Vesta.curve rfl rfl) = (List.range (base - 1)).map fun k => - Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by + Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by have hsize : (pbucketScatter base dp).size = base - 1 := by rw [pbucketScatter, size_foldl_pscatterStep, Array.size_replicate] have hslot : ∀ k, k < base - 1 → ∃ w, (pbucketScatter base dp)[k]? = some w ∧ Valid w ∧ - toAffine w = Msm.bucketOf (dp.map fun t => (t.1, toAffine t.2)) (k + 1) := by + toAffine Vesta.curve rfl rfl w = Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by intro k hk - have hinit : (Array.replicate (base - 1) pid)[k]? = some pid := by + have hinit : (Array.replicate (base - 1) (pid : PVes Fq))[k]? = some pid := by rw [Array.getElem?_replicate, if_pos hk] obtain ⟨w, hw, hwval, hweq⟩ := foldl_pscatterStep_spec dp hdp (Array.replicate (base - 1) pid) k pid hinit valid_pid - exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid, _root_.zero_add]⟩ + exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid Vesta.curve rfl rfl, _root_.zero_add]⟩ constructor · intro P hP obtain ⟨k, hk, hPk⟩ := List.mem_iff_getElem.mp hP @@ -341,24 +341,24 @@ theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes)) (hdp : ∀ p /-- The projective window value via the single-pass scatter (mirror of `Msm.windowValueFast`). -/ -def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PVes)) : PVes := +def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : PVes Fq := (List.foldr paccStep (pid, pid) (pbucketScatter base (pdpOf base i pterms)).toList).2 /-- The scatter-bucketed projective window value is valid and matches `Msm.windowValue` of the `toAffine`-mapped terms — the scatter twin of `pwindowValue_spec`. -/ -theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes)) +theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValueFast base i pterms) - ∧ toAffine (pwindowValueFast base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine t.2)) := by + ∧ toAffine Vesta.curve rfl rfl (pwindowValueFast base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by intro p hp rw [pdpOf, List.mem_map] at hp obtain ⟨t, ht, rfl⟩ := hp exact h t ht obtain ⟨hbval, hbmap⟩ := pbucketScatter_spec base (pdpOf base i pterms) hdp - have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine t.2)) - = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine t.2)) := by + have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) + = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] rw [hdpof] at hbmap obtain ⟨-, hv2, heq⟩ := foldr_paccStep_spec _ hbval @@ -372,16 +372,16 @@ theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes)) the fast serial form of `pippengerProj`. Proven equal to the affine `Msm.pippenger` (`pippengerProjScatter_eq`). -/ def pippengerProjScatter (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) + toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2)))) + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2)))) /-- **The scatter-bucketed projective Pippenger equals the affine Pippenger** — same transport as `pippengerProj_eq`, window values via `pwindowValueFast_spec`. -/ theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : pippengerProjScatter c terms = Msm.pippenger c terms := by rw [pippengerProjScatter] - set pterms := terms.map (fun t => (t.1, ofAffine t.2)) with hpterms + set pterms := terms.map (fun t => (t.1, ofAffine Vesta.curve t.2)) with hpterms set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValueFast (2 ^ c) i pterms with hwin @@ -389,13 +389,13 @@ theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : intro p hp rw [hpterms, List.mem_map] at hp obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine t.2 - have hf : pterms.map (fun t => (t.1, toAffine t.2)) = terms := by + exact valid_ofAffine Vesta.curve rfl rfl t.2 + have hf : pterms.map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) = terms := by rw [hpterms, List.map_map] conv_rhs => rw [← List.map_id terms] apply List.map_congr_left intro t _ - simp only [Function.comp_apply, toAffine_ofAffine, id_eq] + simp only [Function.comp_apply, toAffine_ofAffine Vesta.curve rfl rfl, id_eq] have hwval : ∀ P ∈ windows, Valid P := by intro P hP rw [hwin, List.mem_map] at hP @@ -423,9 +423,9 @@ port. -/ /-- **Windows-parallel scatter-bucketed projective Pippenger**: `pippengerProjScatter` with the window values evaluated as parallel tasks. -/ def pippengerProjScatterPar (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine (phornerList (2 ^ c) + toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) (Msm.parMap (fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine t.2))) + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2))) (List.range (Msm.numWindows c terms)))) /-- The windows-parallel projective Pippenger is the sequential one: `parMap` is `map`. -/ diff --git a/CompElliptic/Curves/Pasta/Fast/Projective.lean b/CompElliptic/Curves/Pasta/Fast/Projective.lean index 5d00624..b473882 100644 --- a/CompElliptic/Curves/Pasta/Fast/Projective.lean +++ b/CompElliptic/Curves/Pasta/Fast/Projective.lean @@ -7,14 +7,22 @@ Authors: Gregor Mitscha-Baude import CompElliptic.Curves.Pasta /-! -# Projective (Renes–Costello–Batina) point arithmetic for Vesta +# Projective (Renes–Costello–Batina) point arithmetic for the Pasta curves The affine group law pays a field inversion per addition. This module replaces it, for the hot `n • point` loop, by the complete projective addition formulas of Renes, Costello and Batina (EUROCRYPT 2016; the EFD `add-2015-rcb` sequence at `a = 0`): single branchless formulas in `(X : Y : Z)` valid for *all* input pairs, with the inversion paid once in `toAffine`. Their -completeness needs the curve to have no 2-torsion, which Vesta's odd prime order gives -(`Vesta.no_onCurve_y_zero`); that is what discharges `Z₃ ≠ 0` outside the genuine identity cases. +completeness needs the curve to have no 2-torsion, which both Pasta curves' odd prime orders give +(`Vesta.no_onCurve_y_zero`, `Pallas.no_onCurve_y_zero`); that is what discharges `Z₃ ≠ 0` +outside the genuine identity cases. + +Everything is generic over the base field `F`: the `padd` closed forms and every polynomial +certificate are identities over `ℤ`, and the completeness arguments need only the no-2-torsion +fact, threaded as the hypothesis `hy0 : ∀ x, ¬ OnCurve 0 5 (x, 0)` (it forces `2 ≠ 0` and +`5 ≠ 0`). The bridge to the affine group `SWPoint E` takes the curve `E` pinned to `A = 0`, +`B = 5`. Each Pasta curve instantiates these by passing its `curve` and `no_onCurve_y_zero`; +Vesta additionally has `paddFast`, the raw-`ℕ` compiled spelling of `padd` at its modulus. Specialized to `a = 0`, `b = 5`, `b3 = 15`, the closed forms are @@ -38,17 +46,19 @@ abbrev Fq := CompElliptic.Fields.Pasta.VestaBaseField /-- The downstream affine group: on-curve points of Vesta with the complete affine group law. -/ abbrev G := SWPoint Vesta.curve -/-- A projective point in `(X : Y : Z)` coordinates over `𝔽_q`. -/ -structure PVes where - X : Fq - Y : Fq - Z : Fq +/-- A projective point in `(X : Y : Z)` coordinates over the base field `F`. -/ +structure PVes (F : Type*) where + X : F + Y : F + Z : F deriving DecidableEq namespace PVes +variable {F : Type*} [Field F] + /-- Renes–Costello–Batina complete addition (`add-2015-rcb`, `a = 0`, `b3 = 15`). -/ -def padd (P Q : PVes) : PVes where +def padd (P Q : PVes F) : PVes F where X := P.X*P.Y*Q.Y^2 - 15*P.X*P.Y*Q.Z^2 - 30*P.X*P.Z*Q.Y*Q.Z + P.Y^2*Q.X*Q.Y - 15*P.Z^2*Q.X*Q.Y - 30*P.Y*P.Z*Q.X*Q.Z Y := P.Y^2*Q.Y^2 + 45*P.X^2*Q.X*Q.Z + 45*P.X*P.Z*Q.X^2 - 225*P.Z^2*Q.Z^2 @@ -56,47 +66,58 @@ def padd (P Q : PVes) : PVes where + 15*P.Y*P.Z*Q.Z^2 + 15*P.Z^2*Q.Y*Q.Z /-- Scalar (representative) rescaling `(X : Y : Z) ↦ (uX : uY : uZ)`. -/ -def smul (u : Fq) (P : PVes) : PVes := ⟨u*P.X, u*P.Y, u*P.Z⟩ +def smul (u : F) (P : PVes F) : PVes F := ⟨u*P.X, u*P.Y, u*P.Z⟩ /-- The projective identity `𝒪 = (0 : 1 : 0)`. -/ -def pid : PVes := ⟨0, 1, 0⟩ +def pid : PVes F := ⟨0, 1, 0⟩ -/-- The homogeneous projective curve equation `Y²Z = X³ + 5Z³` (Vesta, `a = 0`, `b = 5`). -/ -def OnCurveP (P : PVes) : Prop := P.Y^2*P.Z = P.X^3 + 5*P.Z^3 +/-- The homogeneous projective curve equation `Y²Z = X³ + 5Z³` (`a = 0`, `b = 5`). -/ +def OnCurveP (P : PVes F) : Prop := P.Y^2*P.Z = P.X^3 + 5*P.Z^3 /-- `OnCurveP` unfolds definitionally to a field equation, hence is decidable. This is what keeps `toAffine` — and everything downstream of it, `smulFast` in particular — computable. -/ -instance (P : PVes) : Decidable (OnCurveP P) := +instance [DecidableEq F] (P : PVes F) : Decidable (OnCurveP P) := inferInstanceAs (Decidable (P.Y^2*P.Z = P.X^3 + 5*P.Z^3)) /-- A representable projective point: on the projective curve and not the zero vector. -/ -def Valid (P : PVes) : Prop := OnCurveP P ∧ (P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) +def Valid (P : PVes F) : Prop := OnCurveP P ∧ (P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) /-- Affine interpretation as a raw coordinate pair: `Z ≠ 0 ↦ (X/Z, Y/Z)`, `Z = 0 ↦ 𝒪 = (0,0)`. -/ -def aff (P : PVes) : Fq × Fq := if P.Z = 0 then (0, 0) else (P.X / P.Z, P.Y / P.Z) +def aff [DecidableEq F] (P : PVes F) : F × F := + if P.Z = 0 then (0, 0) else (P.X / P.Z, P.Y / P.Z) + +/-- No 2-torsion forces `2 ≠ 0`: in characteristic 2, `(1, 0)` would lie on the curve +(`1 + 5 = 6 = 0`). -/ +theorem two_ne_zero_of_no_y_zero (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) : (2 : F) ≠ 0 := + fun h => hy0 1 (by show (0 : F)^2 = 1^3 + 0*1 + 5; linear_combination (-3) * h) + +/-- No 2-torsion forces `5 ≠ 0`: otherwise `(0, 0)` would lie on the curve. -/ +theorem five_ne_zero_of_no_y_zero (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) : (5 : F) ≠ 0 := + fun h => hy0 0 (by show (0 : F)^2 = 0^3 + 0*0 + 5; rw [h]; ring) /-! ## `ring`/`linear_combination` certificates -Each identity below is a polynomial identity over `𝔽_q`, valid modulo the two curve equations +Each identity below is a polynomial identity over `F`, valid modulo the two curve equations `e1 : y1² = x1³ + 5` and `e2 : y2² = x2³ + 5`. The cofactors were computed by an exact-rational Gröbner/linear-algebra search over `ℚ[x1,y1,x2,y2]` (offline) and are checked here by `ring` -inside `linear_combination`. The `padd`-of-`Z=1`-points evaluation is spelled by `simp only [padd]` -which reduces the coordinate projections. -/ +inside `linear_combination`; being identities over `ℤ`, they hold over any field. The +`padd`-of-`Z=1`-points evaluation is spelled by `simp only [padd]` which reduces the coordinate +projections. -/ -variable {x1 y1 x2 y2 : Fq} +variable {x1 y1 x2 y2 : F} /-- Reading off the coordinates of `padd` on `Z = 1` representatives. -/ -@[simp] theorem padd_z1_X (x1 y1 x2 y2 : Fq) : +@[simp] theorem padd_z1_X (x1 y1 x2 y2 : F) : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).X = y1^2*x2*y2 + x1*y1*y2^2 - 15*x2*y2 - 30*y1*x2 - 30*x1*y2 - 15*x1*y1 := by simp only [padd]; ring -@[simp] theorem padd_z1_Y (x1 y1 x2 y2 : Fq) : +@[simp] theorem padd_z1_Y (x1 y1 x2 y2 : F) : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Y = y1^2*y2^2 + 45*x1*x2^2 + 45*x1^2*x2 - 225 := by simp only [padd]; ring -@[simp] theorem padd_z1_Z (x1 y1 x2 y2 : Fq) : +@[simp] theorem padd_z1_Z (x1 y1 x2 y2 : F) : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := by simp only [padd]; ring @@ -130,13 +151,14 @@ theorem oncurveP_padd_z1 (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) : /-- **Distinct-`x` completeness (2-torsion-free).** If `Z₃ = 0` for two on-curve `Z = 1` points with distinct `x`, then `w = wnum/wden` (the `x`-coordinate of `P − Q`) is a cube root of `−5`, -i.e. `(w, 0)` is a 2-torsion point — impossible on Vesta. Hence `Z₃ ≠ 0`. -/ -theorem Z_ne_zero_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) (hne : x1 ≠ x2) : +i.e. `(w, 0)` is a 2-torsion point — impossible by `hy0`. Hence `Z₃ ≠ 0`. -/ +theorem Z_ne_zero_dist (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) (hne : x1 ≠ x2) : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := by intro hZ have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) - set wnum : Fq := (y1 + y2)^2 - (x1 + x2)*(x2 - x1)^2 with hwnumE - set wden : Fq := (x2 - x1)^2 with hwdenE + set wnum : F := (y1 + y2)^2 - (x1 + x2)*(x2 - x1)^2 with hwnumE + set wden : F := (x2 - x1)^2 with hwdenE have hwdenne : wden ≠ 0 := by rw [hwdenE]; exact pow_ne_zero 2 hd have hZpoly : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z = 3*x1*y1*x2^2 + 3*x1^2*x2*y2 + y1*y2^2 + y1^2*y2 + 15*y2 + 15*y1 := padd_z1_Z x1 y1 x2 y2 @@ -151,9 +173,9 @@ theorem Z_ne_zero_dist (e1 : y1^2 = x1^3 + 5) (e2 : y2^2 = x2^3 + 5) (hne : x1 -- so (wnum/wden) is a cube root of -5, contradicting no 2-torsion have hw : (wnum / wden)^3 = -5 := by rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwdenne), mul_one] - exact Vesta.no_onCurve_y_zero (wnum / wden) (by - show (0 : Fq)^2 = (wnum / wden)^3 + Vesta.a * (wnum / wden) + Vesta.b - rw [hw]; simp [Vesta.a, Vesta.b]) + exact hy0 (wnum / wden) (by + show (0 : F)^2 = (wnum / wden)^3 + 0 * (wnum / wden) + 5 + rw [hw]; ring) /-- **Doubling `Z`-coordinate.** On `Z = 1` representatives with equal points, `Z₃ = 8y³`. -/ theorem Z_doubling (e1 : y1^2 = x1^3 + 5) : @@ -177,16 +199,19 @@ theorem keyy_dbl (e1 : y1^2 = x1^3 + 5) : /-- **Inverse-case identity representative is nonzero (2-torsion-free).** `padd P (−P) = (0 : Y₃ : 0)` with `Y₃ ≠ 0`: if `Y₃ = 0` then `w = wnum2/wden2` (the `x`-coordinate of `2P`) is a cube root of -`−5`, impossible on Vesta. -/ -theorem Y_ne_zero_inv (e1 : y1^2 = x1^3 + 5) (hy : y1 ≠ 0) : +`−5`, impossible by `hy0`. -/ +theorem Y_ne_zero_inv (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (e1 : y1^2 = x1^3 + 5) (hy : y1 ≠ 0) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y ≠ 0 := by intro hY have hYpoly : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Y = y1^4 + 90*x1^3 - 225 := by simp only [padd]; ring rw [hYpoly] at hY - set wnum2 : Fq := 9*x1^4 - 8*x1*y1^2 with hwnum2 - set wden2 : Fq := 4*y1^2 with hwden2E - have hwden2ne : wden2 ≠ 0 := by rw [hwden2E]; exact mul_ne_zero (by decide) (pow_ne_zero 2 hy) + set wnum2 : F := 9*x1^4 - 8*x1*y1^2 with hwnum2 + set wden2 : F := 4*y1^2 with hwden2E + have h4 : (4 : F) ≠ 0 := by + rw [show (4 : F) = 2^2 by norm_num]; exact pow_ne_zero 2 (two_ne_zero_of_no_y_zero hy0) + have hwden2ne : wden2 ≠ 0 := by rw [hwden2E]; exact mul_ne_zero h4 (pow_ne_zero 2 hy) have hcube : wnum2^3 = -5 * wden2^3 := by rw [hwnum2, hwden2E] linear_combination @@ -194,27 +219,28 @@ theorem Y_ne_zero_inv (e1 : y1^2 = x1^3 + 5) (hy : y1 ≠ 0) : + ((-729)*x1^9 + (1215)*x1^6*y1^2 + (-512)*x1^3*y1^4 + (3735)*x1^6 + (-2340)*x1^3*y1^2 + (320)*y1^4 + (-9900)*x1^3 + (1800)*y1^2 + (9000)) * e1 have hw : (wnum2 / wden2)^3 = -5 := by rw [div_pow, hcube, mul_div_assoc, div_self (pow_ne_zero 3 hwden2ne), mul_one] - exact Vesta.no_onCurve_y_zero (wnum2 / wden2) (by - show (0 : Fq)^2 = (wnum2 / wden2)^3 + Vesta.a * (wnum2 / wden2) + Vesta.b - rw [hw]; simp [Vesta.a, Vesta.b]) + exact hy0 (wnum2 / wden2) (by + show (0 : F)^2 = (wnum2 / wden2)^3 + 0 * (wnum2 / wden2) + 5 + rw [hw]; ring) /-- Inverse `X`-coordinate vanishes: `padd P (−P) = (0 : Y₃ : 0)` (pure identity). -/ -theorem X_zero_inv (x1 y1 : Fq) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).X = 0 := by +theorem X_zero_inv (x1 y1 : F) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).X = 0 := by simp only [padd]; ring /-- Inverse `Z`-coordinate vanishes (pure identity). -/ -theorem Z_zero_inv (x1 y1 : Fq) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := by +theorem Z_zero_inv (x1 y1 : F) : (padd ⟨x1, y1, 1⟩ ⟨x1, -y1, 1⟩).Z = 0 := by simp only [padd]; ring /-! ## Scaling (homogeneity) and affine interpretation -/ /-- `padd` is homogeneous of bidegree `(2,2)`: rescaling the inputs rescales the output. -/ -theorem smul_padd (u v : Fq) (P Q : PVes) : +theorem smul_padd (u v : F) (P Q : PVes F) : padd (smul u P) (smul v Q) = smul (u^2*v^2) (padd P Q) := by simp only [padd, smul, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring /-- `aff` is invariant under nonzero rescaling. -/ -theorem aff_smul (u : Fq) (hu : u ≠ 0) (P : PVes) : aff (smul u P) = aff P := by +theorem aff_smul [DecidableEq F] (u : F) (hu : u ≠ 0) (P : PVes F) : + aff (smul u P) = aff P := by rcases eq_or_ne P.Z 0 with h | h · simp [aff, smul, h] · have huz : u * P.Z ≠ 0 := mul_ne_zero hu h @@ -223,11 +249,11 @@ theorem aff_smul (u : Fq) (hu : u ≠ 0) (P : PVes) : aff (smul u P) = aff P := exact ⟨mul_div_mul_left _ _ hu, mul_div_mul_left _ _ hu⟩ /-- `OnCurveP` is preserved by rescaling. -/ -theorem oncurveP_smul (u : Fq) {P : PVes} (h : OnCurveP P) : OnCurveP (smul u P) := by +theorem oncurveP_smul (u : F) {P : PVes F} (h : OnCurveP P) : OnCurveP (smul u P) := by simp only [OnCurveP, smul] at h ⊢; linear_combination (u^3) * h /-- The nonzero-vector condition is preserved by nonzero rescaling. -/ -theorem nezVec_smul (u : Fq) (hu : u ≠ 0) {P : PVes} +theorem nezVec_smul (u : F) (hu : u ≠ 0) {P : PVes F} (h : P.X ≠ 0 ∨ P.Y ≠ 0 ∨ P.Z ≠ 0) : (smul u P).X ≠ 0 ∨ (smul u P).Y ≠ 0 ∨ (smul u P).Z ≠ 0 := by simp only [smul] @@ -236,11 +262,11 @@ theorem nezVec_smul (u : Fq) (hu : u ≠ 0) {P : PVes} · exact Or.inr (Or.inl (mul_ne_zero hu h)) · exact Or.inr (Or.inr (mul_ne_zero hu h)) -@[simp] theorem aff_z1 (x y : Fq) : aff ⟨x, y, 1⟩ = (x, y) := by +@[simp] theorem aff_z1 [DecidableEq F] (x y : F) : aff (⟨x, y, 1⟩ : PVes F) = (x, y) := by simp [aff] /-- `P = P.Z • (X/Z : Y/Z : 1)` when `Z ≠ 0`: every finite point is a rescaled `Z = 1` rep. -/ -theorem eq_smul_normalize {P : PVes} (h : P.Z ≠ 0) : +theorem eq_smul_normalize {P : PVes F} (h : P.Z ≠ 0) : P = smul P.Z ⟨P.X / P.Z, P.Y / P.Z, 1⟩ := by obtain ⟨X, Y, Z⟩ := P simp only [smul, PVes.mk.injEq] @@ -249,21 +275,23 @@ theorem eq_smul_normalize {P : PVes} (h : P.Z ≠ 0) : /-! ## Unfolding the affine group law on `Z = 1` reps -/ /-- `(x₁,y₁)` and `(x₂,y₂)` on the curve are `≠ 𝒪 = (0,0)`. -/ -theorem onCurve_ne_zero {x y : Fq} (h : OnCurve 0 5 (x, y)) : (x, y) ≠ ((0 : Fq), (0 : Fq)) := by +theorem onCurve_ne_zero (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {x y : F} + (h : OnCurve 0 5 (x, y)) : + (x, y) ≠ ((0 : F), (0 : F)) := by intro he rw [Prod.mk.injEq] at he obtain ⟨hx, hy⟩ := he; subst hx; subst hy - exact not_onCurve_zero (show (5 : Fq) ≠ 0 by decide) h + exact not_onCurve_zero (five_ne_zero_of_no_y_zero hy0) h /-- The affine sum in the distinct-`x` branch, with cleared denominators. -/ -theorem add_dist {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) - (hne : x1 ≠ x2) : +theorem add_dist [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {x1 y1 x2 y2 : F} + (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) (hne : x1 ≠ x2) : add 0 (x1, y1) (x2, y2) = (((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2) / (x2 - x1)^2, ((y2 - y1)*(x1*(x2 - x1)^2 - ((y2 - y1)^2 - (x1 + x2)*(x2 - x1)^2)) - y1*(x2 - x1)^3) / (x2 - x1)^3) := by - have hp0 := onCurve_ne_zero h1 - have hq0 := onCurve_ne_zero h2 + have hp0 := onCurve_ne_zero hy0 h1 + have hq0 := onCurve_ne_zero hy0 h2 have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) unfold add dsimp only @@ -272,15 +300,16 @@ theorem add_dist {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 constructor <;> field_simp <;> ring /-- The affine sum in the doubling branch (`a = 0`), with cleared denominators. -/ -theorem add_dbl {x1 y1 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (hy : y1 ≠ 0) : +theorem add_dbl [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {x1 y1 : F} + (h1 : OnCurve 0 5 (x1, y1)) (hy : y1 ≠ 0) : add 0 (x1, y1) (x1, y1) = ((9*x1^4 - 8*x1*y1^2) / (4*y1^2), (3*x1^2*(12*x1*y1^2 - 9*x1^4) - 8*y1^4) / (8*y1^3)) := by - have hp0 := onCurve_ne_zero h1 - have h2y : y1 + y1 ≠ 0 := by rw [← two_mul]; exact mul_ne_zero (by decide) hy - have h2 : (2 : Fq) ≠ 0 := by decide - have h4 : (4 : Fq) ≠ 0 := by decide - have h8 : (8 : Fq) ≠ 0 := by decide + have hp0 := onCurve_ne_zero hy0 h1 + have h2 : (2 : F) ≠ 0 := two_ne_zero_of_no_y_zero hy0 + have h2y : y1 + y1 ≠ 0 := by rw [← two_mul]; exact mul_ne_zero h2 hy + have h4 : (4 : F) ≠ 0 := by rw [show (4 : F) = 2^2 by norm_num]; exact pow_ne_zero 2 h2 + have h8 : (8 : F) ≠ 0 := by rw [show (8 : F) = 2^3 by norm_num]; exact pow_ne_zero 3 h2 unfold add dsimp only rw [if_neg hp0, if_neg hp0, if_pos rfl, if_neg h2y] @@ -291,14 +320,18 @@ theorem add_dbl {x1 y1 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (hy : y1 ≠ 0) : /-- **Core equivalence on `Z = 1` representatives.** For on-curve `(x₁,y₁),(x₂,y₂)`, the RCB projective sum interprets affinely as the complete affine sum, and stays a valid projective point. -/ -theorem padd_spec_z1 {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) : +theorem padd_spec_z1 [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {x1 y1 x2 y2 : F} + (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurve 0 5 (x2, y2)) : aff (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) = add 0 (x1, y1) (x2, y2) ∧ Valid (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := by have e1 : y1^2 = x1^3 + 5 := by have h := h1; simp only [OnCurve] at h; linear_combination h have e2 : y2^2 = x2^3 + 5 := by have h := h2; simp only [OnCurve] at h; linear_combination h have hoc : OnCurveP (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩) := oncurveP_padd_z1 e1 e2 have hy1 : y1 ≠ 0 := by - intro h; exact Vesta.no_onCurve_y_zero x1 (by rw [← h]; exact h1) + intro h; exact hy0 x1 (h ▸ h1) + have htwo : (2 : F) ≠ 0 := two_ne_zero_of_no_y_zero hy0 + have h4 : (4 : F) ≠ 0 := by rw [show (4 : F) = 2^2 by norm_num]; exact pow_ne_zero 2 htwo + have h8 : (8 : F) ≠ 0 := by rw [show (8 : F) = 2^3 by norm_num]; exact pow_ne_zero 3 htwo by_cases hx : x1 = x2 · subst hx by_cases hy : y1 + y2 = 0 @@ -311,7 +344,7 @@ theorem padd_spec_z1 {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurv have hnp : (x1, -y1) = CompElliptic.CurveForms.ShortWeierstrass.neg (x1, y1) := by simp [CompElliptic.CurveForms.ShortWeierstrass.neg] rw [hnp, CompElliptic.CurveForms.ShortWeierstrass.add_neg] - · exact Or.inr (Or.inl (Y_ne_zero_inv e1 hy1)) + · exact Or.inr (Or.inl (Y_ne_zero_inv hy0 e1 hy1)) · -- doubling: y1 = y2 have hyeq : y1 = y2 := by have hz : (y1 - y2) * (y1 + y2) = 0 := by linear_combination e1 - e2 @@ -321,22 +354,22 @@ theorem padd_spec_z1 {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurv subst hyeq have hZv : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z = 8 * y1^3 := Z_doubling e1 have hZne : (padd ⟨x1, y1, 1⟩ ⟨x1, y1, 1⟩).Z ≠ 0 := by - rw [hZv]; exact mul_ne_zero (by decide) (pow_ne_zero 3 hy1) - have hy2 : (4 : Fq) * y1^2 ≠ 0 := mul_ne_zero (by decide) (pow_ne_zero 2 hy1) - have hy3 : (8 : Fq) * y1^3 ≠ 0 := mul_ne_zero (by decide) (pow_ne_zero 3 hy1) + rw [hZv]; exact mul_ne_zero h8 (pow_ne_zero 3 hy1) + have hy2 : (4 : F) * y1^2 ≠ 0 := mul_ne_zero h4 (pow_ne_zero 2 hy1) + have hy3 : (8 : F) * y1^3 ≠ 0 := mul_ne_zero h8 (pow_ne_zero 3 hy1) refine ⟨?_, hoc, ?_⟩ - · rw [aff, if_neg hZne, add_dbl h1 hy1, Prod.mk.injEq] + · rw [aff, if_neg hZne, add_dbl hy0 h1 hy1, Prod.mk.injEq] refine ⟨?_, ?_⟩ · rw [div_eq_div_iff hZne hy2]; linear_combination keyx_dbl e1 · rw [div_eq_div_iff hZne hy3]; linear_combination keyy_dbl e1 · exact Or.inr (Or.inr hZne) · -- distinct x - have hZne : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := Z_ne_zero_dist e1 e2 hx + have hZne : (padd ⟨x1, y1, 1⟩ ⟨x2, y2, 1⟩).Z ≠ 0 := Z_ne_zero_dist hy0 e1 e2 hx have hd : x2 - x1 ≠ 0 := sub_ne_zero.mpr (Ne.symm hx) have hd2 : (x2 - x1)^2 ≠ 0 := pow_ne_zero 2 hd have hd3 : (x2 - x1)^3 ≠ 0 := pow_ne_zero 3 hd refine ⟨?_, hoc, ?_⟩ - · rw [aff, if_neg hZne, add_dist h1 h2 hx, Prod.mk.injEq] + · rw [aff, if_neg hZne, add_dist hy0 h1 h2 hx, Prod.mk.injEq] refine ⟨?_, ?_⟩ · rw [div_eq_div_iff hZne hd2]; linear_combination keyx_dist e1 e2 · rw [div_eq_div_iff hZne hd3]; linear_combination keyy_dist e1 e2 @@ -345,12 +378,13 @@ theorem padd_spec_z1 {x1 y1 x2 y2 : Fq} (h1 : OnCurve 0 5 (x1, y1)) (h2 : OnCurv /-! ## Structural facts about `Valid` points and the identity-input reductions -/ /-- A valid point with `Z = 0` has `X = 0` (only the identity is at infinity). -/ -theorem X_zero_of_Z_zero {P : PVes} (h : OnCurveP P) (hz : P.Z = 0) : P.X = 0 := by +theorem X_zero_of_Z_zero {P : PVes F} (h : OnCurveP P) (hz : P.Z = 0) : P.X = 0 := by have hX3 : P.X ^ 3 = 0 := by rw [OnCurveP, hz] at h; simpa using h.symm exact pow_eq_zero_iff (by norm_num : (3 : ℕ) ≠ 0) |>.mp hX3 /-- A valid point always has nonzero `Y` (no 2-torsion; the identity is `(0 : 1 : 0)`). -/ -theorem Valid.Y_ne_zero {P : PVes} (hP : Valid P) : P.Y ≠ 0 := by +theorem Valid.Y_ne_zero {P : PVes F} (hP : Valid P) (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) : + P.Y ≠ 0 := by rcases eq_or_ne P.Z 0 with hz | hz · have hX := X_zero_of_Z_zero hP.1 hz rcases hP.2 with h | h | h @@ -358,24 +392,24 @@ theorem Valid.Y_ne_zero {P : PVes} (hP : Valid P) : P.Y ≠ 0 := by · exact h · exact absurd hz h · intro hY - refine Vesta.no_onCurve_y_zero (P.X / P.Z) ?_ + refine hy0 (P.X / P.Z) ?_ have key : P.X^3 + 5 * P.Z^3 = 0 := by have h := hP.1; rw [OnCurveP, hY] at h; linear_combination -h - show (0 : Fq)^2 = (P.X / P.Z)^3 + Vesta.a * (P.X / P.Z) + Vesta.b - rw [Vesta.a, Vesta.b]; field_simp; linear_combination -key + show (0 : F)^2 = (P.X / P.Z)^3 + 0 * (P.X / P.Z) + 5 + field_simp; linear_combination -key /-- `padd` with the first argument an identity-type point `(0 : Y₁ : 0)` rescales the second. -/ -theorem padd_idL {P Q : PVes} (hX : P.X = 0) (hZ : P.Z = 0) : +theorem padd_idL {P Q : PVes F} (hX : P.X = 0) (hZ : P.Z = 0) : padd P Q = smul (P.Y^2 * Q.Y) Q := by simp only [padd, smul, hX, hZ, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring /-- `padd` with the second argument an identity-type point `(0 : Y₂ : 0)` rescales the first. -/ -theorem padd_idR {P Q : PVes} (hX : Q.X = 0) (hZ : Q.Z = 0) : +theorem padd_idR {P Q : PVes F} (hX : Q.X = 0) (hZ : Q.Z = 0) : padd P Q = smul (P.Y * Q.Y^2) P := by simp only [padd, smul, hX, hZ, PVes.mk.injEq]; refine ⟨?_, ?_, ?_⟩ <;> ring /-- On-curve reading of the normalized affine coordinates of a finite valid point. -/ -theorem onCurve_norm {P : PVes} (h : OnCurveP P) (hz : P.Z ≠ 0) : +theorem onCurve_norm {P : PVes F} (h : OnCurveP P) (hz : P.Z ≠ 0) : OnCurve 0 5 (P.X / P.Z, P.Y / P.Z) := by have key : P.Y^2 * P.Z = P.X^3 + 5 * P.Z^3 := h show (P.Y / P.Z)^2 = (P.X / P.Z)^3 + 0 * (P.X / P.Z) + 5 @@ -383,10 +417,11 @@ theorem onCurve_norm {P : PVes} (h : OnCurveP P) (hz : P.Z ≠ 0) : /-- **General equivalence.** For any two valid projective points, the RCB sum interprets affinely as the complete affine sum, and stays valid. -/ -theorem padd_spec {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : +theorem padd_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {P Q : PVes F} + (hP : Valid P) (hQ : Valid Q) : aff (padd P Q) = add 0 (aff P) (aff Q) ∧ Valid (padd P Q) := by - have hPY := hP.Y_ne_zero - have hQY := hQ.Y_ne_zero + have hPY := hP.Y_ne_zero hy0 + have hQY := hQ.Y_ne_zero hy0 by_cases hPz : P.Z = 0 · -- P is an identity-type point have hPX := X_zero_of_Z_zero hP.1 hPz @@ -404,7 +439,7 @@ theorem padd_spec {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : · -- both finite: normalize to `Z = 1` and use the core lemma have hP1 := onCurve_norm hP.1 hPz have hQ1 := onCurve_norm hQ.1 hQz - obtain ⟨haff, hvalid⟩ := padd_spec_z1 hP1 hQ1 + obtain ⟨haff, hvalid⟩ := padd_spec_z1 hy0 hP1 hQ1 have hu : P.Z^2 * Q.Z^2 ≠ 0 := mul_ne_zero (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz) have hpadd : padd P Q = smul (P.Z^2 * Q.Z^2) (padd ⟨P.X/P.Z, P.Y/P.Z, 1⟩ ⟨Q.X/Q.Z, Q.Y/Q.Z, 1⟩) := by conv_lhs => rw [eq_smul_normalize hPz, eq_smul_normalize hQz] @@ -417,82 +452,104 @@ theorem padd_spec {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : exact ⟨oncurveP_smul _ hvalid.1, nezVec_smul _ hu hvalid.2⟩ /-- Validity is preserved by `padd` (closure). -/ -theorem valid_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : Valid (padd P Q) := - (padd_spec hP hQ).2 +theorem valid_padd (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {P Q : PVes F} + (hP : Valid P) (hQ : Valid Q) : + Valid (padd P Q) := by + classical exact (padd_spec hy0 hP hQ).2 /-- `aff` is a homomorphism from `padd` to the affine group law on valid inputs. -/ -theorem aff_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : +theorem aff_padd [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) {P Q : PVes F} + (hP : Valid P) (hQ : Valid Q) : aff (padd P Q) = add 0 (aff P) (aff Q) := - (padd_spec hP hQ).1 + (padd_spec hy0 hP hQ).1 /-- The identity `(0 : 1 : 0)` is valid. -/ -theorem valid_pid : Valid pid := by +theorem valid_pid : Valid (pid : PVes F) := by refine ⟨?_, Or.inr (Or.inl one_ne_zero)⟩ simp [OnCurveP, pid] /-- `aff pid = 𝒪`. -/ -@[simp] theorem aff_pid : aff pid = ((0 : Fq), (0 : Fq)) := by simp [aff, pid] +@[simp] theorem aff_pid [DecidableEq F] : aff (pid : PVes F) = ((0 : F), (0 : F)) := by + simp [aff, pid] -/-! ## Bridge to the affine group `G = SWPoint Vesta.curve` -/ +/-! ## Bridge to the affine group `SWPoint E` of a curve `E` with `A = 0`, `B = 5` -/ + +section Bridge + +variable (E : SWCurve F) (hA : E.A = 0) (hB : E.B = 5) /-- Interpret a projective point as an element of the affine group: a finite on-curve point maps to `(X/Z, Y/Z)`, everything else (points at infinity, off-curve junk) to the identity `𝒪`. -/ -def toAffine (P : PVes) : G := +def toAffine [DecidableEq F] (P : PVes F) : SWPoint E := if h : OnCurveP P ∧ P.Z ≠ 0 then - ⟨P.X / P.Z, P.Y / P.Z, Or.inl (onCurve_norm h.1 h.2)⟩ + ⟨P.X / P.Z, P.Y / P.Z, Or.inl (by + rw [hA, hB] + exact onCurve_norm h.1 h.2)⟩ else 0 /-- On valid points, `toAffine` agrees coordinatewise with `aff`. -/ -theorem toAffine_coords {P : PVes} (hP : Valid P) : - ((toAffine P).x, (toAffine P).y) = aff P := by +theorem toAffine_coords [DecidableEq F] {P : PVes F} (hP : Valid P) : + ((toAffine E hA hB P).x, (toAffine E hA hB P).y) = aff P := by rcases eq_or_ne P.Z 0 with hz | hz - · have h0 : toAffine P = 0 := by rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h hz + · have h0 : toAffine E hA hB P = 0 := by rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h hz rw [h0, aff, if_pos hz]; rfl · rw [toAffine, dif_pos ⟨hP.1, hz⟩, aff, if_neg hz] -@[simp] theorem toAffine_pid : toAffine pid = 0 := by +@[simp] theorem toAffine_pid [DecidableEq F] : toAffine E hA hB (pid : PVes F) = 0 := by rw [toAffine, dif_neg]; rintro ⟨_, h⟩; exact h rfl /-- **The homomorphism.** `toAffine` carries the projective RCB addition to the affine group law. -/ -theorem toAffine_padd {P Q : PVes} (hP : Valid P) (hQ : Valid Q) : - toAffine (padd P Q) = toAffine P + toAffine Q := by +theorem toAffine_padd [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + {P Q : PVes F} (hP : Valid P) (hQ : Valid Q) : + toAffine E hA hB (padd P Q) = toAffine E hA hB P + toAffine E hA hB Q := by apply SWPoint.ext_pair - have hL : ((toAffine (padd P Q)).x, (toAffine (padd P Q)).y) = aff (padd P Q) := - toAffine_coords (valid_padd hP hQ) - have hRc : ((toAffine P + toAffine Q).x, (toAffine P + toAffine Q).y) - = add Vesta.curve.A ((toAffine P).x, (toAffine P).y) ((toAffine Q).x, (toAffine Q).y) := rfl - rw [hL, hRc, toAffine_coords hP, toAffine_coords hQ, aff_padd hP hQ] - rfl + have hL : ((toAffine E hA hB (padd P Q)).x, (toAffine E hA hB (padd P Q)).y) + = aff (padd P Q) := + toAffine_coords E hA hB (valid_padd hy0 hP hQ) + have hRc : ((toAffine E hA hB P + toAffine E hA hB Q).x, + (toAffine E hA hB P + toAffine E hA hB Q).y) + = add E.A ((toAffine E hA hB P).x, (toAffine E hA hB P).y) + ((toAffine E hA hB Q).x, (toAffine E hA hB Q).y) := rfl + rw [hL, hRc, toAffine_coords E hA hB hP, toAffine_coords E hA hB hQ, hA, + aff_padd hy0 hP hQ] /-- Materialize an affine group element as a projective representative: the identity as `(0 : 1 : 0)`, a finite point as `(x : y : 1)`. -/ -def ofAffine (p : G) : PVes := +def ofAffine [DecidableEq F] (p : SWPoint E) : PVes F := if p.x = 0 ∧ p.y = 0 then pid else ⟨p.x, p.y, 1⟩ -theorem valid_ofAffine (p : G) : Valid (ofAffine p) := by +include hA hB in +/-- A point of `E` reads as an on-curve pair of `y² = x³ + 5` unless it is `𝒪 = (0, 0)`. -/ +theorem onCurve_of_ne_zero (p : SWPoint E) (h : ¬ (p.x = 0 ∧ p.y = 0)) : + OnCurve 0 5 (p.x, p.y) := by + have hv := p.onCurve + rw [hA, hB] at hv + exact hv.resolve_right (by rw [Prod.mk.injEq]; exact h) + +include hA hB in +theorem valid_ofAffine [DecidableEq F] (p : SWPoint E) : Valid (ofAffine E p) := by rw [ofAffine] by_cases h : p.x = 0 ∧ p.y = 0 · rw [if_pos h]; exact valid_pid · rw [if_neg h] - have hoc : OnCurve 0 5 (p.x, p.y) := by - have hv := p.onCurve - exact hv.resolve_right (by rw [Prod.mk.injEq]; exact h) + have hoc : OnCurve 0 5 (p.x, p.y) := onCurve_of_ne_zero E hA hB p h have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this refine ⟨?_, Or.inr (Or.inr one_ne_zero)⟩ simp only [OnCurveP]; linear_combination e -theorem toAffine_ofAffine (p : G) : toAffine (ofAffine p) = p := by +theorem toAffine_ofAffine [DecidableEq F] (p : SWPoint E) : + toAffine E hA hB (ofAffine E p) = p := by rw [ofAffine] by_cases h : p.x = 0 ∧ p.y = 0 · rw [if_pos h, toAffine_pid] apply SWPoint.ext_pair obtain ⟨hx, hy⟩ := h - show ((0 : G).x, (0 : G).y) = (p.x, p.y) + show ((0 : SWPoint E).x, (0 : SWPoint E).y) = (p.x, p.y) rw [hx, hy]; rfl · rw [if_neg h] - have hoc : OnCurve 0 5 (p.x, p.y) := p.onCurve.resolve_right (by rw [Prod.mk.injEq]; exact h) - have hZ : ((⟨p.x, p.y, 1⟩ : PVes)).Z ≠ 0 := one_ne_zero - have hocp : OnCurveP (⟨p.x, p.y, 1⟩ : PVes) := by + have hoc : OnCurve 0 5 (p.x, p.y) := onCurve_of_ne_zero E hA hB p h + have hZ : ((⟨p.x, p.y, 1⟩ : PVes F)).Z ≠ 0 := one_ne_zero + have hocp : OnCurveP (⟨p.x, p.y, 1⟩ : PVes F) := by have e : p.y^2 = p.x^3 + 5 := by have := hoc; simp only [OnCurve] at this; linear_combination this simp only [OnCurveP]; linear_combination e apply SWPoint.ext_pair @@ -504,13 +561,14 @@ theorem toAffine_ofAffine (p : G) : toAffine (ofAffine p) = p := by /-- Binary double-and-add scalar multiplication over `PVes` using the RCB `padd`, matching the `CompElliptic.binNsmul` recurrence used by the affine group's `nsmul`. -/ -def pnsmulFast (n : ℕ) (P : PVes) : PVes := binNsmul padd pid n P +def pnsmulFast (n : ℕ) (P : PVes F) : PVes F := binNsmul padd pid n P /-- **Fast scalar multiplication is the genuine group action.** By strong induction along the `binNsmul` double-and-add recurrence: each intermediate stays valid (`valid_padd`) and `toAffine` is a homomorphism (`toAffine_padd`), so the projective ladder computes `n • (toAffine P)`. -/ -theorem pnsmulFast_spec {P : PVes} (hP : Valid P) : ∀ n : ℕ, - Valid (pnsmulFast n P) ∧ toAffine (pnsmulFast n P) = n • toAffine P := by +theorem pnsmulFast_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + {P : PVes F} (hP : Valid P) : ∀ n : ℕ, + Valid (pnsmulFast n P) ∧ toAffine E hA hB (pnsmulFast n P) = n • toAffine E hA hB P := by intro n induction n using Nat.strong_induction_on with | _ n ih => @@ -523,29 +581,35 @@ theorem pnsmulFast_spec {P : PVes} (hP : Valid P) : ∀ n : ℕ, obtain ⟨hvq, hq⟩ := ih (n / 2) hlt rw [pnsmulFast] at hvq hq set q := binNsmul padd pid (n / 2) P with hqdef - have hvd : Valid (padd q q) := valid_padd hvq hvq - have hdaff : toAffine (padd q q) = (n / 2) • toAffine P + (n / 2) • toAffine P := by - rw [toAffine_padd hvq hvq, hq] - have key : n • toAffine P - = (n / 2) • toAffine P + (n / 2) • toAffine P + (n % 2) • toAffine P := by + have hvd : Valid (padd q q) := valid_padd hy0 hvq hvq + have hdaff : toAffine E hA hB (padd q q) + = (n / 2) • toAffine E hA hB P + (n / 2) • toAffine E hA hB P := by + rw [toAffine_padd E hA hB hy0 hvq hvq, hq] + have key : n • toAffine E hA hB P + = (n / 2) • toAffine E hA hB P + (n / 2) • toAffine E hA hB P + + (n % 2) • toAffine E hA hB P := by rw [← add_nsmul, ← add_nsmul]; congr 1; omega split · rename_i hodd - refine ⟨valid_padd hvd hP, ?_⟩ - rw [toAffine_padd hvd hP, hdaff, key, hodd, one_nsmul] + refine ⟨valid_padd hy0 hvd hP, ?_⟩ + rw [toAffine_padd E hA hB hy0 hvd hP, hdaff, key, hodd, one_nsmul] · rename_i heven refine ⟨hvd, ?_⟩ rw [hdaff, key, show n % 2 = 0 from by omega, zero_nsmul, _root_.add_zero] -/-- The packaged fast scalar multiplication on `G`, going through projective coordinates. -/ -def smulFast (n : ℕ) (p : G) : G := toAffine (pnsmulFast n (ofAffine p)) +/-- The packaged fast scalar multiplication on `SWPoint E`, going through projective coordinates. -/ +def smulFast [DecidableEq F] (n : ℕ) (p : SWPoint E) : SWPoint E := + toAffine E hA hB (pnsmulFast n (ofAffine E p)) /-- **Correctness of `smulFast`:** it equals the affine scalar multiplication `n • p`, with the field inversion paid once (in the final `toAffine`) instead of once per addition. -/ -theorem smulFast_eq (n : ℕ) (p : G) : smulFast n p = n • p := by - rw [smulFast, (pnsmulFast_spec (valid_ofAffine p) n).2, toAffine_ofAffine] +theorem smulFast_eq [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) (n : ℕ) + (p : SWPoint E) : smulFast E hA hB n p = n • p := by + rw [smulFast, (pnsmulFast_spec E hA hB hy0 (valid_ofAffine E hA hB p) n).2, toAffine_ofAffine] + +end Bridge -/-! ## Fast compiled spelling of `padd` (compiled-tier only) +/-! ## Fast compiled spelling of `padd` (compiled-tier only; Vesta) Compiled generically, every field operation in `padd` goes through boxed `CommRing (ZMod q)` dictionary projections. `paddFast` is the same closed forms over raw `ℕ` representatives with @@ -586,7 +650,7 @@ private theorem cast_val (a : Fq) : ((ZMod.val a : ℕ) : Fq) = a := /-- `padd` over raw `ℕ` representatives: same RCB closed forms, fused mul-mod, shared subproducts. Statement-surface code should keep calling `padd`; the compiler substitutes this body via `padd_eq_paddFast`. -/ -def paddFast (P Q : PVes) : PVes := +def paddFast (P Q : PVes Fq) : PVes Fq := let x1 := P.X.val; let y1 := P.Y.val; let z1 := P.Z.val let x2 := Q.X.val; let y2 := Q.Y.val; let z2 := Q.Z.val let y2sq := fmul y2 y2 @@ -623,7 +687,7 @@ makes interpreted Montgomery a 40× regression). The equality is kept for the co tier: once the fast-field lib ships precompiled (`precompileModules` dylib), registering this `@[csimp]` (or the Montgomery successor) makes every compiled call site (including `native_decide` auxiliaries) run the fused raw-`ℕ` form. -/ -theorem padd_eq_paddFast : @padd = @paddFast := by +theorem padd_eq_paddFast : (padd : PVes Fq → PVes Fq → PVes Fq) = paddFast := by funext P Q simp only [padd, paddFast, PVes.mk.injEq] refine ⟨?_, ?_, ?_⟩ <;> diff --git a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean index 6586478..705ad8a 100644 --- a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean +++ b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean @@ -152,13 +152,13 @@ theorem montVal_c225 : montVal PM.c225 = 225 := by /-! ## The point level -/ /-- Coordinatewise interpretation of a Montgomery triple as a projective point over `𝔽_q`. -/ -def toPVesM (p : PM) : PVes := ⟨montVal p.X, montVal p.Y, montVal p.Z⟩ +def toPVesM (p : PM) : PVes Fq := ⟨montVal p.X, montVal p.Y, montVal p.Z⟩ /-- All three coordinates are well-formed Montgomery residues. -/ def WFP (p : PM) : Prop := WF p.X ∧ WF p.Y ∧ WF p.Z /-- The affine reading of a Montgomery triple. -/ -def toGM (p : PM) : G := toAffine (toPVesM p) +def toGM (p : PM) : G := toAffine Vesta.curve rfl rfl (toPVesM p) @[simp] theorem toPVesM_X (p : PM) : (toPVesM p).X = montVal p.X := rfl @[simp] theorem toPVesM_Y (p : PM) : (toPVesM p).Y = montVal p.Y := rfl @@ -228,15 +228,17 @@ def WV (p : PM) : Prop := WFP p ∧ Valid (toPVesM p) theorem WV_pid : WV PM.pid := ⟨wfp_pid, by rw [toPVesM_pid]; exact valid_pid⟩ theorem WV_padd {p r : PM} (hp : WV p) (hr : WV r) : WV (PM.padd p r) := - ⟨wfp_padd hp.1 hr.1, by rw [toPVesM_padd hp.1 hr.1]; exact valid_padd hp.2 hr.2⟩ + ⟨wfp_padd hp.1 hr.1, by + rw [toPVesM_padd hp.1 hr.1]; exact valid_padd Vesta.no_onCurve_y_zero hp.2 hr.2⟩ -@[simp] theorem toGM_pid : toGM PM.pid = 0 := by rw [toGM, toPVesM_pid, toAffine_pid] +@[simp] theorem toGM_pid : toGM PM.pid = 0 := by + rw [toGM, toPVesM_pid, toAffine_pid Vesta.curve rfl rfl] /-- **The kernel's addition is the affine group addition** on representable points. -/ theorem toGM_padd {p r : PM} (hp : WV p) (hr : WV r) : toGM (PM.padd p r) = toGM p + toGM r := by simp only [toGM] - rw [toPVesM_padd hp.1 hr.1, toAffine_padd hp.2 hr.2] + rw [toPVesM_padd hp.1 hr.1, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hp.2 hr.2] /-! ## The correspondence with the projective statement surface @@ -245,27 +247,28 @@ shared schedule preserves it. -/ /-- The kernel correspondence: a well-formed Montgomery triple denoting a given projective point. -/ -def RM (p : PM) (P : PVes) : Prop := WFP p ∧ toPVesM p = P +def RM (p : PM) (P : PVes Fq) : Prop := WFP p ∧ toPVesM p = P /-- The correspondence on ladder/downsweep state pairs. -/ -def RM2 (s : PM × PM) (s' : PVes × PVes) : Prop := RM s.1 s'.1 ∧ RM s.2 s'.2 +def RM2 (s : PM × PM) (s' : PVes Fq × PVes Fq) : Prop := RM s.1 s'.1 ∧ RM s.2 s'.2 theorem RM_self {p : PM} (h : WFP p) : RM p (toPVesM p) := ⟨h, rfl⟩ -theorem RM_toG {p : PM} {P : PVes} (h : RM p P) : toGM p = toAffine P := by rw [toGM, h.2] +theorem RM_toG {p : PM} {P : PVes Fq} (h : RM p P) : toGM p = toAffine Vesta.curve rfl rfl P := by + rw [toGM, h.2] /-- A corresponding pair inherits representability from the projective side. -/ -theorem RM_valid {p : PM} {P : PVes} (h : RM p P) (hv : Valid P) : WV p := +theorem RM_valid {p : PM} {P : PVes Fq} (h : RM p P) (hv : Valid P) : WV p := ⟨h.1, by rw [h.2]; exact hv⟩ -theorem RM_padd {p r : PM} {P Q : PVes} (hp : RM p P) (hr : RM r Q) : +theorem RM_padd {p r : PM} {P Q : PVes Fq} (hp : RM p P) (hr : RM r Q) : RM (PM.padd p r) (PVes.padd P Q) := by refine ⟨wfp_padd hp.1 hr.1, ?_⟩ rw [toPVesM_padd hp.1 hr.1, hp.2, hr.2] theorem RM_pid : RM PM.pid PVes.pid := ⟨wfp_pid, toPVesM_pid⟩ -theorem RM_pneg {p : PM} {P : PVes} (h : RM p P) : +theorem RM_pneg {p : PM} {P : PVes Fq} (h : RM p P) : RM (PM.pneg p) ⟨P.X, -P.Y, P.Z⟩ := by refine ⟨wfp_pneg h.1, ?_⟩ rw [toPVesM_pneg h.1, h.2] @@ -336,7 +339,8 @@ private theorem ladderM_step {A : G} {n i : ℕ} {st : PM × PM} (h : LadderInvM (all Pasta scalars). Statement shape mirrors `PVes.pnsmulFast_spec`. -/ theorem pnsmulM_spec {p : PM} (hwf : WFP p) (hp : Valid (toPVesM p)) (n : ℕ) (hn : n < 2 ^ 256) : WFP (PM.pnsmul n p) ∧ Valid (toPVesM (PM.pnsmul n p)) ∧ - toAffine (toPVesM (PM.pnsmul n p)) = n • toAffine (toPVesM p) := by + toAffine Vesta.curve rfl rfl (toPVesM (PM.pnsmul n p)) + = n • toAffine Vesta.curve rfl rfl (toPVesM p) := by have base : ∀ m : ℕ, m ≤ 256 → LadderInvM (toGM p) n m ((List.range m).foldl (fun (st : PM × PM) i => @@ -420,16 +424,16 @@ private theorem forall₂_map_self {α β : Type} {R : α → β → Prop} {P : /-- `Array.get!`/`set!` need a default on the `PVes` side as well as on `PM`'s; the projective identity is the right one on both, so an out-of-range read stays a corresponding pair. -/ -instance : Inhabited PVes := ⟨PVes.pid⟩ +instance : Inhabited (PVes Fq) := ⟨PVes.pid⟩ /-- The array-level correspondence: cellwise `RM`. -/ -def RA (a : Array PM) (b : Array PVes) : Prop := List.Forall₂ RM a.toList b.toList +def RA (a : Array PM) (b : Array (PVes Fq)) : Prop := List.Forall₂ RM a.toList b.toList -theorem RA.size {a : Array PM} {b : Array PVes} (h : RA a b) : a.size = b.size := by +theorem RA.size {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) : a.size = b.size := by have := List.Forall₂.length_eq h rwa [Array.length_toList, Array.length_toList] at this -theorem RA.get {a : Array PM} {b : Array PVes} (h : RA a b) (k : ℕ) : RM a[k]! b[k]! := by +theorem RA.get {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) (k : ℕ) : RM a[k]! b[k]! := by by_cases hk : k < a.size · have hk' : k < b.size := h.size ▸ hk rw [getElem!_pos a k hk, getElem!_pos b k hk'] @@ -439,20 +443,21 @@ theorem RA.get {a : Array PM} {b : Array PVes} (h : RA a b) (k : ℕ) : RM a[k]! rw [getElem!_neg a k hk, getElem!_neg b k hk'] exact RM_pid -theorem RA.set {a : Array PM} {b : Array PVes} (h : RA a b) (k : ℕ) {p : PM} {P : PVes} +theorem RA.set {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) (k : ℕ) {p : PM} {P : PVes Fq} (hp : RM p P) : RA (a.set! k p) (b.set! k P) := by simp only [RA, Array.set!_eq_setIfInBounds, Array.toList_setIfInBounds] exact forall₂_set hp h k -theorem RA.modify {a : Array PM} {b : Array PVes} (h : RA a b) (k : ℕ) - {f : PM → PM} {g : PVes → PVes} (hfg : ∀ p P, RM p P → RM (f p) (g P)) : +theorem RA.modify {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) (k : ℕ) + {f : PM → PM} {g : PVes Fq → PVes Fq} (hfg : ∀ p P, RM p P → RM (f p) (g P)) : RA (a.modify k f) (b.modify k g) := by simp only [RA, Array.toList_modify] exact forall₂_modify hfg h k -theorem RA.map_toG {a : Array PM} {b : Array PVes} (h : RA a b) : - a.map toGM = b.map toAffine := by - have := forall₂_map_eq (f := toGM) (g := toAffine) (fun _ _ hr => RM_toG hr) h +theorem RA.map_toG {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) : + a.map toGM = b.map (toAffine Vesta.curve rfl rfl) := by + have := forall₂_map_eq (f := toGM) (g := toAffine Vesta.curve rfl rfl) + (fun _ _ hr => RM_toG hr) h rw [← Array.toList_map, ← Array.toList_map] at this exact Array.toList_inj.mp this @@ -469,7 +474,7 @@ instead of `pnsmulFast (2 ^ c)`), so it goes through `toGM` directly, and `hornerList_windows_eq_msm` reconciles the kernel's fixed `⌈256 / c⌉` windows with `Msm.numWindows`. -/ -private theorem RA_scatterStep {a : Array PM} {b : Array PVes} (h : RA a b) {t : ℕ × PM} +private theorem RA_scatterStep {a : Array PM} {b : Array (PVes Fq)} (h : RA a b) {t : ℕ × PM} (ht : WFP t.2) : RA (PM.scatterStep a t) (MsmProj.pscatterStep b (t.1, toPVesM t.2)) := by simp only [PM.scatterStep, MsmProj.pscatterStep] @@ -489,7 +494,7 @@ private theorem RA_bucketScatter (base : ℕ) (dp : List (ℕ × PM)) (h : ∀ t exact forall₂_replicate RM_pid _ private theorem RM2_foldr_accStep : - ∀ {L : List PM} {L' : List PVes}, List.Forall₂ RM L L' → + ∀ {L : List PM} {L' : List (PVes Fq)}, List.Forall₂ RM L L' → RM2 (L.foldr PM.accStep (PM.pid, PM.pid)) (L'.foldr MsmProj.paccStep (PVes.pid, PVes.pid)) := by intro L L' h @@ -583,17 +588,17 @@ mirrors `MsmProj.pippengerProjScatter_eq`. -/ theorem msmM_spec (c : ℕ) (hc : 0 < c) (terms : List (ℕ × PM)) (hwf : ∀ t ∈ terms, WFP t.2) (hv : ∀ t ∈ terms, Valid (toPVesM t.2)) (hn : ∀ t ∈ terms, t.1 < 2 ^ 256) : - toAffine (toPVesM (PM.msm c terms)) - = Msm.pippenger c (terms.map fun t => (t.1, toAffine (toPVesM t.2))) := by + toAffine Vesta.curve rfl rfl (toPVesM (PM.msm c terms)) + = Msm.pippenger c (terms.map fun t => (t.1, toAffine Vesta.curve rfl rfl (toPVesM t.2))) := by set W := (256 + c - 1) / c with hWdef set pterms := terms.map fun t => (t.1, toPVesM t.2) with hpterms - set aterms := terms.map fun t => (t.1, toAffine (toPVesM t.2)) with haterms + set aterms := terms.map fun t => (t.1, toAffine Vesta.curve rfl rfl (toPVesM t.2)) with haterms have hptv : ∀ p ∈ pterms, Valid p.2 := by intro p hp rw [hpterms, List.mem_map] at hp obtain ⟨t, ht, rfl⟩ := hp exact hv t ht - have hmapaff : pterms.map (fun t => (t.1, toAffine t.2)) = aterms := by + have hmapaff : pterms.map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) = aterms := by rw [hpterms, haterms, List.map_map] rfl -- each window value: well formed, representable, and affinely the `Msm` window value From dccd396e0bf14a815e657f034dfc70a15f1ccec9 Mon Sep 17 00:00:00 2001 From: Martin Allen Date: Thu, 10 Sep 2026 09:22:09 -0700 Subject: [PATCH 2/2] Fast/MsmProj: generalize the projective Pippenger MSM over the base field Every definition and lemma is stated in place, under its original name, over `PVes F` and a curve `E` with `E.A = 0`, `E.B = 5`, threading the no-2-torsion hypothesis `hy0` through the `_spec` lemmas exactly as `Projective.lean` does. The `commit_lagrange` wrappers stay Vesta-specific and pass `Vesta.curve rfl rfl` / `Vesta.no_onCurve_y_zero`; `ProjectiveMontEquiv` passes the same facts at its one `pwindowValueFast_spec` call. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01TUVBzWdyPZ8AWYoGVYADs6 --- CompElliptic/Curves/Pasta/Fast/MsmProj.lean | 250 ++++++++++-------- .../Pasta/Fast/ProjectiveMontEquiv.lean | 3 +- 2 files changed, 141 insertions(+), 112 deletions(-) diff --git a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean index 768e8f7..eaf6791 100644 --- a/CompElliptic/Curves/Pasta/Fast/MsmProj.lean +++ b/CompElliptic/Curves/Pasta/Fast/MsmProj.lean @@ -10,7 +10,7 @@ import CompElliptic.Curves.Pasta.Fast.Projective /-! # The windowed Pippenger MSM run entirely in projective coordinates -Instantiated at the Vesta affine group, every group addition of `Msm.lean` pays a field inversion. +Instantiated at a curve's affine group, every group addition of `Msm.lean` pays a field inversion. This module runs the whole Pippenger interior over `Projective.PVes` with `padd`/`pnsmulFast` — one inversion per MSM instead of one per add — and proves the result equal to the affine accelerator (`pippengerProj_eq`, `pippengerProjScatter_eq`, and `..._eq_msm` to the naive MSM). @@ -20,6 +20,10 @@ Pippenger equality is not re-run here: each fold of `Msm.lean` is mirrored by a version and shown to commute with `toAffine`, carrying `Valid` through every intermediate (`psum_spec`, `pbucketOf_spec`, `foldr_paccStep_spec`, `pwindowValue_spec`, `phornerList_spec`). +Everything is generic over the base field `F` and a curve `E` with `E.A = 0`, `E.B = 5`, with the +no-2-torsion hypothesis `hy0` threaded exactly as in `Projective.lean`; only the `commit_lagrange` +wrappers at the end are Vesta-specific (their coefficients live in `VestaScalarField`). + The `Fast` interfaces are provisional: they are not guaranteed to remain public, and may be folded into the existing API or otherwise changed incompatibly. -/ @@ -34,6 +38,9 @@ open CompElliptic.Curves.Pasta namespace CompElliptic.Curves.Pasta.Fast.MsmProj +variable {F : Type*} [Field F] +variable (E : SWCurve F) (hA : E.A = 0) (hB : E.B = 5) + /-- The Vesta affine group carries a default point, needed to instantiate the `Fast.Msm` wrapper (`commitLagrangeSpec`, `commitLagrangeFastWith_eq`) whose section fixes `[Inhabited G]`. -/ local instance : Inhabited Projective.G := ⟨0⟩ @@ -41,32 +48,35 @@ local instance : Inhabited Projective.G := ⟨0⟩ /-! ## Projective bucket sum (`foldr padd pid`), mirroring `Fast.Msm.bucketOf` -/ /-- The `padd`-fold sum of a list of projective points, from the projective identity `pid`. -/ -def psum (L : List (PVes Fq)) : PVes Fq := L.foldr padd pid +def psum (L : List (PVes F)) : PVes F := L.foldr padd pid -theorem psum_cons (a : PVes Fq) (xs : List (PVes Fq)) : psum (a :: xs) = padd a (psum xs) := rfl +theorem psum_cons (a : PVes F) (xs : List (PVes F)) : psum (a :: xs) = padd a (psum xs) := rfl /-- A projective `padd`-sum of valid points is valid, and `toAffine` carries it to the affine sum. -/ -theorem psum_spec (L : List (PVes Fq)) (h : ∀ P ∈ L, Valid P) : - Valid (psum L) ∧ toAffine Vesta.curve rfl rfl (psum L) = (L.map (toAffine Vesta.curve rfl rfl)).sum := by +theorem psum_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (L : List (PVes F)) (h : ∀ P ∈ L, Valid P) : + Valid (psum L) ∧ toAffine E hA hB (psum L) = (L.map (toAffine E hA hB)).sum := by induction L with - | nil => exact ⟨valid_pid, by simp [psum, toAffine_pid Vesta.curve rfl rfl]⟩ + | nil => exact ⟨valid_pid, by simp [psum, toAffine_pid]⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) obtain ⟨hvxs, hxseq⟩ := ih hxs rw [psum_cons] - exact ⟨valid_padd Vesta.no_onCurve_y_zero ha hvxs, by rw [toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ + exact ⟨valid_padd hy0 ha hvxs, by + rw [toAffine_padd E hA hB hy0 ha hvxs, hxseq, List.map_cons, List.sum_cons]⟩ /-- The projective bucket-`b` sum: `padd`-fold the points whose digit tag is `b`. -/ -def pbucketOf (dp : List (ℕ × PVes Fq)) (b : ℕ) : PVes Fq := +def pbucketOf (dp : List (ℕ × PVes F)) (b : ℕ) : PVes F := psum (dp.filterMap fun p => if p.1 = b then some p.2 else none) /-- The projective bucket sum is valid and matches `Fast.Msm.bucketOf` of the `toAffine`-mapped digit-tagged list. -/ -theorem pbucketOf_spec (dp : List (ℕ × PVes Fq)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : +theorem pbucketOf_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (dp : List (ℕ × PVes F)) (b : ℕ) (h : ∀ p ∈ dp, Valid p.2) : Valid (pbucketOf dp b) - ∧ toAffine Vesta.curve rfl rfl (pbucketOf dp b) - = Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) b := by + ∧ toAffine E hA hB (pbucketOf dp b) + = Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) b := by have hval : ∀ P ∈ dp.filterMap (fun p => if p.1 = b then some p.2 else none), Valid P := by intro P hP rw [List.mem_filterMap] at hP @@ -74,7 +84,7 @@ theorem pbucketOf_spec (dp : List (ℕ × PVes Fq)) (b : ℕ) (h : ∀ p ∈ dp, by_cases hc : q.1 = b · rw [if_pos hc, Option.some.injEq] at hqeq; rw [← hqeq]; exact h q hq · rw [if_neg hc] at hqeq; exact absurd hqeq (by simp) - obtain ⟨hv, heq⟩ := psum_spec _ hval + obtain ⟨hv, heq⟩ := psum_spec E hA hB hy0 _ hval refine ⟨hv, ?_⟩ rw [pbucketOf, heq, Msm.bucketOf, List.filterMap_map, List.map_filterMap] refine congrArg List.sum (congrArg (dp.filterMap ·) ?_) @@ -85,17 +95,20 @@ theorem pbucketOf_spec (dp : List (ℕ × PVes Fq)) (b : ℕ) (h : ∀ p ∈ dp, /-- One step of the projective suffix-sum accumulator: carry `(running, total)`, `padd` the next bucket into `running`, then `padd` `running` into `total`. -/ -def paccStep (a : PVes Fq) (p : PVes Fq × PVes Fq) : PVes Fq × PVes Fq := +def paccStep (a : PVes F) (p : PVes F × PVes F) : PVes F × PVes F := (padd p.1 a, padd p.2 (padd p.1 a)) /-- Folding `paccStep` over valid points keeps both accumulator components valid, and `toAffine` carries the whole fold (componentwise) to the affine `Fast.Msm.accStep` fold. -/ -theorem foldr_paccStep_spec (L : List (PVes Fq)) (h : ∀ P ∈ L, Valid P) : +theorem foldr_paccStep_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (L : List (PVes F)) (h : ∀ P ∈ L, Valid P) : Valid (L.foldr paccStep (pid, pid)).1 ∧ Valid (L.foldr paccStep (pid, pid)).2 - ∧ (toAffine Vesta.curve rfl rfl (L.foldr paccStep (pid, pid)).1, toAffine Vesta.curve rfl rfl (L.foldr paccStep (pid, pid)).2) - = List.foldr Msm.accStep ((0 : Projective.G), (0 : Projective.G)) (L.map (toAffine Vesta.curve rfl rfl)) := by + ∧ (toAffine E hA hB (L.foldr paccStep (pid, pid)).1, + toAffine E hA hB (L.foldr paccStep (pid, pid)).2) + = List.foldr Msm.accStep ((0 : SWPoint E), (0 : SWPoint E)) + (L.map (toAffine E hA hB)) := by induction L with - | nil => exact ⟨valid_pid, valid_pid, by simp [toAffine_pid Vesta.curve rfl rfl]⟩ + | nil => exact ⟨valid_pid, valid_pid, by simp [toAffine_pid]⟩ | cons a xs ih => have ha : Valid a := h a (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -103,30 +116,30 @@ theorem foldr_paccStep_spec (L : List (PVes Fq)) (h : ∀ P ∈ L, Valid P) : have hstep : (a :: xs).foldr paccStep (pid, pid) = paccStep a (xs.foldr paccStep (pid, pid)) := rfl rw [hstep] - have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd Vesta.no_onCurve_y_zero hv1 ha - refine ⟨hv1', valid_padd Vesta.no_onCurve_y_zero hv2 hv1', ?_⟩ + have hv1' : Valid (padd (xs.foldr paccStep (pid, pid)).1 a) := valid_padd hy0 hv1 ha + refine ⟨hv1', valid_padd hy0 hv2 hv1', ?_⟩ rw [List.map_cons, List.foldr_cons, ← heq, Msm.accStep] - simp only [paccStep, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hv1 ha, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hv2 hv1'] + simp only [paccStep, toAffine_padd E hA hB hy0 hv1 ha, toAffine_padd E hA hB hy0 hv2 hv1'] /-! ## Projective window value, mirroring `Fast.Msm.windowValue` -/ /-- The digit-tagged projective term list for window `i`. -/ -def pdpOf (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : List (ℕ × PVes Fq) := +def pdpOf (base i : ℕ) (pterms : List (ℕ × PVes F)) : List (ℕ × PVes F) := pterms.map fun t => (Msm.digit base i t.1, t.2) /-- The projective window value: build the `base − 1` projective buckets, then run the projective suffix-sum accumulation. -/ -def pwindowValue (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : PVes Fq := +def pwindowValue (base i : ℕ) (pterms : List (ℕ × PVes F)) : PVes F := (List.foldr paccStep (pid, pid) ((List.range (base - 1)).map fun k => pbucketOf (pdpOf base i pterms) (k + 1))).2 /-- The projective window value is valid and matches `Fast.Msm.windowValue` of the `toAffine`-mapped terms. -/ -theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) - (h : ∀ p ∈ pterms, Valid p.2) : +theorem pwindowValue_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (base i : ℕ) (pterms : List (ℕ × PVes F)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValue base i pterms) - ∧ toAffine Vesta.curve rfl rfl (pwindowValue base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by + ∧ toAffine E hA hB (pwindowValue base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by intro p hp rw [pdpOf, List.mem_map] at hp @@ -139,16 +152,17 @@ theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) intro P hP rw [hbuck, List.mem_map] at hP obtain ⟨k, _, rfl⟩ := hP - exact (pbucketOf_spec _ _ hdp).1 - obtain ⟨_, hv2, heq⟩ := foldr_paccStep_spec buckets hbval + exact (pbucketOf_spec E hA hB hy0 _ _ hdp).1 + obtain ⟨_, hv2, heq⟩ := foldr_paccStep_spec E hA hB hy0 buckets hbval refine ⟨hv2, ?_⟩ - have hmap : buckets.map (toAffine Vesta.curve rfl rfl) + have hmap : buckets.map (toAffine E hA hB) = (List.range (base - 1)).map fun k => - Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2))) (k + 1) := by + Msm.bucketOf (Msm.dpOf base i (pterms.map fun t => (t.1, toAffine E hA hB t.2))) + (k + 1) := by rw [hbuck, List.map_map] apply List.map_congr_left intro k _ - rw [Function.comp_apply, (pbucketOf_spec _ _ hdp).2] + rw [Function.comp_apply, (pbucketOf_spec E hA hB hy0 _ _ hdp).2] congr 1 simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] rw [Msm.windowValue, ← hmap, ← heq] @@ -157,16 +171,18 @@ theorem pwindowValue_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) /-- Horner across windows in projective coordinates: each `base •` doubling is the fast binary scalar multiplication `pnsmulFast base`, and the window value is folded in with `padd`. -/ -def phornerList (base : ℕ) (vals : List (PVes Fq)) : PVes Fq := +def phornerList (base : ℕ) (vals : List (PVes F)) : PVes F := List.foldr (fun v acc => padd (pnsmulFast base acc) v) pid vals /-- The projective Horner fold is valid and matches `Fast.Msm.hornerList` of the `toAffine`-mapped window values; each `2^c`-fold doubling transports via `pnsmulFast_spec`. -/ -theorem phornerList_spec (base : ℕ) (vals : List (PVes Fq)) (h : ∀ P ∈ vals, Valid P) : +theorem phornerList_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (base : ℕ) (vals : List (PVes F)) (h : ∀ P ∈ vals, Valid P) : Valid (phornerList base vals) - ∧ toAffine Vesta.curve rfl rfl (phornerList base vals) = Msm.hornerList base (vals.map (toAffine Vesta.curve rfl rfl)) := by + ∧ toAffine E hA hB (phornerList base vals) + = Msm.hornerList base (vals.map (toAffine E hA hB)) := by induction vals with - | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList, toAffine_pid Vesta.curve rfl rfl]⟩ + | nil => exact ⟨valid_pid, by simp [phornerList, Msm.hornerList, toAffine_pid]⟩ | cons v xs ih => have hv : Valid v := h v (by simp) have hxs : ∀ P ∈ xs, Valid P := fun P hP => h P (by simp [hP]) @@ -174,9 +190,9 @@ theorem phornerList_spec (base : ℕ) (vals : List (PVes Fq)) (h : ∀ P ∈ val have hstep : phornerList base (v :: xs) = padd (pnsmulFast base (phornerList base xs)) v := rfl rw [hstep] - refine ⟨valid_padd Vesta.no_onCurve_y_zero (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).1 hv, ?_⟩ - rw [toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).1 hv, (pnsmulFast_spec Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hvacc base).2, heq, - List.map_cons] + have hacc := pnsmulFast_spec E hA hB hy0 hvacc base + refine ⟨valid_padd hy0 hacc.1 hv, ?_⟩ + rw [toAffine_padd E hA hB hy0 hacc.1 hv, hacc.2, heq, List.map_cons] simp only [Msm.hornerList, List.foldr_cons] /-! ## The projective Pippenger MSM and its equality to the affine accelerator -/ @@ -185,48 +201,50 @@ theorem phornerList_spec (base : ℕ) (vals : List (PVes Fq)) (h : ∀ P ∈ val `ofAffine`; the same windowed algorithm (digits, buckets, suffix-sum, Horner doublings) runs over `PVes` with `padd`/`pnsmulFast`; a single `toAffine` (one field inversion) is taken at the end. Proven equal to the affine `Fast.Msm.pippenger` (`pippengerProj_eq`). -/ -def pippengerProj (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) +def pippengerProj [DecidableEq F] (c : ℕ) (terms : List (ℕ × SWPoint E)) : SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2)))) + pwindowValue (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2)))) /-- **The projective Pippenger equals the affine Pippenger.** Lifting by `ofAffine` and reading back by `toAffine` is the identity on terms (`toAffine_ofAffine`); each window and the Horner fold commute with `toAffine` (`pwindowValue_spec`, `phornerList_spec`), so the whole projective interior collapses to the affine `Fast.Msm.pippenger`. -/ -theorem pippengerProj_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProj c terms = Msm.pippenger c terms := by +theorem pippengerProj_eq [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProj E hA hB c terms = Msm.pippenger c terms := by rw [pippengerProj] - set pterms := terms.map (fun t => (t.1, ofAffine Vesta.curve t.2)) with hpterms + set pterms := terms.map (fun t => (t.1, ofAffine E t.2)) with hpterms set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValue (2 ^ c) i pterms with hwin have hval : ∀ p ∈ pterms, Valid p.2 := by intro p hp rw [hpterms, List.mem_map] at hp obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine Vesta.curve rfl rfl t.2 - have hf : pterms.map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) = terms := by + exact valid_ofAffine E hA hB t.2 + have hf : pterms.map (fun t => (t.1, toAffine E hA hB t.2)) = terms := by rw [hpterms, List.map_map] conv_rhs => rw [← List.map_id terms] apply List.map_congr_left intro t _ - simp only [Function.comp_apply, toAffine_ofAffine Vesta.curve rfl rfl, id_eq] + simp only [Function.comp_apply, toAffine_ofAffine, id_eq] have hwval : ∀ P ∈ windows, Valid P := by intro P hP rw [hwin, List.mem_map] at hP obtain ⟨i, _, rfl⟩ := hP - exact (pwindowValue_spec (2 ^ c) i pterms hval).1 - rw [(phornerList_spec (2 ^ c) windows hwval).2, Msm.pippenger] + exact (pwindowValue_spec E hA hB hy0 (2 ^ c) i pterms hval).1 + rw [(phornerList_spec E hA hB hy0 (2 ^ c) windows hwval).2, Msm.pippenger] congr 1 rw [hwin, List.map_map] apply List.map_congr_left intro i _ - rw [Function.comp_apply, (pwindowValue_spec (2 ^ c) i pterms hval).2, hf] + rw [Function.comp_apply, (pwindowValue_spec E hA hB hy0 (2 ^ c) i pterms hval).2, hf] /-- **The projective Pippenger equals the naive MSM.** End-to-end correctness for `c ≥ 1`. -/ -theorem pippengerProj_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : - pippengerProj c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProj_eq, Msm.pippenger_eq_msm c hc] +theorem pippengerProj_eq_msm [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProj E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProj_eq E hA hB hy0, Msm.pippenger_eq_msm c hc] /-! ## Single-pass Array bucketing for the projective interior @@ -237,18 +255,18 @@ nose), so it too is transported through `toAffine` (`foldl_pscatterStep_spec`). /-- One projective scatter step: drop digit-`0` terms, otherwise `padd` the point into bucket slot `d − 1` (slot `k` holds bucket `k + 1`). -/ -def pscatterStep (a : Array (PVes Fq)) (p : ℕ × PVes Fq) : Array (PVes Fq) := +def pscatterStep (a : Array (PVes F)) (p : ℕ × PVes F) : Array (PVes F) := if p.1 = 0 then a else a.modify (p.1 - 1) (fun v => padd v p.2) /-- Scatter a digit-tagged projective point list into its `base − 1` buckets in one pass. -/ -def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes Fq)) : Array (PVes Fq) := +def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes F)) : Array (PVes F) := dp.foldl pscatterStep (Array.replicate (base - 1) pid) -@[simp] theorem size_pscatterStep (a : Array (PVes Fq)) (p : ℕ × PVes Fq) : +@[simp] theorem size_pscatterStep (a : Array (PVes F)) (p : ℕ × PVes F) : (pscatterStep a p).size = a.size := by unfold pscatterStep; split <;> simp -@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PVes Fq)) (a : Array (PVes Fq)) : +@[simp] theorem size_foldl_pscatterStep (dp : List (ℕ × PVes F)) (a : Array (PVes F)) : (dp.foldl pscatterStep a).size = a.size := by induction dp generalizing a with | nil => rfl @@ -256,7 +274,7 @@ def pbucketScatter (base : ℕ) (dp : List (ℕ × PVes Fq)) : Array (PVes Fq) : /-- A single projective scatter step through `getElem?`: slot `k` gains a right-`padd` of `x` exactly when the digit is `k + 1`. -/ -theorem getElem?_pscatterStep (a : Array (PVes Fq)) (d : ℕ) (x : PVes Fq) (k : ℕ) : +theorem getElem?_pscatterStep (a : Array (PVes F)) (d : ℕ) (x : PVes F) (k : ℕ) : (pscatterStep a (d, x))[k]? = if d = k + 1 then a[k]?.map (fun v => padd v x) else a[k]? := by unfold pscatterStep @@ -269,13 +287,14 @@ theorem getElem?_pscatterStep (a : Array (PVes Fq)) (d : ℕ) (x : PVes Fq) (k : · rw [if_neg (by omega), if_neg hdk] /-- **The scatter fold invariant, transported through `toAffine`.** Starting from a valid slot -value `v`, slot `k` ends valid and reads — in `G` — as `toAffine v` plus the affine bucket sum -of the processed digit-tagged list. -/ -private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes Fq)) (hdp : ∀ p ∈ dp, Valid p.2) : - ∀ (a : Array (PVes Fq)) (k : ℕ) (v : PVes Fq), a[k]? = some v → Valid v → +value `v`, slot `k` ends valid and reads — in `SWPoint E` — as `toAffine v` plus the affine +bucket sum of the processed digit-tagged list. -/ +private theorem foldl_pscatterStep_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (dp : List (ℕ × PVes F)) (hdp : ∀ p ∈ dp, Valid p.2) : + ∀ (a : Array (PVes F)) (k : ℕ) (v : PVes F), a[k]? = some v → Valid v → ∃ w, (dp.foldl pscatterStep a)[k]? = some w ∧ Valid w ∧ - toAffine Vesta.curve rfl rfl w = toAffine Vesta.curve rfl rfl v - + Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by + toAffine E hA hB w = toAffine E hA hB v + + Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by induction dp with | nil => intro a k v hv hval @@ -290,9 +309,10 @@ private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes Fq)) (hdp : ∀ · have hv' : (pscatterStep a (d, x))[k]? = some (padd v x) := by rw [getElem?_pscatterStep, if_pos hdk, hv, Option.map_some] obtain ⟨w, hw, hwval, hweq⟩ := - ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd Vesta.no_onCurve_y_zero hval hx) + ih hdp' (pscatterStep a (d, x)) k (padd v x) hv' (valid_padd hy0 hval hx) refine ⟨w, hw, hwval, ?_⟩ - rw [hweq, toAffine_padd Vesta.curve rfl rfl Vesta.no_onCurve_y_zero hval hx, List.map_cons, Msm.bucketOf_cons, if_pos hdk, _root_.add_assoc] + rw [hweq, toAffine_padd E hA hB hy0 hval hx, List.map_cons, Msm.bucketOf_cons, if_pos hdk, + _root_.add_assoc] · have hv' : (pscatterStep a (d, x))[k]? = some v := by rw [getElem?_pscatterStep, if_neg hdk, hv] obtain ⟨w, hw, hwval, hweq⟩ := ih hdp' (pscatterStep a (d, x)) k v hv' hval @@ -301,22 +321,25 @@ private theorem foldl_pscatterStep_spec (dp : List (ℕ × PVes Fq)) (hdp : ∀ /-- **The scattered buckets are the affine bucket list, slotwise.** Every slot is valid, and `toAffine` maps the slot list to exactly the bucket list `Msm.windowValue` folds over. -/ -theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes Fq)) (hdp : ∀ p ∈ dp, Valid p.2) : +theorem pbucketScatter_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (base : ℕ) (dp : List (ℕ × PVes F)) (hdp : ∀ p ∈ dp, Valid p.2) : (∀ P ∈ (pbucketScatter base dp).toList, Valid P) - ∧ (pbucketScatter base dp).toList.map (toAffine Vesta.curve rfl rfl) + ∧ (pbucketScatter base dp).toList.map (toAffine E hA hB) = (List.range (base - 1)).map fun k => - Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by + Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by have hsize : (pbucketScatter base dp).size = base - 1 := by rw [pbucketScatter, size_foldl_pscatterStep, Array.size_replicate] have hslot : ∀ k, k < base - 1 → ∃ w, (pbucketScatter base dp)[k]? = some w ∧ Valid w ∧ - toAffine Vesta.curve rfl rfl w = Msm.bucketOf (dp.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) (k + 1) := by + toAffine E hA hB w + = Msm.bucketOf (dp.map fun t => (t.1, toAffine E hA hB t.2)) (k + 1) := by intro k hk - have hinit : (Array.replicate (base - 1) (pid : PVes Fq))[k]? = some pid := by + have hinit : (Array.replicate (base - 1) (pid : PVes F))[k]? = some pid := by rw [Array.getElem?_replicate, if_pos hk] obtain ⟨w, hw, hwval, hweq⟩ := - foldl_pscatterStep_spec dp hdp (Array.replicate (base - 1) pid) k pid hinit valid_pid - exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid Vesta.curve rfl rfl, _root_.zero_add]⟩ + foldl_pscatterStep_spec E hA hB hy0 dp hdp (Array.replicate (base - 1) pid) k pid hinit + valid_pid + exact ⟨w, hw, hwval, by rw [hweq, toAffine_pid, _root_.zero_add]⟩ constructor · intro P hP obtain ⟨k, hk, hPk⟩ := List.mem_iff_getElem.mp hP @@ -341,27 +364,27 @@ theorem pbucketScatter_spec (base : ℕ) (dp : List (ℕ × PVes Fq)) (hdp : ∀ /-- The projective window value via the single-pass scatter (mirror of `Msm.windowValueFast`). -/ -def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PVes Fq)) : PVes Fq := +def pwindowValueFast (base i : ℕ) (pterms : List (ℕ × PVes F)) : PVes F := (List.foldr paccStep (pid, pid) (pbucketScatter base (pdpOf base i pterms)).toList).2 /-- The scatter-bucketed projective window value is valid and matches `Msm.windowValue` of the `toAffine`-mapped terms — the scatter twin of `pwindowValue_spec`. -/ -theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) - (h : ∀ p ∈ pterms, Valid p.2) : +theorem pwindowValueFast_spec [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (base i : ℕ) (pterms : List (ℕ × PVes F)) (h : ∀ p ∈ pterms, Valid p.2) : Valid (pwindowValueFast base i pterms) - ∧ toAffine Vesta.curve rfl rfl (pwindowValueFast base i pterms) - = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by + ∧ toAffine E hA hB (pwindowValueFast base i pterms) + = Msm.windowValue base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by have hdp : ∀ p ∈ pdpOf base i pterms, Valid p.2 := by intro p hp rw [pdpOf, List.mem_map] at hp obtain ⟨t, ht, rfl⟩ := hp exact h t ht - obtain ⟨hbval, hbmap⟩ := pbucketScatter_spec base (pdpOf base i pterms) hdp - have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) - = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) := by + obtain ⟨hbval, hbmap⟩ := pbucketScatter_spec E hA hB hy0 base (pdpOf base i pterms) hdp + have hdpof : (pdpOf base i pterms).map (fun t => (t.1, toAffine E hA hB t.2)) + = Msm.dpOf base i (pterms.map fun t => (t.1, toAffine E hA hB t.2)) := by simp only [pdpOf, Msm.dpOf, List.map_map, Function.comp_def] rw [hdpof] at hbmap - obtain ⟨-, hv2, heq⟩ := foldr_paccStep_spec _ hbval + obtain ⟨-, hv2, heq⟩ := foldr_paccStep_spec E hA hB hy0 _ hbval simp only [pwindowValueFast] refine ⟨hv2, ?_⟩ rw [Msm.windowValue, ← hbmap, ← heq] @@ -371,17 +394,18 @@ theorem pwindowValueFast_spec (base i : ℕ) (pterms : List (ℕ × PVes Fq)) /-- **Windowed Pippenger MSM in projective coordinates with single-pass Array bucketing** — the fast serial form of `pippengerProj`. Proven equal to the affine `Msm.pippenger` (`pippengerProjScatter_eq`). -/ -def pippengerProjScatter (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) +def pippengerProjScatter [DecidableEq F] (c : ℕ) (terms : List (ℕ × SWPoint E)) : SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) ((List.range (Msm.numWindows c terms)).map fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2)))) + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2)))) /-- **The scatter-bucketed projective Pippenger equals the affine Pippenger** — same transport as `pippengerProj_eq`, window values via `pwindowValueFast_spec`. -/ -theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProjScatter c terms = Msm.pippenger c terms := by +theorem pippengerProjScatter_eq [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatter E hA hB c terms = Msm.pippenger c terms := by rw [pippengerProjScatter] - set pterms := terms.map (fun t => (t.1, ofAffine Vesta.curve t.2)) with hpterms + set pterms := terms.map (fun t => (t.1, ofAffine E t.2)) with hpterms set windows := (List.range (Msm.numWindows c terms)).map fun i => pwindowValueFast (2 ^ c) i pterms with hwin @@ -389,29 +413,30 @@ theorem pippengerProjScatter_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : intro p hp rw [hpterms, List.mem_map] at hp obtain ⟨t, _, rfl⟩ := hp - exact valid_ofAffine Vesta.curve rfl rfl t.2 - have hf : pterms.map (fun t => (t.1, toAffine Vesta.curve rfl rfl t.2)) = terms := by + exact valid_ofAffine E hA hB t.2 + have hf : pterms.map (fun t => (t.1, toAffine E hA hB t.2)) = terms := by rw [hpterms, List.map_map] conv_rhs => rw [← List.map_id terms] apply List.map_congr_left intro t _ - simp only [Function.comp_apply, toAffine_ofAffine Vesta.curve rfl rfl, id_eq] + simp only [Function.comp_apply, toAffine_ofAffine, id_eq] have hwval : ∀ P ∈ windows, Valid P := by intro P hP rw [hwin, List.mem_map] at hP obtain ⟨i, _, rfl⟩ := hP - exact (pwindowValueFast_spec (2 ^ c) i pterms hval).1 - rw [(phornerList_spec (2 ^ c) windows hwval).2, Msm.pippenger] + exact (pwindowValueFast_spec E hA hB hy0 (2 ^ c) i pterms hval).1 + rw [(phornerList_spec E hA hB hy0 (2 ^ c) windows hwval).2, Msm.pippenger] congr 1 rw [hwin, List.map_map] apply List.map_congr_left intro i _ - rw [Function.comp_apply, (pwindowValueFast_spec (2 ^ c) i pterms hval).2, hf] + rw [Function.comp_apply, (pwindowValueFast_spec E hA hB hy0 (2 ^ c) i pterms hval).2, hf] /-- The scatter-bucketed projective Pippenger equals the naive MSM. -/ -theorem pippengerProjScatter_eq_msm (c : ℕ) (hc : 0 < c) (terms : List (ℕ × Projective.G)) : - pippengerProjScatter c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProjScatter_eq, Msm.pippenger_eq_msm c hc] +theorem pippengerProjScatter_eq_msm [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatter E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProjScatter_eq E hA hB hy0, Msm.pippenger_eq_msm c hc] /-! ## Windows-parallel projective Pippenger @@ -422,31 +447,32 @@ port. -/ /-- **Windows-parallel scatter-bucketed projective Pippenger**: `pippengerProjScatter` with the window values evaluated as parallel tasks. -/ -def pippengerProjScatterPar (c : ℕ) (terms : List (ℕ × Projective.G)) : Projective.G := - toAffine Vesta.curve rfl rfl (phornerList (2 ^ c) +def pippengerProjScatterPar [DecidableEq F] (c : ℕ) (terms : List (ℕ × SWPoint E)) : + SWPoint E := + toAffine E hA hB (phornerList (2 ^ c) (Msm.parMap (fun i => - pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine Vesta.curve t.2))) + pwindowValueFast (2 ^ c) i (terms.map fun t => (t.1, ofAffine E t.2))) (List.range (Msm.numWindows c terms)))) /-- The windows-parallel projective Pippenger is the sequential one: `parMap` is `map`. -/ -theorem pippengerProjScatterPar_eq (c : ℕ) (terms : List (ℕ × Projective.G)) : - pippengerProjScatterPar c terms = pippengerProjScatter c terms := by +theorem pippengerProjScatterPar_eq [DecidableEq F] (c : ℕ) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatterPar E hA hB c terms = pippengerProjScatter E hA hB c terms := by rw [pippengerProjScatterPar, Msm.parMap_eq_map, pippengerProjScatter] /-- The windows-parallel projective Pippenger equals the naive MSM. -/ -theorem pippengerProjScatterPar_eq_msm (c : ℕ) (hc : 0 < c) - (terms : List (ℕ × Projective.G)) : - pippengerProjScatterPar c terms = (terms.map fun t => t.1 • t.2).sum := by - rw [pippengerProjScatterPar_eq, pippengerProjScatter_eq_msm c hc] +theorem pippengerProjScatterPar_eq_msm [DecidableEq F] (hy0 : ∀ x : F, ¬ OnCurve 0 5 (x, 0)) + (c : ℕ) (hc : 0 < c) (terms : List (ℕ × SWPoint E)) : + pippengerProjScatterPar E hA hB c terms = (terms.map fun t => t.1 • t.2).sum := by + rw [pippengerProjScatterPar_eq, pippengerProjScatter_eq_msm E hA hB hy0 c hc] -/-! ## The `commit_lagrange` wrapper -/ +/-! ## The `commit_lagrange` wrapper (Vesta) -/ /-- The fast `commit_lagrange` run in projective coordinates: projective windowed Pippenger over the `(coeffᵢ.val, basisᵢ)` terms (single final inversion), plus the blind. The terms are zipped identically to `Fast.Msm.commitLagrangeFastWith` so the wrapper equality reuses `zip_terms_eq`. -/ def commitLagrangeProjWith (c : ℕ) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : Projective.G := - pippengerProj c + pippengerProj Vesta.curve rfl rfl c ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map fun t => (t.1.val, t.2)) + blind @@ -456,7 +482,8 @@ theorem commitLagrangeProjWith_eq (c : ℕ) (hc : 0 < c) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : commitLagrangeProjWith c blind basis coeffs = Msm.commitLagrangeSpec blind basis coeffs := by unfold commitLagrangeProjWith Msm.commitLagrangeSpec - rw [pippengerProj_eq, Msm.zip_terms_eq, Msm.pippenger_eq_msm c hc, List.map_map] + rw [pippengerProj_eq Vesta.curve rfl rfl Vesta.no_onCurve_y_zero, Msm.zip_terms_eq, + Msm.pippenger_eq_msm c hc, List.map_map] rfl /-- The fast `commit_lagrange` with scatter-bucketed projective Pippenger — the drop-in @@ -464,7 +491,7 @@ committer for the certificate's per-column pass (serial per column; the 44-colum `parMap` already saturates the cores). -/ def commitLagrangeProjScatterWith (c : ℕ) (blind : Projective.G) (basis : List Projective.G) (coeffs : List Fp) : Projective.G := - pippengerProjScatter c + pippengerProjScatter Vesta.curve rfl rfl c ((coeffs.zip (basis ++ List.replicate (coeffs.length - basis.length) 0)).map fun t => (t.1.val, t.2)) + blind @@ -475,7 +502,8 @@ theorem commitLagrangeProjScatterWith_eq (c : ℕ) (hc : 0 < c) commitLagrangeProjScatterWith c blind basis coeffs = Msm.commitLagrangeSpec blind basis coeffs := by unfold commitLagrangeProjScatterWith Msm.commitLagrangeSpec - rw [pippengerProjScatter_eq, Msm.zip_terms_eq, Msm.pippenger_eq_msm c hc, List.map_map] + rw [pippengerProjScatter_eq Vesta.curve rfl rfl Vesta.no_onCurve_y_zero, Msm.zip_terms_eq, + Msm.pippenger_eq_msm c hc, List.map_map] rfl end CompElliptic.Curves.Pasta.Fast.MsmProj diff --git a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean index 705ad8a..d1606d7 100644 --- a/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean +++ b/CompElliptic/Curves/Pasta/Fast/ProjectiveMontEquiv.lean @@ -607,7 +607,8 @@ theorem msmM_spec (c : ℕ) (hc : 0 < c) (terms : List (ℕ × PM)) intro i have hR := RM_windowValue (2 ^ c) i terms hwf rw [← hpterms] at hR - obtain ⟨hvw, hew⟩ := MsmProj.pwindowValueFast_spec (2 ^ c) i pterms hptv + obtain ⟨hvw, hew⟩ := MsmProj.pwindowValueFast_spec Vesta.curve rfl rfl + Vesta.no_onCurve_y_zero (2 ^ c) i pterms hptv exact ⟨RM_valid hR hvw, by rw [RM_toG hR, hew, hmapaff]⟩ have hvals : ∀ v ∈ (List.range W).map (fun i => PM.windowValue (2 ^ c) i terms), WV v := by intro v hvm