From a197c4d7286246d59e3044d437b3da9119cd5de8 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Wed, 11 Dec 2024 06:54:20 +0000 Subject: [PATCH] fmt --- libcrux-ml-kem/src/ind_cpa.rs | 9 ++++-- libcrux-ml-kem/src/polynomial.rs | 52 ++++++++++++++++++++----------- libcrux-ml-kem/src/vector/avx2.rs | 23 +++++++++----- 3 files changed, 57 insertions(+), 27 deletions(-) diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index 144e79e48..e05db7edf 100644 --- 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 { pub(crate) coefficients: [Vector; VECTORS_IN_RING_ELEMENT], } - #[allow(non_snake_case)] fn ZERO() -> PolynomialRingElement { PolynomialRingElement { @@ -88,7 +87,10 @@ fn from_i16_array(a: &[i16]) -> PolynomialRingElement(myself: &mut PolynomialRingElement, rhs: &PolynomialRingElement) { +fn add_to_ring_element( + myself: &mut PolynomialRingElement, + rhs: &PolynomialRingElement, +) { // 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(myself: &mut PolynomialRingElement(myself: &PolynomialRingElement, mut b: PolynomialRingElement) -> PolynomialRingElement { +fn subtract_reduce( + myself: &PolynomialRingElement, + mut b: PolynomialRingElement, +) -> PolynomialRingElement { // 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(myself: &PolynomialRingElement, message: &PolynomialRingElement, mut result: PolynomialRingElement) -> PolynomialRingElement { +fn add_message_error_reduce( + myself: &PolynomialRingElement, + message: &PolynomialRingElement, + mut result: PolynomialRingElement, +) -> PolynomialRingElement { // 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,7 +166,10 @@ fn add_message_error_reduce(myself: &PolynomialRingElement(myself: &mut PolynomialRingElement, error: &PolynomialRingElement) { +fn add_error_reduce( + myself: &mut PolynomialRingElement, + error: &PolynomialRingElement, +) { // 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 @@ -163,17 +177,18 @@ fn add_error_reduce(myself: &mut PolynomialRingElement(myself: &mut PolynomialRingElement, error: &PolynomialRingElement) { +fn add_standard_error_reduce( + myself: &mut PolynomialRingElement, + error: &PolynomialRingElement, +) { // 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(myself: &mut PolynomialRingElem // calling to_montgomery_domain() on them should return a mod q. let coefficient_normal_form = to_standard_domain::(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(myself: &mut PolynomialRingElem // ))))] #[inline(always)] #[hax_lib::fstar::verification_status(lax)] -fn ntt_multiply(myself: &PolynomialRingElement, rhs: &PolynomialRingElement) -> PolynomialRingElement { +fn ntt_multiply( + myself: &PolynomialRingElement, + rhs: &PolynomialRingElement, +) -> PolynomialRingElement { let mut out = ZERO(); for i in 0..VECTORS_IN_RING_ELEMENT { @@ -266,7 +282,7 @@ impl PolynomialRingElement { /// sum of their constituent coefficients. #[inline(always)] pub(crate) fn add_to_ring_element(&mut self, rhs: &Self) { - add_to_ring_element::(self, rhs); + add_to_ring_element::(self, rhs); } #[inline(always)] diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs index 045d2a4e7..31ff6debe 100644 --- 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(vector: SIMD256Vector) -> SIMD256Vector { SIMD256Vector { - elements: compress::compress_ciphertext_coefficient::( - vector.elements, - ), + elements: compress::compress_ciphertext_coefficient::(vector.elements), } } @@ -90,7 +88,13 @@ fn compress(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), }