fix(STIR/WHIR): correct theorem assumptions and clear non-sorry warnings

[quangvdao]

Summary

• fix STIR and WHIR theorem statements to remove vacuous/over-strong assumptions and align quantifier placement with intended probability semantics
• clean warning-only lint issues across STIR/WHIR (unused simp args, unused hypotheses/instances, style warnings) while keeping all sorry declarations untouched
• update affected theorem/lemma docstrings to reflect corrected statements and notation

Test plan

• lake build ArkLib.ProofSystem.Stir.MainThm ArkLib.ProofSystem.Stir.Folding ArkLib.ProofSystem.Stir.Quotienting ArkLib.ProofSystem.Stir.ProximityGap ArkLib.ProofSystem.Stir.ProximityBound ArkLib.ProofSystem.Stir.OutOfDomSmpl ArkLib.ProofSystem.Stir.Combine ArkLib.ProofSystem.Whir.BlockRelDistance ArkLib.ProofSystem.Whir.OutofDomainSmpl ArkLib.ProofSystem.Whir.RBRSoundness ArkLib.ProofSystem.Whir.ProximityGen ArkLib.ProofSystem.Whir.MutualCorrAgreement ArkLib.ProofSystem.Whir.Folding
• verify remaining STIR/WHIR warnings are only declaration uses sorry

Made with Cursor

[github-actions]

🤖 Gemini PR Summary

Theorem Refinements & Probability Semantics

• Quantifier Alignment: Corrected the placement of universal quantifiers in Whir/Folding.lean, moving function and distance bound variables outside of probability expressions. This ensures probability is measured over random coins for fixed functions, aligning with intended soundness semantics.
• Constraint Relaxation: Removed "vacuous" or overly restrictive preconditions across STIR and WHIR:
  • Eliminated the non-zero constraint on $\varphi$ in the combine_eq_cases lemma.
  • Relaxed initial code-distance and non-membership hypotheses in the main STIR soundness and WHIR Round-by-Round (RBR) soundness theorems.
  • Updated ProximityGap.lean to explicitly require $\delta > 0$ and adjusted conclusions to accommodate distinct codewords for each function index.
• Parameter Consistency: Standardized the use of the dstar degree parameter in combine_theorem to ensure matching degree bounds throughout the inductive steps of the STIR protocol.

Assumption Generalization & Logic

• Typeclass Decoupling: Removed or localized DecidableEq and Fintype requirements in modules such as MainThm, Quotienting, and MutualCorrAgreement. This generalizes the theorems for use in infinite fields or contexts where equality is not computationally decidable.
• Hypothesis Refactoring: Split hypotheses in proximity gap analyses to provide granular control, simplifying the invocation of these lemmas in higher-level soundness proofs.
• Tactic Optimization: Refined proof tactics and linter settings in folding modules to improve compilation performance and maintainability.

Code Quality & Maintenance

• Linter Compliance: Resolved all "warning-only" issues across the STIR and WHIR directories, including unused simp arguments, unused hypotheses/instances, and style-related warnings. All sorry declarations remain untouched.
• Documentation Alignment: Updated docstrings for major theorems and lemmas to reflect corrected mathematical statements and updated notation.
• Verified Test Plan: Confirmed successful builds for all primary STIR and WHIR modules and verified that remaining warnings are strictly limited to declaration uses sorry.

---

Analysis of Changes

Metric	Count
📝 Files Changed	10
✅ Lines Added	111
❌ Lines Removed	111

---

Lean Declarations

✏️ **Affected:** 1 declaration(s) (line number changed)

• lemma quotienting {degree : ℕ} {domain : ι ↪ F} [Nonempty ι] in ArkLib/ProofSystem/Stir/Quotienting.lean moved from L61 to L61

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following code changes violate the provided style guide:

ArkLib/ProofSystem/Stir/Combine.lean

• Line 68: lemma combine_eq_cases lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 71: Variables dstar and degs violate the natural number naming convention. "Natural numbers: m, n, k, ..."
• Line 75: fun x => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 92-105: Indentation of 6 spaces violates the 2-space indentation rule. "Use 2 spaces for indentation."
• Line 116: lemma degreeCor_eq violates the theorem naming convention. "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)." (Should be degree_cor_eq).
• Line 118: fun x => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 158: ... > proximityError ... violates the inequality convention for theorem statements. "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• Line 159: ∑ i degsᵢ violates the binder spacing convention. "Use a space after binders (e.g., ∀ x, not ∀x,)." (Missing comma/space after binder i).
• Line 162: jointAgreement violates the naming convention for structures/types. "Types and Structures: UpperCamelCase (e.g., MonoidHom, Visualizer)."

ArkLib/ProofSystem/Stir/Folding.lean

• Line 152: Variable t violates the natural number naming convention. "Natural numbers: m, n, k, ...". (The guide reserves t for "Sets or Lists").
• Line 155: fun i : Fin 2 => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 158: Hypothesis h_deg_term violates the naming convention for terms. "Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime)." (Should be hDegTerm).

ArkLib/ProofSystem/Stir/MainThm.lean

• Line 117: secpar violates the natural number naming convention. "Natural numbers: m, n, k, ..."
• Line 121: proofLen, qNumtoInput, and qNumtoProofstr violate the natural number naming convention. "Natural numbers: m, n, k, ..."
• Line 121: qNumtoInput violates acronym naming. "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)." (Should be qNumToInput).

ArkLib/ProofSystem/Stir/ProximityGap.lean

• Line 31: lemma proximity_gap lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 36: fun x => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 38: ... > ENNReal.ofReal ... violates the inequality convention for theorem statements. "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• Line 40: S.card ≥ ... violates the inequality convention for theorem statements. "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."

ArkLib/ProofSystem/Stir/Quotienting.lean

• Line 62: lemma quotienting lacks a docstring. "Every definition and major theorem should have a docstring."

ArkLib/ProofSystem/Whir/BlockRelDistance.lean

• Line 128: lemma blockRelDistance_eq_relHammingDist_of_k_eq_i lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 133: lemma blockRelDistance_eq_relHammingDist_of_k_eq_i violates naming conventions for theorems. "Theorems and Proofs: snake_case." (Should be block_rel_distance_eq_rel_hamming_dist_of_k_eq_i).
• Line 135: Hypothesis h_dec violates naming conventions for terms. "Functions and Terms: lowerCamelCase." (Should be hDec).
• Line 172: lemma relHammingDist_le_blockRelDistance lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 178: lemma relHammingDist_le_blockRelDistance violates naming conventions for theorems. "Theorems and Proofs: snake_case."
• Line 188: lemma listBlock_subset_listHamming lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 194: lemma listBlock_subset_listHamming violates naming conventions for theorems. "Theorems and Proofs: snake_case."

ArkLib/ProofSystem/Whir/Folding.lean

• Line 117: lemma fold_f_g lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 215: theorem folding_listdecoding_if_genMutualCorrAgreement lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 222: theorem folding_listdecoding_if_genMutualCorrAgreement violates naming conventions for theorems. "Theorems and Proofs: snake_case."
• Line 235: fun j => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 258: lemma folding_preserves_listdecoding_base lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 273: fun _ : Fin 1 => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."
• Line 290: lemma folding_preserves_listdecoding_bound lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 312: lemma folding_preserves_listdecoding_base_ne_subset lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 331: fun _ : Fin 1 => violates the preferred function syntax. "Prefer fun x ↦ ... over λ x, ...."

ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean

• Line 94: lemma mca_linearCode violates naming conventions for theorems. "Theorems and Proofs: snake_case."
• Line 97: lemma mca_rsc lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 116: theorem mca_johnson_bound_CONJECTURE lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 143: theorem mca_capacity_bound_CONJECTURE lacks a docstring. "Every definition and major theorem should have a docstring."
• Line 188: lemma mca_list_decoding lacks a docstring. "Every definition and major theorem should have a docstring."

ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean

• Line 60: lemma oodSampling_crs_eq_rs lacks a docstring and violates naming conventions for theorems. "Theorems and Proofs: snake_case."
• Line 131: lemma oodSampling_rs_le_bound lacks a docstring and violates naming conventions for theorems. "Theorems and Proofs: snake_case."

ArkLib/ProofSystem/Whir/RBRSoundness.lean

• Line 169: theorem whir_rbr_soundness lacks a docstring. "Every definition and major theorem should have a docstring."

---

📄 **Per-File Summaries**

• ArkLib/ProofSystem/Stir/Combine.lean: Generalize combine_eq_cases by removing the non-zero constraint on φ and update combine_theorem to use the degree parameter dstar consistently.
• ArkLib/ProofSystem/Stir/Folding.lean: Refines proof tactics and updates linter settings for bivariate polynomial lemmas in the STIR folding system.
• ArkLib/ProofSystem/Stir/MainThm.lean: This change simplifies the STIR protocol's soundness theorems by removing redundant DecidableEq requirements and relaxing the distance constraints and non-membership preconditions for the initial codeword.
• ArkLib/ProofSystem/Stir/ProximityGap.lean: Refines the proximity_gap lemma by splitting its hypotheses, adding a positivity requirement for $\delta$, and adjusting the conclusion to allow for distinct codewords for each function index.
• ArkLib/ProofSystem/Stir/Quotienting.lean: Generalize the quotienting lemma by removing the Fintype constraint on the field and simplifying its existential hypothesis through the use of subtype notation.
• ArkLib/ProofSystem/Whir/BlockRelDistance.lean: This update simplifies several lemmas by removing redundant DecidableEq instances and an unnecessary hypothesis on the relative distance parameter.
• ArkLib/ProofSystem/Whir/Folding.lean: Refactor folding and list-decoding lemmas by refining typeclass constraints and moving universal quantifiers for functions and distance bounds outside of probability expressions.
• ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean: This update removes redundant typeclass constraints, such as DecidableEq and Fintype, from several lemmas and theorems in the mutual correlation agreement module.
• ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean: The changes restrict the Fintype F type class constraint to specific lemmas instead of applying it globally to the entire file.
• ArkLib/ProofSystem/Whir/RBRSoundness.lean: Simplifies the WHIR round-by-round soundness theorem by removing redundant DecidableEq constraints and initial code-distance hypotheses.

---

Last updated: 2026-02-27 01:55 UTC.

[alexanderlhicks]

For Folding and subsequently RBRSoundness, this should be replaced by the generic folding (from FRI/follow up) so it's probably ok to leave these out of this PR.
Going to test some changes to the review workflow whilst we're at it.

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2020/654.pdf
https://eprint.iacr.org/2024/1586.pdf
https://eprint.iacr.org/2024/390.pdf
https://eprint.iacr.org/2023/1705.pdf

Internal:
ArkLib/Data/CodingTheory/
ArkLib/Data/Polynomial

Comments:
Please review for correctness with respect to ArkLib internals and the external reference papers (in particular STIR i.e.https://eprint.iacr.org/2024/390.pdf and WHIR i.e. https://eprint.iacr.org/2024/1586.pdf). Identify any possible improvements to the declarations to improve their accuracy and correctness.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:

1. TL;DR

The mathematical reformulation of the STIR/WHIR protocols in this PR is excellent, correctly addressing critical quantifier scoping bugs, edge cases in geometric series evaluations, and initial distance hypotheses. However, the presence of numerous unfinished proofs (sorry) and a few incomplete variable/typeclass cleanups require attention before this can be merged into the main branch.

2. Checklist Coverage

• ✅ Correlated Agreement / Proximity Gap (Quantifier Order): Addressed correctly. The statement in ProximityGap.lean now properly asserts ∀ i, ∃ u rather than the overly restrictive ∃ u, ∀ i, accurately reflecting that each function can agree with a potentially different codeword.
• ✅ Round-by-Round Soundness (Initial Distance Hypotheses): Addressed correctly. The explicit h_not_code and explicit distance bounds have been successfully removed from both stir_rbr_soundness and whir_rbr_soundness.
• ✅ Geometric Series Evaluation in Degree Correction: Addressed correctly. Combine.lean cleanly removes the restrictive φ_neq_0 assumption and handles the $q = \phi(x) \cdot r = 0$ mathematical edge case explicitly, correctly evaluating the geometric sum to $1$.
• ✅ Target Degree Consistency: Addressed correctly. The combine_theorem now appropriately uses dstar ($d^*$) and references the proximity bounds via rate (code φ dstar).
• ✅ Finiteness of Fields for Uniform Probability Measures: Addressed correctly. The global [Fintype F] assumptions were stripped out of files evaluating deterministic polynomials (e.g., Quotienting.lean) and precisely restricted to contexts defining uniform probability measures (e.g., Folding.lean, OutofDomainSmpl.lean, MutualCorrAgreement.lean).

3. Critical Misformalizations

None introduced. In fact, this PR successfully resolves a critical existing misformalization: in Whir/Folding.lean, the universal quantifier ∀ f and its bound implications were correctly extracted from inside the probability measure bounds Pr_{...} to the outside. This mathematically fixes the theorems to accurately evaluate the probability of error over random challenges for an arbitrary, fixed function $f$, rather than evaluating the probability of a universal statement.

4. Key Lean 4 / Mathlib Issues

• Unfinished Proofs (sorry) [Hard Rule Triggered] (Affects 10 files)
  Almost all modified theorem signatures in this PR end in := by sorry. Per the repository's strict formalization guidelines, any pull request containing sorry or admit bypasses the theorem prover and cannot be merged. Affected files: Stir/Combine.lean, Stir/Folding.lean, Stir/MainThm.lean, Stir/ProximityGap.lean, Stir/Quotienting.lean, Whir/BlockRelDistance.lean, Whir/Folding.lean, Whir/MutualCorrAgreement.lean, Whir/OutofDomainSmpl.lean, and Whir/RBRSoundness.lean.
• Incomplete Variable & Typeclass Cleanup (Affects 4 files)
  While the broad removal of unneeded hypotheses and typeclasses was excellent, it left behind several orphaned or shadowed variables:
  • Whir/RBRSoundness.lean: Removing h_not_code left σ₀, δ, d, and dstar unused or locally shadowed in the signature of whir_rbr_soundness.
  • Stir/Quotienting.lean: The parameter (r : F) is completely unused in quotienting and should be dropped.
  • Whir/BlockRelDistance.lean: [DecidableEq (indexPowT S φ i)] was correctly removed from several lemmas, but was missed in listBlock_subset_listHamming and listBlockRelDistance.
  • Whir/MutualCorrAgreement.lean: Redundant [Fintype ι] [Nonempty ι] and [Fintype parℓ] typeclasses remain in proximityListDecodingCondition despite being satisfied by the file-level variable block.
• Unknown Linter Option (Affects Stir/Folding.lean)
  The line set_option linter.flexible false is introduced before degree_bound_bivariate. linter.flexible is not a standard Lean 4 or Mathlib linter. Unless defined locally in the ArkLib project, this will trigger an unknown option warning/error.
• Fragile Proof Patterns & Implicit Coercions (Affects 3 files)
  • Stir/Combine.lean: The proof of combine_eq_cases uses anonymous have : ... hypotheses paired with .elim passing to False. This is fragile; it is highly recommended to explicitly name hypotheses and use the contradiction tactic.
  • Stir/ProximityGap.lean & Whir/Folding.lean: Inequalities mixing ℕ and ℝ≥0 (or ℝ≥0 and ℝ) rely heavily on implicit elaborator coercions (e.g., S.card ≥ (1 - δ) * ...). While it currently parses, be aware that you will likely need to make these coercions explicit (e.g., (S.card : ℝ≥0)) to avoid motive errors when you actually finish these proofs.

5. Overall Verdict

Changes Requested

---

📄 **Review for `ArkLib/ProofSystem/Stir/Combine.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order) [Critical]: ⚠️ Cannot be determined from this diff. The definition of correlated agreement is located in ProximityGap.lean, which is outside the scope of the provided changes.
• Round-by-Round Soundness (Initial Distance Hypotheses) [Major]: ⚠️ Cannot be determined from this diff. The changes targeting this item are located in MainThm.lean and RBRSoundness.lean.
• Geometric Series Evaluation in Degree Correction (Combine) [Major]: ✅ Satisfied. The restrictive φ_neq_0 assumption was cleanly removed from combine_eq_cases. The mathematical edge case $q = \phi(x) \cdot r = 0$ is explicitly handled by the new by_cases hq0 : φ x * r = 0 branch, and the geometric sum natively and correctly evaluates to $1$ via the simp [hq0] call.
• Target Degree Consistency in Combine Theorem [Minor]: ✅ Satisfied. The generic degree parameter has been fully replaced with the target degree dstar ($d^*$) in the declaration of combine_theorem. The proximity bounds correctly reference rate (code φ dstar).
• Finiteness of Fields for Uniform Probability Measures [Minor]: ✅ Satisfied within the scope of this file. The combine_eq_cases lemma cleanly omits [Fintype F] as it is purely algebraic, while combine_theorem correctly inherits the file-level [Fintype F] variable needed for the probability distribution.

Critical Misformalizations:
None.

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): The declaration for combine_theorem concludes with := by sorry. Per the formalization review guidelines, any pull request containing sorry or admit must be flagged for changes prior to merge.

Nitpicks:

• Fragile usage of this: In the proof of combine_eq_cases, you introduce a hypothesis anonymously via have : r' ≠ 1 := by ... and consume it immediately via simp [this]. Relying on the implicitly named this is fragile because it can easily be shadowed by subsequent lines if the proof evolves. It is more idiomatic to explicitly name it, e.g., have hr_neq_one : r' ≠ 1 := by ... followed by simp [hr_neq_one].
• Extraneous .elim syntax: In the line exact (hq0 h0).elim, you are passing the resulting False term to False.elim manually. The idiomatic way to handle this in Lean 4 is to simply use the contradiction tactic, or if you prefer term mode, exact False.elim (hq0 h0).

📄 **Review for `ArkLib/ProofSystem/Stir/Folding.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order) [Critical]: ⚠️ Not applicable. This checklist item concerns mathematical statements in ProximityGap.lean or MutualCorrAgreement.lean and is outside the scope of the provided diff.
• Round-by-Round Soundness (Initial Distance Hypotheses) [Major]: ⚠️ Not applicable. This applies to the RBRSoundness modules, which are not modified in this diff.
• Geometric Series Evaluation in Degree Correction (Combine) [Major]: ⚠️ Not applicable. This applies to Combine.lean.
• Target Degree Consistency in Combine Theorem [Minor]: ⚠️ Not applicable. This applies to Combine.lean.
• Finiteness of Fields for Uniform Probability Measures [Minor]: ⚠️ Not applicable. The [Fintype F] typeclass is already present in the global context of Folding.lean and remains completely unmodified by this diff.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Hard Rule Triggered (sorry): Although not introduced by the newly added lines, the PR contains sorry (visible directly in the diff context at line 143, and elsewhere in the global context). Per the strict reviewer guidelines, any PR containing sorry or admit MUST receive a "Changes Requested" verdict.
• Unknown Linter Option: The diff introduces set_option linter.flexible false in right before degree_bound_bivariate. There is no standard linter.flexible option in standard Lean 4 or Mathlib. Unless this is a custom linter specifically defined within the ArkLib project itself, this will trigger an "unknown option" warning or error. Please verify the exact name of the linter you are trying to disable.

Nitpicks:
None

📄 **Review for `ArkLib/ProofSystem/Stir/MainThm.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order): ⚠️ Not evaluated (not touched by this specific diff).
• Round-by-Round Soundness (Initial Distance Hypotheses): ✅ The diff successfully removes the explicitly supplied h_not_code ($f_0 \notin C_0$) and the constraint Dist.δ 0 ≤ δᵣ(f₀, (Codes.C 0)) from the hypotheses of stir_rbr_soundness, directly reflecting the Spec Analyst's requirement.
• Geometric Series Evaluation in Degree Correction (Combine): ⚠️ Not evaluated (not touched by this diff).
• Target Degree Consistency in Combine Theorem: ⚠️ Not evaluated (not touched by this diff).
• Finiteness of Fields for Uniform Probability Measures: ⚠️ The specific scoping of [Fintype F] is not explicitly altered in this diff, though it correctly remains at the namespace level. The removal of the overly strict [DecidableEq ι] across the namespace and stir_main is a great cleanup.

Critical Misformalizations:
None.

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): Per the instructions, any PR containing sorry or admit must be flagged. Both stir_main and stir_rbr_soundness currently end in sorry, which bypasses the theorem prover. These proofs must be completed (or temporarily stubbed with sorry only during drafting stages not intended for a final merge).

Nitpicks:
None. The removal of the duplicate φ : (i : Fin (M + 1)) → (ι i ↪ F) from stir_rbr_soundness was a great catch!

📄 **Review for `ArkLib/ProofSystem/Stir/ProximityGap.lean`**

Verdict: Changes Requested

Checklist Verification:

• ✅ Correlated Agreement / Proximity Gap (Quantifier Order): The diff correctly updates the quantifier order in the conclusion of proximity_gap. By changing ∃ u, ∀ i to ∀ i, ∃ u, it accurately reflects the mathematical definition that each function $f_i$ agrees with a potentially different codeword $u_i$ on the shared set $S$.
• ⚠️ Round-by-Round Soundness (Initial Distance Hypotheses): Not applicable / Not present in the provided diff (handled in Stir/MainThm.lean / Whir/RBRSoundness.lean).
• ⚠️ Geometric Series Evaluation in Degree Correction (Combine): Not applicable / Not present in the provided diff (handled in Stir/Combine.lean).
• ⚠️ Target Degree Consistency in Combine Theorem: Not applicable / Not present in the provided diff (handled in Stir/Combine.lean).
• ✅ Finiteness of Fields for Uniform Probability Measures: The typeclass [Fintype F] is correctly included in the variable assumptions for proximity_gap, which is mathematically required to construct a uniform probability measure over $\mathbb{F}$ via $ᵖ F.

Critical Misformalizations:

• None. The mathematical reformulation of the hypotheses (replacing the awkward nested ∀ which quantified over an already-bound f) and the correction of the quantifier order in the conclusion accurately reflect the definition of correlated agreement.

Lean 4 / Mathlib Issues:

• Unfinished Proof (sorry): The proof for proximity_gap ends with sorry. Per the repository's strict review guidelines, any PR containing sorry or admit must receive a "Changes Requested" verdict. The proof needs to be completed before this can be merged.

Nitpicks:

• Variable Naming Convention: GenFun uses UpperCamelCase. Standard Lean 4 and Mathlib practice dictates camelCase for variables and function parameters. Consider renaming it to genFun.
• Coercion Clarity: The inequality S.card ≥ (1 - δ) * (Fintype.card ι) implicitly coerces S.card (ℕ) and Fintype.card ι (ℕ) to ℝ≥0 so that they can be multiplied by (1 - δ) : ℝ≥0. While Lean 4's elaborator usually manages this, it is idiomatic and less fragile to write explicit coercions when mixing ℕ and ℝ≥0 in inequalities. Consider mirroring the style used in MutualCorrAgreement.lean: (S.card : ℝ≥0) ≥ (1 - δ) * (Fintype.card ι).

📄 **Review for `ArkLib/ProofSystem/Stir/Quotienting.lean`**

Verdict: Changes Requested

Checklist Verification:

• Finiteness of Fields for Uniform Probability Measures [Minor]: ✅ Verified. The removal of [Fintype F] from the variable block in Quotienting.lean correctly restricts the scope of the finiteness requirement. None of the definitions or lemmas in this file sample from a uniform probability distribution over F. Mathlib's polynomial constructions and evaluations natively work over any [Field F], making the removal of [Fintype F] mathematically correct and optimal for generality.
• (Note: The other checklist items do not apply directly to the changes within Quotienting.lean).

Critical Misformalizations:
None. The modifications to the lemma statement maintain mathematical correctness while improving ergonomics.

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): The quotienting lemma contains a sorry. Per the strict review guidelines, any PR containing unfinished proofs MUST receive a "Changes Requested" verdict. (Note: While this is a pre-existing issue, it is visible in the diff context and triggers the Hard Rule).

Nitpicks:

• Unused Parameter: In lemma quotienting, the parameter (r : F) is declared but completely unused in the hypotheses and the conclusion of the statement. It is likely a leftover from a previous iteration and should be removed.
• Great Refactor: Replacing ∃ (x : S) (hx : x.val ∈ S), ... Ans ⟨x.val, hx⟩ with ∃ x : S, ... Ans x is a fantastic idiomatic cleanup. Since x is already a subtype (x : S), it intrinsically carries the proof that it belongs to S. Avoiding the destructuring and manual reconstruction of the subtype cleans up the theorem statement significantly.
• Typeclass Cleanup: Removing the redundant [DecidableEq F] from the quotienting lemma is correct, as it is already declared in the file's variable block.

📄 **Review for `ArkLib/ProofSystem/Whir/BlockRelDistance.lean`**

Verdict: Changes Requested

Checklist Verification:

• ⚠️ Correlated Agreement / Proximity Gap (Quantifier Order): Not applicable to this diff (addressed in Combine.lean / ProximityGap.lean).
• ⚠️ Round-by-Round Soundness (Initial Distance Hypotheses): Not applicable to this diff (addressed in RBRSoundness.lean / MainThm.lean).
• ⚠️ Geometric Series Evaluation in Degree Correction (Combine): Not applicable to this diff.
• ⚠️ Target Degree Consistency in Combine Theorem: Not applicable to this diff.
• ⚠️ Finiteness of Fields for Uniform Probability Measures: Not applicable to this diff ([Fintype F] scope is not altered here, nor are probability measures evaluated in this file).

Critical Misformalizations:
None. Mathematically, the removal of the hypothesis (hδLe : δ ≤ 1) from listBlock_subset_listHamming is correct. The lemma asserts an inclusion of sets based on a distance threshold. Since the block relative distance is strictly an upper bound for the relative Hamming distance (δᵣ(f, u) ≤ Δᵣ(i, k, f, S', φ', u)), any u with Δᵣ(...) ≤ δ automatically satisfies δᵣ(...) ≤ δ by simple transitivity. This holds algebraically for any δ : ℝ≥0 and does not mathematically require δ ≤ 1.

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): The lemmas blockRelDistance_eq_relHammingDist_of_k_eq_i and relHammingDist_le_blockRelDistance contain sorry. Per repository rules, any PR containing sorry or admit must receive a "Changes Requested" verdict.
• Incomplete Typeclass Cleanup: The diff correctly removes [DecidableEq (indexPowT S φ i)] from blockRelDistance_eq_relHammingDist_of_k_eq_i and relHammingDist_le_blockRelDistance. This is the right move because indexPowT S φ i is a Subtype of F, and F already has [DecidableEq F]. Lean automatically derives DecidableEq for subtypes if the base type has it. However, the author missed a few spots: [DecidableEq (indexPowT S φ i)] is still present in the signature of listBlock_subset_listHamming and listBlockRelDistance (in the unedited portions of the file). These should be removed globally across the file to prevent duplicate/overlapping instance resolution.

Nitpicks:

• The inline comment -- This now works. in blockRelDistance_eq_relHammingDist_of_k_eq_i appears to be leftover debugging scratchpad text from when Finset.univ was failing to resolve properly. It should be removed for codebase cleanliness.

📄 **Review for `ArkLib/ProofSystem/Whir/Folding.lean`**

Verdict: Changes Requested

Checklist Verification:

• ⚠️ Correlated Agreement / Proximity Gap (Quantifier Order) [Critical]: Not directly applicable to this file (pertains to ProximityGap.lean). However, a structurally identical and mathematically critical quantifier scoping bug was correctly fixed in this file! The universal quantifier ∀ f and its bound implications were correctly moved outside of the Pr_{...} probability bounds across multiple theorems.
• ⚠️ Round-by-Round Soundness (Initial Distance Hypotheses) [Major]: Not applicable to Folding.lean.
• ⚠️ Geometric Series Evaluation in Degree Correction (Combine) [Major]: Not applicable to Folding.lean.
• ⚠️ Target Degree Consistency in Combine Theorem [Minor]: Not applicable to Folding.lean.
• ✅ Finiteness of Fields for Uniform Probability Measures [Minor]: Verified. The global [Fintype F] variable was correctly removed. The typeclass is now strictly applied to contexts defining a uniform probability distribution over $\mathbb{F}$ (e.g., folding_listdecoding_if_genMutualCorrAgreement, folding_preserves_listdecoding_base), while intentionally and correctly omitted in purely deterministic contexts like folding_preserves_listdecoding_bound which only evaluate a standard ∀ α : F.

Critical Misformalizations:

• None found in the diff. The PR correctly resolves a major mathematical misformalization by pulling the universal quantifier ∀ f and the distance assumption hδ outside the probability measure Pr_{...}. Previously, the statements were bounding the probability that "for all $f$, if distance holds, then error," which incorrectly evaluates the probability over the universal statement. The new statements accurately evaluate the probability of error over the random folding challenges for an arbitrary, fixed function $f$.

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): Per the formalization rules, any PR containing sorry or admit MUST be flagged for changes. The theorems modified in this diff (folding_listdecoding_if_genMutualCorrAgreement, folding_preserves_listdecoding_base, folding_preserves_listdecoding_bound, and folding_preserves_listdecoding_base_ne_subset) all end with := by sorry. The formal proofs must be provided before this can be approved and merged.
• Implicit Coercion to Real (Potential Pitfall): In folding_listdecoding_if_genMutualCorrAgreement, the bound uses params.errStar ... δ. errStar is typed to take ℝ but δ is ℝ≥0. While Lean 4 handles this via automatic implicit coercion (↑δ), be aware that if you encounter matching issues or motive errors during the actual proof (especially when rewriting sums or inequalities), you may need to make the coercion explicit as (δ : ℝ).

Nitpicks:

• Naming Conventions: In folding_preserves_listdecoding_base, the distance hypothesis was renamed to hδ from hδLe, but the older naming convention might still be lingering in other files. It's good practice to align these across the codebase (e.g., standardizing on hδ).

📄 **Review for `ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order) [Critical]: ⚠️ Not applicable to this diff (relevant to STIR's Combine.lean and ProximityGap.lean).
• Round-by-Round Soundness (Initial Distance Hypotheses) [Major]: ⚠️ Not applicable to this diff.
• Geometric Series Evaluation in Degree Correction (Combine) [Major]: ⚠️ Not applicable to this diff.
• Target Degree Consistency in Combine Theorem [Minor]: ⚠️ Not applicable to this diff.
• Finiteness of Fields for Uniform Probability Measures [Minor]: ✅ Verified. The scoping of typeclasses is handled properly. [Fintype F] is securely maintained in the global variable block at the top of the file, which guarantees mathematically that the uniform probability measures implicitly defining distribution over the field (e.g., Pr_{let r ←$ᵖ Gen.Gen}[...]) are soundly defined over a finite space.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Unfinished Proofs (sorry): The diff modifies the signatures of mca_rsc, mca_johnson_bound_CONJECTURE, mca_capacity_bound_CONJECTURE, and mca_list_decoding. However, all of these declarations still end with := by sorry. As per the strict reviewer rules, any PR containing sorry or admit MUST be flagged with a "Changes Requested" verdict to prevent unfinished proofs from entering the main codebase.

Nitpicks:

• Incomplete Typeclass Cleanup: The diff appropriately drops [Fintype ι] [Nonempty ι] from mca_list_decoding because they are redundant—already provided by the file-level variable block. However, it missed cleaning up those exact same redundant typeclasses in proximityListDecodingCondition located immediately above it. Consider removing the explicit [Fintype ι] [Nonempty ι] and [Fintype parℓ] from proximityListDecodingCondition as well to prevent shadowing and unnecessary binder clutter.
• Removal of [DecidableEq ι]: The removal of [DecidableEq ι] from the theorems is mathematically sound and an excellent cleanup. Abstract evaluation domains do not inherently require decidable equality unless pointwise evaluations are actively compared inside the proof structure. Assuming this successfully compiles with RSGenerator.genRSC, this is an idiomatic improvement.

📄 **Review for `ArkLib/ProofSystem/Whir/OutofDomainSmpl.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order): ⚠️ Not applicable to this file.
• Round-by-Round Soundness (Initial Distance Hypotheses): ⚠️ Not applicable to this file.
• Geometric Series Evaluation in Degree Correction (Combine): ⚠️ Not applicable to this file.
• Target Degree Consistency in Combine Theorem: ⚠️ Not applicable to this file.
• Finiteness of Fields for Uniform Probability Measures: ✅ The diff accurately removes the global [Fintype F] typeclass and appropriately scopes it locally to oodSampling_crs_eq_rs and oodSampling_rs_le_bound. The lemma crs_equiv_rs_random_point_agreement expresses a mathematical equivalence of points in a code and does not involve uniform probability distributions over $\mathbb{F}$ nor compute the field's cardinality. This means the finite field restriction was correctly and safely removed from the global scope.

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• The modified lemma oodSampling_rs_le_bound ends with an incomplete proof (sorry). As per the project's hard rules, any PR containing sorry or admit must receive a "Changes Requested" verdict to flag unfinished formalization.

Nitpicks:
None

📄 **Review for `ArkLib/ProofSystem/Whir/RBRSoundness.lean`**

Verdict: Changes Requested

Checklist Verification:

• Correlated Agreement / Proximity Gap (Quantifier Order) [Critical]: ⚠️ Not applicable to this diff (pertains to STIR proximity gap files).
• Round-by-Round Soundness (Initial Distance Hypotheses) [Major]: ❌ Partially addressed. The PR successfully removes the h_not_code and hδ₀Lt hypotheses from whir_rbr_soundness in ArkLib/ProofSystem/Whir/RBRSoundness.lean (which is mathematically correct, as the IsSecureWithGap relation implicitly defines the threshold for soundness internally without demanding that the protocol assumes all initial functions are outside the code). However, examining the global context, the corresponding hypotheses (h_not_code and hδ₀Le) have not been removed from stir_rbr_soundness in ArkLib/ProofSystem/Stir/MainThm.lean. The PR is incomplete regarding this checklist item.
• Geometric Series Evaluation in Degree Correction (Combine) [Major]: ⚠️ Not applicable to this diff.
• Target Degree Consistency in Combine Theorem [Minor]: ⚠️ Not applicable to this diff.
• Finiteness of Fields for Uniform Probability Measures [Minor]: ⚠️ Not applicable to this diff.

Critical Misformalizations:

• None introduced in the diff. Removing the global universal quantification ∀ f_0 over distance bounds is a mathematically correct and necessary fix to properly state the existence of a uniform protocol $\pi$.

Lean 4 / Mathlib Issues:

• Unused Variables Left Behind: By removing h_not_code and hδ₀Lt, the parameter {σ₀ : F} is now completely orphaned and unused in the signature of whir_rbr_soundness. Additionally, the parameter {δ : ℝ≥0} was already unused. Furthermore, {d dstar : ℕ} are declared as implicit variables at the very top of the theorem but are entirely shadowed by let dstar := ... and let d := ... inside the theorem's existential body. All four of these variables (σ₀, δ, d, dstar) should be removed from the parameter list to prevent compilation warnings and reader confusion.
• Hard Rule (sorry Usage): The whir_rbr_soundness theorem currently evaluates to := by sorry. Although this was pre-existing and not introduced by the diff, any PR containing unfinished proofs mandates a "Changes Requested" verdict.

Nitpicks:

• The removal of the [∀ i : Fin (M + 1), DecidableEq (ι i)] typeclass from the variable block is an excellent cleanup! Operations on indexPowT yield a subtype of F and therefore only inherently require DecidableEq F. Similarly, Code.relHammingDist computes distances by iterating over Fintype elements and determining equality of the outputs in F, removing any strict requirement for decidable equality on the evaluation domains themselves.

[alexanderlhicks]

/review

External:
https://eprint.iacr.org/2020/654.pdf
https://eprint.iacr.org/2024/1586.pdf
https://eprint.iacr.org/2024/390.pdf
https://eprint.iacr.org/2023/1705.pdf

Internal:
ArkLib/Data/CodingTheory/
ArkLib/Data/Polynomial

Comments:
Please review for correctness with respect to ArkLib internals and the external reference papers (in particular STIR i.e.https://eprint.iacr.org/2024/390.pdf and WHIR i.e. https://eprint.iacr.org/2024/1586.pdf). Identify any possible improvements to the declarations to improve their accuracy and correctness.