Operation.put.bound.checked: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/coordinator/Operation.bend as Operation
Lines 85-99 of mylsm-lsm-store@0.6.0.1/src/coordinator/Operation.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/Operation.bend&start_line=85&end_line=99

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

def put.bound.checked(
  payload: Bytes.Bytes,
  actual_length: U32,
  key_lengths: U32 & U32 & U32,
  value_lengths: U32 & U32 & U32
) -> Decision:
  match key_lengths:
    case (key_check, (key_length, key_offset)):
      match value_lengths:
        case (value_check, (value_length, value_copy)):
          put.bound.result(
            Nat.is_eq(U32.to_nat(actual_length),
              Nat.add(8n, Nat.add(U32.to_nat(key_check),
                U32.to_nat(value_check)))),
            payload, (key_length, key_offset), (value_length, value_copy))

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_eq
  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/Operation.bend&name=Decision
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/coordinator/Operation.bend&name=put.bound.result