feat(Poseidon2): prove permute bound obligations

[pitmonticone]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

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

[github-actions]

🤖 Gemini PR Summary

This PR primarily addresses the formal verification of the Poseidon2 hash function by replacing sorry placeholders with autoformalized proofs. In addition to these fixes, it significantly expands the ArkLib library with new primitives for commitment schemes, coding theory, and advanced arithmetic representations.

Features

• Cryptographic Commitment Schemes:
  • Introduced a tensor-based Interactive Oracle Proof (IOP) framework supporting schemes like Ligero, Brakedown, and Binius.
  • Added Trivial Commitment Schemes for basic prover-verifier data exchange and univariate polynomial degree checks.
• Proof Systems & DSL:
  • Established entry points and core aggregations for the Stir and Whir proof systems.
  • Introduced an experimental DSL for specifying vector and polynomial-based interactive oracle relations (IORs).
• Coding Theory:
  • Implemented Reed-Muller codes based on multivariate polynomial evaluations.
  • Added a centralized CodingTheory module for better organization.
• Advanced Arithmetic & Data Structures:
  • Implemented Church-encoded and Cayley Tower natural numbers (CNat, AssocNat) to provide definitionally associative arithmetic operations.
  • Introduced the HasPred, HasSucc, and ToNat typeclasses to standardize numeric interfaces.
  • Added a decomposition utility for Even and Odd polynomials, facilitating FFT-style operations.
• Utility Library Expansions:
  • Lists/Vectors: New utilities for heterogeneous lists (HList), partial sums/products, improved index searching (findIdx'), and vector interleaving/grouping.
  • Mathlib Extensions: Added equivalences between Fin types and fixed-precision integers (UInt8 through UInt64 and BitVec).

Fixes

• Poseidon2 Verification: Completed the formal verification of the permute function by replacing sorry placeholders with proofs validating round constant indexing and slicing.
• Summation Extensionality: Added a missing extensionality lemma for Polynomial.sum to ensure equal summands result in equal sums.

Refactoring

• Module Organization: Updated the main ArkLib.lean entry point and sub-modules (CodingTheory, Stir, Whir) to aggregate new functionality and improve library discoverability.
• CI/CD Optimization:
  • Migrated CI workflows to use the standard lean-action for improved caching and automated builds.
  • Explicitly disabled the linter in CI to streamline the build process for autoformalized content.

Documentation

• Workflow Updates: Updated the documentation deployment workflow to utilize a unified cache key and built-in Lean action caching.

---

Analysis of Changes

Metric	Count
📝 Files Changed	24
✅ Lines Added	2291
❌ Lines Removed	3

---

sorry Tracking

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

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

---

🎨 **Style Guide Adherence**

Error: [Errno 104] Connection reset by peer

---

📄 **Per-File Summaries**

• .github/workflows/ci.yml: The CI workflow was updated to use the standard lean-action for automated caching and builds while explicitly disabling the linter.
• .github/workflows/docs.yml: Update the documentation workflow to use a unified cache key and enable built-in caching for the Lean build action.
• ArkLib.lean: Update the library's main entry point to include several new modules across commitment schemes, data structures, coding theory, and proof systems.
• 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: Introduces trivial commitment schemes where the prover sends data directly and the verifier enforces checks, such as degree bounds for univariate polynomials.
• ArkLib/Data/CNat/AssocNat.lean: Introduces AssocNat, a representation of natural numbers as successor-preserving endomaps of Nat designed to make addition definitionally associative.
• ArkLib/Data/CNat/Church.lean: Implements Church-encoded natural numbers, booleans, and vectors to demonstrate how functional representations enable definitional properties like associativity in arithmetic operations.
• ArkLib/Data/CNat/Defs.lean: Implements the Cayley Tower, an iterated construction of natural numbers (CNat) that uses function composition to provide definitionally associative arithmetic operations.
• ArkLib/Data/Classes/HasPred.lean: Defines the HasPred and LawfulHasPred typeclasses to provide a standardized interface for predecessor operations and their relationship with successor operations, including instances for natural numbers.
• ArkLib/Data/Classes/HasSucc.lean: Defines the HasSucc and LawfulHasSucc typeclasses to provide a standardized successor operation and ensure its consistency with addition by one.
• ArkLib/Data/Classes/ToNat.lean: Defines the ToNat type class and its lawful properties to provide a uniform interface for converting types to natural numbers.
• ArkLib/Data/CodingTheory.lean: Introduced a top-level CodingTheory module that aggregates its various submodules through imports.
• ArkLib/Data/CodingTheory/BerlekampWelch/ToMathlib.lean: Adds an extensionality lemma for Polynomial.sum showing that equal summand functions produce equal sums.
• ArkLib/Data/CodingTheory/ReedMuller.lean: Introduces the ReedMuller.lean file to define Reed-Muller codes as a family of error-correcting codes based on multivariate polynomial evaluations.
• ArkLib/Data/Hash/Poseidon2.lean: Replaced sorry placeholders with formal proofs to validate the indexing and slicing of round constants within the permute function.
• ArkLib/Data/List/BigOperators.lean: Introduces definitions and lemmas for partial sums, partial products, and searching cumulative sums within lists.
• ArkLib/Data/List/Find.lean: This file introduces findIdx' and idxOf' with improved definitional equality, along with variants that return results as bounded Fin types.
• ArkLib/Data/List/HList.lean: Defines heterogeneous lists as a synonym for List (Σ α, α) and provides a basic API, custom notation, and conversions to dependent vectors.
• ArkLib/Data/List/Vector.lean: Added a new file providing utility functions for Vector types, specifically introducing definitions for interleaving vectors and grouping elements into pairs.
• ArkLib/Data/Polynomial/EvenAndOdd.lean: Defines the decomposition of polynomials into even and odd components and provides utilities for FFT-style splitting and evaluation.
• ArkLib/ProofSystem/DSL.lean: Introduces an experimental DSL for specifying vector and polynomial-based interactive oracle relations (IORs).
• ArkLib/ProofSystem/Stir.lean: This file establishes a central entry point for the Stir proof system by aggregating its various constituent submodules.
• ArkLib/ProofSystem/Whir.lean: This PR creates the central entry point for the Whir proof system by aggregating its core components, including folding, soundness, and proximity generation.
• ArkLib/ToMathlib/UInt/Equiv.lean: Defines equivalences between Fin types and various fixed-precision integer types, including UInt8, UInt16, UInt32, UInt64, and BitVec.

---

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

[quangvdao]

small style nit: can you define separate private lemmas for these proofs, then invoke those lemmas, so we don't clog the main definition?