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.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.Map
VCVio.EvalDist.Monad.Seq
VCVio.Interaction.Basic.Append
VCVio.Interaction.Basic.BundledMonad
VCVio.Interaction.Basic.Chain
VCVio.Interaction.Basic.Decoration
VCVio.Interaction.Basic.Interaction
VCVio.Interaction.Basic.MonadDecoration
VCVio.Interaction.Basic.Node
VCVio.Interaction.Basic.Ownership
VCVio.Interaction.Basic.Replicate
VCVio.Interaction.Basic.Sampler
VCVio.Interaction.Basic.Shape
VCVio.Interaction.Basic.Spec
VCVio.Interaction.Basic.SpecFintype
VCVio.Interaction.Basic.StateChain
VCVio.Interaction.Basic.Strategy
VCVio.Interaction.Basic.Syntax
VCVio.Interaction.Concurrent.Bisimulation
VCVio.Interaction.Concurrent.Control
VCVio.Interaction.Concurrent.Current
VCVio.Interaction.Concurrent.Equivalence
VCVio.Interaction.Concurrent.Examples
VCVio.Interaction.Concurrent.Execution
VCVio.Interaction.Concurrent.Fairness
VCVio.Interaction.Concurrent.Frontier
VCVio.Interaction.Concurrent.Independence
VCVio.Interaction.Concurrent.Interleaving
VCVio.Interaction.Concurrent.Liveness
VCVio.Interaction.Concurrent.Machine
VCVio.Interaction.Concurrent.Observation
VCVio.Interaction.Concurrent.Policy
VCVio.Interaction.Concurrent.Process
VCVio.Interaction.Concurrent.Profile
VCVio.Interaction.Concurrent.Refinement
VCVio.Interaction.Concurrent.Run
VCVio.Interaction.Concurrent.Spec
VCVio.Interaction.Concurrent.Trace
VCVio.Interaction.Concurrent.Tree
VCVio.Interaction.Multiparty.Broadcast
VCVio.Interaction.Multiparty.Core
VCVio.Interaction.Multiparty.Directed
VCVio.Interaction.Multiparty.Examples
VCVio.Interaction.Multiparty.Observation
VCVio.Interaction.Multiparty.ObservationProfile
VCVio.Interaction.Multiparty.Profile
VCVio.Interaction.TwoParty.Compose
VCVio.Interaction.TwoParty.Decoration
VCVio.Interaction.TwoParty.Examples
VCVio.Interaction.TwoParty.Refine
VCVio.Interaction.TwoParty.Role
VCVio.Interaction.TwoParty.Strategy
VCVio.Interaction.TwoParty.Swap
VCVio.Interaction.UC.AsyncRuntime
VCVio.Interaction.UC.AsyncSecurity
VCVio.Interaction.UC.Computational
VCVio.Interaction.UC.CorruptionModel
VCVio.Interaction.UC.Emulates
VCVio.Interaction.UC.EnvAction
VCVio.Interaction.UC.EnvOpenProcess
VCVio.Interaction.UC.Interface
VCVio.Interaction.UC.Leakage
VCVio.Interaction.UC.MachineId
VCVio.Interaction.UC.MomentaryCorruption
VCVio.Interaction.UC.Notation
VCVio.Interaction.UC.OpenProcess
VCVio.Interaction.UC.OpenProcessModel
VCVio.Interaction.UC.OpenTheory
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.BundledSemantics
VCVio.OracleComp.SimSemantics.Constructions
VCVio.OracleComp.SimSemantics.PreservesInv
VCVio.OracleComp.SimSemantics.QueryImpl
VCVio.OracleComp.SimSemantics.ReaderT
VCVio.OracleComp.SimSemantics.SimulateQ
VCVio.OracleComp.SimSemantics.StateProjection
VCVio.OracleComp.SimSemantics.StateSeparating
VCVio.OracleComp.SimSemantics.StateT
VCVio.OracleComp.SimSemantics.WriterT
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.Completeness
VCVio.CryptoFoundations.MerkleTree.Inductive.Defs
VCVio.CryptoFoundations.MerkleTree.Vector.Basic
VCVio.Interaction.UC.OpenSyntax.Expr
VCVio.Interaction.UC.OpenSyntax.Interp
VCVio.Interaction.UC.OpenSyntax.Raw
VCVio.OracleComp.QueryTracking.RandomOracle.Basic
VCVio.OracleComp.QueryTracking.RandomOracle.Eager
VCVio.OracleComp.QueryTracking.RandomOracle.Simulation
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