summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBenjamin Beurdouche <bbeurdouche@mozilla.com>2021-03-08 09:59:34 +0000
committerBenjamin Beurdouche <bbeurdouche@mozilla.com>2021-03-08 09:59:34 +0000
commit2f0723e30119e615139e3c382a5bea0fd3835fa2 (patch)
treecf902c385f6788c756e3d1e803bf5ff2927f85e2
parent77d52d51f7721a6d9e6e4f57eb57ecd73f684825 (diff)
downloadnss-hg-2f0723e30119e615139e3c382a5bea0fd3835fa2.tar.gz
Bug 1696800 - HACL* update March 2021 - c95ab70fcb2bc21025d8845281bc4bc8987ca683 r=beurdouche
Differential Revision: https://phabricator.services.mozilla.com/D107387
-rwxr-xr-xautomation/taskcluster/scripts/run_hacl.sh2
-rw-r--r--lib/freebl/verified/Hacl_Bignum25519_51.h676
-rw-r--r--lib/freebl/verified/Hacl_Chacha20.c6
-rw-r--r--lib/freebl/verified/Hacl_Chacha20.h14
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_128.c12
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_128.h14
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_256.c12
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_256.h14
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_32.c8
-rw-r--r--lib/freebl/verified/Hacl_Chacha20Poly1305_32.h14
-rw-r--r--lib/freebl/verified/Hacl_Chacha20_Vec128.c26
-rw-r--r--lib/freebl/verified/Hacl_Chacha20_Vec128.h14
-rw-r--r--lib/freebl/verified/Hacl_Chacha20_Vec256.c26
-rw-r--r--lib/freebl/verified/Hacl_Chacha20_Vec256.h14
-rw-r--r--lib/freebl/verified/Hacl_Curve25519_51.c746
-rw-r--r--lib/freebl/verified/Hacl_Curve25519_51.h15
-rw-r--r--lib/freebl/verified/Hacl_Kremlib.h16
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_128.c10
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_128.h14
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_256.c10
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_256.h14
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_32.c2
-rw-r--r--lib/freebl/verified/Hacl_Poly1305_32.h14
-rw-r--r--lib/freebl/verified/kremlin/include/kremlin/internal/target.h2
-rw-r--r--lib/freebl/verified/kremlin/include/kremlin/internal/types.h22
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128.h5
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128_Verified.h5
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h37
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/LowStar_Endianness.h7
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_gcc64.h5
-rw-r--r--lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_msvc.h9
-rw-r--r--lib/freebl/verified/libintvector.h201
32 files changed, 1172 insertions, 814 deletions
diff --git a/automation/taskcluster/scripts/run_hacl.sh b/automation/taskcluster/scripts/run_hacl.sh
index 84dc9dbc3..7b82c911b 100755
--- a/automation/taskcluster/scripts/run_hacl.sh
+++ b/automation/taskcluster/scripts/run_hacl.sh
@@ -13,7 +13,7 @@ set -e -x -v
# HACL CI.
# When bug 1593647 is resolved, extract the code on CI again.
git clone -q "https://github.com/project-everest/hacl-star" ~/hacl-star
-git -C ~/hacl-star checkout -q e4311991b1526734f99f4e3a0058895a46c63e5c
+git -C ~/hacl-star checkout -q c95ab70fcb2bc21025d8845281bc4bc8987ca683
# Format the C snapshot.
cd ~/hacl-star/dist/mozilla
diff --git a/lib/freebl/verified/Hacl_Bignum25519_51.h b/lib/freebl/verified/Hacl_Bignum25519_51.h
new file mode 100644
index 000000000..173f11188
--- /dev/null
+++ b/lib/freebl/verified/Hacl_Bignum25519_51.h
@@ -0,0 +1,676 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __Hacl_Bignum25519_51_H
+#define __Hacl_Bignum25519_51_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include "kremlin/internal/types.h"
+#include "kremlin/lowstar_endianness.h"
+#include <string.h>
+#include <stdbool.h>
+
+#include "Hacl_Kremlib.h"
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fadd(uint64_t *out, uint64_t *f1, uint64_t *f2)
+{
+ uint64_t f10 = f1[0U];
+ uint64_t f20 = f2[0U];
+ uint64_t f11 = f1[1U];
+ uint64_t f21 = f2[1U];
+ uint64_t f12 = f1[2U];
+ uint64_t f22 = f2[2U];
+ uint64_t f13 = f1[3U];
+ uint64_t f23 = f2[3U];
+ uint64_t f14 = f1[4U];
+ uint64_t f24 = f2[4U];
+ out[0U] = f10 + f20;
+ out[1U] = f11 + f21;
+ out[2U] = f12 + f22;
+ out[3U] = f13 + f23;
+ out[4U] = f14 + f24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsub(uint64_t *out, uint64_t *f1, uint64_t *f2)
+{
+ uint64_t f10 = f1[0U];
+ uint64_t f20 = f2[0U];
+ uint64_t f11 = f1[1U];
+ uint64_t f21 = f2[1U];
+ uint64_t f12 = f1[2U];
+ uint64_t f22 = f2[2U];
+ uint64_t f13 = f1[3U];
+ uint64_t f23 = f2[3U];
+ uint64_t f14 = f1[4U];
+ uint64_t f24 = f2[4U];
+ out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20;
+ out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21;
+ out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22;
+ out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23;
+ out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul(
+ uint64_t *out,
+ uint64_t *f1,
+ uint64_t *f2,
+ FStar_UInt128_uint128 *uu___)
+{
+ uint64_t f10 = f1[0U];
+ uint64_t f11 = f1[1U];
+ uint64_t f12 = f1[2U];
+ uint64_t f13 = f1[3U];
+ uint64_t f14 = f1[4U];
+ uint64_t f20 = f2[0U];
+ uint64_t f21 = f2[1U];
+ uint64_t f22 = f2[2U];
+ uint64_t f23 = f2[3U];
+ uint64_t f24 = f2[4U];
+ uint64_t tmp1 = f21 * (uint64_t)19U;
+ uint64_t tmp2 = f22 * (uint64_t)19U;
+ uint64_t tmp3 = f23 * (uint64_t)19U;
+ uint64_t tmp4 = f24 * (uint64_t)19U;
+ FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
+ FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21);
+ FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22);
+ FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
+ FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
+ FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4));
+ FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20));
+ FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21));
+ FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
+ FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
+ FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3));
+ FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4));
+ FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20));
+ FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21));
+ FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22));
+ FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2));
+ FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3));
+ FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4));
+ FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20));
+ FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21));
+ FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1));
+ FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2));
+ FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3));
+ FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4));
+ FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20));
+ FStar_UInt128_uint128 tmp_w0 = o04;
+ FStar_UInt128_uint128 tmp_w1 = o14;
+ FStar_UInt128_uint128 tmp_w2 = o24;
+ FStar_UInt128_uint128 tmp_w3 = o34;
+ FStar_UInt128_uint128 tmp_w4 = o44;
+ FStar_UInt128_uint128
+ l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+ FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
+ uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+ FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
+ uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+ FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
+ uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+ FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
+ uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+ uint64_t l_4 = tmp01 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ uint64_t o0 = tmp0_;
+ uint64_t o1 = tmp11 + c5;
+ uint64_t o2 = tmp21;
+ uint64_t o3 = tmp31;
+ uint64_t o4 = tmp41;
+ out[0U] = o0;
+ out[1U] = o1;
+ out[2U] = o2;
+ out[3U] = o3;
+ out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul2(
+ uint64_t *out,
+ uint64_t *f1,
+ uint64_t *f2,
+ FStar_UInt128_uint128 *uu___)
+{
+ uint64_t f10 = f1[0U];
+ uint64_t f11 = f1[1U];
+ uint64_t f12 = f1[2U];
+ uint64_t f13 = f1[3U];
+ uint64_t f14 = f1[4U];
+ uint64_t f20 = f2[0U];
+ uint64_t f21 = f2[1U];
+ uint64_t f22 = f2[2U];
+ uint64_t f23 = f2[3U];
+ uint64_t f24 = f2[4U];
+ uint64_t f30 = f1[5U];
+ uint64_t f31 = f1[6U];
+ uint64_t f32 = f1[7U];
+ uint64_t f33 = f1[8U];
+ uint64_t f34 = f1[9U];
+ uint64_t f40 = f2[5U];
+ uint64_t f41 = f2[6U];
+ uint64_t f42 = f2[7U];
+ uint64_t f43 = f2[8U];
+ uint64_t f44 = f2[9U];
+ uint64_t tmp11 = f21 * (uint64_t)19U;
+ uint64_t tmp12 = f22 * (uint64_t)19U;
+ uint64_t tmp13 = f23 * (uint64_t)19U;
+ uint64_t tmp14 = f24 * (uint64_t)19U;
+ uint64_t tmp21 = f41 * (uint64_t)19U;
+ uint64_t tmp22 = f42 * (uint64_t)19U;
+ uint64_t tmp23 = f43 * (uint64_t)19U;
+ uint64_t tmp24 = f44 * (uint64_t)19U;
+ FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
+ FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21);
+ FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22);
+ FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
+ FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
+ FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14));
+ FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20));
+ FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21));
+ FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
+ FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
+ FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13));
+ FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14));
+ FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20));
+ FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21));
+ FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22));
+ FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12));
+ FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13));
+ FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14));
+ FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20));
+ FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21));
+ FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11));
+ FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12));
+ FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13));
+ FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14));
+ FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20));
+ FStar_UInt128_uint128 tmp_w10 = o040;
+ FStar_UInt128_uint128 tmp_w11 = o140;
+ FStar_UInt128_uint128 tmp_w12 = o240;
+ FStar_UInt128_uint128 tmp_w13 = o340;
+ FStar_UInt128_uint128 tmp_w14 = o440;
+ FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40);
+ FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41);
+ FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42);
+ FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43);
+ FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44);
+ FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24));
+ FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40));
+ FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41));
+ FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42));
+ FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43));
+ FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23));
+ FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24));
+ FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40));
+ FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41));
+ FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42));
+ FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22));
+ FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23));
+ FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24));
+ FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40));
+ FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41));
+ FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21));
+ FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22));
+ FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23));
+ FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24));
+ FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40));
+ FStar_UInt128_uint128 tmp_w20 = o04;
+ FStar_UInt128_uint128 tmp_w21 = o141;
+ FStar_UInt128_uint128 tmp_w22 = o241;
+ FStar_UInt128_uint128 tmp_w23 = o34;
+ FStar_UInt128_uint128 tmp_w24 = o44;
+ FStar_UInt128_uint128
+ l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+ FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00));
+ uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+ FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10));
+ uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+ FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20));
+ uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+ FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30));
+ uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+ uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c50 = l_4 >> (uint32_t)51U;
+ uint64_t o100 = tmp0_;
+ uint64_t o112 = tmp10 + c50;
+ uint64_t o122 = tmp20;
+ uint64_t o132 = tmp30;
+ uint64_t o142 = tmp40;
+ FStar_UInt128_uint128
+ l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
+ FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0));
+ uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
+ FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1));
+ uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
+ FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2));
+ uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
+ FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3));
+ uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
+ uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_10 >> (uint32_t)51U;
+ uint64_t o200 = tmp0_0;
+ uint64_t o212 = tmp1 + c5;
+ uint64_t o222 = tmp2;
+ uint64_t o232 = tmp3;
+ uint64_t o242 = tmp4;
+ uint64_t o10 = o100;
+ uint64_t o11 = o112;
+ uint64_t o12 = o122;
+ uint64_t o13 = o132;
+ uint64_t o14 = o142;
+ uint64_t o20 = o200;
+ uint64_t o21 = o212;
+ uint64_t o22 = o222;
+ uint64_t o23 = o232;
+ uint64_t o24 = o242;
+ out[0U] = o10;
+ out[1U] = o11;
+ out[2U] = o12;
+ out[3U] = o13;
+ out[4U] = o14;
+ out[5U] = o20;
+ out[6U] = o21;
+ out[7U] = o22;
+ out[8U] = o23;
+ out[9U] = o24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
+{
+ uint64_t f10 = f1[0U];
+ uint64_t f11 = f1[1U];
+ uint64_t f12 = f1[2U];
+ uint64_t f13 = f1[3U];
+ uint64_t f14 = f1[4U];
+ FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10);
+ FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11);
+ FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12);
+ FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13);
+ FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14);
+ FStar_UInt128_uint128
+ l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+ FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
+ uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+ FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
+ uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+ FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
+ uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+ FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
+ uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+ uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ uint64_t o0 = tmp0_;
+ uint64_t o1 = tmp1 + c5;
+ uint64_t o2 = tmp2;
+ uint64_t o3 = tmp3;
+ uint64_t o4 = tmp4;
+ out[0U] = o0;
+ out[1U] = o1;
+ out[2U] = o2;
+ out[3U] = o3;
+ out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
+{
+ uint64_t f0 = f[0U];
+ uint64_t f1 = f[1U];
+ uint64_t f2 = f[2U];
+ uint64_t f3 = f[3U];
+ uint64_t f4 = f[4U];
+ uint64_t d0 = (uint64_t)2U * f0;
+ uint64_t d1 = (uint64_t)2U * f1;
+ uint64_t d2 = (uint64_t)38U * f2;
+ uint64_t d3 = (uint64_t)19U * f3;
+ uint64_t d419 = (uint64_t)19U * f4;
+ uint64_t d4 = (uint64_t)2U * d419;
+ FStar_UInt128_uint128
+ s0 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0),
+ FStar_UInt128_mul_wide(d4, f1)),
+ FStar_UInt128_mul_wide(d2, f3));
+ FStar_UInt128_uint128
+ s1 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1),
+ FStar_UInt128_mul_wide(d4, f2)),
+ FStar_UInt128_mul_wide(d3, f3));
+ FStar_UInt128_uint128
+ s2 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2),
+ FStar_UInt128_mul_wide(f1, f1)),
+ FStar_UInt128_mul_wide(d4, f3));
+ FStar_UInt128_uint128
+ s3 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3),
+ FStar_UInt128_mul_wide(d1, f2)),
+ FStar_UInt128_mul_wide(f4, d419));
+ FStar_UInt128_uint128
+ s4 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4),
+ FStar_UInt128_mul_wide(d1, f3)),
+ FStar_UInt128_mul_wide(f2, f2));
+ FStar_UInt128_uint128 o00 = s0;
+ FStar_UInt128_uint128 o10 = s1;
+ FStar_UInt128_uint128 o20 = s2;
+ FStar_UInt128_uint128 o30 = s3;
+ FStar_UInt128_uint128 o40 = s4;
+ FStar_UInt128_uint128
+ l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+ FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0));
+ uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+ FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1));
+ uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+ FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2));
+ uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+ FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3));
+ uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+ uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ uint64_t o0 = tmp0_;
+ uint64_t o1 = tmp1 + c5;
+ uint64_t o2 = tmp2;
+ uint64_t o3 = tmp3;
+ uint64_t o4 = tmp4;
+ out[0U] = o0;
+ out[1U] = o1;
+ out[2U] = o2;
+ out[3U] = o3;
+ out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
+{
+ uint64_t f10 = f[0U];
+ uint64_t f11 = f[1U];
+ uint64_t f12 = f[2U];
+ uint64_t f13 = f[3U];
+ uint64_t f14 = f[4U];
+ uint64_t f20 = f[5U];
+ uint64_t f21 = f[6U];
+ uint64_t f22 = f[7U];
+ uint64_t f23 = f[8U];
+ uint64_t f24 = f[9U];
+ uint64_t d00 = (uint64_t)2U * f10;
+ uint64_t d10 = (uint64_t)2U * f11;
+ uint64_t d20 = (uint64_t)38U * f12;
+ uint64_t d30 = (uint64_t)19U * f13;
+ uint64_t d4190 = (uint64_t)19U * f14;
+ uint64_t d40 = (uint64_t)2U * d4190;
+ FStar_UInt128_uint128
+ s00 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10),
+ FStar_UInt128_mul_wide(d40, f11)),
+ FStar_UInt128_mul_wide(d20, f13));
+ FStar_UInt128_uint128
+ s10 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11),
+ FStar_UInt128_mul_wide(d40, f12)),
+ FStar_UInt128_mul_wide(d30, f13));
+ FStar_UInt128_uint128
+ s20 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12),
+ FStar_UInt128_mul_wide(f11, f11)),
+ FStar_UInt128_mul_wide(d40, f13));
+ FStar_UInt128_uint128
+ s30 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13),
+ FStar_UInt128_mul_wide(d10, f12)),
+ FStar_UInt128_mul_wide(f14, d4190));
+ FStar_UInt128_uint128
+ s40 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14),
+ FStar_UInt128_mul_wide(d10, f13)),
+ FStar_UInt128_mul_wide(f12, f12));
+ FStar_UInt128_uint128 o100 = s00;
+ FStar_UInt128_uint128 o110 = s10;
+ FStar_UInt128_uint128 o120 = s20;
+ FStar_UInt128_uint128 o130 = s30;
+ FStar_UInt128_uint128 o140 = s40;
+ uint64_t d0 = (uint64_t)2U * f20;
+ uint64_t d1 = (uint64_t)2U * f21;
+ uint64_t d2 = (uint64_t)38U * f22;
+ uint64_t d3 = (uint64_t)19U * f23;
+ uint64_t d419 = (uint64_t)19U * f24;
+ uint64_t d4 = (uint64_t)2U * d419;
+ FStar_UInt128_uint128
+ s0 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20),
+ FStar_UInt128_mul_wide(d4, f21)),
+ FStar_UInt128_mul_wide(d2, f23));
+ FStar_UInt128_uint128
+ s1 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21),
+ FStar_UInt128_mul_wide(d4, f22)),
+ FStar_UInt128_mul_wide(d3, f23));
+ FStar_UInt128_uint128
+ s2 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22),
+ FStar_UInt128_mul_wide(f21, f21)),
+ FStar_UInt128_mul_wide(d4, f23));
+ FStar_UInt128_uint128
+ s3 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23),
+ FStar_UInt128_mul_wide(d1, f22)),
+ FStar_UInt128_mul_wide(f24, d419));
+ FStar_UInt128_uint128
+ s4 =
+ FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24),
+ FStar_UInt128_mul_wide(d1, f23)),
+ FStar_UInt128_mul_wide(f22, f22));
+ FStar_UInt128_uint128 o200 = s0;
+ FStar_UInt128_uint128 o210 = s1;
+ FStar_UInt128_uint128 o220 = s2;
+ FStar_UInt128_uint128 o230 = s3;
+ FStar_UInt128_uint128 o240 = s4;
+ FStar_UInt128_uint128
+ l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+ FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00));
+ uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+ FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10));
+ uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+ FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20));
+ uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+ FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30));
+ uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+ uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c50 = l_4 >> (uint32_t)51U;
+ uint64_t o101 = tmp0_;
+ uint64_t o111 = tmp10 + c50;
+ uint64_t o121 = tmp20;
+ uint64_t o131 = tmp30;
+ uint64_t o141 = tmp40;
+ FStar_UInt128_uint128
+ l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+ uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
+ FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0));
+ uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
+ FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1));
+ uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
+ FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2));
+ uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
+ FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3));
+ uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
+ uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_10 >> (uint32_t)51U;
+ uint64_t o201 = tmp0_0;
+ uint64_t o211 = tmp1 + c5;
+ uint64_t o221 = tmp2;
+ uint64_t o231 = tmp3;
+ uint64_t o241 = tmp4;
+ uint64_t o10 = o101;
+ uint64_t o11 = o111;
+ uint64_t o12 = o121;
+ uint64_t o13 = o131;
+ uint64_t o14 = o141;
+ uint64_t o20 = o201;
+ uint64_t o21 = o211;
+ uint64_t o22 = o221;
+ uint64_t o23 = o231;
+ uint64_t o24 = o241;
+ out[0U] = o10;
+ out[1U] = o11;
+ out[2U] = o12;
+ out[3U] = o13;
+ out[4U] = o14;
+ out[5U] = o20;
+ out[6U] = o21;
+ out[7U] = o22;
+ out[8U] = o23;
+ out[9U] = o24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_store_felem(uint64_t *u64s, uint64_t *f)
+{
+ uint64_t f0 = f[0U];
+ uint64_t f1 = f[1U];
+ uint64_t f2 = f[2U];
+ uint64_t f3 = f[3U];
+ uint64_t f4 = f[4U];
+ uint64_t l_ = f0 + (uint64_t)0U;
+ uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = l_ >> (uint32_t)51U;
+ uint64_t l_0 = f1 + c0;
+ uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = l_0 >> (uint32_t)51U;
+ uint64_t l_1 = f2 + c1;
+ uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = l_1 >> (uint32_t)51U;
+ uint64_t l_2 = f3 + c2;
+ uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = l_2 >> (uint32_t)51U;
+ uint64_t l_3 = f4 + c3;
+ uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = l_3 >> (uint32_t)51U;
+ uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ uint64_t f01 = tmp0_;
+ uint64_t f11 = tmp1 + c5;
+ uint64_t f21 = tmp2;
+ uint64_t f31 = tmp3;
+ uint64_t f41 = tmp4;
+ uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU);
+ uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU);
+ uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU);
+ uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU);
+ uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU);
+ uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
+ uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU);
+ uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f02 = f0_;
+ uint64_t f12 = f1_;
+ uint64_t f22 = f2_;
+ uint64_t f32 = f3_;
+ uint64_t f42 = f4_;
+ uint64_t o00 = f02 | f12 << (uint32_t)51U;
+ uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U;
+ uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U;
+ uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U;
+ uint64_t o0 = o00;
+ uint64_t o1 = o10;
+ uint64_t o2 = o20;
+ uint64_t o3 = o30;
+ u64s[0U] = o0;
+ u64s[1U] = o1;
+ u64s[2U] = o2;
+ u64s[3U] = o3;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_cswap2(uint64_t bit, uint64_t *p1, uint64_t *p2)
+{
+ uint64_t mask = (uint64_t)0U - bit;
+ for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i++) {
+ uint64_t dummy = mask & (p1[i] ^ p2[i]);
+ p1[i] = p1[i] ^ dummy;
+ p2[i] = p2[i] ^ dummy;
+ }
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __Hacl_Bignum25519_51_H_DEFINED
+#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20.c b/lib/freebl/verified/Hacl_Chacha20.c
index 2e552472b..9a74e9f20 100644
--- a/lib/freebl/verified/Hacl_Chacha20.c
+++ b/lib/freebl/verified/Hacl_Chacha20.c
@@ -95,7 +95,7 @@ rounds(uint32_t *st)
static inline void
chacha20_core(uint32_t *k, uint32_t *ctx, uint32_t ctr)
{
- memcpy(k, ctx, (uint32_t)16U * sizeof(ctx[0U]));
+ memcpy(k, ctx, (uint32_t)16U * sizeof(uint32_t));
uint32_t ctr_u32 = ctr;
k[12U] = k[12U] + ctr_u32;
rounds(k);
@@ -169,9 +169,9 @@ static inline void
chacha20_encrypt_last(uint32_t *ctx, uint32_t len, uint8_t *out, uint32_t incr, uint8_t *text)
{
uint8_t plain[64U] = { 0U };
- memcpy(plain, text, len * sizeof(text[0U]));
+ memcpy(plain, text, len * sizeof(uint8_t));
chacha20_encrypt_block(ctx, plain, incr, plain);
- memcpy(out, plain, len * sizeof(plain[0U]));
+ memcpy(out, plain, len * sizeof(uint8_t));
}
static inline void
diff --git a/lib/freebl/verified/Hacl_Chacha20.h b/lib/freebl/verified/Hacl_Chacha20.h
index bd54a315e..850544234 100644
--- a/lib/freebl/verified/Hacl_Chacha20.h
+++ b/lib/freebl/verified/Hacl_Chacha20.h
@@ -21,14 +21,18 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20_H
+#define __Hacl_Chacha20_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20_H
-#define __Hacl_Chacha20_H
-
#include "Hacl_Kremlib.h"
extern const uint32_t Hacl_Impl_Chacha20_Vec_chacha20_constants[4U];
@@ -51,5 +55,9 @@ Hacl_Chacha20_chacha20_decrypt(
uint8_t *n,
uint32_t ctr);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_128.c b/lib/freebl/verified/Hacl_Chacha20Poly1305_128.c
index 1b98e18af..e45fcd9df 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_128.c
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_128.c
@@ -47,9 +47,9 @@ poly1305_padded_128(Lib_IntVector_Intrinsics_vec128 *ctx, uint32_t len, uint8_t
Lib_IntVector_Intrinsics_vec128 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec128_zero;
- Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load_le(block);
+ Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(block);
Lib_IntVector_Intrinsics_vec128
- b2 = Lib_IntVector_Intrinsics_vec128_load_le(block + (uint32_t)16U);
+ b2 = Lib_IntVector_Intrinsics_vec128_load64_le(block + (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2);
Lib_IntVector_Intrinsics_vec128
hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2);
@@ -480,7 +480,7 @@ poly1305_padded_128(Lib_IntVector_Intrinsics_vec128 *ctx, uint32_t len, uint8_t
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec128_zero;
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem1 * sizeof(last[0U]));
+ memcpy(tmp, last, rem1 * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
@@ -685,7 +685,7 @@ poly1305_padded_128(Lib_IntVector_Intrinsics_vec128 *ctx, uint32_t len, uint8_t
acc0[4U] = o4;
}
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, rem, r * sizeof(rem[0U]));
+ memcpy(tmp, rem, r * sizeof(uint8_t));
if (r > (uint32_t)0U) {
Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U;
Lib_IntVector_Intrinsics_vec128 *acc = ctx;
@@ -912,7 +912,9 @@ poly1305_do_128(
ctx[_i] = Lib_IntVector_Intrinsics_vec128_zero;
uint8_t block[16U] = { 0U };
Hacl_Poly1305_128_poly1305_init(ctx, k);
- poly1305_padded_128(ctx, aadlen, aad);
+ if (aadlen != (uint32_t)0U) {
+ poly1305_padded_128(ctx, aadlen, aad);
+ }
poly1305_padded_128(ctx, mlen, m);
store64_le(block, (uint64_t)aadlen);
store64_le(block + (uint32_t)8U, (uint64_t)mlen);
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_128.h b/lib/freebl/verified/Hacl_Chacha20Poly1305_128.h
index 2c4d46bce..bf5f198a7 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_128.h
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_128.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20Poly1305_128_H
+#define __Hacl_Chacha20Poly1305_128_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20Poly1305_128_H
-#define __Hacl_Chacha20Poly1305_128_H
-
#include "Hacl_Kremlib.h"
#include "Hacl_Chacha20_Vec128.h"
#include "Hacl_Poly1305_128.h"
@@ -56,5 +60,9 @@ Hacl_Chacha20Poly1305_128_aead_decrypt(
uint8_t *cipher,
uint8_t *mac);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20Poly1305_128_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_256.c b/lib/freebl/verified/Hacl_Chacha20Poly1305_256.c
index efbccbfdd..efa598ae1 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_256.c
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_256.c
@@ -47,9 +47,9 @@ poly1305_padded_256(Lib_IntVector_Intrinsics_vec256 *ctx, uint32_t len, uint8_t
Lib_IntVector_Intrinsics_vec256 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec256_zero;
- Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load_le(block);
+ Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(block);
Lib_IntVector_Intrinsics_vec256
- hi = Lib_IntVector_Intrinsics_vec256_load_le(block + (uint32_t)32U);
+ hi = Lib_IntVector_Intrinsics_vec256_load64_le(block + (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256
mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU);
Lib_IntVector_Intrinsics_vec256
@@ -482,7 +482,7 @@ poly1305_padded_256(Lib_IntVector_Intrinsics_vec256 *ctx, uint32_t len, uint8_t
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec256_zero;
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem1 * sizeof(last[0U]));
+ memcpy(tmp, last, rem1 * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
@@ -687,7 +687,7 @@ poly1305_padded_256(Lib_IntVector_Intrinsics_vec256 *ctx, uint32_t len, uint8_t
acc0[4U] = o4;
}
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, rem, r * sizeof(rem[0U]));
+ memcpy(tmp, rem, r * sizeof(uint8_t));
if (r > (uint32_t)0U) {
Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U;
Lib_IntVector_Intrinsics_vec256 *acc = ctx;
@@ -914,7 +914,9 @@ poly1305_do_256(
ctx[_i] = Lib_IntVector_Intrinsics_vec256_zero;
uint8_t block[16U] = { 0U };
Hacl_Poly1305_256_poly1305_init(ctx, k);
- poly1305_padded_256(ctx, aadlen, aad);
+ if (aadlen != (uint32_t)0U) {
+ poly1305_padded_256(ctx, aadlen, aad);
+ }
poly1305_padded_256(ctx, mlen, m);
store64_le(block, (uint64_t)aadlen);
store64_le(block + (uint32_t)8U, (uint64_t)mlen);
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_256.h b/lib/freebl/verified/Hacl_Chacha20Poly1305_256.h
index 550cc0564..09ebbbf3d 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_256.h
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_256.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20Poly1305_256_H
+#define __Hacl_Chacha20Poly1305_256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20Poly1305_256_H
-#define __Hacl_Chacha20Poly1305_256_H
-
#include "Hacl_Kremlib.h"
#include "Hacl_Chacha20_Vec256.h"
#include "Hacl_Poly1305_256.h"
@@ -56,5 +60,9 @@ Hacl_Chacha20Poly1305_256_aead_decrypt(
uint8_t *cipher,
uint8_t *mac);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20Poly1305_256_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_32.c b/lib/freebl/verified/Hacl_Chacha20Poly1305_32.c
index 760e3d548..493a31695 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_32.c
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_32.c
@@ -157,7 +157,7 @@ poly1305_padded_32(uint64_t *ctx, uint32_t len, uint8_t *text)
uint8_t *last = blocks + nb * (uint32_t)16U;
uint64_t e[5U] = { 0U };
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem1 * sizeof(last[0U]));
+ memcpy(tmp, last, rem1 * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
@@ -275,7 +275,7 @@ poly1305_padded_32(uint64_t *ctx, uint32_t len, uint8_t *text)
acc0[4U] = o4;
}
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, rem, r * sizeof(rem[0U]));
+ memcpy(tmp, rem, r * sizeof(uint8_t));
if (r > (uint32_t)0U) {
uint64_t *pre = ctx + (uint32_t)5U;
uint64_t *acc = ctx;
@@ -411,7 +411,9 @@ poly1305_do_32(
uint64_t ctx[25U] = { 0U };
uint8_t block[16U] = { 0U };
Hacl_Poly1305_32_poly1305_init(ctx, k);
- poly1305_padded_32(ctx, aadlen, aad);
+ if (aadlen != (uint32_t)0U) {
+ poly1305_padded_32(ctx, aadlen, aad);
+ }
poly1305_padded_32(ctx, mlen, m);
store64_le(block, (uint64_t)aadlen);
store64_le(block + (uint32_t)8U, (uint64_t)mlen);
diff --git a/lib/freebl/verified/Hacl_Chacha20Poly1305_32.h b/lib/freebl/verified/Hacl_Chacha20Poly1305_32.h
index 615f3f96d..f7854685c 100644
--- a/lib/freebl/verified/Hacl_Chacha20Poly1305_32.h
+++ b/lib/freebl/verified/Hacl_Chacha20Poly1305_32.h
@@ -21,14 +21,18 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20Poly1305_32_H
+#define __Hacl_Chacha20Poly1305_32_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20Poly1305_32_H
-#define __Hacl_Chacha20Poly1305_32_H
-
#include "Hacl_Chacha20.h"
#include "Hacl_Kremlib.h"
#include "Hacl_Poly1305_32.h"
@@ -55,5 +59,9 @@ Hacl_Chacha20Poly1305_32_aead_decrypt(
uint8_t *cipher,
uint8_t *mac);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20Poly1305_32_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20_Vec128.c b/lib/freebl/verified/Hacl_Chacha20_Vec128.c
index cf80c431d..485c78d34 100644
--- a/lib/freebl/verified/Hacl_Chacha20_Vec128.c
+++ b/lib/freebl/verified/Hacl_Chacha20_Vec128.c
@@ -130,7 +130,7 @@ chacha20_core_128(
Lib_IntVector_Intrinsics_vec128 *ctx,
uint32_t ctr)
{
- memcpy(k, ctx, (uint32_t)16U * sizeof(ctx[0U]));
+ memcpy(k, ctx, (uint32_t)16U * sizeof(Lib_IntVector_Intrinsics_vec128));
uint32_t ctr_u32 = (uint32_t)4U * ctr;
Lib_IntVector_Intrinsics_vec128 cv = Lib_IntVector_Intrinsics_vec128_load32(ctr_u32);
k[12U] = Lib_IntVector_Intrinsics_vec128_add32(k[12U], cv);
@@ -334,16 +334,16 @@ Hacl_Chacha20_Vec128_chacha20_encrypt_128(
k[15U] = v15;
for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)16U; i0++) {
Lib_IntVector_Intrinsics_vec128
- x = Lib_IntVector_Intrinsics_vec128_load_le(uu____1 + i0 * (uint32_t)16U);
+ x = Lib_IntVector_Intrinsics_vec128_load32_le(uu____1 + i0 * (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i0]);
- Lib_IntVector_Intrinsics_vec128_store_le(uu____0 + i0 * (uint32_t)16U, y);
+ Lib_IntVector_Intrinsics_vec128_store32_le(uu____0 + i0 * (uint32_t)16U, y);
}
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)256U;
uint8_t *uu____3 = text + nb * (uint32_t)256U;
uint8_t plain[256U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uu____3[0U]));
+ memcpy(plain, uu____3, rem * sizeof(uint8_t));
Lib_IntVector_Intrinsics_vec128 k[16U];
for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
k[_i] = Lib_IntVector_Intrinsics_vec128_zero;
@@ -462,11 +462,11 @@ Hacl_Chacha20_Vec128_chacha20_encrypt_128(
k[15U] = v15;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) {
Lib_IntVector_Intrinsics_vec128
- x = Lib_IntVector_Intrinsics_vec128_load_le(plain + i * (uint32_t)16U);
+ x = Lib_IntVector_Intrinsics_vec128_load32_le(plain + i * (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i]);
- Lib_IntVector_Intrinsics_vec128_store_le(plain + i * (uint32_t)16U, y);
+ Lib_IntVector_Intrinsics_vec128_store32_le(plain + i * (uint32_t)16U, y);
}
- memcpy(uu____2, plain, rem * sizeof(plain[0U]));
+ memcpy(uu____2, plain, rem * sizeof(uint8_t));
}
}
@@ -607,16 +607,16 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128(
k[15U] = v15;
for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)16U; i0++) {
Lib_IntVector_Intrinsics_vec128
- x = Lib_IntVector_Intrinsics_vec128_load_le(uu____1 + i0 * (uint32_t)16U);
+ x = Lib_IntVector_Intrinsics_vec128_load32_le(uu____1 + i0 * (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i0]);
- Lib_IntVector_Intrinsics_vec128_store_le(uu____0 + i0 * (uint32_t)16U, y);
+ Lib_IntVector_Intrinsics_vec128_store32_le(uu____0 + i0 * (uint32_t)16U, y);
}
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)256U;
uint8_t *uu____3 = cipher + nb * (uint32_t)256U;
uint8_t plain[256U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uu____3[0U]));
+ memcpy(plain, uu____3, rem * sizeof(uint8_t));
Lib_IntVector_Intrinsics_vec128 k[16U];
for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
k[_i] = Lib_IntVector_Intrinsics_vec128_zero;
@@ -735,10 +735,10 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128(
k[15U] = v15;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) {
Lib_IntVector_Intrinsics_vec128
- x = Lib_IntVector_Intrinsics_vec128_load_le(plain + i * (uint32_t)16U);
+ x = Lib_IntVector_Intrinsics_vec128_load32_le(plain + i * (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i]);
- Lib_IntVector_Intrinsics_vec128_store_le(plain + i * (uint32_t)16U, y);
+ Lib_IntVector_Intrinsics_vec128_store32_le(plain + i * (uint32_t)16U, y);
}
- memcpy(uu____2, plain, rem * sizeof(plain[0U]));
+ memcpy(uu____2, plain, rem * sizeof(uint8_t));
}
}
diff --git a/lib/freebl/verified/Hacl_Chacha20_Vec128.h b/lib/freebl/verified/Hacl_Chacha20_Vec128.h
index dc59ba1c7..6b3a8e08b 100644
--- a/lib/freebl/verified/Hacl_Chacha20_Vec128.h
+++ b/lib/freebl/verified/Hacl_Chacha20_Vec128.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20_Vec128_H
+#define __Hacl_Chacha20_Vec128_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20_Vec128_H
-#define __Hacl_Chacha20_Vec128_H
-
#include "Hacl_Chacha20.h"
#include "Hacl_Kremlib.h"
@@ -51,5 +55,9 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128(
uint8_t *n,
uint32_t ctr);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20_Vec128_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Chacha20_Vec256.c b/lib/freebl/verified/Hacl_Chacha20_Vec256.c
index 49902c130..72b235123 100644
--- a/lib/freebl/verified/Hacl_Chacha20_Vec256.c
+++ b/lib/freebl/verified/Hacl_Chacha20_Vec256.c
@@ -130,7 +130,7 @@ chacha20_core_256(
Lib_IntVector_Intrinsics_vec256 *ctx,
uint32_t ctr)
{
- memcpy(k, ctx, (uint32_t)16U * sizeof(ctx[0U]));
+ memcpy(k, ctx, (uint32_t)16U * sizeof(Lib_IntVector_Intrinsics_vec256));
uint32_t ctr_u32 = (uint32_t)8U * ctr;
Lib_IntVector_Intrinsics_vec256 cv = Lib_IntVector_Intrinsics_vec256_load32(ctr_u32);
k[12U] = Lib_IntVector_Intrinsics_vec256_add32(k[12U], cv);
@@ -370,16 +370,16 @@ Hacl_Chacha20_Vec256_chacha20_encrypt_256(
k[15U] = v15;
for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)16U; i0++) {
Lib_IntVector_Intrinsics_vec256
- x = Lib_IntVector_Intrinsics_vec256_load_le(uu____1 + i0 * (uint32_t)32U);
+ x = Lib_IntVector_Intrinsics_vec256_load32_le(uu____1 + i0 * (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i0]);
- Lib_IntVector_Intrinsics_vec256_store_le(uu____0 + i0 * (uint32_t)32U, y);
+ Lib_IntVector_Intrinsics_vec256_store32_le(uu____0 + i0 * (uint32_t)32U, y);
}
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)512U;
uint8_t *uu____3 = text + nb * (uint32_t)512U;
uint8_t plain[512U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uu____3[0U]));
+ memcpy(plain, uu____3, rem * sizeof(uint8_t));
Lib_IntVector_Intrinsics_vec256 k[16U];
for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
k[_i] = Lib_IntVector_Intrinsics_vec256_zero;
@@ -530,11 +530,11 @@ Hacl_Chacha20_Vec256_chacha20_encrypt_256(
k[15U] = v15;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) {
Lib_IntVector_Intrinsics_vec256
- x = Lib_IntVector_Intrinsics_vec256_load_le(plain + i * (uint32_t)32U);
+ x = Lib_IntVector_Intrinsics_vec256_load32_le(plain + i * (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i]);
- Lib_IntVector_Intrinsics_vec256_store_le(plain + i * (uint32_t)32U, y);
+ Lib_IntVector_Intrinsics_vec256_store32_le(plain + i * (uint32_t)32U, y);
}
- memcpy(uu____2, plain, rem * sizeof(plain[0U]));
+ memcpy(uu____2, plain, rem * sizeof(uint8_t));
}
}
@@ -707,16 +707,16 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256(
k[15U] = v15;
for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)16U; i0++) {
Lib_IntVector_Intrinsics_vec256
- x = Lib_IntVector_Intrinsics_vec256_load_le(uu____1 + i0 * (uint32_t)32U);
+ x = Lib_IntVector_Intrinsics_vec256_load32_le(uu____1 + i0 * (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i0]);
- Lib_IntVector_Intrinsics_vec256_store_le(uu____0 + i0 * (uint32_t)32U, y);
+ Lib_IntVector_Intrinsics_vec256_store32_le(uu____0 + i0 * (uint32_t)32U, y);
}
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)512U;
uint8_t *uu____3 = cipher + nb * (uint32_t)512U;
uint8_t plain[512U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uu____3[0U]));
+ memcpy(plain, uu____3, rem * sizeof(uint8_t));
Lib_IntVector_Intrinsics_vec256 k[16U];
for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
k[_i] = Lib_IntVector_Intrinsics_vec256_zero;
@@ -867,10 +867,10 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256(
k[15U] = v15;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i++) {
Lib_IntVector_Intrinsics_vec256
- x = Lib_IntVector_Intrinsics_vec256_load_le(plain + i * (uint32_t)32U);
+ x = Lib_IntVector_Intrinsics_vec256_load32_le(plain + i * (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i]);
- Lib_IntVector_Intrinsics_vec256_store_le(plain + i * (uint32_t)32U, y);
+ Lib_IntVector_Intrinsics_vec256_store32_le(plain + i * (uint32_t)32U, y);
}
- memcpy(uu____2, plain, rem * sizeof(plain[0U]));
+ memcpy(uu____2, plain, rem * sizeof(uint8_t));
}
}
diff --git a/lib/freebl/verified/Hacl_Chacha20_Vec256.h b/lib/freebl/verified/Hacl_Chacha20_Vec256.h
index 1ae9ea379..478f2813f 100644
--- a/lib/freebl/verified/Hacl_Chacha20_Vec256.h
+++ b/lib/freebl/verified/Hacl_Chacha20_Vec256.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Chacha20_Vec256_H
+#define __Hacl_Chacha20_Vec256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Chacha20_Vec256_H
-#define __Hacl_Chacha20_Vec256_H
-
#include "Hacl_Chacha20.h"
#include "Hacl_Kremlib.h"
@@ -51,5 +55,9 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256(
uint8_t *n,
uint32_t ctr);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Chacha20_Vec256_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Curve25519_51.c b/lib/freebl/verified/Hacl_Curve25519_51.c
index 2b76eafe2..d366d5ced 100644
--- a/lib/freebl/verified/Hacl_Curve25519_51.c
+++ b/lib/freebl/verified/Hacl_Curve25519_51.c
@@ -23,631 +23,6 @@
#include "Hacl_Curve25519_51.h"
-static inline void
-fadd0(uint64_t *out, uint64_t *f1, uint64_t *f2)
-{
- uint64_t f10 = f1[0U];
- uint64_t f20 = f2[0U];
- uint64_t f11 = f1[1U];
- uint64_t f21 = f2[1U];
- uint64_t f12 = f1[2U];
- uint64_t f22 = f2[2U];
- uint64_t f13 = f1[3U];
- uint64_t f23 = f2[3U];
- uint64_t f14 = f1[4U];
- uint64_t f24 = f2[4U];
- out[0U] = f10 + f20;
- out[1U] = f11 + f21;
- out[2U] = f12 + f22;
- out[3U] = f13 + f23;
- out[4U] = f14 + f24;
-}
-
-static inline void
-fsub0(uint64_t *out, uint64_t *f1, uint64_t *f2)
-{
- uint64_t f10 = f1[0U];
- uint64_t f20 = f2[0U];
- uint64_t f11 = f1[1U];
- uint64_t f21 = f2[1U];
- uint64_t f12 = f1[2U];
- uint64_t f22 = f2[2U];
- uint64_t f13 = f1[3U];
- uint64_t f23 = f2[3U];
- uint64_t f14 = f1[4U];
- uint64_t f24 = f2[4U];
- out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20;
- out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21;
- out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22;
- out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23;
- out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24;
-}
-
-static inline void
-fmul0(uint64_t *out, uint64_t *f1, uint64_t *f2)
-{
- uint64_t f10 = f1[0U];
- uint64_t f11 = f1[1U];
- uint64_t f12 = f1[2U];
- uint64_t f13 = f1[3U];
- uint64_t f14 = f1[4U];
- uint64_t f20 = f2[0U];
- uint64_t f21 = f2[1U];
- uint64_t f22 = f2[2U];
- uint64_t f23 = f2[3U];
- uint64_t f24 = f2[4U];
- uint64_t tmp1 = f21 * (uint64_t)19U;
- uint64_t tmp2 = f22 * (uint64_t)19U;
- uint64_t tmp3 = f23 * (uint64_t)19U;
- uint64_t tmp4 = f24 * (uint64_t)19U;
- FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
- FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21);
- FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22);
- FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
- FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
- FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4));
- FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20));
- FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21));
- FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
- FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
- FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3));
- FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4));
- FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20));
- FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21));
- FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22));
- FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2));
- FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3));
- FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4));
- FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20));
- FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21));
- FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1));
- FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2));
- FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3));
- FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4));
- FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20));
- FStar_UInt128_uint128 tmp_w0 = o04;
- FStar_UInt128_uint128 tmp_w1 = o14;
- FStar_UInt128_uint128 tmp_w2 = o24;
- FStar_UInt128_uint128 tmp_w3 = o34;
- FStar_UInt128_uint128 tmp_w4 = o44;
- FStar_UInt128_uint128
- l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
- FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
- uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
- FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
- uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
- FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
- uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
- FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
- uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
- uint64_t l_4 = tmp01 + c4 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_4 >> (uint32_t)51U;
- uint64_t o0 = tmp0_;
- uint64_t o1 = tmp11 + c5;
- uint64_t o2 = tmp21;
- uint64_t o3 = tmp31;
- uint64_t o4 = tmp41;
- out[0U] = o0;
- out[1U] = o1;
- out[2U] = o2;
- out[3U] = o3;
- out[4U] = o4;
-}
-
-static inline void
-fmul20(uint64_t *out, uint64_t *f1, uint64_t *f2)
-{
- uint64_t f10 = f1[0U];
- uint64_t f11 = f1[1U];
- uint64_t f12 = f1[2U];
- uint64_t f13 = f1[3U];
- uint64_t f14 = f1[4U];
- uint64_t f20 = f2[0U];
- uint64_t f21 = f2[1U];
- uint64_t f22 = f2[2U];
- uint64_t f23 = f2[3U];
- uint64_t f24 = f2[4U];
- uint64_t f30 = f1[5U];
- uint64_t f31 = f1[6U];
- uint64_t f32 = f1[7U];
- uint64_t f33 = f1[8U];
- uint64_t f34 = f1[9U];
- uint64_t f40 = f2[5U];
- uint64_t f41 = f2[6U];
- uint64_t f42 = f2[7U];
- uint64_t f43 = f2[8U];
- uint64_t f44 = f2[9U];
- uint64_t tmp11 = f21 * (uint64_t)19U;
- uint64_t tmp12 = f22 * (uint64_t)19U;
- uint64_t tmp13 = f23 * (uint64_t)19U;
- uint64_t tmp14 = f24 * (uint64_t)19U;
- uint64_t tmp21 = f41 * (uint64_t)19U;
- uint64_t tmp22 = f42 * (uint64_t)19U;
- uint64_t tmp23 = f43 * (uint64_t)19U;
- uint64_t tmp24 = f44 * (uint64_t)19U;
- FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
- FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21);
- FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22);
- FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
- FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
- FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14));
- FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20));
- FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21));
- FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
- FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
- FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13));
- FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14));
- FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20));
- FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21));
- FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22));
- FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12));
- FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13));
- FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14));
- FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20));
- FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21));
- FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11));
- FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12));
- FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13));
- FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14));
- FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20));
- FStar_UInt128_uint128 tmp_w10 = o040;
- FStar_UInt128_uint128 tmp_w11 = o140;
- FStar_UInt128_uint128 tmp_w12 = o240;
- FStar_UInt128_uint128 tmp_w13 = o340;
- FStar_UInt128_uint128 tmp_w14 = o440;
- FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40);
- FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41);
- FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42);
- FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43);
- FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44);
- FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24));
- FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40));
- FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41));
- FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42));
- FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43));
- FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23));
- FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24));
- FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40));
- FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41));
- FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42));
- FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22));
- FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23));
- FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24));
- FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40));
- FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41));
- FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21));
- FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22));
- FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23));
- FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24));
- FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40));
- FStar_UInt128_uint128 tmp_w20 = o04;
- FStar_UInt128_uint128 tmp_w21 = o141;
- FStar_UInt128_uint128 tmp_w22 = o241;
- FStar_UInt128_uint128 tmp_w23 = o34;
- FStar_UInt128_uint128 tmp_w24 = o44;
- FStar_UInt128_uint128
- l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
- uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
- FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00));
- uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
- uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
- FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10));
- uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
- uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
- FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20));
- uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
- uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
- FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30));
- uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
- uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
- uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c50 = l_4 >> (uint32_t)51U;
- uint64_t o100 = tmp0_;
- uint64_t o112 = tmp10 + c50;
- uint64_t o122 = tmp20;
- uint64_t o132 = tmp30;
- uint64_t o142 = tmp40;
- FStar_UInt128_uint128
- l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
- FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0));
- uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
- FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1));
- uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
- FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2));
- uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
- FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3));
- uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
- uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
- uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_10 >> (uint32_t)51U;
- uint64_t o200 = tmp0_0;
- uint64_t o212 = tmp1 + c5;
- uint64_t o222 = tmp2;
- uint64_t o232 = tmp3;
- uint64_t o242 = tmp4;
- uint64_t o10 = o100;
- uint64_t o11 = o112;
- uint64_t o12 = o122;
- uint64_t o13 = o132;
- uint64_t o14 = o142;
- uint64_t o20 = o200;
- uint64_t o21 = o212;
- uint64_t o22 = o222;
- uint64_t o23 = o232;
- uint64_t o24 = o242;
- out[0U] = o10;
- out[1U] = o11;
- out[2U] = o12;
- out[3U] = o13;
- out[4U] = o14;
- out[5U] = o20;
- out[6U] = o21;
- out[7U] = o22;
- out[8U] = o23;
- out[9U] = o24;
-}
-
-static inline void
-fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
-{
- uint64_t f10 = f1[0U];
- uint64_t f11 = f1[1U];
- uint64_t f12 = f1[2U];
- uint64_t f13 = f1[3U];
- uint64_t f14 = f1[4U];
- FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10);
- FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11);
- FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12);
- FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13);
- FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14);
- FStar_UInt128_uint128
- l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
- FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
- uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
- FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
- uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
- FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
- uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
- FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
- uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
- uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_4 >> (uint32_t)51U;
- uint64_t o0 = tmp0_;
- uint64_t o1 = tmp1 + c5;
- uint64_t o2 = tmp2;
- uint64_t o3 = tmp3;
- uint64_t o4 = tmp4;
- out[0U] = o0;
- out[1U] = o1;
- out[2U] = o2;
- out[3U] = o3;
- out[4U] = o4;
-}
-
-static inline void
-fsqr0(uint64_t *out, uint64_t *f)
-{
- uint64_t f0 = f[0U];
- uint64_t f1 = f[1U];
- uint64_t f2 = f[2U];
- uint64_t f3 = f[3U];
- uint64_t f4 = f[4U];
- uint64_t d0 = (uint64_t)2U * f0;
- uint64_t d1 = (uint64_t)2U * f1;
- uint64_t d2 = (uint64_t)38U * f2;
- uint64_t d3 = (uint64_t)19U * f3;
- uint64_t d419 = (uint64_t)19U * f4;
- uint64_t d4 = (uint64_t)2U * d419;
- FStar_UInt128_uint128
- s0 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0),
- FStar_UInt128_mul_wide(d4, f1)),
- FStar_UInt128_mul_wide(d2, f3));
- FStar_UInt128_uint128
- s1 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1),
- FStar_UInt128_mul_wide(d4, f2)),
- FStar_UInt128_mul_wide(d3, f3));
- FStar_UInt128_uint128
- s2 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2),
- FStar_UInt128_mul_wide(f1, f1)),
- FStar_UInt128_mul_wide(d4, f3));
- FStar_UInt128_uint128
- s3 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3),
- FStar_UInt128_mul_wide(d1, f2)),
- FStar_UInt128_mul_wide(f4, d419));
- FStar_UInt128_uint128
- s4 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4),
- FStar_UInt128_mul_wide(d1, f3)),
- FStar_UInt128_mul_wide(f2, f2));
- FStar_UInt128_uint128 o00 = s0;
- FStar_UInt128_uint128 o10 = s1;
- FStar_UInt128_uint128 o20 = s2;
- FStar_UInt128_uint128 o30 = s3;
- FStar_UInt128_uint128 o40 = s4;
- FStar_UInt128_uint128
- l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
- FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0));
- uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
- FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1));
- uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
- FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2));
- uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
- FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3));
- uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
- uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_4 >> (uint32_t)51U;
- uint64_t o0 = tmp0_;
- uint64_t o1 = tmp1 + c5;
- uint64_t o2 = tmp2;
- uint64_t o3 = tmp3;
- uint64_t o4 = tmp4;
- out[0U] = o0;
- out[1U] = o1;
- out[2U] = o2;
- out[3U] = o3;
- out[4U] = o4;
-}
-
-static inline void
-fsqr20(uint64_t *out, uint64_t *f)
-{
- uint64_t f10 = f[0U];
- uint64_t f11 = f[1U];
- uint64_t f12 = f[2U];
- uint64_t f13 = f[3U];
- uint64_t f14 = f[4U];
- uint64_t f20 = f[5U];
- uint64_t f21 = f[6U];
- uint64_t f22 = f[7U];
- uint64_t f23 = f[8U];
- uint64_t f24 = f[9U];
- uint64_t d00 = (uint64_t)2U * f10;
- uint64_t d10 = (uint64_t)2U * f11;
- uint64_t d20 = (uint64_t)38U * f12;
- uint64_t d30 = (uint64_t)19U * f13;
- uint64_t d4190 = (uint64_t)19U * f14;
- uint64_t d40 = (uint64_t)2U * d4190;
- FStar_UInt128_uint128
- s00 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10),
- FStar_UInt128_mul_wide(d40, f11)),
- FStar_UInt128_mul_wide(d20, f13));
- FStar_UInt128_uint128
- s10 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11),
- FStar_UInt128_mul_wide(d40, f12)),
- FStar_UInt128_mul_wide(d30, f13));
- FStar_UInt128_uint128
- s20 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12),
- FStar_UInt128_mul_wide(f11, f11)),
- FStar_UInt128_mul_wide(d40, f13));
- FStar_UInt128_uint128
- s30 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13),
- FStar_UInt128_mul_wide(d10, f12)),
- FStar_UInt128_mul_wide(f14, d4190));
- FStar_UInt128_uint128
- s40 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14),
- FStar_UInt128_mul_wide(d10, f13)),
- FStar_UInt128_mul_wide(f12, f12));
- FStar_UInt128_uint128 o100 = s00;
- FStar_UInt128_uint128 o110 = s10;
- FStar_UInt128_uint128 o120 = s20;
- FStar_UInt128_uint128 o130 = s30;
- FStar_UInt128_uint128 o140 = s40;
- uint64_t d0 = (uint64_t)2U * f20;
- uint64_t d1 = (uint64_t)2U * f21;
- uint64_t d2 = (uint64_t)38U * f22;
- uint64_t d3 = (uint64_t)19U * f23;
- uint64_t d419 = (uint64_t)19U * f24;
- uint64_t d4 = (uint64_t)2U * d419;
- FStar_UInt128_uint128
- s0 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20),
- FStar_UInt128_mul_wide(d4, f21)),
- FStar_UInt128_mul_wide(d2, f23));
- FStar_UInt128_uint128
- s1 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21),
- FStar_UInt128_mul_wide(d4, f22)),
- FStar_UInt128_mul_wide(d3, f23));
- FStar_UInt128_uint128
- s2 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22),
- FStar_UInt128_mul_wide(f21, f21)),
- FStar_UInt128_mul_wide(d4, f23));
- FStar_UInt128_uint128
- s3 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23),
- FStar_UInt128_mul_wide(d1, f22)),
- FStar_UInt128_mul_wide(f24, d419));
- FStar_UInt128_uint128
- s4 =
- FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24),
- FStar_UInt128_mul_wide(d1, f23)),
- FStar_UInt128_mul_wide(f22, f22));
- FStar_UInt128_uint128 o200 = s0;
- FStar_UInt128_uint128 o210 = s1;
- FStar_UInt128_uint128 o220 = s2;
- FStar_UInt128_uint128 o230 = s3;
- FStar_UInt128_uint128 o240 = s4;
- FStar_UInt128_uint128
- l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
- uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
- FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00));
- uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
- uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
- FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10));
- uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
- uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
- FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20));
- uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
- uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
- FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30));
- uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
- uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
- uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c50 = l_4 >> (uint32_t)51U;
- uint64_t o101 = tmp0_;
- uint64_t o111 = tmp10 + c50;
- uint64_t o121 = tmp20;
- uint64_t o131 = tmp30;
- uint64_t o141 = tmp40;
- FStar_UInt128_uint128
- l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
- uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
- FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0));
- uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
- FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1));
- uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
- FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2));
- uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
- FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3));
- uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
- uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
- uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_10 >> (uint32_t)51U;
- uint64_t o201 = tmp0_0;
- uint64_t o211 = tmp1 + c5;
- uint64_t o221 = tmp2;
- uint64_t o231 = tmp3;
- uint64_t o241 = tmp4;
- uint64_t o10 = o101;
- uint64_t o11 = o111;
- uint64_t o12 = o121;
- uint64_t o13 = o131;
- uint64_t o14 = o141;
- uint64_t o20 = o201;
- uint64_t o21 = o211;
- uint64_t o22 = o221;
- uint64_t o23 = o231;
- uint64_t o24 = o241;
- out[0U] = o10;
- out[1U] = o11;
- out[2U] = o12;
- out[3U] = o13;
- out[4U] = o14;
- out[5U] = o20;
- out[6U] = o21;
- out[7U] = o22;
- out[8U] = o23;
- out[9U] = o24;
-}
-
-static void
-store_felem(uint64_t *u64s, uint64_t *f)
-{
- uint64_t f0 = f[0U];
- uint64_t f1 = f[1U];
- uint64_t f2 = f[2U];
- uint64_t f3 = f[3U];
- uint64_t f4 = f[4U];
- uint64_t l_ = f0 + (uint64_t)0U;
- uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
- uint64_t c0 = l_ >> (uint32_t)51U;
- uint64_t l_0 = f1 + c0;
- uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
- uint64_t c1 = l_0 >> (uint32_t)51U;
- uint64_t l_1 = f2 + c1;
- uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
- uint64_t c2 = l_1 >> (uint32_t)51U;
- uint64_t l_2 = f3 + c2;
- uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
- uint64_t c3 = l_2 >> (uint32_t)51U;
- uint64_t l_3 = f4 + c3;
- uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
- uint64_t c4 = l_3 >> (uint32_t)51U;
- uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
- uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
- uint64_t c5 = l_4 >> (uint32_t)51U;
- uint64_t f01 = tmp0_;
- uint64_t f11 = tmp1 + c5;
- uint64_t f21 = tmp2;
- uint64_t f31 = tmp3;
- uint64_t f41 = tmp4;
- uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU);
- uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU);
- uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU);
- uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU);
- uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU);
- uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
- uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU);
- uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU);
- uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU);
- uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU);
- uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU);
- uint64_t f02 = f0_;
- uint64_t f12 = f1_;
- uint64_t f22 = f2_;
- uint64_t f32 = f3_;
- uint64_t f42 = f4_;
- uint64_t o00 = f02 | f12 << (uint32_t)51U;
- uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U;
- uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U;
- uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U;
- uint64_t o0 = o00;
- uint64_t o1 = o10;
- uint64_t o2 = o20;
- uint64_t o3 = o30;
- u64s[0U] = o0;
- u64s[1U] = o1;
- u64s[2U] = o2;
- u64s[3U] = o3;
-}
-
-static inline void
-cswap20(uint64_t bit, uint64_t *p1, uint64_t *p2)
-{
- uint64_t mask = (uint64_t)0U - bit;
- for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i++) {
- uint64_t dummy = mask & (p1[i] ^ p2[i]);
- p1[i] = p1[i] ^ dummy;
- p2[i] = p2[i] ^ dummy;
- }
-}
-
static const uint8_t g25519[32U] = { (uint8_t)9U };
static void
@@ -664,35 +39,35 @@ point_add_and_double(uint64_t *q, uint64_t *p01_tmp1, FStar_UInt128_uint128 *tmp
uint64_t *b = tmp1 + (uint32_t)5U;
uint64_t *ab = tmp1;
uint64_t *dc = tmp1 + (uint32_t)10U;
- fadd0(a, x2, z2);
- fsub0(b, x2, z2);
+ Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2);
+ Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2);
uint64_t *x3 = nq_p1;
uint64_t *z31 = nq_p1 + (uint32_t)5U;
uint64_t *d0 = dc;
uint64_t *c0 = dc + (uint32_t)5U;
- fadd0(c0, x3, z31);
- fsub0(d0, x3, z31);
- fmul20(dc, dc, ab);
- fadd0(x3, d0, c0);
- fsub0(z31, d0, c0);
+ Hacl_Impl_Curve25519_Field51_fadd(c0, x3, z31);
+ Hacl_Impl_Curve25519_Field51_fsub(d0, x3, z31);
+ Hacl_Impl_Curve25519_Field51_fmul2(dc, dc, ab, tmp2);
+ Hacl_Impl_Curve25519_Field51_fadd(x3, d0, c0);
+ Hacl_Impl_Curve25519_Field51_fsub(z31, d0, c0);
uint64_t *a1 = tmp1;
uint64_t *b1 = tmp1 + (uint32_t)5U;
uint64_t *d = tmp1 + (uint32_t)10U;
uint64_t *c = tmp1 + (uint32_t)15U;
uint64_t *ab1 = tmp1;
uint64_t *dc1 = tmp1 + (uint32_t)10U;
- fsqr20(dc1, ab1);
- fsqr20(nq_p1, nq_p1);
+ Hacl_Impl_Curve25519_Field51_fsqr2(dc1, ab1, tmp2);
+ Hacl_Impl_Curve25519_Field51_fsqr2(nq_p1, nq_p1, tmp2);
a1[0U] = c[0U];
a1[1U] = c[1U];
a1[2U] = c[2U];
a1[3U] = c[3U];
a1[4U] = c[4U];
- fsub0(c, d, c);
- fmul1(b1, c, (uint64_t)121665U);
- fadd0(b1, b1, d);
- fmul20(nq, dc1, ab1);
- fmul0(z3, z3, x1);
+ Hacl_Impl_Curve25519_Field51_fsub(c, d, c);
+ Hacl_Impl_Curve25519_Field51_fmul1(b1, c, (uint64_t)121665U);
+ Hacl_Impl_Curve25519_Field51_fadd(b1, b1, d);
+ Hacl_Impl_Curve25519_Field51_fmul2(nq, dc1, ab1, tmp2);
+ Hacl_Impl_Curve25519_Field51_fmul(z3, z3, x1, tmp2);
}
static void
@@ -706,18 +81,18 @@ point_double(uint64_t *nq, uint64_t *tmp1, FStar_UInt128_uint128 *tmp2)
uint64_t *c = tmp1 + (uint32_t)15U;
uint64_t *ab = tmp1;
uint64_t *dc = tmp1 + (uint32_t)10U;
- fadd0(a, x2, z2);
- fsub0(b, x2, z2);
- fsqr20(dc, ab);
+ Hacl_Impl_Curve25519_Field51_fadd(a, x2, z2);
+ Hacl_Impl_Curve25519_Field51_fsub(b, x2, z2);
+ Hacl_Impl_Curve25519_Field51_fsqr2(dc, ab, tmp2);
a[0U] = c[0U];
a[1U] = c[1U];
a[2U] = c[2U];
a[3U] = c[3U];
a[4U] = c[4U];
- fsub0(c, d, c);
- fmul1(b, c, (uint64_t)121665U);
- fadd0(b, b, d);
- fmul20(nq, dc, ab);
+ Hacl_Impl_Curve25519_Field51_fsub(c, d, c);
+ Hacl_Impl_Curve25519_Field51_fmul1(b, c, (uint64_t)121665U);
+ Hacl_Impl_Curve25519_Field51_fadd(b, b, d);
+ Hacl_Impl_Curve25519_Field51_fmul2(nq, dc, ab, tmp2);
}
static void
@@ -731,7 +106,7 @@ montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init)
uint64_t *p01 = p01_tmp1_swap;
uint64_t *p03 = p01;
uint64_t *p11 = p01 + (uint32_t)10U;
- memcpy(p11, init, (uint32_t)10U * sizeof(init[0U]));
+ memcpy(p11, init, (uint32_t)10U * sizeof(uint64_t));
uint64_t *x0 = p03;
uint64_t *z0 = p03 + (uint32_t)5U;
x0[0U] = (uint64_t)1U;
@@ -749,7 +124,7 @@ montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init)
uint64_t *nq1 = p01_tmp1_swap;
uint64_t *nq_p11 = p01_tmp1_swap + (uint32_t)10U;
uint64_t *swap = p01_tmp1_swap + (uint32_t)40U;
- cswap20((uint64_t)1U, nq1, nq_p11);
+ Hacl_Impl_Curve25519_Field51_cswap2((uint64_t)1U, nq1, nq_p11);
point_add_and_double(init, p01_tmp11, tmp2);
swap[0U] = (uint64_t)1U;
for (uint32_t i = (uint32_t)0U; i < (uint32_t)251U; i++) {
@@ -761,26 +136,26 @@ montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init)
bit =
(uint64_t)(key[((uint32_t)253U - i) / (uint32_t)8U] >> ((uint32_t)253U - i) % (uint32_t)8U & (uint8_t)1U);
uint64_t sw = swap1[0U] ^ bit;
- cswap20(sw, nq2, nq_p12);
+ Hacl_Impl_Curve25519_Field51_cswap2(sw, nq2, nq_p12);
point_add_and_double(init, p01_tmp12, tmp2);
swap1[0U] = bit;
}
uint64_t sw = swap[0U];
- cswap20(sw, nq1, nq_p11);
+ Hacl_Impl_Curve25519_Field51_cswap2(sw, nq1, nq_p11);
uint64_t *nq10 = p01_tmp1;
uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U;
point_double(nq10, tmp1, tmp2);
point_double(nq10, tmp1, tmp2);
point_double(nq10, tmp1, tmp2);
- memcpy(out, p0, (uint32_t)10U * sizeof(p0[0U]));
+ memcpy(out, p0, (uint32_t)10U * sizeof(uint64_t));
}
static void
fsquare_times(uint64_t *o, uint64_t *inp, FStar_UInt128_uint128 *tmp, uint32_t n)
{
- fsqr0(o, inp);
+ Hacl_Impl_Curve25519_Field51_fsqr(o, inp, tmp);
for (uint32_t i = (uint32_t)0U; i < n - (uint32_t)1U; i++) {
- fsqr0(o, o);
+ Hacl_Impl_Curve25519_Field51_fsqr(o, o, tmp);
}
}
@@ -788,35 +163,42 @@ static void
finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp)
{
uint64_t t1[20U] = { 0U };
- uint64_t *a = t1;
- uint64_t *b = t1 + (uint32_t)5U;
- uint64_t *c = t1 + (uint32_t)10U;
- uint64_t *t00 = t1 + (uint32_t)15U;
+ uint64_t *a1 = t1;
+ uint64_t *b1 = t1 + (uint32_t)5U;
+ uint64_t *t010 = t1 + (uint32_t)15U;
+ FStar_UInt128_uint128 *tmp10 = tmp;
+ fsquare_times(a1, i, tmp10, (uint32_t)1U);
+ fsquare_times(t010, a1, tmp10, (uint32_t)2U);
+ Hacl_Impl_Curve25519_Field51_fmul(b1, t010, i, tmp);
+ Hacl_Impl_Curve25519_Field51_fmul(a1, b1, a1, tmp);
+ fsquare_times(t010, a1, tmp10, (uint32_t)1U);
+ Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp);
+ fsquare_times(t010, b1, tmp10, (uint32_t)5U);
+ Hacl_Impl_Curve25519_Field51_fmul(b1, t010, b1, tmp);
+ uint64_t *b10 = t1 + (uint32_t)5U;
+ uint64_t *c10 = t1 + (uint32_t)10U;
+ uint64_t *t011 = t1 + (uint32_t)15U;
+ FStar_UInt128_uint128 *tmp11 = tmp;
+ fsquare_times(t011, b10, tmp11, (uint32_t)10U);
+ Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp);
+ fsquare_times(t011, c10, tmp11, (uint32_t)20U);
+ Hacl_Impl_Curve25519_Field51_fmul(t011, t011, c10, tmp);
+ fsquare_times(t011, t011, tmp11, (uint32_t)10U);
+ Hacl_Impl_Curve25519_Field51_fmul(b10, t011, b10, tmp);
+ fsquare_times(t011, b10, tmp11, (uint32_t)50U);
+ Hacl_Impl_Curve25519_Field51_fmul(c10, t011, b10, tmp);
+ uint64_t *b11 = t1 + (uint32_t)5U;
+ uint64_t *c1 = t1 + (uint32_t)10U;
+ uint64_t *t01 = t1 + (uint32_t)15U;
FStar_UInt128_uint128 *tmp1 = tmp;
- fsquare_times(a, i, tmp1, (uint32_t)1U);
- fsquare_times(t00, a, tmp1, (uint32_t)2U);
- fmul0(b, t00, i);
- fmul0(a, b, a);
- fsquare_times(t00, a, tmp1, (uint32_t)1U);
- fmul0(b, t00, b);
- fsquare_times(t00, b, tmp1, (uint32_t)5U);
- fmul0(b, t00, b);
- fsquare_times(t00, b, tmp1, (uint32_t)10U);
- fmul0(c, t00, b);
- fsquare_times(t00, c, tmp1, (uint32_t)20U);
- fmul0(t00, t00, c);
- fsquare_times(t00, t00, tmp1, (uint32_t)10U);
- fmul0(b, t00, b);
- fsquare_times(t00, b, tmp1, (uint32_t)50U);
- fmul0(c, t00, b);
- fsquare_times(t00, c, tmp1, (uint32_t)100U);
- fmul0(t00, t00, c);
- fsquare_times(t00, t00, tmp1, (uint32_t)50U);
- fmul0(t00, t00, b);
- fsquare_times(t00, t00, tmp1, (uint32_t)5U);
- uint64_t *a0 = t1;
+ fsquare_times(t01, c1, tmp1, (uint32_t)100U);
+ Hacl_Impl_Curve25519_Field51_fmul(t01, t01, c1, tmp);
+ fsquare_times(t01, t01, tmp1, (uint32_t)50U);
+ Hacl_Impl_Curve25519_Field51_fmul(t01, t01, b11, tmp);
+ fsquare_times(t01, t01, tmp1, (uint32_t)5U);
+ uint64_t *a = t1;
uint64_t *t0 = t1 + (uint32_t)15U;
- fmul0(o, t0, a0);
+ Hacl_Impl_Curve25519_Field51_fmul(o, t0, a, tmp);
}
static void
@@ -830,8 +212,8 @@ encode_point(uint8_t *o, uint64_t *i)
for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
tmp_w[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
finv(tmp, z, tmp_w);
- fmul0(tmp, tmp, x);
- store_felem(u64s, tmp);
+ Hacl_Impl_Curve25519_Field51_fmul(tmp, tmp, x, tmp_w);
+ Hacl_Impl_Curve25519_Field51_store_felem(u64s, tmp);
for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) {
store64_le(o + i0 * (uint32_t)8U, u64s[i0]);
}
diff --git a/lib/freebl/verified/Hacl_Curve25519_51.h b/lib/freebl/verified/Hacl_Curve25519_51.h
index 05050739c..dade9637b 100644
--- a/lib/freebl/verified/Hacl_Curve25519_51.h
+++ b/lib/freebl/verified/Hacl_Curve25519_51.h
@@ -21,15 +21,20 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Curve25519_51_H
+#define __Hacl_Curve25519_51_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Curve25519_51_H
-#define __Hacl_Curve25519_51_H
-
#include "Hacl_Kremlib.h"
+#include "Hacl_Bignum25519_51.h"
void Hacl_Curve25519_51_scalarmult(uint8_t *out, uint8_t *priv, uint8_t *pub);
@@ -37,5 +42,9 @@ void Hacl_Curve25519_51_secret_to_public(uint8_t *pub, uint8_t *priv);
bool Hacl_Curve25519_51_ecdh(uint8_t *out, uint8_t *priv, uint8_t *pub);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Curve25519_51_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Kremlib.h b/lib/freebl/verified/Hacl_Kremlib.h
index a2116220f..1b47ca3b1 100644
--- a/lib/freebl/verified/Hacl_Kremlib.h
+++ b/lib/freebl/verified/Hacl_Kremlib.h
@@ -21,13 +21,21 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Kremlib_H
+#define __Hacl_Kremlib_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Kremlib_H
-#define __Hacl_Kremlib_H
+static inline uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b);
+
+static inline uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b);
static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
@@ -47,5 +55,9 @@ static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a);
static inline FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Kremlib_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Poly1305_128.c b/lib/freebl/verified/Hacl_Poly1305_128.c
index 7fbd7fc4b..963068d42 100644
--- a/lib/freebl/verified/Hacl_Poly1305_128.c
+++ b/lib/freebl/verified/Hacl_Poly1305_128.c
@@ -29,9 +29,9 @@ Hacl_Impl_Poly1305_Field32xN_128_load_acc2(Lib_IntVector_Intrinsics_vec128 *acc,
Lib_IntVector_Intrinsics_vec128 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec128_zero;
- Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load_le(b);
+ Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(b);
Lib_IntVector_Intrinsics_vec128
- b2 = Lib_IntVector_Intrinsics_vec128_load_le(b + (uint32_t)16U);
+ b2 = Lib_IntVector_Intrinsics_vec128_load64_le(b + (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2);
Lib_IntVector_Intrinsics_vec128 hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2);
Lib_IntVector_Intrinsics_vec128
@@ -803,9 +803,9 @@ Hacl_Poly1305_128_poly1305_update(
Lib_IntVector_Intrinsics_vec128 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec128_zero;
- Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load_le(block);
+ Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(block);
Lib_IntVector_Intrinsics_vec128
- b2 = Lib_IntVector_Intrinsics_vec128_load_le(block + (uint32_t)16U);
+ b2 = Lib_IntVector_Intrinsics_vec128_load64_le(block + (uint32_t)16U);
Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2);
Lib_IntVector_Intrinsics_vec128
hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2);
@@ -1236,7 +1236,7 @@ Hacl_Poly1305_128_poly1305_update(
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec128_zero;
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem * sizeof(last[0U]));
+ memcpy(tmp, last, rem * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
diff --git a/lib/freebl/verified/Hacl_Poly1305_128.h b/lib/freebl/verified/Hacl_Poly1305_128.h
index 8e7cdc74d..49171ddcc 100644
--- a/lib/freebl/verified/Hacl_Poly1305_128.h
+++ b/lib/freebl/verified/Hacl_Poly1305_128.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Poly1305_128_H
+#define __Hacl_Poly1305_128_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Poly1305_128_H
-#define __Hacl_Poly1305_128_H
-
#include "Hacl_Kremlib.h"
void
@@ -62,5 +66,9 @@ Hacl_Poly1305_128_poly1305_finish(
void Hacl_Poly1305_128_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Poly1305_128_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Poly1305_256.c b/lib/freebl/verified/Hacl_Poly1305_256.c
index 6fddf86af..6f5bffd97 100644
--- a/lib/freebl/verified/Hacl_Poly1305_256.c
+++ b/lib/freebl/verified/Hacl_Poly1305_256.c
@@ -29,9 +29,9 @@ Hacl_Impl_Poly1305_Field32xN_256_load_acc4(Lib_IntVector_Intrinsics_vec256 *acc,
Lib_IntVector_Intrinsics_vec256 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec256_zero;
- Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load_le(b);
+ Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(b);
Lib_IntVector_Intrinsics_vec256
- hi = Lib_IntVector_Intrinsics_vec256_load_le(b + (uint32_t)32U);
+ hi = Lib_IntVector_Intrinsics_vec256_load64_le(b + (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256
mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU);
Lib_IntVector_Intrinsics_vec256 m0 = Lib_IntVector_Intrinsics_vec256_interleave_low128(lo, hi);
@@ -1272,9 +1272,9 @@ Hacl_Poly1305_256_poly1305_update(
Lib_IntVector_Intrinsics_vec256 e[5U];
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec256_zero;
- Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load_le(block);
+ Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(block);
Lib_IntVector_Intrinsics_vec256
- hi = Lib_IntVector_Intrinsics_vec256_load_le(block + (uint32_t)32U);
+ hi = Lib_IntVector_Intrinsics_vec256_load64_le(block + (uint32_t)32U);
Lib_IntVector_Intrinsics_vec256
mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU);
Lib_IntVector_Intrinsics_vec256
@@ -1707,7 +1707,7 @@ Hacl_Poly1305_256_poly1305_update(
for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
e[_i] = Lib_IntVector_Intrinsics_vec256_zero;
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem * sizeof(last[0U]));
+ memcpy(tmp, last, rem * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
diff --git a/lib/freebl/verified/Hacl_Poly1305_256.h b/lib/freebl/verified/Hacl_Poly1305_256.h
index 9d5ff5728..62a2ca002 100644
--- a/lib/freebl/verified/Hacl_Poly1305_256.h
+++ b/lib/freebl/verified/Hacl_Poly1305_256.h
@@ -21,15 +21,19 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Poly1305_256_H
+#define __Hacl_Poly1305_256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "libintvector.h"
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Poly1305_256_H
-#define __Hacl_Poly1305_256_H
-
#include "Hacl_Kremlib.h"
void
@@ -62,5 +66,9 @@ Hacl_Poly1305_256_poly1305_finish(
void Hacl_Poly1305_256_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Poly1305_256_H_DEFINED
#endif
diff --git a/lib/freebl/verified/Hacl_Poly1305_32.c b/lib/freebl/verified/Hacl_Poly1305_32.c
index b5b118333..25ee87c1f 100644
--- a/lib/freebl/verified/Hacl_Poly1305_32.c
+++ b/lib/freebl/verified/Hacl_Poly1305_32.c
@@ -340,7 +340,7 @@ Hacl_Poly1305_32_poly1305_update(uint64_t *ctx, uint32_t len, uint8_t *text)
uint8_t *last = text + nb * (uint32_t)16U;
uint64_t e[5U] = { 0U };
uint8_t tmp[16U] = { 0U };
- memcpy(tmp, last, rem * sizeof(last[0U]));
+ memcpy(tmp, last, rem * sizeof(uint8_t));
uint64_t u0 = load64_le(tmp);
uint64_t lo = u0;
uint64_t u = load64_le(tmp + (uint32_t)8U);
diff --git a/lib/freebl/verified/Hacl_Poly1305_32.h b/lib/freebl/verified/Hacl_Poly1305_32.h
index 442b5db42..c552d6f42 100644
--- a/lib/freebl/verified/Hacl_Poly1305_32.h
+++ b/lib/freebl/verified/Hacl_Poly1305_32.h
@@ -21,14 +21,18 @@
* SOFTWARE.
*/
+#ifndef __Hacl_Poly1305_32_H
+#define __Hacl_Poly1305_32_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include <stdbool.h>
-#ifndef __Hacl_Poly1305_32_H
-#define __Hacl_Poly1305_32_H
-
#include "Hacl_Kremlib.h"
extern uint32_t Hacl_Poly1305_32_blocklen;
@@ -45,5 +49,9 @@ void Hacl_Poly1305_32_poly1305_finish(uint8_t *tag, uint8_t *key, uint64_t *ctx)
void Hacl_Poly1305_32_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key);
+#if defined(__cplusplus)
+}
+#endif
+
#define __Hacl_Poly1305_32_H_DEFINED
#endif
diff --git a/lib/freebl/verified/kremlin/include/kremlin/internal/target.h b/lib/freebl/verified/kremlin/include/kremlin/internal/target.h
index 25f0fd0ac..0affdaa80 100644
--- a/lib/freebl/verified/kremlin/include/kremlin/internal/target.h
+++ b/lib/freebl/verified/kremlin/include/kremlin/internal/target.h
@@ -26,6 +26,8 @@
(defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
(!(defined KRML_HOST_EPRINTF)))
#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
+#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#endif
#ifndef KRML_HOST_EXIT
diff --git a/lib/freebl/verified/kremlin/include/kremlin/internal/types.h b/lib/freebl/verified/kremlin/include/kremlin/internal/types.h
index 4654b8c01..2c966cb54 100644
--- a/lib/freebl/verified/kremlin/include/kremlin/internal/types.h
+++ b/lib/freebl/verified/kremlin/include/kremlin/internal/types.h
@@ -54,14 +54,14 @@ typedef const char *Prims_string;
/* This code makes a number of assumptions and should be refined. In particular,
* it assumes that: any non-MSVC amd64 compiler supports int128. Maybe it would
* be easier to just test for defined(__SIZEOF_INT128__) only? */
-#if (defined(__x86_64__) || \
- defined(__x86_64) || \
- defined(__aarch64__) || \
- (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \
- defined(__s390x__) || \
- (defined(_MSC_VER) && !defined(_M_X64) && defined(__clang__)) || \
- (defined(__mips__) && defined(__LP64__)) || \
- (defined(__riscv) && __riscv_xlen == 64) || \
+#if (defined(__x86_64__) || \
+ defined(__x86_64) || \
+ defined(__aarch64__) || \
+ (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \
+ defined(__s390x__) || \
+ (defined(_MSC_VER) && defined(_M_X64) && defined(__clang__)) || \
+ (defined(__mips__) && defined(__LP64__)) || \
+ (defined(__riscv) && __riscv_xlen == 64) || \
defined(__SIZEOF_INT128__))
#define HAS_INT128 1
#endif
@@ -87,6 +87,12 @@ typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t;
#include "kremlin/lowstar_endianness.h"
+#endif
+
+/* Avoid a circular loop: if this header is included via FStar_UInt8_16_32_64,
+ * then don't bring the uint128 definitions into scope. */
+#ifndef __FStar_UInt_8_16_32_64_H
+
#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
#include "fstar_uint128_msvc.h"
#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128.h
index 6f254639f..57b9b7156 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128.h
@@ -3,6 +3,8 @@
Licensed under the Apache 2.0 License.
*/
+#ifndef __FStar_UInt128_H
+#define __FStar_UInt128_H
#include <inttypes.h>
#include <stdbool.h>
#include "kremlin/internal/compat.h"
@@ -10,9 +12,6 @@
#include "kremlin/internal/types.h"
#include "kremlin/internal/target.h"
-#ifndef __FStar_UInt128_H
-#define __FStar_UInt128_H
-
static inline FStar_UInt128_uint128
FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128_Verified.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128_Verified.h
index a7da435c3..a5de03751 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128_Verified.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt128_Verified.h
@@ -3,14 +3,13 @@
Licensed under the Apache 2.0 License.
*/
+#ifndef __FStar_UInt128_Verified_H
+#define __FStar_UInt128_Verified_H
#include <inttypes.h>
#include <stdbool.h>
#include "kremlin/internal/types.h"
#include "kremlin/internal/target.h"
-#ifndef __FStar_UInt128_Verified_H
-#define __FStar_UInt128_Verified_H
-
#include "FStar_UInt_8_16_32_64.h"
static inline uint64_t
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h
index 809ea58ac..08884599c 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h
@@ -3,6 +3,8 @@
Licensed under the Apache 2.0 License.
*/
+#ifndef __FStar_UInt_8_16_32_64_H
+#define __FStar_UInt_8_16_32_64_H
#include <inttypes.h>
#include <stdbool.h>
#include "kremlin/internal/compat.h"
@@ -10,9 +12,6 @@
#include "kremlin/internal/types.h"
#include "kremlin/internal/target.h"
-#ifndef __FStar_UInt_8_16_32_64_H
-#define __FStar_UInt_8_16_32_64_H
-
extern Prims_int FStar_UInt64_n;
extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
@@ -51,13 +50,13 @@ FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
return x_xor_q_ - (uint64_t)1U;
}
-extern Prims_string FStar_UInt64_to_string(uint64_t uu____888);
+extern Prims_string FStar_UInt64_to_string(uint64_t uu___);
-extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu____899);
+extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___);
-extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu____910);
+extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___);
-extern uint64_t FStar_UInt64_of_string(Prims_string uu____921);
+extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
extern Prims_int FStar_UInt32_n;
@@ -97,13 +96,13 @@ FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
return x_xor_q_ - (uint32_t)1U;
}
-extern Prims_string FStar_UInt32_to_string(uint32_t uu____888);
+extern Prims_string FStar_UInt32_to_string(uint32_t uu___);
-extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu____899);
+extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___);
-extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu____910);
+extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___);
-extern uint32_t FStar_UInt32_of_string(Prims_string uu____921);
+extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
extern Prims_int FStar_UInt16_n;
@@ -143,13 +142,13 @@ FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
return x_xor_q_ - (uint16_t)1U;
}
-extern Prims_string FStar_UInt16_to_string(uint16_t uu____888);
+extern Prims_string FStar_UInt16_to_string(uint16_t uu___);
-extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu____899);
+extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___);
-extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu____910);
+extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___);
-extern uint16_t FStar_UInt16_of_string(Prims_string uu____921);
+extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
extern Prims_int FStar_UInt8_n;
@@ -189,13 +188,13 @@ FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
return x_xor_q_ - (uint8_t)1U;
}
-extern Prims_string FStar_UInt8_to_string(uint8_t uu____888);
+extern Prims_string FStar_UInt8_to_string(uint8_t uu___);
-extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu____899);
+extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___);
-extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu____910);
+extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___);
-extern uint8_t FStar_UInt8_of_string(Prims_string uu____921);
+extern uint8_t FStar_UInt8_of_string(Prims_string uu___);
typedef uint8_t FStar_UInt8_byte;
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/LowStar_Endianness.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/LowStar_Endianness.h
index a6bff78d9..6d86cd584 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/LowStar_Endianness.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/LowStar_Endianness.h
@@ -3,6 +3,8 @@
Licensed under the Apache 2.0 License.
*/
+#ifndef __LowStar_Endianness_H
+#define __LowStar_Endianness_H
#include <inttypes.h>
#include <stdbool.h>
#include "kremlin/internal/compat.h"
@@ -10,11 +12,6 @@
#include "kremlin/internal/types.h"
#include "kremlin/internal/target.h"
-#ifndef __LowStar_Endianness_H
-#define __LowStar_Endianness_H
-
-#include "FStar_UInt128.h"
-
static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
static inline FStar_UInt128_uint128 load128_le(uint8_t *x0);
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_gcc64.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_gcc64.h
index 5372de42a..441928def 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_gcc64.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_gcc64.h
@@ -20,6 +20,9 @@
* such, it assumes that the machine integers have been bundled the exact same
* way in both cases. */
+#ifndef FSTAR_UINT128_GCC64
+#define FSTAR_UINT128_GCC64
+
#include "FStar_UInt128.h"
#include "FStar_UInt_8_16_32_64.h"
#include "LowStar_Endianness.h"
@@ -218,3 +221,5 @@ FStar_UInt128_mul32(uint64_t x, uint32_t y)
{
return (uint128_t)x * (uint128_t)y;
}
+
+#endif
diff --git a/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_msvc.h b/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_msvc.h
index fca0e2d96..73addd3a2 100644
--- a/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_msvc.h
+++ b/lib/freebl/verified/kremlin/kremlib/dist/minimal/fstar_uint128_msvc.h
@@ -7,6 +7,10 @@
* F* version: 15104ff8
* KreMLin version: 318b7fa8
*/
+
+#ifndef FSTAR_UINT128_MSVC
+#define FSTAR_UINT128_MSVC
+
#include "kremlin/internal/types.h"
#include "FStar_UInt128.h"
#include "FStar_UInt_8_16_32_64.h"
@@ -526,3 +530,8 @@ FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
return FStar_UInt128_mul_wide_impl(x, y);
#endif
}
+
+#undef low
+#undef high
+
+#endif
diff --git a/lib/freebl/verified/libintvector.h b/lib/freebl/verified/libintvector.h
index 24a221786..e43be92b9 100644
--- a/lib/freebl/verified/libintvector.h
+++ b/lib/freebl/verified/libintvector.h
@@ -3,6 +3,23 @@
#include <sys/types.h>
+// # DEBUGGING FLAGS
+// =================
+// It is possible to debug the trace of the primitives defined in
+// this file by using the [DEBUG_VECTOR_TRACE] C flag.
+// As we use the same vector types to manipulate blocks of uint32 and blocks
+// of uint64, the log results will vary with the endianess, in particular for
+// some generic operations like [and] or [xor]. By default, the printing is
+// performed as if we were manipulating blocks of uint32. If you want to
+// switch to blocks of uint64, use the flag: [DEBUG_VECTOR_TRACE_ELEMENTS_64].
+// Note that if those flags are activated, it may be necessary to tweak a bit
+// the compilation options to build HACL. More specifically, you may need to
+// always activate the compiler options to use vector support (even for files
+// which actually don't make use of vectors, if they have libintvector.h as
+// a dependency). When comparing traces, note that some instructions are not
+// compiled in the same order on the different platforms, but it doesn't lead
+// to a lot of discrepancies in practice.
+
#define Lib_IntVector_Intrinsics_bit_mask64(x) -((x)&1)
#if defined(__x86_64__) || defined(_M_X64)
@@ -96,10 +113,16 @@ typedef __m128i Lib_IntVector_Intrinsics_vec128;
#define Lib_IntVector_Intrinsics_vec128_rotate_right_lanes64(x0, x1) \
(_mm_shuffle_epi32(x0, _MM_SHUFFLE((2 * x1 + 3) % 4, (2 * x1 + 2) % 4, (2 * x1 + 1) % 4, (2 * x1) % 4)))
-#define Lib_IntVector_Intrinsics_vec128_load_le(x0) \
+#define Lib_IntVector_Intrinsics_vec128_load32_le(x0) \
+ (_mm_loadu_si128((__m128i*)(x0)))
+
+#define Lib_IntVector_Intrinsics_vec128_load64_le(x0) \
(_mm_loadu_si128((__m128i*)(x0)))
-#define Lib_IntVector_Intrinsics_vec128_store_le(x0, x1) \
+#define Lib_IntVector_Intrinsics_vec128_store32_le(x0, x1) \
+ (_mm_storeu_si128((__m128i*)(x0), x1))
+
+#define Lib_IntVector_Intrinsics_vec128_store64_le(x0, x1) \
(_mm_storeu_si128((__m128i*)(x0), x1))
#define Lib_IntVector_Intrinsics_vec128_load_be(x0) \
@@ -295,7 +318,10 @@ typedef __m256i Lib_IntVector_Intrinsics_vec256;
#define Lib_IntVector_Intrinsics_vec256_rotate_right_lanes64(x0, x1) \
(_mm256_permute4x64_epi64(x0, _MM_SHUFFLE((x1 + 3) % 4, (x1 + 2) % 4, (x1 + 1) % 4, x1 % 4)))
-#define Lib_IntVector_Intrinsics_vec256_load_le(x0) \
+#define Lib_IntVector_Intrinsics_vec256_load32_le(x0) \
+ (_mm256_loadu_si256((__m256i*)(x0)))
+
+#define Lib_IntVector_Intrinsics_vec256_load64_le(x0) \
(_mm256_loadu_si256((__m256i*)(x0)))
#define Lib_IntVector_Intrinsics_vec256_load32_be(x0) \
@@ -304,7 +330,10 @@ typedef __m256i Lib_IntVector_Intrinsics_vec256;
#define Lib_IntVector_Intrinsics_vec256_load64_be(x0) \
(_mm256_shuffle_epi8(_mm256_loadu_si256((__m256i*)(x0)), _mm256_set_epi8(8, 9, 10, 11, 12, 13, 14, 15, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 0, 1, 2, 3, 4, 5, 6, 7)))
-#define Lib_IntVector_Intrinsics_vec256_store_le(x0, x1) \
+#define Lib_IntVector_Intrinsics_vec256_store32_le(x0, x1) \
+ (_mm256_storeu_si256((__m256i*)(x0), x1))
+
+#define Lib_IntVector_Intrinsics_vec256_store64_le(x0, x1) \
(_mm256_storeu_si256((__m256i*)(x0), x1))
#define Lib_IntVector_Intrinsics_vec256_store32_be(x0, x1) \
@@ -394,7 +423,7 @@ typedef __m256i Lib_IntVector_Intrinsics_vec256;
#define Lib_IntVector_Intrinsics_vec256_interleave_high128(x1, x2) \
(_mm256_permute2x128_si256(x1, x2, 0x31))
-#elif defined(__aarch64__) || defined(_M_ARM64) || defined(__arm__) || defined(_M_ARM)
+#elif (defined(__aarch64__) || defined(_M_ARM64) || defined(__arm__) || defined(_M_ARM)) && !defined(__ARM_32BIT_STATE)
#include <arm_neon.h>
typedef uint32x4_t Lib_IntVector_Intrinsics_vec128;
@@ -473,10 +502,16 @@ typedef uint32x4_t Lib_IntVector_Intrinsics_vec128;
(_mm_shuffle_epi32(x0, _MM_SHUFFLE(2*x1+1,2*x1,2*x2+1,2*x2)))
*/
-#define Lib_IntVector_Intrinsics_vec128_load_le(x0) \
+#define Lib_IntVector_Intrinsics_vec128_load32_le(x0) \
+ (vld1q_u32((const uint32_t*)(x0)))
+
+#define Lib_IntVector_Intrinsics_vec128_load64_le(x0) \
(vld1q_u32((const uint32_t*)(x0)))
-#define Lib_IntVector_Intrinsics_vec128_store_le(x0, x1) \
+#define Lib_IntVector_Intrinsics_vec128_store32_le(x0, x1) \
+ (vst1q_u32((uint32_t*)(x0), (x1)))
+
+#define Lib_IntVector_Intrinsics_vec128_store64_le(x0, x1) \
(vst1q_u32((uint32_t*)(x0), (x1)))
/*
@@ -582,5 +617,155 @@ Lib_IntVector_Intrinsics_vec128_load32s(uint32_t x1, uint32_t x2, uint32_t x3, u
#define Lib_IntVector_Intrinsics_vec128_interleave_high64(x1, x2) \
(vreinterpretq_u32_u64(vzip2q_u64(vreinterpretq_u64_u32(x1), vreinterpretq_u64_u32(x2))))
-#endif
+// IBM z architecture
+#elif defined(__s390x__) // this flag is for GCC only
+
+#include <vecintrin.h>
+
+// The main vector 128 type
+// We can't use uint8_t, uint32_t, uint64_t... instead of unsigned char,
+// unsigned int, unsigned long long: the compiler complains that the parameter
+// combination is invalid.
+typedef unsigned char vector128_8 __attribute__((vector_size(16)));
+typedef unsigned int vector128_32 __attribute__((vector_size(16)));
+typedef unsigned long long vector128_64 __attribute__((vector_size(16)));
+
+typedef vector128_8 Lib_IntVector_Intrinsics_vec128;
+typedef vector128_8 vector128;
+
+// Small helper to change the endianess of the vector's elements, seen as uint32.
+// Note that we can't use vec_revb.
+#define Lib_IntVector_Intrinsics_vec128_load_store_switch_endian32(x0) \
+ ((vector128)(vec_perm((vector128_8)(x0), (vector128_8){}, \
+ (vector128_8){ 3, 2, 1, 0, 7, 6, 5, 4, 11, 10, 9, 8, 15, 14, 13, 12 })))
+
+// Small helper to change the endianess of the vector's elements, seen as uint64
+// Note that we can't use vec_revb.
+#define Lib_IntVector_Intrinsics_vec128_load_store_switch_endian64(x0) \
+ ((vector128)(vec_perm((vector128_8)(x0), (vector128_8){}, \
+ (vector128_8){ 7, 6, 5, 4, 3, 2, 1, 0, 15, 14, 13, 12, 11, 10, 9, 8 })))
+
+#define Lib_IntVector_Intrinsics_vec128_load32_le(x) \
+ ((vector128)Lib_IntVector_Intrinsics_vec128_load_store_switch_endian32( \
+ ((vector128_8)vec_load_len((const uint8_t*)(x), 16))))
+
+#define Lib_IntVector_Intrinsics_vec128_load64_le(x) \
+ ((vector128)Lib_IntVector_Intrinsics_vec128_load_store_switch_endian64( \
+ ((vector128_8)vec_load_len((const uint8_t*)(x), 16))))
+
+#define Lib_IntVector_Intrinsics_vec128_store32_le(x0, x1) \
+ (vec_store_len(((vector128_8)Lib_IntVector_Intrinsics_vec128_load_store_switch_endian32(x1)), \
+ ((uint8_t*)(x0)), (uint32_t)16))
+
+#define Lib_IntVector_Intrinsics_vec128_store64_le(x0, x1) \
+ (vec_store_len(((vector128_8)Lib_IntVector_Intrinsics_vec128_load_store_switch_endian64(x1)), \
+ ((uint8_t*)(x0)), (uint32_t)16))
+
+#define Lib_IntVector_Intrinsics_vec128_add32(x0, x1) \
+ ((vector128)((vector128_32)(((vector128_32)(x0)) + ((vector128_32)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_add64(x0, x1) \
+ ((vector128)((vector128_64)(((vector128_64)(x0)) + ((vector128_64)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_and(x0, x1) \
+ ((vector128)(vec_and((vector128)(x0), (vector128)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_eq32(x0, x1) \
+ ((vector128)(vec_cmpeq(((vector128_32)(x0)), ((vector128_32)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_eq64(x0, x1) \
+ ((vector128)(vec_cmpeq(((vector128_64)(x0)), ((vector128_64)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_extract32(x0, x1) \
+ ((unsigned int)(vec_extract((vector128_32)(x0), x1)))
+
+#define Lib_IntVector_Intrinsics_vec128_extract64(x0, x1) \
+ ((unsigned long long)(vec_extract((vector128_64)(x0), x1)))
+
+#define Lib_IntVector_Intrinsics_vec128_gt32(x0, x1) \
+ ((vector128)((vector128_32)(((vector128_32)(x0)) > ((vector128_32)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_gt64(x0, x1) \
+ ((vector128)((vector128_64)(((vector128_64)(x0)) > ((vector128_64)(x1)))))
+
+#define Lib_IntVector_Intrinsics_vec128_insert32(x0, x1, x2) \
+ ((vector128)((vector128_32)vec_insert((unsigned int)(x1), (vector128_32)(x0), x2)))
+
+#define Lib_IntVector_Intrinsics_vec128_insert64(x0, x1, x2) \
+ ((vector128)((vector128_64)vec_insert((unsigned long long)(x1), (vector128_64)(x0), x2)))
+
+#define Lib_IntVector_Intrinsics_vec128_interleave_high32(x0, x1) \
+ ((vector128)((vector128_32)vec_mergel((vector128_32)(x0), (vector128_32)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_interleave_high64(x0, x1) \
+ ((vector128)((vector128_64)vec_mergel((vector128_64)(x0), (vector128_64)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_interleave_low32(x0, x1) \
+ ((vector128)((vector128_32)vec_mergeh((vector128_32)(x0), (vector128_32)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_interleave_low64(x0, x1) \
+ ((vector128)((vector128_64)vec_mergeh((vector128_64)(x0), (vector128_64)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_load32(x) \
+ ((vector128)((vector128_32){ (unsigned int)(x), (unsigned int)(x), \
+ (unsigned int)(x), (unsigned int)(x) }))
+
+#define Lib_IntVector_Intrinsics_vec128_load32s(x0, x1, x2, x3) \
+ ((vector128)((vector128_32){ (unsigned int)(x0), (unsigned int)(x1), (unsigned int)(x2), (unsigned int)(x3) }))
+
+#define Lib_IntVector_Intrinsics_vec128_load64(x) \
+ ((vector128)((vector128_64)vec_load_pair((unsigned long long)(x), (unsigned long long)(x))))
+
+#define Lib_IntVector_Intrinsics_vec128_lognot(x0) \
+ ((vector128)(vec_xor((vector128)(x0), (vector128)vec_splat_u32(-1))))
+
+// We need to permute the low and high components of the uint64
+// before calling vec_mule. The following helper does that.
+#define Lib_IntVector_Intrinsics_vec128_mul64_perm_low_high_(x0) \
+ ((vector128)(vec_perm((vector128_8)(x0), (vector128_8){}, \
+ (vector128_8){ 4, 5, 6, 7, 0, 1, 2, 3, 12, 13, 14, 15, 8, 9, 10, 11 })))
+
+#define Lib_IntVector_Intrinsics_vec128_mul64(x0, x1) \
+ ((vector128)(vec_mule((vector128_32)Lib_IntVector_Intrinsics_vec128_mul64_perm_low_high_(x0), \
+ (vector128_32)Lib_IntVector_Intrinsics_vec128_mul64_perm_low_high_(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_or(x0, x1) \
+ ((vector128)(vec_or((vector128)(x0), (vector128)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_rotate_left32(x0, x1) \
+ ((vector128)(vec_rli((vector128_32)(x0), (unsigned long)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_rotate_right32(x0, x1) \
+ (Lib_IntVector_Intrinsics_vec128_rotate_left32(x0, (uint32_t)(32 - (x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_rotate_right_lanes32(x0, x1) \
+ ((vector128)(vec_perm((vector128)(x0), (vector128){}, (vector128_8){ \
+ (x1 % 4) * 4 + 0, (x1 % 4) * 4 + 1, (x1 % 4) * 4 + 2, (x1 % 4) * 4 + 3, \
+ ((x1 + 1) % 4) * 4 + 0, ((x1 + 1) % 4) * 4 + 1, ((x1 + 1) % 4) * 4 + 2, ((x1 + 1) % 4) * 4 + 3, \
+ ((x1 + 2) % 4) * 4 + 0, ((x1 + 2) % 4) * 4 + 1, ((x1 + 2) % 4) * 4 + 2, ((x1 + 2) % 4) * 4 + 3, \
+ ((x1 + 3) % 4) * 4 + 0, ((x1 + 3) % 4) * 4 + 1, ((x1 + 3) % 4) * 4 + 2, ((x1 + 3) % 4) * 4 + 3 })))
+
+#define Lib_IntVector_Intrinsics_vec128_shift_left64(x0, x1) \
+ (((vector128)((vector128_64)vec_rli((vector128_64)(x0), (unsigned long)(x1)))) & \
+ ((vector128)((vector128_64){ 0xffffffffffffffff << (x1), 0xffffffffffffffff << (x1) })))
+
+#define Lib_IntVector_Intrinsics_vec128_shift_right64(x0, x1) \
+ (((vector128)((vector128_64)vec_rli((vector128_64)(x0), (unsigned long)(64 - (x1))))) & \
+ ((vector128)((vector128_64){ 0xffffffffffffffff >> (x1), 0xffffffffffffffff >> (x1) })))
+
+// Doesn't work with vec_splat_u64
+#define Lib_IntVector_Intrinsics_vec128_smul64(x0, x1) \
+ ((vector128)(Lib_IntVector_Intrinsics_vec128_mul64(x0, ((vector128_64){ (unsigned long long)(x1), (unsigned long long)(x1) }))))
+
+#define Lib_IntVector_Intrinsics_vec128_sub64(x0, x1) \
+ ((vector128)((vector128_64)(x0) - (vector128_64)(x1)))
+
+#define Lib_IntVector_Intrinsics_vec128_xor(x0, x1) \
+ ((vector128)(vec_xor((vector128)(x0), (vector128)(x1))))
+
+#define Lib_IntVector_Intrinsics_vec128_zero \
+ ((vector128){})
+
+#endif // IBM z architecture
+
#endif