Refactoring CompPoly Out of Arklib

[dhsorens]

Assuming that we merge #303 (although this will likely work no matter the 4.26.0 bump):

In an effort to have Arklib depend on CompPoly, this pull request removes the following files that were ported over to CompPoly:

• ArkLib.Data.Array.Lemmas
• ArkLib.Data.Fin.BigOperators
• ArkLib.Data.List.Lemmas
• ArkLib.Data.MlPoly.Basic
• ArkLib.Data.MlPoly.Equiv
• ArkLib.Data.Nat.Bitwise
• ArkLib.Data.UniPoly.Basic
• ArkLib.Data.Vector.Basic

This pull request corresponds to the pull request on CompPoly that ports over changes to the CompPoly files done in Arklib since they were first ported. We currently pin the version of CompPoly for Arklib to the latest commit en lieu of pinning it to 4.26.0 bc these changes are currently needed to get the dependencies working. For future version bumps, we can coordinate releases of CompPoly with those of Arklib.

[dhsorens]

@alexanderlhicks @quangvdao @chung-thai-nguyen - have I missed anything in Arklib that has already been ported but isn't removed in this PR? We're not currently counting field specs, waiting for the version bump to be merged to do those.

[github-actions]

🤖 Gemini PR Summary

This PR represents a major architectural shift to decouple core mathematical foundations from ArkLib by migrating them into the standalone CompPoly library. The primary goal is to eliminate code duplication and establish CompPoly as a formal dependency for polynomials, field theory, and low-level data lemmas.

Refactoring

This is the primary focus of the PR, involving the wholesale removal of core modules and the redirection of internal dependencies.

• Module Migration & Deletion: Removed extensive modules that have been ported to CompPoly, including:
  • Data Structures: Array.Lemmas, List.Lemmas, Vector.Basic, and Fin.BigOperators.
  • Polynomials: Core implementations for Multilinear (MlPoly), Univariate (UniPoly), and Multivariate notations.
  • Field Theory: Definitions and primality proofs for numerous curves (BN254, BLS12-381, BLS12-377, Secp256k1) and specialized fields (BabyBear, Goldilocks, KoalaBear, Mersenne31).
  • Binary Fields: Removed the GHASH 128-bit binary field implementation and the Binary Tower Field constructions.
  • Algorithms: Moved the Additive Number Theoretic Transform (NTT) implementation and its correctness proofs.
• Import Redirection: Updated import paths across the entire repository (e.g., Coding Theory, Elliptic Curves, Proof Systems) to reference @CompPoly instead of local ArkLib modules.
• Entry Point Cleanup: Streamlined ArkLib.lean by removing deprecated imports for field theory and data structures.
• Logic Extraction: Relocated specialized logic like DCast (dependent casts), CanonicalEuclideanDomain, and PrattCertificate (primality proving) to the external dependency.

Features

• Dependency Management: Updated lakefile.toml and lake-manifest.json to include CompPoly and ExtTreeMapLemmas as formal dependencies.
• Version Pinning: Temporarily pinned CompPoly to a specific commit to ensure compatibility with recent ports before a stable 4.26.0 release.

Documentation

• File Removal: Deleted the README.md within the NonBinaryField directory as the documentation and formalization references have moved to the upstream library.

Fixes

• Upstream Synchronization: Included updates to ensure that changes made to these files while they were in ArkLib are preserved in the transition to CompPoly.

---

Analysis of Changes

Metric	Count
📝 Files Changed	62
✅ Lines Added	23
❌ Lines Removed	23795

---

sorry Tracking

✅ **Removed:** 15 `sorry`(s)

• lemma coprime_three_fieldSize_sub_one : Nat.Coprime 3 (fieldSize - 1) in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• def nodal {R : Type*} [Ring R] (n : ℕ) (ω : R) : UniPoly R in ArkLib/Data/UniPoly/Basic.lean
• lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma isPrimitiveRoot_twoAdicGenerator (bits : Fin (twoAdicity + 1)) : in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma twoAdicGenerator_unit_mem_rootsOfUnity in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma foldl_NTTStage_inductive_aux (h_ℓ : ℓ ≤ r) (k : Fin (ℓ + 1)) in ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean
• lemma cube_map_bijective : in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• def twoAdicGenerators : List Field in ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean
• lemma forwardRange_0_eq_finRange (n : ℕ) [NeZero n] : forwardRange n ⟨n - 1, by in ArkLib/Data/MlPoly/Basic.lean
• def interpolate {R : Type*} [Ring R] (n : ℕ) (ω : R) (r : Vector R n) : UniPoly R in ArkLib/Data/UniPoly/Basic.lean
• lemma NTTStage_correctness (i : Fin (ℓ)) in ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean
• theorem join_eq_iff_dcast_extractLsb {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean

---

🎨 **Style Guide Adherence**

All changes adhere to the style guide.

---

📄 **Per-File Summaries**

• ArkLib.lean: Streamline the ArkLib.lean entry point by removing numerous module imports across various subdirectories, including field theory, data structures, and polynomials.
• ArkLib/Data/Array/Lemmas.lean: Delete the ArkLib/Data/Array/Lemmas.lean file, which contained auxiliary lemmas and utility functions for the Array type.
• ArkLib/Data/Classes/DCast.lean: Delete the DCast.lean file and its associated type classes for handling dependent cast operations on indexed type families.
• ArkLib/Data/CodingTheory/Basic.lean: Updates the import path for bitwise operations from ArkLib.Data.Nat.Bitwise to CompPoly.Data.Nat.Bitwise.
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean: Updated the import path for bitwise natural number operations from ArkLib to the CompPoly library.
• ArkLib/Data/CodingTheory/ReedSolomon.lean: Update the MonomialBasis import path from ArkLib to CompPoly.
• ArkLib/Data/EllipticCurve/BN254.lean: This change updates the BN254 elliptic curve implementation to use field definitions from the CompPoly library instead of local modules.
• ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean: Deletes the AdditiveNTT.lean file, which contained the formalization and correctness proofs of the FRI-Binius variant of the Additive NTT algorithm.
• ArkLib/Data/FieldTheory/AdditiveNTT/Impl.lean: Delete the computable implementation and correctness theorems for the Additive Number Theoretic Transform (NTT).
• ArkLib/Data/FieldTheory/AdditiveNTT/NovelPolynomialBasis.lean: Deleted the file defining the novel polynomial basis and its associated mathematical properties for additive NTTs.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/Basic.lean: Delete the file containing the definitions and irreducibility proofs for the 128-bit GHASH binary field $\text{GF}(2^{128})$.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/Impl.lean: The file ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/Impl.lean, which provided the computable implementation and field verification of $GF(2^{128})$ operations for GHASH, has been deleted.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/Prelude.lean: Remove the GHASH field prelude file, which provided polynomial definitions and correctness theorems for verifying modular squaring and division in $GF(2^{128})$.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/XPowTwoPowGcdCertificate.lean: This change deletes the certificate file providing the formal proof that the greatest common divisor of $X^{2^{64}} + X$ and the GHASH polynomial is 1.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/XPowTwoPowModCertificate.lean: This change deletes the manual certificate file used to verify powers of $X$ modulo the GHASH polynomial through a chain of 128 computational steps.
• ArkLib/Data/FieldTheory/BinaryField/Common.lean: This change deletes the common utility file for binary fields, which provided shared lemmas for polynomials over GF(2), bit vector operations (like carry-less multiplication), and the isomorphism between bit vectors and polynomials.
• ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean: Deleted the file defining the construction, algebraic structure, and multilinear bases of binary tower fields as iterated quadratic extensions of $GF(2)$.
• ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean: Deleted the executable implementation of binary tower fields represented by bit vectors of size $2^k$.
• ArkLib/Data/FieldTheory/BinaryField/Tower/Prelude.lean: This file provided preliminary definitions and theorems on characteristic 2 fields, trace map properties, and quadratic polynomial irreducibility required for the construction of binary tower fields.
• ArkLib/Data/FieldTheory/BinaryField/Tower/TensorAlgebra.lean: Deletes the TensorAlgebra.lean file, which contained formalizations for tensor product algebras and the baseChangeRight basis construction.
• ArkLib/Data/FieldTheory/NonBinaryField/BLS12_377.lean: Removes the definition and primality proof of the BLS12-377 scalar prime field.
• ArkLib/Data/FieldTheory/NonBinaryField/BLS12_381.lean: Delete the definition and primality proof for the BLS12-381 scalar field.
• ArkLib/Data/FieldTheory/NonBinaryField/BN254.lean: Remove the definition and primality proof of the BN254 scalar prime field.
• ArkLib/Data/FieldTheory/NonBinaryField/BabyBear.lean: This change deletes the BabyBear.lean file, removing the definition and primality proof for the BabyBear field.
• ArkLib/Data/FieldTheory/NonBinaryField/Basic.lean: Delete the NonBinaryField type class definition and its associated polynomial lemmas.
• ArkLib/Data/FieldTheory/NonBinaryField/Goldilocks.lean: Delete the definition and primality proof of the Goldilocks prime field ($2^{64} - 2^{32} + 1$).
• ArkLib/Data/FieldTheory/NonBinaryField/KoalaBear.lean: Deletes the definition and properties of the KoalaBear prime field ($2^{31} - 2^{24} + 1$).
• ArkLib/Data/FieldTheory/NonBinaryField/Mersenne.lean: Deleted the file defining the Mersenne31 prime field and its associated primality proof.
• ArkLib/Data/FieldTheory/NonBinaryField/README.md: Remove the README file documenting scalar prime fields for common elliptic curves and their formalization references.
• ArkLib/Data/FieldTheory/NonBinaryField/Secp256k1.lean: Deletes the definitions and primality proofs for the Secp256k1 base and scalar fields.
• ArkLib/Data/Fin/Basic.lean: Updates the DCast import path to reflect its relocation from ArkLib to CompPoly.
• ArkLib/Data/Fin/BigOperators.lean: This change deletes the ArkLib/Data/Fin/BigOperators.lean file, removing its collection of auxiliary lemmas and recursion principles for Fin types and finite summations.
• ArkLib/Data/Fin/Fold.lean: Update the import path for DCast to reflect its relocation from ArkLib to CompPoly.
• ArkLib/Data/Hash/Poseidon2.lean: Updated import paths for KoalaBear field and vector definitions to reflect their relocation to the CompPoly library.
• ArkLib/Data/List/Lemmas.lean: Removes the ArkLib/Data/List/Lemmas.lean file, which contained auxiliary lemmas and utility functions for list operations such as padding, folding, and size matching.
• ArkLib/Data/MlPoly/Basic.lean: Removed the file containing the core definitions, algebraic operations, and basis transformation logic for multilinear polynomials.
• ArkLib/Data/MlPoly/Equiv.lean: Removes the definitions and proofs establishing the equivalence and linear isomorphism between the MlPoly representation and Mathlib's multilinear polynomials.
• ArkLib/Data/MvPolynomial/Degrees.lean: Update the import path for multivariate polynomial notation from ArkLib to CompPoly.
• ArkLib/Data/MvPolynomial/Multilinear.lean: Updated the import path for multivariate polynomial notation from ArkLib to CompPoly.
• ArkLib/Data/MvPolynomial/Notation.lean: Remove the ArkLib/Data/MvPolynomial/Notation.lean file, which provided custom notation and syntax for multivariate polynomial evaluation and finite sets.
• ArkLib/Data/Nat/Bitwise.lean: This change deletes the file ArkLib/Data/Nat/Bitwise.lean, which contained custom utility definitions and lemmas for bitwise operations on natural numbers.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: Update the field theory dependency by replacing the ArkLib.Data.FieldTheory.NonBinaryField.Basic import with CompPoly.Fields.Basic.
• ArkLib/Data/Polynomial/Frobenius.lean: This change deletes the file ArkLib/Data/Polynomial/Frobenius.lean, which established fundamental Frobenius endomorphism identities and divisibility conditions for irreducible polynomials over finite fields.
• ArkLib/Data/Polynomial/MonomialBasis.lean: Remove the definitions and proofs for the monomial basis and finite dimensionality of polynomials with degree less than $n$.
• ArkLib/Data/Probability/Instances.lean: Update the import paths for Fin.BigOperators and Nat.Bitwise from ArkLib to CompPoly.
• ArkLib/Data/RingTheory/AlgebraTower.lean: Removes the definitions and properties of towers of algebras and algebra tower equivalences.
• ArkLib/Data/RingTheory/CanonicalEuclideanDomain.lean: Remove the CanonicalEuclideanDomain class and its associated theory, which provided a framework for unique quotients and remainders in Euclidean domains.
• ArkLib/Data/UniPoly/Basic.lean: Removes the UniPoly implementation and associated theory for computable univariate polynomials.
• ArkLib/Data/Vector/Basic.lean: Deletes the Vector and Matrix utility definitions and associated lemmas.
• ArkLib/OracleReduction/OracleInterface.lean: Updated the MvPolynomial notation import to point to the CompPoly library instead of ArkLib.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean: Update module imports to relocate AdditiveNTT and Vector dependencies from ArkLib to the CompPoly library.
• ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean: Updates the import for TensorAlgebra to reflect its relocation from ArkLib to the CompPoly library.
• ArkLib/ProofSystem/Binius/RingSwitching/Prelude.lean: Updated import paths for binary field and additive NTT modules to reflect their relocation to the CompPoly library.
• ArkLib/ProofSystem/ConstraintSystem/Plonk.lean: Updated the MvPolynomial notation import to point to the CompPoly library instead of ArkLib.
• ArkLib/ProofSystem/Fri/Domain.lean: Update the import source for field theory definitions by replacing ArkLib.Data.FieldTheory with CompPoly.Fields.
• ArkLib/ProofSystem/Stir/Quotienting.lean: Updated the import path for multivariate polynomial notation to reflect its relocation from ArkLib to the CompPoly library.
• ArkLib/ProofSystem/Sumcheck/Impl/Basic.lean: Updated the multilinear polynomial equivalence dependency to point to the new CompPoly library.
• ArkLib/ToMathlib/Finsupp/Fin.lean: Deleted the ArkLib/ToMathlib/Finsupp/Fin.lean file, which provided tuple-like operations and related lemmas for finitely supported functions indexed by Fin n.
• ArkLib/ToMathlib/MvPolynomial/Equiv.lean: Remove the finSuccEquivNth isomorphism and its associated lemmas for converting multivariate polynomials into univariate polynomials over an arbitrary pivot variable.
• ArkLib/ToMathlib/NumberTheory/PrattCertificate.lean: Remove the implementation of Pratt primality certificates and the associated pratt tactic for automated primality proving.
• lake-manifest.json: Updates project dependencies by adding the CompPoly and ExtTreeMapLemmas packages and updating the VCVio and Cli metadata.
• lakefile.toml: Added the CompPoly library as a new dependency to the project.

---

Last updated: 2026-02-18 17:28 UTC.

[alexanderlhicks]

probably best for legibility to put a tag rather than hash here

[dhsorens]

good call, I added the tag v4.26.0-patch1 to CompPoly and have updated this now to rev "v4.26.0-patch1"

[dhsorens]

NB Field specs were also ported into this PR and have been merged. Ready to merge