src/scan/BlockIndexFormatPolicy.bend

mylsm-lsm-store@0.6.0.1 · 51 lines · 10 definitions

1import Base
2
3# Describes the fixed-width section sizes of the separator index layout.
4def header_bytes() -> Nat:
5  8n
6
7# Returns the fixed offset/length metadata width for one data block.
8def entry_bytes() -> Nat:
9  16n
10
11# Returns the extended footer width including its root digest.
12def footer_bytes() -> Nat:
13  44n
14
15# Returns the earliest valid position after the fixed SST header.
16def minimum_data_offset() -> Nat:
17  20n
18
19def nat.clone.pair(+value: Nat) -> Nat & Nat:
20  (Nat.mul(1n, value), Nat.mul(1n, value))
21
22# Computes index bytes from fixed records and the packed separator region.
23def index_bytes(block_count: Nat, separator_bytes: Nat) -> Nat:
24  Nat.add(Nat.add(header_bytes(), Nat.mul(block_count, entry_bytes())),
25    separator_bytes)
26
27# Locates the index from the index length retained in the extended footer.
28def index_offset(file_size: Nat, index_length: Nat) -> Nat:
29  Nat.sub(file_size, Nat.add(footer_bytes(), index_length))
30
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))
43
44# Checks the index/footer interval without underflow or header overlap.
45def interval_valid(file_size: Nat, index_length: Nat) -> Bool:
46  interval_valid.copies(nat.clone.pair(file_size),
47    nat.clone.pair(index_length))
48
49# Checks one separator slice against the packed separator region.
50def separator_valid(offset: Nat, length: Nat, region_length: Nat) -> Bool:
51  Nat.is_le(Nat.add(offset, length), region_length)