1	import Base
2	
3	# Describes the fixed-width section sizes of the separator index layout.
4	def header_bytes() -> Nat:
5	  8n
6	
7	# Returns the fixed offset/length metadata width for one data block.
8	def entry_bytes() -> Nat:
9	  16n
10	
11	# Returns the extended footer width including its root digest.
12	def footer_bytes() -> Nat:
13	  44n
14	
15	# Returns the earliest valid position after the fixed SST header.
16	def minimum_data_offset() -> Nat:
17	  20n
18	
19	def 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.
23	def 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.
28	def 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.
32	def 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.
45	def 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.
50	def separator_valid(offset: Nat, length: Nat, region_length: Nat) -> Bool:
51	  Nat.is_le(Nat.add(offset, length), region_length)