blob: 457c9dc11efd6841746002b01742de2ee3f13ef6 (
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
|
(* This file is autogenerated from Base.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Base.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples.
End TAG.
Ltac add_r pkg :=
let bitwidth := Tag.get pkg TAG.bitwidth in
let r := fresh "r" in
let r := pose_r bitwidth r in
Tag.update pkg TAG.r r.
Ltac add_m pkg :=
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let m := fresh "m" in
let m := pose_m s c m in
Tag.update pkg TAG.m m.
Ltac add_wt pkg :=
let m := Tag.get pkg TAG.m in
let sz := Tag.get pkg TAG.sz in
let wt := fresh "wt" in
let wt := pose_wt m sz wt in
Tag.update pkg TAG.wt wt.
Ltac add_sz2 pkg :=
let sz := Tag.get pkg TAG.sz in
let sz2 := fresh "sz2" in
let sz2 := pose_sz2 sz sz2 in
Tag.update pkg TAG.sz2 sz2.
Ltac add_half_sz pkg :=
let sz := Tag.get pkg TAG.sz in
let half_sz := fresh "half_sz" in
let half_sz := pose_half_sz sz half_sz in
Tag.update pkg TAG.half_sz half_sz.
Ltac add_half_sz_nonzero pkg :=
let half_sz := Tag.get pkg TAG.half_sz in
let half_sz_nonzero := fresh "half_sz_nonzero" in
let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero.
Ltac add_m_enc pkg :=
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 wt := Tag.get pkg TAG.wt in
let m_enc := fresh "m_enc" in
let m_enc := pose_m_enc sz s c wt m_enc in
Tag.update pkg TAG.m_enc m_enc.
Ltac add_coef pkg :=
let sz := Tag.get pkg TAG.sz in
let wt := Tag.get pkg TAG.wt in
let m_enc := Tag.get pkg TAG.m_enc in
let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
let coef := fresh "coef" in
let coef := pose_coef sz wt m_enc coef_div_modulus coef in
Tag.update pkg TAG.coef coef.
Ltac add_coef_mod pkg :=
let sz := Tag.get pkg TAG.sz in
let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let coef := Tag.get pkg TAG.coef in
let coef_mod := fresh "coef_mod" in
let coef_mod := pose_coef_mod sz wt m coef coef_mod in
Tag.update pkg TAG.coef_mod coef_mod.
Ltac add_sz_nonzero pkg :=
let sz := Tag.get pkg TAG.sz in
let sz_nonzero := fresh "sz_nonzero" in
let sz_nonzero := pose_sz_nonzero sz sz_nonzero in
Tag.update pkg TAG.sz_nonzero sz_nonzero.
Ltac add_wt_nonzero pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_nonzero := fresh "wt_nonzero" in
let wt_nonzero := pose_wt_nonzero wt wt_nonzero in
Tag.update pkg TAG.wt_nonzero wt_nonzero.
Ltac add_wt_nonneg pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_nonneg := fresh "wt_nonneg" in
let wt_nonneg := pose_wt_nonneg wt wt_nonneg in
Tag.update pkg TAG.wt_nonneg wt_nonneg.
Ltac add_wt_divides pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_divides := fresh "wt_divides" in
let wt_divides := pose_wt_divides wt wt_divides in
Tag.update pkg TAG.wt_divides wt_divides.
Ltac add_wt_divides' pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_divides := Tag.get pkg TAG.wt_divides in
let wt_divides' := fresh "wt_divides'" in
let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in
Tag.update pkg TAG.wt_divides' wt_divides'.
Ltac add_wt_divides_chains pkg :=
let wt := Tag.get pkg TAG.wt in
let carry_chains := Tag.get pkg TAG.carry_chains in
let wt_divides' := Tag.get pkg TAG.wt_divides' in
let wt_divides_chains := fresh "wt_divides_chains" in
let wt_divides_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains in
Tag.update pkg TAG.wt_divides_chains wt_divides_chains.
Ltac add_wt_pos pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_pos := fresh "wt_pos" in
let wt_pos := pose_wt_pos wt wt_pos in
Tag.update pkg TAG.wt_pos wt_pos.
Ltac add_wt_multiples pkg :=
let wt := Tag.get pkg TAG.wt in
let wt_multiples := fresh "wt_multiples" in
let wt_multiples := pose_wt_multiples wt wt_multiples in
Tag.update pkg TAG.wt_multiples wt_multiples.
Ltac add_Base_package pkg :=
let pkg := add_r pkg in
let pkg := add_m pkg in
let pkg := add_wt pkg in
let pkg := add_sz2 pkg in
let pkg := add_half_sz pkg in
let pkg := add_half_sz_nonzero pkg in
let pkg := add_m_enc pkg in
let pkg := add_coef pkg in
let pkg := add_coef_mod pkg in
let pkg := add_sz_nonzero pkg in
let pkg := add_wt_nonzero pkg in
let pkg := add_wt_nonneg pkg in
let pkg := add_wt_divides pkg in
let pkg := add_wt_divides' pkg in
let pkg := add_wt_divides_chains pkg in
let pkg := add_wt_pos pkg in
let pkg := add_wt_multiples pkg in
Tag.strip_local pkg.
Module MakeBasePackage (PKG : PrePackage).
Module Import MakeBasePackageInternal := MakePackageBase PKG.
Ltac get_r _ := get TAG.r.
Notation r := (ltac:(let v := get_r () in exact v)) (only parsing).
Ltac get_m _ := get TAG.m.
Notation m := (ltac:(let v := get_m () in exact v)) (only parsing).
Ltac get_wt _ := get TAG.wt.
Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing).
Ltac get_sz2 _ := get TAG.sz2.
Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing).
Ltac get_half_sz _ := get TAG.half_sz.
Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing).
Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero.
Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
Ltac get_m_enc _ := get TAG.m_enc.
Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing).
Ltac get_coef _ := get TAG.coef.
Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing).
Ltac get_coef_mod _ := get TAG.coef_mod.
Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing).
Ltac get_sz_nonzero _ := get TAG.sz_nonzero.
Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing).
Ltac get_wt_nonzero _ := get TAG.wt_nonzero.
Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing).
Ltac get_wt_nonneg _ := get TAG.wt_nonneg.
Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing).
Ltac get_wt_divides _ := get TAG.wt_divides.
Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing).
Ltac get_wt_divides' _ := get TAG.wt_divides'.
Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing).
Ltac get_wt_divides_chains _ := get TAG.wt_divides_chains.
Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing).
Ltac get_wt_pos _ := get TAG.wt_pos.
Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing).
Ltac get_wt_multiples _ := get TAG.wt_multiples.
Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing).
End MakeBasePackage.
|
