feat: 4.24 update and VCV upstream changes

[dtumad]

Combined updates to 4.24 and changes needed for recent VCV changes.

WIP do not merge. Also need to change lakefile before merging once upstream PR merges

[github-actions]

🤖 Gemini PR Summary

This diff represents a significant refactoring of the ArkLib library, driven by an upgrade of the Lean toolchain and its dependencies, particularly the VCV-io cryptography library.

The key changes and their purposes are:

• Migration to a New Oracle Abstraction: The core of the refactoring is the replacement of the custom OracleInterface typeclass with the more structured OracleContext from VCV-io. This modernizes how oracles are defined, implemented, and composed throughout the project.

  • The syntax for defining and combining oracle specifications has changed (e.g., ++ₒ is replaced by +).
  • Implementations of provers, verifiers, and commitment schemes are updated to use this new abstraction.
  • Many security proofs and composition logics for oracle reductions are now commented out or marked with sorry, indicating this is a work-in-progress migration.

• API and Type Signature Updates:

  • SelectableType has been consistently replaced with SampleableType, aligning with changes in the underlying probability framework.
  • Verifier functions now return an OptionT, making potential failures explicit in the type signature rather than using implicit failure mechanisms.

• New Feature: Proximity Gaps for Reed-Solomon Codes: A substantial new file, ProximityGap.lean, has been added. This introduces definitions and theorems formalizing the concept of proximity gaps for error-correcting codes, based on the [BCIKS20] paper.

• Dependency-Related Maintenance: A large number of smaller changes across the codebase fix proofs and update syntax to be compatible with the new versions of mathlib and other libraries. This includes minor proof adjustments, tactic changes, and dependency path updates.

---

Analysis of Changes

Metric	Count
📝 Files Changed	96
✅ Lines Added	5898
❌ Lines Removed	4972

---

sorry Tracking

• ✅ Removed: 48 sorry(s)
  • theorem knowledgeSoundness_implies_soundness (relIn : Set (StmtIn × WitIn)) in ArkLib/OracleReduction/Security/Implications.lean
  • def squeezeUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : in ArkLib/Data/Hash/DuplexSponge.lean
  • def Extractor.RoundByRound.liftContext in ArkLib/OracleReduction/LiftContext/Reduction.lean
  • theorem simulateQ'_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) in ArkLib/ToVCVio/SimOracle.lean
  • theorem oracleReduction_completeness (h : init.neverFails) : in ArkLib/ProofSystem/Component/CheckClaim.lean
  • theorem srSoundness_addSalt_implies_srSoundness_original in ArkLib/OracleReduction/Security/Implications.lean
  • theorem challengeOracleInterface_cast {h : n₁ = n₂} {hSpec : pSpec₁.cast h = pSpec₂} in ArkLib/OracleReduction/ProtocolSpec/Cast.lean
  • def oracleVerifier : OracleVerifier oSpec Statement OStatement Unit (OStatement ⊕ᵥ OStatement) in ArkLib/ProofSystem/Component/SendClaim.lean
  • def StateFunction.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • def OracleVerifier.addSalt (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : in ArkLib/OracleReduction/Salt.lean
  • theorem reduction_completeness {ε : ℝ≥0} in ArkLib/ProofSystem/Component/NoInteraction.lean
  • def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop in ArkLib/CommitmentScheme/Basic.lean
  • theorem append_soundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem append_knowledgeSoundness (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • def ratchetUnchecked [Permute C] (sponge : DuplexSponge U C) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
  • theorem srKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/OracleReduction/Security/Implications.lean
  • theorem verifier_rbr_knowledge_soundness : in ArkLib/ProofSystem/Component/CheckClaim.lean
  • theorem cast_processRound (j : Fin n₁) in ArkLib/OracleReduction/Cast.lean
  • theorem cast_id : in ArkLib/OracleReduction/Cast.lean
  • theorem append_run (stmt : Stmt₁) (wit : Wit₁) : in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem rbrKnowledgeSoundness_implies_rbrSoundness in ArkLib/OracleReduction/Security/Implications.lean
  • theorem oracleReduction_rbr_knowledge_soundness : True in ArkLib/ProofSystem/Component/CheckClaim.lean
  • def RoundByRound.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem cast_runToRound (j : Fin (n₁ + 1)) (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Cast.lean
  • theorem OracleReduction.liftContext_toReduction_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
  • theorem seqCompose_rbrSoundness in ArkLib/OracleReduction/Composition/Sequential/General.lean
  • theorem append_completeness (R₁ : Reduction oSpec Stmt₁ Wit₁ Stmt₂ Wit₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem rbrSoundness_implies_soundness (langIn : Set StmtIn) (langOut : Set StmtOut) in ArkLib/OracleReduction/Security/Implications.lean
  • def absorbUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
  • theorem cast_toVerifier (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₁) : in ArkLib/OracleReduction/Cast.lean
  • theorem cast_rbrKnowledgeSoundness (ε : pSpec₁.ChallengeIdx → ℝ≥0) in ArkLib/OracleReduction/Cast.lean
  • def OracleVerifier.append (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem append_rbrSoundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem append_rbrKnowledgeSoundness in ArkLib/OracleReduction/Composition/Sequential/Append.lean
  • theorem OracleVerifier.liftContext_toVerifier_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
  • def numQueries (stmt : StmtIn) (challenges : ∀ i, pSpec.Challenge i) in ArkLib/OracleReduction/Basic.lean
  • theorem fiatShamir_completeness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) in ArkLib/OracleReduction/FiatShamir/Basic.lean
  • theorem completeness : (oracleReduction oSpec Statement OStatement relComp).perfectCompleteness in ArkLib/ProofSystem/Component/SendClaim.lean
  • theorem oracleReduction_rbr_knowledge_soundness : True in ArkLib/ProofSystem/Component/SendWitness.lean
  • theorem cast_completeness (ε : ℝ≥0) (hComplete : R.completeness init impl relIn relOut ε) : in ArkLib/OracleReduction/Cast.lean
  • theorem Reduction.run_of_prover_first [ProverOnly pSpec] (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
  • theorem seqCompose_rbrKnowledgeSoundness in ArkLib/OracleReduction/Composition/Sequential/General.lean
  • theorem Verifier.id_knowledgeSoundness {rel : Set (StmtIn × WitIn)} : in ArkLib/OracleReduction/Security/Basic.lean
  • theorem srKnowledgeSoundness_addSalt_implies_srKnowledgeSoundness_original in ArkLib/OracleReduction/Security/Implications.lean
  • theorem srSoundness_implies_soundness in ArkLib/OracleReduction/Security/Implications.lean
  • theorem cast_run (stmt : StmtIn) (wit : WitIn) : in ArkLib/OracleReduction/Cast.lean
  • theorem rbrKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/OracleReduction/Security/Implications.lean
  • lemma OracleVerifier.append_toVerifier in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• ❌ Added: 26 sorry(s)
  • def foldVerifierOStmtOutSpec : OracleSpec in ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
  • lemma matching_set_is_a_sub_of_coeffs_of_close_proximity in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} : in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma exists_a_set_and_a_matching_polynomial in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma irreducible_H in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma approximate_solution_is_exact_solution_coeffs in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem correlatedAgreement_affine_curves [DecidableEq ι] {k : ℕ} {u : Fin k → ι → F} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem correlatedAgreement_affine_spaces {k : ℕ} [NeZero k] {u : Fin (k + 1) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma modified_guruswami_has_a_solution in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma irreducible_factorization_of_gs_solution in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma gamma_eq_P in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def ofVerify (vrf : (stmtIn : StmtIn) → (challenges : pSpec.Challenges) → in ArkLib/OracleReduction/Basic.lean
  • lemma solution_gamma_is_linear_in_Z in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def commitmentScheme : Commitment.Scheme (oSpec α β γ) α β γ sorry !p[] where in ArkLib/CommitmentScheme/SimpleRO.lean
  • lemma approximate_solution_is_exact_solution_coeffs' in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def OracleVerifier.liftContext in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
  • lemma solution_gamma_matches_word_if_subset_large in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem correlatedAgreement_lines {u : Fin 2 → ι → F} {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma OracleVerifier.id_rbrKnowledgeSoundness in ArkLib/OracleReduction/Security/RoundByRound.lean
  • lemma discr_of_irred_components_nonzero in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def OracleVerifier.run in ArkLib/OracleReduction/Execution.lean
  • lemma exists_factors_with_large_common_root_set in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def Reduction.runWithLog (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
  • lemma exists_points_with_large_matching_subset in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem proximity_gap_RSCodes {k t : ℕ} [NeZero k] [NeZero t] {deg : ℕ} {domain : ι ↪ F} in ArkLib/Data/CodingTheory/ProximityGap.lean
• ✏️ Affected: 1 sorry(s) (line number changed)
  • theorem matchSize_eq_iff_forall_eq (l₁ l₂ : List α) (unit : α) : in ArkLib/Data/List/Lemmas.lean moved from L170 to L171

---

Last updated: 2025-12-17 16:08 UTC. See the main CI run for build status.

[quangvdao]

@dtumad I'm going to base my OracleReduction refactor on top of this branch as well

[dtumad]

@quangvdao This is the basic approach I'm using as a replacement for interfaces (and not making them a type-class). Feels maybe overkill to be using reader monads and things for stuff like this but I think it might be useful long term to allow any monad.

[quangvdao]

I think this is fine. Since this is no longer an instance the name should change to "polynomialOracleCtxt" or something

[quangvdao]

I'm not sure what is standard terminology for this. People just call this "(univariate) polynomial oracle"

[alexanderlhicks]

@dtumad what's the status re: the oracle stuff we looked at during the last arklib meeting?

[github-actions]

🤖 Gemini PR Summary

This pull request is a significant infrastructure update aimed at migrating the codebase to Lean 4.24.0 and aligning with major upstream architectural changes in the VCV (Verifiable Computation and Verification) library.

Note: This is a Work-In-Progress (WIP). Several core modules (including Fiat-Shamir transformations and sequential compositions) have been temporarily commented out to facilitate the transition to the new oracle framework.

Features

• Toolchain Upgrade: Updated Lean 4 version from v4.22.0 to v4.24.0 across the toolchain and lake-manifest.
• Proximity Gap Formalization: Introduced new definitions and theorem statements for proximity gap properties and correlated agreement in Reed-Solomon codes, based on the BCIKS20 paper.
• Enhanced Tactic Integration: Modernized several proof scripts by adopting newer Lean 4 tactics such as aesop and grind for better stability and automation.

Refactoring

• Oracle Framework Overhaul:
  • Transitioned from the OracleInterface typeclass to a more flexible, monadic OracleContext structure.
  • Updated verification logic across ArkLib to use the OptionT monad for improved error handling and modularity.
  • Replaced the oracle composition operator ++ₒ with the standard + notation.
• Typeclass Renaming: Renamed the SelectableType class to SampleableType throughout the entire library (impacting Binius, STIR, Sumcheck, and FRI implementations) to align with updated VCV conventions.
• Code Simplification & Modernization:
  • Refactored legacy induction' tactics to use standard Lean 4 structured induction syntax.
  • Simplified algebraic proofs by replacing manual steps or field_simp with targeted simp lemmas and subst.
  • Updated bitwise and coding theory proofs for better performance and readability.
• Temporary Deactivations: To support the breaking changes in the oracle API, several modules—including Fiat-Shamir, Salted Protocols, Sequential Composition, and specific Oracle Reductions—have been temporarily commented out or stubbed with placeholders.

Fixes

• API Alignment: Corrected function argument structures (e.g., PowerSeries.coeff) and updated proof labels to match library changes (e.g., renaming right_inv cases to right_neg).
• Namespace & Path Corrections: Updated Mathlib imports (e.g., Hadamard product moving to LinearAlgebra.Matrix) and resolved lemma name ambiguities in ArkLib/Data/Vector/Basic.lean.
• Performance Optimization: Increased heartbeat limits and cleared local contexts in complex bivariate polynomial proofs to prevent timeout issues.

Documentation

• Syntax Corrections: Updated documentation syntax for vsum and vprod definitions.
• Developer Notes: Added internal notes regarding the removal of VCVCompatible and the temporary status of proof placeholders during the version update.

---

Analysis of Changes

Metric	Count
📝 Files Changed	96
✅ Lines Added	5998
❌ Lines Removed	5050

---

sorry Tracking

✅ **Removed:** 49 `sorry`(s)

• def OracleVerifier.append (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem simulateQ'_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) in ArkLib/ToVCVio/SimOracle.lean
• def OracleVerifier.liftContext in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• theorem cast_run (stmt : StmtIn) (wit : WitIn) : in ArkLib/OracleReduction/Cast.lean
• theorem append_knowledgeSoundness (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem OracleReduction.liftContext_toReduction_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• theorem rbrKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/OracleReduction/Security/Implications.lean
• theorem append_completeness (R₁ : Reduction oSpec Stmt₁ Wit₁ Stmt₂ Wit₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem knowledgeSoundness_implies_soundness (relIn : Set (StmtIn × WitIn)) in ArkLib/OracleReduction/Security/Implications.lean
• theorem cast_runToRound (j : Fin (n₁ + 1)) (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Cast.lean
• theorem oracleReduction_rbr_knowledge_soundness : True in ArkLib/ProofSystem/Component/CheckClaim.lean
• theorem Verifier.id_knowledgeSoundness {rel : Set (StmtIn × WitIn)} : in ArkLib/OracleReduction/Security/Basic.lean
• lemma OracleVerifier.append_toVerifier in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• def numQueries (stmt : StmtIn) (challenges : ∀ i, pSpec.Challenge i) in ArkLib/OracleReduction/Basic.lean
• theorem fiatShamir_completeness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) in ArkLib/OracleReduction/FiatShamir/Basic.lean
• theorem Reduction.run_of_prover_first [ProverOnly pSpec] (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
• theorem srKnowledgeSoundness_addSalt_implies_srKnowledgeSoundness_original in ArkLib/OracleReduction/Security/Implications.lean
• def squeezeUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : in ArkLib/Data/Hash/DuplexSponge.lean
• theorem verifier_rbr_knowledge_soundness : in ArkLib/ProofSystem/Component/CheckClaim.lean
• theorem reduction_completeness {ε : ℝ≥0} in ArkLib/ProofSystem/Component/NoInteraction.lean
• theorem srSoundness_addSalt_implies_srSoundness_original in ArkLib/OracleReduction/Security/Implications.lean
• theorem rbrKnowledgeSoundness_implies_rbrSoundness in ArkLib/OracleReduction/Security/Implications.lean
• theorem append_soundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem append_rbrKnowledgeSoundness in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• def oracleVerifier : OracleVerifier oSpec Statement OStatement Unit (OStatement ⊕ᵥ OStatement) in ArkLib/ProofSystem/Component/SendClaim.lean
• theorem append_run (stmt : Stmt₁) (wit : Wit₁) : in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem cast_completeness (ε : ℝ≥0) (hComplete : R.completeness init impl relIn relOut ε) : in ArkLib/OracleReduction/Cast.lean
• def Extractor.RoundByRound.liftContext in ArkLib/OracleReduction/LiftContext/Reduction.lean
• def StateFunction.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem OracleVerifier.liftContext_toVerifier_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• theorem rbrSoundness_implies_soundness (langIn : Set StmtIn) (langOut : Set StmtOut) in ArkLib/OracleReduction/Security/Implications.lean
• theorem cast_id : in ArkLib/OracleReduction/Cast.lean
• theorem cast_toVerifier (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₁) : in ArkLib/OracleReduction/Cast.lean
• def OracleVerifier.addSalt (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : in ArkLib/OracleReduction/Salt.lean
• theorem oracleReduction_completeness (h : init.neverFails) : in ArkLib/ProofSystem/Component/CheckClaim.lean
• def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop in ArkLib/CommitmentScheme/Basic.lean
• theorem append_rbrSoundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem srKnowledgeSoundness_implies_knowledgeSoundness in ArkLib/OracleReduction/Security/Implications.lean
• def ratchetUnchecked [Permute C] (sponge : DuplexSponge U C) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
• theorem completeness : (oracleReduction oSpec Statement OStatement relComp).perfectCompleteness in ArkLib/ProofSystem/Component/SendClaim.lean
• theorem cast_rbrKnowledgeSoundness (ε : pSpec₁.ChallengeIdx → ℝ≥0) in ArkLib/OracleReduction/Cast.lean
• def RoundByRound.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem seqCompose_rbrSoundness in ArkLib/OracleReduction/Composition/Sequential/General.lean
• theorem seqCompose_rbrKnowledgeSoundness in ArkLib/OracleReduction/Composition/Sequential/General.lean
• def absorbUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
• theorem srSoundness_implies_soundness in ArkLib/OracleReduction/Security/Implications.lean
• theorem oracleReduction_rbr_knowledge_soundness : True in ArkLib/ProofSystem/Component/SendWitness.lean
• theorem cast_processRound (j : Fin n₁) in ArkLib/OracleReduction/Cast.lean
• theorem challengeOracleInterface_cast {h : n₁ = n₂} {hSpec : pSpec₁.cast h = pSpec₂} in ArkLib/OracleReduction/ProtocolSpec/Cast.lean

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

• lemma matching_set_is_a_sub_of_coeffs_of_close_proximity in ArkLib/Data/CodingTheory/ProximityGap.lean
• theorem correlatedAgreement_affine_curves [DecidableEq ι] {k : ℕ} {u : Fin k → ι → F} in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma gamma_eq_P in ArkLib/Data/CodingTheory/ProximityGap.lean
• def Reduction.runWithLog (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
• lemma guruswami_sudan_for_proximity_gap_property {k m : ℕ} {ωs : Fin n ↪ F} in ArkLib/Data/CodingTheory/ProximityGap.lean
• def ofVerify (vrf : (stmtIn : StmtIn) → (challenges : pSpec.Challenges) → in ArkLib/OracleReduction/Basic.lean
• theorem proximity_gap_RSCodes {k t : ℕ} [NeZero k] [NeZero t] {deg : ℕ} {domain : ι ↪ F} in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma solution_gamma_is_linear_in_Z in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma modified_guruswami_has_a_solution in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma exists_factors_with_large_common_root_set in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma exists_points_with_large_matching_subset in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma approximate_solution_is_exact_solution_coeffs' in ArkLib/Data/CodingTheory/ProximityGap.lean
• def Verifier.KnowledgeStateFunction.id {rel : Set (StmtIn × WitIn)} : in ArkLib/OracleReduction/Security/RoundByRound.lean
• def OracleVerifier.run in ArkLib/OracleReduction/Execution.lean
• lemma solution_gamma_matches_word_if_subset_large in ArkLib/Data/CodingTheory/ProximityGap.lean
• theorem correlatedAgreement_lines {u : Fin 2 → ι → F} {deg : ℕ} {domain : ι ↪ F} {δ : ℝ≥0} in ArkLib/Data/CodingTheory/ProximityGap.lean
• def Verifier.StateFunction.id {lang : Set StmtIn} : in ArkLib/OracleReduction/Security/RoundByRound.lean
• def foldVerifierOStmtOutSpec : OracleSpec in ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
• def commitmentScheme : Commitment.Scheme (oSpec α β γ) α β γ sorry !p[] where in ArkLib/CommitmentScheme/SimpleRO.lean
• theorem correlatedAgreement_affine_spaces {k : ℕ} [NeZero k] {u : Fin (k + 1) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma irreducible_factorization_of_gs_solution in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma exists_a_set_and_a_matching_polynomial in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma approximate_solution_is_exact_solution_coeffs in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma discr_of_irred_components_nonzero in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma irreducible_H in ArkLib/Data/CodingTheory/ProximityGap.lean
• lemma guruswami_sudan_for_proximity_gap_existence {k m : ℕ} {ωs : Fin n ↪ F} {f : Fin n → F} : in ArkLib/Data/CodingTheory/ProximityGap.lean

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

• theorem matchSize_eq_iff_forall_eq (l₁ l₂ : List α) (unit : α) : in ArkLib/Data/List/Lemmas.lean moved from L170 to L171

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the specific lines that violate the conventions:

ArkLib/Data/CodingTheory/ProximityGap.lean

• Lines 1–50 (Module Header): Violates "Include a References section: Each file that cites papers should have a ## References section in its docstring header." (The file cites [BCIKS20] but lacks the required section).
• Line 34: [BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes" by Eli Ben-Sasson... — Violates "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
• Line 38: Using {https://eprint.iacr.org/2020/654}, version 20210703:203025. — Violates "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."

ArkLib/OracleReduction/Basic.lean

• Line 12: TODO(dtumad): update this in context of 4.24 changes — Violates "ArkLib aims to align closely with the established conventions of the Lean community, particularly those used in mathlib." (Mathlib style guide specifies: "TODOs should be written as TODO: <description>. Do not use TODO(name)").

ArkLib/Data/Classes/DCast.lean

• Line 297: subst h — Violates "ArkLib aims to align closely with the established conventions of the Lean community, particularly those used in mathlib." (Mathlib style guide specifies 2-space indentation; this line uses 4 spaces).

ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BadEvents.lean

• Line 32: /- A query tuple (i, q, r) is redundant... -/ — Violates "ArkLib aims to align closely with the established conventions of the Lean community, particularly those used in mathlib." (Mathlib style guide specifies that docstrings for definitions must use /-- ... -/).

ArkLib/OracleReduction/Execution.lean

• Line 15: namespace loggingOracle — Violates "ArkLib aims to align closely with the established conventions of the Lean community, particularly those used in mathlib." (Mathlib naming conventions specify UpperCamelCase for namespaces).

---

📄 **Per-File Summaries**

• ArkLib.lean: Comment out multiple imports related to oracle reduction composition, Fiat-Shamir transformations, and security modules.
• ArkLib/AGM/Basic.lean: Refactor group oracle definitions and implementations to align with updated OracleSpec and QueryImpl API structures.
• ArkLib/CommitmentScheme/Basic.lean: Update the commitment scheme definitions and security properties to use OracleContext instead of OracleInterface for modeling data evaluation queries and responses.
• ArkLib/CommitmentScheme/InductiveMerkleTree.lean: Refactor the Merkle tree oracle specification to use the hash input as the query index and update the verification logic to use the OptionT monad.
• ArkLib/CommitmentScheme/MerkleTree.lean: Refactors the Merkle tree oracle specification and updates proof verification to use OptionT for better error handling.
• ArkLib/CommitmentScheme/SimpleRO.lean: Refactor the oracle specifications and update the commitment scheme implementation to use revised OracleSpec notation and OptionT for verification.
• ArkLib/Data/Classes/DCast.lean: Update the proof of the cast_eq_dcast theorem for Fin to use subst and revised simplification lemmas.
• ArkLib/Data/CodingTheory/Basic.lean: This commit refines and simplifies several proofs related to Hamming distance and coding theory while introducing a temporary breakpoint in the unique decoding radius proof.
• ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean: Rename a proof case label in the solution_to_BerlekampWelch_condition lemma from right_inv to right_neg.
• ArkLib/Data/CodingTheory/BerlekampWelch/ElocPoly.lean: Refactor induction proofs to use standard Lean 4 structured induction syntax instead of the induction' tactic.
• ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean: This update introduces temporary truncation markers and a proof placeholder within the Johnson bound lemmas.
• ArkLib/Data/CodingTheory/JohnsonBound/Choose2.lean: Simplifies the proof of choose_2_convex by replacing the field_simp tactic with simp.
• ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean: This PR streamlines and modernizes the proofs in the Johnson Bound lemmas by replacing manual algebraic steps with automated tactics like aesop and grind and refining inequality rewrites for better stability.
• ArkLib/Data/CodingTheory/Prelims.lean: Update imports and use open statements to simplify the definitions of matrix row and column spans and ranks.
• ArkLib/Data/CodingTheory/ProximityGap.lean: This file formalizes definitions, main theorem statements, and supporting lemmas for proximity gap properties and correlated agreement in Reed-Solomon codes based on the BCIKS20 paper.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: Removes an unnecessary underscore in a PowerSeries.coeff call within the approximate_solution_is_exact_solution_coeffs' lemma to correct the function's argument structure.
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean: Refactor the cardinality calculation in the card_agreeing_cells_notin_D lemma by simplifying the rewrite steps for finset differences.
• ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean: The changes insert a stop command to truncate a proof for a version update and remove an unnecessary rewrite tactic.
• ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean: Removes the Field typeclass constraint from the prevBTField parameter in the binary_tower_inductive_step definition.
• ArkLib/Data/Fin/Basic.lean: This change simplifies the proof of induction_append_left by removing a redundant rfl tactic from the base case.
• ArkLib/Data/Fin/Sigma.lean: Updated induction case labels in finSigmaFinEquiv' and corrected the documentation syntax for the vsum and vprod definitions.
• ArkLib/Data/Hash/DuplexSponge.lean: Refactors permutation oracle specifications and implementations to remove redundant unit indexing and simplify oracle composition.
• ArkLib/Data/List/Lemmas.lean: Added the Mathlib.Tactic.Cases import and adjusted the formatting of the matchSize_eq_iff_forall_eq theorem.
• ArkLib/Data/Matrix/Basic.lean: Updates the import path for Mathlib's Hadamard product to reflect its relocation to LinearAlgebra.Matrix.
• ArkLib/Data/MlPoly/Basic.lean: Refactor and simplify the proof of forwardRange_0_eq_finRange by using List.ext_get and streamlining the internal logic.
• ArkLib/Data/Nat/Bitwise.lean: This PR refactors and simplifies several bitwise proofs, notably sum_eq_xor_plus_twice_and, while applying general code formatting and style improvements throughout the file.
• ArkLib/Data/Polynomial/Bivariate.lean: Optimizes the degreeX_mul proof by increasing the maximum heartbeat limit and clearing unnecessary hypotheses from the local context to improve performance.
• ArkLib/Data/Polynomial/Frobenius.lean: Replaced the proof of exponent divisibility in X_pow_card_pow_dvd_X_pow_card_pow_of_dvd with a sorry placeholder and a comment suggesting a potential replacement lemma.
• ArkLib/Data/UniPoly/Basic.lean: Updated Array.range to Array.Range within commented-out code segments.
• ArkLib/Data/Vector/Basic.lean: Refines vector property proofs by updating simplification tactics and resolving lemma name ambiguities for better stability.
• ArkLib/OracleReduction/BCS/Basic.lean: Comment out unused variable declarations and a placeholder definition related to the BCS transformation.
• ArkLib/OracleReduction/Basic.lean: Refactors the OracleVerifier and OracleProver structures to use a more generalized OracleContext framework and OptionT-based verification to improve oracle composition and modularity.
• ArkLib/OracleReduction/Cast.lean: Simplify oracle statement types and comment out the casting-related definitions and theorems for oracle verifiers and reductions.
• ArkLib/OracleReduction/Composition/Sequential/Append.lean: Comment out the entire implementation of sequential composition for oracle reductions, provers, and verifiers.
• ArkLib/OracleReduction/Composition/Sequential/General.lean: The changes comment out the definitions and security theorems for the sequential composition of provers, verifiers, and oracle reductions.
• ArkLib/OracleReduction/Execution.lean: Refactors the protocol execution and reduction logic to use generalized oracle specifications and OptionT for failure handling, while temporarily disabling related logging and simulation theorems.
• ArkLib/OracleReduction/FiatShamir/Basic.lean: Comment out the Fiat-Shamir transformation implementation and completeness theorem while refactoring the SelectableType constraint to SampleableType.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Defs.lean: Update the oracle composition syntax by replacing the ++ₒ operator with + throughout the file.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BadEvents.lean: Updates the redundantQuery definition to use the capitalized Domain and Range fields of the OracleSpec.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemma.lean: This change updates the oracle composition syntax by replacing the ++ₒ operator with + across several definitions and lemmas.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/ProverTransform.lean: Updated the oracle composition operator from ++ₒ to + in the duplexSpongeToBasicFSAlgo definition.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/TraceTransform.lean: Update the notation for oracle specification composition in basicToDuplexSpongeFSTrace by replacing the ++ₒ operator with +.
• ArkLib/OracleReduction/LiftContext/Lens.lean: Refactored oracle-related lens definitions and structures to use explicit OracleContext parameters instead of implicit OracleInterface typeclass constraints.
• ArkLib/OracleReduction/LiftContext/OracleReduction.lean: This change comments out the core definitions and theorems for lifting oracle reductions while refactoring variable declarations to use explicit OracleContext parameters.
• ArkLib/OracleReduction/LiftContext/Reduction.lean: Refactor the context lifting logic by updating proof structures, migrating from SelectableType to SampleableType, and temporarily disabling round-by-round extractor lifting.
• ArkLib/OracleReduction/OracleInterface.lean: Refactors the oracle interface framework by replacing the OracleInterface type class with a monadic OracleContext structure to improve integration with the oracle specification system.
• ArkLib/OracleReduction/Prelude.lean: Renames SelectableType to SampleableType within the Sampleable class and adds a note about potentially removing VCVCompatible.
• ArkLib/OracleReduction/ProtocolSpec/Basic.lean: Refactors the protocol specification to use OracleContext instead of OracleInterface for messages and challenges and renames the SelectableType class to SampleableType.
• ArkLib/OracleReduction/ProtocolSpec/Cast.lean: Comment out an OracleInterface instance and a theorem related to protocol specification casting.
• ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean: Updates protocol challenge sampling to use SampleableType and comments out several OracleInterface and SubSpec instances for composed protocols.
• ArkLib/OracleReduction/Salt.lean: Comment out the implementation of salted protocols and their associated prover, verifier, and reduction transformations.
• ArkLib/OracleReduction/Security/Basic.lean: Updates and generalizes the core security definitions for oracle reductions by refactoring type parameters, adopting a standardized probability notation, and adjusting the signatures of completeness and soundness.
• ArkLib/OracleReduction/Security/Implications.lean: Update the challenge type constraint to SampleableType and comment out the incomplete security implication theorems.
• ArkLib/OracleReduction/Security/Rewinding.lean: Updates the pSpec.Challenge typeclass constraint to SampleableType and comments out the incomplete Rewinding extractor definitions.
• ArkLib/OracleReduction/Security/RoundByRound.lean: Refactors the round-by-round security framework to generalize oracle contexts and update the probabilistic definitions used in soundness and knowledge soundness proofs.
• ArkLib/OracleReduction/Security/SpecialSoundness.lean: Commented out the definitions and examples for ArityTree and TranscriptTree.
• ArkLib/OracleReduction/Security/StateRestoration.lean: Comment out the definitions and game specifications for state-restoration soundness and knowledge soundness.
• ArkLib/OracleReduction/VectorIOR.lean: Refactors VectorIOR and VectorIOP to use explicit oracle contexts and simplified statement types, replacing generic oracle interfaces with a dedicated vector message oracle implementation.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: Corrects the name of a commented-out typeclass constraint from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean: Update the typeclass constraint for the field L from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/BinaryBasefold/General.lean: Replaces the SelectableType typeclass constraint with SampleableType for the field L.
• ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean: Replace the SelectableType constraint with SampleableType for the field L in the Binary Basefold query phase.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean: Renames the SelectableType typeclass and its associated instances to SampleableType throughout the Binary Basefold protocol specification.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean: Replaces occurrences of the SelectableType typeclass with SampleableType throughout the binary Basefold proof system definitions.
• ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: The update replaces the SelectableType constraint on the field L with SampleableType.
• ArkLib/ProofSystem/Binius/FRIBinius/General.lean: Update the general Binius FRI specification by replacing instances of the SelectableType typeclass with SampleableType.
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Updated the typeclass constraint for the field L from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean: Replaced the SelectableType typeclass constraint with SampleableType for the field L.
• ArkLib/ProofSystem/Binius/RingSwitching/General.lean: Replace all occurrences of SelectableType with SampleableType to reflect a renaming in the underlying library.
• ArkLib/ProofSystem/Binius/RingSwitching/Prelude.lean: Replaces the SelectableType requirement with SampleableType for challenges and field elements within the MLIOPCS structure and associated variable declarations.
• ArkLib/ProofSystem/Binius/RingSwitching/Spec.lean: Renames the SelectableType typeclass and its associated instances to SampleableType throughout the Ring Switching protocol specification.
• ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean: Update the type class constraints for the fields and rings used in the sumcheck phase from SelectableType to SampleableType.
• ArkLib/ProofSystem/Component/CheckClaim.lean: Comment out the entire implementation and proofs for the CheckClaim reduction and oracle reduction components.
• ArkLib/ProofSystem/Component/DoNothing.lean: Comment out the redundant DoNothing reduction and oracle reduction definitions and their associated completeness and soundness theorems.
• ArkLib/ProofSystem/Component/NoInteraction.lean: Comment out the entire implementation of the non-interactive reduction component, including its definitions and completeness theorem.
• ArkLib/ProofSystem/Component/RandomQuery.lean: Generalize the RandomQuery component to support arbitrary query types and execution contexts instead of being restricted to OracleInterface queries.
• ArkLib/ProofSystem/Component/ReduceClaim.lean: Refactors statement types and comments out the oracle reduction and knowledge soundness sections to accommodate ongoing updates to the OracleReduction definition.
• ArkLib/ProofSystem/Component/SendClaim.lean: Comment out the implementation of the SendClaim oracle reduction and its completeness proof.
• ArkLib/ProofSystem/Component/SendWitness.lean: Comment out the completeness theorems and oracle reduction implementations for the SendWitness and SendSingleWitness components.
• ArkLib/ProofSystem/Fri/Domain.lean: Replace field_simp with more targeted simp lemmas to streamline algebraic proofs in the FRI domain.
• ArkLib/ProofSystem/Fri/RoundConsistency.lean: Removed a redundant rewrite step from the proof of the generalised_round_consistency_completeness lemma.
• ArkLib/ProofSystem/Fri/Spec/SingleRound.lean: Refactor OracleStatement and FinalOracleStatement into dependent function types and update the FRI folding round components to integrate with a new oracle context and specification framework.
• ArkLib/ProofSystem/Stir/MainThm.lean: Updates the STIR main theorem and soundness proof by replacing the SelectableType constraint with SampleableType and adjusting VectorIOP signatures to accommodate additional implicit parameters.
• ArkLib/ProofSystem/Sumcheck/Spec/General.lean: Replaced the SelectableType typeclass constraint with SampleableType across the sum-check verifier specification and its associated lemmas.
• ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean: Replaces the SelectableType type class with SampleableType and updates the notation for combining oracle specifications.
• ArkLib/ProofSystem/Whir/RBRSoundness.lean: This change refactors the WHIR round-by-round soundness theorem and its associated definitions to align with updates in the VectorIOP framework and related type class constraints.
• ArkLib/ToMathlib/Finsupp/Fin.lean: Update formatting by adding spaces around the addition operator in the sum_insertNth' lemma.
• ArkLib/ToMathlib/MvPolynomial/Equiv.lean: Add the Mathlib.Tactic.Cases import to provide access to the cases tactic for proofs within the module.
• ArkLib/ToMathlib/NumberTheory/PrattCertificate.lean: Added the Mathlib.Tactic.Cases import to provide access to the cases tactic.
• ArkLib/ToVCVio/DistEq.lean: Update distributional equality definitions by transitioning to the HasEvalSPMF typeclass and refining OracleSpec constraints to use Fintype and Inhabited.
• ArkLib/ToVCVio/Lemmas.lean: Remove redundant lemmas related to failure probabilities and lifted computations that have been upstreamed to the VCVio library.
• ArkLib/ToVCVio/Oracle.lean: Refactor runWithOracle to use simulateQ, rename SelectableType to SampleableType, and simplify associated definitions and theorems to align with current library conventions.
• ArkLib/ToVCVio/SimOracle.lean: Comments out the file's contents as they have been ported to or subsumed by newer implementations.
• lake-manifest.json: Updates project dependencies by bumping several package versions from v4.22.0 to v4.24.0 and updating various repository revisions and URLs.
• lakefile.toml: Update the VCVio and doc-gen4 dependency versions and comment out the CompPoly requirement.
• lean-toolchain: Update the Lean 4 toolchain version from v4.22.0 to v4.24.0.

---

Last updated: 2026-01-07 05:06 UTC.

[dtumad]

Closed for an updated PR #286