index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
/
NewPipeline
Mode
Name
Size
-rw-r--r--
AbstractInterpretation.v
50897
log
plain
-rw-r--r--
AbstractInterpretationProofs.v
50420
log
plain
-rw-r--r--
AbstractInterpretationWf.v
52769
log
plain
-rw-r--r--
Arithmetic.v
189131
log
plain
-rw-r--r--
CLI.v
16419
log
plain
-rw-r--r--
CStringification.v
125982
log
plain
-rw-r--r--
CompilersTestCases.v
13823
log
plain
d---------
ExtractionHaskell
149
log
plain
d---------
ExtractionOCaml
149
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypes.v
107858
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypesProofs.v
3266
log
plain
-rw-r--r--
Language.v
78814
log
plain
-rw-r--r--
LanguageInversion.v
35292
log
plain
-rw-r--r--
LanguageWf.v
64236
log
plain
-rw-r--r--
MiscCompilerPasses.v
6585
log
plain
-rw-r--r--
MiscCompilerPassesProofs.v
9251
log
plain
-rw-r--r--
README.md
4447
log
plain
-rw-r--r--
Rewriter.v
115113
log
plain
-rw-r--r--
RewriterProofs.v
5538
log
plain
-rw-r--r--
RewriterRulesGood.v
36441
log
plain
-rw-r--r--
RewriterWf1.v
45102
log
plain
-rw-r--r--
RewriterWf2.v
55493
log
plain
-rw-r--r--
SlowPrimeSynthesisExamples.v
60994
log
plain
-rw-r--r--
StandaloneHaskellMain.v
2984
log
plain
-rw-r--r--
StandaloneOCamlMain.v
4312
log
plain
-rw-r--r--
Toplevel1.v
183935
log
plain
-rw-r--r--
Toplevel2.v
158868
log
plain
-rw-r--r--
UnderLets.v
8413
log
plain
-rw-r--r--
UnderLetsProofs.v
35967
log
plain
-rw-r--r--
arith_rewrite_head.out
112246
log
plain
-rw-r--r--
fancy_rewrite_head.out
114520
log
plain
-rw-r--r--
haskell.sed
179
log
plain
-rw-r--r--
nbe_rewrite_head.out
122204
log
plain