diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-08-05 11:44:51 -0700 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-08-05 11:44:51 -0700 |
| commit | 2be3fd6b9e4c415801e3519a2e054560d5b8a5fe (patch) | |
| tree | 94c414eb9b73643b8a77dd7c3be0dc9e789d1384 /_CoqProject | |
| parent | 46c8f47e6016a7009d9b908d7d2b91427f0de886 (diff) | |
Define Montgomery reduction / multiplication on Z (#42)
This is partly done for my own benefit, to internalize how Montgomery
multiplication works, and partly done as a template for word-based
Montgomery multiplication when the carrying does not take advantage of
the fact that we are using a pseudomersenne prime.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 5d44d85f6..307a752fd 100644 --- a/_CoqProject +++ b/_CoqProject @@ -53,6 +53,8 @@ src/ModularArithmetic/Tutorial.v src/ModularArithmetic/BarrettReduction/Z.v src/ModularArithmetic/BarrettReduction/ZGeneralized.v src/ModularArithmetic/BarrettReduction/ZHandbook.v +src/ModularArithmetic/Montgomery/Z.v +src/ModularArithmetic/Montgomery/ZProofs.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v |