src/scan/BlockIndexPolicy.bend
mylsm-lsm-store@0.6.0.0 · 71 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.6.0.0/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)