layer-3-text-buffer/README.md

Layer 3 — Text Buffer / Rope (8000 lines target)

What This Layer Does

The core data structure for editable text: a rope (balanced binary tree of string chunks) supporting O(log n) insert, delete, and slice. Also owns the undo tree — a persistent branching history of all edits.

Repos That Contribute

Repo	What to pull
errant	QTT tagged memory for rope nodes; Linear Forth ISA pattern for undo stack
sovereign-array	Lean 4 array language — formal proof of rope invariants; C++20 array ops as rope leaf implementation

What to Build First

1. Rope node type — leaf (u8 slice) and branch (left+right child, cached length)
2. Rope concat / split — fundamental O(log n) ops
3. Rope insert / delete — built on concat/split
4. Line index — O(log n) byte-offset to line/col
5. Undo tree — persistent snapshot with branching (not linear stack)
6. Rope invariant proofs — port from sovereign-array Lean 4 proofs

Key Design Constraints

• Rope nodes allocated from Layer 0 arena; never heap-malloc after init
• Undo tree nodes also in arena; compacted on checkpoint
• QTT tags from errant: each rope leaf carries a provenance tag (for LSP sync)
• Lean 4 proofs from sovereign-array must hold: size(concat(a,b)) = size(a)+size(b)