[CI] update code

cryspen · Sep 7, 2023 · d9b4f92 · d9b4f92
1 parent c6d3969
commit d9b4f92
Show file tree

Hide file tree

Showing 26 changed files with 216 additions and 254 deletions.
diff --git a/include/EverCrypt_AEAD.h b/include/EverCrypt_AEAD.h
@@ -42,6 +42,10 @@ extern "C" {
 
 typedef struct EverCrypt_AEAD_state_s_s EverCrypt_AEAD_state_s;
 
+/**
+Both encryption and decryption require a state that holds the key.
+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);
 
 /**

diff --git a/include/EverCrypt_DRBG.h b/include/EverCrypt_DRBG.h
@@ -36,7 +36,6 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "Lib_RandomBuffer_System.h"
-#include "Lib_Memzero0.h"
 #include "Hacl_Streaming_Types.h"
 #include "Hacl_HMAC_DRBG.h"
 

diff --git a/include/Hacl_Frodo1344.h b/include/Hacl_Frodo1344.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo1344_crypto_bytes;

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

diff --git a/include/Hacl_Frodo640.h b/include/Hacl_Frodo640.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo640_crypto_bytes;

diff --git a/include/Hacl_Frodo976.h b/include/Hacl_Frodo976.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo976_crypto_bytes;

diff --git a/include/Hacl_Hash_Blake2.h b/include/Hacl_Hash_Blake2.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 
 void Hacl_Blake2b_32_blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);

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

diff --git a/include/Hacl_Hash_Blake2s_128.h b/include/Hacl_Hash_Blake2s_128.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "libintvector.h"
 
 void

diff --git a/include/Lib_Memzero0.h b/include/Lib_Memzero0.h
diff --git a/include/TestLib.h b/include/TestLib.h
@@ -55,7 +55,8 @@ extern void TestLib_checku32(uint32_t uu___, uint32_t uu___1);
 
 extern void TestLib_checku64(uint64_t uu___, uint64_t uu___1);
 
-extern void TestLib_compare_and_print(C_String_t uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
+extern void
+TestLib_compare_and_print(Prims_string uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
 
 extern uint8_t *TestLib_unsafe_malloc(uint32_t l);
 

diff --git a/include/libmemzero0.h b/include/libmemzero0.h
@@ -0,0 +1,5 @@
+#include <inttypes.h>
+
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
+
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
diff --git a/include/msvc/libmemzero0.h b/include/msvc/libmemzero0.h
@@ -0,0 +1,5 @@
+#include <inttypes.h>
+
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
+
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
diff --git a/src/EverCrypt_AEAD.c b/src/EverCrypt_AEAD.c
@@ -40,6 +40,10 @@ typedef struct EverCrypt_AEAD_state_s_s
 }
 EverCrypt_AEAD_state_s;
 
+/**
+Both encryption and decryption require a state that holds the key.
+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)
 {
   return true;