Batched FRI soundness

[Julek]

Blueprint of Batched FRI soundness result from "Proximity Gaps for Reed-Solomon Codes" (section 8)

[github-actions]

🤖 Gemini PR Summary

This diff represents a major step towards formalizing the security of the FRI protocol, underpinned by a significant refactoring of the algebraic and field theory libraries.

Here is a summary of the key changes:

• Refactoring of Algebra Towers:

  • The custom AlgebraTower class has been renamed and refactored into TowerOfAlgebra and AssocTowerOfAlgebra. This change is propagated throughout the codebase, particularly in the binary field tower implementation.

• Binary Field Tower Implementation:

  • The definitions for both the abstract (BTField) and concrete (ConcreteBTField using BitVec) binary field towers have been heavily reworked for greater clarity and correctness.
  • A formal equivalence between the abstract and concrete tower constructions (AssocTowerOfAlgebraEquiv) has been introduced, though the proofs are still in progress.

• FRI Security Proof Framework:

  • A new file, ArkLib/ProofSystem/BatchedFri/Security.lean, has been added to lay the groundwork for FRI's soundness proof, referencing the "Proximity Gaps for Reed-Solomon Codes" paper.
  • ArkLib/Data/CodingTheory/ProximityGap.lean is significantly expanded with new sections defining concepts like "correlated agreement on a curve" and "weighted agreement," which are crucial for the security analysis.

• Protocol Specification and Cleanup:

  • The FRI protocol's verifier logic and domain definitions have been cleaned up. For instance, the method for generating query points was simplified.
  • The implementation of the Additive NTT (AdditiveNTT/Impl.lean) was removed, likely to streamline focus on the FRI security proof.
  • Several proofs across the coding theory library have been temporarily replaced with sorry, indicating a work-in-progress refactoring.

In essence, this diff strengthens the algebraic foundations and introduces the core theoretical components required to formally prove the security of the FRI protocol.

---

Analysis of Changes

Metric	Count
📝 Files Changed	19
✅ Lines Added	3003
❌ Lines Removed	3612

---

sorry Tracking

• ❌ Added: 22 sorry(s)
  • theorem weighted_correlated_agreement_for_parameterized_curves' in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma fri_query_soundness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • lemma split_join_via_add_smul_eq_iff_split {k : ℕ} (h_pos : k > 0) in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • instance {t l : ℕ} : in ArkLib/ProofSystem/BatchedFri/Security.lean
  • theorem weighted_correlated_agreement_for_parameterized_curves in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved in ArkLib/Data/CodingTheory/InterleavedCode.lean
  • lemma algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : BTField i) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • lemma fri_round_consistency_completeness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • theorem large_agreement_set_on_curve_implies_correlated_agreement {l : ℕ} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma list_agreement_on_curve_implies_correlated_agreement_bound in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def hli_level_diff_0 (l : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • theorem generator_is_not_lifted_to_succ (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem weighted_correlated_agreement_over_affine_spaces' in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem large_agreement_set_on_curve_implies_correlated_agreement' {l : ℕ} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma sqrt_le_J {q x : ℚ} : in ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
  • theorem unique_linear_decomposition_succ (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • theorem minPoly_of_powerBasisSucc_generator (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem average_proximity_implies_proximity_of_linear_subspace [DecidableEq ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma fri_soundness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • lemma sufficiently_large_list_agreement_on_curve_implies_correlated_agreement in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem towerEquiv_commutes_left (i j : ℕ) (h : i ≤ j) : ∀ r : ConcreteBTField i, in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem weighted_correlated_agreement_over_affine_spaces in ArkLib/Data/CodingTheory/ProximityGap.lean

---

Last updated: 2025-12-09 13:35 UTC. See the main CI run for build status.

[Julek]

@alexanderlhicks @quangvdao See here for typeclass inference issue 🙂