feat(coding-theory): integrate CompPoly's executable Guruswami-Sudan decoder

[olympichek]

Overview

This PR connects ArkLib's Guruswami-Sudan development to the executable decoder recently added in CompPoly. It adds the translation layer needed to run the CompPoly decoder on ArkLib Reed-Solomon inputs and state the result in ArkLib's existing degree-and-distance specification.

This PR includes:

• A small wrapper around CompPoly's decoder parameters and selector interface.
• A bounded search for decoder parameters, with certificates for the conditions ArkLib needs.
• Conversions between ArkLib Reed-Solomon words and CompPoly's packed received-word format.
• Proofs that the executable decoder returns exactly the polynomials described by ArkLib's degree-and-distance specification.
• A bump to CompPoly v4.30.0-patch1, together with the new imports.

Correctness

The main theorem says that the executable output matches the ArkLib specification: returned polynomials have degree < k and are within the requested Hamming radius, and every polynomial with those properties appears in the output. There are also compatibility lemmas relating this statement to ArkLib's existing decoder under the Johnson-radius assumption.

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Formalizes exists_multiplicity_of_johnson to provide multiplicity and list size parameters based on the Johnson radius.
• Establishes soundness and completeness: proves the executable decoder output matches ArkLib’s degree-and-distance specification.
• Relates the executable decoder to ArkLib's existing decoder via compatibility lemmas under the Johnson-radius assumption.
• Proves the existence of interpolation witnesses using capacity bounds.

Executable Integration

• Integrates CompPoly's Guruswami-Sudan decoder and updates the library dependency to v4.30.0-patch1.
• Implements a certified parameter selector that performs a bounded search for valid decoding parameters.
• Adds a translation layer to convert between ArkLib Reed-Solomon words and CompPoly’s packed received-word format.
• Wraps CompPoly’s decoder parameters and selector into an ArkLib-compatible interface.

Refactoring and Infrastructure

• Reorganizes the Guruswami-Sudan module to separate the core algorithm, correctness proofs, and executable integration.
• Simplifies internal proofs within ArkLib/Data/CodingTheory/Prelims.lean to improve maintainability.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	920
❌ Lines Removed	68

---

Lean Declarations

✏️ **Added:** 47 declaration(s)

• def boundedSearchParamSelector {maxM maxW : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem agreement_card_add_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• noncomputable def johnsonParamSelector : GSParamSelector where in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_spec in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def RepresentsArkInput in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationMonomials_size (params : GSInterpParams) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma foldl_size_add {α β : Type*} (step : Array β → α → Array β) (d : α → Nat) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def execParamsOfMultiplicityAndDegree in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• private lemma foldl_push_size {α β : Type*} (g : Array β → α → β) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decode_complete in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem searchParamsUpTo_sound {maxM maxW k n e : Nat} {params : GSExecParams} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem toPoly_degree_lt_of_degreeLt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• lemma exists_multiplicity_of_johnson {k n e : ℕ} in ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean
• theorem candidateMismatchCount_represents_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decode_iff_mem_decoder_of_degree_lt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_mem_decoder_of_degree_lt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem toPoly_natDegree_lt_of_degreeLt in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem paramsCert_of_johnson {k n e : Nat} (hjohnson : JohnsonSpecCondition k n e) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def searchParamsUpTo in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• private theorem cPolynomialOfPoly_toPoly (p : F[X]) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decode_iff_spec in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma sum_map_const {α : Type*} (l : List α) (c : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decodeWithParams_sound in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma length_filter_ofFn_eq_card {α : Type*} {n : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma list_foldl_count_false {α : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma sum_range'_sub_two (m : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def GSSpecSet (k e : Nat) (ωs : Fin n ↪ F) (f : Fin n → F) : Set F[X] in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationConstraints_size {F : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private def cPolynomialOfPoly (p : F[X]) : CompPoly.CPolynomial F in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decodeWithParams_complete in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma list_foldl_count_true {α : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def JohnsonSpecCondition (k n e : Nat) : Prop in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• theorem passesCandidateDistance_represents_hammingDist in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• def paramsPassIntegerChecks in ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean
• theorem matchingPointCount_represents_card in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private def constraintsFold {F : Type*} (points : Array (F × F)) (m : Nat) : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private theorem degreeLt_cPolynomialOfPoly_of_degree_lt {p : F[X]} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem interpolationWitnessExists_of_capacity in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• example : GSParamCert 2 5 1 (execParamsOfMultiplicityAndDegree 2 1 1 3) in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem length_of_represents in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma mem_monomialGrid {D : Nat} {mm : Monomial} : in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem paramsPassIntegerChecks_iff in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem distinctXCoordinates_of_represents in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem mem_decodeWithParams_iff_degree_and_distance in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem searchParamsUpTo_complete {maxM maxW k n e : Nat} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• theorem decode_sound in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean
• private lemma interpolationConstraints_eq_fold {F : Type*} in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Pull Request Guidelines

• Title Format: Ensure the PR title follows <type>(<optional-scope>): <subject>. For example: feat(GuruswamiSudan): add executable GS decoder and correctness proofs.

Style and Naming Guidelines

• Variable Conventions: The use of ωs and f in Correctness.lean is consistent with adjacent Reed-Solomon files, and the use of h prefixes for hypotheses (e.g., hrep, hparams) follows the h, h₁ convention.
• Naming Conventions: Types and Props such as GSParamCert, GSSpecSet, and RepresentsArkInput correctly use UpperCamelCase. Functions like paramsPassIntegerChecks correctly use lowerCamelCase.
• Theorem Naming Logic: Theorem names such as paramsPassIntegerChecks_iff and interpolationWitnessExists_of_capacity correctly use snake_case and follow the _iff and _of_ conventions.

Syntax and Formatting

• Line Length: Several lines in ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean exceed the 100-character limit:
  • Line 126 (declaration of boundedSearchParamSelector): ~147 characters.
  • Line 149 (hypothesis hex in searchParamsUpTo_complete): ~172 characters.
  • Line 411 (declaration of mem_decodeWithParams_iff_degree_and_distance): ~120 characters.
  • Line 639 (hypothesis he in mem_decodeWithParams_iff_mem_decoder_of_degree_lt): ~115 characters.
• Functions: In Correctness.lean, the code uses fun x => ... (e.g., lines 23, 116, 222). Per guidelines, prefer the fun x ↦ ... syntax.
• Operators: Spaces around :, :=, and infix operators are correctly applied throughout the new files.

Documentation Standards

• Declaration Docstrings: Major theorems and definitions in Correctness.lean and Executable.lean have docstrings.
• Citations: The Guruswami-Sudan algorithm and the Johnson bound are referenced in text, but the new modules lack a ## References section in their headers with citation keys (e.g., [GS99]) and corresponding BibTeX entries as required by the Citation Standards for academic papers.
• Sectioning: The use of /-! ### Title -/ for structure is followed correctly in the new files.

---

📄 **Per-File Summaries**

• ArkLib.lean: This update expands the Guruswami-Sudan decoding module by adding imports for its correctness proofs and executable implementation. These changes integrate these submodules into the main library entry point.
• ArkLib/Data/CodingTheory/GuruswamiSudan.lean: This change updates the Guruswami-Sudan module by importing submodules for its executable implementation and correctness proofs, effectively aggregating the algorithm's definition and formal verification into a single entry point.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Correctness.lean: This file establishes the formal correctness of the executable Guruswami-Sudan Reed-Solomon decoder by proving its soundness and completeness relative to the ArkLib specification. It introduces theorems connecting the computational backend to mathematical constraints, such as proving the existence of interpolation witnesses via capacity bounds and the availability of valid parameters within the Johnson radius. The file contains no sorry or admit placeholders.
• ArkLib/Data/CodingTheory/GuruswamiSudan/Executable.lean: This new file establishes an integration layer between ArkLib and the CompPoly library for an executable Guruswami-Sudan decoder. It introduces definitions for parameter certification, search logic, and a certified parameter selector structure that includes soundness and completeness properties relative to the Johnson radius condition.
• ArkLib/Data/CodingTheory/GuruswamiSudan/GuruswamiSudan.lean: Introduces the lemma exists_multiplicity_of_johnson to prove that a valid multiplicity parameter exists when the error count is within the Johnson radius. The proof of mem_decoder_of_dist is modified to utilize this new lemma, refactoring the previous inlined logic into a more modular structure.
• ArkLib/Data/CodingTheory/Prelims.lean: The changes in ArkLib/Data/CodingTheory/Prelims.lean simplify a proof step within the rank_eq_if_subUpFull_eq lemma by replacing a redundant use of Equiv.refl with the identity function. This modification streamlines the existing proof without introducing new theorems, definitions, or sorry placeholders.

---

Last updated: 2026-06-16 14:12 UTC.

[olympichek]

@MavenRain thank you for your review of this PR! I just pushed a pair of new commits to address issues/gaps you pointed out

[Abraxas1010]

Coordination note (complementary lane, no file overlap intended): we are preparing the encoder-side executable bridge — a theorem that CompPoly's Univariate.ReedSolomon.encode output, read through the embedding induced by Domain.node_injective, is a member of ArkLib's ReedSolomon.code (with the messagePoly.toPoly / messagePoly_degree_lt / eval_toPoly witness chain), followed by the NTT fast-encoder equality via forwardImpl_eq_evalOnDomain. Statement-level typing is validated against ArkLib main.

Two touch points with this PR:

1. CompPoly pin: ArkLib's pinned rev 18c1613 predates CompPoly/Univariate/ReedSolomon.lean, and this PR already carries a manifest bump — we plan to base on (or land after) your bump rather than race it.
2. Conversions: if your ArkLib↔CompPoly received-word conversion layer is the intended canonical one, we'll consume it for the codeword direction rather than adding a parallel one — happy to adjust to whatever shape lands here.

Placement guidance welcome (ArkLib/ToCompPoly/CodingTheory/ vs alongside this PR's files).

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.