src/scan/BlockIndexPolicy.bend

mylsm-lsm-store@0.6.0.1 · 71 lines · 15 definitions

1import Base
2import mylsm-lsm-store@0.6.0.1/src/coordinator/QueuePolicy.bend as QueuePolicy
3
4# Describes one bounded page in a serialized block index.
5type PageDecision is Data:
6  Page{first: Nat, count: Nat}
7
8# Returns the fixed bound for all resident serialized-index buffers.
9def resident_budget() -> Nat:
10  65536n
11
12# Counts the input buffer, positional-read assembly, and two hash inputs.
13def buffer_copies() -> Nat:
14  4n
15
16# Bounds one serialized-index read so its live copies fit the resident budget.
17def max_bytes() -> Nat:
18  16384n
19
20# Computes the number of entries that fit beside one page header.
21def max_entries() -> Nat:
22  2047n
23
24# Returns the maximum entries that fit in a page-sized index span.
25def max_blocks() -> Nat:
26  max_entries()
27
28# Counts all bounded resident copies of one serialized-index read.
29def resident_metadata_bytes(page_bytes: Nat) -> Nat:
30  Nat.mul(buffer_copies(), page_bytes)
31
32# Accepts one page only when it fits the resident budget.
33def accepts(entries: Nat) -> Bool:
34  Nat.is_le(entries, max_blocks())
35
36# Bounds one positional index read without restricting the total index size.
37def read_bytes.limit(limit: Nat, remaining: Nat) -> Nat:
38  Nat.min(limit, remaining)
39
40# Applies the resident page limit to one positional index read.
41def read_bytes(remaining: Nat) -> Nat:
42  read_bytes.limit(max_bytes(), remaining)
43
44# Accepts a block ordinal only when a serialized index contains that block.
45def contains(block_count: Nat, index: Nat) -> Bool:
46  Nat.is_lt(index, block_count)
47
48# Combines independent offset copies to validate the complete block interval.
49def entry_valid.copies(
50  offsets: Nat & Nat,
51  data_length: Nat,
52  index_offset: Nat
53) -> Bool:
54  match offsets:
55    case (start, for_end):
56      Nat.is_le(20n, start) &&
57        Nat.is_le(Nat.add(for_end, data_length), index_offset)
58
59# Accepts a block range only when it stays between the header and index.
60def entry_valid(data_offset: Nat, data_length: Nat, index_offset: Nat) -> Bool:
61  entry_valid.copies(QueuePolicy.nat.clone.pair(data_offset), data_length,
62    index_offset)
63
64def page.parts(firsts: Nat & Nat, entries: Nat) -> PageDecision:
65  match firsts:
66    case (first, for_remaining):
67      Page{first, Nat.min(max_entries(), Nat.sub(entries, for_remaining))}
68
69# Selects a fixed-budget index page; a zero count marks the terminal position.
70def page(first: Nat, entries: Nat) -> PageDecision:
71  page.parts(QueuePolicy.nat.clone.pair(first), entries)