fmt

cryspen · Dec 11, 2024 · a197c4d · a197c4d
1 parent 703cabd
commit a197c4d
Show file tree

Hide file tree

Showing 3 changed files with 57 additions and 27 deletions.
diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
@@ -178,7 +178,10 @@ pub(crate) fn serialize_secret_key<const K: usize, const OUT_LEN: usize, Vector:
 #[hax_lib::fstar::options(
     "--max_fuel 15 --z3rlimit 1500 --ext context_pruning --z3refresh --split_queries always"
 )]
-#[cfg_attr(hax, hax_lib::fstar::before("let sample_ring_element_cbd_helper_2
+#[cfg_attr(
+    hax,
+    hax_lib::fstar::before(
+        "let sample_ring_element_cbd_helper_2
       (v_K v_ETA2 v_ETA2_RANDOMNESS_SIZE: usize)
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -202,7 +205,9 @@ pub(crate) fn serialize_secret_key<const K: usize, const OUT_LEN: usize, Vector:
     =
     Lib.Sequence.eq_intro #(Spec.MLKEM.polynomial) #(v v_K)
     (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector error_1) 
-    (Spec.MLKEM.sample_vector_cbd2 #v_K (Seq.slice prf_input 0 32) (sz (v domain_separator)))"))]
+    (Spec.MLKEM.sample_vector_cbd2 #v_K (Seq.slice prf_input 0 32) (sz (v domain_separator)))"
+    )
+)]
 #[cfg_attr(
     hax,
     hax_lib::fstar::before(

diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs
@@ -65,7 +65,6 @@ pub(crate) struct PolynomialRingElement<Vector: Operations> {
     pub(crate) coefficients: [Vector; VECTORS_IN_RING_ELEMENT],
 }
 
-
 #[allow(non_snake_case)]
 fn ZERO<Vector: Operations>() -> PolynomialRingElement<Vector> {
     PolynomialRingElement {
@@ -88,7 +87,10 @@ fn from_i16_array<Vector: Operations>(a: &[i16]) -> PolynomialRingElement<Vector
 /// sum of their constituent coefficients.
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn add_to_ring_element<Vector: Operations, const K: usize>(myself: &mut PolynomialRingElement<Vector>, rhs: &PolynomialRingElement<Vector>) {
+fn add_to_ring_element<Vector: Operations, const K: usize>(
+    myself: &mut PolynomialRingElement<Vector>,
+    rhs: &PolynomialRingElement<Vector>,
+) {
     // The semicolon and parentheses at the end of loop are a workaround
     // for the following bug https://github.com/hacspec/hax/issues/720
     for i in 0..myself.coefficients.len() {
@@ -111,20 +113,29 @@ fn poly_barrett_reduce<Vector: Operations>(myself: &mut PolynomialRingElement<Ve
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn subtract_reduce<Vector: Operations>(myself: &PolynomialRingElement<Vector>, mut b: PolynomialRingElement<Vector>) -> PolynomialRingElement<Vector> {
+fn subtract_reduce<Vector: Operations>(
+    myself: &PolynomialRingElement<Vector>,
+    mut b: PolynomialRingElement<Vector>,
+) -> PolynomialRingElement<Vector> {
     // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting
     for i in 0..VECTORS_IN_RING_ELEMENT {
         let coefficient_normal_form =
             Vector::montgomery_multiply_by_constant(b.coefficients[i], 1441);
-        b.coefficients[i] =
-            Vector::barrett_reduce(Vector::sub(myself.coefficients[i], &coefficient_normal_form));
+        b.coefficients[i] = Vector::barrett_reduce(Vector::sub(
+            myself.coefficients[i],
+            &coefficient_normal_form,
+        ));
     }
     b
 }
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn add_message_error_reduce<Vector: Operations>(myself: &PolynomialRingElement<Vector>, message: &PolynomialRingElement<Vector>, mut result: PolynomialRingElement<Vector>) -> PolynomialRingElement<Vector> {
+fn add_message_error_reduce<Vector: Operations>(
+    myself: &PolynomialRingElement<Vector>,
+    message: &PolynomialRingElement<Vector>,
+    mut result: PolynomialRingElement<Vector>,
+) -> PolynomialRingElement<Vector> {
     // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting
     for i in 0..VECTORS_IN_RING_ELEMENT {
         let coefficient_normal_form =
@@ -155,25 +166,29 @@ fn add_message_error_reduce<Vector: Operations>(myself: &PolynomialRingElement<V
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn add_error_reduce<Vector: Operations>(myself: &mut PolynomialRingElement<Vector>, error: &PolynomialRingElement<Vector>) {
+fn add_error_reduce<Vector: Operations>(
+    myself: &mut PolynomialRingElement<Vector>,
+    error: &PolynomialRingElement<Vector>,
+) {
     // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting
     // The semicolon and parentheses at the end of loop are a workaround
     // for the following bug https://github.com/hacspec/hax/issues/720
     for j in 0..VECTORS_IN_RING_ELEMENT {
         let coefficient_normal_form =
             Vector::montgomery_multiply_by_constant(myself.coefficients[j], 1441);
 
-        myself.coefficients[j] = Vector::barrett_reduce(Vector::add(
-            coefficient_normal_form,
-            &error.coefficients[j],
-        ));
+        myself.coefficients[j] =
+            Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j]));
     }
     ()
 }
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn add_standard_error_reduce<Vector: Operations>(myself: &mut PolynomialRingElement<Vector>, error: &PolynomialRingElement<Vector>) {
+fn add_standard_error_reduce<Vector: Operations>(
+    myself: &mut PolynomialRingElement<Vector>,
+    error: &PolynomialRingElement<Vector>,
+) {
     // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting
     // The semicolon and parentheses at the end of loop are a workaround
     // for the following bug https://github.com/hacspec/hax/issues/720
@@ -182,10 +197,8 @@ fn add_standard_error_reduce<Vector: Operations>(myself: &mut PolynomialRingElem
         // calling to_montgomery_domain() on them should return a mod q.
         let coefficient_normal_form = to_standard_domain::<Vector>(myself.coefficients[j]);
 
-        myself.coefficients[j] = Vector::barrett_reduce(Vector::add(
-            coefficient_normal_form,
-            &error.coefficients[j],
-        ));
+        myself.coefficients[j] =
+            Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j]));
     }
     ()
 }
@@ -230,7 +243,10 @@ fn add_standard_error_reduce<Vector: Operations>(myself: &mut PolynomialRingElem
 // ))))]
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-fn ntt_multiply<Vector: Operations>(myself: &PolynomialRingElement<Vector>, rhs: &PolynomialRingElement<Vector>) -> PolynomialRingElement<Vector> {
+fn ntt_multiply<Vector: Operations>(
+    myself: &PolynomialRingElement<Vector>,
+    rhs: &PolynomialRingElement<Vector>,
+) -> PolynomialRingElement<Vector> {
     let mut out = ZERO();
 
     for i in 0..VECTORS_IN_RING_ELEMENT {
@@ -266,7 +282,7 @@ impl<Vector: Operations> PolynomialRingElement<Vector> {
     /// sum of their constituent coefficients.
     #[inline(always)]
     pub(crate) fn add_to_ring_element<const K: usize>(&mut self, rhs: &Self) {
-        add_to_ring_element::<Vector,K>(self, rhs);
+        add_to_ring_element::<Vector, K>(self, rhs);
     }
 
     #[inline(always)]

diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs
@@ -78,9 +78,7 @@ fn compress_1(vector: SIMD256Vector) -> SIMD256Vector {
         (forall (i:nat). i < 16 ==> bounded (Seq.index (repr $out) i) (v $COEFFICIENT_BITS))"))]
 fn compress<const COEFFICIENT_BITS: i32>(vector: SIMD256Vector) -> SIMD256Vector {
     SIMD256Vector {
-        elements: compress::compress_ciphertext_coefficient::<COEFFICIENT_BITS>(
-            vector.elements,
-        ),
+        elements: compress::compress_ciphertext_coefficient::<COEFFICIENT_BITS>(vector.elements),
     }
 }
 
@@ -90,7 +88,13 @@ fn compress<const COEFFICIENT_BITS: i32>(vector: SIMD256Vector) -> SIMD256Vector
                     Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3 /\\
                     Spec.Utils.is_i16b_array (11207+5*3328) (repr ${vector})"))]
 #[hax_lib::ensures(|out| fstar!("Spec.Utils.is_i16b_array (11207+6*3328) (repr $out)"))]
-fn ntt_layer_1_step(vector: SIMD256Vector, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> SIMD256Vector {
+fn ntt_layer_1_step(
+    vector: SIMD256Vector,
+    zeta0: i16,
+    zeta1: i16,
+    zeta2: i16,
+    zeta3: i16,
+) -> SIMD256Vector {
     SIMD256Vector {
         elements: ntt::ntt_layer_1_step(vector.elements, zeta0, zeta1, zeta2, zeta3),
     }
@@ -124,7 +128,13 @@ fn ntt_layer_3_step(vector: SIMD256Vector, zeta: i16) -> SIMD256Vector {
                     Spec.Utils.is_i16b 1664 zeta2 /\\ Spec.Utils.is_i16b 1664 zeta3  /\\
                     Spec.Utils.is_i16b_array (4*3328) (repr ${vector})"))]
 #[hax_lib::ensures(|out| fstar!("Spec.Utils.is_i16b_array 3328 (repr $out)"))]
-fn inv_ntt_layer_1_step(vector: SIMD256Vector, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> SIMD256Vector {
+fn inv_ntt_layer_1_step(
+    vector: SIMD256Vector,
+    zeta0: i16,
+    zeta1: i16,
+    zeta2: i16,
+    zeta3: i16,
+) -> SIMD256Vector {
     SIMD256Vector {
         elements: ntt::inv_ntt_layer_1_step(vector.elements, zeta0, zeta1, zeta2, zeta3),
     }
@@ -490,8 +500,7 @@ impl Operations for SIMD256Vector {
     #[requires(bytes.len() == 10)]
     #[inline(always)]
     fn deserialize_5(bytes: &[u8]) -> Self {
-        hax_lib::fstar!(
-            "assert (v (Core.Slice.impl__len $bytes) == Seq.length $bytes)");
+        hax_lib::fstar!("assert (v (Core.Slice.impl__len $bytes) == Seq.length $bytes)");
         Self {
             elements: serialize::deserialize_5(bytes),
         }