diff --git a/CMakeLists.txt b/CMakeLists.txt index 825b1192..dcdd2f68 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -93,12 +93,9 @@ if(NOT MSVC) # -pedantic # -Wconversion # -Wsign-conversion - # -Werror=gcc-compat $<$:-g> $<$:-Og> $<$:-O3> - # $<$:-g> - # $<$:-Wno-deprecated-declarations> ) endif() @@ -337,6 +334,9 @@ configure_file(config/Config.h.in config.h) # Now combine everything into the hacl library # # Dynamic library add_library(hacl SHARED ${SOURCES_std} ${VALE_OBJECTS}) +if(NOT MSVC) + target_compile_options(hacl PRIVATE -Wsign-conversion -Wconversion -Wall -Wextra -pedantic) +endif() if(TOOLCHAIN_CAN_COMPILE_VEC128 AND HACL_VEC128_O) add_dependencies(hacl hacl_vec128) diff --git a/include/Hacl_RSAPSS.h b/include/Hacl_RSAPSS.h index 8f4de949..90bd69ce 100644 --- a/include/Hacl_RSAPSS.h +++ b/include/Hacl_RSAPSS.h @@ -43,9 +43,9 @@ extern "C" { Sign a message `msg` and write the signature to `sgnt`. @param a Hash algorithm to use. Allowed values for `a` are ... - * Spec_Hash_Definitions_SHA2_256, - * Spec_Hash_Definitions_SHA2_384, and - * Spec_Hash_Definitions_SHA2_512. + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. @@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`. @@ -105,10 +108,10 @@ Load a public key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. -@return Returns an allocated public key. Note: caller must take care to `free()` the created key. +@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb); @@ -119,11 +122,11 @@ Load a secret key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. -@return Returns an allocated secret key. Note: caller must take care to `free()` the created key. +@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_skey( @@ -138,13 +141,16 @@ uint64_t /** Sign a message `msg` and write the signature to `sgnt`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param salt Pointer to `saltLen` bytes where the salt is read from. @param msgLen Length of message. @@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param sgntLen Length of signature. @param sgnt Pointer to `sgntLen` bytes where the signature is read from. diff --git a/include/internal/Hacl_Bignum25519_51.h b/include/internal/Hacl_Bignum25519_51.h index 9fe5e9fc..25a10503 100644 --- a/include/internal/Hacl_Bignum25519_51.h +++ b/include/internal/Hacl_Bignum25519_51.h @@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul( FStar_UInt128_uint128 *uu___ ) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2( FStar_UInt128_uint128 *uu___ ) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f static inline void Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f0 = f[0U]; uint64_t f1 = f[1U]; uint64_t f2 = f[2U]; @@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint static inline void Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f[0U]; uint64_t f11 = f[1U]; uint64_t f12 = f[2U]; diff --git a/include/msvc/Hacl_RSAPSS.h b/include/msvc/Hacl_RSAPSS.h index 8f4de949..90bd69ce 100644 --- a/include/msvc/Hacl_RSAPSS.h +++ b/include/msvc/Hacl_RSAPSS.h @@ -43,9 +43,9 @@ extern "C" { Sign a message `msg` and write the signature to `sgnt`. @param a Hash algorithm to use. Allowed values for `a` are ... - * Spec_Hash_Definitions_SHA2_256, - * Spec_Hash_Definitions_SHA2_384, and - * Spec_Hash_Definitions_SHA2_512. + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. @@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`. @@ -105,10 +108,10 @@ Load a public key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. -@return Returns an allocated public key. Note: caller must take care to `free()` the created key. +@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb); @@ -119,11 +122,11 @@ Load a secret key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. -@return Returns an allocated secret key. Note: caller must take care to `free()` the created key. +@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_skey( @@ -138,13 +141,16 @@ uint64_t /** Sign a message `msg` and write the signature to `sgnt`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param salt Pointer to `saltLen` bytes where the salt is read from. @param msgLen Length of message. @@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param sgntLen Length of signature. @param sgnt Pointer to `sgntLen` bytes where the signature is read from. diff --git a/include/msvc/internal/Hacl_Bignum25519_51.h b/include/msvc/internal/Hacl_Bignum25519_51.h index 9fe5e9fc..25a10503 100644 --- a/include/msvc/internal/Hacl_Bignum25519_51.h +++ b/include/msvc/internal/Hacl_Bignum25519_51.h @@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul( FStar_UInt128_uint128 *uu___ ) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2( FStar_UInt128_uint128 *uu___ ) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f static inline void Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f0 = f[0U]; uint64_t f1 = f[1U]; uint64_t f2 = f[2U]; @@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint static inline void Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f[0U]; uint64_t f11 = f[1U]; uint64_t f12 = f[2U]; diff --git a/info.txt b/info.txt index 1a29e888..af3dbf98 100644 --- a/info.txt +++ b/info.txt @@ -1,5 +1,5 @@ The code was generated with the following toolchain. -F* version: 155853a14336aa0713dba7db5408f4c8ab512a06 -KaRaMeL version: db63c1de17565be0ec4989f58532717a04e3ff40 -HACL* version: ad60c9d98c9ce8f6a4fa13090511fa4b3a2c137b +F* version: bc622701c668f6b4092760879372968265d4a4e1 +KaRaMeL version: 7cffd27cfefbd220e986e561e8d350f043609f76 +HACL* version: 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c Vale version: 0.3.19 diff --git a/karamel/include/krml/internal/target.h b/karamel/include/krml/internal/target.h index 634c20fc..4903d224 100644 --- a/karamel/include/krml/internal/target.h +++ b/karamel/include/krml/internal/target.h @@ -57,6 +57,14 @@ # define KRML_HOST_IGNORE(x) (void)(x) #endif +#ifndef KRML_MAYBE_UNUSED +# if defined(__GNUC__) +# define KRML_MAYBE_UNUSED __attribute__((unused)) +# else +# define KRML_MAYBE_UNUSED +# endif +#endif + #ifndef KRML_NOINLINE # if defined(_MSC_VER) # define KRML_NOINLINE __declspec(noinline) diff --git a/karamel/krmllib/dist/minimal/Makefile.basic b/karamel/krmllib/dist/minimal/Makefile.basic deleted file mode 100644 index d7a1fdfd..00000000 --- a/karamel/krmllib/dist/minimal/Makefile.basic +++ /dev/null @@ -1,56 +0,0 @@ -# A basic Makefile that KaRaMeL copies in the output directory; this is not -# guaranteed to work and will only work well for very simple projects. This -# Makefile uses: -# - the custom C files passed to your krml invocation -# - the custom C flags passed to your krml invocation -# - the -o option passed to your krml invocation - -include Makefile.include - -ifeq (,$(KRML_HOME)) - $(error please define KRML_HOME to point to the root of your KaRaMeL git checkout) -endif - -CFLAGS += -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal -CFLAGS += -Wall -Wextra -Werror -std=c11 -Wno-unused-variable \ - -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function \ - -Wno-unused-parameter -Wno-infinite-recursion \ - -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -ifeq ($(OS),Windows_NT) -CFLAGS += -D__USE_MINGW_ANSI_STDIO -else -CFLAGS += -fPIC -endif -CFLAGS += $(USER_CFLAGS) - -SOURCES += $(ALL_C_FILES) $(USER_C_FILES) -ifneq (,$(BLACKLIST)) - SOURCES := $(filter-out $(BLACKLIST),$(SOURCES)) -endif -OBJS += $(patsubst %.c,%.o,$(SOURCES)) - -all: $(USER_TARGET) - -$(USER_TARGET): $(OBJS) - -AR ?= ar - -%.a: - $(AR) cr $@ $^ - -%.exe: - $(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a - -%.so: - $(CC) $(CFLAGS) -shared -o $@ $^ - -%.d: %.c - @set -e; rm -f $@; \ - $(CC) -MM -MG $(CFLAGS) $< > $@.$$$$; \ - sed 's,\($(notdir $*)\)\.o[ :]*,$(dir $@)\1.o $@ : ,g' < $@.$$$$ > $@; \ - rm -f $@.$$$$ - -include $(patsubst %.c,%.d,$(SOURCES)) - -clean: - rm -rf *.o *.d $(USER_TARGET) diff --git a/karamel/krmllib/dist/minimal/Makefile.include b/karamel/krmllib/dist/minimal/Makefile.include deleted file mode 100644 index ad532171..00000000 --- a/karamel/krmllib/dist/minimal/Makefile.include +++ /dev/null @@ -1,5 +0,0 @@ -USER_TARGET=libkrmllib.a -USER_CFLAGS= -USER_C_FILES=fstar_uint128.c -ALL_C_FILES= -ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h diff --git a/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h b/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h index e40304b2..ae109004 100644 --- a/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h +++ b/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h @@ -110,7 +110,7 @@ inline static uint128_t FStar_UInt128_mul_wide(uint64_t x, uint64_t y) { inline static uint128_t FStar_UInt128_eq_mask(uint128_t x, uint128_t y) { uint64_t mask = FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) & - FStar_UInt64_eq_mask(x, y); + FStar_UInt64_eq_mask((uint64_t)x, (uint64_t)y); return ((uint128_t)mask) << 64 | mask; } @@ -118,7 +118,7 @@ inline static uint128_t FStar_UInt128_gte_mask(uint128_t x, uint128_t y) { uint64_t mask = (FStar_UInt64_gte_mask(x >> 64, y >> 64) & ~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) | - (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y)); + (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask((uint64_t)x, (uint64_t)y)); return ((uint128_t)mask) << 64 | mask; } diff --git a/karamel/krmllib/dist/minimal/libkrmllib.def b/karamel/krmllib/dist/minimal/libkrmllib.def deleted file mode 100644 index c4ab8e38..00000000 --- a/karamel/krmllib/dist/minimal/libkrmllib.def +++ /dev/null @@ -1,11 +0,0 @@ -LIBRARY libkrmllib - -EXPORTS - FStar_UInt64_eq_mask - FStar_UInt64_gte_mask - FStar_UInt32_eq_mask - FStar_UInt32_gte_mask - FStar_UInt16_eq_mask - FStar_UInt16_gte_mask - FStar_UInt8_eq_mask - FStar_UInt8_gte_mask diff --git a/ocaml/ctypes.depend b/ocaml/ctypes.depend index 86af86df..31393b5e 100644 --- a/ocaml/ctypes.depend +++ b/ocaml/ctypes.depend @@ -1,4 +1,4 @@ -CTYPES_DEPS=lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Spec_stubs.cmx lib/Hacl_Spec_bindings.cmx lib/Hacl_Hash_Blake2_stubs.cmx lib/Hacl_Hash_Blake2_bindings.cmx lib/Hacl_Hash_Blake2b_256_stubs.cmx lib/Hacl_Hash_Blake2b_256_bindings.cmx lib/Hacl_Hash_Blake2s_128_stubs.cmx lib/Hacl_Hash_Blake2s_128_bindings.cmx lib/Hacl_Hash_SHA3_stubs.cmx lib/Hacl_Hash_SHA3_bindings.cmx lib/Hacl_Hash_Base_stubs.cmx lib/Hacl_Hash_Base_bindings.cmx lib/Hacl_Hash_MD5_stubs.cmx lib/Hacl_Hash_MD5_bindings.cmx lib/Hacl_Hash_SHA1_stubs.cmx lib/Hacl_Hash_SHA1_bindings.cmx lib/Hacl_SHA2_Types_stubs.cmx lib/Hacl_SHA2_Types_bindings.cmx lib/Hacl_Hash_SHA2_stubs.cmx lib/Hacl_Hash_SHA2_bindings.cmx lib/EverCrypt_Error_stubs.cmx lib/EverCrypt_Error_bindings.cmx lib/EverCrypt_AutoConfig2_stubs.cmx lib/EverCrypt_AutoConfig2_bindings.cmx lib/EverCrypt_Hash_stubs.cmx lib/EverCrypt_Hash_bindings.cmx lib/Hacl_Chacha20_stubs.cmx lib/Hacl_Chacha20_bindings.cmx lib/Hacl_Salsa20_stubs.cmx lib/Hacl_Salsa20_bindings.cmx lib/Hacl_Bignum_Base_stubs.cmx lib/Hacl_Bignum_Base_bindings.cmx lib/Hacl_Bignum_stubs.cmx lib/Hacl_Bignum_bindings.cmx lib/Hacl_Curve25519_64_stubs.cmx lib/Hacl_Curve25519_64_bindings.cmx lib/Hacl_Bignum25519_51_stubs.cmx lib/Hacl_Bignum25519_51_bindings.cmx lib/Hacl_Curve25519_51_stubs.cmx lib/Hacl_Curve25519_51_bindings.cmx lib/Hacl_Ed25519_stubs.cmx lib/Hacl_Ed25519_bindings.cmx lib/Hacl_Poly1305_32_stubs.cmx lib/Hacl_Poly1305_32_bindings.cmx lib/Hacl_Poly1305_128_stubs.cmx lib/Hacl_Poly1305_128_bindings.cmx lib/Hacl_Poly1305_256_stubs.cmx lib/Hacl_Poly1305_256_bindings.cmx lib/Hacl_NaCl_stubs.cmx lib/Hacl_NaCl_bindings.cmx lib/Hacl_P256_stubs.cmx lib/Hacl_P256_bindings.cmx lib/Hacl_Bignum_K256_stubs.cmx lib/Hacl_Bignum_K256_bindings.cmx lib/Hacl_K256_ECDSA_stubs.cmx lib/Hacl_K256_ECDSA_bindings.cmx lib/Hacl_Frodo_KEM_stubs.cmx lib/Hacl_Frodo_KEM_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_IntTypes_Intrinsics_stubs.cmx lib/Hacl_IntTypes_Intrinsics_bindings.cmx lib/Hacl_IntTypes_Intrinsics_128_stubs.cmx lib/Hacl_IntTypes_Intrinsics_128_bindings.cmx lib/Hacl_RSAPSS_stubs.cmx lib/Hacl_RSAPSS_bindings.cmx lib/Hacl_FFDHE_stubs.cmx lib/Hacl_FFDHE_bindings.cmx lib/Hacl_Frodo640_stubs.cmx lib/Hacl_Frodo640_bindings.cmx lib/Hacl_Chacha20_Vec128_stubs.cmx lib/Hacl_Chacha20_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_128_stubs.cmx lib/Hacl_Chacha20Poly1305_128_bindings.cmx lib/Hacl_HMAC_stubs.cmx lib/Hacl_HMAC_bindings.cmx lib/Hacl_HKDF_stubs.cmx lib/Hacl_HKDF_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_bindings.cmx lib/EverCrypt_Cipher_stubs.cmx lib/EverCrypt_Cipher_bindings.cmx lib/Hacl_GenericField32_stubs.cmx lib/Hacl_GenericField32_bindings.cmx lib/Hacl_SHA2_Vec256_stubs.cmx lib/Hacl_SHA2_Vec256_bindings.cmx lib/Hacl_EC_K256_stubs.cmx lib/Hacl_EC_K256_bindings.cmx lib/Hacl_Bignum4096_stubs.cmx lib/Hacl_Bignum4096_bindings.cmx lib/Hacl_Chacha20_Vec32_stubs.cmx lib/Hacl_Chacha20_Vec32_bindings.cmx lib/EverCrypt_Ed25519_stubs.cmx lib/EverCrypt_Ed25519_bindings.cmx lib/Hacl_Bignum4096_32_stubs.cmx lib/Hacl_Bignum4096_32_bindings.cmx lib/EverCrypt_HMAC_stubs.cmx lib/EverCrypt_HMAC_bindings.cmx lib/Hacl_HMAC_DRBG_stubs.cmx lib/Hacl_HMAC_DRBG_bindings.cmx lib/EverCrypt_DRBG_stubs.cmx lib/EverCrypt_DRBG_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_bindings.cmx lib/Hacl_HPKE_P256_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP128_SHA256_bindings.cmx lib/EverCrypt_Curve25519_stubs.cmx lib/EverCrypt_Curve25519_bindings.cmx lib/Hacl_Chacha20_Vec256_stubs.cmx lib/Hacl_Chacha20_Vec256_bindings.cmx lib/Hacl_Chacha20Poly1305_256_stubs.cmx lib/Hacl_Chacha20Poly1305_256_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_bindings.cmx lib/Hacl_Frodo976_stubs.cmx lib/Hacl_Frodo976_bindings.cmx lib/Hacl_HMAC_Blake2s_128_stubs.cmx lib/Hacl_HMAC_Blake2s_128_bindings.cmx lib/Hacl_HKDF_Blake2s_128_stubs.cmx lib/Hacl_HKDF_Blake2s_128_bindings.cmx lib/Hacl_GenericField64_stubs.cmx lib/Hacl_GenericField64_bindings.cmx lib/Hacl_Frodo1344_stubs.cmx lib/Hacl_Frodo1344_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_bindings.cmx lib/Hacl_Bignum32_stubs.cmx lib/Hacl_Bignum32_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_bindings.cmx lib/Hacl_Bignum256_32_stubs.cmx lib/Hacl_Bignum256_32_bindings.cmx lib/Hacl_SHA2_Vec128_stubs.cmx lib/Hacl_SHA2_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_32_stubs.cmx lib/Hacl_Chacha20Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib/EverCrypt_Poly1305_stubs.cmx lib/EverCrypt_Poly1305_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib/Hacl_Streaming_Poly1305_32_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_bindings.cmx lib/Hacl_Streaming_Blake2_stubs.cmx lib/Hacl_Streaming_Blake2_bindings.cmx lib/Hacl_HPKE_P256_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP256_SHA256_bindings.cmx lib/Hacl_HPKE_P256_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP32_SHA256_bindings.cmx lib/Hacl_Bignum64_stubs.cmx lib/Hacl_Bignum64_bindings.cmx lib/Hacl_Frodo64_stubs.cmx lib/Hacl_Frodo64_bindings.cmx lib/Hacl_HMAC_Blake2b_256_stubs.cmx lib/Hacl_HMAC_Blake2b_256_bindings.cmx lib/Hacl_HKDF_Blake2b_256_stubs.cmx lib/Hacl_HKDF_Blake2b_256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_bindings.cmx lib/EverCrypt_HKDF_stubs.cmx lib/EverCrypt_HKDF_bindings.cmx lib/Hacl_EC_Ed25519_stubs.cmx lib/Hacl_EC_Ed25519_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_bindings.cmx lib/EverCrypt_Chacha20Poly1305_stubs.cmx lib/EverCrypt_Chacha20Poly1305_bindings.cmx lib/EverCrypt_AEAD_stubs.cmx lib/EverCrypt_AEAD_bindings.cmx lib/Hacl_Bignum256_stubs.cmx lib/Hacl_Bignum256_bindings.cmx +CTYPES_DEPS=lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Spec_stubs.cmx lib/Hacl_Spec_bindings.cmx lib/Hacl_Hash_Blake2_stubs.cmx lib/Hacl_Hash_Blake2_bindings.cmx lib/Hacl_Hash_Blake2b_256_stubs.cmx lib/Hacl_Hash_Blake2b_256_bindings.cmx lib/Hacl_Hash_Blake2s_128_stubs.cmx lib/Hacl_Hash_Blake2s_128_bindings.cmx lib/Hacl_Hash_SHA3_stubs.cmx lib/Hacl_Hash_SHA3_bindings.cmx lib/Hacl_Hash_Base_stubs.cmx lib/Hacl_Hash_Base_bindings.cmx lib/Hacl_Hash_MD5_stubs.cmx lib/Hacl_Hash_MD5_bindings.cmx lib/Hacl_Hash_SHA1_stubs.cmx lib/Hacl_Hash_SHA1_bindings.cmx lib/Hacl_SHA2_Types_stubs.cmx lib/Hacl_SHA2_Types_bindings.cmx lib/Hacl_Hash_SHA2_stubs.cmx lib/Hacl_Hash_SHA2_bindings.cmx lib/EverCrypt_Error_stubs.cmx lib/EverCrypt_Error_bindings.cmx lib/EverCrypt_AutoConfig2_stubs.cmx lib/EverCrypt_AutoConfig2_bindings.cmx lib/EverCrypt_Hash_stubs.cmx lib/EverCrypt_Hash_bindings.cmx lib/Hacl_Chacha20_stubs.cmx lib/Hacl_Chacha20_bindings.cmx lib/Hacl_Salsa20_stubs.cmx lib/Hacl_Salsa20_bindings.cmx lib/Hacl_Bignum_Base_stubs.cmx lib/Hacl_Bignum_Base_bindings.cmx lib/Hacl_Bignum_stubs.cmx lib/Hacl_Bignum_bindings.cmx lib/Hacl_Curve25519_64_stubs.cmx lib/Hacl_Curve25519_64_bindings.cmx lib/Hacl_Bignum25519_51_stubs.cmx lib/Hacl_Bignum25519_51_bindings.cmx lib/Hacl_Curve25519_51_stubs.cmx lib/Hacl_Curve25519_51_bindings.cmx lib/Hacl_Ed25519_stubs.cmx lib/Hacl_Ed25519_bindings.cmx lib/Hacl_Poly1305_32_stubs.cmx lib/Hacl_Poly1305_32_bindings.cmx lib/Hacl_Poly1305_128_stubs.cmx lib/Hacl_Poly1305_128_bindings.cmx lib/Hacl_Poly1305_256_stubs.cmx lib/Hacl_Poly1305_256_bindings.cmx lib/Hacl_NaCl_stubs.cmx lib/Hacl_NaCl_bindings.cmx lib/Hacl_P256_stubs.cmx lib/Hacl_P256_bindings.cmx lib/Hacl_Bignum_K256_stubs.cmx lib/Hacl_Bignum_K256_bindings.cmx lib/Hacl_K256_ECDSA_stubs.cmx lib/Hacl_K256_ECDSA_bindings.cmx lib/Hacl_Frodo_KEM_stubs.cmx lib/Hacl_Frodo_KEM_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_IntTypes_Intrinsics_stubs.cmx lib/Hacl_IntTypes_Intrinsics_bindings.cmx lib/Hacl_IntTypes_Intrinsics_128_stubs.cmx lib/Hacl_IntTypes_Intrinsics_128_bindings.cmx lib/Hacl_RSAPSS_stubs.cmx lib/Hacl_RSAPSS_bindings.cmx lib/Hacl_FFDHE_stubs.cmx lib/Hacl_FFDHE_bindings.cmx lib/Hacl_Frodo640_stubs.cmx lib/Hacl_Frodo640_bindings.cmx lib/Hacl_Chacha20_Vec128_stubs.cmx lib/Hacl_Chacha20_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_128_stubs.cmx lib/Hacl_Chacha20Poly1305_128_bindings.cmx lib/Hacl_HMAC_stubs.cmx lib/Hacl_HMAC_bindings.cmx lib/Hacl_HKDF_stubs.cmx lib/Hacl_HKDF_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA512_bindings.cmx lib/EverCrypt_Cipher_stubs.cmx lib/EverCrypt_Cipher_bindings.cmx lib/Hacl_GenericField32_stubs.cmx lib/Hacl_GenericField32_bindings.cmx lib/Hacl_SHA2_Vec256_stubs.cmx lib/Hacl_SHA2_Vec256_bindings.cmx lib/Hacl_EC_K256_stubs.cmx lib/Hacl_EC_K256_bindings.cmx lib/Hacl_Bignum4096_stubs.cmx lib/Hacl_Bignum4096_bindings.cmx lib/Hacl_Chacha20_Vec32_stubs.cmx lib/Hacl_Chacha20_Vec32_bindings.cmx lib/EverCrypt_Ed25519_stubs.cmx lib/EverCrypt_Ed25519_bindings.cmx lib/Hacl_Bignum4096_32_stubs.cmx lib/Hacl_Bignum4096_32_bindings.cmx lib/EverCrypt_HMAC_stubs.cmx lib/EverCrypt_HMAC_bindings.cmx lib/Hacl_HMAC_DRBG_stubs.cmx lib/Hacl_HMAC_DRBG_bindings.cmx lib/EverCrypt_DRBG_stubs.cmx lib/EverCrypt_DRBG_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA512_bindings.cmx lib/Hacl_HPKE_P256_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP128_SHA256_bindings.cmx lib/EverCrypt_Curve25519_stubs.cmx lib/EverCrypt_Curve25519_bindings.cmx lib/Hacl_Chacha20_Vec256_stubs.cmx lib/Hacl_Chacha20_Vec256_bindings.cmx lib/Hacl_Chacha20Poly1305_256_stubs.cmx lib/Hacl_Chacha20Poly1305_256_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA512_bindings.cmx lib/Hacl_Frodo976_stubs.cmx lib/Hacl_Frodo976_bindings.cmx lib/Hacl_HMAC_Blake2s_128_stubs.cmx lib/Hacl_HMAC_Blake2s_128_bindings.cmx lib/Hacl_HKDF_Blake2s_128_stubs.cmx lib/Hacl_HKDF_Blake2s_128_bindings.cmx lib/Hacl_GenericField64_stubs.cmx lib/Hacl_GenericField64_bindings.cmx lib/Hacl_Frodo1344_stubs.cmx lib/Hacl_Frodo1344_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA512_bindings.cmx lib/Hacl_Bignum32_stubs.cmx lib/Hacl_Bignum32_bindings.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP128_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP128_SHA256_bindings.cmx lib/Hacl_Bignum256_32_stubs.cmx lib/Hacl_Bignum256_32_bindings.cmx lib/Hacl_SHA2_Vec128_stubs.cmx lib/Hacl_SHA2_Vec128_bindings.cmx lib/Hacl_Chacha20Poly1305_32_stubs.cmx lib/Hacl_Chacha20Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib/EverCrypt_Poly1305_stubs.cmx lib/EverCrypt_Poly1305_bindings.cmx lib/Hacl_Streaming_Poly1305_32_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve51_CP32_SHA512_bindings.cmx lib/Hacl_Streaming_Blake2_stubs.cmx lib/Hacl_Streaming_Blake2_bindings.cmx lib/Hacl_HPKE_P256_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP256_SHA256_bindings.cmx lib/Hacl_HPKE_P256_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_P256_CP32_SHA256_bindings.cmx lib/Hacl_Bignum64_stubs.cmx lib/Hacl_Bignum64_bindings.cmx lib/Hacl_Frodo64_stubs.cmx lib/Hacl_Frodo64_bindings.cmx lib/Hacl_HMAC_Blake2b_256_stubs.cmx lib/Hacl_HMAC_Blake2b_256_bindings.cmx lib/Hacl_HKDF_Blake2b_256_stubs.cmx lib/Hacl_HKDF_Blake2b_256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA256_bindings.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_stubs.cmx lib/Hacl_HPKE_Curve64_CP32_SHA512_bindings.cmx lib/EverCrypt_HKDF_stubs.cmx lib/EverCrypt_HKDF_bindings.cmx lib/Hacl_EC_Ed25519_stubs.cmx lib/Hacl_EC_Ed25519_bindings.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_stubs.cmx lib/Hacl_HPKE_Curve51_CP256_SHA256_bindings.cmx lib/EverCrypt_Chacha20Poly1305_stubs.cmx lib/EverCrypt_Chacha20Poly1305_bindings.cmx lib/EverCrypt_AEAD_stubs.cmx lib/EverCrypt_AEAD_bindings.cmx lib/Hacl_Bignum256_stubs.cmx lib/Hacl_Bignum256_bindings.cmx lib/Hacl_Streaming_Types_bindings.cmx: lib/Hacl_Streaming_Types_bindings.cmo: lib_gen/Hacl_Streaming_Types_gen.cmx: lib/Hacl_Streaming_Types_bindings.cmx @@ -283,14 +283,14 @@ lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx: lib/Hacl_HPKE_Interface_Hacl_Imp lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmo: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmo lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmo lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.cmx: lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.exe: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_c_stubs.o lib/Hacl_HPKE_Curve51_CP32_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve51_CP32_SHA256_gen.cmx -lib/EverCrypt_Poly1305_bindings.cmx: -lib/EverCrypt_Poly1305_bindings.cmo: -lib_gen/EverCrypt_Poly1305_gen.cmx: lib/EverCrypt_Poly1305_bindings.cmx -lib_gen/EverCrypt_Poly1305_gen.exe: lib/EverCrypt_Poly1305_bindings.cmx lib_gen/EverCrypt_Poly1305_gen.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmo: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmo lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmo lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.cmx: lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.exe: lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_bindings.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_stubs.cmx lib/Hacl_HPKE_Interface_Hacl_Impl_HPKE_Hacl_Meta_HPKE_c_stubs.o lib/Hacl_HPKE_Curve64_CP256_SHA256_bindings.cmx lib_gen/Hacl_HPKE_Curve64_CP256_SHA256_gen.cmx +lib/EverCrypt_Poly1305_bindings.cmx: +lib/EverCrypt_Poly1305_bindings.cmo: +lib_gen/EverCrypt_Poly1305_gen.cmx: lib/EverCrypt_Poly1305_bindings.cmx +lib_gen/EverCrypt_Poly1305_gen.exe: lib/EverCrypt_Poly1305_bindings.cmx lib_gen/EverCrypt_Poly1305_gen.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmx: lib/Hacl_Streaming_Types_bindings.cmx lib/Hacl_Streaming_Types_stubs.cmx lib/Hacl_Streaming_Poly1305_32_bindings.cmo: lib/Hacl_Streaming_Types_bindings.cmo lib/Hacl_Streaming_Types_stubs.cmo lib_gen/Hacl_Streaming_Poly1305_32_gen.cmx: lib/Hacl_Streaming_Poly1305_32_bindings.cmx diff --git a/src/EverCrypt_AEAD.c b/src/EverCrypt_AEAD.c index 564dbc2e..d3a4ffbe 100644 --- a/src/EverCrypt_AEAD.c +++ b/src/EverCrypt_AEAD.c @@ -46,6 +46,8 @@ The state may be reused as many times as desired. */ bool EverCrypt_AEAD_uu___is_Ek(Spec_Agile_AEAD_alg a, EverCrypt_AEAD_state_s projectee) { + KRML_HOST_IGNORE(a); + KRML_HOST_IGNORE(projectee); return true; } @@ -58,8 +60,7 @@ Return the algorithm used in the AEAD state. */ Spec_Agile_AEAD_alg EverCrypt_AEAD_alg_of_state(EverCrypt_AEAD_state_s *s) { - EverCrypt_AEAD_state_s scrut = *s; - Spec_Cipher_Expansion_impl impl = scrut.impl; + Spec_Cipher_Expansion_impl impl = (*s).impl; switch (impl) { case Spec_Cipher_Expansion_Hacl_CHACHA20: @@ -97,6 +98,8 @@ create_in_chacha20_poly1305(EverCrypt_AEAD_state_s **dst, uint8_t *k) static EverCrypt_Error_error_code create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(k); #if HACL_CAN_COMPILE_VALE bool has_aesni = EverCrypt_AutoConfig2_has_aesni(); bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); @@ -108,8 +111,8 @@ create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) uint8_t *ek = (uint8_t *)KRML_HOST_CALLOC((uint32_t)480U, sizeof (uint8_t)); uint8_t *keys_b = ek; uint8_t *hkeys_b = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b); - uint64_t scrut0 = aes128_keyhash_init(keys_b, hkeys_b); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b, hkeys_b)); EverCrypt_AEAD_state_s *p = (EverCrypt_AEAD_state_s *)KRML_HOST_MALLOC(sizeof (EverCrypt_AEAD_state_s)); p[0U] = ((EverCrypt_AEAD_state_s){ .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }); @@ -125,6 +128,8 @@ create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) static EverCrypt_Error_error_code create_in_aes256_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(k); #if HACL_CAN_COMPILE_VALE bool has_aesni = EverCrypt_AutoConfig2_has_aesni(); bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); @@ -136,8 +141,8 @@ create_in_aes256_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) uint8_t *ek = (uint8_t *)KRML_HOST_CALLOC((uint32_t)544U, sizeof (uint8_t)); uint8_t *keys_b = ek; uint8_t *hkeys_b = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b); - uint64_t scrut0 = aes256_keyhash_init(keys_b, hkeys_b); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b, hkeys_b)); EverCrypt_AEAD_state_s *p = (EverCrypt_AEAD_state_s *)KRML_HOST_MALLOC(sizeof (EverCrypt_AEAD_state_s)); p[0U] = ((EverCrypt_AEAD_state_s){ .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }); @@ -203,6 +208,15 @@ encrypt_aes128_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -212,8 +226,7 @@ encrypt_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)304U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -223,8 +236,12 @@ encrypt_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -250,9 +267,7 @@ encrypt_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut0 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -268,7 +283,7 @@ encrypt_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -281,9 +296,7 @@ encrypt_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut0 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -299,7 +312,7 @@ encrypt_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, @@ -327,6 +340,15 @@ encrypt_aes256_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -336,8 +358,7 @@ encrypt_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)368U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -347,8 +368,12 @@ encrypt_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -374,9 +399,7 @@ encrypt_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut0 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -392,7 +415,7 @@ encrypt_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -405,9 +428,7 @@ encrypt_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut0 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -423,7 +444,7 @@ encrypt_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, @@ -525,27 +546,34 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut0 = aes128_key_expansion(k, keys_b0); - uint64_t scrut1 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -555,8 +583,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -582,9 +614,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -600,7 +630,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -613,9 +643,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -631,12 +659,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; #else @@ -669,27 +697,34 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut0 = aes256_key_expansion(k, keys_b0); - uint64_t scrut1 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -699,8 +734,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -726,9 +765,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -744,7 +781,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -757,9 +794,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -775,12 +810,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; #else @@ -805,6 +840,15 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -816,23 +860,21 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut0 = aes128_key_expansion(k, keys_b0); - uint64_t scrut1 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -842,8 +884,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -869,9 +915,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -887,7 +931,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -900,9 +944,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -918,12 +960,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; } @@ -946,6 +988,15 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -957,23 +1008,21 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut0 = aes256_key_expansion(k, keys_b0); - uint64_t scrut1 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -983,8 +1032,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1010,9 +1063,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -1028,7 +1079,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -1041,9 +1092,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -1059,12 +1108,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; } @@ -1087,12 +1136,12 @@ EverCrypt_AEAD_encrypt_expand_chacha20_poly1305( uint8_t *tag ) { + KRML_HOST_IGNORE(iv_len); uint8_t ek[32U] = { 0U }; EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Hacl_CHACHA20, .ek = ek }; memcpy(ek, k, (uint32_t)32U * sizeof (uint8_t)); EverCrypt_AEAD_state_s *s = &p; - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; EverCrypt_Chacha20Poly1305_aead_encrypt(ek0, iv, ad_len, ad, plain_len, plain, cipher, tag); return EverCrypt_Error_Success; } @@ -1173,6 +1222,15 @@ decrypt_aes128_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -1182,8 +1240,7 @@ decrypt_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)304U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -1193,8 +1250,12 @@ decrypt_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1222,7 +1283,7 @@ decrypt_aes128_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut0 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1240,7 +1301,6 @@ decrypt_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } else @@ -1255,7 +1315,7 @@ decrypt_aes128_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut0 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1273,7 +1333,6 @@ decrypt_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1307,6 +1366,15 @@ decrypt_aes256_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -1316,8 +1384,7 @@ decrypt_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)368U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -1327,8 +1394,12 @@ decrypt_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1356,7 +1427,7 @@ decrypt_aes256_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut0 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1374,7 +1445,6 @@ decrypt_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } else @@ -1389,7 +1459,7 @@ decrypt_aes256_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut0 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1407,7 +1477,6 @@ decrypt_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1449,8 +1518,7 @@ decrypt_chacha20_poly1305( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint32_t r = EverCrypt_Chacha20Poly1305_aead_decrypt(ek, iv, ad_len, ad, cipher_len, dst, cipher, tag); if (r == (uint32_t)0U) @@ -1508,8 +1576,7 @@ EverCrypt_AEAD_decrypt( { return EverCrypt_Error_InvalidKey; } - EverCrypt_AEAD_state_s scrut = *s; - Spec_Cipher_Expansion_impl i = scrut.impl; + Spec_Cipher_Expansion_impl i = (*s).impl; switch (i) { case Spec_Cipher_Expansion_Vale_AES128: @@ -1553,12 +1620,21 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b0); - uint64_t scrut0 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1569,8 +1645,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1580,8 +1655,12 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1609,7 +1688,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1627,7 +1706,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1642,7 +1720,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1660,7 +1738,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1702,12 +1779,21 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b0); - uint64_t scrut0 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1718,8 +1804,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1729,8 +1814,12 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1758,7 +1847,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1776,7 +1865,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1791,7 +1879,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1809,7 +1897,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1843,6 +1930,15 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -1854,8 +1950,8 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b0); - uint64_t scrut0 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1866,8 +1962,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1877,8 +1972,12 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1906,7 +2005,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1924,7 +2023,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1939,7 +2037,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1957,7 +2055,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1989,6 +2086,15 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -2000,8 +2106,8 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b0); - uint64_t scrut0 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -2012,8 +2118,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -2023,8 +2128,12 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -2052,7 +2161,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -2070,7 +2179,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -2085,7 +2193,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -2103,7 +2211,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -2214,8 +2321,7 @@ Cleanup and free the AEAD state. */ void EverCrypt_AEAD_free(EverCrypt_AEAD_state_s *s) { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; KRML_HOST_FREE(ek); KRML_HOST_FREE(s); } diff --git a/src/EverCrypt_AutoConfig2.c b/src/EverCrypt_AutoConfig2.c index fe93ef8a..b549d020 100644 --- a/src/EverCrypt_AutoConfig2.c +++ b/src/EverCrypt_AutoConfig2.c @@ -113,75 +113,59 @@ void EverCrypt_AutoConfig2_recall(void) void EverCrypt_AutoConfig2_init(void) { #if HACL_CAN_COMPILE_VALE - uint64_t scrut = check_aesni(); - if (scrut != (uint64_t)0U) + if (check_aesni() != (uint64_t)0U) { cpu_has_aesni[0U] = true; cpu_has_pclmulqdq[0U] = true; } - uint64_t scrut0 = check_sha(); - if (scrut0 != (uint64_t)0U) + if (check_sha() != (uint64_t)0U) { cpu_has_shaext[0U] = true; } - uint64_t scrut1 = check_adx_bmi2(); - if (scrut1 != (uint64_t)0U) + if (check_adx_bmi2() != (uint64_t)0U) { cpu_has_bmi2[0U] = true; cpu_has_adx[0U] = true; } - uint64_t scrut2 = check_avx(); - if (scrut2 != (uint64_t)0U) + if (check_avx() != (uint64_t)0U) { - uint64_t scrut3 = check_osxsave(); - if (scrut3 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut4 = check_avx_xcr0(); - if (scrut4 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { cpu_has_avx[0U] = true; } } } - uint64_t scrut3 = check_avx2(); - if (scrut3 != (uint64_t)0U) + if (check_avx2() != (uint64_t)0U) { - uint64_t scrut4 = check_osxsave(); - if (scrut4 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut5 = check_avx_xcr0(); - if (scrut5 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { cpu_has_avx2[0U] = true; } } } - uint64_t scrut4 = check_sse(); - if (scrut4 != (uint64_t)0U) + if (check_sse() != (uint64_t)0U) { cpu_has_sse[0U] = true; } - uint64_t scrut5 = check_movbe(); - if (scrut5 != (uint64_t)0U) + if (check_movbe() != (uint64_t)0U) { cpu_has_movbe[0U] = true; } - uint64_t scrut6 = check_rdrand(); - if (scrut6 != (uint64_t)0U) + if (check_rdrand() != (uint64_t)0U) { cpu_has_rdrand[0U] = true; } - uint64_t scrut7 = check_avx512(); - if (scrut7 != (uint64_t)0U) + if (check_avx512() != (uint64_t)0U) { - uint64_t scrut8 = check_osxsave(); - if (scrut8 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut9 = check_avx_xcr0(); - if (scrut9 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { - uint64_t scrut10 = check_avx512_xcr0(); - if (scrut10 != (uint64_t)0U) + if (check_avx512_xcr0() != (uint64_t)0U) { cpu_has_avx512[0U] = true; return; diff --git a/src/EverCrypt_DRBG.c b/src/EverCrypt_DRBG.c index f21313e9..13e517e5 100644 --- a/src/EverCrypt_DRBG.c +++ b/src/EverCrypt_DRBG.c @@ -92,6 +92,7 @@ EverCrypt_DRBG_uu___is_SHA1_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA1_s) { return true; @@ -105,6 +106,7 @@ EverCrypt_DRBG_uu___is_SHA2_256_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_256_s) { return true; @@ -118,6 +120,7 @@ EverCrypt_DRBG_uu___is_SHA2_384_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_384_s) { return true; @@ -131,6 +134,7 @@ EverCrypt_DRBG_uu___is_SHA2_512_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_512_s) { return true; diff --git a/src/EverCrypt_Hash.c b/src/EverCrypt_Hash.c index 914a105f..b88df9e2 100644 --- a/src/EverCrypt_Hash.c +++ b/src/EverCrypt_Hash.c @@ -399,7 +399,7 @@ void EverCrypt_Hash_update_multi_256(uint32_t *s, uint8_t *blocks, uint32_t n) if (has_shaext && has_sse) { uint64_t n1 = (uint64_t)n; - uint64_t scrut = sha256_update(s, blocks, n1, k224_256); + KRML_HOST_IGNORE(sha256_update(s, blocks, n1, k224_256)); return; } Hacl_SHA2_Scalar32_sha256_update_nblocks(n * (uint32_t)64U, blocks, s); @@ -2156,8 +2156,7 @@ Perform a run-time test to determine which algorithm was chosen for the given pi Spec_Hash_Definitions_hash_alg EverCrypt_Hash_Incremental_alg_of_state(EverCrypt_Hash_Incremental_hash_state *s) { - EverCrypt_Hash_Incremental_hash_state scrut = *s; - EverCrypt_Hash_state_s *block_state = scrut.block_state; + EverCrypt_Hash_state_s *block_state = (*s).block_state; return alg_of_state(block_state); } diff --git a/src/EverCrypt_Poly1305.c b/src/EverCrypt_Poly1305.c index 717b9527..454c0fce 100644 --- a/src/EverCrypt_Poly1305.c +++ b/src/EverCrypt_Poly1305.c @@ -28,8 +28,13 @@ #include "internal/Vale.h" #include "config.h" -static void poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key) +KRML_MAYBE_UNUSED static void +poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(src); + KRML_HOST_IGNORE(len); + KRML_HOST_IGNORE(key); #if HACL_CAN_COMPILE_VALE uint8_t ctx[192U] = { 0U }; memcpy(ctx + (uint32_t)24U, key, (uint32_t)32U * sizeof (uint8_t)); @@ -38,19 +43,16 @@ static void poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key uint8_t tmp[16U] = { 0U }; if (n_extra == (uint32_t)0U) { - uint64_t scrut = x64_poly1305(ctx, src, (uint64_t)len, (uint64_t)1U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, src, (uint64_t)len, (uint64_t)1U)); } else { uint32_t len16 = n_blocks * (uint32_t)16U; uint8_t *src16 = src; memcpy(tmp, src + len16, n_extra * sizeof (uint8_t)); - uint64_t scrut = x64_poly1305(ctx, src16, (uint64_t)len16, (uint64_t)0U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, src16, (uint64_t)len16, (uint64_t)0U)); memcpy(ctx + (uint32_t)24U, key, (uint32_t)32U * sizeof (uint8_t)); - uint64_t scrut0 = x64_poly1305(ctx, tmp, (uint64_t)n_extra, (uint64_t)1U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, tmp, (uint64_t)n_extra, (uint64_t)1U)); } memcpy(dst, ctx, (uint32_t)16U * sizeof (uint8_t)); #endif diff --git a/src/Hacl_Chacha20_Vec128.c b/src/Hacl_Chacha20_Vec128.c index ed112654..1e0c4ec1 100644 --- a/src/Hacl_Chacha20_Vec128.c +++ b/src/Hacl_Chacha20_Vec128.c @@ -370,9 +370,8 @@ Hacl_Chacha20_Vec128_chacha20_encrypt_128( 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 (uint8_t)); + memcpy(plain, text + nb * (uint32_t)256U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; chacha20_core_128(k, ctx, nb); Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; @@ -676,9 +675,8 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128( 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 (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)256U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; chacha20_core_128(k, ctx, nb); Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; diff --git a/src/Hacl_Chacha20_Vec256.c b/src/Hacl_Chacha20_Vec256.c index 2df300b6..620f5040 100644 --- a/src/Hacl_Chacha20_Vec256.c +++ b/src/Hacl_Chacha20_Vec256.c @@ -470,9 +470,8 @@ Hacl_Chacha20_Vec256_chacha20_encrypt_256( 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 (uint8_t)); + memcpy(plain, text + nb * (uint32_t)512U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; chacha20_core_256(k, ctx, nb); Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; @@ -968,9 +967,8 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256( 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 (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)512U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; chacha20_core_256(k, ctx, nb); Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; diff --git a/src/Hacl_Chacha20_Vec32.c b/src/Hacl_Chacha20_Vec32.c index 6f137f39..2bf4764c 100644 --- a/src/Hacl_Chacha20_Vec32.c +++ b/src/Hacl_Chacha20_Vec32.c @@ -229,9 +229,8 @@ Hacl_Chacha20_Vec32_chacha20_encrypt_32( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = text + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, text + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k[16U] = { 0U }; chacha20_core_32(k, ctx, nb); KRML_MAYBE_FOR16(i, @@ -279,9 +278,8 @@ Hacl_Chacha20_Vec32_chacha20_decrypt_32( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = cipher + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k[16U] = { 0U }; chacha20_core_32(k, ctx, nb); KRML_MAYBE_FOR16(i, diff --git a/src/Hacl_Curve25519_64.c b/src/Hacl_Curve25519_64.c index 526fbd22..fb0974fe 100644 --- a/src/Hacl_Curve25519_64.c +++ b/src/Hacl_Curve25519_64.c @@ -35,7 +35,7 @@ static inline void add_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2) #if HACL_CAN_COMPILE_INLINE_ASM add_scalar(out, f1, f2); #else - uint64_t uu____0 = add_scalar_e(out, f1, f2); + KRML_HOST_IGNORE(add_scalar_e(out, f1, f2)); #endif } @@ -44,7 +44,7 @@ static inline void fadd0(uint64_t *out, uint64_t *f1, uint64_t *f2) #if HACL_CAN_COMPILE_INLINE_ASM fadd(out, f1, f2); #else - uint64_t uu____0 = fadd_e(out, f1, f2); + KRML_HOST_IGNORE(fadd_e(out, f1, f2)); #endif } @@ -53,7 +53,7 @@ static inline void fsub0(uint64_t *out, uint64_t *f1, uint64_t *f2) #if HACL_CAN_COMPILE_INLINE_ASM fsub(out, f1, f2); #else - uint64_t uu____0 = fsub_e(out, f1, f2); + KRML_HOST_IGNORE(fsub_e(out, f1, f2)); #endif } @@ -62,7 +62,7 @@ static inline void fmul0(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *tm #if HACL_CAN_COMPILE_INLINE_ASM fmul(out, f1, f2, tmp); #else - uint64_t uu____0 = fmul_e(tmp, f1, out, f2); + KRML_HOST_IGNORE(fmul_e(tmp, f1, out, f2)); #endif } @@ -71,7 +71,7 @@ static inline void fmul20(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *t #if HACL_CAN_COMPILE_INLINE_ASM fmul2(out, f1, f2, tmp); #else - uint64_t uu____0 = fmul2_e(tmp, f1, out, f2); + KRML_HOST_IGNORE(fmul2_e(tmp, f1, out, f2)); #endif } @@ -80,7 +80,7 @@ static inline void fmul_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2) #if HACL_CAN_COMPILE_INLINE_ASM fmul_scalar(out, f1, f2); #else - uint64_t uu____0 = fmul_scalar_e(out, f1, f2); + KRML_HOST_IGNORE(fmul_scalar_e(out, f1, f2)); #endif } @@ -89,7 +89,7 @@ static inline void fsqr0(uint64_t *out, uint64_t *f1, uint64_t *tmp) #if HACL_CAN_COMPILE_INLINE_ASM fsqr(out, f1, tmp); #else - uint64_t uu____0 = fsqr_e(tmp, f1, out); + KRML_HOST_IGNORE(fsqr_e(tmp, f1, out)); #endif } @@ -98,7 +98,7 @@ static inline void fsqr20(uint64_t *out, uint64_t *f, uint64_t *tmp) #if HACL_CAN_COMPILE_INLINE_ASM fsqr2(out, f, tmp); #else - uint64_t uu____0 = fsqr2_e(tmp, f, out); + KRML_HOST_IGNORE(fsqr2_e(tmp, f, out)); #endif } @@ -107,7 +107,7 @@ static inline void cswap20(uint64_t bit, uint64_t *p1, uint64_t *p2) #if HACL_CAN_COMPILE_INLINE_ASM cswap2(bit, p1, p2); #else - uint64_t uu____0 = cswap2_e(bit, p1, p2); + KRML_HOST_IGNORE(cswap2_e(bit, p1, p2)); #endif } diff --git a/src/Hacl_Ed25519.c b/src/Hacl_Ed25519.c index 9d7c3bd4..f9881e91 100644 --- a/src/Hacl_Ed25519.c +++ b/src/Hacl_Ed25519.c @@ -711,65 +711,53 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) FStar_UInt128_uint128 c00 = carry0; FStar_UInt128_uint128 carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z11, c00), (uint32_t)56U); - uint64_t - t100 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z11, c00)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c10 = carry1; FStar_UInt128_uint128 carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z21, c10), (uint32_t)56U); - uint64_t - t101 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z21, c10)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c20 = carry2; FStar_UInt128_uint128 carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z31, c20), (uint32_t)56U); - uint64_t - t102 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z31, c20)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c30 = carry3; FStar_UInt128_uint128 carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z41, c30), (uint32_t)56U); uint64_t - t103 = + t100 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z41, c30)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c40 = carry4; - uint64_t t410 = t103; + uint64_t t410 = t100; FStar_UInt128_uint128 carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z5, c40), (uint32_t)56U); uint64_t - t104 = + t101 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z5, c40)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c5 = carry5; - uint64_t t51 = t104; + uint64_t t51 = t101; FStar_UInt128_uint128 carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z6, c5), (uint32_t)56U); uint64_t - t105 = + t102 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z6, c5)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c6 = carry6; - uint64_t t61 = t105; + uint64_t t61 = t102; FStar_UInt128_uint128 carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z7, c6), (uint32_t)56U); uint64_t - t106 = + t103 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z7, c6)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c7 = carry7; - uint64_t t71 = t106; + uint64_t t71 = t103; FStar_UInt128_uint128 carry8 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z8, c7), (uint32_t)56U); uint64_t - t107 = + t104 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z8, c7)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c8 = carry8; - uint64_t t81 = t107; + uint64_t t81 = t104; uint64_t t91 = FStar_UInt128_uint128_to_uint64(c8); uint64_t qmu4_ = t410; uint64_t qmu5_ = t51; @@ -818,19 +806,19 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(qdiv3, m1); FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(qdiv4, m0); FStar_UInt128_uint128 carry9 = FStar_UInt128_shift_right(xy00, (uint32_t)56U); - uint64_t t108 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU; + uint64_t t105 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c0 = carry9; - uint64_t t010 = t108; + uint64_t t010 = t105; FStar_UInt128_uint128 carry10 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0), (uint32_t)56U); uint64_t - t109 = + t106 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c11 = carry10; - uint64_t t110 = t109; + uint64_t t110 = t106; FStar_UInt128_uint128 carry11 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, @@ -839,14 +827,14 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c11), (uint32_t)56U); uint64_t - t1010 = + t107 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, xy11), xy20), c11)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c21 = carry11; - uint64_t t210 = t1010; + uint64_t t210 = t107; FStar_UInt128_uint128 carry = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, @@ -856,7 +844,7 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c21), (uint32_t)56U); uint64_t - t1011 = + t108 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, xy12), xy21), @@ -864,7 +852,7 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c21)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c31 = carry; - uint64_t t310 = t1011; + uint64_t t310 = t108; uint64_t t411 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04, @@ -880,24 +868,24 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) uint64_t qmul3 = t310; uint64_t qmul4 = t411; uint64_t b5 = (r0 - qmul0) >> (uint32_t)63U; - uint64_t t1012 = (b5 << (uint32_t)56U) + r0 - qmul0; + uint64_t t109 = (b5 << (uint32_t)56U) + r0 - qmul0; uint64_t c1 = b5; - uint64_t t011 = t1012; + uint64_t t011 = t109; uint64_t b6 = (r1 - (qmul1 + c1)) >> (uint32_t)63U; - uint64_t t1013 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1); + uint64_t t1010 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1); uint64_t c2 = b6; - uint64_t t111 = t1013; + uint64_t t111 = t1010; uint64_t b7 = (r2 - (qmul2 + c2)) >> (uint32_t)63U; - uint64_t t1014 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2); + uint64_t t1011 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2); uint64_t c3 = b7; - uint64_t t211 = t1014; + uint64_t t211 = t1011; uint64_t b8 = (r3 - (qmul3 + c3)) >> (uint32_t)63U; - uint64_t t1015 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3); + uint64_t t1012 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3); uint64_t c4 = b8; - uint64_t t311 = t1015; + uint64_t t311 = t1012; uint64_t b9 = (r4 - (qmul4 + c4)) >> (uint32_t)63U; - uint64_t t1016 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4); - uint64_t t412 = t1016; + uint64_t t1013 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4); + uint64_t t412 = t1013; uint64_t s0 = t011; uint64_t s1 = t111; uint64_t s2 = t211; @@ -914,21 +902,21 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) uint64_t y3 = m31; uint64_t y4 = m41; uint64_t b10 = (s0 - y0) >> (uint32_t)63U; - uint64_t t1017 = (b10 << (uint32_t)56U) + s0 - y0; + uint64_t t1014 = (b10 << (uint32_t)56U) + s0 - y0; uint64_t b0 = b10; - uint64_t t01 = t1017; + uint64_t t01 = t1014; uint64_t b11 = (s1 - (y1 + b0)) >> (uint32_t)63U; - uint64_t t1018 = (b11 << (uint32_t)56U) + s1 - (y1 + b0); + uint64_t t1015 = (b11 << (uint32_t)56U) + s1 - (y1 + b0); uint64_t b1 = b11; - uint64_t t11 = t1018; + uint64_t t11 = t1015; uint64_t b12 = (s2 - (y2 + b1)) >> (uint32_t)63U; - uint64_t t1019 = (b12 << (uint32_t)56U) + s2 - (y2 + b1); + uint64_t t1016 = (b12 << (uint32_t)56U) + s2 - (y2 + b1); uint64_t b2 = b12; - uint64_t t21 = t1019; + uint64_t t21 = t1016; uint64_t b13 = (s3 - (y3 + b2)) >> (uint32_t)63U; - uint64_t t1020 = (b13 << (uint32_t)56U) + s3 - (y3 + b2); + uint64_t t1017 = (b13 << (uint32_t)56U) + s3 - (y3 + b2); uint64_t b3 = b13; - uint64_t t31 = t1020; + uint64_t t31 = t1017; uint64_t b = (s4 - (y4 + b3)) >> (uint32_t)63U; uint64_t t10 = (b << (uint32_t)56U) + s4 - (y4 + b3); uint64_t b4 = b; diff --git a/src/Hacl_FFDHE.c b/src/Hacl_FFDHE.c index 78aaaab6..9cf2ddfb 100644 --- a/src/Hacl_FFDHE.c +++ b/src/Hacl_FFDHE.c @@ -127,7 +127,6 @@ static inline uint64_t ffdhe_check_pk(Spec_FFDHE_ffdhe_alg a, uint64_t *pk_n, ui memset(p_n1, 0U, nLen * sizeof (uint64_t)); uint64_t c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64((uint64_t)0U, p_n[0U], (uint64_t)1U, p_n1); - uint64_t c1; if ((uint32_t)1U < nLen) { uint64_t *a1 = p_n + (uint32_t)1U; @@ -159,12 +158,12 @@ static inline uint64_t ffdhe_check_pk(Spec_FFDHE_ffdhe_alg a, uint64_t *pk_n, ui uint64_t *res_i = res1 + i; c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, (uint64_t)0U, res_i); } - uint64_t c10 = c; - c1 = c10; + uint64_t c1 = c; + KRML_HOST_IGNORE(c1); } else { - c1 = c0; + KRML_HOST_IGNORE(c0); } KRML_CHECK_SIZE(sizeof (uint64_t), nLen); uint64_t b2[nLen]; diff --git a/src/Hacl_Frodo_KEM.c b/src/Hacl_Frodo_KEM.c index 13db363a..4265ac0e 100644 --- a/src/Hacl_Frodo_KEM.c +++ b/src/Hacl_Frodo_KEM.c @@ -30,6 +30,6 @@ void randombytes_(uint32_t len, uint8_t *res) { - bool b = Lib_RandomBuffer_System_randombytes(res, len); + KRML_HOST_IGNORE(Lib_RandomBuffer_System_randombytes(res, len)); } diff --git a/src/Hacl_HMAC_DRBG.c b/src/Hacl_HMAC_DRBG.c index 181a8ef4..0a09aaed 100644 --- a/src/Hacl_HMAC_DRBG.c +++ b/src/Hacl_HMAC_DRBG.c @@ -71,6 +71,8 @@ uint32_t Hacl_HMAC_DRBG_min_length(Spec_Hash_Definitions_hash_alg a) bool Hacl_HMAC_DRBG_uu___is_State(Spec_Hash_Definitions_hash_alg a, Hacl_HMAC_DRBG_state projectee) { + KRML_HOST_IGNORE(a); + KRML_HOST_IGNORE(projectee); return true; } @@ -1084,6 +1086,7 @@ Hacl_HMAC_DRBG_generate( void Hacl_HMAC_DRBG_free(Spec_Hash_Definitions_hash_alg uu___, Hacl_HMAC_DRBG_state s) { + KRML_HOST_IGNORE(uu___); uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; diff --git a/src/Hacl_Hash_Blake2.c b/src/Hacl_Hash_Blake2.c index 194e7157..aecc6165 100644 --- a/src/Hacl_Hash_Blake2.c +++ b/src/Hacl_Hash_Blake2.c @@ -545,6 +545,7 @@ Hacl_Blake2b_32_blake2b_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { FStar_UInt128_uint128 @@ -1192,6 +1193,7 @@ Hacl_Blake2s_32_blake2s_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { uint64_t totlen = prev + (uint64_t)((i + (uint32_t)1U) * (uint32_t)64U); diff --git a/src/Hacl_Hash_Blake2b_256.c b/src/Hacl_Hash_Blake2b_256.c index d0df7cd8..b37ffc5f 100644 --- a/src/Hacl_Hash_Blake2b_256.c +++ b/src/Hacl_Hash_Blake2b_256.c @@ -268,6 +268,7 @@ Hacl_Blake2b_256_blake2b_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { FStar_UInt128_uint128 diff --git a/src/Hacl_Hash_Blake2s_128.c b/src/Hacl_Hash_Blake2s_128.c index 5bf06711..86c4f030 100644 --- a/src/Hacl_Hash_Blake2s_128.c +++ b/src/Hacl_Hash_Blake2s_128.c @@ -268,6 +268,7 @@ Hacl_Blake2s_128_blake2s_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { uint64_t totlen = prev + (uint64_t)((i + (uint32_t)1U) * (uint32_t)64U); diff --git a/src/Hacl_Hash_MD5.c b/src/Hacl_Hash_MD5.c index 1b376960..222ac824 100644 --- a/src/Hacl_Hash_MD5.c +++ b/src/Hacl_Hash_MD5.c @@ -1218,7 +1218,6 @@ void Hacl_Streaming_MD5_legacy_init(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Hash_Core_MD5_legacy_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Hash_SHA1.c b/src/Hacl_Hash_SHA1.c index 80edc004..5ecb3c0b 100644 --- a/src/Hacl_Hash_SHA1.c +++ b/src/Hacl_Hash_SHA1.c @@ -254,7 +254,6 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Hash_Core_SHA1_legacy_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Hash_SHA2.c b/src/Hacl_Hash_SHA2.c index 46fde83f..c93c3616 100644 --- a/src/Hacl_Hash_SHA2.c +++ b/src/Hacl_Hash_SHA2.c @@ -537,7 +537,6 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha256_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -836,7 +835,6 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha224_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -962,7 +960,6 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) Hacl_Streaming_MD_state_64 scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha512_init(block_state); Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -1262,7 +1259,6 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) Hacl_Streaming_MD_state_64 scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha384_init(block_state); Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Hash_SHA3.c b/src/Hacl_Hash_SHA3.c index 5f4707f4..19d13b1b 100644 --- a/src/Hacl_Hash_SHA3.c +++ b/src/Hacl_Hash_SHA3.c @@ -125,10 +125,9 @@ Hacl_Hash_SHA3_update_last_sha3( if (input_len == len) { Hacl_Impl_SHA3_absorb_inner(len, input, s); - uint8_t *uu____0 = input + input_len; uint8_t lastBlock_[200U] = { 0U }; uint8_t *lastBlock = lastBlock_; - memcpy(lastBlock, uu____0, (uint32_t)0U * sizeof (uint8_t)); + memcpy(lastBlock, input + input_len, (uint32_t)0U * sizeof (uint8_t)); lastBlock[0U] = suffix; Hacl_Impl_SHA3_loadState(len, lastBlock, s); if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && (uint32_t)0U == len - (uint32_t)1U) @@ -167,8 +166,7 @@ hash_buf2; Spec_Hash_Definitions_hash_alg Hacl_Streaming_Keccak_get_alg(Hacl_Streaming_Keccak_state *s) { - Hacl_Streaming_Keccak_state scrut = *s; - Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state; + Hacl_Streaming_Keccak_hash_buf block_state = (*s).block_state; return block_state.fst; } @@ -809,6 +807,7 @@ Hacl_Impl_SHA3_keccak( uint8_t *output ) { + KRML_HOST_IGNORE(capacity); uint32_t rateInBytes = rate / (uint32_t)8U; uint64_t s[25U] = { 0U }; absorb(s, rateInBytes, inputByteLen, input, delimitedSuffix); diff --git a/src/Hacl_K256_ECDSA.c b/src/Hacl_K256_ECDSA.c index fb53f3fd..2ffc1060 100644 --- a/src/Hacl_K256_ECDSA.c +++ b/src/Hacl_K256_ECDSA.c @@ -498,7 +498,7 @@ mul_pow2_256_minus_q_add( uint64_t r = c; tmp[len + i0] = r;); memcpy(res + (uint32_t)2U, a, len * sizeof (uint64_t)); - uint64_t uu____0 = bn_add(resLen, res, len + (uint32_t)2U, tmp, res); + KRML_HOST_IGNORE(bn_add(resLen, res, len + (uint32_t)2U, tmp, res)); uint64_t c = bn_add(resLen, res, (uint32_t)4U, e, res); return c; } @@ -514,15 +514,23 @@ static inline void modq(uint64_t *out, uint64_t *a) uint64_t *t01 = tmp; uint64_t m[7U] = { 0U }; uint64_t p[5U] = { 0U }; - uint64_t - c0 = mul_pow2_256_minus_q_add((uint32_t)4U, (uint32_t)7U, t01, a + (uint32_t)4U, a, m); - uint64_t - c10 = mul_pow2_256_minus_q_add((uint32_t)3U, (uint32_t)5U, t01, m + (uint32_t)4U, m, p); + KRML_HOST_IGNORE(mul_pow2_256_minus_q_add((uint32_t)4U, + (uint32_t)7U, + t01, + a + (uint32_t)4U, + a, + m)); + KRML_HOST_IGNORE(mul_pow2_256_minus_q_add((uint32_t)3U, + (uint32_t)5U, + t01, + m + (uint32_t)4U, + m, + p)); uint64_t c2 = mul_pow2_256_minus_q_add((uint32_t)1U, (uint32_t)4U, t01, p + (uint32_t)4U, p, r); - uint64_t c00 = c2; + uint64_t c0 = c2; uint64_t c1 = add4(r, tmp, out); - uint64_t mask = (uint64_t)0U - (c00 + c1); + uint64_t mask = (uint64_t)0U - (c0 + c1); KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, @@ -612,7 +620,7 @@ static inline void qmul_shift_384(uint64_t *res, uint64_t *a, uint64_t *b) uint64_t *res_i = res1 + i; c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, (uint64_t)0U, res_i);); uint64_t c1 = c; - uint64_t uu____0 = c1; + KRML_HOST_IGNORE(c1); uint64_t flag = l[5U] >> (uint32_t)63U; uint64_t mask = (uint64_t)0U - flag; KRML_MAYBE_FOR4(i, @@ -1223,6 +1231,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)118285133003718U, (uint64_t)434519962075150U, (uint64_t)1114612377498854U, (uint64_t)3488596944003813U, (uint64_t)450716531072892U, (uint64_t)66044973203836U }; + KRML_HOST_IGNORE(q2); uint64_t q3[15U] = { @@ -1232,6 +1241,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)265969268774814U, (uint64_t)1913228635640715U, (uint64_t)2831959046949342U, (uint64_t)888030405442963U, (uint64_t)1817092932985033U, (uint64_t)101515844997121U }; + KRML_HOST_IGNORE(q3); uint64_t q4[15U] = { @@ -1241,6 +1251,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)12245672982162U, (uint64_t)2119364213800870U, (uint64_t)2034960311715107U, (uint64_t)3172697815804487U, (uint64_t)4185144850224160U, (uint64_t)2792055915674U }; + KRML_HOST_IGNORE(q4); uint64_t *r1 = scalar; uint64_t *r2 = scalar + (uint32_t)1U; uint64_t *r3 = scalar + (uint32_t)2U; @@ -1605,6 +1616,7 @@ Hacl_K256_ECDSA_ecdsa_sign_hashed_msg( ) { uint64_t oneq[4U] = { (uint64_t)0x1U, (uint64_t)0x0U, (uint64_t)0x0U, (uint64_t)0x0U }; + KRML_HOST_IGNORE(oneq); uint64_t rsdk_q[16U] = { 0U }; uint64_t *r_q = rsdk_q; uint64_t *s_q = rsdk_q + (uint32_t)4U; diff --git a/src/Hacl_RSAPSS.c b/src/Hacl_RSAPSS.c index 19d4e5b4..ceb9a6f0 100644 --- a/src/Hacl_RSAPSS.c +++ b/src/Hacl_RSAPSS.c @@ -404,9 +404,9 @@ load_skey( Sign a message `msg` and write the signature to `sgnt`. @param a Hash algorithm to use. Allowed values for `a` are ... - * Spec_Hash_Definitions_SHA2_256, - * Spec_Hash_Definitions_SHA2_384, and - * Spec_Hash_Definitions_SHA2_512. + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. @@ -518,7 +518,10 @@ Hacl_RSAPSS_rsapss_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`. @@ -637,10 +640,10 @@ Load a public key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. -@return Returns an allocated public key. Note: caller must take care to `free()` the created key. +@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb) @@ -707,11 +710,11 @@ Load a secret key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. -@return Returns an allocated secret key. Note: caller must take care to `free()` the created key. +@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_skey( @@ -804,13 +807,16 @@ uint64_t /** Sign a message `msg` and write the signature to `sgnt`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param salt Pointer to `saltLen` bytes where the salt is read from. @param msgLen Length of message. @@ -873,11 +879,14 @@ Hacl_RSAPSS_rsapss_skey_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param sgntLen Length of signature. @param sgnt Pointer to `sgntLen` bytes where the signature is read from. diff --git a/src/Hacl_Salsa20.c b/src/Hacl_Salsa20.c index e157d5ef..2758f8a4 100644 --- a/src/Hacl_Salsa20.c +++ b/src/Hacl_Salsa20.c @@ -181,6 +181,7 @@ salsa20_encrypt( memcpy(ctx + (uint32_t)11U, k10, (uint32_t)4U * sizeof (uint32_t)); ctx[15U] = (uint32_t)0x6b206574U; uint32_t k[16U] = { 0U }; + KRML_HOST_IGNORE(k); uint32_t rem = len % (uint32_t)64U; uint32_t nb = len / (uint32_t)64U; uint32_t rem1 = len % (uint32_t)64U; @@ -217,9 +218,8 @@ salsa20_encrypt( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = text + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, text + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k1[16U] = { 0U }; salsa20_core(k1, ctx, nb); uint32_t bl[16U] = { 0U }; @@ -294,6 +294,7 @@ salsa20_decrypt( memcpy(ctx + (uint32_t)11U, k10, (uint32_t)4U * sizeof (uint32_t)); ctx[15U] = (uint32_t)0x6b206574U; uint32_t k[16U] = { 0U }; + KRML_HOST_IGNORE(k); uint32_t rem = len % (uint32_t)64U; uint32_t nb = len / (uint32_t)64U; uint32_t rem1 = len % (uint32_t)64U; @@ -330,9 +331,8 @@ salsa20_decrypt( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = cipher + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k1[16U] = { 0U }; salsa20_core(k1, ctx, nb); uint32_t bl[16U] = { 0U }; diff --git a/src/Hacl_Streaming_Blake2.c b/src/Hacl_Streaming_Blake2.c index 4faa859e..948d56c2 100644 --- a/src/Hacl_Streaming_Blake2.c +++ b/src/Hacl_Streaming_Blake2.c @@ -54,7 +54,6 @@ void Hacl_Streaming_Blake2_blake2s_32_no_key_init(Hacl_Streaming_Blake2_blake2s_ Hacl_Streaming_Blake2_blake2s_32_state scrut = *s1; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2_blake2s_32_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2s_32_blake2s_init(block_state.snd, (uint32_t)0U, (uint32_t)32U); Hacl_Streaming_Blake2_blake2s_32_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -354,7 +353,6 @@ void Hacl_Streaming_Blake2_blake2b_32_no_key_init(Hacl_Streaming_Blake2_blake2b_ Hacl_Streaming_Blake2_blake2b_32_state scrut = *s1; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2_blake2b_32_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2b_32_blake2b_init(block_state.snd, (uint32_t)0U, (uint32_t)64U); Hacl_Streaming_Blake2_blake2b_32_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Streaming_Blake2b_256.c b/src/Hacl_Streaming_Blake2b_256.c index d2df234a..bdb5433f 100644 --- a/src/Hacl_Streaming_Blake2b_256.c +++ b/src/Hacl_Streaming_Blake2b_256.c @@ -66,7 +66,6 @@ Hacl_Streaming_Blake2b_256_blake2b_256_no_key_init( Hacl_Streaming_Blake2b_256_blake2b_256_state scrut = *s; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2b_256_blake2b_256_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2b_256_blake2b_init(block_state.snd, (uint32_t)0U, (uint32_t)64U); Hacl_Streaming_Blake2b_256_blake2b_256_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Streaming_Blake2s_128.c b/src/Hacl_Streaming_Blake2s_128.c index eaace7ce..f97bf5d0 100644 --- a/src/Hacl_Streaming_Blake2s_128.c +++ b/src/Hacl_Streaming_Blake2s_128.c @@ -66,7 +66,6 @@ Hacl_Streaming_Blake2s_128_blake2s_128_no_key_init( Hacl_Streaming_Blake2s_128_blake2s_128_state scrut = *s; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2s_128_blake2s_128_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2s_128_blake2s_init(block_state.snd, (uint32_t)0U, (uint32_t)32U); Hacl_Streaming_Blake2s_128_blake2s_128_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/Hacl_Streaming_Poly1305_128.c b/src/Hacl_Streaming_Poly1305_128.c index c752cfb0..c3f7c19a 100644 --- a/src/Hacl_Streaming_Poly1305_128.c +++ b/src/Hacl_Streaming_Poly1305_128.c @@ -58,7 +58,6 @@ Hacl_Streaming_Poly1305_128_init(uint8_t *k, Hacl_Streaming_Poly1305_128_poly130 uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; Lib_IntVector_Intrinsics_vec128 *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_128_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; @@ -312,7 +311,7 @@ Hacl_Streaming_Poly1305_128_finish( { ite1 = r % (uint32_t)16U; } - uint64_t prev_len_last = total_len - (uint64_t)ite1; + KRML_HOST_IGNORE(total_len - (uint64_t)ite1); uint32_t ite2; if (r % (uint32_t)16U == (uint32_t)0U && r > (uint32_t)0U) { diff --git a/src/Hacl_Streaming_Poly1305_256.c b/src/Hacl_Streaming_Poly1305_256.c index c1915ed9..e56275a4 100644 --- a/src/Hacl_Streaming_Poly1305_256.c +++ b/src/Hacl_Streaming_Poly1305_256.c @@ -58,7 +58,6 @@ Hacl_Streaming_Poly1305_256_init(uint8_t *k, Hacl_Streaming_Poly1305_256_poly130 uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; Lib_IntVector_Intrinsics_vec256 *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_256_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; @@ -312,7 +311,7 @@ Hacl_Streaming_Poly1305_256_finish( { ite1 = r % (uint32_t)16U; } - uint64_t prev_len_last = total_len - (uint64_t)ite1; + KRML_HOST_IGNORE(total_len - (uint64_t)ite1); uint32_t ite2; if (r % (uint32_t)16U == (uint32_t)0U && r > (uint32_t)0U) { diff --git a/src/Hacl_Streaming_Poly1305_32.c b/src/Hacl_Streaming_Poly1305_32.c index 89852727..249a622f 100644 --- a/src/Hacl_Streaming_Poly1305_32.c +++ b/src/Hacl_Streaming_Poly1305_32.c @@ -53,7 +53,6 @@ Hacl_Streaming_Poly1305_32_init(uint8_t *k, Hacl_Streaming_Poly1305_32_poly1305_ uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_32_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; diff --git a/src/msvc/EverCrypt_AEAD.c b/src/msvc/EverCrypt_AEAD.c index 564dbc2e..d3a4ffbe 100644 --- a/src/msvc/EverCrypt_AEAD.c +++ b/src/msvc/EverCrypt_AEAD.c @@ -46,6 +46,8 @@ The state may be reused as many times as desired. */ bool EverCrypt_AEAD_uu___is_Ek(Spec_Agile_AEAD_alg a, EverCrypt_AEAD_state_s projectee) { + KRML_HOST_IGNORE(a); + KRML_HOST_IGNORE(projectee); return true; } @@ -58,8 +60,7 @@ Return the algorithm used in the AEAD state. */ Spec_Agile_AEAD_alg EverCrypt_AEAD_alg_of_state(EverCrypt_AEAD_state_s *s) { - EverCrypt_AEAD_state_s scrut = *s; - Spec_Cipher_Expansion_impl impl = scrut.impl; + Spec_Cipher_Expansion_impl impl = (*s).impl; switch (impl) { case Spec_Cipher_Expansion_Hacl_CHACHA20: @@ -97,6 +98,8 @@ create_in_chacha20_poly1305(EverCrypt_AEAD_state_s **dst, uint8_t *k) static EverCrypt_Error_error_code create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(k); #if HACL_CAN_COMPILE_VALE bool has_aesni = EverCrypt_AutoConfig2_has_aesni(); bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); @@ -108,8 +111,8 @@ create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) uint8_t *ek = (uint8_t *)KRML_HOST_CALLOC((uint32_t)480U, sizeof (uint8_t)); uint8_t *keys_b = ek; uint8_t *hkeys_b = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b); - uint64_t scrut0 = aes128_keyhash_init(keys_b, hkeys_b); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b, hkeys_b)); EverCrypt_AEAD_state_s *p = (EverCrypt_AEAD_state_s *)KRML_HOST_MALLOC(sizeof (EverCrypt_AEAD_state_s)); p[0U] = ((EverCrypt_AEAD_state_s){ .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }); @@ -125,6 +128,8 @@ create_in_aes128_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) static EverCrypt_Error_error_code create_in_aes256_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(k); #if HACL_CAN_COMPILE_VALE bool has_aesni = EverCrypt_AutoConfig2_has_aesni(); bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); @@ -136,8 +141,8 @@ create_in_aes256_gcm(EverCrypt_AEAD_state_s **dst, uint8_t *k) uint8_t *ek = (uint8_t *)KRML_HOST_CALLOC((uint32_t)544U, sizeof (uint8_t)); uint8_t *keys_b = ek; uint8_t *hkeys_b = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b); - uint64_t scrut0 = aes256_keyhash_init(keys_b, hkeys_b); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b, hkeys_b)); EverCrypt_AEAD_state_s *p = (EverCrypt_AEAD_state_s *)KRML_HOST_MALLOC(sizeof (EverCrypt_AEAD_state_s)); p[0U] = ((EverCrypt_AEAD_state_s){ .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }); @@ -203,6 +208,15 @@ encrypt_aes128_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -212,8 +226,7 @@ encrypt_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)304U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -223,8 +236,12 @@ encrypt_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -250,9 +267,7 @@ encrypt_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut0 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -268,7 +283,7 @@ encrypt_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -281,9 +296,7 @@ encrypt_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut0 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -299,7 +312,7 @@ encrypt_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, @@ -327,6 +340,15 @@ encrypt_aes256_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -336,8 +358,7 @@ encrypt_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)368U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -347,8 +368,12 @@ encrypt_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -374,9 +399,7 @@ encrypt_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut0 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -392,7 +415,7 @@ encrypt_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -405,9 +428,7 @@ encrypt_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut0 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -423,7 +444,7 @@ encrypt_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, @@ -525,27 +546,34 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut0 = aes128_key_expansion(k, keys_b0); - uint64_t scrut1 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -555,8 +583,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -582,9 +614,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -600,7 +630,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -613,9 +643,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -631,12 +659,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; #else @@ -669,27 +697,34 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut0 = aes256_key_expansion(k, keys_b0); - uint64_t scrut1 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -699,8 +734,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -726,9 +765,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -744,7 +781,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -757,9 +794,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -775,12 +810,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; #else @@ -805,6 +840,15 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -816,23 +860,21 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut0 = aes128_key_expansion(k, keys_b0); - uint64_t scrut1 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -842,8 +884,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -869,9 +915,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -887,7 +931,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -900,9 +944,7 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm128_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm128_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -918,12 +960,12 @@ EverCrypt_AEAD_encrypt_expand_aes128_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; } @@ -946,6 +988,15 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint8_t *tag ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(plain); + KRML_HOST_IGNORE(plain_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(tag); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -957,23 +1008,21 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut0 = aes256_key_expansion(k, keys_b0); - uint64_t scrut1 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; - EverCrypt_Error_error_code r; if (s == NULL) { - r = EverCrypt_Error_InvalidKey; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidKey); } else if (iv_len == (uint32_t)0U) { - r = EverCrypt_Error_InvalidIVLength; + KRML_HOST_IGNORE(EverCrypt_Error_InvalidIVLength); } else { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -983,8 +1032,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1010,9 +1063,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -1028,7 +1079,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } else { @@ -1041,9 +1092,7 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( uint64_t auth_num = (uint64_t)ad_len / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; - uint64_t - scrut2 = - gcm256_encrypt_opt(auth_b_, + KRML_HOST_IGNORE(gcm256_encrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, keys_b, @@ -1059,12 +1108,12 @@ EverCrypt_AEAD_encrypt_expand_aes256_gcm( inout_b, (uint64_t)plain_len, scratch_b1, - tag); + tag)); } memcpy(cipher + (uint32_t)(uint64_t)plain_len / (uint32_t)16U * (uint32_t)16U, inout_b, (uint32_t)(uint64_t)plain_len % (uint32_t)16U * sizeof (uint8_t)); - r = EverCrypt_Error_Success; + KRML_HOST_IGNORE(EverCrypt_Error_Success); } return EverCrypt_Error_Success; } @@ -1087,12 +1136,12 @@ EverCrypt_AEAD_encrypt_expand_chacha20_poly1305( uint8_t *tag ) { + KRML_HOST_IGNORE(iv_len); uint8_t ek[32U] = { 0U }; EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Hacl_CHACHA20, .ek = ek }; memcpy(ek, k, (uint32_t)32U * sizeof (uint8_t)); EverCrypt_AEAD_state_s *s = &p; - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek0 = scrut.ek; + uint8_t *ek0 = (*s).ek; EverCrypt_Chacha20Poly1305_aead_encrypt(ek0, iv, ad_len, ad, plain_len, plain, cipher, tag); return EverCrypt_Error_Success; } @@ -1173,6 +1222,15 @@ decrypt_aes128_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -1182,8 +1240,7 @@ decrypt_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)304U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -1193,8 +1250,12 @@ decrypt_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1222,7 +1283,7 @@ decrypt_aes128_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut0 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1240,7 +1301,6 @@ decrypt_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } else @@ -1255,7 +1315,7 @@ decrypt_aes128_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut0 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1273,7 +1333,6 @@ decrypt_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1307,6 +1366,15 @@ decrypt_aes256_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(s); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE if (s == NULL) { @@ -1316,8 +1384,7 @@ decrypt_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint8_t *scratch_b = ek + (uint32_t)368U; uint8_t *ek1 = ek; uint8_t *keys_b = ek1; @@ -1327,8 +1394,12 @@ decrypt_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1356,7 +1427,7 @@ decrypt_aes256_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut0 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1374,7 +1445,6 @@ decrypt_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } else @@ -1389,7 +1459,7 @@ decrypt_aes256_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut0 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1407,7 +1477,6 @@ decrypt_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut0; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1449,8 +1518,7 @@ decrypt_chacha20_poly1305( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; uint32_t r = EverCrypt_Chacha20Poly1305_aead_decrypt(ek, iv, ad_len, ad, cipher_len, dst, cipher, tag); if (r == (uint32_t)0U) @@ -1508,8 +1576,7 @@ EverCrypt_AEAD_decrypt( { return EverCrypt_Error_InvalidKey; } - EverCrypt_AEAD_state_s scrut = *s; - Spec_Cipher_Expansion_impl i = scrut.impl; + Spec_Cipher_Expansion_impl i = (*s).impl; switch (i) { case Spec_Cipher_Expansion_Vale_AES128: @@ -1553,12 +1620,21 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b0); - uint64_t scrut0 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1569,8 +1645,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1580,8 +1655,12 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1609,7 +1688,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1627,7 +1706,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1642,7 +1720,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1660,7 +1738,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1702,12 +1779,21 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b0); - uint64_t scrut0 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1718,8 +1804,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1729,8 +1814,12 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1758,7 +1847,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1776,7 +1865,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1791,7 +1879,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1809,7 +1897,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1843,6 +1930,15 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -1854,8 +1950,8 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint8_t ek[480U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)176U; - uint64_t scrut = aes128_key_expansion(k, keys_b0); - uint64_t scrut0 = aes128_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes128_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes128_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES128, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -1866,8 +1962,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)304U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -1877,8 +1972,12 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -1906,7 +2005,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1924,7 +2023,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -1939,7 +2037,7 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm128_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -1957,7 +2055,6 @@ EverCrypt_AEAD_decrypt_expand_aes128_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -1989,6 +2086,15 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint8_t *dst ) { + KRML_HOST_IGNORE(k); + KRML_HOST_IGNORE(iv); + KRML_HOST_IGNORE(iv_len); + KRML_HOST_IGNORE(ad); + KRML_HOST_IGNORE(ad_len); + KRML_HOST_IGNORE(cipher); + KRML_HOST_IGNORE(cipher_len); + KRML_HOST_IGNORE(tag); + KRML_HOST_IGNORE(dst); #if HACL_CAN_COMPILE_VALE bool has_pclmulqdq = EverCrypt_AutoConfig2_has_pclmulqdq(); bool has_avx = EverCrypt_AutoConfig2_has_avx(); @@ -2000,8 +2106,8 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint8_t ek[544U] = { 0U }; uint8_t *keys_b0 = ek; uint8_t *hkeys_b0 = ek + (uint32_t)240U; - uint64_t scrut = aes256_key_expansion(k, keys_b0); - uint64_t scrut0 = aes256_keyhash_init(keys_b0, hkeys_b0); + KRML_HOST_IGNORE(aes256_key_expansion(k, keys_b0)); + KRML_HOST_IGNORE(aes256_keyhash_init(keys_b0, hkeys_b0)); EverCrypt_AEAD_state_s p = { .impl = Spec_Cipher_Expansion_Vale_AES256, .ek = ek }; EverCrypt_AEAD_state_s *s = &p; if (s == NULL) @@ -2012,8 +2118,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( { return EverCrypt_Error_InvalidIVLength; } - EverCrypt_AEAD_state_s scrut1 = *s; - uint8_t *ek0 = scrut1.ek; + uint8_t *ek0 = (*s).ek; uint8_t *scratch_b = ek0 + (uint32_t)368U; uint8_t *ek1 = ek0; uint8_t *keys_b = ek1; @@ -2023,8 +2128,12 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint32_t bytes_len = len * (uint32_t)16U; uint8_t *iv_b = iv; memcpy(tmp_iv, iv + bytes_len, iv_len % (uint32_t)16U * sizeof (uint8_t)); - uint64_t - uu____0 = compute_iv_stdcall(iv_b, (uint64_t)iv_len, (uint64_t)len, tmp_iv, tmp_iv, hkeys_b); + KRML_HOST_IGNORE(compute_iv_stdcall(iv_b, + (uint64_t)iv_len, + (uint64_t)len, + tmp_iv, + tmp_iv, + hkeys_b)); uint8_t *inout_b = scratch_b; uint8_t *abytes_b = scratch_b + (uint32_t)16U; uint8_t *scratch_b1 = scratch_b + (uint32_t)32U; @@ -2052,7 +2161,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint64_t len128x6_ = len128x6 / (uint64_t)16U; uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -2070,7 +2179,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } else @@ -2085,7 +2193,7 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( uint64_t len128_num_ = len128_num / (uint64_t)16U; uint64_t len128x6_ = (uint64_t)0U; uint64_t - scrut2 = + c0 = gcm256_decrypt_opt(auth_b_, (uint64_t)ad_len, auth_num, @@ -2103,7 +2211,6 @@ EverCrypt_AEAD_decrypt_expand_aes256_gcm( (uint64_t)cipher_len, scratch_b1, tag); - uint64_t c0 = scrut2; c = c0; } memcpy(dst + (uint32_t)(uint64_t)cipher_len / (uint32_t)16U * (uint32_t)16U, @@ -2214,8 +2321,7 @@ Cleanup and free the AEAD state. */ void EverCrypt_AEAD_free(EverCrypt_AEAD_state_s *s) { - EverCrypt_AEAD_state_s scrut = *s; - uint8_t *ek = scrut.ek; + uint8_t *ek = (*s).ek; KRML_HOST_FREE(ek); KRML_HOST_FREE(s); } diff --git a/src/msvc/EverCrypt_AutoConfig2.c b/src/msvc/EverCrypt_AutoConfig2.c index fe93ef8a..b549d020 100644 --- a/src/msvc/EverCrypt_AutoConfig2.c +++ b/src/msvc/EverCrypt_AutoConfig2.c @@ -113,75 +113,59 @@ void EverCrypt_AutoConfig2_recall(void) void EverCrypt_AutoConfig2_init(void) { #if HACL_CAN_COMPILE_VALE - uint64_t scrut = check_aesni(); - if (scrut != (uint64_t)0U) + if (check_aesni() != (uint64_t)0U) { cpu_has_aesni[0U] = true; cpu_has_pclmulqdq[0U] = true; } - uint64_t scrut0 = check_sha(); - if (scrut0 != (uint64_t)0U) + if (check_sha() != (uint64_t)0U) { cpu_has_shaext[0U] = true; } - uint64_t scrut1 = check_adx_bmi2(); - if (scrut1 != (uint64_t)0U) + if (check_adx_bmi2() != (uint64_t)0U) { cpu_has_bmi2[0U] = true; cpu_has_adx[0U] = true; } - uint64_t scrut2 = check_avx(); - if (scrut2 != (uint64_t)0U) + if (check_avx() != (uint64_t)0U) { - uint64_t scrut3 = check_osxsave(); - if (scrut3 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut4 = check_avx_xcr0(); - if (scrut4 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { cpu_has_avx[0U] = true; } } } - uint64_t scrut3 = check_avx2(); - if (scrut3 != (uint64_t)0U) + if (check_avx2() != (uint64_t)0U) { - uint64_t scrut4 = check_osxsave(); - if (scrut4 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut5 = check_avx_xcr0(); - if (scrut5 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { cpu_has_avx2[0U] = true; } } } - uint64_t scrut4 = check_sse(); - if (scrut4 != (uint64_t)0U) + if (check_sse() != (uint64_t)0U) { cpu_has_sse[0U] = true; } - uint64_t scrut5 = check_movbe(); - if (scrut5 != (uint64_t)0U) + if (check_movbe() != (uint64_t)0U) { cpu_has_movbe[0U] = true; } - uint64_t scrut6 = check_rdrand(); - if (scrut6 != (uint64_t)0U) + if (check_rdrand() != (uint64_t)0U) { cpu_has_rdrand[0U] = true; } - uint64_t scrut7 = check_avx512(); - if (scrut7 != (uint64_t)0U) + if (check_avx512() != (uint64_t)0U) { - uint64_t scrut8 = check_osxsave(); - if (scrut8 != (uint64_t)0U) + if (check_osxsave() != (uint64_t)0U) { - uint64_t scrut9 = check_avx_xcr0(); - if (scrut9 != (uint64_t)0U) + if (check_avx_xcr0() != (uint64_t)0U) { - uint64_t scrut10 = check_avx512_xcr0(); - if (scrut10 != (uint64_t)0U) + if (check_avx512_xcr0() != (uint64_t)0U) { cpu_has_avx512[0U] = true; return; diff --git a/src/msvc/EverCrypt_DRBG.c b/src/msvc/EverCrypt_DRBG.c index 243d8eb4..9591823c 100644 --- a/src/msvc/EverCrypt_DRBG.c +++ b/src/msvc/EverCrypt_DRBG.c @@ -92,6 +92,7 @@ EverCrypt_DRBG_uu___is_SHA1_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA1_s) { return true; @@ -105,6 +106,7 @@ EverCrypt_DRBG_uu___is_SHA2_256_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_256_s) { return true; @@ -118,6 +120,7 @@ EverCrypt_DRBG_uu___is_SHA2_384_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_384_s) { return true; @@ -131,6 +134,7 @@ EverCrypt_DRBG_uu___is_SHA2_512_s( EverCrypt_DRBG_state_s projectee ) { + KRML_HOST_IGNORE(uu___); if (projectee.tag == SHA2_512_s) { return true; diff --git a/src/msvc/EverCrypt_Hash.c b/src/msvc/EverCrypt_Hash.c index 914a105f..b88df9e2 100644 --- a/src/msvc/EverCrypt_Hash.c +++ b/src/msvc/EverCrypt_Hash.c @@ -399,7 +399,7 @@ void EverCrypt_Hash_update_multi_256(uint32_t *s, uint8_t *blocks, uint32_t n) if (has_shaext && has_sse) { uint64_t n1 = (uint64_t)n; - uint64_t scrut = sha256_update(s, blocks, n1, k224_256); + KRML_HOST_IGNORE(sha256_update(s, blocks, n1, k224_256)); return; } Hacl_SHA2_Scalar32_sha256_update_nblocks(n * (uint32_t)64U, blocks, s); @@ -2156,8 +2156,7 @@ Perform a run-time test to determine which algorithm was chosen for the given pi Spec_Hash_Definitions_hash_alg EverCrypt_Hash_Incremental_alg_of_state(EverCrypt_Hash_Incremental_hash_state *s) { - EverCrypt_Hash_Incremental_hash_state scrut = *s; - EverCrypt_Hash_state_s *block_state = scrut.block_state; + EverCrypt_Hash_state_s *block_state = (*s).block_state; return alg_of_state(block_state); } diff --git a/src/msvc/EverCrypt_Poly1305.c b/src/msvc/EverCrypt_Poly1305.c index 717b9527..454c0fce 100644 --- a/src/msvc/EverCrypt_Poly1305.c +++ b/src/msvc/EverCrypt_Poly1305.c @@ -28,8 +28,13 @@ #include "internal/Vale.h" #include "config.h" -static void poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key) +KRML_MAYBE_UNUSED static void +poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key) { + KRML_HOST_IGNORE(dst); + KRML_HOST_IGNORE(src); + KRML_HOST_IGNORE(len); + KRML_HOST_IGNORE(key); #if HACL_CAN_COMPILE_VALE uint8_t ctx[192U] = { 0U }; memcpy(ctx + (uint32_t)24U, key, (uint32_t)32U * sizeof (uint8_t)); @@ -38,19 +43,16 @@ static void poly1305_vale(uint8_t *dst, uint8_t *src, uint32_t len, uint8_t *key uint8_t tmp[16U] = { 0U }; if (n_extra == (uint32_t)0U) { - uint64_t scrut = x64_poly1305(ctx, src, (uint64_t)len, (uint64_t)1U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, src, (uint64_t)len, (uint64_t)1U)); } else { uint32_t len16 = n_blocks * (uint32_t)16U; uint8_t *src16 = src; memcpy(tmp, src + len16, n_extra * sizeof (uint8_t)); - uint64_t scrut = x64_poly1305(ctx, src16, (uint64_t)len16, (uint64_t)0U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, src16, (uint64_t)len16, (uint64_t)0U)); memcpy(ctx + (uint32_t)24U, key, (uint32_t)32U * sizeof (uint8_t)); - uint64_t scrut0 = x64_poly1305(ctx, tmp, (uint64_t)n_extra, (uint64_t)1U); - KRML_HOST_IGNORE((void *)(uint8_t)0U); + KRML_HOST_IGNORE(x64_poly1305(ctx, tmp, (uint64_t)n_extra, (uint64_t)1U)); } memcpy(dst, ctx, (uint32_t)16U * sizeof (uint8_t)); #endif diff --git a/src/msvc/Hacl_Chacha20_Vec128.c b/src/msvc/Hacl_Chacha20_Vec128.c index ed112654..1e0c4ec1 100644 --- a/src/msvc/Hacl_Chacha20_Vec128.c +++ b/src/msvc/Hacl_Chacha20_Vec128.c @@ -370,9 +370,8 @@ Hacl_Chacha20_Vec128_chacha20_encrypt_128( 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 (uint8_t)); + memcpy(plain, text + nb * (uint32_t)256U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; chacha20_core_128(k, ctx, nb); Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; @@ -676,9 +675,8 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128( 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 (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)256U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(16) Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; chacha20_core_128(k, ctx, nb); Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; diff --git a/src/msvc/Hacl_Chacha20_Vec256.c b/src/msvc/Hacl_Chacha20_Vec256.c index 2df300b6..620f5040 100644 --- a/src/msvc/Hacl_Chacha20_Vec256.c +++ b/src/msvc/Hacl_Chacha20_Vec256.c @@ -470,9 +470,8 @@ Hacl_Chacha20_Vec256_chacha20_encrypt_256( 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 (uint8_t)); + memcpy(plain, text + nb * (uint32_t)512U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; chacha20_core_256(k, ctx, nb); Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; @@ -968,9 +967,8 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256( 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 (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)512U, rem * sizeof (uint8_t)); KRML_PRE_ALIGN(32) Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; chacha20_core_256(k, ctx, nb); Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; diff --git a/src/msvc/Hacl_Chacha20_Vec32.c b/src/msvc/Hacl_Chacha20_Vec32.c index 6f137f39..2bf4764c 100644 --- a/src/msvc/Hacl_Chacha20_Vec32.c +++ b/src/msvc/Hacl_Chacha20_Vec32.c @@ -229,9 +229,8 @@ Hacl_Chacha20_Vec32_chacha20_encrypt_32( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = text + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, text + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k[16U] = { 0U }; chacha20_core_32(k, ctx, nb); KRML_MAYBE_FOR16(i, @@ -279,9 +278,8 @@ Hacl_Chacha20_Vec32_chacha20_decrypt_32( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = cipher + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k[16U] = { 0U }; chacha20_core_32(k, ctx, nb); KRML_MAYBE_FOR16(i, diff --git a/src/msvc/Hacl_Curve25519_64.c b/src/msvc/Hacl_Curve25519_64.c index 526fbd22..fb0974fe 100644 --- a/src/msvc/Hacl_Curve25519_64.c +++ b/src/msvc/Hacl_Curve25519_64.c @@ -35,7 +35,7 @@ static inline void add_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2) #if HACL_CAN_COMPILE_INLINE_ASM add_scalar(out, f1, f2); #else - uint64_t uu____0 = add_scalar_e(out, f1, f2); + KRML_HOST_IGNORE(add_scalar_e(out, f1, f2)); #endif } @@ -44,7 +44,7 @@ static inline void fadd0(uint64_t *out, uint64_t *f1, uint64_t *f2) #if HACL_CAN_COMPILE_INLINE_ASM fadd(out, f1, f2); #else - uint64_t uu____0 = fadd_e(out, f1, f2); + KRML_HOST_IGNORE(fadd_e(out, f1, f2)); #endif } @@ -53,7 +53,7 @@ static inline void fsub0(uint64_t *out, uint64_t *f1, uint64_t *f2) #if HACL_CAN_COMPILE_INLINE_ASM fsub(out, f1, f2); #else - uint64_t uu____0 = fsub_e(out, f1, f2); + KRML_HOST_IGNORE(fsub_e(out, f1, f2)); #endif } @@ -62,7 +62,7 @@ static inline void fmul0(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *tm #if HACL_CAN_COMPILE_INLINE_ASM fmul(out, f1, f2, tmp); #else - uint64_t uu____0 = fmul_e(tmp, f1, out, f2); + KRML_HOST_IGNORE(fmul_e(tmp, f1, out, f2)); #endif } @@ -71,7 +71,7 @@ static inline void fmul20(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *t #if HACL_CAN_COMPILE_INLINE_ASM fmul2(out, f1, f2, tmp); #else - uint64_t uu____0 = fmul2_e(tmp, f1, out, f2); + KRML_HOST_IGNORE(fmul2_e(tmp, f1, out, f2)); #endif } @@ -80,7 +80,7 @@ static inline void fmul_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2) #if HACL_CAN_COMPILE_INLINE_ASM fmul_scalar(out, f1, f2); #else - uint64_t uu____0 = fmul_scalar_e(out, f1, f2); + KRML_HOST_IGNORE(fmul_scalar_e(out, f1, f2)); #endif } @@ -89,7 +89,7 @@ static inline void fsqr0(uint64_t *out, uint64_t *f1, uint64_t *tmp) #if HACL_CAN_COMPILE_INLINE_ASM fsqr(out, f1, tmp); #else - uint64_t uu____0 = fsqr_e(tmp, f1, out); + KRML_HOST_IGNORE(fsqr_e(tmp, f1, out)); #endif } @@ -98,7 +98,7 @@ static inline void fsqr20(uint64_t *out, uint64_t *f, uint64_t *tmp) #if HACL_CAN_COMPILE_INLINE_ASM fsqr2(out, f, tmp); #else - uint64_t uu____0 = fsqr2_e(tmp, f, out); + KRML_HOST_IGNORE(fsqr2_e(tmp, f, out)); #endif } @@ -107,7 +107,7 @@ static inline void cswap20(uint64_t bit, uint64_t *p1, uint64_t *p2) #if HACL_CAN_COMPILE_INLINE_ASM cswap2(bit, p1, p2); #else - uint64_t uu____0 = cswap2_e(bit, p1, p2); + KRML_HOST_IGNORE(cswap2_e(bit, p1, p2)); #endif } diff --git a/src/msvc/Hacl_Ed25519.c b/src/msvc/Hacl_Ed25519.c index 9d7c3bd4..f9881e91 100644 --- a/src/msvc/Hacl_Ed25519.c +++ b/src/msvc/Hacl_Ed25519.c @@ -711,65 +711,53 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) FStar_UInt128_uint128 c00 = carry0; FStar_UInt128_uint128 carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z11, c00), (uint32_t)56U); - uint64_t - t100 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z11, c00)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c10 = carry1; FStar_UInt128_uint128 carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z21, c10), (uint32_t)56U); - uint64_t - t101 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z21, c10)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c20 = carry2; FStar_UInt128_uint128 carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z31, c20), (uint32_t)56U); - uint64_t - t102 = - FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z31, c20)) - & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c30 = carry3; FStar_UInt128_uint128 carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z41, c30), (uint32_t)56U); uint64_t - t103 = + t100 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z41, c30)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c40 = carry4; - uint64_t t410 = t103; + uint64_t t410 = t100; FStar_UInt128_uint128 carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z5, c40), (uint32_t)56U); uint64_t - t104 = + t101 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z5, c40)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c5 = carry5; - uint64_t t51 = t104; + uint64_t t51 = t101; FStar_UInt128_uint128 carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z6, c5), (uint32_t)56U); uint64_t - t105 = + t102 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z6, c5)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c6 = carry6; - uint64_t t61 = t105; + uint64_t t61 = t102; FStar_UInt128_uint128 carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z7, c6), (uint32_t)56U); uint64_t - t106 = + t103 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z7, c6)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c7 = carry7; - uint64_t t71 = t106; + uint64_t t71 = t103; FStar_UInt128_uint128 carry8 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z8, c7), (uint32_t)56U); uint64_t - t107 = + t104 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z8, c7)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c8 = carry8; - uint64_t t81 = t107; + uint64_t t81 = t104; uint64_t t91 = FStar_UInt128_uint128_to_uint64(c8); uint64_t qmu4_ = t410; uint64_t qmu5_ = t51; @@ -818,19 +806,19 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(qdiv3, m1); FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(qdiv4, m0); FStar_UInt128_uint128 carry9 = FStar_UInt128_shift_right(xy00, (uint32_t)56U); - uint64_t t108 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU; + uint64_t t105 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c0 = carry9; - uint64_t t010 = t108; + uint64_t t010 = t105; FStar_UInt128_uint128 carry10 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0), (uint32_t)56U); uint64_t - t109 = + t106 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c11 = carry10; - uint64_t t110 = t109; + uint64_t t110 = t106; FStar_UInt128_uint128 carry11 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, @@ -839,14 +827,14 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c11), (uint32_t)56U); uint64_t - t1010 = + t107 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, xy11), xy20), c11)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c21 = carry11; - uint64_t t210 = t1010; + uint64_t t210 = t107; FStar_UInt128_uint128 carry = FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, @@ -856,7 +844,7 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c21), (uint32_t)56U); uint64_t - t1011 = + t108 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, xy12), xy21), @@ -864,7 +852,7 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) c21)) & (uint64_t)0xffffffffffffffU; FStar_UInt128_uint128 c31 = carry; - uint64_t t310 = t1011; + uint64_t t310 = t108; uint64_t t411 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04, @@ -880,24 +868,24 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) uint64_t qmul3 = t310; uint64_t qmul4 = t411; uint64_t b5 = (r0 - qmul0) >> (uint32_t)63U; - uint64_t t1012 = (b5 << (uint32_t)56U) + r0 - qmul0; + uint64_t t109 = (b5 << (uint32_t)56U) + r0 - qmul0; uint64_t c1 = b5; - uint64_t t011 = t1012; + uint64_t t011 = t109; uint64_t b6 = (r1 - (qmul1 + c1)) >> (uint32_t)63U; - uint64_t t1013 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1); + uint64_t t1010 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1); uint64_t c2 = b6; - uint64_t t111 = t1013; + uint64_t t111 = t1010; uint64_t b7 = (r2 - (qmul2 + c2)) >> (uint32_t)63U; - uint64_t t1014 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2); + uint64_t t1011 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2); uint64_t c3 = b7; - uint64_t t211 = t1014; + uint64_t t211 = t1011; uint64_t b8 = (r3 - (qmul3 + c3)) >> (uint32_t)63U; - uint64_t t1015 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3); + uint64_t t1012 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3); uint64_t c4 = b8; - uint64_t t311 = t1015; + uint64_t t311 = t1012; uint64_t b9 = (r4 - (qmul4 + c4)) >> (uint32_t)63U; - uint64_t t1016 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4); - uint64_t t412 = t1016; + uint64_t t1013 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4); + uint64_t t412 = t1013; uint64_t s0 = t011; uint64_t s1 = t111; uint64_t s2 = t211; @@ -914,21 +902,21 @@ static inline void barrett_reduction(uint64_t *z, uint64_t *t) uint64_t y3 = m31; uint64_t y4 = m41; uint64_t b10 = (s0 - y0) >> (uint32_t)63U; - uint64_t t1017 = (b10 << (uint32_t)56U) + s0 - y0; + uint64_t t1014 = (b10 << (uint32_t)56U) + s0 - y0; uint64_t b0 = b10; - uint64_t t01 = t1017; + uint64_t t01 = t1014; uint64_t b11 = (s1 - (y1 + b0)) >> (uint32_t)63U; - uint64_t t1018 = (b11 << (uint32_t)56U) + s1 - (y1 + b0); + uint64_t t1015 = (b11 << (uint32_t)56U) + s1 - (y1 + b0); uint64_t b1 = b11; - uint64_t t11 = t1018; + uint64_t t11 = t1015; uint64_t b12 = (s2 - (y2 + b1)) >> (uint32_t)63U; - uint64_t t1019 = (b12 << (uint32_t)56U) + s2 - (y2 + b1); + uint64_t t1016 = (b12 << (uint32_t)56U) + s2 - (y2 + b1); uint64_t b2 = b12; - uint64_t t21 = t1019; + uint64_t t21 = t1016; uint64_t b13 = (s3 - (y3 + b2)) >> (uint32_t)63U; - uint64_t t1020 = (b13 << (uint32_t)56U) + s3 - (y3 + b2); + uint64_t t1017 = (b13 << (uint32_t)56U) + s3 - (y3 + b2); uint64_t b3 = b13; - uint64_t t31 = t1020; + uint64_t t31 = t1017; uint64_t b = (s4 - (y4 + b3)) >> (uint32_t)63U; uint64_t t10 = (b << (uint32_t)56U) + s4 - (y4 + b3); uint64_t b4 = b; diff --git a/src/msvc/Hacl_FFDHE.c b/src/msvc/Hacl_FFDHE.c index 53b87f73..bc77dbdc 100644 --- a/src/msvc/Hacl_FFDHE.c +++ b/src/msvc/Hacl_FFDHE.c @@ -127,7 +127,6 @@ static inline uint64_t ffdhe_check_pk(Spec_FFDHE_ffdhe_alg a, uint64_t *pk_n, ui memset(p_n1, 0U, nLen * sizeof (uint64_t)); uint64_t c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64((uint64_t)0U, p_n[0U], (uint64_t)1U, p_n1); - uint64_t c1; if ((uint32_t)1U < nLen) { uint64_t *a1 = p_n + (uint32_t)1U; @@ -159,12 +158,12 @@ static inline uint64_t ffdhe_check_pk(Spec_FFDHE_ffdhe_alg a, uint64_t *pk_n, ui uint64_t *res_i = res1 + i; c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, (uint64_t)0U, res_i); } - uint64_t c10 = c; - c1 = c10; + uint64_t c1 = c; + KRML_HOST_IGNORE(c1); } else { - c1 = c0; + KRML_HOST_IGNORE(c0); } KRML_CHECK_SIZE(sizeof (uint64_t), nLen); uint64_t *b2 = (uint64_t *)alloca(nLen * sizeof (uint64_t)); diff --git a/src/msvc/Hacl_Frodo_KEM.c b/src/msvc/Hacl_Frodo_KEM.c index 13db363a..4265ac0e 100644 --- a/src/msvc/Hacl_Frodo_KEM.c +++ b/src/msvc/Hacl_Frodo_KEM.c @@ -30,6 +30,6 @@ void randombytes_(uint32_t len, uint8_t *res) { - bool b = Lib_RandomBuffer_System_randombytes(res, len); + KRML_HOST_IGNORE(Lib_RandomBuffer_System_randombytes(res, len)); } diff --git a/src/msvc/Hacl_HMAC_DRBG.c b/src/msvc/Hacl_HMAC_DRBG.c index 93e47dc9..b3acf354 100644 --- a/src/msvc/Hacl_HMAC_DRBG.c +++ b/src/msvc/Hacl_HMAC_DRBG.c @@ -71,6 +71,8 @@ uint32_t Hacl_HMAC_DRBG_min_length(Spec_Hash_Definitions_hash_alg a) bool Hacl_HMAC_DRBG_uu___is_State(Spec_Hash_Definitions_hash_alg a, Hacl_HMAC_DRBG_state projectee) { + KRML_HOST_IGNORE(a); + KRML_HOST_IGNORE(projectee); return true; } @@ -1104,6 +1106,7 @@ Hacl_HMAC_DRBG_generate( void Hacl_HMAC_DRBG_free(Spec_Hash_Definitions_hash_alg uu___, Hacl_HMAC_DRBG_state s) { + KRML_HOST_IGNORE(uu___); uint8_t *k = s.k; uint8_t *v = s.v; uint32_t *ctr = s.reseed_counter; diff --git a/src/msvc/Hacl_Hash_Blake2.c b/src/msvc/Hacl_Hash_Blake2.c index 194e7157..aecc6165 100644 --- a/src/msvc/Hacl_Hash_Blake2.c +++ b/src/msvc/Hacl_Hash_Blake2.c @@ -545,6 +545,7 @@ Hacl_Blake2b_32_blake2b_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { FStar_UInt128_uint128 @@ -1192,6 +1193,7 @@ Hacl_Blake2s_32_blake2s_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { uint64_t totlen = prev + (uint64_t)((i + (uint32_t)1U) * (uint32_t)64U); diff --git a/src/msvc/Hacl_Hash_Blake2b_256.c b/src/msvc/Hacl_Hash_Blake2b_256.c index d0df7cd8..b37ffc5f 100644 --- a/src/msvc/Hacl_Hash_Blake2b_256.c +++ b/src/msvc/Hacl_Hash_Blake2b_256.c @@ -268,6 +268,7 @@ Hacl_Blake2b_256_blake2b_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { FStar_UInt128_uint128 diff --git a/src/msvc/Hacl_Hash_Blake2s_128.c b/src/msvc/Hacl_Hash_Blake2s_128.c index 5bf06711..86c4f030 100644 --- a/src/msvc/Hacl_Hash_Blake2s_128.c +++ b/src/msvc/Hacl_Hash_Blake2s_128.c @@ -268,6 +268,7 @@ Hacl_Blake2s_128_blake2s_update_multi( uint32_t nb ) { + KRML_HOST_IGNORE(len); for (uint32_t i = (uint32_t)0U; i < nb; i++) { uint64_t totlen = prev + (uint64_t)((i + (uint32_t)1U) * (uint32_t)64U); diff --git a/src/msvc/Hacl_Hash_MD5.c b/src/msvc/Hacl_Hash_MD5.c index 1b376960..222ac824 100644 --- a/src/msvc/Hacl_Hash_MD5.c +++ b/src/msvc/Hacl_Hash_MD5.c @@ -1218,7 +1218,6 @@ void Hacl_Streaming_MD5_legacy_init(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Hash_Core_MD5_legacy_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Hash_SHA1.c b/src/msvc/Hacl_Hash_SHA1.c index 80edc004..5ecb3c0b 100644 --- a/src/msvc/Hacl_Hash_SHA1.c +++ b/src/msvc/Hacl_Hash_SHA1.c @@ -254,7 +254,6 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Hash_Core_SHA1_legacy_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Hash_SHA2.c b/src/msvc/Hacl_Hash_SHA2.c index 46fde83f..c93c3616 100644 --- a/src/msvc/Hacl_Hash_SHA2.c +++ b/src/msvc/Hacl_Hash_SHA2.c @@ -537,7 +537,6 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha256_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -836,7 +835,6 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) Hacl_Streaming_MD_state_32 scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha224_init(block_state); Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -962,7 +960,6 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) Hacl_Streaming_MD_state_64 scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha512_init(block_state); Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -1262,7 +1259,6 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) Hacl_Streaming_MD_state_64 scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_SHA2_Scalar32_sha384_init(block_state); Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Hash_SHA3.c b/src/msvc/Hacl_Hash_SHA3.c index 5f4707f4..19d13b1b 100644 --- a/src/msvc/Hacl_Hash_SHA3.c +++ b/src/msvc/Hacl_Hash_SHA3.c @@ -125,10 +125,9 @@ Hacl_Hash_SHA3_update_last_sha3( if (input_len == len) { Hacl_Impl_SHA3_absorb_inner(len, input, s); - uint8_t *uu____0 = input + input_len; uint8_t lastBlock_[200U] = { 0U }; uint8_t *lastBlock = lastBlock_; - memcpy(lastBlock, uu____0, (uint32_t)0U * sizeof (uint8_t)); + memcpy(lastBlock, input + input_len, (uint32_t)0U * sizeof (uint8_t)); lastBlock[0U] = suffix; Hacl_Impl_SHA3_loadState(len, lastBlock, s); if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && (uint32_t)0U == len - (uint32_t)1U) @@ -167,8 +166,7 @@ hash_buf2; Spec_Hash_Definitions_hash_alg Hacl_Streaming_Keccak_get_alg(Hacl_Streaming_Keccak_state *s) { - Hacl_Streaming_Keccak_state scrut = *s; - Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state; + Hacl_Streaming_Keccak_hash_buf block_state = (*s).block_state; return block_state.fst; } @@ -809,6 +807,7 @@ Hacl_Impl_SHA3_keccak( uint8_t *output ) { + KRML_HOST_IGNORE(capacity); uint32_t rateInBytes = rate / (uint32_t)8U; uint64_t s[25U] = { 0U }; absorb(s, rateInBytes, inputByteLen, input, delimitedSuffix); diff --git a/src/msvc/Hacl_K256_ECDSA.c b/src/msvc/Hacl_K256_ECDSA.c index 19395653..c5dda43f 100644 --- a/src/msvc/Hacl_K256_ECDSA.c +++ b/src/msvc/Hacl_K256_ECDSA.c @@ -498,7 +498,7 @@ mul_pow2_256_minus_q_add( uint64_t r = c; tmp[len + i0] = r;); memcpy(res + (uint32_t)2U, a, len * sizeof (uint64_t)); - uint64_t uu____0 = bn_add(resLen, res, len + (uint32_t)2U, tmp, res); + KRML_HOST_IGNORE(bn_add(resLen, res, len + (uint32_t)2U, tmp, res)); uint64_t c = bn_add(resLen, res, (uint32_t)4U, e, res); return c; } @@ -514,15 +514,23 @@ static inline void modq(uint64_t *out, uint64_t *a) uint64_t *t01 = tmp; uint64_t m[7U] = { 0U }; uint64_t p[5U] = { 0U }; - uint64_t - c0 = mul_pow2_256_minus_q_add((uint32_t)4U, (uint32_t)7U, t01, a + (uint32_t)4U, a, m); - uint64_t - c10 = mul_pow2_256_minus_q_add((uint32_t)3U, (uint32_t)5U, t01, m + (uint32_t)4U, m, p); + KRML_HOST_IGNORE(mul_pow2_256_minus_q_add((uint32_t)4U, + (uint32_t)7U, + t01, + a + (uint32_t)4U, + a, + m)); + KRML_HOST_IGNORE(mul_pow2_256_minus_q_add((uint32_t)3U, + (uint32_t)5U, + t01, + m + (uint32_t)4U, + m, + p)); uint64_t c2 = mul_pow2_256_minus_q_add((uint32_t)1U, (uint32_t)4U, t01, p + (uint32_t)4U, p, r); - uint64_t c00 = c2; + uint64_t c0 = c2; uint64_t c1 = add4(r, tmp, out); - uint64_t mask = (uint64_t)0U - (c00 + c1); + uint64_t mask = (uint64_t)0U - (c0 + c1); KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, @@ -612,7 +620,7 @@ static inline void qmul_shift_384(uint64_t *res, uint64_t *a, uint64_t *b) uint64_t *res_i = res1 + i; c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, (uint64_t)0U, res_i);); uint64_t c1 = c; - uint64_t uu____0 = c1; + KRML_HOST_IGNORE(c1); uint64_t flag = l[5U] >> (uint32_t)63U; uint64_t mask = (uint64_t)0U - flag; KRML_MAYBE_FOR4(i, @@ -1223,6 +1231,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)118285133003718U, (uint64_t)434519962075150U, (uint64_t)1114612377498854U, (uint64_t)3488596944003813U, (uint64_t)450716531072892U, (uint64_t)66044973203836U }; + KRML_HOST_IGNORE(q2); uint64_t q3[15U] = { @@ -1232,6 +1241,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)265969268774814U, (uint64_t)1913228635640715U, (uint64_t)2831959046949342U, (uint64_t)888030405442963U, (uint64_t)1817092932985033U, (uint64_t)101515844997121U }; + KRML_HOST_IGNORE(q3); uint64_t q4[15U] = { @@ -1241,6 +1251,7 @@ static inline void point_mul_g(uint64_t *out, uint64_t *scalar) (uint64_t)12245672982162U, (uint64_t)2119364213800870U, (uint64_t)2034960311715107U, (uint64_t)3172697815804487U, (uint64_t)4185144850224160U, (uint64_t)2792055915674U }; + KRML_HOST_IGNORE(q4); uint64_t *r1 = scalar; uint64_t *r2 = scalar + (uint32_t)1U; uint64_t *r3 = scalar + (uint32_t)2U; @@ -1605,6 +1616,7 @@ Hacl_K256_ECDSA_ecdsa_sign_hashed_msg( ) { uint64_t oneq[4U] = { (uint64_t)0x1U, (uint64_t)0x0U, (uint64_t)0x0U, (uint64_t)0x0U }; + KRML_HOST_IGNORE(oneq); uint64_t rsdk_q[16U] = { 0U }; uint64_t *r_q = rsdk_q; uint64_t *s_q = rsdk_q + (uint32_t)4U; diff --git a/src/msvc/Hacl_RSAPSS.c b/src/msvc/Hacl_RSAPSS.c index ce2fb517..084f10b3 100644 --- a/src/msvc/Hacl_RSAPSS.c +++ b/src/msvc/Hacl_RSAPSS.c @@ -404,9 +404,9 @@ load_skey( Sign a message `msg` and write the signature to `sgnt`. @param a Hash algorithm to use. Allowed values for `a` are ... - * Spec_Hash_Definitions_SHA2_256, - * Spec_Hash_Definitions_SHA2_384, and - * Spec_Hash_Definitions_SHA2_512. + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. @@ -518,7 +518,10 @@ Hacl_RSAPSS_rsapss_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`. @@ -637,10 +640,10 @@ Load a public key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. -@return Returns an allocated public key. Note: caller must take care to `free()` the created key. +@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb) @@ -707,11 +710,11 @@ Load a secret key from key parts. @param modBits Count of bits in modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. -@return Returns an allocated secret key. Note: caller must take care to `free()` the created key. +@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key. */ uint64_t *Hacl_RSAPSS_new_rsapss_load_skey( @@ -804,13 +807,16 @@ uint64_t /** Sign a message `msg` and write the signature to `sgnt`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. @param dBits Count of bits in `d` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. -@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. +@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param salt Pointer to `saltLen` bytes where the salt is read from. @param msgLen Length of message. @@ -875,11 +881,14 @@ Hacl_RSAPSS_rsapss_skey_sign( /** Verify the signature `sgnt` of a message `msg`. -@param a Hash algorithm to use. +@param a Hash algorithm to use. Allowed values for `a` are ... + - Spec_Hash_Definitions_SHA2_256, + - Spec_Hash_Definitions_SHA2_384, and + - Spec_Hash_Definitions_SHA2_512. @param modBits Count of bits in the modulus (`n`). @param eBits Count of bits in `e` value. -@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from. -@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from. +@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from. +@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from. @param saltLen Length of salt. @param sgntLen Length of signature. @param sgnt Pointer to `sgntLen` bytes where the signature is read from. diff --git a/src/msvc/Hacl_Salsa20.c b/src/msvc/Hacl_Salsa20.c index e157d5ef..2758f8a4 100644 --- a/src/msvc/Hacl_Salsa20.c +++ b/src/msvc/Hacl_Salsa20.c @@ -181,6 +181,7 @@ salsa20_encrypt( memcpy(ctx + (uint32_t)11U, k10, (uint32_t)4U * sizeof (uint32_t)); ctx[15U] = (uint32_t)0x6b206574U; uint32_t k[16U] = { 0U }; + KRML_HOST_IGNORE(k); uint32_t rem = len % (uint32_t)64U; uint32_t nb = len / (uint32_t)64U; uint32_t rem1 = len % (uint32_t)64U; @@ -217,9 +218,8 @@ salsa20_encrypt( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = text + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, text + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k1[16U] = { 0U }; salsa20_core(k1, ctx, nb); uint32_t bl[16U] = { 0U }; @@ -294,6 +294,7 @@ salsa20_decrypt( memcpy(ctx + (uint32_t)11U, k10, (uint32_t)4U * sizeof (uint32_t)); ctx[15U] = (uint32_t)0x6b206574U; uint32_t k[16U] = { 0U }; + KRML_HOST_IGNORE(k); uint32_t rem = len % (uint32_t)64U; uint32_t nb = len / (uint32_t)64U; uint32_t rem1 = len % (uint32_t)64U; @@ -330,9 +331,8 @@ salsa20_decrypt( if (rem1 > (uint32_t)0U) { uint8_t *uu____2 = out + nb * (uint32_t)64U; - uint8_t *uu____3 = cipher + nb * (uint32_t)64U; uint8_t plain[64U] = { 0U }; - memcpy(plain, uu____3, rem * sizeof (uint8_t)); + memcpy(plain, cipher + nb * (uint32_t)64U, rem * sizeof (uint8_t)); uint32_t k1[16U] = { 0U }; salsa20_core(k1, ctx, nb); uint32_t bl[16U] = { 0U }; diff --git a/src/msvc/Hacl_Streaming_Blake2.c b/src/msvc/Hacl_Streaming_Blake2.c index 4faa859e..948d56c2 100644 --- a/src/msvc/Hacl_Streaming_Blake2.c +++ b/src/msvc/Hacl_Streaming_Blake2.c @@ -54,7 +54,6 @@ void Hacl_Streaming_Blake2_blake2s_32_no_key_init(Hacl_Streaming_Blake2_blake2s_ Hacl_Streaming_Blake2_blake2s_32_state scrut = *s1; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2_blake2s_32_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2s_32_blake2s_init(block_state.snd, (uint32_t)0U, (uint32_t)32U); Hacl_Streaming_Blake2_blake2s_32_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -354,7 +353,6 @@ void Hacl_Streaming_Blake2_blake2b_32_no_key_init(Hacl_Streaming_Blake2_blake2b_ Hacl_Streaming_Blake2_blake2b_32_state scrut = *s1; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2_blake2b_32_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2b_32_blake2b_init(block_state.snd, (uint32_t)0U, (uint32_t)64U); Hacl_Streaming_Blake2_blake2b_32_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Streaming_Blake2b_256.c b/src/msvc/Hacl_Streaming_Blake2b_256.c index d2df234a..bdb5433f 100644 --- a/src/msvc/Hacl_Streaming_Blake2b_256.c +++ b/src/msvc/Hacl_Streaming_Blake2b_256.c @@ -66,7 +66,6 @@ Hacl_Streaming_Blake2b_256_blake2b_256_no_key_init( Hacl_Streaming_Blake2b_256_blake2b_256_state scrut = *s; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2b_256_blake2b_256_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2b_256_blake2b_init(block_state.snd, (uint32_t)0U, (uint32_t)64U); Hacl_Streaming_Blake2b_256_blake2b_256_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Streaming_Blake2s_128.c b/src/msvc/Hacl_Streaming_Blake2s_128.c index eaace7ce..f97bf5d0 100644 --- a/src/msvc/Hacl_Streaming_Blake2s_128.c +++ b/src/msvc/Hacl_Streaming_Blake2s_128.c @@ -66,7 +66,6 @@ Hacl_Streaming_Blake2s_128_blake2s_128_no_key_init( Hacl_Streaming_Blake2s_128_blake2s_128_state scrut = *s; uint8_t *buf = scrut.buf; Hacl_Streaming_Blake2s_128_blake2s_128_block_state block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Blake2s_128_blake2s_init(block_state.snd, (uint32_t)0U, (uint32_t)32U); Hacl_Streaming_Blake2s_128_blake2s_128_state tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; diff --git a/src/msvc/Hacl_Streaming_Poly1305_128.c b/src/msvc/Hacl_Streaming_Poly1305_128.c index c752cfb0..c3f7c19a 100644 --- a/src/msvc/Hacl_Streaming_Poly1305_128.c +++ b/src/msvc/Hacl_Streaming_Poly1305_128.c @@ -58,7 +58,6 @@ Hacl_Streaming_Poly1305_128_init(uint8_t *k, Hacl_Streaming_Poly1305_128_poly130 uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; Lib_IntVector_Intrinsics_vec128 *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_128_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; @@ -312,7 +311,7 @@ Hacl_Streaming_Poly1305_128_finish( { ite1 = r % (uint32_t)16U; } - uint64_t prev_len_last = total_len - (uint64_t)ite1; + KRML_HOST_IGNORE(total_len - (uint64_t)ite1); uint32_t ite2; if (r % (uint32_t)16U == (uint32_t)0U && r > (uint32_t)0U) { diff --git a/src/msvc/Hacl_Streaming_Poly1305_256.c b/src/msvc/Hacl_Streaming_Poly1305_256.c index c1915ed9..e56275a4 100644 --- a/src/msvc/Hacl_Streaming_Poly1305_256.c +++ b/src/msvc/Hacl_Streaming_Poly1305_256.c @@ -58,7 +58,6 @@ Hacl_Streaming_Poly1305_256_init(uint8_t *k, Hacl_Streaming_Poly1305_256_poly130 uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; Lib_IntVector_Intrinsics_vec256 *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_256_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; @@ -312,7 +311,7 @@ Hacl_Streaming_Poly1305_256_finish( { ite1 = r % (uint32_t)16U; } - uint64_t prev_len_last = total_len - (uint64_t)ite1; + KRML_HOST_IGNORE(total_len - (uint64_t)ite1); uint32_t ite2; if (r % (uint32_t)16U == (uint32_t)0U && r > (uint32_t)0U) { diff --git a/src/msvc/Hacl_Streaming_Poly1305_32.c b/src/msvc/Hacl_Streaming_Poly1305_32.c index 89852727..249a622f 100644 --- a/src/msvc/Hacl_Streaming_Poly1305_32.c +++ b/src/msvc/Hacl_Streaming_Poly1305_32.c @@ -53,7 +53,6 @@ Hacl_Streaming_Poly1305_32_init(uint8_t *k, Hacl_Streaming_Poly1305_32_poly1305_ uint8_t *k_ = scrut.p_key; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; - KRML_HOST_IGNORE((void *)(uint8_t)0U); Hacl_Poly1305_32_poly1305_init(block_state, k); memcpy(k_, k, (uint32_t)32U * sizeof (uint8_t)); uint8_t *k_1 = k_; diff --git a/src/wasm/EverCrypt_Hash.wasm b/src/wasm/EverCrypt_Hash.wasm index 6b1a6c3f..8fdc7b27 100644 Binary files a/src/wasm/EverCrypt_Hash.wasm and b/src/wasm/EverCrypt_Hash.wasm differ diff --git a/src/wasm/Hacl_Bignum.wasm b/src/wasm/Hacl_Bignum.wasm index 579c0d56..b9c99c89 100644 Binary files a/src/wasm/Hacl_Bignum.wasm and b/src/wasm/Hacl_Bignum.wasm differ diff --git a/src/wasm/Hacl_Bignum256.wasm b/src/wasm/Hacl_Bignum256.wasm index b3b04557..24cf0406 100644 Binary files a/src/wasm/Hacl_Bignum256.wasm and b/src/wasm/Hacl_Bignum256.wasm differ diff --git a/src/wasm/Hacl_Bignum256_32.wasm b/src/wasm/Hacl_Bignum256_32.wasm index 3e0b1f72..d949c878 100644 Binary files a/src/wasm/Hacl_Bignum256_32.wasm and b/src/wasm/Hacl_Bignum256_32.wasm differ diff --git a/src/wasm/Hacl_Bignum32.wasm b/src/wasm/Hacl_Bignum32.wasm index 020a40ab..fa107b62 100644 Binary files a/src/wasm/Hacl_Bignum32.wasm and b/src/wasm/Hacl_Bignum32.wasm differ diff --git a/src/wasm/Hacl_Bignum4096.wasm b/src/wasm/Hacl_Bignum4096.wasm index a3db3777..c1ced14d 100644 Binary files a/src/wasm/Hacl_Bignum4096.wasm and b/src/wasm/Hacl_Bignum4096.wasm differ diff --git a/src/wasm/Hacl_Bignum4096_32.wasm b/src/wasm/Hacl_Bignum4096_32.wasm index d937d02c..a088be23 100644 Binary files a/src/wasm/Hacl_Bignum4096_32.wasm and b/src/wasm/Hacl_Bignum4096_32.wasm differ diff --git a/src/wasm/Hacl_Bignum64.wasm b/src/wasm/Hacl_Bignum64.wasm index c848593e..edc590b1 100644 Binary files a/src/wasm/Hacl_Bignum64.wasm and b/src/wasm/Hacl_Bignum64.wasm differ diff --git a/src/wasm/Hacl_Chacha20Poly1305_32.wasm b/src/wasm/Hacl_Chacha20Poly1305_32.wasm index 57b13d12..eb45d058 100644 Binary files a/src/wasm/Hacl_Chacha20Poly1305_32.wasm and b/src/wasm/Hacl_Chacha20Poly1305_32.wasm differ diff --git a/src/wasm/Hacl_Chacha20_Vec32.wasm b/src/wasm/Hacl_Chacha20_Vec32.wasm index 8ca2ca54..6d808d9a 100644 Binary files a/src/wasm/Hacl_Chacha20_Vec32.wasm and b/src/wasm/Hacl_Chacha20_Vec32.wasm differ diff --git a/src/wasm/Hacl_Curve25519_51.wasm b/src/wasm/Hacl_Curve25519_51.wasm index 0ddac4a4..12a0dd5c 100644 Binary files a/src/wasm/Hacl_Curve25519_51.wasm and b/src/wasm/Hacl_Curve25519_51.wasm differ diff --git a/src/wasm/Hacl_GenericField32.wasm b/src/wasm/Hacl_GenericField32.wasm index b8e4b468..52efafdf 100644 Binary files a/src/wasm/Hacl_GenericField32.wasm and b/src/wasm/Hacl_GenericField32.wasm differ diff --git a/src/wasm/Hacl_GenericField64.wasm b/src/wasm/Hacl_GenericField64.wasm index 31f5c165..a475b2db 100644 Binary files a/src/wasm/Hacl_GenericField64.wasm and b/src/wasm/Hacl_GenericField64.wasm differ diff --git a/src/wasm/Hacl_HMAC.wasm b/src/wasm/Hacl_HMAC.wasm index 32bdf466..033e7523 100644 Binary files a/src/wasm/Hacl_HMAC.wasm and b/src/wasm/Hacl_HMAC.wasm differ diff --git a/src/wasm/Hacl_HPKE_Curve51_CP32_SHA256.wasm b/src/wasm/Hacl_HPKE_Curve51_CP32_SHA256.wasm index 000976b0..7f40d696 100644 Binary files a/src/wasm/Hacl_HPKE_Curve51_CP32_SHA256.wasm and b/src/wasm/Hacl_HPKE_Curve51_CP32_SHA256.wasm differ diff --git a/src/wasm/Hacl_HPKE_Curve51_CP32_SHA512.wasm b/src/wasm/Hacl_HPKE_Curve51_CP32_SHA512.wasm index 09384397..1abe9689 100644 Binary files a/src/wasm/Hacl_HPKE_Curve51_CP32_SHA512.wasm and b/src/wasm/Hacl_HPKE_Curve51_CP32_SHA512.wasm differ diff --git a/src/wasm/Hacl_Hash_MD5.wasm b/src/wasm/Hacl_Hash_MD5.wasm index 16b84423..c6c7b045 100644 Binary files a/src/wasm/Hacl_Hash_MD5.wasm and b/src/wasm/Hacl_Hash_MD5.wasm differ diff --git a/src/wasm/Hacl_Hash_SHA1.wasm b/src/wasm/Hacl_Hash_SHA1.wasm index 40ffd059..b345c0a6 100644 Binary files a/src/wasm/Hacl_Hash_SHA1.wasm and b/src/wasm/Hacl_Hash_SHA1.wasm differ diff --git a/src/wasm/Hacl_Hash_SHA3.wasm b/src/wasm/Hacl_Hash_SHA3.wasm index e318aff0..3243ec79 100644 Binary files a/src/wasm/Hacl_Hash_SHA3.wasm and b/src/wasm/Hacl_Hash_SHA3.wasm differ diff --git a/src/wasm/Hacl_K256_ECDSA.wasm b/src/wasm/Hacl_K256_ECDSA.wasm index 3f9a5db6..d1f56f3a 100644 Binary files a/src/wasm/Hacl_K256_ECDSA.wasm and b/src/wasm/Hacl_K256_ECDSA.wasm differ diff --git a/src/wasm/Hacl_NaCl.wasm b/src/wasm/Hacl_NaCl.wasm index bb7e23c3..1762f27f 100644 Binary files a/src/wasm/Hacl_NaCl.wasm and b/src/wasm/Hacl_NaCl.wasm differ diff --git a/src/wasm/Hacl_P256.wasm b/src/wasm/Hacl_P256.wasm index 113d780f..83a71ab2 100644 Binary files a/src/wasm/Hacl_P256.wasm and b/src/wasm/Hacl_P256.wasm differ diff --git a/src/wasm/Hacl_Salsa20.wasm b/src/wasm/Hacl_Salsa20.wasm index 0df1cd76..c712bb36 100644 Binary files a/src/wasm/Hacl_Salsa20.wasm and b/src/wasm/Hacl_Salsa20.wasm differ diff --git a/src/wasm/INFO.txt b/src/wasm/INFO.txt index 7ed8e74a..60cb7b00 100644 --- a/src/wasm/INFO.txt +++ b/src/wasm/INFO.txt @@ -1,4 +1,4 @@ This code was generated with the following toolchain. -F* version: 155853a14336aa0713dba7db5408f4c8ab512a06 -KaRaMeL version: db63c1de17565be0ec4989f58532717a04e3ff40 +F* version: bc622701c668f6b4092760879372968265d4a4e1 +Karamel version: 7cffd27cfefbd220e986e561e8d350f043609f76 Vale version: 0.3.19