This code was generated with the following toolchain.
F* version: 088c54e4e7e01600da7e3edd787bbaed699cbb8c
KreMLin version: 7e02ba7022d8425377e9cb15c111a3d8a7e0912e
Vale version: 0.3.16