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
52862
log
plain
-rw-r--r--
AbstractInterpretationProofs.v
83456
log
plain
-rw-r--r--
AbstractInterpretationWf.v
55036
log
plain
-rw-r--r--
AbstractInterpretationZRangeProofs.v
35666
log
plain
-rw-r--r--
Arithmetic.v
184963
log
plain
-rw-r--r--
CLI.v
18313
log
plain
-rw-r--r--
CStringification.v
125991
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
145044
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypesProofs.v
5426
log
plain
-rw-r--r--
Language.v
79386
log
plain
-rw-r--r--
LanguageInversion.v
33875
log
plain
-rw-r--r--
LanguageWf.v
69285
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
131830
log
plain
-rw-r--r--
RewriterProofs.v
5427
log
plain
-rw-r--r--
RewriterRulesGood.v
23413
log
plain
-rw-r--r--
RewriterWf1.v
54963
log
plain
-rw-r--r--
RewriterWf2.v
72858
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
184377
log
plain
-rw-r--r--
Toplevel2.v
157664
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
97130
log
plain
-rw-r--r--
fancy_rewrite_head.out
92473
log
plain
-rw-r--r--
haskell.sed
179
log
plain
-rw-r--r--
nbe_rewrite_head.out
172646
log
plain