~/jendhub

LAWS.bend

bend-kube-runtime@0.2.0.0 · 304 lines · 33 definitions

1import Base
2import bend-kube-runtime@0.2.0.0/src/json.bend as J
3import bend-kube-runtime@0.2.0.0/src/core.bend as C
4import bend-kube-runtime@0.2.0.0/src/watcher.bend as W
5import bend-kube-runtime@0.2.0.0/src/store.bend as S
6import bend-kube-runtime@0.2.0.0/src/queue.bend as Q
7import bend-kube-runtime@0.2.0.0/src/finalizer.bend as F
8import bend-kube-runtime@0.2.0.0/src/http.bend as H
9import bend-kube-runtime@0.2.0.0/src/utf8.bend as U
10import bend-kube-runtime@0.2.0.0/src/proxy.bend as P
11
12# LAWS
13# ====
14#
15# The rules bend-kube must keep, stated over its pure state machines. They
16# are how client-go and kube-runtime say the API behaves; PROOF.bend proves
17# each one. Humans own this file: change a law only on purpose.
18
19# Watcher (client-go's reflector)
20# -------------------------------
21
22# A watch that answers 410 Gone relists from scratch, at once.
23law watch_gone_relists:
24  for rv: String
25  for f: U32
26  for first: Bool
27  for r: String
28  for m: String
29  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IEvent{C.WError{C.Status{410, r, m}}})
30    == W.Step{W.WState{W.WList{""}, f, True{}}, Nil{}, False{}} : W.Step}
31
32# So does a watch request the server refuses with 410.
33law watch_request_gone_relists:
34  for rv: String
35  for f: U32
36  for first: Bool
37  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IWatchErr{410})
38    == W.Step{W.WState{W.WList{""}, f, True{}}, Nil{}, False{}} : W.Step}
39
40# An expired continue token restarts the list from its first page.
41law list_gone_relists:
42  for c: String
43  for f: U32
44  for first: Bool
45  {W.Watcher.step(W.WState{W.WList{c}, f, first}, W.IListErr{410})
46    == W.Step{W.WState{W.WList{""}, f, True{}}, Nil{}, False{}} : W.Step}
47
48# A failed watch request (not 410) retries from the same version after a
49# backoff, counting the failure.
50law watch_error_backs_off:
51  for rv: String
52  for f: U32
53  for first: Bool
54  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IWatchErr{500})
55    == W.Step{W.WState{W.WWatch{rv}, (f + 1 : U32), False{}}, Nil{}, True{}} : W.Step}
56
57# A watch that ends (the server's timeout) resumes from the same version,
58# with no backoff and no events.
59law watch_end_resumes:
60  for rv: String
61  for f: U32
62  for first: Bool
63  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IWatchEnd{})
64    == W.Step{W.WState{W.WWatch{rv}, 0, False{}}, Nil{}, False{}} : W.Step}
65
66# A bookmark moves the resume version and emits nothing.
67law bookmark_advances:
68  for rv: String
69  for v: String
70  for f: U32
71  for first: Bool
72  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IEvent{C.WBookmark{v}})
73    == W.Step{W.WState{W.WWatch{v}, 0, False{}}, Nil{}, False{}} : W.Step}
74
75# The last page of a list (no continue token) emits its objects, closes
76# the relist with InitDone, and starts watching from the list's version.
77law last_page_watches:
78  for c: String
79  for f: U32
80  for first: Bool
81  for items: List<&2, J.Json>
82  for rv: String
83  {W.Watcher.step(W.WState{W.WList{c}, f, first}, W.IPage{C.Page{items, rv, ""}})
84    == W.Step{W.WState{W.WWatch{rv}, 0, True{}},
85      W.Watcher.init_out(first, W.Watcher.page_outs(items, [W.OInitDone{}])), False{}} : W.Step}
86
87# The first page of a relist opens it with Init.
88law first_page_inits:
89  for items: List<&2, J.Json>
90  {W.Watcher.init_out(True{}, W.Watcher.page_outs(items, Nil{}))
91    == W.OInit{} <> W.Watcher.page_outs(items, Nil{}) : List<&2, W.Out>}
92
93# The watcher's backoff never exceeds 30s, however many failures.
94law watch_backoff_capped:
95  {W.Backoff.delay(6) == 30000 : U32}
96
97# Store (kube-runtime's reflector)
98# --------------------------------
99
100# A relist starts from an empty buffer, whatever the store held.
101law init_clears_buffer:
102  for objs: Map<&2, J.Json>
103  for buf: Map<&2, J.Json>
104  for r: Bool
105  {S.Store.apply(S.Store{objs, buf, r}, W.OInit{})
106    == S.Store{objs, Map.new(&2, J.Json), r} : S.Store}
107
108# InitDone swaps the relisted buffer in whole: objects absent from the
109# relist leave the store, and the store is ready.
110law init_done_swaps:
111  for objs: Map<&2, J.Json>
112  for buf: Map<&2, J.Json>
113  for r: Bool
114  {S.Store.apply(S.Store{objs, buf, r}, W.OInitDone{})
115    == S.Store{buf, Map.new(&2, J.Json), True{}} : S.Store}
116
117# Queue (client-go's workqueue)
118# -----------------------------
119
120# Adding a key that is running does not queue it a second time: it is
121# marked dirty, to run again when the current run ends.
122law add_running_marks_dirty:
123  for f: List<&2, String>
124  for b: List<&2, String>
125  for inq: Map<&2, U32>
126  for run: Map<&2, U32>
127  for d: Map<&2, U32>
128  for g: Map<&2, U32>
129  for fl: Map<&2, U32>
130  for n: U32
131  for mx: U32
132  for key: String
133  for running: {Q.Mp.has(run, key) == True{} : Bool}
134  {Q.Queue.add(Q.Queue{f, b, inq, run, d, g, fl, n, mx}, key)
135    == Q.Queue{f, b, inq, run, Q.Mp.on(d, key), Q.Mp.bump(g, key), fl, n, mx} : Q.Queue}
136
137# Adding a key that already waits changes nothing but its timer.
138law add_waiting_dedups:
139  for f: List<&2, String>
140  for b: List<&2, String>
141  for inq: Map<&2, U32>
142  for run: Map<&2, U32>
143  for d: Map<&2, U32>
144  for g: Map<&2, U32>
145  for fl: Map<&2, U32>
146  for n: U32
147  for mx: U32
148  for key: String
149  for idle: {Q.Mp.has(run, key) == False{} : Bool}
150  for waiting: {Q.Mp.has(inq, key) == True{} : Bool}
151  {Q.Queue.add(Q.Queue{f, b, inq, run, d, g, fl, n, mx}, key)
152    == Q.Queue{f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx} : Q.Queue}
153
154# No key starts while every worker slot is taken.
155law pop_respects_limit:
156  for f: List<&2, String>
157  for b: List<&2, String>
158  for inq: Map<&2, U32>
159  for run: Map<&2, U32>
160  for d: Map<&2, U32>
161  for g: Map<&2, U32>
162  for fl: Map<&2, U32>
163  for n: U32
164  for mx: U32
165  for full: {U32.is_lt(n, mx) == False{} : Bool}
166  {Q.Queue.pop(Q.Queue{f, b, inq, run, d, g, fl, n, mx})
167    == (Q.Queue{f, b, inq, run, d, g, fl, n, mx}, None{}) : Q.Queue & Maybe<&2, String>}
168
169# A failing key backs off for at most 1000s.
170law retry_backoff_capped:
171  {Q.Queue.backoff(18) == 1000000 : U32}
172
173# Finishing a key that is not running changes nothing and arms no timer.
174law done_idle_noop:
175  for q: Q.Queue
176  for key: String
177  for a: Q.Action
178  for idle: {Q.Queue.running(q, key) == False{} : Bool}
179  {Q.Queue.done(q, key, a) == (q, Nil{}) : Q.Queue & List<&2, Q.Timer>}
180
181# Forgetting never disturbs a key that is running.
182law forget_running_keeps:
183  for q: Q.Queue
184  for key: String
185  for running: {Q.Queue.running(q, key) == True{} : Bool}
186  {Q.Queue.forget(q, key) == q : Q.Queue}
187
188# Finalizers (kube-runtime's finalizer)
189# -------------------------------------
190
191# A live object that carries our finalizer is applied.
192law fin_live_applies:
193  for fs: List<&2, String>
194  for name: String
195  for i: U32
196  {F.Fin.state.go(fs, name, Some{i}, False{}) == F.FApply{} : F.FState}
197
198# A deleted object that no longer carries it needs nothing more.
199law fin_gone_done:
200  for fs: List<&2, String>
201  for name: String
202  {F.Fin.state.go(fs, name, None{}, True{}) == F.FDone{} : F.FState}
203
204# A deleted object that still carries it is cleaned up, and the finalizer
205# is removed only through a patch that tests it is still ours, at its index.
206law fin_cleanup_tests:
207  for fs: List<&2, String>
208  for name: String
209  for i: U32
210  {F.Fin.state.go(fs, name, Some{i}, True{}) == F.FCleanup{F.Fin.remove_patch(i, name)} : F.FState}
211
212# HTTP (the keep-alive pool's retry rule)
213# ---------------------------------------
214
215# A connection that ends before any byte of a response is lost, not broken:
216# only then may a request on a reused connection be retried.
217law eof_before_response_is_lost:
218  for t: U32
219  for h: Maybe<&2, H.Head>
220  for o: List<&2, U32>
221  {H.Http.eof(H.Resp{H.PHead{Nil{}, t}, h, o})
222    == H.Resp{H.PLost{"connection closed before a response"}, h, o} : H.Resp}
223
224# Bytes of a response make an early end a broken response, never retried.
225law eof_mid_response_is_broken:
226  for b: U32
227  for bs: List<&2, U32>
228  for t: U32
229  for h: Maybe<&2, H.Head>
230  for o: List<&2, U32>
231  {H.Http.eof(H.Resp{H.PHead{b <> bs, t}, h, o})
232    == H.Resp{H.PErr{"connection closed mid-response"}, h, o} : H.Resp}
233
234# Proxies (Go's ProxyFromEnvironment, as client-go uses it)
235# ---------------------------------------------------------
236
237# localhost and loopback addresses never go through a proxy, whatever
238# HTTPS_PROXY and NO_PROXY say.
239law proxy_skips_localhost:
240  for url: String
241  for no: String
242  for port: U32
243  {P.Proxy.route(url, no, "localhost", port) == P.Direct{} : P.Route}
244
245law proxy_skips_loopback:
246  for url: String
247  for no: String
248  for port: U32
249  {P.Proxy.route(url, no, "127.0.0.1", port) == P.Direct{} : P.Route}
250
251# NO_PROXY=* sends every host around the proxy.
252law no_proxy_star_bypasses:
253  for url: String
254  for port: U32
255  {P.Proxy.route(url, "*", "api.example.com", port) == P.Direct{} : P.Route}
256
257# Without HTTPS_PROXY, connections are direct.
258law no_proxy_url_is_direct:
259  for port: U32
260  {P.Proxy.route("", "", "api.example.com", port) == P.Direct{} : P.Route}
261
262# A proxy bend-kube cannot speak fails the connection: it never falls back
263# to connecting directly.
264law unsupported_proxy_fails:
265  for port: U32
266  {P.Proxy.route("socks5://proxy:1080", "", "api.example.com", port)
267    == P.NoRoute{"HTTPS_PROXY: only http:// proxies are supported"} : P.Route}
268
269# ".corp" bypasses the subdomains of corp, not corp itself.
270law no_proxy_dot_is_subdomains_only:
271  {P.Proxy.route("http://proxy:3128", ".corp", "corp", 443)
272    == P.Via{P.Proxy{"proxy", 3128, ""}} : P.Route}
273
274# "corp" bypasses corp and its subdomains, never a name that merely ends
275# in the same letters.
276law no_proxy_respects_labels:
277  {P.Proxy.route("http://proxy:3128", "corp", "evilcorp", 443)
278    == P.Via{P.Proxy{"proxy", 3128, ""}} : P.Route}
279
280# An entry with a port bypasses only that port.
281law no_proxy_port_narrows:
282  {P.Proxy.route("http://proxy:3128", "api.corp:6443", "api.corp", 443)
283    == P.Via{P.Proxy{"proxy", 3128, ""}} : P.Route}
284
285# Only a 200 opens the tunnel; any other answer fails it, quoted.
286law tunnel_needs_200:
287  {P.Tunnel.feed(P.Tunnel.init(),
288    U.Utf8.encode("HTTP/1.1 407 Proxy Authentication Required\r\n\r\n"))
289    == P.TFail{"proxy refused CONNECT: HTTP/1.1 407 Proxy Authentication Required"} : P.Tunnel}
290
291# Bytes after the proxy's answer, before we spoke TLS, fail the tunnel:
292# nothing the proxy says may become part of the TLS stream.
293law tunnel_rejects_early_bytes:
294  for b: U32
295  for bs: List<&2, U32>
296  {P.Tunnel.feed(P.Tunnel.init(),
297    List.append(&2, U32, U.Utf8.encode("HTTP/1.1 200 OK\r\n\r\n"), b <> bs))
298    == P.TFail{"proxy sent bytes before the TLS handshake"} : P.Tunnel}
299
300# A proxy that hangs up before its answer is whole fails the tunnel.
301law tunnel_end_before_answer:
302  for h: List<&2, U32>
303  {P.Tunnel.feed(P.TMore{h}, Nil{})
304    == P.TFail{"proxy closed the connection before answering CONNECT"} : P.Tunnel}