1	import Base
2	import ./types.bend as T
3	import ./usage.bend as U
4	import ./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	
11	def is_none(+m: Maybe<&2, Nat>) -> Bool:
12	  match m:
13	    case None{}:
14	      True{}
15	    case Some{x}:
16	      False{}
17	
18	def 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.
26	def 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?
34	def 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	
41	def 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.
50	def 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.
54	def 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.
64	def 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.
72	def 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	
75	def 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	
82	def 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.
91	def 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.
101	def 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	
110	def nr.rel(+rel: Bool, +f: Nat) -> Maybe<&2, Nat>:
111	  match rel:
112	    case True{}:
113	      None{}
114	    case False{}:
115	      Some{f}
116	
117	def 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.
125	def 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	
132	def 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	
139	def 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.
150	def 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{}