| # 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) | |