fixed fmt

cryspen · Jun 11, 2024 · ccc7d28 · ccc7d28
1 parent 463f84c
commit ccc7d28
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 37 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti
@@ -17,9 +17,6 @@ let v_COEFFICIENTS_IN_RING_ELEMENT: usize = Rust_primitives.Hax.dropped_body
 
 let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = Rust_primitives.Hax.dropped_body
 
-/// Field modulus: 3329
-let v_FIELD_MODULUS: i16 = Rust_primitives.Hax.dropped_body
-
 /// SHA3 512 digest size
 let v_G_DIGEST_SIZE: usize = Rust_primitives.Hax.dropped_body
 

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.fsti
@@ -60,7 +60,7 @@ val compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
       (requires
         (coefficient_bits =. 4uy || coefficient_bits =. 5uy || coefficient_bits =. 10uy ||
         coefficient_bits =. 11uy) &&
-        fe <. (cast (Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i16) <: u16))
+        fe <. (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS <: i16) <: u16))
       (ensures
         fun result ->
           let result:i16 = result in
@@ -84,7 +84,7 @@ val compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 val compress_message_coefficient (fe: u16)
     : Prims.Pure u8
-      (requires fe <. (cast (Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i16) <: u16))
+      (requires fe <. (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS <: i16) <: u16))
       (ensures
         fun result ->
           let result:u8 = result in
@@ -125,7 +125,9 @@ val montgomery_reduce_element (value: i32)
     : Prims.Pure i16
       (requires
         value >=.
-        ((cast (Core.Ops.Arith.Neg.neg Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS <: i16) <: i32) *!
+        ((Core.Ops.Arith.Neg.neg (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS <: i16) <: i32)
+            <:
+            i32) *!
           v_MONTGOMERY_R
           <:
           i32) &&

diff --git a/libcrux-ml-kem/src/constants.rs b/libcrux-ml-kem/src/constants.rs
@@ -1,7 +1,3 @@
-#[cfg(hax)]
-/// Field modulus: 3329
-pub(crate) const FIELD_MODULUS: i16 = 3329;
-
 /// Each field element needs floor(log_2(FIELD_MODULUS)) + 1 = 12 bits to represent
 pub(crate) const BITS_PER_COEFFICIENT: usize = 12;
 

diff --git a/libcrux-ml-kem/src/hash_functions.rs b/libcrux-ml-kem/src/hash_functions.rs
@@ -174,47 +174,29 @@ pub(crate) mod avx2 {
             let mut out1 = [0u8; LEN];
             let mut out2 = [0u8; LEN];
             let mut out3 = [0u8; LEN];
-            
+
             match K as u8 {
                 2 => {
                     x4::shake256(
-                        &input[0],
-                        &input[1],
-                        &input[0],
-                        &input[0],
-                        &mut out0,
-                        &mut out1,
-                        &mut out2,
-                        &mut out3,
+                        &input[0], &input[1], &input[0], &input[0], &mut out0, &mut out1,
+                        &mut out2, &mut out3,
                     );
                     out[0] = out0;
                     out[1] = out1;
                 }
                 3 => {
                     x4::shake256(
-                        &input[0],
-                        &input[1],
-                        &input[2],
-                        &input[0],
-                        &mut out0,
-                        &mut out1,
-                        &mut out2,
-                        &mut out3,
+                        &input[0], &input[1], &input[2], &input[0], &mut out0, &mut out1,
+                        &mut out2, &mut out3,
                     );
                     out[0] = out0;
                     out[1] = out1;
                     out[2] = out2;
                 }
                 4 => {
                     x4::shake256(
-                        &input[0],
-                        &input[1],
-                        &input[2],
-                        &input[3],
-                        &mut out0,
-                        &mut out1,
-                        &mut out2,
-                        &mut out3,
+                        &input[0], &input[1], &input[2], &input[3], &mut out0, &mut out1,
+                        &mut out2, &mut out3,
                     );
                     out[0] = out0;
                     out[1] = out1;

diff --git a/libcrux-ml-kem/src/vector.rs b/libcrux-ml-kem/src/vector.rs
@@ -143,7 +143,7 @@ fn montgomery_multiply_by_constant(mut v: PortableVector, c: i16) -> PortableVec
 ///
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
-#[cfg_attr(hax, hax_lib::requires(fe < (crate::constants::FIELD_MODULUS as u16)))]
+#[cfg_attr(hax, hax_lib::requires(fe < (FIELD_MODULUS as u16)))]
 #[cfg_attr(hax, hax_lib::ensures(|result|
         hax_lib::implies(833 <= fe && fe <= 2596, || result == 1) &&
         hax_lib::implies(!(833 <= fe && fe <= 2596), || result == 0)
@@ -179,7 +179,7 @@ pub(crate) fn compress_message_coefficient(fe: u16) -> u8 {
          coefficient_bits == 5 ||
          coefficient_bits == 10 ||
          coefficient_bits == 11) &&
-         fe < (crate::constants::FIELD_MODULUS as u16)))]
+         fe < (FIELD_MODULUS as u16)))]
 #[cfg_attr(hax,
      hax_lib::ensures(
      |result| result >= 0 && result < 2i16.pow(coefficient_bits as u32)))]