Crate flint_lean 

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.tla checks. 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 struct gauges.json is written from.

reader

Read access (per-user access design §4.4): the floor tick of a syncer that follows the workspace and never writes to the bucket.

scan

The barrier’s scan-diff (plan §2.1 step 2).

sentinel

The boundary verbs: .flint/publish and .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/sync sentinel invokes (boundary-verbs plan §2.2, D4). Harness- or sentinel-invoked, never background.

trace

The protocol event trace (FLINT_SYNC_EVENT_TRACE=1, or spec.eventTrace on a deployed workspace).

uds

The UDS door (§2.5, Phase 5) — .flint-sync/ctl.sock.

untracked

Finding 10: an upload whose commit never came.

verbs

The one-shot verbs, and which of them holds the publish fence for its whole run.

Structs

LeanConfig

Syncer

Everything a syncer operation needs: store + config + durable state.

Enums

Access

What this syncer may do to the bucket (per-user access design §4.4).

LeanError

SentinelMode

Sentinel posture knob (D0.4). auto = verbs on unless the pre-existing-.flint/ pre-flight trips; force accepts 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’s path_ok) — the scan skips it, classify never makes it delete-eligible, and checkout never materializes a files/.flint/... citation into it.

EXIT_REFUSED

Process exit code for LeanError::Refused (sysexits EX_CONFIG). Mirrored as SYNCER_EXIT_REFUSED in 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.rs uses the same 64 MiB split).

Functions

now_unix

Seconds since the epoch, saturating at 0 on a clock before it.

Type Aliases

LeanResult