/*
* SPDX-FileCopyrightText: 2025 Cryspen Sarl <info@cryspen.com>
*
* SPDX-License-Identifier: MIT or Apache-2.0
*
* This code was generated with the following revisions:
* Charon: 377317d6b25702c46ffff072fa00a3e32095e46f
* Eurydice: b227478b67c6a6e2ff611f978f10d6b7f26472ac
* Karamel: 4e64d915da3c172d1dfad805b8e1a46beff938bc
* F*: unset
* Libcrux: d3ed1c47cd34e327523d0f5444286676b7f7abe1
*/