Model node tree editing in TLA+, and fix the four defects it found

[kmatzen]

Formal model of the node tree under editing, and the fixes for what it found.

specs/NodeTree.tla models the document shape under every gesture a user can make with a mouse — click a row to select, drag a row onto another row, drag a shape in from the palette, drop on empty canvas, press the X, Cmd-D, Cmd-C/Cmd-V, wrap from the Add menu — and checks five safety properties with TLC.

The tree is deliberately not modelled as a tree. kid is a general graph, because the implementation manipulates parent links and child arrays independently; whether the result is still a tree is the question, not an assumption. Kinds are abstracted to arity, with one distinction that does most of the work: text and mesh take no children but are not in NODE_KINDS.primitives, and addNodeFromData asks arity of the dropped node and list membership of the target.

What failed

Four of the five properties fail against the design as shipped.

Property	Depth	What it is
WithinCapacity	2	Import a mesh, drop a box on it → the box becomes a child of the mesh. toSDFNode reads children[0]/children[1] and nothing after, so it never reaches the mesher; incompleteNodeIds flags only nodes with too few children, so nothing warns. The shape is in the outline and is not in the model. Five more paths reach the same state by appending past a kind's arity — move, duplicate, paste, add-child, and the last branch of the palette drop.
IsATree	5	Drag an operation that wraps one shape onto another node. moveNode deletes the source with removeFromTree, whose promote-sole-child rule hands the shape up into the vacated slot, then re-attaches the source still holding it. One id, two places — findNode sees only the first, updateInTree rewrites both.
NoSilentLoss	5	Delete one operand of a union, then delete the union. The vacated slot holds an _empty, so children.length is still 2, so the survivor is not promoted — it is destroyed. Deleting a union that had never lost an operand would have promoted it.
SelectionValid	4	Delete an ancestor of the selected node. removeNode cleared the selection only when the removed id was the selected one, so it dangles; addNodeFromData then bails at if (!targetNode) return, and the palette stops responding with nothing on screen to say why.

Acyclic holds at this bound, but only conditionally — the model's descendant guard consults the true graph where the implementation's findNode sees only the first occurrence of a duplicated id. That is an argument for fixing IsATree, not a reason to relax about cycles.

The fixes

Verified in specs/NodeTreeFixed.tla: all five properties hold, exhaustively at MaxNodes=6, MaxOps=4 (11,301 states) and again at MaxNodes=7, MaxOps=5 (280,582 distinct states, depth 6).

1. moveNode detaches instead of deleting. removeFromTree takes a promote flag; a move passes false, so the subtree travels whole.
2. One attachChild. Fill a vacated slot; else append if the kind has room; else the parent is full, so replace it in place with a union of itself and the newcomer. Every append site routes through it. Unioning in place is not a new gesture — it is what addPrimitive does to the root and what dropping a shape on a shape already did.
3. The drop target is classified by arity, the same question already asked of the dropped node.
4. Promotion counts real operands, and the selection is clamped in commit — the one funnel every mutator already goes through, and where surviving was already being used for undo/redo.

Verification

• All nine counterexamples replayed against the store in src/store/modelerStore.treeShape.test.ts. They fail against the old design and pass against the new one, alongside three controls that must not change.
• Full suite: 515 passed, 3 skipped, 0 failed. tsc --noEmit clean.
• specs/check.sh now runs both specs; NodeTree is expected to produce a counterexample, as WorkerBridge and UndoHistory already are.

One existing test asserted that a drag into a full union yields three children. That assertion was the defect, and it is updated to the capacity-respecting shape.

Reported and deliberately not changed

An operation dragged to empty canvas falls through every branch of addNodeFromData and does nothing, silently. The model reports it. It loses nothing, breaks no invariant, and is asserted by an existing test, so it is documented in specs/README.md and left alone — a UX gap rather than a defect.

🤖 Generated with Claude Code

[github-actions]

🚀 Preview deployed: https://worktree-tla-node-tree.sinter.pages.dev

(updates on every push to this PR)