diff options
| author |  jadep <jadep@mit.edu> | 2019-04-01 05:38:38 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | c0fe35f49d61207d16c6db79936e38edf9661a49 (patch) | |
| tree | 4d4bff49fade9138939f2bfd71eed9fcc50d764f /src/PushButtonSynthesis/MontgomeryReductionReificationCache.v | |
| parent | 299206fc77217802c4431ccda1a7c0cb372f0b87 (diff) | |
rename some things
Diffstat (limited to 'src/PushButtonSynthesis/MontgomeryReductionReificationCache.v')
| -rw-r--r-- | src/PushButtonSynthesis/MontgomeryReductionReificationCache.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v deleted file mode 100644 index 80af335df..000000000 --- a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v +++ /dev/null @@ -1,23 +0,0 @@ -(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) -Require Import Coq.ZArith.ZArith. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.FancyMontgomeryReduction. -Require Import Crypto.PushButtonSynthesis.ReificationCache. -Local Open Scope Z_scope. - -Import Associational Positional Arithmetic.MontgomeryReduction. - -Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) - -Module Export MontgomeryReduction. - Derive reified_montred_gen - SuchThat (is_reification_of reified_montred_gen montred') - As reified_montred_gen_correct. - Proof. Time cache_reify (). Time Qed. - Module Export ReifyHints. - Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache. - End ReifyHints. - Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) -End MontgomeryReduction. |