Hacl_Bignum25519_51.h (33862B)
1 /* MIT License 2 * 3 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation 4 * Copyright (c) 2022-2023 HACL* Contributors 5 * 6 * Permission is hereby granted, free of charge, to any person obtaining a copy 7 * of this software and associated documentation files (the "Software"), to deal 8 * in the Software without restriction, including without limitation the rights 9 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 10 * copies of the Software, and to permit persons to whom the Software is 11 * furnished to do so, subject to the following conditions: 12 * 13 * The above copyright notice and this permission notice shall be included in all 14 * copies or substantial portions of the Software. 15 * 16 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 21 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE 22 * SOFTWARE. 23 */ 24 25 #ifndef __internal_Hacl_Bignum25519_51_H 26 #define __internal_Hacl_Bignum25519_51_H 27 28 #if defined(__cplusplus) 29 extern "C" { 30 #endif 31 32 #include <string.h> 33 #include "krml/internal/types.h" 34 #include "krml/lowstar_endianness.h" 35 #include "krml/internal/target.h" 36 37 #include "internal/Hacl_Krmllib.h" 38 #include "Hacl_Krmllib.h" 39 40 static inline void 41 Hacl_Impl_Curve25519_Field51_fadd(uint64_t *out, uint64_t *f1, uint64_t *f2) 42 { 43 uint64_t f10 = f1[0U]; 44 uint64_t f20 = f2[0U]; 45 uint64_t f11 = f1[1U]; 46 uint64_t f21 = f2[1U]; 47 uint64_t f12 = f1[2U]; 48 uint64_t f22 = f2[2U]; 49 uint64_t f13 = f1[3U]; 50 uint64_t f23 = f2[3U]; 51 uint64_t f14 = f1[4U]; 52 uint64_t f24 = f2[4U]; 53 out[0U] = f10 + f20; 54 out[1U] = f11 + f21; 55 out[2U] = f12 + f22; 56 out[3U] = f13 + f23; 57 out[4U] = f14 + f24; 58 } 59 60 static inline void 61 Hacl_Impl_Curve25519_Field51_fsub(uint64_t *out, uint64_t *f1, uint64_t *f2) 62 { 63 uint64_t f10 = f1[0U]; 64 uint64_t f20 = f2[0U]; 65 uint64_t f11 = f1[1U]; 66 uint64_t f21 = f2[1U]; 67 uint64_t f12 = f1[2U]; 68 uint64_t f22 = f2[2U]; 69 uint64_t f13 = f1[3U]; 70 uint64_t f23 = f2[3U]; 71 uint64_t f14 = f1[4U]; 72 uint64_t f24 = f2[4U]; 73 out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20; 74 out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21; 75 out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22; 76 out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23; 77 out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24; 78 } 79 80 static inline void 81 Hacl_Impl_Curve25519_Field51_fmul( 82 uint64_t *out, 83 uint64_t *f1, 84 uint64_t *f2, 85 FStar_UInt128_uint128 *uu___) 86 { 87 KRML_HOST_IGNORE(uu___); 88 uint64_t f10 = f1[0U]; 89 uint64_t f11 = f1[1U]; 90 uint64_t f12 = f1[2U]; 91 uint64_t f13 = f1[3U]; 92 uint64_t f14 = f1[4U]; 93 uint64_t f20 = f2[0U]; 94 uint64_t f21 = f2[1U]; 95 uint64_t f22 = f2[2U]; 96 uint64_t f23 = f2[3U]; 97 uint64_t f24 = f2[4U]; 98 uint64_t tmp1 = f21 * (uint64_t)19U; 99 uint64_t tmp2 = f22 * (uint64_t)19U; 100 uint64_t tmp3 = f23 * (uint64_t)19U; 101 uint64_t tmp4 = f24 * (uint64_t)19U; 102 FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20); 103 FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21); 104 FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22); 105 FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23); 106 FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24); 107 FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4)); 108 FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20)); 109 FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21)); 110 FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22)); 111 FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23)); 112 FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3)); 113 FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4)); 114 FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20)); 115 FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21)); 116 FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22)); 117 FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2)); 118 FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3)); 119 FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4)); 120 FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20)); 121 FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21)); 122 FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1)); 123 FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2)); 124 FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3)); 125 FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4)); 126 FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20)); 127 FStar_UInt128_uint128 tmp_w0 = o04; 128 FStar_UInt128_uint128 tmp_w1 = o14; 129 FStar_UInt128_uint128 tmp_w2 = o24; 130 FStar_UInt128_uint128 tmp_w3 = o34; 131 FStar_UInt128_uint128 tmp_w4 = o44; 132 FStar_UInt128_uint128 133 l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 134 uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU; 135 uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U)); 136 FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0)); 137 uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU; 138 uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U)); 139 FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1)); 140 uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU; 141 uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U)); 142 FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2)); 143 uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU; 144 uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U)); 145 FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3)); 146 uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU; 147 uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U)); 148 uint64_t l_4 = tmp01 + c4 * (uint64_t)19U; 149 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 150 uint64_t c5 = l_4 >> (uint32_t)51U; 151 uint64_t o0 = tmp0_; 152 uint64_t o1 = tmp11 + c5; 153 uint64_t o2 = tmp21; 154 uint64_t o3 = tmp31; 155 uint64_t o4 = tmp41; 156 out[0U] = o0; 157 out[1U] = o1; 158 out[2U] = o2; 159 out[3U] = o3; 160 out[4U] = o4; 161 } 162 163 static inline void 164 Hacl_Impl_Curve25519_Field51_fmul2( 165 uint64_t *out, 166 uint64_t *f1, 167 uint64_t *f2, 168 FStar_UInt128_uint128 *uu___) 169 { 170 KRML_HOST_IGNORE(uu___); 171 uint64_t f10 = f1[0U]; 172 uint64_t f11 = f1[1U]; 173 uint64_t f12 = f1[2U]; 174 uint64_t f13 = f1[3U]; 175 uint64_t f14 = f1[4U]; 176 uint64_t f20 = f2[0U]; 177 uint64_t f21 = f2[1U]; 178 uint64_t f22 = f2[2U]; 179 uint64_t f23 = f2[3U]; 180 uint64_t f24 = f2[4U]; 181 uint64_t f30 = f1[5U]; 182 uint64_t f31 = f1[6U]; 183 uint64_t f32 = f1[7U]; 184 uint64_t f33 = f1[8U]; 185 uint64_t f34 = f1[9U]; 186 uint64_t f40 = f2[5U]; 187 uint64_t f41 = f2[6U]; 188 uint64_t f42 = f2[7U]; 189 uint64_t f43 = f2[8U]; 190 uint64_t f44 = f2[9U]; 191 uint64_t tmp11 = f21 * (uint64_t)19U; 192 uint64_t tmp12 = f22 * (uint64_t)19U; 193 uint64_t tmp13 = f23 * (uint64_t)19U; 194 uint64_t tmp14 = f24 * (uint64_t)19U; 195 uint64_t tmp21 = f41 * (uint64_t)19U; 196 uint64_t tmp22 = f42 * (uint64_t)19U; 197 uint64_t tmp23 = f43 * (uint64_t)19U; 198 uint64_t tmp24 = f44 * (uint64_t)19U; 199 FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20); 200 FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21); 201 FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22); 202 FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23); 203 FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24); 204 FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14)); 205 FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20)); 206 FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21)); 207 FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22)); 208 FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23)); 209 FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13)); 210 FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14)); 211 FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20)); 212 FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21)); 213 FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22)); 214 FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12)); 215 FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13)); 216 FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14)); 217 FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20)); 218 FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21)); 219 FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11)); 220 FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12)); 221 FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13)); 222 FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14)); 223 FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20)); 224 FStar_UInt128_uint128 tmp_w10 = o040; 225 FStar_UInt128_uint128 tmp_w11 = o140; 226 FStar_UInt128_uint128 tmp_w12 = o240; 227 FStar_UInt128_uint128 tmp_w13 = o340; 228 FStar_UInt128_uint128 tmp_w14 = o440; 229 FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40); 230 FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41); 231 FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42); 232 FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43); 233 FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44); 234 FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24)); 235 FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40)); 236 FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41)); 237 FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42)); 238 FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43)); 239 FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23)); 240 FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24)); 241 FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40)); 242 FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41)); 243 FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42)); 244 FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22)); 245 FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23)); 246 FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24)); 247 FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40)); 248 FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41)); 249 FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21)); 250 FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22)); 251 FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23)); 252 FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24)); 253 FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40)); 254 FStar_UInt128_uint128 tmp_w20 = o04; 255 FStar_UInt128_uint128 tmp_w21 = o141; 256 FStar_UInt128_uint128 tmp_w22 = o241; 257 FStar_UInt128_uint128 tmp_w23 = o34; 258 FStar_UInt128_uint128 tmp_w24 = o44; 259 FStar_UInt128_uint128 260 l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 261 uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU; 262 uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U)); 263 FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00)); 264 uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU; 265 uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U)); 266 FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10)); 267 uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU; 268 uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U)); 269 FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20)); 270 uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU; 271 uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U)); 272 FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30)); 273 uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU; 274 uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U)); 275 uint64_t l_4 = tmp00 + c40 * (uint64_t)19U; 276 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 277 uint64_t c50 = l_4 >> (uint32_t)51U; 278 uint64_t o100 = tmp0_; 279 uint64_t o112 = tmp10 + c50; 280 uint64_t o122 = tmp20; 281 uint64_t o132 = tmp30; 282 uint64_t o142 = tmp40; 283 FStar_UInt128_uint128 284 l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 285 uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU; 286 uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U)); 287 FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0)); 288 uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU; 289 uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U)); 290 FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1)); 291 uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU; 292 uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U)); 293 FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2)); 294 uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU; 295 uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U)); 296 FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3)); 297 uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU; 298 uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U)); 299 uint64_t l_10 = tmp0 + c4 * (uint64_t)19U; 300 uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU; 301 uint64_t c5 = l_10 >> (uint32_t)51U; 302 uint64_t o200 = tmp0_0; 303 uint64_t o212 = tmp1 + c5; 304 uint64_t o222 = tmp2; 305 uint64_t o232 = tmp3; 306 uint64_t o242 = tmp4; 307 uint64_t o10 = o100; 308 uint64_t o11 = o112; 309 uint64_t o12 = o122; 310 uint64_t o13 = o132; 311 uint64_t o14 = o142; 312 uint64_t o20 = o200; 313 uint64_t o21 = o212; 314 uint64_t o22 = o222; 315 uint64_t o23 = o232; 316 uint64_t o24 = o242; 317 out[0U] = o10; 318 out[1U] = o11; 319 out[2U] = o12; 320 out[3U] = o13; 321 out[4U] = o14; 322 out[5U] = o20; 323 out[6U] = o21; 324 out[7U] = o22; 325 out[8U] = o23; 326 out[9U] = o24; 327 } 328 329 static inline void 330 Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2) 331 { 332 uint64_t f10 = f1[0U]; 333 uint64_t f11 = f1[1U]; 334 uint64_t f12 = f1[2U]; 335 uint64_t f13 = f1[3U]; 336 uint64_t f14 = f1[4U]; 337 FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10); 338 FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11); 339 FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12); 340 FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13); 341 FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14); 342 FStar_UInt128_uint128 343 l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 344 uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU; 345 uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U)); 346 FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0)); 347 uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU; 348 uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U)); 349 FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1)); 350 uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU; 351 uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U)); 352 FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2)); 353 uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU; 354 uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U)); 355 FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3)); 356 uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU; 357 uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U)); 358 uint64_t l_4 = tmp0 + c4 * (uint64_t)19U; 359 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 360 uint64_t c5 = l_4 >> (uint32_t)51U; 361 uint64_t o0 = tmp0_; 362 uint64_t o1 = tmp1 + c5; 363 uint64_t o2 = tmp2; 364 uint64_t o3 = tmp3; 365 uint64_t o4 = tmp4; 366 out[0U] = o0; 367 out[1U] = o1; 368 out[2U] = o2; 369 out[3U] = o3; 370 out[4U] = o4; 371 } 372 373 static inline void 374 Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) 375 { 376 KRML_HOST_IGNORE(uu___); 377 uint64_t f0 = f[0U]; 378 uint64_t f1 = f[1U]; 379 uint64_t f2 = f[2U]; 380 uint64_t f3 = f[3U]; 381 uint64_t f4 = f[4U]; 382 uint64_t d0 = (uint64_t)2U * f0; 383 uint64_t d1 = (uint64_t)2U * f1; 384 uint64_t d2 = (uint64_t)38U * f2; 385 uint64_t d3 = (uint64_t)19U * f3; 386 uint64_t d419 = (uint64_t)19U * f4; 387 uint64_t d4 = (uint64_t)2U * d419; 388 FStar_UInt128_uint128 389 s0 = 390 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0), 391 FStar_UInt128_mul_wide(d4, f1)), 392 FStar_UInt128_mul_wide(d2, f3)); 393 FStar_UInt128_uint128 394 s1 = 395 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1), 396 FStar_UInt128_mul_wide(d4, f2)), 397 FStar_UInt128_mul_wide(d3, f3)); 398 FStar_UInt128_uint128 399 s2 = 400 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2), 401 FStar_UInt128_mul_wide(f1, f1)), 402 FStar_UInt128_mul_wide(d4, f3)); 403 FStar_UInt128_uint128 404 s3 = 405 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3), 406 FStar_UInt128_mul_wide(d1, f2)), 407 FStar_UInt128_mul_wide(f4, d419)); 408 FStar_UInt128_uint128 409 s4 = 410 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4), 411 FStar_UInt128_mul_wide(d1, f3)), 412 FStar_UInt128_mul_wide(f2, f2)); 413 FStar_UInt128_uint128 o00 = s0; 414 FStar_UInt128_uint128 o10 = s1; 415 FStar_UInt128_uint128 o20 = s2; 416 FStar_UInt128_uint128 o30 = s3; 417 FStar_UInt128_uint128 o40 = s4; 418 FStar_UInt128_uint128 419 l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 420 uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU; 421 uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U)); 422 FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0)); 423 uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU; 424 uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U)); 425 FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1)); 426 uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU; 427 uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U)); 428 FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2)); 429 uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU; 430 uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U)); 431 FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3)); 432 uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU; 433 uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U)); 434 uint64_t l_4 = tmp0 + c4 * (uint64_t)19U; 435 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 436 uint64_t c5 = l_4 >> (uint32_t)51U; 437 uint64_t o0 = tmp0_; 438 uint64_t o1 = tmp1 + c5; 439 uint64_t o2 = tmp2; 440 uint64_t o3 = tmp3; 441 uint64_t o4 = tmp4; 442 out[0U] = o0; 443 out[1U] = o1; 444 out[2U] = o2; 445 out[3U] = o3; 446 out[4U] = o4; 447 } 448 449 static inline void 450 Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) 451 { 452 KRML_HOST_IGNORE(uu___); 453 uint64_t f10 = f[0U]; 454 uint64_t f11 = f[1U]; 455 uint64_t f12 = f[2U]; 456 uint64_t f13 = f[3U]; 457 uint64_t f14 = f[4U]; 458 uint64_t f20 = f[5U]; 459 uint64_t f21 = f[6U]; 460 uint64_t f22 = f[7U]; 461 uint64_t f23 = f[8U]; 462 uint64_t f24 = f[9U]; 463 uint64_t d00 = (uint64_t)2U * f10; 464 uint64_t d10 = (uint64_t)2U * f11; 465 uint64_t d20 = (uint64_t)38U * f12; 466 uint64_t d30 = (uint64_t)19U * f13; 467 uint64_t d4190 = (uint64_t)19U * f14; 468 uint64_t d40 = (uint64_t)2U * d4190; 469 FStar_UInt128_uint128 470 s00 = 471 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10), 472 FStar_UInt128_mul_wide(d40, f11)), 473 FStar_UInt128_mul_wide(d20, f13)); 474 FStar_UInt128_uint128 475 s10 = 476 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11), 477 FStar_UInt128_mul_wide(d40, f12)), 478 FStar_UInt128_mul_wide(d30, f13)); 479 FStar_UInt128_uint128 480 s20 = 481 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12), 482 FStar_UInt128_mul_wide(f11, f11)), 483 FStar_UInt128_mul_wide(d40, f13)); 484 FStar_UInt128_uint128 485 s30 = 486 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13), 487 FStar_UInt128_mul_wide(d10, f12)), 488 FStar_UInt128_mul_wide(f14, d4190)); 489 FStar_UInt128_uint128 490 s40 = 491 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14), 492 FStar_UInt128_mul_wide(d10, f13)), 493 FStar_UInt128_mul_wide(f12, f12)); 494 FStar_UInt128_uint128 o100 = s00; 495 FStar_UInt128_uint128 o110 = s10; 496 FStar_UInt128_uint128 o120 = s20; 497 FStar_UInt128_uint128 o130 = s30; 498 FStar_UInt128_uint128 o140 = s40; 499 uint64_t d0 = (uint64_t)2U * f20; 500 uint64_t d1 = (uint64_t)2U * f21; 501 uint64_t d2 = (uint64_t)38U * f22; 502 uint64_t d3 = (uint64_t)19U * f23; 503 uint64_t d419 = (uint64_t)19U * f24; 504 uint64_t d4 = (uint64_t)2U * d419; 505 FStar_UInt128_uint128 506 s0 = 507 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20), 508 FStar_UInt128_mul_wide(d4, f21)), 509 FStar_UInt128_mul_wide(d2, f23)); 510 FStar_UInt128_uint128 511 s1 = 512 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21), 513 FStar_UInt128_mul_wide(d4, f22)), 514 FStar_UInt128_mul_wide(d3, f23)); 515 FStar_UInt128_uint128 516 s2 = 517 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22), 518 FStar_UInt128_mul_wide(f21, f21)), 519 FStar_UInt128_mul_wide(d4, f23)); 520 FStar_UInt128_uint128 521 s3 = 522 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23), 523 FStar_UInt128_mul_wide(d1, f22)), 524 FStar_UInt128_mul_wide(f24, d419)); 525 FStar_UInt128_uint128 526 s4 = 527 FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24), 528 FStar_UInt128_mul_wide(d1, f23)), 529 FStar_UInt128_mul_wide(f22, f22)); 530 FStar_UInt128_uint128 o200 = s0; 531 FStar_UInt128_uint128 o210 = s1; 532 FStar_UInt128_uint128 o220 = s2; 533 FStar_UInt128_uint128 o230 = s3; 534 FStar_UInt128_uint128 o240 = s4; 535 FStar_UInt128_uint128 536 l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 537 uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU; 538 uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U)); 539 FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00)); 540 uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU; 541 uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U)); 542 FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10)); 543 uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU; 544 uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U)); 545 FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20)); 546 uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU; 547 uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U)); 548 FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30)); 549 uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU; 550 uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U)); 551 uint64_t l_4 = tmp00 + c40 * (uint64_t)19U; 552 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 553 uint64_t c50 = l_4 >> (uint32_t)51U; 554 uint64_t o101 = tmp0_; 555 uint64_t o111 = tmp10 + c50; 556 uint64_t o121 = tmp20; 557 uint64_t o131 = tmp30; 558 uint64_t o141 = tmp40; 559 FStar_UInt128_uint128 560 l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U)); 561 uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU; 562 uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U)); 563 FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0)); 564 uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU; 565 uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U)); 566 FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1)); 567 uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU; 568 uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U)); 569 FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2)); 570 uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU; 571 uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U)); 572 FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3)); 573 uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU; 574 uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U)); 575 uint64_t l_10 = tmp0 + c4 * (uint64_t)19U; 576 uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU; 577 uint64_t c5 = l_10 >> (uint32_t)51U; 578 uint64_t o201 = tmp0_0; 579 uint64_t o211 = tmp1 + c5; 580 uint64_t o221 = tmp2; 581 uint64_t o231 = tmp3; 582 uint64_t o241 = tmp4; 583 uint64_t o10 = o101; 584 uint64_t o11 = o111; 585 uint64_t o12 = o121; 586 uint64_t o13 = o131; 587 uint64_t o14 = o141; 588 uint64_t o20 = o201; 589 uint64_t o21 = o211; 590 uint64_t o22 = o221; 591 uint64_t o23 = o231; 592 uint64_t o24 = o241; 593 out[0U] = o10; 594 out[1U] = o11; 595 out[2U] = o12; 596 out[3U] = o13; 597 out[4U] = o14; 598 out[5U] = o20; 599 out[6U] = o21; 600 out[7U] = o22; 601 out[8U] = o23; 602 out[9U] = o24; 603 } 604 605 static inline void 606 Hacl_Impl_Curve25519_Field51_store_felem(uint64_t *u64s, uint64_t *f) 607 { 608 uint64_t f0 = f[0U]; 609 uint64_t f1 = f[1U]; 610 uint64_t f2 = f[2U]; 611 uint64_t f3 = f[3U]; 612 uint64_t f4 = f[4U]; 613 uint64_t l_ = f0 + (uint64_t)0U; 614 uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU; 615 uint64_t c0 = l_ >> (uint32_t)51U; 616 uint64_t l_0 = f1 + c0; 617 uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU; 618 uint64_t c1 = l_0 >> (uint32_t)51U; 619 uint64_t l_1 = f2 + c1; 620 uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU; 621 uint64_t c2 = l_1 >> (uint32_t)51U; 622 uint64_t l_2 = f3 + c2; 623 uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU; 624 uint64_t c3 = l_2 >> (uint32_t)51U; 625 uint64_t l_3 = f4 + c3; 626 uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU; 627 uint64_t c4 = l_3 >> (uint32_t)51U; 628 uint64_t l_4 = tmp0 + c4 * (uint64_t)19U; 629 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 630 uint64_t c5 = l_4 >> (uint32_t)51U; 631 uint64_t f01 = tmp0_; 632 uint64_t f11 = tmp1 + c5; 633 uint64_t f21 = tmp2; 634 uint64_t f31 = tmp3; 635 uint64_t f41 = tmp4; 636 uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU); 637 uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU); 638 uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU); 639 uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU); 640 uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU); 641 uint64_t mask = (((m0 & m1) & m2) & m3) & m4; 642 uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU); 643 uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU); 644 uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU); 645 uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU); 646 uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU); 647 uint64_t f02 = f0_; 648 uint64_t f12 = f1_; 649 uint64_t f22 = f2_; 650 uint64_t f32 = f3_; 651 uint64_t f42 = f4_; 652 uint64_t o00 = f02 | f12 << (uint32_t)51U; 653 uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U; 654 uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U; 655 uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U; 656 uint64_t o0 = o00; 657 uint64_t o1 = o10; 658 uint64_t o2 = o20; 659 uint64_t o3 = o30; 660 u64s[0U] = o0; 661 u64s[1U] = o1; 662 u64s[2U] = o2; 663 u64s[3U] = o3; 664 } 665 666 static inline void 667 Hacl_Impl_Curve25519_Field51_cswap2(uint64_t bit, uint64_t *p1, uint64_t *p2) 668 { 669 uint64_t mask = (uint64_t)0U - bit; 670 KRML_MAYBE_FOR10(i, 671 (uint32_t)0U, 672 (uint32_t)10U, 673 (uint32_t)1U, 674 uint64_t dummy = mask & (p1[i] ^ p2[i]); 675 p1[i] = p1[i] ^ dummy; 676 p2[i] = p2[i] ^ dummy;); 677 } 678 679 #if defined(__cplusplus) 680 } 681 #endif 682 683 #define __internal_Hacl_Bignum25519_51_H_DEFINED 684 #endif