policy/bar.bend

cswap-bend-cli@0.1.0.0 · 157 lines · 19 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 no-return bar: after a proactive switch away from account A, A is not
7# a target until it has recovered. `recovered` asks whether A is a better
8# proposition than when the engine left it; `no_return` names the barred
9# slot while the bar stands.
10
11def is_none(+m: Maybe<&2, Nat>) -> Bool:
12  match m:
13    case None{}:
14      True{}
15    case Some{x}:
16      False{}
17
18def trig.is_failover(+t: T.Trigger) -> Bool:
19  match t:
20    case T.Failover{}:
21      True{}
22    case o:
23      False{}
24
25# A failover departure: by the recorded trigger, else by the two nulls.
26def snap.fail(+lt: Maybe<&2, T.Trigger>, +lh: Maybe<&2, Nat>, +lr: Maybe<&2, Nat>) -> Bool:
27  match lt:
28    case Some{t}:
29      trig.is_failover(t)
30    case None{}:
31      is_none(lh) && is_none(lr)
32
33# h > 100 - threshold: would the ranking accept it as a landing spot?
34def gt_land(+h: Maybe<&2, Nat>, +thr: Nat) -> Bool:
35  match h:
36    case None{}:
37      False{}
38    case Some{x}:
39      Nat.is_gt(x, Nat.sub(T.full(), thr))
40
41def rec.finite(+a: Maybe<&2, Nat>) -> Bool:
42  match a:
43    case None{}:
44      False{}
45    case Some{x}:
46      True{}
47
48# Failover departure: no baseline, so read only the present. Landing spot, or
49# its binding reset is meaningfully sooner than the active one's.
50def recov.fail(+h: Maybe<&2, Nat>, +peer: Maybe<&2, Nat>, +act: Maybe<&2, Nat>, +thr: Nat, +now: Nat) -> Bool:
51  gt_land(h, thr) || ((rec.finite(act) || R.rec.within(peer, now)) && R.rec.lt_minus(peer, act))
52
53# Dominance over the active account.
54def recov.dom(+h: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +thr: Nat) -> Bool:
55  match h ah:
56    case None{} _:
57      False{}
58    case Some{x} Some{a}:
59      Nat.is_gt(x, Nat.add(Nat.mul(2n, a), 300n))
60    case Some{x} None{}:
61      Nat.is_gt(x, Nat.sub(T.full(), thr))
62
63# Headroom risen three points past the departure baseline.
64def recov.self(+h: Maybe<&2, Nat>, +lh: Maybe<&2, Nat>) -> Bool:
65  match h lh:
66    case Some{x} Some{l}:
67      Nat.is_ge(x, Nat.min(Nat.add(l, 300n), T.full()))
68    case o _:
69      False{}
70
71# Ordinary departure: dominance, headroom rise, or a sooner binding reset.
72def recov.ord(+h: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +lh: Maybe<&2, Nat>, +lr: Maybe<&2, Nat>, +peer: Maybe<&2, Nat>, +thr: Nat) -> Bool:
73  recov.dom(h, ah, thr) || recov.self(h, lh) || R.rec.lt_minus(peer, lr)
74
75def recov.pick(+isf: Bool, +h: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +lh: Maybe<&2, Nat>, +lr: Maybe<&2, Nat>, +peer: Maybe<&2, Nat>, +act: Maybe<&2, Nat>, +thr: Nat, +now: Nat) -> Bool:
76  match isf:
77    case True{}:
78      recov.fail(h, peer, act, thr, now)
79    case False{}:
80      recov.ord(h, ah, lh, lr, peer, thr)
81
82def recov.snap(+sn: T.Snap, +f: Nat, +current: Nat, +us: List<&2, T.Usage>, +ah: Maybe<&2, Nat>, +thr: Nat, +now: Nat, +ms: List<&2, String>) -> Bool:
83  match sn:
84    case T.NoSnap{}:
85      True{}
86    case T.Snap{lh, lr, ltr}:
87      recov.pick(snap.fail(ltr, lh, lr), U.head.row(U.usage.of(f, us), now, ms), ah, lh, lr, R.rec.row(U.usage.of(f, us), now, ms), R.rec.row(U.usage.of(current, us), now, ms), thr, now)
88
89# Is the account the engine left a better proposition than when it left it?
90# No record of the departure means release.
91def recovered(+st: T.State, +current: Nat, +us: List<&2, T.Usage>, +ah: Maybe<&2, Nat>, +thr: Nat, +now: Nat, +ms: List<&2, String>) -> Bool:
92  match st:
93    case T.State{la, lt, lf, sn}:
94      match lf:
95        case None{}:
96          True{}
97        case Some{f}:
98          recov.snap(sn, f, current, us, ah, thr, now, ms)
99
100# The bar lifts when the account we left beats us outright.
101def nr.release(+hb: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +thr: Nat) -> Bool:
102  match hb ah:
103    case None{} _:
104      False{}
105    case Some{l} Some{a}:
106      Nat.is_ge(l, Nat.mul(2n, a))
107    case Some{l} None{}:
108      Nat.is_gt(l, Nat.sub(T.full(), thr))
109
110def nr.rel(+rel: Bool, +f: Nat) -> Maybe<&2, Nat>:
111  match rel:
112    case True{}:
113      None{}
114    case False{}:
115      Some{f}
116
117def nr.rec(+rec: Bool, +f: Nat, +hb: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +thr: Nat) -> Maybe<&2, Nat>:
118  match rec:
119    case False{}:
120      Some{f}
121    case True{}:
122      nr.rel(nr.release(hb, ah, thr), f)
123
124# Only while the engine still stands where its switch put it.
125def landed_away(+lt: Maybe<&2, Nat>, +current: Nat) -> Bool:
126  match lt:
127    case None{}:
128      False{}
129    case Some{x}:
130      Bool.not(Nat.is_eq(x, current))
131
132def nr.landed(+away: Bool, +f: Nat, +rec: Bool, +hb: Maybe<&2, Nat>, +ah: Maybe<&2, Nat>, +thr: Nat) -> Maybe<&2, Nat>:
133  match away:
134    case True{}:
135      None{}
136    case False{}:
137      nr.rec(rec, f, hb, ah, thr)
138
139def nr.state(+st: T.State, +current: Nat, +rec: Bool, +us: List<&2, T.Usage>, +ah: Maybe<&2, Nat>, +thr: Nat, +now: Nat, +ms: List<&2, String>) -> Maybe<&2, Nat>:
140  match st:
141    case T.State{la, lt, lf, sn}:
142      match lf:
143        case None{}:
144          None{}
145        case Some{f}:
146          nr.landed(landed_away(lt, current), f, rec, U.head.row(U.usage.of(f, us), now, ms), ah, thr)
147
148# The account this engine most recently left, while it is still barred.
149# Proactive and consume-first triggers only: at-limit and failover escape.
150def no_return(+t: T.Trigger, +st: T.State, +current: Nat, +rec: Bool, +us: List<&2, T.Usage>, +ah: Maybe<&2, Nat>, +thr: Nat, +now: Nat, +ms: List<&2, String>) -> Maybe<&2, Nat>:
151  match t:
152    case T.Proactive{}:
153      nr.state(st, current, rec, us, ah, thr, now, ms)
154    case T.ConsumeFirstT{}:
155      nr.state(st, current, rec, us, ah, thr, now, ms)
156    case o:
157      None{}