As all rust computation is happening within a `do` block, we could use Lean `for` loops instead of translating them to Hax folds.
As all rust computation is happening within a
doblock, we could use Leanforloops instead of translating them to Hax folds.