aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/solinas32_2e468m17_19limbs/femul.c
blob: 91ddcff491d8d96962a5932d2c4dfe60a9c34f82 (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
static void femul(uint32_t out[19], const uint32_t in1[19], const uint32_t in2[19]) {
  { const uint32_t x38 = in1[18];
  { const uint32_t x39 = in1[17];
  { const uint32_t x37 = in1[16];
  { const uint32_t x35 = in1[15];
  { const uint32_t x33 = in1[14];
  { const uint32_t x31 = in1[13];
  { const uint32_t x29 = in1[12];
  { const uint32_t x27 = in1[11];
  { const uint32_t x25 = in1[10];
  { const uint32_t x23 = in1[9];
  { const uint32_t x21 = in1[8];
  { const uint32_t x19 = in1[7];
  { const uint32_t x17 = in1[6];
  { const uint32_t x15 = in1[5];
  { const uint32_t x13 = in1[4];
  { const uint32_t x11 = in1[3];
  { const uint32_t x9 = in1[2];
  { const uint32_t x7 = in1[1];
  { const uint32_t x5 = in1[0];
  { const uint32_t x74 = in2[18];
  { const uint32_t x75 = in2[17];
  { const uint32_t x73 = in2[16];
  { const uint32_t x71 = in2[15];
  { const uint32_t x69 = in2[14];
  { const uint32_t x67 = in2[13];
  { const uint32_t x65 = in2[12];
  { const uint32_t x63 = in2[11];
  { const uint32_t x61 = in2[10];
  { const uint32_t x59 = in2[9];
  { const uint32_t x57 = in2[8];
  { const uint32_t x55 = in2[7];
  { const uint32_t x53 = in2[6];
  { const uint32_t x51 = in2[5];
  { const uint32_t x49 = in2[4];
  { const uint32_t x47 = in2[3];
  { const uint32_t x45 = in2[2];
  { const uint32_t x43 = in2[1];
  { const uint32_t x41 = in2[0];
  { uint64_t x76 = (((uint64_t)x5 * x74) + (((uint64_t)x7 * x75) + ((0x2 * ((uint64_t)x9 * x73)) + (((uint64_t)x11 * x71) + (((uint64_t)x13 * x69) + ((0x2 * ((uint64_t)x15 * x67)) + (((uint64_t)x17 * x65) + (((uint64_t)x19 * x63) + ((0x2 * ((uint64_t)x21 * x61)) + (((uint64_t)x23 * x59) + ((0x2 * ((uint64_t)x25 * x57)) + (((uint64_t)x27 * x55) + (((uint64_t)x29 * x53) + ((0x2 * ((uint64_t)x31 * x51)) + (((uint64_t)x33 * x49) + (((uint64_t)x35 * x47) + ((0x2 * ((uint64_t)x37 * x45)) + (((uint64_t)x39 * x43) + ((uint64_t)x38 * x41)))))))))))))))))));
  { uint64_t x77 = ((((uint64_t)x5 * x75) + ((0x2 * ((uint64_t)x7 * x73)) + ((0x2 * ((uint64_t)x9 * x71)) + (((uint64_t)x11 * x69) + ((0x2 * ((uint64_t)x13 * x67)) + ((0x2 * ((uint64_t)x15 * x65)) + (((uint64_t)x17 * x63) + ((0x2 * ((uint64_t)x19 * x61)) + ((0x2 * ((uint64_t)x21 * x59)) + ((0x2 * ((uint64_t)x23 * x57)) + ((0x2 * ((uint64_t)x25 * x55)) + (((uint64_t)x27 * x53) + ((0x2 * ((uint64_t)x29 * x51)) + ((0x2 * ((uint64_t)x31 * x49)) + (((uint64_t)x33 * x47) + ((0x2 * ((uint64_t)x35 * x45)) + ((0x2 * ((uint64_t)x37 * x43)) + ((uint64_t)x39 * x41)))))))))))))))))) + (0x11 * (0x2 * ((uint64_t)x38 * x74))));
  { uint64_t x78 = ((((uint64_t)x5 * x73) + (((uint64_t)x7 * x71) + (((uint64_t)x9 * x69) + (((uint64_t)x11 * x67) + (((uint64_t)x13 * x65) + (((uint64_t)x15 * x63) + (((uint64_t)x17 * x61) + (((uint64_t)x19 * x59) + ((0x2 * ((uint64_t)x21 * x57)) + (((uint64_t)x23 * x55) + (((uint64_t)x25 * x53) + (((uint64_t)x27 * x51) + (((uint64_t)x29 * x49) + (((uint64_t)x31 * x47) + (((uint64_t)x33 * x45) + (((uint64_t)x35 * x43) + ((uint64_t)x37 * x41))))))))))))))))) + (0x11 * (((uint64_t)x39 * x74) + ((uint64_t)x38 * x75))));
  { uint64_t x79 = ((((uint64_t)x5 * x71) + (((uint64_t)x7 * x69) + ((0x2 * ((uint64_t)x9 * x67)) + (((uint64_t)x11 * x65) + (((uint64_t)x13 * x63) + ((0x2 * ((uint64_t)x15 * x61)) + (((uint64_t)x17 * x59) + ((0x2 * ((uint64_t)x19 * x57)) + ((0x2 * ((uint64_t)x21 * x55)) + (((uint64_t)x23 * x53) + ((0x2 * ((uint64_t)x25 * x51)) + (((uint64_t)x27 * x49) + (((uint64_t)x29 * x47) + ((0x2 * ((uint64_t)x31 * x45)) + (((uint64_t)x33 * x43) + ((uint64_t)x35 * x41)))))))))))))))) + (0x11 * ((0x2 * ((uint64_t)x37 * x74)) + (((uint64_t)x39 * x75) + (0x2 * ((uint64_t)x38 * x73))))));
  { uint64_t x80 = ((((uint64_t)x5 * x69) + ((0x2 * ((uint64_t)x7 * x67)) + ((0x2 * ((uint64_t)x9 * x65)) + (((uint64_t)x11 * x63) + ((0x2 * ((uint64_t)x13 * x61)) + ((0x2 * ((uint64_t)x15 * x59)) + ((0x2 * ((uint64_t)x17 * x57)) + ((0x2 * ((uint64_t)x19 * x55)) + ((0x2 * ((uint64_t)x21 * x53)) + ((0x2 * ((uint64_t)x23 * x51)) + ((0x2 * ((uint64_t)x25 * x49)) + (((uint64_t)x27 * x47) + ((0x2 * ((uint64_t)x29 * x45)) + ((0x2 * ((uint64_t)x31 * x43)) + ((uint64_t)x33 * x41))))))))))))))) + (0x11 * ((0x2 * ((uint64_t)x35 * x74)) + ((0x2 * ((uint64_t)x37 * x75)) + ((0x2 * ((uint64_t)x39 * x73)) + (0x2 * ((uint64_t)x38 * x71)))))));
  { uint64_t x81 = ((((uint64_t)x5 * x67) + (((uint64_t)x7 * x65) + (((uint64_t)x9 * x63) + (((uint64_t)x11 * x61) + (((uint64_t)x13 * x59) + ((0x2 * ((uint64_t)x15 * x57)) + (((uint64_t)x17 * x55) + (((uint64_t)x19 * x53) + ((0x2 * ((uint64_t)x21 * x51)) + (((uint64_t)x23 * x49) + (((uint64_t)x25 * x47) + (((uint64_t)x27 * x45) + (((uint64_t)x29 * x43) + ((uint64_t)x31 * x41)))))))))))))) + (0x11 * (((uint64_t)x33 * x74) + (((uint64_t)x35 * x75) + ((0x2 * ((uint64_t)x37 * x73)) + (((uint64_t)x39 * x71) + ((uint64_t)x38 * x69)))))));
  { uint64_t x82 = ((((uint64_t)x5 * x65) + (((uint64_t)x7 * x63) + ((0x2 * ((uint64_t)x9 * x61)) + (((uint64_t)x11 * x59) + ((0x2 * ((uint64_t)x13 * x57)) + ((0x2 * ((uint64_t)x15 * x55)) + (((uint64_t)x17 * x53) + ((0x2 * ((uint64_t)x19 * x51)) + ((0x2 * ((uint64_t)x21 * x49)) + (((uint64_t)x23 * x47) + ((0x2 * ((uint64_t)x25 * x45)) + (((uint64_t)x27 * x43) + ((uint64_t)x29 * x41))))))))))))) + (0x11 * ((0x2 * ((uint64_t)x31 * x74)) + (((uint64_t)x33 * x75) + ((0x2 * ((uint64_t)x35 * x73)) + ((0x2 * ((uint64_t)x37 * x71)) + (((uint64_t)x39 * x69) + (0x2 * ((uint64_t)x38 * x67)))))))));
  { uint64_t x83 = ((((uint64_t)x5 * x63) + ((0x2 * ((uint64_t)x7 * x61)) + ((0x2 * ((uint64_t)x9 * x59)) + ((0x2 * ((uint64_t)x11 * x57)) + ((0x2 * ((uint64_t)x13 * x55)) + ((0x2 * ((uint64_t)x15 * x53)) + ((0x2 * ((uint64_t)x17 * x51)) + ((0x2 * ((uint64_t)x19 * x49)) + ((0x2 * ((uint64_t)x21 * x47)) + ((0x2 * ((uint64_t)x23 * x45)) + ((0x2 * ((uint64_t)x25 * x43)) + ((uint64_t)x27 * x41)))))))))))) + (0x11 * ((0x2 * ((uint64_t)x29 * x74)) + ((0x2 * ((uint64_t)x31 * x75)) + ((0x2 * ((uint64_t)x33 * x73)) + ((0x2 * ((uint64_t)x35 * x71)) + ((0x2 * ((uint64_t)x37 * x69)) + ((0x2 * ((uint64_t)x39 * x67)) + (0x2 * ((uint64_t)x38 * x65))))))))));
  { uint64_t x84 = ((((uint64_t)x5 * x61) + (((uint64_t)x7 * x59) + ((0x2 * ((uint64_t)x9 * x57)) + (((uint64_t)x11 * x55) + (((uint64_t)x13 * x53) + ((0x2 * ((uint64_t)x15 * x51)) + (((uint64_t)x17 * x49) + (((uint64_t)x19 * x47) + ((0x2 * ((uint64_t)x21 * x45)) + (((uint64_t)x23 * x43) + ((uint64_t)x25 * x41))))))))))) + (0x11 * (((uint64_t)x27 * x74) + (((uint64_t)x29 * x75) + ((0x2 * ((uint64_t)x31 * x73)) + (((uint64_t)x33 * x71) + (((uint64_t)x35 * x69) + ((0x2 * ((uint64_t)x37 * x67)) + (((uint64_t)x39 * x65) + ((uint64_t)x38 * x63))))))))));
  { uint64_t x85 = ((((uint64_t)x5 * x59) + ((0x2 * ((uint64_t)x7 * x57)) + ((0x2 * ((uint64_t)x9 * x55)) + (((uint64_t)x11 * x53) + ((0x2 * ((uint64_t)x13 * x51)) + ((0x2 * ((uint64_t)x15 * x49)) + (((uint64_t)x17 * x47) + ((0x2 * ((uint64_t)x19 * x45)) + ((0x2 * ((uint64_t)x21 * x43)) + ((uint64_t)x23 * x41)))))))))) + (0x11 * ((0x2 * ((uint64_t)x25 * x74)) + (((uint64_t)x27 * x75) + ((0x2 * ((uint64_t)x29 * x73)) + ((0x2 * ((uint64_t)x31 * x71)) + (((uint64_t)x33 * x69) + ((0x2 * ((uint64_t)x35 * x67)) + ((0x2 * ((uint64_t)x37 * x65)) + (((uint64_t)x39 * x63) + (0x2 * ((uint64_t)x38 * x61))))))))))));
  { uint64_t x86 = ((((uint64_t)x5 * x57) + (((uint64_t)x7 * x55) + (((uint64_t)x9 * x53) + (((uint64_t)x11 * x51) + (((uint64_t)x13 * x49) + (((uint64_t)x15 * x47) + (((uint64_t)x17 * x45) + (((uint64_t)x19 * x43) + ((uint64_t)x21 * x41))))))))) + (0x11 * (((uint64_t)x23 * x74) + (((uint64_t)x25 * x75) + (((uint64_t)x27 * x73) + (((uint64_t)x29 * x71) + (((uint64_t)x31 * x69) + (((uint64_t)x33 * x67) + (((uint64_t)x35 * x65) + (((uint64_t)x37 * x63) + (((uint64_t)x39 * x61) + ((uint64_t)x38 * x59))))))))))));
  { uint64_t x87 = ((((uint64_t)x5 * x55) + (((uint64_t)x7 * x53) + ((0x2 * ((uint64_t)x9 * x51)) + (((uint64_t)x11 * x49) + (((uint64_t)x13 * x47) + ((0x2 * ((uint64_t)x15 * x45)) + (((uint64_t)x17 * x43) + ((uint64_t)x19 * x41)))))))) + (0x11 * ((0x2 * ((uint64_t)x21 * x74)) + (((uint64_t)x23 * x75) + ((0x2 * ((uint64_t)x25 * x73)) + (((uint64_t)x27 * x71) + (((uint64_t)x29 * x69) + ((0x2 * ((uint64_t)x31 * x67)) + (((uint64_t)x33 * x65) + (((uint64_t)x35 * x63) + ((0x2 * ((uint64_t)x37 * x61)) + (((uint64_t)x39 * x59) + (0x2 * ((uint64_t)x38 * x57))))))))))))));
  { uint64_t x88 = ((((uint64_t)x5 * x53) + ((0x2 * ((uint64_t)x7 * x51)) + ((0x2 * ((uint64_t)x9 * x49)) + (((uint64_t)x11 * x47) + ((0x2 * ((uint64_t)x13 * x45)) + ((0x2 * ((uint64_t)x15 * x43)) + ((uint64_t)x17 * x41))))))) + (0x11 * ((0x2 * ((uint64_t)x19 * x74)) + ((0x2 * ((uint64_t)x21 * x75)) + ((0x2 * ((uint64_t)x23 * x73)) + ((0x2 * ((uint64_t)x25 * x71)) + (((uint64_t)x27 * x69) + ((0x2 * ((uint64_t)x29 * x67)) + ((0x2 * ((uint64_t)x31 * x65)) + (((uint64_t)x33 * x63) + ((0x2 * ((uint64_t)x35 * x61)) + ((0x2 * ((uint64_t)x37 * x59)) + ((0x2 * ((uint64_t)x39 * x57)) + (0x2 * ((uint64_t)x38 * x55)))))))))))))));
  { uint64_t x89 = ((((uint64_t)x5 * x51) + (((uint64_t)x7 * x49) + (((uint64_t)x9 * x47) + (((uint64_t)x11 * x45) + (((uint64_t)x13 * x43) + ((uint64_t)x15 * x41)))))) + (0x11 * (((uint64_t)x17 * x74) + (((uint64_t)x19 * x75) + ((0x2 * ((uint64_t)x21 * x73)) + (((uint64_t)x23 * x71) + (((uint64_t)x25 * x69) + (((uint64_t)x27 * x67) + (((uint64_t)x29 * x65) + (((uint64_t)x31 * x63) + (((uint64_t)x33 * x61) + (((uint64_t)x35 * x59) + ((0x2 * ((uint64_t)x37 * x57)) + (((uint64_t)x39 * x55) + ((uint64_t)x38 * x53)))))))))))))));
  { uint64_t x90 = ((((uint64_t)x5 * x49) + (((uint64_t)x7 * x47) + ((0x2 * ((uint64_t)x9 * x45)) + (((uint64_t)x11 * x43) + ((uint64_t)x13 * x41))))) + (0x11 * ((0x2 * ((uint64_t)x15 * x74)) + (((uint64_t)x17 * x75) + ((0x2 * ((uint64_t)x19 * x73)) + ((0x2 * ((uint64_t)x21 * x71)) + (((uint64_t)x23 * x69) + ((0x2 * ((uint64_t)x25 * x67)) + (((uint64_t)x27 * x65) + (((uint64_t)x29 * x63) + ((0x2 * ((uint64_t)x31 * x61)) + (((uint64_t)x33 * x59) + ((0x2 * ((uint64_t)x35 * x57)) + ((0x2 * ((uint64_t)x37 * x55)) + (((uint64_t)x39 * x53) + (0x2 * ((uint64_t)x38 * x51)))))))))))))))));
  { uint64_t x91 = ((((uint64_t)x5 * x47) + ((0x2 * ((uint64_t)x7 * x45)) + ((0x2 * ((uint64_t)x9 * x43)) + ((uint64_t)x11 * x41)))) + (0x11 * ((0x2 * ((uint64_t)x13 * x74)) + ((0x2 * ((uint64_t)x15 * x75)) + ((0x2 * ((uint64_t)x17 * x73)) + ((0x2 * ((uint64_t)x19 * x71)) + ((0x2 * ((uint64_t)x21 * x69)) + ((0x2 * ((uint64_t)x23 * x67)) + ((0x2 * ((uint64_t)x25 * x65)) + (((uint64_t)x27 * x63) + ((0x2 * ((uint64_t)x29 * x61)) + ((0x2 * ((uint64_t)x31 * x59)) + ((0x2 * ((uint64_t)x33 * x57)) + ((0x2 * ((uint64_t)x35 * x55)) + ((0x2 * ((uint64_t)x37 * x53)) + ((0x2 * ((uint64_t)x39 * x51)) + (0x2 * ((uint64_t)x38 * x49))))))))))))))))));
  { uint64_t x92 = ((((uint64_t)x5 * x45) + (((uint64_t)x7 * x43) + ((uint64_t)x9 * x41))) + (0x11 * (((uint64_t)x11 * x74) + (((uint64_t)x13 * x75) + ((0x2 * ((uint64_t)x15 * x73)) + (((uint64_t)x17 * x71) + (((uint64_t)x19 * x69) + ((0x2 * ((uint64_t)x21 * x67)) + (((uint64_t)x23 * x65) + (((uint64_t)x25 * x63) + (((uint64_t)x27 * x61) + (((uint64_t)x29 * x59) + ((0x2 * ((uint64_t)x31 * x57)) + (((uint64_t)x33 * x55) + (((uint64_t)x35 * x53) + ((0x2 * ((uint64_t)x37 * x51)) + (((uint64_t)x39 * x49) + ((uint64_t)x38 * x47))))))))))))))))));
  { uint64_t x93 = ((((uint64_t)x5 * x43) + ((uint64_t)x7 * x41)) + (0x11 * ((0x2 * ((uint64_t)x9 * x74)) + (((uint64_t)x11 * x75) + ((0x2 * ((uint64_t)x13 * x73)) + ((0x2 * ((uint64_t)x15 * x71)) + (((uint64_t)x17 * x69) + ((0x2 * ((uint64_t)x19 * x67)) + ((0x2 * ((uint64_t)x21 * x65)) + (((uint64_t)x23 * x63) + ((0x2 * ((uint64_t)x25 * x61)) + (((uint64_t)x27 * x59) + ((0x2 * ((uint64_t)x29 * x57)) + ((0x2 * ((uint64_t)x31 * x55)) + (((uint64_t)x33 * x53) + ((0x2 * ((uint64_t)x35 * x51)) + ((0x2 * ((uint64_t)x37 * x49)) + (((uint64_t)x39 * x47) + (0x2 * ((uint64_t)x38 * x45))))))))))))))))))));
  { uint64_t x94 = (((uint64_t)x5 * x41) + (0x11 * ((0x2 * ((uint64_t)x7 * x74)) + ((0x2 * ((uint64_t)x9 * x75)) + ((0x2 * ((uint64_t)x11 * x73)) + ((0x2 * ((uint64_t)x13 * x71)) + ((0x2 * ((uint64_t)x15 * x69)) + ((0x2 * ((uint64_t)x17 * x67)) + ((0x2 * ((uint64_t)x19 * x65)) + ((0x2 * ((uint64_t)x21 * x63)) + ((0x2 * ((uint64_t)x23 * x61)) + ((0x2 * ((uint64_t)x25 * x59)) + ((0x2 * ((uint64_t)x27 * x57)) + ((0x2 * ((uint64_t)x29 * x55)) + ((0x2 * ((uint64_t)x31 * x53)) + ((0x2 * ((uint64_t)x33 * x51)) + ((0x2 * ((uint64_t)x35 * x49)) + ((0x2 * ((uint64_t)x37 * x47)) + ((0x2 * ((uint64_t)x39 * x45)) + (0x2 * ((uint64_t)x38 * x43)))))))))))))))))))));
  { uint64_t x95 = (x94 >> 0x19);
  { uint32_t x96 = ((uint32_t)x94 & 0x1ffffff);
  { uint64_t x97 = (x95 + x93);
  { uint64_t x98 = (x97 >> 0x19);
  { uint32_t x99 = ((uint32_t)x97 & 0x1ffffff);
  { uint64_t x100 = (x98 + x92);
  { uint64_t x101 = (x100 >> 0x18);
  { uint32_t x102 = ((uint32_t)x100 & 0xffffff);
  { uint64_t x103 = (x101 + x91);
  { uint64_t x104 = (x103 >> 0x19);
  { uint32_t x105 = ((uint32_t)x103 & 0x1ffffff);
  { uint64_t x106 = (x104 + x90);
  { uint64_t x107 = (x106 >> 0x19);
  { uint32_t x108 = ((uint32_t)x106 & 0x1ffffff);
  { uint64_t x109 = (x107 + x89);
  { uint64_t x110 = (x109 >> 0x18);
  { uint32_t x111 = ((uint32_t)x109 & 0xffffff);
  { uint64_t x112 = (x110 + x88);
  { uint64_t x113 = (x112 >> 0x19);
  { uint32_t x114 = ((uint32_t)x112 & 0x1ffffff);
  { uint64_t x115 = (x113 + x87);
  { uint64_t x116 = (x115 >> 0x19);
  { uint32_t x117 = ((uint32_t)x115 & 0x1ffffff);
  { uint64_t x118 = (x116 + x86);
  { uint64_t x119 = (x118 >> 0x18);
  { uint32_t x120 = ((uint32_t)x118 & 0xffffff);
  { uint64_t x121 = (x119 + x85);
  { uint64_t x122 = (x121 >> 0x19);
  { uint32_t x123 = ((uint32_t)x121 & 0x1ffffff);
  { uint64_t x124 = (x122 + x84);
  { uint64_t x125 = (x124 >> 0x18);
  { uint32_t x126 = ((uint32_t)x124 & 0xffffff);
  { uint64_t x127 = (x125 + x83);
  { uint64_t x128 = (x127 >> 0x19);
  { uint32_t x129 = ((uint32_t)x127 & 0x1ffffff);
  { uint64_t x130 = (x128 + x82);
  { uint64_t x131 = (x130 >> 0x19);
  { uint32_t x132 = ((uint32_t)x130 & 0x1ffffff);
  { uint64_t x133 = (x131 + x81);
  { uint64_t x134 = (x133 >> 0x18);
  { uint32_t x135 = ((uint32_t)x133 & 0xffffff);
  { uint64_t x136 = (x134 + x80);
  { uint64_t x137 = (x136 >> 0x19);
  { uint32_t x138 = ((uint32_t)x136 & 0x1ffffff);
  { uint64_t x139 = (x137 + x79);
  { uint64_t x140 = (x139 >> 0x19);
  { uint32_t x141 = ((uint32_t)x139 & 0x1ffffff);
  { uint64_t x142 = (x140 + x78);
  { uint64_t x143 = (x142 >> 0x18);
  { uint32_t x144 = ((uint32_t)x142 & 0xffffff);
  { uint64_t x145 = (x143 + x77);
  { uint64_t x146 = (x145 >> 0x19);
  { uint32_t x147 = ((uint32_t)x145 & 0x1ffffff);
  { uint64_t x148 = (x146 + x76);
  { uint64_t x149 = (x148 >> 0x18);
  { uint32_t x150 = ((uint32_t)x148 & 0xffffff);
  { uint64_t x151 = (x96 + (0x11 * x149));
  { uint32_t x152 = (uint32_t) (x151 >> 0x19);
  { uint32_t x153 = ((uint32_t)x151 & 0x1ffffff);
  { uint32_t x154 = (x152 + x99);
  { uint32_t x155 = (x154 >> 0x19);
  { uint32_t x156 = (x154 & 0x1ffffff);
  out[0] = x153;
  out[1] = x156;
  out[2] = (x155 + x102);
  out[3] = x105;
  out[4] = x108;
  out[5] = x111;
  out[6] = x114;
  out[7] = x117;
  out[8] = x120;
  out[9] = x123;
  out[10] = x126;
  out[11] = x129;
  out[12] = x132;
  out[13] = x135;
  out[14] = x138;
  out[15] = x141;
  out[16] = x144;
  out[17] = x147;
  out[18] = x150;
  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
}