feat: 4.24 update and VCV upstream changes #261

dtumad · 2025-10-16T21:18:49Z

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

…dt/downstream-pfun

github-actions · 2025-10-16T21:35:43Z

🤖 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.

…tion?

…M/ArkLib into dt/downstream-pfun

quangvdao · 2025-10-21T17:30:36Z

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

dtumad · 2025-11-05T16:18:00Z

ArkLib/OracleReduction/OracleInterface.lean

-  Query := R
-  Response := R
-  answer := fun poly point => poly.eval point
+def instPolynomial : OracleContext R (ReaderM R[X]) where


@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.

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

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

…dt/downstream-pfun

alexanderlhicks · 2025-12-12T14:28:12Z

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

…M/ArkLib into dt/downstream-pfun

github-actions · 2026-01-07T05:06:07Z

🤖 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 · 2026-01-07T15:59:52Z

Closed for an updated PR #286

alexanderlhicks and others added 2 commits September 28, 2025 10:57

wip bump to 4.24 rc1

de66bf2

start of updating downstream

7632680

dtumad added the draft A pull request that is still work in progress label Oct 16, 2025

Merge branch 'main' of https://github.com/Verified-zkEVM/ArkLib into …

5220980

…dt/downstream-pfun

alexanderlhicks self-assigned this Oct 17, 2025

alexanderlhicks marked this pull request as draft October 17, 2025 09:52

alexanderlhicks and others added 10 commits October 17, 2025 11:32

fix build error and pre-existing sorry

334619c

import Tactic to fix build issue. Todo: replace induction' with induc…

162d56a

…tion?

fix proof in JohnsonBound/Choose2

cd18721

various vcv breaking changes

8219bb4

Merge branch 'dt/downstream-pfun' of https://github.com/Verified-zkEV…

7a62623

…M/ArkLib into dt/downstream-pfun

fix oracle interface (may want to go farther in future

40be741

suggested new interface

f19ce76

issues not involving oracle comp lifting issues

7c52340

Changes to OracleInterface

e8008c7

Merge branch 'main' into dt/downstream-pfun

39edd14

quangvdao and others added 10 commits October 21, 2025 11:59

updating VCV

0240067

merge main

bd1b5e1

some build fixes

ea4afda

small stuff

ac55c9e

fix a couple proofs

7a1af79

fix a couple proofs

8444178

slight clean up

ede6bb3

build errors from indexing change

be4cf1f

fixes to oracle interface

d6e2488

pre fri and johnson

b0b4144

dtumad commented Nov 5, 2025

View reviewed changes

dropping some reduction stuff

0471016

dtumad and others added 7 commits November 5, 2025 11:40

Merge branch 'main' of https://github.com/Verified-zkEVM/ArkLib into …

ed78707

…dt/downstream-pfun

identify main defs

3ed4f36

working towards rbr soundness

c8464d9

fixing oracle reduction definitions

42b7809

Merge branch 'main' of https://github.com/Verified-zkEVM/ArkLib into …

fed4b9b

…dt/downstream-pfun

More fixed oracle context for message queries

ecec6b6

add CompPoly dependency

4ab1bcd

dtumad added 7 commits December 17, 2025 09:35

build errors from vcv fixes

e6910e5

Merge branch 'dt/downstream-pfun' of https://github.com/Verified-zkEV…

f2a89eb

…M/ArkLib into dt/downstream-pfun

tmp comppoly fix until version alignment

0c3e124

Merge remote-tracking branch 'origin' into dt/downstream-pfun

3cda2cb

Most of the basic fixes

0cb87ad

4-26

0e414f5

pre-conflicts

cb4edb7

dtumad closed this Jan 7, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: 4.24 update and VCV upstream changes #261

feat: 4.24 update and VCV upstream changes #261

Uh oh!

dtumad commented Oct 16, 2025

Uh oh!

github-actions bot commented Oct 16, 2025 •

edited

Loading

Uh oh!

quangvdao commented Oct 21, 2025

Uh oh!

dtumad Nov 5, 2025

Uh oh!

quangvdao Nov 5, 2025

Uh oh!

quangvdao Nov 5, 2025

Uh oh!

alexanderlhicks commented Dec 12, 2025

Uh oh!

github-actions bot commented Jan 7, 2026

Uh oh!

dtumad commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

feat: 4.24 update and VCV upstream changes #261

feat: 4.24 update and VCV upstream changes #261

Uh oh!

Conversation

dtumad commented Oct 16, 2025

Uh oh!

github-actions bot commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Uh oh!

quangvdao commented Oct 21, 2025

Uh oh!

dtumad Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

quangvdao Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

quangvdao Nov 5, 2025

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks commented Dec 12, 2025

Uh oh!

github-actions bot commented Jan 7, 2026

🤖 Gemini PR Summary

Features

Refactoring

Fixes

Documentation

Uh oh!

dtumad commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Oct 16, 2025 •

edited

Loading