1	import Base
2	import ../coordinator/QueuePolicy.bend as QueuePolicy
3	
4	# Bounds source reads by the base, delta, and one terminal observation.
5	def budget(base_records: Nat, delta_records: Nat) -> Nat:
6	  Nat.add(Nat.add(base_records, delta_records), 1n)
7	
8	# Reserves writer transitions for every source read plus fixed finalization.
9	def writer_transitions(base_records: Nat, delta_records: Nat) -> Nat:
10	  Nat.add(Nat.mul(3n, budget(base_records, delta_records)), 8n)
11	
12	def nat.clone.pair(value: Nat) -> Nat & Nat:
13	  QueuePolicy.nat.clone.pair(value)