-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy path_CoqProject
80 lines (75 loc) · 3.19 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
-R _build/default/src Verse
_build/default/src/Verse.v
_build/default/src/Verse/AnnotatedCode.v
_build/default/src/Verse/Ast.v
# _build/default/src/Verse/CoarseMeta.v
_build/default/src/Verse/Error.v
_build/default/src/Verse/FFI/Raaz.v
_build/default/src/Verse/FFI/Raaz/Target/C.v
_build/default/src/Verse/HlistMachine.v
_build/default/src/Verse/Language.v
_build/default/src/Verse/Language/Macros.v
_build/default/src/Verse/Language/Macros/BitOps.v
_build/default/src/Verse/Language/Macros/Cache.v
_build/default/src/Verse/Language/Macros/Loops.v
_build/default/src/Verse/Language/Pretty.v
_build/default/src/Verse/Language/Types.v
_build/default/src/Verse/Monad.v
_build/default/src/Verse/Machine/BitVector.v
_build/default/src/Verse/BitVector.v
_build/default/src/Verse/BitVector/Facts.v
_build/default/src/Verse/BitVector/ArithRing.v
_build/default/src/Verse/ModularCode.v
_build/default/src/Verse/Monoid.v
_build/default/src/Verse/Monoid/Interface.v
_build/default/src/Verse/Monoid/PList.v
_build/default/src/Verse/Monoid/Semantics.v
_build/default/src/Verse/NFacts.v
_build/default/src/Verse/Nibble.v
_build/default/src/Verse/Print.v
_build/default/src/Verse/ProofTac.v
_build/default/src/Verse/Scope.v
# _build/default/src/Verse/ScopeStore.v
_build/default/src/Verse/Target.v
_build/default/src/Verse/Target/C.v
_build/default/src/Verse/Target/C/Ast.v
_build/default/src/Verse/Target/C/CodeGen.v
_build/default/src/Verse/Target/C/Pretty.v
_build/default/src/Verse/TypeSystem.v
########################################
## CryptoLib: Actual implementations ##
########################################
_build/default/src/Verse/TestCode/AnnotatedCode.v
_build/default/src/Verse/TestCode/TestCall.v
_build/default/src/Verse/TestCode/TestSemantics.v
_build/default/src/Verse/CryptoLib/blake2.v
_build/default/src/Verse/CryptoLib/blake2/c/portable.v
_build/default/src/Verse/CryptoLib/blake2b/c/portable.v
_build/default/src/Verse/CryptoLib/blake2s/c/portable.v
_build/default/src/Verse/CryptoLib/chacha20/common.v
_build/default/src/Verse/CryptoLib/chacha20/c/portable.v
_build/default/src/Verse/CryptoLib/curve25519/c/portable.v
_build/default/src/Verse/CryptoLib/curve25519/c/field.v
_build/default/src/Verse/CryptoLib/poly1305/c/portable.v
_build/default/src/Verse/CryptoLib/sha2.v
_build/default/src/Verse/CryptoLib/sha2/c/portable.v
# _build/default/src/Verse/CryptoLib/sha2/c/portableAlternate.v
# _build/default/src/Verse/CryptoLib/sha2/c/portableAnnotated.v
_build/default/src/Verse/CryptoLib/sha256/c/portable.v
_build/default/src/Verse/CryptoLib/sha512/c/portable.v
# _build/default/src/Verse/Word.v
# _build/default/src/Verse/CoLoR_VecUtil.v
# _build/default/src/Verse/Tutorial.v
# _build/default/src/Verse/Language/Operators.v
# _build/default/src/Verse/Language/Utils.v
# _build/default/src/Verse/Word.v
# _build/default/src/Verse/WordFacts.v
# _build/default/src/Verse/NFacts.v
# _build/default/src/Verse/WordRing.v
# _build/default/src/Verse/DecFacts.v
# _build/default/src/Verse/Semantics/Store.v
# _build/default/src/Verse/Semantics.v
# _build/default/src/Verse/Semantics/NSemantics.v
# _build/default/src/Verse/Semantics/ScopeStore.v
# _build/default/src/Verse/Semantics/FunctionStore.v
# _build/default/src/Verse/TestCode/TestSemantics.v