Core store file
lease.toml
The single-writer lease, at .working/toml/lease.toml. Present only
while held; its absence is the normal state.
About
Before mutating the store, a run takes the lease. The standard requires it to be made observable at the store's sync target before writes begin, so a second system's reconciliation sees the held lease and refuses; in this build there is no sync runtime (opf sync has not yet landed), so the lease is enforced single-host single-writer only. The file carries the holder, the operation, and an acquired-at timestamp read from the clock at acquisition.
Why
Two runs writing the same store at once can each produce a locally consistent state that cannot merge: a textual merge of TOML records can silently mangle the very records the standard exists to protect. An observable held lease reduces the opportunity for concurrent writes up front, and the consistency contract's divergence check detects, after the fact, a collision that begins inside the propagation window the lease does not cover.
Description
A closed four-key shape: schema, holder, operation,
and acquired_at. Where the concurrent-operation module is enabled, the lease is
additionally recorded as a session_lease record (namespace SL) with the states
held, released, or reconciled.
How it works
A lease is never seized from a live holder. It is reconciled against recorded state on resume or close, and a leftover lease from a dead run is released only through that reconciliation. The standard discloses the residual honestly: between taking the lease and its reaching the sync target there is a propagation window in which two systems can both begin; the divergence check is the overlapping control that catches that collision, and the two layers together, not the lease alone, are the guard.
Generated view
None. The lease is transient operational state, not a record source; no view renders from it.
Value
Concurrency safety that is honest about its bounds. The lease plus the divergence check helps prevent two-writer corruption of the store, and the standard names the window it cannot close rather than implying a promise the mechanism cannot honour.
Usage
- Created by: any mutating operation, at lease acquisition; not scaffolded (a fresh store has no lease).
- Removed by: the holding run at clean close, or reconciliation after a dead run.
- Read by: every operation's consistency check before it acts;
opf doctorvalidates the closed shape; a second system's reconciliation, which refuses while the lease is held.