Bend 2 PoC: ArrowBuf reference counting and allocator accounting laws

[xborder]

What's Changed

Adds dev/bend2/buffer_refcount/, a proof of concept that uses the Bend 2 language to state and machine-check the reference-counting and ownership protocol of buffers in memory-core (ArrowBuf, ReferenceManager / BufferLedger, AllocationManager, BufferAllocator / BaseAllocator / Accountant). No Java code is changed.

• main.bend: the model. One allocator owns a list of allocations (id, size, refcount, freed flag) with an allocated-bytes counter, a limit and a closed flag. Requests: buffer(size), retain(n), release(n), close(), each with the checks the Java makes in the order it makes them. main runs a sample trace; the file compiles to JavaScript (26 KB) and to a native binary (1.1 MB), both verified to run.
• LAWS.bend: 21 laws, each quoting the Javadoc or Preconditions sentence it comes from.
• PROOF.bend: proofs of all 21 laws plus the lemma library they need. bend PROOF.bend prints All terms check. in 0.3 s.
• README.md: what is modelled, the law-to-Javadoc mapping, how to run, results, and observations about the Java.

Laws proven (21)

• Invariant (inv_start, inv_kept): the allocated-bytes counter equals the sum of sizes of live allocations, and every freed flag equals "refcount is 0", at start and after every request. This is the accounting invariant (law 3 of the brief) and "memory is freed exactly when the refcount reaches zero" (law 2) as one inductive invariant.
• Release: release(0) is an error; releasing more than is held ("RefCnt has gone negative") is an error that changes nothing; a release on a freed or unknown buffer is an error, not a silent no-op; release to zero answers true, marks the memory freed and subtracts the size from the counter; a release that keeps memory answers false, keeps the buffer live, lowers the count by exactly n and leaves the counter alone.
• Retain: retain(0) is an error; retain on a freed or unknown buffer is an error and does not revive it; retain on a live buffer adds exactly n and does not touch the counter.
• Allocation: an over-limit request is rejected with no accounting change; a request that fits answers a new buffer with refcount 1 and grows the counter by its size; buffer(0) is the empty buffer.
• Close: close() with an outstanding buffer is an error; with none it succeeds and closes; the two leak checks in BaseAllocator.close agree under the invariant; after close, buffer/retain/release fail and change nothing; a second close() is a no-op.
• Traces (anti-vacuity): buffer; release; close frees and closes cleanly; buffer; retain; release; close keeps one reference and reports the leak; buffer; release; release is an error.

Laws commented out in LAWS.bend

• transfer_preserves_total (ownership transfer between two allocators, law 7): NOT PROVEN. The model has one allocator and one ledger per chunk; a faithful transfer needs the AllocationManager map from allocators to ledgers, an owning ledger per chunk and forceAllocate/releaseBytes on two accountants. Left as follow-up work.
• release_is_atomic: NOT EXPRESSIBLE. Bend is pure and a step is a function; the AtomicIntegerFieldUpdater / synchronized behaviour has no interleaving to quantify over without an explicit scheduler model.
• alloc_overflow_rejected: NOT EXPRESSIBLE. Bend has Nat, U32 and F32 only; the long overflow branch of Accountant.allocate has no model.
• read_within_capacity (ArrowBuf.checkBytes): NOT MODELLED. Expressible, but this model has no per-buffer capacity or indexes.

Mutation tests

Six bugs were injected into main.bend one at a time, the checker run, and the file restored (byte-identical). All six are rejected:

Bug	Result
release past zero answers ok instead of throwing	rejected at release_below_zero_is_error
freeing forgets releaseBytes (counter not decremented)	rejected at the invariant proof (accounting)
retain on a freed buffer revives it	rejected at the invariant proof (bytes appear without the counter moving)
freeing does not mark the chunk released (release0 forgotten)	rejected at the invariant proof (consistency)
buffer(size) ignores the limit	rejected; the false law is alloc_over_limit_rejected (confirmed by adapting the invariant proof under the mutation)
close() never reports a leak	rejected at close_with_live_buffer_is_error

Observations about the Java (documented in the README, nothing changed)

• BufferLedger.retain(int) does not call assertOpen(), unlike release and newArrowBuf; the model's closed_rejects law is stricter than the code for retain.
• retain(int) and release(int) update the count and then check the precondition, so a failing call mutates the count before throwing. The model states the intended contract (state unchanged on error).
• BaseAllocator.close() sets isClosed before checking for leaks, so a leaked buffer can never be released after a failed close (with assertions on). The model reproduces this.

How to run

git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend
cd dev/bend2/buffer_refcount
bun /tmp/bend/bend2/main.ts PROOF.bend     # All terms check.
bun /tmp/bend/bend2/main.ts main.bend      # runs the trace

🤖 Generated with Claude Code

https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj

---

Generated by Claude Code