~/jendhub

def gate.destination.measured

mylsm-lsm-store@0.6.0.1 · src/transfer/Migrate.bend:290

import mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend as Migrate
import Base

290# Applies count and byte limits after duplicating the affine byte count.
291def gate.destination.measured(
292  max_entries: Nat,
293  max_encoded_bytes: Nat,
294  destination_missing: Bool,
295  entry_counts: Nat & Nat,
296  byte_counts: Nat & Nat
297) -> Decision:
298  match entry_counts:
299    case (result_entries, measured_entries):
300      match byte_counts:
301        case (result_bytes, measured_bytes):
302          Bool.pick(Decision, destination_missing,
303            Bool.pick(Decision,
304              Nat.is_le(measured_entries, max_entries) &&
305                Nat.is_le(measured_bytes, max_encoded_bytes),
306              MigrateReady{result_entries, result_bytes},
307              MigrateRejected{ResourceLimit{}}),
308            MigrateRejected{DestinationExists{}})

Uses (9)

Used by (1)