diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6153a11..b2f5756 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -73,17 +73,19 @@ jobs: - name: Fail if the regenerated files differ from the committed ones run: git diff --exit-code CompElliptic/Fields/Pasta.lean CompElliptic/Fields/Jubjub.lean - velu-certificates: - name: Vélu certificates reproduce + sage-checks: + name: sage checks - Vélu certificates and Weil-derivation identities runs-on: ubuntu-latest steps: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: persist-credentials: false - # Sage pinned to the version that generated the committed certificates: - # Singular's `lift` output (the emitted cofactors) can differ between - # versions, so byte-reproducibility needs the same engine as the local - # regeneration. + # One environment for all sage steps. Sage is pinned to the version that + # generated the committed certificates: Singular's `lift` output (the + # emitted cofactors) can differ between versions, so byte-reproducibility + # needs the same engine as the local regeneration. (The Weil-derivation + # checks are exact symbolic assertions over ℚ(a, b, z), so any engine + # verifies those.) - uses: mamba-org/setup-micromamba@f457c30a868e4760d3a6fcea5f25dc655b8edf39 # v3.2.1 with: environment-name: sage @@ -97,6 +99,12 @@ jobs: run: sage scripts/gen_velu_certificates.sage - name: Fail if the regenerated section differs from the committed one run: git diff --exit-code CompElliptic/Isogenies/VeluCertificates.lean + - name: Check the design doc's symbolic identities and certificates + shell: bash -el {0} + run: sage scripts/check_weil_derivations.sage + - name: Confirm the branch statistics on small curves + shell: bash -el {0} + run: sage scripts/check_sswu_small_curves.sage native-lane: name: FastFieldNative lane is core-only @@ -108,6 +116,16 @@ jobs: - name: Check the precompiled lane's import closure run: scripts/check_native_lane.sh + weil-support-refs: + name: design doc lists the Weil supporting facts exactly + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: + persist-credentials: false + - name: Check the doc's references against WeilSupport.lean and the census + run: scripts/check_weil_support_refs.py + csimp-census: name: csimp lemmas are axiom-censused runs-on: ubuntu-latest diff --git a/CompElliptic.lean b/CompElliptic.lean index 47774e4..3922c20 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -19,10 +19,13 @@ import CompElliptic.Isogenies.ThreeIsogeny import CompElliptic.Curves.Pasta import CompElliptic.Curves.IsoPasta import CompElliptic.Curves.PastaOrder +import CompElliptic.Hashing.BranchCovers import CompElliptic.Hashing.CharacterSum import CompElliptic.Hashing.PastaSSWU import CompElliptic.Hashing.SignedLift import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.TwoTermUniformity +import CompElliptic.Hashing.WeilInstance +import CompElliptic.Hashing.WeilSupport import CompElliptic.Hashing.WellDistributed import CompElliptic.TrustBoundary diff --git a/CompElliptic/Fields/Jubjub.lean b/CompElliptic/Fields/Jubjub.lean index 6f9dcd8..bc8d06d 100644 --- a/CompElliptic/Fields/Jubjub.lean +++ b/CompElliptic/Fields/Jubjub.lean @@ -19,11 +19,13 @@ base field (the BLS12-381 scalar field) are not defined here. namespace CompElliptic.Fields.Jubjub --- Jubjub scalar field ℓ (the prime-order subgroup order). +/-- The order `ℓ` of the Jubjub scalar field (the prime-order subgroup order). -/ @[reducible] def JUBJUB_SCALAR_CARD : Nat := 0xe7db4ea6533afa906673b0101343b00a6682093ccc81082d0970e5ed6f72cb7 +/-- The Jubjub scalar field `F_ℓ`. -/ abbrev JubjubScalarField := ZMod JUBJUB_SCALAR_CARD +/-- `ℓ` is prime, by a Pratt certificate. -/ theorem JUBJUB_SCALAR_is_prime : Nat.Prime JUBJUB_SCALAR_CARD := by unfold JUBJUB_SCALAR_CARD refine PrattCertificate'.out (p := 6554484396890773809930967563523245729705921265872317281365359162392183254199) ⟨6, (by reduce_mod_char), ?_⟩ diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean index 4bcdc89..489a4f8 100644 --- a/CompElliptic/Fields/Pasta.lean +++ b/CompElliptic/Fields/Pasta.lean @@ -19,11 +19,13 @@ factorizations of `p-1` and `q-1` (PARI/GP); see also https://github.com/zcash/p namespace CompElliptic.Fields.Pasta --- Pallas base field p (= Vesta scalar field). +/-- The order `p` of the Pallas base field (= the Vesta scalar field). -/ @[reducible] def PALLAS_BASE_CARD : Nat := 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001 +/-- The Pallas base field `F_p` (= the Vesta scalar field). -/ abbrev PallasBaseField := ZMod PALLAS_BASE_CARD +/-- `p` is prime, by a Pratt certificate. -/ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by unfold PALLAS_BASE_CARD refine PrattCertificate'.out (p := 28948022309329048855892746252171976963363056481941560715954676764349967630337) ⟨5, (by reduce_mod_char), ?_⟩ @@ -90,11 +92,13 @@ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by instance : Fact (Nat.Prime PALLAS_BASE_CARD) := ⟨PALLAS_BASE_is_prime⟩ instance : Field PallasBaseField := ZMod.instField PALLAS_BASE_CARD --- Pallas scalar field q (= Vesta base field). +/-- The order `q` of the Pallas scalar field (= the Vesta base field). -/ @[reducible] def PALLAS_SCALAR_CARD : Nat := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001 +/-- The Pallas scalar field `F_q` (= the Vesta base field). -/ abbrev PallasScalarField := ZMod PALLAS_SCALAR_CARD +/-- `q` is prime, by a Pratt certificate. -/ theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by unfold PALLAS_SCALAR_CARD refine PrattCertificate'.out (p := 28948022309329048855892746252171976963363056481941647379679742748393362948097) ⟨5, (by reduce_mod_char), ?_⟩ diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean new file mode 100644 index 0000000..287eed8 --- /dev/null +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -0,0 +1,736 @@ +/- +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.FibreBound + +/-! +# The branch covers of the simplified SWU mapping + +Away from the exceptional input, the simplified SWU mapping offers two +candidate abscissae `x₁ u` and `x₂ u`, and outputs a point over whichever one +makes the curve equation `g x = x³ + A·x + B` a square. This file gives each +branch its hyperelliptic model: the curve equation at the branch abscissa, +cleared of denominators. Writing `ta = (Z·u²)² + Z·u²`, both branches share +the degree-12 core + +`Φ(u) = B²·(ta + 1)³ + A³·ta²` (`phiCore`), + +and the two models are `W² = d_j·(Z·u²+1)·Φ(u)` (`model1`, `model2`) with +twist constants `d₁ = -A³·B·Z³` and `d₂ = -A³·B` (`twist1`, `twist2`). The +main identities `model1_eq` and `model2_eq` state that the model value is +the curve equation at the branch abscissa times the square of an explicit +scaling (`scale1`, `scale2`). `g_x2_eq` is the branch dichotomy in algebraic +form: `g (x₂ u) = (Z·u²)³ · g (x₁ u)`. + +The notation follows `design/weil-constant-derivation.md` §2, which derives +the Weil character-sum bound for the deployed mappings from these models; +`WeilInstance.lean` assembles the formal consumption. + +On a field where `-1` is a square (both Pasta base fields), `Z·u² + 1` never +vanishes (`Zuu_add_one_ne_zero`), so the scalings vanish only at `u = 0` and +the models are nonzero wherever `Φ` is. + +`modelPoints1`/`modelPoints2` collect each cover's rational points in model +coordinates, as a `Finset ((F × F) ⊕ Bool)`. `Sum.inl` carries an affine +model point `(u, W)`, so each set holds the affine solutions of +`W² = H_j(u)`. The models have even degree 14, so each smooth model also +has two points at infinity; they are rational —and included, as +`Sum.inr false` and `Sum.inr true`— exactly when the leading square class +`d_j·Z` is a square. + +The `Bool` is a bare tag: the two points at infinity +are the conjugate pair of places over `u = ∞`, swapped by the hyperelliptic +involution, and the formalization fixes no correspondence between the tags +and the places. Only the pair's cardinality and its common image `𝒪` enter +any statement, so every result is invariant under swapping the tags, and +the cited input's faithfulness needs only some bijection — which either +labelling provides. + +`cover1Map`/`cover2Map` send a model point to the curve: +* an affine point over `u ≠ 0` goes to the point with abscissa `x_j u` and + ordinate `W / s_j u`; +* everything else goes to `𝒪`: the `u = 0` fibre, the points at infinity, + and junk values off the model. + +On the parameter range the derivation targets (`-A·B` a nonsquare, which +holds at the deployed instantiations) the points at infinity genuinely map +to `𝒪`. The correspondence theorems carry that hypothesis. +-/ + +namespace CompElliptic.Hashing + +open Finset CompElliptic.CurveForms.ShortWeierstrass + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] + +/-- The first branch abscissa `x₁ u = B·(ta + 1) / (A·(-ta))`, the value +`(G.mapXYUpToSign u).1` takes when the square-root split chooses the first +branch (and `ta ≠ 0`). -/ +def x1 (G : SSWUParams F) (u : F) : F := + G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1) + / (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + +/-- The second branch abscissa `x₂ u = Z·u² · x₁ u`. -/ +def x2 (G : SSWUParams F) (u : F) : F := G.Z * u^2 * G.x1 u + +/-- The shared degree-12 core `Φ(u) = B²·(ta + 1)³ + A³·ta²` of the two +branch models, with `ta = (Z·u²)² + Z·u²`. -/ +def phiCore (G : SSWUParams F) (u : F) : F := + G.E.B^2 * (((G.Z * u^2)^2 + G.Z * u^2) + 1)^3 + + G.E.A^3 * ((G.Z * u^2)^2 + G.Z * u^2)^2 + +/-- The twist constant `d₁ = -A³·B·Z³` of the first branch model. -/ +def twist1 (G : SSWUParams F) : F := -(G.E.A^3 * G.E.B * G.Z^3) + +/-- The twist constant `d₂ = -A³·B` of the second branch model. `twist1` and +`twist2` differ by `Z³`, which is `Z` times a square: the two models are +quadratic twists of one another by the nonsquare `Z`. -/ +def twist2 (G : SSWUParams F) : F := -(G.E.A^3 * G.E.B) + +/-- The first branch model `H₁(u) = d₁·(Z·u²+1)·Φ(u)`. -/ +def model1 (G : SSWUParams F) (u : F) : F := + G.twist1 * (G.Z * u^2 + 1) * G.phiCore u + +/-- The second branch model `H₂(u) = d₂·(Z·u²+1)·Φ(u)`. -/ +def model2 (G : SSWUParams F) (u : F) : F := + G.twist2 * (G.Z * u^2 + 1) * G.phiCore u + +/-- The scaling `s₁ u = A³·Z³·u³·(Z·u²+1)²` relating the first branch's +ordinate to the model coordinate: `W = y·s₁ u` on the first cover. -/ +def scale1 (G : SSWUParams F) (u : F) : F := + G.E.A^3 * G.Z^3 * u^3 * (G.Z * u^2 + 1)^2 + +/-- The scaling `s₂ u = A³·(Z·u²+1)²` relating the second branch's ordinate +to the model coordinate: `W = y·s₂ u` on the second cover. -/ +def scale2 (G : SSWUParams F) (u : F) : F := + G.E.A^3 * (G.Z * u^2 + 1)^2 + +/-- On a field where `-1` is a square, `Z·u² + 1` never vanishes: a root +would exhibit the nonsquare `Z` as `-1` times a square. This is the +exceptional-set lemma of the derivation: the `t = -1` fibre of the branch +covers has no rational points. -/ +theorem Zuu_add_one_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) + (u : F) : G.Z * u^2 + 1 ≠ 0 := by + intro h + rcases eq_or_ne u 0 with rfl | hu + · simp at h + · obtain ⟨s, hs⟩ := hsq + have hZu : G.Z * u^2 = -1 := by linear_combination h + 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) + +/-- `Φ(0) = B²`: the core is nonzero at `u = 0`. -/ +theorem phiCore_zero (G : SSWUParams F) : G.phiCore 0 = G.E.B^2 := by + simp [phiCore] + +/-- The first model at `u = 0` is `d₁·B²`, in the square class of `d₁`. -/ +theorem model1_zero (G : SSWUParams F) : G.model1 0 = G.twist1 * G.E.B^2 := by + simp [model1, phiCore_zero] + +/-- The second model at `u = 0` is `d₂·B²`, in the square class of `d₂`. -/ +theorem model2_zero (G : SSWUParams F) : G.model2 0 = G.twist2 * G.E.B^2 := by + simp [model2, phiCore_zero] + +/-- The first scaling vanishes exactly at `u = 0` (on a field where `-1` is +a square). -/ +theorem scale1_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) {u : F} + (hu : u ≠ 0) : G.scale1 u ≠ 0 := by + unfold scale1 + exact mul_ne_zero (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 3 G.Z_nonzero)) (pow_ne_zero 3 hu)) + (pow_ne_zero 2 (G.Zuu_add_one_ne_zero hsq u)) + +/-- The second scaling never vanishes (on a field where `-1` is a square). -/ +theorem scale2_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) (u : F) : + G.scale2 u ≠ 0 := by + unfold scale2 + exact mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 2 (G.Zuu_add_one_ne_zero hsq u)) + +section ClearedIdentities + +variable (G : SSWUParams F) + +/-- The defining equation of `x₁ u`, cleared of its denominator: +`x₁ u · (A·(-ta)) = B·(ta + 1)`. -/ +theorem x1_mul_den (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + = G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1) := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + unfold x1 + exact div_mul_cancel₀ _ hden + +/-- **The first branch model identity**: the curve equation at `x₁ u`, times +the square of the scaling `s₁ u`, is the model value `H₁(u)`. Away from +`u = 0` the scaling is nonzero, so `H₁(u)` and `g (x₁ u)` are in the same +square class. -/ +theorem model1_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) * (G.scale1 u)^2 = G.model1 u := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold scale1 model1 twist1 phiCore + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination ((G.E.A^3 * G.Z^3 * u^3 * (G.Z * u^2 + 1)^2)^2 * + ((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + +/-- **The second branch model identity**: the curve equation at `x₂ u`, times +the square of the scaling `s₂ u`, is the model value `H₂(u)`. The scaling is +nowhere zero, so `H₂(u)` and `g (x₂ u)` are in the same square class at every +`u ≠ 0`. -/ +theorem model2_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + ((G.x2 u)^3 + G.E.A * G.x2 u + G.E.B) * (G.scale2 u)^2 = G.model2 u := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold x2 scale2 model2 twist2 phiCore + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination ((G.E.A^3 * (G.Z * u^2 + 1)^2)^2 * + ((G.Z * u^2)^3 + * ((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2) + + G.E.A * (G.Z * u^2) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + +/-- **The branch dichotomy, in algebraic form**: the curve equation at `x₂ u` +is `(Z·u²)³` times the curve equation at `x₁ u`. The factor +`(Z·u²)³ = Z·(Z·u³)²` is `Z` times a nonzero square for `u ≠ 0`, so exactly +one of the two curve-equation values is a square whenever both are nonzero. -/ +theorem g_x2_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B + = (G.Z * u^2)^3 * ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold x2 + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination (G.E.A * (G.Z * u^2) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2 * (1 - (G.Z * u^2)^2)) * hX + +end ClearedIdentities + +section ModelPoints + +variable (G : SSWUParams F) + +include G in +/-- A nonsquare exists only in odd characteristic: in characteristic 2 every +element of a finite field is a square, against `Z_nonsquare`. -/ +theorem ringChar_ne_two : ringChar F ≠ 2 := fun h => + G.Z_nonsquare (FiniteField.isSquare_of_char_two h G.Z) + +/-- The first twist constant is nonzero. -/ +theorem twist1_ne_zero : G.twist1 ≠ 0 := by + unfold twist1 + exact neg_ne_zero.mpr (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + G.E.B_nonzero) (pow_ne_zero 3 G.Z_nonzero)) + +/-- The second twist constant is nonzero. -/ +theorem twist2_ne_zero : G.twist2 ≠ 0 := by + unfold twist2 + exact neg_ne_zero.mpr (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) G.E.B_nonzero) + +/-- The first model never vanishes. At `u = 0` its value is `d₁·B² ≠ 0`. At +`u ≠ 0`, a zero would put the zero-ordinate point `(x₁ u, 0)` on the curve, +which the no-2-torsion hypothesis `hy0` excludes. So the model's rational +points never have `W = 0`: the merged boundary case of the derivation is +empty. -/ +theorem model1_ne_zero (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) (u : F) : + G.model1 u ≠ 0 := by + rcases eq_or_ne u 0 with rfl | hu + · rw [G.model1_zero] + exact mul_ne_zero G.twist1_ne_zero (pow_ne_zero 2 G.E.B_nonzero) + · intro h + rcases mul_eq_zero.mp ((G.model1_eq hsq hu).trans h) with hg | hs + · exact hy0 (G.x1 u) (by simpa [OnCurve] using hg.symm) + · exact pow_ne_zero 2 (G.scale1_ne_zero hsq hu) hs + +/-- The second model never vanishes; see `model1_ne_zero`. -/ +theorem model2_ne_zero (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) (u : F) : + G.model2 u ≠ 0 := by + rcases eq_or_ne u 0 with rfl | hu + · rw [G.model2_zero] + exact mul_ne_zero G.twist2_ne_zero (pow_ne_zero 2 G.E.B_nonzero) + · intro h + rcases mul_eq_zero.mp ((G.model2_eq hsq hu).trans h) with hg | hs + · exact hy0 (G.x2 u) (by simpa [OnCurve] using hg.symm) + · exact pow_ne_zero 2 (G.scale2_ne_zero hsq u) hs + +/-- The point set of the first cover, in model coordinates: the affine +solutions of `W² = H₁(u)`, plus the two points at infinity —tagged by a +bare `Bool`, since neither has a distinguished coordinate— exactly when +the leading square class `d₁·Z` is a square. -/ +def modelPoints1 : Finset ((F × F) ⊕ Bool) := + ((univ.filter fun p : F × F => p.2^2 = G.model1 p.1).image Sum.inl) + ∪ (if IsSquare (G.twist1 * G.Z) then {Sum.inr false, Sum.inr true} else ∅) + +/-- The point set of the second cover, in model coordinates; see +`modelPoints1`. -/ +def modelPoints2 : Finset ((F × F) ⊕ Bool) := + ((univ.filter fun p : F × F => p.2^2 = G.model2 p.1).image Sum.inl) + ∪ (if IsSquare (G.twist2 * G.Z) then {Sum.inr false, Sum.inr true} else ∅) + +/-- The affine members of the first cover's point set: `(u, W)` is in the +set exactly when it solves the model, `W² = H₁(u)`. -/ +@[simp] theorem mem_modelPoints1_inl {p : F × F} : + Sum.inl p ∈ G.modelPoints1 ↔ p.2^2 = G.model1 p.1 := by + unfold modelPoints1 + simp only [mem_union, mem_image, mem_filter, mem_univ, true_and, + Sum.inl.injEq] + constructor + · rintro (⟨q, hq, rfl⟩ | hbad) + · exact hq + · exfalso; revert hbad; split_ifs <;> simp + · intro hp + exact Or.inl ⟨p, hp, rfl⟩ + +/-- The affine members of the second cover's point set: `(u, W)` is in the +set exactly when it solves the model, `W² = H₂(u)`. -/ +@[simp] theorem mem_modelPoints2_inl {p : F × F} : + Sum.inl p ∈ G.modelPoints2 ↔ p.2^2 = G.model2 p.1 := by + unfold modelPoints2 + simp only [mem_union, mem_image, mem_filter, mem_univ, true_and, + Sum.inl.injEq] + constructor + · rintro (⟨q, hq, rfl⟩ | hbad) + · exact hq + · exfalso; revert hbad; split_ifs <;> simp + · intro hp + exact Or.inl ⟨p, hp, rfl⟩ + +/-- The infinite members of the first cover's point set: both points at +infinity are present exactly when the leading square class `d₁·Z` is a +square. -/ +@[simp] theorem mem_modelPoints1_inr {b : Bool} : + Sum.inr b ∈ G.modelPoints1 ↔ IsSquare (G.twist1 * G.Z) := by + unfold modelPoints1 + simp only [mem_union, mem_image] + constructor + · rintro (⟨q, _, hq⟩ | h) + · exact absurd hq (by simp) + · revert h; split_ifs with hsq <;> intro h + · exact hsq + · simp at h + · intro hsq + refine Or.inr ?_ + rw [if_pos hsq] + rcases b <;> simp + +/-- The infinite members of the second cover's point set: both points at +infinity are present exactly when the leading square class `d₂·Z` is a +square. -/ +@[simp] theorem mem_modelPoints2_inr {b : Bool} : + Sum.inr b ∈ G.modelPoints2 ↔ IsSquare (G.twist2 * G.Z) := by + unfold modelPoints2 + simp only [mem_union, mem_image] + constructor + · rintro (⟨q, _, hq⟩ | h) + · exact absurd hq (by simp) + · revert h; split_ifs with hsq <;> intro h + · exact hsq + · simp at h + · intro hsq + refine Or.inr ?_ + rw [if_pos hsq] + rcases b <;> simp + +/-- The covering map of the first cover, in model coordinates. An affine +model point over `u ≠ 0` goes to the curve point with abscissa `x₁ u` and +ordinate `W / s₁ u`. Everything else goes to `𝒪`: the `u = 0` fibre, the +points at infinity, and junk values off the model. The `𝒪` images are +genuine on the parameter range the correspondence theorems target (`-A·B` +a nonsquare). There this cover's rational boundary points sit over `u = 0`, +where the abscissa has a pole. -/ +def cover1Map (hsq : IsSquare (-1 : F)) : (F × F) ⊕ Bool → SWPoint G.E + | .inl p => + if h : p.1 ≠ 0 ∧ p.2^2 = G.model1 p.1 then + ⟨G.x1 p.1, p.2 / G.scale1 p.1, Or.inl (by + show (p.2 / G.scale1 p.1)^2 = (G.x1 p.1)^3 + G.E.A * G.x1 p.1 + G.E.B + rw [div_pow, h.2, ← G.model1_eq hsq h.1, + mul_div_cancel_right₀ _ (pow_ne_zero 2 (G.scale1_ne_zero hsq h.1))])⟩ + else 0 + | .inr _ => 0 + +/-- The covering map of the second cover; see `cover1Map`. On the targeted +parameter range this cover's rational boundary points are at infinity, where +the abscissa has a pole. -/ +def cover2Map (hsq : IsSquare (-1 : F)) : (F × F) ⊕ Bool → SWPoint G.E + | .inl p => + if h : p.1 ≠ 0 ∧ p.2^2 = G.model2 p.1 then + ⟨G.x2 p.1, p.2 / G.scale2 p.1, Or.inl (by + show (p.2 / G.scale2 p.1)^2 = (G.x2 p.1)^3 + G.E.A * G.x2 p.1 + G.E.B + rw [div_pow, h.2, ← G.model2_eq hsq h.1, + mul_div_cancel_right₀ _ (pow_ne_zero 2 (G.scale2_ne_zero hsq p.1))])⟩ + else 0 + | .inr _ => 0 + +end ModelPoints + +end SSWUParams + +/-! ## Counting square roots + +The fibre of a model over `u₀` is the solution set of `W² = H(u₀)`; these +helpers count it. In odd characteristic, a nonzero square has exactly the +two roots `±r`, and a nonsquare has none. -/ + +/-- The solutions of `W² = a` for a nonzero `a` with a root `r`: exactly +`{r, -r}`. -/ +theorem filter_sq_eq_pair {F : Type*} [Field F] [Fintype F] [DecidableEq F] + {a r : F} (hr : r^2 = a) : + (univ.filter fun W : F => W^2 = a) = {r, -r} := by + ext W + simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton] + rw [← hr, sq_eq_sq_iff_eq_or_eq_neg] + +/-- In odd characteristic, a nonzero square has exactly two square roots. -/ +theorem filter_sq_card_of_isSquare {F : Type*} [Field F] [Fintype F] + [DecidableEq F] {a : F} (hchar : ringChar F ≠ 2) (ha : a ≠ 0) + (hsq : IsSquare a) : + (univ.filter fun W : F => W^2 = a).card = 2 := by + obtain ⟨r, hr⟩ := hsq + have hr2 : r^2 = a := by rw [sq]; exact hr.symm + have hr0 : r ≠ 0 := by + rintro rfl + exact ha (by rw [← hr2]; ring) + rw [filter_sq_eq_pair hr2] + refine card_pair_eq_two_iff.mpr fun h => hr0 ?_ + exact (Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm + +/-- A nonsquare has no square roots. -/ +theorem filter_sq_eq_empty {F : Type*} [Field F] [Fintype F] [DecidableEq F] + {a : F} (hns : ¬ IsSquare a) : + (univ.filter fun W : F => W^2 = a) = ∅ := by + rw [filter_eq_empty_iff] + intro W _ + exact fun hW => hns ⟨W, by rw [← hW]; ring⟩ + +/-- A nonsquare times a nonzero square is a nonsquare. -/ +theorem not_isSquare_mul_sq {F : Type*} [Field F] {z c : F} + (hz : ¬ IsSquare z) (hc : c ≠ 0) : ¬ IsSquare (z * c^2) := by + rintro ⟨t, ht⟩ + refine hz ⟨t/c, ?_⟩ + field_simp + linear_combination ht + +/-- A sum over a filtered product, decomposed into a double sum: outer over +the first component, inner over the filter at that component. -/ +theorem sum_filter_prod {α β M : Type*} [Fintype α] [Fintype β] + [DecidableEq α] [DecidableEq β] [AddCommMonoid M] + (P : α → β → Prop) [∀ a b, Decidable (P a b)] (f : α × β → M) : + ∑ p ∈ (univ : Finset (α × β)).filter fun p => P p.1 p.2, f p + = ∑ a, ∑ b ∈ univ.filter fun b => P a b, f (a, b) := by + rw [Finset.sum_filter, Fintype.sum_prod_type] + exact Finset.sum_congr rfl fun a _ => (Finset.sum_filter _ _).symm + +namespace SSWUParams + +/-! ## The fibre over a nonzero input + +Fix `u ≠ 0`. Exactly one branch's curve-equation value `g (x_j u)` is a +nonzero square, and the mapping outputs a point over that branch's abscissa +(`map_x`). On the square branch the model fibre `W² = H_j(u)` has the two +roots `±(map u).y · s_j u`, whose covering-map images are `map u` and +`-(map u)`; on the other branch the fibre is empty. `fibre_sum` packages +this: summed over both covers, any function of the images contributes +exactly `φ (map u) + φ (-(map u))`. -/ + +section FibreSum + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-- The candidate ordinate squares to the curve equation at the output +abscissa: the on-curve fact `onCurve_mapXY`, restated through `map`. -/ +theorem map_y_sq (u : F) : + ((G.map u).y)^2 = ((G.map u).x)^3 + G.E.A * (G.map u).x + G.E.B := + G.onCurve_mapXY u + +/-- **The branch selection.** For `u ≠ 0`, the mapping outputs the branch +whose curve-equation value is a square: the abscissa is `x₁ u` when +`g (x₁ u)` is a square, else `x₂ u`. The square-root split tests exactly +`IsSquare (U / xdiv³)`, and `U / xdiv³ = g (x₁ u)`. -/ +theorem map_x (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + (G.map u).x + = if IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) then G.x1 u + else G.x2 u := by + have hta : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0 := G.ta_ne_zero_of_u_ne_zero hsq hu + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero (neg_ne_zero.mpr hta) + have hX := G.x1_mul_den hsq hu + -- The ratio the square-root split tests is the curve equation at `x₁ u`. + have hUdiv : ((G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + G.E.B * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3 + = ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3 := by + linear_combination (-((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + have hbiff : (sqrtRatio G.d G.lam + (((G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + G.E.B * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3) + ((G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3)).2 = true + ↔ IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) := by + rw [sqrtRatio_true_iff, hUdiv, + mul_div_cancel_right₀ _ (pow_ne_zero 3 hden)] + show (G.mapXYUpToSign u).1 = _ + simp only [mapXYUpToSign] + rw [if_neg hta] + by_cases hgs : IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + · rw [if_pos hgs, hbiff.mpr hgs, if_pos rfl] + rfl + · rw [if_neg hgs, Bool.eq_false_iff.mpr fun h => hgs (hbiff.mp h), + if_neg (by simp)] + unfold x2 x1 + ring + +/-- The first covering map's abscissa at a genuine affine model point. -/ +theorem cover1Map_inl_x (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model1 u) : + (G.cover1Map hsq (Sum.inl (u, W))).x = G.x1 u := by + simp [cover1Map, hu, hW] + +/-- The first covering map's ordinate at a genuine affine model point. -/ +theorem cover1Map_inl_y (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model1 u) : + (G.cover1Map hsq (Sum.inl (u, W))).y = W / G.scale1 u := by + simp [cover1Map, hu, hW] + +/-- The second covering map's abscissa at a genuine affine model point. -/ +theorem cover2Map_inl_x (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model2 u) : + (G.cover2Map hsq (Sum.inl (u, W))).x = G.x2 u := by + simp [cover2Map, hu, hW] + +/-- The second covering map's ordinate at a genuine affine model point. -/ +theorem cover2Map_inl_y (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model2 u) : + (G.cover2Map hsq (Sum.inl (u, W))).y = W / G.scale2 u := by + simp [cover2Map, hu, hW] + +/-- **The fibre over a nonzero input, summed.** Over `u ≠ 0`, the two +covers' affine model fibres together contribute the images `map u` and +`-(map u)`, each once: the square branch's two roots supply them, and the +other branch's fibre is empty. -/ +theorem fibre_sum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + {M : Type*} [AddCommMonoid M] (φ : SWPoint G.E → M) {u : F} (hu : u ≠ 0) : + (∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W)))) + + (∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + = φ (G.map u) + φ (-(G.map u)) := by + have hchar := G.ringChar_ne_two + have hH1 := G.model1_ne_zero hsq hy0 u + have hH2 := G.model2_ne_zero hsq hy0 u + have hg1 : (G.x1 u)^3 + G.E.A * G.x1 u + G.E.B ≠ 0 := fun h => + hH1 (by rw [← G.model1_eq hsq hu, h, zero_mul]) + have hg2 : (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B ≠ 0 := fun h => + hH2 (by rw [← G.model2_eq hsq hu, h, zero_mul]) + have hu3 : G.Z * u^3 ≠ 0 := mul_ne_zero G.Z_nonzero (pow_ne_zero 3 hu) + by_cases hgs : IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + · -- Branch 1 carries the square; branch 2's fibre is empty. + have hx : (G.map u).x = G.x1 u := by rw [G.map_x hsq hu, if_pos hgs] + have hy2 : ((G.map u).y)^2 = (G.x1 u)^3 + G.E.A * G.x1 u + G.E.B := by + rw [← hx]; exact G.map_y_sq u + have hyne : (G.map u).y ≠ 0 := fun h => hg1 (by rw [← hy2, h]; ring) + have hr2 : ((G.map u).y * G.scale1 u)^2 = G.model1 u := by + rw [mul_pow, hy2, G.model1_eq hsq hu] + have hrne : (G.map u).y * G.scale1 u ≠ 0 := + mul_ne_zero hyne (G.scale1_ne_zero hsq hu) + have hns2 : ¬ IsSquare (G.model2 u) := by + obtain ⟨t, ht⟩ := hgs + have ht0 : t ≠ 0 := fun h => hg1 (by rw [ht, h, mul_zero]) + have hM : G.model2 u = G.Z * (G.Z * u^3 * t * G.scale2 u)^2 := by + rw [← G.model2_eq hsq hu, G.g_x2_eq hsq hu, ht]; ring + rw [hM] + exact not_isSquare_mul_sq G.Z_nonsquare + (mul_ne_zero (mul_ne_zero hu3 ht0) (G.scale2_ne_zero hsq u)) + rw [filter_sq_eq_empty hns2, Finset.sum_empty, _root_.add_zero, + filter_sq_eq_pair hr2, Finset.sum_pair fun h => hrne + ((Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm)] + have hP : G.cover1Map hsq (Sum.inl (u, (G.map u).y * G.scale1 u)) + = G.map u := by + refine SWPoint.ext_pair ?_ + rw [G.cover1Map_inl_x hsq hu hr2, G.cover1Map_inl_y hsq hu hr2, hx, + mul_div_cancel_right₀ _ (G.scale1_ne_zero hsq hu)] + have hQ : G.cover1Map hsq (Sum.inl (u, -((G.map u).y * G.scale1 u))) + = -(G.map u) := by + have hr2' : (-((G.map u).y * G.scale1 u))^2 = G.model1 u := by + rw [neg_sq, hr2] + refine SWPoint.ext_pair ?_ + rw [G.cover1Map_inl_x hsq hu hr2', G.cover1Map_inl_y hsq hu hr2', + SWPoint.neg_x, SWPoint.neg_y, hx, neg_div, + mul_div_cancel_right₀ _ (G.scale1_ne_zero hsq hu)] + rw [hP, hQ] + · -- Branch 2 carries the square; branch 1's fibre is empty. + have hZ3 : ¬ IsSquare ((G.Z * u^2)^3) := by + have h : (G.Z * u^2)^3 = G.Z * (G.Z * u^3)^2 := by ring + rw [h] + exact not_isSquare_mul_sq G.Z_nonsquare hu3 + have hgs2 : IsSquare ((G.x2 u)^3 + G.E.A * G.x2 u + G.E.B) := by + rw [G.g_x2_eq hsq hu] + exact isSquare_mul_of_not_isSquare hZ3 hgs + have hx : (G.map u).x = G.x2 u := by rw [G.map_x hsq hu, if_neg hgs] + have hy2 : ((G.map u).y)^2 = (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B := by + rw [← hx]; exact G.map_y_sq u + have hyne : (G.map u).y ≠ 0 := fun h => hg2 (by rw [← hy2, h]; ring) + have hr2 : ((G.map u).y * G.scale2 u)^2 = G.model2 u := by + rw [mul_pow, hy2, G.model2_eq hsq hu] + have hrne : (G.map u).y * G.scale2 u ≠ 0 := + mul_ne_zero hyne (G.scale2_ne_zero hsq u) + have hns1 : ¬ IsSquare (G.model1 u) := by + rw [← G.model1_eq hsq hu] + exact not_isSquare_mul_sq hgs (G.scale1_ne_zero hsq hu) + rw [filter_sq_eq_empty hns1, Finset.sum_empty, _root_.zero_add, + filter_sq_eq_pair hr2, Finset.sum_pair fun h => hrne + ((Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm)] + have hP : G.cover2Map hsq (Sum.inl (u, (G.map u).y * G.scale2 u)) + = G.map u := by + refine SWPoint.ext_pair ?_ + rw [G.cover2Map_inl_x hsq hu hr2, G.cover2Map_inl_y hsq hu hr2, hx, + mul_div_cancel_right₀ _ (G.scale2_ne_zero hsq u)] + have hQ : G.cover2Map hsq (Sum.inl (u, -((G.map u).y * G.scale2 u))) + = -(G.map u) := by + have hr2' : (-((G.map u).y * G.scale2 u))^2 = G.model2 u := by + rw [neg_sq, hr2] + refine SWPoint.ext_pair ?_ + rw [G.cover2Map_inl_x hsq hu hr2', G.cover2Map_inl_y hsq hu hr2', + SWPoint.neg_x, SWPoint.neg_y, hx, neg_div, + mul_div_cancel_right₀ _ (G.scale2_ne_zero hsq u)] + rw [hP, hQ] + +/-- **The covers, summed, with the boundary bookkeeping.** On the parameter +range with `-A·B` a nonsquare, + +`S₁ + S₂ = Σ_{u ≠ 0} (φ (map u) + φ (-(map u))) + 4·φ 𝒪`, + +where `S_j` sums `φ` of the covering-map images over the full point set of +cover `j`, for any `φ` into a commutative additive monoid. The boundary +supplies the `4·φ 𝒪`: +* cover 1 has no points at infinity, and its `u = 0` fibre is a rational + pair mapping to `𝒪`; +* cover 2 has an empty `u = 0` fibre, and its rational pair at infinity + maps to `𝒪`. -/ +theorem modelPoints_sum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) + {M : Type*} [AddCommMonoid M] (φ : SWPoint G.E → M) : + (∑ P ∈ G.modelPoints1, φ (G.cover1Map hsq P)) + + (∑ P ∈ G.modelPoints2, φ (G.cover2Map hsq P)) + = (∑ u ∈ (univ : Finset F).erase 0, + (φ (G.map u) + φ (-(G.map u)))) + 4 • φ 0 := by + have hchar := G.ringChar_ne_two + -- The boundary square classes, under `-A·B` nonsquare: + -- cover 1 has no rational points at infinity … + have hT1 : ¬ IsSquare (G.twist1 * G.Z) := by + have h : G.twist1 * G.Z = -(G.E.A * G.E.B) * (G.E.A * G.Z^2)^2 := by + unfold twist1; ring + rw [h] + exact not_isSquare_mul_sq hAB + (mul_ne_zero G.A_nonzero (pow_ne_zero 2 G.Z_nonzero)) + -- … cover 2 does … + have hT2 : IsSquare (G.twist2 * G.Z) := by + obtain ⟨r, hr⟩ := isSquare_mul_of_not_isSquare hAB G.Z_nonsquare + refine ⟨r * G.E.A, ?_⟩ + unfold twist2 + linear_combination (G.E.A^2) * hr + -- … cover 1's `u = 0` fibre is inhabited … + have h10 : IsSquare (G.model1 0) := by + rw [G.model1_zero] + obtain ⟨r, hr⟩ := isSquare_mul_of_not_isSquare hAB G.Z_nonsquare + refine ⟨r * (G.E.A * G.Z) * G.E.B, ?_⟩ + unfold twist1 + linear_combination (G.E.A^2 * G.Z^2 * G.E.B^2) * hr + -- … and cover 2's is empty. + have h20 : ¬ IsSquare (G.model2 0) := by + rw [G.model2_zero] + have h : G.twist2 * G.E.B^2 = -(G.E.A * G.E.B) * (G.E.A * G.E.B)^2 := by + unfold twist2; ring + rw [h] + exact not_isSquare_mul_sq hAB (mul_ne_zero G.A_nonzero G.E.B_nonzero) + -- Decompose the point-set sums into affine double sums and the boundary. + have hs1 : ∑ P ∈ G.modelPoints1, φ (G.cover1Map hsq P) + = ∑ u, ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W))) := by + unfold modelPoints1 + rw [if_neg hT1, Finset.union_empty, + Finset.sum_image fun _ _ _ _ h => Sum.inl.inj h, + sum_filter_prod (fun u W => W^2 = G.model1 u) + (fun p => φ (G.cover1Map hsq (Sum.inl p)))] + have hs2 : ∑ P ∈ G.modelPoints2, φ (G.cover2Map hsq P) + = (∑ u, ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + (φ 0 + φ 0) := by + unfold modelPoints2 + rw [if_pos hT2, Finset.sum_union (by simp [Finset.disjoint_left]), + Finset.sum_image fun _ _ _ _ h => Sum.inl.inj h, + Finset.sum_insert (by simp), Finset.sum_singleton, + sum_filter_prod (fun u W => W^2 = G.model2 u) + (fun p => φ (G.cover2Map hsq (Sum.inl p)))] + simp [cover2Map] + -- The `u = 0` inner sums: two `𝒪`-images on cover 1, none on cover 2. + have hA0 : ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 0, + φ (G.cover1Map hsq (Sum.inl (0, W))) = 2 • φ 0 := by + calc ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 0, + φ (G.cover1Map hsq (Sum.inl (0, W))) + = ∑ _W ∈ univ.filter fun W : F => W^2 = G.model1 0, φ 0 := + Finset.sum_congr rfl fun W _ => by simp [cover1Map] + _ = ((univ.filter fun W : F => W^2 = G.model1 0).card) • φ 0 := + Finset.sum_const _ + _ = 2 • φ 0 := by + rw [filter_sq_card_of_isSquare hchar + (G.model1_ne_zero hsq hy0 0) h10] + have hB0 : ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 0, + φ (G.cover2Map hsq (Sum.inl (0, W))) = 0 := by + rw [filter_sq_eq_empty h20, Finset.sum_empty] + -- Assemble: split `u = 0` off both outer sums and merge the rest. + rw [hs1, hs2, + ← Finset.add_sum_erase _ _ (mem_univ (0 : F)), + ← Finset.add_sum_erase _ + (fun u => ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) (mem_univ (0 : F)), + hA0, hB0] + have hmerge : (∑ u ∈ (univ : Finset F).erase 0, + ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W)))) + + (∑ u ∈ (univ : Finset F).erase 0, + ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + = ∑ u ∈ (univ : Finset F).erase 0, + (φ (G.map u) + φ (-(G.map u))) := by + rw [← Finset.sum_add_distrib] + exact Finset.sum_congr rfl fun u hu => + G.fibre_sum hsq hy0 φ (Finset.mem_erase.mp hu).1 + rw [← hmerge] + abel + +end FibreSum + +end SSWUParams + +end CompElliptic.Hashing diff --git a/CompElliptic/Hashing/CharacterSum.lean b/CompElliptic/Hashing/CharacterSum.lean index ee4747e..4937d98 100644 --- a/CompElliptic/Hashing/CharacterSum.lean +++ b/CompElliptic/Hashing/CharacterSum.lean @@ -24,10 +24,13 @@ the uniform distribution on `G`. The mappings used to hash to elliptic curves (simplified SWU and its relatives) choose the sign of the `y`-coordinate from the sign of the input. That sign rule makes the mapping **odd**: `f (-u) = -f u`. This file proves that oddness alone -forces two facts: +forces these facts: -* the value multiplicity is symmetric under negation (`IsOdd.mult_neg`); and -* `f` sends `0` to `0` when `G` has odd order (`IsOdd.map_zero`). +* the value multiplicity is symmetric under negation (`IsOdd.mult_neg`); +* `f` sends `0` to `0` when `G` has odd order (`IsOdd.map_zero`); +* the character sum is real (`IsOdd.conj_charSum`), and twice the sum is the + sum of the conjugation-symmetric terms `ψ (f u) + conj (ψ (f u))` + (`IsOdd.two_mul_charSum`). The main identity (`charSum_eq`) rewrites `∑ u, ψ (f u)` as the character transform of `fun Q => mult f Q - 1`, the deviation of the value multiplicity from a perfect @@ -117,4 +120,45 @@ theorem charSum_eq {ψ : AddChar G ℂ} (hψ : ψ ≠ 1) : exact Finset.sum_congr rfl fun Q _ => by ring rw [hsplit, hzero, sub_zero] +omit [DecidableEq G] in +/-- Negating the argument of a complex character conjugates its value: on a +finite group every character value is a root of unity, hence of unit norm, +and `ψ (-P) = (ψ P)⁻¹`. -/ +theorem addChar_map_neg_eq_conj (ψ : AddChar G ℂ) (P : G) : + ψ (-P) = (starRingEnd ℂ) (ψ P) := by + have hpow : ψ P ^ Fintype.card G = 1 := by + rw [← AddChar.map_nsmul_eq_pow, card_nsmul_eq_zero, AddChar.map_zero_eq_one] + rw [AddChar.map_neg_eq_inv, + Complex.inv_eq_conj (Complex.norm_eq_one_of_pow_eq_one hpow + Fintype.card_ne_zero)] + +omit [DecidableEq F] [DecidableEq G] in +/-- **Realness** (design doc §4): the character sum of an odd mapping is fixed +by complex conjugation. Conjugating a term negates the output +(`addChar_map_neg_eq_conj`), which oddness trades for negating the input, and +input negation permutes the domain. -/ +theorem IsOdd.conj_charSum (hf : IsOdd f) (ψ : AddChar G ℂ) : + (starRingEnd ℂ) (∑ u, ψ (f u)) = ∑ u, ψ (f u) := by + rw [map_sum] + calc ∑ u, (starRingEnd ℂ) (ψ (f u)) + = ∑ u, ψ (f (-u)) := by + refine Finset.sum_congr rfl fun u _ => ?_ + rw [hf u, addChar_map_neg_eq_conj] + _ = ∑ u, ψ (f u) := + Fintype.sum_equiv (Equiv.neg F) _ _ fun u => rfl + +omit [DecidableEq F] [DecidableEq G] in +/-- **The doubled character sum, sign-free** (design doc §4): twice the +character sum of an odd mapping is the sum of `ψ (f u) + conj (ψ (f u))` over +inputs. Each term equals `ψ P + ψ (-P)` at `P = f u` +(`addChar_map_neg_eq_conj`), so it is unchanged by negating `f u`: the sign +convention has no influence on it. -/ +theorem IsOdd.two_mul_charSum (hf : IsOdd f) (ψ : AddChar G ℂ) : + 2 * ∑ u, ψ (f u) = ∑ u, (ψ (f u) + (starRingEnd ℂ) (ψ (f u))) := by + have h : ∑ u, (starRingEnd ℂ) (ψ (f u)) = ∑ u, ψ (f u) := by + rw [← map_sum (starRingEnd ℂ) (fun u => ψ (f u)) Finset.univ] + exact hf.conj_charSum ψ + rw [Finset.sum_add_distrib, h] + ring + end CompElliptic.Hashing diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean index 919a523..1e9459e 100644 --- a/CompElliptic/Hashing/FibreBound.lean +++ b/CompElliptic/Hashing/FibreBound.lean @@ -111,6 +111,8 @@ theorem fibrePoly_fst_ne_zero (G : SSWUParams F) (x : F) : 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) +/-- `Φ_x` has degree at most 10: its first factor has degree at most 4, +and its second exactly 6 (`fibrePoly_snd_natDegree`). -/ theorem fibrePoly_natDegree_le (G : SSWUParams F) (x : F) : (G.fibrePoly x).natDegree ≤ 10 := by refine natDegree_mul_le.trans ?_ diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index 03d9abe..b68f6ce 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -10,6 +10,7 @@ import CompElliptic.Curves.PastaOrder import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.SignedLift import CompElliptic.Hashing.FibreBound +import CompElliptic.Hashing.WeilInstance import Mathlib.Tactic.ReduceModChar /-! @@ -184,6 +185,59 @@ theorem norm_charSum_mapToCurve_sub_zeroRepaired (ψ : AddChar (SWPoint curve) ‖∑ u, ψ (mapToCurve u) - ∑ u, ψ (zeroRepaired mapToCurve u)‖ ≤ 2 := norm_charSum_sub_zeroRepaired mapToCurve ψ +/-- `-A·B` for iso-Pallas is a quadratic non-residue, by Euler's criterion +with the power evaluated by fast modular exponentiation. This puts the +deployed instantiation in the branch of the boundary bookkeeping where all +four extra cover points map to `𝒪`; it is the same fact as the emptiness of +the `w = 0` fibre that `weilbound.sage` checks. -/ +theorem neg_AB_not_isSquare : + ¬ IsSquare (-(isoCurve.A * isoCurve.B) : PallasBaseField) := by + have h : (-(isoCurve.A * isoCurve.B) : PallasBaseField) + = 0x20ac6f47c8ff2fb79b416dfa18151f9498e4983c291cb11f8c10b822901f9e44 := by + decide + rw [h, ZMod.euler_criterion PALLAS_BASE_CARD (by decide : + (0x20ac6f47c8ff2fb79b416dfa18151f9498e4983c291cb11f8c10b822901f9e44 + : PallasBaseField) ≠ 0)] + reduce_mod_char + decide + +/-- **The deployed Weil bound for the Pallas mapping.** Weil's theorem at +the two branch covers of iso-Pallas —the `CharSumBounded` inputs at +`100·#F`; see `Hashing/WeilInstance.lean`— gives +`WeilBounded (zeroRepaired mapToCurve)` at the recorded constant `21/2`. +The bound crosses the 3-isogeny because the isogeny is a bijective +homomorphism on rational points, so characters pull back along it. -/ +theorem weilBounded_zeroRepaired_mapToCurve + (h1 : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + (100 * (Fintype.card PallasBaseField : ℝ))) + (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + (100 * (Fintype.card PallasBaseField : ℝ))) : + WeilBounded (zeroRepaired mapToCurve) (21/2) := by + rw [show (21/2 : ℝ) = 10 + 1/2 from by norm_num] + have h1' : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card PallasBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h1 + have h2' : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card PallasBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h2 + have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one + iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 + (by norm_num : (0 : ℝ) < 10) + (by rw [ZMod.card]; norm_num) h1' h2' + have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) + iso_map_bijective + have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) + (zeroRepaired sswu.map u)) = zeroRepaired mapToCurve := by + funext u + rcases eq_or_ne u 0 with rfl | hu + · exact ((congrArg (AddMonoidHom.mk' iso.map iso_map_add) + (if_pos rfl)).trans (map_zero _)).trans (if_pos rfl).symm + · simp [zeroRepaired, hu, mapToCurve] + rw [← hfun] + exact hcomp + /-- The deployed hash-to-curve construction for Pallas after `hash_to_field`: add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : PallasBaseField) : SWPoint curve := @@ -371,6 +425,59 @@ theorem norm_charSum_mapToCurve_sub_zeroRepaired (ψ : AddChar (SWPoint curve) ‖∑ u, ψ (mapToCurve u) - ∑ u, ψ (zeroRepaired mapToCurve u)‖ ≤ 2 := norm_charSum_sub_zeroRepaired mapToCurve ψ +/-- `-A·B` for iso-Vesta is a quadratic non-residue, by Euler's criterion +with the power evaluated by fast modular exponentiation. This puts the +deployed instantiation in the branch of the boundary bookkeeping where all +four extra cover points map to `𝒪`; it is the same fact as the emptiness of +the `w = 0` fibre that `weilbound.sage` checks. -/ +theorem neg_AB_not_isSquare : + ¬ IsSquare (-(isoCurve.A * isoCurve.B) : VestaBaseField) := by + have h : (-(isoCurve.A * isoCurve.B) : VestaBaseField) + = 0x3722d4398ccc606a2c8a49902dbae3b72c59d02c5890bd61eb2e37c567e5258 := by + decide + rw [h, ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : + (0x3722d4398ccc606a2c8a49902dbae3b72c59d02c5890bd61eb2e37c567e5258 + : VestaBaseField) ≠ 0)] + reduce_mod_char + decide + +/-- **The deployed Weil bound for the Vesta mapping.** Weil's theorem at +the two branch covers of iso-Vesta —the `CharSumBounded` inputs at +`100·#F`; see `Hashing/WeilInstance.lean`— gives +`WeilBounded (zeroRepaired mapToCurve)` at the recorded constant `21/2`. +The bound crosses the 3-isogeny because the isogeny is a bijective +homomorphism on rational points, so characters pull back along it. -/ +theorem weilBounded_zeroRepaired_mapToCurve + (h1 : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + (100 * (Fintype.card VestaBaseField : ℝ))) + (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + (100 * (Fintype.card VestaBaseField : ℝ))) : + WeilBounded (zeroRepaired mapToCurve) (21/2) := by + rw [show (21/2 : ℝ) = 10 + 1/2 from by norm_num] + have h1' : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card VestaBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h1 + have h2' : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card VestaBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h2 + have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one + iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 + (by norm_num : (0 : ℝ) < 10) + (by rw [ZMod.card]; norm_num) h1' h2' + have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) + iso_map_bijective + have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) + (zeroRepaired sswu.map u)) = zeroRepaired mapToCurve := by + funext u + rcases eq_or_ne u 0 with rfl | hu + · exact ((congrArg (AddMonoidHom.mk' iso.map iso_map_add) + (if_pos rfl)).trans (map_zero _)).trans (if_pos rfl).symm + · simp [zeroRepaired, hu, mapToCurve] + rw [← hfun] + exact hcomp + /-- The deployed hash-to-curve construction for Vesta after `hash_to_field`: add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : VestaBaseField) : SWPoint curve := diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index 84e2220..ccab9bc 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -68,14 +68,9 @@ 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. 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`). + statistical distance. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), the + derived constant `C = 21/2` puts the statistical distance near `2^{-120}` + (`design/weil-constant-derivation.md`; 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 @@ -341,12 +336,11 @@ 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)²`. 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 +`(#G - 1)·C⁴/(#F)²`. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), the derived +constant `C = 21/2` makes the statistical distance about `2^{-120}` (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`". -/ theorem sq_sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ} (h : WeilBounded f C) : diff --git a/CompElliptic/Hashing/WeilInstance.lean b/CompElliptic/Hashing/WeilInstance.lean new file mode 100644 index 0000000..83c076f --- /dev/null +++ b/CompElliptic/Hashing/WeilInstance.lean @@ -0,0 +1,161 @@ +/- +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.BranchCovers +import CompElliptic.Hashing.WellDistributed + +/-! +# The Weil input at the branch covers + +This file states the shape in which Weil's theorem enters the formalization, +and derives `WeilBounded` for the zero-repaired mapping from it. + +`CharSumBounded s h B` says every nontrivial character of the target group +sums to at most `B` on the images of the point set `s` under `h`, in squared +norm. Weil's theorem — in the form of FFSTV's Lemma 1 and Theorem 3 +() — bounds such a sum over a genus-`g̃` +covering of an elliptic curve by `(2·g̃ - 2)·√q`, provided the covering does +not factor through a nontrivial unramified subcover. The branch covers have +genus 6, and their total ramification over `A·x + B = 0` rules every +unramified subcover out; both derivations are cited from +`design/weil-constant-derivation.md` §2–3. Mathlib does not yet have the +vocabulary to state them (genus, places, covers of curves); the +vocabulary, on the Riemann's-inequality route, is tracked at +. + +The derivation is parametric in the per-cover constant `c`: inputs at +`c²·#F`, conclusion at `c + 1/2`. The parameter exists because the cited +constant depends on which genus fact the citation uses, and the two +candidates differ in formalization cost, not just in value. The deployed +citation takes `c = 10 = 2·6 - 2` from the exact genus. Riemann's +inequality (Stichtenoth, *Algebraic Function Fields and Codes*, 2nd ed., +§3.11) bounds the genus by `(2 - 1)·(14 - 1) = 13`, from the two field +generators alone. That is elementary divisor counting, far below the +Riemann–Hurwitz tier that exact genus 6 needs. The corresponding constant +is `c = 24`; the regularity distance scales with the square of the +consumed constant `c + 1/2`, so the cost is `(24.5/10.5)² ≈ 2^{2.44}`. +Parameterizing keeps every consumer unchanged if the cited constant +moves. + +`cover_charSum` is the sign-free assembly (design doc §4): for every +character `ψ`, + +`S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2`, + +where `S_j` sums `ψ` over cover `j`'s images and `S` sums it over the +zero-repaired mapping's outputs. `weilBounded_zeroRepaired` combines the +assembly with the two cover bounds and exact square-free arithmetic: + +`‖S(ψ)‖² ≤ (c + 1/2)²·#F` for every nontrivial `ψ`, + +that is, `WeilBounded (zeroRepaired G.map) (c + 1/2)`, on any field with +`#F ≥ 4·c + 4` where `-1` is a square, `-A·B` is a nonsquare, the curve +has no 2-torsion, and the sign function is genuine. The deployed +instantiations take `c = 10`, so `21/2` and `#F ≥ 44`. +-/ + +namespace CompElliptic.Hashing + +open Finset CompElliptic.CurveForms.ShortWeierstrass + +/-- A squared character-sum bound over a finite point set: every nontrivial +character of the target group sums to at most `B` on the images, in squared +norm. Weil's theorem supplies such bounds for the rational points of curve +coverings, with `B = ((2·g̃ - 2))²·q` for a genus-`g̃` covering over a field +of size `q`; see the module docstring. -/ +def CharSumBounded {ι G' : Type*} [AddCommGroup G'] (s : Finset ι) + (h : ι → G') (B : ℝ) : Prop := + ∀ ψ : AddChar G' ℂ, ψ ≠ 1 → ‖∑ P ∈ s, ψ (h P)‖^2 ≤ B + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-- **The sign-free assembly** (design doc §4): for every character `ψ` of +the curve group, the two covers' character sums combine to + +`S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2`, + +with `S(ψ)` the character sum of the zero-repaired mapping. Negating the +input permutes the nonzero inputs and negates the output, so the two +per-input images `±(map u)` sum to twice the mapping's character sum; the +four boundary points contribute `ψ 𝒪 = 1` each, and the repaired `u = 0` +input supplies the `-2` that turns `+ 4` into `+ 2`. -/ +theorem cover_charSum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) (hsgn : IsSignFunction G.sgn) + (ψ : AddChar (SWPoint G.E) ℂ) : + (∑ P ∈ G.modelPoints1, ψ (G.cover1Map hsq P)) + + (∑ P ∈ G.modelPoints2, ψ (G.cover2Map hsq P)) + = 2 * (∑ u, ψ (zeroRepaired G.map u)) + 2 := by + rw [G.modelPoints_sum hsq hy0 hAB (fun P => ψ P), Finset.sum_add_distrib] + have hneg : (∑ u ∈ (univ : Finset F).erase 0, ψ (-(G.map u))) + = ∑ u ∈ (univ : Finset F).erase 0, ψ (G.map u) := by + refine Finset.sum_equiv (Equiv.neg F) (fun u => ?_) (fun u hu => ?_) + · simp [Finset.mem_erase] + · simp only [Equiv.neg_apply, + G.map_neg hsgn (Finset.mem_erase.mp hu).1] + have hfull : (∑ u, ψ (zeroRepaired G.map u)) + = 1 + ∑ u ∈ (univ : Finset F).erase 0, ψ (G.map u) := by + rw [← Finset.add_sum_erase _ _ (mem_univ (0 : F))] + congr 1 + · simp [zeroRepaired] + · exact Finset.sum_congr rfl fun u hu => by + simp [zeroRepaired, (Finset.mem_erase.mp hu).1] + rw [hneg, hfull, AddChar.map_zero_eq_one] + ring + +/-- **`WeilBounded` from the two cover bounds, parametrically in the +constant.** For a per-cover constant `c > 0`: if both covers' character +sums are bounded by `c²·#F` in squared norm, the zero-repaired mapping is +Weil-bounded at `c + 1/2`, on any field with `#F ≥ 4·c + 4`. The extra +half absorbs the assembly's boundary terms, square-root-free; its size is +conventional, not forced — the sharp bound is `c·√#F + 1`, so any positive +slack would do at a matching field-size threshold. A half is a round +choice whose cost is invisible at the deployed sizes; the recorded +deployed constant `21/2` is the same convention at `c = 10`. The module +docstring records why `c` is a parameter. -/ +theorem weilBounded_zeroRepaired (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) (hsgn : IsSignFunction G.sgn) + {c : ℝ} (hc : 0 < c) (hq : 4*c + 4 ≤ (Fintype.card F : ℝ)) + (h1 : CharSumBounded G.modelPoints1 (G.cover1Map hsq) + (c^2 * (Fintype.card F : ℝ))) + (h2 : CharSumBounded G.modelPoints2 (G.cover2Map hsq) + (c^2 * (Fintype.card F : ℝ))) : + WeilBounded (zeroRepaired G.map) (c + 1/2) := by + intro ψ hψ + have hid := G.cover_charSum hsq hy0 hAB hsgn ψ + have ha := h1 ψ hψ + have hb := h2 ψ hψ + set S := ∑ u, ψ (zeroRepaired G.map u) with hS + set S₁ := ∑ P ∈ G.modelPoints1, ψ (G.cover1Map hsq P) with hS₁ + set S₂ := ∑ P ∈ G.modelPoints2, ψ (G.cover2Map hsq P) with hS₂ + have hnorm : 2 * ‖S‖ ≤ ‖S₁‖ + ‖S₂‖ + 2 := by + calc 2 * ‖S‖ = ‖(2 : ℂ) * S‖ := by + rw [norm_mul, RCLike.norm_ofNat] + _ = ‖S₁ + S₂ - 2‖ := by rw [show (2 : ℂ) * S = S₁ + S₂ - 2 from by + linear_combination -hid] + _ ≤ ‖S₁ + S₂‖ + ‖(2 : ℂ)‖ := norm_sub_le _ _ + _ ≤ (‖S₁‖ + ‖S₂‖) + 2 := by + rw [RCLike.norm_ofNat] + gcongr + exact norm_add_le _ _ + have h4 : 4 * ‖S‖^2 ≤ (‖S₁‖ + ‖S₂‖ + 2)^2 := by + nlinarith [hnorm, norm_nonneg S, norm_nonneg S₁, norm_nonneg S₂] + -- The linear term: `4·(‖S₁‖ + ‖S₂‖) + 4 ≤ (4·c + 1)·#F`. + have hlin : 4 * (‖S₁‖ + ‖S₂‖) + 4 ≤ (4*c + 1) * (Fintype.card F : ℝ) := by + nlinarith [ha, hb, hc, sq_nonneg (‖S₁‖ - ‖S₂‖), + sq_nonneg (‖S₁‖ + ‖S₂‖ - 2*c), + mul_nonneg hc.le (sub_nonneg.mpr hq), + norm_nonneg S₁, norm_nonneg S₂] + nlinarith [h4, hlin, ha, hb, sq_nonneg (‖S₁‖ - ‖S₂‖), norm_nonneg S₁, + norm_nonneg S₂] + +end SSWUParams + +end CompElliptic.Hashing diff --git a/CompElliptic/Hashing/WeilSupport.lean b/CompElliptic/Hashing/WeilSupport.lean new file mode 100644 index 0000000..90ee58e --- /dev/null +++ b/CompElliptic/Hashing/WeilSupport.lean @@ -0,0 +1,780 @@ +/- +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.BranchCovers +import Mathlib.FieldTheory.RatFunc.Basic +import Mathlib.FieldTheory.Separable +import Mathlib.RingTheory.AdjoinRoot +import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed +import Mathlib.RingTheory.Polynomial.Eisenstein.Basic + +/-! +# Supporting facts for the Weil-constant derivation + +The cited steps of `design/weil-constant-derivation.md` —the genus of the +branch covers (§2) and their total ramification (§3)— cannot be stated in +Lean without vocabulary Mathlib does not yet have. Their *inputs* can. This +file proves those inputs, so that the paper proof's checkable algebra is +machine-checked and only the two genuinely geometric steps remain cited +(; the vocabulary itself +is ). + +The genus computation (§2) consumes: +* `phiPoly_squarefree` — the core `Φ` is squarefree, by the design doc's + own argument: `Φ = φ ∘ ta` for the cubic `φ` (`phiPoly_eq_comp`), `φ` is + separable (`phiCubic_separable`, by a Bézout certificate whose constant + is `A³·B²·(4·A³ + 27·B²)` —exactly the standing nonzero quantities—), + and `Φ` is coprime to each factor of `ta′`; +* `phiPoly_natDegree` and the model degrees — `Φ` has degree 12, and the + models `H_j` degree 14 with squarefreeness (`model1Poly_squarefree`, + `model2Poly_squarefree`), which is what the hyperelliptic genus formula + `g = ⌊(14 - 1)/2⌋ = 6` is applied to (Galbraith, *Mathematics of Public + Key Cryptography*, ch. 10; Stichtenoth, *Algebraic Function Fields and + Codes*, 2nd ed., ch. 6). + +The ramification argument (§3) consumes: +* `p2Poly_isEisensteinAt` and `p1RecipPoly_isEisensteinAt` — the branch + quartics over `F[w]` satisfy the classical Eisenstein irreducibility + criterion (`Polynomial.IsEisensteinAt`) at the ideal `(w)`; +* `eval_g_neg_B_div_A` — `g(-B/A) = -(B/A)³ ≠ 0` (this is why `w` is a + uniformizer at both points over `w = 0`). + +The monodromy cross-check (§3) consumes `v4TestPoly_not_isSquare` and +`c4TestPoly_not_isSquare`: the biquadratic V₄/C₄ square classes +`B·(A·x + B)` and `B·(A·x - 3·B)` are not squares in the function +field. The field is presented via `gPoly` as the quadratic algebra +`K[Y]/(Y² - ĝ)` over `K = F_q(x)`. The section header below describes +the decomposition machinery. + +The Eisenstein criterion is that the leading coefficient lies outside the +ideal, every lower coefficient lies inside it, and the constant coefficient +lies outside its square. The cited total-ramification argument relies on +this criterion's transplant to places of function fields (Stichtenoth, +*Algebraic Function Fields and Codes*, 2nd ed., ch. 3; design doc, +Background). The transplant is a statement about any discrete valuation on +the coefficient field — it instantiates the criterion rather than being a +new theorem. Its hypotheses force the polynomial's Newton polygon to be a +single segment from `(0, 1)` to `(n, 0)`, so every root has valuation `1/n` +(Milne, *Algebraic Number Theory*, course notes, ch. 7, Prop. 7.44 — +stated there for characteristic zero, but the argument is +characteristic-free). This yields irreducibility and ramification index +`n` —total ramification— at once. The classical form instantiates this at +`ℤ` localized at a prime; the function-field form instantiates it at the +local ring of a place of the base curve, a uniformizer standing in for +the prime — here `w` itself, by `g_neg_B_div_A_ne_zero`. Our statements +check the coefficient pattern at the polynomial ring `F[w]`; the passage +to the valuation at the two places is part of the cited step. + +Everything here is stated over the polynomial rings `F[u]` and `(F[w])[u]`; +the connection from these inputs to genus 6 and to the no-unramified-subcover +condition is the cited part. +-/ + +namespace CompElliptic.Hashing + +open Polynomial + +/-- A Bézout identity with a nonzero constant right-hand side witnesses +coprimality: divide through by the constant. -/ +theorem isCoprime_of_bezout {F : Type*} [Field F] {p q u v : Polynomial F} + {c : F} (hc : c ≠ 0) (h : u*p + v*q = C c) : IsCoprime p q := by + refine ⟨C c⁻¹ * u, C c⁻¹ * v, ?_⟩ + calc C c⁻¹ * u * p + C c⁻¹ * v * q = C c⁻¹ * (u*p + v*q) := by ring + _ = 1 := by rw [h, ← C_mul, inv_mul_cancel₀ hc, C_1] + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-! ## The core `Φ` as a polynomial -/ + +/-- The core `Φ(u) = B²·(ta + 1)³ + A³·ta²` as a polynomial in `u` +(`phiCore` is its evaluation). -/ +noncomputable def phiPoly : Polynomial F := + (C G.E.B)^2 * (G.taPoly + 1)^3 + (C G.E.A)^3 * G.taPoly^2 + +/-- `phiPoly` evaluates to the pointwise core `phiCore`. -/ +theorem eval_phiPoly (u : F) : G.phiPoly.eval u = G.phiCore u := by + simp only [phiPoly, phiCore, taPoly, tPoly, eval_add, eval_mul, eval_pow, + eval_C, eval_X, eval_one] + +/-- `Φ` has degree exactly 12; its leading coefficient is `B²·Z⁶`. -/ +theorem phiPoly_natDegree : G.phiPoly.natDegree = 12 := by + rw [phiPoly, taPoly, tPoly] + compute_degree! + exact ⟨G.E.B_nonzero, G.Z_nonzero⟩ + +/-! ## The models `H_j = d_j·(Z·u²+1)·Φ` as polynomials -/ + +/-- The first model `H₁ = d₁·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model1Poly : Polynomial F := + C G.twist1 * ((G.tPoly + 1) * G.phiPoly) + +/-- The second model `H₂ = d₂·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model2Poly : Polynomial F := + C G.twist2 * ((G.tPoly + 1) * G.phiPoly) + +/-- `model1Poly` evaluates to the pointwise model `model1`. -/ +theorem eval_model1Poly (u : F) : G.model1Poly.eval u = G.model1 u := by + simp only [model1Poly, model1, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-- `model2Poly` evaluates to the pointwise model `model2`. -/ +theorem eval_model2Poly (u : F) : G.model2Poly.eval u = G.model2 u := by + simp only [model2Poly, model2, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-! ## The genus inputs: `Φ` at `u = 0`, and coprime to `Z·X² + 1` -/ + +/-- `Φ` has constant coefficient `B²`: it is coprime to `X`. This is the +design doc's `φ(ta(0)) = B² ≠ 0` case of the squarefreeness lemma. -/ +theorem phiPoly_coeff_zero : G.phiPoly.coeff 0 = G.E.B^2 := by + rw [coeff_zero_eq_eval_zero, G.eval_phiPoly, G.phiCore_zero] + +/-- `Φ` is coprime to `Z·X² + 1`: modulo that factor, `ta = 0` and +`Φ = B²`. This is the design doc's coprimality of `Φ` with the models' +quadratic factor. -/ +theorem phiPoly_isCoprime_tPoly_add_one : + IsCoprime G.phiPoly (G.tPoly + 1) := by + refine isCoprime_of_bezout (u := 1) + (v := -(G.tPoly * ((C G.E.B)^2 * G.taPoly^2 + + (3*(C G.E.B)^2 + (C G.E.A)^3) * G.taPoly + 3*(C G.E.B)^2))) + (c := G.E.B^2) (pow_ne_zero 2 G.E.B_nonzero) ?_ + have hC : (C (G.E.B^2) : Polynomial F) = (C G.E.B)^2 := map_pow _ _ _ + rw [hC, phiPoly, taPoly, tPoly] + ring + +/-- `Z·X² + 1` is separable: its Bézout certificate against its derivative +`2·Z·X` has the constant `2`. -/ +theorem tPoly_add_one_separable : (G.tPoly + 1).Separable := by + have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + have hd : (G.tPoly + 1).derivative = 2 * C G.Z * X := by + simp only [tPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] + ring + rw [Polynomial.separable_def, hd] + refine isCoprime_of_bezout (u := 2) (v := -X) (c := 2) h2 ?_ + have hC2 : (C (2 : F) : Polynomial F) = 2 := map_ofNat _ 2 + rw [tPoly, hC2] + ring + +/-! ## Separability of the cubic, by Bézout certificate + +The cofactors were computed by `xgcd` in `scripts/check_weil_derivations.sage`; +the identity's constant is `A³·B²·(4·A³ + 27·B²)`, nonzero exactly from the +standing assumptions plus ellipticity. -/ + +/-- The cubic `φ(T) = B²·(T + 1)³ + A³·T²` through which the core factors: +`Φ = φ ∘ ta` (design doc §2, the squarefreeness lemma). -/ +noncomputable def phiCubic : Polynomial F := + (C G.E.B)^2 * (X + 1)^3 + (C G.E.A)^3 * X^2 + +/-- `Φ` factors through `ta`: `Φ = φ ∘ ta`. -/ +theorem phiPoly_eq_comp : G.phiPoly = G.phiCubic.comp G.taPoly := by + simp only [phiPoly, phiCubic, add_comp, mul_comp, pow_comp, C_comp, X_comp, + one_comp] + +/-- The derivative of the cubic `φ`. -/ +theorem phiCubic_derivative : + G.phiCubic.derivative = 3*(C G.E.B)^2 * (X + 1)^2 + 2*(C G.E.A)^3 * X := by + simp only [phiCubic, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] + ring + +/-- **The cubic `φ` is separable**, by the Bézout certificate +`s·φ + t·φ′ = A³·B²·(4·A³ + 27·B²)` computed in +`scripts/check_weil_derivations.sage`: the identity's constant is a product +of exactly the standing nonzero quantities. -/ +theorem phiCubic_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.phiCubic.Separable := by + refine isCoprime_of_bezout + (u := (6*(C G.E.A)^3*(C G.E.B)^2 + 36*(C G.E.B)^4) * X + + (4*(C G.E.A)^6 + 36*(C G.E.A)^3*(C G.E.B)^2 + 63*(C G.E.B)^4)) + (v := -((2*(C G.E.A)^3*(C G.E.B)^2 + 12*(C G.E.B)^4) * X^2) + - (2*(C G.E.A)^6 + 18*(C G.E.A)^3*(C G.E.B)^2 + 33*(C G.E.B)^4) * X + - (3*(C G.E.A)^3*(C G.E.B)^2 + 21*(C G.E.B)^4)) + (c := G.E.A^3 * G.E.B^2 * (4*G.E.A^3 + 27*G.E.B^2)) + (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 2 G.E.B_nonzero)) hdisc) ?_ + have hC : (C (G.E.A^3 * G.E.B^2 * (4*G.E.A^3 + 27*G.E.B^2)) : Polynomial F) + = (C G.E.A)^3 * (C G.E.B)^2 * (4*(C G.E.A)^3 + 27*(C G.E.B)^2) := by + simp only [map_mul, map_pow, map_add, map_ofNat] + rw [phiCubic_derivative, phiCubic, hC] + ring + +/-! ## `Φ` is coprime to the factors of `ta′` -/ + +/-- The derivative of `ta` factors as `(2·Z·X)·(2·Z·X² + 1)` — the critical +points of `ta` are `u = 0` and the locus `Z·u² = -1/2`. -/ +theorem taPoly_derivative : + G.taPoly.derivative = (2 * C G.Z * X) * (2 * C G.Z * X^2 + 1) := by + simp only [taPoly, tPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, Nat.cast_ofNat, map_ofNat] + ring + +/-- A polynomial with nonzero constant coefficient is coprime to `X`. -/ +theorem _root_.CompElliptic.Hashing.isCoprime_X_of_coeff_zero + {F : Type*} [Field F] {p : Polynomial F} (h : p.coeff 0 ≠ 0) : + IsCoprime p X := by + refine isCoprime_of_bezout (u := 1) (v := -p.divX) (c := p.coeff 0) h ?_ + linear_combination -(X_mul_divX_add p) + +/-- Nonzero constants are coprime to everything. -/ +theorem _root_.CompElliptic.Hashing.isCoprime_C_of_ne_zero + {F : Type*} [Field F] {p : Polynomial F} {c : F} (hc : c ≠ 0) : + IsCoprime p (C c) := + ⟨0, C c⁻¹, by simp [← C_mul, inv_mul_cancel₀ hc]⟩ + +/-- The even-powers polynomial `Ψ` with `64·Φ = Ψ(2·Z·X² + 1)`: the core, +re-expanded around the second critical locus of `ta`. Its constant term is +the ellipticity `4·A³ + 27·B²` — the design doc's `64·φ(-1/4)`. -/ +noncomputable def psiPoly : Polynomial F := + (C G.E.B)^2 * X^6 + (4*(C G.E.A)^3 + 9*(C G.E.B)^2) * X^4 + + (27*(C G.E.B)^2 - 8*(C G.E.A)^3) * X^2 + + (4*(C G.E.A)^3 + 27*(C G.E.B)^2) + +/-- `Ψ`'s constant coefficient is the ellipticity. -/ +theorem psiPoly_coeff_zero : + G.psiPoly.coeff 0 = 4*G.E.A^3 + 27*G.E.B^2 := by + rw [coeff_zero_eq_eval_zero] + simp [psiPoly] + +/-- The re-expansion `64·Φ = Ψ(2·Z·X² + 1)`, checked symbolically in +`scripts/check_weil_derivations.sage`. -/ +theorem phiPoly_64_eq : + 64 * G.phiPoly = G.psiPoly.comp (2 * C G.Z * X^2 + 1) := by + simp only [psiPoly, phiPoly, taPoly, tPoly, add_comp, mul_comp, pow_comp, + sub_comp, C_comp, X_comp, ofNat_comp, Nat.cast_ofNat] + ring + +/-- `Φ` is coprime to `2·Z·X² + 1`: modulo that factor, `64·Φ` is the +nonzero constant `4·A³ + 27·B²`. This is the design doc's `ta = -1/4` case +of the squarefreeness lemma. -/ +theorem phiPoly_isCoprime_snd (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + IsCoprime G.phiPoly (2 * C G.Z * X^2 + 1) := by + refine isCoprime_of_bezout (u := 64) + (v := -(G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1))) + (c := 4*G.E.A^3 + 27*G.E.B^2) hdisc ?_ + have h := X_mul_divX_add G.psiPoly + rw [G.psiPoly_coeff_zero] at h + have hcomp : G.psiPoly.comp (2 * C G.Z * X^2 + 1) + = (2 * C G.Z * X^2 + 1) * G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1) + + C (4*G.E.A^3 + 27*G.E.B^2) := by + conv_lhs => rw [← h] + simp only [add_comp, mul_comp, X_comp, C_comp] + calc 64 * G.phiPoly + -(G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1)) + * (2 * C G.Z * X^2 + 1) + = G.psiPoly.comp (2 * C G.Z * X^2 + 1) + - (2 * C G.Z * X^2 + 1) * G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1) + := by rw [G.phiPoly_64_eq]; ring + _ = C (4*G.E.A^3 + 27*G.E.B^2) := by rw [hcomp]; ring + +/-! ## `Φ` is squarefree -/ + +/-- **`Φ` is separable**: its derivative is `(φ′ ∘ ta)·ta′` by the chain +rule, `φ′ ∘ ta` is coprime to `Φ = φ ∘ ta` because the cubic's Bézout +certificate transports along composition, and each factor of `ta′` is +handled by the two critical-value cases. This is the design doc's +squarefreeness lemma (§2), step for step. -/ +theorem phiPoly_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.phiPoly.Separable := by + have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + rw [Polynomial.separable_def, G.phiPoly_eq_comp, derivative_comp, + taPoly_derivative, ← G.phiPoly_eq_comp] + refine IsCoprime.mul_right (IsCoprime.mul_right ?_ ?_) ?_ + · -- `2·Z·X`: a nonzero constant times `X`, and `Φ(0) = B² ≠ 0`. + have hconst : (2 : Polynomial F) * C G.Z = C (2 * G.Z) := by + rw [C_mul, map_ofNat] + rw [hconst] + exact IsCoprime.mul_right + (isCoprime_C_of_ne_zero (mul_ne_zero h2 G.Z_nonzero)) + (isCoprime_X_of_coeff_zero (by + rw [G.phiPoly_coeff_zero] + exact pow_ne_zero 2 G.E.B_nonzero)) + · exact G.phiPoly_isCoprime_snd hdisc + · -- `φ′ ∘ ta`, by transporting the cubic's certificate along `comp ta`. + rw [G.phiPoly_eq_comp] + exact IsCoprime.map (G.phiCubic_separable hdisc) + (eval₂RingHom (C : F →+* Polynomial F) G.taPoly) + +/-- **`Φ` is squarefree** — the input the cited hyperelliptic genus formula +consumes (design doc §2). -/ +theorem phiPoly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.phiPoly := + (G.phiPoly_separable hdisc).squarefree + +/-! ## The models are squarefree of degree 14 -/ + +/-- **The first model is squarefree**: a unit times the product of the two +coprime separable factors `Z·X² + 1` and `Φ`. -/ +theorem model1Poly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.model1Poly := by + refine Polynomial.Separable.squarefree ?_ + rw [model1Poly] + have hunit : IsUnit (C G.twist1) := isUnit_C.mpr G.twist1_ne_zero.isUnit + refine Polynomial.Separable.mul ((separable_C _).mpr G.twist1_ne_zero.isUnit) + (Polynomial.Separable.mul G.tPoly_add_one_separable + (G.phiPoly_separable hdisc) + ((G.phiPoly_isCoprime_tPoly_add_one).symm)) ?_ + exact (isCoprime_C_of_ne_zero G.twist1_ne_zero).symm + +/-- **The second model is squarefree**; see `model1Poly_squarefree`. -/ +theorem model2Poly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.model2Poly := by + refine Polynomial.Separable.squarefree ?_ + rw [model2Poly] + refine Polynomial.Separable.mul ((separable_C _).mpr G.twist2_ne_zero.isUnit) + (Polynomial.Separable.mul G.tPoly_add_one_separable + (G.phiPoly_separable hdisc) + ((G.phiPoly_isCoprime_tPoly_add_one).symm)) ?_ + exact (isCoprime_C_of_ne_zero G.twist2_ne_zero).symm + +/-- **The first model has degree 14** — with squarefreeness, the input to +the cited genus formula `g = ⌊(14 - 1)/2⌋ = 6` (Galbraith ch. 10; +Stichtenoth ch. 6). -/ +theorem model1Poly_natDegree : G.model1Poly.natDegree = 14 := by + rw [model1Poly, phiPoly, taPoly, tPoly] + compute_degree! + repeat' constructor + all_goals first + | exact G.E.B_nonzero + | exact G.Z_nonzero + | exact G.twist1_ne_zero + +/-- **The second model has degree 14**; see `model1Poly_natDegree`. -/ +theorem model2Poly_natDegree : G.model2Poly.natDegree = 14 := by + rw [model2Poly, phiPoly, taPoly, tPoly] + compute_degree! + repeat' constructor + all_goals first + | exact G.E.B_nonzero + | exact G.Z_nonzero + | exact G.twist2_ne_zero + +/-! ## The fibre over `w = 0` -/ + +/-- `g(-B/A) = -(B/A)³`: the curve equation at the abscissa of the two +points over `w = 0`. -/ +theorem eval_g_neg_B_div_A : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B + = -(G.E.B/G.E.A)^3 := by + have hA := G.A_nonzero + field_simp + ring + +/-- `g(-B/A) ≠ 0`: the two points over `w = 0` have nonzero ordinate, so +`w` vanishes simply at each — the input that makes the Eisenstein pattern +mean total ramification in the cited argument. -/ +theorem g_neg_B_div_A_ne_zero : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B ≠ 0 := by + rw [G.eval_g_neg_B_div_A] + exact neg_ne_zero.mpr (pow_ne_zero 3 + (div_ne_zero G.E.B_nonzero G.A_nonzero)) + +/-! ## The branch quartics are Eisenstein at `w = 0` + +The design doc's §3 works over the function field of the curve, where `w` +vanishes simply at the two points over `w = 0` (because +`g(-B/A) = -(B/A)³ ≠ 0`). The checkable input is the Eisenstein coefficient +pattern of the quartics over `F[w]`, at the ideal `(w)`; the step from the +pattern to total ramification —and from there to the absence of unramified +subcovers— is the cited part. -/ + +/-- The second branch quartic `P₂ = B·Z²·u⁴ + Z·w·u² + w`, over `F[w]` +(the inner variable is `w`, the outer `u`). -/ +noncomputable def p2Poly : Polynomial (Polynomial F) := + C (C (G.E.B * G.Z^2)) * X^4 + C (C G.Z * X) * X^2 + C (X : Polynomial F) + +/-- The reciprocal of the first branch quartic: +`B·u⁴ + Z·w·u² + Z²·w`. -/ +noncomputable def p1RecipPoly : Polynomial (Polynomial F) := + C (C G.E.B) * X^4 + C (C G.Z * X) * X^2 + C (C (G.Z^2) * X) + +/-- `P₂` has degree 4. -/ +theorem p2Poly_natDegree : G.p2Poly.natDegree = 4 := by + rw [p2Poly] + compute_degree! + exact ⟨G.E.B_nonzero, G.Z_nonzero⟩ + +/-- The reciprocal quartic has degree 4. -/ +theorem p1RecipPoly_natDegree : G.p1RecipPoly.natDegree = 4 := by + rw [p1RecipPoly] + compute_degree! + exact G.E.B_nonzero + +/-- Coefficients of `P₂`, by direct computation. -/ +theorem p2Poly_coeff : + G.p2Poly.coeff 0 = (X : Polynomial F) ∧ G.p2Poly.coeff 1 = 0 + ∧ G.p2Poly.coeff 2 = C G.Z * X ∧ G.p2Poly.coeff 3 = 0 + ∧ G.p2Poly.coeff 4 = C (G.E.B * G.Z^2) := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + · simp only [p2Poly, coeff_add, coeff_C_mul, coeff_X_pow, coeff_C] + norm_num + +/-- Coefficients of the reciprocal quartic, by direct computation. -/ +theorem p1RecipPoly_coeff : + G.p1RecipPoly.coeff 0 = C (G.Z^2) * X ∧ G.p1RecipPoly.coeff 1 = 0 + ∧ G.p1RecipPoly.coeff 2 = C G.Z * X ∧ G.p1RecipPoly.coeff 3 = 0 + ∧ G.p1RecipPoly.coeff 4 = C G.E.B := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + · simp only [p1RecipPoly, coeff_add, coeff_C_mul, coeff_X_pow, coeff_C] + norm_num + +/-- `X² ∤ c·X` in `F[w]` for a nonzero constant `c`: degree comparison. -/ +theorem _root_.CompElliptic.Hashing.not_X_sq_dvd {F : Type*} [Field F] + {c : Polynomial F} (hc : c ≠ 0) + (hdeg : c.natDegree = 0) : ¬ (X:Polynomial F)^2 ∣ c * X := by + intro hdvd + have hne : c * (X:Polynomial F) ≠ 0 := + mul_ne_zero hc X_ne_zero + have := Polynomial.natDegree_le_of_dvd hdvd hne + rw [natDegree_mul hc X_ne_zero, hdeg, natDegree_X, natDegree_pow, + natDegree_X] at this + omega + +/-- **`P₂` is Eisenstein at `(w)`** — the checkable input to the cited +total-ramification argument over the two points with `w = 0` (design doc +§3). Concretely: the leading coefficient `B·Z²` is not divisible by `w`, +the lower coefficients `w`, `0`, `Z·w`, `0` all are, and the constant +coefficient `w` is not divisible by `w²`. -/ +theorem p2Poly_isEisensteinAt : + G.p2Poly.IsEisensteinAt (Ideal.span {(X : Polynomial F)}) := by + obtain ⟨h0, h1, h2, h3, h4⟩ := G.p2Poly_coeff + have hdeg := G.p2Poly_natDegree + constructor + · -- The leading coefficient `B·Z²` is a unit, not in `(w)`. + rw [Polynomial.leadingCoeff, hdeg, h4, Ideal.mem_span_singleton, + X_dvd_iff, coeff_C] + exact fun h => G.E.B_nonzero (by + rcases mul_eq_zero.mp h with hB | hZ + · exact hB + · exact absurd hZ (pow_ne_zero 2 G.Z_nonzero)) + · -- Every lower coefficient is divisible by `w`. + intro n hn + rw [hdeg] at hn + interval_cases n <;> + simp [h0, h1, h2, h3, Ideal.mem_span_singleton, dvd_mul_left] + · -- The constant coefficient `w` is not in `(w)²`. + rw [h0, Ideal.span_singleton_pow, Ideal.mem_span_singleton] + intro hdvd + have := Polynomial.natDegree_le_of_dvd hdvd X_ne_zero + rw [natDegree_pow, natDegree_X] at this + omega + +/-- **The reciprocal of `P₁` is Eisenstein at `(w)`**; with +`p2Poly_isEisensteinAt`, both covers are totally ramified over `w = 0` in +the cited argument. -/ +theorem p1RecipPoly_isEisensteinAt : + G.p1RecipPoly.IsEisensteinAt (Ideal.span {(X : Polynomial F)}) := by + obtain ⟨h0, h1, h2, h3, h4⟩ := G.p1RecipPoly_coeff + have hdeg := G.p1RecipPoly_natDegree + constructor + · rw [Polynomial.leadingCoeff, hdeg, h4, Ideal.mem_span_singleton, + X_dvd_iff, coeff_C] + exact G.E.B_nonzero + · intro n hn + rw [hdeg] at hn + interval_cases n <;> + simp [h0, h1, h2, h3, Ideal.mem_span_singleton, dvd_mul_left] + · rw [h0, Ideal.span_singleton_pow, Ideal.mem_span_singleton] + exact not_X_sq_dvd (C_ne_zero.mpr (pow_ne_zero 2 G.Z_nonzero)) + (natDegree_C _) + +/-! ## The monodromy square exclusions + +Design doc §3 pins the monodromy group at full `D₄`: the biquadratic +V₄/C₄ square-class tests reduce to `B·(A·x + B)` and `B·(A·x - 3·B)` +being squares in `F_q(E′)`, and both fail. The paper argument is +divisor parity. Its checkable core is elementary, because `F_q(E′)` is +the quadratic algebra `K[Y]/(Y² - ĝ)` over `K = F_q(x)`: + +* a square from the base decomposes there — `a = p²` or `a = ĝ·p²` in + `K` (`sq_or_mul_sq_of_isSquare_adjoinRoot`); +* a rational square root of a polynomial is a polynomial + (`exists_sq_eq_of_ratFunc_sq` — `F[X]` is integrally closed); +* a squarefree polynomial of positive degree is not a polynomial square + (`not_isSquare_ratFunc_of_squarefree`) — the affine shadow of the + divisor parity. + +The Kappe–Warren reduction to the two square classes stays cited; it is +checked symbolically in `scripts/check_weil_derivations.sage`, along +with the Bézout certificates used below. -/ + +/-- A rational square root of a polynomial is a polynomial: `F[X]` is +integrally closed in `F(X)`, and an element whose square is a polynomial +is integral over `F[X]`. -/ +theorem _root_.CompElliptic.Hashing.exists_sq_eq_of_ratFunc_sq + {F : Type*} [Field F] {n : Polynomial F} {p : RatFunc F} + (h : p^2 = algebraMap (Polynomial F) (RatFunc F) n) : + ∃ f : Polynomial F, f^2 = n := by + have hint : IsIntegral (Polynomial F) p := + ⟨X^2 - C n, monic_X_pow_sub_C n (by norm_num), by + simp only [eval₂_sub, eval₂_pow, eval₂_X, eval₂_C] + rw [h, sub_self]⟩ + obtain ⟨f, hf⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint + refine ⟨f, IsFractionRing.injective (Polynomial F) (RatFunc F) ?_⟩ + rw [map_pow, hf, h] + +/-- A squarefree polynomial of positive degree is not a square in the +rational-function field: a rational square root would be a polynomial +(`exists_sq_eq_of_ratFunc_sq`). Its square divides the squarefree +target, so it is a unit and the target is constant. -/ +theorem _root_.CompElliptic.Hashing.not_isSquare_ratFunc_of_squarefree + {F : Type*} [Field F] {n : Polynomial F} (hsf : Squarefree n) + (hdeg : n.natDegree ≠ 0) : + ¬ IsSquare (algebraMap (Polynomial F) (RatFunc F) n) := by + rintro ⟨p, hp⟩ + obtain ⟨f, hf⟩ := exists_sq_eq_of_ratFunc_sq (p := p) + (by rw [sq]; exact hp.symm) + have hunit : IsUnit f := hsf f ⟨1, by rw [← hf]; ring⟩ + refine hdeg ?_ + rw [← hf, natDegree_pow, natDegree_eq_zero_of_isUnit hunit, mul_zero] + +/-- **Squares from the base of a quadratic extension decompose**. Write +a square root of `a` in `K[Y]/(Y² - g)` as `p₀ + p₁·Y`; its square is +`(p₀² + g·p₁²) + 2·p₀·p₁·Y`. So away from characteristic 2, either +`a = p₀²` or `a = g·p₁²` in `K`. -/ +theorem _root_.CompElliptic.Hashing.sq_or_mul_sq_of_isSquare_adjoinRoot + {K : Type*} [Field K] (h2 : (2 : K) ≠ 0) {g a : K} + (h : IsSquare (AdjoinRoot.of (X^2 - C g) a)) : + (∃ p : K, a = p^2) ∨ ∃ p : K, a = g * p^2 := by + have hmonic : (X^2 - C g).Monic := monic_X_pow_sub_C g (by norm_num) + have hdeg2 : (X^2 - C g).degree = 2 := degree_X_pow_sub_C (by norm_num) g + -- Representations `of x + of y · root` are unique: a difference lifts + -- to a polynomial of degree at most 1 divisible by the monic quadratic. + have huniq : ∀ x y x' y' : K, + AdjoinRoot.of (X^2 - C g) x + + AdjoinRoot.of (X^2 - C g) y * AdjoinRoot.root (X^2 - C g) + = AdjoinRoot.of (X^2 - C g) x' + + AdjoinRoot.of (X^2 - C g) y' * AdjoinRoot.root (X^2 - C g) → + x = x' ∧ y = y' := by + intro x y x' y' hxy + have hmk : AdjoinRoot.mk (X^2 - C g) + (C (x - x') + C (y - y') * X) = 0 := by + rw [map_add, map_mul, AdjoinRoot.mk_C, AdjoinRoot.mk_C, + AdjoinRoot.mk_X, map_sub, map_sub] + linear_combination hxy + have hzero : (C (x - x') + C (y - y') * X : Polynomial K) = 0 := by + refine eq_zero_of_dvd_of_degree_lt (AdjoinRoot.mk_eq_zero.mp hmk) ?_ + rw [hdeg2, add_comm] + exact lt_of_le_of_lt degree_linear_le + (by exact_mod_cast (by norm_num : (1 : ℕ) < 2)) + constructor + · have h0 : x - x' = 0 := by + simpa using congrArg (fun p => Polynomial.coeff p 0) hzero + exact sub_eq_zero.mp h0 + · have h1 : y - y' = 0 := by + simpa using congrArg (fun p => Polynomial.coeff p 1) hzero + exact sub_eq_zero.mp h1 + obtain ⟨z, hz⟩ := h + obtain ⟨r, rfl⟩ := AdjoinRoot.mk_surjective z + -- Reduce the representative modulo the monic quadratic. + have hzr : AdjoinRoot.mk (X^2 - C g) r + = AdjoinRoot.mk (X^2 - C g) (r %ₘ (X^2 - C g)) := by + conv_lhs => rw [← modByMonic_add_div r (X^2 - C g)] + rw [map_add, map_mul, AdjoinRoot.mk_self, zero_mul, add_zero] + set p0 := (r %ₘ (X^2 - C g)).coeff 0 with hp0 + set p1 := (r %ₘ (X^2 - C g)).coeff 1 with hp1 + have hrep : r %ₘ (X^2 - C g) = C p1 * X + C p0 := by + rcases eq_or_ne (r %ₘ (X^2 - C g)) 0 with h0 | h0 + · rw [hp0, hp1, h0] + simp + · refine eq_X_add_C_of_degree_le_one ?_ + have hlt := degree_modByMonic_lt r hmonic + rw [hdeg2, degree_eq_natDegree h0] at hlt + rw [degree_eq_natDegree h0] + exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast hlt) + have hroot : (AdjoinRoot.root (X^2 - C g))^2 + = AdjoinRoot.of (X^2 - C g) g := by + have h0 := AdjoinRoot.mk_self (f := X^2 - C g) + rw [map_sub, map_pow, AdjoinRoot.mk_X, AdjoinRoot.mk_C, + sub_eq_zero] at h0 + exact h0 + -- Expand `of a = (of p1 · root + of p0)²` over the basis `{1, root}`. + have hexpand : AdjoinRoot.of (X^2 - C g) a + = AdjoinRoot.of (X^2 - C g) (p0^2 + g * p1^2) + + AdjoinRoot.of (X^2 - C g) (2 * p0 * p1) + * AdjoinRoot.root (X^2 - C g) := by + rw [hz, hzr, hrep] + simp only [map_add, map_mul, map_pow, map_ofNat, AdjoinRoot.mk_C, + AdjoinRoot.mk_X] + linear_combination (AdjoinRoot.of (X^2 - C g) p1)^2 * hroot + obtain ⟨ha, hb⟩ := huniq a 0 (p0^2 + g * p1^2) (2 * p0 * p1) (by + rw [map_zero, zero_mul, add_zero] + exact hexpand) + have hzero : p0 = 0 ∨ p1 = 0 := by + rcases mul_eq_zero.mp hb.symm with h' | h' + · rcases mul_eq_zero.mp h' with h'' | h'' + · exact absurd h'' h2 + · exact Or.inl h'' + · exact Or.inr h' + rcases hzero with h' | h' + · exact Or.inr ⟨p1, by rw [ha, h']; ring⟩ + · exact Or.inl ⟨p0, by rw [ha, h']; ring⟩ + +/-- The curve cubic `g = X³ + A·X + B` as a polynomial over `F`. +Adjoining a square root of its image `ĝ` in `K = F_q(x)` presents the +function field `F_q(E′)`. -/ +noncomputable def gPoly : Polynomial F := X^3 + C G.E.A * X + C G.E.B + +/-- `g` is separable, by the Bézout certificate +`(27·B - 18·A·X)·g + (6·A·X² - 9·B·X + 4·A²)·g′ = 4·A³ + 27·B²` +(checked in `scripts/check_weil_derivations.sage`): the constant is +nonzero exactly by ellipticity. -/ +theorem gPoly_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.gPoly.Separable := by + have hd : G.gPoly.derivative = 3 * X^2 + C G.E.A := by + simp only [gPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, Nat.cast_ofNat, map_ofNat] + ring + rw [Polynomial.separable_def, hd] + refine isCoprime_of_bezout + (u := 27 * C G.E.B - 18 * C G.E.A * X) + (v := 6 * C G.E.A * X^2 - 9 * C G.E.B * X + 4 * (C G.E.A)^2) + (c := 4*G.E.A^3 + 27*G.E.B^2) hdisc ?_ + have hC : (C (4*G.E.A^3 + 27*G.E.B^2) : Polynomial F) + = 4*(C G.E.A)^3 + 27*(C G.E.B)^2 := by + simp only [map_add, map_mul, map_pow, map_ofNat] + rw [gPoly, hC] + ring + +/-- `ĝ` is not a square in `F_q(x)`: `g` is squarefree of odd degree. So +`Y² - ĝ` is irreducible and the quadratic algebra below is the function +field `F_q(E′)` itself. (The exclusions need only the ring structure, so +that last step stays informal.) -/ +theorem gPoly_not_isSquare_ratFunc + (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (algebraMap (Polynomial F) (RatFunc F) G.gPoly) := by + refine not_isSquare_ratFunc_of_squarefree + (G.gPoly_separable hdisc).squarefree ?_ + have h3 : G.gPoly.natDegree = 3 := by unfold gPoly; compute_degree! + omega + +/-- **The common core of the two exclusions**: for any linear `l` +coprime to `g`, the class `B·l` is not a square in the quadratic +algebra `K[Y]/(Y² - ĝ)`. A square would decompose as `p²` or `ĝ·p²` +over `K` (`sq_or_mul_sq_of_isSquare_adjoinRoot`), and each case +descends to a polynomial square (`exists_sq_eq_of_ratFunc_sq`). That +contradicts the squarefreeness of `B·l` (degree 1) and of `B·l·g` +(degree 4) respectively, by `not_isSquare_ratFunc_of_squarefree`. -/ +theorem not_isSquare_adjoinRoot_of_linear + (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) {l : Polynomial F} + (hdeg : l.natDegree = 1) (hcop : IsCoprime l G.gPoly) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) (C G.E.B * l))) := by + intro hsq + -- Characteristic ≠ 2 (`Z` is a nonsquare) transfers to `F_q(x)`. + have h2F : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + have h2P : (2 : Polynomial F) ≠ 0 := fun h => h2F (by + simpa using congrArg (fun p => Polynomial.coeff p 0) h) + have h2 : (2 : RatFunc F) ≠ 0 := fun h => h2P + (IsFractionRing.injective (Polynomial F) (RatFunc F) + (by rw [map_ofNat, map_zero]; exact h)) + -- The linear factor and both products are squarefree, with known + -- degrees. + have hl0 : l ≠ 0 := fun h => by simp [h] at hdeg + have hl1 : l.coeff 1 ≠ 0 := by + have hlc := leadingCoeff_ne_zero.mpr hl0 + rwa [Polynomial.leadingCoeff, hdeg] at hlc + have hlsep : l.Separable := by + have hd : l.derivative = C (l.coeff 1) := by + conv_lhs => rw [eq_X_add_C_of_natDegree_le_one hdeg.le] + simp only [derivative_add, derivative_mul, derivative_C, + derivative_X, zero_mul, mul_one, zero_add, add_zero] + rw [Polynomial.separable_def, hd] + exact isCoprime_C_of_ne_zero hl1 + have hτsep : (C G.E.B * l).Separable := + Polynomial.Separable.mul ((separable_C _).mpr G.E.B_nonzero.isUnit) + hlsep ((isCoprime_C_of_ne_zero G.E.B_nonzero).symm) + have hτdeg : (C G.E.B * l).natDegree = 1 := by + rw [natDegree_mul (C_ne_zero.mpr G.E.B_nonzero) hl0, natDegree_C, + zero_add, hdeg] + have hgm : G.gPoly.Monic := by + unfold gPoly + rw [add_assoc] + exact monic_X_pow_add (lt_of_le_of_lt degree_linear_le + (by exact_mod_cast (by norm_num : (1 : ℕ) < 3))) + have hg3 : G.gPoly.natDegree = 3 := by unfold gPoly; compute_degree! + have hτgsf : Squarefree (C G.E.B * l * G.gPoly) := + (Polynomial.Separable.mul hτsep (G.gPoly_separable hdisc) + (IsCoprime.mul_left ((isCoprime_C_of_ne_zero G.E.B_nonzero).symm) + hcop)).squarefree + -- Decompose the square over the base field and refute both cases. + rcases sq_or_mul_sq_of_isSquare_adjoinRoot h2 hsq with ⟨p, hp⟩ | ⟨p, hp⟩ + · exact not_isSquare_ratFunc_of_squarefree hτsep.squarefree + (by rw [hτdeg]; norm_num) ⟨p, by rw [hp, sq]⟩ + · refine not_isSquare_ratFunc_of_squarefree hτgsf + (by rw [natDegree_mul (mul_ne_zero (C_ne_zero.mpr G.E.B_nonzero) hl0) + hgm.ne_zero, hτdeg, hg3]; norm_num) + ⟨algebraMap (Polynomial F) (RatFunc F) G.gPoly * p, ?_⟩ + rw [map_mul, hp] + ring + +/-- The V₄-test square class of the branch quartics: `B·w = B·(A·x + B)`. -/ +noncomputable def v4TestPoly : Polynomial F := + C G.E.B * (C G.E.A * X + C G.E.B) + +/-- The C₄-test square class of the branch quartics: `B·(A·x - 3·B)`. -/ +noncomputable def c4TestPoly : Polynomial F := + C G.E.B * (C G.E.A * X - 3 * C G.E.B) + +/-- **The V₄ exclusion** (design doc §3): `B·(A·x + B)` is not a square +in the function field. The coprimality certificate is +`(A²·X² - A·B·X + (B² + A³))·(A·X + B) - A³·g = B³` (checked in +`scripts/check_weil_derivations.sage`). -/ +theorem v4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) G.v4TestPoly)) := by + have hdeg : (C G.E.A * X + C G.E.B).natDegree = 1 := by + compute_degree! + all_goals exact G.A_nonzero + have hcop : IsCoprime (C G.E.A * X + C G.E.B) G.gPoly := by + refine isCoprime_of_bezout + (u := (C G.E.A)^2 * X^2 - C G.E.A * C G.E.B * X + + ((C G.E.B)^2 + (C G.E.A)^3)) + (v := -(C G.E.A)^3) + (c := G.E.B^3) (pow_ne_zero 3 G.E.B_nonzero) ?_ + have hC : (C (G.E.B^3) : Polynomial F) = (C G.E.B)^3 := map_pow _ _ _ + rw [gPoly, hC] + ring + unfold v4TestPoly + exact G.not_isSquare_adjoinRoot_of_linear hdisc hdeg hcop + +/-- **The C₄ exclusion** (design doc §3): `B·(A·x - 3·B)` is not a square +in the function field. The coprimality certificate is +`A³·g - (A²·X² + 3·A·B·X + (9·B² + A³))·(A·X - 3·B) = B·(4·A³ + 27·B²)` +(checked in `scripts/check_weil_derivations.sage`); its constant is again +a product of the standing nonzero quantities. -/ +theorem c4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) G.c4TestPoly)) := by + have hdeg : (C G.E.A * X - 3 * C G.E.B).natDegree = 1 := by + compute_degree! + all_goals exact G.A_nonzero + have hcop : IsCoprime (C G.E.A * X - 3 * C G.E.B) G.gPoly := by + refine isCoprime_of_bezout + (u := -((C G.E.A)^2 * X^2 + 3 * C G.E.A * C G.E.B * X + + (9*(C G.E.B)^2 + (C G.E.A)^3))) + (v := (C G.E.A)^3) + (c := G.E.B * (4*G.E.A^3 + 27*G.E.B^2)) + (mul_ne_zero G.E.B_nonzero hdisc) ?_ + have hC : (C (G.E.B * (4*G.E.A^3 + 27*G.E.B^2)) : Polynomial F) + = C G.E.B * (4*(C G.E.A)^3 + 27*(C G.E.B)^2) := by + simp only [map_mul, map_add, map_pow, map_ofNat] + rw [gPoly, hC] + ring + unfold c4TestPoly + exact G.not_isSquare_adjoinRoot_of_linear hdisc hdeg hcop + +end SSWUParams + +end CompElliptic.Hashing diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 09198b3..293ff2d 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -106,13 +106,14 @@ 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 bound is proven in + the deployed sizes with margin `≈ 2^{126}`. 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. + and Theorem 3, and standard hyperelliptic point bookkeeping). The + calculation and the paper proof's supporting facts are formalized + (`Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, + `Hashing/WeilSupport.lean`). Separately, `WeilBounded` itself is an + external input to the formalization. -/ namespace CompElliptic.Hashing @@ -140,4 +141,20 @@ theorem WeilBounded.deviation {f : F → G} {C : ℝ} (h : WeilBounded f C) ‖∑ Q, ((mult f Q : ℂ) - 1) * ψ Q‖^2 ≤ C^2 * (Fintype.card F : ℝ) := by rw [← charSum_eq hψ]; exact h ψ hψ +omit [AddCommGroup F] [DecidableEq F] [Fintype G] [DecidableEq G] in +/-- The Weil bound transfers along a bijective homomorphism of the target +group. Characters of the new target pull back along the homomorphism; +surjectivity keeps nontrivial characters nontrivial, and the pulled-back +sum is the original one. This is what carries the bound across the deployed +isogeny, which is bijective on rational points. -/ +theorem WeilBounded.comp {G' : Type*} [AddCommGroup G'] [Fintype G'] + [DecidableEq G'] {f : F → G} {C : ℝ} (h : WeilBounded f C) (e : G →+ G') + (he : Function.Bijective e) : WeilBounded (fun u => e (f u)) C := by + intro ψ hψ + have hone : (1 : AddChar G' ℂ).compAddMonoidHom e = 1 := by + ext a; simp + have hne : ψ.compAddMonoidHom e ≠ 1 := fun hc => + hψ (AddChar.compAddMonoidHom_injective_left e he.2 (hc.trans hone.symm)) + simpa using h (ψ.compAddMonoidHom e) hne + end CompElliptic.Hashing diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index fc6cb6d..9810f6b 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -6,6 +6,8 @@ Authors: Daira-Emma Hopwood -/ import CompElliptic.Curves.PastaOrder import CompElliptic.Hashing.PastaSSWU +import CompElliptic.Hashing.TwoTermUniformity +import CompElliptic.Hashing.WeilSupport import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv @@ -140,3 +142,133 @@ assert_axioms CompElliptic.Curves.Pasta.Fast.Msm.pippengerFastPar_eq_msm assert_axioms CompElliptic.Curves.Pasta.Fast.Msm.commitLagrangeFastWith_eq assert_axioms CompElliptic.Curves.Pasta.Fast.ProjectiveMont.pnsmulM_spec assert_axioms CompElliptic.Curves.Pasta.Fast.ProjectiveMont.msmM_spec + +/-! ## The Weil-derivation design doc's citations + +`design/weil-constant-derivation.md` is a pencil-and-paper proof whose reader relies on +every Lean declaration it cites. To avoid a resulting axiom-checking gap, every such +declaration must be pinned here (checked in CI by `scripts/check_weil_support_refs.py`). +Definitions of polynomials in these modules use Mathlib's noncomputable ones, so they +take `assert_axioms` like the theorems and `Prop`-shaped definitions. -/ + +/-! ### The abscissae, branch covers, and models (`Hashing/BranchCovers.lean`, +`Hashing/FibreBound.lean`, `Hashing/SimplifiedSWU.lean`, `Hashing/SignedLift.lean`) -/ + +assert_computable CompElliptic.Hashing.SSWUParams.x1 +assert_computable CompElliptic.Hashing.SSWUParams.x2 +assert_computable CompElliptic.Hashing.SSWUParams.phiCore +assert_computable CompElliptic.Hashing.SSWUParams.twist1 +assert_computable CompElliptic.Hashing.SSWUParams.twist2 +assert_computable CompElliptic.Hashing.SSWUParams.model1 +assert_computable CompElliptic.Hashing.SSWUParams.model2 +assert_computable CompElliptic.Hashing.SSWUParams.scale1 +assert_computable CompElliptic.Hashing.SSWUParams.scale2 +assert_computable CompElliptic.Hashing.sgn0 +assert_axioms CompElliptic.Hashing.SSWUParams.map_neg +assert_axioms CompElliptic.Hashing.SSWUParams.Zuu_add_one_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.ta_ne_zero_of_u_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.g_x2_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model1_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model2_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model1_zero +assert_axioms CompElliptic.Hashing.SSWUParams.model2_zero +assert_axioms CompElliptic.Hashing.SSWUParams.scale1_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.scale2_ne_zero + +/-! ### The model point sets and covering maps (`Hashing/BranchCovers.lean`) -/ + +assert_computable CompElliptic.Hashing.SSWUParams.modelPoints1 +choice +assert_computable CompElliptic.Hashing.SSWUParams.modelPoints2 +choice +assert_computable CompElliptic.Hashing.SSWUParams.cover1Map +choice +assert_computable CompElliptic.Hashing.SSWUParams.cover2Map +choice +assert_axioms CompElliptic.Hashing.SSWUParams.fibre_sum +assert_axioms CompElliptic.Hashing.SSWUParams.modelPoints_sum + +/-! ### The supporting facts of the cited steps (`Hashing/WeilSupport.lean`) -/ + +assert_axioms CompElliptic.Hashing.isCoprime_of_bezout +assert_axioms CompElliptic.Hashing.isCoprime_X_of_coeff_zero +assert_axioms CompElliptic.Hashing.isCoprime_C_of_ne_zero +assert_axioms CompElliptic.Hashing.not_X_sq_dvd +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly_separable +assert_axioms CompElliptic.Hashing.SSWUParams.eval_g_neg_B_div_A +assert_axioms CompElliptic.Hashing.SSWUParams.g_neg_B_div_A_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic_derivative +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic_separable +assert_axioms CompElliptic.Hashing.SSWUParams.taPoly_derivative +assert_axioms CompElliptic.Hashing.SSWUParams.tPoly_add_one_separable +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_phiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_eq_comp +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_coeff_zero +assert_axioms CompElliptic.Hashing.SSWUParams.psiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.psiPoly_coeff_zero +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_64_eq +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_isCoprime_snd +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_isCoprime_tPoly_add_one +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_separable +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_model1Poly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_model2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_coeff +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_isEisensteinAt +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_coeff +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_isEisensteinAt +assert_axioms CompElliptic.Hashing.not_isSquare_ratFunc_of_squarefree +assert_axioms CompElliptic.Hashing.exists_sq_eq_of_ratFunc_sq +assert_axioms CompElliptic.Hashing.sq_or_mul_sq_of_isSquare_adjoinRoot +assert_axioms CompElliptic.Hashing.SSWUParams.not_isSquare_adjoinRoot_of_linear +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly_not_isSquare_ratFunc +assert_axioms CompElliptic.Hashing.SSWUParams.v4TestPoly +assert_axioms CompElliptic.Hashing.SSWUParams.v4TestPoly_not_isSquare +assert_axioms CompElliptic.Hashing.SSWUParams.c4TestPoly +assert_axioms CompElliptic.Hashing.SSWUParams.c4TestPoly_not_isSquare + +/-! ### Characters and realness (`Hashing/CharacterSum.lean`) -/ + +assert_axioms CompElliptic.Hashing.charSum_eq +assert_axioms CompElliptic.Hashing.addChar_map_neg_eq_conj +assert_axioms CompElliptic.Hashing.IsOdd.mult_neg +assert_axioms CompElliptic.Hashing.IsOdd.conj_charSum +assert_axioms CompElliptic.Hashing.IsOdd.two_mul_charSum + +/-! ### The Weil-input shape and the assembly (`Hashing/WeilInstance.lean`, +`Hashing/WellDistributed.lean`, `Hashing/TwoTermUniformity.lean`) -/ + +assert_axioms CompElliptic.Hashing.CharSumBounded +assert_axioms CompElliptic.Hashing.SSWUParams.cover_charSum +assert_axioms CompElliptic.Hashing.SSWUParams.weilBounded_zeroRepaired +assert_axioms CompElliptic.Hashing.WeilBounded +assert_axioms CompElliptic.Hashing.WeilBounded.comp +assert_axioms CompElliptic.Hashing.sum_abs_prob_dev_le +assert_axioms CompElliptic.Hashing.sum_abs_prob_dev_transport_le + +/-! ### The deployed instances (`Hashing/PastaSSWU.lean`) -/ + +assert_computable CompElliptic.Curves.Pasta.Pallas.mapToCurve +choice +native( + CompElliptic.Fields.Pasta.pallasBase) +assert_computable CompElliptic.Curves.Pasta.Vesta.mapToCurve +choice +native( + CompElliptic.Fields.Pasta.vestaBase) +assert_axioms CompElliptic.Curves.Pasta.Pallas.neg_AB_not_isSquare +assert_axioms CompElliptic.Curves.Pasta.Vesta.neg_AB_not_isSquare +assert_axioms CompElliptic.Curves.Pasta.Pallas.weilBounded_zeroRepaired_mapToCurve +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.weilBounded_zeroRepaired_mapToCurve +native( + CompElliptic.Fields.Pasta.vestaBase, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_isoGpt) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 37ba871..343fbaa 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -11,17 +11,28 @@ 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²⁵⁴. +and q > 2^{254}. 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. +established mathematics: Weil's theorem in the form of Lemma 1 and +Theorem 3 of Farashahi–Fouque–Shparlinski–Tibouchi–Voloch +([eprint 2010/539](https://eprint.iacr.org/2010/539), "FFSTV"), and the +standard point bookkeeping for hyperelliptic models [Galbraith, ch. 10]. +The symbolic identities it relies on are checked by +`scripts/check_weil_derivations.sage`; the per-instance facts (the empty +w = 0 fibre, the Frobenius statistics, the square-class witnesses) by +`weilbound.sage`. The calculation from the per-cover Weil inputs to the +deployed constants is machine-checked (CompElliptic's +`Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, and +`Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two +cited steps (`Hashing/WeilSupport.lean`, whose facts are referenced at +their points of use below; CI checks that this document references all +of that file's declarations). Every declaration cited here is also +pinned in the axiom census (`CompElliptic/TrustBoundary.lean`), and CI +checks that too: a reader of this proof relies on everything it cites, +so an unpinned citation would be a gap in axiom-checking. The cited +steps themselves and Weil's theorem stay on paper — the vocabulary they +need is tracked at #30. ## Background @@ -34,8 +45,8 @@ Public Key Cryptography*, CUP 2012, free 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 +- **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). @@ -82,34 +93,43 @@ as above. - **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] + constant term exactly once, leading coefficient a unit. The + transplant is an instantiation rather than a new theorem — the + criterion is a statement about any discrete valuation, whose + hypotheses force the Newton polygon to a single segment of slope + −1/n, so every root has valuation 1/n. Its conclusion is what we + use: the polynomial is irreducible there and the cover is *totally + ramified* over that place. [Stichtenoth, ch. 3] [Newton polygons: + J. S. Milne, *Algebraic Number Theory*, course notes, ch. 7, + Prop. 7.44 (stated for characteristic zero, but the argument is + characteristic-free) — free at ] 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. +follow FFSTV's Theorem 6, adapted to these parameters and to +sign-freeness. ## 1. The branch covers -For ta ≠ 0 the simplified SWU abscissae are +For ta ≠ 0 the simplified SWU abscissae are (`x1`, `x2`) 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. +g(x₂) = t³·g(x₁) with t = Z·u² in the square class of Z (in cleared +form, `g_x2_eq`). 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 away +from 0 (`SSWUParams.map_neg`); on each deployed curve this is +`isOdd_zeroRepaired_mapToCurve`. 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.) +has no solutions (`Zuu_add_one_ne_zero`): **ta vanishes only at u = 0** +(`ta_ne_zero_of_u_ne_zero`), 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: @@ -130,22 +150,27 @@ 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** +with the **shared degree-12 core** (`phiPoly`, matching the pointwise +`phiCore` by `eval_phiPoly`) Φ(u) = B²·(ta + 1)³ + A³·ta². Using ta = Z·u²·(Z·u²+1) and clearing squares, the two curves have -hyperelliptic models +hyperelliptic models (`model1Poly`, `model2Poly`, evaluating to the +pointwise `model1`, `model2` by `eval_model1Poly`, `eval_model2Poly`; +their relation to the curve equation at x_j is `model1_eq`, `model2_eq`) 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. +So C₁ and C₂ are **quadratic twists of one another by Z** (`twist1`, +`twist2`, differing by Z³ = Z times a square) — 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). The +Z·u²+1 (`phiPoly_coeff_zero`, `phiPoly_isCoprime_tPoly_add_one`, with the +quadratic factor separable, `tPoly_add_one_separable`); its degree is +exactly 12 (leading coefficient B²·Z⁶ ≠ 0; `phiPoly_natDegree`). The odd-multiplicity part of the right-hand side is therefore (Z·u²+1)·Φ, of degree 14 — provided Φ is squarefree, which holds unconditionally: @@ -153,21 +178,34 @@ of degree 14 — provided Φ is squarefree, which holds unconditionally: 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 +φ(T) = B²·(T+1)³ + A³·T² = B²·T³ + (A³+3·B²)·T² + 3·B²·T + B² +(`phiCubic`, `phiPoly`, `phiPoly_eq_comp`; the derivative +`phiCubic_derivative`). 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 formal counterpart avoids the discriminant: `phiCubic_separable` +witnesses coprimality of φ and φ′ directly, by a Bézout identity with +constant A³·B²·(4·A³ + 27·B²), through the generic `isCoprime_of_bezout`.) +Otherwise ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2; +`taPoly_derivative`), so either u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0 +(`phiPoly_coeff_zero`, via `isCoprime_X_of_coeff_zero`), or Z·u₀² = −1/2, +where ta(u₀) = −1/4 and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity. +(Formally: the re-expansion 64·Φ = Ψ(2·Z·u² + 1), `psiPoly`, +`phiPoly_64_eq`, has constant term the ellipticity, `psiPoly_coeff_zero`, +giving `phiPoly_isCoprime_snd`.) Either way Φ(u₀) ≠ 0, a contradiction. ∎ + +The lemma is `phiPoly_squarefree` in `Hashing/WeilSupport.lean` +(separability `phiPoly_separable`, assembled with the generic +`isCoprime_C_of_ne_zero`), and the models inherit it: +`model1Poly_squarefree` and `model2Poly_squarefree`, squarefree of +degree exactly 14 (`model1Poly_natDegree`, `model2Poly_natDegree`). The discriminant factorization and both critical values are checked -symbolically in `scripts/weil-derivation-checks.sage`. So each C_j is +symbolically in `scripts/check_weil_derivations.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 @@ -183,31 +221,64 @@ 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 +(−B/A, ±y₀) with y₀² = g(−B/A) = −(B/A)³ ≠ 0 (B ≠ 0; +`eval_g_neg_B_div_A`, `g_neg_B_div_A_ne_zero`). 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. + coefficient B·Z² a unit (`p2Poly`, with the coefficient pattern + `p2Poly_coeff`, degree `p2Poly_natDegree`, and the criterion + `p2Poly_isEisensteinAt`). 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 = ∞. + polynomial B·u⁴ + Z·w·u² + Z²·w is Eisenstein at the same points + (`p1RecipPoly`, `p1RecipPoly_coeff`, `p1RecipPoly_natDegree`, + `p1RecipPoly_isEisensteinAt`, with `not_X_sq_dvd` for the (w)² + condition), 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. +with no condition beyond A·B ≠ 0. The coefficient patterns and the +fibre ordinate above are the formalized inputs; the step from them to +total ramification is the cited part. + +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. For +both quartics, these reduce to the same two classes: B·(A·x + B) and +B·(A·x − 3·B) being squares in F_q(E′). (The reductions are checked +symbolically in `scripts/check_weil_derivations.sage`.) Both fail by +divisor parity: each class 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. This is consistent +with the script's Frobenius statistics (5000 samples per branch match +the D₄ cycle-type proportions ⅛, ¼, ⅜, ¼ to within ±0.006) and with +its nonsquare specialization witnesses. + +The two failures are formalized as `v4TestPoly_not_isSquare` and +`c4TestPoly_not_isSquare` (the classes are `v4TestPoly`, `c4TestPoly`), +with no vocabulary beyond polynomials. F_q(E′) is the quadratic algebra +K[Y]/(Y² − ĝ) over K = F_q(x), for ĝ the image of the curve cubic +`gPoly`. The algebra is the field itself, because ĝ is not a square in +K (`gPoly_not_isSquare_ratFunc`, via `gPoly_separable`). The parity +argument's affine form rests on three facts: + +- a square from the base decomposes as p² or ĝ·p² + (`sq_or_mul_sq_of_isSquare_adjoinRoot`, in characteristic ≠ 2); +- a rational square root of a polynomial is a polynomial + (`exists_sq_eq_of_ratFunc_sq` — F_q[x] is integrally closed); +- a squarefree polynomial of positive degree is not a polynomial + square (`not_isSquare_ratFunc_of_squarefree`). + +The shared core `not_isSquare_adjoinRoot_of_linear` applies these to +B·l of degree 1 and to B·l·g of degree 4. The coprimality of each +linear factor l with g comes from a Bézout certificate. The two +constants are B³ and B·(4·A³ + 27·B²) — ellipticity yet again. (The +certificates are normalized with positive constants. That matches the +file's other certificates, and it keeps a negation out of the +constant-lifting step of the Lean proofs; it is why they differ by +sign from the naïve division remainders.) ## 4. The sign-free assembly @@ -215,16 +286,23 @@ 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. +(This is the cited Weil input. It enters the formal development squared +and over the model point sets, as the two `CharSumBounded` hypotheses +at bound 100·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 +u → −u shows S_f(χ) is real (`IsOdd.conj_charSum`), 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. +(`IsOdd.two_mul_charSum`), and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends +only on the ±-class of f(u) — which the sign rule never influences +(the identity χ(−P) = χ̄(P) behind the pairing is +`addChar_map_neg_eq_conj`). This is the same reduction that +`CharacterSum.lean` formalizes as the ±-class multiplicity form +(`charSum_eq`, with the symmetry from `IsOdd.mult_neg`). **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 @@ -234,19 +312,25 @@ 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. +exactly when the leading coefficient of H_j is a square. This reading +is what the point sets `modelPoints1`, `modelPoints2` encode: the +affine solutions of W² = H_j(u), plus the pair at infinity exactly +when the leading square class d_j·Z 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, +s₂ = A³·(Z·u²+1)² (`scale1`, `scale2`); the identities +g(x_j(u))·s_j(u)² = H_j(u) are checked symbolically and proven as +`model1_eq`, `model2_eq`. Since Z·u²+1 has no rational roots (−1/Z is +a nonsquare; `Zuu_add_one_ne_zero`), s_j(u₀) ≠ 0 for every input +u₀ ∉ {0} (`scale1_ne_zero`, `scale2_ne_zero`). 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: +(χ + χ̄)(f(u₀)); the other branch's fibre has no rational points. The +last two sentences are `fibre_sum`, with h_j in model coordinates as +`cover1Map`, `cover2Map`. 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 @@ -254,7 +338,8 @@ boundary cases: 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 = 0**: H_j(0) = d_j·B², in the square class of d_j + (`model1_zero`, `model2_zero`). - **u = ∞**: the leading coefficient of H_j is d_j·B²·Z⁷, in the square class of d_j·Z. @@ -266,7 +351,8 @@ 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 +fibre; the Euler certificates `neg_AB_not_isSquare`, one per +iso-curve), 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: @@ -274,6 +360,10 @@ Summing, with f(0) = 𝒪 and χ(𝒪) = 1: S_{C₁}(χ) + S_{C₂}(χ) = Σ_{u ≠ 0} (χ + χ̄)(f(u)) + 4 = 2·S_f(χ) − 2·χ(𝒪) + 4 = 2·S_f(χ) + 2. +The first equality is `modelPoints_sum`, stated for any +commutative-monoid-valued φ with the boundary contributing 4·φ(𝒪); +the character form through to the + 2 is `cover_charSum`. + (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 @@ -287,17 +377,24 @@ case, so this variant is not needed for them.) so |S_f(χ)| ≤ 10·√q + 1 for every nontrivial χ, on both deployed 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. +gives 10·√q + 3.) The square-root-free formal counterpart is +`weilBounded_zeroRepaired`: two `CharSumBounded` inputs at c²·#F yield +`WeilBounded` at c + 1/2, parametrically in the per-cover constant c; +the deployed c = 10 gives the recorded 21/2. 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. +transfers to the full `mapToCurve` verbatim (`WeilBounded.comp`; per +curve, `weilBounded_zeroRepaired_mapToCurve`). 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. +(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2^{126}. The +downstream regularity distance ε ≈ C²·√(#G)/#F (the budget shape of +`sum_abs_prob_dev_le`, carried to the deployed mapping by +`sum_abs_prob_dev_transport_le`) comes to about 2^{-120}, improving +the ≈ 2^{-116} previously quoted from the FFSTV-sized constant. diff --git a/scripts/check_sswu_small_curves.sage b/scripts/check_sswu_small_curves.sage new file mode 100644 index 0000000..9faae97 --- /dev/null +++ b/scripts/check_sswu_small_curves.sage @@ -0,0 +1,87 @@ +# Exact simplified-SWU branch statistics on small curves. +# +# The ironwood book's group-hash page makes three heuristic claims about +# the deployed-shape mapping, confirmed here by exhaustive computation on +# small instances (q ≡ 1 (mod 4), A·B ≠ 0, odd prime order, -A·B a +# nonsquare, Z the first nonsquare ∉ {0, -1}): +# +# * the images of the two branches f₁ and f₂ coincide, apart from a +# negligible proportion of exceptional points (the single-branch +# count is reported, not asserted — we have not proven a bound on +# the exceptional cases; it is zero at every instance here); +# * about 3/8 of the group is reached, with about 1/8 of the points +# having 4 preimages and about 1/4 having 2 (asserted to within +# 3/√q, the Lang–Weil-shaped error; the constants are not +# optimized); +# * every reached point other than 𝒪 has exactly 2 or 4 preimages +# (asserted exactly: a target's quadratic has 1 or 2 realizable +# roots, each contributing one preimage per branch). +# +# The w = 0 fibre is empty when -A·B is a nonsquare, so the only +# exceptional output is 𝒪 (from the repaired input u = 0). + +def sgn0(x): + return Integer(x) % 2 + +def find_instance(q): + F = GF(q) + for a in range(1, 50): + for b in range(1, 50): + A, B = F(a), F(b) + if 4*A^3 + 27*B^2 == 0: + continue + E = EllipticCurve(F, [A, B]) + N = E.order() + if not (N.is_prime() and N % 2 == 1): + continue + if (-A*B).is_square(): + continue + Z = next(F(z) for z in range(2, q) + if not F(z).is_square() and F(z) != F(-1)) + return (F, E, A, B, Z, N) + return None + +def sswu(F, E, A, B, Z, u): + """The deployed-shape mapping, and which branch produced the point.""" + if u == 0: + return (E(0), None) # the zero-repaired exceptional input + t = Z*u^2 + ta = t^2 + t + assert ta != 0 # t = -1 has no solutions for q ≡ 1 (mod 4) + x1 = B*(ta + 1) / (A*(-ta)) + for branch, x in ((1, x1), (2, t*x1)): + g = x^3 + A*x + B + assert g != 0 # a root would be rational 2-torsion + if g.is_square(): + y = g.sqrt() + if sgn0(y) != sgn0(u): + y = -y + return (E((x, y)), branch) + raise AssertionError("neither branch value is a square") + +for q in [101, 149, 197, 401, 601, 1009, 10009]: + assert q % 4 == 1 + inst = find_instance(q) + assert inst is not None, f"no instance found for q = {q}" + F, E, A, B, Z, N = inst + hist = {} + branches = {} + for u in F: + P, branch = sswu(F, E, A, B, Z, u) + if branch is None: + continue + hist[P] = hist.get(P, 0) + 1 + branches.setdefault(P, set()).add(branch) + assert set(hist.values()) <= {2, 4}, sorted(set(hist.values())) + reached = len(hist) + single = sum(1 for s in branches.values() if len(s) == 1) + four = sum(1 for c in hist.values() if c == 4) + two = reached - four + tol = 3/sqrt(q) + for count, target in [(reached, 3/8), (four, 1/8), (two, 1/4)]: + assert abs(count/N - target) <= tol, (q, count, N, target) + print(f"q={q} A={A} B={B} Z={Z} N={N}: reached {reached}/{N} " + f"(3/8·N ≈ {float(3*N/8):.0f}), 4-preimage {four} (N/8 ≈ {float(N/8):.0f}), " + f"2-preimage {two} (N/4 ≈ {float(N/4):.0f}), single-branch points {single}") + +print("small-curve branch statistics: OK") diff --git a/scripts/weil-derivation-checks.sage b/scripts/check_weil_derivations.sage similarity index 60% rename from scripts/weil-derivation-checks.sage rename to scripts/check_weil_derivations.sage index d5f7138..efd6721 100644 --- a/scripts/weil-derivation-checks.sage +++ b/scripts/check_weil_derivations.sage @@ -60,6 +60,20 @@ assert phi(0) == b^2 assert 64*phi(-1/QQ(4)) == 4*a^3 + 27*b^2 print("φ composition, discriminant, and critical values: OK") +# The certificates transcribed in Hashing/WeilSupport.lean: φ's Bézout +# cofactors, the re-expansion 64·Φ = Ψ(2·z·u² + 1), and the coprimality +# decomposition of Φ against z·u² + 1: +s3 = (6*a^3*b^2 + 36*b^4)*T + (4*a^6 + 36*a^3*b^2 + 63*b^4) +t3 = (-2*a^3*b^2 - 12*b^4)*T^2 + (-2*a^6 - 18*a^3*b^2 - 33*b^4)*T \ + + (-3*a^3*b^2 - 21*b^4) +assert s3*phi + t3*phi.derivative() == a^3*b^2*(4*a^3 + 27*b^2) +Psi = b^2*T^6 + (4*a^3 + 9*b^2)*T^4 + (27*b^2 - 8*a^3)*T^2 \ + + (4*a^3 + 27*b^2) +assert 64*Phi == Psi(2*z*u^2 + 1) +assert Psi(0) == 4*a^3 + 27*b^2 +assert Phi == ta*(b^2*ta^2 + (3*b^2 + a^3)*ta + 3*b^2) + b^2 +print("WeilSupport certificates: 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") @@ -84,3 +98,32 @@ 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") + +# Monodromy square-exclusion certificates (design doc §3, WeilSupport): +# g's separability, the coprimality of the V₄/C₄ linear factors with g, +# and the Kappe–Warren reductions to the square classes b·w and +# b·(w − 4·b) = b·(a·x − 3·b). +Rx = PolynomialRing(K, 'x') +X = Rx.gen() +gx = X^3 + a*X + b +gd = gx.derivative() +assert (27*b - 18*a*X)*gx + (6*a*X^2 - 9*b*X + 4*a^2)*gd \ + == 4*a^3 + 27*b^2 +assert (a^2*X^2 - a*b*X + (b^2 + a^3))*(a*X + b) - a^3*gx == b^3 +assert a^3*gx - (a^2*X^2 + 3*a*b*X + (9*b^2 + a^3))*(a*X - 3*b) \ + == b*(4*a^3 + 27*b^2) +assert gx(3*b/a) == b*(4*a^3 + 27*b^2)/a^3 +print("monodromy Bézout certificates: OK") + +# The Kappe–Warren square-class reductions. Writing each quartic monically +# as u⁴ + p·u² + q over F_q(E′): V₄ needs q a square, C₄ needs q·(p² − 4·q) +# a square. Both quartics reduce both tests to the same two square classes: +FW = PolynomialRing(K, 'w').fraction_field() +w = FW.gen() +p1q, q1q = 1/FW(z), b/(z^2*w) +p2q, q2q = w/(b*z), w/(b*z^2) +assert q1q * (b*w) == (b/z)^2 +assert q2q * (b*w) == (w/z)^2 +assert q1q*(p1q^2 - 4*q1q) * (b*(w - 4*b)) == (b*(w - 4*b)/(z^2*w))^2 +assert q2q*(p2q^2 - 4*q2q) * (b*(w - 4*b)) == (w*(w - 4*b)/(b*z^2))^2 +print("Kappe–Warren square-class reductions: OK") diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py new file mode 100755 index 0000000..cb629df --- /dev/null +++ b/scripts/check_weil_support_refs.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Check the design doc's references to the formalized facts: every +declaration of CompElliptic/Hashing/WeilSupport.lean must be referenced +(backticked) somewhere in design/weil-constant-derivation.md, and every +backticked identifier in the doc (dot-qualified ones included) must +resolve to a declaration — its exact fully qualified name anywhere in +CompElliptic, or a dot-path suffix of one under the relevant modules +(CompElliptic.{Hashing,Curves}). A citation that also matches a name +outside the relevant modules must qualify itself. Every declaration a +citation can refer to must be named directly in an `assert_axioms` or +`assert_computable` entry of CompElliptic/TrustBoundary.lean: the doc +is a pencil-and-paper proof whose reader relies on everything it cites, +so an unpinned citation would be a gap in axiom-checking. Declared Lean +names that could be mistaken for a filename or an allowlisted non-Lean +term are rejected outright, so the citation filters cannot silently +mask a real declaration. Run from the repository root; exits non-zero +on violation.""" +import pathlib +import re +import sys + +# Backticked identifiers that are not Lean declarations (RFC and spec +# names, Sage identifiers, and similar). +ALLOWED_NON_LEAN = { + 'map_to_curve_simple_swu', 'hash_to_field', +} + +DECL_RE = re.compile( + r'^(private +|protected +)?(?:noncomputable +|partial +|unsafe +)?' + r'(?:theorem|lemma|def|abbrev|instance|axiom|opaque|inductive' + r'|structure|class) ' + r"(_root_\.)?([A-Za-z_][A-Za-z0-9_']*(?:\.[A-Za-z_][A-Za-z0-9_']*)*)") +NS_RE = re.compile(r"^namespace +([A-Za-z_][A-Za-z0-9_.']*)") +END_RE = re.compile(r"^end +([A-Za-z_][A-Za-z0-9_.']*)") +FILENAME_RE = re.compile(r"\.(lean|sage|py|md|toml|yml|sh)$") + + +def declared_names(path: pathlib.Path) -> set: + """The fully qualified names declared in a Lean file. The enclosing + namespace is reconstructed from the `namespace`/`end` pairs above each + declaration — `end ` pops only a matching innermost `namespace`, so + a named `section ... end` cannot corrupt the stack — the same + reconstruction as ironwood's `scripts/check_endpoint_census.sh`. A + `_root_.` prefix ignores the enclosing namespace; a `private` + declaration is not citable, so it is not collected.""" + names = set() + stack = [] + for line in path.read_text().splitlines(): + m = NS_RE.match(line) + if m: + stack.append(m.group(1)) + continue + m = END_RE.match(line) + if m: + if stack and stack[-1] == m.group(1): + stack.pop() + continue + m = DECL_RE.match(line) + if m and not (m.group(1) or '').startswith('private'): + names.add(m.group(3) if m.group(2) or not stack + else '.'.join(stack) + '.' + m.group(3)) + return names + + +def is_path_suffix(name: str, full: str) -> bool: + """Whether `name` is a dot-path suffix of `full`, on segment + boundaries.""" + return full == name or full.endswith('.' + name) + + +root = pathlib.Path(__file__).resolve().parent.parent +support = declared_names(root / 'CompElliptic/Hashing/WeilSupport.lean') +everywhere = set() +for f in (root / 'CompElliptic').rglob('*.lean'): + everywhere |= declared_names(f) +relevant = {full for full in everywhere + if full.startswith('CompElliptic.Hashing.') + or full.startswith('CompElliptic.Curves.')} +confusable = {full for full in everywhere + if any(is_path_suffix(name, full) for name in ALLOWED_NON_LEAN) + or FILENAME_RE.search(full)} + +doc = (root / 'design/weil-constant-derivation.md').read_text() +listed = set(re.findall( + r'`([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)`', doc)) +# Backticked filenames (`BranchCovers.lean`, `weilbound.sage`) are file +# references, not declarations. +listed = {name for name in listed + if name not in ALLOWED_NON_LEAN + and not FILENAME_RE.search(name)} + +# A citation resolves when it either matches the fully qualified name +# exactly, or it is a dot-path suffix of the fully qualified name of +# some declaration under a "relevant" module (see above). Final-segment +# matching alone would let a bogus `junk.last` resolve against any +# declaration ending in `last`. Allowing matches in any module would +# incur a greater risk of typos accidentally matching unrelated names. +missing = {full for full in support + if not any(is_path_suffix(name, full) for name in listed)} +unknown = {name for name in listed + if name not in everywhere # exact match + and not any(is_path_suffix(name, full) for full in relevant)} + +# There should not be any non-fully-qualified references that match names +# outside the relevant modules. An unknown citation selects no referents: +# its remedy is fixing the citation, so it must not also demand +# qualification or pins here and below. +irrelevant = {full for full in everywhere + if full not in relevant + and any(name not in unknown + and name != full and is_path_suffix(name, full) + for name in listed)} + +# Census entries are written fully qualified, so a reference is pinned when +# *every* declaration of which it is a dot-path suffix is included in the +# census. So an ambiguous short reference (e.g. `mapToCurve`) requires all +# of its potential referents to be pinned. Cases already reported as +# "irrelevant" matches are excluded. +pins = set(re.findall( + r'^assert_(?:axioms|computable) +(?:_root_\.)?' + r'([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', + (root / 'CompElliptic/TrustBoundary.lean').read_text(), re.M)) +unpinned = {full for full in everywhere + if full not in pins and full not in irrelevant + and any(name not in unknown and is_path_suffix(name, full) + for name in listed)} + +if missing: + print("declared in WeilSupport.lean but not referenced in the doc:", + *sorted(missing), sep='\n ') +if unknown: + print("backticked in the doc but not found as a relevant or fully qualified" + " declaration (add to ALLOWED_NON_LEAN if intentional):", + *sorted(unknown), sep='\n ') +if irrelevant: + print("referenced in the doc but matches a name outside the relevant modules" + " (qualify to avoid ambiguity):", + *sorted(irrelevant), sep='\n ') +if unpinned: + print("referenced in the doc but not pinned in the axiom census" + " (CompElliptic/TrustBoundary.lean):", + *sorted(unpinned), sep='\n ') +if confusable: + print("declared Lean name that looks like a filename or a name in" + " the ALLOWED_NON_LEAN list:", + *sorted(confusable), sep='\n ') + +sys.exit(1 if (missing or unknown or irrelevant or unpinned or confusable) else 0) diff --git a/scripts/gen_jubjub.py b/scripts/gen_jubjub.py index be21966..912a9ba 100644 --- a/scripts/gen_jubjub.py +++ b/scripts/gen_jubjub.py @@ -56,6 +56,8 @@ if __name__ == "__main__": out = HEADER out += field_block("JUBJUB_SCALAR", L, "JubjubScalarField", - "Jubjub scalar field ℓ (the prime-order subgroup order).") + "The order `ℓ` of the Jubjub scalar field (the prime-order subgroup order).", + "The Jubjub scalar field `F_ℓ`.", + "`ℓ` is prime, by a Pratt certificate.") out += FOOTER print(out, end="") diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py index e5ccd02..d76a1ab 100644 --- a/scripts/gen_pasta.py +++ b/scripts/gen_pasta.py @@ -88,8 +88,12 @@ def vestaBase : TonelliShanks VestaBaseField where if __name__ == "__main__": out = HEADER out += field_block("PALLAS_BASE", P, "PallasBaseField", - "Pallas base field p (= Vesta scalar field).") + "The order `p` of the Pallas base field (= the Vesta scalar field).", + "The Pallas base field `F_p` (= the Vesta scalar field).", + "`p` is prime, by a Pratt certificate.") out += field_block("PALLAS_SCALAR", Q, "PallasScalarField", - "Pallas scalar field q (= Vesta base field).") + "The order `q` of the Pallas scalar field (= the Vesta base field).", + "The Pallas scalar field `F_q` (= the Vesta base field).", + "`q` is prime, by a Pratt certificate.") out += FOOTER print(out, end="") diff --git a/scripts/pratt.py b/scripts/pratt.py index a3cba3a..2026b2e 100644 --- a/scripts/pratt.py +++ b/scripts/pratt.py @@ -69,11 +69,14 @@ def theorem(name: str, card: int) -> str: return f"theorem {name}_is_prime : Nat.Prime {name}_CARD := by\n unfold {name}_CARD\n{body}" -def field_block(name: str, card: int, fieldabbrev: str, doc: str) -> str: +def field_block(name: str, card: int, fieldabbrev: str, carddoc: str, + fielddoc: str, primedoc: str) -> str: return ( - f"\n-- {doc}\n" + f"\n/-- {carddoc} -/\n" f"@[reducible] def {name}_CARD : Nat := 0x{card:x}\n\n" + f"/-- {fielddoc} -/\n" f"abbrev {fieldabbrev} := ZMod {name}_CARD\n\n" + f"/-- {primedoc} -/\n" f"{theorem(name, card)}\n\n" f"instance : Fact (Nat.Prime {name}_CARD) := ⟨{name}_is_prime⟩\n" f"instance : Field {fieldabbrev} := ZMod.instField {name}_CARD\n"