Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
@franziskuskiefer
franziskuskiefer committed Oct 11, 2023
1 parent 079be45 commit 70b4970
Show file tree
Hide file tree
Showing 32 changed files with 247 additions and 89 deletions.
4 changes: 2 additions & 2 deletions info.txt
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
The code was generated with the following toolchain.
F* version: bc622701c668f6b4092760879372968265d4a4e1
KaRaMeL version: aef72b2b5a44b338b856a177819d1bfa0d7cc5b6
HACL* version: 1a20576fc736d51e1ab3c317b46ba81560b75786
KaRaMeL version: 7cffd27cfefbd220e986e561e8d350f043609f76
HACL* version: 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c
Vale version: 0.3.19
8 changes: 8 additions & 0 deletions karamel/include/krml/internal/target.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
56 changes: 0 additions & 56 deletions karamel/krmllib/dist/minimal/Makefile.basic
View file

This file was deleted.

5 changes: 0 additions & 5 deletions karamel/krmllib/dist/minimal/Makefile.include
View file

This file was deleted.

11 changes: 0 additions & 11 deletions karamel/krmllib/dist/minimal/libkrmllib.def
View file

This file was deleted.

112 changes: 112 additions & 0 deletions src/EverCrypt_AEAD.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,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();
Expand Down Expand Up @@ -126,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();
Expand Down Expand Up @@ -204,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)
{
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -524,6 +546,15 @@ 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;
Expand Down Expand Up @@ -666,6 +697,15 @@ 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;
Expand Down Expand Up @@ -800,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();
Expand Down Expand Up @@ -939,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();
Expand Down Expand Up @@ -1164,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)
{
Expand Down Expand Up @@ -1299,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)
{
Expand Down Expand Up @@ -1544,6 +1620,15 @@ 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;
Expand Down Expand Up @@ -1694,6 +1779,15 @@ 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;
Expand Down Expand Up @@ -1836,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();
Expand Down Expand Up @@ -1983,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();
Expand Down
7 changes: 6 additions & 1 deletion src/EverCrypt_Poly1305.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
6 changes: 0 additions & 6 deletions src/Hacl_Ed25519.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -711,18 +711,12 @@ 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);
KRML_HOST_IGNORE(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);
KRML_HOST_IGNORE(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);
KRML_HOST_IGNORE(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);
Expand Down
Loading

0 comments on commit 70b4970

Please sign in to comment.