Module lease 

Execution lease + fencing (slice B5 of docs/proposals/multi-device-sync.md, §“Deep dive: the execution-lease / fencing protocol”).

What this slice delivers: DETERMINISTIC LEDGER CONVERGENCE + a durable idempotency oracle — NOT exactly-once execution. The exactly-once execution gate is B6’s dispatch fence: a dispatch-time linearizable “am I still epoch N?” read plus a durable non-fenced idempotency read (crate::fold::SyncState::committed_run) before the external side effect. That is necessary, not an optimization; the fold below gates the ledger, not the side effect. Do not read “the fold fences the write” as “the fold makes execution safe” — it does not.

Replicating state is a leaderless CRDT fold — safe with any number of concurrent writers (that is B1–B4). Performing actions is not: a tool call has an external side effect and is not idempotent, so if two sites both hold the agent and the same scheduled trigger fires, the email goes out twice. B5 adds the two mechanisms the proposal specs for that:

1. A separate LeaseCoordinator (liveness). The crisp principle, from the proposal: the lease is for liveness; only the fence is for safety. A lease demands linearizable compare-and-swap — exactly one holder per agent at a time — which the eventually-consistent crate::relay::Relay structurally cannot provide (an FsRelay over a synced folder gives no consensus; two sites could each append “I take it” and both believe they won). So the lease lives behind its own trait, never bolted onto Relay. The proposal’s data/control split: the relay stays a dumb, E2E-ciphertext ordered log for content; the lease register holds only non-sensitive metadata (agent_id, holder, epoch, expiry), so a coordinator can serialize it in cleartext without breaching E2E. InMemoryLeaseCoordinator is the honest in-process reference — Arc<Mutex> CAS is genuinely linearizable within one process (exactly as InMemoryRelay is the honest single-process relay). A distributed backend (Cosmos if_match, a single-writer daemon, Postgres advisory locks) is B6; the trait is its contract.

2. Fencing as a fold property, over two views. The epoch a successful acquire mints is the monotone fencing token (never reused). Since car-sync is the state layer, B5 realizes fencing as a deterministic fold rule over the leased crate::oplog::Surface::Intent surface, yielding two per-agent views (crate::fold::IntentAgent):

   • committed_runs — the durable idempotency ORACLE. Keep-all, fence-independent: a commit is a permanent fact, recorded whatever its epoch and never cleared by a later epoch or by compaction. crate::fold::SyncState::committed_run is the correct “did this run already execute?” lookup — the read a B6 dispatch fence performs before any external write.
   • runs — the “who holds now” view. Per-agent epoch fencing applies to pending intents (a stale zombie holder’s pending is fenced, order-independently, without a wall-clock race — fencing beats HLC), while committed/failed records are terminal-immune (never reverted, never cleared). Read via crate::fold::SyncState::intent. This is NOT the idempotency oracle — a fenced pending is absent here even when the run committed under a prior epoch.

   Two partitioned sites that both believe they hold the lease both write intents; after convergence the ledger converges deterministically (the higher-epoch pending wins runs; committed facts survive in committed_runs).

Idempotency ties B7. A scheduled/triggered run’s id is content-derived (car_proto::deterministic_run_id), so two sites computing the same occurrence produce the same run_id. An Intent keys on that run_id, so a lease holder and a just-failed-over holder proposing the same logical run collapse to one committed-oracle record.

Honesty (the proposal’s tier-3 residual). For an external resource that doesn’t understand CAR’s tokens, exactly-once is impossible without that resource’s cooperation. B5 does not close that: it converges the ledger and provides the durable committed-oracle read; the dispatch-time fence + the oracle-read-before-effect (B6) are what make execution single-shot in the common cases, with a documented bounded residual — not a false exactly-once claim, and NOT something the fold alone provides.

Structs

InMemoryLeaseCoordinator

The honest in-process reference coordinator: a linearizable CAS register behind Arc<Mutex> (genuinely linearizable within one process — the mutex serializes every CAS), over an injected WallClock for server-authoritative expiry. Clone shares the same register, so two device handles contend over one linearizable cell — exactly the concurrency the exclusivity/fencing tests exercise.

Intent

A leased execution intent — the proposal’s write-ahead ledger entry, folded under crate::oplog::FoldTier::Leased. run_id is the B7 deterministic run id (the idempotency key), epoch the lease’s fencing token.

Lease

A granted lease — the proposal’s Lease { agent_id, holder, epoch, expires_at }. epoch is the fencing token: strictly monotone per agent, never reused, minted on every successful LeaseCoordinator::acquire.

Enums

IntentStatus

The monotone lifecycle of one execution intent: pending → committed | failed. Monotone means a terminal state (either) supersedes pending in the fold, and never regresses.

LeaseError

A lease-coordination failure.

Constants

INTENT_FIELD_AGENT

INTENT_FIELD_EPOCH

INTENT_FIELD_ID

Payload field names for crate::oplog::Surface::Intent ops. These are part of the serialized payload the fold reads; keep them stable.

INTENT_FIELD_STATUS

Traits

LeaseCoordinator

The lease-coordination contract — the linearizable single-key register per agent the proposal requires (Cosmos if_match / a single-writer daemon in B6). Distinct from crate::relay::Relay on purpose: Relay is eventually consistent and cannot host a lease.

Functions

intent_agent

The agent an intent op belongs to — the fencing group. Missing/malformed reads as "" so the fold stays total (a well-formed Intent never omits it).

intent_epoch

The fencing epoch an intent op carries. Missing/malformed reads as 0 (below any real lease epoch, which start at 1), so a malformed op is fenced rather than promoted.

intent_is_committed

Is this intent op committed specifically (not merely terminal)? Feeds the fence-independent idempotency oracle (crate::fold::IntentAgent::committed_runs) — a failed run is terminal but NOT committed, so it may be retried.

intent_status_rank

The monotone status rank of an intent op (IntentStatus::rank); an unknown/absent status reads as pending (0).