Bend 2 PoC: PollFlightInfo and endpoint expiry laws

[xborder]

What's Changed

Adds dev/bend2/poll_flight_info/, a proof-of-concept that uses the Bend 2 language to specify and machine-check one area of Arrow Flight: the PollFlightInfo long-running query protocol, FlightEndpoint.expiration_time, RenewFlightEndpoint and CancelFlightInfo. It follows the layout of the prepared-statement model from the research branch (dev/bend2/prepared_statement/). No Java code is touched.

• main.bend: the server model. Queries with progress (a Nat out of 100), a poll-descriptor expiry tick and endpoints with expiry ticks; requests AStart, APoll, ACancel, ADoGet, ARenew, ATick, AFail; a runnable sample trace in main.
• LAWS.bend: 22 laws, each quoting the Flight.proto or Flight.rst sentence it comes from.
• 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, results and mutation tests.

Laws proven (22)

• Invariant: inv_start, inv_kept (ids below the counter, progress at most 100, kept by every request).
• Progress: progress_bounded ("must be in [0.0, 1.0]"); poll_monotone (endpoints only appended, and this server's progress never decreases across a poll, any one request, and a poll again).
• Descriptors: unknown_descriptor_rejected, expired_descriptor_rejected (error, and the query is cancelled), done_poll_complete (progress 100, descriptor unset, all endpoints, state unchanged), fresh_query_polls (anti-vacuity).
• Cancellation: cancel_running (CANCELLED and the query is cancelled), cancelled_poll_rejected, cancelled_doget_rejected, cancel_idempotent, failed_not_cancellable, failed_poll_rejected.
• Endpoint expiry: doget_before_expiry, doget_after_expiry, renew_extends (strictly later expiry), renew_expired_rejected, renewed_doget_ok.
• Closed traces proven by computation: trace_doget_fresh (start, poll, tick, poll, DoGet before expiry streams), trace_doget_expired, trace_completes.

Decisions where the spec leaves room (argued in the README): cancelling a complete FlightInfo answers CANCELLED and its endpoints stop streaming (per Flight.rst and ExpirationTimeCancelFlightInfoScenario); a failed query answers NOT_CANCELLABLE; re-sending the original descriptor starts a new query rather than erroring; an endpoint is valid while now < exp; renewal requires a still-valid endpoint.

Commented out in LAWS.bend, 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". Timing of the RPC return; the model is a pure state-and-request-to-response function with no notion of blocking.
• NOT EXPRESSIBLE: progress as a double in [0.0, 1.0]. Bend has no F64 and F32 is axiomatic; progress_bounded is the Nat-out-of-100 form.
• NOT EXPRESSIBLE: expiration_time as a google.protobuf.Timestamp against a wall clock. No 64-bit integers, no clock; time is a Nat tick advanced by ATick.
• NOT PROVEN: poll_monotone_trace, the form with an arbitrary list of requests between the two polls. It follows from the one-step law once two more invariants (ids never forgotten; cancelled/failed absorbing) are proven; not done in this session.

Mutation tests

Seven bugs were introduced one at a time; each is rejected by bend PROOF.bend, and the file was restored (check green again) after each.

Mutation	Bug	Law falsified
tick advances with Nat.sub	progress regresses	poll_monotone
complete query answers progress 0	finished query reports 0	done_poll_complete
doget_run always answers data	DoGet ignores expiration	doget_after_expiry
expired-descriptor branch answers a PollInfo	descriptor accepted after expiry	expired_descriptor_rejected
AStart does not advance the counter	ids reissued	inv_kept
cancel_st(QDone) = QDone	cancelled complete info still readable	cancelled_poll_rejected, cancelled_doget_rejected
renewed(exp, now) = exp	renewal does not extend	renew_extends

In two rows the checker stops first at a proof or annotation that merely mentions the changed shape (proof brittleness, as noted in the research README); the README records where it stops and which law is actually false.

Build

bend main.bend -o out.js (32 KB, runs under node) and bend main.bend -o out (1.1 MB native via clang) both build and print the sample trace. Build outputs are not committed.

🤖 Generated with Claude Code

https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj

---

Generated by Claude Code