Ship Sync

Every Ship app is multiplayer by default: local live reads, optimistic writes exactly as far as the compiler can prove honest, server as sole authority, offline as a typed posture. Sync is what the compiler does with schema, queries, mutations, effects, and both targets — not a bolted-on library.

Builds on databases, browser programs, services/effects. Implementation is staged; open branches are linked at the end.

Surface Sketch

database Punchlist(Postgres) {
  table Projects {
    id: ProjectId #{ primary = True; };
    crew_id: CrewId #{
      references = Crews.id;
      topic = Topic.Via(Crews, :crew_member);
    };
    code: ProjectCode #{
      unique = True;
      topic = Topic.Token(:share_link);
    };
    client_name: String #{ pii = :shred; };
  }

  table Items {
    id: ItemId #{ primary = True; };
    project_id: ProjectId #{
      references = Projects.id;
      topic = Topic.Via(Projects, :on_project);
    };
    parent_id: Option(ItemId);
    title: String;
    status: ItemStatus;
    sort_key: SortKey;
    archived_at: Option(Instant) #{ soft_delete = True; };

    #{
      tree = {
        parent = Items.parent_id;
        order = Items.sort_key;
        scope = Items.project_id;
      };
    };
  }

  table Stock {
    id: StockId #{ primary = True; };
    crew_id: CrewId #{ references = Crews.id; };
    sku: PartSku;
    on_hand: Int #{ check = sql("on_hand >= 0"); };
  }

  retention { hot = Duration.days(30); trash = Duration.days(30); }

}

let items_for_project = live query(project_id: ProjectId) {
  from item in Punchlist.Items,
  where item.project_id == project_id,
  select item;
};

mutation(Accepted) RenameItem {
  type Params = { id: ItemId; title: String; }
  let apply = (params: Params) => [
    Punchlist.Items.update(params.id, { title = Set(params.title); }),
  ];
}

mutation(Request) CloseItemWithPart {
  type Params = { item_id: ItemId; stock_id: StockId; }
  let apply = (params: Params) => [
    Punchlist.Stock.update(params.stock_id, { on_hand = Inc(-1); }),
    Punchlist.Items.update(params.item_id, { status = Set(:done); }),
  ];
}

program(Web) {
  subscription items_for_project(model.project_id) :items;

  let update = (model, message) => match message {
    | :renamed { id; title } -> {
      command(RenameItem({ id; title }));
      model
    }
  };

  let view = (model) => Html.main([
    Synced.match(model.items, {
      on_load = skeleton;
      on_error = retry_screen;
      on_entries = board;
    }),
    Surface.Html.footer(model.items),
  ]);
}

Mutations → Operations

A mutation is a compiler-known module. Required apply takes Params and returns a vector of typed ops, captured once at commit. Invocation is an ordinary call: command(RenameItem({ id; title })).

type FieldOp('a) =
  | Set('a)     // last write in server order wins
  | Inc(Int)    // composes over any base

type Op =
  | Insert { table: TableId; row: Row }
  | Update { table: TableId; key: RowKey; ops: Vector((FieldId, FieldOp)) }
  | Delete { table: TableId; key: RowKey }        // purge mutations only
  | Reparent { table: TableId; key: RowKey; parent: Option(RowKey); order: SortKey }

apply may read params/locals; it may not read replica row fields. Stale replica reads must be captured before apply (greppable; demotes kind). One op vector is used four ways: speculate (client fold), authorize (SQL txn), record (tenant log + before-images), broadcast (topic-filtered deltas).

The mutation is the transaction on both sides — no BEGIN/COMMIT to remember. Two atomic writes are one mutation; mutations do not call mutations. Callers get nothing back: fire-and-confirm; ack is the fact on the broadcast; failures are Failed entries.

Authority-only durable work (email, webhooks, indexing, imports) is planned as module-backed workflows and steps. Atomic workflow start in the authority transaction remains 240-durable-workflow-storage-and-transactional-start.md.

Kinds

mutation(Accepted) RenameItem { … }
mutation(Request) CloseItemWithPart { … }

Kind	Compiler must prove	Runtime	UI
Accepted	every touched invariant merge-safe; ops base-independent	instant, offline-safe, never refused	render plain
Request	speculatability only	queues; authority may refuse/correct	pending until watermark

Proofs range over ops, never replica absences. Modeled invariants: NOT NULL, PKs, FKs, non-volatile defaults, CHECK in Ship AST. Opaque SQL/triggers/partial indexes force Request. Declaring weaker than provable is a warning; stronger is a compile error. Kinds re-verified at authority; client tier is advisory. Kind appears in .shc — changing it is API review.

Derived Updates

Rows are immutable values — no save(). Schema-owned field patches:

command(Punchlist.Items.update(id, { title = Set("Fix door"); }));

Kind classified per field; non-writable fields absent from patch type; schema changes reprice writes in contracts / ship sync diff. Patch shape vs database updates raw-value patch: 232-sync-derived-update-patch-shape.md. Named mutations remain the unit for intent, undo labels, and contract hash.

Undo Is Forward

History never rewinds. Inverse ops (before-images / Inc credits / re-insert) submit as a new mutation. Policies: undo :derived (default, silent), undo :compensate(m), undo :none. Stack is per (program, user, session), batch-based (History.batch); consecutive same-field Sets coalesce. Redo replays intent under current baselines (FailedRedo if illegal). Inverses rebase. History.history() is read-only for Edit menus.

Reads

let items_for_project = live query(project_id: ProjectId) { … }; // replicated

Shape	Behavior
single-table indexed predicate	live
declared FK includes	live
aggregates / sorts over synced sets	client folds (Live.derive)
ORDER BY … LIMIT, windows	deferred cursor protocol
search, opaque SQL	ordinary query today; refresh policy deferred

Same bounded predicate fragment drives membership, fanout, and optimistic overlay. A future refresh-query mode and its re-run policy remain open: 224-sync-refresh-rerun-policy.md. Cursor windows: 226-sync-cursor-protocol-windows.md.

User-Defined Properties

Patterns.PropertyBag is the blessed user-defined-field shape, not new core syntax: a definitions table plus a typed EAV values table and generated helpers. Multi-select insert/delete pairs stay one mutation. Formulas over in-scope replica inputs use Live.derive; formulas requiring unsynced rows or now() are server-computed refresh values with typed staleness.

Replicas subscribe to values by (table_id, prop_id in visible_props), not every property in a tenant. Schema-in-data evolves as data: never mutate a property's type in place; add a definition, migrate values, then archive the old one. Whether typed-null partial indexes remain modeled by the kind checker is tracked with the other ShipRel rule gaps: 222-sync-kind-rule-table-gaps.md.

Synced Model

subscription items_for_project(model.project_id) :items;
// model.items : Synced(Item) = AsyncData(Vector(Entry(Item)), SyncError)

type AsyncData('a, 'e) =
  | Idle
  | Loading
  | Refreshing('a)
  | Failure('e)
  | Stale { data: 'a; as_of: Instant; failure: 'e }
  | Success { data: 'a; as_of: Instant }

type Entry('row) =
  | Confirmed('row)
  | Saving { value: 'row }                              // Accepted path
  | Pending { value: 'row }                              // Request path
  | Corrected { from: 'row; to: 'row }
  | Failed { value: 'row; base: 'row; failure: WriteError }

Cardinality: select item → vector of entries; select maybe project → Option(Entry) (live may go None mid-subscription). Field name is failure (error reserved). Headless helpers: Synced.match, Entry.match — pure functions; screens may drop to raw match.

Two-way propagation is not an app callback. Committed facts fold into the subscribed scope; local confirmation and remote edits share one path. Different fields compose by server order; same-field LWW in fact order. Focused inputs own drafts until commit (presence is advisory, not a lock). Request may refuse (Failed) or correct (Corrected); row stays rendered.

First paint is true. Cold loads SSR Success with replica snapshot + watermark; hydration attaches without re-render. Skeletons only for warm navigation / scope rebuilds.

Laws (generated tests):

1. Pending renders in the target state — never spinner-where-content-was; Accepted is byte-identical Pending→Confirmed (ack_frame_stability); divergent Request answers are Corrected.

2. Settled is settled — Confirmed changes only by a new fact.

3. No honest vanishing — optimistic filter outs stay pinned (FilteredOut) until authority confirms.

Topics And Permissions

Rows reach a replica through the live queries a program subscribes to, scoped by their parameters. Topic-based membership (topic = Topic.Via(...)) is an open design in 225-sync-membership-backfill-and-revocation.md; the compiler rejects topic table metadata until it is implemented.

Offline

Surface	Offline behavior
Accepted	applies instantly, queues, confirms on reconnect
Request	local target + “will send”; settle on reconnect
offline :unavailable	disabled with typed reason; never queues
refresh, workflows, server expansion	unavailable; Stale / Failure(:not_replicated)

Compiler derives the offline column (ship sync report); declarations may only restrict. Installable targets get a generated service worker (hand-written SW voids the seal). Offline cold boot = durable confirmed replica as Success/Stale { as_of }. Reconnect: reads first (atomic reveals), then FIFO queue drain into Surface.Html.offline_changes. Pins / Replica.storage() / typed eviction receipts. Blobs/PWA storage: 228-sync-offline-blobs-and-pwa-storage.md.

Queues, Evolution, Durable Workflows

Queued writes carry idempotency keys and retry policy; poison → typed dead-letter (exhaustiveness forces UX). Contract hash (name, args, kind, undo)

• declared migrate / supports_queued_versions — never silent discard or reinterpret. Kind changes replay at current kind; semantic changes must dead-letter.

  O(rows)/O(audience) work is a durable workflow: module-backed, chunked, idempotent per step, and represented by typed status rows when product UI needs progress. Retry, reversal, step identity, native persistence, transactional start, and actor-owned execution remain gated by 240 and the actor questions.

  Batches: facts chunk on the wire at a 256KB soft cap (shared seq / mutation / idempotency) and reassemble before folding; a single op over the cap is an error. The batch is the atomicity/undo unit. Intra-batch parent refs can prove Accepted.

  Template expansion is client-side when its source is in the replica. Otherwise authority expands one atomic mutation while the client renders Pending(Expanding), then bootstraps the complete scope — never a partial tree. A batch-level subtree pin keeps pending render cost proportional to visible rows. Work beyond the interactive budget uses the import/workflow path. Imports use import mode (bulk apply + scope rebuild, not delta storms).

Trees, Trash, Erasure

Table metadata #{ tree = { parent; order; scope }; } — no separate tree DSL. reparent is recognized/invertible; cycles rejected in txn (client advisory Failed(:cycle)). Soft delete via #{ soft_delete = True; } on archived_at; hard Delete only behind #{ purges = True } mutations. Restore reads current trash rows, not the log.

PII fields encrypted per subject; purge shreds keys; historical reads return Redacted / Purged(seq). One retention block per DB (+ per-table narrows); legal_hold pins. Field history capability gated; as-of typed by retention tier. Branches fork and never merge. Retention/PII residue: 229-sync-history-retention-and-pii.md.

Presence And CollabString

Presence: per-client LWW blobs on a walkthrough-scoped channel (≤1KB typed budget), ~100ms throttle, 30s TTL for crash liveness only. Same membership scopes as reads; force-clear on eviction. No Encode into rows. Transport: BroadcastChannel same-origin + POST /sync/presence / SSE presence. Never in the fact log. Over-budget blobs are dropped with a development diagnostic, never truncated into invalid partial values.

CollabString is the one CRDT/event-graph surface — not String with hopeful merge. Row fact owns document id; sidecar carries string CRDT ops. Required CollabString columns get SQL DEFAULT '' automatically (empty row stub; apps do not write #{ default = ""; }). Marks + inline refs are part of the contract; cursors are presence. Offline matches row sync (scope catch-up then document drain). Undo is forward via History.batch. Html.collab_string is a stdlib element whose browser runtime owns IME, selection, and a11y. VDOM patches only Ship-owned children; foreign extension siblings left alone.

Status: CollabString is Jupiter-shaped OT (ship_string) with Wave pending+buffer. A WASM string OT engine is last resort. Latency product target: one-frame local typing; remote ops <50ms p50 / <150ms p95 same-region when hot. General userland CRDT columns and editor plugins that write the document log are refused.

View Layer

Closed honesty types → total headless helpers + standard components:

Synced.match / Entry.match
Surface.entry / Surface.list / Surface.writes
Surface.Html.list / footer / offline_changes

Defaults follow kinds: Saving quiet, Pending calm saving, Failed stays visible. Retry/dismiss/undo wire to runtime commands. A11y contract tested. Theming (Surface.ViewDefaults) touches only the rendered layer.

Transport And Deployment

SSE down, HTTP POST up. Catch-up deltas?after=seq is cacheable GET. One protocol version per deploy (deploy fence); no negotiation. WebSockets opt-in for sustained >10Hz cursors only. Ops residue: 227-sync-transport-operations.md.

The native server owns SSE as a pull-based BodyStream over bounded channels. Idle streams do not own threads; disconnect cancellation closes the request scope, and heartbeats are reactor-driven chunks.

Closed world:

• Sync requires database …(Postgres) — SQLite is not a sync deployment

• Authority only on blessed targets; no middleware inside ordering/membership/broadcast

• Evergreen browsers, stated per release

• Generated client sealed: zero exports, zero npm; ship sync report --bundle prints a per-app receipt. Initial CI-held targets are ≤42KB gzipped for the core and ≤28KB for the thin all-Request posture; CollabString and presence are separate opt-in chunks. The gates land with the first runtime artifacts.

  All-Request / no-replica apps compile to a thin SSR+POST posture.

Tooling And Testing

• ship sync report / ship sync diff --against <tag> — kinds, offline, contract hash, demotion blast radius, bundle receipt

• Runtime telemetry on write tiers / demotions

• ship dev --offline — airplane toggle + queue overlay

• SyncSim.airplane(...) — named offline/reconnect schedule helper

• Generated airplane_test — queue offline work, reconnect, then assert convergence, zero silent loss, and honest states at every phase

  ShipRel is the one relational core (client fold, simulation authority, kind verifier, rule table). Differential battery vs real Postgres in CI. ship test runs synced programs under deterministic simulation; property battery generated from schema/mutations. Kind rule-table gaps: 222-sync-kind-rule-table-gaps.md. Reserved/budget writes: 223-sync-reserved-budget-writes.md.

Refuses

• CRDTs for application rows (CollabString is the one admission)

• Git-style merge of data branches

• Bitemporality

• Wire-version negotiation

• Public JS API / userland access to generated runtime

• Full no-JS operation (floor is SSR content + visibly inert controls)

• Windowed live queries / live search in v1 (use an ordinary server query until the cursor or future refresh protocol lands)

Open Questions

• 240 — workflow storage / transactional start

• 222 — kind rule-table gaps

• 223 — reserved/budget writes

• 224 — refresh re-run policy

• 225 — membership backfill/revocation

• 226 — cursor protocol

• 227 — transport operations

• 228 — offline blobs/PWA

• 229 — history retention/PII

• 232 — derived update patch shape