[CI] update code

include/Hacl_Bignum256.h

@@ -129,7 +129,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1
 */
-bool Hacl_Bignum256_mod(uint64_t *n, uint64_t *a, uint64_t *res);
+bool Hacl_Bignum256_mod_op(uint64_t *n, uint64_t *a, uint64_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Bignum256_32.h

@@ -128,7 +128,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1
 */
-bool Hacl_Bignum256_32_mod(uint32_t *n, uint32_t *a, uint32_t *res);
+bool Hacl_Bignum256_32_mod_op(uint32_t *n, uint32_t *a, uint32_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Bignum32.h

@@ -122,7 +122,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1 
 */
-bool Hacl_Bignum32_mod(uint32_t len, uint32_t *n, uint32_t *a, uint32_t *res);
+bool Hacl_Bignum32_mod_op(uint32_t len, uint32_t *n, uint32_t *a, uint32_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Bignum4096.h

@@ -133,7 +133,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1 
 */
-bool Hacl_Bignum4096_mod(uint64_t *n, uint64_t *a, uint64_t *res);
+bool Hacl_Bignum4096_mod_op(uint64_t *n, uint64_t *a, uint64_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Bignum4096_32.h

@@ -132,7 +132,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1 
 */
-bool Hacl_Bignum4096_32_mod(uint32_t *n, uint32_t *a, uint32_t *res);
+bool Hacl_Bignum4096_32_mod_op(uint32_t *n, uint32_t *a, uint32_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Bignum64.h

@@ -123,7 +123,7 @@ Write `a mod n` in `res`.
    • 1 < n
    • n % 2 = 1 
 */
-bool Hacl_Bignum64_mod(uint32_t len, uint64_t *n, uint64_t *a, uint64_t *res);
+bool Hacl_Bignum64_mod_op(uint32_t len, uint64_t *n, uint64_t *a, uint64_t *res);
 
 /**
 Write `a ^ b mod n` in `res`.

include/Hacl_Ed25519.h

@@ -47,16 +47,16 @@ extern "C" {
 /**
 Compute the public key from the private key.
 
-  The outparam `public_key`  points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+  @param[out] public_key Points to 32 bytes of valid memory, i.e., `uint8_t[32]`. Must not overlap the memory location of `private_key`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 */
 void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
 
 /**
 Compute the expanded keys for an Ed25519 signature.
 
-  The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
-  The argument `private_key`   points to 32 bytes of valid memory, i.e., uint8_t[32].
+  @param[out] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`. Must not overlap the memory location of `private_key`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 
   If one needs to sign several messages under the same private key, it is more efficient
   to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -66,11 +66,10 @@ void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);
 /**
 Create an Ed25519 signature with the (precomputed) expanded keys.
 
-  The outparam `signature`     points to 64 bytes of valid memory, i.e., uint8_t[64].
-  The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
-  The argument `msg`    points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-
-  The argument `expanded_keys` is obtained through `expand_keys`.
+  @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `expanded_keys` nor `msg`.
+  @param[in] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`, containing the expanded keys obtained by invoking `expand_keys`.
+  @param[in] msg_len Length of `msg`.
+  @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
   If one needs to sign several messages under the same private key, it is more efficient
   to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -86,9 +85,10 @@ Hacl_Ed25519_sign_expanded(
 /**
 Create an Ed25519 signature.
 
-  The outparam `signature`   points to 64 bytes of valid memory, i.e., uint8_t[64].
-  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `msg`  points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `private_key` nor `msg`.
+  @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
+  @param[in] msg_len Length of `msg`.
+  @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
   The function first calls `expand_keys` and then invokes `sign_expanded`.
 
@@ -101,11 +101,12 @@ Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, ui
 /**
 Verify an Ed25519 signature.
 
-  The function returns `true` if the signature is valid and `false` otherwise.
+  @param public_key Points to 32 bytes of valid memory containing the public key, i.e., `uint8_t[32]`.
+  @param msg_len Length of `msg`.
+  @param msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
+  @param signature Points to 64 bytes of valid memory containing the signature, i.e., `uint8_t[64]`.
 
-  The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
-  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-  The argument `signature`  points to 64 bytes of valid memory, i.e., uint8_t[64].
+  @return Returns `true` if the signature is valid and `false` otherwise.
 */
 bool
 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature);

include/internal/Hacl_Bignum_Base.h

@@ -72,9 +72,9 @@ Hacl_Bignum_Convert_bn_from_bytes_be_uint64(uint32_t len, uint8_t *b, uint64_t *
   memcpy(tmp + tmpLen - len, b, len * sizeof (uint8_t));
   for (uint32_t i = 0U; i < bnLen; i++)
   {
-    uint64_t *os = res;
     uint64_t u = load64_be(tmp + (bnLen - i - 1U) * 8U);
     uint64_t x = u;
+    uint64_t *os = res;
     os[i] = x;
   }
 }
@@ -372,8 +372,8 @@ Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
   memset(res, 0U, (aLen + aLen) * sizeof (uint32_t));
   for (uint32_t i0 = 0U; i0 < aLen; i0++)
   {
-    uint32_t *ab = a;
     uint32_t a_j = a[i0];
+    uint32_t *ab = a;
     uint32_t *res_j = res + i0;
     uint32_t c = 0U;
     for (uint32_t i = 0U; i < i0 / 4U; i++)
@@ -400,7 +400,16 @@ Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
     uint32_t r = c;
     res[i0 + i0] = r;
   }
-  uint32_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, res, res);
+  KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
+  uint32_t a_copy0[aLen + aLen];
+  memset(a_copy0, 0U, (aLen + aLen) * sizeof (uint32_t));
+  KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
+  uint32_t b_copy0[aLen + aLen];
+  memset(b_copy0, 0U, (aLen + aLen) * sizeof (uint32_t));
+  memcpy(a_copy0, res, (aLen + aLen) * sizeof (uint32_t));
+  memcpy(b_copy0, res, (aLen + aLen) * sizeof (uint32_t));
+  uint32_t r = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, a_copy0, b_copy0, res);
+  uint32_t c0 = r;
   KRML_MAYBE_UNUSED_VAR(c0);
   KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
   uint32_t tmp[aLen + aLen];
@@ -413,7 +422,16 @@ Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
     tmp[2U * i] = lo;
     tmp[2U * i + 1U] = hi;
   }
-  uint32_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, tmp, res);
+  KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
+  uint32_t a_copy[aLen + aLen];
+  memset(a_copy, 0U, (aLen + aLen) * sizeof (uint32_t));
+  KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
+  uint32_t b_copy[aLen + aLen];
+  memset(b_copy, 0U, (aLen + aLen) * sizeof (uint32_t));
+  memcpy(a_copy, res, (aLen + aLen) * sizeof (uint32_t));
+  memcpy(b_copy, tmp, (aLen + aLen) * sizeof (uint32_t));
+  uint32_t r0 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, a_copy, b_copy, res);
+  uint32_t c1 = r0;
   KRML_MAYBE_UNUSED_VAR(c1);
 }
 
@@ -423,8 +441,8 @@ Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
   memset(res, 0U, (aLen + aLen) * sizeof (uint64_t));
   for (uint32_t i0 = 0U; i0 < aLen; i0++)
   {
-    uint64_t *ab = a;
     uint64_t a_j = a[i0];
+    uint64_t *ab = a;
     uint64_t *res_j = res + i0;
     uint64_t c = 0ULL;
     for (uint32_t i = 0U; i < i0 / 4U; i++)
@@ -451,7 +469,16 @@ Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
     uint64_t r = c;
     res[i0 + i0] = r;
   }
-  uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, res, res);
+  KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
+  uint64_t a_copy0[aLen + aLen];
+  memset(a_copy0, 0U, (aLen + aLen) * sizeof (uint64_t));
+  KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
+  uint64_t b_copy0[aLen + aLen];
+  memset(b_copy0, 0U, (aLen + aLen) * sizeof (uint64_t));
+  memcpy(a_copy0, res, (aLen + aLen) * sizeof (uint64_t));
+  memcpy(b_copy0, res, (aLen + aLen) * sizeof (uint64_t));
+  uint64_t r = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, a_copy0, b_copy0, res);
+  uint64_t c0 = r;
   KRML_MAYBE_UNUSED_VAR(c0);
   KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
   uint64_t tmp[aLen + aLen];
@@ -464,7 +491,16 @@ Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
     tmp[2U * i] = lo;
     tmp[2U * i + 1U] = hi;
   }
-  uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, tmp, res);
+  KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
+  uint64_t a_copy[aLen + aLen];
+  memset(a_copy, 0U, (aLen + aLen) * sizeof (uint64_t));
+  KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
+  uint64_t b_copy[aLen + aLen];
+  memset(b_copy, 0U, (aLen + aLen) * sizeof (uint64_t));
+  memcpy(a_copy, res, (aLen + aLen) * sizeof (uint64_t));
+  memcpy(b_copy, tmp, (aLen + aLen) * sizeof (uint64_t));
+  uint64_t r0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, a_copy, b_copy, res);
+  uint64_t c1 = r0;
   KRML_MAYBE_UNUSED_VAR(c1);
 }
 

include/internal/Hacl_Bignum_K256.h

@@ -104,11 +104,11 @@ static inline void Hacl_K256_Field_load_felem(uint64_t *f, uint8_t *b)
     0U,
     4U,
     1U,
-    uint64_t *os = tmp;
     uint8_t *bj = b + i * 8U;
     uint64_t u = load64_be(bj);
     uint64_t r = u;
     uint64_t x = r;
+    uint64_t *os = tmp;
     os[i] = x;);
   uint64_t s0 = tmp[3U];
   uint64_t s1 = tmp[2U];
@@ -589,7 +589,9 @@ static inline void Hacl_K256_Field_fnegate_conditional_vartime(uint64_t *f, bool
     f[2U] = f2;
     f[3U] = f3;
     f[4U] = f4;
-    Hacl_K256_Field_fnormalize(f, f);
+    uint64_t f_copy[5U] = { 0U };
+    memcpy(f_copy, f, 5U * sizeof (uint64_t));
+    Hacl_K256_Field_fnormalize(f, f_copy);
     return;
   }
 }
@@ -598,7 +600,9 @@ static inline void Hacl_Impl_K256_Finv_fsquare_times_in_place(uint64_t *out, uin
 {
   for (uint32_t i = 0U; i < b; i++)
   {
-    Hacl_K256_Field_fsqr(out, out);
+    uint64_t x_copy[5U] = { 0U };
+    memcpy(x_copy, out, 5U * sizeof (uint64_t));
+    Hacl_K256_Field_fsqr(out, x_copy);
   }
 }
 
@@ -607,7 +611,9 @@ static inline void Hacl_Impl_K256_Finv_fsquare_times(uint64_t *out, uint64_t *a,
   memcpy(out, a, 5U * sizeof (uint64_t));
   for (uint32_t i = 0U; i < b; i++)
   {
-    Hacl_K256_Field_fsqr(out, out);
+    uint64_t x_copy[5U] = { 0U };
+    memcpy(x_copy, out, 5U * sizeof (uint64_t));
+    Hacl_K256_Field_fsqr(out, x_copy);
   }
 }
 
@@ -618,49 +624,81 @@ static inline void Hacl_Impl_K256_Finv_fexp_223_23(uint64_t *out, uint64_t *x2,
   uint64_t x44[5U] = { 0U };
   uint64_t x88[5U] = { 0U };
   Hacl_Impl_K256_Finv_fsquare_times(x2, f, 1U);
-  Hacl_K256_Field_fmul(x2, x2, f);
+  uint64_t f1_copy[5U] = { 0U };
+  memcpy(f1_copy, x2, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(x2, f1_copy, f);
   Hacl_Impl_K256_Finv_fsquare_times(x3, x2, 1U);
-  Hacl_K256_Field_fmul(x3, x3, f);
+  uint64_t f1_copy0[5U] = { 0U };
+  memcpy(f1_copy0, x3, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(x3, f1_copy0, f);
   Hacl_Impl_K256_Finv_fsquare_times(out, x3, 3U);
-  Hacl_K256_Field_fmul(out, out, x3);
+  uint64_t f1_copy1[5U] = { 0U };
+  memcpy(f1_copy1, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy1, x3);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 3U);
-  Hacl_K256_Field_fmul(out, out, x3);
+  uint64_t f1_copy2[5U] = { 0U };
+  memcpy(f1_copy2, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy2, x3);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 2U);
-  Hacl_K256_Field_fmul(out, out, x2);
+  uint64_t f1_copy3[5U] = { 0U };
+  memcpy(f1_copy3, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy3, x2);
   Hacl_Impl_K256_Finv_fsquare_times(x22, out, 11U);
-  Hacl_K256_Field_fmul(x22, x22, out);
+  uint64_t f1_copy4[5U] = { 0U };
+  memcpy(f1_copy4, x22, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(x22, f1_copy4, out);
   Hacl_Impl_K256_Finv_fsquare_times(x44, x22, 22U);
-  Hacl_K256_Field_fmul(x44, x44, x22);
+  uint64_t f1_copy5[5U] = { 0U };
+  memcpy(f1_copy5, x44, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(x44, f1_copy5, x22);
   Hacl_Impl_K256_Finv_fsquare_times(x88, x44, 44U);
-  Hacl_K256_Field_fmul(x88, x88, x44);
+  uint64_t f1_copy6[5U] = { 0U };
+  memcpy(f1_copy6, x88, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(x88, f1_copy6, x44);
   Hacl_Impl_K256_Finv_fsquare_times(out, x88, 88U);
-  Hacl_K256_Field_fmul(out, out, x88);
+  uint64_t f1_copy7[5U] = { 0U };
+  memcpy(f1_copy7, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy7, x88);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 44U);
-  Hacl_K256_Field_fmul(out, out, x44);
+  uint64_t f1_copy8[5U] = { 0U };
+  memcpy(f1_copy8, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy8, x44);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 3U);
-  Hacl_K256_Field_fmul(out, out, x3);
+  uint64_t f1_copy9[5U] = { 0U };
+  memcpy(f1_copy9, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy9, x3);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 23U);
-  Hacl_K256_Field_fmul(out, out, x22);
+  uint64_t f1_copy10[5U] = { 0U };
+  memcpy(f1_copy10, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy10, x22);
 }
 
 static inline void Hacl_Impl_K256_Finv_finv(uint64_t *out, uint64_t *f)
 {
   uint64_t x2[5U] = { 0U };
   Hacl_Impl_K256_Finv_fexp_223_23(out, x2, f);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 5U);
-  Hacl_K256_Field_fmul(out, out, f);
+  uint64_t f1_copy[5U] = { 0U };
+  memcpy(f1_copy, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy, f);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 3U);
-  Hacl_K256_Field_fmul(out, out, x2);
+  uint64_t f1_copy0[5U] = { 0U };
+  memcpy(f1_copy0, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy0, x2);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 2U);
-  Hacl_K256_Field_fmul(out, out, f);
+  uint64_t f1_copy1[5U] = { 0U };
+  memcpy(f1_copy1, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy1, f);
 }
 
 static inline void Hacl_Impl_K256_Finv_fsqrt(uint64_t *out, uint64_t *f)
 {
   uint64_t x2[5U] = { 0U };
   Hacl_Impl_K256_Finv_fexp_223_23(out, x2, f);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 6U);
-  Hacl_K256_Field_fmul(out, out, x2);
+  uint64_t f1_copy[5U] = { 0U };
+  memcpy(f1_copy, out, 5U * sizeof (uint64_t));
+  Hacl_K256_Field_fmul(out, f1_copy, x2);
   Hacl_Impl_K256_Finv_fsquare_times_in_place(out, 2U);
 }
 

include/internal/Hacl_Frodo_KEM.h

@@ -182,9 +182,9 @@ Hacl_Impl_Matrix_matrix_from_lbytes(uint32_t n1, uint32_t n2, uint8_t *b, uint16
 {
   for (uint32_t i = 0U; i < n1 * n2; i++)
   {
-    uint16_t *os = res;
     uint16_t u = load16_le(b + 2U * i);
     uint16_t x = u;
+    uint16_t *os = res;
     os[i] = x;
   }
 }