This code was generated with the following toolchain.
F* version: 0601978e78abe9e520ac2af31ad9859ce493942a
KreMLin version: 3e82a6e6e1caf7cb69d73d7e537d9e3fd5a6edd6
Vale version: 0.3.16