1	import Base
2	import ./LAWS.bend as Laws
3	import ./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	
11	def Laws.watch_gone_relists(rv, f, first, r, m):
12	  {==}
13	
14	def Laws.watch_request_gone_relists(rv, f, first):
15	  {==}
16	
17	def Laws.list_gone_relists(c, f, first):
18	  {==}
19	
20	def Laws.watch_error_backs_off(rv, f, first):
21	  {==}
22	
23	def Laws.watch_end_resumes(rv, f, first):
24	  {==}
25	
26	def Laws.bookmark_advances(rv, v, f, first):
27	  {==}
28	
29	def Laws.last_page_watches(c, f, first, items, rv):
30	  {==}
31	
32	def Laws.first_page_inits(items):
33	  {==}
34	
35	def Laws.watch_backoff_capped():
36	  {==}
37	
38	def Laws.init_clears_buffer(objs, buf, r):
39	  {==}
40	
41	def Laws.init_done_swaps(objs, buf, r):
42	  {==}
43	
44	def Laws.retry_backoff_capped():
45	  {==}
46	
47	# The hypothesis rewrites the running test to True; the rest computes.
48	def 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	
54	def 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.
64	def 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	
74	def 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	
80	def 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.
86	def 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	
91	def 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	
96	def Laws.fin_live_applies(fs, name, i):
97	  {==}
98	
99	def Laws.fin_gone_done(fs, name):
100	  {==}
101	
102	def Laws.fin_cleanup_tests(fs, name, i):
103	  {==}
104	
105	def Laws.eof_before_response_is_lost(t, h, o):
106	  {==}
107	
108	def Laws.eof_mid_response_is_broken(b, bs, t, h, o):
109	  {==}
110	
111	def Laws.proxy_skips_localhost(url, no, port):
112	  {==}
113	
114	def Laws.proxy_skips_loopback(url, no, port):
115	  {==}
116	
117	def Laws.no_proxy_star_bypasses(url, port):
118	  {==}
119	
120	def Laws.no_proxy_url_is_direct(port):
121	  {==}
122	
123	def Laws.unsupported_proxy_fails(port):
124	  {==}
125	
126	def Laws.no_proxy_dot_is_subdomains_only():
127	  {==}
128	
129	def Laws.no_proxy_respects_labels():
130	  {==}
131	
132	def Laws.no_proxy_port_narrows():
133	  {==}
134	
135	def Laws.tunnel_needs_200():
136	  {==}
137	
138	def Laws.tunnel_rejects_early_bytes(b, bs):
139	  {==}
140	
141	def Laws.tunnel_end_before_answer(h):
142	  {==}