BlockIndexFormatPolicy.interval_valid.copies: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexFormatPolicy.bend as BlockIndexFormatPolicy
Lines 31-42 of mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexFormatPolicy.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexFormatPolicy.bend&start_line=31&end_line=42

import Base

# Checks the index/footer interval without overflowing its containing file.
def interval_valid.copies(
  sizes: Nat & Nat,
  indices: Nat & Nat
) -> Bool:
  match sizes:
    case (measured_size, checked_size):
      match indices:
        case (measured_length, checked_length):
          Nat.is_le(Nat.add(footer_bytes(), measured_length), measured_size) &&
            Nat.is_le(minimum_data_offset(),
              index_offset(checked_size, checked_length))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=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/BlockIndexFormatPolicy.bend&name=footer_bytes
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexFormatPolicy.bend&name=index_offset
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexFormatPolicy.bend&name=minimum_data_offset