-
Notifications
You must be signed in to change notification settings - Fork 9
/
_CoqProject
105 lines (92 loc) · 3.61 KB
/
_CoqProject
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
-Q theories SSProve
theories/Mon/Base.v
theories/Mon/SPropBase.v
theories/Mon/SPropMonadicStructures.v
theories/Mon/Monoid.v
theories/Mon/MonadExamples.v
theories/Mon/SpecificationMonads.v
theories/Mon/DijkstraMonadExamples.v
theories/Mon/FiniteProbabilities.v
theories/Relational/Category.v
theories/Relational/RelativeMonads.v
theories/Relational/EnrichedSetting.v
theories/Relational/Rel.v
theories/Relational/OrderEnrichedCategory.v
theories/Relational/OrderEnrichedRelativeMonadExamples.v
theories/Relational/GenericRulesSimple.v
theories/Relational/Commutativity.v
theories/Crypt/Prelude.v
theories/Crypt/Axioms.v
theories/Crypt/Casts.v
theories/Crypt/choice_type.v
# Categorical semantics
theories/Crypt/rhl_semantics/ChoiceAsOrd.v
theories/Crypt/rhl_semantics/more_categories/RelativeMonadMorph_prod.v
theories/Crypt/rhl_semantics/more_categories/LaxComp.v
theories/Crypt/rhl_semantics/more_categories/OrderEnrichedRelativeAdjunctions.v
theories/Crypt/rhl_semantics/more_categories/LaxFunctorsAndTransf.v
theories/Crypt/rhl_semantics/more_categories/LaxMorphismOfRelAdjunctions.v
theories/Crypt/rhl_semantics/more_categories/TransformingLaxMorph.v
theories/Crypt/rhl_semantics/more_categories/InitialRelativeMonad.v
theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v
theories/Crypt/rhl_semantics/free_monad/UniversalFreeMap.v
theories/Crypt/rhl_semantics/only_prob/SubDistr.v
theories/Crypt/rhl_semantics/only_prob/Couplings.v
theories/Crypt/rhl_semantics/only_prob/Theta_dens.v
theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v
theories/Crypt/rhl_semantics/only_prob/ThetaDex.v
theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v
theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v
theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v
#theories/Crypt/rhl_semantics/state_prob/LiftStateful.v
# Prob rules
theories/Crypt/rules/RulesProb.v
# Crypto
theories/Crypt/rules/UniformDistrLemmas.v
#theories/Crypt/rules/UniformDistr.v
# theories/Crypt/examples/deprecated/otp.v
theories/Crypt/package/pkg_core_definition.v
theories/Crypt/package/pkg_composition.v
theories/Crypt/package/pkg_notation.v
theories/Crypt/package/pkg_tactics.v
theories/Crypt/package/pkg_heap.v
theories/Crypt/package/pkg_semantics.v
theories/Crypt/package/pkg_lookup.v
theories/Crypt/package/pkg_advantage.v
theories/Crypt/package/pkg_invariants.v
theories/Crypt/package/pkg_distr.v
theories/Crypt/package/pkg_rhl.v
theories/Crypt/package/pkg_user_util.v
theories/Crypt/package/pkg_interpreter.v
theories/Crypt/Package.v
# State + Prob
theories/Crypt/rules/RulesStateProb.v
theories/Crypt/rules/UniformStateProb.v
#std. distributions
# theories/Crypt/only_prob/SymmetricSchemeStateProbStdDistr.v
# Examples
theories/Crypt/examples/package_usage_example.v
theories/Crypt/examples/interpreter_test.v
theories/Crypt/examples/concrete_groups.v
theories/Crypt/examples/PRF.v
theories/Crypt/examples/AsymScheme.v
theories/Crypt/examples/DDH.v
theories/Crypt/examples/ElGamal.v
theories/Crypt/examples/OTP.v
theories/Crypt/examples/KEMDEM.v
theories/Crypt/examples/RandomOracle.v
theories/Crypt/examples/SigmaProtocol.v
theories/Crypt/examples/Schnorr.v
# theories/Crypt/examples/OVN.v
theories/Crypt/examples/Executor.v
# Examples from https://github.com/Som1Lse/joy-of-ssprove
theories/Crypt/examples/MACCCA.v
theories/Crypt/examples/PRFMAC.v
theories/Crypt/examples/PRFPRG.v
theories/Crypt/examples/PRPCCA.v
theories/Crypt/examples/SecretSharing.v
theories/Crypt/examples/ShamirSecretSharing.v
theories/Crypt/examples/StretchPRG.v
theories/Crypt/examples/SymmRatchet.v
# Printing the axioms of all results from the paper
theories/Crypt/Main.v