This code was generated with the following toolchain.
F* version: 2caed2b17fb9925669c4a5511fa1deebb3f065a2
KreMLin version: 295f119db3fbbf237ba6c040576bc72a7691dbf8
Vale version: 0.3.13
