diff options
| author |  David Benjamin <davidben@google.com> | 2018-02-12 16:54:55 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2018-03-09 18:02:01 -0500 |
| commit | 4f6f5f7a930fdbe08bbbb2aa87f8bee0f8bf56ab (patch) | |
| tree | dff8cdef098c66bcf16563e7ebdcf87476d7b436 /_CoqProject | |
| parent | 291dcc2fd37e2338aafa5f5d9c5db70c2af07c12 (diff) | |
Prove another Barrett reduction variant.
This variant comes from
http://www.ridiculousfish.com/blog/posts/labor-of-division-episode-i.html.
It was useful for
https://boringssl-review.googlesource.com/#/c/boringssl/+/25887.
TODO - Talk to Andres to figure out all the ways this could be done more
cleanly. It was originally a standalone file.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 4d8765bd7..9baa1bb62 100644 --- a/_CoqProject +++ b/_CoqProject @@ -24,6 +24,7 @@ src/Arithmetic/ModularArithmeticTheorems.v src/Arithmetic/PrimeFieldTheorems.v src/Arithmetic/BarrettReduction/Generalized.v src/Arithmetic/BarrettReduction/HAC.v +src/Arithmetic/BarrettReduction/RidiculousFish.v src/Arithmetic/BarrettReduction/Wikipedia.v src/Arithmetic/MontgomeryReduction/Definition.v src/Arithmetic/MontgomeryReduction/Proofs.v |