diff options
Diffstat (limited to 'lib/freebl/verified/Hacl_Bignum25519_51.h')
| -rw-r--r-- | lib/freebl/verified/Hacl_Bignum25519_51.h | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/lib/freebl/verified/Hacl_Bignum25519_51.h b/lib/freebl/verified/Hacl_Bignum25519_51.h index 173f11188..d53e43c21 100644 --- a/lib/freebl/verified/Hacl_Bignum25519_51.h +++ b/lib/freebl/verified/Hacl_Bignum25519_51.h @@ -28,12 +28,12 @@ extern "C" { #endif -#include "kremlin/internal/types.h" -#include "kremlin/lowstar_endianness.h" #include <string.h> -#include <stdbool.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" -#include "Hacl_Kremlib.h" +#include "Hacl_Krmllib.h" static inline void Hacl_Impl_Curve25519_Field51_fadd(uint64_t *out, uint64_t *f1, uint64_t *f2) @@ -661,11 +661,13 @@ 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; - } + KRML_MAYBE_FOR10(i, + (uint32_t)0U, + (uint32_t)10U, + (uint32_t)1U, + uint64_t dummy = mask & (p1[i] ^ p2[i]); + p1[i] = p1[i] ^ dummy; + p2[i] = p2[i] ^ dummy;); } #if defined(__cplusplus) |