ByteBlockReader.transition.budget.state: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockReader.bend as ByteBlockReader
Lines 98-109 of mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockReader.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockReader.bend&start_line=98&end_line=109

import Base
import mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexPolicy.bend as BlockIndexPolicy

# Computes enough transitions to visit blocks and stream their index pages.
def transition.budget.state(file: File, state: State) -> Nat & Reader:
  match state:
    case State{+size, header, +index_offset, used, total, +block_count,
        next_block, decoded, root_hash, index_hash, last_key, selected}:
      +blocks = U32.to_nat(block_count)
      +index_bytes = Nat.sub(size, Nat.add(index_offset, 44n))
      +page_bytes = BlockIndexPolicy.max_bytes()
      +pages = Nat.div(Nat.add(index_bytes, Nat.sub(page_bytes, 1n)), page_bytes)
      (Nat.add(Nat.add(Nat.mul(4n, blocks), Nat.mul(3n, pages)), 4n),
        Reader{file, State{size, header, index_offset, used, total, block_count,
          next_block, decoded, root_hash, index_hash, last_key, selected}})

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexPolicy.bend&name=max_bytes
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockReader.bend&name=Reader
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockReader.bend&name=State