Bend 2 research notes, a proven Flight SQL prepared-statement model, and a differential conformance test

[xborder]

What's Changed

Research on the Bend 2 programming language (released 2026-09-17) and where it could be applied around Arrow, Arrow Flight and Flight SQL; a proven Bend 2 model of the Flight SQL prepared-statement lifecycle; and a JUnit test that uses that model as an oracle to validate the two example Flight SQL servers. No production Java code or build changes.

dev/bend2/README.md

Research notes covering what Bend 2 is (dependently typed, affine, LAWS.bend/PROOF.bend checked on every build, C/CUDA/Metal/JS targets), its type theory and trust model, tooling, stated limitations, how to run it, what proving costs in practice, and an assessment of where it fits with Arrow:

• Good fit: executable, proven specifications of protocol lifecycles (Flight SQL prepared statements, transactions and savepoints, PollFlightInfo, session options) and using compiled models as test oracles for the Java implementation.
• Feasible but expensive: columnar and IPC structural invariants (no mod/div lemmas in Base, no int64).
• Not a fit: verified code called from Java (no JVM target, no stable ABI), GPU kernels over Arrow buffers, constraining Java code with laws.

dev/bend2/prepared_statement/

A Bend 2 model of the Flight SQL prepared-statement lifecycle (main.bend) with six laws (LAWS.bend) and their proofs (PROOF.bend). The spec says a server "may return an updated handle" on bind, so the model takes a policy flag: rotate the handle (stateless style) or keep it.

• closed_never_executes: after ClosePreparedStatement, executing the handle is an error, under either policy.
• created_handle_executes: the handle returned by create executes (anti-vacuity).
• stale_handle_rejected: under rotation, after a DoPut bind rotates the handle, the old handle is rejected, per the spec's "the server is responsible for detecting the case where the client does not use the updated handle and should return an error".
• kept_handle_executes: under the keeping policy, a bound handle still executes.
• fresh_start, fresh_kept: all live handles stay below the issue counter at start and after every request, so the stale-handle law covers every reachable state.

bend PROOF.bend prints All terms check. in about 0.2 s. Three injected bugs (bind keeps the old handle live, close is a no-op, counter not advanced on create) each make the check fail. The model compiles to JavaScript and to a native binary.

Differential conformance test (dev/bend2/DIFFERENTIAL_TESTING.md)

The laws only constrain the Bend model, so a bridge to Java was built:

• traces.bend enumerates 1085 request sequences (all of length 1 to 3 over create, bind, execute and close on two handle ids, plus longer ones starting with create), runs them through the proven model under both policies, and prints the expected response per request. The output is committed at flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt, so the Java build needs no Bend toolchain.
• TestFlightSqlBendConformance replays every trace against FlightSqlExample (keep column) and FlightSqlStatelessExample (rotate column) through the raw FlightClient, mapping the model's handle ids to the bytes each server issues, and compares success or error per request. Deviations are bucketed by category and each server carries a documented known-deviation set; the test fails if a category appears or disappears.

Results:

Server	Steps compared	Deviations
FlightSqlExample (stateful)	4221	none
FlightSqlStatelessExample	4221	3 categories

The stateless example encodes the query into the handle and validates nothing server-side, so it executes and binds stale and closed handles (the spec says the server "should return an error"), and it fails to bind a rotated handle a second time because it parses the rotated bytes as SQL (the spec allows chaining DoPut handles). These are recorded in the test as known deviations with the reason for each.

The document explains the chain of trust (spec sentence to law, law to proof, proof to generated expectations, expectations to replay), what the test does and does not establish, and how to extend it to other servers and to the other models.

Follow-up proofs of concept for transactions and savepoints, IPC stream ordering, buffer reference counting and PollFlightInfo are being prepared as separate PRs.

🤖 Generated with Claude Code

https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj