1	import Base
2	import ./types.bend as T
3	import ./usage.bend as U
4	import ./rank.bend as R
5	
6	# The pickers: one ranking family per tick (headroom, weekly reset, or
7	# recovery), each choosing the first account with the best key.
8	
9	# The family a candidate is judged in: weekly reset (consume-first), the
10	# recovery tiers (back soon, back late, one-way fallback).
11	type Fam is Data:
12	  FReset{}
13	  FRec0{}
14	  FRec1{}
15	  FFall{}
16	
17	# A candidate's ranking time (reset or recovery; None is inf) and headroom.
18	type RH is Data:
19	  RH{r: Maybe<&2, Nat>, h: Nat}
20	
21	# A pick before it is tagged with its ranking mode: nothing, or a slot with
22	# the key it won on.
23	type Pm is Data:
24	  PmNone{}
25	  PmAt{slot: Nat, r: Maybe<&2, Nat>, h: Nat}
26	
27	# The tagged pick.
28	type Pk is Data:
29	  PkNone{}
30	  PkAt{slot: Nat, r: Maybe<&2, Nat>, h: Nat, mode: T.Mode}
31	
32	# Everything the pickers read: the trigger, whether the strategy is
33	# consume-first, whether this is recovery mode, the active headroom (0 when
34	# unknown), the best candidate headroom, the active account's binding recovery
35	# and weekly reset, the threshold, and the selection context.
36	type Rk is Data:
37	  Rk{t: T.Trigger, cf: Bool, rm: Bool, ah0: Nat, best: Nat, ar: Maybe<&2, Nat>, ars: Maybe<&2, Nat>, thr: Nat, s: R.Sel}
38	
39	# The best ranking time so far among the family's candidates.
40	type Mn is Data:
41	  MnNone{}
42	  MnAt{r: Maybe<&2, Nat>}
43	
44	# The least headroom a target needs: at-limit and failover take any
45	# headroom; proactive must land below the threshold and beat the active
46	# account by the hysteresis margin.
47	def need.of(+t: T.Trigger, +ah: Nat, +hy: Nat, +thr: Nat) -> Nat:
48	  match t:
49	    case T.Proactive{}:
50	      Nat.max(Nat.add(ah, hy), Nat.add(Nat.sub(T.full(), thr), 1n))
51	    case o:
52	      1n
53	
54	def trig.pc(+t: T.Trigger) -> Bool:
55	  match t:
56	    case T.Proactive{}:
57	      True{}
58	    case T.ConsumeFirstT{}:
59	      True{}
60	    case o:
61	      False{}
62	
63	def strat.cf(+st: T.Strategy) -> Bool:
64	  match st:
65	    case T.ConsumeFirst{}:
66	      True{}
67	    case T.Best{}:
68	      False{}
69	
70	def ah.or0(+ah: Maybe<&2, Nat>) -> Nat:
71	  match ah:
72	    case None{}:
73	      0n
74	    case Some{x}:
75	      x
76	
77	def rk.mk(+t: T.Trigger, +ah: Maybe<&2, Nat>, +ab: Bool, +best: Nat, +ar: Maybe<&2, Nat>, +ars: Maybe<&2, Nat>, +thr: Nat, +hy: Nat, +cf: Bool, +active: Nat, +bar: Maybe<&2, Nat>, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Rk:
78	  Rk{t, cf, ab && trig.pc(t), ah.or0(ah), best, ar, ars, thr, R.Sel{active, bar, need.of(t, ah.or0(ah), hy, thr), us, now, ms}}
79	
80	def rk.bar(+rk: Rk, +bar: Maybe<&2, Nat>) -> Rk:
81	  match rk:
82	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
83	      match s:
84	        case R.Sel{active, b0, need, us, now, ms}:
85	          Rk{t, cf, rm, ah0, best, ar, ars, thr, R.Sel{active, bar, need, us, now, ms}}
86	
87	# ---------------------------------------------------- family candidates
88	
89	def land.gate(+t: T.Trigger, +h: Nat, +thr: Nat) -> Bool:
90	  match t:
91	    case T.AtLimit{}:
92	      True{}
93	    case T.Failover{}:
94	      True{}
95	    case o:
96	      Nat.is_ge(h, Nat.add(Nat.sub(T.full(), thr), 1n))
97	
98	def reset.sooner(+rc: Maybe<&2, Nat>, +ars: Maybe<&2, Nat>) -> Bool:
99	  match rc ars:
100	    case Some{a} Some{b}:
101	      Nat.is_lt(a, b)
102	    case o _:
103	      False{}
104	
105	def reset.gate(+t: T.Trigger, +rc: Maybe<&2, Nat>, +ars: Maybe<&2, Nat>) -> Bool:
106	  match t:
107	    case T.ConsumeFirstT{}:
108	      reset.sooner(rc, ars)
109	    case o:
110	      True{}
111	
112	def rh.if(+ok: Bool, +rc: Maybe<&2, Nat>, +h: Nat) -> Maybe<&2, RH>:
113	  match ok:
114	    case True{}:
115	      Some{RH{rc, h}}
116	    case False{}:
117	      None{}
118	
119	# Is this candidate ranked by recovery rather than by headroom?
120	def by_recovery(+rc: Maybe<&2, Nat>, +ar: Maybe<&2, Nat>, +ah0: Nat, +best: Nat, +now: Nat) -> Bool:
121	  (Nat.is_le(ah0, 300n) && Nat.is_le(best, 300n)) || R.rec.within(rc, now) || R.rec.within(ar, now)
122	
123	def cdn.rec0(+h: Nat, +rc: Maybe<&2, Nat>, +rk: Rk) -> Maybe<&2, RH>:
124	  match rk:
125	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
126	      match s:
127	        case R.Sel{active, bar, need, us, now, ms}:
128	          rh.if(by_recovery(rc, ar, ah0, best, now) && R.rec.lt_minus(rc, ar), rc, h)
129	
130	def cdn.rec1(+h: Nat, +rc: Maybe<&2, Nat>, +rk: Rk) -> Maybe<&2, RH>:
131	  match rk:
132	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
133	      match s:
134	        case R.Sel{active, bar, need, us, now, ms}:
135	          rh.if(Bool.not(by_recovery(rc, ar, ah0, best, now)) && Nat.is_ge(h, Nat.mul(2n, ah0)), rc, h)
136	
137	def cdn.fall(+h: Nat, +rc: Maybe<&2, Nat>, +rk: Rk) -> Maybe<&2, RH>:
138	  match rk:
139	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
140	      match s:
141	        case R.Sel{active, bar, need, us, now, ms}:
142	          rh.if(Bool.not(by_recovery(rc, ar, ah0, best, now)) && Nat.is_lt(h, Nat.mul(2n, ah0)) && Nat.is_le(ah0, 300n) && Nat.is_ge(h, ah0) && R.rec.lt_minus(rc, ar), rc, h)
143	
144	def cdn.reset(+h: Nat, +rc: Maybe<&2, Nat>, +rk: Rk) -> Maybe<&2, RH>:
145	  match rk:
146	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
147	      rh.if(land.gate(t, h, thr) && reset.gate(t, rc, ars), rc, h)
148	
149	def cdn.fam(+rk: Rk, +f: Fam, +h: Nat, +a: T.Account) -> Maybe<&2, RH>:
150	  match rk:
151	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
152	      match s:
153	        case R.Sel{active, bar, need, us, now, ms}:
154	          match f:
155	            case FReset{}:
156	              cdn.reset(h, R.seven.row(U.usage.of(U.account.slot(a), us), now, ms), rk)
157	            case FRec0{}:
158	              cdn.rec0(h, R.rec.row(U.usage.of(U.account.slot(a), us), now, ms), rk)
159	            case FRec1{}:
160	              cdn.rec1(h, R.rec.row(U.usage.of(U.account.slot(a), us), now, ms), rk)
161	            case FFall{}:
162	              cdn.fall(h, R.rec.row(U.usage.of(U.account.slot(a), us), now, ms), rk)
163	
164	def cdn.at(+m: Maybe<&2, Nat>, +f: Fam, +a: T.Account, +rk: Rk) -> Maybe<&2, RH>:
165	  match m:
166	    case None{}:
167	      None{}
168	    case Some{h}:
169	      cdn.fam(rk, f, h, a)
170	
171	def rk.sel(+rk: Rk) -> R.Sel:
172	  match rk:
173	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
174	      s
175	
176	# A candidate of family f, with its ranking time and headroom.
177	def cdn(+a: T.Account, +rk: Rk, +f: Fam) -> Maybe<&2, RH>:
178	  cdn.at(R.elig(a, rk.sel(rk)), f, a, rk)
179	
180	# ------------------------------------------------- headroom family pickers
181	
182	def top.step(+c: Maybe<&2, Nat>, +acc: Nat) -> Nat:
183	  match c:
184	    case None{}:
185	      acc
186	    case Some{h}:
187	      Nat.max(acc, h)
188	
189	# The most headroom any candidate offers (0 when there is none).
190	def top(+as: List<&2, T.Account>, +s: R.Sel, +acc: Nat) -> Nat:
191	  match as:
192	    case Nil{}:
193	      acc
194	    case Con{a, t}:
195	      top(t, s, top.step(R.cand(a, s), acc))
196	
197	def first.hit(+c: Maybe<&2, Nat>, +h: Nat) -> Bool:
198	  match c:
199	    case None{}:
200	      False{}
201	    case Some{x}:
202	      Nat.is_eq(x, h)
203	
204	def first.pick(+hit: Bool, +slot: Nat, +rest: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
205	  match hit:
206	    case True{}:
207	      Some{slot}
208	    case False{}:
209	      rest
210	
211	# The first account (sequence order breaks ties) whose candidate headroom is h.
212	def first(+as: List<&2, T.Account>, +s: R.Sel, +h: Nat) -> Maybe<&2, Nat>:
213	  match as:
214	    case Nil{}:
215	      None{}
216	    case Con{a, t}:
217	      first.pick(first.hit(R.cand(a, s), h), U.account.slot(a), first(t, s, h))
218	
219	def pk.slot(+m: Maybe<&2, Nat>, +r: Maybe<&2, Nat>, +h: Nat) -> Pm:
220	  match m:
221	    case None{}:
222	      PmNone{}
223	    case Some{slot}:
224	      PmAt{slot, r, h}
225	
226	def pick.head.at(+h0: Nat, +as: List<&2, T.Account>, +s: R.Sel) -> Pm:
227	  match h0:
228	    case 0n:
229	      PmNone{}
230	    case 1n+p:
231	      pk.slot(first(as, s, h0), None{}, h0)
232	
233	def pick.head(+as: List<&2, T.Account>, +s: R.Sel) -> Pm:
234	  pick.head.at(top(as, s, 0n), as, s)
235	
236	# --------------------------------------------- reset / recovery pickers
237	
238	def mn.min(+m: Mn, +r: Maybe<&2, Nat>) -> Mn:
239	  match m:
240	    case MnNone{}:
241	      MnAt{r}
242	    case MnAt{x}:
243	      MnAt{R.rec.min(x, r)}
244	
245	def minr.step(+c: Maybe<&2, RH>, +m: Mn) -> Mn:
246	  match c:
247	    case None{}:
248	      m
249	    case Some{x}:
250	      match x:
251	        case RH{r, h}:
252	          mn.min(m, r)
253	
254	# The earliest ranking time among the family's candidates.
255	def minr(+as: List<&2, T.Account>, +rk: Rk, +f: Fam, +m: Mn) -> Mn:
256	  match as:
257	    case Nil{}:
258	      m
259	    case Con{a, t}:
260	      minr(t, rk, f, minr.step(cdn(a, rk, f), m))
261	
262	def maxh.pick(+hit: Bool, +h: Nat, +acc: Nat) -> Nat:
263	  match hit:
264	    case True{}:
265	      Nat.max(acc, h)
266	    case False{}:
267	      acc
268	
269	def maxh.step(+c: Maybe<&2, RH>, +r0: Maybe<&2, Nat>, +acc: Nat) -> Nat:
270	  match c:
271	    case None{}:
272	      acc
273	    case Some{x}:
274	      match x:
275	        case RH{r, h}:
276	          maxh.pick(R.rec.req(r, r0), h, acc)
277	
278	# The most headroom among the family's candidates whose time is r0.
279	def maxh(+as: List<&2, T.Account>, +rk: Rk, +f: Fam, +r0: Maybe<&2, Nat>, +acc: Nat) -> Nat:
280	  match as:
281	    case Nil{}:
282	      acc
283	    case Con{a, t}:
284	      maxh(t, rk, f, r0, maxh.step(cdn(a, rk, f), r0, acc))
285	
286	def maxall.step(+c: Maybe<&2, RH>, +acc: Nat) -> Nat:
287	  match c:
288	    case None{}:
289	      acc
290	    case Some{x}:
291	      match x:
292	        case RH{r, h}:
293	          Nat.max(acc, h)
294	
295	# The most headroom among the family's candidates.
296	def maxall(+as: List<&2, T.Account>, +rk: Rk, +f: Fam, +acc: Nat) -> Nat:
297	  match as:
298	    case Nil{}:
299	      acc
300	    case Con{a, t}:
301	      maxall(t, rk, f, maxall.step(cdn(a, rk, f), acc))
302	
303	def minat.pick(+hit: Bool, +r: Maybe<&2, Nat>, +m: Mn) -> Mn:
304	  match hit:
305	    case True{}:
306	      mn.min(m, r)
307	    case False{}:
308	      m
309	
310	def minat.step(+c: Maybe<&2, RH>, +h0: Nat, +m: Mn) -> Mn:
311	  match c:
312	    case None{}:
313	      m
314	    case Some{x}:
315	      match x:
316	        case RH{r, h}:
317	          minat.pick(Nat.is_eq(h, h0), r, m)
318	
319	# The earliest time among the family's candidates with headroom h0.
320	def minat(+as: List<&2, T.Account>, +rk: Rk, +f: Fam, +h0: Nat, +m: Mn) -> Mn:
321	  match as:
322	    case Nil{}:
323	      m
324	    case Con{a, t}:
325	      minat(t, rk, f, h0, minat.step(cdn(a, rk, f), h0, m))
326	
327	def firstrh.hit(+c: Maybe<&2, RH>, +r0: Maybe<&2, Nat>, +h0: Nat) -> Bool:
328	  match c:
329	    case None{}:
330	      False{}
331	    case Some{x}:
332	      match x:
333	        case RH{r, h}:
334	          R.rec.req(r, r0) && Nat.is_eq(h, h0)
335	
336	# The first account whose key is exactly (r0, h0).
337	def firstrh(+as: List<&2, T.Account>, +rk: Rk, +f: Fam, +r0: Maybe<&2, Nat>, +h0: Nat) -> Maybe<&2, Nat>:
338	  match as:
339	    case Nil{}:
340	      None{}
341	    case Con{a, t}:
342	      first.pick(firstrh.hit(cdn(a, rk, f), r0, h0), U.account.slot(a), firstrh(t, rk, f, r0, h0))
343	
344	def pick.rh.go(+h0: Nat, +r0: Maybe<&2, Nat>, +as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
345	  pk.slot(firstrh(as, rk, f, r0, h0), r0, h0)
346	
347	def pick.rh.at(+m: Mn, +as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
348	  match m:
349	    case MnNone{}:
350	      PmNone{}
351	    case MnAt{r0}:
352	      pick.rh.go(maxh(as, rk, f, r0, 0n), r0, as, rk, f)
353	
354	# Earliest time first, then most headroom, then sequence order.
355	def pick.rh(+as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
356	  pick.rh.at(minr(as, rk, f, MnNone{}), as, rk, f)
357	
358	def pick.hr.go(+m: Mn, +h0: Nat, +as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
359	  match m:
360	    case MnNone{}:
361	      PmNone{}
362	    case MnAt{r0}:
363	      pk.slot(firstrh(as, rk, f, r0, h0), r0, h0)
364	
365	def pick.hr.at(+h0: Nat, +as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
366	  match h0:
367	    case 0n:
368	      PmNone{}
369	    case 1n+p:
370	      pick.hr.go(minat(as, rk, f, h0, MnNone{}), h0, as, rk, f)
371	
372	# Most headroom first, then earliest time, then sequence order.
373	def pick.hr(+as: List<&2, T.Account>, +rk: Rk, +f: Fam) -> Pm:
374	  pick.hr.at(maxall(as, rk, f, 0n), as, rk, f)
375	
376	def pk.of(+mode: T.Mode, +p: Pm) -> Pk:
377	  match p:
378	    case PmNone{}:
379	      PkNone{}
380	    case PmAt{slot, r, h}:
381	      PkAt{slot, r, h, mode}
382	
383	def pick.rec.late(+p1: Pm, +as: List<&2, T.Account>, +rk: Rk) -> Pk:
384	  match p1:
385	    case PmNone{}:
386	      pk.of(T.MFallback{}, pick.rh(as, rk, FFall{}))
387	    case PmAt{slot, r, h}:
388	      pk.of(T.MRec1{}, p1)
389	
390	def pick.rec.mid(+p0: Pm, +as: List<&2, T.Account>, +rk: Rk) -> Pk:
391	  match p0:
392	    case PmNone{}:
393	      pick.rec.late(pick.hr(as, rk, FRec1{}), as, rk)
394	    case PmAt{slot, r, h}:
395	      pk.of(T.MRec0{}, p0)
396	
397	# Recovery mode: back-soon candidates by soonest recovery, else back-late
398	# ones by headroom, else the one-way fallback.
399	def pick.rec(+as: List<&2, T.Account>, +rk: Rk) -> Pk:
400	  pick.rec.mid(pick.rh(as, rk, FRec0{}), as, rk)
401	
402	def rk.cf(+rk: Rk) -> Bool:
403	  match rk:
404	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
405	      cf
406	
407	def rk.rm(+rk: Rk) -> Bool:
408	  match rk:
409	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
410	      rm
411	
412	def pick.cf(+cf: Bool, +as: List<&2, T.Account>, +rk: Rk) -> Pk:
413	  match cf:
414	    case True{}:
415	      pk.of(T.MReset{}, pick.rh(as, rk, FReset{}))
416	    case False{}:
417	      pk.of(T.MHead{}, pick.head(as, rk.sel(rk)))
418	
419	def pick.fam(+rm: Bool, +as: List<&2, T.Account>, +rk: Rk) -> Pk:
420	  match rm:
421	    case True{}:
422	      pick.rec(as, rk)
423	    case False{}:
424	      pick.cf(rk.cf(rk), as, rk)
425	
426	# The oauth pick for one ranking context.
427	def pick(+as: List<&2, T.Account>, +rk: Rk) -> Pk:
428	  pick.fam(rk.rm(rk), as, rk)
429	
430	def rk.active(+rk: Rk) -> Nat:
431	  match rk:
432	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
433	      match s:
434	        case R.Sel{active, bar, need, us, now, ms}:
435	          active
436	
437	def rk.us(+rk: Rk) -> List<&2, T.Usage>:
438	  match rk:
439	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
440	      match s:
441	        case R.Sel{active, bar, need, us, now, ms}:
442	          us
443	
444	def rk.now(+rk: Rk) -> Nat:
445	  match rk:
446	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
447	      match s:
448	        case R.Sel{active, bar, need, us, now, ms}:
449	          now
450	
451	def rk.ms(+rk: Rk) -> List<&2, String>:
452	  match rk:
453	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
454	      match s:
455	        case R.Sel{active, bar, need, us, now, ms}:
456	          ms
457	
458	def rk.bar_of(+rk: Rk) -> Maybe<&2, Nat>:
459	  match rk:
460	    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
461	      match s:
462	        case R.Sel{active, bar, need, us, now, ms}:
463	          bar