Importing field specifications

[dhsorens]

This pull request imports field specs from Arklib, starting with nonbinary fields.

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

[github-actions]

🤖 Gemini PR Summary

This pull request integrates field specifications from Arklib into the library, focusing on non-binary prime fields. It introduces both the infrastructure for formal primality proofs and the definitions for several widely used elliptic curve scalar fields.

Features

• New Finite Field Implementations: Added definitions and formal primality proofs for several industry-standard prime fields:
  • Elliptic Curve Fields: BLS12-377, BLS12-381, BN254, and Secp256k1 (base and scalar).
  • STARK-friendly Fields: BabyBear, Goldilocks, and KoalaBear (including precomputed 2-adic roots of unity).
  • Mersenne Fields: Mersenne-31 ($2^{31} - 1$).
• Pratt Primality Certificates: Implemented a pratt tactic and supporting infrastructure to automate formal proofs of primality using the Lucas test.
• Non-Binary Field Abstraction: Introduced the NonBinaryField type class to provide a unified interface for non-binary field operations.

Refactoring

• Library Reorganization: Centralized finite field imports in the main CompPoly.lean entry point.
• Identity Logic: Established coefficient identities for polynomial compositions (specifically for $-X$ and $X^2$) within CompPoly/Fields/Basic.lean to support broader polynomial arithmetic.

Documentation

• Fields Documentation: Added a new README.md in the CompPoly/Fields/ directory explaining the included scalar prime fields and the methodology for their formal primality proofs.

---

Analysis of Changes

Metric	Count
📝 Files Changed	12
✅ Lines Added	1219
❌ Lines Removed	0

---

sorry Tracking

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

• lemma cube_map_bijective : in CompPoly/Fields/KoalaBear.lean
• def twoAdicGenerators : List Field in CompPoly/Fields/KoalaBear.lean
• lemma isPrimitiveRoot_twoAdicGenerator (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean
• lemma coprime_three_fieldSize_sub_one : Nat.Coprime 3 (fieldSize - 1) in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) : in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerator_unit_mem_rootsOfUnity in CompPoly/Fields/KoalaBear.lean
• lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt in CompPoly/Fields/KoalaBear.lean
• lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2) in CompPoly/Fields/KoalaBear.lean

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the lines that violate the guidelines:

• File Names: CompPoly/Fields/BLS12_377.lean, CompPoly/Fields/BLS12_381.lean, CompPoly/Fields/BN254.lean, CompPoly/Fields/Secp256k1.lean

  • Violation: "Files: UpperCamelCase.lean (e.g., BinarySearch.lean)" and "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."

• CompPoly/Fields/Basic.lean:18: class NonBinaryField (F : Type*) extends Field F where

  • Violation: "Generic types: α, β, γ, ..." (using F for a type).

• CompPoly/Fields/Basic.lean:39: variable {F : Type*} [Field F]

  • Violation: "Generic types: α, β, γ, ..." (using F for a type).

• CompPoly/Fields/Basic.lean:53: (Empty line inside coeffs_of_comp_minus_x proof block)

  • Violation: "Empty Lines: Avoid empty lines inside definitions or proofs."

• CompPoly/Fields/Basic.lean:70: (Empty line inside comp_x_square_coeff proof block)

  • Violation: "Empty Lines: Avoid empty lines inside definitions or proofs."

• CompPoly/Fields/KoalaBear.lean:141: lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1) := by

  • Violation: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)" (using lowerCamelCase for twoAdicity).

• CompPoly/Fields/KoalaBear.lean:173: (Empty line inside twoAdicGenerators_order proof block)

  • Violation: "Empty Lines: Avoid empty lines inside definitions or proofs."

• CompPoly/Fields/PrattCertificate.lean:211: def powMod (a b m : ℕ) : ℕ := Id.run do

  • Violation: "Natural numbers: m, n, k, ..." (using a, b for natural numbers).

• CompPoly/Fields/PrattCertificate.lean:417: theorem ZMod.powEqOfPowMod :

  • Violation: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."

• CompPoly/Fields/PrattCertificate.lean:450: theorem ZMod.powNeOfPowMod :

  • Violation: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."

• CompPoly/Fields/PrattCertificate.lean:517: theorem Nat.Prime_of_isNat : ∀ {n n' : ℕ}, IsNat n n' → n'.Prime → n.Prime

  • Violation: "Theorems and Proofs: snake_case" (using isNat and capitalization).

• CompPoly/Fields/Secp256k1.lean:28: def BASE_FIELD_CARD : Nat := 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f

  • Violation: "Functions and Terms: lowerCamelCase."

• CompPoly/Fields/Secp256k1.lean:77: theorem BaseField_is_prime : Nat.Prime BASE_FIELD_CARD := by

  • Violation: "Theorems and Proofs: snake_case" (Capitalization of BaseField).

• CompPoly/Fields/Secp256k1.lean:92: def SCALAR_FIELD_CARD : Nat := 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141

  • Violation: "Functions and Terms: lowerCamelCase."

• CompPoly/Fields/Secp256k1.lean:139: theorem ScalarField_is_prime : Nat.Prime SCALAR_FIELD_CARD := by

  • Violation: "Theorems and Proofs: snake_case" (Capitalization of ScalarField).

• CompPoly/Fields/BLS12_377.lean:33: theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by

  • Violation: "Theorems and Proofs: snake_case" (Capitalization of ScalarField).

• CompPoly/Fields/BN254.lean:21: theorem ScalarField_is_prime : Nat.Prime scalarFieldSize := by

  • Violation: "Theorems and Proofs: snake_case" (Capitalization of ScalarField).

---

📄 **Per-File Summaries**

• CompPoly.lean: Added imports for various finite field implementations and Pratt certificates to the library.
• 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/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 documenting the scalar prime fields for common elliptic curves and their associated formal primality proofs.
• CompPoly/Fields/Secp256k1.lean: Defines the Secp256k1 base and scalar prime fields and provides their primality proofs using Pratt certificates.

---

Last updated: 2026-02-13 13:51 UTC.