policy/exhaust.bend

cswap-bend-cli@0.1.0.0 · 178 lines · 22 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
5import cswap-bend-cli@0.1.0.0/policy/pick.bend as K
6
7# Why nothing qualified: which accounts are readable, which are exhausted,
8# and the earliest moment a blocked account is usable again.
9
10# How an account is blocked: not at all, at 100 % with no known reset, or
11# until the latest reset among its windows at 100 %.
12type Br is Data:
13  NotBlocked{}
14  BlockedNoTs{}
15  BlockedAt{t: Nat}
16
17type Er is Data:
18  ErNone{}
19  ErAt{t: Nat}
20  ErPoison{}
21
22def readable.at(+ok: Bool, +m: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
23  match ok:
24    case True{}:
25      m
26    case False{}:
27      None{}
28
29# The trusted headroom of a candidate, backoff or not.
30def readable.acct(+a: T.Account, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Maybe<&2, Nat>:
31  readable.at(R.isc(a, active), U.head.row(U.usage.of(U.account.slot(a), us), now, ms))
32
33def is_some(+m: Maybe<&2, Nat>) -> Bool:
34  match m:
35    case None{}:
36      False{}
37    case Some{x}:
38      True{}
39
40# Some candidate has a trusted reading.
41def any_known(+as: List<&2, T.Account>, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Bool:
42  match as:
43    case Nil{}:
44      False{}
45    case Con{a, t}:
46      is_some(readable.acct(a, active, us, now, ms)) || any_known(t, active, us, now, ms)
47
48def exhausted.known(+m: Maybe<&2, Nat>) -> Bool:
49  match m:
50    case None{}:
51      False{}
52    case Some{h}:
53      Nat.is_eq(h, 0n)
54
55def exhausted.at(+base: Bool, +m: Maybe<&2, Nat>) -> Bool:
56  match base:
57    case False{}:
58      True{}
59    case True{}:
60      exhausted.known(m)
61
62# Every OAuth candidate is readable and at its limit.
63def all_exhausted(+as: List<&2, T.Account>, +active: Nat, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Bool:
64  match as:
65    case Nil{}:
66      True{}
67    case Con{a, t}:
68      exhausted.at(R.isc(a, active), readable.acct(a, active, us, now, ms)) && all_exhausted(t, active, us, now, ms)
69
70def any_cand(+as: List<&2, T.Account>, +active: Nat) -> Bool:
71  match as:
72    case Nil{}:
73      False{}
74    case Con{a, t}:
75      R.isc(a, active) || any_cand(t, active)
76
77def any_api(+as: List<&2, T.Account>, +active: Nat) -> Bool:
78  match as:
79    case Nil{}:
80      False{}
81    case Con{a, t}:
82      R.isapi(a, active) || any_api(t, active)
83
84# The first last-resort API-key candidate, in sequence order.
85def api.first(+as: List<&2, T.Account>, +active: Nat) -> Maybe<&2, Nat>:
86  match as:
87    case Nil{}:
88      None{}
89    case Con{a, t}:
90      K.first.pick(R.isapi(a, active), U.account.slot(a), api.first(t, active))
91
92# -------------------------------------------------- earliest recovery
93
94def br.upd(+acc: Br, +r: Maybe<&2, Nat>) -> Br:
95  match acc r:
96    case NotBlocked{} None{}:
97      BlockedNoTs{}
98    case BlockedNoTs{} None{}:
99      BlockedNoTs{}
100    case BlockedAt{x} None{}:
101      BlockedAt{x}
102    case NotBlocked{} Some{t}:
103      BlockedAt{t}
104    case BlockedNoTs{} Some{t}:
105      BlockedAt{t}
106    case BlockedAt{x} Some{t}:
107      BlockedAt{Nat.max(x, t)}
108
109def br.if(+blocked: Bool, +acc: Br, +r: Maybe<&2, Nat>) -> Br:
110  match blocked:
111    case True{}:
112      br.upd(acc, r)
113    case False{}:
114      acc
115
116def br.win(+ws: List<&2, T.Win>, +acc: Br) -> Br:
117  match ws:
118    case Nil{}:
119      acc
120    case Con{w, t}:
121      match w:
122        case T.Win{p, r}:
123          br.win(t, br.if(Nat.is_ge(p, T.full()), acc, r))
124
125def br.fresh(+ok: Bool, +u: T.Usage, +ms: List<&2, String>) -> Br:
126  match ok:
127    case True{}:
128      br.win(U.windows(u, ms), NotBlocked{})
129    case False{}:
130      NotBlocked{}
131
132def br.row(+m: Maybe<&2, T.Usage>, +now: Nat, +ms: List<&2, String>) -> Br:
133  match m:
134    case None{}:
135      NotBlocked{}
136    case Some{u}:
137      br.fresh(U.trusted(u, now, ms), u, ms)
138
139def er.min(+e: Er, +t: Nat) -> Er:
140  match e:
141    case ErNone{}:
142      ErAt{t}
143    case ErAt{x}:
144      ErAt{Nat.min(x, t)}
145    case ErPoison{}:
146      ErPoison{}
147
148def er.at(+past: Bool, +e: Er, +t: Nat) -> Er:
149  match past:
150    case True{}:
151      ErPoison{}
152    case False{}:
153      er.min(e, t)
154
155def er.step(+e: Er, +b: Br, +now: Nat) -> Er:
156  match b:
157    case NotBlocked{}:
158      e
159    case BlockedNoTs{}:
160      ErPoison{}
161    case BlockedAt{t}:
162      er.at(Nat.is_le(t, now), e, t)
163
164def er.out(+e: Er) -> Maybe<&2, Nat>:
165  match e:
166    case ErAt{t}:
167      Some{t}
168    case o:
169      None{}
170
171# Earliest moment any blocked account (the live one included) is usable
172# again; None when it cannot be proven.
173def earliest(+as: List<&2, T.Account>, +us: List<&2, T.Usage>, +now: Nat, +ms: List<&2, String>, +e: Er) -> Er:
174  match as:
175    case Nil{}:
176      e
177    case Con{a, t}:
178      earliest(t, us, now, ms, er.step(e, br.row(U.usage.of(U.account.slot(a), us), now, ms), now))