feat(ProximityGen): prove genRSC

[pitmonticone]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Hello,

This PR, autoformalized by the @Aristotle-Harmonic team, focuses on the formal verification of the Reed–Solomon code generator (genRSC) and significantly expands the foundational infrastructure of the ArkLib library.

Key highlights include the formalization of the proximity gap theorem for Reed-Solomon codes and a major expansion of the library's coding theory and proof system components.

Features

• Proof Systems & Proximity: Formalizes the proximity property of the Reed–Solomon code generator in ProximityGen.lean, utilizing the Proximity Gap Theorem (BCIKS20).
• Commitment Schemes: Introduces a tensor-based Interactive Oracle Proof (IOP) framework (supporting Ligero, Brakedown, and Binius) and defines trivial commitment schemes for degree-bound enforcement.
• Coding Theory: Adds implementations for Reed-Muller codes and consolidates coding theory submodules under a new central entry point.
• Advanced Data Structures:
  • Implements AssocNat and CNat hierarchy for natural numbers with definitional associativity.
  • Provides Church encodings for natural numbers, booleans, and vectors.
  • Introduces a Heterogeneous List (HList) type and expanded utility functions for Vector (interleaving and grouping).
• Domain-Specific Language (DSL): Adds an experimental DSL for specifying vector and polynomial-based interactive oracle proofs.
• Numeric Typeclasses: Defines new typeclasses for standardized numeric operations, including HasPred, HasSucc, and ToNat.

Refactoring

• CI/CD Optimization: Streamlined the GitHub Actions workflows by migrating to the standard lean-action for improved cache management and project builds.
• Library Entry Points: Updated ArkLib.lean and added top-level modules for the Stir and Whir proof systems to better organize exports.
• Indexing Improvements: Introduced alternative list indexing functions that provide better definitional equality and Fin type support.

Fixes

• Polynomial Utilities: Added lemmas for even/odd polynomial decomposition to support FFT-style operations.
• Mathlib Compatibility: Added an extensionality lemma for Polynomial.sum and established equivalences between machine integers (UInt8-UInt64) and Fin types.
• List Operations: Improved theorems for analyzing partial sums and products within lists.

Documentation

• Updated the docs.yml workflow to utilize generic cache keys and GitHub Action caching for more reliable documentation builds.

---

Analysis of Changes

Metric	Count
📝 Files Changed	24
✅ Lines Added	2293
❌ Lines Removed	2

---

sorry Tracking

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

• instance [Zero T] [ToNat T] : DecidableEq (Cayley T) in ArkLib/Data/CNat/Defs.lean
• theorem add_comm (m n : ChurchNat α) : add m n = add n m in ArkLib/Data/CNat/Church.lean
• theorem pred_succ {T : Type u} [HasSucc T] [Zero T] [ToNat T] (x : Cayley T) : in ArkLib/Data/CNat/Defs.lean
• def findSumIdx' (l : List ℕ) (j : Fin l.sum) : Fin l.length in ArkLib/Data/List/BigOperators.lean
• theorem mul_add {a b c : AssocNat} : a * (b + c) = a * b + a * c in ArkLib/Data/CNat/AssocNat.lean
• def findSumIdxWith (l : List ℕ) (j : Fin l.sum) : (i : Fin l.length) × Fin (l.get i) in ArkLib/Data/List/BigOperators.lean
• theorem succ_mul {a b : AssocNat} : (succ a) * b = a * b + b in ArkLib/Data/CNat/AssocNat.lean
• def pred (n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem toFun_eq_const_plus (t : AssocNat) : ∀ m : Nat, t m = t 0 + m in ArkLib/Data/CNat/AssocNat.lean
• theorem mul_distrib_add {a b : CNat 1} : a * (b + 1) = a * b + a in ArkLib/Data/CNat/Defs.lean
• def interleave {n : Nat} (xs : Vector α n) (ys : Vector α n) : Vector α (2 * n) in ArkLib/Data/List/Vector.lean
• def sub (m n : ChurchNat α) : ChurchNat α in ArkLib/Data/CNat/Church.lean
• theorem zero_mul {a : AssocNat} : 0 * a = 0 in ArkLib/Data/CNat/AssocNat.lean
• theorem ofNat_toNat (n : ChurchNat ℕ) : ofNat (toNat n) = n in ArkLib/Data/CNat/Church.lean

---

🎨 **Style Guide Adherence**

Here are the specific lines that violate the ArkLib Style Guide:

General / File Naming

• File ArkLib/ProofSystem/DSL.lean: Violates "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Should be Dsl.lean).

ArkLib/Data/CNat/AssocNat.lean

• Lines 1–2: Violates "Use standard file headers including copyright, license (Apache 2.0), and authors."
• Lines 39, 60, 64, 80, 183, 273, 281: Violates "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Lines 44, 53, 56: Violates "Place by at the end of the line preceding the tactic block."
• Lines 44, 53, 136, 229, 248, 249: Violates "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."

ArkLib/Data/CNat/Church.lean

• Lines 59, 62, 67, 70, 79, 210, 213, 217, 221, 225, 240, 269: Violates "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Lines 210, 213, 216, 220, 224, 233, 237, 241: Violates "Every definition and major theorem should have a docstring."

ArkLib/Data/CNat/Defs.lean

• Line 29: Violates "u, v, w, ... : Universes; α, β, γ, ... : Generic types" (Uses T for a generic type).
• Lines 41, 60, 86, 127, 240, 248: Violates "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Lines 49, 53: Violates "Place by at the end of the line preceding the tactic block."
• Line 346: Violates "Put spaces on both sides of :, :=, and infix operators." (Missing space before :=).

ArkLib/Data/Polynomial/EvenAndOdd.lean

• Line 69: Violates "Place by at the end of the line preceding the tactic block."
• Lines 70, 71, 72, 206, 207, 208, 282, 283, 290, 291: Violates "Place [delimiters] before a line break rather than at the start of the next line." (Lines start with , or ←).

ArkLib/ProofSystem/Whir/ProximityGen.lean

• Lines 86–122: Violates "Each file that cites papers should have a ## References section in its docstring header" (Cites [BCIKS20] on line 97 without a References section).
• Line 101: Violates "Theorems and Proofs: snake_case" and "Acronyms: Treat as words" (Uses proximityGap_smoothRSC instead of proximity_gap_smooth_rsc).

ArkLib/ToMathlib/UInt/Equiv.lean

• Lines 9, 14, 19, 24, 29: Violates "Every definition and major theorem should have a docstring."
• Lines 9, 14, 19, 24: Violates "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Uses UInt).
• Lines 10, 11, 16, 17, 22, 23, 28, 29, 34, 35: Violates "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).

---

📄 **Per-File Summaries**

• .github/workflows/ci.yml: Simplify the CI workflow by migrating to the standard lean-action for automatic cache management and disabling the linter.
• .github/workflows/docs.yml: Updated the documentation workflow to use more generic cache keys and enable GitHub action caching for project builds.
• ArkLib.lean: Update the library's main entry point to export additional modules related to commitment schemes, coding theory, proof systems, and general data structures.
• ArkLib/CommitmentScheme/Tensor.lean: Defines the tensor-based interactive oracle proof (IOP) framework underlying polynomial commitment schemes such as Ligero, Brakedown, and Binius.
• ArkLib/CommitmentScheme/Trivial.lean: This file defines trivial commitment schemes where the prover sends data directly and the verifier performs validation checks, such as enforcing degree bounds on univariate polynomials.
• ArkLib/Data/CNat/AssocNat.lean: Defines AssocNat, a representation of natural numbers as successor-preserving endomorphisms that makes addition definitionally associative.
• ArkLib/Data/CNat/Church.lean: This file provides a foundational implementation of Church encodings for natural numbers, booleans, and vectors to demonstrate their definitional properties and theoretical connection to the project's natural number representations.
• ArkLib/Data/CNat/Defs.lean: Defines the Cayley transformation and the iterated CNat hierarchy to provide a representation of natural numbers where arithmetic operations, such as addition, are definitionally associative.
• ArkLib/Data/Classes/HasPred.lean: Introduces the HasPred and LawfulHasPred typeclasses for predecessor operations and provides instances for natural numbers.
• ArkLib/Data/Classes/HasSucc.lean: Defines the HasSucc and LawfulHasSucc typeclasses to provide a generic successor operation and ensure its consistency with addition, including instances for natural numbers.
• ArkLib/Data/Classes/ToNat.lean: Defines the ToNat and LawfulToNat type classes to provide a standardized interface for converting various types to natural numbers.
• ArkLib/Data/CodingTheory.lean: This change creates a new entry point file that aggregates all submodules within the coding theory library.
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean: Adds an extensionality lemma for the Polynomial.sum operator.
• ArkLib/Data/CodingTheory/ReedMuller.lean: Initializes the ReedMuller.lean file to define Reed-Muller codes as error-correcting codes based on evaluations of multivariate polynomials.
• ArkLib/Data/List/BigOperators.lean: Defines functions and theorems for computing and analyzing partial sums and products of lists, including utilities for locating indices based on cumulative totals.
• ArkLib/Data/List/Find.lean: Introduces alternative list indexing functions with improved definitional equality and provides versions that return Fin types.
• ArkLib/Data/List/HList.lean: Defines a heterogeneous list type (HList) as a list of sigma types, along with basic operations and conversions to dependent vectors.
• ArkLib/Data/List/Vector.lean: This PR creates a new file defining utility functions for Vector, including operations to interleave vectors and group vector elements into pairs.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: Defines the even and odd parts of a polynomial and provides lemmas for their decomposition and evaluation to support FFT-style splitting.
• ArkLib/ProofSystem/DSL.lean: Introduces an experimental domain-specific language (DSL) for specifying vector and polynomial-based interactive oracle proofs (IORs).
• ArkLib/ProofSystem/Stir.lean: This new file serves as a top-level module that aggregates all the subcomponents and theorems of the Stir proof system library.
• ArkLib/ProofSystem/Whir.lean: This file serves as a central entry point for the Whir proof system by aggregating its various constituent modules.
• ArkLib/ProofSystem/Whir/ProximityGen.lean: Formalizes the proximity property of the Reed–Solomon code generator by introducing the proximityGap_smoothRSC axiom based on the Proximity Gap Theorem from BCIKS20.
• ArkLib/ToMathlib/UInt/Equiv.lean: Defines equivalences between Fin types and their corresponding machine integer (UInt8 through UInt64) and BitVec representations.

---

Last updated: 2026-02-24 17:42 UTC.

[quangvdao]

I'm against merging this until this can be made fully rigorous and not axiomatized

[pitmonticone]

Yes, I should close this PR for now.