Skip to content

Commit

Permalink
fixed conflict
Browse files Browse the repository at this point in the history
  • Loading branch information
karthikbhargavan committed Jun 27, 2024
2 parents e6b6397 + 7d40ffc commit d3ca0bd
Show file tree
Hide file tree
Showing 42 changed files with 20,255 additions and 217 deletions.
23 changes: 23 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ members = [
"libcrux-kem",
"libcrux-hmac",
"libcrux-hkdf",
"libcrux-ecdh",
"libcrux-ecdh", "libcrux-psq",
]

[workspace.package]
Expand Down
2 changes: 1 addition & 1 deletion benchmarks/benches/sha2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ macro_rules! impl_comp {
($fun:ident, $libcrux:expr, $ring:expr, $rust_crypto:ty, $openssl:expr) => {
// Comparing libcrux performance for different payload sizes and other implementations.
fn $fun(c: &mut Criterion) {
const PAYLOAD_SIZES: [usize; 1] = [1024 * 1024 * 10];
const PAYLOAD_SIZES: [usize; 5] = [100, 1024, 2048, 4096, 8192];

let mut group = c.benchmark_group(stringify!($fun).replace("_", " "));

Expand Down
5 changes: 4 additions & 1 deletion libcrux-ml-kem/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,12 @@ libcrux-intrinsics = { version = "0.0.2-pre.2", path = "../libcrux-intrinsics" }
hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/" }

[features]
default = ["std"]
default = ["std", "mlkem512", "mlkem768", "mlkem1024"]
simd128 = ["libcrux-sha3/simd128"]
simd256 = ["libcrux-sha3/simd256"]
mlkem512 = []
mlkem768 = []
mlkem1024 = []
std = []
kyber = []

Expand Down
26 changes: 17 additions & 9 deletions libcrux-ml-kem/c.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,10 @@ portable_only=0
no_hacl=0
no_charon=0
clean=0
config=c.yaml
out=c
glue=$EURYDICE_HOME/include/eurydice_glue.h
features=

# Parse command line arguments.
all_args=("$@")
Expand All @@ -25,6 +29,10 @@ while [ $# -gt 0 ]; do
--no-hacl) no_hacl=1 ;;
--no-charon) no_charon=1 ;;
-c | --clean) clean=1 ;;
--config) config="$2"; shift ;;
--out) out="$2"; shift ;;
--glue) glue="$2"; shift ;;
--mlkem768) features="--cargo-arg=--no-default-features --cargo-arg=--features=mlkem768" ;;
esac
shift
done
Expand All @@ -38,20 +46,20 @@ fi
if [[ "$no_charon" = 0 ]]; then
rm -rf ../libcrux_ml_kem.llbc ../libcrux_sha3.llbc
echo "Running charon (sha3) ..."
(cd ../libcrux-sha3 && RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon --errors-as-warnings)
(cd ../libcrux-sha3 && RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon)
if ! [[ -f ../libcrux_sha3.llbc ]]; then
echo "😱😱😱 You are the victim of this bug: https://hacspec.zulipchat.com/#narrow/stream/433829-Circus/topic/charon.20declines.20to.20generate.20an.20llbc.20file"
echo "Suggestion: rm -rf ../target or cargo clean"
exit 1
fi
echo "Running charon (ml-kem) ..."
RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon --errors-as-warnings
RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon $features
else
echo "Skipping charon"
fi

mkdir -p c
cd c
mkdir -p $out
cd $out

# Clean only when requesting it.
# Note that we can not extract for all platforms on any platform right now.
Expand All @@ -62,18 +70,18 @@ if [[ "$clean" = 1 ]]; then
fi

echo "Running eurydice ..."
$EURYDICE_HOME/eurydice --config ../c.yaml ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc
$EURYDICE_HOME/eurydice --config ../$config ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc
cp $EURYDICE_HOME/include/eurydice_glue.h .

clang-format --style=Google -i *.c *.h
clang-format --style=Google -i internal/*.h
clang-format --style=Google -i intrinsics/*.h

# Write out infos about the used tools
[ -n "$CHARON_REV" ] || export CHARON_REV=$(git -C $CHARON_HOME rev-parse HEAD)
[ -n "$EURYDICE_REV" ] || export EURYDICE_REV=$(git -C $EURYDICE_HOME rev-parse HEAD)
[ -n "$KRML_REV" ] || export KRML_REV=$(git -C $KRML_HOME rev-parse HEAD)
[ -n "$FSTAR_REV" ] || export FSTAR_REV=$(git -C $FSTAR_HOME rev-parse HEAD)
[[ -z "$CHARON_REV" && -d $CHARON_HOME/.git ]] && export CHARON_REV=$(git -C $CHARON_HOME rev-parse HEAD)
[[ -z "$EURYDICE_REV" && -d $EURYDICE_HOME/.git ]] && export EURYDICE_REV=$(git -C $EURYDICE_HOME rev-parse HEAD)
[[ -z "$KRML_REV" && -d $KRML_HOME/.git ]] && export KRML_REV=$(git -C $KRML_HOME rev-parse HEAD)
[[ -z "$FSTAR_REV" && -d $FSTAR_HOME/.git ]] && export FSTAR_REV=$(git -C $FSTAR_HOME rev-parse HEAD)
rm -f code_gen.txt
echo "This code was generated with the following tools:" >> code_gen.txt
echo -n "Charon: " >> code_gen.txt
Expand Down
11 changes: 0 additions & 11 deletions libcrux-ml-kem/c/internal/libcrux_core.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,6 @@ extern "C" {
#include "../libcrux_core.h"
#include "eurydice_glue.h"

extern void core_fmt_rt__core__fmt__rt__Argument__a__1__none(
core_fmt_rt_Argument *x0);

extern core_fmt_Arguments core_fmt__core__fmt__Arguments__a__2__new_v1(
Eurydice_slice x0, Eurydice_slice x1);

#define CORE_NUM__U32_8__BITS (32U)

static inline uint32_t core_num__u8_6__count_ones(uint8_t x0);
Expand Down Expand Up @@ -216,11 +210,6 @@ void core_result__core__result__Result_T__E___unwrap__uint8_t_10size_t__core_arr
core_result_Result__uint8_t_10size_t__core_array_TryFromSliceError self,
uint8_t ret[10U]);

typedef struct core_option_Option__Eurydice_slice_uint8_t_s {
core_option_Option__size_t_tags tag;
Eurydice_slice f0;
} core_option_Option__Eurydice_slice_uint8_t;

typedef struct
core_result_Result__int16_t_16size_t__core_array_TryFromSliceError_s {
core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;
Expand Down
115 changes: 52 additions & 63 deletions libcrux-ml-kem/c/libcrux_mlkem_portable.c
Original file line number Diff line number Diff line change
Expand Up @@ -2206,72 +2206,61 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_
inline size_t libcrux_ml_kem_vector_portable_sampling_rej_sample(
Eurydice_slice a, Eurydice_slice result) {
size_t sampled = (size_t)0U;
core_slice_iter_Chunks iter =
core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter(
core_slice___Slice_T___chunks(a, (size_t)3U, uint8_t,
core_slice_iter_Chunks),
core_slice_iter_Chunks, core_slice_iter_Chunks);
while (true) {
core_option_Option__Eurydice_slice_uint8_t uu____0 =
core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next(
&iter, uint8_t, core_option_Option__Eurydice_slice_uint8_t);
if (uu____0.tag == core_option_None) {
break;
} else {
Eurydice_slice bytes = uu____0.f0;
int16_t b1 = (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t,
uint8_t *, uint8_t);
int16_t b2 = (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t,
uint8_t *, uint8_t);
int16_t b3 = (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t,
uint8_t *, uint8_t);
int16_t d1 = (b2 & (int16_t)15) << 8U | b1;
int16_t d2 = b3 << 4U | b2 >> 4U;
bool uu____1;
int16_t uu____2;
bool uu____3;
size_t uu____4;
int16_t uu____5;
size_t uu____6;
int16_t uu____7;
if (d1 < LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS) {
if (sampled < (size_t)16U) {
int16_t uu____8 = d1;
Eurydice_slice_index(result, sampled, int16_t, int16_t *, int16_t) =
uu____8;
sampled++;
uu____2 = d2;
uu____7 = LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS;
uu____1 = uu____2 < uu____7;
if (uu____1) {
uu____4 = sampled;
uu____3 = uu____4 < (size_t)16U;
if (uu____3) {
uu____5 = d2;
uu____6 = sampled;
Eurydice_slice_index(result, uu____6, int16_t, int16_t *,
int16_t) = uu____5;
sampled++;
continue;
}
for (size_t i = (size_t)0U;
i < core_slice___Slice_T___len(a, uint8_t, size_t) / (size_t)3U; i++) {
size_t i0 = i;
int16_t b1 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)0U,
uint8_t, uint8_t *, uint8_t);
int16_t b2 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)1U,
uint8_t, uint8_t *, uint8_t);
int16_t b3 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)2U,
uint8_t, uint8_t *, uint8_t);
int16_t d1 = (b2 & (int16_t)15) << 8U | b1;
int16_t d2 = b3 << 4U | b2 >> 4U;
bool uu____0;
int16_t uu____1;
bool uu____2;
size_t uu____3;
int16_t uu____4;
size_t uu____5;
int16_t uu____6;
if (d1 < LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS) {
if (sampled < (size_t)16U) {
int16_t uu____7 = d1;
Eurydice_slice_index(result, sampled, int16_t, int16_t *, int16_t) =
uu____7;
sampled++;
uu____1 = d2;
uu____6 = LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS;
uu____0 = uu____1 < uu____6;
if (uu____0) {
uu____3 = sampled;
uu____2 = uu____3 < (size_t)16U;
if (uu____2) {
uu____4 = d2;
uu____5 = sampled;
Eurydice_slice_index(result, uu____5, int16_t, int16_t *, int16_t) =
uu____4;
sampled++;
continue;
}
continue;
}
continue;
}
uu____2 = d2;
uu____7 = LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS;
uu____1 = uu____2 < uu____7;
if (uu____1) {
uu____4 = sampled;
uu____3 = uu____4 < (size_t)16U;
if (uu____3) {
uu____5 = d2;
uu____6 = sampled;
Eurydice_slice_index(result, uu____6, int16_t, int16_t *, int16_t) =
uu____5;
sampled++;
continue;
}
}
uu____1 = d2;
uu____6 = LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS;
uu____0 = uu____1 < uu____6;
if (uu____0) {
uu____3 = sampled;
uu____2 = uu____3 < (size_t)16U;
if (uu____2) {
uu____4 = d2;
uu____5 = sampled;
Eurydice_slice_index(result, uu____5, int16_t, int16_t *, int16_t) =
uu____4;
sampled++;
continue;
}
}
}
Expand Down
Loading

0 comments on commit d3ca0bd

Please sign in to comment.