formal: forced-collision TLA+ model for the node-store seam (PO-STORE-1B/2/3)

[hartsock]

The node-store seam (#31) ships with [proof target: …] labels marking the Lean/TLA+
obligations as deferred (not shipped). This issue tracks the highest-value piece:
a forced-collision TLA+ model for MemoryStore / the seam laws.

Why

PO-STORE-3's Collision branch (divergent bytes under a live id) has no executable
Rust counterpart: AddressedBytes always derives a real BLAKE3 id, so the branch is only
reachable via a genuine hash collision. A tiny, deliberately non-injective address
function in TLC exercises exactly the branch cryptography makes impractical to hit in Rust.
(Do not model the hash as injective — that sweeps the collision behavior under the rug.)

Model sketch

VARIABLE store            \* partial function Id -> Bytes
Address(b) ∈ SmallFiniteIdSet   \* deliberately non-injective

Insert(b) ==
  LET id == Address(b) IN
  IF id ∉ DOMAIN store
     THEN store' = [store EXCEPT ![id] = b] /\ result' = "Ok"
  ELSE IF store[id] = b
     THEN UNCHANGED store /\ result' = "Ok"
  ELSE UNCHANGED store /\ result' = "Collision"

Add DropWrite, MisfileWrite, RebindOtherEntry, ReadCorrect, ReadSubstituted,
Crash, Retry actions to cover PO-STORE-1B (backend acknowledgement) and PO-STORE-2.

Invariants to check

• PutReturnsDerivedAddress — PutOk(id, b) => id = Address(b) (seam theorem).
• VerifiedReadSound — a verified read returns Ok(b) only if Address(b) = id.
• NoRebind — a live mapping is never overwritten with different bytes.
• CollisionLeavesStateUnchanged — an occupied-different insert leaves store unchanged and yields Collision.
• SameBytesAreIdempotent — re-inserting equal bytes is a no-op Ok.
• DomainNeverShrinks — grow-only.
• Backend theorem (per-backend refinement, NOT a seam theorem): InsertOk(id, b) => store[id] = b — false for an arbitrary NodeStore, proved for MemoryStore.

Layout + gate

formal/tla/NodeStore.tla
formal/tla/NodeStore.cfg

Run TLC on the tiny forced-collision universe in a CI job (mirror the existing per-check
jobs in .github/workflows/ci.yml). Lean read/insert + typed-round-trip laws
(formal/lean/StoreLaws.lean) are a lower-priority follow-up on top of this.

Source of the model + invariants: the #69 review (third round).