CatCryptCore.lean

/-
Copyright (c) 2026 CatCrypt Contributors. All rights reserved.
Released under MIT license as described in the file LICENSE.
Authors: CatCrypt Contributors
-/

module

-- Lemmas for Mathlib (the upstream queue)
public import CatCryptCore.ForMathlib

-- Probability and core computation
public import CatCryptCore.Prob.SDistr
public import CatCryptCore.Prob.Coupling
public import CatCryptCore.Prob.Support
public import CatCryptCore.Prob.Conditional
public import CatCryptCore.Prob.BirthdayBound
public import CatCryptCore.Prob.SchwartzZippel
public import CatCryptCore.Prob.SchwartzZippelGaloisRing
public import CatCryptCore.Prob.XorBij
public import CatCryptCore.Core.Basic
public import CatCryptCore.Core.Location
public import CatCryptCore.Core.Heap
public import CatCryptCore.Core.Code
public import CatCryptCore.Core.CodeSequence
public import CatCryptCore.Core.SPTree
public import CatCryptCore.Core.SPTreeTimed
public import CatCryptCore.Core.SPTreeTimedOps
public import CatCryptCore.Core.StdDoBridge
public import CatCryptCore.Core.GenHeap
public import CatCryptCore.Core.GenHeapRandomOracle

-- Non-uniform sampling and the unbounded loop
public import CatCryptCore.NonUniform

-- Relational logic (pRHL)
public import CatCryptCore.Relational.Basic
public import CatCryptCore.Relational.Judgment
public import CatCryptCore.Relational.DeadSample
public import CatCryptCore.Relational.Rules
public import CatCryptCore.Relational.Sync
public import CatCryptCore.Relational.Frame
public import CatCryptCore.Relational.Separation
public import CatCryptCore.Relational.Reorder
public import CatCryptCore.Relational.ForLoop

-- Package algebra
public import CatCryptCore.Package.Interface
public import CatCryptCore.Package.RawPackage
public import CatCryptCore.Package.ValidPackage
public import CatCryptCore.Package.Locations

-- Category-theoretic foundation
public import CatCryptCore.Category.KlPMF
public import CatCryptCore.Category.KlSPComp
public import CatCryptCore.Category.Fam
public import CatCryptCore.Category.PkgFam
public import CatCryptCore.Category.Cocartesian
public import CatCryptCore.Category.Affine
public import CatCryptCore.Category.Effectus
public import CatCryptCore.Category.ProtCategory
public import CatCryptCore.Category.ProtBicat
public import CatCryptCore.Category.CoParaGradedBridge
public import CatCryptCore.Category.XCategoricalModel
public import CatCryptCore.Refinement.RRel
public import CatCryptCore.Refinement.RRelLoop
public import CatCryptCore.Refinement.Programs
public import CatCryptCore.XDijkstra.XDijkstraAll
public import CatCryptCore.XDijkstra.XMvcgenControl
public import CatCryptCore.XDijkstra.XMvcgenReg
public import CatCryptCore.XDijkstra.XMorphismInstance
public import CatCryptCore.XDijkstra.XQuantaleGradeCore
public import CatCryptCore.XDijkstra.GradedWP
public import CatCryptCore.XDijkstra.GradedDo
public import CatCryptCore.XDijkstra.XCostMonad
public import CatCryptCore.XDijkstra.XCostMonadModel
public import CatCryptCore.XDijkstra.XTimedMonad
public import CatCryptCore.Complexity.D.Cost
public import CatCryptCore.Complexity.D.TimeAdm
public import CatCryptCore.Complexity.D.Reflect
public import CatCryptCore.Complexity.D.Asymptotic
public import CatCryptCore.Complexity.D.Link
public import CatCryptCore.XDijkstra.XErrMonad
public import CatCryptCore.XDijkstra.XAdvantageHybrid
public import CatCryptCore.XDijkstra.Rel.XRelMvcgenControl
public import CatCryptCore.XDijkstra.Rel.XCombinedAutomation
public import CatCryptCore.XDijkstra.Rel.XCoreProtocolReduction
public import CatCryptCore.XDijkstra.Rel.XProbUCBaseline
public import CatCryptCore.Category.XCategoricalModelRel
public import CatCryptCore.Relational.Approx
public import CatCryptCore.Relational.RelationalQ0
public import CatCryptCore.Crypto.UCMonad.SDistrInstance
public import CatCryptCore.XDijkstra.Demo

-- Deep embedding
public import CatCryptCore.Deep.RawCode
public import CatCryptCore.Deep.Location
public import CatCryptCore.Deep.Package
public import CatCryptCore.Deep.Eval
public import CatCryptCore.Deep.PackageEquiv
public import CatCryptCore.Deep.PkgCategory
public import CatCryptCore.Deep.Deterministic
public import CatCryptCore.Deep.DeterministicInterp
public import CatCryptCore.Deep.Strategy
public import CatCryptCore.Deep.ProofFrog
public import CatCryptCore.Deep.HybridDemo
public import CatCryptCore.Deep.Bridge
public import CatCryptCore.Deep.Tactics
public import CatCryptCore.Deep.Reflect
public import CatCryptCore.Deep.GamePackage
public import CatCryptCore.Deep.OracleGamePackage
public import CatCryptCore.Deep.ReflectUCHelpers

-- Semantic bridge
public import CatCryptCore.Bridge.SemPkg
public import CatCryptCore.Bridge.PkgEval
public import CatCryptCore.Bridge.MonoidalBridge

-- Unary logic, nominal sets
public import CatCryptCore.Unary
public import CatCryptCore.Nominal

-- Tactics
public import CatCryptCore.Tactics
public import CatCryptCore.Tactics.ProofTermAudit
public import CatCryptCore.Tactics.BindVcgenSum
public import CatCryptCore.Tactics.VC
public import CatCryptCore.Tactics.StdCosts
public import CatCryptCore.Tactics.StdCostsPoly
public import CatCryptCore.Tactics.DeriveTimedStructure

-- Crypto foundation
public import CatCryptCore.Crypto.Game
public import CatCryptCore.Crypto.Advantage
public import CatCryptCore.Crypto.SDist
public import CatCryptCore.Crypto.SDistrLift
public import CatCryptCore.Crypto.UC
public import CatCryptCore.Crypto.UCMonad
public import CatCryptCore.Crypto.UCMonad.LeakageExceptT
public import CatCryptCore.Crypto.UCMonad.UCLeakageDecomp
public import CatCryptCore.Crypto.UCMonad.SPCompInstance
public import CatCryptCore.Crypto.RC
public import CatCryptCore.Crypto.UCAlg
public import CatCryptCore.Crypto.UCComposition
public import CatCryptCore.Crypto.UCDSL
public import CatCryptCore.Crypto.UCConcrete
public import CatCryptCore.Crypto.UCConcreteOracle
public import CatCryptCore.Crypto.UCAdmClass
public import CatCryptCore.Crypto.UCAdmClass.SPCompInstance
public import CatCryptCore.Crypto.UCLevels
public import CatCryptCore.Crypto.DummyAdversary
public import CatCryptCore.Crypto.CompUCEquivalence
public import CatCryptCore.Crypto.MonadCostModel
public import CatCryptCore.Crypto.QueryBoundedUC
public import CatCryptCore.Crypto.SizeBoundedUC
public import CatCryptCore.Crypto.CTAdmClass
public import CatCryptCore.Crypto.ConcreteReductions
public import CatCryptCore.Crypto.UCMonad.RoundM
public import CatCryptCore.Crypto.UCMonad.RoundMCompDist
public import CatCryptCore.Crypto.UCAdmClass.SDistrInstance
public import CatCryptCore.Crypto.RCL3
public import CatCryptCore.Crypto.RCL3SPComp
public import CatCryptCore.Crypto.TraceRelating
public import CatCryptCore.Crypto.AGM
public import CatCryptCore.Crypto.SecurityDefs
public import CatCryptCore.Crypto.Encryption
public import CatCryptCore.Crypto.HybridArgument
public import CatCryptCore.Crypto.NomAdvantage
public import CatCryptCore.Crypto.EvalComplete
public import CatCryptCore.Crypto.ExtractedAlgebra
public import CatCryptCore.Crypto.ExtractedOracle
public import CatCryptCore.Crypto.ExtractedPairing
public import CatCryptCore.Crypto.NomPkgBridge
public import CatCryptCore.Crypto.EasyCryptBridge
public import CatCryptCore.Crypto.BadEvent
public import CatCryptCore.Crypto.ForkingLemma
public import CatCryptCore.Crypto.VerifierPair
public import CatCryptCore.Crypto.GameReject
public import CatCryptCore.Crypto.GeneralForkingLemma
public import CatCryptCore.Crypto.TreeForkingLemma
public import CatCryptCore.Crypto.SwitchingLemma
public import CatCryptCore.Crypto.MultiQueryPRF
public import CatCryptCore.Crypto.MultiKeyPRF
public import CatCryptCore.Crypto.OracleAdversary
public import CatCryptCore.Crypto.OracleAdversaryTimed
public import CatCryptCore.Crypto.OracleUpTo
public import CatCryptCore.Crypto.OracleAdversaryRelabelTimed
public import CatCryptCore.Crypto.OracleForkingLemma
public import CatCryptCore.Crypto.OracleBadDraw
public import CatCryptCore.Crypto.FiatShamirROM.EagerMarker
public import CatCryptCore.Crypto.FiatShamirROM.Game
public import CatCryptCore.Crypto.FiatShamirROM.Reduction
public import CatCryptCore.Crypto.FiatShamirROM.Schnorr
public import CatCryptCore.Crypto.FiatShamirROM.SignerHybrid
public import CatCryptCore.Crypto.FiatShamirROM.StraightLine
public import CatCryptCore.Crypto.FiatShamirROM.StraightLineCls
public import CatCryptCore.Crypto.FiatShamirROM.StraightLineMk
public import CatCryptCore.Crypto.FiatShamirROM.StatHVZK
public import CatCryptCore.Crypto.FiatShamirROM.ProgFlag
public import CatCryptCore.Crypto.FiatShamirROM.KeyRecovery
public import CatCryptCore.Crypto.FiatShamirROM.KeyRecoveryMult
public import CatCryptCore.Crypto.FiatShamirROM.KeyRecoveryFlag
public import CatCryptCore.Crypto.FiatShamirROM.Timed
public import CatCryptCore.Crypto.FiatShamirROM.Bridge
public import CatCryptCore.Crypto.SPCompPMF
public import CatCryptCore.Crypto.PRPPRFSwitching
public import CatCryptCore.Crypto.PRFAssumption
public import CatCryptCore.Crypto.PrTrueCover
public import CatCryptCore.Crypto.Assumptions.Catalog
public import CatCryptCore.Crypto.Assumptions.DLGroupParam
public import CatCryptCore.Crypto.Assumptions.CRCoins
public import CatCryptCore.Crypto.Assumptions.LWE
public import CatCryptCore.Crypto.Assumptions.DualPRF
public import CatCryptCore.Crypto.Signatures.Scheme
public import CatCryptCore.Crypto.Signatures.EUFCMA
public import CatCryptCore.Crypto.Signatures.EUFCMAPMF
public import CatCryptCore.Crypto.BLSSig.Security

-- Fujisaki–Okamoto transforms, FIPS 203 KEM, total variation
public import CatCryptCore.Crypto.OracleSimulation
public import CatCryptCore.Crypto.OracleSubst
public import CatCryptCore.Crypto.OracleEval
public import CatCryptCore.Crypto.OracleCollision
public import CatCryptCore.Crypto.TV
public import CatCryptCore.Crypto.Constructions.ECBCPRFFlag
public import CatCryptCore.Crypto.PKE.Games
public import CatCryptCore.Crypto.PKE.FOTransformT
public import CatCryptCore.Crypto.PKE.LWEPKE
public import CatCryptCore.Crypto.AKE.KeySchedule
public import CatCryptCore.Crypto.Messaging.FSPRG
public import CatCryptCore.Crypto.Messaging.CKA
public import CatCryptCore.Crypto.Messaging.FSAEAD
public import CatCryptCore.Crypto.Messaging.DoubleRatchet
public import CatCryptCore.Crypto.PAKE.DHPAKE
public import CatCryptCore.Crypto.Signatures.Threshold
public import CatCryptCore.Crypto.FiatShamirROM.MPCitH
public import CatCryptCore.Crypto.Anon.Signalling
public import CatCryptCore.Crypto.Anon.SignallingUC
public import CatCryptCore.Crypto.OT.Games
public import CatCryptCore.Crypto.OTExtension.IKNP
public import CatCryptCore.Crypto.PRPPRFPmfGame
public import CatCryptCore.Crypto.FiatShamirROM.Verification
public import CatCryptCore.Crypto.ROProgramming
public import CatCryptCore.Crypto.Messaging.KEMCKA
public import CatCryptCore.Crypto.HashThenRF
public import CatCryptCore.Crypto.EagerLazyRF
public import CatCryptCore.Crypto.KEM.Games
public import CatCryptCore.Crypto.KEM.FOTransformU
public import CatCryptCore.Crypto.KEM.FOTransformTimed
public import CatCryptCore.Crypto.KEM.FOTransform
public import CatCryptCore.Crypto.KEM.FIPS203KEM
public import CatCryptCore.Crypto.KEM.FIPS203Security

-- Quantum foundations: instruments, channels, trace norm, tensor products
public import CatCryptCore.Quantum.Instrument
public import CatCryptCore.Quantum.InstrumentCP
public import CatCryptCore.Quantum.CPInstrument
public import CatCryptCore.Quantum.CPCompMonad
public import CatCryptCore.Quantum.TraceNorm
public import CatCryptCore.Quantum.UnitaryChannel
public import CatCryptCore.Quantum.CPMap
public import CatCryptCore.Quantum.DualMap
public import CatCryptCore.Quantum.Measurement
public import CatCryptCore.Quantum.TensorProduct
public import CatCryptCore.Quantum.KroneckerPSD
public import CatCryptCore.Quantum.ChoiKraus
public import CatCryptCore.Quantum.PartialTrace
public import CatCryptCore.Quantum.Stinespring

-- Quantum distinguishing distance, diamond norm, classical lifts, quantum relational Hoare logic
public import CatCryptCore.Quantum.QRHL
public import CatCryptCore.Quantum.ClassicalEmbed
public import CatCryptCore.Quantum.ClassicalEmbedGame
public import CatCryptCore.Quantum.ClassicalLift
public import CatCryptCore.Quantum.ClassicalDiamondLift
public import CatCryptCore.Quantum.BehavioralLift
public import CatCryptCore.Quantum.BehavioralLiftGames
public import CatCryptCore.Crypto.UCMonad.QuantumUC
public import CatCryptCore.Crypto.UCMonad.LocalOpFunctorial
public import CatCryptCore.Crypto.UCMonad.DiamondNormStates
public import CatCryptCore.Crypto.UCMonad.DiamondNorm
public import CatCryptCore.Crypto.UCMonad.DiamondDominates
public import CatCryptCore.Crypto.UCMonad.CPCompUC
public import CatCryptCore.Crypto.UCMonad.DiamondTensorStable
public import CatCryptCore.Crypto.UCMonad.DiamondEmulation
public import CatCryptCore.Crypto.UCMonad.QIndistDiamond

-- Quantum random-oracle model: semi-classical one-way to hiding, KEM games and hops
public import CatCryptCore.Quantum.QROM.CoherentCleanRun
public import CatCryptCore.Quantum.QROM.CoinBadNumeric
public import CatCryptCore.Quantum.QROM.CollisionWeight
public import CatCryptCore.Quantum.QROM.CompositePerTable
public import CatCryptCore.Quantum.QROM.DeltaStarLeLambda
public import CatCryptCore.Quantum.QROM.FindToGuessGeneral
public import CatCryptCore.Quantum.QROM.FindToGuess
public import CatCryptCore.Quantum.QROM.GenericSearchUniform
public import CatCryptCore.Quantum.QROM.HopChallengeKey
public import CatCryptCore.Quantum.QROM.HopCoinChallenge
public import CatCryptCore.Quantum.QROM.HopDecaps
public import CatCryptCore.Quantum.QROM.HopDecapsBijection
public import CatCryptCore.Quantum.QROM.HopDecapsNumeric
public import CatCryptCore.Quantum.QROM.HopDecapsNumericClose
public import CatCryptCore.Quantum.QROM.HopDecapsSharp
public import CatCryptCore.Quantum.QROM.HopDecapsSparse2
public import CatCryptCore.Quantum.QROM.HopJPrefix
public import CatCryptCore.Quantum.QROM.HopKeyFromCiphertext
public import CatCryptCore.Quantum.QROM.HopResampleGood
public import CatCryptCore.Quantum.QROM.KEMAdvNormalForm
public import CatCryptCore.Quantum.QROM.KEMAdvNormalFormMR
public import CatCryptCore.Quantum.QROM.KEMAdvGeneral
public import CatCryptCore.Quantum.QROM.KEMAdvDilate
public import CatCryptCore.Quantum.QROM.O2HGeneral
public import CatCryptCore.Quantum.QROM.MeasureReprogram
public import CatCryptCore.Quantum.QROM.FiatShamir
public import CatCryptCore.Quantum.QROM.Rewinding
public import CatCryptCore.Quantum.QROM.FiatShamirSigma
public import CatCryptCore.Quantum.QROM.CompressedOracle
public import CatCryptCore.Quantum.QROM.CompressedOracleLocal
public import CatCryptCore.Quantum.QROM.CPRun
public import CatCryptCore.Quantum.QROM.KEMGuessReduction
public import CatCryptCore.Quantum.QROM.KEMOwcpaReduction
public import CatCryptCore.Quantum.QROM.KEMQuantumGame
public import CatCryptCore.Quantum.QROM.KEMGameCP
public import CatCryptCore.Quantum.QROM.KWiseOracle
public import CatCryptCore.Quantum.QROM.MeasuredQueryRun
public import CatCryptCore.Quantum.QROM.MultiRound
public import CatCryptCore.Quantum.QROM.MultiRoundCoherent
public import CatCryptCore.Quantum.QROM.NormalFormPrefix
public import CatCryptCore.Quantum.QROM.NumericCorrectness
public import CatCryptCore.Quantum.QROM.O2HTheorem
public import CatCryptCore.Quantum.QROM.OracleRegisterProbe
public import CatCryptCore.Quantum.QROM.PermUnitaryCore
public import CatCryptCore.Quantum.QROM.OracleLaws
public import CatCryptCore.Quantum.QROM.OracleRegisterMixture
public import CatCryptCore.Quantum.QROM.PRFAdvEmbed
public import CatCryptCore.Quantum.QROM.QAdvGame
public import CatCryptCore.Quantum.QROM.QIndcpaAux
public import CatCryptCore.Quantum.QROM.QOwcpaAux
public import CatCryptCore.Quantum.QROM.QOwcpaAuxMeasured
public import CatCryptCore.Quantum.QROM.QuantumOWCPA
public import CatCryptCore.Quantum.QROM.QueryRoundAgreement
public import CatCryptCore.Quantum.QROM.QueryRoundDeferred
public import CatCryptCore.Quantum.QROM.QueryRoundPerms
public import CatCryptCore.Quantum.QROM.ResampleKeyHop
public import CatCryptCore.Quantum.QROM.RoundWeightDeferred
public import CatCryptCore.Quantum.QROM.SearchOffChallenge
public import CatCryptCore.Quantum.QROM.SemiClassicalOracle
public import CatCryptCore.Quantum.QROM.SparseSearch
public import CatCryptCore.Quantum.QROM.TTransformQROM
public import CatCryptCore.Quantum.QROM.PolyOracle
public import CatCryptCore.Quantum.QROM.PRFChain
public import CatCryptCore.Quantum.QROM.QMLWEAux

-- Machine types, the field Z/3329Z and the number-theoretic transform
public import CatCryptCore.Hax.CType
public import CatCryptCore.Crypto.Util.ZMod3329
public import CatCryptCore.Crypto.Lattice.Negacyclic
public import CatCryptCore.Crypto.Lattice.BitReversalGeneric
public import CatCryptCore.Crypto.Lattice.ConcreteNttRoots
public import CatCryptCore.Crypto.Lattice.CyclicConvolutionGeneric
public import CatCryptCore.Crypto.Lattice.DFTBijectionGeneric
public import CatCryptCore.Crypto.Lattice.NegacyclicTransformGeneric
public import CatCryptCore.Crypto.Lattice.NTTFullInversionGeneric
public import CatCryptCore.Crypto.Lattice.NTTInverseGeneric
public import CatCryptCore.Crypto.Lattice.NTTRecursionPass
public import CatCryptCore.Crypto.Lattice.SignedNegacyclicConv

-- ML-KEM (FIPS 203): specification, module-LWE PKE, and ML-KEM-512 IND-CCA in the QROM
public import CatCryptCore.Crypto.MLKEM.Compress
public import CatCryptCore.Crypto.MLKEM.Libcrux.RqAlgebra
public import CatCryptCore.Crypto.MLKEM.Spec.Coeffs
public import CatCryptCore.Crypto.MLKEM.Spec.Ntt
public import CatCryptCore.Crypto.MLKEM.ConcreteParams
public import CatCryptCore.Crypto.MLKEM.Infrastructure.FEL
public import CatCryptCore.Crypto.MLKEM.MLWE
public import CatCryptCore.Crypto.MLKEM.MLWE_PKE_Basic
public import CatCryptCore.Crypto.MLKEM.MLWE_PKE_Scheme
public import CatCryptCore.Crypto.MLKEM.MLWE_PKE_Stateful
public import CatCryptCore.Crypto.MLKEM.PKE_ROM
public import CatCryptCore.Crypto.MLKEM.FOFromMLWE
public import CatCryptCore.Crypto.MLKEM.Sampler
public import CatCryptCore.Crypto.MLKEM.SamplerCbd
public import CatCryptCore.Crypto.MLKEM.XOFMatrix
public import CatCryptCore.Crypto.MLKEM.CompressedPKE
public import CatCryptCore.Crypto.MLKEM.CorrectnessBounds
public import CatCryptCore.Crypto.MLKEM.MLKEM512Params
public import CatCryptCore.Crypto.MLKEM.MLKEM512Hypotheses
public import CatCryptCore.Crypto.MLKEM.MLKEM512FailureBound
public import CatCryptCore.Crypto.MLKEM.FIPS203QROMQuantumMLWE
public import CatCryptCore.Crypto.MLKEM.MLKEM512QROM
public import CatCryptCore.Crypto.MLKEM.MLKEM512QROMFinal
public import CatCryptCore.Crypto.MLKEM.CollisionSpreadLemmas
public import CatCryptCore.Crypto.MLKEM.CollisionSpreadBound
public import CatCryptCore.Crypto.MLKEM.MLKEM512QROMNumeric
public import CatCryptCore.Crypto.MLKEM.PRFOracle
public import CatCryptCore.Crypto.MLKEM.PRFAuxHop
public import CatCryptCore.Crypto.MLKEM.PRFBadTable
public import CatCryptCore.Crypto.MLKEM.PRFBadTableKeyed
public import CatCryptCore.Crypto.MLKEM.PRFCoinWeak
public import CatCryptCore.Crypto.MLKEM.PRFInstance512
public import CatCryptCore.Crypto.MLKEM.PRFKEMChain
public import CatCryptCore.Crypto.MLKEM.PRFMLWE
public import CatCryptCore.Crypto.MLKEM.MLKEM512QROMPrf
public import CatCryptCore.Crypto.MLKEM.CollisionSpreadIdeal

-- UC ideal functionalities (F_commit, F_ZK, F_OT) + shared group scaffolding
public import CatCryptCore.Examples.GroupParam
public import CatCryptCore.Crypto.Commitment.PedersenUC
public import CatCryptCore.Crypto.ZK.SigmaUCZK
public import CatCryptCore.Crypto.ZK.LinearSigmaUC
public import CatCryptCore.Crypto.OT.DualModeOT

-- Transparent functionalities, hybrid composition, the clock and the network
public import CatCryptCore.Crypto.UCTransparent
public import CatCryptCore.Crypto.UCTransparentHybrid
public import CatCryptCore.Crypto.UCTransparentAdv
public import CatCryptCore.Crypto.UCTransparentExample
public import CatCryptCore.Crypto.UCClockNetworkDet
public import CatCryptCore.Crypto.UCClockNetwork

-- Ethereum proof-of-stake consensus: Casper FFG, PoS-NSB, finality layers, the UC stack
public import CatCryptCore.Prob.Concentration
public import CatCryptCore.Consensus.FFG
public import CatCryptCore.Consensus.FFGExamples
public import CatCryptCore.Consensus.FFGDynamic
public import CatCryptCore.Consensus.FFGDynamicExamples
public import CatCryptCore.Consensus.Finality
public import CatCryptCore.Consensus.FinalityExamples
public import CatCryptCore.Consensus.FinalityValidity
public import CatCryptCore.Consensus.FinalityUpdated
public import CatCryptCore.Consensus.FinalityUpdatedProb
public import CatCryptCore.Consensus.PoSNSB.Model
public import CatCryptCore.Consensus.PoSNSB.Steps
public import CatCryptCore.Consensus.PoSNSB.Invariants
public import CatCryptCore.Consensus.PoSNSB.TreeChain
public import CatCryptCore.Consensus.PoSNSB.ChainGrowth
public import CatCryptCore.Consensus.PoSNSB.ChainQualityPrelims
public import CatCryptCore.Consensus.PoSNSB.ChainQuality
public import CatCryptCore.Consensus.PoSNSB.ChainQualityTip
public import CatCryptCore.Consensus.PoSNSB.CommonPrefixPrelims
public import CatCryptCore.Consensus.PoSNSB.CommonPrefix
public import CatCryptCore.Consensus.PoSNSB.Prob.Hash
public import CatCryptCore.Consensus.PoSNSB.Prob.Slots
public import CatCryptCore.Consensus.PoSNSB.Prob.Protocol
public import CatCryptCore.Consensus.PoSNSB.Prob.Reduction
public import CatCryptCore.Consensus.PoSNSB.Prob.Collision
public import CatCryptCore.Consensus.PoSNSB.Prob
public import CatCryptCore.Consensus.PoSNSB.Prob.Time
public import CatCryptCore.Consensus.PoSNSB.Prob.ROM
public import CatCryptCore.Consensus.PoSNSB.Prob.Uniform
public import CatCryptCore.Consensus.PoSNSB.Prob.Erasure
public import CatCryptCore.Consensus.PoSNSB.Prob.Script
public import CatCryptCore.Consensus.PoSNSB.ProbExamples
public import CatCryptCore.Consensus.UC.FTree
public import CatCryptCore.Consensus.UC.FinalityGadget
public import CatCryptCore.Consensus.UC.FinalityLive
public import CatCryptCore.Consensus.UC.Finality
public import CatCryptCore.Consensus.UC.Chain
public import CatCryptCore.Consensus.UC.ChainEnv
public import CatCryptCore.Consensus.UC.ChainEnvRealize
public import CatCryptCore.Consensus.UC.StackEnv
public import CatCryptCore.Consensus.UC.ChainEnvROM
public import CatCryptCore.Consensus.UC.Stack
public import CatCryptCore.Consensus.UC.StackExamples

-- Classical curve mathematics
public import CatCryptCore.Crypto.KeyAgreement.MontgomeryLadder
public import CatCryptCore.Crypto.KeyAgreement.MontgomeryAsWeierstrass
public import CatCryptCore.Crypto.KeyAgreement.MontgomeryXOnly
public import CatCryptCore.Crypto.KeyAgreement.Curve25519
public import CatCryptCore.Examples.DeepHybrid
public import CatCryptCore.Examples.OneTimePad
public import CatCryptCore.Examples.ReflectTacticDemo
public import CatCryptCore.Examples.OT
public import CatCryptCore.Examples.PRF
public import CatCryptCore.Examples.PRFTimed
public import CatCryptCore.Examples.PRFMAC
public import CatCryptCore.Examples.PRFMACTimed
public import CatCryptCore.Examples.PRFPRG
public import CatCryptCore.Examples.PRG
public import CatCryptCore.Examples.Sigma
public import CatCryptCore.Examples.PKE.Scheme
public import CatCryptCore.Examples.PKE.OneToMany
public import CatCryptCore.Examples.PKE.MultiInstance
public import CatCryptCore.Examples.Cryptobox.Scheme
public import CatCryptCore.Examples.Cryptobox.KEY
public import CatCryptCore.Examples.Cryptobox.PKEY
public import CatCryptCore.Examples.Cryptobox.PKEYQ
public import CatCryptCore.Examples.Cryptobox.SAE
public import CatCryptCore.Examples.Cryptobox.NIKE
public import CatCryptCore.Examples.Cryptobox.PKAE
public import CatCryptCore.Examples.Cryptobox.AE
public import CatCryptCore.Examples.Cryptobox.Cryptobox
public import CatCryptCore.Examples.Cryptobox.GameHopping
public import CatCryptCore.Examples.Cryptobox.HYBRID
public import CatCryptCore.Examples.Commitments.CommitmentScheme
public import CatCryptCore.Examples.Commitments.PolyCommitScheme
public import CatCryptCore.Examples.Commitments.KZG.Def
public import CatCryptCore.Examples.Commitments.KZG.KnowledgeSoundness
public import CatCryptCore.Examples.Commitments.Pedersen
public import CatCryptCore.Examples.EncryptThenMAC
public import CatCryptCore.Examples.BasicHash
public import CatCryptCore.Examples.KEMDEM
public import CatCryptCore.Examples.Schnorr
public import CatCryptCore.Examples.ElGamal
public import CatCryptCore.Examples.MAC
public import CatCryptCore.Examples.SecretSharing
public import CatCryptCore.Examples.ShamirSecretSharing
public import CatCryptCore.Examples.Commitment
public import CatCryptCore.Examples.CPAFromPRF
public import CatCryptCore.Examples.EtMCCA
public import CatCryptCore.Examples.CTRMode
public import CatCryptCore.Examples.CBCMode
public import CatCryptCore.Examples.DiffieHellman
public import CatCryptCore.Examples.CyclicGroupDDH
public import CatCryptCore.Examples.CyclicGroupModule
public import CatCryptCore.Examples.HashedElGamal
public import CatCryptCore.Examples.ChaumPedersen
public import CatCryptCore.Examples.UniversalHash
public import CatCryptCore.Examples.DetCPA
public import CatCryptCore.Examples.CoinToss
public import CatCryptCore.Examples.INDCPA
public import CatCryptCore.Examples.ElGamalDDH
public import CatCryptCore.Examples.ElGamalUCConcrete
public import CatCryptCore.Crypto.Assumptions.OWFTimed
public import CatCryptCore.Crypto.BLSSig.SecurityTimed
public import CatCryptCore.Crypto.Commitment.PedersenUCTimed
public import CatCryptCore.Crypto.GeneralForkingLemmaTimed
public import CatCryptCore.Crypto.OT.DualModeOTTimed
public import CatCryptCore.Crypto.OT.GamesTimed
public import CatCryptCore.Crypto.OTExtension.IKNPTimed
public import CatCryptCore.Crypto.ZK.SigmaUCZKTimed
public import CatCryptCore.Examples.CBCModeTimed
public import CatCryptCore.Examples.CPAFromPRFTimed
public import CatCryptCore.Examples.DiffieHellmanTimed
public import CatCryptCore.Examples.ElGamalDDHTimed
public import CatCryptCore.Examples.ElGamalTimed
public import CatCryptCore.Examples.HashedElGamalTimed
public import CatCryptCore.Examples.KEMDEMTimed
public import CatCryptCore.Examples.OTTimed
public import CatCryptCore.Examples.PRGTimed

/-! # CatCrypt Core — umbrella

Top-level entry point for the minimal-basis release. Re-exports the
program-logic + package-algebra stack, native forking lemmas, and the classical
Montgomery-curve and X25519 mathematics. VCVio / ArkLib interoperability is not
part of this basis — it lives in the separate `catcrypt-vcvio` / `catcrypt-arklib`
packages built on top of core. -/

@[expose] public section