1	# Quantified queue contracts. Heap ordering is an explicit input invariant;
2	# selection safety and cancellation/one-shot laws do not require it.
3	import Base
4	import bend-kit-collections@0.1.4.1/heap.bend as H
5	import ./queue.bend as Q
6	
7	# Ordinary & pairs are affine even when their fields are Data. Invariant
8	# conjunctions contain only evidence, so a Data constructor permits reuse.
9	type Both<-A: Data, -B: Data> is Data:
10	  Both{left: A, right: B}
11	
12	def state(-A: Data, r: Q.State<A> & Maybe<&2, Q.Ticket<A>>) -> Q.State<A>:
13	  (s, t) = r
14	  s
15	
16	def selected(-A: Data, r: Q.State<A> & Maybe<&2, Q.Ticket<A>>) -> Maybe<&2, Q.Ticket<A>>:
17	  (s, t) = r
18	  t
19	
20	def requeued(-A: Data, r: Q.State<A> & Bool) -> Bool:
21	  (s, b) = r
22	  b
23	
24	def enqueued(-A: Data, r: Q.State<A> & Nat) -> Q.State<A>:
25	  (s, i) = r
26	  s
27	
28	def assigned(-A: Data, r: Q.State<A> & Nat) -> Nat:
29	  (s, i) = r
30	  i
31	
32	# Reference semantics are deliberately simple; the live transition takes one
33	# pass and its equivalence is proved universally, including duplicate IDs.
34	def complete.reference(-A: Data, +i: Nat, s: Q.State<A>) -> Q.State<A> & Maybe<&2, Q.Ticket<A>>:
35	  match s:
36	    case Q.State{n, h, +r}:
37	      (Q.State{n, h, Q.remove.list(A, r, i)}, Q.find.list(A, r, i))
38	
39	def requeue.reference(~A: Data, i: Nat, d: Nat, s: Q.State<A>) -> Q.State<A> & Bool:
40	  Q.requeue.completed(~A, complete.reference(A, i, s), d)
41	
42	law take_equivalent:
43	  for -A: Data
44	  for +xs: List<&2, Q.Ticket<A>>
45	  for +i: Nat
46	  {Q.take.list(A, xs, i) == Q.Taken{Q.remove.list(A, xs, i), Q.find.list(A, xs, i)} : Q.Taken<A>}
47	
48	law complete_equivalent:
49	  for -A: Data
50	  for +i: Nat
51	  for +s: Q.State<A>
52	  {Q.complete(A, i, s) == complete.reference(A, i, s) : Q.State<A> & Maybe<&2, Q.Ticket<A>>}
53	
54	law requeue_equivalent:
55	  for ~A: Data
56	  for +i: Nat
57	  for d: Nat
58	  for +s: Q.State<A>
59	  {Q.requeue(~A, i, d, s) == requeue.reference(~A, i, d, s) : Q.State<A> & Bool}
60	
61	def absent.list(-A: Data, xs: List<&2, Q.Ticket<A>>, +i: Nat) -> Data:
62	  match xs:
63	    case Nil{}:
64	      Unit
65	    case Con{t, rest}:
66	      Both<{Nat.is_eq(Q.id(A, t), i) == False{} : Bool}, absent.list(A, rest, i)>
67	
68	def all.heap(-A: Data, -P: Q.Ticket<A> -> Data, h: H.Heap<Q.Ticket<A>>) -> Data:
69	  match h:
70	    case H.HLeaf{}:
71	      Unit
72	    case H.HNode{n, t, l, r}:
73	      Both<P(t), Both<all.heap(A, P, l), all.heap(A, P, r)>>
74	
75	def absent.ticket(-A: Data, i: Nat, t: Q.Ticket<A>) -> Data:
76	  {Nat.is_eq(Q.id(A, t), i) == False{} : Bool}
77	
78	def bound.ticket(-A: Data, lower: Q.Ticket<A>, t: Q.Ticket<A>) -> Data:
79	  {Q.le(A, lower, t) == True{} : Bool}
80	
81	def absent.heap(-A: Data, h: H.Heap<Q.Ticket<A>>, +i: Nat) -> Data:
82	  all.heap(A, absent.ticket(A, i), h)
83	
84	def below(-A: Data, h: H.Heap<Q.Ticket<A>>, +t: Q.Ticket<A>) -> Data:
85	  all.heap(A, bound.ticket(A, t), h)
86	
87	# The root must bound both subtrees recursively, not just its direct children.
88	# No law takes the desired selection result as an assumption.
89	# Cached sizes are a separate construction invariant of collections' heap:
90	# new/push/merge build them and remove.heap recomputes each retained size.
91	# ordered deliberately concerns ordering only. The order/absence merge lemmas
92	# hold even for malformed sizes; they do not claim element conservation for
93	# forged HNode values whose merge fuel can run out early.
94	def ordered(-A: Data, h: H.Heap<Q.Ticket<A>>) -> Data:
95	  match h:
96	    case H.HLeaf{}:
97	      Unit
98	    case H.HNode{n, +t, +l, +r}:
99	      Both<Both<below(A, l, t), below(A, r, t)>, Both<ordered(A, l), ordered(A, r)>>
100	
101	def due(-A: Data, t: Maybe<&2, Q.Ticket<A>>, now: Nat) -> Data:
102	  match t:
103	    case None{}:
104	      Unit
105	    case Some{t}:
106	      {Nat.is_le(Q.deadline(A, t), now) == True{} : Bool}
107	
108	def minimum(-A: Data, h: H.Heap<Q.Ticket<A>>, selected: Maybe<&2, Q.Ticket<A>>) -> Data:
109	  match selected:
110	    case None{}:
111	      Unit
112	    case Some{t}:
113	      below(A, h, t)
114	
115	law new_ordered:
116	  for -A: Data
117	  ordered(A, Q.pending(A, Q.new(A)))
118	
119	law select_due:
120	  for ~A: Data
121	  for now: Nat
122	  for s: Q.State<A>
123	  due(A, selected(A, Q.select(~A, now, s)), now)
124	
125	law select_minimum:
126	  for ~A: Data
127	  for now: Nat
128	  for +s: Q.State<A>
129	  for e: ordered(A, Q.pending(A, s))
130	  minimum(A, Q.pending(A, s), selected(A, Q.select(~A, now, s)))
131	
132	law equal_deadline_fifo:
133	  for -A: Data
134	  for i: Nat
135	  for j: Nat
136	  for d: Nat
137	  for x: A
138	  for y: A
139	  {Q.le(A, Q.Ticket{i, d, x}, Q.Ticket{j, d, y}) == Nat.is_le(i, j) : Bool}
140	
141	law enqueue_id:
142	  for ~A: Data
143	  for d: Nat
144	  for x: A
145	  for +s: Q.State<A>
146	  {Q.next_id(A, enqueued(A, Q.enqueue(~A, d, x, s))) == 1n+Q.next_id(A, s) : Nat}
147	
148	law cancel_pending_absent:
149	  for ~A: Data
150	  for i: Nat
151	  for s: Q.State<A>
152	  absent.heap(A, Q.pending(A, Q.cancel(~A, i, s)), i)
153	
154	law cancel_running_absent:
155	  for ~A: Data
156	  for i: Nat
157	  for s: Q.State<A>
158	  absent.list(A, Q.running(A, Q.cancel(~A, i, s)), i)
159	
160	law absent_find:
161	  for -A: Data
162	  for +xs: List<&2, Q.Ticket<A>>
163	  for +i: Nat
164	  for e: absent.list(A, xs, i)
165	  {Q.find.list(A, xs, i) == None{} : Maybe<&2, Q.Ticket<A>>}
166	
167	law complete_one_shot:
168	  for -A: Data
169	  for +i: Nat
170	  for s: Q.State<A>
171	  {selected(A, Q.complete(A, i, state(A, Q.complete(A, i, s)))) == None{} : Maybe<&2, Q.Ticket<A>>}
172	
173	law cancel_complete:
174	  for ~A: Data
175	  for +i: Nat
176	  for s: Q.State<A>
177	  {selected(A, Q.complete(A, i, Q.cancel(~A, i, s))) == None{} : Maybe<&2, Q.Ticket<A>>}
178	
179	law cancel_requeue:
180	  for ~A: Data
181	  for +i: Nat
182	  for d: Nat
183	  for s: Q.State<A>
184	  {requeued(A, Q.requeue(~A, i, d, Q.cancel(~A, i, s))) == False{} : Bool}
185	
186	law complete_requeue:
187	  for ~A: Data
188	  for +i: Nat
189	  for d: Nat
190	  for s: Q.State<A>
191	  {requeued(A, Q.requeue(~A, i, d, state(A, Q.complete(A, i, s)))) == False{} : Bool}
192	
193	# An absent ID stays absent on every selection, in both registries. Combined
194	# with cancellation above this covers any number of intervening selections.
195	law select_absent:
196	  for ~A: Data
197	  for now: Nat
198	  for +i: Nat
199	  for +s: Q.State<A>
200	  for eh: absent.heap(A, Q.pending(A, s), i)
201	  for er: absent.list(A, Q.running(A, s), i)
202	  absent.heap(A, Q.pending(A, state(A, Q.select(~A, now, s))), i) & absent.list(A, Q.running(A, state(A, Q.select(~A, now, s))), i)
203	
204	law absent_selected:
205	  for ~A: Data
206	  for now: Nat
207	  for +i: Nat
208	  for +s: Q.State<A>
209	  for eh: absent.heap(A, Q.pending(A, s), i)
210	  for t: Q.Ticket<A>
211	  for e: {selected(A, Q.select(~A, now, s)) == Some{t} : Maybe<&2, Q.Ticket<A>>}
212	  {Nat.is_eq(Q.id(A, t), i) == False{} : Bool}
213	
214	law enqueue_ordered:
215	  for ~A: Data
216	  for d: Nat
217	  for x: A
218	  for +s: Q.State<A>
219	  for e: ordered(A, Q.pending(A, s))
220	  ordered(A, Q.pending(A, enqueued(A, Q.enqueue(~A, d, x, s))))
221	
222	law select_ordered:
223	  for ~A: Data
224	  for now: Nat
225	  for +s: Q.State<A>
226	  for e: ordered(A, Q.pending(A, s))
227	  ordered(A, Q.pending(A, state(A, Q.select(~A, now, s))))
228	
229	law cancel_ordered:
230	  for ~A: Data
231	  for i: Nat
232	  for +s: Q.State<A>
233	  for e: ordered(A, Q.pending(A, s))
234	  ordered(A, Q.pending(A, Q.cancel(~A, i, s)))
235	
236	def requeue.state(-A: Data, r: Q.State<A> & Bool) -> Q.State<A>:
237	  (s, b) = r
238	  s
239	
240	law requeue_ordered:
241	  for ~A: Data
242	  for +i: Nat
243	  for d: Nat
244	  for +s: Q.State<A>
245	  for e: ordered(A, Q.pending(A, s))
246	  ordered(A, Q.pending(A, requeue.state(A, Q.requeue(~A, i, d, s))))
247	
248	law complete_ordered:
249	  for -A: Data
250	  for i: Nat
251	  for +s: Q.State<A>
252	  for e: ordered(A, Q.pending(A, s))
253	  ordered(A, Q.pending(A, state(A, Q.complete(A, i, s))))
254	
255	law enqueue_assigned_id:
256	  for ~A: Data
257	  for d: Nat
258	  for x: A
259	  for +s: Q.State<A>
260	  {assigned(A, Q.enqueue(~A, d, x, s)) == Q.next_id(A, s) : Nat}
261	
262	law cancel_keeps_counter:
263	  for ~A: Data
264	  for i: Nat
265	  for +s: Q.State<A>
266	  {Q.next_id(A, Q.cancel(~A, i, s)) == Q.next_id(A, s) : Nat}
267	
268	law complete_keeps_counter:
269	  for -A: Data
270	  for i: Nat
271	  for +s: Q.State<A>
272	  {Q.next_id(A, state(A, Q.complete(A, i, s))) == Q.next_id(A, s) : Nat}
273	
274	law select_keeps_counter:
275	  for ~A: Data
276	  for now: Nat
277	  for +s: Q.State<A>
278	  {Q.next_id(A, state(A, Q.select(~A, now, s))) == Q.next_id(A, s) : Nat}
279	
280	law requeue_keeps_counter:
281	  for ~A: Data
282	  for i: Nat
283	  for d: Nat
284	  for +s: Q.State<A>
285	  {Q.next_id(A, requeue.state(A, Q.requeue(~A, i, d, s))) == Q.next_id(A, s) : Nat}
286	
287	# The running token, not a newly assigned ID, is moved back to pending.
288	law requeue_token:
289	  for ~A: Data
290	  for +i: Nat
291	  for d: Nat
292	  for old: Nat
293	  for x: A
294	  for n: Nat
295	  for h: H.Heap<Q.Ticket<A>>
296	  for r: List<&2, Q.Ticket<A>>
297	  {Q.requeue(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r})
298	   == (Q.State{n, H.Heap.push(~Q.Ticket<A>, ~(a => b => Q.le(A, a, b)), Q.Ticket{i, d, x}, h), Q.remove.list(A, Q.Ticket{i, old, x} <> r, i)}, True{}) : Q.State<A> & Bool}
299	
300	law complete_token:
301	  for -A: Data
302	  for +i: Nat
303	  for old: Nat
304	  for x: A
305	  for n: Nat
306	  for h: H.Heap<Q.Ticket<A>>
307	  for r: List<&2, Q.Ticket<A>>
308	  {selected(A, Q.complete(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r}))
309	   == Some{Q.Ticket{i, old, x}} : Maybe<&2, Q.Ticket<A>>}