[CI] update code

cryspen · Mar 4, 2025 · 54c310c · 54c310c
1 parent 05c3d8f
commit 54c310c
Show file tree

Hide file tree

Showing 421 changed files with 19,578 additions and 5,464 deletions.
diff --git a/include/EverCrypt_AEAD.h b/include/EverCrypt_AEAD.h
@@ -37,8 +37,6 @@ extern "C" {
 
 #include "Hacl_Spec.h"
 #include "EverCrypt_Error.h"
-#include "EverCrypt_Chacha20Poly1305.h"
-#include "EverCrypt_AutoConfig2.h"
 
 typedef struct EverCrypt_AEAD_state_s_s EverCrypt_AEAD_state_s;
 

diff --git a/include/EverCrypt_Chacha20Poly1305.h b/include/EverCrypt_Chacha20Poly1305.h
@@ -35,11 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_AEAD_Chacha20Poly1305_Simd256.h"
-#include "Hacl_AEAD_Chacha20Poly1305_Simd128.h"
-#include "Hacl_AEAD_Chacha20Poly1305.h"
-#include "EverCrypt_AutoConfig2.h"
-
 void
 EverCrypt_Chacha20Poly1305_aead_encrypt(
   uint8_t *k,

diff --git a/include/EverCrypt_Curve25519.h b/include/EverCrypt_Curve25519.h
@@ -35,10 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Curve25519_64.h"
-#include "Hacl_Curve25519_51.h"
-#include "EverCrypt_AutoConfig2.h"
-
 /**
 Calculate a public point from a secret/private key.
 

diff --git a/include/EverCrypt_DRBG.h b/include/EverCrypt_DRBG.h
@@ -35,9 +35,7 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_RandomBuffer_System.h"
 #include "Hacl_Streaming_Types.h"
-#include "Hacl_HMAC_DRBG.h"
 
 typedef Spec_Hash_Definitions_hash_alg EverCrypt_DRBG_supported_alg;
 

diff --git a/include/EverCrypt_Ed25519.h b/include/EverCrypt_Ed25519.h
@@ -35,8 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Ed25519.h"
-
 void EverCrypt_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
 
 void EverCrypt_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);

diff --git a/include/EverCrypt_HMAC.h b/include/EverCrypt_HMAC.h
@@ -36,17 +36,11 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "Hacl_Streaming_Types.h"
-#include "Hacl_Krmllib.h"
-#include "Hacl_Hash_SHA2.h"
-#include "Hacl_Hash_Blake2s.h"
-#include "Hacl_Hash_Blake2b.h"
 
 bool EverCrypt_HMAC_is_supported_alg(Spec_Hash_Definitions_hash_alg uu___);
 
 typedef Spec_Hash_Definitions_hash_alg EverCrypt_HMAC_supported_alg;
 
-extern void (*EverCrypt_HMAC_hash_256)(uint8_t *x0, uint8_t *x1, uint32_t x2);
-
 void
 EverCrypt_HMAC_compute(
   Spec_Hash_Definitions_hash_alg a,

diff --git a/include/EverCrypt_Hash.h b/include/EverCrypt_Hash.h
@@ -36,27 +36,13 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "Hacl_Streaming_Types.h"
-#include "Hacl_Krmllib.h"
-#include "Hacl_Hash_SHA3.h"
-#include "Hacl_Hash_SHA2.h"
-#include "Hacl_Hash_Blake2s_Simd128.h"
-#include "Hacl_Hash_Blake2s.h"
-#include "Hacl_Hash_Blake2b_Simd256.h"
-#include "Hacl_Hash_Blake2b.h"
 #include "EverCrypt_Error.h"
-#include "EverCrypt_AutoConfig2.h"
 
 typedef struct EverCrypt_Hash_state_s_s EverCrypt_Hash_state_s;
 
 uint32_t EverCrypt_Hash_Incremental_hash_len(Spec_Hash_Definitions_hash_alg a);
 
-typedef struct EverCrypt_Hash_Incremental_state_t_s
-{
-  EverCrypt_Hash_state_s *block_state;
-  uint8_t *buf;
-  uint64_t total_len;
-}
-EverCrypt_Hash_Incremental_state_t;
+typedef struct EverCrypt_Hash_Incremental_state_t_s EverCrypt_Hash_Incremental_state_t;
 
 /**
 Allocate initial state for the agile hash. The argument `a` stands for the

diff --git a/include/EverCrypt_Poly1305.h b/include/EverCrypt_Poly1305.h
@@ -35,11 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_MAC_Poly1305_Simd256.h"
-#include "Hacl_MAC_Poly1305_Simd128.h"
-#include "Hacl_MAC_Poly1305.h"
-#include "EverCrypt_AutoConfig2.h"
-
 void EverCrypt_Poly1305_mac(uint8_t *output, uint8_t *input, uint32_t input_len, uint8_t *key);
 
 #if defined(__cplusplus)

diff --git a/include/Hacl_AEAD_Chacha20Poly1305.h b/include/Hacl_AEAD_Chacha20Poly1305.h
@@ -35,8 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Chacha20.h"
-
 /**
 Encrypt a message `input` with key `key`.
 

diff --git a/include/Hacl_AEAD_Chacha20Poly1305_Simd128.h b/include/Hacl_AEAD_Chacha20Poly1305_Simd128.h
@@ -35,8 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Chacha20_Vec128.h"
-
 /**
 Encrypt a message `input` with key `key`.
 

diff --git a/include/Hacl_AEAD_Chacha20Poly1305_Simd256.h b/include/Hacl_AEAD_Chacha20Poly1305_Simd256.h
@@ -35,8 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Chacha20_Vec256.h"
-
 /**
 Encrypt a message `input` with key `key`.
 

diff --git a/include/Hacl_Bignum.h b/include/Hacl_Bignum.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Krmllib.h"
 #include "lib_intrinsics.h"
 
 typedef struct Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_s

diff --git a/include/Hacl_Bignum256.h b/include/Hacl_Bignum256.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Hacl_Krmllib.h"
 #include "Hacl_Bignum.h"
 
 /*******************************************************************************