feat(MainThm): prove stir_rbr_soundness

[pitmonticone]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

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

[github-actions]

🤖 Gemini PR Summary

This pull request completes a major milestone in the ArkLib library by providing the formal proof for stir_rbr_soundness. Beyond the core theorem, the PR introduces a significant amount of foundational infrastructure, including new data structures, commitment schemes, and proof system utilities.

Features

• STIR Proof System: Completes the proof for stir_rbr_soundness in MainThm.lean, replacing previous placeholders with a formal verification of the Round-By-Round soundness for the STIR protocol.
• Commitment Schemes:
  • Introduces Tensor-based polynomial commitment schemes and their associated square-root Interactive Oracle Proofs (IOPs).
  • Adds a Trivial commitment scheme for bounded-degree univariate polynomials where data is sent directly to the verifier.
• Coding Theory:
  • Initializes the ReedMuller module for multivariate polynomial evaluations.
  • Adds foundational extensionality theorems for polynomial sums.
• Foundational Data Structures & Arithmetic:
  • CNat (Church Numerals): Implements a hierarchy of functional natural number encodings (Church, AssocNat, Cayley Tower) to leverage definitional associativity for addition and multiplication.
  • Heterogeneous Lists: Adds HList (lists of sigma types) with support for dependent vector conversions.
  • Polynomial Utilities: Implements decomposition of polynomials into even and odd parts, including evaluation and transformation lemmas.
• Proof System DSL: Introduces an experimental Domain-Specific Language (DSL) for defining vector and polynomial-based IOPs using scalar and vector operations.
• WHIR Proof System: Establishes the top-level module for the WHIR proof system, aggregating folding and proximity generation components.
• Type Equivalences: Defines equivalences between Fin (2^n) and fixed-width unsigned integers (UInt8 through UInt64) and BitVec.

Refactoring

• Typeclass Standardization: Introduced HasSucc, HasPred, and ToNat typeclasses to provide a uniform interface for successor/predecessor operations and natural number conversions.
• List Utility Enhancements:
  • Optimized List indexing functions (findIdx, idxOf) for better definitional equality.
  • Added interleave and chunkPairwise utilities for vectors.
  • Implemented partial sums and cumulative sum-based element location in BigOperators.lean.
• Public API Expansion: Updated the root ArkLib.lean to export the newly created modules across commitment schemes, coding theory, and data structures.

Fixes

• CI/CD Infrastructure:
  • Updated ci.yml and docs.yml to utilize standard Lean action caching, improving build performance.
  • Note: Linting has been temporarily disabled in the CI workflow to bypass existing errors and facilitate the merging of these proofs.

Documentation

• Updated the documentation workflow's caching configuration to generalize cache keys and enable GitHub caching for project builds.

---

Analysis of Changes

Metric	Count
📝 Files Changed	24
✅ Lines Added	2264
❌ Lines Removed	4

---

sorry Tracking

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

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

---

🎨 **Style Guide Adherence**

The following code changes violate the ArkLib style guide on several points regarding file headers, module documentation, declaration docstrings, and tactic formatting.

Header and Module Documentation Violations

• ArkLib/Data/CNat/AssocNat.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/Data/CodingTheory.lean:1: "Use standard file headers including copyright, license (Apache 2.0), and authors."
• ArkLib/Data/CodingTheory.lean:1: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."

Missing Declaration Docstrings

Rule: "Every definition and major theorem should have a docstring."

• ArkLib/Data/CNat/AssocNat.lean:70: def subNat (c : AssocNat) : Nat → AssocNat
• ArkLib/Data/CNat/AssocNat.lean:80: def sub (a b : AssocNat) : AssocNat :=
• ArkLib/Data/CNat/AssocNat.lean:86: def mulNat (a : AssocNat) : Nat → AssocNat
• ArkLib/Data/CNat/AssocNat.lean:91: def mul (a b : AssocNat) : AssocNat :=
• ArkLib/Data/CNat/AssocNat.lean:257: def toAssocNat (f : AssocFin n) : AssocNat := f.val
• ArkLib/Data/CNat/AssocNat.lean:260: def toFin (f : AssocFin n) : Fin (AssocNat.toNat n) :=
• ArkLib/Data/CNat/AssocNat.lean:264: def ofFin {n : AssocNat} (f : Fin (AssocNat.toNat n)) : AssocFin n :=
• ArkLib/Data/CNat/Church.lean:53: def ChurchNat (α : Type) : Type := (α → α) → α → α
• ArkLib/Data/CNat/Church.lean:229: def isZero {α : Type} (n : ChurchNat α) : ChurchBool α :=
• ArkLib/Data/CNat/Church.lean:233: def leq {α : Type} (m n : ChurchNat α) : ChurchBool α :=
• ArkLib/Data/CNat/Church.lean:237: def lt {α : Type} (m n : ChurchNat α) : ChurchBool α :=
• ArkLib/Data/CNat/Church.lean:242: def ValidChurchNat : Type :=
• ArkLib/Data/CNat/Church.lean:277: def ChurchVec (α : Type) : Type := (α → List α → List α) → List α → List α
• ArkLib/Data/CNat/Defs.lean:89: def mulNat [Zero T] (a : Cayley T) : Nat → Cayley T
• ArkLib/Data/CNat/Defs.lean:115: def subNat [Zero T] [ToNat T] (a : Cayley T) : Nat → Cayley T
• ArkLib/Data/CNat/Defs.lean:128: def powNat [Zero T] [One T] [ToNat T] (a : Cayley T) : Nat → Cayley T
• ArkLib/Data/CNat/Defs.lean:142: def divNat [Zero T] [DecidableEq T] [ToNat T]
• ArkLib/Data/CNat/Defs.lean:171: def modNat [Zero T] [DecidableEq T] [ToNat T]
• ArkLib/Data/CNat/Defs.lean:255: def CayleyTower (n : ℕ) : (T : Type) × (HasSucc T) :=
• ArkLib/Data/List/BigOperators.lean:18: def partialSum {α : Type*} [AddMonoid α] (l : List α) : List α :=
• ArkLib/Data/List/BigOperators.lean:24: def partialProd {α : Type*} [Monoid α] (l : List α) : List α :=
• ArkLib/Data/List/BigOperators.lean:41: def findSum (l : List α) (j : α) : Option α :=
• ArkLib/Data/List/Find.lean:16: def findIdx' (p : α → Bool) (l : List α) : ℕ :=
• ArkLib/Data/List/Find.lean:32: def idxOf' [BEq α] (a : α) (l : List α) : ℕ :=
• ArkLib/Data/List/HList.lean:29: def nil : HList := []
• ArkLib/Data/List/HList.lean:31: def cons (x : Σ α : Type u, α) (xs : HList) : HList :=
• ArkLib/Data/List/HList.lean:92: def DVec {m : Type v} (α : m → Type u) : Type (max u v) :=
• ArkLib/Data/Polynomial/EvenAndOdd.lean:210: lemma f_eq_evenPart_plus_x_oddPart {f : Polynomial F} :
• ArkLib/ToMathlib/UInt/Equiv.lean:9: def finUInt8Equiv : Fin (2 ^ 8) ≃ UInt8 where

Tactic Formatting Violations

Rule: "Place by at the end of the line preceding the tactic block. Indent the tactic block."

• ArkLib/Data/CNat/AssocNat.lean:137: theorem succ_mul ... : (succ a) * b = a * b + b := by sorry
• ArkLib/Data/CNat/AssocNat.lean:140: theorem mul_add ... : a * (b + c) = a * b + a * c := by sorry
• ArkLib/Data/CNat/AssocNat.lean:143: theorem one_mul {a : AssocNat} : 1 * a = a := by (The by is on the same line as the theorem signature).
• ArkLib/Data/CNat/Church.lean:131: theorem add_zero : @add α zero = @id (ChurchNat α) := rfl (Preferred as term mode, but if using tactics elsewhere, consistency is required; however, the following lines violate the specific by rule).
• ArkLib/Data/CNat/Church.lean:192: theorem add_comm (m n : ChurchNat α) : add m n = add n m := by (The by is on the same line as the signature).
• ArkLib/Data/Polynomial/EvenAndOdd.lean:175: private lemma evenPart_eq_evenPart' {f : Polynomial F} : evenPart f = evenPart' f := by (The by is on the same line as the signature).

---

📄 **Per-File Summaries**

• .github/workflows/ci.yml: Updated the CI workflow to utilize the standard Lean action's built-in caching while disabling linting to bypass existing errors.
• .github/workflows/docs.yml: Updates the documentation workflow's caching configuration by generalizing the cache key and enabling GitHub caching for the project build.
• ArkLib.lean: Expanded the library's public API by importing several new modules for commitment schemes, coding theory, data structures, and proof systems.
• ArkLib/CommitmentScheme/Tensor.lean: Adds a new file to define tensor-based polynomial commitment schemes and their underlying square-root IOPs.
• ArkLib/CommitmentScheme/Trivial.lean: Introduces trivial commitment schemes where the prover sends data directly to the verifier, specifically defining a trivial polynomial commitment scheme for bounded-degree 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 implements Church encoding for natural numbers, booleans, and vectors to demonstrate the definitional properties of functional arithmetic in Lean.
• ArkLib/Data/CNat/Defs.lean: Implements the Cayley Tower and CNat hierarchy, providing iterated encodings of natural numbers where operations like addition and multiplication gain definitional associativity through a functional representation.
• ArkLib/Data/Classes/HasPred.lean: Defines the HasPred and LawfulHasPred typeclasses to provide a predecessor operation and ensure it acts as a left inverse to the successor operation, with an implementation for natural numbers.
• ArkLib/Data/Classes/HasSucc.lean: Defines the HasSucc and LawfulHasSucc typeclasses to provide a successor operation and ensure its equivalence to adding one.
• ArkLib/Data/Classes/ToNat.lean: Defines the ToNat type class and its lawful counterpart to provide a uniform interface for converting types to natural numbers consistently with zero and successor operations.
• ArkLib/Data/CodingTheory.lean: This new file serves as a top-level module that aggregates all submodules within the coding theory directory.
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean: This file adds an extensionality theorem for polynomial sums, proving that two sums are equal if their underlying summand functions are pointwise equal.
• ArkLib/Data/CodingTheory/ReedMuller.lean: Initializes the ReedMuller.lean module to provide a foundation for defining Reed-Muller error-correcting codes as evaluations of multivariate polynomials.
• ArkLib/Data/List/BigOperators.lean: Introduces definitions and theorems for computing partial sums and products of lists, along with utilities for locating elements based on cumulative sums.
• ArkLib/Data/List/Find.lean: Introduces variants of list indexing functions, such as findIdx and idxOf, with improved definitional equality and versions that return Fin types.
• ArkLib/Data/List/HList.lean: Defines a heterogeneous list type (HList) as a list of sigma types and provides basic operations, lemmas, and conversions to dependent vectors.
• ArkLib/Data/List/Vector.lean: Defines utility functions interleave and chunkPairwise for the List.Vector type in a new file.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: Defines the even and odd parts of a polynomial and provides lemmas for their decomposition, evaluation, and transformation.
• ArkLib/ProofSystem/DSL.lean: Introduces an experimental domain-specific language (DSL) for defining vector and polynomial-based Interactive Oracle Proofs (IORs) using scalar and vector operations.
• ArkLib/ProofSystem/Stir.lean: This file defines the Stir proof system module by aggregating its various sub-components through a central set of imports.
• ArkLib/ProofSystem/Stir/MainThm.lean: Replaces the sorry placeholder in the stir_rbr_soundness theorem with a formal proof.
• ArkLib/ProofSystem/Whir.lean: This file establishes the top-level module for the WHIR proof system by importing its core components, including folding, soundness proofs, and proximity generation.
• ArkLib/ToMathlib/UInt/Equiv.lean: Defines equivalences between Fin (2 ^ n) and various fixed-width integer types, specifically UInt8, UInt16, UInt32, UInt64, and BitVec.

---

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

[quangvdao]

Thanks for spotting this! I have restated the theorem (correctly) in #377