1 /* Autogenerated: src/ExtractionOCaml/unsaturated_solinas --static 25519 10 '2^255 - 19' 32 carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes carry_scmul121666 */ 2 /* curve description: 25519 */ 3 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, carry_scmul121666 */ 4 /* n = 10 (from "10") */ 5 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */ 6 /* machine_wordsize = 32 (from "32") */ 7 8 /* Computed values: */ 9 /* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */ 10 11 #include <stdint.h> 12 typedef unsigned char fiat_25519_uint1; 13 typedef signed char fiat_25519_int1; 14 15 #if (-1 & 3) != 3 16 #error "This code only works on a two's complement system" 17 #endif 18 19 20 /* 21 * The function fiat_25519_addcarryx_u26 is an addition with carry. 22 * Postconditions: 23 * out1 = (arg1 + arg2 + arg3) mod 2^26 24 * out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋ 25 * 26 * Input Bounds: 27 * arg1: [0x0 ~> 0x1] 28 * arg2: [0x0 ~> 0x3ffffff] 29 * arg3: [0x0 ~> 0x3ffffff] 30 * Output Bounds: 31 * out1: [0x0 ~> 0x3ffffff] 32 * out2: [0x0 ~> 0x1] 33 */ 34 static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 35 uint32_t x1 = ((arg1 + arg2) + arg3); 36 uint32_t x2 = (x1 & UINT32_C(0x3ffffff)); 37 fiat_25519_uint1 x3 = (fiat_25519_uint1)(x1 >> 26); 38 *out1 = x2; 39 *out2 = x3; 40 } 41 42 /* 43 * The function fiat_25519_subborrowx_u26 is a subtraction with borrow. 44 * Postconditions: 45 * out1 = (-arg1 + arg2 + -arg3) mod 2^26 46 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋ 47 * 48 * Input Bounds: 49 * arg1: [0x0 ~> 0x1] 50 * arg2: [0x0 ~> 0x3ffffff] 51 * arg3: [0x0 ~> 0x3ffffff] 52 * Output Bounds: 53 * out1: [0x0 ~> 0x3ffffff] 54 * out2: [0x0 ~> 0x1] 55 */ 56 static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 57 int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); 58 fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 26); 59 uint32_t x3 = (x1 & UINT32_C(0x3ffffff)); 60 *out1 = x3; 61 *out2 = (fiat_25519_uint1)(0x0 - x2); 62 } 63 64 /* 65 * The function fiat_25519_addcarryx_u25 is an addition with carry. 66 * Postconditions: 67 * out1 = (arg1 + arg2 + arg3) mod 2^25 68 * out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ 69 * 70 * Input Bounds: 71 * arg1: [0x0 ~> 0x1] 72 * arg2: [0x0 ~> 0x1ffffff] 73 * arg3: [0x0 ~> 0x1ffffff] 74 * Output Bounds: 75 * out1: [0x0 ~> 0x1ffffff] 76 * out2: [0x0 ~> 0x1] 77 */ 78 static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 79 uint32_t x1 = ((arg1 + arg2) + arg3); 80 uint32_t x2 = (x1 & UINT32_C(0x1ffffff)); 81 fiat_25519_uint1 x3 = (fiat_25519_uint1)(x1 >> 25); 82 *out1 = x2; 83 *out2 = x3; 84 } 85 86 /* 87 * The function fiat_25519_subborrowx_u25 is a subtraction with borrow. 88 * Postconditions: 89 * out1 = (-arg1 + arg2 + -arg3) mod 2^25 90 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ 91 * 92 * Input Bounds: 93 * arg1: [0x0 ~> 0x1] 94 * arg2: [0x0 ~> 0x1ffffff] 95 * arg3: [0x0 ~> 0x1ffffff] 96 * Output Bounds: 97 * out1: [0x0 ~> 0x1ffffff] 98 * out2: [0x0 ~> 0x1] 99 */ 100 static void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 101 int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); 102 fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 25); 103 uint32_t x3 = (x1 & UINT32_C(0x1ffffff)); 104 *out1 = x3; 105 *out2 = (fiat_25519_uint1)(0x0 - x2); 106 } 107 108 /* 109 * The function fiat_25519_cmovznz_u32 is a single-word conditional move. 110 * Postconditions: 111 * out1 = (if arg1 = 0 then arg2 else arg3) 112 * 113 * Input Bounds: 114 * arg1: [0x0 ~> 0x1] 115 * arg2: [0x0 ~> 0xffffffff] 116 * arg3: [0x0 ~> 0xffffffff] 117 * Output Bounds: 118 * out1: [0x0 ~> 0xffffffff] 119 */ 120 static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { 121 fiat_25519_uint1 x1 = (!(!arg1)); 122 uint32_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT32_C(0xffffffff)); 123 // Note this line has been patched from the synthesized code to add value 124 // barriers. 125 // 126 // Clang recognizes this pattern as a select. While it usually transforms it 127 // to a cmov, it sometimes further transforms it into a branch, which we do 128 // not want. 129 uint32_t x3 = ((value_barrier_u32(x2) & arg3) | (value_barrier_u32(~x2) & arg2)); 130 *out1 = x3; 131 } 132 133 /* 134 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. 135 * Postconditions: 136 * eval out1 mod m = (eval arg1 * eval arg2) mod m 137 * 138 * Input Bounds: 139 * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 140 * arg2: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 141 * Output Bounds: 142 * out1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 143 */ 144 static void fiat_25519_carry_mul(uint32_t out1[10], const uint32_t arg1[10], const uint32_t arg2[10]) { 145 uint64_t x1 = ((uint64_t)(arg1[9]) * ((arg2[9]) * UINT8_C(0x26))); 146 uint64_t x2 = ((uint64_t)(arg1[9]) * ((arg2[8]) * UINT8_C(0x13))); 147 uint64_t x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * UINT8_C(0x26))); 148 uint64_t x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * UINT8_C(0x13))); 149 uint64_t x5 = ((uint64_t)(arg1[9]) * ((arg2[5]) * UINT8_C(0x26))); 150 uint64_t x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * UINT8_C(0x13))); 151 uint64_t x7 = ((uint64_t)(arg1[9]) * ((arg2[3]) * UINT8_C(0x26))); 152 uint64_t x8 = ((uint64_t)(arg1[9]) * ((arg2[2]) * UINT8_C(0x13))); 153 uint64_t x9 = ((uint64_t)(arg1[9]) * ((arg2[1]) * UINT8_C(0x26))); 154 uint64_t x10 = ((uint64_t)(arg1[8]) * ((arg2[9]) * UINT8_C(0x13))); 155 uint64_t x11 = ((uint64_t)(arg1[8]) * ((arg2[8]) * UINT8_C(0x13))); 156 uint64_t x12 = ((uint64_t)(arg1[8]) * ((arg2[7]) * UINT8_C(0x13))); 157 uint64_t x13 = ((uint64_t)(arg1[8]) * ((arg2[6]) * UINT8_C(0x13))); 158 uint64_t x14 = ((uint64_t)(arg1[8]) * ((arg2[5]) * UINT8_C(0x13))); 159 uint64_t x15 = ((uint64_t)(arg1[8]) * ((arg2[4]) * UINT8_C(0x13))); 160 uint64_t x16 = ((uint64_t)(arg1[8]) * ((arg2[3]) * UINT8_C(0x13))); 161 uint64_t x17 = ((uint64_t)(arg1[8]) * ((arg2[2]) * UINT8_C(0x13))); 162 uint64_t x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * UINT8_C(0x26))); 163 uint64_t x19 = ((uint64_t)(arg1[7]) * ((arg2[8]) * UINT8_C(0x13))); 164 uint64_t x20 = ((uint64_t)(arg1[7]) * ((arg2[7]) * UINT8_C(0x26))); 165 uint64_t x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * UINT8_C(0x13))); 166 uint64_t x22 = ((uint64_t)(arg1[7]) * ((arg2[5]) * UINT8_C(0x26))); 167 uint64_t x23 = ((uint64_t)(arg1[7]) * ((arg2[4]) * UINT8_C(0x13))); 168 uint64_t x24 = ((uint64_t)(arg1[7]) * ((arg2[3]) * UINT8_C(0x26))); 169 uint64_t x25 = ((uint64_t)(arg1[6]) * ((arg2[9]) * UINT8_C(0x13))); 170 uint64_t x26 = ((uint64_t)(arg1[6]) * ((arg2[8]) * UINT8_C(0x13))); 171 uint64_t x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * UINT8_C(0x13))); 172 uint64_t x28 = ((uint64_t)(arg1[6]) * ((arg2[6]) * UINT8_C(0x13))); 173 uint64_t x29 = ((uint64_t)(arg1[6]) * ((arg2[5]) * UINT8_C(0x13))); 174 uint64_t x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * UINT8_C(0x13))); 175 uint64_t x31 = ((uint64_t)(arg1[5]) * ((arg2[9]) * UINT8_C(0x26))); 176 uint64_t x32 = ((uint64_t)(arg1[5]) * ((arg2[8]) * UINT8_C(0x13))); 177 uint64_t x33 = ((uint64_t)(arg1[5]) * ((arg2[7]) * UINT8_C(0x26))); 178 uint64_t x34 = ((uint64_t)(arg1[5]) * ((arg2[6]) * UINT8_C(0x13))); 179 uint64_t x35 = ((uint64_t)(arg1[5]) * ((arg2[5]) * UINT8_C(0x26))); 180 uint64_t x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * UINT8_C(0x13))); 181 uint64_t x37 = ((uint64_t)(arg1[4]) * ((arg2[8]) * UINT8_C(0x13))); 182 uint64_t x38 = ((uint64_t)(arg1[4]) * ((arg2[7]) * UINT8_C(0x13))); 183 uint64_t x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * UINT8_C(0x13))); 184 uint64_t x40 = ((uint64_t)(arg1[3]) * ((arg2[9]) * UINT8_C(0x26))); 185 uint64_t x41 = ((uint64_t)(arg1[3]) * ((arg2[8]) * UINT8_C(0x13))); 186 uint64_t x42 = ((uint64_t)(arg1[3]) * ((arg2[7]) * UINT8_C(0x26))); 187 uint64_t x43 = ((uint64_t)(arg1[2]) * ((arg2[9]) * UINT8_C(0x13))); 188 uint64_t x44 = ((uint64_t)(arg1[2]) * ((arg2[8]) * UINT8_C(0x13))); 189 uint64_t x45 = ((uint64_t)(arg1[1]) * ((arg2[9]) * UINT8_C(0x26))); 190 uint64_t x46 = ((uint64_t)(arg1[9]) * (arg2[0])); 191 uint64_t x47 = ((uint64_t)(arg1[8]) * (arg2[1])); 192 uint64_t x48 = ((uint64_t)(arg1[8]) * (arg2[0])); 193 uint64_t x49 = ((uint64_t)(arg1[7]) * (arg2[2])); 194 uint64_t x50 = ((uint64_t)(arg1[7]) * ((arg2[1]) * 0x2)); 195 uint64_t x51 = ((uint64_t)(arg1[7]) * (arg2[0])); 196 uint64_t x52 = ((uint64_t)(arg1[6]) * (arg2[3])); 197 uint64_t x53 = ((uint64_t)(arg1[6]) * (arg2[2])); 198 uint64_t x54 = ((uint64_t)(arg1[6]) * (arg2[1])); 199 uint64_t x55 = ((uint64_t)(arg1[6]) * (arg2[0])); 200 uint64_t x56 = ((uint64_t)(arg1[5]) * (arg2[4])); 201 uint64_t x57 = ((uint64_t)(arg1[5]) * ((arg2[3]) * 0x2)); 202 uint64_t x58 = ((uint64_t)(arg1[5]) * (arg2[2])); 203 uint64_t x59 = ((uint64_t)(arg1[5]) * ((arg2[1]) * 0x2)); 204 uint64_t x60 = ((uint64_t)(arg1[5]) * (arg2[0])); 205 uint64_t x61 = ((uint64_t)(arg1[4]) * (arg2[5])); 206 uint64_t x62 = ((uint64_t)(arg1[4]) * (arg2[4])); 207 uint64_t x63 = ((uint64_t)(arg1[4]) * (arg2[3])); 208 uint64_t x64 = ((uint64_t)(arg1[4]) * (arg2[2])); 209 uint64_t x65 = ((uint64_t)(arg1[4]) * (arg2[1])); 210 uint64_t x66 = ((uint64_t)(arg1[4]) * (arg2[0])); 211 uint64_t x67 = ((uint64_t)(arg1[3]) * (arg2[6])); 212 uint64_t x68 = ((uint64_t)(arg1[3]) * ((arg2[5]) * 0x2)); 213 uint64_t x69 = ((uint64_t)(arg1[3]) * (arg2[4])); 214 uint64_t x70 = ((uint64_t)(arg1[3]) * ((arg2[3]) * 0x2)); 215 uint64_t x71 = ((uint64_t)(arg1[3]) * (arg2[2])); 216 uint64_t x72 = ((uint64_t)(arg1[3]) * ((arg2[1]) * 0x2)); 217 uint64_t x73 = ((uint64_t)(arg1[3]) * (arg2[0])); 218 uint64_t x74 = ((uint64_t)(arg1[2]) * (arg2[7])); 219 uint64_t x75 = ((uint64_t)(arg1[2]) * (arg2[6])); 220 uint64_t x76 = ((uint64_t)(arg1[2]) * (arg2[5])); 221 uint64_t x77 = ((uint64_t)(arg1[2]) * (arg2[4])); 222 uint64_t x78 = ((uint64_t)(arg1[2]) * (arg2[3])); 223 uint64_t x79 = ((uint64_t)(arg1[2]) * (arg2[2])); 224 uint64_t x80 = ((uint64_t)(arg1[2]) * (arg2[1])); 225 uint64_t x81 = ((uint64_t)(arg1[2]) * (arg2[0])); 226 uint64_t x82 = ((uint64_t)(arg1[1]) * (arg2[8])); 227 uint64_t x83 = ((uint64_t)(arg1[1]) * ((arg2[7]) * 0x2)); 228 uint64_t x84 = ((uint64_t)(arg1[1]) * (arg2[6])); 229 uint64_t x85 = ((uint64_t)(arg1[1]) * ((arg2[5]) * 0x2)); 230 uint64_t x86 = ((uint64_t)(arg1[1]) * (arg2[4])); 231 uint64_t x87 = ((uint64_t)(arg1[1]) * ((arg2[3]) * 0x2)); 232 uint64_t x88 = ((uint64_t)(arg1[1]) * (arg2[2])); 233 uint64_t x89 = ((uint64_t)(arg1[1]) * ((arg2[1]) * 0x2)); 234 uint64_t x90 = ((uint64_t)(arg1[1]) * (arg2[0])); 235 uint64_t x91 = ((uint64_t)(arg1[0]) * (arg2[9])); 236 uint64_t x92 = ((uint64_t)(arg1[0]) * (arg2[8])); 237 uint64_t x93 = ((uint64_t)(arg1[0]) * (arg2[7])); 238 uint64_t x94 = ((uint64_t)(arg1[0]) * (arg2[6])); 239 uint64_t x95 = ((uint64_t)(arg1[0]) * (arg2[5])); 240 uint64_t x96 = ((uint64_t)(arg1[0]) * (arg2[4])); 241 uint64_t x97 = ((uint64_t)(arg1[0]) * (arg2[3])); 242 uint64_t x98 = ((uint64_t)(arg1[0]) * (arg2[2])); 243 uint64_t x99 = ((uint64_t)(arg1[0]) * (arg2[1])); 244 uint64_t x100 = ((uint64_t)(arg1[0]) * (arg2[0])); 245 uint64_t x101 = (x100 + (x45 + (x44 + (x42 + (x39 + (x35 + (x30 + (x24 + (x17 + x9))))))))); 246 uint64_t x102 = (x101 >> 26); 247 uint32_t x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff)); 248 uint64_t x104 = (x91 + (x82 + (x74 + (x67 + (x61 + (x56 + (x52 + (x49 + (x47 + x46))))))))); 249 uint64_t x105 = (x92 + (x83 + (x75 + (x68 + (x62 + (x57 + (x53 + (x50 + (x48 + x1))))))))); 250 uint64_t x106 = (x93 + (x84 + (x76 + (x69 + (x63 + (x58 + (x54 + (x51 + (x10 + x2))))))))); 251 uint64_t x107 = (x94 + (x85 + (x77 + (x70 + (x64 + (x59 + (x55 + (x18 + (x11 + x3))))))))); 252 uint64_t x108 = (x95 + (x86 + (x78 + (x71 + (x65 + (x60 + (x25 + (x19 + (x12 + x4))))))))); 253 uint64_t x109 = (x96 + (x87 + (x79 + (x72 + (x66 + (x31 + (x26 + (x20 + (x13 + x5))))))))); 254 uint64_t x110 = (x97 + (x88 + (x80 + (x73 + (x36 + (x32 + (x27 + (x21 + (x14 + x6))))))))); 255 uint64_t x111 = (x98 + (x89 + (x81 + (x40 + (x37 + (x33 + (x28 + (x22 + (x15 + x7))))))))); 256 uint64_t x112 = (x99 + (x90 + (x43 + (x41 + (x38 + (x34 + (x29 + (x23 + (x16 + x8))))))))); 257 uint64_t x113 = (x102 + x112); 258 uint64_t x114 = (x113 >> 25); 259 uint32_t x115 = (uint32_t)(x113 & UINT32_C(0x1ffffff)); 260 uint64_t x116 = (x114 + x111); 261 uint64_t x117 = (x116 >> 26); 262 uint32_t x118 = (uint32_t)(x116 & UINT32_C(0x3ffffff)); 263 uint64_t x119 = (x117 + x110); 264 uint64_t x120 = (x119 >> 25); 265 uint32_t x121 = (uint32_t)(x119 & UINT32_C(0x1ffffff)); 266 uint64_t x122 = (x120 + x109); 267 uint64_t x123 = (x122 >> 26); 268 uint32_t x124 = (uint32_t)(x122 & UINT32_C(0x3ffffff)); 269 uint64_t x125 = (x123 + x108); 270 uint64_t x126 = (x125 >> 25); 271 uint32_t x127 = (uint32_t)(x125 & UINT32_C(0x1ffffff)); 272 uint64_t x128 = (x126 + x107); 273 uint64_t x129 = (x128 >> 26); 274 uint32_t x130 = (uint32_t)(x128 & UINT32_C(0x3ffffff)); 275 uint64_t x131 = (x129 + x106); 276 uint64_t x132 = (x131 >> 25); 277 uint32_t x133 = (uint32_t)(x131 & UINT32_C(0x1ffffff)); 278 uint64_t x134 = (x132 + x105); 279 uint64_t x135 = (x134 >> 26); 280 uint32_t x136 = (uint32_t)(x134 & UINT32_C(0x3ffffff)); 281 uint64_t x137 = (x135 + x104); 282 uint64_t x138 = (x137 >> 25); 283 uint32_t x139 = (uint32_t)(x137 & UINT32_C(0x1ffffff)); 284 uint64_t x140 = (x138 * UINT8_C(0x13)); 285 uint64_t x141 = (x103 + x140); 286 uint32_t x142 = (uint32_t)(x141 >> 26); 287 uint32_t x143 = (uint32_t)(x141 & UINT32_C(0x3ffffff)); 288 uint32_t x144 = (x142 + x115); 289 fiat_25519_uint1 x145 = (fiat_25519_uint1)(x144 >> 25); 290 uint32_t x146 = (x144 & UINT32_C(0x1ffffff)); 291 uint32_t x147 = (x145 + x118); 292 out1[0] = x143; 293 out1[1] = x146; 294 out1[2] = x147; 295 out1[3] = x121; 296 out1[4] = x124; 297 out1[5] = x127; 298 out1[6] = x130; 299 out1[7] = x133; 300 out1[8] = x136; 301 out1[9] = x139; 302 } 303 304 /* 305 * The function fiat_25519_carry_square squares a field element and reduces the result. 306 * Postconditions: 307 * eval out1 mod m = (eval arg1 * eval arg1) mod m 308 * 309 * Input Bounds: 310 * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 311 * Output Bounds: 312 * out1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 313 */ 314 static void fiat_25519_carry_square(uint32_t out1[10], const uint32_t arg1[10]) { 315 uint32_t x1 = ((arg1[9]) * UINT8_C(0x13)); 316 uint32_t x2 = (x1 * 0x2); 317 uint32_t x3 = ((arg1[9]) * 0x2); 318 uint32_t x4 = ((arg1[8]) * UINT8_C(0x13)); 319 uint64_t x5 = ((uint64_t)x4 * 0x2); 320 uint32_t x6 = ((arg1[8]) * 0x2); 321 uint32_t x7 = ((arg1[7]) * UINT8_C(0x13)); 322 uint32_t x8 = (x7 * 0x2); 323 uint32_t x9 = ((arg1[7]) * 0x2); 324 uint32_t x10 = ((arg1[6]) * UINT8_C(0x13)); 325 uint64_t x11 = ((uint64_t)x10 * 0x2); 326 uint32_t x12 = ((arg1[6]) * 0x2); 327 uint32_t x13 = ((arg1[5]) * UINT8_C(0x13)); 328 uint32_t x14 = ((arg1[5]) * 0x2); 329 uint32_t x15 = ((arg1[4]) * 0x2); 330 uint32_t x16 = ((arg1[3]) * 0x2); 331 uint32_t x17 = ((arg1[2]) * 0x2); 332 uint32_t x18 = ((arg1[1]) * 0x2); 333 uint64_t x19 = ((uint64_t)(arg1[9]) * (x1 * 0x2)); 334 uint64_t x20 = ((uint64_t)(arg1[8]) * x2); 335 uint64_t x21 = ((uint64_t)(arg1[8]) * x4); 336 uint64_t x22 = ((arg1[7]) * ((uint64_t)x2 * 0x2)); 337 uint64_t x23 = ((arg1[7]) * x5); 338 uint64_t x24 = ((uint64_t)(arg1[7]) * (x7 * 0x2)); 339 uint64_t x25 = ((uint64_t)(arg1[6]) * x2); 340 uint64_t x26 = ((arg1[6]) * x5); 341 uint64_t x27 = ((uint64_t)(arg1[6]) * x8); 342 uint64_t x28 = ((uint64_t)(arg1[6]) * x10); 343 uint64_t x29 = ((arg1[5]) * ((uint64_t)x2 * 0x2)); 344 uint64_t x30 = ((arg1[5]) * x5); 345 uint64_t x31 = ((arg1[5]) * ((uint64_t)x8 * 0x2)); 346 uint64_t x32 = ((arg1[5]) * x11); 347 uint64_t x33 = ((uint64_t)(arg1[5]) * (x13 * 0x2)); 348 uint64_t x34 = ((uint64_t)(arg1[4]) * x2); 349 uint64_t x35 = ((arg1[4]) * x5); 350 uint64_t x36 = ((uint64_t)(arg1[4]) * x8); 351 uint64_t x37 = ((arg1[4]) * x11); 352 uint64_t x38 = ((uint64_t)(arg1[4]) * x14); 353 uint64_t x39 = ((uint64_t)(arg1[4]) * (arg1[4])); 354 uint64_t x40 = ((arg1[3]) * ((uint64_t)x2 * 0x2)); 355 uint64_t x41 = ((arg1[3]) * x5); 356 uint64_t x42 = ((arg1[3]) * ((uint64_t)x8 * 0x2)); 357 uint64_t x43 = ((uint64_t)(arg1[3]) * x12); 358 uint64_t x44 = ((uint64_t)(arg1[3]) * (x14 * 0x2)); 359 uint64_t x45 = ((uint64_t)(arg1[3]) * x15); 360 uint64_t x46 = ((uint64_t)(arg1[3]) * ((arg1[3]) * 0x2)); 361 uint64_t x47 = ((uint64_t)(arg1[2]) * x2); 362 uint64_t x48 = ((arg1[2]) * x5); 363 uint64_t x49 = ((uint64_t)(arg1[2]) * x9); 364 uint64_t x50 = ((uint64_t)(arg1[2]) * x12); 365 uint64_t x51 = ((uint64_t)(arg1[2]) * x14); 366 uint64_t x52 = ((uint64_t)(arg1[2]) * x15); 367 uint64_t x53 = ((uint64_t)(arg1[2]) * x16); 368 uint64_t x54 = ((uint64_t)(arg1[2]) * (arg1[2])); 369 uint64_t x55 = ((arg1[1]) * ((uint64_t)x2 * 0x2)); 370 uint64_t x56 = ((uint64_t)(arg1[1]) * x6); 371 uint64_t x57 = ((uint64_t)(arg1[1]) * (x9 * 0x2)); 372 uint64_t x58 = ((uint64_t)(arg1[1]) * x12); 373 uint64_t x59 = ((uint64_t)(arg1[1]) * (x14 * 0x2)); 374 uint64_t x60 = ((uint64_t)(arg1[1]) * x15); 375 uint64_t x61 = ((uint64_t)(arg1[1]) * (x16 * 0x2)); 376 uint64_t x62 = ((uint64_t)(arg1[1]) * x17); 377 uint64_t x63 = ((uint64_t)(arg1[1]) * ((arg1[1]) * 0x2)); 378 uint64_t x64 = ((uint64_t)(arg1[0]) * x3); 379 uint64_t x65 = ((uint64_t)(arg1[0]) * x6); 380 uint64_t x66 = ((uint64_t)(arg1[0]) * x9); 381 uint64_t x67 = ((uint64_t)(arg1[0]) * x12); 382 uint64_t x68 = ((uint64_t)(arg1[0]) * x14); 383 uint64_t x69 = ((uint64_t)(arg1[0]) * x15); 384 uint64_t x70 = ((uint64_t)(arg1[0]) * x16); 385 uint64_t x71 = ((uint64_t)(arg1[0]) * x17); 386 uint64_t x72 = ((uint64_t)(arg1[0]) * x18); 387 uint64_t x73 = ((uint64_t)(arg1[0]) * (arg1[0])); 388 uint64_t x74 = (x73 + (x55 + (x48 + (x42 + (x37 + x33))))); 389 uint64_t x75 = (x74 >> 26); 390 uint32_t x76 = (uint32_t)(x74 & UINT32_C(0x3ffffff)); 391 uint64_t x77 = (x64 + (x56 + (x49 + (x43 + x38)))); 392 uint64_t x78 = (x65 + (x57 + (x50 + (x44 + (x39 + x19))))); 393 uint64_t x79 = (x66 + (x58 + (x51 + (x45 + x20)))); 394 uint64_t x80 = (x67 + (x59 + (x52 + (x46 + (x22 + x21))))); 395 uint64_t x81 = (x68 + (x60 + (x53 + (x25 + x23)))); 396 uint64_t x82 = (x69 + (x61 + (x54 + (x29 + (x26 + x24))))); 397 uint64_t x83 = (x70 + (x62 + (x34 + (x30 + x27)))); 398 uint64_t x84 = (x71 + (x63 + (x40 + (x35 + (x31 + x28))))); 399 uint64_t x85 = (x72 + (x47 + (x41 + (x36 + x32)))); 400 uint64_t x86 = (x75 + x85); 401 uint64_t x87 = (x86 >> 25); 402 uint32_t x88 = (uint32_t)(x86 & UINT32_C(0x1ffffff)); 403 uint64_t x89 = (x87 + x84); 404 uint64_t x90 = (x89 >> 26); 405 uint32_t x91 = (uint32_t)(x89 & UINT32_C(0x3ffffff)); 406 uint64_t x92 = (x90 + x83); 407 uint64_t x93 = (x92 >> 25); 408 uint32_t x94 = (uint32_t)(x92 & UINT32_C(0x1ffffff)); 409 uint64_t x95 = (x93 + x82); 410 uint64_t x96 = (x95 >> 26); 411 uint32_t x97 = (uint32_t)(x95 & UINT32_C(0x3ffffff)); 412 uint64_t x98 = (x96 + x81); 413 uint64_t x99 = (x98 >> 25); 414 uint32_t x100 = (uint32_t)(x98 & UINT32_C(0x1ffffff)); 415 uint64_t x101 = (x99 + x80); 416 uint64_t x102 = (x101 >> 26); 417 uint32_t x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff)); 418 uint64_t x104 = (x102 + x79); 419 uint64_t x105 = (x104 >> 25); 420 uint32_t x106 = (uint32_t)(x104 & UINT32_C(0x1ffffff)); 421 uint64_t x107 = (x105 + x78); 422 uint64_t x108 = (x107 >> 26); 423 uint32_t x109 = (uint32_t)(x107 & UINT32_C(0x3ffffff)); 424 uint64_t x110 = (x108 + x77); 425 uint64_t x111 = (x110 >> 25); 426 uint32_t x112 = (uint32_t)(x110 & UINT32_C(0x1ffffff)); 427 uint64_t x113 = (x111 * UINT8_C(0x13)); 428 uint64_t x114 = (x76 + x113); 429 uint32_t x115 = (uint32_t)(x114 >> 26); 430 uint32_t x116 = (uint32_t)(x114 & UINT32_C(0x3ffffff)); 431 uint32_t x117 = (x115 + x88); 432 fiat_25519_uint1 x118 = (fiat_25519_uint1)(x117 >> 25); 433 uint32_t x119 = (x117 & UINT32_C(0x1ffffff)); 434 uint32_t x120 = (x118 + x91); 435 out1[0] = x116; 436 out1[1] = x119; 437 out1[2] = x120; 438 out1[3] = x94; 439 out1[4] = x97; 440 out1[5] = x100; 441 out1[6] = x103; 442 out1[7] = x106; 443 out1[8] = x109; 444 out1[9] = x112; 445 } 446 447 /* 448 * The function fiat_25519_carry reduces a field element. 449 * Postconditions: 450 * eval out1 mod m = eval arg1 mod m 451 * 452 * Input Bounds: 453 * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 454 * Output Bounds: 455 * out1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 456 */ 457 static void fiat_25519_carry(uint32_t out1[10], const uint32_t arg1[10]) { 458 uint32_t x1 = (arg1[0]); 459 uint32_t x2 = ((x1 >> 26) + (arg1[1])); 460 uint32_t x3 = ((x2 >> 25) + (arg1[2])); 461 uint32_t x4 = ((x3 >> 26) + (arg1[3])); 462 uint32_t x5 = ((x4 >> 25) + (arg1[4])); 463 uint32_t x6 = ((x5 >> 26) + (arg1[5])); 464 uint32_t x7 = ((x6 >> 25) + (arg1[6])); 465 uint32_t x8 = ((x7 >> 26) + (arg1[7])); 466 uint32_t x9 = ((x8 >> 25) + (arg1[8])); 467 uint32_t x10 = ((x9 >> 26) + (arg1[9])); 468 uint32_t x11 = ((x1 & UINT32_C(0x3ffffff)) + ((x10 >> 25) * UINT8_C(0x13))); 469 uint32_t x12 = ((fiat_25519_uint1)(x11 >> 26) + (x2 & UINT32_C(0x1ffffff))); 470 uint32_t x13 = (x11 & UINT32_C(0x3ffffff)); 471 uint32_t x14 = (x12 & UINT32_C(0x1ffffff)); 472 uint32_t x15 = ((fiat_25519_uint1)(x12 >> 25) + (x3 & UINT32_C(0x3ffffff))); 473 uint32_t x16 = (x4 & UINT32_C(0x1ffffff)); 474 uint32_t x17 = (x5 & UINT32_C(0x3ffffff)); 475 uint32_t x18 = (x6 & UINT32_C(0x1ffffff)); 476 uint32_t x19 = (x7 & UINT32_C(0x3ffffff)); 477 uint32_t x20 = (x8 & UINT32_C(0x1ffffff)); 478 uint32_t x21 = (x9 & UINT32_C(0x3ffffff)); 479 uint32_t x22 = (x10 & UINT32_C(0x1ffffff)); 480 out1[0] = x13; 481 out1[1] = x14; 482 out1[2] = x15; 483 out1[3] = x16; 484 out1[4] = x17; 485 out1[5] = x18; 486 out1[6] = x19; 487 out1[7] = x20; 488 out1[8] = x21; 489 out1[9] = x22; 490 } 491 492 /* 493 * The function fiat_25519_add adds two field elements. 494 * Postconditions: 495 * eval out1 mod m = (eval arg1 + eval arg2) mod m 496 * 497 * Input Bounds: 498 * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 499 * arg2: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 500 * Output Bounds: 501 * out1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 502 */ 503 static void fiat_25519_add(uint32_t out1[10], const uint32_t arg1[10], const uint32_t arg2[10]) { 504 uint32_t x1 = ((arg1[0]) + (arg2[0])); 505 uint32_t x2 = ((arg1[1]) + (arg2[1])); 506 uint32_t x3 = ((arg1[2]) + (arg2[2])); 507 uint32_t x4 = ((arg1[3]) + (arg2[3])); 508 uint32_t x5 = ((arg1[4]) + (arg2[4])); 509 uint32_t x6 = ((arg1[5]) + (arg2[5])); 510 uint32_t x7 = ((arg1[6]) + (arg2[6])); 511 uint32_t x8 = ((arg1[7]) + (arg2[7])); 512 uint32_t x9 = ((arg1[8]) + (arg2[8])); 513 uint32_t x10 = ((arg1[9]) + (arg2[9])); 514 out1[0] = x1; 515 out1[1] = x2; 516 out1[2] = x3; 517 out1[3] = x4; 518 out1[4] = x5; 519 out1[5] = x6; 520 out1[6] = x7; 521 out1[7] = x8; 522 out1[8] = x9; 523 out1[9] = x10; 524 } 525 526 /* 527 * The function fiat_25519_sub subtracts two field elements. 528 * Postconditions: 529 * eval out1 mod m = (eval arg1 - eval arg2) mod m 530 * 531 * Input Bounds: 532 * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 533 * arg2: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 534 * Output Bounds: 535 * out1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 536 */ 537 static void fiat_25519_sub(uint32_t out1[10], const uint32_t arg1[10], const uint32_t arg2[10]) { 538 uint32_t x1 = ((UINT32_C(0x7ffffda) + (arg1[0])) - (arg2[0])); 539 uint32_t x2 = ((UINT32_C(0x3fffffe) + (arg1[1])) - (arg2[1])); 540 uint32_t x3 = ((UINT32_C(0x7fffffe) + (arg1[2])) - (arg2[2])); 541 uint32_t x4 = ((UINT32_C(0x3fffffe) + (arg1[3])) - (arg2[3])); 542 uint32_t x5 = ((UINT32_C(0x7fffffe) + (arg1[4])) - (arg2[4])); 543 uint32_t x6 = ((UINT32_C(0x3fffffe) + (arg1[5])) - (arg2[5])); 544 uint32_t x7 = ((UINT32_C(0x7fffffe) + (arg1[6])) - (arg2[6])); 545 uint32_t x8 = ((UINT32_C(0x3fffffe) + (arg1[7])) - (arg2[7])); 546 uint32_t x9 = ((UINT32_C(0x7fffffe) + (arg1[8])) - (arg2[8])); 547 uint32_t x10 = ((UINT32_C(0x3fffffe) + (arg1[9])) - (arg2[9])); 548 out1[0] = x1; 549 out1[1] = x2; 550 out1[2] = x3; 551 out1[3] = x4; 552 out1[4] = x5; 553 out1[5] = x6; 554 out1[6] = x7; 555 out1[7] = x8; 556 out1[8] = x9; 557 out1[9] = x10; 558 } 559 560 /* 561 * The function fiat_25519_opp negates a field element. 562 * Postconditions: 563 * eval out1 mod m = -eval arg1 mod m 564 * 565 * Input Bounds: 566 * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 567 * Output Bounds: 568 * out1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 569 */ 570 static void fiat_25519_opp(uint32_t out1[10], const uint32_t arg1[10]) { 571 uint32_t x1 = (UINT32_C(0x7ffffda) - (arg1[0])); 572 uint32_t x2 = (UINT32_C(0x3fffffe) - (arg1[1])); 573 uint32_t x3 = (UINT32_C(0x7fffffe) - (arg1[2])); 574 uint32_t x4 = (UINT32_C(0x3fffffe) - (arg1[3])); 575 uint32_t x5 = (UINT32_C(0x7fffffe) - (arg1[4])); 576 uint32_t x6 = (UINT32_C(0x3fffffe) - (arg1[5])); 577 uint32_t x7 = (UINT32_C(0x7fffffe) - (arg1[6])); 578 uint32_t x8 = (UINT32_C(0x3fffffe) - (arg1[7])); 579 uint32_t x9 = (UINT32_C(0x7fffffe) - (arg1[8])); 580 uint32_t x10 = (UINT32_C(0x3fffffe) - (arg1[9])); 581 out1[0] = x1; 582 out1[1] = x2; 583 out1[2] = x3; 584 out1[3] = x4; 585 out1[4] = x5; 586 out1[5] = x6; 587 out1[6] = x7; 588 out1[7] = x8; 589 out1[8] = x9; 590 out1[9] = x10; 591 } 592 593 /* 594 * The function fiat_25519_selectznz is a multi-limb conditional select. 595 * Postconditions: 596 * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) 597 * 598 * Input Bounds: 599 * arg1: [0x0 ~> 0x1] 600 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 601 * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 602 * Output Bounds: 603 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] 604 */ 605 static void fiat_25519_selectznz(uint32_t out1[10], fiat_25519_uint1 arg1, const uint32_t arg2[10], const uint32_t arg3[10]) { 606 uint32_t x1; 607 fiat_25519_cmovznz_u32(&x1, arg1, (arg2[0]), (arg3[0])); 608 uint32_t x2; 609 fiat_25519_cmovznz_u32(&x2, arg1, (arg2[1]), (arg3[1])); 610 uint32_t x3; 611 fiat_25519_cmovznz_u32(&x3, arg1, (arg2[2]), (arg3[2])); 612 uint32_t x4; 613 fiat_25519_cmovznz_u32(&x4, arg1, (arg2[3]), (arg3[3])); 614 uint32_t x5; 615 fiat_25519_cmovznz_u32(&x5, arg1, (arg2[4]), (arg3[4])); 616 uint32_t x6; 617 fiat_25519_cmovznz_u32(&x6, arg1, (arg2[5]), (arg3[5])); 618 uint32_t x7; 619 fiat_25519_cmovznz_u32(&x7, arg1, (arg2[6]), (arg3[6])); 620 uint32_t x8; 621 fiat_25519_cmovznz_u32(&x8, arg1, (arg2[7]), (arg3[7])); 622 uint32_t x9; 623 fiat_25519_cmovznz_u32(&x9, arg1, (arg2[8]), (arg3[8])); 624 uint32_t x10; 625 fiat_25519_cmovznz_u32(&x10, arg1, (arg2[9]), (arg3[9])); 626 out1[0] = x1; 627 out1[1] = x2; 628 out1[2] = x3; 629 out1[3] = x4; 630 out1[4] = x5; 631 out1[5] = x6; 632 out1[6] = x7; 633 out1[7] = x8; 634 out1[8] = x9; 635 out1[9] = x10; 636 } 637 638 /* 639 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. 640 * Postconditions: 641 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] 642 * 643 * Input Bounds: 644 * arg1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 645 * Output Bounds: 646 * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]] 647 */ 648 static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { 649 uint32_t x1; 650 fiat_25519_uint1 x2; 651 fiat_25519_subborrowx_u26(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0x3ffffed)); 652 uint32_t x3; 653 fiat_25519_uint1 x4; 654 fiat_25519_subborrowx_u25(&x3, &x4, x2, (arg1[1]), UINT32_C(0x1ffffff)); 655 uint32_t x5; 656 fiat_25519_uint1 x6; 657 fiat_25519_subborrowx_u26(&x5, &x6, x4, (arg1[2]), UINT32_C(0x3ffffff)); 658 uint32_t x7; 659 fiat_25519_uint1 x8; 660 fiat_25519_subborrowx_u25(&x7, &x8, x6, (arg1[3]), UINT32_C(0x1ffffff)); 661 uint32_t x9; 662 fiat_25519_uint1 x10; 663 fiat_25519_subborrowx_u26(&x9, &x10, x8, (arg1[4]), UINT32_C(0x3ffffff)); 664 uint32_t x11; 665 fiat_25519_uint1 x12; 666 fiat_25519_subborrowx_u25(&x11, &x12, x10, (arg1[5]), UINT32_C(0x1ffffff)); 667 uint32_t x13; 668 fiat_25519_uint1 x14; 669 fiat_25519_subborrowx_u26(&x13, &x14, x12, (arg1[6]), UINT32_C(0x3ffffff)); 670 uint32_t x15; 671 fiat_25519_uint1 x16; 672 fiat_25519_subborrowx_u25(&x15, &x16, x14, (arg1[7]), UINT32_C(0x1ffffff)); 673 uint32_t x17; 674 fiat_25519_uint1 x18; 675 fiat_25519_subborrowx_u26(&x17, &x18, x16, (arg1[8]), UINT32_C(0x3ffffff)); 676 uint32_t x19; 677 fiat_25519_uint1 x20; 678 fiat_25519_subborrowx_u25(&x19, &x20, x18, (arg1[9]), UINT32_C(0x1ffffff)); 679 uint32_t x21; 680 fiat_25519_cmovznz_u32(&x21, x20, 0x0, UINT32_C(0xffffffff)); 681 uint32_t x22; 682 fiat_25519_uint1 x23; 683 fiat_25519_addcarryx_u26(&x22, &x23, 0x0, x1, (x21 & UINT32_C(0x3ffffed))); 684 uint32_t x24; 685 fiat_25519_uint1 x25; 686 fiat_25519_addcarryx_u25(&x24, &x25, x23, x3, (x21 & UINT32_C(0x1ffffff))); 687 uint32_t x26; 688 fiat_25519_uint1 x27; 689 fiat_25519_addcarryx_u26(&x26, &x27, x25, x5, (x21 & UINT32_C(0x3ffffff))); 690 uint32_t x28; 691 fiat_25519_uint1 x29; 692 fiat_25519_addcarryx_u25(&x28, &x29, x27, x7, (x21 & UINT32_C(0x1ffffff))); 693 uint32_t x30; 694 fiat_25519_uint1 x31; 695 fiat_25519_addcarryx_u26(&x30, &x31, x29, x9, (x21 & UINT32_C(0x3ffffff))); 696 uint32_t x32; 697 fiat_25519_uint1 x33; 698 fiat_25519_addcarryx_u25(&x32, &x33, x31, x11, (x21 & UINT32_C(0x1ffffff))); 699 uint32_t x34; 700 fiat_25519_uint1 x35; 701 fiat_25519_addcarryx_u26(&x34, &x35, x33, x13, (x21 & UINT32_C(0x3ffffff))); 702 uint32_t x36; 703 fiat_25519_uint1 x37; 704 fiat_25519_addcarryx_u25(&x36, &x37, x35, x15, (x21 & UINT32_C(0x1ffffff))); 705 uint32_t x38; 706 fiat_25519_uint1 x39; 707 fiat_25519_addcarryx_u26(&x38, &x39, x37, x17, (x21 & UINT32_C(0x3ffffff))); 708 uint32_t x40; 709 fiat_25519_uint1 x41; 710 fiat_25519_addcarryx_u25(&x40, &x41, x39, x19, (x21 & UINT32_C(0x1ffffff))); 711 uint32_t x42 = (x40 << 6); 712 uint32_t x43 = (x38 << 4); 713 uint32_t x44 = (x36 << 3); 714 uint32_t x45 = (x34 * (uint32_t)0x2); 715 uint32_t x46 = (x30 << 6); 716 uint32_t x47 = (x28 << 5); 717 uint32_t x48 = (x26 << 3); 718 uint32_t x49 = (x24 << 2); 719 uint32_t x50 = (x22 >> 8); 720 uint8_t x51 = (uint8_t)(x22 & UINT8_C(0xff)); 721 uint32_t x52 = (x50 >> 8); 722 uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); 723 uint8_t x54 = (uint8_t)(x52 >> 8); 724 uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); 725 uint32_t x56 = (x54 + x49); 726 uint32_t x57 = (x56 >> 8); 727 uint8_t x58 = (uint8_t)(x56 & UINT8_C(0xff)); 728 uint32_t x59 = (x57 >> 8); 729 uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); 730 uint8_t x61 = (uint8_t)(x59 >> 8); 731 uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); 732 uint32_t x63 = (x61 + x48); 733 uint32_t x64 = (x63 >> 8); 734 uint8_t x65 = (uint8_t)(x63 & UINT8_C(0xff)); 735 uint32_t x66 = (x64 >> 8); 736 uint8_t x67 = (uint8_t)(x64 & UINT8_C(0xff)); 737 uint8_t x68 = (uint8_t)(x66 >> 8); 738 uint8_t x69 = (uint8_t)(x66 & UINT8_C(0xff)); 739 uint32_t x70 = (x68 + x47); 740 uint32_t x71 = (x70 >> 8); 741 uint8_t x72 = (uint8_t)(x70 & UINT8_C(0xff)); 742 uint32_t x73 = (x71 >> 8); 743 uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); 744 uint8_t x75 = (uint8_t)(x73 >> 8); 745 uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff)); 746 uint32_t x77 = (x75 + x46); 747 uint32_t x78 = (x77 >> 8); 748 uint8_t x79 = (uint8_t)(x77 & UINT8_C(0xff)); 749 uint32_t x80 = (x78 >> 8); 750 uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff)); 751 uint8_t x82 = (uint8_t)(x80 >> 8); 752 uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); 753 uint8_t x84 = (uint8_t)(x82 & UINT8_C(0xff)); 754 uint32_t x85 = (x32 >> 8); 755 uint8_t x86 = (uint8_t)(x32 & UINT8_C(0xff)); 756 uint32_t x87 = (x85 >> 8); 757 uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff)); 758 fiat_25519_uint1 x89 = (fiat_25519_uint1)(x87 >> 8); 759 uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); 760 uint32_t x91 = (x89 + x45); 761 uint32_t x92 = (x91 >> 8); 762 uint8_t x93 = (uint8_t)(x91 & UINT8_C(0xff)); 763 uint32_t x94 = (x92 >> 8); 764 uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); 765 uint8_t x96 = (uint8_t)(x94 >> 8); 766 uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff)); 767 uint32_t x98 = (x96 + x44); 768 uint32_t x99 = (x98 >> 8); 769 uint8_t x100 = (uint8_t)(x98 & UINT8_C(0xff)); 770 uint32_t x101 = (x99 >> 8); 771 uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff)); 772 uint8_t x103 = (uint8_t)(x101 >> 8); 773 uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); 774 uint32_t x105 = (x103 + x43); 775 uint32_t x106 = (x105 >> 8); 776 uint8_t x107 = (uint8_t)(x105 & UINT8_C(0xff)); 777 uint32_t x108 = (x106 >> 8); 778 uint8_t x109 = (uint8_t)(x106 & UINT8_C(0xff)); 779 uint8_t x110 = (uint8_t)(x108 >> 8); 780 uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); 781 uint32_t x112 = (x110 + x42); 782 uint32_t x113 = (x112 >> 8); 783 uint8_t x114 = (uint8_t)(x112 & UINT8_C(0xff)); 784 uint32_t x115 = (x113 >> 8); 785 uint8_t x116 = (uint8_t)(x113 & UINT8_C(0xff)); 786 uint8_t x117 = (uint8_t)(x115 >> 8); 787 uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff)); 788 out1[0] = x51; 789 out1[1] = x53; 790 out1[2] = x55; 791 out1[3] = x58; 792 out1[4] = x60; 793 out1[5] = x62; 794 out1[6] = x65; 795 out1[7] = x67; 796 out1[8] = x69; 797 out1[9] = x72; 798 out1[10] = x74; 799 out1[11] = x76; 800 out1[12] = x79; 801 out1[13] = x81; 802 out1[14] = x83; 803 out1[15] = x84; 804 out1[16] = x86; 805 out1[17] = x88; 806 out1[18] = x90; 807 out1[19] = x93; 808 out1[20] = x95; 809 out1[21] = x97; 810 out1[22] = x100; 811 out1[23] = x102; 812 out1[24] = x104; 813 out1[25] = x107; 814 out1[26] = x109; 815 out1[27] = x111; 816 out1[28] = x114; 817 out1[29] = x116; 818 out1[30] = x118; 819 out1[31] = x117; 820 } 821 822 /* 823 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. 824 * Postconditions: 825 * eval out1 mod m = bytes_eval arg1 mod m 826 * 827 * Input Bounds: 828 * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]] 829 * Output Bounds: 830 * out1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 831 */ 832 static void fiat_25519_from_bytes(uint32_t out1[10], const uint8_t arg1[32]) { 833 uint32_t x1 = ((uint32_t)(arg1[31]) << 18); 834 uint32_t x2 = ((uint32_t)(arg1[30]) << 10); 835 uint32_t x3 = ((uint32_t)(arg1[29]) << 2); 836 uint32_t x4 = ((uint32_t)(arg1[28]) << 20); 837 uint32_t x5 = ((uint32_t)(arg1[27]) << 12); 838 uint32_t x6 = ((uint32_t)(arg1[26]) << 4); 839 uint32_t x7 = ((uint32_t)(arg1[25]) << 21); 840 uint32_t x8 = ((uint32_t)(arg1[24]) << 13); 841 uint32_t x9 = ((uint32_t)(arg1[23]) << 5); 842 uint32_t x10 = ((uint32_t)(arg1[22]) << 23); 843 uint32_t x11 = ((uint32_t)(arg1[21]) << 15); 844 uint32_t x12 = ((uint32_t)(arg1[20]) << 7); 845 uint32_t x13 = ((uint32_t)(arg1[19]) << 24); 846 uint32_t x14 = ((uint32_t)(arg1[18]) << 16); 847 uint32_t x15 = ((uint32_t)(arg1[17]) << 8); 848 uint8_t x16 = (arg1[16]); 849 uint32_t x17 = ((uint32_t)(arg1[15]) << 18); 850 uint32_t x18 = ((uint32_t)(arg1[14]) << 10); 851 uint32_t x19 = ((uint32_t)(arg1[13]) << 2); 852 uint32_t x20 = ((uint32_t)(arg1[12]) << 19); 853 uint32_t x21 = ((uint32_t)(arg1[11]) << 11); 854 uint32_t x22 = ((uint32_t)(arg1[10]) << 3); 855 uint32_t x23 = ((uint32_t)(arg1[9]) << 21); 856 uint32_t x24 = ((uint32_t)(arg1[8]) << 13); 857 uint32_t x25 = ((uint32_t)(arg1[7]) << 5); 858 uint32_t x26 = ((uint32_t)(arg1[6]) << 22); 859 uint32_t x27 = ((uint32_t)(arg1[5]) << 14); 860 uint32_t x28 = ((uint32_t)(arg1[4]) << 6); 861 uint32_t x29 = ((uint32_t)(arg1[3]) << 24); 862 uint32_t x30 = ((uint32_t)(arg1[2]) << 16); 863 uint32_t x31 = ((uint32_t)(arg1[1]) << 8); 864 uint8_t x32 = (arg1[0]); 865 uint32_t x33 = (x32 + (x31 + (x30 + x29))); 866 uint8_t x34 = (uint8_t)(x33 >> 26); 867 uint32_t x35 = (x33 & UINT32_C(0x3ffffff)); 868 uint32_t x36 = (x3 + (x2 + x1)); 869 uint32_t x37 = (x6 + (x5 + x4)); 870 uint32_t x38 = (x9 + (x8 + x7)); 871 uint32_t x39 = (x12 + (x11 + x10)); 872 uint32_t x40 = (x16 + (x15 + (x14 + x13))); 873 uint32_t x41 = (x19 + (x18 + x17)); 874 uint32_t x42 = (x22 + (x21 + x20)); 875 uint32_t x43 = (x25 + (x24 + x23)); 876 uint32_t x44 = (x28 + (x27 + x26)); 877 uint32_t x45 = (x34 + x44); 878 uint8_t x46 = (uint8_t)(x45 >> 25); 879 uint32_t x47 = (x45 & UINT32_C(0x1ffffff)); 880 uint32_t x48 = (x46 + x43); 881 uint8_t x49 = (uint8_t)(x48 >> 26); 882 uint32_t x50 = (x48 & UINT32_C(0x3ffffff)); 883 uint32_t x51 = (x49 + x42); 884 uint8_t x52 = (uint8_t)(x51 >> 25); 885 uint32_t x53 = (x51 & UINT32_C(0x1ffffff)); 886 uint32_t x54 = (x52 + x41); 887 uint32_t x55 = (x54 & UINT32_C(0x3ffffff)); 888 uint8_t x56 = (uint8_t)(x40 >> 25); 889 uint32_t x57 = (x40 & UINT32_C(0x1ffffff)); 890 uint32_t x58 = (x56 + x39); 891 uint8_t x59 = (uint8_t)(x58 >> 26); 892 uint32_t x60 = (x58 & UINT32_C(0x3ffffff)); 893 uint32_t x61 = (x59 + x38); 894 uint8_t x62 = (uint8_t)(x61 >> 25); 895 uint32_t x63 = (x61 & UINT32_C(0x1ffffff)); 896 uint32_t x64 = (x62 + x37); 897 uint8_t x65 = (uint8_t)(x64 >> 26); 898 uint32_t x66 = (x64 & UINT32_C(0x3ffffff)); 899 uint32_t x67 = (x65 + x36); 900 out1[0] = x35; 901 out1[1] = x47; 902 out1[2] = x50; 903 out1[3] = x53; 904 out1[4] = x55; 905 out1[5] = x57; 906 out1[6] = x60; 907 out1[7] = x63; 908 out1[8] = x66; 909 out1[9] = x67; 910 } 911 912 /* 913 * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result. 914 * Postconditions: 915 * eval out1 mod m = (121666 * eval arg1) mod m 916 * 917 * Input Bounds: 918 * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] 919 * Output Bounds: 920 * out1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]] 921 */ 922 static void fiat_25519_carry_scmul_121666(uint32_t out1[10], const uint32_t arg1[10]) { 923 uint64_t x1 = ((uint64_t)UINT32_C(0x1db42) * (arg1[9])); 924 uint64_t x2 = ((uint64_t)UINT32_C(0x1db42) * (arg1[8])); 925 uint64_t x3 = ((uint64_t)UINT32_C(0x1db42) * (arg1[7])); 926 uint64_t x4 = ((uint64_t)UINT32_C(0x1db42) * (arg1[6])); 927 uint64_t x5 = ((uint64_t)UINT32_C(0x1db42) * (arg1[5])); 928 uint64_t x6 = ((uint64_t)UINT32_C(0x1db42) * (arg1[4])); 929 uint64_t x7 = ((uint64_t)UINT32_C(0x1db42) * (arg1[3])); 930 uint64_t x8 = ((uint64_t)UINT32_C(0x1db42) * (arg1[2])); 931 uint64_t x9 = ((uint64_t)UINT32_C(0x1db42) * (arg1[1])); 932 uint64_t x10 = ((uint64_t)UINT32_C(0x1db42) * (arg1[0])); 933 uint32_t x11 = (uint32_t)(x10 >> 26); 934 uint32_t x12 = (uint32_t)(x10 & UINT32_C(0x3ffffff)); 935 uint64_t x13 = (x11 + x9); 936 uint32_t x14 = (uint32_t)(x13 >> 25); 937 uint32_t x15 = (uint32_t)(x13 & UINT32_C(0x1ffffff)); 938 uint64_t x16 = (x14 + x8); 939 uint32_t x17 = (uint32_t)(x16 >> 26); 940 uint32_t x18 = (uint32_t)(x16 & UINT32_C(0x3ffffff)); 941 uint64_t x19 = (x17 + x7); 942 uint32_t x20 = (uint32_t)(x19 >> 25); 943 uint32_t x21 = (uint32_t)(x19 & UINT32_C(0x1ffffff)); 944 uint64_t x22 = (x20 + x6); 945 uint32_t x23 = (uint32_t)(x22 >> 26); 946 uint32_t x24 = (uint32_t)(x22 & UINT32_C(0x3ffffff)); 947 uint64_t x25 = (x23 + x5); 948 uint32_t x26 = (uint32_t)(x25 >> 25); 949 uint32_t x27 = (uint32_t)(x25 & UINT32_C(0x1ffffff)); 950 uint64_t x28 = (x26 + x4); 951 uint32_t x29 = (uint32_t)(x28 >> 26); 952 uint32_t x30 = (uint32_t)(x28 & UINT32_C(0x3ffffff)); 953 uint64_t x31 = (x29 + x3); 954 uint32_t x32 = (uint32_t)(x31 >> 25); 955 uint32_t x33 = (uint32_t)(x31 & UINT32_C(0x1ffffff)); 956 uint64_t x34 = (x32 + x2); 957 uint32_t x35 = (uint32_t)(x34 >> 26); 958 uint32_t x36 = (uint32_t)(x34 & UINT32_C(0x3ffffff)); 959 uint64_t x37 = (x35 + x1); 960 uint32_t x38 = (uint32_t)(x37 >> 25); 961 uint32_t x39 = (uint32_t)(x37 & UINT32_C(0x1ffffff)); 962 uint32_t x40 = (x38 * UINT8_C(0x13)); 963 uint32_t x41 = (x12 + x40); 964 fiat_25519_uint1 x42 = (fiat_25519_uint1)(x41 >> 26); 965 uint32_t x43 = (x41 & UINT32_C(0x3ffffff)); 966 uint32_t x44 = (x42 + x15); 967 fiat_25519_uint1 x45 = (fiat_25519_uint1)(x44 >> 25); 968 uint32_t x46 = (x44 & UINT32_C(0x1ffffff)); 969 uint32_t x47 = (x45 + x18); 970 out1[0] = x43; 971 out1[1] = x46; 972 out1[2] = x47; 973 out1[3] = x21; 974 out1[4] = x24; 975 out1[5] = x27; 976 out1[6] = x30; 977 out1[7] = x33; 978 out1[8] = x36; 979 out1[9] = x39; 980 } 981 982