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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
(** * Push-Button Synthesis of Unsaturated Solinas: Reification Cache *)
Require Import Coq.ZArith.ZArith.
Require Import Coq.derive.Derive.
Require Import Crypto.Arithmetic.Core.
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 UnsaturatedSolinas.
Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0.
Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1.
Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c).
(**
<<
#!/usr/bin/env python
indent = ' '
print((indent + '(' + r'''**
<<
%s
>>
*''' + ')\n') % open(__file__, 'r').read())
for i in ('carry_mul', 'carry_square', 'carry_scmul', 'carry', 'encode', 'add', 'sub', 'opp', 'zero', 'one', 'prime'):
print((r'''%sDerive reified_%s_gen
SuchThat (is_reification_of reified_%s_gen %smod)
As reified_%s_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache.
Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n')
for (op, opmod) in (('to_bytes', 'freeze_to_bytesmod'), ('from_bytes', 'from_bytesmod')):
print((r'''%sDerive reified_%s_gen
SuchThat (is_reification_of reified_%s_gen %s)
As reified_%s_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache.
Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n')
>>
*)
Derive reified_carry_mul_gen
SuchThat (is_reification_of reified_carry_mul_gen carry_mulmod)
As reified_carry_mul_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification carry_mulmod (proj1 reified_carry_mul_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_carry_mul_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_carry_mul_gen_correct) : interp_gen_cache.
Local Opaque reified_carry_mul_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_carry_square_gen
SuchThat (is_reification_of reified_carry_square_gen carry_squaremod)
As reified_carry_square_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification carry_squaremod (proj1 reified_carry_square_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_carry_square_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_carry_square_gen_correct) : interp_gen_cache.
Local Opaque reified_carry_square_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_carry_scmul_gen
SuchThat (is_reification_of reified_carry_scmul_gen carry_scmulmod)
As reified_carry_scmul_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification carry_scmulmod (proj1 reified_carry_scmul_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_carry_scmul_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_carry_scmul_gen_correct) : interp_gen_cache.
Local Opaque reified_carry_scmul_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_carry_gen
SuchThat (is_reification_of reified_carry_gen carrymod)
As reified_carry_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification carrymod (proj1 reified_carry_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_carry_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_carry_gen_correct) : interp_gen_cache.
Local Opaque reified_carry_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_encode_gen
SuchThat (is_reification_of reified_encode_gen encodemod)
As reified_encode_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache.
Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_add_gen
SuchThat (is_reification_of reified_add_gen addmod)
As reified_add_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache.
Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_sub_gen
SuchThat (is_reification_of reified_sub_gen submod)
As reified_sub_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache.
Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_opp_gen
SuchThat (is_reification_of reified_opp_gen oppmod)
As reified_opp_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache.
Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_zero_gen
SuchThat (is_reification_of reified_zero_gen zeromod)
As reified_zero_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache.
Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_one_gen
SuchThat (is_reification_of reified_one_gen onemod)
As reified_one_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache.
Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_prime_gen
SuchThat (is_reification_of reified_prime_gen primemod)
As reified_prime_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification primemod (proj1 reified_prime_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_prime_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_prime_gen_correct) : interp_gen_cache.
Local Opaque reified_prime_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_to_bytes_gen
SuchThat (is_reification_of reified_to_bytes_gen freeze_to_bytesmod)
As reified_to_bytes_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification freeze_to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache.
Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *)
Derive reified_from_bytes_gen
SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod)
As reified_from_bytes_gen_correct.
Proof. Time cache_reify (). Time Qed.
Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen.
Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache.
Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache.
Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *)
End UnsaturatedSolinas.
|
