Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make more modules panic free #713

Open
wants to merge 16 commits into
base: main
Choose a base branch
from
Open

Make more modules panic free #713

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
7493d52
Make portable/sampling.rs panic-free
mamonet Dec 12, 2024
ddc982b
Fix MLKEM extract
mamonet Dec 12, 2024
cb45a8e
fmt
karthikbhargavan Dec 15, 2024
29e08c7
Merge branch 'dev' into dev-panic-free
karthikbhargavan Dec 15, 2024
8bfd6fc
verification status clarification
karthikbhargavan Dec 16, 2024
a40526d
Merge remote-tracking branch 'origin/dev' into dev-panic-free
mamonet Dec 17, 2024
61129bc
Make polynomial.rs panic-free
mamonet Dec 20, 2024
fdbede1
Remove commented out functions
mamonet Dec 20, 2024
2505360
Merge branch 'main' into dev-panic-free
karthikbhargavan Dec 20, 2024
3ee2d1f
fmt
karthikbhargavan Dec 20, 2024
d5ee5b1
Merge branch 'main' into dev-panic-free
franziskuskiefer Dec 23, 2024
979f296
Merge main into dev-panic-free
mamonet Jan 16, 2025
b83353c
Fix verification
mamonet Jan 17, 2025
7e5d393
Merge main into dev-panic-free
mamonet Jan 17, 2025
a157e78
Update verification_status.md
karthikbhargavan Jan 17, 2025
a7798a3
Update verification_status.md
karthikbhargavan Jan 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 38 additions & 16 deletions libcrux-ml-kem/c/libcrux_mlkem_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2644,6 +2644,16 @@ ntt_multiply_ef_79(libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *self,
return ntt_multiply_79(self, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.add_vector
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics

*/
static KRML_MUSTINLINE __m256i add_vector_79(__m256i lhs, __m256i *rhs) {
return libcrux_ml_kem_vector_avx2_add_9a(lhs, rhs);
}

/**
Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise
sum of their constituent coefficients.
Expand All @@ -2657,14 +2667,16 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_ab(
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *rhs) {
__m256i _myself[16U];
memcpy(_myself, myself->coefficients, (size_t)16U * sizeof(__m256i));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(Eurydice_array_to_slice(
(size_t)16U, myself->coefficients, __m256i),
__m256i);
i++) {
size_t i0 = i;
myself->coefficients[i0] = libcrux_ml_kem_vector_avx2_add_9a(
myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] =
add_vector_79(myself->coefficients[i0], &rhs->coefficients[i0]);
}
}

Expand Down Expand Up @@ -2711,8 +2723,7 @@ static KRML_MUSTINLINE void add_standard_error_reduce_79(
__m256i coefficient_normal_form =
to_standard_domain_79(myself->coefficients[j]);
myself->coefficients[j] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form,
&error->coefficients[j]));
add_vector_79(coefficient_normal_form, &error->coefficients[j]));
}
}

Expand Down Expand Up @@ -3317,8 +3328,7 @@ static KRML_MUSTINLINE void add_error_reduce_79(
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
myself->coefficients[j], (int16_t)1441);
myself->coefficients[j] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form,
&error->coefficients[j]));
add_vector_79(coefficient_normal_form, &error->coefficients[j]));
}
}

Expand Down Expand Up @@ -3436,10 +3446,9 @@ add_message_error_reduce_79(
__m256i coefficient_normal_form =
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
result.coefficients[i0], (int16_t)1441);
__m256i tmp = libcrux_ml_kem_vector_avx2_add_9a(myself->coefficients[i0],
&message->coefficients[i0]);
__m256i tmp0 =
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form, &tmp);
__m256i tmp =
add_vector_79(myself->coefficients[i0], &message->coefficients[i0]);
__m256i tmp0 = add_vector_79(coefficient_normal_form, &tmp);
result.coefficients[i0] =
libcrux_ml_kem_vector_avx2_barrett_reduce_9a(tmp0);
}
Expand Down Expand Up @@ -4567,6 +4576,16 @@ deserialize_then_decompress_ring_element_v_ed(Eurydice_slice serialized) {
return deserialize_then_decompress_4_79(serialized);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.sub_vector
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics

*/
static KRML_MUSTINLINE __m256i sub_vector_79(__m256i lhs, __m256i *rhs) {
return libcrux_ml_kem_vector_avx2_sub_9a(lhs, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
Expand All @@ -4583,8 +4602,7 @@ subtract_reduce_79(libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *myself,
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
b.coefficients[i0], (int16_t)1441);
b.coefficients[i0] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_sub_9a(myself->coefficients[i0],
&coefficient_normal_form));
sub_vector_79(myself->coefficients[i0], &coefficient_normal_form));
}
return b;
}
Expand Down Expand Up @@ -5725,14 +5743,16 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_42(
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *rhs) {
__m256i _myself[16U];
memcpy(_myself, myself->coefficients, (size_t)16U * sizeof(__m256i));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(Eurydice_array_to_slice(
(size_t)16U, myself->coefficients, __m256i),
__m256i);
i++) {
size_t i0 = i;
myself->coefficients[i0] = libcrux_ml_kem_vector_avx2_add_9a(
myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] =
add_vector_79(myself->coefficients[i0], &rhs->coefficients[i0]);
}
}

Expand Down Expand Up @@ -7778,14 +7798,16 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_89(
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *rhs) {
__m256i _myself[16U];
memcpy(_myself, myself->coefficients, (size_t)16U * sizeof(__m256i));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(Eurydice_array_to_slice(
(size_t)16U, myself->coefficients, __m256i),
__m256i);
i++) {
size_t i0 = i;
myself->coefficients[i0] = libcrux_ml_kem_vector_avx2_add_9a(
myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] =
add_vector_79(myself->coefficients[i0], &rhs->coefficients[i0]);
}
}

Expand Down
59 changes: 44 additions & 15 deletions libcrux-ml-kem/c/libcrux_mlkem_portable.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3852,6 +3852,18 @@ ntt_multiply_ef_96(libcrux_ml_kem_polynomial_PolynomialRingElement_1d *self,
return ntt_multiply_96(self, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.add_vector
with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
with const generics

*/
static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
add_vector_96(libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs) {
return libcrux_ml_kem_vector_portable_add_2c(lhs, rhs);
}

/**
Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise
sum of their constituent coefficients.
Expand All @@ -3865,6 +3877,10 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_d0(
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *rhs) {
libcrux_ml_kem_vector_portable_vector_type_PortableVector _myself[16U];
memcpy(_myself, myself->coefficients,
(size_t)16U *
sizeof(libcrux_ml_kem_vector_portable_vector_type_PortableVector));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(
Eurydice_array_to_slice(
Expand All @@ -3874,8 +3890,7 @@ static KRML_MUSTINLINE void add_to_ring_element_d0(
i++) {
size_t i0 = i;
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_add_2c(myself->coefficients[i0],
&rhs->coefficients[i0]);
add_vector_96(myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] = uu____0;
}
}
Expand Down Expand Up @@ -3927,8 +3942,7 @@ static KRML_MUSTINLINE void add_standard_error_reduce_96(
to_standard_domain_96(myself->coefficients[j]);
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_barrett_reduce_2c(
libcrux_ml_kem_vector_portable_add_2c(coefficient_normal_form,
&error->coefficients[j]));
add_vector_96(coefficient_normal_form, &error->coefficients[j]));
myself->coefficients[j] = uu____0;
}
}
Expand Down Expand Up @@ -4547,8 +4561,7 @@ static KRML_MUSTINLINE void add_error_reduce_96(
myself->coefficients[j], (int16_t)1441);
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_barrett_reduce_2c(
libcrux_ml_kem_vector_portable_add_2c(coefficient_normal_form,
&error->coefficients[j]));
add_vector_96(coefficient_normal_form, &error->coefficients[j]));
myself->coefficients[j] = uu____0;
}
}
Expand Down Expand Up @@ -4677,10 +4690,9 @@ add_message_error_reduce_96(
libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_2c(
result.coefficients[i0], (int16_t)1441);
libcrux_ml_kem_vector_portable_vector_type_PortableVector tmp =
libcrux_ml_kem_vector_portable_add_2c(myself->coefficients[i0],
&message->coefficients[i0]);
add_vector_96(myself->coefficients[i0], &message->coefficients[i0]);
libcrux_ml_kem_vector_portable_vector_type_PortableVector tmp0 =
libcrux_ml_kem_vector_portable_add_2c(coefficient_normal_form, &tmp);
add_vector_96(coefficient_normal_form, &tmp);
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_barrett_reduce_2c(tmp0);
result.coefficients[i0] = uu____0;
Expand Down Expand Up @@ -5608,6 +5620,18 @@ deserialize_then_decompress_ring_element_v_ff(Eurydice_slice serialized) {
return deserialize_then_decompress_5_96(serialized);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.sub_vector
with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
with const generics

*/
static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector
sub_vector_96(libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs) {
return libcrux_ml_kem_vector_portable_sub_2c(lhs, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce
with types libcrux_ml_kem_vector_portable_vector_type_PortableVector
Expand All @@ -5626,8 +5650,7 @@ subtract_reduce_96(libcrux_ml_kem_polynomial_PolynomialRingElement_1d *myself,
b.coefficients[i0], (int16_t)1441);
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_barrett_reduce_2c(
libcrux_ml_kem_vector_portable_sub_2c(myself->coefficients[i0],
&coefficient_normal_form));
sub_vector_96(myself->coefficients[i0], &coefficient_normal_form));
b.coefficients[i0] = uu____0;
}
return b;
Expand Down Expand Up @@ -6738,6 +6761,10 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_a0(
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *rhs) {
libcrux_ml_kem_vector_portable_vector_type_PortableVector _myself[16U];
memcpy(_myself, myself->coefficients,
(size_t)16U *
sizeof(libcrux_ml_kem_vector_portable_vector_type_PortableVector));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(
Eurydice_array_to_slice(
Expand All @@ -6747,8 +6774,7 @@ static KRML_MUSTINLINE void add_to_ring_element_a0(
i++) {
size_t i0 = i;
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_add_2c(myself->coefficients[i0],
&rhs->coefficients[i0]);
add_vector_96(myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] = uu____0;
}
}
Expand Down Expand Up @@ -8816,6 +8842,10 @@ with const generics
static KRML_MUSTINLINE void add_to_ring_element_1b(
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_1d *rhs) {
libcrux_ml_kem_vector_portable_vector_type_PortableVector _myself[16U];
memcpy(_myself, myself->coefficients,
(size_t)16U *
sizeof(libcrux_ml_kem_vector_portable_vector_type_PortableVector));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(
Eurydice_array_to_slice(
Expand All @@ -8825,8 +8855,7 @@ static KRML_MUSTINLINE void add_to_ring_element_1b(
i++) {
size_t i0 = i;
libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 =
libcrux_ml_kem_vector_portable_add_2c(myself->coefficients[i0],
&rhs->coefficients[i0]);
add_vector_96(myself->coefficients[i0], &rhs->coefficients[i0]);
myself->coefficients[i0] = uu____0;
}
}
Expand Down
46 changes: 36 additions & 10 deletions libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2254,6 +2254,18 @@ libcrux_ml_kem_polynomial_ntt_multiply_ef_79(
return libcrux_ml_kem_polynomial_ntt_multiply_79(self, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.add_vector
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics

*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE __m256i
libcrux_ml_kem_polynomial_add_vector_79(__m256i lhs, __m256i *rhs) {
return libcrux_ml_kem_vector_avx2_add_9a(lhs, rhs);
}

/**
Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise
sum of their constituent coefficients.
Expand All @@ -2268,13 +2280,15 @@ KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE void libcrux_ml_kem_polynomial_add_to_ring_element_ab(
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *myself,
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *rhs) {
__m256i _myself[16U];
memcpy(_myself, myself->coefficients, (size_t)16U * sizeof(__m256i));
for (size_t i = (size_t)0U;
i < Eurydice_slice_len(Eurydice_array_to_slice(
(size_t)16U, myself->coefficients, __m256i),
__m256i);
i++) {
size_t i0 = i;
myself->coefficients[i0] = libcrux_ml_kem_vector_avx2_add_9a(
myself->coefficients[i0] = libcrux_ml_kem_polynomial_add_vector_79(
myself->coefficients[i0], &rhs->coefficients[i0]);
}
}
Expand Down Expand Up @@ -2436,6 +2450,18 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_montgomery_ab(
libcrux_ml_kem_polynomial_poly_barrett_reduce_ef_79(re);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.sub_vector
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics

*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE __m256i
libcrux_ml_kem_polynomial_sub_vector_79(__m256i lhs, __m256i *rhs) {
return libcrux_ml_kem_vector_avx2_sub_9a(lhs, rhs);
}

/**
A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
Expand All @@ -2454,8 +2480,8 @@ libcrux_ml_kem_polynomial_subtract_reduce_79(
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
b.coefficients[i0], (int16_t)1441);
b.coefficients[i0] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_sub_9a(myself->coefficients[i0],
&coefficient_normal_form));
libcrux_ml_kem_polynomial_sub_vector_79(myself->coefficients[i0],
&coefficient_normal_form));
}
return b;
}
Expand Down Expand Up @@ -3813,8 +3839,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_polynomial_add_error_reduce_79(
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
myself->coefficients[j], (int16_t)1441);
myself->coefficients[j] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form,
&error->coefficients[j]));
libcrux_ml_kem_polynomial_add_vector_79(coefficient_normal_form,
&error->coefficients[j]));
}
}

Expand Down Expand Up @@ -3943,10 +3969,10 @@ libcrux_ml_kem_polynomial_add_message_error_reduce_79(
__m256i coefficient_normal_form =
libcrux_ml_kem_vector_avx2_montgomery_multiply_by_constant_9a(
result.coefficients[i0], (int16_t)1441);
__m256i tmp = libcrux_ml_kem_vector_avx2_add_9a(myself->coefficients[i0],
&message->coefficients[i0]);
__m256i tmp = libcrux_ml_kem_polynomial_add_vector_79(
myself->coefficients[i0], &message->coefficients[i0]);
__m256i tmp0 =
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form, &tmp);
libcrux_ml_kem_polynomial_add_vector_79(coefficient_normal_form, &tmp);
result.coefficients[i0] =
libcrux_ml_kem_vector_avx2_barrett_reduce_9a(tmp0);
}
Expand Down Expand Up @@ -5101,8 +5127,8 @@ libcrux_ml_kem_polynomial_add_standard_error_reduce_79(
libcrux_ml_kem_vector_traits_to_standard_domain_79(
myself->coefficients[j]);
myself->coefficients[j] = libcrux_ml_kem_vector_avx2_barrett_reduce_9a(
libcrux_ml_kem_vector_avx2_add_9a(coefficient_normal_form,
&error->coefficients[j]));
libcrux_ml_kem_polynomial_add_vector_79(coefficient_normal_form,
&error->coefficients[j]));
}
}

Expand Down
Loading
Loading