1	# Retry policy: a shared attempt budget, an operation deadline, bounded backoff, and a circuit breaker.
2	# All times are ms on one monotonic clock. The caller reads the clock; these defs are pure.
3	import Base
4	
5	# left: attempts the whole operation may still start, the first one included. Nested layers share one Budget.
6	# deadline: no attempt starts at or after this time. None: no deadline.
7	type Budget is Data:
8	  Budget{left: Nat, deadline: Maybe<&2, Nat>}
9	
10	type Deny is Data:
11	  DenyLate{}
12	  DenySpent{}
13	  DenyOpen{}
14	
15	type Gate is Data:
16	  GateGo{}
17	  GateNo{why: Deny}
18	
19	# threshold: failures in a row, each inside window ms of the newest, that open the circuit. cooldown: ms it stays open.
20	# probes: attempts allowed at once while half-open.
21	type Circuit is Data:
22	  Circuit{threshold: Nat, window: Nat, cooldown: Nat, probes: Nat}
23	
24	# Closed: the failures since the last success that are still inside the window, newest first.
25	# Open: no attempt before until. Half: probes in flight.
26	type State is Data:
27	  CircuitClosed{fails: List<&2, Nat>}
28	  CircuitOpen{until: Nat}
29	  CircuitHalf{busy: Nat}
30	
31	type Breaker is Data:
32	  BreakerOff{}
33	  BreakerOn{circuit: Circuit, state: State}
34	
35	# Settled: a success. Failed: a failure that another try would repeat. Unsafe: a transient failure of a
36	# request that must not repeat. Transient: another try can help; after is the server's wait in ms.
37	type Outcome is Data:
38	  Settled{}
39	  Failed{}
40	  Unsafe{}
41	  Transient{after: Maybe<&2, Nat>}
42	
43	# attempts: tries in one layer, the first one included. base: the first backoff in ms. cap: the longest wait in ms.
44	# deadline: ms from the start of the operation to its deadline. None: no deadline.
45	type Policy is Data:
46	  Policy{attempts: Nat, base: Nat, cap: U32, deadline: Maybe<&2, Nat>}
47	
48	type Plan is Data:
49	  PlanStop{}
50	  PlanWait{ms: Nat}
51	
52	# ---- budget
53	
54	def Budget.new(+attempts: Nat, +now: Nat, ms: Maybe<&2, Nat>) -> Budget:
55	  match ms:
56	    case None{}:
57	      Budget{attempts, None{}}
58	    case Some{m}:
59	      Budget{attempts, Some{Nat.add(now, m)}}
60	
61	def Budget.late(+now: Nat, d: Maybe<&2, Nat>) -> Bool:
62	  match d:
63	    case None{}:
64	      False{}
65	    case Some{t}:
66	      Nat.is_le(t, now)
67	
68	# ---- circuit
69	
70	# The failure times still inside the window: now < t + window. Newest first, so the first old time ends the list.
71	def prune(+now: Nat, +window: Nat, fs: List<&2, Nat>) -> List<&2, Nat>:
72	  match fs:
73	    case Nil{}:
74	      Nil{}
75	    case Con{+t, rest}:
76	      Bool.pick(List<&2, Nat>, Nat.is_lt(now, Nat.add(t, window)), Con{t, prune(now, window, rest)}, Nil{})
77	
78	def Circuit.probes(c: Circuit) -> Nat:
79	  Circuit{t, w, cd, p} = c
80	  p
81	
82	def Circuit.cooldown(c: Circuit) -> Nat:
83	  Circuit{t, w, cd, p} = c
84	  cd
85	
86	def half.admit(go: Bool, +k: Nat) -> State & Bool:
87	  match go:
88	    case True{}:
89	      (CircuitHalf{1n+k}, True{})
90	    case False{}:
91	      (CircuitHalf{k}, False{})
92	
93	def open.admit(early: Bool, +p: Nat, +u: Nat) -> State & Bool:
94	  match early:
95	    case True{}:
96	      (CircuitOpen{u}, False{})
97	    case False{}:
98	      half.admit(Nat.is_lt(0n, p), 0n)
99	
100	# Closed admits. Open admits nothing before until; at or after until it turns half-open and admits a probe.
101	# Half-open admits while fewer than probes are in flight.
102	def State.admit(+c: Circuit, s: State, +now: Nat) -> State & Bool:
103	  match s:
104	    case CircuitClosed{fs}:
105	      (CircuitClosed{fs}, True{})
106	    case CircuitOpen{+u}:
107	      open.admit(Nat.is_lt(now, u), Circuit.probes(c), u)
108	    case CircuitHalf{+k}:
109	      half.admit(Nat.is_lt(k, Circuit.probes(c)), k)
110	
111	def closed.trip(under: Bool, fs: List<&2, Nat>, +until: Nat) -> State:
112	  match under:
113	    case True{}:
114	      CircuitClosed{fs}
115	    case False{}:
116	      CircuitOpen{until}
117	
118	def closed.fail(+c: Circuit, fs: List<&2, Nat>, +now: Nat) -> State:
119	  Circuit{+t, +w, +cd, p} = c
120	  +kept = {Con{now, prune(now, w, fs)} : List<&2, Nat>}
121	  closed.trip(Nat.is_lt(List.length(&2, Nat, kept), t), kept, Nat.add(now, cd))
122	
123	# A closed success clears the failures. A closed failure opens the circuit when the window then holds threshold
124	# failures. A half-open success closes it; a half-open failure opens it again for cooldown. An attempt that ends
125	# while open changes nothing.
126	def State.done(+c: Circuit, s: State, +now: Nat, failed: Bool) -> State:
127	  match s:
128	    case CircuitClosed{fs}:
129	      match failed:
130	        case False{}:
131	          CircuitClosed{Nil{}}
132	        case True{}:
133	          closed.fail(c, fs, now)
134	    case CircuitOpen{u}:
135	      CircuitOpen{u}
136	    case CircuitHalf{k}:
137	      match failed:
138	        case False{}:
139	          CircuitClosed{Nil{}}
140	        case True{}:
141	          CircuitOpen{Nat.add(now, Circuit.cooldown(c))}
142	
143	def Breaker.new(c: Circuit) -> Breaker:
144	  BreakerOn{c, CircuitClosed{Nil{}}}
145	
146	def Breaker.on(+c: Circuit, x: State & Bool) -> Breaker & Bool:
147	  (s, ok) = x
148	  (BreakerOn{c, s}, ok)
149	
150	def Breaker.admit(br: Breaker, +now: Nat) -> Breaker & Bool:
151	  match br:
152	    case BreakerOff{}:
153	      (BreakerOff{}, True{})
154	    case BreakerOn{+c, s}:
155	      Breaker.on(c, State.admit(c, s, now))
156	
157	def Breaker.done(br: Breaker, +now: Nat, failed: Bool) -> Breaker:
158	  match br:
159	    case BreakerOff{}:
160	      BreakerOff{}
161	    case BreakerOn{+c, s}:
162	      BreakerOn{c, State.done(c, s, now, failed)}
163	
164	# ---- admission
165	
166	def admit.ok(ok: Bool, br: Breaker, +p: Nat, d: Maybe<&2, Nat>) -> Breaker & Budget & Gate:
167	  match ok:
168	    case True{}:
169	      (br, Budget{p, d}, GateGo{})
170	    case False{}:
171	      (br, Budget{1n+p, d}, GateNo{DenyOpen{}})
172	
173	def admit.breaker(x: Breaker & Bool, +p: Nat, d: Maybe<&2, Nat>) -> Breaker & Budget & Gate:
174	  (br, ok) = x
175	  admit.ok(ok, br, p, d)
176	
177	def admit.late(late: Bool, br: Breaker, left: Nat, d: Maybe<&2, Nat>, +now: Nat) -> Breaker & Budget & Gate:
178	  match late:
179	    case True{}:
180	      (br, Budget{left, d}, GateNo{DenyLate{}})
181	    case False{}:
182	      match left:
183	        case 0n:
184	          (br, Budget{0n, d}, GateNo{DenySpent{}})
185	        case 1n+p:
186	          admit.breaker(Breaker.admit(br, now), p, d)
187	
188	# Ask to start one attempt at now. The deadline is checked first, then the budget, then the breaker.
189	# Only GateGo takes one attempt from the budget.
190	def admit(br: Breaker, b: Budget, +now: Nat) -> Breaker & Budget & Gate:
191	  Budget{left, +d} = b
192	  admit.late(Budget.late(now, d), br, left, d, now)
193	
194	# ---- backoff
195	
196	# min(cap, base * 2^n), doubled one step at a time, so no step passes cap.
197	def delay(n: Nat, +base: Nat, +cap: Nat) -> Nat:
198	  match n:
199	    case 0n:
200	      Nat.min(base, cap)
201	    case 1n+p:
202	      +d = delay(p, base, cap)
203	      Nat.min(Nat.add(d, d), cap)
204	
205	# Equal jitter: d / 2, plus r mod (d / 2 + 1). The wait is in [d / 2, d] for every r.
206	def jitter(+d: Nat, +r: Nat) -> Nat:
207	  +h = Nat.div(d, 2n)
208	  Nat.add(h, Nat.mod(r, 1n+h))
209	
210	# The wait before retry n (0 first): the server's wait when it gave one, else the jittered backoff. At most cap.
211	def wait(after: Maybe<&2, Nat>, p: Policy, +n: Nat, +r: Nat) -> Nat:
212	  match after:
213	    case None{}:
214	      Policy{a, +base, +cap, d} = p
215	      jitter(delay(n, base, U32.to_nat(cap)), r)
216	    case Some{+ms}:
217	      Policy{a, base, +cap, d} = p
218	      Nat.min(ms, U32.to_nat(cap))
219	
220	def plan.left(left: Nat, +w: Nat, d: Maybe<&2, Nat>, +now: Nat) -> Plan:
221	  match left:
222	    case 0n:
223	      PlanStop{}
224	    case 1n+k:
225	      Bool.pick(Plan, Budget.late(Nat.add(now, w), d), PlanStop{}, PlanWait{w})
226	
227	def plan.at(+w: Nat, b: Budget, +now: Nat) -> Plan:
228	  Budget{left, d} = b
229	  plan.left(left, w, d, now)
230	
231	# After an attempt ends at now: stop, or wait ms and then ask admit again. Settled, Failed, and Unsafe always stop.
232	# A transient outcome stops when the budget is spent or the wait would reach the deadline.
233	def plan(o: Outcome, p: Policy, b: Budget, +n: Nat, +now: Nat, +r: Nat) -> Plan:
234	  match o:
235	    case Settled{}:
236	      PlanStop{}
237	    case Failed{}:
238	      PlanStop{}
239	    case Unsafe{}:
240	      PlanStop{}
241	    case Transient{after}:
242	      plan.at(wait(after, p, n, r), b, now)
243	
244	# Failed, Unsafe, and Transient count as failures for the breaker.
245	def failed(o: Outcome) -> Bool:
246	  match o:
247	    case Settled{}:
248	      False{}
249	    case Failed{}:
250	      True{}
251	    case Unsafe{}:
252	      True{}
253	    case Transient{after}:
254	      True{}