Eurydice_slice_index
((uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *) ^
(uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *));
((uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *) &
((uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *) &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) & 1U);
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 1U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 2U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 3U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 4U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 5U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 6U &
(uint32_t)Eurydice_slice_index(v, (size_t)0U, uint8_t, uint8_t *) >> 7U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) & 1U);
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 1U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 2U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 3U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 4U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 5U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 6U &
(uint32_t)Eurydice_slice_index(v, (size_t)1U, uint8_t, uint8_t *) >> 7U &
Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *))
(uint32_t)libcrux_secrets_int_as_u8_f5(Eurydice_slice_index(
Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *))
(uint32_t)libcrux_secrets_int_as_u8_f5(Eurydice_slice_index(
Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *))
(uint32_t)libcrux_secrets_int_as_u8_f5(Eurydice_slice_index(
Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *))
(uint32_t)libcrux_secrets_int_as_u8_f5(Eurydice_slice_index(
(uint32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *) &
(uint32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *) >>
(uint32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *) &
(uint32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *) >>
(uint32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *) &
(uint32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *) >>
(uint32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *) &
(uint32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *) >>
Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) & (int16_t)255);
Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) & (int16_t)63)
Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) >> 8U &
Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) & (int16_t)15)
Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) >> 6U &
Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) & (int16_t)3)
Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 4U &
Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *) >> 2U &
Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *))
Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *)) &
Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(bytes, (size_t)9U, uint8_t, uint8_t *))
Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *)) >>
Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) & (int16_t)255);
Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *) >> 8U |
(Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) & (int16_t)15)
Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *) >> 4U &
Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *));
Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *));
Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *));
int16_t b1 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)0U,
int16_t b2 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)1U,
int16_t b3 = (int16_t)Eurydice_slice_index(a, i0 * (size_t)3U + (size_t)2U,
Eurydice_slice_index(result, sampled, int16_t, int16_t *) = d1;
Eurydice_slice_index(result, sampled, int16_t, int16_t *) = d2;
(((uint32_t)Eurydice_slice_index(byte_chunk, (size_t)0U, uint8_t,
(uint32_t)Eurydice_slice_index(byte_chunk, (size_t)1U, uint8_t,
(uint32_t)Eurydice_slice_index(byte_chunk, (size_t)2U, uint8_t,
(uint32_t)Eurydice_slice_index(byte_chunk, (size_t)3U, uint8_t,