index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Compilers
/
Z
Mode
Name
Size
-rw-r--r--
ArithmeticSimplifier.v
31075
log
plain
-rw-r--r--
ArithmeticSimplifierInterp.v
11792
log
plain
-rw-r--r--
ArithmeticSimplifierUtil.v
3140
log
plain
-rw-r--r--
ArithmeticSimplifierWf.v
9197
log
plain
-rw-r--r--
BinaryNotationConstants.v
613063
log
plain
d---------
Bounds
391
log
plain
-rw-r--r--
CNotations.v
2553213
log
plain
-rw-r--r--
CommonSubexpressionElimination.v
8361
log
plain
-rw-r--r--
CommonSubexpressionEliminationInterp.v
977
log
plain
-rw-r--r--
CommonSubexpressionEliminationWf.v
1199
log
plain
-rw-r--r--
FoldTypes.v
562
log
plain
-rw-r--r--
GeneralizeVar.v
656
log
plain
-rw-r--r--
GeneralizeVarInterp.v
801
log
plain
-rw-r--r--
GeneralizeVarWf.v
967
log
plain
-rw-r--r--
HexNotationConstants.v
732901
log
plain
-rw-r--r--
Inline.v
376
log
plain
-rw-r--r--
InlineConstAndOp.v
665
log
plain
-rw-r--r--
InlineConstAndOpByRewrite.v
722
log
plain
-rw-r--r--
InlineConstAndOpByRewriteInterp.v
493
log
plain
-rw-r--r--
InlineConstAndOpByRewriteWf.v
457
log
plain
-rw-r--r--
InlineConstAndOpInterp.v
516
log
plain
-rw-r--r--
InlineConstAndOpWf.v
397
log
plain
-rw-r--r--
InlineInterp.v
833
log
plain
-rw-r--r--
InlineWf.v
502
log
plain
-rw-r--r--
InterpSideConditions.v
446
log
plain
-rw-r--r--
JavaNotations.v
92146
log
plain
-rw-r--r--
MapCastByDeBruijn.v
1341
log
plain
-rw-r--r--
MapCastByDeBruijnInterp.v
3058
log
plain
-rw-r--r--
MapCastByDeBruijnWf.v
2849
log
plain
d---------
Named
200
log
plain
-rw-r--r--
OpInversion.v
799
log
plain
-rw-r--r--
Reify.v
4924
log
plain
-rw-r--r--
RewriteAddToAdc.v
2402
log
plain
-rw-r--r--
RewriteAddToAdcInterp.v
3929
log
plain
-rw-r--r--
RewriteAddToAdcWf.v
1660
log
plain
-rw-r--r--
Syntax.v
5075
log
plain
d---------
Syntax
72
log
plain
-rw-r--r--
TypeInversion.v
1317
log
plain