diff options
Diffstat (limited to 'lib/freebl/verified/karamel/krmllib/dist/minimal')
10 files changed, 1597 insertions, 0 deletions
diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h new file mode 100644 index 000000000..4affcee35 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h @@ -0,0 +1,75 @@ +/* + Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. +*/ + +#ifndef __FStar_UInt128_H +#define __FStar_UInt128_H + +#include <inttypes.h> +#include <stdbool.h> +#include "krml/internal/compat.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/types.h" +#include "krml/internal/target.h" +static inline FStar_UInt128_uint128 +FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a); + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s); + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s); + +static inline bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 +FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b); + +static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a); + +static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a); + +static inline FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y); + +static inline FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y); + +#define __FStar_UInt128_H_DEFINED +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h new file mode 100644 index 000000000..8f235c314 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h @@ -0,0 +1,327 @@ +/* + Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. +*/ + +#ifndef __FStar_UInt128_Verified_H +#define __FStar_UInt128_Verified_H + +#include "FStar_UInt_8_16_32_64.h" +#include <inttypes.h> +#include <stdbool.h> +#include "krml/internal/types.h" +#include "krml/internal/target.h" +static inline uint64_t +FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b) +{ + return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U; +} + +static inline uint64_t +FStar_UInt128_carry(uint64_t a, uint64_t b) +{ + return FStar_UInt128_constant_time_carry(a, b); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return FStar_UInt128_sub_mod_impl(a, b); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low & b.low; + lit.high = a.high & b.high; + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low ^ b.low; + lit.high = a.high ^ b.high; + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low | b.low; + lit.high = a.high | b.high; + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_lognot(FStar_UInt128_uint128 a) +{ + FStar_UInt128_uint128 lit; + lit.low = ~a.low; + lit.high = ~a.high; + return lit; +} + +static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U; + +static inline uint64_t +FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s) +{ + return (hi << s) + (lo >> (FStar_UInt128_u32_64 - s)); +} + +static inline uint64_t +FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s) +{ + return FStar_UInt128_add_u64_shift_left(hi, lo, s); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s == (uint32_t)0U) { + return a; + } else { + FStar_UInt128_uint128 lit; + lit.low = a.low << s; + lit.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s); + return lit; + } +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s) +{ + FStar_UInt128_uint128 lit; + lit.low = (uint64_t)0U; + lit.high = a.low << (s - FStar_UInt128_u32_64); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s < FStar_UInt128_u32_64) { + return FStar_UInt128_shift_left_small(a, s); + } else { + return FStar_UInt128_shift_left_large(a, s); + } +} + +static inline uint64_t +FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s) +{ + return (lo >> s) + (hi << (FStar_UInt128_u32_64 - s)); +} + +static inline uint64_t +FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s) +{ + return FStar_UInt128_add_u64_shift_right(hi, lo, s); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s == (uint32_t)0U) { + return a; + } else { + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s); + lit.high = a.high >> s; + return lit; + } +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s) +{ + FStar_UInt128_uint128 lit; + lit.low = a.high >> (s - FStar_UInt128_u32_64); + lit.high = (uint64_t)0U; + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s < FStar_UInt128_u32_64) { + return FStar_UInt128_shift_right_small(a, s); + } else { + return FStar_UInt128_shift_right_large(a, s); + } +} + +static inline bool +FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.low == b.low && a.high == b.high; +} + +static inline bool +FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high > b.high || (a.high == b.high && a.low > b.low); +} + +static inline bool +FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high < b.high || (a.high == b.high && a.low < b.low); +} + +static inline bool +FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high > b.high || (a.high == b.high && a.low >= b.low); +} + +static inline bool +FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high < b.high || (a.high == b.high && a.low <= b.low); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high); + lit.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = + (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)); + lit.high = + (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)); + return lit; +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_uint64_to_uint128(uint64_t a) +{ + FStar_UInt128_uint128 lit; + lit.low = a; + lit.high = (uint64_t)0U; + return lit; +} + +static inline uint64_t +FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a) +{ + return a.low; +} + +static inline uint64_t +FStar_UInt128_u64_mod_32(uint64_t a) +{ + return a & (uint64_t)0xffffffffU; +} + +static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U; + +static inline uint64_t +FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo) +{ + return lo + (hi << FStar_UInt128_u32_32); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_mul32(uint64_t x, uint32_t y) +{ + FStar_UInt128_uint128 lit; + lit.low = + FStar_UInt128_u32_combine((x >> FStar_UInt128_u32_32) * (uint64_t)y + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32), + FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * (uint64_t)y)); + lit.high = + ((x >> FStar_UInt128_u32_32) * (uint64_t)y + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32)) >> FStar_UInt128_u32_32; + return lit; +} + +static inline uint64_t +FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo) +{ + return lo + (hi << FStar_UInt128_u32_32); +} + +static inline FStar_UInt128_uint128 +FStar_UInt128_mul_wide(uint64_t x, uint64_t y) +{ + FStar_UInt128_uint128 lit; + lit.low = + FStar_UInt128_u32_combine_(FStar_UInt128_u64_mod_32(x) * (y >> FStar_UInt128_u32_32) + + FStar_UInt128_u64_mod_32((x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)), + FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y))); + lit.high = + (x >> FStar_UInt128_u32_32) * (y >> FStar_UInt128_u32_32) + + (((x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)) >> FStar_UInt128_u32_32) + + ((FStar_UInt128_u64_mod_32(x) * (y >> FStar_UInt128_u32_32) + + FStar_UInt128_u64_mod_32((x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32))) >> + FStar_UInt128_u32_32); + return lit; +} + +#define __FStar_UInt128_Verified_H_DEFINED +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h new file mode 100644 index 000000000..51f3eead1 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h @@ -0,0 +1,218 @@ +/* + Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. +*/ + +#ifndef __FStar_UInt_8_16_32_64_H +#define __FStar_UInt_8_16_32_64_H + +#include <inttypes.h> +#include <stdbool.h> +#include "krml/internal/compat.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/types.h" +#include "krml/internal/target.h" +extern Prims_int FStar_UInt64_n; + +extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee); + +extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee); + +extern Prims_int FStar_UInt64_v(uint64_t x); + +extern uint64_t FStar_UInt64_uint_to_t(Prims_int x); + +extern uint64_t FStar_UInt64_zero; + +extern uint64_t FStar_UInt64_one; + +extern uint64_t FStar_UInt64_minus(uint64_t a); + +extern uint32_t FStar_UInt64_n_minus_one; + +static inline uint64_t +FStar_UInt64_eq_mask(uint64_t a, uint64_t b) +{ + uint64_t x = a ^ b; + uint64_t minus_x = ~x + (uint64_t)1U; + uint64_t x_or_minus_x = x | minus_x; + uint64_t xnx = x_or_minus_x >> (uint32_t)63U; + return xnx - (uint64_t)1U; +} + +static inline uint64_t +FStar_UInt64_gte_mask(uint64_t a, uint64_t b) +{ + uint64_t x = a; + uint64_t y = b; + uint64_t x_xor_y = x ^ y; + uint64_t x_sub_y = x - y; + uint64_t x_sub_y_xor_y = x_sub_y ^ y; + uint64_t q = x_xor_y | x_sub_y_xor_y; + uint64_t x_xor_q = x ^ q; + uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U; + return x_xor_q_ - (uint64_t)1U; +} + +extern Prims_string FStar_UInt64_to_string(uint64_t uu___); + +extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___); + +extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___); + +extern uint64_t FStar_UInt64_of_string(Prims_string uu___); + +extern Prims_int FStar_UInt32_n; + +extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee); + +extern Prims_int FStar_UInt32___proj__Mk__item__v(uint32_t projectee); + +extern Prims_int FStar_UInt32_v(uint32_t x); + +extern uint32_t FStar_UInt32_uint_to_t(Prims_int x); + +extern uint32_t FStar_UInt32_zero; + +extern uint32_t FStar_UInt32_one; + +extern uint32_t FStar_UInt32_minus(uint32_t a); + +extern uint32_t FStar_UInt32_n_minus_one; + +static inline uint32_t +FStar_UInt32_eq_mask(uint32_t a, uint32_t b) +{ + uint32_t x = a ^ b; + uint32_t minus_x = ~x + (uint32_t)1U; + uint32_t x_or_minus_x = x | minus_x; + uint32_t xnx = x_or_minus_x >> (uint32_t)31U; + return xnx - (uint32_t)1U; +} + +static inline uint32_t +FStar_UInt32_gte_mask(uint32_t a, uint32_t b) +{ + uint32_t x = a; + uint32_t y = b; + uint32_t x_xor_y = x ^ y; + uint32_t x_sub_y = x - y; + uint32_t x_sub_y_xor_y = x_sub_y ^ y; + uint32_t q = x_xor_y | x_sub_y_xor_y; + uint32_t x_xor_q = x ^ q; + uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U; + return x_xor_q_ - (uint32_t)1U; +} + +extern Prims_string FStar_UInt32_to_string(uint32_t uu___); + +extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___); + +extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___); + +extern uint32_t FStar_UInt32_of_string(Prims_string uu___); + +extern Prims_int FStar_UInt16_n; + +extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee); + +extern Prims_int FStar_UInt16___proj__Mk__item__v(uint16_t projectee); + +extern Prims_int FStar_UInt16_v(uint16_t x); + +extern uint16_t FStar_UInt16_uint_to_t(Prims_int x); + +extern uint16_t FStar_UInt16_zero; + +extern uint16_t FStar_UInt16_one; + +extern uint16_t FStar_UInt16_minus(uint16_t a); + +extern uint32_t FStar_UInt16_n_minus_one; + +static inline uint16_t +FStar_UInt16_eq_mask(uint16_t a, uint16_t b) +{ + uint16_t x = a ^ b; + uint16_t minus_x = ~x + (uint16_t)1U; + uint16_t x_or_minus_x = x | minus_x; + uint16_t xnx = x_or_minus_x >> (uint32_t)15U; + return xnx - (uint16_t)1U; +} + +static inline uint16_t +FStar_UInt16_gte_mask(uint16_t a, uint16_t b) +{ + uint16_t x = a; + uint16_t y = b; + uint16_t x_xor_y = x ^ y; + uint16_t x_sub_y = x - y; + uint16_t x_sub_y_xor_y = x_sub_y ^ y; + uint16_t q = x_xor_y | x_sub_y_xor_y; + uint16_t x_xor_q = x ^ q; + uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U; + return x_xor_q_ - (uint16_t)1U; +} + +extern Prims_string FStar_UInt16_to_string(uint16_t uu___); + +extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___); + +extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___); + +extern uint16_t FStar_UInt16_of_string(Prims_string uu___); + +extern Prims_int FStar_UInt8_n; + +extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee); + +extern Prims_int FStar_UInt8___proj__Mk__item__v(uint8_t projectee); + +extern Prims_int FStar_UInt8_v(uint8_t x); + +extern uint8_t FStar_UInt8_uint_to_t(Prims_int x); + +extern uint8_t FStar_UInt8_zero; + +extern uint8_t FStar_UInt8_one; + +extern uint8_t FStar_UInt8_minus(uint8_t a); + +extern uint32_t FStar_UInt8_n_minus_one; + +static inline uint8_t +FStar_UInt8_eq_mask(uint8_t a, uint8_t b) +{ + uint8_t x = a ^ b; + uint8_t minus_x = ~x + (uint8_t)1U; + uint8_t x_or_minus_x = x | minus_x; + uint8_t xnx = x_or_minus_x >> (uint32_t)7U; + return xnx - (uint8_t)1U; +} + +static inline uint8_t +FStar_UInt8_gte_mask(uint8_t a, uint8_t b) +{ + uint8_t x = a; + uint8_t y = b; + uint8_t x_xor_y = x ^ y; + uint8_t x_sub_y = x - y; + uint8_t x_sub_y_xor_y = x_sub_y ^ y; + uint8_t q = x_xor_y | x_sub_y_xor_y; + uint8_t x_xor_q = x ^ q; + uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U; + return x_xor_q_ - (uint8_t)1U; +} + +extern Prims_string FStar_UInt8_to_string(uint8_t uu___); + +extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___); + +extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___); + +extern uint8_t FStar_UInt8_of_string(Prims_string uu___); + +typedef uint8_t FStar_UInt8_byte; + +#define __FStar_UInt_8_16_32_64_H_DEFINED +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h new file mode 100644 index 000000000..5feb077a4 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h @@ -0,0 +1,25 @@ +/* + Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. +*/ + +#ifndef __LowStar_Endianness_H +#define __LowStar_Endianness_H + +#include "FStar_UInt128.h" +#include <inttypes.h> +#include <stdbool.h> +#include "krml/internal/compat.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/types.h" +#include "krml/internal/target.h" +static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1); + +static inline FStar_UInt128_uint128 load128_le(uint8_t *x0); + +static inline void store128_be(uint8_t *x0, FStar_UInt128_uint128 x1); + +static inline FStar_UInt128_uint128 load128_be(uint8_t *x0); + +#define __LowStar_Endianness_H_DEFINED +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic b/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic new file mode 100644 index 000000000..672b58015 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic @@ -0,0 +1,56 @@ +# 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 $(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/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include b/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include new file mode 100644 index 000000000..ad5321718 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include @@ -0,0 +1,5 @@ +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/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h new file mode 100644 index 000000000..33cff6b6d --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h @@ -0,0 +1,225 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. */ + +/******************************************************************************/ +/* Machine integers (128-bit arithmetic) */ +/******************************************************************************/ + +/* This header contains two things. + * + * First, an implementation of 128-bit arithmetic suitable for 64-bit GCC and + * Clang, i.e. all the operations from FStar.UInt128. + * + * Second, 128-bit operations from C.Endianness (or LowStar.Endianness), + * suitable for any compiler and platform (via a series of ifdefs). This second + * part is unfortunate, and should be fixed by moving {load,store}128_{be,le} to + * FStar.UInt128 to avoid a maze of preprocessor guards and hand-written code. + * */ + +/* This file is used for both the minimal and generic krmllib distributions. As + * such, it assumes that the machine integers have been bundled the exact same + * way in both cases. */ + +#ifndef FSTAR_UINT128_GCC64 +#define FSTAR_UINT128_GCC64 + +#include "FStar_UInt128.h" +#include "FStar_UInt_8_16_32_64.h" +#include "LowStar_Endianness.h" + +/* GCC + using native unsigned __int128 support */ + +inline static uint128_t +load128_le(uint8_t *b) +{ + uint128_t l = (uint128_t)load64_le(b); + uint128_t h = (uint128_t)load64_le(b + 8); + return (h << 64 | l); +} + +inline static void +store128_le(uint8_t *b, uint128_t n) +{ + store64_le(b, (uint64_t)n); + store64_le(b + 8, (uint64_t)(n >> 64)); +} + +inline static uint128_t +load128_be(uint8_t *b) +{ + uint128_t h = (uint128_t)load64_be(b); + uint128_t l = (uint128_t)load64_be(b + 8); + return (h << 64 | l); +} + +inline static void +store128_be(uint8_t *b, uint128_t n) +{ + store64_be(b, (uint64_t)(n >> 64)); + store64_be(b + 8, (uint64_t)n); +} + +inline static uint128_t +FStar_UInt128_add(uint128_t x, uint128_t y) +{ + return x + y; +} + +inline static uint128_t +FStar_UInt128_mul(uint128_t x, uint128_t y) +{ + return x * y; +} + +inline static uint128_t +FStar_UInt128_add_mod(uint128_t x, uint128_t y) +{ + return x + y; +} + +inline static uint128_t +FStar_UInt128_sub(uint128_t x, uint128_t y) +{ + return x - y; +} + +inline static uint128_t +FStar_UInt128_sub_mod(uint128_t x, uint128_t y) +{ + return x - y; +} + +inline static uint128_t +FStar_UInt128_logand(uint128_t x, uint128_t y) +{ + return x & y; +} + +inline static uint128_t +FStar_UInt128_logor(uint128_t x, uint128_t y) +{ + return x | y; +} + +inline static uint128_t +FStar_UInt128_logxor(uint128_t x, uint128_t y) +{ + return x ^ y; +} + +inline static uint128_t +FStar_UInt128_lognot(uint128_t x) +{ + return ~x; +} + +inline static uint128_t +FStar_UInt128_shift_left(uint128_t x, uint32_t y) +{ + return x << y; +} + +inline static uint128_t +FStar_UInt128_shift_right(uint128_t x, uint32_t y) +{ + return x >> y; +} + +inline static uint128_t +FStar_UInt128_uint64_to_uint128(uint64_t x) +{ + return (uint128_t)x; +} + +inline static uint64_t +FStar_UInt128_uint128_to_uint64(uint128_t x) +{ + return (uint64_t)x; +} + +inline static uint128_t +FStar_UInt128_mul_wide(uint64_t x, uint64_t y) +{ + return ((uint128_t)x) * 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); + return ((uint128_t)mask) << 64 | mask; +} + +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)); + return ((uint128_t)mask) << 64 | mask; +} + +inline static uint64_t +FStar_UInt128___proj__Mkuint128__item__low(uint128_t x) +{ + return (uint64_t)x; +} + +inline static uint64_t +FStar_UInt128___proj__Mkuint128__item__high(uint128_t x) +{ + return (uint64_t)(x >> 64); +} + +inline static uint128_t +FStar_UInt128_add_underspec(uint128_t x, uint128_t y) +{ + return x + y; +} + +inline static uint128_t +FStar_UInt128_sub_underspec(uint128_t x, uint128_t y) +{ + return x - y; +} + +inline static bool +FStar_UInt128_eq(uint128_t x, uint128_t y) +{ + return x == y; +} + +inline static bool +FStar_UInt128_gt(uint128_t x, uint128_t y) +{ + return x > y; +} + +inline static bool +FStar_UInt128_lt(uint128_t x, uint128_t y) +{ + return x < y; +} + +inline static bool +FStar_UInt128_gte(uint128_t x, uint128_t y) +{ + return x >= y; +} + +inline static bool +FStar_UInt128_lte(uint128_t x, uint128_t y) +{ + return x <= y; +} + +inline static uint128_t +FStar_UInt128_mul32(uint64_t x, uint32_t y) +{ + return (uint128_t)x * (uint128_t)y; +} + +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h new file mode 100644 index 000000000..e9b366e25 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h @@ -0,0 +1,571 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. */ + +/* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel> + * then hand-edited to use MSVC intrinsics KaRaMeL invocation: + * C:\users\barrybo\mitls2c\karamel\_build\src\Karamel.native -minimal -fnouint128 C:/users/barrybo/mitls2c/FStar/ulib/FStar.UInt128.fst -tmpdir ../secure_api/out/runtime_switch/uint128 -skip-compilation -add-include "krmllib0.h" -drop FStar.Int.Cast.Full -bundle FStar.UInt128=FStar.*,Prims + * F* version: 15104ff8 + * KaRaMeL version: 318b7fa8 + */ + +#ifndef FSTAR_UINT128_MSVC +#define FSTAR_UINT128_MSVC + +#include "krml/internal/types.h" +#include "FStar_UInt128.h" +#include "FStar_UInt_8_16_32_64.h" + +#ifndef _MSC_VER +#error This file only works with the MSVC compiler +#endif + +/* JP: need to rip out HAS_OPTIMIZED since the header guards in types.h are now + * done properly and only include this file when we know for sure we are on + * 64-bit MSVC. */ + +#if defined(_M_X64) && !defined(KRML_VERIFIED_UINT128) +#define HAS_OPTIMIZED 1 +#else +#define HAS_OPTIMIZED 0 +#endif + +// Define .low and .high in terms of the __m128i fields, to reduce +// the amount of churn in this file. +#if HAS_OPTIMIZED +#include <intrin.h> +#include <immintrin.h> +#define low m128i_u64[0] +#define high m128i_u64[1] +#endif + +inline static FStar_UInt128_uint128 +load128_le(uint8_t *b) +{ +#if HAS_OPTIMIZED + return _mm_loadu_si128((__m128i *)b); +#else + FStar_UInt128_uint128 lit; + lit.low = load64_le(b); + lit.high = load64_le(b + 8); + return lit; +#endif +} + +inline static void +store128_le(uint8_t *b, FStar_UInt128_uint128 n) +{ + store64_le(b, n.low); + store64_le(b + 8, n.high); +} + +inline static FStar_UInt128_uint128 +load128_be(uint8_t *b) +{ + uint64_t l = load64_be(b + 8); + uint64_t h = load64_be(b); +#if HAS_OPTIMIZED + return _mm_set_epi64x(h, l); +#else + FStar_UInt128_uint128 lit; + lit.low = l; + lit.high = h; + return lit; +#endif +} + +inline static void +store128_be(uint8_t *b, uint128_t n) +{ + store64_be(b, n.high); + store64_be(b + 8, n.low); +} + +inline static uint64_t +FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b) +{ + return (a ^ (a ^ b | a - b ^ b)) >> (uint32_t)63U; +} + +inline static uint64_t +FStar_UInt128_carry(uint64_t a, uint64_t b) +{ + return FStar_UInt128_constant_time_carry(a, b); +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + uint64_t l, h; + + unsigned char carry = + _addcarry_u64(0, a.low, b.low, &l); // low/CF = a.low+b.low+0 + _addcarry_u64(carry, a.high, b.high, &h); // high = a.high+b.high+CF + return _mm_set_epi64x(h, l); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return FStar_UInt128_add(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low; + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return FStar_UInt128_add(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low + b.low; + lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + uint64_t l, h; + + unsigned char borrow = _subborrow_u64(0, a.low, b.low, &l); + _subborrow_u64(borrow, a.high, b.high, &h); + return _mm_set_epi64x(h, l); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return FStar_UInt128_sub(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + FStar_UInt128_uint128 lit; + lit.low = a.low - b.low; + lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low); + return lit; +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return FStar_UInt128_sub(a, b); +#else + return FStar_UInt128_sub_mod_impl(a, b); +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return _mm_and_si128(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low & b.low; + lit.high = a.high & b.high; + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return _mm_xor_si128(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low ^ b.low; + lit.high = a.high ^ b.high; + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + return _mm_or_si128(a, b); +#else + FStar_UInt128_uint128 lit; + lit.low = a.low | b.low; + lit.high = a.high | b.high; + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_lognot(FStar_UInt128_uint128 a) +{ +#if HAS_OPTIMIZED + return _mm_andnot_si128(a, a); +#else + FStar_UInt128_uint128 lit; + lit.low = ~a.low; + lit.high = ~a.high; + return lit; +#endif +} + +static const uint32_t FStar_UInt128_u32_64 = (uint32_t)64U; + +inline static uint64_t +FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s) +{ + return (hi << s) + (lo >> FStar_UInt128_u32_64 - s); +} + +inline static uint64_t +FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s) +{ + return FStar_UInt128_add_u64_shift_left(hi, lo, s); +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s == (uint32_t)0U) + return a; + else { + FStar_UInt128_uint128 lit; + lit.low = a.low << s; + lit.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s); + return lit; + } +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s) +{ + FStar_UInt128_uint128 lit; + lit.low = (uint64_t)0U; + lit.high = a.low << s - FStar_UInt128_u32_64; + return lit; +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s) +{ +#if HAS_OPTIMIZED + if (s == 0) { + return a; + } else if (s < FStar_UInt128_u32_64) { + uint64_t l = a.low << s; + uint64_t h = __shiftleft128(a.low, a.high, (unsigned char)s); + return _mm_set_epi64x(h, l); + } else { + return _mm_set_epi64x(a.low << (s - FStar_UInt128_u32_64), 0); + } +#else + if (s < FStar_UInt128_u32_64) + return FStar_UInt128_shift_left_small(a, s); + else + return FStar_UInt128_shift_left_large(a, s); +#endif +} + +inline static uint64_t +FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s) +{ + return (lo >> s) + (hi << FStar_UInt128_u32_64 - s); +} + +inline static uint64_t +FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s) +{ + return FStar_UInt128_add_u64_shift_right(hi, lo, s); +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s) +{ + if (s == (uint32_t)0U) + return a; + else { + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s); + lit.high = a.high >> s; + return lit; + } +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s) +{ + FStar_UInt128_uint128 lit; + lit.low = a.high >> s - FStar_UInt128_u32_64; + lit.high = (uint64_t)0U; + return lit; +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s) +{ +#if HAS_OPTIMIZED + if (s == 0) { + return a; + } else if (s < FStar_UInt128_u32_64) { + uint64_t l = __shiftright128(a.low, a.high, (unsigned char)s); + uint64_t h = a.high >> s; + return _mm_set_epi64x(h, l); + } else { + return _mm_set_epi64x(0, a.high >> (s - FStar_UInt128_u32_64)); + } +#else + if (s < FStar_UInt128_u32_64) + return FStar_UInt128_shift_right_small(a, s); + else + return FStar_UInt128_shift_right_large(a, s); +#endif +} + +inline static bool +FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.low == b.low && a.high == b.high; +} + +inline static bool +FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high > b.high || a.high == b.high && a.low > b.low; +} + +inline static bool +FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high < b.high || a.high == b.high && a.low < b.low; +} + +inline static bool +FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high > b.high || a.high == b.high && a.low >= b.low; +} + +inline static bool +FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ + return a.high < b.high || a.high == b.high && a.low <= b.low; +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED + // PCMPW to produce 4 32-bit values, all either 0x0 or 0xffffffff + __m128i r32 = _mm_cmpeq_epi32(a, b); + // Shuffle 3,2,1,0 into 2,3,0,1 (swapping dwords inside each half) + __m128i s32 = _mm_shuffle_epi32(r32, _MM_SHUFFLE(2, 3, 0, 1)); + // Bitwise and to compute (3&2),(2&3),(1&0),(0&1) + __m128i ret64 = _mm_and_si128(r32, s32); + // Swap the two 64-bit values to form s64 + __m128i s64 = + _mm_shuffle_epi32(ret64, _MM_SHUFFLE(1, 0, 3, 2)); // 3,2,1,0 -> 1,0,3,2 + // And them together + return _mm_and_si128(ret64, s64); +#else + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high); + lit.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) +{ +#if HAS_OPTIMIZED && 0 + // ge - compare 3,2,1,0 for >= and generating 0 or 0xffffffff for each + // eq - compare 3,2,1,0 for == and generating 0 or 0xffffffff for each + // slot 0 = ge0 | (eq0 & ge1) | (eq0 & eq1 & ge2) | (eq0 & eq1 & eq2 & ge3) + // then splat slot 0 to 3,2,1,0 + __m128i gt = _mm_cmpgt_epi32(a, b); + __m128i eq = _mm_cmpeq_epi32(a, b); + __m128i ge = _mm_or_si128(gt, eq); + __m128i ge0 = ge; + __m128i eq0 = eq; + __m128i ge1 = _mm_srli_si128(ge, 4); // shift ge from 3,2,1,0 to 0x0,3,2,1 + __m128i t1 = _mm_and_si128(eq0, ge1); + __m128i ret = _mm_or_si128(ge, t1); // ge0 | (eq0 & ge1) is now in 0 + __m128i eq1 = _mm_srli_si128(eq, 4); // shift eq from 3,2,1,0 to 0x0,3,2,1 + __m128i ge2 = + _mm_srli_si128(ge1, 4); // shift original ge from 3,2,1,0 to 0x0,0x0,3,2 + __m128i t2 = + _mm_and_si128(eq0, _mm_and_si128(eq1, ge2)); // t2 = (eq0 & eq1 & ge2) + ret = _mm_or_si128(ret, t2); + __m128i eq2 = _mm_srli_si128(eq1, 4); // shift eq from 3,2,1,0 to 0x0,00,00,3 + __m128i ge3 = + _mm_srli_si128(ge2, 4); // shift original ge from 3,2,1,0 to 0x0,0x0,0x0,3 + __m128i t3 = _mm_and_si128( + eq0, _mm_and_si128( + eq1, _mm_and_si128(eq2, ge3))); // t3 = (eq0 & eq1 & eq2 & ge3) + ret = _mm_or_si128(ret, t3); + return _mm_shuffle_epi32( + ret, + _MM_SHUFFLE(0, 0, 0, 0)); // the result is in 0. Shuffle into all dwords. +#else + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt64_gte_mask(a.high, b.high) & + ~FStar_UInt64_eq_mask(a.high, b.high) | + FStar_UInt64_eq_mask(a.high, b.high) & + FStar_UInt64_gte_mask(a.low, b.low); + lit.high = FStar_UInt64_gte_mask(a.high, b.high) & + ~FStar_UInt64_eq_mask(a.high, b.high) | + FStar_UInt64_eq_mask(a.high, b.high) & + FStar_UInt64_gte_mask(a.low, b.low); + return lit; +#endif +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_uint64_to_uint128(uint64_t a) +{ +#if HAS_OPTIMIZED + return _mm_set_epi64x(0, a); +#else + FStar_UInt128_uint128 lit; + lit.low = a; + lit.high = (uint64_t)0U; + return lit; +#endif +} + +inline static uint64_t +FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a) +{ + return a.low; +} + +inline static uint64_t +FStar_UInt128_u64_mod_32(uint64_t a) +{ + return a & (uint64_t)0xffffffffU; +} + +static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U; + +inline static uint64_t +FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo) +{ + return lo + (hi << FStar_UInt128_u32_32); +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_mul32(uint64_t x, uint32_t y) +{ +#if HAS_OPTIMIZED + uint64_t l, h; + l = _umul128(x, (uint64_t)y, &h); + return _mm_set_epi64x(h, l); +#else + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt128_u32_combine( + (x >> FStar_UInt128_u32_32) * (uint64_t)y + + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> + FStar_UInt128_u32_32), + FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * (uint64_t)y)); + lit.high = (x >> FStar_UInt128_u32_32) * (uint64_t)y + + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> + FStar_UInt128_u32_32) >> + FStar_UInt128_u32_32; + return lit; +#endif +} + +/* Note: static headers bring scope collision issues when they define types! + * Because now client (karamel-generated) code will include this header and + * there might be type collisions if the client code uses quadruples of uint64s. + * So, we cannot use the karamel-generated name. */ +typedef struct K_quad_s { + uint64_t fst; + uint64_t snd; + uint64_t thd; + uint64_t f3; +} K_quad; + +inline static K_quad +FStar_UInt128_mul_wide_impl_t_(uint64_t x, uint64_t y) +{ + K_quad tmp; + tmp.fst = FStar_UInt128_u64_mod_32(x); + tmp.snd = FStar_UInt128_u64_mod_32( + FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)); + tmp.thd = x >> FStar_UInt128_u32_32; + tmp.f3 = (x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> + FStar_UInt128_u32_32); + return tmp; +} + +static uint64_t +FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo) +{ + return lo + (hi << FStar_UInt128_u32_32); +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_mul_wide_impl(uint64_t x, uint64_t y) +{ + K_quad scrut = + FStar_UInt128_mul_wide_impl_t_(x, y); + uint64_t u1 = scrut.fst; + uint64_t w3 = scrut.snd; + uint64_t x_ = scrut.thd; + uint64_t t_ = scrut.f3; + FStar_UInt128_uint128 lit; + lit.low = FStar_UInt128_u32_combine_( + u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_), w3); + lit.high = + x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) + + (u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_) >> + FStar_UInt128_u32_32); + return lit; +} + +inline static FStar_UInt128_uint128 +FStar_UInt128_mul_wide(uint64_t x, uint64_t y) +{ +#if HAS_OPTIMIZED + uint64_t l, h; + l = _umul128(x, y, &h); + return _mm_set_epi64x(h, l); +#else + return FStar_UInt128_mul_wide_impl(x, y); +#endif +} + +#undef low +#undef high + +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h new file mode 100644 index 000000000..61fe85c49 --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h @@ -0,0 +1,84 @@ +/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. + Licensed under the Apache 2.0 License. */ + +#ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H +#define FSTAR_UINT128_STRUCT_ENDIANNESS_H + +/* Hand-written implementation of endianness-related uint128 functions + * for the extracted uint128 implementation */ + +/* Access 64-bit fields within the int128. */ +#define HIGH64_OF(x) ((x)->high) +#define LOW64_OF(x) ((x)->low) + +/* A series of definitions written using pointers. */ + +inline static void +load128_le_(uint8_t *b, uint128_t *r) +{ + LOW64_OF(r) = load64_le(b); + HIGH64_OF(r) = load64_le(b + 8); +} + +inline static void +store128_le_(uint8_t *b, uint128_t *n) +{ + store64_le(b, LOW64_OF(n)); + store64_le(b + 8, HIGH64_OF(n)); +} + +inline static void +load128_be_(uint8_t *b, uint128_t *r) +{ + HIGH64_OF(r) = load64_be(b); + LOW64_OF(r) = load64_be(b + 8); +} + +inline static void +store128_be_(uint8_t *b, uint128_t *n) +{ + store64_be(b, HIGH64_OF(n)); + store64_be(b + 8, LOW64_OF(n)); +} + +#ifndef KRML_NOSTRUCT_PASSING + +inline static uint128_t +load128_le(uint8_t *b) +{ + uint128_t r; + load128_le_(b, &r); + return r; +} + +inline static void +store128_le(uint8_t *b, uint128_t n) +{ + store128_le_(b, &n); +} + +inline static uint128_t +load128_be(uint8_t *b) +{ + uint128_t r; + load128_be_(b, &r); + return r; +} + +inline static void +store128_be(uint8_t *b, uint128_t n) +{ + store128_be_(b, &n); +} + +#else /* !defined(KRML_STRUCT_PASSING) */ + +#define print128 print128_ +#define load128_le load128_le_ +#define store128_le store128_le_ +#define load128_be load128_be_ +#define store128_be store128_be_ + +#endif /* KRML_STRUCT_PASSING */ + +#endif diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def b/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def new file mode 100644 index 000000000..c4ab8e38e --- /dev/null +++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def @@ -0,0 +1,11 @@ +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 |