Distributed tracker model #

This is the coordination contract for tk: one local write path per machine, immutable Git facts exchanged between machines, and compare-and-swap on the store ref for a decision that must have one winner. The model follows Irmin's separation of a content-addressed block store from mutable branch heads. It does not require one scheduler, one project, or one repository set for the whole fleet.

tk does not manage code branches. Its durable issue state belongs in a dedicated tracker Git repository. Code repositories and their branches only link to that store; making a new code branch does not create another copy of claims or issue state.

1. Properties and invariants #

One local write path per machine. Worktrees and agents on one machine share a tracker store and coordinator. Another machine has its own clone and may work while disconnected.
One identity per store ref. The organization store is a Git repository, independent of the projects that link to it. Repository ID plus full ref name identifies a decision; a checkout path or remote alias does not.
No lost edits. Additive edits and external Git commits discovered later remain available for merge or named conflict. Missing facts are unknown, and deletion is observed rather than silently undone.
Schema-valid deterministic rows. A store commit contains its schema and rows. Mergeable fields follow declared rules; incompatible scalar edits are exposed as conflicts, not arbitrary visible winners.
Exclusive lifecycle transitions. One published row has at most one claim holder. Claim, release and close validate the current row and update it in one commit; they never merge as fields.
Convergence. Immutable facts with stable IDs and causal parents converge under duplicate, delayed and reordered delivery. A late fact can invalidate a projection but cannot validate a stale precondition.
Evidence-bound closure. A close identifies the accepted landing and the checks or reading that justify it. Changed code or schema needs a fresh validation.
No branch fork of issue state. One designated ref in the tracker repository orders active rows and claims. Another branch in that tracker repository is a proposal, not a second live authority. Creating or switching a branch in a linked code repository never copies the store.

The tracker schema and lifecycle rules live in the dedicated tracker store. A code project's link to that store creates no independent issue policy or claim authority. A writer with a stale schema or store head must reread before publishing; incompatible row edits are named conflicts.

2. Synchronization model #

Identity and authority #

A machine runs one local tk write path. Its worktrees, commands and agents share the same local store ref and index. Local indexes and journals are projections or recovery records, not copies of global authority.
The tracker repository is a separate Git repository, one per issue namespace. Its designated store ref contains the schema and rows. Code checkouts link to that repository; they do not carry its database in their branch trees. A Git branch of the tracker repository other than the designated store ref can carry proposed edits, but no active claim is read from it.
An organization owns one issue namespace and one designated tracker store ref. Its repository identity and full ref name are the coordination key for row transitions. Several code checkouts may link to that store; each uses the same row IDs and claims. A checkout path or remote alias is not a second issue authority. Ambiguous store links refuse a write.
A fact is an immutable Git object with a stable operation ID, writer identity, causal parents and payload. A writer appends facts to its own history. Receiving the same fact twice has the same effect as receiving it once. A new writer, including one made by cloning a machine, gets a new identity. A machine joins the facts it can see and derives its tracker view; a missing repository or writer is unknown, not evidence of absence.
The authority for a decision is the current value of the Git ref that decision changes at its designated publication endpoint. On one machine the write path serializes its own attempts using an exact local ref compare-and-swap. Across machines the publisher uses an expected-value lease against that endpoint. Mirrors can lag or diverge; they do not each grant an exclusive decision. A successful local decision is not a globally published decision until the designated lease succeeds. No machine owns a shared repository merely because it owns a project containing it.

The store schema and lifecycle policy are versioned inputs to every transition. A validation result binds their digest as well as the candidate tree. They live in the same candidate tree as the rows on the designated tracker ref. A policy change moves that ref, so a writer validating the old policy loses the comparison if another machine publishes the change first. The result is a named conflict or a new validation, never an arbitrary choice of whichever machine ran first.

Facts converge by fetching writer histories, retaining both sides of a fork, deduplicating operation IDs and replaying a deterministic projection from the causal frontier. A late or reordered fact can change that projection; it cannot retroactively validate an old precondition. Garbage collection cannot assume that a fixed list of machines has acknowledged a fact. It needs an explicit retention or checkpoint rule that preserves recovery and late discovery.

code repository
  refs/heads/main, refs/heads/feature  code histories; no issue authority

tracker repository
  refs/heads/main                  active issue store
  refs/tk/writers/WRITER           immutable fact history and proposals

The designated tracker store ref is the only active issue projection. A tracker branch can hold proposed changes but does not fork claim authority.

For example, machines A and B both read one open row. A publishes a claim on the store ref. B's lease against the old value fails, so B fetches A's commit and reruns the claim transition, which now reports the holder. Additive edits that B made meanwhile can still merge by field rule. Neither machine needs a complete list of every project using the store.

One transition protocol #

Row transitions form a pure state machine. Its input is an immutable store snapshot, a proposed operation, causal facts and explicit time; its output is a candidate or a named conflict. It neither fetches Git nor updates a local index. The Eio layer loads and validates Git trees, persists candidates, compares the store ref, fetches on loss and feeds the new observation back to the pure transition. Generated schedules exercise the pure machine as an oracle; a thin Eio adapter runs the same schedules against real tracker repositories and rebuilt indexes.

Observe the current target ref, its reachable facts, the relevant schema and dependencies. Preserve an external ref move as a new observation. Deletion is an observed ref state, not a request to recreate the old tip.
Construct a candidate from that view. Record an immutable intent with its input ref value, output value and content identity. If a dependency or repository is unknown, keep the intent waiting.
Validate the exact candidate tree and schema. A validation result names those inputs, so a changed ref or schema invalidates reuse of that result.
Compare-and-swap the target ref from the observed value to the validated value. Publish with the same expected remote value. On a lost comparison, fetch, adopt the winner's history, rebuild the candidate and revalidate. Preserve every displaced commit under a reachable ref while reconciling.
Append the result as a fact and replay it idempotently after a crash. Facts can be delivered more than once; a store ref move has one winner at each observed value.

Each repository ref is serialized separately. Git gives no atomic update across independent repositories. An operation that spans stores therefore needs a durable intent with each old and new ref value and a completion manifest as its visibility boundary. Recovery finishes a partial move or reports the conflicting ref for adoption; it does not erase a peer's commit.

3. Git primitives and their limits #

Primitive	Use	Limit
Immutable blobs, trees and commits	Bind rows, schema, comments and validation to content	Objects need reachable refs for discovery and retention.
Commit parents and merge base	Find the common ancestor for typed row merges	Git's text merge cannot decide claim or schema invariants.
Per-writer refs and fetch	Exchange additive facts among machines	Fetch can lag; unseen facts remain unknown.
Local `update-ref` with expected old value	Serialize one local store-head transition	It covers only that local repository.
Push with an exact expected-value lease	Choose one published store-head transition	The lease checks a ref value, not row semantics or evidence.
Rescue refs and reachability	Retain concurrent or displaced edits	Garbage collection needs an explicit retention rule.

mrdt supplies pure three-way merge rules for selected fields. It cannot replace the store ref comparison: its replica layer assumes a fixed peer set, and a total merge cannot decide an exclusive lifecycle transition.

4. Mapping `tk` data into Git #

Tracker data	Git representation and rule	Why the invariant holds
Organization store and schema	Dedicated tracker Git repository; schema and rows in one candidate tree on the designated store ref	Each row is read under the schema committed with it, independently of any code branch.
Row identity and content	Stable row ID names its path; `row.json` and body are blobs in commits	Concurrent histories preserve both versions for merge or conflict.
Labels, edges and checks	`mrdt` three-way set merge against the Git common ancestor	Independent edits converge under the declared remove-wins rule.
Comments	Separate files with stable comment IDs, joined by identity	Independent comments cannot overwrite one another.
Body, title and priority	Body uses line merge with explicit conflict; incompatible scalar edits refuse	An arbitrary winner cannot silently change meaning or priority.
Claim, release and close	Pure row transition, one Git commit, exact ref comparison and remote lease	One published head orders exclusive decisions; a loser rereads before acting.
Landing evidence	Content identity of candidate and check or reading recorded with close	Later ref movement cannot make stale evidence certify a new tree.
Code checkout link, local index and backup	Code checkouts link to the tracker repository; the local index is a rebuildable projection of its reachable facts	Creating a code branch cannot fork an issue claim, and a stale cache cannot override newer Git history.

The store tree is also the human review format: deterministic row.json, body.md, separate comment files and small commits that name the operation. An index accelerates queries, while ordinary Git history and repository browsers can show what changed. The index is never the only durable copy. The same facts may be projected into TODO.md files for human reading and editing. Export is deterministic and includes stable issue IDs and the store revision from which the file was rendered. Import parses an edit into typed tracker operations, validates changed fields and lifecycle preconditions, and compares the designated store ref with that revision. If the store moved, import rebases independent edits by the field merge rules and reports a named conflict for incompatible changes; it never replaces the current store with the Markdown file. Only the accepted Git commit makes an edit durable. A Markdown branch or stale projection does not create a second issue owner.

Tracker policy #

One store per organization gives all worktrees on a machine one local write path, while another machine keeps its own store clone and can produce facts. The designated published store ref orders changes that require exclusive preconditions. A disconnected machine may record additive edits and proposals locally; it cannot promise an exclusive claim, release or close until the published ref accepts the precondition. Losing a push causes a fetch, a merge of independent fields and a retry or a named conflict.

Labels, edges and checks use the field-specific three-way set merge in mrdt; uniquely identified comments join as independent facts. A concurrent change to one scalar is exposed as a conflict, rather than choosing an arbitrary visible winner. Claim, release and close are state transitions with preconditions on the current row. They are serialized at the store ref and are never silently merged as ordinary fields. A closing decision also names the landing evidence it validated. A project that shares the same tracker store with another project does not get a separate claim authority merely by linking to it.

This is the target distributed contract. The pure row merge and single-machine store primitives do not by themselves implement writer-history exchange, remote leases or recovery across machines.