car-sync
Multi-device sync core for the Common Agent Runtime — the oplog +
deterministic fold + checkpoint/compaction + relay transport + execution
lease/fencing + transcript resume (slices B1, B4, B3, B5, and B2 of
docs/proposals/multi-device-sync.md).
The proposal's frame: sync events, not files. Every state-changing
operation becomes a content-addressed, replica-tagged OpRecord in an
append-only oplog; sync is "send me the ops I don't have"; and every device
folds the full op-set into materialized state deterministically. Because the
fold is commutative, associative, and idempotent over the op-set (CRDT
properties), two devices writing simultaneously converge the moment they
exchange ops.
What's here (pure, library-only)
-
oplog—OpRecord { op_id, hlc, device_id, seq, prev, scope, surface, payload }exactly as the proposal specs it, plus the per-deviceseq/prevhash-chain that makes a log order-verifiable (verify_log).op_idis content-derived via the shipped B7 discipline (SHA-256 +0x1fseparators, thecar_proto::deterministic_run_idpattern) over every field including chain position, so it is both the retransmission-dedup key and a tamper-evident cover.DeviceLogis the writer: it maintains the chain and stamps the HLC shape ({wall_ms, counter, device_id}) fromHlcClock, the real hybrid logical clock (B3) — standard send/receive rules (max of local wall and everything witnessed; counter ticks on ties), monotone under clock skew, regression, and same-millisecond bursts. Wall readings are injectable (WallClock;system_clock()is the one opt-in real-time source — library logic never reads system time), andDeviceLog::newdefaults to an always-0 wall under which the HLC degenerates to exactly B1's pure-Lamport order: one code path, same wire shape. -
fold—fold(ops) -> SyncStateunder the proposal's per-surface fold rules: grow-only surfaces (conversations, knowledge, skills, trajectories, runs) union by stable ID; registry surfaces (declagents, file registries) resolve LWW-per-record by HLC — not per file. Routing follows "sync the observations, not the result" and folds as a multiset keyed byop_id(two byte-identical observations are two events — only retransmission dedups): the fold materializes the canonically-ordered observation stream andSyncState::replayruns a caller-injected apply (the EMA stays out of the crate).state_hashis the divergence-detection invariant ("same frontier ⇒ same snapshot hash");registry_as_lwwprojects a folded registry ontocar_state::crdt::LwwMap, and the tests provefold(union of ops)≡crdt_merge(per-device exports)where the domains overlap. -
journal— durable JSONL persistence in thecar-eventlogidiom: append-only, flush-per-record, torn-line tolerant on load, tail-healing on open (a torn last line is newline-terminated before the next append so the post-crash record isn't glued onto garbage), and single-writer enforced via an exclusive advisory lock on<path>.lock(thecar-registrysupervisor pattern) — a secondopenon the same path fails withWouldBlock. B4 addstruncate_to: an atomic temp+rename rewrite to a retained tail, executed under that same lock, stamping aTruncationMarker(naming the covering checkpoint) as the new file's first line — atomic with the truncation. The marker fences the permanent-fork hazard at runtime:loadrefuses a marked journal (useload_with_marker+resume_anchored), andDeviceLog::resumerefuses an own-chain non-zero start (ChainError::TruncatedChain). -
checkpoint(B4) —Checkpoint: a serialized fold at a frontier — per-device{seq, hlc, head}frontier entries, covered scope tags, theSyncStatesnapshot,state_hash(the divergence invariant), andcheckpoint_hash: the whole-record content address (frontier + scopes + state; file<checkpoint_hash>.checkpoint.json). Same frontier ⇒ same file (relay dedup for free) AND same file ⇒ same checkpoint — the fold dedups cross-device, so two different frontiers can share one folded state, and a state-only address would fork chains on resume.loadrecomputes both hashes and cross-checks the file name; a tampered state, tampered frontier, or renamed file is rejected loudly, never folded. The recorded chain heads make a checkpoint the anchored head of a truncated log:verify_anchored(checkpoint, tail)proves the composition carries the full log's integrity guarantee,resume_anchoredcontinues a device's chain past truncation without forking at seq 0, andfold_onto(checkpoint.state, tail) == fold(full log)— byte-identical, per surface including the routing multiset — is the tested equivalence that makes compaction safe. -
compact(B4) — the GC protocol's device-side core. Per-surface snapshot retention per the proposal's table (RetentionPolicy::proposal_default): conversations last-N by payloadtimestamp, runs 50/agent + 30 days (parity withRunStore::gc), trajectories last-D, knowledge/skills keep-all. Every retention-dropped id-bearing entry leaves a minimal tombstone stub ({"id", "tombstone": true}, original op identity kept, quota-neutral, idempotent), so a"supersedes"reference resolves against a tombstone even when it arrives after compaction — no time hole; id-less entries drop entirely. Event-stream surfaces reject any rule but keep-all — observation multisets replay from genesis. The age rules' reference instant defaults toas_of_from_ops(max payload timestamp among the below-frontier ops — pure over the fold's own inputs, so every device derives the same instant).AckTableis the fold-frontier bookkeeping (per-device acked HLC, monotone-only advance, temp+rename persistence); the stable frontier ismin(acked)and compaction refuses to drop anything above any device's acked frontier (or to run at all for a device with no ack entry, or over a journal that already carries a truncation marker).compact_and_truncateenforces the crash-ordering invariant by construction: checkpoint durable FIRST, then truncate — a crash between the steps leaves the full journal plus a redundant (idempotently recomputable) checkpoint; acknowledged data is never lost; an empty compaction is a no-op (no empty checkpoint file). -
relay(B3) — theRelaytrait (push/pull(since per-device seq frontier) → {ops, latest_checkpoint_ptr}/ack/checkpoint_put/get/roster) with two reference implementations:InMemoryRelayand the shared-directoryFsRelayloopback (the realistic single-user two-Mac case: exclusive advisory lock, temp+rename state file, content-addressed checkpoint files re-verified on every load). The relay holds one verified chain per device — a pushed op must continue the relay-held chain (fork / gap / foreign / tampered = typed error; retransmission dedups onop_id). Pull cursors are per-device seqs, not HLCs, so a straggler's late (old-HLC) ops still reach every peer. Stable frontier =min(acked)over non-evicted roster devices; a device silent pastRelayConfig::eviction_horizon_ms(the proposal's horizonH) is roster-markedEvicted— its ack no longer pins GC — and is reinstated only by an ack at/above the current stable frontier. GC drops an op only when BOTH at/below the stable frontier AND covered by a stored checkpoint; retained chains stay gap-free (prefix drops, dropped head remembered for chain continuity), and a pull into truncated space fails loudly (FrontierTruncated— the cold-bootstrap signal). Checkpoints dedup oncheckpoint_hash, the whole-record content address, neverstate_hash(the B4 contract); the latest pointer advances only to a frontier-dominating checkpoint. Deliberate deviation (documented in the module docs, binding on B6): the proposal's "reject ops older thanH" rule is not implemented — seq+checkpoint truncation makes accepted-op-in-truncated-space structurally impossible, so straggler re-entry is lossless instead of lossy. -
session(B3) —SyncSession, the device-side pump holding the binding contracts by construction:appendjournals (flushed) before an op is pushable (journal-durable before transmit — B1 MUST); pulled ops areverify_log/verify_anchored-checked before folding; folds are journaled before the ack, whose value is derived from journal-held ops only, so acking merely-received state has no API path (B4 MUST). Retry/crash-mid-pump idempotent (op_id dedup both directions, monotone acks). Cold bootstrap / post-eviction re-entry (bootstrap/rebase):checkpoint_get+pull(since = checkpoint frontier)+resume_anchored— neverDeviceLog::resume; the rebased journal carries the truncation marker so the naive-load fence holds — with locally-held ops the checkpoint doesn't cover (a returning straggler's unpushed writes) carried across the rebase and pushed after.publish_checkpointcomputes and uploads the device-side checkpoint at the relay's stable frontier (device-computed because under B6's E2E the relay can never fold). -
lease(B5) — execution lease + fencing: single-leader execution over the leaderless replication above. It delivers deterministic ledger convergence + a durable idempotency oracle — NOT exactly-once execution (that is B6's dispatch fence). ALeaseCoordinatortrait (acquire/renew/release/current) provides a linearizable CAS register per agent — deliberately separate fromRelay, which is eventually consistent and cannot host a lease.acquiregrants only if unheld/expired and bumps the monotone, never-reusedepoch(the fencing token);InMemoryLeaseCoordinatoris the honest in-process reference (Arc<Mutex>CAS, likeInMemoryRelay). Fencing is a fold property with two views on the leasedSurface::Intentsurface (FoldTier::Leased):committed_runs— a fence-independent, keep-all idempotency oracle (SyncState::committed_run), the correct "did this run already execute?" lookup, surviving epoch bumps AND compaction; andruns— the "who holds now" view, where pending intents are per-agent fenced (a zombie's stale pending loses deterministically, without a wall-clock race — fencing beats HLC) while committed/failed records are terminal-immune.fold_onto(checkpoint, tail) == fold(full)holds across an epoch bump. Idempotency keys on the B7 deterministicrun_id.SyncSession::record_intent(ungated, journal-durable, with a terminal guard that no-ops a pending/failed write for an already-committed run) +record_intent_if_current(best-effort local lease gate) +committed_run(the oracle a B6 dispatch fence reads). The register holds only non-sensitive metadata, so it never breaches E2E. Intents are keep-all in compaction (CompactError::IntentRetentionrejects any trim). Fencing is per-agent (the spec — it fences a zombie's unique post-failover pending too). -
conversation(B2) — transcript resume: the conversation surface as an ordered, role-threaded projection of the oplog.SyncState::transcript( conversation_id)folds theSurface::Conversationentries into a causally(hlc, op_id)-orderedVec<Turn>(two devices talking to the same agent concurrently interleave deterministically by(wall, counter, device_id)), andresume_messages(conversation_id)returns the repaired, provider-validVec<Message>(the realcar-inference-types::Message) car-inference's multi-turn path replays to continue the conversation — the verbatim conversation-resume path the 0.25 removal (docs/solutions/conversation-persistence-removed-in-0.25.md) deferred to sync, now shipped and oplog-native (not the removedConversationStore). A conversation turn is an event stream keyed byop_id(kernel-review correction — op identity IS turn identity; content-keying silently dropped two genuine same-timestamp turns): a resent op dedups, two distinct authorings never collapse. It reuses the routing multiset machinery but is an independent multiset (no path-dependent replay —is_replay_stream == false), so it toleratesLastNretention. Because HLC order is deterministic but says nothing about concurrent turns,resume_messagesruns a repair (coalesce adjacent same-role turns, drop an orphantool_resultfrom aLastNcut mid-exchange, strip a dangling assistanttool_call) so the sequence is never provider-invalid — the "runtime validates" thesis on the projection. The 0.25 compaction-vs-store incoherence cannot recur — the oplog is the one source of truth and the transcript is a projection of the same folded state B4's checkpoint serializes, so a resume afterLastNcompaction is exactly the retained window + live tail in order, and local compaction is byte- and hash-identical to global retention. car-sync builds the realMessagefrom the shared pure-serdecar-inference-typescrate (no Candle/MLX weight), so a shape change is a compile error, not a runtimefrom_valuebreak. The daemon/memgine adoption (feedingresume_messagesinto the engine's multi-turn path + the semantic-summary boundary) is B6.
Determinism discipline: all folded state is BTreeMap-backed and nothing in
the fold/retention path reads a clock (age rules take an explicit
as_of_ms) — the two non-determinism leaks the proposal
explicitly warns about. The fold stays order-independent even on invalid
input (a forged colliding op_id tiebreaks on content, not arrival order),
but ops from a remote/untrusted source MUST pass verify_log (or
verify_anchored, when composing with a checkpoint) before folding.
Contracts callers must hold:
- Journal-durable before transmit.
DeviceLog::resumere-derivesnext_seqfrom the journal; a crash between "op transmitted" and "op journaled" re-mints thatseqfor a different op — a permanentDuplicateSeqfork on union. AlwaysOplogJournal::appendfirst. - Device identity is asserted, not authenticated. The hash chain proves
internal consistency; a forger who recomputes hashes passes
verify_log, andCheckpoint::verifyproves integrity, not origin. Cryptographic device identity (op/checkpoint signing) is B6 — until then, trust in a log's origin comes from the transport that delivered it. - Checkpoint durable before truncation.
compact_and_truncateholds this by construction; anyone drivingCheckpoint::save+OplogJournal::truncate_toby hand MUST keep that order — truncation makes the dropped ops unrecoverable from the journal, and the checkpoint named by the truncation marker is what still accounts for them. - An ack asserts durably-folded state (MUST, binding on B3). Report
ack(frontier)only after the ops at/below it are durably persisted and folded — an ack sent from memory ahead of the fsync lets compaction drop ops the acking device then loses in a crash. The mirror of journal-durable-before-transmit.
Scope note: B1 stamps ONE seq/prev chain per device across scopes, so
B4 checkpoints whole-chain and records the covered scope tags —
per-scope frontiers land when B3/B6 split the relay streams (and with them
the chains) by scope.
What's deliberately NOT here
No network daemon wiring, no encryption — the relay here is a trait + an
in-process/filesystem loopback; the wire surface speaks the same contract
later. Later slices: the sync.* WS/FFI surface + the network relay
backend + E2E encryption + checkpoint/op signing + per-scope streams (B6,
signing the whole-record content address and honoring
scopes-as-encryption-audiences), recompaction over a checkpoint base
(re-planning a journal that already carries a truncation marker — a
base-anchored session skips publish_checkpoint for the same reason),
device-side relay-driven local compaction (folding relay roster acks into
a local AckTable for compact_and_truncate), the distributed
LeaseCoordinator backend + the tier-3 executor fence call-site + the
lease.*/sync.* wire surface (B6, on top of B5's core here), and
transcript resume + files-are-projections write-path rerouting (B2). B7
(deterministic run ids, car_proto::deterministic_run_id) shipped earlier
and is the id discipline reused here (and by B5's leased-intent idempotency
key).
Quick example
use ;
use json;
let mut laptop_a = new;
let mut laptop_b = new;
let op1 = laptop_a.append;
laptop_b.observe; // lamport receive rule
let op2 = laptop_b.append;
// Any delivery order, any duplication — same state, same hash.
let ops = vec!;
verify_log.unwrap;
let state = fold;
assert_eq!;
// Durable journal: append-only JSONL, torn-tail tolerant on load.
let mut journal = open.unwrap;
for op in &ops
Compaction (B4): once every device has acked past a frontier, checkpoint and truncate — checkpoint durable first, equivalence guaranteed:
use ;
let mut acks = new;
acks.ack; // monotone-only; min(acked) is the frontier
acks.ack;
let outcome = compact_and_truncate.unwrap;
// The invariant that makes it safe (pinned per surface by the tests):
// fold_onto(checkpoint.state, retained tail) == fold(full log)
// (a truncated journal is marked: load() now errors — read the tail +
// marker explicitly, and resume via resume_anchored, never resume())
let = load_with_marker.unwrap;
assert_eq!;
let reconstructed = fold_onto;
assert_eq!;
Sync (B3): two Macs converging through a shared-directory relay — each side pumps (push journal-durable ops → pull → verify → journal the folds → ack) until quiescent:
use ;
use json;
use Path;
let relay_dir = new; // any shared dir
let mut relay = open.unwrap;
let mut a = open.unwrap;
// Local write: stamped by the hybrid clock, journal-durable BEFORE it can
// ever be transmitted.
a.append.unwrap;
// One reconciliation round; retry-safe at every crash point.
let report = a.pump.unwrap;
assert_eq!;
// A brand-new (or evicted-and-returning) device cold-bootstraps:
// checkpoint_get + pull(since = checkpoint frontier) + resume_anchored —
// locally-held unpushed writes survive the rebase and push on the next pump.
let mut b = bootstrap.unwrap;
b.pump.unwrap;
assert_eq!; // the divergence invariant