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
52016
log
plain
-rw-r--r--
AbstractInterpretationProofs.v
81955
log
plain
-rw-r--r--
AbstractInterpretationWf.v
54088
log
plain
-rw-r--r--
AbstractInterpretationZRangeProofs.v
35636
log
plain
d---------
Algebra
381
log
plain
-rw-r--r--
Arithmetic.v
228472
log
plain
d---------
Arithmetic
242
log
plain
-rw-r--r--
BoundsPipeline.v
29947
log
plain
-rw-r--r--
CLI.v
18754
log
plain
-rw-r--r--
COperationSpecifications.v
23722
log
plain
-rw-r--r--
CStringification.v
125943
log
plain
-rw-r--r--
CompilersTestCases.v
13907
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
-rw-r--r--
GENERATEDIdentifiersWithoutTypes.v
152427
log
plain
-rw-r--r--
GENERATEDIdentifiersWithoutTypesProofs.v
10287
log
plain
-rw-r--r--
Language.v
82127
log
plain
-rw-r--r--
LanguageInversion.v
37018
log
plain
-rw-r--r--
LanguageWf.v
86421
log
plain
-rw-r--r--
MiscCompilerPasses.v
5118
log
plain
-rw-r--r--
MiscCompilerPassesProofs.v
8721
log
plain
d---------
Primitives
87
log
plain
-rw-r--r--
PushButtonSynthesis.v
142516
log
plain
d---------
PushButtonSynthesis
46
log
plain
-rw-r--r--
Rewriter.v
164549
log
plain
-rw-r--r--
RewriterInterpProofs1.v
83735
log
plain
-rw-r--r--
RewriterProofs.v
10614
log
plain
-rw-r--r--
RewriterRulesGood.v
23337
log
plain
-rw-r--r--
RewriterRulesInterpGood.v
47607
log
plain
-rw-r--r--
RewriterWf1.v
141933
log
plain
-rw-r--r--
RewriterWf2.v
59759
log
plain
-rw-r--r--
SlowPrimeSynthesisExamples.v
61025
log
plain
d---------
Spec
325
log
plain
-rw-r--r--
StandaloneHaskellMain.v
2761
log
plain
-rw-r--r--
StandaloneOCamlMain.v
4091
log
plain
-rw-r--r--
Toplevel2.v
160866
log
plain
-rw-r--r--
UnderLets.v
8465
log
plain
-rw-r--r--
UnderLetsProofs.v
55741
log
plain
d---------
Util
2783
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
9200
log
plain
-rw-r--r--
fancy_with_casts_rewrite_head.out
635522
log
plain
-rw-r--r--
haskell.sed
179
log
plain
-rw-r--r--
nbe_rewrite_head.out
118667
log
plain