git:20261021.687d0f9 to git:20261021.9d445e8

- description: Check OptChat's store writer lease (one writer per store directory, every write made under it) with a TLA+ model and real-process tests against src/store.ts. Use when a change touches the lease, Store.open/close, /optchat new, or how the rules ledger and metrics are written, or when asked whether the single-writer lock holds.

- **Promise.** One OMP session at a time has a store directory open, and everything written into that directory is written by the session that holds its lease. A second opener gets `StoreLeaseConflictError("Store is already open by another writer")` and changes nothing.

- The lease is a kernel object bound to the directory's inode: an abstract Unix socket named `omp-optchat-sha256(dev:ino)` on Linux (`acquireLease`, `src/store.ts:387-425`), a `flock` on the root descriptor on macOS (391). Death of the process frees it; there is no lock file, pid, or timeout.

- bun run verify:lease # model, then real code: about 12 s (model 10 s, real code 1.5 s)

- bun run verify:lease --traces # also print each open finding's counterexample

- bun run verify:lease --real-only # real code only, 1.5 s

-

- ## Open findings

-

- Both are real code paths, reproduced by the real-process harness (`real/archive-renames-open-store`, `real/sidecar-writes-follow-the-inode`) and found by TLC without any user action beyond two OMP sessions on one directory. Nothing in the product code was changed.

-

- **F1: `/optchat new` can rename a store another session has open.** `ArchiveOnlyClosed`. Steps, in the code's words:

- 1. Session p1 runs `/optchat new`: `shutdown()` closes the rules ledger and `store.close()` (`index.ts:1619, 1631`); `release` frees the lease (`store.ts:449-450`).

- 2. Session p2 starts and calls `Store.open(config.directory)` (`index.ts:662`): `openRoot` opens the same directory, `acquireLease` binds its lease: p2 holds the store.

- 3. p1 calls `archiveStoreDirectory(store.directory)` (`index.ts:1654`): it claims the archive name with `mkdir` and `renameSync(directory, archive)` (`store.ts:649, 655`). It renames by path and holds no lease, so p2's live store moves to the archive.

- 4. p1 reopens `config.directory` (`index.ts:1665`): a fresh empty store, its own lease, so it succeeds.

- Harm: p2 keeps writing into the directory the user was told is a closed archive, while p1's new chat sits at the old path; while p2 lives, `--optchat-dir <archive>` fails with the conflict error. The window is the time between `closeLease` (`store.ts:434`) and `renameSync` (`store.ts:655`): narrow, but real. Fix direction, modeled as `ArchiveUnderLease` and verified: keep the lease through the rename, and rename only if `store.directory` still names the leased inode.

- **F2: the rules ledger and the metrics file are written by path, not through the store's root descriptor.** `SidecarWritesUnderLease`. The store follows its inode after a move (`store.ts:746-749`), but `RuleLedger.write` opens `join(store.directory, "ledger.jsonl")` on every event (`system1/ledger.ts:60, 145`) and `appendMetric` opens `join(store.directory, "metrics.jsonl")` (`index.ts:2066, 895`; `metrics.ts:140`). After the directory is displaced (a user `mv`, or F1), session B's ledger and metrics writes land in whichever store is now at that path, held by another session. This contradicts `ledger.ts:50` ("Only the leased session writes it"). Harness replay: B opens D and its ledger; D is renamed away; C opens a fresh store at D; B's `rule` and `metric` land in C's directory, B's `append` goes to the moved directory. Fix direction, modeled as `LedgerAtInode` and verified: open the ledger and metrics files relative to the root descriptor.

- Do not weaken either property to make the check pass. When one is fixed, the finding row turns `GONE` and the exit code is 1; follow the update procedure to make it a guarantee.

- | `Mkdir`, `OpenRootFd`, `FdPath` | `openRoot` 346-355, `makeDirectory` 316-323, `fdPath` 285, `Store.open` 781-785 | one syscall each; a symlink spelling resolves once, at `openat` |

- | `Acquire` | `acquireLease` 387-425 | one kernel `bind` (`server.listen`, 422) or `flock` (391) |

- | `Recover`, `StoreWrite` | `openStream` 787-797, `replay` torn-line repair, `collectGarbage` 702-739, `assertWritable` 812-820, appends | synchronous fd-relative writes after the lease |

- | `LedgerOpen`, `SidecarWrite` | `index.ts:677`, `system1/ledger.ts:141-156`, `index.ts:892-899`, `metrics.ts:137-146` | one `open` by pathname per event |

- | `OpenFails` | `Store.open` catch 802-809, `index.ts:683-686` | `release` closes descriptors, then the lease |

- | `Shutdown`, `Release`, `Archive` | `index.ts:1611-1632, 1638-1673`, `store.ts:1086-1091, 438-453, 645-672` | `close()` is synchronous up to `release`; the rename is one syscall |

- | `Crash`, `Restart` | `store.ts:420-421`, the module doc 743-745 | the kernel frees sockets and descriptors on death |

- | `MoveRoot` | doc comment 746-749, `tests/store.test.ts:1032-1043, 1253-1254` | a user `mv` of an open store directory |

- Variants of `Variant`: `Current`; broken: `NoLease`, `PathKey`, `WriteBeforeLease`, `NoCrashRelease`, `LeakOnFailedOpen`; fixed: `ArchiveUnderLease`, `LedgerAtInode`. Each broken variant must violate exactly the property it names, and `model.ts` lists the pairs.

- - Two sessions (`Procs`), three directory inodes (`Inodes`), two spellings of the path (`"D"` and a symlink `"L"`). About 71,000 states for the largest run. A third session is not checked.

- - Linux and macOS leases are the same action (`Acquire`). The model cannot tell them apart; only the Linux lease runs here. All writers must share a network namespace (`store.ts:421`).

- - The real-process harness runs only against this machine's platform and filesystem (local, private POSIX permissions).

- - macOS `flock` (391-398), run only by reading the code.

- - Lease loss while open (`assertWritable`, 812-820, checks `server.listening`): the model has no event that closes a server under a live store.

- Sync commit: `8d8b9964e09b79c2caf8dd5d615ed40f51e4d5d6` (the verification was confirmed against the code at this commit; the last commit that changed a covered file is `a4094a0`, v0.13.0).

- | `src/store.ts` | `StoreLeaseConflictError` 86, `fdPath` 285, `makeDirectory` 316-323, `openRoot` 346-355, `openStream`/`openExistingStream` 357-373, `acquireLease` 387-425, `closeLease` 427-436, `release` 438-453, `archiveStoreDirectory` 645-672, `collectGarbage` 702-739, `Store.open` 771-810, `assertWritable` 812-820, `replay` repair 904-909, `close` 1086-1091 |

- | `src/index.ts` | `open` 649-706, `record` 892-899, `shutdown` 1611-1632, `startNewChat` 1638-1673, `reopen` 1688-1697, `metricsFile` 2066 |

- | `src/system1/ledger.ts` | `RuleLedger.open` 64-68, `write` 141-156, the doc comment 50 |

- | `src/metrics.ts` | `appendMetric` 137-146 |

- 1. Does the change touch covered code? `git diff --stat 8d8b996 -- src/store.ts src/index.ts src/system1/ledger.ts src/metrics.ts` (use the sync commit above; after you move it, use the new one). Also look for code that moved, and for new code that opens a file in the store directory, or acquires or releases a lease.

- 5. When a finding is fixed: move its property from the `finding` rows to `guarantee` in `model.ts`, turn its `real.ts` probe from `FINDINGS` into `GUARANTEES` (flip the assertion), and keep the fixed variant as a broken one.

- `bun run verify:lease` already breaks four copies of `store.ts` (`MUTANTS` in `real.ts`) and requires each to be caught. To check the check on the real file, edit `src/store.ts` in place and run it:

- The `broken` lines copy `src/store.ts` too, so a break in the file can make some of them fail on their own (a copy that never conflicts cannot show a leak). Read the `guarantee` lines first. Then `git checkout src/store.ts` and rerun: 19 ok, 6 open findings, 0 failed. Never commit the break.