From 4f6f5f7a930fdbe08bbbb2aa87f8bee0f8bf56ab Mon Sep 17 00:00:00 2001 From: David Benjamin Date: Mon, 12 Feb 2018 16:54:55 -0500 Subject: 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. --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') 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 -- cgit v1.2.3