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
52064
log
plain
-rw-r--r--
AbstractInterpretationProofs.v
82135
log
plain
-rw-r--r--
AbstractInterpretationWf.v
54220
log
plain
-rw-r--r--
AbstractInterpretationZRangeProofs.v
35823
log
plain
-rw-r--r--
Arithmetic.v
186569
log
plain
-rw-r--r--
CLI.v
18754
log
plain
-rw-r--r--
CStringification.v
125991
log
plain
-rw-r--r--
CompilersTestCases.v
14051
log
plain
d---------
ExtractionHaskell
149
log
plain
d---------
ExtractionOCaml
149
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypes.v
154210
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypesProofs.v
8653
log
plain
-rw-r--r--
Language.v
80389
log
plain
-rw-r--r--
LanguageInversion.v
33875
log
plain
-rw-r--r--
LanguageWf.v
82821
log
plain
-rw-r--r--
MiscCompilerPasses.v
5142
log
plain
-rw-r--r--
MiscCompilerPassesProofs.v
8817
log
plain
-rw-r--r--
README.md
4451
log
plain
-rw-r--r--
Rewriter.v
137635
log
plain
-rw-r--r--
RewriterProofs.v
9694
log
plain
-rw-r--r--
RewriterRulesGood.v
23571
log
plain
-rw-r--r--
RewriterRulesInterpGood.v
30330
log
plain
-rw-r--r--
RewriterWf1.v
99244
log
plain
-rw-r--r--
RewriterWf2.v
60292
log
plain
-rw-r--r--
SlowPrimeSynthesisExamples.v
61029
log
plain
-rw-r--r--
StandaloneHaskellMain.v
2799
log
plain
-rw-r--r--
StandaloneOCamlMain.v
4129
log
plain
-rw-r--r--
Toplevel1.v
186562
log
plain
-rw-r--r--
Toplevel2.v
158738
log
plain
-rw-r--r--
UnderLets.v
8489
log
plain
-rw-r--r--
UnderLetsProofs.v
38793
log
plain
-rw-r--r--
arith_rewrite_head.out
75233
log
plain
-rw-r--r--
arith_with_casts_rewrite_head.out
125981
log
plain
-rw-r--r--
fancy_rewrite_head.out
110876
log
plain
-rw-r--r--
fancy_with_casts_rewrite_head.out
9211
log
plain
-rw-r--r--
haskell.sed
179
log
plain
-rw-r--r--
nbe_rewrite_head.out
118667
log
plain