Byte-at-a-time decoder accumulator threaded by a `nat-eliminate` over the
input length. Every step is O(1): it peels one byte with `bytes-head` /
`bytes-tail` (both O(1) on the `[Word8]` representation), advances the offset
with `succ` (O(1)), and either prepends a completed codepoint onto
`utf8MachineReversed` or updates `utf8MachinePending`. It must avoid
`bytes-eliminate`, `bytes-length` and `naturalAdd` in the loop: the reference
machine folds the ENTIRE tail to build a (here unused) induction for those, so
one call is O(remaining) and per-step use would be O(length^2). Fuel equals
the byte count exactly, so a step never reads past the end (no empty test is
needed). `Failed` is a fixed point that absorbs any surplus fuel.
182constructor UTF8DecodeMachineGoingThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.