1	import Base
2	import ../Keys.bend as Keys
3	import ../coordinator/QueuePolicy.bend as QueuePolicy
4	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
5	
6	# Holds the binary-search interval and latest eligible block ordinal.
7	type Search is Data:
8	  Search{low: Nat, high: Nat, best: Nat}
9	
10	# Selects the lower or upper half of the separator search interval.
11	type Move is Data:
12	  SearchLower{}
13	  SearchUpper{}
14	
15	def midpoint.copies(lows: Nat & Nat, high: Nat) -> Nat:
16	  match lows:
17	    case (offset, subtractor):
18	      Nat.add(offset, Nat.div(Nat.sub(high, subtractor), 2n))
19	
20	# Chooses the midpoint of a half-open block-index interval.
21	def midpoint(low: Nat, high: Nat) -> Nat:
22	  midpoint.copies(QueuePolicy.nat.clone.pair(low), high)
23	
24	def move.order(is_less: Bool) -> Move:
25	  match is_less:
26	    case True{}: SearchLower{}
27	    case False{}: SearchUpper{}
28	
29	# Compares the target key with one block's first-key separator.
30	def move(target: Bytes.Bytes, separator: Bytes.Bytes) -> Move:
31	  move.order(Cmp.is_lt(Keys.Bytes.cmp(target, separator)))
32	
33	def advance.lower(state: Search, mid: Nat) -> Search:
34	  match state:
35	    case Search{low, _, best}: Search{low, mid, best}
36	
37	def advance.upper.copies(state: Search, mids: Nat & Nat) -> Search:
38	  match state:
39	    case Search{_, high, _}:
40	      match mids:
41	        case (next_mid, candidate):
42	          Search{Nat.add(next_mid, 1n), high, candidate}
43	
44	def advance.upper(state: Search, mid: Nat) -> Search:
45	  advance.upper.copies(state, QueuePolicy.nat.clone.pair(mid))
46	
47	# Advances the interval and candidate after one separator comparison.
48	def advance(state: Search, direction: Move, mid: Nat) -> Search:
49	  match direction:
50	    case SearchLower{}: advance.lower(state, mid)
51	    case SearchUpper{}: advance.upper(state, mid)
52	
53	# Reports whether the half-open search interval remains nonempty.
54	def active(state: Search) -> Bool:
55	  match state:
56	    case Search{low, high, _}: Nat.is_lt(low, high)
57	
58	# Returns the latest separator not greater than the target key.
59	def selected_block(state: Search) -> Nat:
60	  match state:
61	    case Search{_, _, best}: best