LAWS.bend
bend-kube-runtime@0.1.1.0 · 304 lines · 0 definitions
1import Base
2import bend-kube-runtime@0.1.1.0/src/json.bend as J
3import bend-kube-runtime@0.1.1.0/src/core.bend as C
4import bend-kube-runtime@0.1.1.0/src/watcher.bend as W
5import bend-kube-runtime@0.1.1.0/src/store.bend as S
6import bend-kube-runtime@0.1.1.0/src/queue.bend as Q
7import bend-kube-runtime@0.1.1.0/src/finalizer.bend as F
8import bend-kube-runtime@0.1.1.0/src/http.bend as H
9import bend-kube-runtime@0.1.1.0/src/utf8.bend as U
10import bend-kube-runtime@0.1.1.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}