Merge pull request #245 from cryspen/franziskus/towards-ml-kem-c-extr…

…action1

Workarounds for Charon issues in portable ml-kem

.gitignore

@@ -11,3 +11,4 @@ fuzz/artifacts
 proofs/fstar/extraction/.cache
 __pycache__
 kyber-crate/
+*.llbc

libcrux-ml-kem/.gitignore

@@ -1,3 +1,4 @@
 Cargo.lock
 proofs/fstar/extraction/.cache/
 proofs/fstar/extraction/.depend
+c

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

libcrux-ml-kem/src/sampling.rs

@@ -158,23 +158,25 @@ pub(super) fn sample_from_xof<const K: usize>(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;
+ }
  }
  }
  }

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;