Documentation
VCVio
Search
return to top
source
Imports
Init
VCVio.Prelude
VCVio.CryptoFoundations.CommitmentScheme
VCVio.CryptoFoundations.DataEncapMech
VCVio.CryptoFoundations.Fischlin
VCVio.CryptoFoundations.FujisakiOkamoto
VCVio.CryptoFoundations.GPVHashAndSign
VCVio.CryptoFoundations.HashCommitment
VCVio.CryptoFoundations.IdenSchemeWithAbort
VCVio.CryptoFoundations.KEMDEM
VCVio.CryptoFoundations.KeyEncapMech
VCVio.CryptoFoundations.MacAlg
VCVio.CryptoFoundations.MacFromPRF
VCVio.CryptoFoundations.PRF
VCVio.CryptoFoundations.PRG
VCVio.CryptoFoundations.ReplayFork
VCVio.CryptoFoundations.ReplayForkStdDo
VCVio.CryptoFoundations.SecExp
VCVio.CryptoFoundations.SeededFork
VCVio.CryptoFoundations.SigmaProtocol
VCVio.CryptoFoundations.SignatureAlg
VCVio.CryptoFoundations.SymmEncAlg
VCVio.EvalDist.BitVec
VCVio.EvalDist.Bool
VCVio.EvalDist.Fintype
VCVio.EvalDist.Inequalities
VCVio.EvalDist.List
VCVio.EvalDist.Option
VCVio.EvalDist.Prod
VCVio.EvalDist.RenyiDivergence
VCVio.EvalDist.TVDist
VCVio.OracleComp.EvalDist
VCVio.OracleComp.FinRatPMF
VCVio.OracleComp.OracleComp
VCVio.OracleComp.OracleContext
VCVio.OracleComp.OracleQuery
VCVio.OracleComp.OracleSpec
VCVio.OracleComp.ProbComp
VCVio.OracleComp.ProbCompLift
VCVio.OracleComp.QueryTracking
VCVio.OracleComp.RunIO
VCVio.OracleComp.Traversal
VCVio.ProgramLogic.Notation
VCVio.ProgramLogic.NotationCore
VCVio.ProgramLogic.SeededFork
VCVio.ProgramLogic.Tactics
VCVio.StateSeparating.Advantage
VCVio.StateSeparating.CellRef
VCVio.StateSeparating.DistEquiv
VCVio.StateSeparating.Hybrid
VCVio.StateSeparating.IdenticalUntilBad
VCVio.StateSeparating.IndistAt
VCVio.CryptoFoundations.AsymmEncAlg.Defs
VCVio.CryptoFoundations.AsymmEncAlg.INDCCA
VCVio.CryptoFoundations.AsymmEncAlg.INDCPA
VCVio.CryptoFoundations.Asymptotics.Negligible
VCVio.CryptoFoundations.Asymptotics.ReductionCost
VCVio.CryptoFoundations.Asymptotics.Security
VCVio.CryptoFoundations.FiatShamir.QueryBounds
VCVio.CryptoFoundations.FiatShamir.Sigma
VCVio.CryptoFoundations.FiatShamir.WithAbort
VCVio.CryptoFoundations.FujisakiOkamoto.Composed
VCVio.CryptoFoundations.FujisakiOkamoto.Defs
VCVio.CryptoFoundations.FujisakiOkamoto.TTransform
VCVio.CryptoFoundations.FujisakiOkamoto.UTransform
VCVio.CryptoFoundations.HardnessAssumptions.CollisionResistance
VCVio.CryptoFoundations.HardnessAssumptions.DiffieHellman
VCVio.CryptoFoundations.HardnessAssumptions.EntropySmoothing
VCVio.CryptoFoundations.HardnessAssumptions.HardRelation
VCVio.CryptoFoundations.HardnessAssumptions.OneWay
VCVio.EvalDist.Defs.AlternativeMonad
VCVio.EvalDist.Defs.Basic
VCVio.EvalDist.Defs.Instances
VCVio.EvalDist.Defs.NeverFails
VCVio.EvalDist.Defs.Semantics
VCVio.EvalDist.Defs.Support
VCVio.EvalDist.Instances.ErrorT
VCVio.EvalDist.Instances.FinRatPMF
VCVio.EvalDist.Instances.OptionT
VCVio.EvalDist.Instances.ReaderT
VCVio.EvalDist.Monad.Basic
VCVio.EvalDist.Monad.Disagreement
VCVio.EvalDist.Monad.Map
VCVio.EvalDist.Monad.Seq
VCVio.Interaction.UC.AsyncRuntime
VCVio.Interaction.UC.AsyncSecurity
VCVio.Interaction.UC.Computational
VCVio.Interaction.UC.Runtime
VCVio.Interaction.UC.Standard
VCVio.Interaction.UC.StdDoBridge
VCVio.OracleComp.Coercions.Add
VCVio.OracleComp.Coercions.SubSpec
VCVio.OracleComp.Coinductive.Bridge
VCVio.OracleComp.Constructions.BitVec
VCVio.OracleComp.Constructions.GenerateSeed
VCVio.OracleComp.Constructions.Replicate
VCVio.OracleComp.Constructions.SampleableType
VCVio.OracleComp.HasQuery.Basic
VCVio.OracleComp.HasQuery.Morphism
VCVio.OracleComp.QueryTracking.Birthday
VCVio.OracleComp.QueryTracking.CachingLoggingOracle
VCVio.OracleComp.QueryTracking.CachingOracle
VCVio.OracleComp.QueryTracking.Collision
VCVio.OracleComp.QueryTracking.CostModel
VCVio.OracleComp.QueryTracking.CountingOracle
VCVio.OracleComp.QueryTracking.Enforcement
VCVio.OracleComp.QueryTracking.HandlerSimp
VCVio.OracleComp.QueryTracking.Iter
VCVio.OracleComp.QueryTracking.LoggingOracle
VCVio.OracleComp.QueryTracking.ObservationOracle
VCVio.OracleComp.QueryTracking.ProgrammingOracle
VCVio.OracleComp.QueryTracking.QueryBound
VCVio.OracleComp.QueryTracking.QueryCost
VCVio.OracleComp.QueryTracking.ResourceProfile
VCVio.OracleComp.QueryTracking.SeededOracle
VCVio.OracleComp.QueryTracking.Structures
VCVio.OracleComp.QueryTracking.SubSpec
VCVio.OracleComp.QueryTracking.Tracing
VCVio.OracleComp.QueryTracking.Unpredictability
VCVio.OracleComp.QueryTracking.WriterCost
VCVio.OracleComp.SimSemantics.Append
VCVio.OracleComp.SimSemantics.SimulateQ
VCVio.ProgramLogic.Relational.Basic
VCVio.ProgramLogic.Relational.Examples
VCVio.ProgramLogic.Relational.FromUnary
VCVio.ProgramLogic.Relational.HandlerFromUnary
VCVio.ProgramLogic.Relational.Leakage
VCVio.ProgramLogic.Relational.ProgrammingOracle
VCVio.ProgramLogic.Relational.Quantitative
VCVio.ProgramLogic.Relational.QuantitativeDefs
VCVio.ProgramLogic.Relational.SimulateQ
VCVio.ProgramLogic.Tactics.Common
VCVio.ProgramLogic.Tactics.Handler
VCVio.ProgramLogic.Tactics.Relational
VCVio.ProgramLogic.Tactics.Unary
VCVio.ProgramLogic.Unary.Examples
VCVio.ProgramLogic.Unary.HandlerSpecs
VCVio.ProgramLogic.Unary.HoarePropTriple
VCVio.ProgramLogic.Unary.HoareTriple
VCVio.ProgramLogic.Unary.SimulateQ
VCVio.ProgramLogic.Unary.StdDoBridge
VCVio.ProgramLogic.Unary.StdDoExamples
VCVio.ProgramLogic.Unary.WriterTBridge
VCVio.CryptoFoundations.AsymmEncAlg.INDCPA.GenericLift
VCVio.CryptoFoundations.AsymmEncAlg.INDCPA.OneTime
VCVio.CryptoFoundations.AsymmEncAlg.INDCPA.Oracle
VCVio.CryptoFoundations.FiatShamir.Sigma.CmaToNma
VCVio.CryptoFoundations.FiatShamir.Sigma.Fork
VCVio.CryptoFoundations.FiatShamir.Sigma.Reductions
VCVio.CryptoFoundations.FiatShamir.Sigma.Security
VCVio.CryptoFoundations.FiatShamir.WithAbort.Cost
VCVio.CryptoFoundations.FiatShamir.WithAbort.ExpectedCost
VCVio.CryptoFoundations.FiatShamir.WithAbort.Security
VCVio.CryptoFoundations.MerkleTree.Inductive.Binding
VCVio.CryptoFoundations.MerkleTree.Inductive.Completeness
VCVio.CryptoFoundations.MerkleTree.Inductive.Defs
VCVio.CryptoFoundations.MerkleTree.Inductive.Extractability
VCVio.CryptoFoundations.MerkleTree.Inductive.QueryBound
VCVio.CryptoFoundations.MerkleTree.Inductive.Uniqueness
VCVio.CryptoFoundations.MerkleTree.Vector.Completeness
VCVio.CryptoFoundations.MerkleTree.Vector.Defs
VCVio.OracleComp.QueryTracking.RandomOracle.Basic
VCVio.OracleComp.QueryTracking.RandomOracle.Eager
VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable
VCVio.OracleComp.QueryTracking.RandomOracle.Simulation
VCVio.OracleComp.SimSemantics.OptionT.Basic
VCVio.OracleComp.SimSemantics.QueryImpl.Basic
VCVio.OracleComp.SimSemantics.QueryImpl.Constructions
VCVio.OracleComp.SimSemantics.ReaderT.Basic
VCVio.OracleComp.SimSemantics.StateT.Basic
VCVio.OracleComp.SimSemantics.StateT.BundledSemantics
VCVio.OracleComp.SimSemantics.StateT.PreservesInv
VCVio.OracleComp.SimSemantics.StateT.StateProjection
VCVio.OracleComp.SimSemantics.StateT.StateSeparating
VCVio.OracleComp.SimSemantics.WriterT.Basic
VCVio.OracleComp.SimSemantics.WriterT.PreservesInv
VCVio.ProgramLogic.Relational.Loom.Coherence
VCVio.ProgramLogic.Relational.Loom.Probabilistic
VCVio.ProgramLogic.Relational.Loom.Qualitative
VCVio.ProgramLogic.Relational.Loom.Quantitative
VCVio.ProgramLogic.Tactics.Common.Backward
VCVio.ProgramLogic.Tactics.Common.Core
VCVio.ProgramLogic.Tactics.Common.Naming
VCVio.ProgramLogic.Tactics.Common.Registry
VCVio.ProgramLogic.Tactics.Common.SpecIR
VCVio.ProgramLogic.Tactics.Common.Suggestions
VCVio.ProgramLogic.Tactics.Common.WpStepDispatch
VCVio.ProgramLogic.Tactics.Common.WpStepRegistry
VCVio.ProgramLogic.Tactics.Relational.Internals
VCVio.ProgramLogic.Tactics.Unary.Internals
VCVio.ProgramLogic.Unary.Loom.Coherence
VCVio.ProgramLogic.Unary.Loom.Probabilistic
VCVio.ProgramLogic.Unary.Loom.Qualitative
VCVio.ProgramLogic.Unary.Loom.Quantitative
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Bridge
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Chain
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Compatibility
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Games
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Hops
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.SimpAttr
VCVio.CryptoFoundations.FiatShamir.Sigma.Stateful.Spec
Imported by