aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/solinas32_2e480m2e240m1_20limbs/fesquare.c
blob: 599462a501dac9eeb732aa80bd07be16c8b22cf0 (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
static void fesquare(uint32_t out[20], const uint32_t in1[20]) {
  { const uint32_t x37 = in1[19];
  { const uint32_t x38 = in1[18];
  { const uint32_t x36 = in1[17];
  { const uint32_t x34 = in1[16];
  { const uint32_t x32 = in1[15];
  { const uint32_t x30 = in1[14];
  { const uint32_t x28 = in1[13];
  { const uint32_t x26 = in1[12];
  { const uint32_t x24 = in1[11];
  { const uint32_t x22 = in1[10];
  { const uint32_t x20 = in1[9];
  { const uint32_t x18 = in1[8];
  { const uint32_t x16 = in1[7];
  { const uint32_t x14 = in1[6];
  { const uint32_t x12 = in1[5];
  { const uint32_t x10 = in1[4];
  { const uint32_t x8 = in1[3];
  { const uint32_t x6 = in1[2];
  { const uint32_t x4 = in1[1];
  { const uint32_t x2 = in1[0];
  { uint64_t x39 = (((uint64_t)(x20 + x37) * (x20 + x37)) - ((uint64_t)x20 * x20));
  { uint64_t x40 = ((((uint64_t)(x18 + x38) * (x20 + x37)) + ((uint64_t)(x20 + x37) * (x18 + x38))) - (((uint64_t)x18 * x20) + ((uint64_t)x20 * x18)));
  { uint64_t x41 = ((((uint64_t)(x16 + x36) * (x20 + x37)) + (((uint64_t)(x18 + x38) * (x18 + x38)) + ((uint64_t)(x20 + x37) * (x16 + x36)))) - (((uint64_t)x16 * x20) + (((uint64_t)x18 * x18) + ((uint64_t)x20 * x16))));
  { uint64_t x42 = ((((uint64_t)(x14 + x34) * (x20 + x37)) + (((uint64_t)(x16 + x36) * (x18 + x38)) + (((uint64_t)(x18 + x38) * (x16 + x36)) + ((uint64_t)(x20 + x37) * (x14 + x34))))) - (((uint64_t)x14 * x20) + (((uint64_t)x16 * x18) + (((uint64_t)x18 * x16) + ((uint64_t)x20 * x14)))));
  { uint64_t x43 = ((((uint64_t)(x12 + x32) * (x20 + x37)) + (((uint64_t)(x14 + x34) * (x18 + x38)) + (((uint64_t)(x16 + x36) * (x16 + x36)) + (((uint64_t)(x18 + x38) * (x14 + x34)) + ((uint64_t)(x20 + x37) * (x12 + x32)))))) - (((uint64_t)x12 * x20) + (((uint64_t)x14 * x18) + (((uint64_t)x16 * x16) + (((uint64_t)x18 * x14) + ((uint64_t)x20 * x12))))));
  { uint64_t x44 = ((((uint64_t)(x10 + x30) * (x20 + x37)) + (((uint64_t)(x12 + x32) * (x18 + x38)) + (((uint64_t)(x14 + x34) * (x16 + x36)) + (((uint64_t)(x16 + x36) * (x14 + x34)) + (((uint64_t)(x18 + x38) * (x12 + x32)) + ((uint64_t)(x20 + x37) * (x10 + x30))))))) - (((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + ((uint64_t)x20 * x10)))))));
  { uint64_t x45 = ((((uint64_t)(x8 + x28) * (x20 + x37)) + (((uint64_t)(x10 + x30) * (x18 + x38)) + (((uint64_t)(x12 + x32) * (x16 + x36)) + (((uint64_t)(x14 + x34) * (x14 + x34)) + (((uint64_t)(x16 + x36) * (x12 + x32)) + (((uint64_t)(x18 + x38) * (x10 + x30)) + ((uint64_t)(x20 + x37) * (x8 + x28)))))))) - (((uint64_t)x8 * x20) + (((uint64_t)x10 * x18) + (((uint64_t)x12 * x16) + (((uint64_t)x14 * x14) + (((uint64_t)x16 * x12) + (((uint64_t)x18 * x10) + ((uint64_t)x20 * x8))))))));
  { uint64_t x46 = ((((uint64_t)(x6 + x26) * (x20 + x37)) + (((uint64_t)(x8 + x28) * (x18 + x38)) + (((uint64_t)(x10 + x30) * (x16 + x36)) + (((uint64_t)(x12 + x32) * (x14 + x34)) + (((uint64_t)(x14 + x34) * (x12 + x32)) + (((uint64_t)(x16 + x36) * (x10 + x30)) + (((uint64_t)(x18 + x38) * (x8 + x28)) + ((uint64_t)(x20 + x37) * (x6 + x26))))))))) - (((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + (((uint64_t)x10 * x16) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + (((uint64_t)x16 * x10) + (((uint64_t)x18 * x8) + ((uint64_t)x20 * x6)))))))));
  { uint64_t x47 = ((((uint64_t)(x4 + x24) * (x20 + x37)) + (((uint64_t)(x6 + x26) * (x18 + x38)) + (((uint64_t)(x8 + x28) * (x16 + x36)) + (((uint64_t)(x10 + x30) * (x14 + x34)) + (((uint64_t)(x12 + x32) * (x12 + x32)) + (((uint64_t)(x14 + x34) * (x10 + x30)) + (((uint64_t)(x16 + x36) * (x8 + x28)) + (((uint64_t)(x18 + x38) * (x6 + x26)) + ((uint64_t)(x20 + x37) * (x4 + x24)))))))))) - (((uint64_t)x4 * x20) + (((uint64_t)x6 * x18) + (((uint64_t)x8 * x16) + (((uint64_t)x10 * x14) + (((uint64_t)x12 * x12) + (((uint64_t)x14 * x10) + (((uint64_t)x16 * x8) + (((uint64_t)x18 * x6) + ((uint64_t)x20 * x4))))))))));
  { uint64_t x48 = ((((uint64_t)(x2 + x22) * (x20 + x37)) + (((uint64_t)(x4 + x24) * (x18 + x38)) + (((uint64_t)(x6 + x26) * (x16 + x36)) + (((uint64_t)(x8 + x28) * (x14 + x34)) + (((uint64_t)(x10 + x30) * (x12 + x32)) + (((uint64_t)(x12 + x32) * (x10 + x30)) + (((uint64_t)(x14 + x34) * (x8 + x28)) + (((uint64_t)(x16 + x36) * (x6 + x26)) + (((uint64_t)(x18 + x38) * (x4 + x24)) + ((uint64_t)(x20 + x37) * (x2 + x22))))))))))) - (((uint64_t)x2 * x20) + (((uint64_t)x4 * x18) + (((uint64_t)x6 * x16) + (((uint64_t)x8 * x14) + (((uint64_t)x10 * x12) + (((uint64_t)x12 * x10) + (((uint64_t)x14 * x8) + (((uint64_t)x16 * x6) + (((uint64_t)x18 * x4) + ((uint64_t)x20 * x2)))))))))));
  { uint64_t x49 = ((((uint64_t)(x2 + x22) * (x18 + x38)) + (((uint64_t)(x4 + x24) * (x16 + x36)) + (((uint64_t)(x6 + x26) * (x14 + x34)) + (((uint64_t)(x8 + x28) * (x12 + x32)) + (((uint64_t)(x10 + x30) * (x10 + x30)) + (((uint64_t)(x12 + x32) * (x8 + x28)) + (((uint64_t)(x14 + x34) * (x6 + x26)) + (((uint64_t)(x16 + x36) * (x4 + x24)) + ((uint64_t)(x18 + x38) * (x2 + x22)))))))))) - (((uint64_t)x2 * x18) + (((uint64_t)x4 * x16) + (((uint64_t)x6 * x14) + (((uint64_t)x8 * x12) + (((uint64_t)x10 * x10) + (((uint64_t)x12 * x8) + (((uint64_t)x14 * x6) + (((uint64_t)x16 * x4) + ((uint64_t)x18 * x2))))))))));
  { uint64_t x50 = ((((uint64_t)(x2 + x22) * (x16 + x36)) + (((uint64_t)(x4 + x24) * (x14 + x34)) + (((uint64_t)(x6 + x26) * (x12 + x32)) + (((uint64_t)(x8 + x28) * (x10 + x30)) + (((uint64_t)(x10 + x30) * (x8 + x28)) + (((uint64_t)(x12 + x32) * (x6 + x26)) + (((uint64_t)(x14 + x34) * (x4 + x24)) + ((uint64_t)(x16 + x36) * (x2 + x22))))))))) - (((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))));
  { uint64_t x51 = ((((uint64_t)(x2 + x22) * (x14 + x34)) + (((uint64_t)(x4 + x24) * (x12 + x32)) + (((uint64_t)(x6 + x26) * (x10 + x30)) + (((uint64_t)(x8 + x28) * (x8 + x28)) + (((uint64_t)(x10 + x30) * (x6 + x26)) + (((uint64_t)(x12 + x32) * (x4 + x24)) + ((uint64_t)(x14 + x34) * (x2 + x22)))))))) - (((uint64_t)x2 * x14) + (((uint64_t)x4 * x12) + (((uint64_t)x6 * x10) + (((uint64_t)x8 * x8) + (((uint64_t)x10 * x6) + (((uint64_t)x12 * x4) + ((uint64_t)x14 * x2))))))));
  { uint64_t x52 = ((((uint64_t)(x2 + x22) * (x12 + x32)) + (((uint64_t)(x4 + x24) * (x10 + x30)) + (((uint64_t)(x6 + x26) * (x8 + x28)) + (((uint64_t)(x8 + x28) * (x6 + x26)) + (((uint64_t)(x10 + x30) * (x4 + x24)) + ((uint64_t)(x12 + x32) * (x2 + x22))))))) - (((uint64_t)x2 * x12) + (((uint64_t)x4 * x10) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + (((uint64_t)x10 * x4) + ((uint64_t)x12 * x2)))))));
  { uint64_t x53 = ((((uint64_t)(x2 + x22) * (x10 + x30)) + (((uint64_t)(x4 + x24) * (x8 + x28)) + (((uint64_t)(x6 + x26) * (x6 + x26)) + (((uint64_t)(x8 + x28) * (x4 + x24)) + ((uint64_t)(x10 + x30) * (x2 + x22)))))) - (((uint64_t)x2 * x10) + (((uint64_t)x4 * x8) + (((uint64_t)x6 * x6) + (((uint64_t)x8 * x4) + ((uint64_t)x10 * x2))))));
  { uint64_t x54 = ((((uint64_t)(x2 + x22) * (x8 + x28)) + (((uint64_t)(x4 + x24) * (x6 + x26)) + (((uint64_t)(x6 + x26) * (x4 + x24)) + ((uint64_t)(x8 + x28) * (x2 + x22))))) - (((uint64_t)x2 * x8) + (((uint64_t)x4 * x6) + (((uint64_t)x6 * x4) + ((uint64_t)x8 * x2)))));
  { uint64_t x55 = ((((uint64_t)(x2 + x22) * (x6 + x26)) + (((uint64_t)(x4 + x24) * (x4 + x24)) + ((uint64_t)(x6 + x26) * (x2 + x22)))) - (((uint64_t)x2 * x6) + (((uint64_t)x4 * x4) + ((uint64_t)x6 * x2))));
  { uint64_t x56 = ((((uint64_t)(x2 + x22) * (x4 + x24)) + ((uint64_t)(x4 + x24) * (x2 + x22))) - (((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)));
  { uint64_t x57 = (((uint64_t)(x2 + x22) * (x2 + x22)) - ((uint64_t)x2 * x2));
  { uint64_t x58 = (((((uint64_t)x20 * x20) + ((uint64_t)x37 * x37)) + x49) + x39);
  { uint64_t x59 = ((((((uint64_t)x18 * x20) + ((uint64_t)x20 * x18)) + (((uint64_t)x38 * x37) + ((uint64_t)x37 * x38))) + x50) + x40);
  { uint64_t x60 = ((((((uint64_t)x16 * x20) + (((uint64_t)x18 * x18) + ((uint64_t)x20 * x16))) + (((uint64_t)x36 * x37) + (((uint64_t)x38 * x38) + ((uint64_t)x37 * x36)))) + x51) + x41);
  { uint64_t x61 = ((((((uint64_t)x14 * x20) + (((uint64_t)x16 * x18) + (((uint64_t)x18 * x16) + ((uint64_t)x20 * x14)))) + (((uint64_t)x34 * x37) + (((uint64_t)x36 * x38) + (((uint64_t)x38 * x36) + ((uint64_t)x37 * x34))))) + x52) + x42);
  { uint64_t x62 = ((((((uint64_t)x12 * x20) + (((uint64_t)x14 * x18) + (((uint64_t)x16 * x16) + (((uint64_t)x18 * x14) + ((uint64_t)x20 * x12))))) + (((uint64_t)x32 * x37) + (((uint64_t)x34 * x38) + (((uint64_t)x36 * x36) + (((uint64_t)x38 * x34) + ((uint64_t)x37 * x32)))))) + x53) + x43);
  { uint64_t x63 = ((((((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + ((uint64_t)x20 * x10)))))) + (((uint64_t)x30 * x37) + (((uint64_t)x32 * x38) + (((uint64_t)x34 * x36) + (((uint64_t)x36 * x34) + (((uint64_t)x38 * x32) + ((uint64_t)x37 * x30))))))) + x54) + x44);
  { uint64_t x64 = ((((((uint64_t)x8 * x20) + (((uint64_t)x10 * x18) + (((uint64_t)x12 * x16) + (((uint64_t)x14 * x14) + (((uint64_t)x16 * x12) + (((uint64_t)x18 * x10) + ((uint64_t)x20 * x8))))))) + (((uint64_t)x28 * x37) + (((uint64_t)x30 * x38) + (((uint64_t)x32 * x36) + (((uint64_t)x34 * x34) + (((uint64_t)x36 * x32) + (((uint64_t)x38 * x30) + ((uint64_t)x37 * x28)))))))) + x55) + x45);
  { uint64_t x65 = ((((((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + (((uint64_t)x10 * x16) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + (((uint64_t)x16 * x10) + (((uint64_t)x18 * x8) + ((uint64_t)x20 * x6)))))))) + (((uint64_t)x26 * x37) + (((uint64_t)x28 * x38) + (((uint64_t)x30 * x36) + (((uint64_t)x32 * x34) + (((uint64_t)x34 * x32) + (((uint64_t)x36 * x30) + (((uint64_t)x38 * x28) + ((uint64_t)x37 * x26))))))))) + x56) + x46);
  { uint64_t x66 = ((((((uint64_t)x4 * x20) + (((uint64_t)x6 * x18) + (((uint64_t)x8 * x16) + (((uint64_t)x10 * x14) + (((uint64_t)x12 * x12) + (((uint64_t)x14 * x10) + (((uint64_t)x16 * x8) + (((uint64_t)x18 * x6) + ((uint64_t)x20 * x4))))))))) + (((uint64_t)x24 * x37) + (((uint64_t)x26 * x38) + (((uint64_t)x28 * x36) + (((uint64_t)x30 * x34) + (((uint64_t)x32 * x32) + (((uint64_t)x34 * x30) + (((uint64_t)x36 * x28) + (((uint64_t)x38 * x26) + ((uint64_t)x37 * x24)))))))))) + x57) + x47);
  { uint64_t x67 = ((((uint64_t)x2 * x20) + (((uint64_t)x4 * x18) + (((uint64_t)x6 * x16) + (((uint64_t)x8 * x14) + (((uint64_t)x10 * x12) + (((uint64_t)x12 * x10) + (((uint64_t)x14 * x8) + (((uint64_t)x16 * x6) + (((uint64_t)x18 * x4) + ((uint64_t)x20 * x2)))))))))) + (((uint64_t)x22 * x37) + (((uint64_t)x24 * x38) + (((uint64_t)x26 * x36) + (((uint64_t)x28 * x34) + (((uint64_t)x30 * x32) + (((uint64_t)x32 * x30) + (((uint64_t)x34 * x28) + (((uint64_t)x36 * x26) + (((uint64_t)x38 * x24) + ((uint64_t)x37 * x22)))))))))));
  { uint64_t x68 = (((((uint64_t)x2 * x18) + (((uint64_t)x4 * x16) + (((uint64_t)x6 * x14) + (((uint64_t)x8 * x12) + (((uint64_t)x10 * x10) + (((uint64_t)x12 * x8) + (((uint64_t)x14 * x6) + (((uint64_t)x16 * x4) + ((uint64_t)x18 * x2))))))))) + (((uint64_t)x22 * x38) + (((uint64_t)x24 * x36) + (((uint64_t)x26 * x34) + (((uint64_t)x28 * x32) + (((uint64_t)x30 * x30) + (((uint64_t)x32 * x28) + (((uint64_t)x34 * x26) + (((uint64_t)x36 * x24) + ((uint64_t)x38 * x22)))))))))) + x39);
  { uint64_t x69 = (((((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))) + (((uint64_t)x22 * x36) + (((uint64_t)x24 * x34) + (((uint64_t)x26 * x32) + (((uint64_t)x28 * x30) + (((uint64_t)x30 * x28) + (((uint64_t)x32 * x26) + (((uint64_t)x34 * x24) + ((uint64_t)x36 * x22))))))))) + x40);
  { uint64_t x70 = (((((uint64_t)x2 * x14) + (((uint64_t)x4 * x12) + (((uint64_t)x6 * x10) + (((uint64_t)x8 * x8) + (((uint64_t)x10 * x6) + (((uint64_t)x12 * x4) + ((uint64_t)x14 * x2))))))) + (((uint64_t)x22 * x34) + (((uint64_t)x24 * x32) + (((uint64_t)x26 * x30) + (((uint64_t)x28 * x28) + (((uint64_t)x30 * x26) + (((uint64_t)x32 * x24) + ((uint64_t)x34 * x22)))))))) + x41);
  { uint64_t x71 = (((((uint64_t)x2 * x12) + (((uint64_t)x4 * x10) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + (((uint64_t)x10 * x4) + ((uint64_t)x12 * x2)))))) + (((uint64_t)x22 * x32) + (((uint64_t)x24 * x30) + (((uint64_t)x26 * x28) + (((uint64_t)x28 * x26) + (((uint64_t)x30 * x24) + ((uint64_t)x32 * x22))))))) + x42);
  { uint64_t x72 = (((((uint64_t)x2 * x10) + (((uint64_t)x4 * x8) + (((uint64_t)x6 * x6) + (((uint64_t)x8 * x4) + ((uint64_t)x10 * x2))))) + (((uint64_t)x22 * x30) + (((uint64_t)x24 * x28) + (((uint64_t)x26 * x26) + (((uint64_t)x28 * x24) + ((uint64_t)x30 * x22)))))) + x43);
  { uint64_t x73 = (((((uint64_t)x2 * x8) + (((uint64_t)x4 * x6) + (((uint64_t)x6 * x4) + ((uint64_t)x8 * x2)))) + (((uint64_t)x22 * x28) + (((uint64_t)x24 * x26) + (((uint64_t)x26 * x24) + ((uint64_t)x28 * x22))))) + x44);
  { uint64_t x74 = (((((uint64_t)x2 * x6) + (((uint64_t)x4 * x4) + ((uint64_t)x6 * x2))) + (((uint64_t)x22 * x26) + (((uint64_t)x24 * x24) + ((uint64_t)x26 * x22)))) + x45);
  { uint64_t x75 = (((((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)) + (((uint64_t)x22 * x24) + ((uint64_t)x24 * x22))) + x46);
  { uint64_t x76 = ((((uint64_t)x2 * x2) + ((uint64_t)x22 * x22)) + x47);
  { uint32_t x77 = (uint32_t) (x67 >> 0x18);
  { uint32_t x78 = ((uint32_t)x67 & 0xffffff);
  { uint64_t x79 = (x48 >> 0x18);
  { uint32_t x80 = ((uint32_t)x48 & 0xffffff);
  { uint64_t x81 = ((0x1000000 * x79) + x80);
  { uint64_t x82 = (x81 >> 0x18);
  { uint32_t x83 = ((uint32_t)x81 & 0xffffff);
  { uint64_t x84 = ((x77 + x66) + x82);
  { uint64_t x85 = (x84 >> 0x18);
  { uint32_t x86 = ((uint32_t)x84 & 0xffffff);
  { uint64_t x87 = (x76 + x82);
  { uint64_t x88 = (x87 >> 0x18);
  { uint32_t x89 = ((uint32_t)x87 & 0xffffff);
  { uint64_t x90 = (x85 + x65);
  { uint64_t x91 = (x90 >> 0x18);
  { uint32_t x92 = ((uint32_t)x90 & 0xffffff);
  { uint64_t x93 = (x88 + x75);
  { uint64_t x94 = (x93 >> 0x18);
  { uint32_t x95 = ((uint32_t)x93 & 0xffffff);
  { uint64_t x96 = (x91 + x64);
  { uint64_t x97 = (x96 >> 0x18);
  { uint32_t x98 = ((uint32_t)x96 & 0xffffff);
  { uint64_t x99 = (x94 + x74);
  { uint64_t x100 = (x99 >> 0x18);
  { uint32_t x101 = ((uint32_t)x99 & 0xffffff);
  { uint64_t x102 = (x97 + x63);
  { uint64_t x103 = (x102 >> 0x18);
  { uint32_t x104 = ((uint32_t)x102 & 0xffffff);
  { uint64_t x105 = (x100 + x73);
  { uint64_t x106 = (x105 >> 0x18);
  { uint32_t x107 = ((uint32_t)x105 & 0xffffff);
  { uint64_t x108 = (x103 + x62);
  { uint64_t x109 = (x108 >> 0x18);
  { uint32_t x110 = ((uint32_t)x108 & 0xffffff);
  { uint64_t x111 = (x106 + x72);
  { uint64_t x112 = (x111 >> 0x18);
  { uint32_t x113 = ((uint32_t)x111 & 0xffffff);
  { uint64_t x114 = (x109 + x61);
  { uint64_t x115 = (x114 >> 0x18);
  { uint32_t x116 = ((uint32_t)x114 & 0xffffff);
  { uint64_t x117 = (x112 + x71);
  { uint64_t x118 = (x117 >> 0x18);
  { uint32_t x119 = ((uint32_t)x117 & 0xffffff);
  { uint64_t x120 = (x115 + x60);
  { uint64_t x121 = (x120 >> 0x18);
  { uint32_t x122 = ((uint32_t)x120 & 0xffffff);
  { uint64_t x123 = (x118 + x70);
  { uint64_t x124 = (x123 >> 0x18);
  { uint32_t x125 = ((uint32_t)x123 & 0xffffff);
  { uint64_t x126 = (x121 + x59);
  { uint64_t x127 = (x126 >> 0x18);
  { uint32_t x128 = ((uint32_t)x126 & 0xffffff);
  { uint64_t x129 = (x124 + x69);
  { uint32_t x130 = (uint32_t) (x129 >> 0x18);
  { uint32_t x131 = ((uint32_t)x129 & 0xffffff);
  { uint64_t x132 = (x127 + x58);
  { uint64_t x133 = (x132 >> 0x18);
  { uint32_t x134 = ((uint32_t)x132 & 0xffffff);
  { uint64_t x135 = (x130 + x68);
  { uint32_t x136 = (uint32_t) (x135 >> 0x18);
  { uint32_t x137 = ((uint32_t)x135 & 0xffffff);
  { uint64_t x138 = (x133 + x83);
  { uint32_t x139 = (uint32_t) (x138 >> 0x18);
  { uint32_t x140 = ((uint32_t)x138 & 0xffffff);
  { uint32_t x141 = (x136 + x78);
  { uint32_t x142 = (x141 >> 0x18);
  { uint32_t x143 = (x141 & 0xffffff);
  { uint64_t x144 = (((uint64_t)0x1000000 * x139) + x140);
  { uint32_t x145 = (uint32_t) (x144 >> 0x18);
  { uint32_t x146 = ((uint32_t)x144 & 0xffffff);
  { uint32_t x147 = ((x142 + x86) + x145);
  { uint32_t x148 = (x147 >> 0x18);
  { uint32_t x149 = (x147 & 0xffffff);
  { uint32_t x150 = (x89 + x145);
  { uint32_t x151 = (x150 >> 0x18);
  { uint32_t x152 = (x150 & 0xffffff);
  out[0] = x152;
  out[1] = (x151 + x95);
  out[2] = x101;
  out[3] = x107;
  out[4] = x113;
  out[5] = x119;
  out[6] = x125;
  out[7] = x131;
  out[8] = x137;
  out[9] = x143;
  out[10] = x149;
  out[11] = (x148 + x92);
  out[12] = x98;
  out[13] = x104;
  out[14] = x110;
  out[15] = x116;
  out[16] = x122;
  out[17] = x128;
  out[18] = x134;
  out[19] = x146;
  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
}