policy/safe.bend

cswap-bend-cli@0.1.0.0 · 203 lines · 28 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# Behaviour profiles, part 1: the strategies other than `best`, and the one
7# candidate picker they share. A strategy only chooses a ranking key; whether
8# a candidate may be chosen at all is `safe`, the same for every strategy.
9#
10# `safe`: an OAuth account that is enabled and not the live slot, with a
11# trusted reading whose headroom is above zero, and not in backoff. Unlike
12# `best` (which keeps a backoff row with a still-trusted reading eligible to
13# stay byte-identical with the reference), these strategies skip an account
14# in backoff.
15
16type Algo is Data:
17  ABest{}
18  ARoundRobin{}
19  ASoonestReset{}
20  ASticky{}
21  ADrainFirst{}
22
23# A candidate with its ranking key (smaller wins: `k1`, then `k2`) and its
24# headroom. `k1` None is infinity.
25type Cd is Data:
26  Cd{slot: Nat, k1: Maybe<&2, Nat>, k2: Nat, h: Nat}
27
28# The reading is decision-grade and carries a headroom.
29def known(+m: Maybe<&2, Nat>) -> Bool:
30  match m:
31    case None{}:
32      False{}
33    case Some{x}:
34      True{}
35
36def exhausted(+m: Maybe<&2, Nat>) -> Bool:
37  match m:
38    case None{}:
39      False{}
40    case Some{x}:
41      Nat.is_eq(x, 0n)
42
43def backed_off(+m: Maybe<&2, T.Usage>, +now: Nat) -> Bool:
44  match m:
45    case None{}:
46      False{}
47    case Some{u}:
48      U.in_backoff(u, now)
49
50# A row with a trusted headroom above zero, not in backoff.
51def row.safe(+m: Maybe<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Bool:
52  known(U.head.row(m, now, ms)) && Bool.not(exhausted(U.head.row(m, now, ms))) && Bool.not(backed_off(m, now))
53
54def safe(+a: T.Account, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Bool:
55  R.isc(a, active) && row.safe(U.usage.of(U.account.slot(a), us), now, ms)
56
57def h.of(+m: Maybe<&2, Nat>) -> Nat:
58  match m:
59    case None{}:
60      0n
61    case Some{x}:
62      x
63
64# ---------------------------------------------------------------- ranking keys
65
66def rr.group.at(+after: Bool) -> Nat:
67  match after:
68    case True{}:
69      0n
70    case False{}:
71      1n
72
73def rr.group(+slot: Nat, +active: Nat) -> Nat:
74  rr.group.at(Nat.is_gt(slot, active))
75
76# round-robin: the next slot after the live one, wrapping to the lowest.
77# soonest-reset: the weekly window that resets first (unknown last), then more
78# headroom. drain-first: the least headroom (the most used). best, sticky: the
79# most headroom. Ties go to the first account in sequence order.
80def key1(+algo: Algo, +active: Nat, +slot: Nat, +reset: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
81  match algo:
82    case ARoundRobin{}:
83      Some{rr.group(slot, active)}
84    case ASoonestReset{}:
85      reset
86    case o:
87      Some{0n}
88
89def key2(+algo: Algo, +slot: Nat, +h: Nat) -> Nat:
90  match algo:
91    case ARoundRobin{}:
92      slot
93    case ADrainFirst{}:
94      h
95    case o:
96      Nat.sub(T.full(), h)
97
98def key(+algo: Algo, +active: Nat, +slot: Nat, +h: Nat, +reset: Maybe<&2, Nat>) -> Cd:
99  Cd{slot, key1(algo, active, slot, reset), key2(algo, slot, h), h}
100
101def lt1(+a: Maybe<&2, Nat>, +b: Maybe<&2, Nat>) -> Bool:
102  R.rec.rle(a, b) && Bool.not(R.rec.req(a, b))
103
104# c ranks strictly before d.
105def cd.lt(+c: Cd, +d: Cd) -> Bool:
106  match c d:
107    case Cd{s1, a1, a2, h1} Cd{s2, b1, b2, h2}:
108      lt1(a1, b1) || (R.rec.req(a1, b1) && Nat.is_lt(a2, b2))
109
110# ------------------------------------------------------------- the candidates
111
112def cand.need(+ok: Bool, +c: Cd) -> Maybe<&2, Cd>:
113  match ok:
114    case True{}:
115      Some{c}
116    case False{}:
117      None{}
118
119def cand.rows(+algo: Algo, +a: T.Account, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>, +need: Nat, +m: Maybe<&2, T.Usage>) -> Maybe<&2, Cd>:
120  cand.need(Nat.is_ge(h.of(U.head.row(m, now, ms)), need), key(algo, active, U.account.slot(a), h.of(U.head.row(m, now, ms)), R.seven.row(m, now, ms)))
121
122# The candidate `a` is when it is safe and has the headroom the landing needs.
123def cand.go(+sf: Bool, +algo: Algo, +a: T.Account, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>, +need: Nat) -> Maybe<&2, Cd>:
124  match sf:
125    case True{}:
126      cand.rows(algo, a, active, us, now, ms, need, U.usage.of(U.account.slot(a), us))
127    case False{}:
128      None{}
129
130def cand(+algo: Algo, +a: T.Account, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>, +need: Nat) -> Maybe<&2, Cd>:
131  cand.go(safe(a, active, us, now, ms), algo, a, active, us, now, ms, need)
132
133def merge.at(+tail_first: Bool, +c: Cd, +d: Cd) -> Maybe<&2, Cd>:
134  match tail_first:
135    case True{}:
136      Some{d}
137    case False{}:
138      Some{c}
139
140def merge.some(+c: Cd, +tail: Maybe<&2, Cd>) -> Maybe<&2, Cd>:
141  match tail:
142    case None{}:
143      Some{c}
144    case Some{d}:
145      merge.at(cd.lt(d, c), c, d)
146
147# The head's candidate against the best of the rest; the head keeps a tie.
148def merge(+m: Maybe<&2, Cd>, +tail: Maybe<&2, Cd>) -> Maybe<&2, Cd>:
149  match m:
150    case None{}:
151      tail
152    case Some{c}:
153      merge.some(c, tail)
154
155# The best candidate in sequence order.
156def pick(+algo: Algo, +as: List<&2, T.Account>, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>, +need: Nat) -> Maybe<&2, Cd>:
157  match as:
158    case Nil{}:
159      None{}
160    case Con{a, t}:
161      merge(cand(algo, a, active, us, now, ms, need), pick(algo, t, active, us, now, ms, need))
162
163# ----------------------------------------------------------------------- names
164
165def name.pick(+hit: Bool, +a: Algo, +rest: Maybe<&2, Algo>) -> Maybe<&2, Algo>:
166  match hit:
167    case True{}:
168      Some{a}
169    case False{}:
170      rest
171
172# The strategy a name stands for.
173def parse(+s: String) -> Maybe<&2, Algo>:
174  name.pick(String.eq(s, "best"), ABest{},
175    name.pick(String.eq(s, "round-robin"), ARoundRobin{},
176      name.pick(String.eq(s, "soonest-reset"), ASoonestReset{},
177        name.pick(String.eq(s, "sticky"), ASticky{},
178          name.pick(String.eq(s, "drain-first"), ADrainFirst{}, None{})))))
179
180def name(+algo: Algo) -> String:
181  match algo:
182    case ABest{}:
183      "best"
184    case ARoundRobin{}:
185      "round-robin"
186    case ASoonestReset{}:
187      "soonest-reset"
188    case ASticky{}:
189      "sticky"
190    case ADrainFirst{}:
191      "drain-first"
192
193def names() -> List<&2, String>:
194  ["best", "round-robin", "soonest-reset", "sticky", "drain-first"]
195
196# `best` keeps the reference's engine (and its looser eligibility); the rest
197# use `pick`.
198def strict(+algo: Algo) -> Bool:
199  match algo:
200    case ABest{}:
201      False{}
202    case o:
203      True{}