-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathVCVio.lean
50 lines (50 loc) · 2.32 KB
/
VCVio.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
import VCVio.CryptoFoundations.AsymmEncAlg
import VCVio.CryptoFoundations.Asymptotics.Negligible
import VCVio.CryptoFoundations.Asymptotics.PolyTimeOC
import VCVio.CryptoFoundations.FiatShamir
import VCVio.CryptoFoundations.Fork
import VCVio.CryptoFoundations.HardnessAssumptions.DiffieHellman
import VCVio.CryptoFoundations.HardnessAssumptions.HardHomogeneousSpace
import VCVio.CryptoFoundations.HardnessAssumptions.HardRelation
import VCVio.CryptoFoundations.SecExp
import VCVio.CryptoFoundations.SigmaAlg
import VCVio.CryptoFoundations.SignatureAlg
import VCVio.CryptoFoundations.SymmEncAlg
import VCVio.OracleComp.Coercions.Append
import VCVio.OracleComp.Coercions.HasUnifSelect
import VCVio.OracleComp.Coercions.SimOracle
import VCVio.OracleComp.Coercions.SubSpec
import VCVio.OracleComp.Constructions.GenerateSeed
import VCVio.OracleComp.Constructions.Replicate
import VCVio.OracleComp.Constructions.UniformSelect
import VCVio.OracleComp.DistSemantics.ActiveOracles
import VCVio.OracleComp.DistSemantics.Alternative
import VCVio.OracleComp.DistSemantics.BitVec
import VCVio.OracleComp.DistSemantics.EvalDist
import VCVio.OracleComp.DistSemantics.HEq
import VCVio.OracleComp.DistSemantics.List
import VCVio.OracleComp.DistSemantics.Prod
import VCVio.OracleComp.DistSemantics.Seq
import VCVio.OracleComp.DistSemantics.Simulate
import VCVio.OracleComp.DistSemantics.Support
import VCVio.OracleComp.NoFailure
import VCVio.OracleComp.OracleComp
import VCVio.OracleComp.OracleImpl
import VCVio.OracleComp.OracleSpec
import VCVio.OracleComp.QueryBound
import VCVio.OracleComp.RunIO
import VCVio.OracleComp.SimSemantics.Append
import VCVio.OracleComp.SimSemantics.Constructions
import VCVio.OracleComp.SimSemantics.IsTracking
import VCVio.OracleComp.SimSemantics.QueryTracking.CachingOracle
import VCVio.OracleComp.SimSemantics.QueryTracking.CountingOracle
import VCVio.OracleComp.SimSemantics.QueryTracking.LoggingOracle
import VCVio.OracleComp.SimSemantics.QueryTracking.RandOracle
import VCVio.OracleComp.SimSemantics.QueryTracking.SeededOracle
import VCVio.OracleComp.SimSemantics.Simulate
import VCVio.OracleComp.SimSemantics.Transformers.WriterT
import VCVio.OracleComp.SimSemantics.UntilSwap
import VCVio.ProgramLogic.Relational.Basic
import VCVio.ProgramLogic.Unary.DijkstraMonad
import VCVio.ProgramLogic.Unary.Examples
import VCVio.ProgramLogic.Unary.HoareTriple