This code was generated with the following toolchain.
F* version: 8201465eb7e0c9c8d8f5513779f40eb55d468bc8
KreMLin version: 2cec61205ad7ecb57514d7f2b0f8283d0a22c6c7
Vale version: 0.3.13
