1	import Base
2	import ../coordinator/QueuePolicy.bend as QueuePolicy
3	
4	# Describes one bounded page in a serialized block index.
5	type PageDecision is Data:
6	  Page{first: Nat, count: Nat}
7	
8	# Returns the fixed bound for all resident serialized-index buffers.
9	def resident_budget() -> Nat:
10	  65536n
11	
12	# Counts the input buffer, positional-read assembly, and two hash inputs.
13	def buffer_copies() -> Nat:
14	  4n
15	
16	# Bounds one serialized-index read so its live copies fit the resident budget.
17	def max_bytes() -> Nat:
18	  16384n
19	
20	# Computes the number of entries that fit beside one page header.
21	def max_entries() -> Nat:
22	  2047n
23	
24	# Returns the maximum entries that fit in a page-sized index span.
25	def max_blocks() -> Nat:
26	  max_entries()
27	
28	# Counts all bounded resident copies of one serialized-index read.
29	def 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.
33	def accepts(entries: Nat) -> Bool:
34	  Nat.is_le(entries, max_blocks())
35	
36	# Bounds one positional index read without restricting the total index size.
37	def 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.
41	def 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.
45	def 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.
49	def 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.
60	def 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	
64	def 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.
70	def page(first: Nat, entries: Nat) -> PageDecision:
71	  page.parts(QueuePolicy.nat.clone.pair(first), entries)