def interval_valid.copies

mylsm-lsm-store@0.6.0.1 · src/scan/BlockIndexFormatPolicy.bend:31

import Base

31# Checks the index/footer interval without overflowing its containing file.
32def interval_valid.copies(
33  sizes: Nat & Nat,
34  indices: Nat & Nat
35) -> Bool:
36  match sizes:
37    case (measured_size, checked_size):
38      match indices:
39        case (measured_length, checked_length):
40          Nat.is_le(Nat.add(footer_bytes(), measured_length), measured_size) &&
41            Nat.is_le(minimum_data_offset(),
42              index_offset(checked_size, checked_length))