Skip to content

Commit 273bda3

Browse files
dderjoeldderjoel
committed
updated C-Fiat
1 parent 98125fd commit 273bda3

File tree

1 file changed

+104
-112
lines changed

1 file changed

+104
-112
lines changed

‎src/third_party/secp256k1_dettman_64.h

Lines changed: 104 additions & 112 deletions
Original file line numberDiff line numberDiff line change
@@ -43,75 +43,71 @@ FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef unsigned __int128 fiat_secp256k1_d
4343
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
4444
fiat_secp256k1_dettman_uint128 x1;
4545
uint64_t x2;
46-
uint64_t x3;
47-
fiat_secp256k1_dettman_uint128 x4;
46+
fiat_secp256k1_dettman_uint128 x3;
47+
uint64_t x4;
4848
uint64_t x5;
49-
uint64_t x6;
50-
fiat_secp256k1_dettman_uint128 x7;
49+
fiat_secp256k1_dettman_uint128 x6;
50+
uint64_t x7;
5151
uint64_t x8;
5252
uint64_t x9;
5353
uint64_t x10;
54-
uint64_t x11;
55-
fiat_secp256k1_dettman_uint128 x12;
54+
fiat_secp256k1_dettman_uint128 x11;
55+
uint64_t x12;
5656
uint64_t x13;
57-
uint64_t x14;
58-
fiat_secp256k1_dettman_uint128 x15;
57+
fiat_secp256k1_dettman_uint128 x14;
58+
uint64_t x15;
5959
uint64_t x16;
60-
uint64_t x17;
61-
fiat_secp256k1_dettman_uint128 x18;
60+
fiat_secp256k1_dettman_uint128 x17;
61+
uint64_t x18;
6262
uint64_t x19;
63-
uint64_t x20;
64-
fiat_secp256k1_dettman_uint128 x21;
63+
fiat_secp256k1_dettman_uint128 x20;
64+
uint64_t x21;
6565
uint64_t x22;
66-
uint64_t x23;
67-
fiat_secp256k1_dettman_uint128 x24;
68-
uint64_t x25;
66+
fiat_secp256k1_dettman_uint128 x23;
67+
uint64_t x24;
68+
fiat_secp256k1_dettman_uint128 x25;
6969
uint64_t x26;
70-
fiat_secp256k1_dettman_uint128 x27;
71-
uint64_t x28;
70+
uint64_t x27;
71+
fiat_secp256k1_dettman_uint128 x28;
7272
uint64_t x29;
73-
fiat_secp256k1_dettman_uint128 x30;
73+
uint64_t x30;
7474
uint64_t x31;
75-
uint64_t x32;
76-
uint64_t x33;
7775
x1 = ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[4]));
7876
x2 = (uint64_t)(x1 >> 64);
79-
x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
80-
x4 = ((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[0]))))) + ((fiat_secp256k1_dettman_uint128)x3 * UINT64_C(0x1000003d10)));
81-
x5 = (uint64_t)(x4 >> 52);
82-
x6 = (uint64_t)(x4 & UINT64_C(0xfffffffffffff));
83-
x7 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[0])))))) + x5) + ((fiat_secp256k1_dettman_uint128)x2 * UINT64_C(0x1000003d10000)));
84-
x8 = (uint64_t)(x7 >> 52);
85-
x9 = (uint64_t)(x7 & UINT64_C(0xfffffffffffff));
86-
x10 = (x9 >> 48);
87-
x11 = (x9 & UINT64_C(0xffffffffffff));
88-
x12 = ((((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[2])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[1]))))) + x8);
89-
x13 = (uint64_t)(x12 >> 52);
90-
x14 = (uint64_t)(x12 & UINT64_C(0xfffffffffffff));
91-
x15 = (((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)((x14 << 4) + x10) * UINT64_C(0x1000003d1)));
92-
x16 = (uint64_t)(x15 >> 52);
93-
x17 = (uint64_t)(x15 & UINT64_C(0xfffffffffffff));
94-
x18 = ((((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[3])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[2])))) + x13);
95-
x19 = (uint64_t)(x18 >> 52);
96-
x20 = (uint64_t)(x18 & UINT64_C(0xfffffffffffff));
97-
x21 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[0]))) + x16) + ((fiat_secp256k1_dettman_uint128)x20 * UINT64_C(0x1000003d10)));
98-
x22 = (uint64_t)(x21 >> 52);
99-
x23 = (uint64_t)(x21 & UINT64_C(0xfffffffffffff));
100-
x24 = ((((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[4])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[3]))) + x19);
101-
x25 = (uint64_t)(x24 >> 64);
102-
x26 = (uint64_t)(x24 & UINT64_C(0xffffffffffffffff));
103-
x27 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[0])))) + x22) + ((fiat_secp256k1_dettman_uint128)x26 * UINT64_C(0x1000003d10)));
104-
x28 = (uint64_t)(x27 >> 52);
105-
x29 = (uint64_t)(x27 & UINT64_C(0xfffffffffffff));
106-
x30 = ((x6 + x28) + ((fiat_secp256k1_dettman_uint128)x25 * UINT64_C(0x1000003d10000)));
107-
x31 = (uint64_t)(x30 >> 52);
108-
x32 = (uint64_t)(x30 & UINT64_C(0xfffffffffffff));
109-
x33 = (x11 + x31);
110-
out1[0] = x17;
111-
out1[1] = x23;
112-
out1[2] = x29;
113-
out1[3] = x32;
114-
out1[4] = x33;
77+
x3 = ((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[0]))))) + ((fiat_secp256k1_dettman_uint128)(uint64_t)x1 * UINT64_C(0x1000003d10)));
78+
x4 = (uint64_t)(x3 >> 52);
79+
x5 = (uint64_t)(x3 & UINT64_C(0xfffffffffffff));
80+
x6 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[0])))))) + x4) + ((fiat_secp256k1_dettman_uint128)x2 * UINT64_C(0x1000003d10000)));
81+
x7 = (uint64_t)(x6 >> 52);
82+
x8 = (uint64_t)(x6 & UINT64_C(0xfffffffffffff));
83+
x9 = (x8 >> 48);
84+
x10 = (x8 & UINT64_C(0xffffffffffff));
85+
x11 = ((((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[3])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[2])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[1]))))) + x7);
86+
x12 = (uint64_t)(x11 >> 52);
87+
x13 = (uint64_t)(x11 & UINT64_C(0xfffffffffffff));
88+
x14 = (((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)((x13 << 4) + x9) * UINT64_C(0x1000003d1)));
89+
x15 = (uint64_t)(x14 >> 52);
90+
x16 = (uint64_t)(x14 & UINT64_C(0xfffffffffffff));
91+
x17 = ((((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[4])) + (((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[3])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[2])))) + x12);
92+
x18 = (uint64_t)(x17 >> 52);
93+
x19 = (uint64_t)(x17 & UINT64_C(0xfffffffffffff));
94+
x20 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[0]))) + x15) + ((fiat_secp256k1_dettman_uint128)x19 * UINT64_C(0x1000003d10)));
95+
x21 = (uint64_t)(x20 >> 52);
96+
x22 = (uint64_t)(x20 & UINT64_C(0xfffffffffffff));
97+
x23 = ((((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[4])) + ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[3]))) + x18);
98+
x24 = (uint64_t)(x23 >> 64);
99+
x25 = (((((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[2])) + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[0])))) + x21) + ((fiat_secp256k1_dettman_uint128)(uint64_t)x23 * UINT64_C(0x1000003d10)));
100+
x26 = (uint64_t)(x25 >> 52);
101+
x27 = (uint64_t)(x25 & UINT64_C(0xfffffffffffff));
102+
x28 = ((x5 + x26) + ((fiat_secp256k1_dettman_uint128)x24 * UINT64_C(0x1000003d10000)));
103+
x29 = (uint64_t)(x28 >> 52);
104+
x30 = (uint64_t)(x28 & UINT64_C(0xfffffffffffff));
105+
x31 = (x10 + x29);
106+
out1[0] = x16;
107+
out1[1] = x22;
108+
out1[2] = x27;
109+
out1[3] = x30;
110+
out1[4] = x31;
115111
}
116112

117113
/*
@@ -132,77 +128,73 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_square(uin
132128
uint64_t x4;
133129
fiat_secp256k1_dettman_uint128 x5;
134130
uint64_t x6;
135-
uint64_t x7;
136-
fiat_secp256k1_dettman_uint128 x8;
131+
fiat_secp256k1_dettman_uint128 x7;
132+
uint64_t x8;
137133
uint64_t x9;
138-
uint64_t x10;
139-
fiat_secp256k1_dettman_uint128 x11;
134+
fiat_secp256k1_dettman_uint128 x10;
135+
uint64_t x11;
140136
uint64_t x12;
141137
uint64_t x13;
142138
uint64_t x14;
143-
uint64_t x15;
144-
fiat_secp256k1_dettman_uint128 x16;
139+
fiat_secp256k1_dettman_uint128 x15;
140+
uint64_t x16;
145141
uint64_t x17;
146-
uint64_t x18;
147-
fiat_secp256k1_dettman_uint128 x19;
142+
fiat_secp256k1_dettman_uint128 x18;
143+
uint64_t x19;
148144
uint64_t x20;
149-
uint64_t x21;
150-
fiat_secp256k1_dettman_uint128 x22;
145+
fiat_secp256k1_dettman_uint128 x21;
146+
uint64_t x22;
151147
uint64_t x23;
152-
uint64_t x24;
153-
fiat_secp256k1_dettman_uint128 x25;
148+
fiat_secp256k1_dettman_uint128 x24;
149+
uint64_t x25;
154150
uint64_t x26;
155-
uint64_t x27;
156-
fiat_secp256k1_dettman_uint128 x28;
157-
uint64_t x29;
151+
fiat_secp256k1_dettman_uint128 x27;
152+
uint64_t x28;
153+
fiat_secp256k1_dettman_uint128 x29;
158154
uint64_t x30;
159-
fiat_secp256k1_dettman_uint128 x31;
160-
uint64_t x32;
155+
uint64_t x31;
156+
fiat_secp256k1_dettman_uint128 x32;
161157
uint64_t x33;
162-
fiat_secp256k1_dettman_uint128 x34;
158+
uint64_t x34;
163159
uint64_t x35;
164-
uint64_t x36;
165-
uint64_t x37;
166160
x1 = ((arg1[3]) * 0x2);
167161
x2 = ((arg1[2]) * 0x2);
168162
x3 = ((arg1[1]) * 0x2);
169163
x4 = ((arg1[0]) * 0x2);
170164
x5 = ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg1[4]));
171165
x6 = (uint64_t)(x5 >> 64);
172-
x7 = (uint64_t)(x5 & UINT64_C(0xffffffffffffffff));
173-
x8 = ((((fiat_secp256k1_dettman_uint128)x4 * (arg1[3])) + ((fiat_secp256k1_dettman_uint128)x3 * (arg1[2]))) + ((fiat_secp256k1_dettman_uint128)x7 * UINT64_C(0x1000003d10)));
174-
x9 = (uint64_t)(x8 >> 52);
175-
x10 = (uint64_t)(x8 & UINT64_C(0xfffffffffffff));
176-
x11 = (((((fiat_secp256k1_dettman_uint128)x4 * (arg1[4])) + (((fiat_secp256k1_dettman_uint128)x3 * (arg1[3])) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg1[2])))) + x9) + ((fiat_secp256k1_dettman_uint128)x6 * UINT64_C(0x1000003d10000)));
177-
x12 = (uint64_t)(x11 >> 52);
178-
x13 = (uint64_t)(x11 & UINT64_C(0xfffffffffffff));
179-
x14 = (x13 >> 48);
180-
x15 = (x13 & UINT64_C(0xffffffffffff));
181-
x16 = ((((fiat_secp256k1_dettman_uint128)x3 * (arg1[4])) + ((fiat_secp256k1_dettman_uint128)x2 * (arg1[3]))) + x12);
182-
x17 = (uint64_t)(x16 >> 52);
183-
x18 = (uint64_t)(x16 & UINT64_C(0xfffffffffffff));
184-
x19 = (((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg1[0])) + ((fiat_secp256k1_dettman_uint128)((x18 << 4) + x14) * UINT64_C(0x1000003d1)));
185-
x20 = (uint64_t)(x19 >> 52);
186-
x21 = (uint64_t)(x19 & UINT64_C(0xfffffffffffff));
187-
x22 = ((((fiat_secp256k1_dettman_uint128)x2 * (arg1[4])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg1[3]))) + x17);
188-
x23 = (uint64_t)(x22 >> 52);
189-
x24 = (uint64_t)(x22 & UINT64_C(0xfffffffffffff));
190-
x25 = ((((fiat_secp256k1_dettman_uint128)x4 * (arg1[1])) + x20) + ((fiat_secp256k1_dettman_uint128)x24 * UINT64_C(0x1000003d10)));
191-
x26 = (uint64_t)(x25 >> 52);
192-
x27 = (uint64_t)(x25 & UINT64_C(0xfffffffffffff));
193-
x28 = (((fiat_secp256k1_dettman_uint128)x1 * (arg1[4])) + x23);
194-
x29 = (uint64_t)(x28 >> 64);
195-
x30 = (uint64_t)(x28 & UINT64_C(0xffffffffffffffff));
196-
x31 = (((((fiat_secp256k1_dettman_uint128)x4 * (arg1[2])) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg1[1]))) + x26) + ((fiat_secp256k1_dettman_uint128)x30 * UINT64_C(0x1000003d10)));
197-
x32 = (uint64_t)(x31 >> 52);
198-
x33 = (uint64_t)(x31 & UINT64_C(0xfffffffffffff));
199-
x34 = ((x10 + x32) + ((fiat_secp256k1_dettman_uint128)x29 * UINT64_C(0x1000003d10000)));
200-
x35 = (uint64_t)(x34 >> 52);
201-
x36 = (uint64_t)(x34 & UINT64_C(0xfffffffffffff));
202-
x37 = (x15 + x35);
203-
out1[0] = x21;
204-
out1[1] = x27;
205-
out1[2] = x33;
206-
out1[3] = x36;
207-
out1[4] = x37;
166+
x7 = ((((fiat_secp256k1_dettman_uint128)x4 * (arg1[3])) + ((fiat_secp256k1_dettman_uint128)x3 * (arg1[2]))) + ((fiat_secp256k1_dettman_uint128)(uint64_t)x5 * UINT64_C(0x1000003d10)));
167+
x8 = (uint64_t)(x7 >> 52);
168+
x9 = (uint64_t)(x7 & UINT64_C(0xfffffffffffff));
169+
x10 = (((((fiat_secp256k1_dettman_uint128)x4 * (arg1[4])) + (((fiat_secp256k1_dettman_uint128)x3 * (arg1[3])) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg1[2])))) + x8) + ((fiat_secp256k1_dettman_uint128)x6 * UINT64_C(0x1000003d10000)));
170+
x11 = (uint64_t)(x10 >> 52);
171+
x12 = (uint64_t)(x10 & UINT64_C(0xfffffffffffff));
172+
x13 = (x12 >> 48);
173+
x14 = (x12 & UINT64_C(0xffffffffffff));
174+
x15 = ((((fiat_secp256k1_dettman_uint128)x3 * (arg1[4])) + ((fiat_secp256k1_dettman_uint128)x2 * (arg1[3]))) + x11);
175+
x16 = (uint64_t)(x15 >> 52);
176+
x17 = (uint64_t)(x15 & UINT64_C(0xfffffffffffff));
177+
x18 = (((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg1[0])) + ((fiat_secp256k1_dettman_uint128)((x17 << 4) + x13) * UINT64_C(0x1000003d1)));
178+
x19 = (uint64_t)(x18 >> 52);
179+
x20 = (uint64_t)(x18 & UINT64_C(0xfffffffffffff));
180+
x21 = ((((fiat_secp256k1_dettman_uint128)x2 * (arg1[4])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg1[3]))) + x16);
181+
x22 = (uint64_t)(x21 >> 52);
182+
x23 = (uint64_t)(x21 & UINT64_C(0xfffffffffffff));
183+
x24 = ((((fiat_secp256k1_dettman_uint128)x4 * (arg1[1])) + x19) + ((fiat_secp256k1_dettman_uint128)x23 * UINT64_C(0x1000003d10)));
184+
x25 = (uint64_t)(x24 >> 52);
185+
x26 = (uint64_t)(x24 & UINT64_C(0xfffffffffffff));
186+
x27 = (((fiat_secp256k1_dettman_uint128)x1 * (arg1[4])) + x22);
187+
x28 = (uint64_t)(x27 >> 64);
188+
x29 = (((((fiat_secp256k1_dettman_uint128)x4 * (arg1[2])) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg1[1]))) + x25) + ((fiat_secp256k1_dettman_uint128)(uint64_t)x27 * UINT64_C(0x1000003d10)));
189+
x30 = (uint64_t)(x29 >> 52);
190+
x31 = (uint64_t)(x29 & UINT64_C(0xfffffffffffff));
191+
x32 = ((x9 + x30) + ((fiat_secp256k1_dettman_uint128)x28 * UINT64_C(0x1000003d10000)));
192+
x33 = (uint64_t)(x32 >> 52);
193+
x34 = (uint64_t)(x32 & UINT64_C(0xfffffffffffff));
194+
x35 = (x14 + x33);
195+
out1[0] = x20;
196+
out1[1] = x26;
197+
out1[2] = x31;
198+
out1[3] = x34;
199+
out1[4] = x35;
208200
}

0 commit comments

Comments
 (0)