queue_laws.bend

bend-kit-scheduler@0.4.1.0 · 309 lines · 47 definitions

1# Quantified queue contracts. Heap ordering is an explicit input invariant;
2# selection safety and cancellation/one-shot laws do not require it.
3import Base
4import bend-kit-collections@0.1.4.1/heap.bend as H
5import bend-kit-scheduler@0.4.1.0/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.
9type Both<-A: Data, -B: Data> is Data:
10  Both{left: A, right: B}
11
12def state(-A: Data, r: Q.State<A> & Maybe<&2, Q.Ticket<A>>) -> Q.State<A>:
13  (s, t) = r
14  s
15
16def selected(-A: Data, r: Q.State<A> & Maybe<&2, Q.Ticket<A>>) -> Maybe<&2, Q.Ticket<A>>:
17  (s, t) = r
18  t
19
20def requeued(-A: Data, r: Q.State<A> & Bool) -> Bool:
21  (s, b) = r
22  b
23
24def enqueued(-A: Data, r: Q.State<A> & Nat) -> Q.State<A>:
25  (s, i) = r
26  s
27
28def 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.
34def 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
39def 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
42law 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
48law 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
54law 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
61def 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
68def 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
75def absent.ticket(-A: Data, i: Nat, t: Q.Ticket<A>) -> Data:
76  {Nat.is_eq(Q.id(A, t), i) == False{} : Bool}
77
78def bound.ticket(-A: Data, lower: Q.Ticket<A>, t: Q.Ticket<A>) -> Data:
79  {Q.le(A, lower, t) == True{} : Bool}
80
81def absent.heap(-A: Data, h: H.Heap<Q.Ticket<A>>, +i: Nat) -> Data:
82  all.heap(A, absent.ticket(A, i), h)
83
84def 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.
94def 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
101def 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
108def 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
115law new_ordered:
116  for -A: Data
117  ordered(A, Q.pending(A, Q.new(A)))
118
119law 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
125law 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
132law 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
141law 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
148law 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
154law 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
160law 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
167law 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
173law 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
179law 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
186law 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.
195law 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
204law 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
214law 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
222law 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
229law 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
236def requeue.state(-A: Data, r: Q.State<A> & Bool) -> Q.State<A>:
237  (s, b) = r
238  s
239
240law 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
248law 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
255law 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
262law 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
268law 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
274law 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
280law 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.
288law 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
300law 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>>}