diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-05 19:30:44 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-09 16:47:33 -0700 |
| commit | 7d3f54c975d24dc2f5fd8a0e31e004d74d7a3dd0 (patch) | |
| tree | 854f1f859b1cfa8b60e4f62479fbb3d5bad174d4 /_CoqProject | |
| parent | 97dd7cca1433f0cf42d28df671de54e4cfb746e0 (diff) | |
Specify a type of bounded integers for mod arith
Also use it to implement Montgomery reduction and Barrett reduction.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 307a752fd..2840c3b91 100644 --- a/_CoqProject +++ b/_CoqProject @@ -50,10 +50,13 @@ src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/Tutorial.v +src/ModularArithmetic/ZBounded.v src/ModularArithmetic/BarrettReduction/Z.v +src/ModularArithmetic/BarrettReduction/ZBounded.v src/ModularArithmetic/BarrettReduction/ZGeneralized.v src/ModularArithmetic/BarrettReduction/ZHandbook.v src/ModularArithmetic/Montgomery/Z.v +src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v |