Expand description
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).
Re-exports§
pub use gauges::status_report;pub use gauges::Gauges;pub use gauges::StatusReport;
Modules§
- barrier
- The publish barrier (plan §2.1, seven steps) — the machine
lean/formal/LeanSubtree.tlachecks. Order is load-bearing: consume → scan → intent/window → uploads → manifest CAS (merge) → GC deletes LAST → baseline rewrite. - checkout
- Checkout + the restart matrix (plan §2.1).
- chunk
- Content-defined chunking of the manifest’s key stream
(
docs/plans/flint-lean-chunked-manifest-design.md§3). - control
- The
.flint/control namespace (boundary-verbs plan §2.0, D0/D11): the agent’s side of the file protocol. - gauges
.flint-sync/gauges.json— the Phase-3 observability minimum (§2.6; review ledger OF-6).- inbox
- The inbox/window cell (plan §2.2): ONE CAS document that is both the HITL inbox and the barrier-window token.
- lease
- The subtree lease, held for ONE BARRIER’s commit section (design
2026-09-13,
docs/plans/flint-lean-writer-lease-and-gated-assessment.md§4), with a FIFO ticket so W writers wait at most W barriers. - manifest
- The lean subtree manifest: one JSON document, CAS-written, the atomic commit point every reader trusts (checkout, sync, DR).
- metrics
/metrics(D15, §8 Q5) — Prometheus exposition rendered from the SAME structgauges.jsonis written from.- scan
- The barrier’s scan-diff (plan §2.1 step 2).
- sentinel
- The boundary verbs:
.flint/publishand.flint/sync(plan §2.1, §2.2 — D1, D2, D3, D3.1, D12). - state
- Durable emptyDir bookkeeping (plan §2.1 “restart matrix”).
- sync
- The sync verb (v1, HITL — decided §9 Q4), plus the scoped form the
.flint/syncsentinel invokes (boundary-verbs plan §2.2, D4). Harness- or sentinel-invoked, never background. - trace
- The protocol event trace (
FLINT_SYNC_EVENT_TRACE=1, orspec.eventTraceon a deployed workspace). - uds
- The UDS door (§2.5, Phase 5) —
.flint-sync/ctl.sock. - verbs
- The one-shot verbs, and which of them holds the publish fence for its whole run.
Structs§
- Lean
Config - Syncer
- Everything a syncer operation needs: store + config + durable state.
Enums§
- Lean
Error - Sentinel
Mode - Sentinel posture knob (D0.4).
auto= verbs on unless the pre-existing-.flint/pre-flight trips;forceaccepts consumption of pre-existing sentinel-named files.
Constants§
- CONTROL_
DIR - The workspace-local control namespace (boundary-verbs plan D0): the
agent’s side of the file protocol. Reserved exactly as the gateway
reserves
.flint/on the HTTP side (flint-lean-gateway’spath_ok) — the scan skips it,classifynever makes it delete-eligible, and checkout never materializes afiles/.flint/...citation into it. - EXIT_
REFUSED - Process exit code for
LeanError::Refused(sysexitsEX_CONFIG). Mirrored asSYNCER_EXIT_REFUSEDin the CSI node plugin, which does not depend on this crate; drill leg S22 is where the two are checked against each other. - LEAN_
DIR - Reserved control namespace inside the subtree prefix. Never scanned, never part of a checkout, never GC’d by the barrier.
- SENTINEL_
PROTOCOL - Protocol version advertised in
.flint/capabilities.json. - STATE_
DIR - The syncer’s durable bookkeeping directory inside the workspace (emptyDir-scoped: survives container restarts, dies with the pod).
- SYNCER_
VERSION - This binary’s version, echoed to the agent (
capabilities.json) and to the operator (the lease cell’s echo, §2.6). Both mixed-version holes — agent↔syncer and operator↔syncer — are detected by comparing what is RUNNING against what was asked for, and neither comparison exists without a version on the running side. - WHOLE_
PUT_ MAX - Default whole-object publish ceiling; larger files go through the
multipart compose path (
tier/flush.rsuses the same 64 MiB split).
Functions§
- now_
unix - Seconds since the epoch, saturating at 0 on a clock before it.