aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2016-08-04 11:44:34 -0700
committerGravatar GitHub <noreply@github.com>2016-08-04 11:44:34 -0700
commitc29fa1ad5e2609575c29c217c341690205f0b5b0 (patch)
tree458bba6ce18b0f3f495475e1c7465101d942c4e0 /_CoqProject
parentf23858c3a204a11a6dc0bdd250ebb97dedb986ac (diff)
Implement Barrett Reduction following HAC 14.42 (#45)
From http://cacr.uwaterloo.ca/hac/about/chap14.pdf This should take care of most of #43, at least the specification on Z part of it.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 7a2de03e0..5d44d85f6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -52,6 +52,7 @@ src/ModularArithmetic/PseudoMersenneBaseParams.v
src/ModularArithmetic/Tutorial.v
src/ModularArithmetic/BarrettReduction/Z.v
src/ModularArithmetic/BarrettReduction/ZGeneralized.v
+src/ModularArithmetic/BarrettReduction/ZHandbook.v
src/Spec/CompleteEdwardsCurve.v
src/Spec/EdDSA.v
src/Spec/Encoding.v