diff options
author | Jason Gross <jgross@mit.edu> | 2019-01-17 15:07:47 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-01-18 19:44:48 -0500 |
commit | cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd (patch) | |
tree | 4540df27da661c35fdc5246f1692fa124003ff6f /src/PushButtonSynthesis/SaturatedSolinasReificationCache.v | |
parent | b99dd6da3b6370bc225d3b501bda07c49fd29c12 (diff) |
Split up PushButtonSynthesis.v
Closes #497
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinasReificationCache.v')
-rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinasReificationCache.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v new file mode 100644 index 000000000..ccc48e2cd --- /dev/null +++ b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v @@ -0,0 +1,28 @@ +(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +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 SaturatedSolinas. + Definition mulmod + (s : Z) + (c : list (Z * Z)) + (log2base : Z) + (n nreductions : nat) + := @Rows.mulmod (weight log2base 1) (2^log2base) s c n nreductions. + + Derive reified_mul_gen + SuchThat (is_reification_of reified_mul_gen mulmod) + As reified_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) +End SaturatedSolinas. |