Importing field specifications

[dhsorens]

This pull request imports field specs from Arklib, starting with nonbinary fields. Instead of differentiating between Binary and non-Binary fields in the file structure, I've opted to default to "Fields" referring to the nonbinary fields. Binary fields are in their own subdirectory, as well as AdditiveNTT.

Corresponds to a sister pull request: Verified-zkEVM/ArkLib#309

[github-actions]

🤖 Gemini PR Summary

This pull request performs a major import of field specifications and algebraic constructions from Arklib, specifically focusing on finite field implementations required for zero-knowledge proof systems. The changes establish a foundational layer for both non-binary (prime) fields and binary fields, including formal verification of their properties and associated algorithms like the Additive NTT.

Features

• Finite Field Implementations:
  • Prime Fields: Added definitions and primality proofs for several standard curves and ZK-optimized fields, including BLS12-377, BLS12-381, BN254, BabyBear, Goldilocks, KoalaBear, Mersenne-31, and Secp256k1.
  • Binary Fields: Introduced $GF(2^{128})$ via BF128Ghash and a generic Binary Tower Field construction ($GF(2^{2^k})$) as iterated quadratic extensions.
• Primality Verification: Implemented Pratt primality certificates and an automated pratt tactic to formally verify large primes using the Lucas test.
• Additive NTT (FRI-Binius): Formalized the FRI-Binius variant of the Additive NTT algorithm, including abstract mathematical definitions, computable implementations, and proofs of correctness.
• Polynomial Basis & Algebraic Structures:
  • Defined a Novel Polynomial Basis using subspace vanishing polynomials.
  • Established identities for the Frobenius endomorphism and the factorization of $X^q - X$.
  • Introduced the Monomial Basis for polynomial submodules and rank proofs.
• Advanced Type Classes:
  • DCast / DCast₂ / DCast₃: New classes for dependent cast operations on indexed type families.
  • AlgebraTower: Formalized sequences of algebras and their equivalences.
  • CanonicalEuclideanDomain: Ensured unique quotients and remainders for integers and polynomials.

Refactoring

• Library Organization: Restructured the Fields directory to treat non-binary fields as the default, while isolating binary field logic into a specific Binary subdirectory.
• Mathlib Extensions: Added utility operations for Finsupp (e.g., snoc, insertNth) and generalized multivariate polynomial equivalences (finSuccEquivNth).
• System Maintenance: Updated scripts/style-exceptions.txt to accommodate larger file sizes and specific import patterns necessitated by the complex algebraic proofs.

Documentation

• Fields README: Created CompPoly/Fields/README.md to document the infrastructure for formally verified prime fields and primality certificates.
• Code Documentation: Added docstrings explaining the mathematical foundations of the GHASH polynomial, binary tower constructions, and the Additive NTT implementation.

---

Analysis of Changes

Metric	Count
📝 Files Changed	34
✅ Lines Added	19684
❌ Lines Removed	0

---

sorry Tracking

❌ **Added:** 12 `sorry`(s)

• lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerator_unit_mem_rootsOfUnity in CompPoly/Fields/KoalaBear.lean
• theorem join_eq_iff_dcast_extractLsb {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) in CompPoly/Fields/Binary/Tower/Impl.lean
• lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean
• lemma foldl_NTTStage_inductive_aux (h_ℓ : ℓ ≤ r) (k : Fin (ℓ + 1)) in CompPoly/Fields/AdditiveNTT/AdditiveNTT.lean
• lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt in CompPoly/Fields/KoalaBear.lean
• lemma coprime_three_fieldSize_sub_one : Nat.Coprime 3 (fieldSize - 1) in CompPoly/Fields/KoalaBear.lean
• lemma cube_map_bijective : in CompPoly/Fields/KoalaBear.lean
• lemma NTTStage_correctness (i : Fin (ℓ)) in CompPoly/Fields/AdditiveNTT/AdditiveNTT.lean
• def twoAdicGenerators : List Field in CompPoly/Fields/KoalaBear.lean
• lemma isPrimitiveRoot_twoAdicGenerator (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean

---

🎨 **Style Guide Adherence**

This review identifies violations of the CompPoly Style Guide found in the provided code changes.

CompPoly/Data/Classes/DCast.lean

• Line 31: theorem congrArg₃ violates "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 35: theorem congrArg₄ violates "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 126: cases ha; simp at hb; cases hb; simp at hc; cases hc; simp violates "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 175: cases ha; simp at hb; cases hb; simp at hc; cases hc; simp at hd; cases hd; simp violates "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."

CompPoly/Data/Polynomial/Frobenius.lean

• Line 57: Polynomial.X^(Fintype.card Fq) violates "Put spaces on both sides of :, :=, and infix operators."
• Line 136: (L := L) (Fq:=Fq) violates "Put spaces on both sides of :, :=, and infix operators." (missing space around :=).
• Line 153: (f + g)^(Fintype.card Fq) violates "Put spaces on both sides of :, :=, and infix operators."
• Line 167: (f + g)^(Fintype.card Fq) violates "Put spaces on both sides of :, :=, and infix operators."
• Line 245: x ^ (Fintype.card K) = x (Note: spacing around ^ is inconsistent with lines 57, 131, etc.)
• Line 353: eval₂ (algebraMap Fq K) α (X ^ (q ^ d) - X) = 0 (Line exceeds 100 characters in some contexts, but specifically check spacing rules).

CompPoly/Data/Polynomial/MonomialBasis.lean

• Line 41: monomials_in_submodule:Fin n violates "Put spaces on both sides of :, :=, and infix operators." (missing space after :).
• Line 79: ... range monomials_in_submodule) = ⊤ :=by violates "Place by at the end of the line preceding the tactic block." and "Put spaces on both sides of :, :=, and infix operators."

CompPoly/Data/RingTheory/AlgebraTower.lean

• Line 45: (i:=i) (j:=j) (h:=h) violates "Put spaces on both sides of :, :=, and infix operators."
• Line 60: fun (x : C i) (y : C j) (z : C k) => by violates "Functions: Prefer fun x ↦ ... over λ x, ..." (use of => instead of ↦).
• Line 73: (i:=i) (j:=j) (h:=h) (r:=r) violates "Put spaces on both sides of :, :=, and infix operators."

CompPoly/Fields/AdditiveNTT/AdditiveNTT.lean

• Line 144: (m:=splitPointIntoCoeffs 𝔽q β h_ℓ_add_R_rate i h_i x) violates "Put spaces on both sides of :, :=, and infix operators."
• Line 1056: (sDomain_basis 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (h_i := by simp only; apply Nat.lt_add_of_pos_right_of_le; omega)).repr x) j = x_coeffs j := by violates "Line Length: Keep lines under 100 characters." (154 characters).
• Line 1083: Empty line between let x_coeffs_fs ... and let rhs_sum ... violates "Avoid empty lines inside definitions or proofs."

CompPoly/Fields/AdditiveNTT/NovelPolynomialBasis.lean

• Line 51: (2:ℕ)^i.val violates "Put spaces on both sides of :, :=, and infix operators." (missing spaces around : and ^).
• Line 1334: (ℓ:=ℓ) (h_ℓ:=h_ℓ) (a:=a) violates "Put spaces on both sides of :, :=, and infix operators." (missing spaces around :=).

---

📄 **Per-File Summaries**

• CompPoly.lean: Expanded the project's scope by importing numerous new modules related to finite field implementations, additive NTT algorithms, and specialized polynomial properties.
• CompPoly/Data/Classes/DCast.lean: Introduces a hierarchy of type classes (DCast, DCast₂, DCast₃) for performing and reasoning about dependent cast operations on indexed type families to facilitate rewriting and theorem stating.
• CompPoly/Data/MvPolynomial/Notation.lean: Defines custom notation and specialized syntax for multivariate polynomial evaluation, degree restrictions, and related algebraic constructions.
• CompPoly/Data/Polynomial/Frobenius.lean: This file establishes fundamental identities and divisibility properties for polynomials over finite fields involving the Frobenius endomorphism, including the factorization of $X^q - X$ and the characterization of irreducible polynomials dividing $X^{q^n} - X$.
• CompPoly/Data/Polynomial/MonomialBasis.lean: This file defines the monomial basis for the submodule of polynomials with degree less than $n$ and proves that the rank of this space is $n$.
• CompPoly/Data/RingTheory/AlgebraTower.lean: Defines the AlgebraTower class and AlgebraTowerEquiv structure to formalize sequences of algebras and their equivalences indexed by a preorder.
• CompPoly/Data/RingTheory/CanonicalEuclideanDomain.lean: Defines the CanonicalEuclideanDomain typeclass to ensure unique quotients and remainders, providing instances for integers, polynomials, and fields along with associated algebraic identities.
• CompPoly/Fields/AdditiveNTT/AdditiveNTT.lean: This file implements the FRI-Binius variant of the Additive NTT algorithm and provides a formal proof of its correctness, including definitions for intermediate evaluation domains, quotient maps, and novel polynomial bases.
• CompPoly/Fields/AdditiveNTT/Impl.lean: Provides a computable implementation of the Additive NTT algorithm and proves its equivalence to the abstract mathematical definitions.
• CompPoly/Fields/AdditiveNTT/NovelPolynomialBasis.lean: This file defines and formalizes the novel polynomial basis for finite fields using subspace vanishing polynomials and proves its properties, recursive structure, and change-of-basis transformations.
• CompPoly/Fields/BLS12_377.lean: Defines the BLS12-377 scalar prime field and establishes its primality using a Pratt certificate.
• CompPoly/Fields/BLS12_381.lean: Defines the BLS12-381 scalar field and proves its primality using a Pratt certificate.
• CompPoly/Fields/BN254.lean: Defines the BN254 scalar prime field and provides a formal proof of its primality using Pratt certificates.
• CompPoly/Fields/BabyBear.lean: This file defines the BabyBear field and provides a proof of its primality using the Pratt certificate tactic.
• CompPoly/Fields/Basic.lean: Defines the NonBinaryField type class and establishes coefficient identities for polynomial compositions with $-X$ and $X^2$.
• CompPoly/Fields/Binary/BF128Ghash/Basic.lean: Defines the $GF(2^{128})$ field using the GHASH polynomial and proves its fundamental properties, including the irreducibility of its defining polynomial via Rabin's test.
• CompPoly/Fields/Binary/BF128Ghash/Impl.lean: This file provides a computable implementation of the $GF(2^{128})$ field for GHASH using BitVec operations, including modular reduction and Itoh-Tsujii inversion, along with a formal proof of its isomorphism to the standard polynomial quotient ring.
• CompPoly/Fields/Binary/BF128Ghash/Prelude.lean: This file defines the GHASH polynomial for $GF(2^{128})$ and provides correctness theorems for modular squaring and division verification functions using BitVec operations.
• CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean: This file provides a formal certificate for the GCD condition $\gcd(X^{2^{64}} + X, \text{ghashPoly}) = 1$ in the BF128Ghash field by explicitly verifying each step of the Euclidean algorithm.
• CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean: This file provides a computational certificate proving the modular identity $X^{2^{128}} \equiv X \pmod{\text{ghashPoly}}$ in the BF128Ghash field through a sequence of 128 verified squaring steps.
• CompPoly/Fields/Binary/Common.lean: This file provides shared utility lemmas and definitions for binary field implementations, including arithmetic properties of polynomials over $\mathbb{F}_2$, carry-less bit vector operations, and the isomorphism between bit vectors and polynomials.
• CompPoly/Fields/Binary/Tower/Basic.lean: This file defines the binary tower field $GF(2^{2^k})$ as an iterated quadratic extension of $GF(2)$ and formalizes its tower algebra structure, canonical embeddings, and multilinear bases.
• CompPoly/Fields/Binary/Tower/Impl.lean: This file provides an executable implementation of binary tower fields using bit vectors of size $2^k$, including field arithmetic, Karatsuba-like multiplication, and proofs of their algebraic structure and equivalence to abstract tower constructions.
• CompPoly/Fields/Binary/Tower/Prelude.lean: This file establishes the foundational field-theoretic definitions and theorems, particularly regarding polynomial irreducibility, trace maps, and linear representations, required for constructing binary tower field extensions.
• CompPoly/Fields/Binary/Tower/TensorAlgebra.lean: Defines Basis.baseChangeRight to lift a $K$-basis of a field extension to a basis of the tensor product algebra over the base-changed field.
• CompPoly/Fields/Goldilocks.lean: Defines the Goldilocks prime field and proves its characteristic is prime using a Pratt certificate.
• CompPoly/Fields/KoalaBear.lean: Defines the KoalaBear finite field ($2^{31} - 2^{24} + 1$), including its primality proof and precomputed 2-adic roots of unity.
• CompPoly/Fields/Mersenne.lean: Defines the Mersenne-31 prime field ($2^{31} - 1$) and provides a proof of its primality using a Pratt certificate.
• CompPoly/Fields/PrattCertificate.lean: Implements Pratt primality certificates and an automated pratt tactic for proving primality using the Lucas test.
• CompPoly/Fields/README.md: Added a README file to document the library's formally verified prime fields and primality certificate infrastructure for zero-knowledge protocols.
• CompPoly/Fields/Secp256k1.lean: Defines the Secp256k1 base and scalar prime fields and provides their primality proofs using Pratt certificates.
• CompPoly/ToMathlib/Finsupp/Fin.lean: This file defines tuple-like operations for Finsupp maps on Fin n—such as init, snoc, and insertNth—and establishes their basic properties and summation identities.
• CompPoly/ToMathlib/MvPolynomial/Equiv.lean: Introduces finSuccEquivNth, a generalization of finSuccEquiv that treats an arbitrary variable index as the indeterminate of a univariate polynomial ring.
• scripts/style-exceptions.txt: Update the style exceptions to allow for increased file lengths and specific import violations in several CompPoly files.

---

Last updated: 2026-02-17 17:27 UTC.

[dhsorens]

@alexanderlhicks @Julek @quangvdao in porting in the field specifications from Arklib I've opted to have Fields in their own directory, and to keep all the common (nonbinary) fields in the Fields/ directory; when importing binary fields later, I will likely put them in Fields/Binary - what do you think of this file organization?