1	import Base
2	
3	# Classifies invalid, terminal, and continuing block traversal states.
4	type Advance is Data:
5	  Invalid{}
6	  Finish{}
7	  Continue{remaining: Nat}
8	
9	# Decrements the declared block count exactly once after a validated block.
10	def after_block(remaining: Nat) -> Advance:
11	  match remaining:
12	    case 0n: Invalid{}
13	    case 1n: Finish{}
14	    case 1n+rest: Continue{rest}
15	
16	# Returns the number of blocks left in a continuing traversal.
17	def remaining(decision: Advance) -> Nat:
18	  match decision:
19	    case Continue{remaining}: remaining
20	    case _: 0n
21	
22	def write.page.size() -> Nat:
23	  16n
24	
25	def write.pages(entries: Nat) -> Nat:
26	  Nat.div(Nat.add(entries, 15n), write.page.size())
27	
28	def write.fuel(entries: Nat) -> Nat:
29	  Nat.add(Nat.mul(3n, write.pages(entries)), 1n)
30	
31	def max.exchange.bytes() -> Nat:
32	  67108864n
33	
34	def exchange.fits(limit: Nat, size: Nat) -> Bool:
35	  Nat.is_le(size, limit)