feat: Define BN254 curve

ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean

@@ -80,7 +80,7 @@ theorem decoder_dist_impl_mem
   :
   p ∈ decoder k r D e ωs f := by sorry
 
-/-- The degree bound (a.k.a. `D_X`) for instantiation of Guruswami-Sudan 
+/-- The degree bound (a.k.a. `D_X`) for instantiation of Guruswami-Sudan
     in lemma 5.3 of the Proximity Gap paper.
     D_X(m) = (m + 1/2)√ρn.
 -/
@@ -91,28 +91,28 @@ noncomputable def proximity_gap_degree_bound (k m : ℕ) : ℕ :=
 /-- The ball radius from lemma 5.3 of the Proximity Gap paper,
     which follows from the Johnson bound.
     δ₀(ρ, m) = 1 - √ρ - √ρ/2m.
--/ 
+-/
 noncomputable def proximity_gap_johnson (k m : ℕ) : ℕ :=
   let rho := (k + 1 : ℚ) / n
   Nat.floor ((1 : ℝ) - Real.sqrt rho - Real.sqrt rho / (2 * m))
 
-/-- The first part of lemma 5.3 from the Proximity gap paper. 
+/-- The first part of lemma 5.3 from the Proximity gap paper.
     Given the D_X (`proximity_gap_degree_bound`) and δ₀ (`proximity_gap_johnson`),
     a solution to Guruswami-Sudan system exists.
 -/
-lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F}:
+lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} :
   ∃ Q, Condition k m (proximity_gap_degree_bound (n := n) k m) ωs f Q := by
   sorry
 
 /-- The second part of lemma 5.3 from the Proximity gap paper.
     For any solution Q of the Guruswami-Sudan system, and for any
-    polynomial P ∈ RS[n, k, ρ] such that Δ(w, P) ≤ δ₀(ρ, m), 
+    polynomial P ∈ RS[n, k, ρ] such that Δ(w, P) ≤ δ₀(ρ, m),
     we have that Y - P(X) divides Q(X, Y) in the polynomial ring
     F[X][Y].
 -/
 lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F}
   {f : Fin n → F}
-  {Q : F[X][X]} 
+  {Q : F[X][X]}
   {p : ReedSolomon.code ωs n}
   (h : Δ₀(f, (ReedSolomon.codewordToPoly p).eval ∘ f) ≤ proximity_gap_johnson (n := n) k m)
   :

ArkLib/Data/EllipticCurve/BN254.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
+import ArkLib.Data.FieldTheory.NonBinaryField.BN254
+import ArkLib.ToMathlib.NumberTheory.PrattCertificate
+import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
+
+/-!
+# BN254 Elliptic Curve
+
+WARNING: this is experimental. Use with caution!
+
+This file defines the BN254 elliptic curve, a pairing-friendly curve used in
+cryptographic applications.
+
+The BN254 curve is defined over a prime field with the equation Y² = X³ + 3.
+
+## Main definitions
+
+* `BN254.BASE_FIELD_CARD`: The characteristic of the base field
+* `BN254.BaseField`: The base field F_p where the curve is defined
+* `BN254.curve`: The BN254 elliptic curve as a Weierstrass curve
+* `BN254.generator`: A generator point on the curve
+
+## References
+
+The BN254 curve parameters follow the specification used in Ethereum's alt_bn128
+precompiles and various zero-knowledge proof systems.
+
+
+-/
+
+namespace BN254
+
+/-- The base field characteristic (prime p) for BN254 elliptic curve -/
+@[reducible]
+def BASE_FIELD_CARD : Nat :=
+  21888242871839275222246405745257275088696311157297823662689037894645226208583
+
+/-- The base field F_p over which the BN254 elliptic curve is defined -/
+abbrev BaseField := ZMod BASE_FIELD_CARD
+
+/-- Proof that the BN254 base field characteristic is prime -/
+theorem BaseField_is_prime : Nat.Prime BASE_FIELD_CARD := by
+  unfold BASE_FIELD_CARD
+  -- This is a well-known 254-bit prime used in the BN254 curve
+  -- For now we'll use sorry; in practice this would need a full primality proof
+  sorry
+
+instance : Fact (Nat.Prime BASE_FIELD_CARD) := ⟨BaseField_is_prime⟩
+
+instance : Field BaseField := ZMod.instField BASE_FIELD_CARD
+
+/-- The BN254 elliptic curve: Y² = X³ + 3 -/
+def curve : WeierstrassCurve BaseField := {
+  a₁ := 0,  -- coefficient of XY
+  a₂ := 0,  -- coefficient of X²
+  a₃ := 0,  -- coefficient of Y
+  a₄ := 0,  -- coefficient of X
+  a₆ := 3   -- constant term (so we have Y² = X³ + 3)
+}
+
+/-- The BN254 curve is in short normal form -/
+instance : curve.IsShortNF := by constructor <;> rfl
+
+/-- The BN254 curve is elliptic (has non-zero discriminant) -/
+instance : curve.IsElliptic := by
+  -- For short form Y² = X³ + aX + b, discriminant is -16(4a³ + 27b²)
+  -- Here a = 0, b = 3, so discriminant is -16(27 * 9) = -16 * 243 = -3888
+  -- Since the base field prime is much larger than 3888, this is non-zero
+  constructor
+  rw [WeierstrassCurve.Δ_of_isShortNF]
+  simp [curve]
+  grind
+
+/-- A generator point `(1, 2)` on the BN254 curve.
+
+NOTE: some places assume generator is `(-1, 2)` instead. -/
+def generator : BaseField × BaseField := (1, 2)
+
+/-- The generator point is on the curve -/
+theorem generator_on_curve : let (x, y) := generator
+  y^2 = x^3 + 3 := by
+  simp [generator]
+  norm_num
+
+end BN254

ArkLib/Data/FieldTheory/NonBinaryField/BLS12_377.lean

@@ -23,12 +23,14 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 
 namespace BLS12_377
 
-notation "SCALAR_FIELD_CARD" =>
+@[reducible]
+def SCALAR_FIELD_CARD : Nat :=
   8444461749428370424248824938781546531375899335154063827935233455917409239041
 
 abbrev ScalarField := ZMod SCALAR_FIELD_CARD
 
 theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD := by
+  unfold SCALAR_FIELD_CARD
   refine PrattCertificate'.out (p := SCALAR_FIELD_CARD) ⟨22, (by reduce_mod_char), ?_⟩
   refine .split [2 ^ 47, 3, 5, 7, 13, 499, 958612291309063373, 9586122913090633729 ^ 2]
     (fun r hr => ?_) (by norm_num)

ArkLib/Data/FieldTheory/NonBinaryField/BLS12_381.lean

@@ -23,12 +23,14 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 
 namespace BLS12_381
 
-notation "SCALAR_FIELD_CARD" =>
+@[reducible]
+def SCALAR_FIELD_CARD : Nat :=
   52435875175126190479447740508185965837690552500527637822603658699938581184513
 
 abbrev ScalarField := ZMod SCALAR_FIELD_CARD
 
 theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD := by
+  unfold SCALAR_FIELD_CARD
   refine PrattCertificate'.out (p := SCALAR_FIELD_CARD) ⟨7, (by reduce_mod_char), ?_⟩
   refine .split [2 ^ 32, 3, 11, 19, 10177, 125527, 859267, 906349 ^ 2, 2508409, 2529403, 52437899,
     254760293 ^ 2] (fun r hr => ?_) (by norm_num)

ArkLib/Data/FieldTheory/NonBinaryField/BN254.lean

@@ -13,12 +13,14 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 
 namespace BN254
 
-notation "SCALAR_FIELD_CARD" =>
+@[reducible]
+def SCALAR_FIELD_CARD : Nat :=
   21888242871839275222246405745257275088548364400416034343698204186575808495617
 
 abbrev ScalarField := ZMod SCALAR_FIELD_CARD
 
 theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD := by
+  unfold SCALAR_FIELD_CARD
   refine PrattCertificate'.out (p := SCALAR_FIELD_CARD) ⟨5, (by reduce_mod_char), ?_⟩
   refine .split [2 ^ 28, 3 ^ 2, 13, 29, 983, 11003, 237073, 405928799, 1670836401704629,
     13818364434197438864469338081] (fun r hr => ?_) (by norm_num)

ArkLib/Data/FieldTheory/NonBinaryField/BabyBear.lean

@@ -15,10 +15,13 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 namespace BabyBear
 
 -- 2^{31} - 2^{27} + 1
-notation "FIELD_SIZE" => 2013265921
+@[reducible]
+def FIELD_CARD : Nat := 2013265921
 
-abbrev Field := ZMod FIELD_SIZE
+abbrev Field := ZMod FIELD_CARD
 
-theorem is_prime : Nat.Prime FIELD_SIZE := by pratt
+theorem is_prime : Nat.Prime FIELD_CARD := by
+  unfold FIELD_CARD
+  pratt
 
 end BabyBear

ArkLib/Data/FieldTheory/NonBinaryField/Goldilocks.lean

@@ -15,10 +15,13 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 namespace Goldilocks
 
 -- 2^{64} - 2^{32} + 1
-notation "FIELD_SIZE" => 18446744069414584321
+@[reducible]
+def FIELD_CARD : Nat := 18446744069414584321
 
-abbrev Field := ZMod FIELD_SIZE
+abbrev Field := ZMod FIELD_CARD
 
-theorem is_prime : Nat.Prime FIELD_SIZE := by pratt
+theorem is_prime : Nat.Prime FIELD_CARD := by
+  unfold FIELD_CARD
+  pratt
 
 end Goldilocks

ArkLib/Data/FieldTheory/NonBinaryField/Mersenne.lean

@@ -15,10 +15,13 @@ import ArkLib.ToMathlib.NumberTheory.PrattCertificate
 namespace Mersenne31
 
 -- 2^{31} - 1
-notation "FIELD_SIZE" => 2147483647
+@[reducible]
+def FIELD_CARD : Nat := 2147483647
 
-abbrev Field := ZMod FIELD_SIZE
+abbrev Field := ZMod FIELD_CARD
 
-theorem is_prime : Nat.Prime FIELD_SIZE := by pratt
+theorem is_prime : Nat.Prime FIELD_CARD := by
+  unfold FIELD_CARD
+  pratt
 
 end Mersenne31

ArkLib/Data/FieldTheory/NonBinaryField/Secp256k1.lean

@@ -25,11 +25,12 @@ namespace Secp256k1
 
 -- Base field
 
-notation "BASE_FIELD_CARD" => 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f
+@[reducible]
+def BASE_FIELD_CARD : Nat := 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f
 
 /- Alternative representation -/
 example : BASE_FIELD_CARD = 2 ^ 256 - 2 ^ 32 - 2 ^ 9 - 2 ^ 8 - 2 ^ 7 - 2 ^ 6 - 2 ^ 4 - 1
-  := by norm_num
+  := by unfold BASE_FIELD_CARD; norm_num
 
 abbrev BaseField := ZMod BASE_FIELD_CARD
 
@@ -70,6 +71,7 @@ abbrev BaseField := ZMod BASE_FIELD_CARD
 -/
 
 theorem BaseField_is_prime : Nat.Prime BASE_FIELD_CARD := by
+  unfold BASE_FIELD_CARD
   refine PrattCertificate'.out (p := BASE_FIELD_CARD) ⟨3, (by reduce_mod_char), ?_⟩
   refine .split [2, 3, 7, 13441,
     205115282021455665897114700593932402728804164701536103180137503955397371]
@@ -108,11 +110,13 @@ instance : Field BaseField := ZMod.instField BASE_FIELD_CARD
 
 -- Scalar field
 
-notation "SCALAR_FIELD_CARD" => 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141
+@[reducible]
+def SCALAR_FIELD_CARD : Nat := 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141
 
 abbrev ScalarField := ZMod SCALAR_FIELD_CARD
 
 theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD := by
+  unfold SCALAR_FIELD_CARD
   refine PrattCertificate'.out (p := SCALAR_FIELD_CARD) ⟨7, (by reduce_mod_char), ?_⟩
   refine .split [2 ^ 6, 3, 149, 631, 107361793816595537, 174723607534414371449,
     341948486974166000522343609283189] (fun r hr => ?_) (by norm_num)

ArkLib/Data/Polynomial/Bivariate.lean

@@ -55,13 +55,13 @@ def natWeightedDegree (p : F[X][Y]) (u v : ℕ) : ℕ :=
 -/
 def support [DecidableEq F] (p : F[X][Y]) : Finset (ℕ × ℕ) :=
   let deg := natWeightedDegree p 1 1
-  Finset.image 
-    (fun x => (x.1.val, x.2.val)) 
+  Finset.image
+    (fun x => (x.1.val, x.2.val))
     ({x : Fin deg.succ × Fin deg.succ | coeff p x.1 x.2 ≠ 0})
 
 
 /-- Root multiplicity of (0,0).
-    It is the minimal sum `i + j` over all `(i, j)` such that 
+    It is the minimal sum `i + j` over all `(i, j)` such that
     the (i,j)-coefficient of `f` is not zero.
 -/
 def rootMultiplicity₀ [DecidableEq F] : Option ℕ :=
@@ -167,7 +167,7 @@ def evalX : Polynomial F :=
 Evaluating a bivariate polynomial in the first variable `X` on a set of points. This results in
 a set of univariate polynomials in `Y`.
 -/
-def evalSetX (P : Finset F) [Nonempty P]: Set (Polynomial F) :=
+def evalSetX (P : Finset F) [Nonempty P] : Set (Polynomial F) :=
   {h : Polynomial F | ∃ a ∈ P, evalX a f = h}
 
 /--
@@ -220,7 +220,7 @@ lemma quotient_nezero_iff_coeffs_nezero (q : F[X][Y]) (hg : g ≠ 0)
 The `X` degree of the bivarate quotient is bounded above by the difference of the `X`-degrees of
 the divisor and divident.
 -/
-lemma quotient_degX [IsDomain F](q : F[X][Y]) (h_quot_XY : g = q * f) (hf : f ≠ 0) (hg : g ≠ 0) :
+lemma quotient_degX [IsDomain F] (q : F[X][Y]) (h_quot_XY : g = q * f) (hf : f ≠ 0) (hg : g ≠ 0) :
   degreeX q ≤ degreeX g - degreeX f := by
   rw [h_quot_XY, degreeX_mul q f]
   · aesop

scripts/lintWhitespace.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+tmpfile=$(mktemp)
+issues_found=0
+
+find ArkLib -type f -name "*.lean" | while IFS= read -r file; do
+    # Check for trailing whitespace and print line number if found
+    while IFS=: read -r line_num line; do
+        echo "Trailing whitespace found in $file at line $line_num: $line"
+        echo 1 > "$tmpfile"
+    done < <(grep -n "[[:blank:]]$" "$file")
+
+    # Check if the last line ends with a new line
+    if [ "$(tail -c 1 "$file" | od -c | awk 'NR==1 {print $2}')" != "\n" ]; then
+        echo "Last line does not end with a new line in: $file"
+        echo 1 > "$tmpfile"
+    fi
+done
+
+if [ -f "$tmpfile" ]; then
+    issues_found=$(<"$tmpfile")
+fi
+rm -f "$tmpfile"
+
+exit $issues_found