Bend 2 PoC: IPC stream ordering laws

[xborder]

What's Changed

Adds dev/bend2/ipc_stream_ordering/, a proof of concept that uses the Bend 2 language to specify and machine-check the message-ordering rules of the Arrow IPC streaming and file formats. Nothing outside that directory changes; no Java code is touched.

• main.bend: a validating reader modelled as a state machine over abstract messages (MSchema{ids}, MDict{id, isDelta}, MBatch{refs}, MEos), with a dictionary table of id to segment count, plus a writer model (schema, dictionaries, batches, EOS) and a runnable main that prints six traces.
• LAWS.bend: 22 laws, each quoting the sentence of Columnar.rst or the ArrowReader / ArrowWriter behaviour it formalises.
• PROOF.bend: proofs of all 22. bend PROOF.bend prints All terms check. in 0.3 s.
• README.md: the model, every law with its spec sentence, how to run, build and mutation results.

Laws proven

1. Schema first, once: schema_first, schema_accepted, schema_once.
2. Dictionaries before use: batch_needs_dictionary, batch_accepted, all_null_batch_needs_no_dictionary (the spec's all-null edge case).
3. Delta dictionaries: delta_needs_base, delta_appends (segment count grows by one).
4. Replacement: dictionary_defined, replacement_in_stream, no_replacement_in_file, undeclared_dictionary_rejected, and the invariant declared_start / declared_kept (the table only holds ids the schema declared).
5. End of stream: eos_accepted, nothing_after_eos, eos_is_final (trace form).
6. Anti-vacuity: the spec's own delta and replacement examples, spec_delta_example, spec_replacement_example_stream, spec_replacement_example_file (file reader answers exactly accept accept accept reject accept accept).
7. Round trip: writer_round_trip and writer_round_trip_state: for either format, any distinct dictionary ids and any number of batches, the writer's output is accepted in full and every dictionary ends up defined.

Laws commented out

Kept in LAWS.bend with a reason above each:

• metadata_padded_to_8 (NOT EXPRESSIBLE): no bytes in the model, and Bend's Base has no Nat.mod theory.
• body_length_fits_int64 (NOT EXPRESSIBLE): Bend has no 64-bit integer type.
• footer_matches_stream and footer-order delta application (NOT MODELLED): the footer and random access are outside this model; the reader is the sequential stream reader a file embeds.

Modelling choices worth a look

• A delta for an id with no dictionary is rejected, following the spec ("allows existing dictionaries to be expanded"). ArrowReader.loadDictionary is more lenient and appends to the empty vector created from the schema. Mutation M4 shows the checker catches a switch to Java's rule.
• Writing the model surfaced that ArrowStreamReader.checkDictionaries is effectively vacuous: dictionaries is populated for every declared id in initialize(), so !dictionaries.containsKey(id) is never true. Noted in the README; not changed here.

Mutation tests

Each bug was introduced into a copy of main.bend, bend PROOF.bend run, and the copy discarded. All seven are rejected:

#	Mutation	Rejected at
M1	batch with an undefined dictionary accepted	batch_needs_dictionary
M2	file reader allows replacement	no_replace.fin (no_replacement_in_file)
M3	messages accepted after EOS	declared_kept first, then nothing_after_eos
M4	delta with no base accepted	delta_base.fin (delta_needs_base)
M5	delta ignored, segment count not bumped	segs_bump.fin (delta_appends)
M6	writer omits the schema	writer_round_trip
M7	second schema accepted	schema_once

Builds

bend main.bend -o out.js (26 KB, runs under node) and bend main.bend -o out (1.1 MB native via clang) both build and print the six traces. No build outputs are committed.

How to run

git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend
cd dev/bend2/ipc_stream_ordering
bun /tmp/bend/bend2/main.ts PROOF.bend   # All terms check.
bun /tmp/bend/bend2/main.ts main.bend    # six sample traces

🤖 Generated with Claude Code

https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj

---

Generated by Claude Code