CursorCodec.item.key.bound.check: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/coordinator/CursorCodec.bend as CursorCodec
Lines 212-225 of mylsm-lsm-store@0.6.0.1/src/coordinator/CursorCodec.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/CursorCodec.bend&start_line=212&end_line=225

import Base
import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes

# Accepts key lengths that leave a complete value length word.
def item.key.bound.check(
  payload: Bytes.Bytes,
  sizes: U32 & U32,
  key_lengths: U32 & U32
) -> Decision:
  match sizes:
    case (checked_size, retained_size):
      match key_lengths:
        case (checked_key_length, retained_key_length):
          item.key.bound.checked(Nat.is_le(
            Nat.add(9n, U32.to_nat(checked_key_length)),
            U32.to_nat(checked_size)), payload, retained_size,
            retained_key_length)

Uses (9):
  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.is_le
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=Bytes
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/CursorCodec.bend&name=Decision
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/CursorCodec.bend&name=item.key.bound.checked