flint-lean: the checkout/publish syncer core (plan of record: docs/plans/flint-lean-plan.md v2).
Lean is a SEPARATE front end from the hub: no NFS, no daemon in the
data path. An agent pod gets a full local checkout on an emptyDir
(real ext4/APFS POSIX), and a syncer publishes snapshots to the
bucket through a barrier. Durability is RPO-shaped (the flush floor);
coherence is snapshot-level (the subtree manifest CAS is the atomic
commit point). This module reuses tier::store (ObjectStore,
GenerationStamps, conditional puts, the epoch cell) as a library and
deliberately does NOT reuse the hub's flush/arbitration machinery —
the plan pins that: the hub's 412 arbitration is LOCAL-WINS-overwrite
(tier/flush.rs), which is exactly wrong under HITL second writers.
The protocol here is the machine checked by lean/formal/ LeanSubtree.tla (20-run gate). The load-bearing rules, each of
which a model mutation rediscovers when broken:
- Barrier order: consume inbox → scan → intent/window → uploads → manifest CAS (merge) → deletes LAST as GC of keys the NEW manifest no longer references → baseline rewrite. (v1's upload→delete→CAS order dangles the manifest on a crash.)
- HITL writes land as object + inbox entry, never direct manifest edits; the barrier never runs against an unconsumed inbox.
- Never If-Match-overwrite an ETag this syncer did not itself publish or consume: a foreign 412 parks the path and surfaces a conflict; own-crashed-PUT is recognized by flush_uuid and adopted.
- GC deletes are HEAD-guarded on the recognized ETag.
- Takeover rotation: a successor CAS-rewrites the manifest (seq++, content-identical) BEFORE serving, so a deposed straggler's manifest CAS 412s; every publish carries its epoch.
- Restart matrix: marker present ⇒ never re-materialize (a re-checkout would resurrect unpublished deletes); reload the persisted baseline, rescan, self-recognize the lease via the persisted incarnation id (emptyDir-scoped — a replacement pod gets a fresh identity and takes the takeover path).
- Deletion basis: a path is delete-eligible only if absent in two consecutive scans AND present in our own baseline (the rename-vs-walk guard).