From c0fe35f49d61207d16c6db79936e38edf9661a49 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 1 Apr 2019 05:38:38 -0400 Subject: rename some things --- .../FancyMontgomeryReductionReificationCache.v | 24 ++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v (limited to 'src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v') diff --git a/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v new file mode 100644 index 000000000..7a475a53a --- /dev/null +++ b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v @@ -0,0 +1,24 @@ +(** * Push-Button Snthesis of fancy mongomery reduction : Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.FancyMontgomeryReduction. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional. + +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. -- cgit v1.2.3