ArkLib.lean

import ArkLib.AGM.Basic
import ArkLib.CommitmentScheme.Basic
import ArkLib.CommitmentScheme.Fold
import ArkLib.CommitmentScheme.InductiveMerkleTree
import ArkLib.CommitmentScheme.KZG
import ArkLib.CommitmentScheme.MerkleTree
import ArkLib.CommitmentScheme.SimpleRO
import ArkLib.CommitmentScheme.Tensor
import ArkLib.CommitmentScheme.Trivial
import ArkLib.Data.CNat.AssocNat
import ArkLib.Data.CNat.Church
import ArkLib.Data.CNat.Defs
import ArkLib.Data.Classes.FunEquiv
import ArkLib.Data.Classes.HasPred
import ArkLib.Data.Classes.HasSize
import ArkLib.Data.Classes.HasSucc
import ArkLib.Data.Classes.Initialize
import ArkLib.Data.Classes.Serde
import ArkLib.Data.Classes.Slice
import ArkLib.Data.Classes.ToNat
import ArkLib.Data.CodingTheory
import ArkLib.Data.CodingTheory.Basic
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
import ArkLib.Data.CodingTheory.DivergenceOfSets
import ArkLib.Data.CodingTheory.GuruswamiSudan
import ArkLib.Data.CodingTheory.GuruswamiSudan.GuruswamiSudan
import ArkLib.Data.CodingTheory.InterleavedCode
import ArkLib.Data.CodingTheory.JohnsonBound.Basic
import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
import ArkLib.Data.CodingTheory.ListDecodability
import ArkLib.Data.CodingTheory.PolishchukSpielman
import ArkLib.Data.CodingTheory.PolishchukSpielman.Degrees
import ArkLib.Data.CodingTheory.PolishchukSpielman.Existence
import ArkLib.Data.CodingTheory.PolishchukSpielman.PolishchukSpielman
import ArkLib.Data.CodingTheory.PolishchukSpielman.Resultant
import ArkLib.Data.CodingTheory.Prelims
import ArkLib.Data.CodingTheory.ProximityGap.AHIV22
import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20
import ArkLib.Data.CodingTheory.ProximityGap.Basic
import ArkLib.Data.CodingTheory.ProximityGap.DG25
import ArkLib.Data.CodingTheory.ReedMuller
import ArkLib.Data.CodingTheory.ReedSolomon
import ArkLib.Data.EllipticCurve.BN254
import ArkLib.Data.Fin.Basic
import ArkLib.Data.Fin.Fold
import ArkLib.Data.Fin.Lift
import ArkLib.Data.Fin.Sigma
import ArkLib.Data.Fin.Tuple.Defs
import ArkLib.Data.Fin.Tuple.Lemmas
import ArkLib.Data.Fin.Tuple.Notation
import ArkLib.Data.Fin.Tuple.TakeDrop
import ArkLib.Data.GroupTheory.PrimeOrder
import ArkLib.Data.GroupTheory.Smooth
import ArkLib.Data.Hash.DomainSep
import ArkLib.Data.Hash.DuplexSponge
import ArkLib.Data.Hash.Poseidon2
import ArkLib.Data.List.BigOperators
import ArkLib.Data.List.Find
import ArkLib.Data.List.HList
import ArkLib.Data.List.Vector
import ArkLib.Data.Matrix.Basic
import ArkLib.Data.Matrix.Sparse
import ArkLib.Data.Misc.Basic
import ArkLib.Data.MvPolynomial.Degrees
import ArkLib.Data.MvPolynomial.Interpolation
import ArkLib.Data.MvPolynomial.LinearMvExtension
import ArkLib.Data.MvPolynomial.Multilinear
import ArkLib.Data.MvPolynomial.MvPolynomialLike
import ArkLib.Data.MvPolynomial.Sumcheck
import ArkLib.Data.Polynomial.Bivariate
import ArkLib.Data.Polynomial.EvenAndOdd
import ArkLib.Data.Polynomial.Interface
import ArkLib.Data.Polynomial.PolynomialLike
import ArkLib.Data.Polynomial.Prelims
import ArkLib.Data.Polynomial.RationalFunctions
import ArkLib.Data.Polynomial.SplitFold
import ArkLib.Data.Probability.Instances
import ArkLib.Data.Probability.Notation
import ArkLib.OracleReduction.BCS.Basic
import ArkLib.OracleReduction.Basic
import ArkLib.OracleReduction.Cast
import ArkLib.OracleReduction.Composition.Parallel.Basic
import ArkLib.OracleReduction.Composition.Sequential.Append
import ArkLib.OracleReduction.Composition.Sequential.General
import ArkLib.OracleReduction.Equiv
import ArkLib.OracleReduction.Execution
import ArkLib.OracleReduction.FiatShamir.Basic
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Defs
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.AbortAnalysis
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Backtrack
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BadEvents
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Completeness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemma
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lookahead
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ProverTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Soundness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TraceTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
import ArkLib.OracleReduction.LiftContext.Lens
import ArkLib.OracleReduction.LiftContext.OracleReduction
import ArkLib.OracleReduction.LiftContext.Reduction
import ArkLib.OracleReduction.OracleInterface
import ArkLib.OracleReduction.Prelude
import ArkLib.OracleReduction.ProtocolSpec.Basic
import ArkLib.OracleReduction.ProtocolSpec.Cast
import ArkLib.OracleReduction.ProtocolSpec.SeqCompose
import ArkLib.OracleReduction.Salt
import ArkLib.OracleReduction.Security.Basic
import ArkLib.OracleReduction.Security.Implications
import ArkLib.OracleReduction.Security.Rewinding
import ArkLib.OracleReduction.Security.RoundByRound
import ArkLib.OracleReduction.Security.SpecialSoundness
import ArkLib.OracleReduction.Security.StateRestoration
import ArkLib.OracleReduction.VectorIOR
import ArkLib.ProofSystem.BatchedFri.Spec.General
import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.General
import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.FRIBinius.General
import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
import ArkLib.ProofSystem.Binius.RingSwitching.BatchingPhase
import ArkLib.ProofSystem.Binius.RingSwitching.General
import ArkLib.ProofSystem.Binius.RingSwitching.Prelude
import ArkLib.ProofSystem.Binius.RingSwitching.Spec
import ArkLib.ProofSystem.Binius.RingSwitching.SumcheckPhase
import ArkLib.ProofSystem.Component.CheckClaim
import ArkLib.ProofSystem.Component.DoNothing
import ArkLib.ProofSystem.Component.NoInteraction
import ArkLib.ProofSystem.Component.RandomQuery
import ArkLib.ProofSystem.Component.ReduceClaim
import ArkLib.ProofSystem.Component.SendClaim
import ArkLib.ProofSystem.Component.SendWitness
import ArkLib.ProofSystem.ConstraintSystem.Lookup
import ArkLib.ProofSystem.ConstraintSystem.MemoryChecking
import ArkLib.ProofSystem.ConstraintSystem.Plonk
import ArkLib.ProofSystem.ConstraintSystem.R1CS
import ArkLib.ProofSystem.DSL
import ArkLib.ProofSystem.Fri.Domain
import ArkLib.ProofSystem.Fri.RoundConsistency
import ArkLib.ProofSystem.Fri.Spec.General
import ArkLib.ProofSystem.Fri.Spec.SingleRound
import ArkLib.ProofSystem.Plonk.Basic
import ArkLib.ProofSystem.Spartan.Basic
import ArkLib.ProofSystem.Stir
import ArkLib.ProofSystem.Stir.Combine
import ArkLib.ProofSystem.Stir.Folding
import ArkLib.ProofSystem.Stir.MainThm
import ArkLib.ProofSystem.Stir.OutOfDomSmpl
import ArkLib.ProofSystem.Stir.ProximityBound
import ArkLib.ProofSystem.Stir.ProximityGap
import ArkLib.ProofSystem.Stir.Quotienting
import ArkLib.ProofSystem.Sumcheck.Impl.Basic
import ArkLib.ProofSystem.Sumcheck.Spec.General
import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound
import ArkLib.ProofSystem.Whir
import ArkLib.ProofSystem.Whir.BlockRelDistance
import ArkLib.ProofSystem.Whir.Folding
import ArkLib.ProofSystem.Whir.MutualCorrAgreement
import ArkLib.ProofSystem.Whir.OutofDomainSmpl
import ArkLib.ProofSystem.Whir.ProximityGen
import ArkLib.ProofSystem.Whir.RBRSoundness
import ArkLib.ToMathlib.BigOperators.Fin
import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic
import ArkLib.ToMathlib.Data.IndexedBinaryTree.Equiv
import ArkLib.ToMathlib.Data.IndexedBinaryTree.Lemmas
import ArkLib.ToMathlib.Finset.Basic
import ArkLib.ToMathlib.UInt.Equiv
import ArkLib.ToVCVio.DistEq
import ArkLib.ToVCVio.Lemmas
import ArkLib.ToVCVio.Oracle
import ArkLib.ToVCVio.SimOracle