Skip to content

Commit a518598

Browse files
sipasipa
committed
Add overflow analysis to field_5x52_int128_impl.h
1 parent fa0d620 commit a518598

File tree

1 file changed

+97
-0
lines changed

1 file changed

+97
-0
lines changed

‎src/field_5x52_int128_impl.h‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,23 @@
77

88
#include <stdint.h>
99

10+
#ifdef VERIFY
11+
#define VERIFY_BITS(x, n) VERIFY_CHECK(((x) >> (n)) == 0)
12+
#else
13+
#define VERIFY_BITS(x, n) do { } while(0)
14+
#endif
15+
1016
SECP256K1_INLINE static void secp256k1_fe_mul_inner(const uint64_t *a, const uint64_t *b, uint64_t *r) {
17+
VERIFY_BITS(a[0], 56);
18+
VERIFY_BITS(a[1], 56);
19+
VERIFY_BITS(a[2], 56);
20+
VERIFY_BITS(a[3], 56);
21+
VERIFY_BITS(a[4], 52);
22+
VERIFY_BITS(b[0], 56);
23+
VERIFY_BITS(b[1], 56);
24+
VERIFY_BITS(b[2], 56);
25+
VERIFY_BITS(b[3], 56);
26+
VERIFY_BITS(b[4], 52);
1127

1228
const uint64_t M = 0xFFFFFFFFFFFFFULL, R = 0x1000003D10ULL;
1329
// [... a b c] is a shorthand for ... + a<<104 + b<<52 + c<<0 mod n.
@@ -20,83 +36,127 @@ SECP256K1_INLINE static void secp256k1_fe_mul_inner(const uint64_t *a, const uin
2036
+ (__int128)a[1] * b[2]
2137
+ (__int128)a[2] * b[1]
2238
+ (__int128)a[3] * b[0];
39+
VERIFY_BITS(d, 114);
2340
// [d 0 0 0] = [p3 0 0 0]
2441
c = (__int128)a[4] * b[4];
42+
VERIFY_BITS(c, 112);
2543
// [c 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
2644
d += (c & M) * R; c >>= 52;
45+
VERIFY_BITS(d, 115);
46+
VERIFY_BITS(c, 60);
2747
// [c 0 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
2848
uint64_t t3 = d & M; d >>= 52;
49+
VERIFY_BITS(t3, 52);
50+
VERIFY_BITS(d, 63);
2951
// [c 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
3052

3153
d += (__int128)a[0] * b[4]
3254
+ (__int128)a[1] * b[3]
3355
+ (__int128)a[2] * b[2]
3456
+ (__int128)a[3] * b[1]
3557
+ (__int128)a[4] * b[0];
58+
VERIFY_BITS(d, 115);
3659
// [c 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
3760
d += c * R;
61+
VERIFY_BITS(d, 116);
3862
// [d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
3963
uint64_t t4 = d & M; d >>= 52;
64+
VERIFY_BITS(t4, 52);
65+
VERIFY_BITS(d, 64);
4066
// [d t4 t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
4167
uint64_t tx = (t4 >> 48); t4 &= (M >> 4);
68+
VERIFY_BITS(tx, 4);
69+
VERIFY_BITS(t4, 48);
4270
// [d t4+(tx<<48) t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
4371

4472
c = (__int128)a[0] * b[0];
73+
VERIFY_BITS(c, 112);
4574
// [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 0 p4 p3 0 0 p0]
4675
d += (__int128)a[1] * b[4]
4776
+ (__int128)a[2] * b[3]
4877
+ (__int128)a[3] * b[2]
4978
+ (__int128)a[4] * b[1];
79+
VERIFY_BITS(d, 115);
5080
// [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
5181
uint64_t u0 = d & M; d >>= 52;
82+
VERIFY_BITS(u0, 52);
83+
VERIFY_BITS(d, 63);
5284
// [d u0 t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
5385
// [d 0 t4+(tx<<48)+(u0<<52) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
5486
u0 = (u0 << 4) | tx;
87+
VERIFY_BITS(u0, 56);
5588
// [d 0 t4+(u0<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
5689
c += (__int128)u0 * (R >> 4);
90+
VERIFY_BITS(c, 115);
5791
// [d 0 t4 t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
5892
uint64_t t0 = c & M; c >>= 52;
93+
VERIFY_BITS(t0, 52);
94+
VERIFY_BITS(c, 61);
5995
// [d 0 t4 t3 0 c t0] = [p8 0 0 p5 p4 p3 0 0 p0]
6096

6197
c += (__int128)a[0] * b[1]
6298
+ (__int128)a[1] * b[0];
99+
VERIFY_BITS(c, 114);
63100
// [d 0 t4 t3 0 c t0] = [p8 0 0 p5 p4 p3 0 p1 p0]
64101
d += (__int128)a[2] * b[4]
65102
+ (__int128)a[3] * b[3]
66103
+ (__int128)a[4] * b[2];
104+
VERIFY_BITS(d, 114);
67105
// [d 0 t4 t3 0 c t0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
68106
c += (d & M) * R; d >>= 52;
107+
VERIFY_BITS(c, 115);
108+
VERIFY_BITS(d, 62);
69109
// [d 0 0 t4 t3 0 c t0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
70110
uint64_t t1 = c & M; c >>= 52;
111+
VERIFY_BITS(t1, 52);
112+
VERIFY_BITS(c, 63);
71113
// [d 0 0 t4 t3 c t1 t0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
72114

73115
c += (__int128)a[0] * b[2]
74116
+ (__int128)a[1] * b[1]
75117
+ (__int128)a[2] * b[0];
118+
VERIFY_BITS(c, 114);
76119
// [d 0 0 t4 t3 c t1 t0] = [p8 0 p6 p5 p4 p3 p2 p1 p0]
77120
d += (__int128)a[3] * b[4]
78121
+ (__int128)a[4] * b[3];
122+
VERIFY_BITS(d, 114);
79123
// [d 0 0 t4 t3 c t1 t0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
80124
c += (d & M) * R; d >>= 52;
125+
VERIFY_BITS(c, 115);
126+
VERIFY_BITS(d, 62);
81127
// [d 0 0 0 t4 t3 c t1 t0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
82128

83129
r[0] = t0;
130+
VERIFY_BITS(r[0], 52);
84131
// [d 0 0 0 t4 t3 c t1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
85132
r[1] = t1;
133+
VERIFY_BITS(r[1], 52);
86134
// [d 0 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
87135
r[2] = c & M; c >>= 52;
136+
VERIFY_BITS(r[2], 52);
137+
VERIFY_BITS(c, 63);
88138
// [d 0 0 0 t4 t3+c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
89139
c += d * R + t3;;
140+
VERIFY_BITS(c, 100);
90141
// [t4 c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
91142
r[3] = c & M; c >>= 52;
143+
VERIFY_BITS(r[3], 52);
144+
VERIFY_BITS(c, 48);
92145
// [t4+c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
93146
c += t4;
147+
VERIFY_BITS(c, 49);
94148
// [c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
95149
r[4] = c;
150+
VERIFY_BITS(r[4], 49);
96151
// [r4 r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
97152
}
98153

99154
SECP256K1_INLINE static void secp256k1_fe_sqr_inner(const uint64_t *a, uint64_t *r) {
155+
VERIFY_BITS(a[0], 56);
156+
VERIFY_BITS(a[1], 56);
157+
VERIFY_BITS(a[2], 56);
158+
VERIFY_BITS(a[3], 56);
159+
VERIFY_BITS(a[4], 52);
100160

101161
const uint64_t M = 0xFFFFFFFFFFFFFULL, R = 0x1000003D10ULL;
102162
// [... a b c] is a shorthand for ... + a<<104 + b<<52 + c<<0 mod n.
@@ -109,69 +169,106 @@ SECP256K1_INLINE static void secp256k1_fe_sqr_inner(const uint64_t *a, uint64_t
109169

110170
d = (__int128)(a0*2) * a3
111171
+ (__int128)(a1*2) * a2;
172+
VERIFY_BITS(d, 114);
112173
// [d 0 0 0] = [p3 0 0 0]
113174
c = (__int128)a4 * a4;
175+
VERIFY_BITS(c, 112);
114176
// [c 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
115177
d += (c & M) * R; c >>= 52;
178+
VERIFY_BITS(d, 115);
179+
VERIFY_BITS(c, 60);
116180
// [c 0 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
117181
uint64_t t3 = d & M; d >>= 52;
182+
VERIFY_BITS(t3, 52);
183+
VERIFY_BITS(d, 63);
118184
// [c 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 0 p3 0 0 0]
119185

120186
a4 *= 2;
121187
d += (__int128)a0 * a4
122188
+ (__int128)(a1*2) * a3
123189
+ (__int128)a2 * a2;
190+
VERIFY_BITS(d, 115);
124191
// [c 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
125192
d += c * R;
193+
VERIFY_BITS(d, 116);
126194
// [d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
127195
uint64_t t4 = d & M; d >>= 52;
196+
VERIFY_BITS(t4, 52);
197+
VERIFY_BITS(d, 64);
128198
// [d t4 t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
129199
uint64_t tx = (t4 >> 48); t4 &= (M >> 4);
200+
VERIFY_BITS(tx, 4);
201+
VERIFY_BITS(t4, 48);
130202
// [d t4+(tx<<48) t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0]
131203

132204
c = (__int128)a0 * a0;
205+
VERIFY_BITS(c, 112);
133206
// [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 0 p4 p3 0 0 p0]
134207
d += (__int128)a1 * a4
135208
+ (__int128)(a2*2) * a3;
209+
VERIFY_BITS(d, 114);
136210
// [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
137211
uint64_t u0 = d & M; d >>= 52;
212+
VERIFY_BITS(u0, 52);
213+
VERIFY_BITS(d, 62);
138214
// [d u0 t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
139215
// [d 0 t4+(tx<<48)+(u0<<52) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
140216
u0 = (u0 << 4) | tx;
217+
VERIFY_BITS(u0, 56);
141218
// [d 0 t4+(u0<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
142219
c += (__int128)u0 * (R >> 4);
220+
VERIFY_BITS(c, 113);
143221
// [d 0 t4 t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0]
144222
r[0] = c & M; c >>= 52;
223+
VERIFY_BITS(r[0], 52);
224+
VERIFY_BITS(c, 61);
145225
// [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 0 p0]
146226

147227
a0 *= 2;
148228
c += (__int128)a0 * a1;
229+
VERIFY_BITS(c, 114);
149230
// [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 p1 p0]
150231
d += (__int128)a2 * a4
151232
+ (__int128)a3 * a3;
233+
VERIFY_BITS(d, 114);
152234
// [d 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
153235
c += (d & M) * R; d >>= 52;
236+
VERIFY_BITS(c, 115);
237+
VERIFY_BITS(d, 62);
154238
// [d 0 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
155239
r[1] = c & M; c >>= 52;
240+
VERIFY_BITS(r[1], 52);
241+
VERIFY_BITS(c, 63);
156242
// [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 0 p1 p0]
157243

158244
c += (__int128)a0 * a2
159245
+ (__int128)a1 * a1;
246+
VERIFY_BITS(c, 114);
160247
// [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 p2 p1 p0]
161248
d += (__int128)a3 * a4;
249+
VERIFY_BITS(d, 114);
162250
// [d 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
163251
c += (d & M) * R; d >>= 52;
252+
VERIFY_BITS(c, 115);
253+
VERIFY_BITS(d, 62);
164254
// [d 0 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
165255
r[2] = c & M; c >>= 52;
256+
VERIFY_BITS(r[2], 52);
257+
VERIFY_BITS(c, 63);
166258
// [d 0 0 0 t4 t3+c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
167259

168260
c += d * R + t3;;
261+
VERIFY_BITS(c, 100);
169262
// [t4 c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
170263
r[3] = c & M; c >>= 52;
264+
VERIFY_BITS(r[3], 52);
265+
VERIFY_BITS(c, 48);
171266
// [t4+c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
172267
c += t4;
268+
VERIFY_BITS(c, 49);
173269
// [c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
174270
r[4] = c;
271+
VERIFY_BITS(r[4], 49);
175272
// [r4 r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0]
176273
}
177274

0 commit comments

Comments
 (0)