PROOF.bend
bend-kube-runtime@0.1.1.0 · 142 lines · 0 definitions
1import Base
2import bend-kube-runtime@0.1.1.0/LAWS.bend as Laws
3import bend-kube-runtime@0.1.1.0/src/queue.bend as Q
4
5# PROOF
6# =====
7#
8# A proof of every law in LAWS.bend. `bend PROOF.bend` must print
9# ALL PROOFS CHECK before a commit.
10
11def Laws.watch_gone_relists(rv, f, first, r, m):
12 {==}
13
14def Laws.watch_request_gone_relists(rv, f, first):
15 {==}
16
17def Laws.list_gone_relists(c, f, first):
18 {==}
19
20def Laws.watch_error_backs_off(rv, f, first):
21 {==}
22
23def Laws.watch_end_resumes(rv, f, first):
24 {==}
25
26def Laws.bookmark_advances(rv, v, f, first):
27 {==}
28
29def Laws.last_page_watches(c, f, first, items, rv):
30 {==}
31
32def Laws.first_page_inits(items):
33 {==}
34
35def Laws.watch_backoff_capped():
36 {==}
37
38def Laws.init_clears_buffer(objs, buf, r):
39 {==}
40
41def Laws.init_done_swaps(objs, buf, r):
42 {==}
43
44def Laws.retry_backoff_capped():
45 {==}
46
47# The hypothesis rewrites the running test to True; the rest computes.
48def Laws.add_running_marks_dirty(f, b, inq, run, d, g, fl, n, mx, key, running):
49 %Equal.sym(Bool, Q.Mp.has(run, key), True{}, running) :
50 {Q.Queue.add.go(f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx, key, _, Q.Mp.has(inq, key))
51 == Q.Queue{f, b, inq, run, Q.Mp.on(d, key), Q.Mp.bump(g, key), fl, n, mx} : Q.Queue}
52 {==}
53
54def Laws.add_waiting_dedups(f, b, inq, run, d, g, fl, n, mx, key, idle, waiting):
55 %Equal.sym(Bool, Q.Mp.has(run, key), False{}, idle) :
56 {Q.Queue.add.go(f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx, key, _, Q.Mp.has(inq, key))
57 == Q.Queue{f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx} : Q.Queue}
58 %Equal.sym(Bool, Q.Mp.has(inq, key), True{}, waiting) :
59 {Q.Queue.add.go(f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx, key, False{}, _)
60 == Q.Queue{f, b, inq, run, d, Q.Mp.bump(g, key), fl, n, mx} : Q.Queue}
61 {==}
62
63# With no free slot, pop.go answers None whatever the front holds.
64def Proof.pop_full(f: List<&2, String>, b: List<&2, String>, inq: Map<&2, U32>,
65 run: Map<&2, U32>, d: Map<&2, U32>, g: Map<&2, U32>, fl: Map<&2, U32>, n: U32, mx: U32) ->
66 {Q.Queue.pop.go(f, b, inq, run, d, g, fl, n, mx, False{})
67 == (Q.Queue{f, b, inq, run, d, g, fl, n, mx}, None{}) : Q.Queue & Maybe<&2, String>}:
68 match f:
69 case Nil{}:
70 {==}
71 case Con{h, t}:
72 {==}
73
74def Laws.pop_respects_limit(f, b, inq, run, d, g, fl, n, mx, full):
75 %Equal.sym(Bool, U32.is_lt(n, mx), False{}, full) :
76 {Q.Queue.pop.go(f, b, inq, run, d, g, fl, n, mx, _)
77 == (Q.Queue{f, b, inq, run, d, g, fl, n, mx}, None{}) : Q.Queue & Maybe<&2, String>}
78 Proof.pop_full(f, b, inq, run, d, g, fl, n, mx)
79
80def Laws.done_idle_noop(q, key, a, idle):
81 %Equal.sym(Bool, Q.Queue.running(q, key), False{}, idle) :
82 {Q.Queue.done.go(q, key, a, _) == (q, Nil{}) : Q.Queue & List<&2, Q.Timer>}
83 {==}
84
85# A busy key leaves any queue as it is.
86def Proof.forget_busy(q: Q.Queue, key: String) -> {Q.Queue.forget.go(q, key, True{}) == q : Q.Queue}:
87 match q:
88 case Q.Queue{f, b, i, r, d, g, fl, n, mx}:
89 {==}
90
91def Laws.forget_running_keeps(q, key, running):
92 %Equal.sym(Bool, Q.Queue.running(q, key), True{}, running) :
93 {Q.Queue.forget.go(q, key, Bool.or(_, Q.Queue.waiting(q, key))) == q : Q.Queue}
94 Proof.forget_busy(q, key)
95
96def Laws.fin_live_applies(fs, name, i):
97 {==}
98
99def Laws.fin_gone_done(fs, name):
100 {==}
101
102def Laws.fin_cleanup_tests(fs, name, i):
103 {==}
104
105def Laws.eof_before_response_is_lost(t, h, o):
106 {==}
107
108def Laws.eof_mid_response_is_broken(b, bs, t, h, o):
109 {==}
110
111def Laws.proxy_skips_localhost(url, no, port):
112 {==}
113
114def Laws.proxy_skips_loopback(url, no, port):
115 {==}
116
117def Laws.no_proxy_star_bypasses(url, port):
118 {==}
119
120def Laws.no_proxy_url_is_direct(port):
121 {==}
122
123def Laws.unsupported_proxy_fails(port):
124 {==}
125
126def Laws.no_proxy_dot_is_subdomains_only():
127 {==}
128
129def Laws.no_proxy_respects_labels():
130 {==}
131
132def Laws.no_proxy_port_narrows():
133 {==}
134
135def Laws.tunnel_needs_200():
136 {==}
137
138def Laws.tunnel_rejects_early_bytes(b, bs):
139 {==}
140
141def Laws.tunnel_end_before_answer(h):
142 {==}