Formalizing the document for multiplayer

The Lean 4 project in formal/ examines whether this editor’s model and operations can support offline concurrent edits. It covers the document’s structural namespaces, not just canvas layers: pages, components, instance overrides, styles, variables, modes, component properties and asset references.

The starting point is schema 0.27.0 at commit 867320684554b695bfd0f5196e312b66ccb2a1c9. This is an analysis of that design, not an implementation of multiplayer and not a proof that the TypeScript or C++ implementation is correct. The checked results concern explicitly defined Lean abstractions. The formalization is maintained independently of the TypeScript/C++ implementation; correspondence must be reviewed explicitly.

1. What the formal document represents

The document remains a set of ID-indexed namespaces. Finite lists represent maps in Lean, with unique-key conditions. Numeric IDs abstract branded string IDs; this preserves identity comparisons in the examples. It does not prove that the production ID generator never collides.

structure Document where
  id : Id := 0
  title : Payload := 0
  metadata : Option Payload := none
  pageOrder : List Id := []
  pages : List Page := []
  nodes : List Node := []
  components : List Component := []
  theme : Theme := {}
  assets : List Resource := []
  deriving DecidableEq, Repr, BEq

The node kinds match the model’s frame, group, text, code, shape, image, video, connector and instance variants. Nodes on pages and inside component definitions share one node namespace. Page roots and component roots own disjoint trees. An instance references a definition; expanded virtual layers are not independently stored nodes in this abstraction.

ResourceKey distinguishes node styles, text styles, code styles, variable collections, variables, modes, component properties, images, videos and fonts. A scope distinguishes mode IDs local to a collection and property IDs local to a component; variable IDs are global across collections. References carry an expected type. Resource-to-resource references cover such dependencies as a text style’s font or a collection’s mode. Node references include those inside rich-text runs and instance overrides, not just direct node fields.

structuralValid checks unique identifiers and component keys, page ordering, existing roots, single ownership, one parent, acyclic hierarchy, existing typed references, same-owner connector targets, property ID/name uniqueness and an acyclic component dependency graph. A group-root page is allowed by this structural model, matching the model boundary rather than the narrower canvas assumption reported in issue #231.

Payloads stand for fields not interpreted in these proofs. In particular, this is not the complete schema validator: expression typing, allowed override fields, mode membership rules, detailed resource values, rich-text formatting, vector topology, finite numeric ranges and component-root geometry still need separate specifications. Extracting every dependency from these payloads is an explicit obligation, represented by ExtractionContract; no certified TypeScript extractor is claimed.

2. Operations and the batch boundary

The Lean Operation type represents every current DocumentOperation tag. The inventory describes the pinned source revision; it is not enforced against later TypeScript changes.

| Current operation | Structural meaning and preconditions | | --- | --- | | document.set-title, document.set-metadata | Replace one document field | | node.insert | Fresh subtree IDs, existing container, valid insertion position | | node.remove | Remove a non-root subtree | | node.move | Existing parents, valid position after removal, no cycle | | node.replace | Same ID and kind; container children cannot change | | page.insert, page.remove, page.move | Add/remove a page-owned tree or change page order | | page.replace | Same page ID and root | | theme.replace | Replace the complete style/variable namespace | | asset.put, asset.remove | Add/replace or remove an asset; references checked at the batch boundary | | component.insert | Add a definition and its fresh tree | | component.remove | Refuse while an instance or override references the definition | | component.replace | Keep component key and root identity |

The raw structural interpreter returns an optional document: no result means the equivalent of a model error. It is not a rule to discard incoming CRDT updates. A structural batch runs its operations, removes newly empty groups, releases references to removed connector targets, then validates the result.

def applyStructural (d : Document) (ops : List Operation) : Option Document := do
  let next ← rawBatch d ops
  let result := structuralEffects d next
  if structuralValid result then some result else none

This projection excludes numeric group refitting and sizing repair. In the actual reducer those occur before validation, and application dispatch adds further layout operations. successful_structural_batch_is_valid proves only that the structural interpreter publishes a result that passed its predicate. It does not prove that every edit succeeds or that independently valid edits can merge. A multi-operation batch also does not establish network atomicity; transport and publication boundaries have not been specified here.

3. Structure, geometry, layout and renderer results

The useful separation has four parts. Pure computation and structural computation are not synonyms: geometry can be pure while still involving floating point and many dependent nodes.

| Part | Current code | Formal treatment | | --- | --- | --- | | Structural edits and reference checks | model operations, codec, component/variable lookup | Finite structural interpreter and validity predicate, with stated omissions | | Geometry from stored values | geometry, group-bounds, node-sizing, vector topology | Numeric payloads and explicit future arithmetic obligations; no font oracle needed for group bounds | | Font-dependent layout | text-measurement, instance-resolver, frame-layout, computed-text-fit, component-cascade | Inputs and an external measurement function; equality across platforms is not assumed | | Retained-renderer results | fitTextToFonts, strokeOutlineCommand, vectorBooleanCommand | External results whose inputs, freshness and publication must be checked |

withAutoLayoutOperations computes a preview, derives replacement nodes and runs a component cascade. The same surface operation, such as replacing a node, may therefore have very different dependencies depending on its content and ancestors. A static operation tag alone cannot classify a user command.

The text-measurement code uses Pretext and Canvas measurements in TypeScript. The native renderer also measures text; font arrival can amend stored frames later. The formal separation does not assume that TypeScript means structural or that C++ is the only source of platform-dependent computation.

Three stages need explicit contracts: plan an edit from its dependencies, apply concrete authored changes, and calculate derived presentation. This chapter specifies the required separation; it does not move production code between those stages yet.

4. What the counterexamples establish

All witnesses below are proved by Lean’s kernel over finite values, using decide. They are not successful random tests presented as universal proofs.

| Checked result | Consequence for CRDT integration | | --- | --- | | Whole-node and whole-theme replacements do not commute | Capture authored fields rather than replicate stale complete objects | | Numeric-position insertions do not commute | Use a defined sequence/tree merge rule | | Repeating insertion fails | Existing operations are not an idempotent network protocol | | A stale container property replacement fails after child insertion | Property writes currently carry unrelated topology | | Opposing locally valid moves cannot both replay | Local cycle rejection does not define a distributed tree algorithm | | Component deletion and new instantiation have valid separate branches but an invalid combined state | Reference validity needs a merge policy in addition to convergence | | Style and variable deletion have the same reference problem | The work extends across the entire document, including theme data | | Independent component nesting edits can create a dependency cycle | A convergent layer tree is not sufficient for component references | | Empty-group deletion changes the outcome by delivery order | Implicit destructive cleanup needs a concurrency specification | | Commit amendment retains the ID while changing the document | Commit IDs cannot serve as immutable replicated event identities | | Snapshot restoration discards current state | Shared undo needs an explicit actor/action policy |

Here the starting document has an unused component. Alice deletes it; Bob creates an instance. Each branch is structurally valid; combining Alice’s removal with Bob’s reference is not. This is distinct from deleting a component with five instances: the pinned model refuses that deletion, and a separate Lean witness represents that refusal policy.

theorem component_conflict_has_valid_branches :
    StructurallyValid withComponent ∧ StructurallyValid deleted ∧ StructurallyValid inserted ∧
    ¬ StructurallyValid mergedDeletion := by decide

Concurrency also defines a small pointwise maximum register model, proves its commutative, associative and idempotent merge laws, and proves that its reference validity predicate is not closed under merge. This formally separates convergence from application validity. The register model is not Loro’s implementation and its tokens are event versions, not numerical maxima of user property values.

5. When independent work is safe

The positive result uses read and write sets. A transaction must leave fields outside its writes unchanged, and its written results must depend only on its declared reads. The two transactions must satisfy:

structure Independent (a b : Transaction Key Value) : Prop where
  writesDisjoint : ∀ k, k ∈ a.writes → k ∉ b.writes
  aReadsUnaffected : ∀ k, k ∈ a.reads → k ∉ b.writes
  bReadsUnaffected : ∀ k, k ∈ b.reads → k ∉ a.writes

Under those hypotheses, their execution order cannot affect the final state:

theorem independent_transactions_commute (a b : Transaction Key Value)
    (ind : Independent a b) (s : Store Key Value) : b.run (a.run s) = a.run (b.run s) := by
  have ar : AgreeOn a.reads s (b.run s) := by
    intro k hk
    exact (b.frame s k (ind.aReadsUnaffected k hk)).symm
  have br : AgreeOn b.reads s (a.run s) := by
    intro k hk
    exact (a.frame s k (ind.bReadsUnaffected k hk)).symm
  funext k
  by_cases ha : k ∈ a.writes
  · rw [b.frame (a.run s) k (ind.writesDisjoint k ha)]
    exact a.dependsOnReads s (b.run s) ar k ha
  · by_cases hb : k ∈ b.writes
    · rw [a.frame (b.run s) k ha]
      exact (b.dependsOnReads s (a.run s) br k hb).symm
    · rw [b.frame (a.run s) k hb, a.frame s k ha,
        a.frame (b.run s) k ha, b.frame s k hb]

This theorem quantifies over arbitrary keys, values and starting states. It is stronger than checking a few edits. Its hypotheses are also substantial: reads must include variable and style resolution, component consumers, parent layout, connector effects and anything that decides whether a command is refused. Writes must include induced changes, not just the selected layers.

A separate counterexample proves that disjoint writes alone do not suffice: one operation can read a field the other writes. Frame boundaries and selected node IDs therefore cannot by themselves establish independence. The repository does not yet have a certified dependency extractor or a proof that production commands meet these hypotheses. Those are concrete remaining obligations, not assumptions hidden in a claim that multiplayer is safe.

6. Layout agreement is a separate property

A measurement input identifies authored state, resources, available fonts and the engine version. stale_measurement_refused proves rejection when the input does not match. But two fresh measurements can still disagree:

theorem fresh_measurements_can_disagree :
    accept exampleInput (measure (fun _ => (100, 20)) exampleInput) = some (100, 20) ∧
    accept exampleInput (measure (fun _ => (101, 20)) exampleInput) = some (101, 20) := by decide

The theorem uses two different measurement functions with the same declared input. A version check cannot establish numerical agreement. We prove equality of derived geometry only with an explicit measurement-agreement hypothesis. No theorem asserts that the present browser and Skia implementations satisfy it.

There are two specified directions, neither implemented by this branch:

• Keep local layout outside replicated authored state. We prove it cannot alter that state; this does not promise identical layout or pixels.
• Replicate a concrete computed result rather than re-running its calculation at each receiver. Replay can then use the same value, but freshness, dependency completeness, conflict resolution and authority still need proofs.

A further witness shows why an authored document version alone is insufficient: the font/resource input may change without that version changing. Complete input identities are used in Lean; replacing them with hashes would add a collision assumption that is not present in these proofs.

7. History and identity

The current DocumentStore has branching snapshot history. A history group can amend the current commit without replacing its ID:

theorem equal_commit_id_does_not_imply_equal_document :
    ∃ a b : Revision, a.id = b.id ∧ a.document ≠ b.document := by
  exact ⟨{ id := 1, document := {} }, { id := 1, document := { title := 2 } }, rfl, by decide⟩

That behavior is useful for local undo but incompatible with treating a commit ID as immutable event identity. A replicated event log needs its own stable identity and causal order. Whether human undo overwrites a collaborator’s later value, and how guarded agent reversal behaves, remain product semantics to specify. The field-inverse theorem proves preservation only for a different field; it deliberately says nothing about same-field conflicts.

8. Proof limits and remaining work

The current findings do not depend on trusting a CRDT library. They expose obligations at the application layer above any convergent store.

| Obligation | Status | | --- | --- | | Structural namespaces and operation inventory | Defined for the pinned source revision | | Concrete concurrency failures | Proved for the abstraction | | Sufficient read/write independence conditions | Proved for abstract total transactions | | Structural validation after successful structural batches | Proved; does not imply merge closure | | TypeScript-to-Lean extraction/refinement | Contract defined; not proved | | Complete codec and expression/property typing | Not formalized | | Group, auto-layout and component-cascade arithmetic | Dependencies identified; algorithms not verified | | Cross-platform text, font and renderer agreement | Explicit hypothesis; not proved | | Rich-text merge, topology edits, deletion and reference-resolution policies | Need operation-specific specifications and proofs | | Loro algorithm, delivery protocol, atomic publication, persistence and migrations | Outside this branch |

The next design work should produce a dependency-complete command planner, choose merge policies for the failed invariants, and prove either merge closure or the soundness of a deterministic resolution layer. Merely wrapping CRDT imports in the current validator would reject some legitimate concurrent work; the counterexamples explain why.

9. Check the theorems independently

The project pins Lean 4.31.0 and depends only on its standard library. No Python, Node.js or application build is needed. From the repository root:

cd formal
lake build
lake env leanchecker Multiplayer Audit

Lake builds the model and its proof audit. The audit examines the transitive axiom dependencies of compiled project declarations, including private helpers, proof-valued definitions and generated declarations. Only Lean’s standard logical axioms are allowed; admitted proofs, custom axioms and native-evaluation shortcuts fail. The second command rechecks the compiled modules.

The source inventory in formal/source-map.json is documentation of the reviewed revision, not an enforcement mechanism. There are no source hashes or automatic checks against the TypeScript/C++ implementation. When applying a formal result to newer code, review the correspondence explicitly. The formalization and application may evolve independently.

The Lean workflow runs only for changes to Lean sources, the Lean toolchain/build configuration or the workflow itself, and for manual runs. It uses the project’s home Linux runner for same-repository pull requests and main, with GitHub-hosted Ubuntu for fork pull requests. Its only work is building, auditing and rechecking Lean proofs. It does not run application tests or documentation builds.

The documentation site is built separately through its existing command:

pnpm docs:api --skip-cpp

This chapter’s Lean blocks are read from the source files using the same snippet mechanism as the Electron guide. Building the documentation does not invoke Lean.