This code was generated with the following toolchain.
F* version: 7b347386330d0e5a331a220535b6f15288903234
Karamel version: 254e099bd586b17461845f6b0cab44c3ef5080e9
Vale version: 0.3.19
