This code was generated with the following toolchain.
F* version: cfb65605a2b89df8d6c9ebd70127ca13b6208d24
KreMLin version: 03ccd42fb2b59fdb3b84c1c4ece2226a88a433e8
Vale version: 0.3.16
