Bend 2 PoC: Flight SQL transaction and savepoint laws

[xborder]

What's Changed

Adds dev/bend2/flightsql_transactions/, a proof of concept that uses the Bend 2 language to state and prove the transaction and savepoint lifecycle of Flight SQL, as written in the comments of arrow-format/FlightSql.proto (ActionBeginTransaction, ActionBeginSavepoint, ActionEndTransaction COMMIT/ROLLBACK, ActionEndSavepoint RELEASE/ROLLBACK, and the optional transaction_id on statements). It follows the prepared-statement prototype on claude/bend2-arrow-integration-pgexut and reuses its proof helpers; only this new directory is in the PR, no Java code is touched.

• main.bend: the server model. One id counter, live transaction ids, live savepoints tagged with their transaction (newest first), the five requests, and a runnable trace in main.
• LAWS.bend: 19 laws, each quoting the proto sentence it comes from, plus three properties kept as comments with the reason they cannot be expressed.
• PROOF.bend: the proofs. bend PROOF.bend prints All terms check. in 0.32 s.
• README.md: what is modelled, the readings chosen where the proto is silent, how to run, results, mutation tests.

Laws proven (19)

Law	Proto sentence
ended_tx_rejected	"the transaction handle is invalidated": after EndTransaction on t, every request naming t (BeginSavepoint, EndTransaction, statement) is an error, from any state
ended_tx_kills_savepoints	"as are all associated savepoints": EndSavepoint on a savepoint of an ended transaction is an error (needs the id invariant)
commit_rollback_same_state	COMMIT and ROLLBACK are the same lifecycle transition
savepoint_needs_live_tx, savepoint_in_live_tx, savepoint_bound_to_tx	"Creates a savepoint within a transaction" / "The transaction to which a savepoint belongs"
end_savepoint_keeps_txs	rolling back to or releasing a savepoint never changes which transactions are live
release_kills_savepoint	"Releasing a savepoint invalidates that savepoint"
release_keeps_other_savepoints	chosen reading: release drops only that savepoint (JDBC/PostgreSQL also drop later ones; the proto does not say so)
rollback_keeps_savepoint	"Rolling back to a savepoint does not invalidate the savepoint"
rollback_kills_later_savepoints	"but invalidates all savepoints created after the current savepoint" (needs the id invariant)
rollback_keeps_earlier_savepoints	complement of the above
statement_needs_live_tx, statement_autocommit, statement_in_live_tx	"Include the query as part of this transaction (if unset, the query is auto-committed)"
fresh_tx_runs_statement, fresh_tx_takes_savepoint	anti-vacuity: the id BeginTransaction returns is usable
inv_start, inv_kept	the invariant (ids strictly descending and below the counter, hence unique and never reissued) holds initially and is preserved by every request, so the laws stated for invariant states cover every reachable state

Kept as comments, not proven

• NOT EXPRESSIBLE timeout: "If the transaction times out, then it is automatically rolled back". The model has no clock; a timeout is an event between requests, not a request.
• NOT EXPRESSIBLE opaque bytes handles: Bend has no byte or 64-bit integer type; ids are Nats from one counter and only "never reissued" is stated.
• NOT EXPRESSIBLE "Only supported if FLIGHT_SQL_TRANSACTION is ... SUPPORT_SAVEPOINT": feature negotiation lives in GetSqlInfo, a separate RPC.

Every law that was attempted was proven; there is no NOT PROVEN entry.

Mutation tests

Seven bugs injected into main.bend one at a time, each rejected by bend PROOF.bend, files restored afterwards:

1. commit does not retire the transaction's savepoints
2. rollback to a savepoint drops the savepoint itself
3. a statement on an ended transaction succeeds
4. BeginTransaction does not advance the counter
5. release also drops later savepoints (the JDBC reading)
6. rollback keeps the later savepoints
7. ending a savepoint also ends the transaction

The README records, per mutation, the law that becomes false and where the checker first fails (often an earlier proof step that spelled out the old shape of the model rather than the violated law, the brittleness noted in the research notes).

Builds

bend main.bend -o out.js (21 KB, runs under node) and bend main.bend -o out (1.1 MB native via clang 18) both build and print the expected trace [Id(0), Id(1), Id(2), Done, Err, Done, Done, Err, Err, Done]. No build outputs are committed.

Observation

While reading FlightSqlClient for the semantics: rollback(Savepoint) sends END_SAVEPOINT_RELEASE, the same action as release(Savepoint). Under the model that call performs the release transition, after which the savepoint is gone, rather than the rollback transition that keeps it. Not changed in this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj

---

Generated by Claude Code