Lines Matching refs:U
484 static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
490 if (s == (uint32_t)0U)
507 - return ((FStar_UInt128_uint128){.low = (uint64_t)0U, .high = a.low << (s - FStar_UInt128_u32_6…
509 + ret.low = (uint64_t)0U;
520 if (s == (uint32_t)0U)
537 …turn ((FStar_UInt128_uint128){.low = a.high >> (s - FStar_UInt128_u32_64), .high = (uint64_t)0U });
540 + ret.high = (uint64_t)0U;
575 - return ((FStar_UInt128_uint128){.low = a, .high = (uint64_t)0U });
578 + ret.high = (uint64_t)0U;
640 - for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
642 + for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
643 uint8_t *x0 = input + (uint32_t)4U * i;
650 - for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
652 + for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
654 uint8_t *x0 = output + (uint32_t)4U * i;
685 st[d] = Hacl_Impl_Chacha20_rotate_left(sda, (uint32_t)16U);
697 st[b] = Hacl_Impl_Chacha20_rotate_left(sda0, (uint32_t)12U);
709 st[d] = Hacl_Impl_Chacha20_rotate_left(sda1, (uint32_t)8U);
721 st[b] = Hacl_Impl_Chacha20_rotate_left(sda2, (uint32_t)7U);
728 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
730 + for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
737 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
739 + for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
745 uint32_t *ib = b + (uint32_t)16U;
746 uint32_t *ob = b + (uint32_t)32U;
749 Hacl_Lib_LoadStore32_uint32s_from_le_bytes(ib, plain, (uint32_t)16U);
750 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
751 + for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
758 uint8_t block[64U] = { 0U };
763 - for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
765 + for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
773 - for (uint32_t i = (uint32_t)0U; i < num_blocks; i = i + (uint32_t)1U) {
775 + for (i = (uint32_t)0U; i < num_blocks; i = i + (uint32_t)1U) {
776 uint8_t *b = plain + (uint32_t)64U * i;
777 uint8_t *o = output + (uint32_t)64U * i;
801 vec k0 = k[0U];
802 vec k1 = k[1U];
803 vec k2 = k[2U];
804 vec k3 = k[3U];
806 - uint8_t *b = stream_block + (uint32_t)16U;
807 - uint8_t *c = stream_block + (uint32_t)32U;
808 - uint8_t *d = stream_block + (uint32_t)48U;
810 + b = stream_block + (uint32_t)16U;
811 + c = stream_block + (uint32_t)32U;
812 + d = stream_block + (uint32_t)48U;
828 st[0U] =
834 - vec k1 = vec_load128_le(k + (uint32_t)16U);
836 + k1 = vec_load128_le(k + (uint32_t)16U);
837 st[1U] = k0;
838 st[2U] = k1;
840 - uint8_t *x00 = n1 + (uint32_t)4U;
842 - uint8_t *x0 = n1 + (uint32_t)8U;
846 + x00 = n1 + (uint32_t)4U;
848 + x0 = n1 + (uint32_t)8U;
851 st[3U] = v1;
855 vec sd0 = st[3U];
857 vec sd10 = vec_rotate_left(vec_xor(sd0, sa10), (uint32_t)16U);
873 st[0U] = sa10;
874 st[3U] = sd10;
875 - vec sa0 = st[2U];
876 - vec sb1 = st[3U];
877 - vec sd2 = st[1U];
879 - vec sd11 = vec_rotate_left(vec_xor(sd2, sa11), (uint32_t)12U);
880 + sa0 = st[2U];
881 + sb1 = st[3U];
882 + sd2 = st[1U];
884 + sd11 = vec_rotate_left(vec_xor(sd2, sa11), (uint32_t)12U);
885 st[2U] = sa11;
886 st[1U] = sd11;
887 - vec sa2 = st[0U];
888 - vec sb2 = st[1U];
889 - vec sd3 = st[3U];
891 - vec sd12 = vec_rotate_left(vec_xor(sd3, sa12), (uint32_t)8U);
892 + sa2 = st[0U];
893 + sb2 = st[1U];
894 + sd3 = st[3U];
896 + sd12 = vec_rotate_left(vec_xor(sd3, sa12), (uint32_t)8U);
897 st[0U] = sa12;
898 st[3U] = sd12;
899 - vec sa3 = st[2U];
900 - vec sb = st[3U];
901 - vec sd = st[1U];
903 - vec sd1 = vec_rotate_left(vec_xor(sd, sa1), (uint32_t)7U);
904 + sa3 = st[2U];
905 + sb = st[3U];
906 + sd = st[1U];
908 + sd1 = vec_rotate_left(vec_xor(sd, sa1), (uint32_t)7U);
909 st[2U] = sa1;
910 st[1U] = sd1;
923 - vec r1 = st[1U];
924 - vec r20 = st[2U];
925 - vec r30 = st[3U];
926 + r1 = st[1U];
927 + r20 = st[2U];
928 + r30 = st[3U];
929 st[1U] = vec_shuffle_right(r1, (uint32_t)1U);
930 st[2U] = vec_shuffle_right(r20, (uint32_t)2U);
931 st[3U] = vec_shuffle_right(r30, (uint32_t)3U);
933 - vec r10 = st[1U];
934 - vec r2 = st[2U];
935 - vec r3 = st[3U];
936 + r10 = st[1U];
937 + r2 = st[2U];
938 + r3 = st[3U];
939 st[1U] = vec_shuffle_right(r10, (uint32_t)3U);
940 st[2U] = vec_shuffle_right(r2, (uint32_t)2U);
941 st[3U] = vec_shuffle_right(r3, (uint32_t)1U);
948 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
949 + for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
959 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
960 + for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
968 - KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
969 vec k[4U];
970 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
972 + KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
973 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
980 uint8_t block[64U] = { 0U };
985 - for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
987 + for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
995 - KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
996 vec k[4U];
997 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
999 + KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1000 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
1008 - KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1009 vec k0[4U];
1010 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
1012 + vec k1[4U];
1013 + vec k2[4U];
1020 + KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1021 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
1023 KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1024 - vec k1[4U];
1025 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
1026 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
1028 KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1029 - vec k2[4U];
1030 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
1031 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
1035 - uint8_t *p1 = plain + (uint32_t)64U;
1036 - uint8_t *p2 = plain + (uint32_t)128U;
1038 - uint8_t *o1 = output + (uint32_t)64U;
1039 - uint8_t *o2 = output + (uint32_t)128U;
1041 + p1 = plain + (uint32_t)64U;
1042 + p2 = plain + (uint32_t)128U;
1044 + o1 = output + (uint32_t)64U;
1045 + o2 = output + (uint32_t)128U;
1053 - for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
1055 + for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
1063 - KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1064 vec buf[4U];
1065 - for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
1068 + KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
1069 + for (_i = 0U; _i < (uint32_t)4U; ++_i)
1093 uint64_t tmp = output[4U];
1096 uint32_t ctr = (uint32_t)5U - (uint32_t)0U - (uint32_t)1U;
1097 uint64_t z = output[ctr - (uint32_t)1U];
1101 output[0U] = tmp;
1102 - uint64_t b0 = output[0U];
1103 + b0 = output[0U];
1104 output[0U] = (uint64_t)19U * b0;
1113 uint64_t input2i = input21[0U];
1119 - uint32_t i = (uint32_t)4U;
1121 + i = (uint32_t)4U;
1129 uint64_t tmp[5U] = { 0U };
1135 + FStar_UInt128_t t[5U];
1140 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1141 KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1142 - FStar_UInt128_t t[5U];
1143 - for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
1144 + for (_i = 0U; _i < (uint32_t)5U; ++_i)
1145 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
1148 - FStar_UInt128_t b4 = t[4U];
1149 - FStar_UInt128_t b0 = t[0U];
1155 + b4 = t[4U];
1156 + b0 = t[0U];
1159 FStar_UInt128_mul_wide((uint64_t)19U,
1160 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1161 t[4U] = b4_;
1162 t[0U] = b0_;
1164 - uint64_t i0 = output[0U];
1165 - uint64_t i1 = output[1U];
1167 - uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
1168 + i0 = output[0U];
1169 + i1 = output[1U];
1171 + i1_ = i1 + (i0 >> (uint32_t)51U);
1172 output[0U] = i0_;
1173 output[1U] = i1_;
1176 uint64_t d2 = r2 * (uint64_t)2U * (uint64_t)19U;
1177 uint64_t d419 = r4 * (uint64_t)19U;
1178 uint64_t d4 = d419 * (uint64_t)2U;
1195 FStar_UInt128_mul_wide(r3 * (uint64_t)19U, r3));
1228 - FStar_UInt128_t b4 = tmp[4U];
1229 - FStar_UInt128_t b0 = tmp[0U];
1234 + b4 = tmp[4U];
1235 + b0 = tmp[0U];
1239 FStar_UInt128_mul_wide((uint64_t)19U,
1240 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1241 tmp[4U] = b4_;
1242 tmp[0U] = b0_;
1244 - uint64_t i0 = output[0U];
1245 - uint64_t i1 = output[1U];
1247 - uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
1248 + i0 = output[0U];
1249 + i1 = output[1U];
1251 + i1_ = i1 + (i0 >> (uint32_t)51U);
1252 output[0U] = i0_;
1253 output[1U] = i1_;
1261 - for (uint32_t i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U)
1262 + for (i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U)
1269 - KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1270 FStar_UInt128_t t[5U];
1271 - for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
1273 + KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1274 + for (_i = 0U; _i < (uint32_t)5U; ++_i)
1275 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
1276 memcpy(output, input, (uint32_t)5U * sizeof input[0U]);
1282 - KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1283 FStar_UInt128_t t[5U];
1284 - for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
1286 + KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1287 + for (_i = 0U; _i < (uint32_t)5U; ++_i)
1288 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
1293 uint64_t *t00 = buf + (uint32_t)5U;
1294 uint64_t *b0 = buf + (uint32_t)10U;
1302 Hacl_Bignum_Fsquare_fsquare_times(a, z, (uint32_t)1U);
1303 Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)2U);
1306 Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)1U);
1308 Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U);
1309 - uint64_t *t01 = buf + (uint32_t)5U;
1310 - uint64_t *b1 = buf + (uint32_t)10U;
1311 - uint64_t *c0 = buf + (uint32_t)15U;
1312 + t01 = buf + (uint32_t)5U;
1313 + b1 = buf + (uint32_t)10U;
1314 + c0 = buf + (uint32_t)15U;
1316 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U);
1319 Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U);
1321 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U);
1323 - uint64_t *t0 = buf + (uint32_t)5U;
1324 - uint64_t *b = buf + (uint32_t)10U;
1325 - uint64_t *c = buf + (uint32_t)15U;
1327 + t0 = buf + (uint32_t)5U;
1328 + b = buf + (uint32_t)10U;
1329 + c = buf + (uint32_t)15U;
1331 Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U);
1336 uint64_t tmp[5U] = { 0U };
1342 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]);
1343 - uint64_t b0 = tmp[0U];
1344 - uint64_t b1 = tmp[1U];
1345 - uint64_t b2 = tmp[2U];
1346 - uint64_t b3 = tmp[3U];
1347 - uint64_t b4 = tmp[4U];
1348 + b0 = tmp[0U];
1349 + b1 = tmp[1U];
1350 + b2 = tmp[2U];
1351 + b3 = tmp[3U];
1352 + b4 = tmp[4U];
1353 tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;
1354 tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U;
1355 tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U;
1360 - KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1361 FStar_UInt128_t tmp[5U];
1362 - for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
1368 + KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
1369 + for (_i = 0U; _i < (uint32_t)5U; ++_i)
1370 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
1372 uint64_t xi = b[0U];
1374 tmp[4U] = FStar_UInt128_mul_wide(xi, s);
1377 - FStar_UInt128_t b4 = tmp[4U];
1378 - FStar_UInt128_t b0 = tmp[0U];
1383 + b4 = tmp[4U];
1384 + b0 = tmp[0U];
1388 FStar_UInt128_mul_wide((uint64_t)19U,
1389 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1395 if (!(ctr == (uint32_t)0U)) {
1397 - uint32_t i = ctr - (uint32_t)1U;
1398 + i = ctr - (uint32_t)1U;
1403 uint64_t *origxprime = buf + (uint32_t)5U;
1404 uint64_t *xxprime0 = buf + (uint32_t)25U;
1405 uint64_t *zzprime0 = buf + (uint32_t)30U;
1415 + uint64_t scalar = (uint64_t)121665U;
1416 memcpy(origx, x, (uint32_t)5U * sizeof x[0U]);
1423 - uint64_t *origxprime0 = buf + (uint32_t)5U;
1424 - uint64_t *xx0 = buf + (uint32_t)15U;
1425 - uint64_t *zz0 = buf + (uint32_t)20U;
1426 - uint64_t *xxprime = buf + (uint32_t)25U;
1427 - uint64_t *zzprime = buf + (uint32_t)30U;
1428 - uint64_t *zzzprime = buf + (uint32_t)35U;
1429 + origxprime0 = buf + (uint32_t)5U;
1430 + xx0 = buf + (uint32_t)15U;
1431 + zz0 = buf + (uint32_t)20U;
1432 + xxprime = buf + (uint32_t)25U;
1433 + zzprime = buf + (uint32_t)30U;
1434 + zzzprime = buf + (uint32_t)35U;
1435 memcpy(origxprime0, xxprime, (uint32_t)5U * sizeof xxprime[0U]);
1440 Hacl_Bignum_Fsquare_fsquare_times(xx0, x, (uint32_t)1U);
1441 Hacl_Bignum_Fsquare_fsquare_times(zz0, z, (uint32_t)1U);
1442 - uint64_t *zzz = buf + (uint32_t)10U;
1443 - uint64_t *xx = buf + (uint32_t)15U;
1444 - uint64_t *zz = buf + (uint32_t)20U;
1445 + zzz = buf + (uint32_t)10U;
1446 + xx = buf + (uint32_t)15U;
1447 + zz = buf + (uint32_t)20U;
1450 - uint64_t scalar = (uint64_t)121665U;
1457 uint64_t bit = (uint64_t)(byt >> (uint32_t)7U);
1461 - uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U);
1462 + bit0 = (uint64_t)(byt >> (uint32_t)7U);
1472 - uint8_t byt1 = byt << (uint32_t)1U;
1473 + byt1 = byt << (uint32_t)1U;
1479 if (!(i == (uint32_t)0U)) {
1480 uint32_t i_ = i - (uint32_t)1U;
1483 - uint8_t byt_ = byt << (uint32_t)2U;
1484 + byt_ = byt << (uint32_t)2U;
1498 - uint64_t i0 = input[0U];
1499 - uint64_t i1 = input[1U];
1501 - uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
1502 + i0 = input[0U];
1503 + i1 = input[1U];
1505 + i1_ = i1 + (i0 >> (uint32_t)51U);
1506 input[0U] = i0_;
1507 input[1U] = i1_;
1510 uint64_t buf0[10U] = { 0U };
1512 uint64_t *z = buf0 + (uint32_t)5U;
1514 + uint8_t e[32U] = { 0U };
1521 + uint64_t buf[15U] = { 0U };
1525 z[0U] = (uint64_t)1U;
1527 - uint8_t e[32U] = { 0U };
1529 memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]);
1530 - uint8_t e0 = e[0U];
1531 - uint8_t e31 = e[31U];
1532 - uint8_t e01 = e0 & (uint8_t)248U;
1533 - uint8_t e311 = e31 & (uint8_t)127U;
1534 - uint8_t e312 = e311 | (uint8_t)64U;
1535 + e0 = e[0U];
1536 + e31 = e[31U];
1537 + e01 = e0 & (uint8_t)248U;
1538 + e311 = e31 & (uint8_t)127U;
1539 + e312 = e311 | (uint8_t)64U;
1540 e[0U] = e01;
1541 e[31U] = e312;
1543 - uint64_t buf[15U] = { 0U };
1549 x[0U] = (uint64_t)1U;
1570 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1572 + for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1580 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1582 + for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1590 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1592 + for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1595 uint64_t tctrp1 = tmp[ctr + (uint32_t)1U];
1600 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1602 + for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1605 uint32_t tctrp1 = tmp[ctr + (uint32_t)1U];
1609 uint32_t tmp = output[4U];
1610 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1612 + for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1613 uint32_t ctr = (uint32_t)5U - i - (uint32_t)1U;
1614 uint32_t z = output[ctr - (uint32_t)1U];
1620 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1623 + for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
1628 - uint32_t i = (uint32_t)4U;
1630 + i = (uint32_t)4U;
1638 uint32_t tmp[5U] = { 0U };
1639 - memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1640 uint64_t t[5U] = { 0U };
1645 + memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1650 - uint32_t i0 = output[0U];
1651 - uint32_t i1 = output[1U];
1653 - uint32_t i1_ = i1 + (i0 >> (uint32_t)26U);
1654 + i0 = output[0U];
1655 + i1 = output[1U];
1657 + i1_ = i1 + (i0 >> (uint32_t)26U);
1658 output[0U] = i0_;
1659 output[1U] = i1_;
1665 - for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1667 + for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
1672 uint32_t r2 = i2 >> (uint32_t)4U & (uint32_t)0x3ffffffU;
1673 uint32_t r3 = i3 >> (uint32_t)6U & (uint32_t)0x3ffffffU;
1674 uint32_t r4 = i4 >> (uint32_t)8U;
1677 tmp[0U] = r0;
1678 tmp[1U] = r1;
1679 tmp[2U] = r2;
1680 tmp[3U] = r3;
1681 tmp[4U] = r4;
1682 - uint32_t b4 = tmp[4U];
1684 + b4 = tmp[4U];
1686 tmp[4U] = b4_;
1690 uint32_t r2 = i2 >> (uint32_t)4U & (uint32_t)0x3ffffffU;
1691 uint32_t r3 = i3 >> (uint32_t)6U & (uint32_t)0x3ffffffU;
1692 uint32_t r4 = i4 >> (uint32_t)8U;
1697 tmp[0U] = r0;
1698 tmp[1U] = r1;
1699 tmp[2U] = r2;
1700 tmp[3U] = r3;
1701 tmp[4U] = r4;
1716 uint8_t zero1 = (uint8_t)0U;
1717 - KRML_CHECK_SIZE(zero1, (uint32_t)16U);
1718 uint8_t block[16U];
1719 - for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
1723 + KRML_CHECK_SIZE(zero1, (uint32_t)16U);
1724 + for (_i = 0U; _i < (uint32_t)16U; ++_i)
1730 memcpy(block, m, i * sizeof m[0U]);
1731 block[i0] = (uint8_t)1U;
1786 - uint32_t t0 = acc[0U];
1787 - uint32_t t10 = acc[1U];
1788 - uint32_t t20 = acc[2U];
1789 - uint32_t t30 = acc[3U];
1790 - uint32_t t40 = acc[4U];
1791 - uint32_t t1_ = t10 + (t0 >> (uint32_t)26U);
1794 - uint32_t t2_ = t20 + (t1_ >> (uint32_t)26U);
1796 - uint32_t t3_ = t30 + (t2_ >> (uint32_t)26U);
1798 - uint32_t t4_ = t40 + (t3_ >> (uint32_t)26U);
1800 + t0 = acc[0U];
1801 + t10 = acc[1U];
1802 + t20 = acc[2U];
1803 + t30 = acc[3U];
1804 + t40 = acc[4U];
1805 + t1_ = t10 + (t0 >> (uint32_t)26U);
1808 + t2_ = t20 + (t1_ >> (uint32_t)26U);
1810 + t3_ = t30 + (t2_ >> (uint32_t)26U);
1812 + t4_ = t40 + (t3_ >> (uint32_t)26U);
1814 acc[0U] = t0_;
1815 acc[1U] = t1__;
1816 acc[2U] = t2__;
1817 acc[3U] = t3__;
1818 acc[4U] = t4_;
1820 - uint32_t t00 = acc[0U];
1821 - uint32_t t1 = acc[1U];
1822 - uint32_t t2 = acc[2U];
1823 - uint32_t t3 = acc[3U];
1824 - uint32_t t4 = acc[4U];
1825 - uint32_t t1_0 = t1 + (t00 >> (uint32_t)26U);
1827 - uint32_t t2_0 = t2 + (t1_0 >> (uint32_t)26U);
1829 - uint32_t t3_0 = t3 + (t2_0 >> (uint32_t)26U);
1831 - uint32_t t4_0 = t4 + (t3_0 >> (uint32_t)26U);
1833 + t00 = acc[0U];
1834 + t1 = acc[1U];
1835 + t2 = acc[2U];
1836 + t3 = acc[3U];
1837 + t4 = acc[4U];
1838 + t1_0 = t1 + (t00 >> (uint32_t)26U);
1840 + t2_0 = t2 + (t1_0 >> (uint32_t)26U);
1842 + t3_0 = t3 + (t2_0 >> (uint32_t)26U);
1844 + t4_0 = t4 + (t3_0 >> (uint32_t)26U);
1846 acc[0U] = t0_0;
1847 acc[1U] = t1__0;
1848 acc[2U] = t2__0;
1849 acc[3U] = t3__0;
1850 acc[4U] = t4_0;
1852 - uint32_t i0 = acc[0U];
1853 - uint32_t i1 = acc[1U];
1855 - uint32_t i1_ = i1 + (i0 >> (uint32_t)26U);
1856 + i0 = acc[0U];
1857 + i1 = acc[1U];
1859 + i1_ = i1 + (i0 >> (uint32_t)26U);
1860 acc[0U] = i0_;
1861 acc[1U] = i1_;
1862 - uint32_t a0 = acc[0U];
1863 - uint32_t a1 = acc[1U];
1864 - uint32_t a2 = acc[2U];
1865 - uint32_t a3 = acc[3U];
1866 - uint32_t a4 = acc[4U];
1878 + a0 = acc[0U];
1879 + a1 = acc[1U];
1880 + a2 = acc[2U];
1881 + a3 = acc[3U];
1882 + a4 = acc[4U];
1894 acc[0U] = a0_;
1895 acc[1U] = a1_;
1896 acc[2U] = a2_;
1910 if (!(len1 == (uint64_t)0U)) {
1912 uint8_t *tail1 = m + (uint32_t)16U;
1915 - uint64_t len2 = len1 - (uint64_t)1U;
1916 + len2 = len1 - (uint64_t)1U;
1923 …UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)104U)) & (uint32_t)0x3fff…
1927 x0[0U] = r0;
1928 x0[1U] = r1;
1929 x0[2U] = r2;
1930 x0[3U] = r3;
1931 x0[4U] = r4;
1938 x00[0U] = (uint32_t)0U;
1939 x00[1U] = (uint32_t)0U;
1940 x00[2U] = (uint32_t)0U;
1944 uint8_t *last_block = m + (uint32_t)((uint64_t)16U * len16);
1949 if (!(rem16 == (uint64_t)0U))
1961 uint32_t buf[10U] = { 0U };
1963 uint32_t *h = buf + (uint32_t)5U;
1977 - uint8_t *key_s = k1 + (uint32_t)16U;
1978 + key_s = k1 + (uint32_t)16U;
1984 - uint32_t h0 = acc[0U];
1985 - uint32_t h1 = acc[1U];
1986 - uint32_t h2 = acc[2U];
1987 - uint32_t h3 = acc[3U];
1988 - uint32_t h4 = acc[4U];
1995 + h0 = acc[0U];
1996 + h1 = acc[1U];
1997 + h2 = acc[2U];
1998 + h3 = acc[3U];
1999 + h4 = acc[4U];
2002 (uint32_t)104U),
2006 … (uint32_t)26U),
2016 …UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)104U)) & (uint32_t)0x3fff…
2020 x0[0U] = r0;
2021 x0[1U] = r1;
2022 x0[2U] = r2;
2023 x0[3U] = r3;
2024 x0[4U] = r4;
2031 x00[0U] = (uint32_t)0U;
2032 x00[1U] = (uint32_t)0U;
2033 x00[2U] = (uint32_t)0U;
2041 if (!((uint64_t)len1 == (uint64_t)0U))