From d5e43906769f49b6edcb186e67849f8c0e6654b5 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 20 Sep 2026 15:08:41 +0000 Subject: [PATCH] Bend 2 PoC: PollFlightInfo and endpoint expiry laws Add dev/bend2/poll_flight_info, a checked Bend 2 model of the Arrow Flight long-running query protocol: PollFlightInfo and PollInfo, FlightEndpoint.expiration_time, RenewFlightEndpoint and CancelFlightInfo. - main.bend: the server model (queries with progress, poll-descriptor expiry and endpoints with expiry ticks; requests Start, Poll, Cancel, DoGet, Renew, Tick, Fail) with a runnable sample trace. - LAWS.bend: 22 laws, each quoting the Flight.proto or Flight.rst sentence it comes from (progress bounded and monotone, endpoints append-only, unknown and expired descriptors rejected, complete query reports full info with the descriptor unset, cancel semantics and idempotence, DoGet before and after expiry, renewal strictly extends, freshness invariant, anti-vacuity traces). Properties Bend cannot express (long-poll timing, double progress, timestamps) and the trace form of monotonicity are kept as comments with the reason. - PROOF.bend: proofs of all 22 laws; `bend PROOF.bend` prints "All terms check." in 0.3 s. - README.md: what is modelled, the decisions taken where the spec leaves room, how to run, and seven mutation tests, each rejected by the checker. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01BrToZSS2oYHyEoo8JvLJog --- dev/bend2/poll_flight_info/LAWS.bend | 522 ++++++++++ dev/bend2/poll_flight_info/PROOF.bend | 1321 +++++++++++++++++++++++++ dev/bend2/poll_flight_info/README.md | 268 +++++ dev/bend2/poll_flight_info/main.bend | 540 ++++++++++ 4 files changed, 2651 insertions(+) create mode 100644 dev/bend2/poll_flight_info/LAWS.bend create mode 100644 dev/bend2/poll_flight_info/PROOF.bend create mode 100644 dev/bend2/poll_flight_info/README.md create mode 100644 dev/bend2/poll_flight_info/main.bend diff --git a/dev/bend2/poll_flight_info/LAWS.bend b/dev/bend2/poll_flight_info/LAWS.bend new file mode 100644 index 0000000000..614543ad99 --- /dev/null +++ b/dev/bend2/poll_flight_info/LAWS.bend @@ -0,0 +1,522 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The laws of the PollFlightInfo model. The human states them; +# PROOF.bend must prove them. Each law quotes the sentence of +# Flight.proto or docs/source/format/Flight.rst it comes from, or is a +# sanity check that keeps the others from being satisfied vacuously. +# Laws the model cannot express or the session could not prove are +# kept here commented out, with the reason. + +import Base +import ./main.bend as PF + +# Predicates +# ---------- + +# the truth of a Bool as a type: Unit when True, Empty when False +def T(b: Bool) -> Data: + match b: + case True{}: + Unit + case False{}: + Empty + +# a running query's progress is within FULL +def st_ok(st: PF.QState) -> Bool: + match st: + case PF.QRunning{p}: + Nat.is_le(p, PF.FULL()) + case PF.QDone{}: + True{} + case PF.QCancelled{}: + True{} + case PF.QFailed{}: + True{} + +# every query id is below the counter (so no id is ever reissued) and +# every progress is within FULL +def all_ok(qs: List<&2, PF.Query>, +next: Nat) -> Bool: + match qs: + case Nil{}: + True{} + case Con{PF.Query{id, PF.QBody{st, pexp, eps}}, t}: + (Nat.is_lt(id, next) && st_ok(st)) && all_ok(t, next) + +def Inv(qs: List<&2, PF.Query>, +next: Nat) -> Data: + T(all_ok(qs, next)) + +def Inv_s(s: PF.Server) -> Data: + PF.Server{qs, next, now} = s + Inv(qs, next) + +def queries(s: PF.Server) -> List<&2, PF.Query>: + PF.Server{qs, next, now} = s + qs + +# observations of a looked-up query +def mq_running(m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + True{} + case PF.QDone{}: + False{} + case PF.QCancelled{}: + False{} + case PF.QFailed{}: + False{} + +def mq_done(m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + False{} + case PF.QDone{}: + True{} + case PF.QCancelled{}: + False{} + case PF.QFailed{}: + False{} + +def mq_cancelled(m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + False{} + case PF.QDone{}: + False{} + case PF.QCancelled{}: + True{} + case PF.QFailed{}: + False{} + +def mq_failed(m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + False{} + case PF.QDone{}: + False{} + case PF.QCancelled{}: + False{} + case PF.QFailed{}: + True{} + +# a running query whose poll descriptor has expired +def poll_expired(+now: Nat, m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + Bool.not(Nat.is_lt(now, pexp)) + case PF.QDone{}: + False{} + case PF.QCancelled{}: + False{} + case PF.QFailed{}: + False{} + +# the endpoints of a looked-up query, as tickets +def tickets_of(m: Maybe<&2, PF.QBody>) -> List<&2, Nat>: + match m: + case None{}: + Nil{} + case Some{PF.QBody{st, pexp, eps}}: + PF.tickets(eps) + +# the expiry of endpoint tk of a looked-up query +def exp_of(+tk: Nat, m: Maybe<&2, PF.QBody>) -> Maybe<&2, Nat>: + match m: + case None{}: + None{} + case Some{PF.QBody{st, pexp, eps}}: + PF.find_ep(tk, eps) + +# whether the query's results are still served: running or complete +def st_live(st: PF.QState) -> Bool: + match st: + case PF.QRunning{p}: + True{} + case PF.QDone{}: + True{} + case PF.QCancelled{}: + False{} + case PF.QFailed{}: + False{} + +def ep_before(+now: Nat, e: Maybe<&2, Nat>) -> Bool: + match e: + case None{}: + False{} + case Some{exp}: + Nat.is_lt(now, exp) + +def ep_after(+now: Nat, e: Maybe<&2, Nat>) -> Bool: + match e: + case None{}: + False{} + case Some{exp}: + Bool.not(Nat.is_lt(now, exp)) + +# endpoint tk of a live query exists and now < expiration +def ep_valid(+now: Nat, +tk: Nat, m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + st_live(st) && ep_before(now, PF.find_ep(tk, eps)) + +# endpoint tk of a live query exists and its expiration has passed +def ep_expired(+now: Nat, +tk: Nat, m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + False{} + case Some{PF.QBody{st, pexp, eps}}: + st_live(st) && ep_after(now, PF.find_ep(tk, eps)) + +# observations of responses +def prog_ok(r: PF.Resp) -> Bool: + match r: + case PF.RPoll{p, d, info}: + Nat.is_le(p, PF.FULL()) + case _: + True{} + +# xs is a prefix of ys +def is_prefix(xs: List<&2, Nat>, ys: List<&2, Nat>) -> Bool: + match xs ys: + case Nil{} _: + True{} + case Con{x, xt} Nil{}: + False{} + case Con{x, xt} Con{y, yt}: + Nat.is_eq(x, y) && is_prefix(xt, yt) + +# a later PollInfo reports at least the progress and extends the +# endpoints of an earlier one; vacuous unless both are PollInfos +def Resp.mono(r1: PF.Resp, r2: PF.Resp) -> Bool: + match r1 r2: + case PF.RPoll{p1, d1, i1} PF.RPoll{p2, d2, i2}: + Nat.is_le(p1, p2) && is_prefix(i1, i2) + case _ _: + True{} + +# the renewed endpoint's expiry is strictly later than the old one +def ren_later(old: Maybe<&2, Nat>, r: PF.Resp) -> Bool: + match old r: + case Some{exp} PF.REndpoint{tk, exp2}: + Nat.is_lt(exp, exp2) + case _ _: + False{} + +# Invariant +# --------- + +# LAW: the initial state satisfies the invariant +law inv_start: + Inv_s(PF.start()) + +# LAW: every request keeps the invariant: ids stay below the counter +# and progress stays within FULL +law inv_kept: + for a : PF.Act + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : Inv(qs, next) + Inv_s(PF.state(PF.step(a, qs, next, now))) + +# Progress +# -------- + +# LAW (Flight.proto, PollInfo.progress): "If known, must be in +# [0.0, 1.0]". In the Nat model: a PollInfo's progress is at most FULL. +law progress_bounded: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : Inv(qs, next) + T(prog_ok(PF.resp(PF.poll(q, qs, next, now)))) + +# LAW (Flight.proto, PollInfo.info): "Subsequent PollInfo responses may +# only append new endpoints to info." And, stronger than the proto, +# which says progress "need not be monotonic or nondecreasing", this +# server's progress never decreases: polling a query, letting any one +# request happen, and polling it again yields at least the progress and +# a superlist of the endpoints of the first poll. +law poll_monotone: + for a : PF.Act + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : Inv(qs, next) + T(Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.step(a, qs, next, now)))))) + +# Descriptors +# ----------- + +# LAW (Flight.rst): "The client should use the descriptor (not the +# original FlightDescriptor) to call the next PollFlightInfo()." A poll +# descriptor the server never issued (an id at or above the counter) is +# an error. Re-sending the original descriptor is AStart, which starts a +# new query rather than polling the old one. +law unknown_descriptor_rejected: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : Inv(qs, next) + for u : T(Nat.is_le(next, q)) + {PF.resp(PF.poll(q, qs, next, now)) == PF.RErr{} : PF.Resp} + +# LAW (Flight.proto, PollFlightInfo): "A client can't use +# PollInfo.flight_descriptor after PollInfo.expiration_time passes. A +# server might not accept the retry descriptor anymore and the query +# may be cancelled." Polling an expired descriptor is an error, and the +# query is cancelled afterwards. +law expired_descriptor_rejected: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(poll_expired(now, PF.find(q, qs))) + {PF.resp(PF.poll(q, qs, next, now)) == PF.RErr{} : PF.Resp} & T(mq_cancelled(PF.find(q, queries(PF.state(PF.poll(q, qs, next, now)))))) + +# LAW (Flight.proto, PollInfo.flight_descriptor): "If unset, the query +# is complete." and PollInfo.info: "If 'flight_descriptor' is not +# specified, the query is complete and 'info' specifies all results." +# Polling a complete query answers progress FULL, no descriptor and +# every endpoint of the query, and leaves the server unchanged. +law done_poll_complete: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(mq_done(PF.find(q, qs))) + {PF.poll(q, qs, next, now) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp} + +# LAW (anti-vacuity): the descriptor a start returns polls +# successfully, with progress 0 and no endpoints yet. +law fresh_query_polls: + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + {PF.resp(PF.step_s(PF.APoll{next}, PF.state(PF.step(PF.AStart{}, qs, next, now)))) == PF.RPoll{0n, Some{next}, Nil{}} : PF.Resp} + +# Cancellation +# ------------ + +# LAW (Flight.proto, CancelStatus): "CANCEL_STATUS_CANCELLED = 1; The +# cancellation request is complete." Cancelling a running query answers +# CANCELLED and the query is cancelled. +law cancel_running: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(mq_running(PF.find(q, qs))) + {PF.resp(PF.cancel(q, qs, next, now)) == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & T(mq_cancelled(PF.find(q, queries(PF.state(PF.cancel(q, qs, next, now)))))) + +# LAW (Flight.proto, PollFlightInfo): "A client may use the +# CancelFlightInfo action with PollInfo.info to cancel the running +# query." Once cancelled, polling the query is an error, from any state. +law cancelled_poll_rejected: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + {PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.cancel(q, qs, next, now)))) == PF.RErr{} : PF.Resp} + +# LAW (ExpirationTimeProducer, Java integration test): "The client can't +# read data from endpoints even within 6 seconds after the action." +# Once cancelled, DoGet on any of the query's endpoints is an error. +law cancelled_doget_rejected: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.cancel(q, qs, next, now)))) == PF.RErr{} : PF.Resp} + +# LAW (Flight.proto, CancelStatus): "Subsequent requests with the same +# payload may return CANCELLED or a NOT_FOUND error." This server +# repeats its first answer: cancelling twice answers the same as once. +law cancel_idempotent: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + {PF.resp(PF.step_s(PF.ACancel{q}, PF.state(PF.cancel(q, qs, next, now)))) == PF.resp(PF.cancel(q, qs, next, now)) : PF.Resp} + +# LAW (Flight.proto, CancelStatus): "CANCEL_STATUS_NOT_CANCELLABLE = 3; +# The query is not cancellable." A failed query has nothing left to +# cancel and answers NOT_CANCELLABLE. +law failed_not_cancellable: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(mq_failed(PF.find(q, qs))) + {PF.resp(PF.cancel(q, qs, next, now)) == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp} + +# LAW (Flight.rst): "A server should return an error status instead of a +# response if the query fails." Polling a query after it failed is an +# error. +law failed_poll_rejected: + for +q : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(mq_running(PF.find(q, qs))) + {PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.step(PF.AFail{q}, qs, next, now)))) == PF.RErr{} : PF.Resp} + +# Endpoint expiration +# ------------------- + +# LAW (Flight.rst): "If an endpoint has expiration time, the client can +# get data multiple times by DoGet until the expiration time is +# reached." Before the expiry tick, DoGet streams (and, since DoGet does +# not change the state, does so again on the next call). +law doget_before_expiry: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(ep_valid(now, tk, PF.find(q, qs))) + {PF.resp(PF.doget(q, tk, qs, next, now)) == PF.RData{} : PF.Resp} + +# LAW (Flight.rst, same sentence): once the expiration time is reached, +# DoGet is an error. +law doget_after_expiry: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(ep_expired(now, tk, PF.find(q, qs))) + {PF.resp(PF.doget(q, tk, qs, next, now)) == PF.RErr{} : PF.Resp} + +# LAW (Flight.rst): "the client may be able to extend the expiration +# time by RenewFlightEndpoint action", and the Java integration test: +# "Renewed FlightEndpoint must have newer expiration time". Renewing a +# valid endpoint answers an endpoint whose expiry is strictly later. +law renew_extends: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(ep_valid(now, tk, PF.find(q, qs))) + T(ren_later(exp_of(tk, PF.find(q, qs)), PF.resp(PF.renew(q, tk, qs, next, now)))) + +# LAW (model decision): an endpoint whose expiration has passed cannot +# be renewed; the server may already have released its data. +law renew_expired_rejected: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(ep_expired(now, tk, PF.find(q, qs))) + {PF.resp(PF.renew(q, tk, qs, next, now)) == PF.RErr{} : PF.Resp} + +# LAW (ExpirationTimeProducer): "The client can read data from endpoints +# multiple times within more 10 seconds after the action." After a +# renewal, DoGet on the renewed endpoint streams. +law renewed_doget_ok: + for +q : Nat + for +tk : Nat + for +qs : List<&2, PF.Query> + for +next : Nat + for +now : Nat + for w : T(ep_valid(now, tk, PF.find(q, qs))) + {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.renew(q, tk, qs, next, now)))) == PF.RData{} : PF.Resp} + +# Sample traces +# ------------- + +# LAW (anti-vacuity, closed trace): start, poll, tick, poll, then DoGet +# on the fresh endpoint before its expiry streams data. +law trace_doget_fresh: + {PF.resp(PF.replay([PF.AStart{}, PF.APoll{0n}, PF.ATick{}, PF.APoll{0n}, PF.ADoGet{0n, 0n}])) == PF.RData{} : PF.Resp} + +# LAW (closed trace): the same endpoint, ETTL ticks later, is expired. +law trace_doget_expired: + {PF.resp(PF.replay([PF.AStart{}, PF.APoll{0n}, PF.ATick{}, PF.APoll{0n}, PF.ATick{}, PF.ATick{}, PF.ADoGet{0n, 0n}])) == PF.RErr{} : PF.Resp} + +# LAW (closed trace): four ticks complete the query; the poll then has +# no descriptor and lists the four endpoints. +law trace_completes: + {PF.resp(PF.replay([PF.AStart{}, PF.ATick{}, PF.APoll{0n}, PF.ATick{}, PF.APoll{0n}, PF.ATick{}, PF.APoll{0n}, PF.ATick{}, PF.APoll{0n}])) == PF.RPoll{PF.FULL(), None{}, [0n, 1n, 2n, 3n]} : PF.Resp} + +# Not modelled +# ------------ + +# NOT EXPRESSIBLE: Flight.proto, PollFlightInfo: "A server should not +# respond until the result would be different from last time." This is +# a timing (liveness) property of when the RPC returns, not of what it +# returns. The model is a pure function from state and request to +# response; it has no notion of blocking, so the law cannot be stated. +# +# NOT EXPRESSIBLE: Flight.proto, PollFlightInfo: "The first +# PollFlightInfo call should return as quickly as possible." Same +# reason: there is no time-to-respond in the model. +# +# NOT EXPRESSIBLE: Flight.proto, PollInfo.progress: "optional double +# progress = 3; ... must be in [0.0, 1.0]". Bend has no F64 and its F32 +# is axiomatic (nothing about floats can be proven), so progress is a +# Nat out of FULL() = 100; progress_bounded is that law's Nat form. +# +# NOT EXPRESSIBLE: expiration_time as a google.protobuf.Timestamp +# (int64 seconds + int32 nanos) against wall-clock time. Bend has no +# 64-bit integers and no clock the checker can reason about, so time is +# a Nat tick advanced by the ATick request. +# +# NOT PROVEN: the trace form of poll_monotone ("for any list of requests +# between two polls"). It follows from poll_monotone by induction once +# two more invariants are proven: an issued id is never forgotten, and +# QCancelled / QFailed are absorbing (so an error between two PollInfos +# cannot happen). Both are true of the model but were not proven in +# this session; the one-step law with an arbitrary intermediate request +# is what is checked. +# +# law poll_monotone_trace: +# for acts : List +# for +q : Nat +# for +qs : List<&2, PF.Query> +# for +next : Nat +# for +now : Nat +# for w : Inv(qs, next) +# T(Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.run(acts, (PF.Server{qs, next, now}, PF.RErr{}))))))) diff --git a/dev/bend2/poll_flight_info/PROOF.bend b/dev/bend2/poll_flight_info/PROOF.bend new file mode 100644 index 0000000000..9f89758159 --- /dev/null +++ b/dev/bend2/poll_flight_info/PROOF.bend @@ -0,0 +1,1321 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The proofs. Imports the model (as PF) and the claims (as Laws) and +# fills every law they state; `bend PROOF.bend` is the whole check. +# +# Two idioms recur. A computed Bool or Maybe cannot be matched in +# place, so a `.fin` helper takes it as a parameter c together with an +# equation e about it, matches c, and rewrites the goal with e inside +# each case ("inspect"). And a rewrite may not precede a match on a +# parameter, so every helper matches first and rewrites inside the +# cases. + +import Base +import ./main.bend as PF +import ./LAWS.bend as Laws + +# Proof kit +# --------- + +# T(True{}) from an equation +def true_T(b: Bool, e: {True{} == b : Bool}) -> Laws.T(b): + %e : Laws.T(_) + Unit{} + +def disc(b: Bool) -> Type: + match b: + case True{}: + Unit + case False{}: + Empty + +# True and False clash +def true_ne_false(e: {True{} == False{} : Bool}) -> Empty: + %e : disc(_) + Unit{} + +# an equation from T(b) +def T_true(b: Bool, w: Laws.T(b)) -> {True{} == b : Bool}: + match b: + case True{}: + {==} + case False{}: + Empty.absurd({True{} == False{} : Bool}, w) + +# T(c && b) splits into T(c) and T(b); c is a parameter so it can be matched +def split.fin(c: Bool, -b: Bool, w: Laws.T(c && b), -P: Type, k: Laws.T(c) -> Laws.T(b) -> P) -> P: + match c: + case True{}: + k(Unit{}, w) + case False{}: + Empty.absurd(P, w) + +# T(c) and T(b) join into T(c && b) +def join.fin(c: Bool, -b: Bool, wc: Laws.T(c), wb: Laws.T(b)) -> Laws.T(c && b): + match c: + case True{}: + wb + case False{}: + Empty.absurd(Laws.T(False{} && b), wc) + +# T(Bool.not(c)) refutes T(c) +def not_both.fin(c: Bool, w: Laws.T(c), n: Laws.T(Bool.not(c)), -P: Type) -> P: + match c: + case True{}: + Empty.absurd(P, n) + case False{}: + Empty.absurd(P, w) + +# Lemmas on Nat +# ------------- + +# a nat equals itself +def eq_refl(n: Nat) -> {True{} == Nat.is_eq(n, n) : Bool}: + match n: + case 0n: + {==} + case 1n+p: + eq_refl(p) + +# a true Nat.is_eq is an equality +def eq_sound(x: Nat, h: Nat, e: {True{} == Nat.is_eq(x, h) : Bool}) -> {x == h : Nat}: + match x h: + case 0n 0n: + {==} + case 0n 1n+q: + Empty.absurd({0n == 1n+q : Nat}, true_ne_false(e)) + case 1n+p 0n: + Empty.absurd({1n+p == 0n : Nat}, true_ne_false(e)) + case 1n+p 1n+q: + %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat} + {==} + +# n < n + 1 +def lt_succ(n: Nat) -> Laws.T(Nat.is_lt(n, 1n+n)): + match n: + case 0n: + Unit{} + case 1n+p: + lt_succ(p) + +# x < n implies x < n + 1 +def lt_mono(x: Nat, n: Nat, w: Laws.T(Nat.is_lt(x, n))) -> Laws.T(Nat.is_lt(x, 1n+n)): + match x n: + case 0n 0n: + Empty.absurd(Laws.T(Nat.is_lt(0n, 1n)), w) + case 0n 1n+q: + Unit{} + case 1n+p 0n: + Empty.absurd(Laws.T(Nat.is_lt(1n+p, 1n)), w) + case 1n+p 1n+q: + lt_mono(p, q, w) + +# x < n implies x <= n +def lt_le(x: Nat, n: Nat, w: Laws.T(Nat.is_lt(x, n))) -> Laws.T(Nat.is_le(x, n)): + match x n: + case 0n 0n: + Empty.absurd(Laws.T(Nat.is_le(0n, 0n)), w) + case 0n 1n+q: + Unit{} + case 1n+p 0n: + Empty.absurd(Laws.T(Nat.is_le(1n+p, 0n)), w) + case 1n+p 1n+q: + lt_le(p, q, w) + +# n <= n +def le_refl(n: Nat) -> Laws.T(Nat.is_le(n, n)): + match n: + case 0n: + Unit{} + case 1n+p: + le_refl(p) + +# p <= p + k +def le_add(p: Nat, k: Nat) -> Laws.T(Nat.is_le(p, Nat.add(p, k))): + match p k: + case 0n 0n: + Unit{} + case 0n 1n+q: + Unit{} + case 1n+p2 k2: + le_add(p2, k2) + +# m >= e implies e < m + 1 +def ge_lt_succ(e: Nat, m: Nat, w: Laws.T(Nat.is_ge(m, e))) -> Laws.T(Nat.is_lt(e, 1n+m)): + match e m: + case 0n 0n: + Unit{} + case 0n 1n+q: + Unit{} + case 1n+p 0n: + Empty.absurd(Laws.T(Nat.is_lt(1n+p, 1n)), w) + case 1n+p 1n+q: + ge_lt_succ(p, q, w) + +# m >= a + 1 implies m >= a +def ge_pred(a: Nat, m: Nat, w: Laws.T(Nat.is_ge(m, 1n+a))) -> Laws.T(Nat.is_ge(m, a)): + match a m: + case 0n 0n: + Empty.absurd(Laws.T(Nat.is_ge(0n, 0n)), w) + case 0n 1n+q: + Unit{} + case 1n+p 0n: + Empty.absurd(Laws.T(Nat.is_ge(0n, 1n+p)), w) + case 1n+p 1n+q: + ge_pred(p, q, w) + +# Base's max law as a T fact +def max_ge_l(+a: Nat, +b: Nat) -> Laws.T(Nat.is_ge(Nat.max(a, b), a)): + true_T(Nat.is_ge(Nat.max(a, b), a), Equal.sym(Bool, Nat.is_ge(Nat.max(a, b), a), True{}, Nat.max_ge_l(a, b))) + +def max_ge_r(+a: Nat, +b: Nat) -> Laws.T(Nat.is_ge(Nat.max(a, b), b)): + true_T(Nat.is_ge(Nat.max(a, b), b), Equal.sym(Bool, Nat.is_ge(Nat.max(a, b), b), True{}, Nat.max_ge_r(a, b))) + +# the renewed expiry is strictly later than the old one +def renewed_later(+exp: Nat, +now: Nat) -> Laws.T(Nat.is_lt(exp, PF.renewed(exp, now))): + ge_lt_succ(exp, Nat.max(exp, Nat.add(PF.ETTL(), now)), max_ge_l(exp, Nat.add(PF.ETTL(), now))) + +# the renewed expiry is still ahead of the clock +def renewed_valid(+exp: Nat, +now: Nat) -> Laws.T(Nat.is_lt(now, PF.renewed(exp, now))): + ge_lt_succ(now, Nat.max(exp, Nat.add(PF.ETTL(), now)), + ge_pred(now, Nat.max(exp, Nat.add(PF.ETTL(), now)), + ge_pred(1n+now, Nat.max(exp, Nat.add(PF.ETTL(), now)), max_ge_r(exp, Nat.add(PF.ETTL(), now))))) + +# a touched descriptor is valid now +def pttl_valid(now: Nat) -> {True{} == Nat.is_lt(now, Nat.add(PF.PTTL(), now)) : Bool}: + match now: + case 0n: + {==} + case 1n+p: + pttl_valid(p) + +# id < next and next <= q imply q != id +def lt_le_ne(id: Nat, next: Nat, q: Nat, w: Laws.T(Nat.is_lt(id, next)), u: Laws.T(Nat.is_le(next, q))) -> {False{} == Nat.is_eq(q, id) : Bool}: + match id next q: + case 0n 0n c: + Empty.absurd({False{} == Nat.is_eq(c, 0n) : Bool}, w) + case 1n+i 0n c: + Empty.absurd({False{} == Nat.is_eq(c, 1n+i) : Bool}, w) + case i 1n+n 0n: + Empty.absurd({False{} == Nat.is_eq(0n, i) : Bool}, u) + case 0n 1n+n 1n+c: + {==} + case 1n+i 1n+n 1n+c: + lt_le_ne(i, n, c, w, u) + +# Lemmas on find and upd +# ---------------------- + +# a lookup after an update is the update of the lookup +def upd_m(+op: PF.Op, +now: Nat, +q: Nat, m: Maybe<&2, PF.QBody>) -> Maybe<&2, PF.QBody>: + match m: + case None{}: + None{} + case Some{body}: + Some{PF.apply(op, now, q, body)} + +def find_upd.fin(+q: Nat, +op: PF.Op, +now: Nat, +id: Nat, +body: PF.QBody, -t: List<&2, PF.Query>, + rec: {upd_m(op, now, q, PF.find(q, t)) == PF.find(q, PF.upd(op, now, t)) : Maybe<&2, PF.QBody>}, + c: Bool, e: {c == Nat.is_eq(q, id) : Bool}) + -> {upd_m(op, now, q, PF.pick_q(c, body, PF.find(q, t))) == PF.pick_q(c, PF.apply(op, now, id, body), PF.find(q, PF.upd(op, now, t))) : Maybe<&2, PF.QBody>}: + match c: + case True{}: + %eq_sound(q, id, e) : {Some{PF.apply(op, now, q, body)} == Some{PF.apply(op, now, _, body)} : Maybe<&2, PF.QBody>} + {==} + case False{}: + rec + +def find_upd(+q: Nat, +op: PF.Op, +now: Nat, qs: List<&2, PF.Query>) -> {upd_m(op, now, q, PF.find(q, qs)) == PF.find(q, PF.upd(op, now, qs)) : Maybe<&2, PF.QBody>}: + match qs: + case Nil{}: + {==} + case Con{PF.Query{+id, +body}, t}: + find_upd.fin(q, op, now, id, body, t, find_upd(q, op, now, t), Nat.is_eq(q, id), {==}) + +# a lookup of an id at or above the counter finds nothing +def find_unknown.fin(+q: Nat, +next: Nat, +id: Nat, -body: PF.QBody, -t: List<&2, PF.Query>, + rec: Laws.T(Laws.all_ok(t, next)) -> {None{} == PF.find(q, t) : Maybe<&2, PF.QBody>}, + u: Laws.T(Nat.is_le(next, q)), c: Bool, e: {c == Nat.is_eq(q, id) : Bool}, wid: Laws.T(Nat.is_lt(id, next)), wt: Laws.T(Laws.all_ok(t, next))) + -> {None{} == PF.pick_q(c, body, PF.find(q, t)) : Maybe<&2, PF.QBody>}: + match c: + case True{}: + Empty.absurd({None{} == Some{body} : Maybe<&2, PF.QBody>}, + true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(q, id), False{}, e, Equal.sym(Bool, False{}, Nat.is_eq(q, id), lt_le_ne(id, next, q, wid, u))))) + case False{}: + rec(wt) + +def find_unknown(+q: Nat, qs: List<&2, PF.Query>, +next: Nat, +u: Laws.T(Nat.is_le(next, q))) -> Laws.T(Laws.all_ok(qs, next)) -> {None{} == PF.find(q, qs) : Maybe<&2, PF.QBody>}: + match qs: + case Nil{}: + w => {==} + case Con{PF.Query{+id, PF.QBody{st, pexp, eps}}, +t}: + w => split.fin(Nat.is_lt(id, next) && Laws.st_ok(st), Laws.all_ok(t, next), w, {None{} == PF.find(q, PF.Query{id, PF.QBody{st, pexp, eps}} <> t) : Maybe<&2, PF.QBody>}, + wh => wt => split.fin(Nat.is_lt(id, next), Laws.st_ok(st), wh, {None{} == PF.find(q, PF.Query{id, PF.QBody{st, pexp, eps}} <> t) : Maybe<&2, PF.QBody>}, + wid => wst => find_unknown.fin(q, next, id, PF.QBody{st, pexp, eps}, t, find_unknown(q, t, next, u), u, Nat.is_eq(q, id), {==}, wid, wt))) + +# the invariant, seen through a lookup: a found running query's progress is within FULL +def mst_ok(m: Maybe<&2, PF.QBody>) -> Bool: + match m: + case None{}: + True{} + case Some{PF.QBody{st, pexp, eps}}: + Laws.st_ok(st) + +def find_ok.fin(c: Bool, -st: PF.QState, -pexp: Nat, -eps: List<&2, PF.Endpoint>, -t: List<&2, PF.Query>, +q: Nat, + wst: Laws.T(Laws.st_ok(st)), rec: Laws.T(mst_ok(PF.find(q, t)))) + -> Laws.T(mst_ok(PF.pick_q(c, PF.QBody{st, pexp, eps}, PF.find(q, t)))): + match c: + case True{}: + wst + case False{}: + rec + +def find_ok(+q: Nat, qs: List<&2, PF.Query>, +next: Nat) -> Laws.T(Laws.all_ok(qs, next)) -> Laws.T(mst_ok(PF.find(q, qs))): + match qs: + case Nil{}: + w => Unit{} + case Con{PF.Query{+id, PF.QBody{st, pexp, eps}}, +t}: + w => split.fin(Nat.is_lt(id, next) && Laws.st_ok(st), Laws.all_ok(t, next), w, Laws.T(mst_ok(PF.find(q, PF.Query{id, PF.QBody{st, pexp, eps}} <> t))), + wh => wt => split.fin(Nat.is_lt(id, next), Laws.st_ok(st), wh, Laws.T(mst_ok(PF.find(q, PF.Query{id, PF.QBody{st, pexp, eps}} <> t))), + wid => wst => find_ok.fin(Nat.is_eq(q, id), st, pexp, eps, t, q, wst, find_ok(q, t, next)(wt)))) + +# Invariant preservation +# ---------------------- + +# a bound below next is a bound below next + 1 +def mono(qs: List<&2, PF.Query>, +next: Nat, w: Laws.T(Laws.all_ok(qs, next))) -> Laws.T(Laws.all_ok(qs, 1n+next)): + match qs: + case Nil{}: + Unit{} + case Con{PF.Query{+id, PF.QBody{+st, pexp, eps}}, +t}: + split.fin(Nat.is_lt(id, next) && Laws.st_ok(st), Laws.all_ok(t, next), w, Laws.T(Laws.all_ok(PF.Query{id, PF.QBody{st, pexp, eps}} <> t, 1n+next)), + wh => wt => split.fin(Nat.is_lt(id, next), Laws.st_ok(st), wh, Laws.T(Laws.all_ok(PF.Query{id, PF.QBody{st, pexp, eps}} <> t, 1n+next)), + wid => wst => join.fin(Nat.is_lt(id, 1n+next) && Laws.st_ok(st), Laws.all_ok(t, 1n+next), + join.fin(Nat.is_lt(id, 1n+next), Laws.st_ok(st), lt_mono(id, next, wid), wst), mono(t, next, wt)))) + +# a tick keeps progress within FULL: over the verdict c of is_lt(p + STEP, FULL) +def tick_ok.fin(c: Bool, +p: Nat, e: {c == Nat.is_lt(Nat.add(p, PF.STEP()), PF.FULL()) : Bool}) -> Laws.T(Laws.st_ok(PF.advance(Nat.add(p, PF.STEP()), c))): + match c: + case True{}: + lt_le(Nat.add(p, PF.STEP()), PF.FULL(), true_T(Nat.is_lt(Nat.add(p, PF.STEP()), PF.FULL()), e)) + case False{}: + Unit{} + +def tick_st_ok(st: PF.QState, w: Laws.T(Laws.st_ok(st))) -> Laws.T(Laws.st_ok(PF.tick_st(st))): + match st: + case PF.QRunning{+p}: + tick_ok.fin(Nat.is_lt(Nat.add(p, PF.STEP()), PF.FULL()), p, {==}) + case PF.QDone{}: + Unit{} + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +def cancel_st_ok(st: PF.QState) -> Laws.T(Laws.st_ok(PF.cancel_st(st))): + match st: + case PF.QRunning{p}: + Unit{} + case PF.QDone{}: + Unit{} + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +def fail_st_ok(st: PF.QState) -> Laws.T(Laws.st_ok(PF.fail_st(st))): + match st: + case PF.QRunning{p}: + Unit{} + case PF.QDone{}: + Unit{} + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# the verdict c of a targeted op's id test picks the new or the old body +def when_ok.fin(c: Bool, -a: PF.QBody, -b: PF.QBody, wa: Laws.T(mst_ok(Some{a})), wb: Laws.T(mst_ok(Some{b}))) -> Laws.T(mst_ok(Some{PF.when_b(c, a, b)})): + match c: + case True{}: + wa + case False{}: + wb + +# every op keeps a body's progress within FULL +def apply_ok(op: PF.Op, +now: Nat, +id: Nat, body: PF.QBody) -> Laws.T(mst_ok(Some{body})) -> Laws.T(mst_ok(Some{PF.apply(op, now, id, body)})): + match op body: + case PF.OpTick{} PF.QBody{+st, pexp, eps}: + w => tick_st_ok(st, w) + case PF.OpTouch{q} PF.QBody{+st, +pexp, +eps}: + +w => when_ok.fin(Nat.is_eq(q, id), PF.touch_body(now, PF.QBody{st, pexp, eps}), PF.QBody{st, pexp, eps}, w, w) + case PF.OpCancel{q} PF.QBody{+st, +pexp, +eps}: + w => when_ok.fin(Nat.is_eq(q, id), PF.cancel_body(PF.QBody{st, pexp, eps}), PF.QBody{st, pexp, eps}, cancel_st_ok(st), w) + case PF.OpFail{q} PF.QBody{+st, +pexp, +eps}: + w => when_ok.fin(Nat.is_eq(q, id), PF.fail_body(PF.QBody{st, pexp, eps}), PF.QBody{st, pexp, eps}, fail_st_ok(st), w) + case PF.OpRenew{q, tk} PF.QBody{+st, +pexp, +eps}: + +w => when_ok.fin(Nat.is_eq(q, id), PF.renew_body(tk, now, PF.QBody{st, pexp, eps}), PF.QBody{st, pexp, eps}, w, w) + +def all_ok_cons(+id: Nat, body: PF.QBody, -rest: List<&2, PF.Query>, +next: Nat, + wid: Laws.T(Nat.is_lt(id, next)), wb: Laws.T(mst_ok(Some{body})), wr: Laws.T(Laws.all_ok(rest, next))) + -> Laws.T(Laws.all_ok(PF.Query{id, body} <> rest, next)): + match body: + case PF.QBody{+st, pexp, eps}: + join.fin(Nat.is_lt(id, next) && Laws.st_ok(st), Laws.all_ok(rest, next), join.fin(Nat.is_lt(id, next), Laws.st_ok(st), wid, wb), wr) + +# the head of an updated list is ok: the body after apply, as a pattern +def upd_body_ok(op: PF.Op, +now: Nat, +id: Nat, body: PF.QBody, -rest: List<&2, PF.Query>, +next: Nat, + wid: Laws.T(Nat.is_lt(id, next)), wa: Laws.T(mst_ok(Some{PF.apply(op, now, id, body)})), wr: Laws.T(Laws.all_ok(rest, next))) + -> Laws.T(Laws.all_ok(PF.Query{id, PF.apply(op, now, id, body)} <> rest, next)): + all_ok_cons(id, PF.apply(op, now, id, body), rest, next, wid, wa, wr) + +# an update keeps the invariant +def upd_ok(+op: PF.Op, +now: Nat, qs: List<&2, PF.Query>, +next: Nat) -> Laws.T(Laws.all_ok(qs, next)) -> Laws.T(Laws.all_ok(PF.upd(op, now, qs), next)): + match qs: + case Nil{}: + w => Unit{} + case Con{PF.Query{+id, PF.QBody{+st, +pexp, +eps}}, +t}: + w => split.fin(Nat.is_lt(id, next) && Laws.st_ok(st), Laws.all_ok(t, next), w, Laws.T(Laws.all_ok(PF.upd(op, now, PF.Query{id, PF.QBody{st, pexp, eps}} <> t), next)), + wh => wt => split.fin(Nat.is_lt(id, next), Laws.st_ok(st), wh, Laws.T(Laws.all_ok(PF.upd(op, now, PF.Query{id, PF.QBody{st, pexp, eps}} <> t), next)), + wid => wst => upd_body_ok(op, now, id, PF.QBody{st, pexp, eps}, PF.upd(op, now, t), next, wid, apply_ok(op, now, id, PF.QBody{st, pexp, eps})(wst), upd_ok(op, now, t, next)(wt)))) + +# Invariant laws +# -------------- + +def Laws.inv_start(): + Unit{} + +# the state after a poll, over the lookup m and its verdicts +def kept_poll_run.fin(alive: Bool, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, -p: Nat, -eps: List<&2, PF.Endpoint>, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.poll_run(q, qs, next, now, p, eps, alive))): + match alive: + case True{}: + upd_ok(PF.OpTouch{q}, now, qs, next)(w) + case False{}: + upd_ok(PF.OpCancel{q}, now, qs, next)(w) + +def kept_poll.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.poll.fin(q, qs, next, now, m))): + match m: + case None{}: + w + case Some{PF.QBody{st, +pexp, eps}}: + match st: + case PF.QRunning{p}: + kept_poll_run.fin(Nat.is_lt(now, pexp), q, qs, next, now, p, eps, w) + case PF.QDone{}: + w + case PF.QCancelled{}: + w + case PF.QFailed{}: + w + +def kept_cancel.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.cancel.fin(q, qs, next, now, m))): + match m: + case None{}: + w + case Some{PF.QBody{st, pexp, eps}}: + upd_ok(PF.OpCancel{q}, now, qs, next)(w) + +def kept_renew_ep.fin(valid: Bool, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, -exp: Nat, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.renew_ep_r(q, tk, qs, next, now, exp, valid))): + match valid: + case True{}: + upd_ok(PF.OpRenew{q, tk}, now, qs, next)(w) + case False{}: + w + +def kept_renew_run.fin(e: Maybe<&2, Nat>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.renew_run(q, tk, qs, next, now, e))): + match e: + case None{}: + w + case Some{+exp}: + kept_renew_ep.fin(Nat.is_lt(now, exp), q, tk, qs, next, now, exp, w) + +def kept_renew.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.Inv_s(PF.state(PF.renew.fin(q, tk, qs, next, now, m))): + match m: + case None{}: + w + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + kept_renew_run.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QDone{}: + kept_renew_run.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QCancelled{}: + w + case PF.QFailed{}: + w + +def Laws.inv_kept(a, qs, next, now, w): + match a: + case PF.AStart{}: + join.fin(Nat.is_lt(next, 1n+next) && Laws.st_ok(PF.QRunning{0n}), Laws.all_ok(qs, 1n+next), + join.fin(Nat.is_lt(next, 1n+next), Laws.st_ok(PF.QRunning{0n}), lt_succ(next), Unit{}), mono(qs, next, w)) + case PF.APoll{+q}: + kept_poll.fin(PF.find(q, qs), q, qs, next, now, w) + case PF.ACancel{+q}: + kept_cancel.fin(PF.find(q, qs), q, qs, next, now, w) + case PF.ADoGet{q, tk}: + w + case PF.ARenew{+q, +tk}: + kept_renew.fin(PF.find(q, qs), q, tk, qs, next, now, w) + case PF.ATick{}: + upd_ok(PF.OpTick{}, 1n+now, qs, next)(w) + case PF.AFail{+q}: + upd_ok(PF.OpFail{q}, now, qs, next)(w) + +# Self-targeted ops +# ----------------- +# an op aimed at q, applied to q's own body, is the plain body change + +def touch_self(+q: Nat, +now: Nat, +body: PF.QBody) -> {PF.touch_body(now, body) == PF.apply(PF.OpTouch{q}, now, q, body) : PF.QBody}: + %eq_refl(q) : {PF.touch_body(now, body) == PF.when_b(_, PF.touch_body(now, body), body) : PF.QBody} + {==} + +def cancel_self(+q: Nat, +now: Nat, +body: PF.QBody) -> {PF.cancel_body(body) == PF.apply(PF.OpCancel{q}, now, q, body) : PF.QBody}: + %eq_refl(q) : {PF.cancel_body(body) == PF.when_b(_, PF.cancel_body(body), body) : PF.QBody} + {==} + +def fail_self(+q: Nat, +now: Nat, +body: PF.QBody) -> {PF.fail_body(body) == PF.apply(PF.OpFail{q}, now, q, body) : PF.QBody}: + %eq_refl(q) : {PF.fail_body(body) == PF.when_b(_, PF.fail_body(body), body) : PF.QBody} + {==} + +def renew_self(+q: Nat, +tk: Nat, +now: Nat, +body: PF.QBody) -> {PF.renew_body(tk, now, body) == PF.apply(PF.OpRenew{q, tk}, now, q, body) : PF.QBody}: + %eq_refl(q) : {PF.renew_body(tk, now, body) == PF.when_b(_, PF.renew_body(tk, now, body), body) : PF.QBody} + {==} + +# Lemmas on endpoints +# ------------------- + +# a list is a prefix of itself +def prefix_refl(xs: List<&2, Nat>) -> Laws.T(Laws.is_prefix(xs, xs)): + match xs: + case Nil{}: + Unit{} + case Con{+x, t}: + join.fin(Nat.is_eq(x, x), Laws.is_prefix(t, t), true_T(Nat.is_eq(x, x), eq_refl(x)), prefix_refl(t)) + +# appending an endpoint keeps the old tickets as a prefix +def prefix_snoc(eps: List<&2, PF.Endpoint>, e: PF.Endpoint) -> Laws.T(Laws.is_prefix(PF.tickets(eps), PF.tickets(PF.snoc(eps, e)))): + match eps: + case Nil{}: + Unit{} + case Con{PF.Endpoint{+tk, exp}, t}: + join.fin(Nat.is_eq(tk, tk), Laws.is_prefix(PF.tickets(t), PF.tickets(PF.snoc(t, e))), true_T(Nat.is_eq(tk, tk), eq_refl(tk)), prefix_snoc(t, e)) + +# renewing keeps the tickets +def tickets_renew(+tk: Nat, +now: Nat, eps: List<&2, PF.Endpoint>) -> {PF.tickets(eps) == PF.tickets(PF.renew_ep(tk, now, eps)) : List<&2, Nat>}: + match eps: + case Nil{}: + {==} + case Con{PF.Endpoint{+etk, +exp}, t}: + %tickets_renew(tk, now, t) : {etk <> PF.tickets(t) == etk <> _ : List<&2, Nat>} + {==} + +def prefix_renew(+tk: Nat, +now: Nat, +eps: List<&2, PF.Endpoint>) -> Laws.T(Laws.is_prefix(PF.tickets(eps), PF.tickets(PF.renew_ep(tk, now, eps)))): + %tickets_renew(tk, now, eps) : Laws.T(Laws.is_prefix(PF.tickets(eps), _)) + prefix_refl(PF.tickets(eps)) + +# an endpoint lookup after a renewal is the renewal of the lookup +def ren_m(+now: Nat, m: Maybe<&2, Nat>) -> Maybe<&2, Nat>: + match m: + case None{}: + None{} + case Some{exp}: + Some{PF.renewed(exp, now)} + +def find_ep_renew.fin(c: Bool, +tk: Nat, +now: Nat, +exp: Nat, -t: List<&2, PF.Endpoint>, + rec: {ren_m(now, PF.find_ep(tk, t)) == PF.find_ep(tk, PF.renew_ep(tk, now, t)) : Maybe<&2, Nat>}) + -> {ren_m(now, PF.pick_n(c, exp, PF.find_ep(tk, t))) == PF.pick_n(c, PF.when_n(c, PF.renewed(exp, now), exp), PF.find_ep(tk, PF.renew_ep(tk, now, t))) : Maybe<&2, Nat>}: + match c: + case True{}: + {==} + case False{}: + rec + +def find_ep_renew(+tk: Nat, +now: Nat, eps: List<&2, PF.Endpoint>) -> {ren_m(now, PF.find_ep(tk, eps)) == PF.find_ep(tk, PF.renew_ep(tk, now, eps)) : Maybe<&2, Nat>}: + match eps: + case Nil{}: + {==} + case Con{PF.Endpoint{+etk, +exp}, t}: + find_ep_renew.fin(Nat.is_eq(tk, etk), tk, now, exp, t, find_ep_renew(tk, now, t)) + +# Progress laws +# ------------- + +def bounded_run.fin(alive: Bool, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +p: Nat, +eps: List<&2, PF.Endpoint>, wp: Laws.T(Nat.is_le(p, PF.FULL()))) + -> Laws.T(Laws.prog_ok(PF.resp(PF.poll_run(q, qs, next, now, p, eps, alive)))): + match alive: + case True{}: + wp + case False{}: + Unit{} + +def bounded.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, wm: Laws.T(mst_ok(m))) + -> Laws.T(Laws.prog_ok(PF.resp(PF.poll.fin(q, qs, next, now, m)))): + match m: + case None{}: + Unit{} + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + bounded_run.fin(Nat.is_lt(now, pexp), q, qs, next, now, p, eps, wm) + case PF.QDone{}: + Unit{} + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +def Laws.progress_bounded(q, qs, next, now, w): + bounded.fin(PF.find(q, qs), q, qs, next, now, find_ok(q, qs, next)(w)) + +# Descriptor laws +# --------------- + +def Laws.unknown_descriptor_rejected(q, qs, next, now, w, u): + %find_unknown(q, qs, next, u)(w) : {PF.resp(PF.poll.fin(q, qs, next, now, _)) == PF.RErr{} : PF.Resp} + {==} + +# after a cancel aimed at q, q's running body is cancelled +def cancelled_after(+q: Nat, +qs: List<&2, PF.Query>, +now: Nat, +p: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>, + e: {Some{PF.QBody{PF.QRunning{p}, pexp, eps}} == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> Laws.T(Laws.mq_cancelled(PF.find(q, PF.upd(PF.OpCancel{q}, now, qs)))): + %find_upd(q, PF.OpCancel{q}, now, qs) : Laws.T(Laws.mq_cancelled(_)) + %e : Laws.T(Laws.mq_cancelled(upd_m(PF.OpCancel{q}, now, q, _))) + %cancel_self(q, now, PF.QBody{PF.QRunning{p}, pexp, eps}) : Laws.T(Laws.mq_cancelled(Some{_})) + Unit{} + +def expired_run.fin(alive: Bool, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +p: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>, + w: Laws.T(Bool.not(alive)), e: {Some{PF.QBody{PF.QRunning{p}, pexp, eps}} == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.poll_run(q, qs, next, now, p, eps, alive)) == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, Laws.queries(PF.state(PF.poll_run(q, qs, next, now, p, eps, alive)))))): + match alive: + case True{}: + Empty.absurd({PF.RPoll{p, Some{q}, PF.tickets(eps)} == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, PF.upd(PF.OpTouch{q}, now, qs)))), w) + case False{}: + ({==}, cancelled_after(q, qs, now, p, pexp, eps, e)) + +def expired.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, + w: Laws.T(Laws.poll_expired(now, m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.poll.fin(q, qs, next, now, m)) == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, Laws.queries(PF.state(PF.poll.fin(q, qs, next, now, m)))))): + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, qs))), w) + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + expired_run.fin(Nat.is_lt(now, pexp), q, qs, next, now, p, pexp, eps, w, e) + case PF.QDone{}: + Empty.absurd({PF.RPoll{PF.FULL(), None{}, PF.tickets(eps)} == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, qs))), w) + case PF.QCancelled{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, qs))), w) + case PF.QFailed{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, qs))), w) + +def Laws.expired_descriptor_rejected(q, qs, next, now, w): + expired.fin(PF.find(q, qs), q, qs, next, now, w, {==}) + +def done.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, + w: Laws.T(Laws.mq_done(m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.poll.fin(q, qs, next, now, m) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp}: + match m: + case None{}: + Empty.absurd({(PF.Server{qs, next, now}, PF.RErr{}) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp}, w) + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + Empty.absurd({PF.poll_run(q, qs, next, now, p, eps, Nat.is_lt(now, pexp)) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp}, w) + case PF.QDone{}: + %e : {(PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, PF.tickets(eps)}) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(_)}) : PF.Server & PF.Resp} + {==} + case PF.QCancelled{}: + Empty.absurd({(PF.Server{qs, next, now}, PF.RErr{}) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp}, w) + case PF.QFailed{}: + Empty.absurd({(PF.Server{qs, next, now}, PF.RErr{}) == (PF.Server{qs, next, now}, PF.RPoll{PF.FULL(), None{}, Laws.tickets_of(PF.find(q, qs))}) : PF.Server & PF.Resp}, w) + +def Laws.done_poll_complete(q, qs, next, now, w): + done.fin(PF.find(q, qs), q, qs, next, now, w, {==}) + +def Laws.fresh_query_polls(qs, next, now): + %eq_refl(next) : {PF.resp(PF.poll.fin(next, PF.Query{next, PF.fresh(now)} <> qs, 1n+next, now, PF.pick_q(_, PF.fresh(now), PF.find(next, qs)))) == PF.RPoll{0n, Some{next}, Nil{}} : PF.Resp} + %pttl_valid(now) : {PF.resp(PF.poll_run(next, PF.Query{next, PF.fresh(now)} <> qs, 1n+next, now, 0n, Nil{}, _)) == PF.RPoll{0n, Some{next}, Nil{}} : PF.Resp} + {==} + +# Cancellation laws +# ----------------- + +def cancel_run.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, + w: Laws.T(Laws.mq_running(m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.cancel.fin(q, qs, next, now, m)) == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, Laws.queries(PF.state(PF.cancel.fin(q, qs, next, now, m)))))): + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, qs))), w) + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + ({==}, cancelled_after(q, qs, now, p, pexp, eps, e)) + case PF.QDone{}: + Empty.absurd({PF.RCancel{PF.CsCancelled{}} == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, PF.upd(PF.OpCancel{q}, now, qs)))), w) + case PF.QCancelled{}: + Empty.absurd({PF.RCancel{PF.CsCancelled{}} == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, PF.upd(PF.OpCancel{q}, now, qs)))), w) + case PF.QFailed{}: + Empty.absurd({PF.RCancel{PF.CsNotCancellable{}} == PF.RCancel{PF.CsCancelled{}} : PF.Resp} & Laws.T(Laws.mq_cancelled(PF.find(q, PF.upd(PF.OpCancel{q}, now, qs)))), w) + +def Laws.cancel_running(q, qs, next, now, w): + cancel_run.fin(PF.find(q, qs), q, qs, next, now, w, {==}) + +# polling a cancelled body is an error, whatever it was before +def cpr_st(st: PF.QState, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> {PF.resp(PF.poll.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, Some{PF.cancel_body(PF.QBody{st, pexp, eps})})) == PF.RErr{} : PF.Resp}: + match st: + case PF.QRunning{p}: + {==} + case PF.QDone{}: + {==} + case PF.QCancelled{}: + {==} + case PF.QFailed{}: + {==} + +def cpr.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.cancel.fin(q, qs, next, now, m)))) == PF.RErr{} : PF.Resp}: + match m: + case None{}: + %e : {PF.resp(PF.poll.fin(q, qs, next, now, _)) == PF.RErr{} : PF.Resp} + {==} + case Some{PF.QBody{+st, +pexp, +eps}}: + %find_upd(q, PF.OpCancel{q}, now, qs) : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, _)) == PF.RErr{} : PF.Resp} + %e : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, upd_m(PF.OpCancel{q}, now, q, _))) == PF.RErr{} : PF.Resp} + %cancel_self(q, now, PF.QBody{st, pexp, eps}) : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, Some{_})) == PF.RErr{} : PF.Resp} + cpr_st(st, q, qs, next, now, pexp, eps) + +def Laws.cancelled_poll_rejected(q, qs, next, now): + cpr.fin(PF.find(q, qs), q, qs, next, now, {==}) + +def cdr_st(st: PF.QState, +tk: Nat, +now: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> {PF.doget.fin(tk, now, Some{PF.cancel_body(PF.QBody{st, pexp, eps})}) == PF.RErr{} : PF.Resp}: + match st: + case PF.QRunning{p}: + {==} + case PF.QDone{}: + {==} + case PF.QCancelled{}: + {==} + case PF.QFailed{}: + {==} + +def cdr.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.cancel.fin(q, qs, next, now, m)))) == PF.RErr{} : PF.Resp}: + match m: + case None{}: + %e : {PF.doget.fin(tk, now, _) == PF.RErr{} : PF.Resp} + {==} + case Some{PF.QBody{+st, +pexp, +eps}}: + %find_upd(q, PF.OpCancel{q}, now, qs) : {PF.doget.fin(tk, now, _) == PF.RErr{} : PF.Resp} + %e : {PF.doget.fin(tk, now, upd_m(PF.OpCancel{q}, now, q, _)) == PF.RErr{} : PF.Resp} + %cancel_self(q, now, PF.QBody{st, pexp, eps}) : {PF.doget.fin(tk, now, Some{_}) == PF.RErr{} : PF.Resp} + cdr_st(st, tk, now, pexp, eps) + +def Laws.cancelled_doget_rejected(q, tk, qs, next, now): + cdr.fin(PF.find(q, qs), q, tk, qs, next, now, {==}) + +def ci_st(st: PF.QState, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> {PF.resp(PF.cancel.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, Some{PF.cancel_body(PF.QBody{st, pexp, eps})})) == PF.resp(PF.cancel.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})) : PF.Resp}: + match st: + case PF.QRunning{p}: + {==} + case PF.QDone{}: + {==} + case PF.QCancelled{}: + {==} + case PF.QFailed{}: + {==} + +def ci.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.ACancel{q}, PF.state(PF.cancel.fin(q, qs, next, now, m)))) == PF.resp(PF.cancel.fin(q, qs, next, now, m)) : PF.Resp}: + match m: + case None{}: + %e : {PF.resp(PF.cancel.fin(q, qs, next, now, _)) == PF.RErr{} : PF.Resp} + {==} + case Some{PF.QBody{+st, +pexp, +eps}}: + %find_upd(q, PF.OpCancel{q}, now, qs) : {PF.resp(PF.cancel.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, _)) == PF.resp(PF.cancel.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})) : PF.Resp} + %e : {PF.resp(PF.cancel.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, upd_m(PF.OpCancel{q}, now, q, _))) == PF.resp(PF.cancel.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})) : PF.Resp} + %cancel_self(q, now, PF.QBody{st, pexp, eps}) : {PF.resp(PF.cancel.fin(q, PF.upd(PF.OpCancel{q}, now, qs), next, now, Some{_})) == PF.resp(PF.cancel.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})) : PF.Resp} + ci_st(st, q, qs, next, now, pexp, eps) + +def Laws.cancel_idempotent(q, qs, next, now): + ci.fin(PF.find(q, qs), q, qs, next, now, {==}) + +def fnc.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.T(Laws.mq_failed(m))) + -> {PF.resp(PF.cancel.fin(q, qs, next, now, m)) == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp}, w) + case Some{PF.QBody{st, pexp, eps}}: + match st: + case PF.QRunning{p}: + Empty.absurd({PF.RCancel{PF.CsCancelled{}} == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp}, w) + case PF.QDone{}: + Empty.absurd({PF.RCancel{PF.CsCancelled{}} == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp}, w) + case PF.QCancelled{}: + Empty.absurd({PF.RCancel{PF.CsCancelled{}} == PF.RCancel{PF.CsNotCancellable{}} : PF.Resp}, w) + case PF.QFailed{}: + {==} + +def Laws.failed_not_cancellable(q, qs, next, now, w): + fnc.fin(PF.find(q, qs), q, qs, next, now, w) + +def fpr.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, + w: Laws.T(Laws.mq_running(m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, PF.find(q, PF.upd(PF.OpFail{q}, now, qs)))) == PF.RErr{} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, PF.find(q, PF.upd(PF.OpFail{q}, now, qs)))) == PF.RErr{} : PF.Resp}, w) + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + %find_upd(q, PF.OpFail{q}, now, qs) : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, _)) == PF.RErr{} : PF.Resp} + %e : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, upd_m(PF.OpFail{q}, now, q, _))) == PF.RErr{} : PF.Resp} + %fail_self(q, now, PF.QBody{PF.QRunning{p}, pexp, eps}) : {PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, Some{_})) == PF.RErr{} : PF.Resp} + {==} + case PF.QDone{}: + Empty.absurd({PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, PF.find(q, PF.upd(PF.OpFail{q}, now, qs)))) == PF.RErr{} : PF.Resp}, w) + case PF.QCancelled{}: + Empty.absurd({PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, PF.find(q, PF.upd(PF.OpFail{q}, now, qs)))) == PF.RErr{} : PF.Resp}, w) + case PF.QFailed{}: + Empty.absurd({PF.resp(PF.poll.fin(q, PF.upd(PF.OpFail{q}, now, qs), next, now, PF.find(q, PF.upd(PF.OpFail{q}, now, qs)))) == PF.RErr{} : PF.Resp}, w) + +def Laws.failed_poll_rejected(q, qs, next, now, w): + fpr.fin(PF.find(q, qs), q, qs, next, now, w, {==}) + +# Endpoint laws +# ------------- + +def dbe_v.fin(valid: Bool, w: Laws.T(valid)) -> {PF.doget_ep(valid) == PF.RData{} : PF.Resp}: + match valid: + case True{}: + {==} + case False{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, w) + +def dbe_ep.fin(e: Maybe<&2, Nat>, +now: Nat, w: Laws.T(Laws.ep_before(now, e))) -> {PF.doget_run(now, e) == PF.RData{} : PF.Resp}: + match e: + case None{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, w) + case Some{+exp}: + dbe_v.fin(Nat.is_lt(now, exp), w) + +def dbe.fin(m: Maybe<&2, PF.QBody>, +tk: Nat, +now: Nat, w: Laws.T(Laws.ep_valid(now, tk, m))) -> {PF.doget.fin(tk, now, m) == PF.RData{} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, w) + case Some{PF.QBody{st, pexp, +eps}}: + match st: + case PF.QRunning{p}: + dbe_ep.fin(PF.find_ep(tk, eps), now, w) + case PF.QDone{}: + dbe_ep.fin(PF.find_ep(tk, eps), now, w) + case PF.QCancelled{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, w) + case PF.QFailed{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, w) + +def Laws.doget_before_expiry(q, tk, qs, next, now, w): + dbe.fin(PF.find(q, qs), tk, now, w) + +def dae_v.fin(valid: Bool, n: Laws.T(Bool.not(valid))) -> {PF.doget_ep(valid) == PF.RErr{} : PF.Resp}: + match valid: + case True{}: + Empty.absurd({PF.RData{} == PF.RErr{} : PF.Resp}, n) + case False{}: + {==} + +def dae_ep.fin(e: Maybe<&2, Nat>, +now: Nat, w: Laws.T(Laws.ep_after(now, e))) -> {PF.doget_run(now, e) == PF.RErr{} : PF.Resp}: + match e: + case None{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp}, w) + case Some{+exp}: + dae_v.fin(Nat.is_lt(now, exp), w) + +def dae.fin(m: Maybe<&2, PF.QBody>, +tk: Nat, +now: Nat, w: Laws.T(Laws.ep_expired(now, tk, m))) -> {PF.doget.fin(tk, now, m) == PF.RErr{} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp}, w) + case Some{PF.QBody{st, pexp, +eps}}: + match st: + case PF.QRunning{p}: + dae_ep.fin(PF.find_ep(tk, eps), now, w) + case PF.QDone{}: + dae_ep.fin(PF.find_ep(tk, eps), now, w) + case PF.QCancelled{}: + {==} + case PF.QFailed{}: + {==} + +def Laws.doget_after_expiry(q, tk, qs, next, now, w): + dae.fin(PF.find(q, qs), tk, now, w) + +def rx_v.fin(valid: Bool, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +exp: Nat, w: Laws.T(valid)) + -> Laws.T(Laws.ren_later(Some{exp}, PF.resp(PF.renew_ep_r(q, tk, qs, next, now, exp, valid)))): + match valid: + case True{}: + renewed_later(exp, now) + case False{}: + Empty.absurd(Laws.T(Laws.ren_later(Some{exp}, PF.RErr{})), w) + +def rx_ep.fin(e: Maybe<&2, Nat>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.T(Laws.ep_before(now, e))) + -> Laws.T(Laws.ren_later(e, PF.resp(PF.renew_run(q, tk, qs, next, now, e)))): + match e: + case None{}: + Empty.absurd(Laws.T(Laws.ren_later(None{}, PF.RErr{})), w) + case Some{+exp}: + rx_v.fin(Nat.is_lt(now, exp), q, tk, qs, next, now, exp, w) + +def rx.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.T(Laws.ep_valid(now, tk, m))) + -> Laws.T(Laws.ren_later(Laws.exp_of(tk, m), PF.resp(PF.renew.fin(q, tk, qs, next, now, m)))): + match m: + case None{}: + Empty.absurd(Laws.T(Laws.ren_later(None{}, PF.RErr{})), w) + case Some{PF.QBody{st, pexp, +eps}}: + match st: + case PF.QRunning{p}: + rx_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QDone{}: + rx_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QCancelled{}: + Empty.absurd(Laws.T(Laws.ren_later(PF.find_ep(tk, eps), PF.RErr{})), w) + case PF.QFailed{}: + Empty.absurd(Laws.T(Laws.ren_later(PF.find_ep(tk, eps), PF.RErr{})), w) + +def Laws.renew_extends(q, tk, qs, next, now, w): + rx.fin(PF.find(q, qs), q, tk, qs, next, now, w) + +def rr_v.fin(valid: Bool, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +exp: Nat, n: Laws.T(Bool.not(valid))) + -> {PF.resp(PF.renew_ep_r(q, tk, qs, next, now, exp, valid)) == PF.RErr{} : PF.Resp}: + match valid: + case True{}: + Empty.absurd({PF.REndpoint{tk, PF.renewed(exp, now)} == PF.RErr{} : PF.Resp}, n) + case False{}: + {==} + +def rr_ep.fin(e: Maybe<&2, Nat>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.T(Laws.ep_after(now, e))) + -> {PF.resp(PF.renew_run(q, tk, qs, next, now, e)) == PF.RErr{} : PF.Resp}: + match e: + case None{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp}, w) + case Some{+exp}: + rr_v.fin(Nat.is_lt(now, exp), q, tk, qs, next, now, exp, w) + +def rr.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.T(Laws.ep_expired(now, tk, m))) + -> {PF.resp(PF.renew.fin(q, tk, qs, next, now, m)) == PF.RErr{} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.RErr{} == PF.RErr{} : PF.Resp}, w) + case Some{PF.QBody{st, pexp, +eps}}: + match st: + case PF.QRunning{p}: + rr_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QDone{}: + rr_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, w) + case PF.QCancelled{}: + {==} + case PF.QFailed{}: + {==} + +def Laws.renew_expired_rejected(q, tk, qs, next, now, w): + rr.fin(PF.find(q, qs), q, tk, qs, next, now, w) + +# DoGet on the renewed body, over the query's state +def rdo_st(st: PF.QState, +tk: Nat, +now: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>, +exp: Nat, + wl: Laws.T(Laws.st_live(st)), ee: {Some{exp} == PF.find_ep(tk, eps) : Maybe<&2, Nat>}) + -> {PF.doget.fin(tk, now, Some{PF.QBody{st, pexp, PF.renew_ep(tk, now, eps)}}) == PF.RData{} : PF.Resp}: + match st: + case PF.QRunning{p}: + %find_ep_renew(tk, now, eps) : {PF.doget_run(now, _) == PF.RData{} : PF.Resp} + %ee : {PF.doget_run(now, ren_m(now, _)) == PF.RData{} : PF.Resp} + %T_true(Nat.is_lt(now, PF.renewed(exp, now)), renewed_valid(exp, now)) : {PF.doget_ep(_) == PF.RData{} : PF.Resp} + {==} + case PF.QDone{}: + %find_ep_renew(tk, now, eps) : {PF.doget_run(now, _) == PF.RData{} : PF.Resp} + %ee : {PF.doget_run(now, ren_m(now, _)) == PF.RData{} : PF.Resp} + %T_true(Nat.is_lt(now, PF.renewed(exp, now)), renewed_valid(exp, now)) : {PF.doget_ep(_) == PF.RData{} : PF.Resp} + {==} + case PF.QCancelled{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, wl) + case PF.QFailed{}: + Empty.absurd({PF.RErr{} == PF.RData{} : PF.Resp}, wl) + +def rdo_v.fin(valid: Bool, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>, +exp: Nat, + w: Laws.T(valid), wl: Laws.T(Laws.st_live(st)), ee: {Some{exp} == PF.find_ep(tk, eps) : Maybe<&2, Nat>}, e: {Some{PF.QBody{st, pexp, eps}} == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.renew_ep_r(q, tk, qs, next, now, exp, valid)))) == PF.RData{} : PF.Resp}: + match valid: + case True{}: + %find_upd(q, PF.OpRenew{q, tk}, now, qs) : {PF.doget.fin(tk, now, _) == PF.RData{} : PF.Resp} + %e : {PF.doget.fin(tk, now, upd_m(PF.OpRenew{q, tk}, now, q, _)) == PF.RData{} : PF.Resp} + %renew_self(q, tk, now, PF.QBody{st, pexp, eps}) : {PF.doget.fin(tk, now, Some{_}) == PF.RData{} : PF.Resp} + rdo_st(st, tk, now, pexp, eps, exp, wl, ee) + case False{}: + Empty.absurd({PF.doget.fin(tk, now, PF.find(q, qs)) == PF.RData{} : PF.Resp}, w) + +def rdo_ep.fin(ep: Maybe<&2, Nat>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>, + w: Laws.T(Laws.ep_before(now, ep)), wl: Laws.T(Laws.st_live(st)), ee: {ep == PF.find_ep(tk, eps) : Maybe<&2, Nat>}, e: {Some{PF.QBody{st, pexp, eps}} == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.renew_run(q, tk, qs, next, now, ep)))) == PF.RData{} : PF.Resp}: + match ep: + case None{}: + Empty.absurd({PF.doget.fin(tk, now, PF.find(q, qs)) == PF.RData{} : PF.Resp}, w) + case Some{+exp}: + rdo_v.fin(Nat.is_lt(now, exp), q, tk, qs, next, now, st, pexp, eps, exp, w, wl, ee, e) + +def rdo.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +tk: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, + w: Laws.T(Laws.ep_valid(now, tk, m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> {PF.resp(PF.step_s(PF.ADoGet{q, tk}, PF.state(PF.renew.fin(q, tk, qs, next, now, m)))) == PF.RData{} : PF.Resp}: + match m: + case None{}: + Empty.absurd({PF.doget.fin(tk, now, PF.find(q, qs)) == PF.RData{} : PF.Resp}, w) + case Some{PF.QBody{st, +pexp, +eps}}: + match st: + case PF.QRunning{+p}: + rdo_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, PF.QRunning{p}, pexp, eps, w, Unit{}, {==}, e) + case PF.QDone{}: + rdo_ep.fin(PF.find_ep(tk, eps), q, tk, qs, next, now, PF.QDone{}, pexp, eps, w, Unit{}, {==}, e) + case PF.QCancelled{}: + Empty.absurd({PF.doget.fin(tk, now, PF.find(q, qs)) == PF.RData{} : PF.Resp}, w) + case PF.QFailed{}: + Empty.absurd({PF.doget.fin(tk, now, PF.find(q, qs)) == PF.RData{} : PF.Resp}, w) + +def Laws.renewed_doget_ok(q, tk, qs, next, now, w): + rdo.fin(PF.find(q, qs), q, tk, qs, next, now, w, {==}) + +# Sample traces +# ------------- + +def Laws.trace_doget_fresh(): + {==} + +def Laws.trace_doget_expired(): + {==} + +def Laws.trace_completes(): + {==} + +# Monotonicity +# ------------ +# poll_monotone: a poll of q, any one request, and a poll of q again. +# The second poll sees either the same list (DoGet, a poll or cancel or +# renew that found nothing), the list with a new query in front +# (Start), or the list after one upd (everything else). For an upd, +# find_upd turns the second lookup into apply on the first lookup's +# body, and mono_apply is a case analysis on the op and the state. + +# a PollInfo is at least itself +def mono_refl(r: PF.Resp) -> Laws.T(Laws.Resp.mono(r, r)): + match r: + case PF.RPoll{+p, d, +i}: + join.fin(Nat.is_le(p, p), Laws.is_prefix(i, i), le_refl(p), prefix_refl(i)) + case PF.RCancel{c}: + Unit{} + case PF.RData{}: + Unit{} + case PF.REndpoint{tk, exp}: + Unit{} + case PF.RAck{}: + Unit{} + case PF.RErr{}: + Unit{} + +# two polls of running bodies, over both liveness verdicts +def mono_run2.fin(a1: Bool, a2: Bool, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, + +p1: Nat, +p2: Nat, +eps1: List<&2, PF.Endpoint>, +eps2: List<&2, PF.Endpoint>, + wp: Laws.T(Nat.is_le(p1, p2)), wi: Laws.T(Laws.is_prefix(PF.tickets(eps1), PF.tickets(eps2)))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll_run(q, qs1, next1, now1, p1, eps1, a1)), PF.resp(PF.poll_run(q, qs2, next2, now2, p2, eps2, a2)))): + match a1 a2: + case True{} True{}: + join.fin(Nat.is_le(p1, p2), Laws.is_prefix(PF.tickets(eps1), PF.tickets(eps2)), wp, wi) + case True{} False{}: + Unit{} + case False{} True{}: + Unit{} + case False{} False{}: + Unit{} + +# a poll of a running body against an error +def mono_run_err.fin(a1: Bool, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +p1: Nat, +eps1: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll_run(q, qs1, next1, now1, p1, eps1, a1)), PF.RErr{})): + match a1: + case True{}: + Unit{} + case False{}: + Unit{} + +# a poll of a running body against a complete one +def mono_run_done.fin(a1: Bool, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +p1: Nat, +eps1: List<&2, PF.Endpoint>, +eps2: List<&2, PF.Endpoint>, + wp: Laws.T(Nat.is_le(p1, PF.FULL())), wi: Laws.T(Laws.is_prefix(PF.tickets(eps1), PF.tickets(eps2)))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll_run(q, qs1, next1, now1, p1, eps1, a1)), PF.RPoll{PF.FULL(), None{}, PF.tickets(eps2)})): + match a1: + case True{}: + join.fin(Nat.is_le(p1, PF.FULL()), Laws.is_prefix(PF.tickets(eps1), PF.tickets(eps2)), wp, wi) + case False{}: + Unit{} + +# the same body polled twice, from any two states +def mono_same(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.QBody{st, pexp, eps}})))): + match st: + case PF.QRunning{+p}: + mono_run2.fin(Nat.is_lt(now1, pexp), Nat.is_lt(now2, pexp), q, qs1, next1, now1, qs2, next2, now2, p, p, eps, eps, le_refl(p), prefix_refl(PF.tickets(eps))) + case PF.QDone{}: + prefix_refl(PF.tickets(eps)) + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +def mono_same_m(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, m: Maybe<&2, PF.QBody>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, m)), PF.resp(PF.poll.fin(q, qs2, next2, now2, m)))): + match m: + case None{}: + Unit{} + case Some{PF.QBody{+st, +pexp, +eps}}: + mono_same(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps) + +# the body after a tick, over the verdict c of is_lt(p + STEP, FULL) +def mono_tick_run.fin(c: Bool, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, + +p: Nat, +pexp: Nat, +eps: List<&2, PF.Endpoint>, wm: Laws.T(Nat.is_le(p, PF.FULL()))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll_run(q, qs1, next1, now1, p, eps, Nat.is_lt(now1, pexp))), + PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.QBody{PF.advance(Nat.add(p, PF.STEP()), c), pexp, PF.snoc(eps, PF.Endpoint{PF.length(eps), Nat.add(PF.ETTL(), now2)})}})))): + match c: + case True{}: + mono_run2.fin(Nat.is_lt(now1, pexp), Nat.is_lt(now2, pexp), q, qs1, next1, now1, qs2, next2, now2, p, Nat.add(p, PF.STEP()), + eps, PF.snoc(eps, PF.Endpoint{PF.length(eps), Nat.add(PF.ETTL(), now2)}), le_add(p, PF.STEP()), prefix_snoc(eps, PF.Endpoint{PF.length(eps), Nat.add(PF.ETTL(), now2)})) + case False{}: + mono_run_done.fin(Nat.is_lt(now1, pexp), q, qs1, next1, now1, p, eps, PF.snoc(eps, PF.Endpoint{PF.length(eps), Nat.add(PF.ETTL(), now2)}), + wm, prefix_snoc(eps, PF.Endpoint{PF.length(eps), Nat.add(PF.ETTL(), now2)})) + +def mono_tick(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>, wm: Laws.T(Laws.st_ok(st))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.tick_body(now2, PF.QBody{st, pexp, eps})})))): + match st: + case PF.QRunning{+p}: + mono_tick_run.fin(Nat.is_lt(Nat.add(p, PF.STEP()), PF.FULL()), q, qs1, next1, now1, qs2, next2, now2, p, pexp, eps, wm) + case PF.QDone{}: + prefix_refl(PF.tickets(eps)) + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# the body after a touch: its descriptor is valid again +def mono_touch(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.touch_body(now2, PF.QBody{st, pexp, eps})})))): + match st: + case PF.QRunning{+p}: + %pttl_valid(now2) : Laws.T(Laws.Resp.mono(PF.resp(PF.poll_run(q, qs1, next1, now1, p, eps, Nat.is_lt(now1, pexp))), PF.resp(PF.poll_run(q, qs2, next2, now2, p, eps, _)))) + mono_run2.fin(Nat.is_lt(now1, pexp), True{}, q, qs1, next1, now1, qs2, next2, now2, p, p, eps, eps, le_refl(p), prefix_refl(PF.tickets(eps))) + case PF.QDone{}: + prefix_refl(PF.tickets(eps)) + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# the body after a cancel: an error, or unchanged +def mono_cancel_b(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.cancel_body(PF.QBody{st, pexp, eps})})))): + match st: + case PF.QRunning{+p}: + mono_run_err.fin(Nat.is_lt(now1, pexp), q, qs1, next1, now1, p, eps) + case PF.QDone{}: + Unit{} + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# the body after a failure: an error, or unchanged +def mono_fail_b(+q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.fail_body(PF.QBody{st, pexp, eps})})))): + match st: + case PF.QRunning{+p}: + mono_run_err.fin(Nat.is_lt(now1, pexp), q, qs1, next1, now1, p, eps) + case PF.QDone{}: + prefix_refl(PF.tickets(eps)) + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# the body after a renewal: the same tickets +def mono_renew_b(+q: Nat, +tk: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.renew_body(tk, now2, PF.QBody{st, pexp, eps})})))): + match st: + case PF.QRunning{+p}: + mono_run2.fin(Nat.is_lt(now1, pexp), Nat.is_lt(now2, pexp), q, qs1, next1, now1, qs2, next2, now2, p, p, eps, PF.renew_ep(tk, now2, eps), le_refl(p), prefix_renew(tk, now2, eps)) + case PF.QDone{}: + prefix_renew(tk, now2, eps) + case PF.QCancelled{}: + Unit{} + case PF.QFailed{}: + Unit{} + +# a targeted op changed q's body or left it alone, over the verdict c of its id test +def mono_when.fin(c: Bool, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, +st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>, +new: PF.QBody, + wn: Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{new}))))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.when_b(c, new, PF.QBody{st, pexp, eps})})))): + match c: + case True{}: + wn + case False{}: + mono_same(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps) + +# every op: the second poll is at least the first +def mono_apply(op: PF.Op, +q: Nat, +qs1: List<&2, PF.Query>, +next1: Nat, +now1: Nat, +qs2: List<&2, PF.Query>, +next2: Nat, +now2: Nat, +st: PF.QState, +pexp: Nat, +eps: List<&2, PF.Endpoint>, wm: Laws.T(Laws.st_ok(st))) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs1, next1, now1, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, qs2, next2, now2, Some{PF.apply(op, now2, q, PF.QBody{st, pexp, eps})})))): + match op: + case PF.OpTick{}: + mono_tick(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps, wm) + case PF.OpTouch{q2}: + mono_when.fin(Nat.is_eq(q2, q), q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps, PF.touch_body(now2, PF.QBody{st, pexp, eps}), + mono_touch(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps)) + case PF.OpCancel{q2}: + mono_when.fin(Nat.is_eq(q2, q), q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps, PF.cancel_body(PF.QBody{st, pexp, eps}), + mono_cancel_b(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps)) + case PF.OpFail{q2}: + mono_when.fin(Nat.is_eq(q2, q), q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps, PF.fail_body(PF.QBody{st, pexp, eps}), + mono_fail_b(q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps)) + case PF.OpRenew{q2, +tk}: + mono_when.fin(Nat.is_eq(q2, q), q, qs1, next1, now1, qs2, next2, now2, st, pexp, eps, PF.renew_body(tk, now2, PF.QBody{st, pexp, eps}), + mono_renew_b(q, tk, qs1, next1, now1, qs2, next2, now2, st, pexp, eps)) + +# a poll before and after an update of the query list +def mono_upd.fin(m: Maybe<&2, PF.QBody>, +q: Nat, +op: PF.Op, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +now2: Nat, + wm: Laws.T(mst_ok(m)), e: {m == PF.find(q, qs) : Maybe<&2, PF.QBody>}) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs, next, now, m)), PF.resp(PF.poll.fin(q, PF.upd(op, now2, qs), next, now2, PF.find(q, PF.upd(op, now2, qs)))))): + match m: + case None{}: + Unit{} + case Some{PF.QBody{+st, +pexp, +eps}}: + %find_upd(q, op, now2, qs) : Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, PF.upd(op, now2, qs), next, now2, _)))) + %e : Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs, next, now, Some{PF.QBody{st, pexp, eps}})), PF.resp(PF.poll.fin(q, PF.upd(op, now2, qs), next, now2, upd_m(op, now2, q, _))))) + mono_apply(op, q, qs, next, now, PF.upd(op, now2, qs), next, now2, st, pexp, eps, wm) + +def mono_upd(+q: Nat, +op: PF.Op, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +now2: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.poll(q, PF.upd(op, now2, qs), next, now2)))): + mono_upd.fin(PF.find(q, qs), q, op, qs, next, now, now2, find_ok(q, qs, next)(w), {==}) + +# the intermediate request is a poll of q2 +def mono_poll_run.fin(alive: Bool, +q2: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +p2: Nat, +eps2: List<&2, PF.Endpoint>, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.poll_run(q2, qs, next, now, p2, eps2, alive)))))): + match alive: + case True{}: + mono_upd(q, PF.OpTouch{q2}, qs, next, now, now, w) + case False{}: + mono_upd(q, PF.OpCancel{q2}, qs, next, now, now, w) + +def mono_poll.fin(m2: Maybe<&2, PF.QBody>, +q2: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.poll.fin(q2, qs, next, now, m2)))))): + match m2: + case None{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case Some{PF.QBody{st2, +pexp2, +eps2}}: + match st2: + case PF.QRunning{+p2}: + mono_poll_run.fin(Nat.is_lt(now, pexp2), q2, q, qs, next, now, p2, eps2, w) + case PF.QDone{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case PF.QCancelled{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case PF.QFailed{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + +# the intermediate request is a cancel of q2 +def mono_cancel.fin(m2: Maybe<&2, PF.QBody>, +q2: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.cancel.fin(q2, qs, next, now, m2)))))): + match m2: + case None{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case Some{PF.QBody{st2, pexp2, eps2}}: + mono_upd(q, PF.OpCancel{q2}, qs, next, now, now, w) + +# the intermediate request is a renewal of (q2, tk) +def mono_renew_v.fin(valid: Bool, +q2: Nat, +tk: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, +exp: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.renew_ep_r(q2, tk, qs, next, now, exp, valid)))))): + match valid: + case True{}: + mono_upd(q, PF.OpRenew{q2, tk}, qs, next, now, now, w) + case False{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + +def mono_renew_ep.fin(ep: Maybe<&2, Nat>, +q2: Nat, +tk: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.renew_run(q2, tk, qs, next, now, ep)))))): + match ep: + case None{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case Some{+exp}: + mono_renew_v.fin(Nat.is_lt(now, exp), q2, tk, q, qs, next, now, exp, w) + +def mono_renew.fin(m2: Maybe<&2, PF.QBody>, +q2: Nat, +tk: Nat, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.step_s(PF.APoll{q}, PF.state(PF.renew.fin(q2, tk, qs, next, now, m2)))))): + match m2: + case None{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case Some{PF.QBody{st2, pexp2, +eps2}}: + match st2: + case PF.QRunning{p2}: + mono_renew_ep.fin(PF.find_ep(tk, eps2), q2, tk, q, qs, next, now, w) + case PF.QDone{}: + mono_renew_ep.fin(PF.find_ep(tk, eps2), q2, tk, q, qs, next, now, w) + case PF.QCancelled{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case PF.QFailed{}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + +# next <= q from q == next +def le_of_eq(+q: Nat, +next: Nat, eqn: {q == next : Nat}) -> Laws.T(Nat.is_le(next, q)): + %eqn : Laws.T(Nat.is_le(_, q)) + le_refl(q) + +# the intermediate request is a start: the new query is q itself (then +# the first poll found nothing, by freshness) or another one +def mono_start.fin(c: Bool, +q: Nat, +qs: List<&2, PF.Query>, +next: Nat, +now: Nat, e: {c == Nat.is_eq(q, next) : Bool}, w: Laws.Inv(qs, next)) + -> Laws.T(Laws.Resp.mono(PF.resp(PF.poll(q, qs, next, now)), PF.resp(PF.poll.fin(q, PF.Query{next, PF.fresh(now)} <> qs, 1n+next, now, PF.pick_q(c, PF.fresh(now), PF.find(q, qs)))))): + match c: + case True{}: + %find_unknown(q, qs, next, le_of_eq(q, next, eq_sound(q, next, e)))(w) : Laws.T(Laws.Resp.mono(PF.resp(PF.poll.fin(q, qs, next, now, _)), PF.resp(PF.poll.fin(q, PF.Query{next, PF.fresh(now)} <> qs, 1n+next, now, Some{PF.fresh(now)})))) + Unit{} + case False{}: + mono_same_m(q, qs, next, now, PF.Query{next, PF.fresh(now)} <> qs, 1n+next, now, PF.find(q, qs)) + +def Laws.poll_monotone(a, q, qs, next, now, w): + match a: + case PF.AStart{}: + mono_start.fin(Nat.is_eq(q, next), q, qs, next, now, {==}, w) + case PF.APoll{+q2}: + mono_poll.fin(PF.find(q2, qs), q2, q, qs, next, now, w) + case PF.ACancel{+q2}: + mono_cancel.fin(PF.find(q2, qs), q2, q, qs, next, now, w) + case PF.ADoGet{q2, tk}: + mono_refl(PF.resp(PF.poll(q, qs, next, now))) + case PF.ARenew{+q2, +tk}: + mono_renew.fin(PF.find(q2, qs), q2, tk, q, qs, next, now, w) + case PF.ATick{}: + mono_upd(q, PF.OpTick{}, qs, next, now, 1n+now, w) + case PF.AFail{+q2}: + mono_upd(q, PF.OpFail{q2}, qs, next, now, now, w) diff --git a/dev/bend2/poll_flight_info/README.md b/dev/bend2/poll_flight_info/README.md new file mode 100644 index 0000000000..42709a49a1 --- /dev/null +++ b/dev/bend2/poll_flight_info/README.md @@ -0,0 +1,268 @@ + + +# Bend 2 proof of concept: PollFlightInfo and endpoint expiry + +A checked [Bend 2](https://github.com/bendlang/bend) model of the Arrow +Flight long-running query protocol: the `PollFlightInfo` RPC and its +`PollInfo` message, `FlightEndpoint.expiration_time`, and the +`RenewFlightEndpoint` and `CancelFlightInfo` actions. The protocol's +"must" and "should" sentences from `arrow-format/Flight.proto` and +`docs/source/format/Flight.rst` are stated as laws in `LAWS.bend` and +proven against the model in `PROOF.bend`; `bend PROOF.bend` refuses to +pass while any law is unproven or false. + +This follows the layout and proof kit of the prepared-statement model +in `dev/bend2/prepared_statement/` (research branch). Written against +Bend 2.0.21, commit `6018e28` of bendlang/bend, on 2026-09-20. + +| File | Lines | Content | +| --- | ---: | --- | +| `main.bend` | 540 | the model, plus a runnable sample trace in `main` | +| `LAWS.bend` | 522 | 22 laws, each with the spec sentence it comes from, and the laws that cannot be stated | +| `PROOF.bend` | 1321 | the proofs and the lemma library they need | + +## 1. What is modelled + +The server is `Server{qs, next, now}`: a list of queries, the next +query id to issue, and a clock. A query is `Query{id, body}` with +`QBody{st, pexp, eps}`: its state, the tick at which its poll +descriptor expires, and its endpoints in creation order. States are +`QRunning{progress}`, `QDone{}`, `QCancelled{}` and `QFailed{}`. An +endpoint is `Endpoint{tk, exp}`: a ticket index and an expiry tick. + +Requests (`Act`) map onto the Flight RPCs and actions: + +| Request | Flight operation | Effect in the model | +| --- | --- | --- | +| `AStart{}` | `PollFlightInfo` with an original descriptor | starts query `next`, running at progress 0, descriptor valid for `PTTL` ticks; answers `PollInfo` with descriptor `next` | +| `APoll{q}` | `PollFlightInfo` with `PollInfo.flight_descriptor` | running: answers progress, descriptor and endpoints, refreshes the descriptor expiry; expired descriptor: error and the query is cancelled; complete: complete info, descriptor unset; cancelled or failed: error | +| `ACancel{q}` | `DoAction CancelFlightInfo` | running or complete: `CANCELLED`, query becomes cancelled; failed: `NOT_CANCELLABLE`; unknown: error | +| `ADoGet{q, tk}` | `DoGet` | streams while the query is running or complete and `now < exp`; error otherwise; the state is unchanged | +| `ARenew{q, tk}` | `DoAction RenewFlightEndpoint` | a still-valid endpoint of a running or complete query gets expiry `1 + max(exp, now + ETTL)`; expired, unknown, cancelled or failed: error | +| `ATick{}` | the clock | `now + 1`; every running query gains `STEP` progress (completing when it would reach `FULL`) and one new endpoint valid for `ETTL` ticks | +| `AFail{q}` | the query's execution fails | running becomes failed | + +Abstractions forced by Bend (no U64, no F64, no timestamps, F32 +axiomatic): time is a `Nat` tick advanced by `ATick`; progress is a +`Nat` out of `FULL() = 100` with `STEP() = 25`; the poll descriptor of a +query is its id, as `PollFlightInfoProducer` encodes it into command +bytes; a ticket is the pair (query id, endpoint index), as +`ExpirationTimeProducer` encodes the index into the ticket. + +Decisions taken where the spec leaves room, and why: + +- **Cancelling a complete query answers `CANCELLED`** and its endpoints + stop streaming. Flight.rst says of a complete `FlightInfo` that "the + client may be able to cancel the returned FlightInfo by + CancelFlightInfo action", and the Java integration scenario + `ExpirationTimeCancelFlightInfoScenario` cancels the info returned by + `GetFlightInfo`, expects `CANCELLED`, and then expects every `DoGet` + to fail. `NOT_CANCELLABLE` is answered for a failed query, which has + nothing left to cancel. `CANCELLING` needs asynchronous cancellation + and is not produced; `UNSPECIFIED` is discouraged by the proto. +- **Cancelling twice answers `CANCELLED` again.** The proto allows + "CANCELLED or a NOT_FOUND error"; the model picks the idempotent + answer. (`ExpirationTimeProducer` answers `NOT_CANCELLABLE` here, + which the proto text does not list.) +- **Re-sending the original descriptor starts a new query** rather than + polling the old one, because the proto says `PollFlightInfo` with a + descriptor "start[s] a query"; that is `AStart`. The law about using + the wrong descriptor is therefore about descriptors the server never + issued (`unknown_descriptor_rejected`) and expired ones + (`expired_descriptor_rejected`). +- **An endpoint is valid while `now < exp`**, reading "until the + expiration time is reached" as exclusive. (The Java producer uses + `Instant.now().isAfter(expirationTime)`, which is inclusive; the + difference is one tick and the laws would go through either way.) +- **Renewal requires a still-valid endpoint**, since the server may have + released an expired endpoint's data. The Java producer renews + unconditionally; that reading would drop `renew_expired_rejected`. +- **Polling an expired descriptor cancels the query**, following "the + query may be cancelled" in the proto. + +## 2. The laws + +All 22 laws below are proven; `bend PROOF.bend` prints +`All terms check.` in 0.3 s. Laws over arbitrary states quantify over +every `qs`, `next` and `now`, and where they need the invariant they +assume it (`Inv`: every id is below the counter and every running +progress is at most `FULL`); `inv_start` and `inv_kept` show every +reachable state satisfies it. + +| Law | Source sentence | Claim | +| --- | --- | --- | +| `inv_start`, `inv_kept` | (invariant, task item 7) | the initial state is fresh and bounded, and every request keeps it so | +| `progress_bounded` | proto `PollInfo.progress`: "If known, must be in [0.0, 1.0]" | a `PollInfo`'s progress is at most `FULL` | +| `poll_monotone` | proto `PollInfo.info`: "Subsequent PollInfo responses may only append new endpoints to info"; and, stronger than the proto ("need not be monotonic or nondecreasing"), this server's progress never decreases | poll `q`, let any one request happen, poll `q` again: the second `PollInfo` has at least the progress of the first and its endpoints as a prefix; vacuous when either poll is an error | +| `unknown_descriptor_rejected` | Flight.rst: "The client should use the descriptor (not the original FlightDescriptor)" | a descriptor at or above the counter is an error | +| `expired_descriptor_rejected` | proto `PollFlightInfo`: "A client can't use PollInfo.flight_descriptor after PollInfo.expiration_time passes ... the query may be cancelled" | polling an expired descriptor is an error and the query is cancelled | +| `done_poll_complete` | proto `PollInfo.flight_descriptor`: "If unset, the query is complete"; `PollInfo.info`: "'info' specifies all results" | polling a complete query answers `FULL`, no descriptor and every endpoint, and leaves the server unchanged | +| `fresh_query_polls` | (anti-vacuity) | the descriptor a start returns polls successfully with progress 0 and no endpoints | +| `cancel_running` | proto `CancelStatus`: "CANCELLED ... The cancellation request is complete" | cancelling a running query answers `CANCELLED` and the query is cancelled | +| `cancelled_poll_rejected` | proto `PollFlightInfo`: "A client may use the CancelFlightInfo action ... to cancel the running query" | after a cancel, polling the query is an error, from any state | +| `cancelled_doget_rejected` | `ExpirationTimeProducer`: "The client can't read data from endpoints even within 6 seconds after the action" | after a cancel, `DoGet` on any endpoint of the query is an error | +| `cancel_idempotent` | proto `CancelStatus`: "Subsequent requests with the same payload may return CANCELLED" | cancelling twice answers the same as once, from any state | +| `failed_not_cancellable` | proto `CancelStatus`: "NOT_CANCELLABLE ... The query is not cancellable" | cancelling a failed query answers `NOT_CANCELLABLE` | +| `failed_poll_rejected` | Flight.rst: "A server should return an error status instead of a response if the query fails" | after a running query fails, polling it is an error | +| `doget_before_expiry` | Flight.rst: "the client can get data multiple times by DoGet until the expiration time is reached" | before the expiry tick, `DoGet` streams (and does not change the state, so it streams again) | +| `doget_after_expiry` | same sentence | at or after the expiry tick, `DoGet` is an error | +| `renew_extends` | Flight.rst: "the client may be able to extend the expiration time by RenewFlightEndpoint"; Java scenario: "Renewed FlightEndpoint must have newer expiration time" | renewing a valid endpoint answers an endpoint whose expiry is strictly later | +| `renew_expired_rejected` | (model decision, above) | renewing an expired endpoint is an error | +| `renewed_doget_ok` | `ExpirationTimeProducer`: "The client can read data from endpoints multiple times within more 10 seconds after the action" | after a renewal, `DoGet` on the renewed endpoint streams | +| `trace_doget_fresh` | (anti-vacuity, task item 6) | start, poll, tick, poll, `DoGet` on the fresh endpoint before expiry streams | +| `trace_doget_expired` | | the same endpoint two ticks later is expired | +| `trace_completes` | | four ticks complete the query; the poll then has no descriptor and lists four endpoints | + +The last three are closed traces, proven by computation (`{==}`); they +double as executable tests of the model. + +### Not expressible or not proven + +Kept in `LAWS.bend` as comments with the reason: + +- **NOT EXPRESSIBLE** "A server should not respond until the result + would be different from last time" and "The first PollFlightInfo call + should return as quickly as possible" (proto). Both are about *when* + the RPC returns. The model is a pure function from state and request + to response, with no notion of blocking or elapsed time within a + call, so neither sentence has a statement. +- **NOT EXPRESSIBLE** `progress` as a `double` in `[0.0, 1.0]`. Bend has + no F64 and its F32 is axiomatic, so nothing about floats can be + proven. `progress_bounded` is the `Nat`-out-of-100 form. +- **NOT EXPRESSIBLE** `expiration_time` as a `google.protobuf.Timestamp` + (int64 seconds and int32 nanos) against a wall clock. Bend has no + 64-bit integers and no clock the checker can reason about. Time is a + tick advanced by an explicit request. +- **NOT PROVEN** `poll_monotone_trace`, the form of `poll_monotone` with + an arbitrary list of requests between the two polls. It follows from + the one-step law by induction once two more invariants are proven: + an issued id is never forgotten, and `QCancelled`/`QFailed` are + absorbing, so an error between two `PollInfo`s cannot occur. Both are + true of the model; they were not proven in this session, so the + one-step law with an arbitrary intermediate request is what is + checked. + +## 3. How to run + +The Bend 2 installer host was not reachable from the environment, so +the checker was run from a clone of the repository with bun: + +```sh +git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend +BEND="bun /tmp/bend/bend2/main.ts" +cd dev/bend2/poll_flight_info +$BEND PROOF.bend # checks LAWS.bend against main.bend: "All terms check." +$BEND main.bend # runs the sample trace in main +$BEND main.bend -o out.js # JavaScript; node out.js +$BEND main.bend -o out # native binary via clang; ./out +``` + +## 4. Results + +`bend PROOF.bend` prints `All terms check.` in 0.34 s wall time. The +JavaScript target builds to a 32 KB file and the native target to a +1.1 MB binary in 6.7 s; both run the sample trace in `main` and print, +one line per request: + +``` +PollInfo(progress=0/100, descriptor=0, tickets=[]) AStart +PollInfo(progress=0/100, descriptor=0, tickets=[]) APoll 0 +Ack ATick +PollInfo(progress=25/100, descriptor=0, tickets=[0 ]) APoll 0 +Data ADoGet (0, 0) now=1 < exp=3 +FlightEndpoint(ticket=0, expires=4) ARenew (0, 0) 1 + max(3, 1 + 2) +Ack ATick +Ack ATick +Data ADoGet (0, 0) now=3 < exp=4, renewed +CancelFlightInfoResult(CANCELLED) ACancel 0 +Err ADoGet (0, 0) cancelled +CancelFlightInfoResult(CANCELLED) ACancel 0 idempotent +Err APoll 0 cancelled +``` + +### Mutation tests + +Seven bugs were introduced into `main.bend` one at a time, the check +was run, and the file restored (`git diff` clean and +`All terms check.` again after each). Every mutation was rejected. + +| Mutation | Protocol bug | Law it falsifies | Where the checker stops first | +| --- | --- | --- | --- | +| `tick_st` advances with `Nat.sub(p, STEP())` | progress regresses on every tick | `poll_monotone` (`le_add`) | `tick_st_ok`, an invariant proof whose rewrite spells out `Nat.add(p, 25n)` | +| complete query answers `RPoll{0n, ...}` | a finished query reports progress 0 | `done_poll_complete` | an `Empty.absurd` annotation in `expired.fin` that spells out `RPoll{100n, ...}`; with that one annotation updated, `done.fin`: expected `RPoll{0n, ...}`, observed `RPoll{100n, ...}` | +| `doget_run` answers `RData{}` for any found endpoint | `DoGet` ignores `expiration_time` | `doget_after_expiry` | `dbe_ep.fin`: observed `doget_ep(is_lt(now, exp))`, expected `RData{}` | +| `poll_run`'s expired branch answers a `PollInfo` and touches the descriptor | server accepts a descriptor after `PollInfo.expiration_time` | `expired_descriptor_rejected` | `kept_poll_run.fin`: `upd(OpTouch)` where `upd(OpCancel)` was proven | +| `AStart` does not advance `next` | query ids reissued | `inv_kept` | `inv_kept`'s start case: `is_lt(next, next)` | +| `cancel_st(QDone{}) = QDone{}` | cancelling a complete `FlightInfo` leaves its endpoints readable | `cancelled_poll_rejected`, `cancelled_doget_rejected` | `cpr_st`'s `QDone` case: observed `RErr{}`, expected `RPoll{100n, ...}` | +| `renewed(exp, now) = exp` | `RenewFlightEndpoint` does not extend | `renew_extends` | `renewed_later`: expected `is_lt(exp, exp)` | + +Two rows show the brittleness the prepared-statement notes describe: +the mutation genuinely falsifies a law, but the first failure the +checker reports is in a proof or annotation that merely mentions the +changed shape. Either way `bend PROOF.bend` fails, which is what +`LAWS.bend` promises; telling "the law is false" from "the proof needs +re-shaping" is left to the reader. The `AStart` row is the counterpart +of the same row in the prepared-statement model. + +### What it cost + +The proof is 2.4 lines per line of model, against 1.7 for the +prepared-statement model. The extra cost is one law, `poll_monotone`, +whose proof is about 300 lines: a case analysis over the intermediate +request, then over the update it applies to the polled query's body, +then over that body's state and the two liveness verdicts. Everything +else is 10 to 40 lines per law once the two commutation lemmas +(`find_upd`: a lookup after an update is the update of the lookup; +`find_ep_renew`: the same for endpoints) and the `Nat` lemma library +are in place. Bend's Base still ships almost no arithmetic: `n < n+1`, +`x < n ⇒ x < n+1`, `x < n ⇒ x ≤ n`, `p ≤ p + k`, `m ≥ e ⇒ e < m+1`, and +the soundness of `Nat.is_eq` are all proven here by hand. + +Two Bend rules shaped every proof and are worth knowing before writing +another one. A `match` may only scrutinise a parameter or a +pattern-bound variable, so every computed `Bool` or `Maybe` goes +through a helper (`.fin`) that takes it as a parameter together with an +equation about it. And a rewrite (`%e : P`) may not precede a `match` +on a parameter, so every helper matches first and rewrites inside each +case; the equation's type is refined by the match, which is what makes +the rewrite land. Constructor names are global, so `Done{}` and +`Fail{}` collide with Base and everything is prefixed. + +## 5. Sources + +- `arrow-format/Flight.proto`: `PollFlightInfo`, `PollInfo`, + `CancelFlightInfoRequest`, `CancelStatus`, `CancelFlightInfoResult`, + `FlightEndpoint.expiration_time`, `RenewFlightEndpointRequest`. +- Arrow format docs, `docs/source/format/Flight.rst`, sections + "Downloading Data" (endpoint expiration, renewal, cancellation) and + "Downloading Data by Running a Heavy Query": + https://github.com/apache/arrow/blob/main/docs/source/format/Flight.rst +- Java: `flight/flight-core/.../PollInfo.java`, `FlightEndpoint.java`, + `CancelStatus.java`, `FlightProducer.pollFlightInfo`, + `FlightClient.pollInfo`, `cancelFlightInfo`, `renewFlightEndpoint`; + integration scenarios `PollFlightInfoScenario`, + `PollFlightInfoProducer`, `ExpirationTimeProducer`, + `ExpirationTimeCancelFlightInfoScenario`, + `ExpirationTimeRenewFlightEndpointScenario` under + `flight/flight-integration-tests/`. +- Bend 2: https://github.com/bendlang/bend (`guide/GUIDE.md`, + `bend2/base.bend`, `demos/proof_insertion_sort`, + `demos/app_win_is_bug_2d`), and the research notes in + `dev/bend2/README.md` on the research branch. diff --git a/dev/bend2/poll_flight_info/main.bend b/dev/bend2/poll_flight_info/main.bend new file mode 100644 index 0000000000..e686ebdbb0 --- /dev/null +++ b/dev/bend2/poll_flight_info/main.bend @@ -0,0 +1,540 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# A model of the Arrow Flight long-running query protocol: the +# PollFlightInfo RPC, FlightEndpoint expiration, and the +# RenewFlightEndpoint and CancelFlightInfo actions (Flight.proto, +# docs/source/format/Flight.rst). Written in Bend 2 so that LAWS.bend +# can state the protocol's "must" and "should" sentences and +# PROOF.bend can prove the model obeys them. +# +# Abstractions (Bend has no U64, no F64 and no timestamps): +# - time is a Nat tick that advances on an explicit ATick request; +# - progress is a Nat out of FULL() = 100 instead of a double in [0, 1]; +# - the poll descriptor of a query is its id, as PollFlightInfoProducer +# encodes it into the command bytes; a ticket is (query id, index). +# +# bend main.bend # checks the model and runs the sample trace in main +# bend PROOF.bend # checks LAWS.bend against this model + +import Base + +# Constants +# --------- + +# progress is reported out of FULL; a tick of work adds STEP +def FULL() -> Nat: + 100n + +def STEP() -> Nat: + 25n + +# how many ticks a poll descriptor stays valid after a poll +def PTTL() -> Nat: + 3n + +# how many ticks an endpoint stays valid after it is produced +def ETTL() -> Nat: + 2n + +# Protocol +# -------- + +# CancelStatus of CancelFlightInfoResult. The model answers CANCELLED +# and NOT_CANCELLABLE; CANCELLING needs asynchronous cancellation and +# UNSPECIFIED is discouraged by the proto ("servers should avoid"). +type CancelSt is Data: + CsUnspecified{} + CsCancelled{} + CsCancelling{} + CsNotCancellable{} + +# one client request or server-side event, by Flight RPC / action +type Act is Data: + AStart{} # PollFlightInfo with an original descriptor: starts a query + APoll{q: Nat} # PollFlightInfo with PollInfo.flight_descriptor q + ACancel{q: Nat} # DoAction CancelFlightInfo on the query's FlightInfo + ADoGet{q: Nat, tk: Nat} # DoGet with the ticket (q, tk) + ARenew{q: Nat, tk: Nat} # DoAction RenewFlightEndpoint on endpoint (q, tk) + ATick{} # the clock advances one tick; running queries make progress + AFail{q: Nat} # the query's execution fails inside the server + +# the server's answer +type Resp is Data: + RPoll{progress: Nat, desc: Maybe<&2, Nat>, info: List<&2, Nat>} # PollInfo + RCancel{status: CancelSt} # CancelFlightInfoResult + RData{} # a DoGet stream + REndpoint{tk: Nat, exp: Nat} # the renewed FlightEndpoint + RAck{} # a server-side event + RErr{} # an error status + +# State +# ----- + +# an endpoint of a query's FlightInfo: its ticket index and expiry tick +type Endpoint is Data: + Endpoint{tk: Nat, exp: Nat} + +type QState is Data: + QRunning{progress: Nat} + QDone{} + QCancelled{} + QFailed{} + +# the mutable part of a query: state, poll-descriptor expiry, endpoints +# in creation order +type QBody is Data: + QBody{st: QState, pexp: Nat, eps: List<&2, Endpoint>} + +type Query is Data: + Query{id: Nat, body: QBody} + +# the queries, the next id to issue, the clock +type Server is Data: + Server{qs: List<&2, Query>, next: Nat, now: Nat} + +# List helpers +# ------------ + +def pick_q(c: Bool, x: QBody, rest: Maybe<&2, QBody>) -> Maybe<&2, QBody>: + match c: + case True{}: + Some{x} + case False{}: + rest + +# the body of the first query with id q +def find(+q: Nat, qs: List<&2, Query>) -> Maybe<&2, QBody>: + match qs: + case Nil{}: + None{} + case Con{Query{+id, body}, t}: + pick_q(Nat.is_eq(q, id), body, find(q, t)) + +def pick_n(c: Bool, x: Nat, rest: Maybe<&2, Nat>) -> Maybe<&2, Nat>: + match c: + case True{}: + Some{x} + case False{}: + rest + +# the expiry of the first endpoint with ticket tk +def find_ep(+tk: Nat, eps: List<&2, Endpoint>) -> Maybe<&2, Nat>: + match eps: + case Nil{}: + None{} + case Con{Endpoint{+etk, exp}, t}: + pick_n(Nat.is_eq(tk, etk), exp, find_ep(tk, t)) + +# the tickets of the endpoints, in order: the info of a PollInfo +def tickets(eps: List<&2, Endpoint>) -> List<&2, Nat>: + match eps: + case Nil{}: + Nil{} + case Con{Endpoint{tk, exp}, t}: + tk <> tickets(t) + +def snoc(eps: List<&2, Endpoint>, e: Endpoint) -> List<&2, Endpoint>: + match eps: + case Nil{}: + [e] + case Con{h, t}: + h <> snoc(t, e) + +def length(eps: List<&2, Endpoint>) -> Nat: + match eps: + case Nil{}: + 0n + case Con{h, t}: + 1n+length(t) + +# Per-query transitions +# --------------------- + +# a tick of work: advance progress, or complete when it would reach FULL +def advance(p: Nat, more: Bool) -> QState: + match more: + case True{}: + QRunning{p} + case False{}: + QDone{} + +def tick_st(st: QState) -> QState: + match st: + case QRunning{+p}: + advance(Nat.add(p, STEP()), Nat.is_lt(Nat.add(p, STEP()), FULL())) + case QDone{}: + QDone{} + case QCancelled{}: + QCancelled{} + case QFailed{}: + QFailed{} + +# a running query also produces one more endpoint per tick, valid for ETTL +def tick_eps(st: QState, +now: Nat, +eps: List<&2, Endpoint>) -> List<&2, Endpoint>: + match st: + case QRunning{p}: + snoc(eps, Endpoint{length(eps), Nat.add(ETTL(), now)}) + case QDone{}: + eps + case QCancelled{}: + eps + case QFailed{}: + eps + +def tick_body(+now: Nat, body: QBody) -> QBody: + QBody{+st, pexp, eps} = body + QBody{tick_st(st), pexp, tick_eps(st, now, eps)} + +# a successful poll keeps the descriptor alive for another PTTL +def touch_body(now: Nat, body: QBody) -> QBody: + QBody{st, pexp, eps} = body + QBody{st, Nat.add(PTTL(), now), eps} + +# CancelFlightInfo: a running or complete query (and its results) is +# cancelled; a failed one has nothing left to cancel +def cancel_st(st: QState) -> QState: + match st: + case QRunning{p}: + QCancelled{} + case QDone{}: + QCancelled{} + case QCancelled{}: + QCancelled{} + case QFailed{}: + QFailed{} + +def cancel_body(body: QBody) -> QBody: + QBody{st, pexp, eps} = body + QBody{cancel_st(st), pexp, eps} + +def cancel_status(st: QState) -> CancelSt: + match st: + case QRunning{p}: + CsCancelled{} + case QDone{}: + CsCancelled{} + case QCancelled{}: + CsCancelled{} + case QFailed{}: + CsNotCancellable{} + +# only a running query can fail +def fail_st(st: QState) -> QState: + match st: + case QRunning{p}: + QFailed{} + case QDone{}: + QDone{} + case QCancelled{}: + QCancelled{} + case QFailed{}: + QFailed{} + +def fail_body(body: QBody) -> QBody: + QBody{st, pexp, eps} = body + QBody{fail_st(st), pexp, eps} + +# RenewFlightEndpoint: the new expiry is strictly later than the old +# one and at least a full ETTL from now +def renewed(+exp: Nat, now: Nat) -> Nat: + 1n+Nat.max(exp, Nat.add(ETTL(), now)) + +def when_n(c: Bool, a: Nat, b: Nat) -> Nat: + match c: + case True{}: + a + case False{}: + b + +def renew_ep(+tk: Nat, +now: Nat, eps: List<&2, Endpoint>) -> List<&2, Endpoint>: + match eps: + case Nil{}: + Nil{} + case Con{Endpoint{+etk, +exp}, t}: + Endpoint{etk, when_n(Nat.is_eq(tk, etk), renewed(exp, now), exp)} <> renew_ep(tk, now, t) + +def renew_body(tk: Nat, now: Nat, body: QBody) -> QBody: + QBody{st, pexp, eps} = body + QBody{st, pexp, renew_ep(tk, now, eps)} + +# Updates over the query list +# --------------------------- + +# a state change, applied to every query (OpTick) or to the query with +# the given id (the others) +type Op is Data: + OpTick{} + OpTouch{q: Nat} + OpCancel{q: Nat} + OpFail{q: Nat} + OpRenew{q: Nat, tk: Nat} + +def when_b(c: Bool, a: QBody, b: QBody) -> QBody: + match c: + case True{}: + a + case False{}: + b + +# the new body of the query with id `id` +def apply(op: Op, +now: Nat, +id: Nat, +body: QBody) -> QBody: + match op: + case OpTick{}: + tick_body(now, body) + case OpTouch{q}: + when_b(Nat.is_eq(q, id), touch_body(now, body), body) + case OpCancel{q}: + when_b(Nat.is_eq(q, id), cancel_body(body), body) + case OpFail{q}: + when_b(Nat.is_eq(q, id), fail_body(body), body) + case OpRenew{q, tk}: + when_b(Nat.is_eq(q, id), renew_body(tk, now, body), body) + +def upd(+op: Op, +now: Nat, qs: List<&2, Query>) -> List<&2, Query>: + match qs: + case Nil{}: + Nil{} + case Con{Query{+id, body}, t}: + Query{id, apply(op, now, id, body)} <> upd(op, now, t) + +# Requests +# -------- + +# PollFlightInfo with a poll descriptor. A running query answers its +# progress, its descriptor and the endpoints so far, unless the +# descriptor expired, in which case the query is cancelled ("the query +# may be cancelled"). A complete query answers the complete FlightInfo +# with the descriptor unset. A cancelled or failed query is an error. +def poll_run(+q: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, p: Nat, eps: List<&2, Endpoint>, alive: Bool) -> Server & Resp: + match alive: + case True{}: + (Server{upd(OpTouch{q}, now, qs), next, now}, RPoll{p, Some{q}, tickets(eps)}) + case False{}: + (Server{upd(OpCancel{q}, now, qs), next, now}, RErr{}) + +def poll.fin(+q: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, m: Maybe<&2, QBody>) -> Server & Resp: + match m: + case None{}: + (Server{qs, next, now}, RErr{}) + case Some{QBody{st, pexp, eps}}: + match st: + case QRunning{p}: + poll_run(q, qs, next, now, p, eps, Nat.is_lt(now, pexp)) + case QDone{}: + (Server{qs, next, now}, RPoll{FULL(), None{}, tickets(eps)}) + case QCancelled{}: + (Server{qs, next, now}, RErr{}) + case QFailed{}: + (Server{qs, next, now}, RErr{}) + +def poll(+q: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat) -> Server & Resp: + poll.fin(q, qs, next, now, find(q, qs)) + +# CancelFlightInfo: NOT_FOUND on an unknown query, else the status of +# the query's state, and the query becomes cancelled +def cancel.fin(+q: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, m: Maybe<&2, QBody>) -> Server & Resp: + match m: + case None{}: + (Server{qs, next, now}, RErr{}) + case Some{QBody{st, pexp, eps}}: + (Server{upd(OpCancel{q}, now, qs), next, now}, RCancel{cancel_status(st)}) + +def cancel(+q: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat) -> Server & Resp: + cancel.fin(q, qs, next, now, find(q, qs)) + +# DoGet: the endpoint of a running or complete query streams while +# now < expiration; a cancelled or failed query's endpoints are gone +def doget_ep(valid: Bool) -> Resp: + match valid: + case True{}: + RData{} + case False{}: + RErr{} + +def doget_run(+now: Nat, e: Maybe<&2, Nat>) -> Resp: + match e: + case None{}: + RErr{} + case Some{exp}: + doget_ep(Nat.is_lt(now, exp)) + +def doget.fin(+tk: Nat, +now: Nat, m: Maybe<&2, QBody>) -> Resp: + match m: + case None{}: + RErr{} + case Some{QBody{st, pexp, eps}}: + match st: + case QRunning{p}: + doget_run(now, find_ep(tk, eps)) + case QDone{}: + doget_run(now, find_ep(tk, eps)) + case QCancelled{}: + RErr{} + case QFailed{}: + RErr{} + +def doget(+q: Nat, +tk: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat) -> Server & Resp: + (Server{qs, next, now}, doget.fin(tk, now, find(q, qs))) + +# RenewFlightEndpoint: a still-valid endpoint of a running or complete +# query gets a later expiry; an expired endpoint, or one of a cancelled +# or failed query, is an error +def renew_ep_r(+q: Nat, +tk: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, exp: Nat, valid: Bool) -> Server & Resp: + match valid: + case True{}: + (Server{upd(OpRenew{q, tk}, now, qs), next, now}, REndpoint{tk, renewed(exp, now)}) + case False{}: + (Server{qs, next, now}, RErr{}) + +def renew_run(+q: Nat, +tk: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, e: Maybe<&2, Nat>) -> Server & Resp: + match e: + case None{}: + (Server{qs, next, now}, RErr{}) + case Some{+exp}: + renew_ep_r(q, tk, qs, next, now, exp, Nat.is_lt(now, exp)) + +def renew.fin(+q: Nat, +tk: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat, m: Maybe<&2, QBody>) -> Server & Resp: + match m: + case None{}: + (Server{qs, next, now}, RErr{}) + case Some{QBody{st, pexp, eps}}: + match st: + case QRunning{p}: + renew_run(q, tk, qs, next, now, find_ep(tk, eps)) + case QDone{}: + renew_run(q, tk, qs, next, now, find_ep(tk, eps)) + case QCancelled{}: + (Server{qs, next, now}, RErr{}) + case QFailed{}: + (Server{qs, next, now}, RErr{}) + +def renew(+q: Nat, +tk: Nat, +qs: List<&2, Query>, +next: Nat, +now: Nat) -> Server & Resp: + renew.fin(q, tk, qs, next, now, find(q, qs)) + +# a new query: running, no progress, no endpoints, descriptor valid for PTTL +def fresh(now: Nat) -> QBody: + QBody{QRunning{0n}, Nat.add(PTTL(), now), Nil{}} + +# one request against one state +def step(a: Act, +qs: List<&2, Query>, +next: Nat, +now: Nat) -> Server & Resp: + match a: + case AStart{}: + (Server{Query{next, fresh(now)} <> qs, 1n+next, now}, RPoll{0n, Some{next}, Nil{}}) + case APoll{q}: + poll(q, qs, next, now) + case ACancel{q}: + cancel(q, qs, next, now) + case ADoGet{q, tk}: + doget(q, tk, qs, next, now) + case ARenew{q, tk}: + renew(q, tk, qs, next, now) + case ATick{}: + (Server{upd(OpTick{}, 1n+now, qs), next, 1n+now}, RAck{}) + case AFail{q}: + (Server{upd(OpFail{q}, now, qs), next, now}, RAck{}) + +# projections of a step +def state(sr: Server & Resp) -> Server: + (s, r) = sr + s + +def resp(sr: Server & Resp) -> Resp: + (s, r) = sr + r + +# a request against a whole server +def step_s(a: Act, s: Server) -> Server & Resp: + Server{qs, next, now} = s + step(a, qs, next, now) + +def start() -> Server: + Server{Nil{}, 0n, 0n} + +# a whole trace, threading the state and the last response +def run(acts: List, sr: Server & Resp) -> Server & Resp: + match acts: + case Nil{}: + sr + case a <> rest: + (s, last) = sr + run(rest, step_s(a, s)) + +def replay(acts: List) -> Server & Resp: + run(acts, (start(), RErr{})) + +# Show +# ---- + +def CancelSt.show(c: CancelSt) -> String: + match c: + case CsUnspecified{}: + "UNSPECIFIED" + case CsCancelled{}: + "CANCELLED" + case CsCancelling{}: + "CANCELLING" + case CsNotCancellable{}: + "NOT_CANCELLABLE" + +def Desc.show(d: Maybe<&2, Nat>) -> String: + match d: + case None{}: + "unset" + case Some{q}: + Nat.show(q) + +def Info.show(ts: List<&2, Nat>) -> String: + match ts: + case Nil{}: + "" + case Con{t, rest}: + Nat.show(t) ++ " " ++ Info.show(rest) + +def Resp.show(r: Resp) -> String: + match r: + case RPoll{p, d, info}: + "PollInfo(progress=" ++ Nat.show(p) ++ "/100, descriptor=" ++ Desc.show(d) ++ ", tickets=[" ++ Info.show(info) ++ "])" + case RCancel{c}: + "CancelFlightInfoResult(" ++ CancelSt.show(c) ++ ")" + case RData{}: + "Data" + case REndpoint{tk, exp}: + "FlightEndpoint(ticket=" ++ Nat.show(tk) ++ ", expires=" ++ Nat.show(exp) ++ ")" + case RAck{}: + "Ack" + case RErr{}: + "Err" + +# print the response to each request of a trace, in order +def show_trace(acts: List, +s: Server) -> IO(Unit): + match acts: + case Nil{}: + IO.pure(Unit, Unit{}) + case Con{+a, rest}: + do IO: + IO.print(Resp.show(resp(step_s(a, s)))) + show_trace(rest, state(step_s(a, s))) + +# start a query (id 0); poll; tick; poll (progress 25, ticket 0); +# DoGet ticket 0 before its expiry; renew it; tick twice past the +# original expiry; DoGet again (renewed, so still valid); cancel; +# DoGet after cancel (Err); cancel again (CANCELLED); poll (Err) +def main() -> IO(Unit): + show_trace([AStart{}, APoll{0n}, ATick{}, APoll{0n}, ADoGet{0n, 0n}, ARenew{0n, 0n}, + ATick{}, ATick{}, ADoGet{0n, 0n}, ACancel{0n}, ADoGet{0n, 0n}, ACancel{0n}, APoll{0n}], + start())