Make Constrained RS codes not depend on Smooth

[ElijahVlasov]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Make Constrained RS codes not depend on Smooth

This pull request removes the dependency of constrained and multi-constrained Reed–Solomon codes on the Smooth typeclass/infrastructure and replaces them with a self-contained module. The change is purely a restructuring of the codebase: the old Smooth-based definitions are deleted, and a new module Constrained.lean introduces equivalent definitions that do not reference Smooth. No existing theorems are broken (the new lemma rs_code_is_multi_constrained recovers the ordinary Reed–Solomon code as the zero-constraint case), and no sorry or admit placeholders are added. A single import line in ArkLib.lean ensures the new module is transitively available.

Dependency Cleanup (Removal of Smooth-based infrastructure)

• ArkLib/Data/CodingTheory/ReedSolomon.lean – The entire block defining the Smooth typeclass, smoothCode definition, mVdecode linear map, toWeightAssignment and weightConstraint helpers, and the constrainedCode/multiConstrainedCode set definitions has been deleted. This removes all reliance on the Smooth module.
• No replacement code is added in this file; the constrained-code support is moved to the new module below.

Mathematical Formalization (New standalone module)

• ArkLib/Data/CodingTheory/ReedSolomon/Constrained.lean – Introduces formal counterparts to Definitions 4.5 and 4.6 of the WHIR paper (ACFY24). Key definitions:
  • toWeightAssignment (private helper)
  • weightConstraint – predicate expressing a linear constraint on weights
  • constrainedCode – set of codewords satisfying a single weight constraint
  • multiConstrainedCode – set of codewords satisfying multiple weight constraints
• Proves rs_code_is_multi_constrained : the ordinary Reed–Solomon code equals the multi-constrained code with no constraints (using simp).
• No sorry or admit placeholders.

Infrastructure

• ArkLib.lean – Added import of ArkLib.Data.CodingTheory.ReedSolomon.Constrained so that the new definitions are visible through the top-level ArkLib namespace.

Notes

• The PR body is empty; the description above is derived from the per-file summaries and reflects the actual code changes.
• The restructuring makes constrained Reed–Solomon codes independent of the Smooth typeclass, fulfilling the PR title’s objective.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	67
❌ Lines Removed	56

---

Lean Declarations

✏️ Removed: 6 declaration(s)

ArkLib/Data/CodingTheory/ReedSolomon.lean (6)

• def constrainedCode
• def multiConstrainedCode
• def weightConstraint
• noncomputable def mVdecode :
• noncomputable def smoothCode
• private noncomputable def toWeightAssignment

✏️ Added: 5 declaration(s)

ArkLib/Data/CodingTheory/ReedSolomon/Constrained.lean (5)

• def constrainedCode
• def multiConstrainedCode
• def weightConstraint
• lemma rs_code_is_multi_constrained
• private noncomputable def toWeightAssignment

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import of ArkLib.Data.CodingTheory.ReedSolomon.Constrained, making the ReedSolomon module's constrained variant available to all files that transitively import ArkLib. This is part of expanding the coding theory sublibrary with a constrained Reed–Solomon code module, which likely defines codes where codewords are restricted to a subspace or satisfy additional linear constraints.
• ArkLib/Data/CodingTheory/ReedSolomon.lean: Removes the entire block defining Smooth Reed-Solomon code variants and their weight- and multi-constrained analogues: the Smooth typeclass, smoothCode definition, mVdecode linear map, toWeightAssignment and weightConstraint helpers, and the constrainedCode and multiConstrainedCode set definitions. These removals delete the initial implementation of constrained Reed-Solomon code support without any replacement in this diff.
• ArkLib/Data/CodingTheory/ReedSolomon/Constrained.lean: This new file adds formal definitions for constrained and multi-constrained Reed–Solomon codes as described in Definitions 4.5 and 4.6 of the WHIR paper (ACFY24). It introduces the private helper toWeightAssignment, the predicates weightConstraint, constrainedCode, and multiConstrainedCode, and proves the lemma rs_code_is_multi_constrained that the ordinary Reed–Solomon code coincides with the zero-constraint multi-constrained code (via simp). No sorries or admits are present.

---

Last updated: 2026-08-30 12:04 UTC.

[quangvdao]

Thanks, Ilia — moving the constrained-code definitions out of the generic ReedSolomon module and onto the concrete smooth FFT domain is a sensible architectural direction.

I reviewed exact head 4089b8b46e6f0298bfb6391e85e99c52ba06102f against its recorded base d57c8e11855c2fd528b8521f4e3b90dd2d7a64c9, and checked it against current upstream main at 5a9626d331d713c7e74efa7e3d93b7d0ec9c4dc2.

Verdict

Requesting changes. The definitions themselves correspond sensibly to WHIR Definitions 4.5 and 4.6, but the PR currently breaks a documented public declaration and fails required checks.

Merge blockers

1. [P2] Public API / blueprint regression. The move deletes ReedSolomon.smoothCode (and also mVdecode) while blueprint/src/coding_theory/defs.tex still declares ReedSolomon.smoothCode. The blueprint checker therefore fails with ReedSolomon.smoothCode is missing. Please either:

   • retain/move these declarations, using deprecated compatibility aliases if the new API should replace them; or
   • make the removal explicit, update the blueprint and documentation, and provide a migration path for the old public API.

   Since the stated goal is only to remove the Smooth dependency from constrained codes, preserving the unrelated public names is the smallest repair.

2. Required hygiene. The whitespace job identifies trailing spaces on lines 61–62 of Constrained.lean (and git diff --check also reports the blank line at EOF). The new module also needs the repository-required module docstring with a ## References section and a properly formatted [ACFY24] citation.

3. API transition. The old constrained-code API accepted an arbitrary embedding with [Smooth domain]; the replacement accepts only SmoothCosetFftDomain n F. That may be the intended boundary, but it is a public narrowing. Please either supply a compatibility bridge or explain the deliberate break and update affected documentation/consumers.

Nonblocking source/coverage request

rs_code_is_multi_constrained uses (t=0), so the result follows from an empty family of constraints. If this is intended to capture the WHIR observation that an ordinary smooth RS code is constrained by the zero weight/target, please add the explicit one-zero-constraint theorem (or explain why the empty-family formulation is the desired library statement). That would be a more falsifiable source bridge than the vacuous Fin 0 case.

Validation

• The exact head completes the Lean build and normal validation path; imports and docs-integrity checks pass.
• The combined build workflow fails at blueprint declaration checking, and whitespace fails as above.
• No new sorry, admit, unsafe declaration, or axiom was found.
• The branch is behind current main, but a synthetic merge-tree check is currently clean.

Please also use a conventional title such as refactor(coding-theory): decouple constrained RS codes from Smooth and expand the PR body with motivation, compatibility impact, and source correspondence. Thanks again — this should be a compact repair once the API decision is made.

[quangvdao]

[P2] Preserve or deliberately migrate this public declaration. Removing smoothCode is broader than decoupling constrainedCode from the Smooth class, and it immediately breaks the blueprint's \lean{ReedSolomon.smoothCode} declaration check. The smallest repair is to retain/move it (and consider a deprecated compatibility alias if its replacement changes type); otherwise update the blueprint/docs and describe the migration explicitly.