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.

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

Draft
wants to merge 11 commits into
base: main
Choose a base branch
from
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/code_gen.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
Libcrux: da72c141597b1db012f3bc23a96330f6de112770
Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/internal/libcrux_core.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __internal_libcrux_core_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __internal_libcrux_mlkem_avx2_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __internal_libcrux_mlkem_portable_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __internal_libcrux_sha3_avx2_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __internal_libcrux_sha3_internal_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_core.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "internal/libcrux_core.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_core.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_core_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem1024.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem1024_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem1024_avx2.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem1024_avx2_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem1024_portable.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem1024_portable_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem512.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem512_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem512_avx2.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem512_avx2_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem512_portable.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem512_portable.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem512_portable.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem512_portable_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem768.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem768_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem768_avx2.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem768_avx2_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem768_portable.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "libcrux_mlkem768_portable.h"
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem768_portable.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem768_portable_H
Expand Down
56 changes: 39 additions & 17 deletions libcrux-ml-kem/c/libcrux_mlkem_avx2.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#include "internal/libcrux_mlkem_avx2.h"
Expand Down 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 @@ -4568,6 +4577,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 @@ -4584,8 +4603,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 @@ -5727,14 +5745,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 @@ -7782,14 +7802,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
2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/libcrux_mlkem_avx2.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: da72c141597b1db012f3bc23a96330f6de112770
* Libcrux: 2505360d54e1bcdd7165398ad6ada928ae8b568b
*/

#ifndef __libcrux_mlkem_avx2_H
Expand Down
Loading
Loading