def next.levels

emerging-ezjson@1.3.0.0 · src/pull.bend:1442

import Base

1442# the levels of the walk's budget: next.grow runs levels 0 to 32 of leaves of
1443# next.leaf() jumps, so a walk may jump back from a plain word 4 (2^33 - 1)
1444# times, more than the 2^32 - 1 it had. A byte step keeps the count
1445# and shrinks the suffix instead, so a long string does not burn it. The
1446# levels, not the count, are the literal, so a proof about `next` never
1447# expands four billion successors
1448def next.levels() -> Nat:
1449  33n