BlockIndexPolicy.entry_valid.copies: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexPolicy.bend as BlockIndexPolicy
Lines 48-57 of mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexPolicy.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/BlockIndexPolicy.bend&start_line=48&end_line=57

import Base

# Combines independent offset copies to validate the complete block interval.
def entry_valid.copies(
  offsets: Nat & Nat,
  data_length: Nat,
  index_offset: Nat
) -> Bool:
  match offsets:
    case (start, for_end):
      Nat.is_le(20n, start) &&
        Nat.is_le(Nat.add(for_end, data_length), index_offset)

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=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