feat: Update to 4.26 and fix breaking changes in VCV

[dtumad]

Before Merge: Update PR description

Corresponding VCV change: Verified-zkEVM/VCV-io#90

[github-actions]

🤖 Gemini PR Summary

This PR performs a major toolchain and library migration, upgrading the project from Lean 4.22.0 to 4.26.0 and aligning with significant breaking changes in the VCVio dependency. The primary focus is the refactoring of the oracle-based proof system framework.

Features

• Toolchain Upgrade: Updates Lean toolchain to v4.26.0 and synchronizes mathlib and doc-gen4 dependencies.
• Oracle System Migration: Transitions the codebase from the OracleInterface typeclass-based approach to a more explicit OracleContext and OracleSpec API.
• Typeclass Evolution: Replaces the SelectableType constraint with SampleableType across protocol specifications, challenge generation, and security definitions.
• Probability Framework Update: Updates distributional equality constraints, replacing HasEvalDist with HasEvalSPMF to match updated upstream definitions.

Fixes

• Mathlib Compatibility: Fixes broken imports and lemma references resulting from Mathlib's reorganization (e.g., Matrix.Rank, TensorProduct, and Finsupp lemmas).
• Namespace Resolution: Resolves ambiguities in standard library lemmas by utilizing the _root_ prefix and fully qualifying theorem names (e.g., Int.mul_le_mul_right).
• Tactic Adjustments: Corrects induction syntax and proof steps affected by changes in the Finset.sum_bij' tactic and other core Lean 4 tactics.

Refactoring

• Oracle Composition: Refactors oracle specification syntax, replacing the ++ₒ operator with the standard + operator.
• Verification Logic: Integrates OptionT across commitment schemes and oracle reductions to handle failure states more robustly in verification functions.
• Inductive Proofs: Modernizes proof scripts by adopting the structured induction ... with | ... syntax throughout the library.
• Simplified Definitions: Streamlines various data structures (e.g., ArkLib/Data/Classes/DCast.lean, ArkLib/Data/Fin/Basic.lean) by utilizing definitional equality and removing redundant tactic steps.
• Protocol Components: Refactors high-level components like RandomQuery, VectorIOR, and MerkleTree to align with the new OracleContext representation.

Documentation & Maintenance

• Incomplete Proof Handling: Introduces sorry placeholders and stop commands in several complex modules (e.g., JohnsonBound, Binius, Spartan, STIR) to allow the project to compile while breaking changes in the underlying theory are addressed.
• Code Deactivation: Comments out specific security analyses and proof system components (e.g., Fiat-Shamir, FRI, Binius specific imports) that require further update to be compatible with the new VCV architecture.

---

Analysis of Changes

Metric	Count
📝 Files Changed	102
✅ Lines Added	6190
❌ Lines Removed	5728

---

sorry Tracking

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

• theorem cast_rbrKnowledgeSoundness (ε : pSpec₁.ChallengeIdx → ℝ≥0) in ArkLib/OracleReduction/Cast.lean
• def oracleReduction.randomQuery : OracleReduction oSpec in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem randomOracle_neverFails_iff_runWithOracle_neverFails {β} in ArkLib/ToVCVio/Oracle.lean
• theorem randomOracle_cache_neverFails_iff_runWithOracle_neverFails {β} in ArkLib/ToVCVio/Oracle.lean
• def oracleReduction.checkClaim : OracleReduction oSpec in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem append_knowledgeSoundness (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem Reduction.run_of_prover_first [ProverOnly pSpec] (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
• theorem simulateQ'_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) in ArkLib/ToVCVio/SimOracle.lean
• theorem cast_processRound (j : Fin n₁) in ArkLib/OracleReduction/Cast.lean
• theorem OracleReduction.liftContext_toReduction_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• theorem OracleVerifier.liftContext_toVerifier_comm in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• def squeezeUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : in ArkLib/Data/Hash/DuplexSponge.lean
• theorem oracleReduction_completeness (h : init.neverFails) : in ArkLib/ProofSystem/Component/CheckClaim.lean
• def oracleReduction.linearCombination : in ArkLib/ProofSystem/Spartan/Basic.lean
• def oracleVerifier : OracleVerifier oSpec Statement OStatement Unit (OStatement ⊕ᵥ OStatement) in ArkLib/ProofSystem/Component/SendClaim.lean
• def oracleReduction.firstChallenge : in ArkLib/ProofSystem/Spartan/Basic.lean
• def OracleVerifier.liftContext in ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• theorem runWithOracle_succeeds_iff_simulateQ_randomOracle_neverFails in ArkLib/ToVCVio/Oracle.lean
• def oracleReduction.sendEvalClaim : in ArkLib/ProofSystem/Spartan/Basic.lean
• def secondSumCheckVirtualPolynomial in ArkLib/ProofSystem/Spartan/Basic.lean
• def oracleReduction.reduceClaim : OracleReduction oSpec in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem cast_runToRound (j : Fin (n₁ + 1)) (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Cast.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 oracleReduction_rbr_knowledge_soundness : True in ArkLib/ProofSystem/Component/CheckClaim.lean
• theorem oracleVerifier_eq_verifier : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• def proverRound (i : Fin n) : ProverRound oSpec (pSpec R deg) where in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem stir_rbr_soundness in ArkLib/ProofSystem/Stir/MainThm.lean
• lemma OracleVerifier.append_toVerifier in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem oracleReduction_perfectCompleteness (hInit : init.neverFails) : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• def RoundByRound.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem challengeOracleInterface_cast {h : n₁ = n₂} {hSpec : pSpec₁.cast h = pSpec₂} in ArkLib/OracleReduction/ProtocolSpec/Cast.lean
• theorem oracleVerifier_rbrKnowledgeSoundness [Fintype R] : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem seqCompose_rbrSoundness in ArkLib/OracleReduction/Composition/Sequential/General.lean
• theorem reduction_perfectCompleteness (hInit : init.neverFails) : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem cast_id : in ArkLib/OracleReduction/Cast.lean
• instance oCtxLens_complete : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem completeness : (oracleReduction oSpec Statement OStatement relComp).perfectCompleteness in ArkLib/ProofSystem/Component/SendClaim.lean
• theorem append_soundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem cast_toVerifier (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₁) : in ArkLib/OracleReduction/Cast.lean
• def OracleVerifier.append (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• def StateFunction.append in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem append_rbrKnowledgeSoundness in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem whir_rbr_soundness in ArkLib/ProofSystem/Whir/RBRSoundness.lean
• def ratchetUnchecked [Permute C] (sponge : DuplexSponge U C) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
• theorem append_run (stmt : Stmt₁) (wit : Wit₁) : in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem reduction_completeness {ε : ℝ≥0} in ArkLib/ProofSystem/Component/NoInteraction.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
• instance extractorLens_rbr_knowledge_soundness : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem verifier_rbr_knowledge_soundness : in ArkLib/ProofSystem/Component/CheckClaim.lean
• def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop in ArkLib/CommitmentScheme/Basic.lean
• def oracleReduction.sendClaim : OracleReduction oSpec (StmtIn R) (OStmtIn R deg) Unit in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• theorem append_rbrSoundness {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• def numQueries (stmt : StmtIn) (challenges : ∀ i, pSpec.Challenge i) in ArkLib/OracleReduction/Basic.lean
• theorem append_completeness (R₁ : Reduction oSpec Stmt₁ Wit₁ Stmt₂ Wit₂ pSpec₁) in ArkLib/OracleReduction/Composition/Sequential/Append.lean
• theorem verifier_rbrKnowledgeSoundness [Fintype R] : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
• def absorbUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) : DuplexSponge U C in ArkLib/Data/Hash/DuplexSponge.lean
• def OracleVerifier.addSalt (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : in ArkLib/OracleReduction/Salt.lean
• theorem stir_main in ArkLib/ProofSystem/Stir/MainThm.lean
• theorem cast_run (stmt : StmtIn) (wit : WitIn) : in ArkLib/OracleReduction/Cast.lean
• def Extractor.RoundByRound.liftContext in ArkLib/OracleReduction/LiftContext/Reduction.lean
• def oracleVerifier : OracleVerifier oSpec (StmtIn R) (OStmtIn R deg) (StmtOut R) (OStmtOut R deg) in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean

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

• def OracleVerifier.run in ArkLib/OracleReduction/Execution.lean
• def commitmentScheme : Commitment.Scheme (oSpec α β γ) α β γ sorry !p[] where in ArkLib/CommitmentScheme/SimpleRO.lean
• def Reduction.runWithLog (stmt : StmtIn) (wit : WitIn) in ArkLib/OracleReduction/Execution.lean
• def ofVerify (vrf : (stmtIn : StmtIn) → (challenges : pSpec.Challenges) → in ArkLib/OracleReduction/Basic.lean
• def relIn : (StmtIn × ∀ i, OStmtIn OStatement i) → WitIn → Prop in ArkLib/ProofSystem/Component/RandomQuery.lean
• def foldVerifierOStmtOutSpec : OracleSpec in ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
• abbrev SEP_BYTE : String in ArkLib/Data/Hash/DomainSep.lean
• def rbrSoundness_queryImpl : in ArkLib/OracleReduction/Security/RoundByRound.lean

---

🎨 **Style Guide Adherence**

As a senior engineer, I have reviewed the code changes for adherence to the ArkLib Style Guide and the referenced mathlib conventions. The following lines violate the guide:

1. Prohibited Development Commands (stop)

The stop keyword is a development-only command that halts compilation. It is not permitted in the master branch.

• ArkLib/CommitmentScheme/InductiveMerkleTree.lean:117, 128, 228, 313
• ArkLib/Data/CodingTheory/Basic.lean:1609
• ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean:80, 100, 291
• ArkLib/Data/CodingTheory/JohnsonBound/Expectations.lean:145
• ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean:55, 112, 122, 135, 146, 165, 185, 229, 248, 289, 299, 327, 350, 375, 386, 402, 416, 462, 540
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean:461, 926
• ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean:2382
• ArkLib/Data/Fin/Sigma.lean:461, 483, 495
• ArkLib/OracleReduction/Basic.lean:337
• ArkLib/OracleReduction/LiftContext/Reduction.lean:196, 228, 358, 505
• ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean:136
• ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean:333, 345
• ArkLib/ProofSystem/Component/RandomQuery.lean:74, 91
• ArkLib/ProofSystem/Component/ReduceClaim.lean:70
• ArkLib/OracleReduction/Security/RoundByRound.lean:250, 427, 561, 581

Violation: "ArkLib aims to align closely with the established conventions... particularly those used in mathlib." (Mathlib conventions strictly prohibit development commands like stop or #exit in production code).

2. Usage of sorry

The use of sorry indicates incomplete proofs or definitions, which should be resolved before merging.

• ArkLib/CommitmentScheme/InductiveMerkleTree.lean:245
• ArkLib/CommitmentScheme/MerkleTree.lean:192
• ArkLib/CommitmentScheme/SimpleRO.lean:55
• ArkLib/Data/CodingTheory/Basic.lean:1389
• ArkLib/Data/CodingTheory/JohnsonBound/Choose2.lean:44
• ArkLib/Data/CodingTheory/BerlekampWelch/Existence.lean:116
• ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean:2764
• ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean:662
• ArkLib/Data/Hash/DomainSep.lean:86
• ArkLib/OracleReduction/Basic.lean:307, 617, 626
• ArkLib/OracleReduction/Security/RoundByRound.lean:286
• ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean:277, 431, 435
• ArkLib/ProofSystem/Component/RandomQuery.lean:88
• ArkLib/ProofSystem/Component/SendClaim.lean:63, 65, 78
• ArkLib/ProofSystem/Component/SendWitness.lean:128, 148, 151

Violation: "ArkLib aims to align closely with the established conventions... particularly those used in mathlib." (Mathlib conventions prohibit sorry in the final codebase).

3. Commented-out Code

Massive blocks of code have been commented out rather than deleted.

• ArkLib.lean:126-137, 148-149, 152-153, 156-171, 185-186
• ArkLib/CommitmentScheme/Basic.lean:126-168
• ArkLib/CommitmentScheme/SimpleRO.lean:50-54
• ArkLib/OracleReduction/Basic.lean:557-578, 613-642
• ArkLib/OracleReduction/Cast.lean:111-255
• ArkLib/OracleReduction/Composition/Sequential/Append.lean:25-635
• ArkLib/OracleReduction/Composition/Sequential/General.lean:25-578
• ArkLib/ToVCVio/SimOracle.lean:24-184

Violation: "Adhering to this style guide ensures consistency... making it easier for everyone to read, understand, and maintain the code." (Mathlib style requires removing dead or commented-out code).

4. Naming Conventions

• ArkLib/OracleReduction/Basic.lean:321: QueryImpl.addReaderT (Mixed naming)
• ArkLib/OracleReduction/Basic.lean:361: OracleContext.add_ReaderT (Mixed naming: snake_case and CamelCase)
• ArkLib/OracleReduction/Security/RoundByRound.lean:284: rbrSoundness_queryImpl (Snake_case)

Violation: "Please follow the mathlib Style Guide. This covers naming conventions..." (Mathlib uses lowerCamelCase for definitions/terms and UpperCamelCase for types).

5. Citation and Reference Standards

• ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean:83: "Reference: [Gur04, Prop. 3.3]"

Violation: "Each file that cites papers should have a ## References section in its docstring header." (The diff does not show the required References section added to the header).

6. TODO Formatting

• ArkLib/OracleReduction/Basic.lean:12: TODO(dtumad)
• ArkLib/OracleReduction/Basic.lean:83: TODO(dtumad)

Violation: "ArkLib aims to align closely with... mathlib." (Mathlib style guide discourages personal tags in TODOs; they should generally be formatted as TODO or linked to a tracking issue).

---

📄 **Per-File Summaries**

• ArkLib.lean: Comment out multiple imports related to Fiat-Shamir transformations, security analyses, and specific proof system components like FRI and Binius.
• ArkLib/AGM/Basic.lean: Refactor oracle definitions and implementations to align with a revised OracleSpec API and simplified composition syntax.
• ArkLib/CommitmentScheme/Basic.lean: This PR refactors the commitment scheme framework to use OracleContext instead of OracleInterface for data queries and updates the correctness and binding definitions to align with this new representation.
• ArkLib/CommitmentScheme/InductiveMerkleTree.lean: Refactor the OracleSpec for Merkle trees to use a direct mapping from pairs to values and update associated definitions, proofs, and the verifyProof return type accordingly.
• ArkLib/CommitmentScheme/MerkleTree.lean: Refactored the Merkle tree implementation and proofs to align with updated OracleSpec definitions and OptionT-based failure handling.
• ArkLib/CommitmentScheme/SimpleRO.lean: Refactor the oracle specifications and update the commitment and verification functions to align with a revised OracleSpec API and incorporate OptionT for verification logic.
• ArkLib/Data/Classes/DCast.lean: Simplifies the proof of cast_eq_dcast for Fin by using definitional equality (rfl).
• ArkLib/Data/CodingTheory/Basic.lean: Refine and update various proofs in the coding theory module by simplifying Finset rewrites, tightening simp calls, and introducing placeholders for incomplete logic.
• ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean: Update a proof case name in the solution_to_BerlekampWelch_condition lemma to maintain compatibility with changes in the Finset.sum_bij' tactic.
• ArkLib/Data/CodingTheory/BerlekampWelch/ElocPoly.lean: Refactor induction proofs to use the standard Lean 4 induction ... with syntax.
• ArkLib/Data/CodingTheory/BerlekampWelch/Existence.lean: Replaces a tactic-based proof step with a sorry placeholder in the E_and_Q_BerlekampWelch_condition lemma.
• ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean: This update inserts several stop commands and a sorry to truncate and skip portions of the proofs, likely for debugging or performance purposes.
• ArkLib/Data/CodingTheory/JohnsonBound/Choose2.lean: Replaced the final proof step of the choose_2_convex theorem with a placeholder, leaving the proof incomplete.
• ArkLib/Data/CodingTheory/JohnsonBound/Expectations.lean: This change simplifies a proof step in e_ball_le_radius and truncates the processing of the min_dist_le_d proof using the stop command.
• ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean: This change inserts stop commands into several lemmas to truncate formal proof verification, likely for debugging or incremental development purposes.
• ArkLib/Data/CodingTheory/Prelims.lean: Update the Matrix.Rank import path and simplify the proof for a Nonempty instance.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: Updated the PowerSeries.coeff function call by removing an unnecessary underscore placeholder.
• ArkLib/Data/CodingTheory/ProximityGap/DG25.lean: Added several stop commands to halt Lean's proof processing and compilation at specific locations within the file.
• ArkLib/Data/FieldTheory/AdditiveNTT/AdditiveNTT.lean: This change introduces a stop command and replaces a proof step with sorry to temporarily bypass proof verification in AdditiveNTT.lean.
• ArkLib/Data/FieldTheory/AdditiveNTT/NovelPolynomialBasis.lean: Refactor polynomial splitting proofs to utilize the updated and simplified Splits API and its associated lemmas.
• ArkLib/Data/FieldTheory/BinaryField/BF128Ghash/Basic.lean: This change simplifies the characteristic 2 proof for BF128Ghash by removing a redundant explicit type argument.
• ArkLib/Data/FieldTheory/BinaryField/Common.lean: Corrects the inequality tactics used in the proof of the toPoly_shiftLeft_no_overflow lemma.
• ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean: Replaced a BitVec rewrite with a sorry placeholder in the proof of join_eq_iff_dcast_extractLsb to temporarily bypass a proof step.
• ArkLib/Data/FieldTheory/BinaryField/Tower/TensorAlgebra.lean: Refines imports by replacing Mathlib.RingTheory.TensorProduct.Basic with Mathlib.RingTheory.TensorProduct.Maps.
• ArkLib/Data/Fin/Basic.lean: Simplifies the proof of the induction_append_left theorem by removing a redundant rfl tactic.
• ArkLib/Data/Fin/Sigma.lean: Update divSum? to use Fin.find?, rename induction cases, and truncate several proofs with stop commands.
• ArkLib/Data/Hash/DomainSep.lean: Replaces the definition of the SEP_BYTE separator with a sorry placeholder.
• ArkLib/Data/Hash/DuplexSponge.lean: Refactored the duplex sponge's oracle specifications and implementations to simplify query syntax and streamline simulation calls by removing redundant unit parameters and placeholder proofs.
• ArkLib/Data/List/Lemmas.lean: Refactor the proof of the zipWith_const lemma to use a more explicit induction structure.
• ArkLib/Data/Matrix/Basic.lean: Updated the Hadamard matrix import path to align with the current Mathlib directory structure.
• ArkLib/Data/MlPoly/Basic.lean: Inserted a stop command to halt processing within the proof of the forwardRange_0_eq_finRange lemma.
• ArkLib/Data/Nat/Bitwise.lean: Comment out redundant ENNReal division lemmas and update the induction case names in the sum_eq_xor_plus_twice_and proof for better clarity.
• ArkLib/Data/Polynomial/Bivariate.lean: This change temporarily bypasses incomplete or failing proofs in the bivariate polynomial theory by introducing sorry and stop commands.
• ArkLib/Data/Polynomial/Frobenius.lean: Refactor polynomial splitting and divisibility proofs to align with updated Mathlib naming conventions and simplify property applications.
• ArkLib/Data/RingTheory/CanonicalEuclideanDomain.lean: Fully qualify the mul_le_mul_right lemma as Int.mul_le_mul_right in the Int instance's proof to ensure correct theorem resolution.
• ArkLib/Data/Vector/Basic.lean: Fully qualify standard library lemmas with the _root_ prefix to resolve namespace ambiguities and simplify proof steps.
• ArkLib/OracleReduction/BCS/Basic.lean: Comment out unused variable declarations and type definitions within the OracleReduction namespace.
• ArkLib/OracleReduction/Basic.lean: Refactored the interactive oracle reduction framework to replace typeclass-based oracle interfaces with explicit oracle contexts and updated verification logic for better composability.
• ArkLib/OracleReduction/Cast.lean: Simplify oracle statement types and comment out the casting implementations and theorems for oracle verifiers and reductions.
• ArkLib/OracleReduction/Composition/Sequential/Append.lean: Comment out the entire content of the file, effectively deactivating the definitions and theorems for the sequential composition of oracle reductions.
• ArkLib/OracleReduction/Composition/Sequential/General.lean: Comments out the definitions and security theorems for sequential composition and updates a type constraint from SelectableType to SampleableType.
• ArkLib/OracleReduction/Execution.lean: Refactor the interactive reduction execution framework to support generalized oracle specifications and utilize OptionT for handling verifier outcomes.
• ArkLib/OracleReduction/FiatShamir/Basic.lean: Update the oracle composition operator to + and transition the challenge type requirement from SelectableType to SampleableType.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Defs.lean: Update oracle specification composition by replacing the ++ₒ operator with the + operator throughout the file.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemma.lean: Replaces the ++ₒ operator with + to update the syntax for combining oracle specifications across game definitions and lemmas.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/ProverTransform.lean: Update the type signature of duplexSpongeToBasicFSAlgo to use the + operator instead of ++ₒ for combining oracle specifications.
• ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/TraceTransform.lean: Update the oracle composition operator from ++ₒ to + in the basicToDuplexSpongeFSTrace function signature.
• ArkLib/OracleReduction/LiftContext/Lens.lean: Updates oracle lens definitions to use explicit OracleContext parameters instead of typeclass-based oracle interfaces.
• ArkLib/OracleReduction/LiftContext/OracleReduction.lean: Comment out the implementation and associated security theorems for context lifting in oracle reductions.
• ArkLib/OracleReduction/LiftContext/Reduction.lean: Refactor the lifting context reduction by updating the syntax for accessing oracle computation support and refining monad instances and typeclass requirements.
• ArkLib/OracleReduction/OracleInterface.lean: Refactor the oracle reduction system by replacing the OracleInterface type class with a new OracleContext structure and updating associated polynomial evaluation instances.
• ArkLib/OracleReduction/Prelude.lean: The Sampleable typeclass was updated to extend SampleableType instead of SelectableType.
• ArkLib/OracleReduction/ProtocolSpec/Basic.lean: Refactor protocol oracles to use SampleableType and OracleContext while refining the indexing for challenge oracles.
• ArkLib/OracleReduction/ProtocolSpec/Cast.lean: Comment out the OracleInterface instance and the related casting theorem for protocol specifications.
• ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean: Renames the SelectableType typeclass requirement to SampleableType for protocol challenges and comments out several OracleInterface instances and lemmas for protocol compositions.
• ArkLib/OracleReduction/Salt.lean: Comment out the implementation of protocol salting for specifications, transcripts, provers, and verifiers.
• ArkLib/OracleReduction/Security/Basic.lean: Refactor the security definitions for completeness, soundness, and knowledge soundness to utilize OptionT and updated probability notation.
• ArkLib/OracleReduction/Security/Implications.lean: Update the typeclass constraint for protocol challenges to use SampleableType instead of SelectableType.
• ArkLib/OracleReduction/Security/Rewinding.lean: This change updates the typeclass constraint for protocol challenges from SelectableType to SampleableType.
• ArkLib/OracleReduction/Security/RoundByRound.lean: Refactors the round-by-round security definitions to utilize generalized oracle contexts and introduces a run_simulate helper function to streamline the simulation logic in proofs.
• ArkLib/OracleReduction/Security/StateRestoration.lean: Update the state restoration security definitions to use the + operator for oracle composition and replace the SelectableType constraint with SampleableType.
• ArkLib/OracleReduction/VectorIOR.lean: Refactor VectorIOR and VectorIOP definitions to use explicit oracle contexts and a new message oracle implementation for vector indexing instead of generic oracle interfaces.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: The changes update a typeclass reference in a comment and simplify the application of the Fin.castSucc_lt_succ lemma in foldStepRelOutProp.
• ArkLib/ProofSystem/Binius/BinaryBasefold/CoreInteractionPhase.lean: Update the typeclass constraint for field L by replacing SelectableType with SampleableType.
• ArkLib/ProofSystem/Binius/BinaryBasefold/General.lean: Updates the typeclass constraint for the field L from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean: Inserted a stop command to halt processing within the getSumcheckRoundPoly function during the proof of polynomial degree bounds.
• ArkLib/ProofSystem/Binius/BinaryBasefold/QueryPhase.lean: Updated the typeclass constraint for field $L$ from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Spec.lean: Renamed SelectableType to SampleableType and commented out several OracleInterface instances within the Binary Basefold protocol specification.
• ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean: Replaces the SelectableType typeclass constraint with SampleableType throughout the binary Basefold proof system definitions.
• ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: Updated the typeclass constraint for field L from SelectableType to SampleableType.
• ArkLib/ProofSystem/Binius/FRIBinius/General.lean: Renames the SelectableType typeclass to SampleableType across the FRI Binius protocol variable constraints and challenge instances.
• ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Replaces the SelectableType typeclass constraint with SampleableType for the field L.
• ArkLib/ProofSystem/Binius/RingSwitching/BatchingPhase.lean: Updates the batching phase's type constraints for field L by replacing the SelectableType requirement with SampleableType.
• ArkLib/ProofSystem/Binius/RingSwitching/General.lean: Replace the SelectableType typeclass with SampleableType throughout the file.
• ArkLib/ProofSystem/Binius/RingSwitching/Prelude.lean: Refactor the oracle and challenge definitions in the Binius ring-switching infrastructure to use OracleContext and SampleableType.
• ArkLib/ProofSystem/Binius/RingSwitching/Spec.lean: Rename the SelectableType typeclass and its associated instances to SampleableType throughout the Binius Ring-Switching specification.
• ArkLib/ProofSystem/Binius/RingSwitching/SumcheckPhase.lean: Replaces the SelectableType type class constraint with SampleableType for the field and ring types used in the Binius ring-switching sumcheck phase.
• ArkLib/ProofSystem/Component/CheckClaim.lean: Comment out the implementation and formal proofs for the CheckClaim reduction component.
• ArkLib/ProofSystem/Component/DoNothing.lean: Comment out the implementation and associated theorems of the DoNothing reduction and oracle reduction.
• ArkLib/ProofSystem/Component/NoInteraction.lean: Comment out the definitions and completeness theorems for non-interactive proof system reductions.
• ArkLib/ProofSystem/Component/RandomQuery.lean: Refactor the RandomQuery component to generalize oracle interactions by replacing the OracleInterface dependency with a generic query type and an OracleContext.
• ArkLib/ProofSystem/Component/ReduceClaim.lean: Simplifies statement and witness type parameters and comments out the round-by-round extractor, knowledge soundness theorems, and the entire oracle reduction section.
• ArkLib/ProofSystem/Component/SendClaim.lean: Commented out the core protocol specifications, prover, and verifier definitions for the SendClaim oracle reduction.
• ArkLib/ProofSystem/Component/SendWitness.lean: This change comments out the oracle reduction implementation and associated completeness proofs for the SendWitness and SendSingleWitness components.
• ArkLib/ProofSystem/Fri/Domain.lean: Replaced several field_simp tactic calls with sorry placeholders in domain-related lemmas.
• ArkLib/ProofSystem/Fri/RoundConsistency.lean: This update replaces an automated aesop proof step with a sorry placeholder and removes a redundant rewrite within the FRI round consistency completeness lemma.
• ArkLib/ProofSystem/Fri/Spec/SingleRound.lean: Refactored the FRI proof system's oracle statement types and integrated a new OracleContext and OracleSpec framework into the round specifications.
• ArkLib/ProofSystem/Spartan/Basic.lean: Commented out the definitions for oracle interfaces and various protocol steps within the Spartan proof system.
• ArkLib/ProofSystem/Stir/MainThm.lean: Comment out the STIR main theorem and its associated round-by-round soundness lemma while performing minor refactoring of their type signatures.
• ArkLib/ProofSystem/Sumcheck/Spec/General.lean: Comment out the sum-check protocol definitions and theorems and replace the SelectableType constraint with SampleableType.
• ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean: This change replaces the SelectableType typeclass with SampleableType and comments out a large portion of the file's sum-check round logic and security theorems.
• ArkLib/ProofSystem/Whir/RBRSoundness.lean: This change comments out the round-by-round soundness theorem and its associated oracle interface definitions for the WHIR protocol.
• ArkLib/ToMathlib/Finsupp/Fin.lean: Remove the redundant Fin.prod_insertNth and Fin.sum_insertNth lemmas and update local references to use the versions provided by the upstream library.
• ArkLib/ToMathlib/MvPolynomial/Equiv.lean: Refactor proofs to use structured induction syntax and updated tactic conventions for improved readability and style.
• ArkLib/ToMathlib/NumberTheory/PrattCertificate.lean: Refactor induction proofs in Nat.Prime.dvd_mul_list and PrattPart.out to use the structured Lean 4 induction ... with | syntax.
• ArkLib/ToVCVio/DistEq.lean: Update the typeclass constraints for distributional equality by replacing HasEvalDist with HasEvalSPMF and refining the requirements for oracle specifications.
• ArkLib/ToVCVio/Lemmas.lean: This change removes several auxiliary lemmas regarding failure probabilities and support sets for oracle computations, likely because they were temporary or are being moved to a core library.
• ArkLib/ToVCVio/Oracle.lean: Refactors the oracle simulation interface and replaces SelectableType with SampleableType while commenting out deprecated theorems and definitions.
• ArkLib/ToVCVio/SimOracle.lean: Remove the simulateQ' logic and related theorems and comment out the SimOracle definitions and namespace.
• lake-manifest.json: Update multiple package dependencies and revisions, primarily upgrading core components like mathlib and doc-gen4 from version 4.22.0 to 4.26.0.
• lakefile.toml: Updated the revisions for the VCVio and doc-gen4 dependencies.
• lean-toolchain: Update the Lean 4 toolchain version from v4.22.0 to v4.26.0.

---

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