Lines Matching +full:14 +full:v
1 /* $OpenBSD: libcrux_mlkem768_sha3.h,v 1.2 2024/10/27 02:06:01 djm Exp $ */
163 static inline void core_num__u64_9__to_le_bytes(uint64_t v, uint8_t buf[8]) { in core_num__u64_9__to_le_bytes() argument
164 v = htole64(v); in core_num__u64_9__to_le_bytes()
165 memcpy(buf, &v, sizeof(v)); in core_num__u64_9__to_le_bytes()
168 uint64_t v; in core_num__u64_9__from_le_bytes() local
169 memcpy(&v, buf, sizeof(v)); in core_num__u64_9__from_le_bytes()
170 return le64toh(v); in core_num__u64_9__from_le_bytes()
174 uint32_t v; in core_num__u32_8__from_le_bytes() local
175 memcpy(&v, buf, sizeof(v)); in core_num__u32_8__from_le_bytes()
176 return le32toh(v); in core_num__u32_8__from_le_bytes()
185 const uint8_t v[16] = { 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4 }; in core_num__u8_6__count_ones()
186 return v[x0 & 0xf] + v[(x0 >> 4) & 0xf]; in core_num__u8_6__count_ones()
438 libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#14}
2010 - LEFT= 14
2015 return x << (uint32_t)(int32_t)14 | x >> (uint32_t)(int32_t)50; in libcrux_sha3_portable_keccak_rotate_left_cb22()
2021 - LEFT= 14
2037 - LEFT= 14
4313 (size_t)8U, (size_t)14U, (size_t)15U, (size_t)21U};
4320 (size_t)2U, (size_t)61U, (size_t)56U, (size_t)14U};
4808 ret[14U] = 0U; in libcrux_sha3_generic_keccak_zero_block_9d_e6()
5256 ret[14U] = 0U; in libcrux_sha3_generic_keccak_zero_block_9d_e60()
5700 static inline uint32_t libcrux_sha3_from_eb(libcrux_sha3_Algorithm v) { in libcrux_sha3_from_eb() argument
5702 switch (v) { in libcrux_sha3_from_eb()
5732 static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) { in libcrux_sha3_from_2d() argument
5734 switch (v) { in libcrux_sha3_from_2d()
5917 libcrux_ml_kem_vector_portable_serialize_serialize_11_int(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_serialize_11_int() argument
5918 uint8_t r0 = (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *); in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5919 uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5923 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5926 uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5930 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5934 (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 2U & in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5936 uint8_t r4 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5940 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5943 uint8_t r5 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5947 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5950 uint8_t r6 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5954 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5958 (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) >> 1U & in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5960 uint8_t r8 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5964 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5967 uint8_t r9 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5971 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5975 (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) >> 3U); in libcrux_ml_kem_vector_portable_serialize_serialize_11_int()
5991 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_11() argument
5994 Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_11()
5997 Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, in libcrux_ml_kem_vector_portable_serialize_serialize_11()
6014 result[14U] = r11_21.f3; in libcrux_ml_kem_vector_portable_serialize_serialize_11()
6126 lit.elements[14U] = (int16_t)0; in libcrux_ml_kem_vector_portable_vector_type_zero()
6138 libcrux_ml_kem_vector_portable_vector_type_PortableVector v = in libcrux_ml_kem_vector_portable_serialize_deserialize_11() local
6140 v.elements[0U] = v0_7.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6141 v.elements[1U] = v0_7.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6142 v.elements[2U] = v0_7.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6143 v.elements[3U] = v0_7.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6144 v.elements[4U] = v0_7.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6145 v.elements[5U] = v0_7.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6146 v.elements[6U] = v0_7.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6147 v.elements[7U] = v0_7.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6148 v.elements[8U] = v8_15.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6149 v.elements[9U] = v8_15.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6150 v.elements[10U] = v8_15.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6151 v.elements[11U] = v8_15.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6152 v.elements[12U] = v8_15.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6153 v.elements[13U] = v8_15.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6154 v.elements[14U] = v8_15.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6155 v.elements[15U] = v8_15.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6156 return v; in libcrux_ml_kem_vector_portable_serialize_deserialize_11()
6443 {14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U,
6445 {0U, 1U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6447 {2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6449 {0U, 1U, 2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6451 {4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6453 {0U, 1U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6455 {2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6457 {0U, 1U, 2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U,
6459 {6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6461 {0U, 1U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6463 {2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6465 {0U, 1U, 2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U,
6467 {4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6469 {0U, 1U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U,
6471 {2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U,
6473 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U,
6475 {8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6477 {0U, 1U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6479 {2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6481 {0U, 1U, 2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6483 {4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6485 {0U, 1U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6487 {2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6489 {0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U,
6491 {6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U,
6493 {0U, 1U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6495 {2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6497 {0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U,
6499 {4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U,
6501 {0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U,
6503 {2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U,
6505 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U,
6507 {10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6509 {0U, 1U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U,
6511 {2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U,
6513 {0U, 1U, 2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6515 {4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U,
6517 {0U, 1U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6519 {2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6521 {0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U,
6523 {6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U,
6525 {0U, 1U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6527 {2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6529 {0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U,
6531 {4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6533 {0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U,
6535 {2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U,
6537 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U,
6539 {8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U,
6541 {0U, 1U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6543 {2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6545 {0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6547 {4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6549 {0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6551 {2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6553 {0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U,
6555 {6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U,
6557 {0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6559 {2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6561 {0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U,
6563 {4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U,
6565 {0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U,
6567 {2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U,
6569 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U,
6571 {12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U,
6573 {0U, 1U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6575 {2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6577 {0U, 1U, 2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6579 {4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6581 {0U, 1U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6583 {2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6585 {0U, 1U, 2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U,
6587 {6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6589 {0U, 1U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6591 {2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6593 {0U, 1U, 2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U,
6595 {4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6597 {0U, 1U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U,
6599 {2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U,
6601 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U,
6603 {8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6605 {0U, 1U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6607 {2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6609 {0U, 1U, 2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6611 {4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6613 {0U, 1U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6615 {2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6617 {0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U,
6619 {6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6621 {0U, 1U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6623 {2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6625 {0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U,
6627 {4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U,
6629 {0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U,
6631 {2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U,
6633 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U,
6635 {10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U,
6637 {0U, 1U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6639 {2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6641 {0U, 1U, 2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6643 {4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6645 {0U, 1U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6647 {2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6649 {0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U,
6651 {6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6653 {0U, 1U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6655 {2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6657 {0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U,
6659 {4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6661 {0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U,
6663 {2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U,
6665 {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U,
6667 {8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U,
6669 {0U, 1U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6671 {2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6673 {0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6675 {4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6677 {0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6679 {2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6681 {0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U,
6683 {6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U,
6685 {0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6687 {2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6689 {0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U,
6691 {4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U,
6693 {0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U,
6695 {2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U,
6698 13U, 14U, 15U}};
6759 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t c) { in libcrux_ml_kem_vector_portable_arithmetic_multiply_by_constant() argument
6764 v.elements[uu____0] = v.elements[uu____0] * c; in libcrux_ml_kem_vector_portable_arithmetic_multiply_by_constant()
6766 return v; in libcrux_ml_kem_vector_portable_arithmetic_multiply_by_constant()
6775 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t c) { in libcrux_ml_kem_vector_portable_multiply_by_constant_0d() argument
6776 return libcrux_ml_kem_vector_portable_arithmetic_multiply_by_constant(v, c); in libcrux_ml_kem_vector_portable_multiply_by_constant_0d()
6781 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t c) { in libcrux_ml_kem_vector_portable_arithmetic_bitwise_and_with_constant() argument
6786 v.elements[uu____0] = v.elements[uu____0] & c; in libcrux_ml_kem_vector_portable_arithmetic_bitwise_and_with_constant()
6788 return v; in libcrux_ml_kem_vector_portable_arithmetic_bitwise_and_with_constant()
6797 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t c) { in libcrux_ml_kem_vector_portable_bitwise_and_with_constant_0d() argument
6798 return libcrux_ml_kem_vector_portable_arithmetic_bitwise_and_with_constant(v, in libcrux_ml_kem_vector_portable_bitwise_and_with_constant_0d()
6804 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329() argument
6817 if (v.elements[i] >= (int16_t)3329) { in libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329()
6819 v.elements[uu____1] = v.elements[uu____1] - (int16_t)3329; in libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329()
6823 return v; in libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329()
6833 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_cond_subtract_3329_0d() argument
6834 return libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329(v); in libcrux_ml_kem_vector_portable_cond_subtract_3329_0d()
6874 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce() argument
6878 v.elements[i0] = in libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce()
6880 v.elements[i0]); in libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce()
6882 return v; in libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce()
6891 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_barrett_reduce_0d() argument
6892 return libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce(v); in libcrux_ml_kem_vector_portable_barrett_reduce_0d()
6954 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t c) { in libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_by_constant() argument
6958 v.elements[i0] = in libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_by_constant()
6960 v.elements[i0], c); in libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_by_constant()
6962 return v; in libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_by_constant()
6971 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t r) { in libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_0d() argument
6973 v, r); in libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_0d()
7010 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_compress_1() argument
7014 v.elements[i0] = (int16_t) in libcrux_ml_kem_vector_portable_compress_compress_1()
7016 (uint16_t)v.elements[i0]); in libcrux_ml_kem_vector_portable_compress_compress_1()
7018 return v; in libcrux_ml_kem_vector_portable_compress_compress_1()
7027 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_1_0d() argument
7028 return libcrux_ml_kem_vector_portable_compress_compress_1(v); in libcrux_ml_kem_vector_portable_compress_1_0d()
7050 libcrux_ml_kem_vector_portable_vector_type_PortableVector *v, int16_t zeta, in libcrux_ml_kem_vector_portable_ntt_ntt_step() argument
7054 v->elements[j], zeta); in libcrux_ml_kem_vector_portable_ntt_ntt_step()
7055 v->elements[j] = v->elements[i] - t; in libcrux_ml_kem_vector_portable_ntt_ntt_step()
7056 v->elements[i] = v->elements[i] + t; in libcrux_ml_kem_vector_portable_ntt_ntt_step()
7061 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step() argument
7063 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)0U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7065 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)1U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7067 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)4U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7069 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)5U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7071 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta2, (size_t)8U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7073 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta2, (size_t)9U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7075 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta3, (size_t)12U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7076 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7077 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta3, (size_t)13U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7079 return v; in libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step()
7096 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step() argument
7098 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)0U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7100 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)1U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7102 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)2U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7104 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)3U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7106 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)8U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7108 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)9U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7110 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)10U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7111 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7112 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)11U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7114 return v; in libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step()
7130 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta) { in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step() argument
7131 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)0U, (size_t)8U); in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7132 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)1U, (size_t)9U); in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7133 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)2U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7135 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)3U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7137 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)4U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7139 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)5U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7141 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)6U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7142 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7143 libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)7U, in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7145 return v; in libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step()
7159 libcrux_ml_kem_vector_portable_vector_type_PortableVector *v, int16_t zeta, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_step() argument
7161 int16_t a_minus_b = v->elements[j] - v->elements[i]; in libcrux_ml_kem_vector_portable_ntt_inv_ntt_step()
7162 v->elements[i] = in libcrux_ml_kem_vector_portable_ntt_inv_ntt_step()
7164 v->elements[i] + v->elements[j]); in libcrux_ml_kem_vector_portable_ntt_inv_ntt_step()
7165 v->elements[j] = in libcrux_ml_kem_vector_portable_ntt_inv_ntt_step()
7172 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step() argument
7174 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)0U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7176 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)1U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7178 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)4U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7180 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)5U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7182 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta2, (size_t)8U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7184 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta2, (size_t)9U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7186 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta3, (size_t)12U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7187 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7188 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta3, (size_t)13U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7190 return v; in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step()
7207 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step() argument
7209 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)0U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7211 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)1U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7213 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)2U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7215 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)3U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7217 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)8U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7219 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)9U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7221 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)10U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7222 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7223 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)11U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7225 return v; in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step()
7242 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta) { in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step() argument
7243 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)0U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7245 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)1U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7247 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)2U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7249 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)3U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7251 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)4U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7253 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)5U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7255 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)6U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7256 (size_t)14U); in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7257 libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)7U, in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7259 return v; in libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step()
7336 lhs, rhs, -zeta3, (size_t)14U, (size_t)15U, &out); in libcrux_ml_kem_vector_portable_ntt_ntt_multiply()
7355 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_1() argument
7362 (uint32_t)(uint8_t)v.elements[i0] << (uint32_t)i0; in libcrux_ml_kem_vector_portable_serialize_serialize_1()
7368 (uint32_t)result[uu____1] | (uint32_t)(uint8_t)v.elements[i0] in libcrux_ml_kem_vector_portable_serialize_serialize_1()
7385 libcrux_ml_kem_vector_portable_serialize_deserialize_1(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_deserialize_1() argument
7391 v, (size_t)0U, uint8_t, uint8_t *) >> in libcrux_ml_kem_vector_portable_serialize_deserialize_1()
7399 v, (size_t)1U, uint8_t, uint8_t *) >> in libcrux_ml_kem_vector_portable_serialize_deserialize_1()
7423 libcrux_ml_kem_vector_portable_serialize_serialize_4_int(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_serialize_4_int() argument
7425 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7427 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7430 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7432 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)2U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7435 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7437 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)4U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7440 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7442 (uint32_t)(uint8_t)Eurydice_slice_index(v, (size_t)6U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_4_int()
7450 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_4() argument
7454 Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, in libcrux_ml_kem_vector_portable_serialize_serialize_4()
7458 Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, in libcrux_ml_kem_vector_portable_serialize_serialize_4()
7529 libcrux_ml_kem_vector_portable_vector_type_PortableVector v = in libcrux_ml_kem_vector_portable_serialize_deserialize_4() local
7531 v.elements[0U] = v0_7.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7532 v.elements[1U] = v0_7.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7533 v.elements[2U] = v0_7.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7534 v.elements[3U] = v0_7.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7535 v.elements[4U] = v0_7.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7536 v.elements[5U] = v0_7.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7537 v.elements[6U] = v0_7.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7538 v.elements[7U] = v0_7.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7539 v.elements[8U] = v8_15.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7540 v.elements[9U] = v8_15.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7541 v.elements[10U] = v8_15.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7542 v.elements[11U] = v8_15.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7543 v.elements[12U] = v8_15.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7544 v.elements[13U] = v8_15.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7545 v.elements[14U] = v8_15.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7546 v.elements[15U] = v8_15.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7547 return v; in libcrux_ml_kem_vector_portable_serialize_deserialize_4()
7568 libcrux_ml_kem_vector_portable_serialize_serialize_5_int(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_serialize_5_int() argument
7570 (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) | in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7571 Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) << 5U); in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7573 (uint8_t)((Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) >> 3U | in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7574 Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7576 Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) << 7U); in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7578 (uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) >> 1U | in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7579 Eurydice_slice_index(v, (size_t)4U, int16_t, int16_t *) << 4U); in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7581 (uint8_t)((Eurydice_slice_index(v, (size_t)4U, int16_t, int16_t *) >> 4U | in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7582 Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7584 Eurydice_slice_index(v, (size_t)6U, int16_t, int16_t *) << 6U); in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7586 (uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, int16_t *) >> 2U | in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7587 Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) << 3U); in libcrux_ml_kem_vector_portable_serialize_serialize_5_int()
7594 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_5() argument
7597 Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_5()
7599 Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, in libcrux_ml_kem_vector_portable_serialize_serialize_5()
7683 libcrux_ml_kem_vector_portable_vector_type_PortableVector v = in libcrux_ml_kem_vector_portable_serialize_deserialize_5() local
7685 v.elements[0U] = v0_7.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7686 v.elements[1U] = v0_7.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7687 v.elements[2U] = v0_7.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7688 v.elements[3U] = v0_7.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7689 v.elements[4U] = v0_7.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7690 v.elements[5U] = v0_7.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7691 v.elements[6U] = v0_7.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7692 v.elements[7U] = v0_7.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7693 v.elements[8U] = v8_15.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7694 v.elements[9U] = v8_15.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7695 v.elements[10U] = v8_15.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7696 v.elements[11U] = v8_15.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7697 v.elements[12U] = v8_15.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7698 v.elements[13U] = v8_15.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7699 v.elements[14U] = v8_15.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7700 v.elements[15U] = v8_15.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7701 return v; in libcrux_ml_kem_vector_portable_serialize_deserialize_5()
7714 libcrux_ml_kem_vector_portable_serialize_serialize_10_int(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_serialize_10_int() argument
7716 (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) & in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7718 uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7722 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7726 uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7730 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7734 uint8_t r3 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7738 (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7743 (uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) >> 2U & in libcrux_ml_kem_vector_portable_serialize_serialize_10_int()
7751 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_10() argument
7754 Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)4U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_10()
7756 Eurydice_array_to_subslice2(v.elements, (size_t)4U, (size_t)8U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_10()
7758 Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)12U, in libcrux_ml_kem_vector_portable_serialize_serialize_10()
7761 Eurydice_array_to_subslice2(v.elements, (size_t)12U, (size_t)16U, in libcrux_ml_kem_vector_portable_serialize_serialize_10()
7778 result[14U] = r10_14.f4; in libcrux_ml_kem_vector_portable_serialize_serialize_10()
7863 libcrux_ml_kem_vector_portable_vector_type_PortableVector v = in libcrux_ml_kem_vector_portable_serialize_deserialize_10() local
7865 v.elements[0U] = v0_7.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7866 v.elements[1U] = v0_7.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7867 v.elements[2U] = v0_7.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7868 v.elements[3U] = v0_7.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7869 v.elements[4U] = v0_7.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7870 v.elements[5U] = v0_7.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7871 v.elements[6U] = v0_7.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7872 v.elements[7U] = v0_7.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7873 v.elements[8U] = v8_15.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7874 v.elements[9U] = v8_15.snd; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7875 v.elements[10U] = v8_15.thd; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7876 v.elements[11U] = v8_15.f3; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7877 v.elements[12U] = v8_15.f4; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7878 v.elements[13U] = v8_15.f5; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7879 v.elements[14U] = v8_15.f6; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7880 v.elements[15U] = v8_15.f7; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7881 return v; in libcrux_ml_kem_vector_portable_serialize_deserialize_10()
7900 libcrux_ml_kem_vector_portable_serialize_serialize_12_int(Eurydice_slice v) { in libcrux_ml_kem_vector_portable_serialize_serialize_12_int() argument
7902 (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) & in libcrux_ml_kem_vector_portable_serialize_serialize_12_int()
7905 (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) >> 8U | in libcrux_ml_kem_vector_portable_serialize_serialize_12_int()
7906 (Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) & in libcrux_ml_kem_vector_portable_serialize_serialize_12_int()
7910 (uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) >> 4U & in libcrux_ml_kem_vector_portable_serialize_serialize_12_int()
7917 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, in libcrux_ml_kem_vector_portable_serialize_serialize_12() argument
7920 Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)2U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7922 Eurydice_array_to_subslice2(v.elements, (size_t)2U, (size_t)4U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7924 Eurydice_array_to_subslice2(v.elements, (size_t)4U, (size_t)6U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7926 Eurydice_array_to_subslice2(v.elements, (size_t)6U, (size_t)8U, int16_t)); in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7928 Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)10U, in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7931 Eurydice_array_to_subslice2(v.elements, (size_t)10U, (size_t)12U, in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7934 Eurydice_array_to_subslice2(v.elements, (size_t)12U, (size_t)14U, in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7937 Eurydice_array_to_subslice2(v.elements, (size_t)14U, (size_t)16U, in libcrux_ml_kem_vector_portable_serialize_serialize_12()
7954 result[14U] = r12_14.thd; in libcrux_ml_kem_vector_portable_serialize_serialize_12()
8033 re.elements[14U] = v14_15.fst; in libcrux_ml_kem_vector_portable_serialize_deserialize_12()
8216 lit.coefficients[14U] = libcrux_ml_kem_vector_portable_ZERO_0d(); in libcrux_ml_kem_polynomial_ZERO_89_ea()
8322 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b() argument
8326 int32_t decompressed = (int32_t)v.elements[i0] * in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b()
8330 v.elements[i0] = (int16_t)decompressed; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b()
8332 return v; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b()
8347 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a() argument
8349 v); in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a()
8386 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b0() argument
8390 int32_t decompressed = (int32_t)v.elements[i0] * in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b0()
8394 v.elements[i0] = (int16_t)decompressed; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b0()
8396 return v; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b0()
8411 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a0() argument
8413 v); in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a0()
8467 libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t fer) { in libcrux_ml_kem_vector_traits_montgomery_multiply_fe_67() argument
8468 return libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_0d(v, in libcrux_ml_kem_vector_traits_montgomery_multiply_fe_67()
8691 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b1() argument
8695 int32_t decompressed = (int32_t)v.elements[i0] * in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b1()
8699 v.elements[i0] = (int16_t)decompressed; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b1()
8701 return v; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b1()
8716 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a1() argument
8718 v); in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a1()
8755 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b2() argument
8759 int32_t decompressed = (int32_t)v.elements[i0] * in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b2()
8763 v.elements[i0] = (int16_t)decompressed; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b2()
8765 return v; in libcrux_ml_kem_vector_portable_compress_decompress_ciphertext_coefficient_6b2()
8780 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a2() argument
8782 v); in libcrux_ml_kem_vector_portable_decompress_ciphertext_coefficient_0d_5a2()
9101 Compute v − InverseNTT(sᵀ ◦ NTT(u))
9111 libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *v, in libcrux_ml_kem_matrix_compute_message_b3() argument
9124 result = libcrux_ml_kem_polynomial_subtract_reduce_89_d4(v, result); in libcrux_ml_kem_matrix_compute_message_b3()
9135 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_arithmetic_shift_right_94() argument
9139 v.elements[i0] = v.elements[i0] >> (uint32_t)(int32_t)15; in libcrux_ml_kem_vector_portable_arithmetic_shift_right_94()
9141 return v; in libcrux_ml_kem_vector_portable_arithmetic_shift_right_94()
9155 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_shift_right_0d_19() argument
9156 return libcrux_ml_kem_vector_portable_arithmetic_shift_right_94(v); in libcrux_ml_kem_vector_portable_shift_right_0d_19()
9206 This function implements <strong>Algorithm 14</strong> of the
9209 Algorithm 14 is reproduced below:
9219 v ← Decompress_{dᵥ}(ByteDecode_{dᵥ}(c₂))
9221 w ← v - NTT-¹(ŝᵀ ◦ NTT(u))
9244 libcrux_ml_kem_polynomial_PolynomialRingElement_f0 v = in libcrux_ml_kem_ind_cpa_decrypt_unpacked_6d() local
9249 libcrux_ml_kem_matrix_compute_message_b3(&v, secret_key->secret_as_ntt, in libcrux_ml_kem_ind_cpa_decrypt_unpacked_6d()
9950 coin flips. If, for example, `eta = ETA`, each ring coefficient is a value `v`
9951 such such that `v ∈ {-ETA, -ETA + 1, ..., 0, ..., ETA + 1, ETA}` and:
9954 - If v < 0, Pr[v] = Pr[-v]
9955 - If v >= 0, Pr[v] = BINOMIAL_COEFFICIENT(2 * ETA; ETA - v) / 2 ^ (2 * ETA)
9958 The values `v < 0` are mapped to the appropriate `KyberFieldElement`.
9964 + (ETA)Pr[ETA] = 0 since Pr[-v] = Pr[v] when v < 0.
9972 = sum_(v=-ETA to ETA)v^2 * (BINOMIAL_COEFFICIENT(2 * ETA; ETA - v) /
10389 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_traits_decompress_1_63() argument
10393 libcrux_ml_kem_vector_portable_sub_0d(uu____0, &v), (int16_t)1665); in libcrux_ml_kem_vector_traits_decompress_1_63()
10493 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_compress_02() argument
10499 (uint8_t)(int32_t)10, (uint16_t)v.elements[i0]); in libcrux_ml_kem_vector_portable_compress_compress_02()
10500 v.elements[i0] = uu____0; in libcrux_ml_kem_vector_portable_compress_compress_02()
10502 return v; in libcrux_ml_kem_vector_portable_compress_compress_02()
10516 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_0d_28() argument
10517 return libcrux_ml_kem_vector_portable_compress_compress_02(v); in libcrux_ml_kem_vector_portable_compress_0d_28()
10554 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_compress_020() argument
10560 (uint8_t)(int32_t)11, (uint16_t)v.elements[i0]); in libcrux_ml_kem_vector_portable_compress_compress_020()
10561 v.elements[i0] = uu____0; in libcrux_ml_kem_vector_portable_compress_compress_020()
10563 return v; in libcrux_ml_kem_vector_portable_compress_compress_020()
10577 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_0d_280() argument
10578 return libcrux_ml_kem_vector_portable_compress_compress_020(v); in libcrux_ml_kem_vector_portable_compress_0d_280()
10665 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_compress_021() argument
10671 (uint8_t)(int32_t)4, (uint16_t)v.elements[i0]); in libcrux_ml_kem_vector_portable_compress_compress_021()
10672 v.elements[i0] = uu____0; in libcrux_ml_kem_vector_portable_compress_compress_021()
10674 return v; in libcrux_ml_kem_vector_portable_compress_compress_021()
10688 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_0d_281() argument
10689 return libcrux_ml_kem_vector_portable_compress_compress_021(v); in libcrux_ml_kem_vector_portable_compress_0d_281()
10725 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_compress_022() argument
10731 (uint8_t)(int32_t)5, (uint16_t)v.elements[i0]); in libcrux_ml_kem_vector_portable_compress_compress_022()
10732 v.elements[i0] = uu____0; in libcrux_ml_kem_vector_portable_compress_compress_022()
10734 return v; in libcrux_ml_kem_vector_portable_compress_compress_022()
10748 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_portable_compress_0d_282() argument
10749 return libcrux_ml_kem_vector_portable_compress_compress_022(v); in libcrux_ml_kem_vector_portable_compress_0d_282()
10860 libcrux_ml_kem_polynomial_PolynomialRingElement_f0 v = in libcrux_ml_kem_ind_cpa_encrypt_60() local
10871 libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____6 = v; in libcrux_ml_kem_ind_cpa_encrypt_60()
11235 libcrux_ml_kem_vector_portable_vector_type_PortableVector v) { in libcrux_ml_kem_vector_traits_to_standard_domain_59() argument
11237 v, LIBCRUX_ML_KEM_VECTOR_TRAITS_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS); in libcrux_ml_kem_vector_traits_to_standard_domain_59()