index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Mode
Name
Size
-rw-r--r--
AbstractInterpretation.v
56732
log
plain
-rw-r--r--
AbstractInterpretationProofs.v
84566
log
plain
-rw-r--r--
AbstractInterpretationWf.v
57561
log
plain
-rw-r--r--
AbstractInterpretationZRangeProofs.v
37317
log
plain
d---------
Algebra
381
log
plain
d---------
Arithmetic
703
log
plain
-rw-r--r--
BoundsPipeline.v
30988
log
plain
-rw-r--r--
CLI.v
21193
log
plain
-rw-r--r--
COperationSpecifications.v
23116
log
plain
-rw-r--r--
CStringification.v
134903
log
plain
-rw-r--r--
CompilersTestCases.v
13927
log
plain
d---------
Curves
109
log
plain
-rw-r--r--
Demo.v
9935
log
plain
d---------
ExtractionHaskell
149
log
plain
d---------
ExtractionOCaml
149
log
plain
d---------
Fancy
189
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypes.v
193248
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypesProofs.v
8920
log
plain
-rw-r--r--
Language.v
93716
log
plain
-rw-r--r--
LanguageInversion.v
41365
log
plain
-rw-r--r--
LanguageWf.v
92278
log
plain
-rw-r--r--
MiscCompilerPasses.v
5118
log
plain
-rw-r--r--
MiscCompilerPassesProofs.v
8721
log
plain
d---------
Primitives
87
log
plain
d---------
PushButtonSynthesis
792
log
plain
-rw-r--r--
Rewriter.v
150948
log
plain
-rw-r--r--
RewriterInterpProofs1.v
83599
log
plain
-rw-r--r--
RewriterProofs.v
11693
log
plain
-rw-r--r--
RewriterRules.v
49115
log
plain
-rw-r--r--
RewriterRulesGood.v
18035
log
plain
-rw-r--r--
RewriterRulesInterpGood.v
60003
log
plain
-rw-r--r--
RewriterRulesProofs.v
24975
log
plain
-rw-r--r--
RewriterWf1.v
157952
log
plain
-rw-r--r--
RewriterWf2.v
59774
log
plain
-rw-r--r--
SlowPrimeSynthesisExamples.v
70637
log
plain
d---------
Spec
325
log
plain
-rw-r--r--
StandaloneHaskellMain.v
2718
log
plain
-rw-r--r--
StandaloneOCamlMain.v
4048
log
plain
-rw-r--r--
TAPSort.v
480
log
plain
-rw-r--r--
UnderLets.v
10675
log
plain
-rw-r--r--
UnderLetsProofs.v
78065
log
plain
d---------
Util
2823
log
plain
-rw-r--r--
arith_rewrite_head.out
95226
log
plain
-rw-r--r--
arith_with_casts_rewrite_head.out
172839
log
plain
-rw-r--r--
fancy_rewrite_head.out
13195
log
plain
-rw-r--r--
fancy_with_casts_rewrite_head.out
400465
log
plain
-rw-r--r--
haskell.sed
179
log
plain
-rw-r--r--
nbe_rewrite_head.out
144032
log
plain
-rw-r--r--
strip_literal_casts_rewrite_head.out
14260
log
plain