From e761436908ab7a42eb4f6373ee04e8ebc32ce318 Mon Sep 17 00:00:00 2001 From: Greg Pomerantz Date: Mon, 17 Aug 2026 09:57:21 -0400 Subject: [PATCH] Prove tap-to-position is scroll-offset independent; fix float32 decomposition bug MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The screen->line tap mapping only needs the sub-line scroll remainder (tapLocalY adds r, never the full scroll) because the visible glyph layout is window-relative and IMEWindowStartByte re-anchors it to the file. That holds for every scroll offset IF the window start line k=floor(s/lh) and the sub-line remainder r stay consistent. Property test (4000 random scroll/tap pairs, asserting against an independent drawn-geometry ground truth, not the tap code's own math) exposed a real bug: int(s/lh) in the Dp float32 domain rounds the quotient to nearest and can round UP across an integer boundary while the float64 mod still reflects the line below. In a sub-pixel-wide band of scroll offsets the window started one line too far while the draw shift lagged by one line - the whole rendered window (and every tapped line) shifted by one. Fix: one shared float64 floor decomposition (scrollDecompose) used by the window start (visibleByteRangePrecise/Estimate), the renderer's sub-line shift (visibleScrollOffset), the tap mapping (tapLocalY), and chunk prefetching. Also route the shaper's line height (previously ignored by visibleByteRangePrecise) through VisibleByteRange. On-device cross-check: at s=4246.9 (r=13.3) and s=4210.7 (r=10.7), taps on visually identified lines typed markers that landed on exactly those lines in the file on disk; profiler ScrollDP, screenshot, formula, and disk all agreed. Docs: scroll decomposition invariant in architecture.md §6.2, pipeline hop 2 in doc/README.md, Phase 10 in development_plan.md. --- doc/README.md | 14 ++- doc/architecture.md | 13 ++ doc/development_plan.md | 50 +++++++- internal/editor/chunked_buffer.go | 37 ++++-- internal/editor/state.go | 63 ++++++++-- internal/editor/tap_scroll_property_test.go | 132 ++++++++++++++++++++ 6 files changed, 280 insertions(+), 29 deletions(-) create mode 100644 internal/editor/tap_scroll_property_test.go diff --git a/doc/README.md b/doc/README.md index b38985b..11f6612 100644 --- a/doc/README.md +++ b/doc/README.md @@ -105,10 +105,16 @@ hops, not inside a space): this is the only space `adb`/screenshots touch. 2. **app dp → text-local dp** — the tap/drag handlers (`localX = x − EditorRegion.X`, `localY = tapLocalY(...)`). - **Y adds only the sub-line scroll remainder** (`ScrollOffset mod - lineHeight`), never the full scroll: the visible glyph layout is - window-relative, so adding the full scroll maps a tap to a line far - below the window (the Phase 7 tap-to-position bug). + **Y adds only the sub-line scroll remainder**, never the full scroll: + the visible glyph layout is window-relative, so adding the full scroll + maps a tap to a line far below the window (the Phase 7 tap-to-position + bug). The remainder and the window's start line come from ONE shared + float64 floor decomposition of `ScrollOffset` (line k, remainder r, with + k·lineHeight ≤ ScrollOffset < (k+1)·lineHeight): the window starts at + content line k, the renderer shifts the windowed layout up by r, and a + tap a dp below the region top maps to content line k + + ⌊(a+r)/lineHeight⌋ = ⌊(a+ScrollOffset)/lineHeight⌋ — the line actually + under the finger, for every scroll offset (architecture.md §6.2). 3. **text-local dp → window-relative glyph byte** — `visualLine = y / lineHeight`, then glyph x-search within that line group. `GlyphLayout.ByteOffsets` are relative to the **top of the diff --git a/doc/architecture.md b/doc/architecture.md index 1638952..a7456fa 100644 --- a/doc/architecture.md +++ b/doc/architecture.md @@ -233,6 +233,19 @@ Only the visible byte range is shaped and drawn each frame: - `VisibleByteRange` maps scroll offset + viewport height → `[startLine, endLine]` via the `LineIndex`, then to a byte range. The range is always bounded by real lines of the document. +- **Scroll decomposition invariant.** The scroll offset s is split into a + content line k and sub-line remainder r (k·lh ≤ s < (k+1)·lh) by a single + float64 floor decomposition, and the three consumers of that split MUST + stay in lockstep: the window start line (VisibleByteRange), the renderer's + sub-line shift (the windowed layout is drawn shifted up by r), and the tap + mapping (`tapLocalY` adds r). With them consistent, a tap a dp below the + region top always maps to content line k + ⌊(a+r)/lh⌋ = + ⌊(a+s)/lh⌋ — the line actually under the finger — for every s ≥ 0. The + decomposition must be computed in float64: a raw `int(s/lh)` in the Dp + float32 domain can round the quotient UP across an integer boundary while + a float64 mod still reflects the line below, so the window start and the + remainder disagree by one line in a sub-pixel-wide band of offsets and the + whole rendered window (hence every tapped line) shifts by one. - **Never shape the whole file.** Lesson learned (Phase 3): the shaper's internal `document` retains the backing array of its largest layout forever (`reset()` keeps the cap), so one whole-file layout permanently inflated diff --git a/doc/development_plan.md b/doc/development_plan.md index 1f14828..2453893 100644 --- a/doc/development_plan.md +++ b/doc/development_plan.md @@ -1,8 +1,9 @@ # Development Plan: reach a lean, usable Android text editor -Status: v8, 2026-08-17 (Phases 0–3 + doc reorg + Phase 6 scroll-perf/clamping +Status: v9, 2026-08-17 (Phases 0–3 + doc reorg + Phase 6 scroll-perf/clamping verification + tap-to-position-cursor fix + selection + real-file e2e + -Android arrow/shift workaround + touch selection). Written +Android arrow/shift workaround + touch selection + scroll-offset tap proof & +float32 decomposition fix). Written against the **live** repo `/home/gmp/pad`. v1 (the widget-rebuild plan) is superseded — see §12 for why. Doc reorganization (2026-08-16): the over-detailed docs (`*_implementation_plan.md`, `touch.md`, `element_model.md`, @@ -24,7 +25,13 @@ refactor); fixed with `tapLocalY`. (2) the `GlyphLayout` byte offsets are window-relative but the four cursor functions (tap, Home, End, vertical move) treated them as absolute, so the cursor snapped to the window top; fixed by adding the `IMEWindowStartByte` window base at each cursor boundary (`glyphBase`). Both -have regression tests. +have regression tests. Phase 10 (2026-08-17) proved the tap mapping +scroll-offset independent by property test (4000 random scroll/tap pairs) and +on-device (marker typed on a visually identified line landed on exactly that +line at two fractional scroll positions); the property test exposed a float32 +`int(s/lh)` rounding bug that could shift the rendered window — and every +tapped line — by one in a sub-pixel band of scroll offsets, now fixed with a +single shared float64 floor decomposition (see §5, Phase 10). Phase 8 (2026-08-16/17) added **text selection** (shift+arrow extend; insert/ backspace/delete replace the selection; IME unions its range with the active selection) with rendering + IME wiring. It also added **real-file e2e tests** @@ -410,6 +417,43 @@ contracts; the highlights: menu close-on-tap, plain-tap caret placement, and scroll-drag not firing a long press. +### Phase 10 — proving tap-to-position is scroll-offset independent — DONE (2026-08-17) + +Question: does the screen→line tap mapping account for the scroll offset, and +can it be shown to map a screen tap to the right document line at *any* scroll +offset? The answer was "yes, except one razor-thin band" — and the exception is +now fixed and property-tested. + +- **The mapping is structurally scroll-aware.** The visible glyph layout is + window-relative, so a tap only needs the *sub-line* remainder of the scroll + offset (`tapLocalY` adds r, never the full scroll), and the window start + line k = floor(s/lh) re-anchors window-relative bytes to absolute file bytes + (`IMEWindowStartByte`). With k and r consistent, a tap a dp below the region + top always lands on content line k + ⌊(a+r)/lh⌋ = ⌊(a+s)/lh⌋ — the line + under the finger — for every s ≥ 0, wrapped or not (wrap only changes which + real line a display line belongs to, never the drawn geometry). +- **Bug found by the property test:** `int(s/lh)` in the Dp float32 domain + rounds the quotient to nearest, and can round UP across an integer boundary + while the float64 remainder still reflects the line below. In a + sub-pixel-wide band of scroll offsets the window started one line too far + while the draw shift said one line back — the whole rendered window (and + every tapped line) was off by one. Fixed with a single shared float64 floor + decomposition (`scrollDecompose`) used by the window start + (`visibleByteRangePrecise`/`Estimate`), the renderer's sub-line shift + (`visibleScrollOffset`), the tap mapping (`tapLocalY`), and chunk + prefetching — the three consumers cannot disagree by construction. +- **Proof:** `tap_scroll_property_test.go` — 4000 random (scroll offset, tap + position) pairs (integer-line, near-boundary, and arbitrary fractional + offsets) assert the cursor lands on the line whose *independently computed* + drawn range contains the finger (ground truth ⌊(a+s)/lh⌋, not the tap code's + own math). Failed on the exact-boundary case before the fix; green after. +- **On-device cross-check:** at two scroll positions (s = 4246.9 dp, r = 13.3; + s = 4210.7 dp, r = 10.7, both with a fractional sub-line remainder read + from the profiler CSV), a tap on a visually identified line typed a marker + that landed on exactly that line in the file on disk (line 264 and line 258 + of a 300-line file). Screenshot, profiler ScrollDP, formula, and disk all + agreed. + ## 6. File-size decision (re-framed) v1 framed this as "accept a limit vs build a windowed editor." The live repo diff --git a/internal/editor/chunked_buffer.go b/internal/editor/chunked_buffer.go index 522bc77..4ba088b 100644 --- a/internal/editor/chunked_buffer.go +++ b/internal/editor/chunked_buffer.go @@ -2,6 +2,7 @@ package editor import ( "bytes" + "math" "sort" "strings" @@ -441,22 +442,27 @@ func (cb *ChunkedBuffer) VisibleByteRange(scrollOffset ui.Dp, byteOffset int, vi // least one visual line, so shaping viewportHeight/lineHeight real lines // always yields at least as many visual lines as fit in the viewport. The // extra wrapped lines are simply clipped by the renderer. + lineH := lineHeight + if lineH <= 0 { + lineH = EditorLineHeight() + } if cb.LineIndex == nil { - start, end = cb.visibleByteRangeEstimate(scrollOffset, viewportHeight) + start, end = cb.visibleByteRangeEstimate(scrollOffset, viewportHeight, lineH) return start, end, 0 } - start, end = cb.visibleByteRangePrecise(scrollOffset, viewportHeight) + start, end = cb.visibleByteRangePrecise(scrollOffset, viewportHeight, lineH) return start, end, 0 } // visibleByteRangeEstimate approximates the visible byte range using // heuristic estimates. Used when the line index is not yet available. -func (cb *ChunkedBuffer) visibleByteRangeEstimate(scrollOffset ui.Dp, viewportHeight ui.Dp) (start, end int) { - // Use the editor's line height constant for consistency. - lineHeight := EditorLineHeight() +func (cb *ChunkedBuffer) visibleByteRangeEstimate(scrollOffset ui.Dp, viewportHeight ui.Dp, lineHeight ui.Dp) (start, end int) { + if lineHeight <= 0 { + lineHeight = EditorLineHeight() + } - startLine := int(scrollOffset / lineHeight) - endLine := int((scrollOffset + viewportHeight) / lineHeight) + startLine, _ := scrollDecompose(scrollOffset, lineHeight) + endLine := int(math.Ceil(float64(scrollOffset+viewportHeight) / float64(lineHeight))) // Clamp line numbers to reasonable bounds totalLinesEstimate := 0 @@ -522,15 +528,20 @@ func (cb *ChunkedBuffer) visibleByteRangeEstimate(scrollOffset ui.Dp, viewportHe } // visibleByteRangePrecise uses the LineIndex to find the exact byte range. -func (cb *ChunkedBuffer) visibleByteRangePrecise(scrollOffset ui.Dp, viewportHeight ui.Dp) (start, end int) { +func (cb *ChunkedBuffer) visibleByteRangePrecise(scrollOffset ui.Dp, viewportHeight ui.Dp, lineHeight ui.Dp) (start, end int) { if cb.LineIndex == nil || len(cb.LineIndex.Offsets) == 0 { - return cb.visibleByteRangeEstimate(scrollOffset, viewportHeight) + return cb.visibleByteRangeEstimate(scrollOffset, viewportHeight, lineHeight) + } + if lineHeight <= 0 { + lineHeight = EditorLineHeight() } - lineHeight := EditorLineHeight() - - startLine := int(scrollOffset / lineHeight) - endLine := int((scrollOffset + viewportHeight) / lineHeight) + // startLine must use the same floor decomposition as the renderer's + // sub-line shift and tapLocalY (scrollDecompose); a raw int(s/lh) in the + // Dp float32 domain can round the quotient up across an integer boundary + // and disagree with the remainder by one line. + startLine, _ := scrollDecompose(scrollOffset, lineHeight) + endLine := int(math.Ceil(float64(scrollOffset+viewportHeight) / float64(lineHeight))) if startLine < 0 { startLine = 0 diff --git a/internal/editor/state.go b/internal/editor/state.go index 25af123..da69ce3 100644 --- a/internal/editor/state.go +++ b/internal/editor/state.go @@ -3,7 +3,6 @@ package editor import ( "fmt" "log" - "math" "sort" "time" "unicode" @@ -1645,23 +1644,27 @@ func EditorLayout(screenWidth, screenHeight ui.Dp, wordWrap bool) []ui.Element { } // Adjust scroll offset to be relative to visibleContent origin - visibleScrollOffset = ui.Dp(math.Mod(float64(TheState.ScrollOffset), float64(lineHeight))) + // Sub-line shift for the renderer: the SAME decomposition the window + // start used (VisibleByteRange above), so the drawn geometry and the + // window's content lines agree for every scroll offset. + _, subLine := scrollDecompose(TheState.ScrollOffset, lineHeight) + visibleScrollOffset = ui.Dp(subLine) // Map scroll offset to a chunk index // Estimate line-to-byte conversion if LineIndex is missing var scrollByteOffset int if li := cb.LineIndex; li != nil { - // Precise - lineHeight := EditorLineHeight() - startLine := int(TheState.ScrollOffset / lineHeight) - if startLine < li.LineCount() { - scrollByteOffset = li.ByteOffset(startLine) + // Precise: same decomposition as the window start above. + prefetchLine, _ := scrollDecompose(TheState.ScrollOffset, lineHeight) + if prefetchLine < li.LineCount() { + scrollByteOffset = li.ByteOffset(prefetchLine) } else { scrollByteOffset = int(cb.FileLen()) } } else { // Estimate - scrollByteOffset = int(TheState.ScrollOffset/EditorLineHeight()) * 50 + prefetchLine, _ := scrollDecompose(TheState.ScrollOffset, EditorLineHeight()) + scrollByteOffset = prefetchLine * 50 } scrollChunk := scrollByteOffset / cb.ChunkSize() @@ -1762,8 +1765,50 @@ func EditorLayout(screenWidth, screenHeight ui.Dp, wordWrap bool) []ui.Element { // window's line count, clamping the cursor to the bottom line of the viewport on // any large file (it only worked by luck on small files whose window spanned the // tapped content-line number). +// scrollDecompose splits a scroll offset s into content line k and sub-line +// remainder r such that k*lh <= s < (k+1)*lh — the floor decomposition in the +// Dp domain, computed in float64. +// +// k and r must be the SINGLE shared source of both the window start line +// (visibleByteRangePrecise/Estimate) and the sub-line draw/tap remainder +// (visibleScrollOffset in layoutFrame, tapLocalY). Computing k as +// int(s/lh) in the Dp float32 domain can round the quotient UP across an +// integer boundary while the (float64) remainder still reflects the line +// below; the two bookkeeping values then disagree by one line in a +// sub-pixel-wide band of scroll offsets, shifting the rendered window — and +// with it every tapped content line — by one. The float64 decomposition with +// the r<0 / r>=lh corrections keeps k and r consistent for every s >= 0. +func scrollDecompose(s ui.Dp, lh ui.Dp) (k int, r float64) { + sf, lf := float64(s), float64(lh) + if lf <= 0 { + return 0, 0 + } + k = int(sf / lf) + r = sf - float64(k)*lf + if r < 0 { + k-- + r = sf - float64(k)*lf + } + if r >= lf { + k++ + r = sf - float64(k)*lf + } + if k < 0 { + k, r = 0, sf + } + return k, r +} + func tapLocalY(ptY, regionTopY ui.Dp, scrollOffset ui.Dp) float64 { - return float64(ptY-regionTopY) + math.Mod(float64(scrollOffset), float64(EditorLineHeight())) + // Same line height the renderer used to shape the window, and the same + // floor decomposition as the window start, so the tap maps to the drawn + // geometry for every scroll offset. + lh := EditorLineHeight() + if gl := TheState.Editor.GlyphLayout; gl.LineHeight > 0 { + lh = gl.LineHeight + } + _, r := scrollDecompose(scrollOffset, lh) + return float64(ptY-regionTopY) + r } // SetCursorFromPoint updates the cursor position based on text-local diff --git a/internal/editor/tap_scroll_property_test.go b/internal/editor/tap_scroll_property_test.go new file mode 100644 index 0000000..cd20c04 --- /dev/null +++ b/internal/editor/tap_scroll_property_test.go @@ -0,0 +1,132 @@ +package editor + +import ( + "fmt" + "math" + "math/rand" + "testing" + + "pad/internal/io/pool/types" + "pad/internal/ui" +) + +// This file proves the scroll-offset independence of tap-to-position. +// +// The invariant under test, for a no-wrap file where content line n occupies +// content-y [n*lh, (n+1)*lh): +// +// For every scroll offset s >= 0 and every tap point ptY inside the visible +// region, the cursor must land on the content line whose DRAWN range +// contains the tap. Drawn range of window display line j is +// [reg.Y - r + j*lh, reg.Y - r + (j+1)*lh), where r = s mod lh (the +// renderer shifts the windowed layout up by exactly r: +// `y := reg.Y - scrollOffset` in drawWrappedText, scrollOffset = +// Mod(ScrollOffset, lineHeight)). +// +// Independent ground truth: content_y = (ptY - reg.Y) + s, so the tapped +// content line is floor(content_y / lh). That formula uses only "the content +// is shifted up by s" — it does NOT reuse tapLocalY. +// +// The code path under test is HandleTapAt -> tapLocalY -> SetCursorFromPoint +// -> textPosFromLocalPoint, with a GlyphLayout fabricated the way the +// windowed layout is (window display line j = content line k+j, baseline +// (j+1)*lh, window-relative byte offsets) and IMEWindowStartByte set to the +// same line k = floor(s/lh) that visibleByteRangePrecise picks +// (startLine := int(scrollOffset / lineHeight)). +// +// If the window-start coupling, the draw shift, or tapLocalY's sub-line +// remainder ever disagree, this test fails for some (s, ptY) pair. +func TestTapPosition_ScrollInvariant_Property(t *testing.T) { + const ( + lines = 500 + bytesPerLine = 5 // "L123\n" + regionTop = float64(62) // editor region top, app dp (matches layoutFrame) + viewportH = float64(760) // app dp + ) + lineHeight := float64(EditorLineHeight()) + // Build the file once. + var file string + for i := 0; i < lines; i++ { + file += fmt.Sprintf("L%03d\n", i) + } + cb := NewChunkedBuffer("/prop.txt", DefaultChunkSize, nil, "") + cb.SetContent([]byte(file)) + + // Build the same line index the BuildLineIndex task produces. + offsets := []int32{0} + for i := 0; i < len(file); i++ { + if file[i] == '\n' { + offsets = append(offsets, int32(i+1)) + } + } + cb.LineIndex = types.NewLineIndex(offsets, 0, int64(len(file))) + + rng := rand.New(rand.NewSource(42)) + maxS := float64(lines) * lineHeight + + for tc := 0; tc < 4000; tc++ { + // Random scroll offset: a mix of small, large, integer-line and + // fractional-line values. + var s float64 + switch tc % 4 { + case 0: + s = rng.Float64() * maxS // anywhere + case 1: + s = float64(int(rng.Float64() * maxS)) // exact integer dp + case 2: + s = float64(rng.Intn(lines)) * lineHeight // exact line boundary + case 3: + s = float64(rng.Intn(lines))*lineHeight + rng.Float64()*(lineHeight-1) // near boundary + } + sOff := ui.Dp(s) + + // What layoutFrame/visibleByteRangePrecise does: window starts at + // content line k = floor(s / lh). + start, _, _ := cb.VisibleByteRange(sOff, 0, ui.Dp(viewportH), EditorLineHeight(), false, ui.GlyphLayout{}, nil) + if start%bytesPerLine != 0 { + t.Fatalf("test setup: window start %d not on a line boundary", start) + } + k := start / bytesPerLine + + // Fabricate the windowed GlyphLayout exactly as the shaper would for + // a no-wrap file: window display line j = content line k+j. + nWin := int(math.Min(viewportH/lineHeight+2, float64(lines-k))) + var gl ui.GlyphLayout + for j := 0; j < nWin; j++ { + gl.ByteOffsets = append(gl.ByteOffsets, j*bytesPerLine) + gl.X = append(gl.X, 10) + gl.Y = append(gl.Y, ui.Dp(float64(j+1)*lineHeight)) + gl.Advance = append(gl.Advance, 10) + } + + TheState = NewState() + TheState.Editor.ChunkedBuffer = cb + TheState.Editor.GlyphLayout = gl + TheState.Editor.IMEWindowStartByte = start + TheState.ScrollOffset = sOff + TheState.EditorRegion = ui.Region{X: 10, Y: ui.Dp(regionTop), W: 390, H: ui.Dp(viewportH)} + + // Random tap inside the visible region. + a := rng.Float64() * viewportH // tap y relative to region top + ptY := ui.Dp(regionTop + a) + + HandleTapAt(15, ptY) + + // Independent ground truth: content_y = a + s -> content line. + wantLine := int(math.Floor((a + s) / lineHeight)) + if wantLine >= lines { + wantLine = lines - 1 + } + // Taps below the last shaped window line clamp to it (no glyphs + // further down), matching textPosFromLocalPoint's documented clamp. + if k+nWin-1 < wantLine { + wantLine = k + nWin - 1 + } + got := TheState.Editor.CursorPosition + wantLo, wantHi := wantLine*bytesPerLine, wantLine*bytesPerLine+bytesPerLine + if got < wantLo || got >= wantHi { + t.Fatalf("s=%.2f (k=%d) tap a=%.2f: cursor=%d, want line %d [bytes %d,%d)", + s, k, a, got, wantLine, wantLo, wantHi) + } + } +}