bend-kit-scheduler Releases (5): 0.4.1.0 0xddf158a45b677a352eef521b11c25f57 indexed https://jend.leeeet.dev/files.txt?path=bend-kit-scheduler@0.4.1.0 0.4.0.0 0x72e8324e6301879360718d145b91b762 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-scheduler@0.4.0.0 0.3.0.0 0x355167368b46de39ede21286fd4d9a78 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-scheduler@0.3.0.0 0.2.0.0 0x5f14902bda92dea7eab2b8da03967100 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-scheduler@0.2.0.0 0.1.0.0 0xd5d0bc5368c1bc2a6fbc863a812e64a1 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-scheduler@0.1.0.0 Definitions (126, 1 to 100 shown): Queue.Ticket (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=Ticket) type Ticket<-A: Data> is Data: Ticket{id: Nat, deadline: Nat, payload: A} Queue.State (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=State) type State<-A: Data> is Data: State{next_id: Nat, pending: H.Heap>, running: List<&2, Ticket>} Queue.id (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=id) def id(-A: Data, t: Ticket) -> Nat: Queue.deadline (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=deadline) def deadline(-A: Data, t: Ticket) -> Nat: Queue.payload (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=payload) def payload(-A: Data, t: Ticket) -> A: Queue.le.same (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=le.same) def le.same(b: Bool, i: Nat, j: Nat, d: Nat, e: Nat) -> Bool: Queue.le (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=le) def le(-A: Data, a: Ticket, b: Ticket) -> Bool: Queue.new (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=new) def new(-A: Data) -> State: Queue.enqueue (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=enqueue) def enqueue(~A: Data, d: Nat, x: A, s: State) -> State & Nat: Queue.select.due (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=select.due) def select.due(~A: Data, b: Bool, i: Nat, h: H.Heap>, r: List<&2, Ticket>, t: Ticket, l: H.Heap>, q: H.Heap>) -> State & Maybe<&2, Ticket>: Queue.select (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=select) def select(~A: Data, now: Nat, s: State) -> State & Maybe<&2, Ticket>: Queue.remove.list.keep (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.list.keep) # ponytail: eager O(n) cancellation; indexed deletion if cancellation dominates. def remove.list.keep(-A: Data, b: Bool, t: Ticket, rest: List<&2, Ticket>) -> List<&2, Ticket>: Queue.remove.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.list) def remove.list(-A: Data, xs: List<&2, Ticket>, +i: Nat) -> List<&2, Ticket>: Queue.remove.heap.keep (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.heap.keep) def remove.heap.keep(~A: Data, b: Bool, t: Ticket, l: H.Heap>, r: H.Heap>) -> H.Heap>: Queue.remove.heap (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.heap) def remove.heap(~A: Data, h: H.Heap>, +i: Nat) -> H.Heap>: Queue.cancel (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=cancel) def cancel(~A: Data, i: Nat, s: State) -> State: Queue.find.list.choose (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=find.list.choose) # Reference observation for laws; completion uses the single-pass take below. def find.list.choose(-A: Data, b: Bool, t: Ticket, rest: Maybe<&2, Ticket>) -> Maybe<&2, Ticket>: Queue.find.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=find.list) def find.list(-A: Data, xs: List<&2, Ticket>, +i: Nat) -> Maybe<&2, Ticket>: Queue.Taken (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=Taken) type Taken<-A: Data> is Data: Taken{remaining: List<&2, Ticket>, found: Maybe<&2, Ticket>} Queue.take.keep (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=take.keep) # Remove all matching entries and return the first token in one traversal. def take.keep(-A: Data, b: Bool, t: Ticket, result: Taken) -> Taken: Queue.take.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=take.list) def take.list(-A: Data, xs: List<&2, Ticket>, +i: Nat) -> Taken: Queue.complete.taken (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=complete.taken) def complete.taken(-A: Data, result: Taken, n: Nat, h: H.Heap>) -> State & Maybe<&2, Ticket>: Queue.complete (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=complete) def complete(-A: Data, i: Nat, s: State) -> State & Maybe<&2, Ticket>: Queue.requeue.found (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=requeue.found) def requeue.found(~A: Data, found: Maybe<&2, Ticket>, d: Nat, s: State) -> State & Bool: Queue.requeue.completed (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=requeue.completed) def requeue.completed(~A: Data, r: State & Maybe<&2, Ticket>, d: Nat) -> State & Bool: Queue.requeue (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=requeue) def requeue(~A: Data, i: Nat, d: Nat, s: State) -> State & Bool: Queue.next_id (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=next_id) # Non-consuming observations used by adapters and laws. def next_id(-A: Data, s: State) -> Nat: Queue.pending (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=pending) def pending(-A: Data, s: State) -> H.Heap>: Queue.running (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=running) def running(-A: Data, s: State) -> List<&2, Ticket>: QueueLaws.Both (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=Both) # Ordinary & pairs are affine even when their fields are Data. Invariant # conjunctions contain only evidence, so a Data constructor permits reuse. type Both<-A: Data, -B: Data> is Data: Both{left: A, right: B} QueueLaws.state (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=state) def state(-A: Data, r: Q.State & Maybe<&2, Q.Ticket>) -> Q.State: QueueLaws.selected (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=selected) def selected(-A: Data, r: Q.State & Maybe<&2, Q.Ticket>) -> Maybe<&2, Q.Ticket>: QueueLaws.requeued (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeued) def requeued(-A: Data, r: Q.State & Bool) -> Bool: QueueLaws.enqueued (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=enqueued) def enqueued(-A: Data, r: Q.State & Nat) -> Q.State: QueueLaws.assigned (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=assigned) def assigned(-A: Data, r: Q.State & Nat) -> Nat: QueueLaws.complete.reference (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete.reference) # Reference semantics are deliberately simple; the live transition takes one # pass and its equivalence is proved universally, including duplicate IDs. def complete.reference(-A: Data, +i: Nat, s: Q.State) -> Q.State & Maybe<&2, Q.Ticket>: QueueLaws.requeue.reference (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue.reference) def requeue.reference(~A: Data, i: Nat, d: Nat, s: Q.State) -> Q.State & Bool: QueueLaws.take_equivalent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=take_equivalent) law take_equivalent: for -A: Data for +xs: List<&2, Q.Ticket> for +i: Nat {Q.take.list(A, xs, i) == Q.Taken{Q.remove.list(A, xs, i), Q.find.list(A, xs, i)} : Q.Taken} QueueLaws.complete_equivalent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_equivalent) law complete_equivalent: for -A: Data for +i: Nat for +s: Q.State {Q.complete(A, i, s) == complete.reference(A, i, s) : Q.State & Maybe<&2, Q.Ticket>} QueueLaws.requeue_equivalent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue_equivalent) law requeue_equivalent: for ~A: Data for +i: Nat for d: Nat for +s: Q.State {Q.requeue(~A, i, d, s) == requeue.reference(~A, i, d, s) : Q.State & Bool} QueueLaws.absent.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=absent.list) def absent.list(-A: Data, xs: List<&2, Q.Ticket>, +i: Nat) -> Data: QueueLaws.all.heap (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=all.heap) def all.heap(-A: Data, -P: Q.Ticket -> Data, h: H.Heap>) -> Data: QueueLaws.absent.ticket (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=absent.ticket) def absent.ticket(-A: Data, i: Nat, t: Q.Ticket) -> Data: QueueLaws.bound.ticket (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=bound.ticket) def bound.ticket(-A: Data, lower: Q.Ticket, t: Q.Ticket) -> Data: QueueLaws.absent.heap (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=absent.heap) def absent.heap(-A: Data, h: H.Heap>, +i: Nat) -> Data: QueueLaws.below (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=below) def below(-A: Data, h: H.Heap>, +t: Q.Ticket) -> Data: QueueLaws.ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=ordered) # The root must bound both subtrees recursively, not just its direct children. # No law takes the desired selection result as an assumption. # Cached sizes are a separate construction invariant of collections' heap: # new/push/merge build them and remove.heap recomputes each retained size. # ordered deliberately concerns ordering only. The order/absence merge lemmas # hold even for malformed sizes; they do not claim element conservation for # forged HNode values whose merge fuel can run out early. def ordered(-A: Data, h: H.Heap>) -> Data: QueueLaws.due (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=due) def due(-A: Data, t: Maybe<&2, Q.Ticket>, now: Nat) -> Data: QueueLaws.minimum (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=minimum) def minimum(-A: Data, h: H.Heap>, selected: Maybe<&2, Q.Ticket>) -> Data: QueueLaws.new_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=new_ordered) law new_ordered: for -A: Data ordered(A, Q.pending(A, Q.new(A))) QueueLaws.select_due (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=select_due) law select_due: for ~A: Data for now: Nat for s: Q.State due(A, selected(A, Q.select(~A, now, s)), now) QueueLaws.select_minimum (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=select_minimum) law select_minimum: for ~A: Data for now: Nat for +s: Q.State for e: ordered(A, Q.pending(A, s)) minimum(A, Q.pending(A, s), selected(A, Q.select(~A, now, s))) QueueLaws.equal_deadline_fifo (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=equal_deadline_fifo) law equal_deadline_fifo: for -A: Data for i: Nat for j: Nat for d: Nat for x: A for y: A {Q.le(A, Q.Ticket{i, d, x}, Q.Ticket{j, d, y}) == Nat.is_le(i, j) : Bool} QueueLaws.enqueue_id (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=enqueue_id) law enqueue_id: for ~A: Data for d: Nat for x: A for +s: Q.State {Q.next_id(A, enqueued(A, Q.enqueue(~A, d, x, s))) == 1n+Q.next_id(A, s) : Nat} QueueLaws.cancel_pending_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_pending_absent) law cancel_pending_absent: for ~A: Data for i: Nat for s: Q.State absent.heap(A, Q.pending(A, Q.cancel(~A, i, s)), i) QueueLaws.cancel_running_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_running_absent) law cancel_running_absent: for ~A: Data for i: Nat for s: Q.State absent.list(A, Q.running(A, Q.cancel(~A, i, s)), i) QueueLaws.absent_find (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=absent_find) law absent_find: for -A: Data for +xs: List<&2, Q.Ticket> for +i: Nat for e: absent.list(A, xs, i) {Q.find.list(A, xs, i) == None{} : Maybe<&2, Q.Ticket>} QueueLaws.complete_one_shot (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_one_shot) law complete_one_shot: for -A: Data for +i: Nat for s: Q.State {selected(A, Q.complete(A, i, state(A, Q.complete(A, i, s)))) == None{} : Maybe<&2, Q.Ticket>} QueueLaws.cancel_complete (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_complete) law cancel_complete: for ~A: Data for +i: Nat for s: Q.State {selected(A, Q.complete(A, i, Q.cancel(~A, i, s))) == None{} : Maybe<&2, Q.Ticket>} QueueLaws.cancel_requeue (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_requeue) law cancel_requeue: for ~A: Data for +i: Nat for d: Nat for s: Q.State {requeued(A, Q.requeue(~A, i, d, Q.cancel(~A, i, s))) == False{} : Bool} QueueLaws.complete_requeue (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_requeue) law complete_requeue: for ~A: Data for +i: Nat for d: Nat for s: Q.State {requeued(A, Q.requeue(~A, i, d, state(A, Q.complete(A, i, s)))) == False{} : Bool} QueueLaws.select_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=select_absent) # An absent ID stays absent on every selection, in both registries. Combined # with cancellation above this covers any number of intervening selections. law select_absent: for ~A: Data for now: Nat for +i: Nat for +s: Q.State for eh: absent.heap(A, Q.pending(A, s), i) for er: absent.list(A, Q.running(A, s), i) 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) QueueLaws.absent_selected (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=absent_selected) law absent_selected: for ~A: Data for now: Nat for +i: Nat for +s: Q.State for eh: absent.heap(A, Q.pending(A, s), i) for t: Q.Ticket for e: {selected(A, Q.select(~A, now, s)) == Some{t} : Maybe<&2, Q.Ticket>} {Nat.is_eq(Q.id(A, t), i) == False{} : Bool} QueueLaws.enqueue_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=enqueue_ordered) law enqueue_ordered: for ~A: Data for d: Nat for x: A for +s: Q.State for e: ordered(A, Q.pending(A, s)) ordered(A, Q.pending(A, enqueued(A, Q.enqueue(~A, d, x, s)))) QueueLaws.select_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=select_ordered) law select_ordered: for ~A: Data for now: Nat for +s: Q.State for e: ordered(A, Q.pending(A, s)) ordered(A, Q.pending(A, state(A, Q.select(~A, now, s)))) QueueLaws.cancel_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_ordered) law cancel_ordered: for ~A: Data for i: Nat for +s: Q.State for e: ordered(A, Q.pending(A, s)) ordered(A, Q.pending(A, Q.cancel(~A, i, s))) QueueLaws.requeue.state (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue.state) def requeue.state(-A: Data, r: Q.State & Bool) -> Q.State: QueueLaws.requeue_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue_ordered) law requeue_ordered: for ~A: Data for +i: Nat for d: Nat for +s: Q.State for e: ordered(A, Q.pending(A, s)) ordered(A, Q.pending(A, requeue.state(A, Q.requeue(~A, i, d, s)))) QueueLaws.complete_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_ordered) law complete_ordered: for -A: Data for i: Nat for +s: Q.State for e: ordered(A, Q.pending(A, s)) ordered(A, Q.pending(A, state(A, Q.complete(A, i, s)))) QueueLaws.enqueue_assigned_id (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=enqueue_assigned_id) law enqueue_assigned_id: for ~A: Data for d: Nat for x: A for +s: Q.State {assigned(A, Q.enqueue(~A, d, x, s)) == Q.next_id(A, s) : Nat} QueueLaws.cancel_keeps_counter (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=cancel_keeps_counter) law cancel_keeps_counter: for ~A: Data for i: Nat for +s: Q.State {Q.next_id(A, Q.cancel(~A, i, s)) == Q.next_id(A, s) : Nat} QueueLaws.complete_keeps_counter (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_keeps_counter) law complete_keeps_counter: for -A: Data for i: Nat for +s: Q.State {Q.next_id(A, state(A, Q.complete(A, i, s))) == Q.next_id(A, s) : Nat} QueueLaws.select_keeps_counter (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=select_keeps_counter) law select_keeps_counter: for ~A: Data for now: Nat for +s: Q.State {Q.next_id(A, state(A, Q.select(~A, now, s))) == Q.next_id(A, s) : Nat} QueueLaws.requeue_keeps_counter (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue_keeps_counter) law requeue_keeps_counter: for ~A: Data for i: Nat for d: Nat for +s: Q.State {Q.next_id(A, requeue.state(A, Q.requeue(~A, i, d, s))) == Q.next_id(A, s) : Nat} QueueLaws.requeue_token (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=requeue_token) # The running token, not a newly assigned ID, is moved back to pending. law requeue_token: for ~A: Data for +i: Nat for d: Nat for old: Nat for x: A for n: Nat for h: H.Heap> for r: List<&2, Q.Ticket> {Q.requeue(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r}) == (Q.State{n, H.Heap.push(~Q.Ticket, ~(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 & Bool} QueueLaws.complete_token (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=complete_token) law complete_token: for -A: Data for +i: Nat for old: Nat for x: A for n: Nat for h: H.Heap> for r: List<&2, Q.Ticket> {selected(A, Q.complete(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r})) == Some{Q.Ticket{i, old, x}} : Maybe<&2, Q.Ticket>} QueueProof.split (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=split) def split(-P: Bool -> Type, b: Bool, yes: {b == True{} : Bool} -> P(True{}), no: {b == False{} : Bool} -> P(False{})) -> P(b): QueueProof.take_equivalent.step (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=take_equivalent.step) def take_equivalent.step(-A: Data, b: Bool, t: Q.Ticket, rest: List<&2, Q.Ticket>, found: Maybe<&2, Q.Ticket>) -> {Q.take.keep(A, b, t, Q.Taken{rest, found}) == Q.Taken{Q.remove.list.keep(A, b, t, rest), Q.find.list.choose(A, b, t, found)} : Q.Taken}: QueueProof.key_refl (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_refl) def key_refl(+d: Nat, +i: Nat) -> {Q.le.same(Nat.is_eq(d, d), i, i, d, d) == True{} : Bool}: QueueProof.key_succ (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_succ) def key_succ(b: Bool, i: Nat, j: Nat, d: Nat, e: Nat) -> {Q.le.same(b, i, j, 1n+d, 1n+e) == Q.le.same(b, i, j, d, e) : Bool}: QueueProof.key_succ.premise (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_succ.premise) def key_succ.premise(+d: Nat, +e: Nat, +i: Nat, +j: Nat, +b: Bool, p: {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == b : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == b : Bool}: QueueProof.key_succ.conclusion (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_succ.conclusion) def key_succ.conclusion(+d: Nat, +e: Nat, +i: Nat, +j: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == True{} : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == True{} : Bool}: QueueProof.key_flip (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_flip) def key_flip(+d: Nat, +e: Nat, +i: Nat, +j: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == False{} : Bool}) -> {Q.le.same(Nat.is_eq(e, d), j, i, e, d) == True{} : Bool}: QueueProof.key_trans (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=key_trans) def key_trans(+d: Nat, +e: Nat, +f: Nat, +i: Nat, +j: Nat, +k: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == True{} : Bool}, q: {Q.le.same(Nat.is_eq(e, f), j, k, e, f) == True{} : Bool}) -> {Q.le.same(Nat.is_eq(d, f), i, k, d, f) == True{} : Bool}: QueueProof.le_refl (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=le_refl) def le_refl(-A: Data, t: Q.Ticket) -> {Q.le(A, t, t) == True{} : Bool}: QueueProof.le_flip (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=le_flip) def le_flip(-A: Data, a: Q.Ticket, b: Q.Ticket, e: {Q.le(A, a, b) == False{} : Bool}) -> {Q.le(A, b, a) == True{} : Bool}: QueueProof.le_trans (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=le_trans) def le_trans(-A: Data, a: Q.Ticket, b: Q.Ticket, c: Q.Ticket, e: {Q.le(A, a, b) == True{} : Bool}, f: {Q.le(A, b, c) == True{} : Bool}) -> {Q.le(A, a, c) == True{} : Bool}: QueueProof.merge_all (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_all) # Merging cannot introduce an element that violates any predicate P. Fuel zero # returns the left heap, so this lemma does not trust cached heap sizes. def merge_all(~A: Data, -P: Q.Ticket -> Data, +fuel: Nat, +a: H.Heap>, +b: H.Heap>, +ea: L.all.heap(A, P, a), +eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge.go(~Q.Ticket, ~(x => y => Q.le(A, x, y)), fuel, a, b)): QueueProof.merge_all.full (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_all.full) def merge_all.full(~A: Data, -P: Q.Ticket -> Data, +a: H.Heap>, +b: H.Heap>, ea: L.all.heap(A, P, a), eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge(~Q.Ticket, ~(x => y => Q.le(A, x, y)), a, b)): QueueProof.below_trans (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=below_trans) def below_trans(-A: Data, h: H.Heap>, +a: Q.Ticket, +b: Q.Ticket, e: {Q.le(A, a, b) == True{} : Bool}, eh: L.below(A, h, b)) -> L.below(A, h, a): QueueProof.merge_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_ordered) def merge_ordered(~A: Data, +fuel: Nat, +a: H.Heap>, +b: H.Heap>, +ea: L.ordered(A, a), +eb: L.ordered(A, b)) -> L.ordered(A, H.Heap.merge.go(~Q.Ticket, ~(x => y => Q.le(A, x, y)), fuel, a, b)): QueueProof.merge_ordered.full (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_ordered.full) def merge_ordered.full(~A: Data, +a: H.Heap>, +b: H.Heap>, ea: L.ordered(A, a), eb: L.ordered(A, b)) -> L.ordered(A, H.Heap.merge(~Q.Ticket, ~(x => y => Q.le(A, x, y)), a, b)): QueueProof.remove_all (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=remove_all) def remove_all(~A: Data, -P: Q.Ticket -> Data, +h: H.Heap>, +i: Nat, +eh: L.all.heap(A, P, h)) -> L.all.heap(A, P, Q.remove.heap(~A, h, i)): QueueProof.remove_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=remove_ordered) def remove_ordered(~A: Data, +h: H.Heap>, +i: Nat, +eh: L.ordered(A, h)) -> L.ordered(A, Q.remove.heap(~A, h, i)): QueueProof.remove_absent.heap (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=remove_absent.heap) def remove_absent.heap(~A: Data, +h: H.Heap>, +i: Nat) -> L.absent.heap(A, Q.remove.heap(~A, h, i), i): QueueProof.remove_absent.list (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=remove_absent.list) def remove_absent.list(-A: Data, +xs: List<&2, Q.Ticket>, +i: Nat) -> L.absent.list(A, Q.remove.list(A, xs, i), i): QueueProof.requeue_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=requeue_absent) def requeue_absent(~A: Data, +i: Nat, d: Nat, +s: Q.State, e: {Q.find.list(A, Q.running(A, s), i) == None{} : Maybe<&2, Q.Ticket>}) -> {L.requeued(A, Q.requeue(~A, i, d, s)) == False{} : Bool}: QueueProof.selected_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=selected_absent) def selected_absent(-A: Data, +i: Nat, m: Maybe<&2, Q.Ticket>) -> Data: QueueProof.select_selected_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=select_selected_absent) def select_selected_absent(~A: Data, now: Nat, +i: Nat, +s: Q.State, eh: L.absent.heap(A, Q.pending(A, s), i)) -> selected_absent(A, i, L.selected(A, Q.select(~A, now, s))): QueueProof.push_ordered (https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=push_ordered) def push_ordered(~A: Data, t: Q.Ticket, h: H.Heap>, e: L.ordered(A, h)) -> L.ordered(A, H.Heap.push(~Q.Ticket, ~(x => y => Q.le(A, x, y)), t, h)): More: https://jend.leeeet.dev/packages/bend-kit-scheduler.txt?definitions_offset=100