From eddefaeb56068fd6c046e51312350077864c55f9 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 2 May 2024 12:46:45 +0200 Subject: [PATCH] Workarounds for Charon issues --- .gitignore | 1 + libcrux-ml-kem/.gitignore | 1 + libcrux-ml-kem/c.sh | 2 +- libcrux-ml-kem/src/sampling.rs | 36 +++++++++++++++-------------- libcrux-ml-kem/src/simd/portable.rs | 14 +++++------ 5 files changed, 29 insertions(+), 25 deletions(-) diff --git a/.gitignore b/.gitignore index 5c3e1d548..f2eb8a8ef 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,4 @@ fuzz/artifacts proofs/fstar/extraction/.cache __pycache__ kyber-crate/ +*.llbc diff --git a/libcrux-ml-kem/.gitignore b/libcrux-ml-kem/.gitignore index af27795c5..fed5ebf9b 100644 --- a/libcrux-ml-kem/.gitignore +++ b/libcrux-ml-kem/.gitignore @@ -1,3 +1,4 @@ Cargo.lock proofs/fstar/extraction/.cache/ proofs/fstar/extraction/.depend +c diff --git a/libcrux-ml-kem/c.sh b/libcrux-ml-kem/c.sh index 7a74b06ee..3b1f8b3e8 100755 --- a/libcrux-ml-kem/c.sh +++ b/libcrux-ml-kem/c.sh @@ -15,7 +15,7 @@ mkdir -p c cd c echo "Running eurydice ..." -$EURYDICE_HOME/eurydice --config ../c.yaml ../libcrux_kyber.llbc +$EURYDICE_HOME/eurydice --config ../c.yaml ../../libcrux_ml_kem.llbc cp $EURYDICE_HOME/include/eurydice_glue.h . if [[ -n "$HACL_PACKAGES_HOME" ]]; then diff --git a/libcrux-ml-kem/src/sampling.rs b/libcrux-ml-kem/src/sampling.rs index 002b85488..74edc5c2b 100644 --- a/libcrux-ml-kem/src/sampling.rs +++ b/libcrux-ml-kem/src/sampling.rs @@ -158,23 +158,25 @@ pub(super) fn sample_from_xof(seeds: [[u8; 34]; K]) -> [Polynomi fn sample_from_binomial_distribution_2(randomness: &[u8]) -> PolynomialRingElement { let mut sampled_i32s = [0i32; 256]; - for (chunk_number, byte_chunk) in randomness.chunks_exact(4).enumerate() { - let random_bits_as_u32: u32 = (byte_chunk[0] as u32) - | (byte_chunk[1] as u32) << 8 - | (byte_chunk[2] as u32) << 16 - | (byte_chunk[3] as u32) << 24; - - let even_bits = random_bits_as_u32 & 0x55555555; - let odd_bits = (random_bits_as_u32 >> 1) & 0x55555555; - let coin_toss_outcomes = even_bits + odd_bits; - - cloop! { - for outcome_set in (0..u32::BITS).step_by(4) { - let outcome_1 = ((coin_toss_outcomes >> outcome_set) & 0x3) as i32; - let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 2)) & 0x3) as i32; - - let offset = (outcome_set >> 2) as usize; - sampled_i32s[8 * chunk_number + offset] = outcome_1 - outcome_2; + cloop! { + for (chunk_number, byte_chunk) in randomness.chunks_exact(4).enumerate() { + let random_bits_as_u32: u32 = (byte_chunk[0] as u32) + | (byte_chunk[1] as u32) << 8 + | (byte_chunk[2] as u32) << 16 + | (byte_chunk[3] as u32) << 24; + + let even_bits = random_bits_as_u32 & 0x55555555; + let odd_bits = (random_bits_as_u32 >> 1) & 0x55555555; + let coin_toss_outcomes = even_bits + odd_bits; + + cloop! { + for outcome_set in (0..u32::BITS).step_by(4) { + let outcome_1 = ((coin_toss_outcomes >> outcome_set) & 0x3) as i32; + let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 2)) & 0x3) as i32; + + let offset = (outcome_set >> 2) as usize; + sampled_i32s[8 * chunk_number + offset] = outcome_1 - outcome_2; + } } } } diff --git a/libcrux-ml-kem/src/simd/portable.rs b/libcrux-ml-kem/src/simd/portable.rs index 7fd8d9820..f0cbff6fc 100644 --- a/libcrux-ml-kem/src/simd/portable.rs +++ b/libcrux-ml-kem/src/simd/portable.rs @@ -228,7 +228,7 @@ fn ntt_multiply( zeta0: i32, zeta1: i32, ) -> PortableVector { - let mut out = PortableVector::ZERO(); + let mut out = ZERO(); let product = ntt_multiply_binomials( (lhs.elements[0], lhs.elements[1]), (rhs.elements[0], rhs.elements[1]), @@ -275,7 +275,7 @@ fn serialize_1(v: PortableVector) -> u8 { #[inline(always)] fn deserialize_1(v: u8) -> PortableVector { - let mut result = PortableVector::ZERO(); + let mut result = ZERO(); for i in 0..FIELD_ELEMENTS_IN_VECTOR { result.elements[i] = ((v >> i) & 0x1) as i32; } @@ -297,7 +297,7 @@ fn serialize_4(v: PortableVector) -> [u8; 4] { #[inline(always)] fn deserialize_4(bytes: &[u8]) -> PortableVector { - let mut v = PortableVector::ZERO(); + let mut v = ZERO(); v.elements[0] = (bytes[0] & 0x0F) as i32; v.elements[1] = ((bytes[0] >> 4) & 0x0F) as i32; @@ -329,7 +329,7 @@ fn serialize_5(v: PortableVector) -> [u8; 5] { #[inline(always)] fn deserialize_5(bytes: &[u8]) -> PortableVector { - let mut v = PortableVector::ZERO(); + let mut v = ZERO(); v.elements[0] = (bytes[0] & 0x1F) as i32; v.elements[1] = ((bytes[1] & 0x3) << 3 | (bytes[0] >> 5)) as i32; @@ -364,7 +364,7 @@ fn serialize_10(v: PortableVector) -> [u8; 10] { #[inline(always)] fn deserialize_10(bytes: &[u8]) -> PortableVector { - let mut result = PortableVector::ZERO(); + let mut result = ZERO(); result.elements[0] = ((bytes[1] as i32 & 0x03) << 8 | (bytes[0] as i32 & 0xFF)) as i32; result.elements[1] = ((bytes[2] as i32 & 0x0F) << 6 | (bytes[1] as i32 >> 2)) as i32; @@ -398,7 +398,7 @@ fn serialize_11(v: PortableVector) -> [u8; 11] { #[inline(always)] fn deserialize_11(bytes: &[u8]) -> PortableVector { - let mut result = PortableVector::ZERO(); + let mut result = ZERO(); result.elements[0] = ((bytes[1] as i32 & 0x7) << 8 | bytes[0] as i32) as i32; result.elements[1] = ((bytes[2] as i32 & 0x3F) << 5 | (bytes[1] as i32 >> 3)) as i32; result.elements[2] = ((bytes[4] as i32 & 0x1) << 10 @@ -438,7 +438,7 @@ fn serialize_12(v: PortableVector) -> [u8; 12] { #[inline(always)] fn deserialize_12(bytes: &[u8]) -> PortableVector { - let mut re = PortableVector::ZERO(); + let mut re = ZERO(); let byte0 = bytes[0] as i32; let byte1 = bytes[1] as i32;