This code was generated with the following toolchain.
F* version: 3ff998c60bb0efe9925fc94e8fb8b785b9485af0
Karamel version: 834986e78b5b72c617ab242e0dce97fa15e3e811
Vale version: 0.3.19
