Prove tap-to-position is scroll-offset independent; fix float32 decomposition bug

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.
This commit is contained in:
Greg Pomerantz 2026-08-17 09:57:21 -04:00
parent 7f2d3144eb
commit e761436908
6 changed files with 280 additions and 29 deletions

View File

@ -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

View File

@ -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

View File

@ -1,8 +1,9 @@
# Development Plan: reach a lean, usable Android text editor
Status: v8, 2026-08-17 (Phases 03 + doc reorg + Phase 6 scroll-perf/clamping
Status: v9, 2026-08-17 (Phases 03 + 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

View File

@ -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

View File

@ -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

View File

@ -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)
}
}
}