index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
ModularArithmetic
Mode
Name
Size
d---------
BarrettReduction
150
log
plain
-rw-r--r--
Conversion.v
15057
log
plain
-rw-r--r--
ExtPow2BaseMulProofs.v
1424
log
plain
-rw-r--r--
ExtendedBaseVector.v
8415
log
plain
-rw-r--r--
ModularArithmeticTheorems.v
12844
log
plain
-rw-r--r--
ModularBaseSystem.v
5761
log
plain
-rw-r--r--
ModularBaseSystemList.v
4062
log
plain
-rw-r--r--
ModularBaseSystemListProofs.v
21715
log
plain
-rw-r--r--
ModularBaseSystemListZOperations.v
2561
log
plain
-rw-r--r--
ModularBaseSystemListZOperationsProofs.v
798
log
plain
-rw-r--r--
ModularBaseSystemOpt.v
40525
log
plain
-rw-r--r--
ModularBaseSystemProofs.v
45032
log
plain
-rw-r--r--
ModularBaseSystemWord.v
946
log
plain
d---------
Montgomery
106
log
plain
-rw-r--r--
Pow2Base.v
2868
log
plain
-rw-r--r--
Pow2BaseProofs.v
65609
log
plain
-rw-r--r--
Pre.v
4870
log
plain
-rw-r--r--
PrimeFieldTheorems.v
10965
log
plain
-rw-r--r--
PseudoMersenneBaseParamProofs.v
3480
log
plain
-rw-r--r--
PseudoMersenneBaseParams.v
900
log
plain
-rw-r--r--
Tutorial.v
6175
log
plain
-rw-r--r--
ZBounded.v
9403
log
plain
-rw-r--r--
ZBoundedZ.v
3247
log
plain
