Snapshot.reserve.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 278-295 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=278&end_line=295

import Base

# Computes the updated retained-byte total and both admission checks.
def reserve.bytes(
  retained: Nat & Nat,
  requested: Nat & Nat,
  snapshot_count: Nat & Nat,
  max_snapshots: Nat,
  max_retained_bytes: Nat
) -> Nat & (Nat & (Bool & Bool)):
  match retained:
    case (retained_value, retained_check):
      match requested:
        case (requested_value, requested_check):
          match snapshot_count:
            case (count_output, count_check):
              (count_output,
                (Nat.add(retained_value, requested_value),
                  (Nat.is_lt(count_check, max_snapshots),
                  Nat.is_le(Nat.add(retained_check, requested_check), max_retained_bytes))))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma