policy/pick.bend

cswap-bend-cli@0.1.0.0 · 463 lines · 66 definitions

1import Base
2import cswap-bend-cli@0.1.0.0/policy/types.bend as T
3import cswap-bend-cli@0.1.0.0/policy/usage.bend as U
4import cswap-bend-cli@0.1.0.0/policy/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).
11type 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.
18type 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.
23type Pm is Data:
24  PmNone{}
25  PmAt{slot: Nat, r: Maybe<&2, Nat>, h: Nat}
26
27# The tagged pick.
28type 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.
36type 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.
40type 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.
47def 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
54def 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
63def strat.cf(+st: T.Strategy) -> Bool:
64  match st:
65    case T.ConsumeFirst{}:
66      True{}
67    case T.Best{}:
68      False{}
69
70def ah.or0(+ah: Maybe<&2, Nat>) -> Nat:
71  match ah:
72    case None{}:
73      0n
74    case Some{x}:
75      x
76
77def 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
80def 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
89def 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
98def 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
105def 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
112def 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?
120def 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
123def 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
130def 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
137def 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
144def 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
149def 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
164def 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
171def 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.
177def 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
182def 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).
190def 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
197def 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
204def 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.
212def 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
219def 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
226def 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
233def 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
238def 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
245def 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.
255def 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
262def 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
269def 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.
279def 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
286def 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.
296def 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
303def 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
310def 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.
320def 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
327def 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).
337def 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
344def 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
347def 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.
355def 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
358def 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
365def 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.
373def 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
376def 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
383def 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
390def 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.
399def pick.rec(+as: List<&2, T.Account>, +rk: Rk) -> Pk:
400  pick.rec.mid(pick.rh(as, rk, FRec0{}), as, rk)
401
402def rk.cf(+rk: Rk) -> Bool:
403  match rk:
404    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
405      cf
406
407def rk.rm(+rk: Rk) -> Bool:
408  match rk:
409    case Rk{t, cf, rm, ah0, best, ar, ars, thr, s}:
410      rm
411
412def 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
419def 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.
427def pick(+as: List<&2, T.Account>, +rk: Rk) -> Pk:
428  pick.fam(rk.rm(rk), as, rk)
429
430def 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
437def 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
444def 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
451def 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
458def 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