blob: 52ed4ad33720bf286ffae2983dd0a661ec1d3482 (
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
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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(* This file is autogenerated from Defaults.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Defaults.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := mul_code_correct | square_code_correct | carry_sig | zero_sig | one_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
End TAG.
Ltac add_mul_code_correct pkg P_extra_prove_mul_eq :=
Tag.update_by_tac_if_not_exists
pkg
TAG.mul_code_correct
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let sz2 := Tag.get pkg TAG.sz2 in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let mul_code := Tag.get pkg TAG.mul_code in
let mul_code_correct := fresh "mul_code_correct" in
let mul_code_correct := pose_mul_code_correct P_extra_prove_mul_eq sz sz2 wt s c mul_code mul_code_correct in
constr:(mul_code_correct)).
Ltac add_square_code_correct pkg P_extra_prove_square_eq :=
Tag.update_by_tac_if_not_exists
pkg
TAG.square_code_correct
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let sz2 := Tag.get pkg TAG.sz2 in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let square_code := Tag.get pkg TAG.square_code in
let square_code_correct := fresh "square_code_correct" in
let square_code_correct := pose_square_code_correct P_extra_prove_square_eq sz sz2 wt s c square_code square_code_correct in
constr:(square_code_correct)).
Ltac add_carry_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.carry_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let carry_chains := Tag.get pkg TAG.carry_chains in
let carry_sig := fresh "carry_sig" in
let carry_sig := pose_carry_sig wt m base sz s c carry_chains carry_sig in
constr:(carry_sig)).
Ltac add_zero_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.zero_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let base_pos := Tag.get pkg TAG.base_pos in
let zero_sig := fresh "zero_sig" in
let zero_sig := pose_zero_sig wt m base sz sz_nonzero base_pos zero_sig in
constr:(zero_sig)).
Ltac add_one_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.one_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let base_pos := Tag.get pkg TAG.base_pos in
let one_sig := fresh "one_sig" in
let one_sig := pose_one_sig wt m base sz sz_nonzero base_pos one_sig in
constr:(one_sig)).
Ltac add_add_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.add_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let add_sig := fresh "add_sig" in
let add_sig := pose_add_sig wt m base sz add_sig in
constr:(add_sig)).
Ltac add_sub_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.sub_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let coef := Tag.get pkg TAG.coef in
let sub_sig := fresh "sub_sig" in
let sub_sig := pose_sub_sig wt m base sz coef sub_sig in
constr:(sub_sig)).
Ltac add_opp_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.opp_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let coef := Tag.get pkg TAG.coef in
let opp_sig := fresh "opp_sig" in
let opp_sig := pose_opp_sig wt m base sz coef opp_sig in
constr:(opp_sig)).
Ltac add_mul_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.mul_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let mul_code := Tag.get pkg TAG.mul_code in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let s_nonzero := Tag.get pkg TAG.s_nonzero in
let base_pos := Tag.get pkg TAG.base_pos in
let mul_code_correct := Tag.get pkg TAG.mul_code_correct in
let mul_sig := fresh "mul_sig" in
let mul_sig := pose_mul_sig wt m base sz s c mul_code sz_nonzero s_nonzero base_pos mul_code_correct mul_sig in
constr:(mul_sig)).
Ltac add_square_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.square_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let square_code := Tag.get pkg TAG.square_code in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let s_nonzero := Tag.get pkg TAG.s_nonzero in
let base_pos := Tag.get pkg TAG.base_pos in
let square_code_correct := Tag.get pkg TAG.square_code_correct in
let square_sig := fresh "square_sig" in
let square_sig := pose_square_sig wt m base sz s c square_code sz_nonzero s_nonzero base_pos square_code_correct square_sig in
constr:(square_sig)).
Ltac add_ring pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.ring
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let wt_divides' := Tag.get pkg TAG.wt_divides' in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let zero_sig := Tag.get pkg TAG.zero_sig in
let one_sig := Tag.get pkg TAG.one_sig in
let opp_sig := Tag.get pkg TAG.opp_sig in
let add_sig := Tag.get pkg TAG.add_sig in
let sub_sig := Tag.get pkg TAG.sub_sig in
let mul_sig := Tag.get pkg TAG.mul_sig in
let ring := fresh "ring" in
let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in
constr:(ring)).
Ltac add_Defaults_package pkg P_extra_prove_mul_eq P_extra_prove_square_eq :=
let pkg := add_mul_code_correct pkg P_extra_prove_mul_eq in
let pkg := add_square_code_correct pkg P_extra_prove_square_eq in
let pkg := add_carry_sig pkg in
let pkg := add_zero_sig pkg in
let pkg := add_one_sig pkg in
let pkg := add_add_sig pkg in
let pkg := add_sub_sig pkg in
let pkg := add_opp_sig pkg in
let pkg := add_mul_sig pkg in
let pkg := add_square_sig pkg in
let pkg := add_ring pkg in
Tag.strip_subst_local pkg.
Module MakeDefaultsPackage (PKG : PrePackage).
Module Import MakeDefaultsPackageInternal := MakePackageBase PKG.
Ltac get_mul_code_correct _ := get TAG.mul_code_correct.
Notation mul_code_correct := (ltac:(let v := get_mul_code_correct () in exact v)) (only parsing).
Ltac get_square_code_correct _ := get TAG.square_code_correct.
Notation square_code_correct := (ltac:(let v := get_square_code_correct () in exact v)) (only parsing).
Ltac get_carry_sig _ := get TAG.carry_sig.
Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing).
Ltac get_zero_sig _ := get TAG.zero_sig.
Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
Ltac get_one_sig _ := get TAG.one_sig.
Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing).
Ltac get_add_sig _ := get TAG.add_sig.
Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
Ltac get_sub_sig _ := get TAG.sub_sig.
Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing).
Ltac get_opp_sig _ := get TAG.opp_sig.
Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing).
Ltac get_mul_sig _ := get TAG.mul_sig.
Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing).
Ltac get_square_sig _ := get TAG.square_sig.
Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing).
Ltac get_ring _ := get TAG.ring.
Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing).
End MakeDefaultsPackage.
|
