CursorOpenCodec.field.sized.inputs: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/coordinator/CursorOpenCodec.bend as CursorOpenCodec
Lines 103-118 of mylsm-lsm-store@0.6.0.1/src/coordinator/CursorOpenCodec.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/CursorOpenCodec.bend&start_line=103&end_line=118

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

# Separates validation inputs from the values passed to the slice decision.
def field.sized.inputs(
  payload: Bytes.Bytes,
  totals: U32 & U32,
  offsets: U32 & U32,
  lengths: U32 & U32
) -> BoundResult:
  match totals:
    case (_, check_total):
      match offsets:
        case (slice_offset, check_offset):
          match lengths:
            case (slice_length, check_length):
              field.sized.decision(payload, slice_offset, slice_length,
                Nat.is_le(Nat.add(Nat.add(U32.to_nat(check_offset), 4n),
                  U32.to_nat(check_length)), U32.to_nat(check_total)))

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/CursorOpenCodec.bend&name=BoundResult
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/CursorOpenCodec.bend&name=field.sized.decision