1	import Base
2	import ./src/json.bend as J
3	import ./src/core.bend as C
4	import ./src/watcher.bend as W
5	import ./src/store.bend as S
6	import ./src/queue.bend as Q
7	import ./src/finalizer.bend as F
8	import ./src/http.bend as H
9	import ./src/utf8.bend as U
10	import ./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.
23	law 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.
33	law 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.
41	law 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.
50	law 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.
59	law 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.
67	law 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.
77	law 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.
88	law 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.
94	law 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.
101	law 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.
110	law 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.
122	law 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.
138	law 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.
155	law 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.
170	law 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.
174	law 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.
182	law 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.
192	law 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.
199	law 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.
206	law 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.
217	law 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.
225	law 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.
239	law 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	
245	law 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.
252	law 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.
258	law 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.
264	law 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.
270	law 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.
276	law 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.
281	law 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.
286	law 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.
293	law 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.
301	law 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}