Snapshot.registry.release.input.bytes: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend as Snapshot
Lines 374-393 of mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend&start_line=374&end_line=393

import Base

# Separates byte arithmetic inputs so both admission checks retain their values.
def registry.release.input.bytes(
  count_copies: Nat & Nat,
  count_original: Nat,
  bytes_copies: Nat & Nat,
  bytes_original: Nat,
  release_copies: Nat & Nat
) -> RegistryReleaseDecision:
  match count_copies:
    case (count_for_subtract, count_for_check):
      match bytes_copies:
        case (bytes_for_subtract, bytes_for_check):
          match release_copies:
            case (released_for_subtract, released_for_check):
              registry.release.result(
                (Nat.sub(count_for_subtract, 1n),
                  Nat.sub(bytes_for_subtract, released_for_subtract)),
                Registry{count_original, bytes_original},
                (Nat.is_lt(0n, count_for_check),
                  Nat.is_le(released_for_check, bytes_for_check)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Nat.is_lt
  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=mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend&name=Registry
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend&name=RegistryReleaseDecision
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend&name=registry.release.result