Reduce the deployed Weil bound to Weil's theorem at the branch covers

.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

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

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), ?_⟩

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), ?_⟩