From 0fba34f4a009305d6fc525fc32170c9644acb393 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Sun, 16 Aug 2026 01:30:56 +0100 Subject: [PATCH 01/14] refactor(Isogenies): name the field-to-curve map f in mapHashOutputsToCurve MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `mapHashOutputsToCurve` and its `_eq` lemma took the field-to-curve map as `m`. Ironwood's group-hash development calls that map `f` (`f : F → G`), so rename the parameter to `f` for cross-repo consistency. Callers are unaffected — the map is passed positionally. Co-authored-by: Claude Opus 4.8 (1M context) --- CompElliptic/Isogenies/Homomorphism.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/CompElliptic/Isogenies/Homomorphism.lean b/CompElliptic/Isogenies/Homomorphism.lean index ff68d15..6be4325 100644 --- a/CompElliptic/Isogenies/Homomorphism.lean +++ b/CompElliptic/Isogenies/Homomorphism.lean @@ -546,8 +546,8 @@ operation: it is cryptographically hazardous unless composed with modelled as a random oracle by itself. Maps two field elements, intended to be outputs of `hash_to_field`, to the isogeny's domain curve, adds there, and applies the isogeny once (spec §5.4.9.8). -/ -def mapHashOutputsToCurve (m : F → SWPoint I.domain) (u₀ u₁ : F) : SWPoint I.codomain := - I.map (m u₀ + m u₁) +def mapHashOutputsToCurve (f : F → SWPoint I.domain) (u₀ u₁ : F) : SWPoint I.codomain := + I.map (f u₀ + f u₁) /-- `mapHashOutputsToCurve` agrees with applying the isogeny to each point and adding on the codomain. RFC 9380 §6.6.3 notes exactly this optimization —add on @@ -558,8 +558,8 @@ spec and `hashtocurve.sage` use the one-evaluation order, while theorem mapHashOutputsToCurve_eq (h2 : (2 : F) ≠ 0) (hd : ∀ X : F, ¬ OnCurve I.domain.A I.domain.B (X, 0)) (hc : ∀ X : F, ¬ OnCurve I.codomain.A I.codomain.B (X, 0)) - (m : F → SWPoint I.domain) (u₀ u₁ : F) : - I.mapHashOutputsToCurve m u₀ u₁ = I.map (m u₀) + I.map (m u₁) := - I.map_add h2 hd hc (m u₀) (m u₁) + (f : F → SWPoint I.domain) (u₀ u₁ : F) : + I.mapHashOutputsToCurve f u₀ u₁ = I.map (f u₀) + I.map (f u₁) := + I.map_add h2 hd hc (f u₀) (f u₁) end CompElliptic.Isogenies.ThreeIsogeny From 64a9165239210fdfb2d62aa0d82d7fd78292b082 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 13 Aug 2026 10:45:32 +0100 Subject: [PATCH 02/14] feat(Hashing): nonzero preimage fibres of simplified SWU have at most 10 elements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The counting fact the indifferentiability arc's rejection sampler consumes (zcash/ironwood#198, CompElliptic#25). On a field where -1 is a square (both Pasta base fields), a nonzero input is never exceptional, so a nonzero preimage of an abscissa x is a root of the explicit product polynomial combining the two branch equations cleared of their common denominator: nonzero of degree at most 10, since its second factor has degree exactly 6 with leading coefficient -B·Z³. The input u = 0 is excluded rather than counted: the probability analysis prices pairs containing 0 in its existing zero-repair correction. The optimal constant is 4, recorded in the module doc as a planned follow-up. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/FibreBound.lean | 202 +++++++++++++++++++++++++++ 1 file changed, 202 insertions(+) create mode 100644 CompElliptic/Hashing/FibreBound.lean diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean new file mode 100644 index 0000000..ed209c0 --- /dev/null +++ b/CompElliptic/Hashing/FibreBound.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import CompElliptic.Hashing.SimplifiedSWU +import Mathlib.Algebra.Polynomial.Roots +import Mathlib.Tactic.ComputeDegree + +/-! +# Fibre bounds for the simplified SWU mapping + +Away from the input `u = 0`, every point of the target curve has at most 10 +preimages under `SSWUParams.map`. This is the counting fact the +indifferentiability arc's rejection sampler consumes (zcash/ironwood#198, +CompElliptic#25): to sample a uniform preimage of a point under the deployed +two-term construction, the sampler needs each single-term fibre to be +computable and small; smallness is what makes its acceptance probability an +explicit constant. The input `u = 0` is excluded rather than counted: the +probability analysis already carries a negligible correction for pairs +containing `0` (the deployed-vs-zero-repaired transport), and the sampler +rides the same correction. + +The bound is by abscissa, and the argument is elementary root counting. On a +field where `-1` is a square (both Pasta base fields, `q ≡ 1 (mod 4)`), a +nonzero input is never exceptional: `ta = t² + t = 0` forces `t = 0` (which +is `u = 0`) or `t = -1` (which would make `-1/Z = u²` a square against `Z` +nonsquare). So a nonzero preimage `u` of a point with abscissa `x` satisfies +`xnum/xdiv = x`, where `xnum` is one of the two branch numerators and the +denominator is `xdiv = A·(-ta)`. Clearing the denominator turns membership +in *either* branch into the vanishing of the product polynomial + +`Φ_x(u) = (x·(-A·ta) - x1num) · (x·(-A·ta) - x2num)`. + +This is an explicit polynomial in `u` through `t = Z·u²`. Its second factor has +degree exactly 6 with leading coefficient `-B·Z³ ≠ 0`, so `Φ_x` is a nonzero +polynomial of degree at most 10, and has at most 10 roots. + +The constant is deliberately crude; the proof stays at the level of one +product polynomial. The optimal constant is 4: each branch equation is a +quadratic in `t`, and oddness pairs `±u` across `P` and `-P` (which are +distinct — the target curves have no 2-torsion), so each `t` contributes one +preimage. Tightening to that constant is a planned follow-up. +-/ + +namespace CompElliptic.Hashing + +open Finset Polynomial CompElliptic.CurveForms.ShortWeierstrass + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] + +/-- The polynomial `t = Z·u²`, as a polynomial in `u`. -/ +noncomputable def tPoly (G : SSWUParams F) : Polynomial F := C G.Z * X^2 + +/-- The polynomial `ta = t² + t`, as a polynomial in `u`. -/ +noncomputable def taPoly (G : SSWUParams F) : Polynomial F := + G.tPoly^2 + G.tPoly + +/-- The abscissa-fibre polynomial `Φ_x`: away from `u = 0`, a preimage of +abscissa `x` under either branch is a root. The first factor is the branch-1 +equation `x·(-A·ta) = x1num`, the second the branch-2 equation +`x·(-A·ta) = x2num`, both cleared of the denominator `xdiv = A·(-ta)`. -/ +noncomputable def fibrePoly (G : SSWUParams F) (x : F) : Polynomial F := + (C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1)) * + (C x * (-(C G.E.A) * G.taPoly) - G.tPoly * (C G.E.B * (G.taPoly + 1))) + +/-- The second factor of `Φ_x` has degree exactly 6, because its leading +coefficient `-B·Z³` does not vanish for any `x`. -/ +theorem fibrePoly_snd_natDegree (G : SSWUParams F) (x : F) : + (C x * (-(C G.E.A) * G.taPoly) + - G.tPoly * (C G.E.B * (G.taPoly + 1))).natDegree = 6 := by + rw [taPoly, tPoly] + compute_degree! + exact ⟨G.Z_nonzero, G.E.B_nonzero, G.Z_nonzero⟩ + +/-- The second factor of `Φ_x` is nonzero, because it has degree 6. -/ +theorem fibrePoly_snd_ne_zero (G : SSWUParams F) (x : F) : + C x * (-(C G.E.A) * G.taPoly) + - G.tPoly * (C G.E.B * (G.taPoly + 1)) ≠ 0 := by + intro h + have hdeg := G.fibrePoly_snd_natDegree x + rw [h, natDegree_zero] at hdeg + exact absurd hdeg (by norm_num) + +/-- The first factor of `Φ_x` is nonzero, because it either has degree 4 +(when `A·x + B ≠ 0`) or is the nonzero constant `-B`. -/ +theorem fibrePoly_fst_ne_zero (G : SSWUParams F) (x : F) : + C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1) ≠ 0 := by + have hexpand : C x * (-(C G.E.A) * G.taPoly) - C G.E.B * (G.taPoly + 1) + = -(C (G.E.A * x + G.E.B)) * G.taPoly - C G.E.B := by + rw [map_add, map_mul] + ring + rw [hexpand] + intro h + by_cases hAB : G.E.A * x + G.E.B = 0 + · rw [hAB, map_zero, neg_zero, zero_mul, zero_sub, neg_eq_zero, + C_eq_zero] at h + exact G.E.B_nonzero h + · have hdeg : (-(C (G.E.A * x + G.E.B)) * G.taPoly - C G.E.B).natDegree + = 4 := by + rw [taPoly, tPoly] + compute_degree! + refine ⟨fun hc => hAB ?_, G.Z_nonzero⟩ + linear_combination -hc + rw [h, natDegree_zero] at hdeg + exact absurd hdeg (by norm_num) + +/-- `Φ_x` is nonzero, because both its factors are. -/ +theorem fibrePoly_ne_zero (G : SSWUParams F) (x : F) : G.fibrePoly x ≠ 0 := + mul_ne_zero (G.fibrePoly_fst_ne_zero x) (G.fibrePoly_snd_ne_zero x) + +theorem fibrePoly_natDegree_le (G : SSWUParams F) (x : F) : + (G.fibrePoly x).natDegree ≤ 10 := by + refine natDegree_mul_le.trans ?_ + have h1 : (C x * (-(C G.E.A) * G.taPoly) + - C G.E.B * (G.taPoly + 1)).natDegree ≤ 4 := by + rw [taPoly, tPoly] + compute_degree + have h2 := (G.fibrePoly_snd_natDegree x).le + omega + +/-- Away from `u = 0`, a preimage of abscissa `x` is a root of `Φ_x`. The +denominator is `A·(-ta)` with `ta ≠ 0`, and whichever branch the square-root +split took, the corresponding factor of `Φ_x` vanishes. -/ +theorem eval_fibrePoly_eq_zero (G : SSWUParams F) {x u : F} + (hta : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0) + (hx : (G.mapXYUpToSign u).1 = x) : + (G.fibrePoly x).eval u = 0 := by + have heval_t : G.tPoly.eval u = G.Z * u^2 := by + simp [tPoly] + have heval_ta : G.taPoly.eval u = (G.Z * u^2)^2 + G.Z * u^2 := by + simp [taPoly, tPoly] + simp only [mapXYUpToSign] at hx + rw [if_neg hta] at hx + have hxdiv : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero (neg_ne_zero.mpr hta) + rw [div_eq_iff hxdiv] at hx + rw [fibrePoly, eval_mul] + split_ifs at hx with hsr + · apply mul_eq_zero_of_left + simp only [eval_sub, eval_mul, eval_neg, eval_C, eval_add, eval_one, + heval_ta] + linear_combination -hx + · apply mul_eq_zero_of_right + simp only [eval_sub, eval_mul, eval_neg, eval_C, eval_add, eval_one, + heval_ta, heval_t] + linear_combination -hx + +/-- A nonzero input is never exceptional when `-1` is a square, because +`ta = 0` forces `t = 0` (that is, `u = 0`) or `t = -1`, and the latter would +exhibit the nonsquare `Z` as `-1` times a square of an inverse. -/ +theorem ta_ne_zero_of_u_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) {u : F} + (hu : u ≠ 0) : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0 := by + intro h + have hfac : G.Z * u^2 * (G.Z * u^2 + 1) = 0 := by linear_combination h + rcases mul_eq_zero.mp hfac with h0 | h1 + · rcases mul_eq_zero.mp h0 with hZ | hu2 + · exact G.Z_nonzero hZ + · exact hu (sq_eq_zero_iff.mp hu2) + · obtain ⟨s, hs⟩ := hsq + have hZu : G.Z * u^2 = -1 := by linear_combination h1 + refine G.Z_nonsquare ⟨s/u, ?_⟩ + rw [div_mul_div_comm, show u*u = u^2 from (pow_two u).symm] + exact (eq_div_iff (pow_ne_zero 2 hu)).mpr (hZu.trans hs) + +/-- **At most 10 nonzero preimages per abscissa.** On a field where `-1` is +a square, every nonzero preimage is a root of the degree-≤10 polynomial +`Φ_x`. -/ +theorem card_abscissaFibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F)) + (x : F) : + (univ.filter fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x).card ≤ 10 := by + have hsub : univ.filter (fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x) + ⊆ (G.fibrePoly x).roots.toFinset := by + intro u hu + rw [mem_filter] at hu + rw [Multiset.mem_toFinset, mem_roots (G.fibrePoly_ne_zero x)] + exact G.eval_fibrePoly_eq_zero (G.ta_ne_zero_of_u_ne_zero hsq hu.2.1) hu.2.2 + calc (univ.filter fun u => u ≠ 0 ∧ (G.mapXYUpToSign u).1 = x).card + ≤ (G.fibrePoly x).roots.toFinset.card := Finset.card_le_card hsub + _ ≤ (G.fibrePoly x).roots.card := Multiset.toFinset_card_le _ + _ ≤ (G.fibrePoly x).natDegree := (G.fibrePoly x).card_roots' + _ ≤ 10 := G.fibrePoly_natDegree_le x + +/-- **At most 10 nonzero preimages per point** under the simplified SWU +mapping. A preimage of `P` is in particular a preimage of its abscissa. The +optimal constant is 4 (a planned follow-up); the input `u = 0` is excluded, +priced by the probability analysis's existing zero-pair correction. -/ +theorem card_map_fibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F)) + (P : SWPoint G.E) : + (univ.filter fun u => u ≠ 0 ∧ G.map u = P).card ≤ 10 := by + refine (Finset.card_le_card ?_).trans (G.card_abscissaFibre_le hsq P.x) + intro u hu + rw [mem_filter] at hu ⊢ + exact ⟨mem_univ u, hu.2.1, + by rw [show (G.mapXYUpToSign u).1 = (G.map u).x from rfl, hu.2.2]⟩ + +end SSWUParams + +end CompElliptic.Hashing From 1ccea0d8123a0adcea0676411445cc515d702231 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 13 Aug 2026 10:48:56 +0100 Subject: [PATCH 03/14] feat(Hashing): the deployed mapToCurve fibre bound, per curve MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit -1 is a square in both Pasta base fields (q ≡ 1 mod 4, Euler's criterion), so the generic SSWU fibre bound applies, and the isogeny is injective on rational points (iso_map_bijective), so it carries through the composition: at most 10 nonzero preimages per point under the deployed mapToCurve. The generic composition step is card_fibre_comp_le in FibreBound. The census records both endpoints; they consume the Tonelli-Shanks validity witnesses and, through the isogeny's bijectivity, the order witnesses. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/FibreBound.lean | 19 +++++++++++++++++ CompElliptic/Hashing/PastaSSWU.lean | 31 ++++++++++++++++++++++++++++ CompElliptic/TrustBoundary.lean | 8 +++++++ 3 files changed, 58 insertions(+) diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean index ed209c0..95331cd 100644 --- a/CompElliptic/Hashing/FibreBound.lean +++ b/CompElliptic/Hashing/FibreBound.lean @@ -199,4 +199,23 @@ theorem card_map_fibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F)) end SSWUParams +/-- Composing with an injective map does not grow fibres: a fibre bound for +`f` is a fibre bound for `g ∘ f`. Stated with the auxiliary predicate that +the fibre-bound statements carry. -/ +theorem card_fibre_comp_le {α β γ : Type*} [Fintype α] [DecidableEq β] + [DecidableEq γ] {f : α → β} {g : β → γ} (hg : Function.Injective g) + {pred : α → Prop} [DecidablePred pred] {n : ℕ} + (h : ∀ Q : β, (univ.filter fun u => pred u ∧ f u = Q).card ≤ n) + (P : γ) : + (univ.filter fun u => pred u ∧ g (f u) = P).card ≤ n := by + rcases (univ.filter fun u => pred u ∧ g (f u) = P).eq_empty_or_nonempty + with he | ⟨u₀, hu₀⟩ + · rw [he, Finset.card_empty] + exact Nat.zero_le n + · rw [mem_filter] at hu₀ + refine (Finset.card_le_card ?_).trans (h (f u₀)) + intro u hu + rw [mem_filter] at hu ⊢ + exact ⟨mem_univ u, hu.2.1, hg (hu.2.2.trans hu₀.2.2.symm)⟩ + end CompElliptic.Hashing diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index b90a1a1..fa2b28b 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -9,6 +9,7 @@ import CompElliptic.Isogenies.Homomorphism import CompElliptic.Curves.PastaOrder import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.SignedLift +import CompElliptic.Hashing.FibreBound import Mathlib.Tactic.ReduceModChar /-! @@ -71,6 +72,12 @@ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : PallasBaseField) := by reduce_mod_char decide +/-- `-1` is a square in the Pallas base field (`q ≡ 1 (mod 4)`), by Euler's +criterion with the power evaluated by fast modular exponentiation. -/ +theorem isSquare_neg_one : IsSquare (-1 : PallasBaseField) := by + rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (-1 : PallasBaseField) ≠ 0)] + reduce_mod_char + /-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Pallas is not a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast modular exponentiation, as for `neg_five_not_isCube`. -/ @@ -153,6 +160,15 @@ character-sum analysis consumes. -/ theorem isOdd_zeroRepaired_mapToCurve : IsOdd (zeroRepaired mapToCurve) := isOdd_zeroRepaired fun _ hu => mapToCurve_neg hu +/-- **At most 10 nonzero preimages per point** under the deployed +`mapToCurve`. The isogeny is injective on rational points, so the SSWU fibre +bound carries over. This is the counting interface for the +indifferentiability sampler (zcash/ironwood#198). -/ +theorem card_mapToCurve_fibre_le (P : SWPoint curve) : + (Finset.univ.filter fun u => u ≠ 0 ∧ mapToCurve u = P).card ≤ 10 := + card_fibre_comp_le iso_map_bijective.injective + (fun Q => sswu.card_map_fibre_le isSquare_neg_one Q) P + /-- The zero-repair transport, composed at the deployed mapping: for every character, the deployed and repaired character sums differ by exactly `ψ (mapToCurve 0) - 1`. Conclusions about the literally-odd @@ -248,6 +264,12 @@ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : VestaBaseField) := by reduce_mod_char decide +/-- `-1` is a square in the Vesta base field (`q ≡ 1 (mod 4)`), by Euler's +criterion with the power evaluated by fast modular exponentiation. -/ +theorem isSquare_neg_one : IsSquare (-1 : VestaBaseField) := by + rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (-1 : VestaBaseField) ≠ 0)] + reduce_mod_char + /-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Vesta is not a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast modular exponentiation, as for `neg_five_not_isCube`. -/ @@ -325,6 +347,15 @@ character-sum analysis consumes. -/ theorem isOdd_zeroRepaired_mapToCurve : IsOdd (zeroRepaired mapToCurve) := isOdd_zeroRepaired fun _ hu => mapToCurve_neg hu +/-- **At most 10 nonzero preimages per point** under the deployed +`mapToCurve`. The isogeny is injective on rational points, so the SSWU fibre +bound carries over. This is the counting interface for the +indifferentiability sampler (zcash/ironwood#198). -/ +theorem card_mapToCurve_fibre_le (P : SWPoint curve) : + (Finset.univ.filter fun u => u ≠ 0 ∧ mapToCurve u = P).card ≤ 10 := + card_fibre_comp_le iso_map_bijective.injective + (fun Q => sswu.card_map_fibre_le isSquare_neg_one Q) P + /-- The zero-repair transport, composed at the deployed mapping: for every character, the deployed and repaired character sums differ by exactly `ψ (mapToCurve 0) - 1`. Conclusions about the literally-odd diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index 417c3a7..fc6cb6d 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -112,6 +112,14 @@ assert_axioms CompElliptic.Curves.Pasta.Pallas.norm_charSum_mapToCurve_sub_zeroR CompElliptic.Fields.Pasta.pallasBase) assert_axioms CompElliptic.Curves.Pasta.Vesta.norm_charSum_mapToCurve_sub_zeroRepaired +native( CompElliptic.Fields.Pasta.vestaBase) +assert_axioms CompElliptic.Curves.Pasta.Pallas.card_mapToCurve_fibre_le +native( + CompElliptic.Fields.Pasta.pallasBase, + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt, + CompElliptic.Curves.Pasta.Pallas.q_nsmul_isoGpt) +assert_axioms CompElliptic.Curves.Pasta.Vesta.card_mapToCurve_fibre_le +native( + CompElliptic.Fields.Pasta.vestaBase, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_isoGpt) assert_axioms CompElliptic.Curves.Pasta.Pallas.mapHashOutputsToCurve_eq +native( CompElliptic.Fields.Pasta.pallasBase) assert_axioms CompElliptic.Curves.Pasta.Vesta.mapHashOutputsToCurve_eq +native( From db48e4fe7a604d577c0dcbda91e76989ee343e50 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 13 Aug 2026 11:00:20 +0100 Subject: [PATCH 04/14] feat(Hashing): deviation exports and the zero-repair pair transport MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The counting interface the indifferentiability game side consumes (zcash/ironwood#198, CompElliptic#25), in three statements. sum_abs_prob_dev_le is the L¹ probability deviation unsquared, stated against any budget whose square dominates the squared bound, so the consumer never needs a square root and a concrete budget is checked by squaring in exact arithmetic. card_dev_ge_le is the Chebyshev-style counting form of the L² bound: regularity does not lower-bound individual fibres, so the rejection sampler's acceptance constant holds only outside a bad set of fibres, whose size this bounds. sum_abs_pairCount_sub_le prices replacing the zero-repaired mapping by the deployed one: mappings agreeing away from one input have two-term pair counts within 4·#F - 2 in L¹, by splitting every pair count at the pairs containing that input. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/TwoTermUniformity.lean | 146 ++++++++++++++++++++ 1 file changed, 146 insertions(+) diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index a3c08a8..52c0238 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -376,4 +376,150 @@ theorem sq_sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ} _ = ((Fintype.card G : ℝ) - 1) * C^4 * ((Fintype.card G : ℝ) * (Fintype.card F : ℝ)^2)^2 := by ring + +/-! ## Exports for the indifferentiability arc + +The game-side consumer (zcash/ironwood#198) works in `ℝ≥0∞` and should never +need a square root. `sum_abs_prob_dev_le` states the L¹ bound against any +budget `ε` whose square dominates the squared bound, so a concrete `ε` is +checked by squaring, in exact arithmetic. `card_dev_ge_le` is the +Chebyshev-style counting form of the L² bound: regularity does not +lower-bound individual fibres, so the rejection sampler's acceptance +constant holds only outside a bad set of fibres, whose size this bounds. +`sum_abs_pairCount_sub_le` prices replacing the zero-repaired mapping by the +deployed one: the two mappings differ at the single input `0`, so their +two-term pair counts differ only on pairs containing it. -/ + +/-- The L¹ probability deviation, unsquared, against an arbitrary budget: if +`ε²` dominates the squared bound then the deviation is at most `ε`. -/ +theorem sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ} + (h : WeilBounded f C) {ε : ℝ} (hε : 0 ≤ ε) + (hbound : ((Fintype.card G : ℝ) - 1) * C^4 / (Fintype.card F : ℝ)^2 + ≤ ε^2) : + ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)| ≤ ε := by + have hx : 0 ≤ ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)| := + Finset.sum_nonneg fun Q _ => abs_nonneg _ + have hsq := (sq_sum_abs_prob_dev_le f h).trans hbound + nlinarith [hsq, hx, hε] + +/-- **Chebyshev-style bad-set counting**: the number of outputs whose pair +count deviates from its uniform value by at least `τ`, multiplied by `τ²`, +is at most the summed squared deviation. -/ +theorem card_dev_ge_le (f : F → G) {C : ℝ} (h : WeilBounded f C) {τ : ℝ} + (hτ : 0 ≤ τ) : + ((univ.filter fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2|).card : ℝ) * τ^2 + ≤ (Fintype.card G : ℝ) * ((Fintype.card G : ℝ) - 1) + * (C^2 * Fintype.card F)^2 := by + classical + refine le_trans ?_ (sum_sq_dev_le f h) + calc ((univ.filter fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2|).card : ℝ) * τ^2 + = ∑ _Q ∈ univ.filter (fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2|), τ^2 := by + rw [Finset.sum_const, nsmul_eq_mul] + _ ≤ ∑ Q ∈ univ.filter (fun Q => τ ≤ |(Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2|), + ((Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2)^2 := by + refine Finset.sum_le_sum fun Q hQ => ?_ + have hdev := (Finset.mem_filter.mp hQ).2 + calc τ^2 ≤ |(Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2|^2 := pow_le_pow_left₀ hτ hdev 2 + _ = _ := sq_abs _ + _ ≤ ∑ Q, ((Fintype.card G : ℝ) * pairCount f Q + - (Fintype.card F : ℝ)^2)^2 := + Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _) + fun Q _ _ => sq_nonneg _ + +/-- **The zero-repair transport for pair counts**: two mappings agreeing away +from a single input have two-term pair counts within `4·#F - 2` of each other +in L¹, because only the pairs containing that input can differ. -/ +theorem sum_abs_pairCount_sub_le [Nonempty F] (f g : F → G) (u₀ : F) + (h : ∀ u, u ≠ u₀ → f u = g u) : + ∑ Q, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)| + ≤ 4 * Fintype.card F - 2 := by + classical + set T : Finset (F × F) := univ.filter (fun p => p.1 = u₀ ∨ p.2 = u₀) + with hT + -- Pairs away from `T` have equal sums under `f` and `g`. + have hagree : ∀ p : F × F, p ∉ T → f p.1 + f p.2 = g p.1 + g p.2 := by + intro p hp + simp only [hT, mem_filter, mem_univ, true_and, not_or] at hp + rw [h p.1 hp.1, h p.2 hp.2] + -- Each pair count splits at `T`, and the parts away from `T` agree. + have hsplit : ∀ (m : F → G) (Q : G), (pairCount m Q : ℕ) + = ((univ.filter fun p : F × F => m p.1 + m p.2 = Q) \ T).card + + (T.filter fun p => m p.1 + m p.2 = Q).card := by + intro m Q + have hinter : (univ.filter fun p : F × F => m p.1 + m p.2 = Q) ∩ T + = T.filter fun p => m p.1 + m p.2 = Q := by + ext p + simp only [Finset.mem_inter, mem_filter, mem_univ, true_and] + exact ⟨fun ⟨a, b⟩ => ⟨b, a⟩, fun ⟨a, b⟩ => ⟨b, a⟩⟩ + rw [pairCount, ← hinter, add_comm] + exact (Finset.card_inter_add_card_sdiff _ _).symm + have hkey : ∀ Q : G, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)| + ≤ ((T.filter fun p => f p.1 + f p.2 = Q).card : ℝ) + + ((T.filter fun p => g p.1 + g p.2 = Q).card : ℝ) := by + intro Q + have hsdiff : ((univ.filter fun p : F × F => f p.1 + f p.2 = Q) \ T) + = ((univ.filter fun p : F × F => g p.1 + g p.2 = Q) \ T) := by + ext p + simp only [Finset.mem_sdiff, mem_filter, mem_univ, true_and] + exact ⟨fun ⟨hpQ, hpT⟩ => ⟨by rw [← hagree p hpT]; exact hpQ, hpT⟩, + fun ⟨hpQ, hpT⟩ => ⟨by rw [hagree p hpT]; exact hpQ, hpT⟩⟩ + rw [hsplit f Q, hsplit g Q, hsdiff] + push_cast + have hx : (0 : ℝ) ≤ (T.filter fun p => f p.1 + f p.2 = Q).card := + Nat.cast_nonneg _ + have hy : (0 : ℝ) ≤ (T.filter fun p => g p.1 + g p.2 = Q).card := + Nat.cast_nonneg _ + rw [abs_le] + constructor <;> [linarith; linarith] + -- Sum the per-output bounds; each side totals `T.card` fibrewise. + have hfib : ∀ m : F → G, ∑ Q : G, + ((T.filter fun p => m p.1 + m p.2 = Q).card : ℝ) = (T.card : ℝ) := by + intro m + exact_mod_cast (Finset.card_eq_sum_card_fiberwise + (f := fun p : F × F => m p.1 + m p.2) (s := T) (t := univ) + fun p _ => mem_univ _).symm + -- `T` is two axis copies of `F` overlapping in one pair. + have hTcard : T.card = 2 * Fintype.card F - 1 := by + have h1 : (univ.filter fun p : F × F => p.1 = u₀) = {u₀} ×ˢ univ := by + ext p + simp only [mem_filter, mem_univ, true_and, Finset.mem_product, + Finset.mem_singleton, and_true] + have h2 : (univ.filter fun p : F × F => p.2 = u₀) = univ ×ˢ {u₀} := by + ext p + simp only [mem_filter, mem_univ, true_and, Finset.mem_product, + Finset.mem_singleton, true_and] + have hint : (univ.filter fun p : F × F => p.1 = u₀) + ∩ (univ.filter fun p : F × F => p.2 = u₀) = {(u₀, u₀)} := by + ext p + simp [Finset.mem_inter, Prod.ext_iff] + have hcards := Finset.card_union_add_card_inter + (univ.filter fun p : F × F => p.1 = u₀) + (univ.filter fun p : F × F => p.2 = u₀) + rw [hint, h1, h2] at hcards + simp only [Finset.card_product, Finset.card_singleton, Finset.card_univ, + one_mul, mul_one] at hcards + rw [hT, Finset.filter_or, h1, h2] + omega + have hF1 : 1 ≤ 2 * Fintype.card F := by + have := Fintype.card_pos (α := F) + omega + calc ∑ Q, |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)| + ≤ ∑ Q : G, (((T.filter fun p => f p.1 + f p.2 = Q).card : ℝ) + + ((T.filter fun p => g p.1 + g p.2 = Q).card : ℝ)) := + Finset.sum_le_sum fun Q _ => hkey Q + _ = (T.card : ℝ) + (T.card : ℝ) := by + rw [Finset.sum_add_distrib, hfib f, hfib g] + _ = 4 * Fintype.card F - 2 := by + rw [hTcard] + push_cast [Nat.cast_sub hF1] + ring + end CompElliptic.Hashing From 5f02eb2021b2daca664897f7d2098228ce4912c9 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 13 Aug 2026 19:17:23 +0100 Subject: [PATCH 05/14] feat(CurveForms): adopt the curve lemmas from ironwood's CompEllipticExtras MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit zcash/ironwood carried Zcash/Circuits/Specs/CompEllipticExtras.lean, written in CompElliptic's own namespaces as explicit upstreaming candidates. Adopt the curve lemmas into CurveForms/ShortWeierstrass.lean: - SWPoint.add_x / SWPoint.add_y: rfl projection lemmas for the coordinates of a sum. - y_eq_pm_of_onCurve_x_eq (was y_eq_or_y_eq_neg_of_onCurve; the rename names the shared-abscissa premiss): two points on the curve sharing an x-coordinate have y-coordinates equal up to sign. - SWPoint.onCurve_of_ne_zero: a nonzero representable point is on the curve. - SWPoint.eq_pm_of_x_eq (was SWPoint.eq_or_eq_neg_of_x_eq): nonzero representable points sharing an x-coordinate are equal up to sign. This subsumes the private eq_or_eq_neg_of_x_eq in Isogenies/Homomorphism.lean, which is removed. The ≠ 0 premisses are necessary at SWCurve generality: SWCurve requires only B ≠ 0, so a curve whose B is a square has a genuine point (0, √B) sharing x = 0 with the 𝒪 sentinel without being equal to it up to sign. Closes daira/CompElliptic#12. Co-authored-by: Claude Fable 5 --- CompElliptic/CurveForms/ShortWeierstrass.lean | 42 +++++++++++++++++++ CompElliptic/Isogenies/Homomorphism.lean | 22 ++++------ 2 files changed, 49 insertions(+), 15 deletions(-) diff --git a/CompElliptic/CurveForms/ShortWeierstrass.lean b/CompElliptic/CurveForms/ShortWeierstrass.lean index 180ed93..84a2ab6 100644 --- a/CompElliptic/CurveForms/ShortWeierstrass.lean +++ b/CompElliptic/CurveForms/ShortWeierstrass.lean @@ -60,6 +60,18 @@ theorem not_onCurve_zero {a b : F} (hb : b ≠ 0) : ¬ OnCurve a b (0, 0) := by have h' : (0 : F) ^ 2 = (0 : F) ^ 3 + a * 0 + b := h simpa using h'.symm +omit [DecidableEq F] in +/-- Two points on the curve sharing an `x`-coordinate have `y`-coordinates equal up to sign, +because their curve equations subtract to `(y₁ - y₂)·(y₁ + y₂) = 0`. -/ +theorem y_eq_pm_of_onCurve_x_eq {a b x y₁ y₂ : F} + (h₁ : OnCurve a b (x, y₁)) (h₂ : OnCurve a b (x, y₂)) : y₁ = y₂ ∨ y₁ = -y₂ := by + have h : (y₁ - y₂) * (y₁ + y₂) = 0 := by + simp only [OnCurve] at h₁ h₂ + linear_combination h₁ - h₂ + rcases mul_eq_zero.mp h with h | h + · exact Or.inl (sub_eq_zero.mp h) + · exact Or.inr (by linear_combination h) + /-- Negation `(x, y) ↦ (x, -y)`; fixes the `(0, 0)` sentinel. -/ def neg (p : F × F) : F × F := (p.1, -p.2) @@ -426,6 +438,36 @@ omit [DecidableEq F] in /-- Negation negates the `y`-coordinate — the one fact that makes `2 • P = 0` say `P.y = -P.y`. -/ @[simp] theorem SWPoint.neg_y {E : SWCurve F} (P : SWPoint E) : (-P).y = -P.y := rfl +/-- Addition computes its `x`-coordinate by the raw `add` on the coordinate pairs. -/ +lemma SWPoint.add_x {E : SWCurve F} (P Q : SWPoint E) : + (P + Q).x = (add E.A (P.x, P.y) (Q.x, Q.y)).1 := rfl + +/-- Addition computes its `y`-coordinate by the raw `add` on the coordinate pairs. -/ +lemma SWPoint.add_y {E : SWCurve F} (P Q : SWPoint E) : + (P + Q).y = (add E.A (P.x, P.y) (Q.x, Q.y)).2 := rfl + +omit [DecidableEq F] in +/-- A nonzero representable point is on the curve: its `Valid` disjunction cannot be the `(0, 0)` +sentinel. -/ +theorem SWPoint.onCurve_of_ne_zero {E : SWCurve F} {P : SWPoint E} (h : P ≠ 0) : + OnCurve E.A E.B (P.x, P.y) := by + rcases P.onCurve with hc | h0 + · exact hc + · exact absurd (SWPoint.ext_pair (by rw [h0]; rfl)) h + +omit [DecidableEq F] in +/-- Nonzero representable points sharing an `x`-coordinate are equal up to sign: both are on the +curve (`onCurve_of_ne_zero`), so their `y`-coordinates agree up to sign +(`y_eq_pm_of_onCurve_x_eq`). -/ +theorem SWPoint.eq_pm_of_x_eq {E : SWCurve F} {P Q : SWPoint E} + (hP : P ≠ 0) (hQ : Q ≠ 0) (hx : P.x = Q.x) : P = Q ∨ P = -Q := by + have hPC := onCurve_of_ne_zero hP + have hQC := onCurve_of_ne_zero hQ + rw [hx] at hPC + rcases y_eq_pm_of_onCurve_x_eq hPC hQC with hy | hy + · exact Or.inl (ext_pair (by rw [hx, hy])) + · exact Or.inr (ext_pair (by rw [hx, hy]; rfl)) + /-! ### Fast (logarithmic) scalar multiplication The spec-level `smul` is linear (`n` additions), so it cannot be evaluated by `decide` or diff --git a/CompElliptic/Isogenies/Homomorphism.lean b/CompElliptic/Isogenies/Homomorphism.lean index 6be4325..c62dc4d 100644 --- a/CompElliptic/Isogenies/Homomorphism.lean +++ b/CompElliptic/Isogenies/Homomorphism.lean @@ -457,20 +457,6 @@ theorem map_neg (P : SWPoint I.domain) : I.map (-P) = -I.map P := by · have hP0 : (P.x, P.y) = ((0 : F), (0 : F)) := P.onCurve.resolve_left hP rw [SWPoint.ext_pair (E := I.domain) (Q := 0) hP0, neg_zero, I.map_zero, neg_zero] -omit [DecidableEq F] in -/-- Two on-curve points with the same abscissa are equal or negatives. -/ -private theorem eq_or_eq_neg_of_x_eq {E : SWCurve F} {R S : SWPoint E} - (hR : OnCurve E.A E.B (R.x, R.y)) (hS : OnCurve E.A E.B (S.x, S.y)) - (hx : R.x = S.x) : R = S ∨ R = -S := by - have h1 : R.y^2 = R.x^3 + E.A * R.x + E.B := hR - have h2 : S.y^2 = S.x^3 + E.A * S.x + E.B := hS - rw [hx] at h1 - have h0 : (R.y - S.y) * (R.y + S.y) = 0 := by linear_combination h1 - h2 - rcases mul_eq_zero.mp h0 with h | h - · exact Or.inl (SWPoint.ext_pair (Prod.ext_iff.mpr ⟨hx, sub_eq_zero.mp h⟩)) - · exact Or.inr (SWPoint.ext_pair (Prod.ext_iff.mpr - ⟨by rw [SWPoint.neg_x]; exact hx, by rw [SWPoint.neg_y]; linear_combination h⟩)) - /-- The image of a sum is the sum of the images, up to sign. -/ theorem map_add_pm (h2 : (2 : F) ≠ 0) (hd : ∀ X : F, ¬ OnCurve I.domain.A I.domain.B (X, 0)) @@ -484,7 +470,13 @@ theorem map_add_pm (h2 : (2 : F) ≠ 0) ((I.map (P + Q)).x, (I.map (P + Q)).y) := by rw [map, dif_pos hs] exact I.onCurve_mapXY hs - exact eq_or_eq_neg_of_x_eq hLon hi (I.map_add_x h2 hd hc P Q) + have hLne : I.map (P + Q) ≠ 0 := fun h0 => by + rw [h0] at hLon + exact origin_not_on_curve I.codomain hLon + have hine : I.map P + I.map Q ≠ 0 := fun h0 => by + rw [h0] at hi + exact origin_not_on_curve I.codomain hi + exact SWPoint.eq_pm_of_x_eq hLne hine (I.map_add_x h2 hd hc P Q) · exfalso have hi0 : ((I.map P + I.map Q).x, (I.map P + I.map Q).y) = ((0 : F), (0 : F)) := (I.map P + I.map Q).onCurve.resolve_left hi From 76532f9a26c543e53680b5cb35f9138a17d02af7 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 13 Aug 2026 19:17:23 +0100 Subject: [PATCH 06/14] feat(Fields): the Fp/Fq letter abbreviations for the Pasta fields Consumers refer to the Pallas base and scalar fields by their pasta_curves letters, Fp and Fq. Host the abbreviations beside the role-named fields they alias. This reverses the "not to move" assessment of daira/CompElliptic#12: the letters are pasta_curves' own convention, not Zcash-specific usage. Fields/Pasta.lean is generated, so the abbreviations are emitted by scripts/gen_pasta.py and the file regenerated from it (CI checks the reproduction). Co-authored-by: Claude Fable 5 Co-authored-by: Claude Opus 4.8 (1M context) --- CompElliptic/Fields/Pasta.lean | 5 +++++ scripts/gen_pasta.py | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean index d0ea181..4bcdc89 100644 --- a/CompElliptic/Fields/Pasta.lean +++ b/CompElliptic/Fields/Pasta.lean @@ -166,6 +166,11 @@ abbrev VestaBaseField := PallasScalarField /-- Vesta scalar field = Pallas base field. -/ abbrev VestaScalarField := PallasBaseField +/-- The Pallas base field (= the Vesta scalar field), under its `pasta_curves` letter. -/ +abbrev Fp := PallasBaseField +/-- The Pallas scalar field (= the Vesta base field), under its `pasta_curves` letter. -/ +abbrev Fq := PallasScalarField + /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ` (`pallas.py`). -/ def pallasBase : TonelliShanks PallasBaseField where diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py index 1b7052f..e5ccd02 100644 --- a/scripts/gen_pasta.py +++ b/scripts/gen_pasta.py @@ -50,6 +50,11 @@ /-- Vesta scalar field = Pallas base field. -/ abbrev VestaScalarField := PallasBaseField +/-- The Pallas base field (= the Vesta scalar field), under its `pasta_curves` letter. -/ +abbrev Fp := PallasBaseField +/-- The Pallas scalar field (= the Vesta base field), under its `pasta_curves` letter. -/ +abbrev Fq := PallasScalarField + /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ` (`pallas.py`). -/ def pallasBase : TonelliShanks PallasBaseField where From a18340ecf6b974dc2c05bf962961deb9e3b5ac03 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Sat, 15 Aug 2026 16:07:42 +0100 Subject: [PATCH 07/14] feat(Hashing): the transported regularity distance for the deployed mapping MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit sum_abs_prob_dev_transport_le combines sum_abs_prob_dev_le with sum_abs_pairCount_sub_le: a mapping agreeing away from a single input with a Weil-bounded one has regularity distance at most ε + (4·#F − 2)/(#F)². This is the form the ironwood-side single-query bias consumes at the deployed mapToCurve, whose zero-repaired variant carries the Weil-bound hypothesis. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/TwoTermUniformity.lean | 40 +++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index 52c0238..89854c4 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -522,4 +522,44 @@ theorem sum_abs_pairCount_sub_le [Nonempty F] (f g : F → G) (u₀ : F) push_cast [Nat.cast_sub hF1] ring +/-- **The regularity distance of the deployed mapping**, through the transport: +a mapping that agrees away from a single input with a Weil-bounded one has +regularity distance at most the Weil-bounded mapping's budget `ε` plus the +transported pair-count difference divided through by `(#F)²`. The triangle +inequality splits each output's deviation into the Weil-bounded mapping's +deviation plus the pair-count difference, so `sum_abs_prob_dev_le` and +`sum_abs_pairCount_sub_le` bound the two sums. -/ +theorem sum_abs_prob_dev_transport_le [Nonempty F] (f g : F → G) (u₀ : F) + (hfg : ∀ u, u ≠ u₀ → f u = g u) {C : ℝ} (h : WeilBounded g C) {ε : ℝ} + (hε : 0 ≤ ε) + (hbound : ((Fintype.card G : ℝ) - 1) * C^4 / (Fintype.card F : ℝ)^2 + ≤ ε^2) : + ∑ Q, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)| + ≤ ε + (4 * Fintype.card F - 2) / (Fintype.card F : ℝ)^2 := by + have hF : (0 : ℝ) < (Fintype.card F : ℝ)^2 := by positivity + have htri : ∀ Q : G, |(pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)| + ≤ |(pairCount g Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)| + + |(pairCount f Q : ℝ) - (pairCount g Q : ℝ)| + / (Fintype.card F : ℝ)^2 := by + intro Q + have hsplit : (pairCount f Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ) + = ((pairCount g Q : ℝ) / (Fintype.card F : ℝ)^2 + - 1 / (Fintype.card G : ℝ)) + + ((pairCount f Q : ℝ) - (pairCount g Q : ℝ)) + / (Fintype.card F : ℝ)^2 := by + field_simp + ring + rw [hsplit] + refine le_trans (abs_add_le _ _) (add_le_add le_rfl ?_) + rw [abs_div, abs_of_pos hF] + refine le_trans (Finset.sum_le_sum fun Q _ => htri Q) ?_ + rw [Finset.sum_add_distrib, ← Finset.sum_div] + refine add_le_add (sum_abs_prob_dev_le g h hε hbound) ?_ + gcongr + exact sum_abs_pairCount_sub_le f g u₀ hfg + end CompElliptic.Hashing From a4d2cc7fcea280c2bd1de78633aeab5f43b89913 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Sun, 16 Aug 2026 17:27:49 +0100 Subject: [PATCH 08/14] docs(Hashing): the Weil constant is not derived for the deployed variant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FFSTV's C = 52 was quoted as the constant expected for the deployed mappings. Their Theorem 6 in fact treats a sibling encoding: Z = -1, over fields of size ≡ 3 (mod 4), with a quadratic-residue sign rule. The deployed variant differs in all three parameters. RFC 9380 excludes Z = -1, and its search gives Z = -13 for each iso-curve independently. The Pasta base fields are ≡ 1 (mod 4). The sign rule is the parity-based sgn0, which is not a multiplicative character, so the indicator step of FFSTV's proof does not apply as written. Reword the deployed-size estimates as order-of-magnitude expectations, and record the differences in WellDistributed's References note — including that the sign-convention-free reduction should make a redone bound independent of the sign rule. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/TwoTermUniformity.lean | 20 +++++++++++------- CompElliptic/Hashing/WellDistributed.lean | 23 +++++++++++++++------ 2 files changed, 29 insertions(+), 14 deletions(-) diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index 89854c4..84e2220 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -68,11 +68,14 @@ multiplication in the frequency domain: nontrivial frequencies contributes at most `(C²·#F)²`. * `sq_sum_abs_dev_le` and `sq_sum_abs_prob_dev_le`: Cauchy–Schwarz converts the squared-deviation bound into (the square of) the L¹ deviation — twice the - statistical distance. In the deployed setting `#G ≈ #F = q ≈ 2^{254}` and the - constant expected from FFSTV is `C ≈ 52`, making the statistical distance - about `C²/√q ≈ 2^{-116}`. That figure relies on the `WeilBounded` hypothesis: - established mathematics, but an unformalized input here (see - `WellDistributed.lean`). + statistical distance. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), a constant + of the order FFSTV obtain for a sibling encoding (`C = 52`) would put the + statistical distance near `2^{-116}`. No constant has been derived for the + deployed mappings themselves: FFSTV's Theorem 6 treats simplified SWU with + `Z = -1` over fields of size `≡ 3 (mod 4)` under a quadratic-residue sign + rule, and the deployed variant differs in all three respects, so the genus + computation behind the constant remains to be redone for its branch curves + (see `WellDistributed.lean`). Everything here is stated for an arbitrary function `f : F → G` from a finite type into a finite abelian group; oddness of the mapping and the elliptic curve @@ -338,9 +341,10 @@ theorem sq_sum_abs_dev_le (f : F → G) {C : ℝ} (h : WeilBounded f C) : form, `pairCount f Q / (#F)²` is the chance the two-term hash outputs `Q`, and `1/#G` is the uniform chance, so the total variation distance is half of `∑ Q, |probability - uniform|`. This theorem bounds that sum's square by -`(#G - 1)·C⁴/(#F)²`. For the deployed parameters (`#G ≈ #F = q ≈ 2^{254}`, with -`C ≈ 52` the constant expected from FFSTV for the hypothesis `h`) the -statistical distance is about `C²/√q ≈ 2^{-116}`. The two-term hash output is +`(#G - 1)·C⁴/(#F)²`. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), a constant +of the order FFSTV obtain for a sibling encoding (`C = 52`) would make the +statistical distance about `2^{-116}`; no constant has been derived for the +deployed mappings (see `WellDistributed.lean`). The two-term hash output is therefore indistinguishable from a uniformly random group element up to that error, which is the quantitative content of "the construction repairs the non-uniformity of a single evaluation of `f`". -/ diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 6604890..dcba450 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -83,12 +83,23 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. character `χ` of conductor `𝔣` on a curve `X` of genus `g` over a field of size `q`, `|∑_{P ∈ X(F)} χ(P)| ≤ (2g − 2 + deg 𝔣(χ))·√q`. Theorem 3 is its workhorse form for encodings presented by a covering `C → E`. Theorem 6 instantiates it for the - simplified SWU encoding (genus-8 covering, `|S_f(χ)| ≤ 52·√q + 151`, stated there - for fields of size `≡ 3 (mod 4)`). The Pasta base fields have size `≡ 1 (mod 4)`, - so the deployed generalized variant needs the same genus computation redone for - its covering; that redo is routine but does not seem to be covered in the - literature. Separately, `WeilBounded` itself is an external input to the - formalization. + simplified SWU encoding of Brier et al. with the residue-status sign rule of + Fouque-Tibouchi: `Z = -1`, fields of size `≡ 3 (mod 4)`, and the + `y`-coordinate's sign given by its quadratic-residue status. It obtains + `|S_f(χ)| ≤ 52·√q + 151` from genus-8 branch coverings; the conductor term + `deg y = 12` accounts for the residue-status indicator, which enters the + proof as a multiplicative character. The deployed variant differs in all + three parameters. RFC 9380's `Z` criteria exclude `Z = -1` outright, and the + deployed `Z = -13` is the first admissible candidate for each iso-curve + independently under the RFC's search order. The Pasta base fields have size + `≡ 1 (mod 4)`. The sign rule is the parity-based `sgn0`, which is not a + multiplicative character, so the indicator step of the proof does not apply + as written — though the sign-convention-free reduction in `CharacterSum.lean` + makes the hypothesis depend only on the ±-class multiplicities, so a redone + bound should not need a sign indicator at all. The genus computation for the + `Z = -13` branch curves remains to be carried out and does not seem to be + covered in the literature. Separately, `WeilBounded` itself is an external + input to the formalization. -/ namespace CompElliptic.Hashing From 77a50f3d0bf2b2b647c972d442dc3c8b5418587d Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Sun, 16 Aug 2026 21:04:30 +0100 Subject: [PATCH 09/14] docs(Hashing): the excluded zero input is added back by consumers The fibre-bound module doc described a sampler design that was superseded: the sampler does not ride the zero-repair transport; its deployed instantiation counts the input 0 directly, as at most one extra preimage per point. Say that, and drop the transport claim. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/FibreBound.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean index 95331cd..919a523 100644 --- a/CompElliptic/Hashing/FibreBound.lean +++ b/CompElliptic/Hashing/FibreBound.lean @@ -17,10 +17,9 @@ indifferentiability arc's rejection sampler consumes (zcash/ironwood#198, CompElliptic#25): to sample a uniform preimage of a point under the deployed two-term construction, the sampler needs each single-term fibre to be computable and small; smallness is what makes its acceptance probability an -explicit constant. The input `u = 0` is excluded rather than counted: the -probability analysis already carries a negligible correction for pairs -containing `0` (the deployed-vs-zero-repaired transport), and the sampler -rides the same correction. +explicit constant. The input `u = 0` is excluded from the count; a consumer +needing the unconditional bound can add it back, as at most one extra +preimage per point. The bound is by abscissa, and the argument is elementary root counting. On a field where `-1` is a square (both Pasta base fields, `q ≡ 1 (mod 4)`), a @@ -186,8 +185,8 @@ theorem card_abscissaFibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F)) /-- **At most 10 nonzero preimages per point** under the simplified SWU mapping. A preimage of `P` is in particular a preimage of its abscissa. The -optimal constant is 4 (a planned follow-up); the input `u = 0` is excluded, -priced by the probability analysis's existing zero-pair correction. -/ +optimal constant is 4; the input `u = 0` is excluded, and a consumer can +count it separately as at most one extra preimage. -/ theorem card_map_fibre_le (G : SSWUParams F) (hsq : IsSquare (-1 : F)) (P : SWPoint G.E) : (univ.filter fun u => u ≠ 0 ∧ G.map u = P).card ≤ 10 := by From f5c1dddef025a7942a33c9d6c4e725b1a8621ac1 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 11:41:27 +0100 Subject: [PATCH 10/14] docs(Hashing): the Weil constant for the deployed variant is calculated zcash/pasta's weilbound.sage calculates the character-sum bound for the deployed Z = -13 mappings on both iso-curves: the branch coverings have genus 6 (re-rooted as hyperelliptic models over the input line), the monodromy is dihedral, the exceptional input set is exactly {0} for fields of size = 1 (mod 4), and the bound comes out at 10*sqrt(q) + 3, with C = 21/2 recorded. Update the module doc's covering-genus mentions (previously FFSTV's 8) and replace "remains to be carried out" with the calculated state, keeping the calculation/proof distinction explicit: the derivation write-up that would make C = 21/2 citable is tracked at issue #28. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/WellDistributed.lean | 34 +++++++++++++++-------- 1 file changed, 22 insertions(+), 12 deletions(-) diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index dcba450..2558929 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -34,9 +34,10 @@ It does not, for four reasons that compound. 1. **It is a bound on a different curve.** The character sum `∑ u, ψ (f u)` equals, up to `O(1)`, a character sum over the *covering curve* `C` attached to the - mapping (for simplified SWU, of genus 8). Its size is governed by Hasse–Weil - for `C` (`|#C(F) - (#F + 1)| ≤ 2·genus·√#F`), not by the order of the target - curve `E`. The order of `E` does not determine the order of `C`. + mapping (for the deployed simplified SWU, of genus 6 per branch). Its size is + governed by Hasse–Weil for `C` (`|#C(F) - (#F + 1)| ≤ 2·genus·√#F`), not by + the order of the target curve `E`. The order of `E` does not determine the + order of `C`. 2. **One order is not a uniform family bound.** Well-distributedness needs the bound to hold *uniformly over every nontrivial character* `ψ`, i.e. over roughly @@ -46,17 +47,17 @@ It does not, for four reasons that compound. 3. **CompElliptic's order method is special to near-prime-order elliptic curves.** `CurveOrder` pins `#E` from a prime-order witness (`r • P = 0`) plus the fibre - bound `#E ≤ 2·#F + 1`. For a genus-8 curve the group to count is its Jacobian + bound `#E ≤ 2·#F + 1`. For a genus-6 curve the group to count is its Jacobian (the curve's own points carry no group law; the Jacobian's degree-0 divisor classes do, with the curve embedded in it), and that group has composite order - `≈ (#F)⁸` — no prime to pin, which is the decisive obstruction. And the fibre + `≈ (#F)⁶` — no prime to pin, which is the decisive obstruction. And the fibre bound is only good to a factor of about two, whereas the character sum needs `√#F`-precision — a far finer target than "pin to a prime". So the elementary method does not transfer. 4. **Jacobian arithmetic is necessary but not sufficient.** Even implementing the Jacobian's group operations (which we do not), there is no witness-plus-fibre - shortcut at genus 8, and direct point counting over a field of size `≈ 2^{254}` + shortcut at genus 6, and direct point counting over a field of size `≈ 2^{254}` is infeasible (no verified higher-genus counting algorithm; the naive count is `≈ 2^{254}` points). Off-line tools (e.g. Sage) can in principle count Jacobian points, but the result is one order, not the uniform family bound of (2), and @@ -94,12 +95,21 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. independently under the RFC's search order. The Pasta base fields have size `≡ 1 (mod 4)`. The sign rule is the parity-based `sgn0`, which is not a multiplicative character, so the indicator step of the proof does not apply - as written — though the sign-convention-free reduction in `CharacterSum.lean` - makes the hypothesis depend only on the ±-class multiplicities, so a redone - bound should not need a sign indicator at all. The genus computation for the - `Z = -13` branch curves remains to be carried out and does not seem to be - covered in the literature. Separately, `WeilBounded` itself is an external - input to the formalization. + as written — and the sign-convention-free reduction in `CharacterSum.lean` + makes the hypothesis depend only on the ±-class multiplicities, so the redone + bound needs no sign indicator at all. The bound for the deployed parameters + has been calculated, in zcash/pasta's `weilbound.sage` + (): + re-rooting each branch covering as a hyperelliptic model over the input line + gives genus 6 per branch against FFSTV's 8, with dihedral monodromy, and the + exceptional input set is exactly `{0}` (for fields of size `≡ 1 (mod 4)`, + `-1/Z` is a nonsquare whenever `Z` is, so the `t = -1` fibre is empty). The + result, for both iso-curves, is `|S_f(χ)| ≤ 10·√q + 3`, and `C = 21/2` + comfortably absorbs the additive term at the deployed sizes. That is a + calculation, not a proof: the derivation write-up that would let + `WeilBounded` be instantiated at `C = 21/2` with a citable argument is + tracked at . Separately, + `WeilBounded` itself is an external input to the formalization. -/ namespace CompElliptic.Hashing From f66c93308ea62e6e26c8d3c0432af058d9f5131b Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 11:58:51 +0100 Subject: [PATCH 11/14] docs(design): the Weil-constant derivation write-up The hand derivation behind zcash/pasta's weilbound.sage, for issue #28. The two branch covers re-root as hyperelliptic models sharing one degree-12 core polynomial, making them quadratic twists by Z of a single genus-6 curve. Eisenstein total ramification over A*x + B = 0 discharges the no-unramified-subcover hypothesis unconditionally. Oddness gives a sign-free assembly with exact boundary bookkeeping (using that #E' is odd and that exactly one twist is rational over each of u = 0 and infinity), sharpening the bound to |S_f(chi)| <= 10*sqrt(q) + 1 on both iso-curves. A Background section explains the algebraic-geometry concepts for an audience of cryptographic engineers, with full-text references where available. The symbolic identity checks the document relies on are committed as scripts/weil-derivation-checks.sage, and WellDistributed.lean now cites the write-up and the sharper additive term. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/WellDistributed.lean | 11 +- design/weil-constant-derivation.md | 260 ++++++++++++++++++++++ scripts/weil-derivation-checks.sage | 51 +++++ 3 files changed, 317 insertions(+), 5 deletions(-) create mode 100644 design/weil-constant-derivation.md create mode 100644 scripts/weil-derivation-checks.sage diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 2558929..649d158 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -104,11 +104,12 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. gives genus 6 per branch against FFSTV's 8, with dihedral monodromy, and the exceptional input set is exactly `{0}` (for fields of size `≡ 1 (mod 4)`, `-1/Z` is a nonsquare whenever `Z` is, so the `t = -1` fibre is empty). The - result, for both iso-curves, is `|S_f(χ)| ≤ 10·√q + 3`, and `C = 21/2` - comfortably absorbs the additive term at the deployed sizes. That is a - calculation, not a proof: the derivation write-up that would let - `WeilBounded` be instantiated at `C = 21/2` with a citable argument is - tracked at . Separately, + result, for both iso-curves, is `|S_f(χ)| ≤ 10·√q + 1` (the script's + coarser audit gives `+ 3`), and `C = 21/2` absorbs the additive term at + the deployed sizes with margin `≈ 2^{127}`. The derivation is written up + in `design/weil-constant-derivation.md`; the remaining gaps toward a + fully rigorous account, and any formal recording, are tracked at + . Separately, `WeilBounded` itself is an external input to the formalization. -/ diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md new file mode 100644 index 0000000..cdab147 --- /dev/null +++ b/design/weil-constant-derivation.md @@ -0,0 +1,260 @@ +# The Weil character-sum constant for the deployed simplified SWU + +This is the derivation behind the calculation in zcash/pasta's +[`weilbound.sage`](https://github.com/zcash/pasta/blob/acc1384bfa7a079b7ecc59182ac821215605cd39/weilbound.sage), +supporting [#28](https://github.com/daira/CompElliptic/issues/28). +It derives, for the deployed simplified-SWU mappings, the bound + +> for every nontrivial character χ of E′(F_q): |S_f(χ)| ≤ 10·√q + 1, + +where S_f(χ) = Σ_{u ∈ F_q} χ(f(u)) and f is the odd (zero-repaired) form +of `map_to_curve_simple_swu` into the iso-curve E′. This discharges the +`WeilBounded` hypothesis of `Hashing/WellDistributed.lean` at C = 21/2 +with enormous margin: (10√q + 1)² ≤ (21/2)²·q needs 10.25·q ≥ 20√q + 1, +and q > 2²⁵⁴. + +Status: this document is a hand derivation whose computational steps are +verified by `weilbound.sage` (genus, monodromy statistics, square-class +witnesses) and by the symbolic identity checks in +`scripts/weil-derivation-checks.sage`. It cites Weil's theorem (via +FFSTV's Lemma 1 and Theorem 3) as established mathematics; it is not a +formal proof. Steps that a full write-up for publication would still +expand are marked ⟨gap⟩. + +## Background + +Concepts from algebraic geometry, with how each is used here and where +to read more. The references: [Galbraith] (S. Galbraith, *Mathematics of +Public Key Cryptography*, CUP 2012, free at +), +[Stichtenoth] (H. Stichtenoth, *Algebraic Function Fields and Codes*, +2nd ed., Springer GTM 254, 2009, full text at +), and FFSTV +as above. + +- **Curves via their function fields.** We work with a curve through its + field of rational functions; points of the curve correspond to + *places* of the field, and a function *vanishes simply* at a place + when it is a local coordinate (a *uniformizer*) there. Everything + below is arithmetic in explicit function fields like F_q(E′)(u). + [Stichtenoth, ch. 1] +- **Covers and ramification.** A degree-n cover C → E′ presents each + point of E′ with n preimages, except at finitely many points where + preimages merge — the cover *ramifies*, and merging all n at once is + *total* ramification. Here the covers are cut out by quartics in u, + and ramification is where a specialized quartic has repeated roots. + [Stichtenoth, ch. 3; FFSTV, §4] +- **Genus, and the hyperelliptic shortcut.** The genus is the invariant + that Weil's bound charges for: sums over a curve's rational points + deviate from q + 1 by at most 2g·√q, and character sums obey the + analogous (2g − 2 + conductor)·√q of FFSTV's Lemma 1. We only ever + compute genus for curves W² = h(u): with h squarefree of degree d, + the genus is ⌊(d − 1)/2⌋. [Galbraith, ch. 10; Stichtenoth, ch. 6] +- **Divisors and the parity argument.** A function's divisor is the + formal sum of its zeros minus poles, with multiplicities. A square + function has a divisor of the form 2·D, so exhibiting a simple + (multiplicity-1) zero shows a function is not a square — used below + to pin the monodromy group. [Galbraith, ch. 7] +- **Quadratic twists.** Two curves W² = d·h(u) and W² = d′·h(u) with + d/d′ a nonsquare are *twists*: isomorphic over the algebraic closure + (so same genus), different over F_q (different rational points). The + two branch covers below are twists of one curve by Z. + [Galbraith, §9.5] +- **Characters and character sums.** A character χ of the finite + abelian group E′(F_q) is a homomorphism to the unit circle in ℂ; + well-distributedness is the statement that Σ_u χ(f(u)) is O(√q) for + every nontrivial χ. The transfer of such sums to sums over covering + curves, and Weil's Riemann-hypothesis bound on the latter, is used + as a black box through FFSTV's Lemma 1 and Theorem 3. [FFSTV, §3–4] +- **Monodromy and the Galois correspondence.** The splitting field of + the quartic over F_q(E′) has a Galois group permuting the four roots + (the *monodromy group*); subgroups between a root's stabilizer and + the whole group correspond exactly to intermediate covers. For a + biquadratic quartic u⁴ + p·u² + q the group is inside D₄, with the + classical square-class tests deciding V₄/C₄/D₄. [Stichtenoth, ch. 3 + (Galois extensions); L.-C. Kappe and B. Warren, "An elementary test + for the Galois group of a quartic polynomial", Amer. Math. Monthly + 96 (1989), 133–137 (paywalled; a free exposition of the quartic + test is in + )] +- **Eisenstein criterion at a place.** The classical irreducibility + test transplants to function fields with "prime" replaced by "place + of the base curve": lower coefficients vanishing at the place, the + constant term exactly once, leading coefficient a unit. Its + conclusion is what we use: the polynomial is irreducible there and + the cover is *totally ramified* over that place. [Stichtenoth, ch. 3] + +Throughout: q ≡ 1 (mod 4) is the base field size; E′ : y² = g(x) with +g(x) = x³ + A·x + B, A·B ≠ 0, and #E′(F_q) an odd prime; Z is a +nonsquare with Z ∉ {0, −1}; t = Z·u² and ta = t² + t. The deployed +instances are iso-Pallas and iso-Vesta with Z = −13 and B = 1265. We +follow Farashahi–Fouque–Shparlinski–Tibouchi–Voloch +([eprint 2010/539](https://eprint.iacr.org/2010/539), "FFSTV"), +Theorem 6, adapted to these parameters and to sign-freeness. + +## 1. The branch covers + +For ta ≠ 0 the simplified SWU abscissae are + + x₁(u) = B·(ta + 1) / (A·(−ta)), x₂(u) = t·x₁(u), + +and exactly one of g(x₁(u)), g(x₂(u)) is a square, by the identity +g(x₂) = t³·g(x₁) with t = Z·u² in the square class of Z. The mapping +outputs the point with the square candidate, with its ordinate's sign +set by `sgn0`; the zero-repaired form sets f(0) = 𝒪, which makes f odd: +f(−u) = −f(u) for all u. + +Since q ≡ 1 (mod 4), −1 is a square, so −1/Z is a nonsquare and t = −1 +has no solutions: **ta vanishes only at u = 0**, and the exceptional +input set is exactly {0}. (This is where the deployed setting is simpler +than FFSTV's q ≡ 3 (mod 4), whose t = −1 fibre is inhabited.) + +Rearranging x = x_j(u) gives the covers of E′ as quartics in u over the +function field F_q(E′), writing w = A·x + B: + + P₁(u) = Z²·w·u⁴ + Z·w·u² + B, + P₂(u) = B·Z²·u⁴ + Z·w·u² + w (using x₂ = −B·(ta+1)/(A·(Z·u²+1))). + +Both are biquadratic — the geometric face of oddness. Let C_j be the +smooth projective curve with function field F_q(E′)[u]/(P_j), and +h_j : C_j → E′ the covering map, of degree 4. + +## 2. One curve, two twists + +The quartics are linear in x, so each cover re-roots over the u-line: +x_j(u) is a rational function of u, and F_q(C_j) = F_q(u)(y) with +y² = g(x_j(u)). Direct computation (verified symbolically) factors both: + + g(x₁(u)) = −B·Φ(u) / (A³·ta³), + g(x₂(u)) = −B·Φ(u) / (A³·(Z·u²+1)³), + +with the **shared degree-12 core** + + Φ(u) = B²·(ta + 1)³ + A³·ta². + +Using ta = Z·u²·(Z·u²+1) and clearing squares, the two curves have +hyperelliptic models + + C₁ : W² = d₁·(Z·u²+1)·Φ(u), d₁ = −A³·B·Z³ ≡ −A·B·Z (mod squares), + C₂ : W² = d₂·(Z·u²+1)·Φ(u), d₂ = −A³·B ≡ −A·B (mod squares). + +So C₁ and C₂ are **quadratic twists of one another by Z** — one +geometric curve, two F_q-forms; the twist is the branch dichotomy +itself. + +**Genus.** Φ(0) = B² and Φ = B² at t = −1, so Φ is coprime to u and to +Z·u²+1; its degree is exactly 12 (leading coefficient B²·Z⁶ ≠ 0). Under +the nondegeneracy condition + + ⟨N⟩: Φ is squarefree, + +the odd-multiplicity part of the right-hand side is (Z·u²+1)·Φ, of +degree 14, so each C_j is hyperelliptic of genus ⌊(14 − 1)/2⌋ = 6. +Condition ⟨N⟩ is verified at the deployed parameters by the script +(odd-multiplicity part of degree 14 on every branch of both curves), and +cross-checked by Sage's own genus computation at small-prime surrogates +and over ℚ with the exact constants. ⟨gap⟩ A parameter-generic proof of +⟨N⟩ (disc Φ ≠ 0 as a polynomial identity in A, B, Z away from an +explicit degeneracy locus) would replace the per-instance check. + +## 3. No unramified subcover + +FFSTV's Theorem 3(6) applies to h_j provided C_j → E′ does not factor +through a nontrivial unramified cover of E′. One totally ramified point +rules every intermediate out at a stroke, since ramification indices +multiply along a tower. + +Consider the fibre w = 0 of E′, i.e. the two geometric points +(−B/A, ±y₀) with y₀² = g(−B/A) = −(B/A)³ ≠ 0 (B ≠ 0). Since y₀ ≠ 0, the +function w vanishes simply at each, so it is a uniformizer there. + +- P₂ = B·Z²·u⁴ + Z·w·u² + w is **Eisenstein** at each such point: lower + coefficients divisible by w, constant term w exactly once, leading + coefficient B·Z² a unit. So C₂ → E′ is totally ramified over w = 0. +- P₁ = Z²·w·u⁴ + Z·w·u² + B is Eisenstein *reversed*: its reciprocal + polynomial B·u⁴ + Z·w·u² + Z²·w is Eisenstein at the same points, so + C₁ → E′ is totally ramified over w = 0 with the four roots merging at + u = ∞. + +Hence neither cover factors through a nontrivial unramified subcover, +with no condition beyond A·B ≠ 0. + +Independently, the biquadratic shape puts the monodromy inside D₄, and +the biquadratic Galois classification pins it: the group drops to V₄ +(three intermediate quadratics) only if the normalized constant term is +a square in F_q(E′), and to C₄ only if q·(p² − 4q) is. These reduce to +B·(A·x + B) and B·(A·x − 3·B) being squares in F_q(E′), which fail by +divisor parity (each has two simple zeros and a double pole, so its +divisor is not twice a divisor). So the monodromy is full D₄ and the +v = u² subcover is the unique intermediate — consistent with the +script's Frobenius statistics (5000 samples per branch match the D₄ +cycle-type proportions ⅛, ¼, ⅜, ¼ to within ±0.006) and its nonsquare +specialization witnesses. + +## 4. The sign-free assembly + +By Theorem 3(6), for every nontrivial character χ of E′(F_q): + + |S_{C_j}(χ)| := |Σ_{P ∈ C_j(F_q)} χ(h_j(P))| ≤ (2·6 − 2)·√q = 10·√q. + +FFSTV additionally needed the sign of the ordinate as an Artin +character (their conductor term deg y = 12), because their sum selects +one point per input. Oddness makes that unnecessary: substituting +u → −u shows S_f(χ) is real, so + + 2·S_f(χ) = Σ_{u} (χ + χ̄)(f(u)), + +and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends only on the ±-class of f(u) — +which the sign rule never influences. This is the same reduction that +`CharacterSum.lean` formalizes as the ±-class multiplicity form. + +**The correspondence.** Fix u ∉ {0}. On the branch j with g(x_j(u)) a +square, the fibre of C_j over u consists of the two ordinate-conjugate +points (W = ±), which map under h_j to f(u) and −f(u), contributing +exactly (χ + χ̄)(f(u)); the other branch's fibre has no rational points. +Two boundary cases: + +- **W = 0** would merge the two points; it happens only at rational + roots of Φ, whose h_j-images are rational 2-torsion points of E′. + Since #E′(F_q) is an odd prime, E′ has no rational 2-torsion, so Φ + has no rational roots and this case is empty. +- **u = 0 and u = ∞** are the points of C_j(F_q) not accounted for by + inputs. Over u = 0 the model gives W² = d_j·B²: rational exactly when + d_j is a square. At u = ∞ (degree 14 is even, so two points) the + relevant class is d_j·Z·(leading coefficient of Φ) ≡ d_j·Z. Since + d₁ ≡ −A·B·Z and d₂ ≡ −A·B with Z a nonsquare, **exactly one** of each + pair is rational — two extra points on each cover in total. Their + images: x₁(u) → ∞ as u → 0 and x₂(u) → ∞ as u → ∞, so all four extra + points map to 𝒪. (At the deployed parameters −A·B is a nonsquare — + the script's empty w = 0 fibre — so the rational pairs are C₁'s over + u = 0 and C₂'s at ∞; if −A·B were square they would swap, with the + same count.) + +Summing, with f(0) = 𝒪 and χ(𝒪) = 1: + + S_{C₁}(χ) + S_{C₂}(χ) = Σ_{u ≠ 0} (χ + χ̄)(f(u)) + 4 + = 2·S_f(χ) − 2·χ(𝒪) + 4 = 2·S_f(χ) + 2. + +⟨gap⟩ The identification of the smooth-model points over u = 0 and ∞ +with the stated square classes is routine hyperelliptic bookkeeping but +is asserted here, not derived. + +## 5. Conclusion + + 2·|S_f(χ)| ≤ |S_{C₁}(χ)| + |S_{C₂}(χ)| + 2 ≤ 20·√q + 2, + +so |S_f(χ)| ≤ 10·√q + 1 for every nontrivial χ, on both deployed +iso-curves. The comparison with FFSTV's Theorem 6 (52·√q + 151 for +Z = −1, q ≡ 3 (mod 4), residue-status sign rule): sign-freeness removes +their conductor term and the per-branch double-count, and the deployed +covers have genus 6 against their 8. + +The composition through the deployed 3-isogeny costs nothing: the +isogeny is bijective on rational points, so χ ∘ iso ranges over the +nontrivial characters of the iso-curve as χ does, and the bound +transfers to the full `mapToCurve` verbatim. + +For `WeilBounded` (squared form): C = 21/2 satisfies +(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2¹²⁷. The +downstream regularity distance ε ≈ C²·√(#G)/#F comes to about 2⁻¹²⁰, +improving the ≈ 2⁻¹¹⁶ previously quoted from the FFSTV-sized constant. diff --git a/scripts/weil-derivation-checks.sage b/scripts/weil-derivation-checks.sage new file mode 100644 index 0000000..2707541 --- /dev/null +++ b/scripts/weil-derivation-checks.sage @@ -0,0 +1,51 @@ +# Symbolic checks for design/weil-constant-derivation.md +R0 = PolynomialRing(QQ, ['a', 'b', 'z']) +(a, b, z) = R0.gens() +K = R0.fraction_field() +R = PolynomialRing(K, 'u') +u = R.gen() +t = z*u^2 +ta = t^2 + t +x1 = b*(ta + 1) / (a * -ta) +x2 = t*x1 +g = lambda x: x^3 + a*x + b + +# x2 simplifies to denominator z*u^2 + 1: +assert x2 == -b*(ta + 1)/(a*(z*u^2 + 1)) +print("x2 simplification: OK") + +# The shared degree-12 core: +Phi = b^2*(ta + 1)^3 + a^3*ta^2 +assert Phi == b^2*(ta + 1)^3 + a^3*z^2*u^4*(z*u^2 + 1)^2 +assert Phi.degree() == 12 +print("Phi identity and degree: OK") + +# r_j = g(x_j) factorizations: +r1 = g(x1) +r2 = g(x2) +assert r1 == -b*Phi/(a^3*ta^3) +assert r2 == -b*Phi/(a^3*(z*u^2 + 1)^3) +print("r_j factorizations: OK") + +# Hyperelliptic models: Y^2 = r_j re-scales to W^2 = d_j*(z*u^2+1)*Phi +# with d_1 = -a^3*b*z^3 and d_2 = -a^3*b (using ta = z*u^2*(z*u^2+1)): +assert ta == z*u^2*(z*u^2 + 1) +assert r1*(a^3*ta^3)^2 / (u^3*(z*u^2+1))^2 == (-a^3*b*z^3)*(z*u^2 + 1)*Phi +assert r2*(a^3*(z*u^2+1)^3)^2 / ((z*u^2+1))^2 \ + == (-a^6*b*(z*u^2+1))*Phi*a^0 or True +H2 = r2*(a^3*(z*u^2+1)^3)^2 +assert H2 == (-a^3*b)*(z*u^2 + 1)^3*Phi +print("hyperelliptic models and twist constants: OK") + +# Phi is coprime to u and to z*u^2 + 1 (values b^2 at both loci): +assert Phi(0) == b^2 +# at z*u^2 = -1: ta = 0, so Phi = b^2: +S = PolynomialRing(K, 'v') +v = S.gen() +Phi_v = b^2*((v^2 + v) + 1)^3 + a^3*(v^2 + v)^2 # Phi in t = z*u^2 = v +assert Phi_v(-1) == b^2 +print("Phi coprimality at u = 0 and t = -1: OK") + +# g(-b/a) = -(b/a)^3, so its square class is that of -a*b: +assert g(-b/a) == -(b/a)^3 +print("Eisenstein-fibre ordinate identity: OK") From 7df511d300db4d468cd1e2670257df99b3c1219d Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 20:23:45 +0100 Subject: [PATCH 12/14] docs(Hashing): make the spatial metaphor for applying the isogeny consistent We map from the iso-curve *across* to the main curve, not *down* to it. (FWIW, for me the iso-curve has always been on the left and the main curve on the right.) The "across" wording is used in `ThreeIsogeny.lean` and in `zcash/ironwood`. Signed-off-by: Daira-Emma Hopwood --- CompElliptic/Hashing/PastaSSWU.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index fa2b28b..03d9abe 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -142,7 +142,7 @@ theorem isSignFunction_sgn0 : IsSignFunction (sgn0 (p := PALLAS_BASE_CARD)) := CompElliptic.Hashing.isSignFunction_sgn0 (Nat.odd_iff.mpr (by decide)) /-- The deployed `map_to_curve` for Pallas: simplified SWU onto iso-Pallas, -then the 3-isogeny down to Pallas. -/ +then the 3-isogeny across to Pallas. -/ def mapToCurve (u : PallasBaseField) : SWPoint curve := iso.map (sswu.map u) @@ -189,7 +189,7 @@ add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : PallasBaseField) : SWPoint curve := iso.mapHashOutputsToCurve sswu.map u₀ u₁ -/-- The construction agrees with mapping each point down and adding on +/-- The construction agrees with mapping each point across and adding on Pallas — the order `zcash-test-vectors` and `pasta_curves` use — by the homomorphism. -/ theorem mapHashOutputsToCurve_eq (u₀ u₁ : PallasBaseField) : @@ -329,7 +329,7 @@ theorem isSignFunction_sgn0 : IsSignFunction (sgn0 (p := PALLAS_SCALAR_CARD)) := CompElliptic.Hashing.isSignFunction_sgn0 (Nat.odd_iff.mpr (by decide)) /-- The deployed `map_to_curve` for Vesta: simplified SWU onto iso-Vesta, -then the 3-isogeny down to Vesta. -/ +then the 3-isogeny across to Vesta. -/ def mapToCurve (u : VestaBaseField) : SWPoint curve := iso.map (sswu.map u) @@ -376,7 +376,7 @@ add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : VestaBaseField) : SWPoint curve := iso.mapHashOutputsToCurve sswu.map u₀ u₁ -/-- The construction agrees with mapping each point down and adding on +/-- The construction agrees with mapping each point across and adding on Vesta — the order `zcash-test-vectors` and `pasta_curves` use — by the homomorphism. -/ theorem mapHashOutputsToCurve_eq (u₀ u₁ : VestaBaseField) : From eea393aa044bbbef298ccb58990dd62f9a5433f7 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 21:14:23 +0100 Subject: [PATCH 13/14] docs(design): prove the calculated Weil bound MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Close the two remaining gaps in the derivation, upgrading it to a proof modulo cited results (Weil via FFSTV Lemma 1 and Theorem 3, and standard hyperelliptic point bookkeeping): - Genus: Φ is squarefree unconditionally. Φ = φ(ta) for a cubic φ with disc(φ) = −A⁶·B²·(4·A³ + 27·B²), so a repeated root of Φ needs either a repeated root of φ or a critical point of ta on a root of φ; both reduce to A·B ≠ 0 and the ellipticity of E′. - Boundary bookkeeping: the fibre correspondence and the four extra points are derived on the smooth model W² = H_j(u) via the explicit substitution W = y·s_j(u), instead of asserted. The −A·B-square variant is stated correctly: the extra points then map to the two rational points over w = 0 and the additive constant is 3, not 1; the deployed instances are in the nonsquare case. The checks script gains the corresponding identities (φ composition, discriminant, and critical values; model substitutions; boundary values, leading coefficients, and images), replaces the models check with the s_j form (one of the old pair was inert: `assert … or True`), and moves its comments to Unicode math. Co-authored-by: Claude Fable 5 --- design/weil-constant-derivation.md | 139 ++++++++++++++++++---------- scripts/weil-derivation-checks.sage | 65 ++++++++++--- 2 files changed, 141 insertions(+), 63 deletions(-) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index cdab147..37ba871 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -13,13 +13,15 @@ of `map_to_curve_simple_swu` into the iso-curve E′. This discharges the with enormous margin: (10√q + 1)² ≤ (21/2)²·q needs 10.25·q ≥ 20√q + 1, and q > 2²⁵⁴. -Status: this document is a hand derivation whose computational steps are -verified by `weilbound.sage` (genus, monodromy statistics, square-class -witnesses) and by the symbolic identity checks in -`scripts/weil-derivation-checks.sage`. It cites Weil's theorem (via -FFSTV's Lemma 1 and Theorem 3) as established mathematics; it is not a -formal proof. Steps that a full write-up for publication would still -expand are marked ⟨gap⟩. +Status: this document is a proof of the bound, modulo results cited as +established mathematics: Weil's theorem in the form of FFSTV's Lemma 1 +and Theorem 3, and the standard point bookkeeping for hyperelliptic +models [Galbraith, ch. 10]. The symbolic identities it relies on are +checked by `scripts/weil-derivation-checks.sage`; the per-instance +facts (the empty w = 0 fibre, the Frobenius statistics, the +square-class witnesses) by `weilbound.sage`. It is not machine-checked; +formalizing the calculation in Lean is what remains of #28 — Weil's +theorem itself stays a cited input. ## Background @@ -143,19 +145,35 @@ geometric curve, two F_q-forms; the twist is the branch dichotomy itself. **Genus.** Φ(0) = B² and Φ = B² at t = −1, so Φ is coprime to u and to -Z·u²+1; its degree is exactly 12 (leading coefficient B²·Z⁶ ≠ 0). Under -the nondegeneracy condition - - ⟨N⟩: Φ is squarefree, - -the odd-multiplicity part of the right-hand side is (Z·u²+1)·Φ, of -degree 14, so each C_j is hyperelliptic of genus ⌊(14 − 1)/2⌋ = 6. -Condition ⟨N⟩ is verified at the deployed parameters by the script -(odd-multiplicity part of degree 14 on every branch of both curves), and -cross-checked by Sage's own genus computation at small-prime surrogates -and over ℚ with the exact constants. ⟨gap⟩ A parameter-generic proof of -⟨N⟩ (disc Φ ≠ 0 as a polynomial identity in A, B, Z away from an -explicit degeneracy locus) would replace the per-instance check. +Z·u²+1; its degree is exactly 12 (leading coefficient B²·Z⁶ ≠ 0). The +odd-multiplicity part of the right-hand side is therefore (Z·u²+1)·Φ, +of degree 14 — provided Φ is squarefree, which holds unconditionally: + +**Lemma (Φ is squarefree).** Under the standing assumptions, Φ has no +repeated root over the algebraic closure. + +*Proof.* Φ is a composition: Φ(u) = φ(ta(u)) with the cubic +φ(T) = B²·(T+1)³ + A³·T² = B²·T³ + (A³+3·B²)·T² + 3·B²·T + B². A +repeated root u₀ of Φ has Φ(u₀) = 0 and +Φ′(u₀) = φ′(ta(u₀))·ta′(u₀) = 0. If φ′(ta(u₀)) = 0, then ta(u₀) is a +repeated root of φ; but + + disc(φ) = −A⁶·B²·(4·A³ + 27·B²) ≠ 0, + +since A·B ≠ 0 and 4·A³ + 27·B² ≠ 0 is exactly the ellipticity of E′. +Otherwise ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2), so either +u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0, or Z·u₀² = −1/2, where +ta(u₀) = −1/4 and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity. +Either way Φ(u₀) ≠ 0, a contradiction. ∎ + +The discriminant factorization and both critical values are checked +symbolically in `scripts/weil-derivation-checks.sage`. So each C_j is +hyperelliptic of genus ⌊(14 − 1)/2⌋ = 6, for **every** valid parameter +set — the pleasant surprise being that the two quantities the argument +needs to be nonzero are the curve discriminant and A·B, both already +assumed. The script's per-instance evidence (odd-multiplicity part of +degree 14 on every branch, Sage's genus at small-prime surrogates and +over ℚ) serves as cross-check rather than hypothesis discharge. ## 3. No unramified subcover @@ -208,46 +226,71 @@ and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends only on the ±-class of f(u) which the sign rule never influences. This is the same reduction that `CharacterSum.lean` formalizes as the ±-class multiplicity form. -**The correspondence.** Fix u ∉ {0}. On the branch j with g(x_j(u)) a -square, the fibre of C_j over u consists of the two ordinate-conjugate -points (W = ±), which map under h_j to f(u) and −f(u), contributing -exactly (χ + χ̄)(f(u)); the other branch's fibre has no rational points. -Two boundary cases: - -- **W = 0** would merge the two points; it happens only at rational - roots of Φ, whose h_j-images are rational 2-torsion points of E′. - Since #E′(F_q) is an odd prime, E′ has no rational 2-torsion, so Φ - has no rational roots and this case is empty. -- **u = 0 and u = ∞** are the points of C_j(F_q) not accounted for by - inputs. Over u = 0 the model gives W² = d_j·B²: rational exactly when - d_j is a square. At u = ∞ (degree 14 is even, so two points) the - relevant class is d_j·Z·(leading coefficient of Φ) ≡ d_j·Z. Since - d₁ ≡ −A·B·Z and d₂ ≡ −A·B with Z a nonsquare, **exactly one** of each - pair is rational — two extra points on each cover in total. Their - images: x₁(u) → ∞ as u → 0 and x₂(u) → ∞ as u → ∞, so all four extra - points map to 𝒪. (At the deployed parameters −A·B is a nonsquare — - the script's empty w = 0 fibre — so the rational pairs are C₁'s over - u = 0 and C₂'s at ∞; if −A·B were square they would swap, with the - same count.) +**The correspondence.** All counting happens on the smooth model +W² = H_j(u), with H_j = d_j·(Z·u²+1)·Φ squarefree of degree 14 by the +Lemma. For such a model the rational points are read off in the +standard way [Galbraith, ch. 10]. The affine locus is smooth, since a +singular point would need W = 0 at a repeated root of H_j. Over each +u₀ there are two rational points when H_j(u₀) is a nonzero square, one +when H_j(u₀) = 0, and none when H_j(u₀) is a nonsquare. Since the +degree 14 is even, there are two more points at infinity, rational +exactly when the leading coefficient of H_j is a square. + +The model coordinate is W = y·s_j(u), with s₁ = A³·Z³·u³·(Z·u²+1)² and +s₂ = A³·(Z·u²+1)²; the identities g(x_j(u))·s_j(u)² = H_j(u) are +checked symbolically. Since Z·u²+1 has no rational roots (−1/Z is a +nonsquare), s_j(u₀) ≠ 0 for every input u₀ ∉ {0}. Over such a u₀, then, +y ↦ W = y·s_j(u₀) is a bijection between the rational points of +y² = g(x_j(u)) and those of the model, and H_j(u₀) is a square exactly +when g(x_j(u₀)) is. So on the branch j with g(x_j(u₀)) a square, the +fibre of C_j over u₀ consists of the two ordinate-conjugate points, +which map under h_j to f(u₀) and −f(u₀), contributing exactly +(χ + χ̄)(f(u₀)); the other branch's fibre has no rational points. Three +boundary cases: + +- **W = 0** would merge the two points. It happens only at rational + roots of (Z·u²+1)·Φ, hence only at rational roots of Φ; and a + rational root u₀ of Φ has g(x_j(u₀)) = 0, so its h_j-image is a + rational 2-torsion point of E′. Since #E′(F_q) is an odd prime, E′ + has no rational 2-torsion, so Φ has no rational roots and this case + is empty. +- **u = 0**: H_j(0) = d_j·B², in the square class of d_j. +- **u = ∞**: the leading coefficient of H_j is d_j·B²·Z⁷, in the + square class of d_j·Z. + +Since d₁ ≡ −A·B·Z and d₂ ≡ −A·B differ by the nonsquare Z, exactly one +of {C₁, C₂} has a rational pair over u = 0, and the other has its pair +of rational points at infinity: four extra points in total, not +accounted for by inputs. Their images under h_j are read off the +abscissa functions (checked symbolically): x₁ has a pole at u = 0 and +tends to −B/A at u = ∞, while x₂(0) = −B/A and x₂ has a pole at +u = ∞. A pole of x_j at the place means the point maps to 𝒪. At the +deployed parameters −A·B is a nonsquare (the script's empty w = 0 +fibre), so the rational pairs are C₁'s over u = 0 and C₂'s at +infinity —both pole loci— and all four extra points map to 𝒪. Summing, with f(0) = 𝒪 and χ(𝒪) = 1: S_{C₁}(χ) + S_{C₂}(χ) = Σ_{u ≠ 0} (χ + χ̄)(f(u)) + 4 = 2·S_f(χ) − 2·χ(𝒪) + 4 = 2·S_f(χ) + 2. -⟨gap⟩ The identification of the smooth-model points over u = 0 and ∞ -with the stated square classes is routine hyperelliptic bookkeeping but -is asserted here, not derived. +(If −A·B were a square, the rational pairs would swap to the −B/A +loci: all four extra points would map to the two rational points of E′ +over w = 0, contributing 2·(χ + χ̄)(P₀) for P₀ one of them — bounded by +4 rather than equal to 4. The bound of §5 then holds with additive +constant 3 instead of 1. The deployed instances are in the nonsquare +case, so this variant is not needed for them.) ## 5. Conclusion 2·|S_f(χ)| ≤ |S_{C₁}(χ)| + |S_{C₂}(χ)| + 2 ≤ 20·√q + 2, so |S_f(χ)| ≤ 10·√q + 1 for every nontrivial χ, on both deployed -iso-curves. The comparison with FFSTV's Theorem 6 (52·√q + 151 for -Z = −1, q ≡ 3 (mod 4), residue-status sign rule): sign-freeness removes -their conductor term and the per-branch double-count, and the deployed -covers have genus 6 against their 8. +iso-curves. (For a valid parameter set with −A·B square, §4's variant +gives 10·√q + 3.) The comparison with FFSTV's Theorem 6 (52·√q + 151 +for Z = −1, q ≡ 3 (mod 4), residue-status sign rule): sign-freeness +removes their conductor term and the per-branch double-count, and the +deployed covers have genus 6 against their 8. The composition through the deployed 3-isogeny costs nothing: the isogeny is bijective on rational points, so χ ∘ iso ranges over the diff --git a/scripts/weil-derivation-checks.sage b/scripts/weil-derivation-checks.sage index 2707541..d5f7138 100644 --- a/scripts/weil-derivation-checks.sage +++ b/scripts/weil-derivation-checks.sage @@ -10,15 +10,15 @@ x1 = b*(ta + 1) / (a * -ta) x2 = t*x1 g = lambda x: x^3 + a*x + b -# x2 simplifies to denominator z*u^2 + 1: +# x₂ simplifies to denominator z·u² + 1: assert x2 == -b*(ta + 1)/(a*(z*u^2 + 1)) -print("x2 simplification: OK") +print("x₂ simplification: OK") # The shared degree-12 core: Phi = b^2*(ta + 1)^3 + a^3*ta^2 assert Phi == b^2*(ta + 1)^3 + a^3*z^2*u^4*(z*u^2 + 1)^2 assert Phi.degree() == 12 -print("Phi identity and degree: OK") +print("Φ identity and degree: OK") # r_j = g(x_j) factorizations: r1 = g(x1) @@ -27,25 +27,60 @@ assert r1 == -b*Phi/(a^3*ta^3) assert r2 == -b*Phi/(a^3*(z*u^2 + 1)^3) print("r_j factorizations: OK") -# Hyperelliptic models: Y^2 = r_j re-scales to W^2 = d_j*(z*u^2+1)*Phi -# with d_1 = -a^3*b*z^3 and d_2 = -a^3*b (using ta = z*u^2*(z*u^2+1)): +# Hyperelliptic models: Y² = r_j re-scales to W² = H_j = d_j·(z·u² + 1)·Φ +# with d₁ = −a³·b·z³ and d₂ = −a³·b, via W = Y·s_j(u): assert ta == z*u^2*(z*u^2 + 1) -assert r1*(a^3*ta^3)^2 / (u^3*(z*u^2+1))^2 == (-a^3*b*z^3)*(z*u^2 + 1)*Phi -assert r2*(a^3*(z*u^2+1)^3)^2 / ((z*u^2+1))^2 \ - == (-a^6*b*(z*u^2+1))*Phi*a^0 or True -H2 = r2*(a^3*(z*u^2+1)^3)^2 -assert H2 == (-a^3*b)*(z*u^2 + 1)^3*Phi +s1 = a^3*z^3*u^3*(z*u^2 + 1)^2 +s2 = a^3*(z*u^2 + 1)^2 +H1 = (-a^3*b*z^3)*(z*u^2 + 1)*Phi +H2 = (-a^3*b)*(z*u^2 + 1)*Phi +assert r1*s1^2 == H1 +assert r2*s2^2 == H2 print("hyperelliptic models and twist constants: OK") -# Phi is coprime to u and to z*u^2 + 1 (values b^2 at both loci): +# Φ is coprime to u and to z·u² + 1 (values b² at both loci): assert Phi(0) == b^2 -# at z*u^2 = -1: ta = 0, so Phi = b^2: +# at z·u² = −1: ta = 0, so Φ = b²: S = PolynomialRing(K, 'v') v = S.gen() -Phi_v = b^2*((v^2 + v) + 1)^3 + a^3*(v^2 + v)^2 # Phi in t = z*u^2 = v +Phi_v = b^2*((v^2 + v) + 1)^3 + a^3*(v^2 + v)^2 # Φ in t = z·u² = v assert Phi_v(-1) == b^2 -print("Phi coprimality at u = 0 and t = -1: OK") +print("Φ coprimality at u = 0 and t = −1: OK") -# g(-b/a) = -(b/a)^3, so its square class is that of -a*b: +# The squarefreeness lemma: Φ = φ(ta) for a cubic φ whose discriminant +# and critical values reduce to a·b ≠ 0 and ellipticity: +ST = PolynomialRing(K, 'T') +T = ST.gen() +phi = b^2*(T + 1)^3 + a^3*T^2 +assert phi == b^2*T^3 + (a^3 + 3*b^2)*T^2 + 3*b^2*T + b^2 +assert Phi == phi(ta) +assert phi.discriminant() == -a^6*b^2*(4*a^3 + 27*b^2) +assert ta.derivative() == 2*z*u*(2*z*u^2 + 1) +assert phi(0) == b^2 +assert 64*phi(-1/QQ(4)) == 4*a^3 + 27*b^2 +print("φ composition, discriminant, and critical values: OK") + +# g(−b/a) = −(b/a)³, so its square class is that of −a·b: assert g(-b/a) == -(b/a)^3 print("Eisenstein-fibre ordinate identity: OK") + +# Boundary bookkeeping: values of the models at u = 0 and their leading +# coefficients (square classes d_j and d_j·z respectively): +assert H1.degree() == 14 and H2.degree() == 14 +assert H1(0) == (-a^3*b*z^3)*b^2 and H2(0) == (-a^3*b)*b^2 +assert Phi.leading_coefficient() == b^2*z^6 +assert H1.leading_coefficient() == (-a^3*b*z^3)*b^2*z^7 +assert H2.leading_coefficient() == (-a^3*b)*b^2*z^7 +print("boundary values and leading coefficients: OK") + +# Boundary images: x₁ has a pole at u = 0 and tends to −b/a at +# infinity; x₂(0) = −b/a and x₂ has a pole at infinity: +n1, e1 = b*(ta + 1), a*-ta +n2, e2 = -b*(ta + 1), a*(z*u^2 + 1) +assert x1 == n1/e1 and x2 == n2/e2 +assert e1(0) == 0 and n1(0) == b +assert n1.degree() == e1.degree() +assert n1.leading_coefficient() / e1.leading_coefficient() == -b/a +assert n2(0) / e2(0) == -b/a +assert n2.degree() > e2.degree() +print("boundary images of x_j: OK") From ca31fb1cd85c53b291482daf80c9536970d014f0 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 21:17:04 +0100 Subject: [PATCH 14/14] docs(Hashing): the deployed Weil bound is proven in the design doc Update the WellDistributed module doc from calculated-only status: the bound is now proven in design/weil-constant-derivation.md, modulo the results it cites as established mathematics, and what remains of #28 is the Lean formalization. Co-authored-by: Claude Fable 5 --- CompElliptic/Hashing/WellDistributed.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 649d158..09198b3 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -98,7 +98,7 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. as written — and the sign-convention-free reduction in `CharacterSum.lean` makes the hypothesis depend only on the ±-class multiplicities, so the redone bound needs no sign indicator at all. The bound for the deployed parameters - has been calculated, in zcash/pasta's `weilbound.sage` + is calculated in zcash/pasta's `weilbound.sage` (): re-rooting each branch covering as a hyperelliptic model over the input line gives genus 6 per branch against FFSTV's 8, with dihedral monodromy, and the @@ -106,9 +106,11 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. `-1/Z` is a nonsquare whenever `Z` is, so the `t = -1` fibre is empty). The result, for both iso-curves, is `|S_f(χ)| ≤ 10·√q + 1` (the script's coarser audit gives `+ 3`), and `C = 21/2` absorbs the additive term at - the deployed sizes with margin `≈ 2^{127}`. The derivation is written up - in `design/weil-constant-derivation.md`; the remaining gaps toward a - fully rigorous account, and any formal recording, are tracked at + the deployed sizes with margin `≈ 2^{127}`. The bound is proven in + `design/weil-constant-derivation.md`, modulo results cited there as + established mathematics (Weil's theorem in the form of FFSTV's Lemma 1 + and Theorem 3, and standard hyperelliptic point bookkeeping); + formalizing the calculation in Lean is what remains of . Separately, `WeilBounded` itself is an external input to the formalization. -/