Designing a convergent editor

Alice deletes a button component. Bob, working offline, places an instance of that button on a slide. When they reconnect, whose edit should survive?

Keeping both sounds fair, until the instance points to a definition that no longer exists. Choosing whichever edit arrived last sounds simple, until two computers receive them in different orders. Even getting both computers to agree does not tell us whether the resulting document makes sense.

This is the central design problem of a local-first editor. Each person must be able to work without waiting for a server, and their work must come together into something the editor can still use. A CRDT gives us rules for merging information. We also need rules for what that information means.

Start with the document

A slide is more than a tree of rectangles. Text refers to styles; styles and node properties can depend on variables; instances refer to component definitions elsewhere in the document. A connector follows another node, and a frame may size itself around its children. Deleting or moving one object can change the meaning of another without touching its stored properties.

The formal model therefore includes every node kind, along with component definitions, nested overrides, variable collections and modes, named styles, and assets. Text includes paragraphs, runs and font settings. Paths include vertices, segments and handles. These distinctions matter: moving a path vertex and changing a text style cannot share one undifferentiated editing rule.

inductive Body where
  | frame (placement : Placement) (children : List Id) (layout : Layout)
      (style : VisualStyle) (clip : Bool) (guides : List Guide)
  | group (placement : Placement) (children : List Id) (clip : Bool)
  | text (placement : Placement) (data : TextData)
  | code (placement : Placement) (data : CodeData)
  | shape (placement : Placement) (geometry : ShapeGeometry) (style : VisualStyle)
  | path (network : VectorNetwork) (transform : Matrix) (style : VisualStyle)
      (startCap endCap : Option Cap)
  | image (placement : Placement) (asset : Id) (fit : MediaFit) (crop : Option Box) (alt : String)
  | video (placement : Placement) (asset : Id) (fit : MediaFit) (crop : Option Box) (alt : String)
  | connector (placement : Placement) (start finish : Endpoint) (routing : Routing)
      (stroke : Stroke) (startCap endCap : Cap) (cornerRadius cornerSmoothing : Number)
  | instanceNode (placement : Placement) (componentId : Id)
      (overrides : List (LayerPath × LayerOverride)) (propertyValues : Entries PropertyValue)
  deriving DecidableEq, Repr

There are two useful questions to ask about each property: where does its value come from, and what does it affect? A width may be written directly, resolved from a variable, or calculated from content. A font size affects measurement, layout and painting. A lock affects which edits are allowed. A shadow usually leaves layout sizing alone, but changes painted bounds; a command that fits a selection around those bounds may depend on it.

That is why “cosmetic” is a conditional label. We can leave a pigment value out of a proof about parent-child relationships. We cannot leave shadow geometry out of a proof about an operation that reads painted bounds. The formalization allows an omission only when the observation being studied does not depend on that information.

Merge the edit the person made

Suppose Alice moves a rectangle while Bob renames it. If each edit sends a whole replacement node, one can erase the other. If each writes its own field, both survive. This also applies inside styles, variable modes and component overrides: the useful boundary is the property someone changed.

But splitting everything into smaller fields is not always correct. When a node moves to another parent, its local coordinates acquire a different meaning. Taking Alice’s parent and Bob’s coordinates could put the node somewhere neither person intended. Parent, position in the child order, and local transform need to travel as a coherent placement decision.

Ordering needs identity too. “Insert at index 3” depends on the list at the time the command runs. Two people can see different lists. Stable element identities and ordering keys let a merge resolve a shared gap consistently. They do not, on their own, settle what happens when Alice moves frame A into B while Bob moves B into A. That needs a tree policy which cannot create a cycle.

The same distinction applies to history. A drag may produce many replication events, but it should appear as one action in the history panel. Undo should create a new edit that reverses the intended action while respecting other people’s work. Restoring the whole document from a previous snapshot would also restore things the person did not mean to undo.

One edit can move many things

Change a button label from “Go” to “Continue.” The text becomes wider, the button grows, and the next button moves aside. A frame set to hug its contents may grow as well. These visible changes arise from one authored edit.

The proposed boundary keeps text, constraints, sizing modes and explicitly set geometry in the shared document. A separate layout snapshot holds measured text, resolved hug dimensions, group bounds and connector routes. Recalculation updates that snapshot. It does not manufacture shared resize operations for every object that moved.

This gives us two different dependency questions. What must be recalculated? follows from the changed input through the layout graph. Can these commands interfere? depends on what each command reads and what authored data it writes. A command that reads a measured width also depends on the text, font, style and other inputs behind that measurement.

structure Command (g : Graph Input Query) (Value : Type) where
  reads : Input → Prop
  queries : Query → Prop
  writes : Input → Prop
  writesAuthored : ∀ i, writes i → isAuthored i
  run : (Input → Value) → Input → Value
  frame : ∀ s i, ¬ writes i → run s i = s i
  readsSound : ∀ a b, AgreeOn (expandedReads g reads queries) a b →
    ∀ i, writes i → run a i = run b i

Those inputs matter across platforms. A measurement made before a font or style change may already be stale when it arrives. Matching input versions lets us reject that result; it does not prove that two font engines measure identically. For an operation such as Outline stroke, the calculated path becomes an intentional edit. We can share that path instead of asking every receiver to recreate it. The command still needs a rule for which measurements it accepts.

Removing an empty group is different again. It changes authored structure, so it belongs in the command’s write set and needs a concurrency rule. Recomputing a group’s bounds belongs in layout invalidation. Treating both as incidental “cleanup” hides a distinction that multiplayer needs to preserve.

Watch the edits meet

These illustrations explore three proposed behaviors: independent fields keep both edits, a removed library entry can still support an instance, and a text edit causes local layout to catch up. They show the design, rather than a running multiplayer implementation. Use the timeline to compare each stage.

What does deleting a component mean?

Alice wants the button removed from the library. Bob needs its definition to render an instance he created offline. Those intentions can coexist if removing the library entry does not immediately destroy the definition.

The small retention structure in the formalization separates installed definitions, library deletion markers and retention claims. An instance’s claim comes with the availability of the definition it needs. Merging combines that information, so hiding an entry never takes away a definition needed by a claim. “Available” here means the data has arrived, not merely a flag announcing it.

/-- If each local delta brings the definitions its references require, their
    merge preserves availability even when another peer hides a definition. -/
theorem validity_closed_under_merge (a b : State Key) (ha : Valid a) (hb : Valid b) :
    Valid ((model Key).merge a b) := by
  intro k hk
  change (needed a k || needed b k) = true at hk
  change (known a k || known b k) = true
  cases hka : needed a k with
  | true => simp [ha k hka]
  | false =>
    have hkb : needed b k = true := by simpa [hka] using hk
    simp [hb k hkb]

This is a candidate policy, not the current component implementation. Its proof covers reference availability for any pair of admissible states. Mutable component contents need further rules, and retaining data forever is not a storage strategy. Reclaiming a definition requires knowing that an offline peer cannot still introduce a reference to it.

Variables and named styles raise the same deletion question. Cycles raise a different one: two component definitions may each gain a reference to the other without either person’s local check noticing a problem. Protecting the layer tree does not protect the component graph. Each relationship needs a policy whose validity survives merging, rather than a check that only succeeds locally.

Where proof helps

Consider a laptop reconnecting after a day offline. Updates may arrive out of order, in different batches, or more than once. For a state-based CRDT, three merge laws make those differences harmless: swapping the operands does not change the result; regrouping merges does not change it; merging the same state twice adds nothing. These are commutativity, associativity and idempotence.

structure JoinModel (State : Type) where
  empty : State
  merge : State → State → State
  commutative : ∀ a b, merge a b = merge b a
  associative : ∀ a b c, merge (merge a b) c = merge a (merge b c)
  idempotent : ∀ a, merge a a = a
  emptyLeft : ∀ a, merge empty a = a

Lean checks that these laws imply equal results after receiving the same set of deltas. An operation-based design has a different contract: concurrent operations must commute, while dependent operations need causal delivery. Neither approach requires every ordinary editor command to commute with every other command.

The application needs another proof alongside convergence: merging admissible states must preserve the rules required to produce a valid document. That is what the retention example demonstrates for one kind of reference. The read/write contracts also let us prove that independent commands commute, provided their declared dependencies are complete.

The value of writing these claims in Lean is that a missing assumption cannot be supplied by an encouraging example. If a command secretly reads a font, its independence argument is incomplete. If a deletion rule loses a referenced definition, agreeing on the lost data does not rescue document validity.

There is still no proof for the whole editor. The typed schema describes the non-cosmetic parts of the current model; it is not a verified translation of the TypeScript implementation or the renderer. General tree conflict resolution, rich-text and vector merging, collaborative undo, and cross-platform measurement remain design work. The formalization sources contain the precise definitions and worked conflict cases.

These contracts leave the choice of replication library open. Loro may provide some of the structures, and some may need to be built here. Either way, the criterion stays the same: edits converge, and the document they produce retains a meaning the editor can use.