tor-browser

The Tor Browser
git clone https://git.dasho.dev/tor-browser.git
Log | Files | Refs | README | LICENSE

libcrux_mlkem_portable.h (26247B)


      1 /*
      2 * SPDX-FileCopyrightText: 2025 Cryspen Sarl <info@cryspen.com>
      3 *
      4 * SPDX-License-Identifier: MIT or Apache-2.0
      5 *
      6 * This code was generated with the following revisions:
      7 * Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
      8 * Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
      9 * Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
     10 * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
     11 * Libcrux: 68dfed5a4a9e40277f62828471c029afed1ecdcc
     12 */
     13 
     14 #ifndef libcrux_mlkem_portable_H
     15 #define libcrux_mlkem_portable_H
     16 
     17 #include "eurydice_glue.h"
     18 
     19 #if defined(__cplusplus)
     20 extern "C" {
     21 #endif
     22 
     23 void libcrux_ml_kem_hash_functions_portable_G(Eurydice_slice input,
     24                                              uint8_t ret[64U]);
     25 
     26 void libcrux_ml_kem_hash_functions_portable_H(Eurydice_slice input,
     27                                              uint8_t ret[32U]);
     28 
     29 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_ELEMENTS_IN_VECTOR ((size_t)16U)
     30 
     31 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS \
     32    ((int16_t)1353)
     33 
     34 typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s {
     35    int16_t elements[16U];
     36 } libcrux_ml_kem_vector_portable_vector_type_PortableVector;
     37 
     38 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     39 libcrux_ml_kem_vector_portable_vector_type_zero(void);
     40 
     41 /**
     42 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     43 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
     44 */
     45 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     46 libcrux_ml_kem_vector_portable_ZERO_b8(void);
     47 
     48 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     49 libcrux_ml_kem_vector_portable_vector_type_from_i16_array(Eurydice_slice array);
     50 
     51 /**
     52 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     53 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
     54 */
     55 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     56 libcrux_ml_kem_vector_portable_from_i16_array_b8(Eurydice_slice array);
     57 
     58 void libcrux_ml_kem_vector_portable_vector_type_to_i16_array(
     59    libcrux_ml_kem_vector_portable_vector_type_PortableVector x,
     60    int16_t ret[16U]);
     61 
     62 /**
     63 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     64 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
     65 */
     66 void libcrux_ml_kem_vector_portable_to_i16_array_b8(
     67    libcrux_ml_kem_vector_portable_vector_type_PortableVector x,
     68    int16_t ret[16U]);
     69 
     70 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     71 libcrux_ml_kem_vector_portable_vector_type_from_bytes(Eurydice_slice array);
     72 
     73 /**
     74 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     75 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
     76 */
     77 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     78 libcrux_ml_kem_vector_portable_from_bytes_b8(Eurydice_slice array);
     79 
     80 void libcrux_ml_kem_vector_portable_vector_type_to_bytes(
     81    libcrux_ml_kem_vector_portable_vector_type_PortableVector x,
     82    Eurydice_slice bytes);
     83 
     84 /**
     85 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     86 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
     87 */
     88 void libcrux_ml_kem_vector_portable_to_bytes_b8(
     89    libcrux_ml_kem_vector_portable_vector_type_PortableVector x,
     90    Eurydice_slice bytes);
     91 
     92 libcrux_ml_kem_vector_portable_vector_type_PortableVector
     93 libcrux_ml_kem_vector_portable_arithmetic_add(
     94    libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
     95    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs);
     96 
     97 /**
     98 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
     99 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    100 */
    101 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    102 libcrux_ml_kem_vector_portable_add_b8(
    103    libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
    104    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs);
    105 
    106 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    107 libcrux_ml_kem_vector_portable_arithmetic_sub(
    108    libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
    109    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs);
    110 
    111 /**
    112 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    113 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    114 */
    115 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    116 libcrux_ml_kem_vector_portable_sub_b8(
    117    libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs,
    118    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs);
    119 
    120 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    121 libcrux_ml_kem_vector_portable_arithmetic_multiply_by_constant(
    122    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec, int16_t c);
    123 
    124 /**
    125 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    126 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    127 */
    128 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    129 libcrux_ml_kem_vector_portable_multiply_by_constant_b8(
    130    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec, int16_t c);
    131 
    132 /**
    133 Note: This function is not secret independent
    134 Only use with public values.
    135 */
    136 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    137 libcrux_ml_kem_vector_portable_arithmetic_cond_subtract_3329(
    138    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec);
    139 
    140 /**
    141 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    142 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    143 */
    144 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    145 libcrux_ml_kem_vector_portable_cond_subtract_3329_b8(
    146    libcrux_ml_kem_vector_portable_vector_type_PortableVector v);
    147 
    148 #define LIBCRUX_ML_KEM_VECTOR_PORTABLE_ARITHMETIC_BARRETT_MULTIPLIER \
    149    ((int32_t)20159)
    150 
    151 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_BARRETT_SHIFT ((int32_t)26)
    152 
    153 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_BARRETT_R \
    154    ((int32_t)1 << (uint32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_BARRETT_SHIFT)
    155 
    156 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS ((int16_t)3329)
    157 
    158 /**
    159 Signed Barrett Reduction
    160 
    161 Given an input `value`, `barrett_reduce` outputs a representative `result`
    162 such that:
    163 
    164 - result ≡ value (mod FIELD_MODULUS)
    165 - the absolute value of `result` is bound as follows:
    166 
    167 `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
    168 
    169 Note: The input bound is 28296 to prevent overflow in the multiplication of
    170 quotient by FIELD_MODULUS
    171 
    172 */
    173 int16_t libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element(
    174    int16_t value);
    175 
    176 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    177 libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce(
    178    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec);
    179 
    180 /**
    181 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    182 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    183 */
    184 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    185 libcrux_ml_kem_vector_portable_barrett_reduce_b8(
    186    libcrux_ml_kem_vector_portable_vector_type_PortableVector vector);
    187 
    188 #define LIBCRUX_ML_KEM_VECTOR_TRAITS_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R \
    189    (62209U)
    190 
    191 #define LIBCRUX_ML_KEM_VECTOR_PORTABLE_ARITHMETIC_MONTGOMERY_SHIFT (16U)
    192 
    193 /**
    194 Signed Montgomery Reduction
    195 
    196 Given an input `value`, `montgomery_reduce` outputs a representative `o`
    197 such that:
    198 
    199 - o ≡ value · MONTGOMERY_R^(-1) (mod FIELD_MODULUS)
    200 - the absolute value of `o` is bound as follows:
    201 
    202 `|result| ≤ ceil(|value| / MONTGOMERY_R) + 1665
    203 
    204 In particular, if `|value| ≤ FIELD_MODULUS-1 * FIELD_MODULUS-1`, then `|o| <=
    205 FIELD_MODULUS-1`. And, if `|value| ≤ pow2 16 * FIELD_MODULUS-1`, then `|o| <=
    206 FIELD_MODULUS + 1664
    207 
    208 */
    209 int16_t libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element(
    210    int32_t value);
    211 
    212 /**
    213 If `fe` is some field element 'x' of the Kyber field and `fer` is congruent to
    214 `y · MONTGOMERY_R`, this procedure outputs a value that is congruent to
    215 `x · y`, as follows:
    216 
    217    `fe · fer ≡ x · y · MONTGOMERY_R (mod FIELD_MODULUS)`
    218 
    219 `montgomery_reduce` takes the value `x · y · MONTGOMERY_R` and outputs a
    220 representative `x · y · MONTGOMERY_R * MONTGOMERY_R^{-1} ≡ x · y (mod
    221 FIELD_MODULUS)`.
    222 */
    223 int16_t libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer(
    224    int16_t fe, int16_t fer);
    225 
    226 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    227 libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_by_constant(
    228    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec, int16_t c);
    229 
    230 /**
    231 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    232 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    233 */
    234 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    235 libcrux_ml_kem_vector_portable_montgomery_multiply_by_constant_b8(
    236    libcrux_ml_kem_vector_portable_vector_type_PortableVector vector,
    237    int16_t constant);
    238 
    239 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    240 libcrux_ml_kem_vector_portable_arithmetic_bitwise_and_with_constant(
    241    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec, int16_t c);
    242 
    243 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    244 libcrux_ml_kem_vector_portable_arithmetic_to_unsigned_representative(
    245    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    246 
    247 /**
    248 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    249 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    250 */
    251 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    252 libcrux_ml_kem_vector_portable_to_unsigned_representative_b8(
    253    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    254 
    255 /**
    256 The `compress_*` functions implement the `Compress` function specified in the
    257 NIST FIPS 203 standard (Page 18, Expression 4.5), which is defined as:
    258 
    259 ```plaintext
    260 Compress_d: ℤq -> ℤ_{2ᵈ}
    261 Compress_d(x) = ⌈(2ᵈ/q)·x⌋
    262 ```
    263 
    264 Since `⌈x⌋ = ⌊x + 1/2⌋` we have:
    265 
    266 ```plaintext
    267 Compress_d(x) = ⌊(2ᵈ/q)·x + 1/2⌋
    268               = ⌊(2^{d+1}·x + q) / 2q⌋
    269 ```
    270 
    271 For further information about the function implementations, consult the
    272 `implementation_notes.pdf` document in this directory.
    273 
    274 The NIST FIPS 203 standard can be found at
    275 <https://csrc.nist.gov/pubs/fips/203/ipd>.
    276 */
    277 uint8_t libcrux_ml_kem_vector_portable_compress_compress_message_coefficient(
    278    uint16_t fe);
    279 
    280 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    281 libcrux_ml_kem_vector_portable_compress_compress_1(
    282    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    283 
    284 /**
    285 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    286 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    287 */
    288 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    289 libcrux_ml_kem_vector_portable_compress_1_b8(
    290    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    291 
    292 uint32_t libcrux_ml_kem_vector_portable_arithmetic_get_n_least_significant_bits(
    293    uint8_t n, uint32_t value);
    294 
    295 int16_t libcrux_ml_kem_vector_portable_compress_compress_ciphertext_coefficient(
    296    uint8_t coefficient_bits, uint16_t fe);
    297 
    298 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    299 libcrux_ml_kem_vector_portable_compress_decompress_1(
    300    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    301 
    302 /**
    303 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    304 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    305 */
    306 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    307 libcrux_ml_kem_vector_portable_decompress_1_b8(
    308    libcrux_ml_kem_vector_portable_vector_type_PortableVector a);
    309 
    310 void libcrux_ml_kem_vector_portable_ntt_ntt_step(
    311    libcrux_ml_kem_vector_portable_vector_type_PortableVector *vec,
    312    int16_t zeta, size_t i, size_t j);
    313 
    314 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    315 libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step(
    316    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    317    int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3);
    318 
    319 /**
    320 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    321 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    322 */
    323 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    324 libcrux_ml_kem_vector_portable_ntt_layer_1_step_b8(
    325    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0,
    326    int16_t zeta1, int16_t zeta2, int16_t zeta3);
    327 
    328 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    329 libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step(
    330    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    331    int16_t zeta0, int16_t zeta1);
    332 
    333 /**
    334 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    335 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    336 */
    337 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    338 libcrux_ml_kem_vector_portable_ntt_layer_2_step_b8(
    339    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0,
    340    int16_t zeta1);
    341 
    342 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    343 libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step(
    344    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    345    int16_t zeta);
    346 
    347 /**
    348 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    349 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    350 */
    351 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    352 libcrux_ml_kem_vector_portable_ntt_layer_3_step_b8(
    353    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta);
    354 
    355 void libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(
    356    libcrux_ml_kem_vector_portable_vector_type_PortableVector *vec,
    357    int16_t zeta, size_t i, size_t j);
    358 
    359 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    360 libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step(
    361    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    362    int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3);
    363 
    364 /**
    365 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    366 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    367 */
    368 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    369 libcrux_ml_kem_vector_portable_inv_ntt_layer_1_step_b8(
    370    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0,
    371    int16_t zeta1, int16_t zeta2, int16_t zeta3);
    372 
    373 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    374 libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step(
    375    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    376    int16_t zeta0, int16_t zeta1);
    377 
    378 /**
    379 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    380 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    381 */
    382 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    383 libcrux_ml_kem_vector_portable_inv_ntt_layer_2_step_b8(
    384    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0,
    385    int16_t zeta1);
    386 
    387 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    388 libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step(
    389    libcrux_ml_kem_vector_portable_vector_type_PortableVector vec,
    390    int16_t zeta);
    391 
    392 /**
    393 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    394 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    395 */
    396 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    397 libcrux_ml_kem_vector_portable_inv_ntt_layer_3_step_b8(
    398    libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta);
    399 
    400 /**
    401 Compute the product of two Kyber binomials with respect to the
    402 modulus `X² - zeta`.
    403 
    404 This function almost implements <strong>Algorithm 11</strong> of the
    405 NIST FIPS 203 standard, which is reproduced below:
    406 
    407 ```plaintext
    408 Input:  a₀, a₁, b₀, b₁ ∈ ℤq.
    409 Input: γ ∈ ℤq.
    410 Output: c₀, c₁ ∈ ℤq.
    411 
    412 c₀ ← a₀·b₀ + a₁·b₁·γ
    413 c₁ ← a₀·b₁ + a₁·b₀
    414 return c₀, c₁
    415 ```
    416 We say "almost" because the coefficients output by this function are in
    417 the Montgomery domain (unlike in the specification).
    418 
    419 The NIST FIPS 203 standard can be found at
    420 <https://csrc.nist.gov/pubs/fips/203/ipd>.
    421 */
    422 void libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(
    423    libcrux_ml_kem_vector_portable_vector_type_PortableVector *a,
    424    libcrux_ml_kem_vector_portable_vector_type_PortableVector *b, int16_t zeta,
    425    size_t i, libcrux_ml_kem_vector_portable_vector_type_PortableVector *out);
    426 
    427 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    428 libcrux_ml_kem_vector_portable_ntt_ntt_multiply(
    429    libcrux_ml_kem_vector_portable_vector_type_PortableVector *lhs,
    430    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs,
    431    int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3);
    432 
    433 /**
    434 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    435 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    436 */
    437 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    438 libcrux_ml_kem_vector_portable_ntt_multiply_b8(
    439    libcrux_ml_kem_vector_portable_vector_type_PortableVector *lhs,
    440    libcrux_ml_kem_vector_portable_vector_type_PortableVector *rhs,
    441    int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3);
    442 
    443 void libcrux_ml_kem_vector_portable_serialize_serialize_1(
    444    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    445    uint8_t ret[2U]);
    446 
    447 void libcrux_ml_kem_vector_portable_serialize_1(
    448    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    449    uint8_t ret[2U]);
    450 
    451 /**
    452 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    453 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    454 */
    455 void libcrux_ml_kem_vector_portable_serialize_1_b8(
    456    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    457    uint8_t ret[2U]);
    458 
    459 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    460 libcrux_ml_kem_vector_portable_serialize_deserialize_1(Eurydice_slice v);
    461 
    462 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    463 libcrux_ml_kem_vector_portable_deserialize_1(Eurydice_slice a);
    464 
    465 /**
    466 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    467 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    468 */
    469 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    470 libcrux_ml_kem_vector_portable_deserialize_1_b8(Eurydice_slice a);
    471 
    472 typedef struct uint8_t_x4_s {
    473    uint8_t fst;
    474    uint8_t snd;
    475    uint8_t thd;
    476    uint8_t f3;
    477 } uint8_t_x4;
    478 
    479 uint8_t_x4 libcrux_ml_kem_vector_portable_serialize_serialize_4_int(
    480    Eurydice_slice v);
    481 
    482 void libcrux_ml_kem_vector_portable_serialize_serialize_4(
    483    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    484    uint8_t ret[8U]);
    485 
    486 void libcrux_ml_kem_vector_portable_serialize_4(
    487    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    488    uint8_t ret[8U]);
    489 
    490 /**
    491 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    492 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    493 */
    494 void libcrux_ml_kem_vector_portable_serialize_4_b8(
    495    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    496    uint8_t ret[8U]);
    497 
    498 typedef struct int16_t_x8_s {
    499    int16_t fst;
    500    int16_t snd;
    501    int16_t thd;
    502    int16_t f3;
    503    int16_t f4;
    504    int16_t f5;
    505    int16_t f6;
    506    int16_t f7;
    507 } int16_t_x8;
    508 
    509 int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_4_int(
    510    Eurydice_slice bytes);
    511 
    512 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    513 libcrux_ml_kem_vector_portable_serialize_deserialize_4(Eurydice_slice bytes);
    514 
    515 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    516 libcrux_ml_kem_vector_portable_deserialize_4(Eurydice_slice a);
    517 
    518 /**
    519 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    520 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    521 */
    522 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    523 libcrux_ml_kem_vector_portable_deserialize_4_b8(Eurydice_slice a);
    524 
    525 typedef struct uint8_t_x5_s {
    526    uint8_t fst;
    527    uint8_t snd;
    528    uint8_t thd;
    529    uint8_t f3;
    530    uint8_t f4;
    531 } uint8_t_x5;
    532 
    533 uint8_t_x5 libcrux_ml_kem_vector_portable_serialize_serialize_5_int(
    534    Eurydice_slice v);
    535 
    536 void libcrux_ml_kem_vector_portable_serialize_serialize_5(
    537    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    538    uint8_t ret[10U]);
    539 
    540 void libcrux_ml_kem_vector_portable_serialize_5(
    541    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    542    uint8_t ret[10U]);
    543 
    544 /**
    545 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    546 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    547 */
    548 void libcrux_ml_kem_vector_portable_serialize_5_b8(
    549    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    550    uint8_t ret[10U]);
    551 
    552 int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_5_int(
    553    Eurydice_slice bytes);
    554 
    555 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    556 libcrux_ml_kem_vector_portable_serialize_deserialize_5(Eurydice_slice bytes);
    557 
    558 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    559 libcrux_ml_kem_vector_portable_deserialize_5(Eurydice_slice a);
    560 
    561 /**
    562 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    563 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    564 */
    565 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    566 libcrux_ml_kem_vector_portable_deserialize_5_b8(Eurydice_slice a);
    567 
    568 uint8_t_x5 libcrux_ml_kem_vector_portable_serialize_serialize_10_int(
    569    Eurydice_slice v);
    570 
    571 void libcrux_ml_kem_vector_portable_serialize_serialize_10(
    572    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    573    uint8_t ret[20U]);
    574 
    575 void libcrux_ml_kem_vector_portable_serialize_10(
    576    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    577    uint8_t ret[20U]);
    578 
    579 /**
    580 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    581 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    582 */
    583 void libcrux_ml_kem_vector_portable_serialize_10_b8(
    584    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    585    uint8_t ret[20U]);
    586 
    587 int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_10_int(
    588    Eurydice_slice bytes);
    589 
    590 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    591 libcrux_ml_kem_vector_portable_serialize_deserialize_10(Eurydice_slice bytes);
    592 
    593 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    594 libcrux_ml_kem_vector_portable_deserialize_10(Eurydice_slice a);
    595 
    596 /**
    597 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    598 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    599 */
    600 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    601 libcrux_ml_kem_vector_portable_deserialize_10_b8(Eurydice_slice a);
    602 
    603 typedef struct uint8_t_x11_s {
    604    uint8_t fst;
    605    uint8_t snd;
    606    uint8_t thd;
    607    uint8_t f3;
    608    uint8_t f4;
    609    uint8_t f5;
    610    uint8_t f6;
    611    uint8_t f7;
    612    uint8_t f8;
    613    uint8_t f9;
    614    uint8_t f10;
    615 } uint8_t_x11;
    616 
    617 uint8_t_x11 libcrux_ml_kem_vector_portable_serialize_serialize_11_int(
    618    Eurydice_slice v);
    619 
    620 void libcrux_ml_kem_vector_portable_serialize_serialize_11(
    621    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    622    uint8_t ret[22U]);
    623 
    624 void libcrux_ml_kem_vector_portable_serialize_11(
    625    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    626    uint8_t ret[22U]);
    627 
    628 /**
    629 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    630 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    631 */
    632 void libcrux_ml_kem_vector_portable_serialize_11_b8(
    633    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    634    uint8_t ret[22U]);
    635 
    636 int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_11_int(
    637    Eurydice_slice bytes);
    638 
    639 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    640 libcrux_ml_kem_vector_portable_serialize_deserialize_11(Eurydice_slice bytes);
    641 
    642 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    643 libcrux_ml_kem_vector_portable_deserialize_11(Eurydice_slice a);
    644 
    645 /**
    646 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    647 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    648 */
    649 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    650 libcrux_ml_kem_vector_portable_deserialize_11_b8(Eurydice_slice a);
    651 
    652 typedef struct uint8_t_x3_s {
    653    uint8_t fst;
    654    uint8_t snd;
    655    uint8_t thd;
    656 } uint8_t_x3;
    657 
    658 uint8_t_x3 libcrux_ml_kem_vector_portable_serialize_serialize_12_int(
    659    Eurydice_slice v);
    660 
    661 void libcrux_ml_kem_vector_portable_serialize_serialize_12(
    662    libcrux_ml_kem_vector_portable_vector_type_PortableVector v,
    663    uint8_t ret[24U]);
    664 
    665 void libcrux_ml_kem_vector_portable_serialize_12(
    666    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    667    uint8_t ret[24U]);
    668 
    669 /**
    670 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    671 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    672 */
    673 void libcrux_ml_kem_vector_portable_serialize_12_b8(
    674    libcrux_ml_kem_vector_portable_vector_type_PortableVector a,
    675    uint8_t ret[24U]);
    676 
    677 typedef struct int16_t_x2_s {
    678    int16_t fst;
    679    int16_t snd;
    680 } int16_t_x2;
    681 
    682 int16_t_x2 libcrux_ml_kem_vector_portable_serialize_deserialize_12_int(
    683    Eurydice_slice bytes);
    684 
    685 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    686 libcrux_ml_kem_vector_portable_serialize_deserialize_12(Eurydice_slice bytes);
    687 
    688 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    689 libcrux_ml_kem_vector_portable_deserialize_12(Eurydice_slice a);
    690 
    691 /**
    692 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    693 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    694 */
    695 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    696 libcrux_ml_kem_vector_portable_deserialize_12_b8(Eurydice_slice a);
    697 
    698 size_t libcrux_ml_kem_vector_portable_sampling_rej_sample(
    699    Eurydice_slice a, Eurydice_slice result);
    700 
    701 /**
    702 This function found in impl {libcrux_ml_kem::vector::traits::Operations for
    703 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    704 */
    705 size_t libcrux_ml_kem_vector_portable_rej_sample_b8(Eurydice_slice a,
    706                                                    Eurydice_slice out);
    707 
    708 /**
    709 This function found in impl {core::clone::Clone for
    710 libcrux_ml_kem::vector::portable::vector_type::PortableVector}
    711 */
    712 libcrux_ml_kem_vector_portable_vector_type_PortableVector
    713 libcrux_ml_kem_vector_portable_vector_type_clone_9c(
    714    libcrux_ml_kem_vector_portable_vector_type_PortableVector *self);
    715 
    716 #if defined(__cplusplus)
    717 }
    718 #endif
    719 
    720 #define libcrux_mlkem_portable_H_DEFINED
    721 #endif /* libcrux_mlkem_portable_H */