blob: 0f811e3cf1d399b00f0031391f8c24603786dd94 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *)
Require Import Coq.ZArith.ZArith.
Require Import Coq.derive.Derive.
Require Import Crypto.Arithmetic.Saturated.
Require Import Crypto.PushButtonSynthesis.ReificationCache.
Local Open Scope Z_scope.
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.
|
