The code was generated with the following toolchain.
F* version: e617752a1b014a16892f7d8772d62e5c234f06c1
KaRaMeL version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b
HACL* version: 86a0aed822bd80b03e4810e23518181f0edec5f6
Vale version: 0.3.19
