else
        acc
    else
      acc
    termination_by s.bsize - i.1
  loop 0 0 ""
/-- Normalize invalid tab stop values.
    Tab stop 0 would break modulo logic, so clamp to 1. -/
def normalizeTabStop (tabStop : Nat) : Nat :=
  if tabStop == 0 then 1 else tabStop
/-- Display width contribution of a tab at a given display column. -/
def tabWidthAt (tabStop : Nat) (col : Nat) : Nat :=
  let ts := normalizeTabStop tabStop
  let rem := col % ts
  if rem == 0 then ts else ts - rem
/-- Character width with tab-stop awareness. -/
def charWidthAt (tabStop : Nat) (col : Nat) (c : Char) : Nat :=
  if c == '\t' then
    tabWidthAt tabStop col
  else
    charWidth c
/-- Display text for a character with tab-stop awareness. -/
def getDisplayStringAt (tabStop : Nat) (col : Nat) (c : Char) : String :=
  if c == '\t' then
    "".pushn ' ' (tabWidthAt tabStop col)
  else
    getDisplayString c
/-- Calculate the total visual width of a string with tab-stop awareness. -/
def stringWidthWithTabStop (s : String) (tabStop : Nat) : Nat :=
  let rec loop (cs : List Char) (acc : Nat) : Nat :=
    match cs with
    | [] => acc
    | c :: rest =>
      let w := charWidthAt tabStop acc c
      loop rest (acc + w)
  loop s.toList 0
/-- Calculate the total visual width of a substring with tab-stop awareness. -/
def substringWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) : Nat :=
  let rec loop (i : String.Pos.Raw) (acc : Nat) : Nat :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let i' := s.next i
      have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
      let w := charWidthAt tabStop acc c
      loop i' (acc + w)
    else
      acc
    termination_by s.bsize - i.1
  loop 0 0
/-- Convert a display column to a character index (0-based), tab-stop aware. -/
def displayColToCharIndexWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=
  let rec loop (cs : List Char) (idx width : Nat) : Nat :=
    match cs with
    | [] => idx
    | c :: rest =>
      let w := charWidthAt tabStop width c
      if width + w > col then
        idx
      else
        loop rest (idx + 1) (width + w)
  loop s.toList 0 0
/-- Display width of the first `idx` characters in a string, tab-stop aware. -/
def displayWidthAtCharIndexWithTabStop (s : String) (tabStop : Nat) (idx : Nat) : Nat :=
  let rec loop (cs : List Char) (i acc : Nat) : Nat :=
    match cs with
    | [] => acc
    | c :: rest =>
      if i >= idx then
        acc
      else
        let w := charWidthAt tabStop acc c
        loop rest (i + 1) (acc + w)
  loop s.toList 0 0
/-- Convert a display column to a UTF-8 byte offset within a string, tab-stop aware. -/
def displayColToByteOffsetWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=
  let rec loop (cs : List Char) (byteAcc widthAcc : Nat) : Nat :=
    match cs with
    | [] => byteAcc
    | c :: rest =>
      let w := charWidthAt tabStop widthAcc c
      let b := c.toString.toUTF8.size
      if widthAcc + w > col then
        byteAcc
      else
        loop rest (byteAcc + b) (widthAcc + w)
  loop s.toList 0 0
/-- Build display-column to byte-offset index with tab-stop awareness. -/
def buildDisplayByteIndexWithTabStop (s : String) (tabStop : Nat) : Array (Nat × Nat) :=
  let rec loop (cs : List Char) (disp bytes : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=
    match cs with
    | [] => acc
    | c :: rest =>
      let w := charWidthAt tabStop disp c
      let b := c.toString.toUTF8.size
      let disp' := disp + w
      let bytes' := bytes + b
      loop rest disp' bytes' (acc.push (disp', bytes'))
  loop s.toList 0 0 #[(0, 0)]
/-- Compute next display column (one character advance), tab-stop aware. -/
def nextDisplayColWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=
  let idx := displayColToCharIndexWithTabStop s tabStop col
  let startWidth := displayWidthAtCharIndexWithTabStop s tabStop idx
  if col < startWidth then
    startWidth
  else
    let chars := s.toList
    if idx < chars.length then
      let w := charWidthAt tabStop startWidth (chars[idx]!)
      startWidth + w
    else
      col
/-- Compute previous display column (one character back), tab-stop aware. -/
def prevDisplayColWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=
  if col == 0 then
    0
  else
    let idx := displayColToCharIndexWithTabStop s tabStop col
    let startWidth := displayWidthAtCharIndexWithTabStop s tabStop idx
    if col > startWidth then
      startWidth
    else if idx == 0 then
      0
    else
      displayWidthAtCharIndexWithTabStop s tabStop (idx - 1)
/-- Drop `width` display columns from substring start, tab-stop aware. -/
def dropByDisplayWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) (width : Nat) : Substring.Raw :=
  let rec loop (i : String.Pos.Raw) (acc : Nat) : Substring.Raw :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let w := charWidthAt tabStop acc c
      if acc + w > width then
        s.extract i ⟨s.bsize⟩
      else
        let i' := s.next i
        have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
        loop i' (acc + w)
    else
      s.extract i ⟨s.bsize⟩
    termination_by s.bsize - i.1
  loop 0 0
/-- Take characters from substring until visual width limit, tab-stop aware. -/
def takeByDisplayWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) (width : Nat) : String :=
  let rec loop (i : String.Pos.Raw) (currW : Nat) (acc : String) : String :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let w := charWidthAt tabStop currW c
      if currW + w <= width then
        let i' := s.next i
        have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
        loop i' (currW + w) (acc ++ getDisplayStringAt tabStop currW c)

      let lineIndex := cachedIdx.getD (ViE.Unicode.buildDisplayByteIndex lineStr)

      let lineIndex := cachedIdx.getD (ViE.Unicode.buildDisplayByteIndexWithTabStop lineStr state.config.tabStop)

                  let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
                  let dl := takeVisual sub availableWidth

                  let sub := ViE.Unicode.dropByDisplayWidthWithTabStop lineStr.toRawSubstring state.config.tabStop view.scrollCol.val
                  let dl := ViE.Unicode.takeByDisplayWidthWithTabStop sub state.config.tabStop availableWidth

                          (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))

                          (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndexWithTabStop lineStr state.config.tabStop))

                        (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))

                        (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndexWithTabStop lineStr state.config.tabStop))

              let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
              let dl := takeVisual sub availableWidth

              let sub := ViE.Unicode.dropByDisplayWidthWithTabStop lineStr.toRawSubstring state.config.tabStop view.scrollCol.val
              let dl := ViE.Unicode.takeByDisplayWidthWithTabStop sub state.config.tabStop availableWidth

                      (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))

                      (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndexWithTabStop lineStr state.config.tabStop))

                    (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))

                    (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndexWithTabStop lineStr state.config.tabStop))

    let sub := ViE.Unicode.dropByDisplayWidth raw.toRawSubstring view.scrollCol.val
    let plainShown := takeVisual sub textW
    let shownW := Unicode.stringWidth plainShown

    let sub := ViE.Unicode.dropByDisplayWidthWithTabStop raw.toRawSubstring st.config.tabStop view.scrollCol.val
    let plainShown := ViE.Unicode.takeByDisplayWidthWithTabStop sub st.config.tabStop textW
    let shownW := Unicode.stringWidthWithTabStop plainShown st.config.tabStop

    buffer := buffer ++ renderFloatingOverlay rows cols overlay

    buffer := buffer ++ renderFloatingOverlay rows cols stateAfterLayout.config.tabStop overlay

        match computeFloatingOverlayLayout rows cols overlay with

        match computeFloatingOverlayLayout rows cols stateAfterLayout.config.tabStop overlay with

            let lineW := Unicode.stringWidth line

            let lineW := Unicode.stringWidthWithTabStop line stateAfterLayout.config.tabStop

def computeFloatingOverlayLayout (rows cols : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do

def computeFloatingOverlayLayout (rows cols : Nat) (tabStop : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do

  let naturalWidthContent := lines.foldl (fun acc ln => max acc (Unicode.stringWidth ln)) 0
  let naturalWidth := max naturalWidthContent (Unicode.stringWidth titleText)

  let naturalWidthContent := lines.foldl (fun acc ln => max acc (Unicode.stringWidthWithTabStop ln tabStop)) 0
  let naturalWidth := max naturalWidthContent (Unicode.stringWidthWithTabStop titleText tabStop)

def renderFloatingOverlay (rows cols : Nat) (overlay : FloatingOverlay) : Array String := Id.run do
  let some layout := computeFloatingOverlayLayout rows cols overlay | return #[]

def renderFloatingOverlay (rows cols : Nat) (tabStop : Nat) (overlay : FloatingOverlay) : Array String := Id.run do
  let some layout := computeFloatingOverlayLayout rows cols tabStop overlay | return #[]

    let clippedTitle := Unicode.takeByDisplayWidth titleText.toRawSubstring innerWidth
    out := out.push s!"| {rightPadVisual clippedTitle innerWidth} |"

    let clippedTitle := Unicode.takeByDisplayWidthWithTabStop titleText.toRawSubstring tabStop innerWidth
    let titleW := Unicode.stringWidthWithTabStop clippedTitle tabStop
    let titlePad := if titleW < innerWidth then "".pushn ' ' (innerWidth - titleW) else ""
    out := out.push s!"| {clippedTitle}{titlePad} |"

    let clipped := Unicode.takeByDisplayWidth raw.toRawSubstring innerWidth

    let clipped := Unicode.takeByDisplayWidthWithTabStop raw.toRawSubstring tabStop innerWidth
    let clippedW := Unicode.stringWidthWithTabStop clipped tabStop
    let pad := if clippedW < innerWidth then "".pushn ' ' (innerWidth - clippedW) else ""

    out := out.push s!"| {rightPadVisual clipped innerWidth} |"

    out := out.push s!"| {clipped}{pad} |"

  tabStop : Nat := 4

def lineDisplayWidth (buffer : FileBuffer) (row : Row) : Nat :=
  ViE.getLineLengthFromBuffer buffer row |>.getD 0

def lineDisplayWidth (tabStop : Nat) (buffer : FileBuffer) (row : Row) : Nat :=
  ViE.getLineLengthFromBufferWithTabStop buffer row tabStop |>.getD 0

def charAtDisplayCol (lineStr : String) (col : Col) : Char :=
  let idx := ViE.Unicode.displayColToCharIndex lineStr col.val

def charAtDisplayCol (tabStop : Nat) (lineStr : String) (col : Col) : Char :=
  let idx := ViE.Unicode.displayColToCharIndexWithTabStop lineStr tabStop col.val

def nextCol (buffer : FileBuffer) (row : Row) (col : Col) : Col :=

def nextCol (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Col :=

  ⟨ViE.Unicode.nextDisplayCol lineStr col.val⟩

  ⟨ViE.Unicode.nextDisplayColWithTabStop lineStr tabStop col.val⟩

def prevCol (buffer : FileBuffer) (row : Row) (col : Col) : Col :=

def prevCol (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Col :=

  ⟨ViE.Unicode.prevDisplayCol lineStr col.val⟩

  ⟨ViE.Unicode.prevDisplayColWithTabStop lineStr tabStop col.val⟩

  let tabStop := s.config.tabStop

     let newCol := prevCol s.getActiveBuffer cursor.row cursor.col

     let newCol := prevCol tabStop s.getActiveBuffer cursor.row cursor.col

  let tabStop := s.config.tabStop

  let limit := lineDisplayWidth buffer cursor.row
  let newCol := nextCol buffer cursor.row cursor.col

  let limit := lineDisplayWidth tabStop buffer cursor.row
  let newCol := nextCol tabStop buffer cursor.row cursor.col

  let tabStop := s.config.tabStop

    let lineLen := lineDisplayWidth s.getActiveBuffer newRow

    let lineLen := lineDisplayWidth tabStop s.getActiveBuffer newRow

  let tabStop := s.config.tabStop

    let lineLen := lineDisplayWidth buffer newRow

    let lineLen := lineDisplayWidth tabStop buffer newRow

  let tabStop := s.config.tabStop

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

  let len := lineDisplayWidth tabStop s.getActiveBuffer cursor.row

  let tabStop := s.config.tabStop

  let lineLen := lineDisplayWidth buffer newRow

  let lineLen := lineDisplayWidth tabStop buffer newRow

  let tabStop := s.config.tabStop

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

  let len := lineDisplayWidth tabStop s.getActiveBuffer cursor.row

  let tabStop := s.config.tabStop

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

  let len := lineDisplayWidth tabStop s.getActiveBuffer cursor.row

  def findNextForwardCore (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) (fuel : Nat) : Row × Col :=

  def findNextForwardCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) (fuel : Nat) : Row × Col :=

      let lineLen := lineDisplayWidth buffer row

      let lineLen := lineDisplayWidth tabStop buffer row

           let nextLen := lineDisplayWidth buffer nextRow

           let nextLen := lineDisplayWidth tabStop buffer nextRow

              findNextForwardCore buffer nextRow 0 true fuel

              findNextForwardCore tabStop buffer nextRow 0 true fuel

        let c := charAtDisplayCol lineStr col

        let c := charAtDisplayCol tabStop lineStr col

             findNextForwardCore buffer row (nextCol buffer row col) true fuel

             findNextForwardCore tabStop buffer row (nextCol tabStop buffer row col) true fuel

             findNextWordEndForwardCore buffer row (nextCol buffer row col) isKw fuel

             findNextWordEndForwardCore tabStop buffer row (nextCol tabStop buffer row col) isKw fuel

              findNextForwardCore buffer row (nextCol buffer row col) started fuel

              findNextForwardCore tabStop buffer row (nextCol tabStop buffer row col) started fuel

  def findNextWordEndForwardCore (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) (fuel : Nat) : Row × Col :=

  def findNextWordEndForwardCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) (fuel : Nat) : Row × Col :=

      let lineLen := lineDisplayWidth buffer row

      let lineLen := lineDisplayWidth tabStop buffer row

          findNextForwardCore buffer row.succ 0 true fuel

          findNextForwardCore tabStop buffer row.succ 0 true fuel

        let c := charAtDisplayCol lineStr col

        let c := charAtDisplayCol tabStop lineStr col

           findNextForwardCore buffer row (nextCol buffer row col) true fuel

           findNextForwardCore tabStop buffer row (nextCol tabStop buffer row col) true fuel

           findNextWordEndForwardCore buffer row (nextCol buffer row col) wasTv fuel

           findNextWordEndForwardCore tabStop buffer row (nextCol tabStop buffer row col) wasTv fuel

def findNextForward (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=
  findNextForwardCore buffer row col started (wordMoveFuel buffer)

def findNextForward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=
  findNextForwardCore tabStop buffer row col started (wordMoveFuel buffer)

def findNextWordEndForward (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=
  findNextWordEndForwardCore buffer row col wasTv (wordMoveFuel buffer)

def findNextWordEndForward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=
  findNextWordEndForwardCore tabStop buffer row col wasTv (wordMoveFuel buffer)

  let tabStop := s.config.tabStop

  let currLineLen := lineDisplayWidth buffer cursor.row

  let currLineLen := lineDisplayWidth tabStop buffer cursor.row

                      findNextForward buffer cursor.row.succ 0 true

                      findNextForward tabStop buffer cursor.row.succ 0 true

                      let ch := charAtDisplayCol lineStr cursor.col

                      let ch := charAtDisplayCol tabStop lineStr cursor.col

                         findNextForward buffer cursor.row (nextCol buffer cursor.row cursor.col) true

                         findNextForward tabStop buffer cursor.row (nextCol tabStop buffer cursor.row cursor.col) true

                         findNextWordEndForward buffer cursor.row (nextCol buffer cursor.row cursor.col) isKw

                         findNextWordEndForward tabStop buffer cursor.row (nextCol tabStop buffer cursor.row cursor.col) isKw

                         findNextForward buffer cursor.row.succ 0 true

                         findNextForward tabStop buffer cursor.row.succ 0 true

  let finalLineLen := lineDisplayWidth buffer r

  let finalLineLen := lineDisplayWidth tabStop buffer r

  def findPrevStartCore (buffer : FileBuffer) (row : Row) (col : Col) (fuel : Nat) : Row × Col :=

  def findPrevStartCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (fuel : Nat) : Row × Col :=

      let c := charAtDisplayCol lineStr col

      let c := charAtDisplayCol tabStop lineStr col

               let prevLen := lineDisplayWidth buffer prevRow
               if prevLen > 0 then findPrevStartCore buffer prevRow ⟨prevLen - 1⟩ fuel else (prevRow, 0)

               let prevLen := lineDisplayWidth tabStop buffer prevRow
               if prevLen > 0 then findPrevStartCore tabStop buffer prevRow ⟨prevLen - 1⟩ fuel else (prevRow, 0)

            findPrevStartCore buffer row (prevCol buffer row col) fuel

            findPrevStartCore tabStop buffer row (prevCol tabStop buffer row col) fuel

         consumeWordBackwardCore buffer row col isKw fuel

         consumeWordBackwardCore tabStop buffer row col isKw fuel

  def consumeWordBackwardCore (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) (fuel : Nat) : Row × Col :=

  def consumeWordBackwardCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) (fuel : Nat) : Row × Col :=

      let c := charAtDisplayCol lineStr col

      let c := charAtDisplayCol tabStop lineStr col

         (row, nextCol buffer row col)

         (row, nextCol tabStop buffer row col)

         else consumeWordBackwardCore buffer row (prevCol buffer row col) wantKw fuel

         else consumeWordBackwardCore tabStop buffer row (prevCol tabStop buffer row col) wantKw fuel

def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
  findPrevStartCore buffer row col (wordMoveFuel buffer)

def findPrevStart (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
  findPrevStartCore tabStop buffer row col (wordMoveFuel buffer)

def consumeWordBackward (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordBackwardCore buffer row col wantKw (wordMoveFuel buffer)

def consumeWordBackward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordBackwardCore tabStop buffer row col wantKw (wordMoveFuel buffer)

  let tabStop := s.config.tabStop

      let lineLen := lineDisplayWidth buffer cursor.row

      let lineLen := lineDisplayWidth tabStop buffer cursor.row

               let prevLen := lineDisplayWidth buffer prevRow

               let prevLen := lineDisplayWidth tabStop buffer prevRow

                  findPrevStart buffer prevRow ⟨prevLen - 1⟩

                  findPrevStart tabStop buffer prevRow ⟨prevLen - 1⟩

            findPrevStart buffer cursor.row (prevCol buffer cursor.row startCol)

            findPrevStart tabStop buffer cursor.row (prevCol tabStop buffer cursor.row startCol)

  def findNextEndCore (buffer : FileBuffer) (row : Row) (col : Col) (fuel : Nat) : Row × Col :=

  def findNextEndCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (fuel : Nat) : Row × Col :=

      let lineLen := lineDisplayWidth buffer row

      let lineLen := lineDisplayWidth tabStop buffer row

           findNextEndCore buffer row.succ 0 fuel

           findNextEndCore tabStop buffer row.succ 0 fuel

         let c := charAtDisplayCol lineStr col

         let c := charAtDisplayCol tabStop lineStr col

            findNextEndCore buffer row (nextCol buffer row col) fuel

            findNextEndCore tabStop buffer row (nextCol tabStop buffer row col) fuel

            consumeWordToEndCore buffer row col isKw fuel

            consumeWordToEndCore tabStop buffer row col isKw fuel

  def consumeWordToEndCore (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) (fuel : Nat) : Row × Col :=

  def consumeWordToEndCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) (fuel : Nat) : Row × Col :=

      let lineLen := lineDisplayWidth buffer row
      let nextColVal := (nextCol buffer row col).val

      let lineLen := lineDisplayWidth tabStop buffer row
      let nextColVal := (nextCol tabStop buffer row col).val

         let nextC := charAtDisplayCol lineStr (nextCol buffer row col)

         let nextC := charAtDisplayCol tabStop lineStr (nextCol tabStop buffer row col)

            consumeWordToEndCore buffer row (nextCol buffer row col) wantKw fuel

            consumeWordToEndCore tabStop buffer row (nextCol tabStop buffer row col) wantKw fuel

def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
  findNextEndCore buffer row col (wordMoveFuel buffer)

def findNextEnd (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
  findNextEndCore tabStop buffer row col (wordMoveFuel buffer)

def consumeWordToEnd (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordToEndCore buffer row col wantKw (wordMoveFuel buffer)

def consumeWordToEnd (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordToEndCore tabStop buffer row col wantKw (wordMoveFuel buffer)

  let tabStop := s.config.tabStop

  let currLineLen := lineDisplayWidth buffer cursor.row

  let currLineLen := lineDisplayWidth tabStop buffer cursor.row

  let startCol : Col := nextCol buffer cursor.row cursor.col

  let startCol : Col := nextCol tabStop buffer cursor.row cursor.col

            findNextEnd buffer cursor.row.succ 0

            findNextEnd tabStop buffer cursor.row.succ 0

         findNextEnd buffer cursor.row startCol

         findNextEnd tabStop buffer cursor.row startCol

  let tabStop := s.config.tabStop

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

  let delta := ViE.Unicode.charWidth c

  let delta := ViE.Unicode.charWidthAt tabStop cursor.col.val c

  let tabStop := s.config.tabStop

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

  let tabStop := s.config.tabStop

    let prevC := prevCol buffer cursor.row cursor.col

    let prevC := prevCol tabStop buffer cursor.row cursor.col

       match ViE.getOffsetFromPointInBuffer buffer cursor.row.val prevC.val,
             ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with

       match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val prevC.val tabStop,
             ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

    let newLen := ViE.getLineLengthFromBuffer s'.getActiveBuffer prevRow |>.getD 0

    let newLen := lineDisplayWidth tabStop s'.getActiveBuffer prevRow

  let tabStop := s.config.tabStop

  let lineLen := lineDisplayWidth buffer cursor.row
  let nextC := nextCol buffer cursor.row cursor.col

  let lineLen := lineDisplayWidth tabStop buffer cursor.row
  let nextC := nextCol tabStop buffer cursor.row cursor.col

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,
          ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,
          ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with

  let newLen := lineDisplayWidth newBuffer cursor.row

  let newLen := lineDisplayWidth tabStop newBuffer cursor.row

     let newCol := ViE.Unicode.prevDisplayCol lineStr newLen

     let newCol := ViE.Unicode.prevDisplayColWithTabStop lineStr tabStop newLen

  let tabStop := s.config.tabStop

    match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,
          ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer p1.row.val p1.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer p2.row.val p2.col.val tabStop with

  let tabStop := s.config.tabStop

  let lineLen := lineDisplayWidth buffer endP.row

  let lineLen := lineDisplayWidth tabStop buffer endP.row

  let targetCol := if endP.col.val < lineLen then ViE.Unicode.nextDisplayCol lineStr endP.col.val else lineLen

  let targetCol := if endP.col.val < lineLen then ViE.Unicode.nextDisplayColWithTabStop lineStr tabStop endP.col.val else lineLen

  let tabStop := s.config.tabStop

  let lineWidth := ViE.Unicode.stringWidth line

  let lineWidth := ViE.Unicode.stringWidthWithTabStop line tabStop

        ViE.Unicode.nextDisplayCol line cursor.col.val

        ViE.Unicode.nextDisplayColWithTabStop line tabStop cursor.col.val

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val targetCol with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val targetCol tabStop with

  let lastWidth := ViE.Unicode.stringWidth lastLine

  let lastWidth := ViE.Unicode.stringWidthWithTabStop lastLine tabStop

def firstNonBlankCol (line : String) : Nat :=

def firstNonBlankCol (line : String) (tabStop : Nat) : Nat :=

        loop rest (col + ViE.Unicode.charWidth c)

        loop rest (col + ViE.Unicode.charWidthAt tabStop col c)

  let col := firstNonBlankCol lineStr

  let col := firstNonBlankCol lineStr s.config.tabStop

  let tabStop := s.config.tabStop

  let lineWidth := ViE.Unicode.stringWidth line

  let lineWidth := ViE.Unicode.stringWidthWithTabStop line tabStop

        ViE.Unicode.nextDisplayCol line cursor.col.val

        ViE.Unicode.nextDisplayColWithTabStop line tabStop cursor.col.val

        let lineW := ViE.Unicode.stringWidth lineStr

        let lineW := ViE.Unicode.stringWidthWithTabStop lineStr tabStop

            let insertOff := ViE.getOffsetFromPointInBuffer buf row lineW |>.getD (buf.table.tree.length)

            let insertOff := ViE.getOffsetFromPointInBufferWithTabStop buf row lineW tabStop |>.getD (buf.table.tree.length)

            let off' := ViE.getOffsetFromPointInBuffer buf' row targetCol |>.getD insertOff

            let off' := ViE.getOffsetFromPointInBufferWithTabStop buf' row targetCol tabStop |>.getD insertOff

            let off := ViE.getOffsetFromPointInBuffer buf row targetCol |>.getD 0

            let off := ViE.getOffsetFromPointInBufferWithTabStop buf row targetCol tabStop |>.getD 0

  let tabStop := s.config.tabStop

  let currentOffset := match ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val with

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row.val cursor.col.val tabStop with

  let tabStop := s.config.tabStop

  let currentOffset := match ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val with

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row.val cursor.col.val tabStop with

  tabStop := 4

        | '\x09' => Key.ctrl 'i'

        | '\x09' => Key.char '\t'

private def PieceTable.findLineForOffsetCore (pt : PieceTable) (target : Nat) (low high : Nat) (fuel : Nat) : Option (Nat × Nat) :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
    if low > high then none
    else
      let mid := (low + high) / 2
      match pt.getLineRange mid with
      | some (start, len) =>
        let endOff := start + len
        if target >= start && target <= endOff then
          some (mid, target - start)
        else if target < start then
           if mid == 0 then none
           else PieceTable.findLineForOffsetCore pt target low (mid - 1) fuel
        else
           PieceTable.findLineForOffsetCore pt target (mid + 1) high fuel
      | none => none

private def PieceTable.findLineForOffsetCore (pt : PieceTable) (target : Nat) (low highExcl : Nat) : Option (Nat × Nat) :=
  if low >= highExcl then none
  else
    let mid := low + (highExcl - low) / 2
    match pt.getLineRange mid with
    | some (start, len) =>
      let endOff := start + len
      if target >= start && target <= endOff then
        some (mid, target - start)
      else if target < start then
        PieceTable.findLineForOffsetCore pt target low mid
      else
        PieceTable.findLineForOffsetCore pt target (mid + 1) highExcl
    | none => none
  termination_by highExcl - low
  decreasing_by
    · simp_wf
      omega
    · simp_wf
      omega

  let fuel := pt.lineCount + 1
  PieceTable.findLineForOffsetCore pt target low high fuel

  PieceTable.findLineForOffsetCore pt target low (high + 1)

private def concatCore (l : ViE.PieceTree) (r : ViE.PieceTree) (pt : ViE.PieceTable) (fuel : Nat) : ViE.PieceTree :=
  match fuel with
  | 0 =>
    -- Rebuild into a balanced tree in pathological cases instead of creating deep chains.
    fromPieces (toPieces l ++ toPieces r) pt
  | fuel + 1 =>
    match l, r with
    | ViE.PieceTree.empty, _ => r
    | _, ViE.PieceTree.empty => l
    | ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>
      -- Try to merge the last piece of ps1 with the first piece of ps2

private def concatCore (l : ViE.PieceTree) (r : ViE.PieceTree) (pt : ViE.PieceTable) : ViE.PieceTree :=
  match l, r with
  | ViE.PieceTree.empty, _ => r
  | _, ViE.PieceTree.empty => l
  | ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>
      -- Fast path for adjacent leaves; preserve piece merging behavior.

      else if ps1.size > 0 then l
      else r
    | ViE.PieceTree.internal cs1 _ _, ViE.PieceTree.internal cs2 _ _ =>
      let h1 := height l
      let h2 := height r
      if h1 == h2 then
        -- Merge boundary children
        let lastChild := cs1.back!
        let firstChild := cs2[0]!
        let merged := concatCore lastChild firstChild pt fuel
        match merged with
        | ViE.PieceTree.internal newCS s _ =>
          if s.height == h1 then
             -- newCS is at the same level as siblings
             let combined := (cs1.pop) ++ newCS ++ (cs2.extract 1 cs2.size)
             if combined.size <= ViE.NodeCapacity then mkInternal combined
             else
               let mid := combined.size / 2
               mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
          else
             -- height did not increase, just one child
             let combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)
             if combined.size <= ViE.NodeCapacity then mkInternal combined
             else
               let mid := combined.size / 2
               mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
        | _ =>
          let combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)
          if combined.size <= ViE.NodeCapacity then mkInternal combined
          else
            let mid := combined.size / 2
            mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
      else if h1 > h2 then
        -- Insert r into l's right side
        let lastChild := cs1.back!
        let newLast := concatCore lastChild r pt fuel
        match newLast with
        | ViE.PieceTree.internal newChildren s _ =>
          if s.height == h1 then
             -- Split happened at l's level
             let combined := (cs1.pop) ++ newChildren
             if combined.size <= ViE.NodeCapacity then mkInternal combined
             else
                let mid := combined.size / 2
                mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
          else
             mkInternal ((cs1.pop).push newLast)
        | _ => mkInternal ((cs1.pop).push newLast)

      else if ps1.size > 0 then
        l

        -- Insert l into r's left side
        let firstChild := cs2[0]!
        let newFirst := concatCore l firstChild pt fuel
        match newFirst with
        | ViE.PieceTree.internal newChildren s _ =>
          if s.height == h2 then
             let combined := newChildren ++ (cs2.extract 1 cs2.size)
             if combined.size <= ViE.NodeCapacity then mkInternal combined
             else
                let mid := combined.size / 2
                mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]
          else
             mkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))
        | _ => mkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))
    -- Mixed types: wrap the smaller one and recurse
    | ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concatCore (mkInternal #[l]) r pt fuel
    | ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concatCore l (mkInternal #[r]) pt fuel
  termination_by fuel
  decreasing_by
    all_goals exact Nat.lt_succ_self _

        r
  | _, _ =>
      -- For mixed or internal trees, rebuild a balanced tree from in-order pieces.
      fromPieces (toPieces l ++ toPieces r) pt

  -- Cap recursion depth and rely on balanced fallback when exhausted.
  let rawFuel := (height l + height r + 4) * 8 + 64
  let fuel := min rawFuel 2048
  concatCore l r pt fuel

  concatCore l r pt

private def splitCore (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) (fuel : Nat) : (ViE.PieceTree × ViE.PieceTree) :=
  match fuel with
  | 0 => (t, ViE.PieceTree.empty)
  | fuel + 1 =>
      match t with
      | ViE.PieceTree.empty => (ViE.PieceTree.empty, ViE.PieceTree.empty)

private def splitCore (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) : (ViE.PieceTree × ViE.PieceTree) :=
  Id.run do
    if offset == 0 then
      return (ViE.PieceTree.empty, t)
    let mut node := t
    let mut off := offset
    let mut frames : Array (Array ViE.PieceTree × Array ViE.PieceTree) := #[]
    while true do
      match node with
      | ViE.PieceTree.empty =>
          return (ViE.PieceTree.empty, ViE.PieceTree.empty)

          Id.run do
            let mut i := 0
            let mut accOffset := 0
            while i < pieces.size do
              let p := pieces[i]!
              if offset < accOffset + p.length then
                let relOffset := offset - accOffset
                if relOffset == 0 then
                  return (mkLeaf (pieces.extract 0 i) pt, mkLeaf (pieces.extract i pieces.size) pt)

          let mut i := 0
          let mut accOffset := 0
          let mut leftTree := node
          let mut rightTree := ViE.PieceTree.empty
          let mut found := false
          while i < pieces.size && !found do
            let p := pieces[i]!
            if off < accOffset + p.length then
              let relOffset := off - accOffset
              if relOffset == 0 then
                leftTree := mkLeaf (pieces.extract 0 i) pt
                rightTree := mkLeaf (pieces.extract i pieces.size) pt
              else

                return (mkLeaf ((pieces.extract 0 i).push p1) pt, mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)) pt)

                leftTree := mkLeaf ((pieces.extract 0 i).push p1) pt
                rightTree := mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)) pt
              found := true
            else

            return (t, ViE.PieceTree.empty)

          if !found then
            leftTree := node
            rightTree := ViE.PieceTree.empty
          let mut l := leftTree
          let mut r := rightTree
          let mut fi := frames.size
          while fi > 0 do
            let j := fi - 1
            let (leftSibs, rightSibs) := frames[j]!
            l := mkInternal (leftSibs.push l)
            r := mkInternal (#[r] ++ rightSibs)
            fi := j
          return (l, r)

          Id.run do
            let mut i := 0
            let mut accOffset := 0
            while i < children.size do
              let c := children[i]!
              let cLen := length c
              if offset < accOffset + cLen then
                let (l, r) := splitCore c (offset - accOffset) pt fuel
                let leftSide := mkInternal ((children.extract 0 i).push l)
                let rightSide := mkInternal (#[r] ++ (children.extract (i + 1) children.size))
                return (leftSide, rightSide)

          let mut i := 0
          let mut accOffset := 0
          let mut found := false
          while i < children.size && !found do
            let c := children[i]!
            let cLen := length c
            if off < accOffset + cLen then
              frames := frames.push (children.extract 0 i, children.extract (i + 1) children.size)
              node := c
              off := off - accOffset
              found := true
            else

          if !found then

  termination_by fuel
  decreasing_by
    all_goals exact Nat.lt_succ_self _

    return (t, ViE.PieceTree.empty)

  let fuel := (height t + 4) * 32 + 64
  splitCore t offset pt fuel

  splitCore t offset pt

private def getBytesCore (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) (fuel : Nat) : ByteArray :=
  let rec collect (fuel : Nat) (t : ViE.PieceTree) (off : Nat) (l : Nat) (acc : Array ByteArray) : (Array ByteArray × Nat) :=
    match fuel with
    | 0 => (acc, 0)
    | fuel + 1 =>
        if l == 0 then (acc, 0)
        else
          match t with
          | ViE.PieceTree.empty => (acc, 0)
          | ViE.PieceTree.leaf pieces _ _ =>
              Id.run do
                let mut i := 0
                let mut accOffset := 0
                let mut currAcc := acc
                let mut remain := l
                while i < pieces.size && remain > 0 do
                  let p := pieces[i]!
                  let pLen := p.length
                  if off < accOffset + pLen then
                    let pStart := if off > accOffset then off - accOffset else 0
                    let readLen := min remain (pLen - pStart)
                    let buf := PieceTableHelper.getBuffer pt p.source
                    let slice := buf.extract (p.start + pStart) (p.start + pStart + readLen)
                    currAcc := currAcc.push slice
                    remain := remain - readLen
                  accOffset := accOffset + pLen
                  i := i + 1
                return (currAcc, l - remain)
          | ViE.PieceTree.internal children _ _ =>
              Id.run do
                let mut i := 0
                let mut accOffset := 0
                let mut currAcc := acc
                let mut remain := l
                while i < children.size && remain > 0 do
                  let c := children[i]!
                  let cLen := length c
                  if off < accOffset + cLen then
                    let cStart := if off > accOffset then off - accOffset else 0
                    let (newAcc, readInThisChild) := collect fuel c cStart remain currAcc
                    currAcc := newAcc
                    remain := remain - readInThisChild
                  accOffset := accOffset + cLen
                  i := i + 1
                return (currAcc, l - remain)
  let (chunks, _) := collect fuel t offset len #[]
  chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])

private def getBytesCore (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : ByteArray :=
  if len == 0 then
    ByteArray.mk #[]
  else
    let endOffset := offset + len
    let chunks := Id.run do
      let mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]
      let mut out : Array ByteArray := #[]
      let mut cursor := offset
      let mut remain := len
      while remain > 0 && !stack.isEmpty do
        match stack with
        | [] => pure ()
        | (node, baseOffset) :: rest =>
            stack := rest
            let nodeLen := length node
            let nodeEnd := baseOffset + nodeLen
            if nodeEnd <= cursor || baseOffset >= endOffset then
              pure ()
            else
              match node with
              | ViE.PieceTree.empty => pure ()
              | ViE.PieceTree.leaf pieces _ _ =>
                  let mut i := 0
                  let mut pieceBase := baseOffset
                  while i < pieces.size && remain > 0 do
                    let p := pieces[i]!
                    let pStart := pieceBase
                    let pEnd := pieceBase + p.length
                    if pEnd > cursor && pStart < endOffset then
                      let startInPiece := if cursor > pStart then cursor - pStart else 0
                      let maxReadable := p.length - startInPiece
                      let untilEnd := endOffset - (pStart + startInPiece)
                      let readLen := min remain (min maxReadable untilEnd)
                      if readLen > 0 then
                        let buf := PieceTableHelper.getBuffer pt p.source
                        let slice := buf.extract (p.start + startInPiece) (p.start + startInPiece + readLen)
                        out := out.push slice
                        cursor := cursor + readLen
                        remain := remain - readLen
                    pieceBase := pieceBase + p.length
                    i := i + 1
              | ViE.PieceTree.internal children _ _ =>
                  let mut i := children.size
                  let mut childEnd := nodeEnd
                  while i > 0 do
                    let j := i - 1
                    let child := children[j]!
                    let childLen := length child
                    let childStart := childEnd - childLen
                    if childEnd > cursor && childStart < endOffset then
                      stack := (child, childStart) :: stack
                    childEnd := childStart
                    i := j
      return out
    chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])

  let fuel := (height t + 4) * 32 + 64
  getBytesCore t offset len pt fuel

  getBytesCore t offset len pt

private def findNthNewlineLeafCore (t : ViE.PieceTree) (n : Nat) (pt : ViE.PieceTable) (accOffset : Nat) (fuel : Nat)

private def findNthNewlineLeafCore (t : ViE.PieceTree) (n : Nat) (pt : ViE.PieceTable) (accOffset : Nat)

  match fuel with
  | 0 => none
  | fuel + 1 =>
      match t with
      | ViE.PieceTree.empty => none

  Id.run do
    let mut node := t
    let mut currN := n
    let mut currOff := accOffset
    while true do
      match node with
      | ViE.PieceTree.empty =>
          return none

          Id.run do
            let mut i := 0
            let mut currN := n
            let mut currOff := accOffset
            while i < pieces.size do
              let p := pieces[i]!
              if currN < p.lineBreaks then
                let buf := PieceTableHelper.getBuffer pt p.source
                let mut j := 0
                let mut targetN := currN
                let mut relOffset := p.length
                let mut done := false
                while j < p.length && !done do
                  if buf[p.start + j]! == 10 then
                    if targetN == 0 then
                      relOffset := j + 1
                      done := true
                    else
                      targetN := targetN - 1
                  j := j + 1
                return some (p, currOff, relOffset)
              currN := currN - p.lineBreaks
              currOff := currOff + p.length
              i := i + 1
            return none

          let mut i := 0
          while i < pieces.size do
            let p := pieces[i]!
            if currN < p.lineBreaks then
              let buf := PieceTableHelper.getBuffer pt p.source
              let mut j := 0
              let mut targetN := currN
              let mut relOffset := p.length
              let mut done := false
              while j < p.length && !done do
                if buf[p.start + j]! == 10 then
                  if targetN == 0 then
                    relOffset := j + 1
                    done := true
                  else
                    targetN := targetN - 1
                j := j + 1
              return some (p, currOff, relOffset)
            currN := currN - p.lineBreaks
            currOff := currOff + p.length
            i := i + 1
          return none

          Id.run do
            let mut i := 0
            let mut currN := n
            let mut currOff := accOffset
            while i < children.size do
              let child := children[i]!
              let childLines := lineBreaks child
              if currN < childLines then
                return findNthNewlineLeafCore child currN pt currOff fuel

          let mut i := 0
          let mut found := false
          while i < children.size && !found do
            let child := children[i]!
            let childLines := lineBreaks child
            if currN < childLines then
              node := child
              found := true
            else

          if !found then

  termination_by fuel
  decreasing_by
    all_goals exact Nat.lt_succ_self _

    return none

  let fuel := (height t + 4) * 32 + 64
  findNthNewlineLeafCore t n pt 0 fuel

  findNthNewlineLeafCore t n pt 0

private def maximalSuffixLoopCore (x : ByteArray) (useLe : Bool) (m ms j k p : Int) (fuel : Nat) : (Int × Int) :=
  match fuel with
  | 0 => (ms, p)
  | fuel + 1 =>
      if j + k >= m then
        (ms, p)
      else
        let a := x[Int.toNat (j + k)]!
        let b := x[Int.toNat (ms + k)]!
        if useLe then
          if a < b then
            maximalSuffixLoopCore x useLe m ms (j + k) 1 (j + k - ms) fuel
          else if a == b then
            if k != p then
              maximalSuffixLoopCore x useLe m ms j (k + 1) p fuel
            else
              maximalSuffixLoopCore x useLe m ms (j + p) 1 p fuel

def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=
  Id.run do
    let mut ms := ms
    let mut j := j
    let mut k := k
    let mut p := p
    -- Keep an execution cap for robustness against malformed index states.
    let mNat := Int.toNat m
    let mut steps := (mNat + 1) * (mNat + 1) + 1
    while steps > 0 && j + k < m do
      let a := x[Int.toNat (j + k)]!
      let b := x[Int.toNat (ms + k)]!
      if useLe then
        if a < b then
          let jk := j + k
          j := jk
          k := 1
          p := jk - ms
        else if a == b then
          if k != p then
            k := k + 1

            maximalSuffixLoopCore x useLe m j (j + 1) 1 1 fuel

            j := j + p
            k := 1

          if a > b then
            maximalSuffixLoopCore x useLe m ms (j + k) 1 (j + k - ms) fuel
          else if a == b then
            if k != p then
              maximalSuffixLoopCore x useLe m ms j (k + 1) p fuel
            else
              maximalSuffixLoopCore x useLe m ms (j + p) 1 p fuel
          else
            maximalSuffixLoopCore x useLe m j (j + 1) 1 1 fuel
  termination_by fuel
  decreasing_by
    all_goals exact Nat.lt_succ_self _
def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=
  let mNat := Int.toNat m
  let fuel := (mNat + 1) * (mNat + 1) + 1
  maximalSuffixLoopCore x useLe m ms j k p fuel

          ms := j
          j := j + 1
          k := 1
          p := 1
      else if a > b then
        let jk := j + k
        j := jk
        k := 1
        p := jk - ms
      else if a == b then
        if k != p then
          k := k + 1
        else
          j := j + p
          k := 1
      else
        ms := j
        j := j + 1
        k := 1
        p := 1
      steps := steps - 1
    return (ms, p)

private def twoWayForward1Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) (fuel : Nat) : Int :=
  match fuel with
  | 0 => j
  | fuel + 1 =>
      if j >= n then
        j
      else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
        twoWayForward1Core haystack needle i n (j + 1) fuel
      else
        j
  termination_by fuel

private def twoWayForward1Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Nat) : Nat :=
  if j >= n then
    j
  else if haystack[i + j]! == needle[j]! then
    twoWayForward1Core haystack needle i n (j + 1)
  else
    j
  termination_by n - j

    all_goals exact Nat.lt_succ_self _

    simp_wf
    omega

  let fuel := Int.toNat (Int.ofNat n - j) + 1
  twoWayForward1Core haystack needle i n j fuel

  Int.ofNat (twoWayForward1Core haystack needle i n (Int.toNat j))

private def twoWayBackward1Core (haystack needle : ByteArray) (i : Nat) (mem : Int) (j : Int) (fuel : Nat) : Int :=
  match fuel with
  | 0 => j
  | fuel + 1 =>
      if j <= mem then
        j
      else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
        twoWayBackward1Core haystack needle i mem (j - 1) fuel
      else
        j
  termination_by fuel

private def twoWayBackward1Core (haystack needle : ByteArray) (i : Nat) (mem : Int) (steps : Nat) : Int :=
  if hSteps : steps = 0 then
    mem
  else
    let j := mem + Int.ofNat steps
    if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
      twoWayBackward1Core haystack needle i mem (steps - 1)
    else
      j
  termination_by steps

    all_goals exact Nat.lt_succ_self _

    have hstepsPos : 0 < steps := Nat.pos_of_ne_zero hSteps
    exact Nat.sub_lt hstepsPos (by decide : 0 < 1)

  let fuel := Int.toNat (j - mem) + 1
  twoWayBackward1Core haystack needle i mem j fuel

  if j <= mem then
    j
  else
    let steps := Int.toNat (j - mem)
    twoWayBackward1Core haystack needle i mem steps

private def twoWayForward2Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) (fuel : Nat) : Int :=
  match fuel with
  | 0 => j
  | fuel + 1 =>
      if j >= n then
        j
      else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
        twoWayForward2Core haystack needle i n (j + 1) fuel
      else
        j
  termination_by fuel

private def twoWayForward2Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Nat) : Nat :=
  if j >= n then
    j
  else if haystack[i + j]! == needle[j]! then
    twoWayForward2Core haystack needle i n (j + 1)
  else
    j
  termination_by n - j

    all_goals exact Nat.lt_succ_self _

    simp_wf
    omega

  let fuel := Int.toNat (Int.ofNat n - j) + 1
  twoWayForward2Core haystack needle i n j fuel

  Int.ofNat (twoWayForward2Core haystack needle i n (Int.toNat j))

private def twoWayBackward2Core (haystack needle : ByteArray) (i : Nat) (j : Int) (fuel : Nat) : Int :=
  match fuel with
  | 0 => j
  | fuel + 1 =>
      if j < 0 then
        j
      else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
        twoWayBackward2Core haystack needle i (j - 1) fuel
      else
        j
  termination_by fuel

private def twoWayBackward2Core (haystack needle : ByteArray) (i : Nat) (steps : Nat) : Int :=
  if hSteps : steps = 0 then
    -1
  else
    let j := Int.ofNat steps - 1
    if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
      twoWayBackward2Core haystack needle i (steps - 1)
    else
      j
  termination_by steps

    all_goals exact Nat.lt_succ_self _

    have hstepsPos : 0 < steps := Nat.pos_of_ne_zero hSteps
    exact Nat.sub_lt hstepsPos (by decide : 0 < 1)

  let fuel := Int.toNat (j + 1) + 1
  twoWayBackward2Core haystack needle i j fuel

  if j < 0 then
    j
  else
    twoWayBackward2Core haystack needle i (Int.toNat (j + 1))

private def twoWayShortLoopCore (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (mem : Int) (fuel : Nat) : Option Nat :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
      if i > maxStart then

private def twoWayShortLoopCore (haystack needle : ByteArray) (_start maxStart msNat pNat n : Nat) (i : Nat) (mem : Int) : Option Nat :=
  if i > maxStart then
    none
  else
    let j0 := max (Int.ofNat msNat) mem + 1
    let j := twoWayForward1 haystack needle i n j0
    if j >= n then
      let j2 := twoWayBackward1 haystack needle i mem (Int.ofNat msNat)
      if j2 <= mem then
        some i
      else
        let nextI := i + pNat
        if nextI <= i then
          none
        else
          let nextMem := Int.ofNat (n - pNat - 1)
          twoWayShortLoopCore haystack needle _start maxStart msNat pNat n nextI nextMem
    else
      let shift := Int.toNat (j - Int.ofNat msNat)
      if shift == 0 then

        let j0 := max (Int.ofNat msNat) mem + 1
        let j := twoWayForward1 haystack needle i n j0
        if j >= n then
          let j2 := twoWayBackward1 haystack needle i mem (Int.ofNat msNat)
          if j2 <= mem then
            some i
          else
            let nextI := i + pNat
            let nextMem := Int.ofNat (n - pNat - 1)
            twoWayShortLoopCore haystack needle start maxStart msNat pNat n nextI nextMem fuel

        let nextI := i + shift
        if nextI <= i then
          none

          let shift := Int.toNat (j - Int.ofNat msNat)
          twoWayShortLoopCore haystack needle start maxStart msNat pNat n (i + shift) (-1) fuel
  termination_by fuel

          twoWayShortLoopCore haystack needle _start maxStart msNat pNat n nextI (-1)
  termination_by maxStart + 1 - i

    all_goals exact Nat.lt_succ_self _

    ·
      simp_wf
      grind
    ·
      simp_wf
      grind

  let fuel := if start <= maxStart then maxStart - start + 2 else 1
  twoWayShortLoopCore haystack needle start maxStart msNat pNat n i mem fuel

  twoWayShortLoopCore haystack needle start maxStart msNat pNat n i mem

private def twoWayLongLoopCore (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (fuel : Nat) : Option Nat :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
      if i > maxStart then

private def twoWayLongLoopCore (haystack needle : ByteArray) (_start maxStart msNat pNat n : Nat) (i : Nat) : Option Nat :=
  if i > maxStart then
    none
  else
    let j := twoWayForward2 haystack needle i n (Int.ofNat (msNat + 1))
    if j >= n then
      let j2 := twoWayBackward2 haystack needle i (Int.ofNat msNat)
      if j2 < 0 then
        some i
      else
        let nextI := i + pNat
        if nextI <= i then
          none
        else
          twoWayLongLoopCore haystack needle _start maxStart msNat pNat n nextI
    else
      let shift := Int.toNat (j - Int.ofNat msNat)
      if shift == 0 then

        let j := twoWayForward2 haystack needle i n (Int.ofNat (msNat + 1))
        if j >= n then
          let j2 := twoWayBackward2 haystack needle i (Int.ofNat msNat)
          if j2 < 0 then
            some i
          else
            let nextI := i + pNat
            twoWayLongLoopCore haystack needle start maxStart msNat pNat n nextI fuel

        let nextI := i + shift
        if nextI <= i then
          none

          let shift := Int.toNat (j - Int.ofNat msNat)
          twoWayLongLoopCore haystack needle start maxStart msNat pNat n (i + shift) fuel
  termination_by fuel

          twoWayLongLoopCore haystack needle _start maxStart msNat pNat n nextI
  termination_by maxStart + 1 - i

    all_goals exact Nat.lt_succ_self _

    ·
      simp_wf
      grind
    ·
      simp_wf
      grind

  let fuel := if start <= maxStart then maxStart - start + 2 else 1
  twoWayLongLoopCore haystack needle start maxStart msNat pNat n i fuel

  twoWayLongLoopCore haystack needle start maxStart msNat pNat n i

    let rec loop (i : Nat) (last : Option Nat) (fuel : Nat) : Option Nat :=
      match fuel with
      | 0 => last
      | fuel + 1 =>
          if i > maxStart then last
          else
            match findPatternInBytes haystack needle i with
            | some idx =>
                if idx > maxStart then last
                else loop (idx + 1) (some idx) fuel
            | none => last
    loop 0 none (maxStart + 1)

    let rec loop (i : Nat) (last : Option Nat) : Option Nat :=
      if i > maxStart then last
      else
        match findPatternInBytes haystack needle i with
        | some idx =>
            if idx > maxStart then last
            else if idx < i then last
            else loop (idx + 1) (some idx)
        | none => last
      termination_by maxStart + 1 - i
      decreasing_by
        simp_wf
        omega
    loop 0 none

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat) (fuel : Nat)

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat)

      let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)
        (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (fuelN : Nat)
        : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
        match fuelN with
        | 0 => (none, cache, order)
        | fuelN + 1 =>
            if baseOffset + length node <= startOffset then
              (none, cache, order)
            else
              match node with
              | ViE.PieceTree.empty => (none, cache, order)
              | ViE.PieceTree.leaf _ _ m =>
                  let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0
                  let remain := length node - relStart
                  let globalStart := baseOffset + relStart
                  let available := total - globalStart
                  let readLen := min (remain + overlap) available
                  if readLen < pattern.size then
                    (none, cache, order)
                  else
                    let crossesBoundary := readLen > remain
                    if !crossesBoundary && !bloomMayContain m.bits hashes then
                      (none, cache, order)

      Id.run do
        let mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]
        let mut cacheAcc := cache
        let mut orderAcc := order
        while !stack.isEmpty do
          match stack with
          | [] => pure ()
          | (node, baseOffset) :: rest =>
              stack := rest
              if baseOffset + length node <= startOffset then
                pure ()
              else
                match node with
                | ViE.PieceTree.empty => pure ()
                | ViE.PieceTree.leaf _ _ m =>
                    let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0
                    let remain := length node - relStart
                    let globalStart := baseOffset + relStart
                    let available := total - globalStart
                    let readLen := min (remain + overlap) available
                    if readLen < pattern.size then
                      pure ()
                    else
                      let crossesBoundary := readLen > remain
                      if !crossesBoundary && !bloomMayContain m.bits hashes then
                        pure ()
                      else
                        let bytes := getBytes t globalStart readLen pt
                        match findPatternInBytes bytes pattern 0 with
                        | some idx => return (some (globalStart + idx), cacheAcc, orderAcc)
                        | none => pure ()
                | ViE.PieceTree.internal children _ m =>
                    if !bloomMayContain m.bits hashes then
                      pure ()

                      let bytes := getBytes t globalStart readLen pt
                      match findPatternInBytes bytes pattern 0 with
                      | some idx => (some (globalStart + idx), cache, order)
                      | none => (none, cache, order)
              | ViE.PieceTree.internal children _ m =>
                  if !bloomMayContain m.bits hashes then
                    (none, cache, order)
                  else
                    Id.run do
                      let mut i := 0
                      let mut offset := baseOffset
                      let mut cacheAcc := cache
                      let mut orderAcc := order
                      while i < children.size do
                        let child := children[i]!

                      let mut i := children.size
                      let mut childEnd := baseOffset + length node
                      while i > 0 do
                        let j := i - 1
                        let child := children[j]!

                        let childEnd := offset + childLen

                        let childStart := childEnd - childLen

                          let (res, cache', order') := searchNode child offset cacheAcc orderAcc fuelN
                          cacheAcc := cache'
                          orderAcc := order'
                          match res with
                          | some _ => return (res, cacheAcc, orderAcc)
                          | none => pure ()
                        offset := childEnd
                        i := i + 1
                      return (none, cacheAcc, orderAcc)
      searchNode t 0 cache order fuel

                          stack := (child, childStart) :: stack
                        childEnd := childStart
                        i := j
        return (none, cacheAcc, orderAcc)

  let fuel := (height t + 4) * 32 + 64
  searchNextCore t pt pattern startOffset chunkSize useBloom cache order cacheMax fuel

  searchNextCore t pt pattern startOffset chunkSize useBloom cache order cacheMax

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat) (fuel : Nat)

  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (_cacheMax : Nat)

      let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)
        (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (fuelN : Nat)
        : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
        match fuelN with
        | 0 => (none, cache, order)
        | fuelN + 1 =>
            if baseOffset >= end0 then
              (none, cache, order)
            else
              match node with
              | ViE.PieceTree.empty => (none, cache, order)
              | ViE.PieceTree.leaf _ _ m =>
                  let relEnd := min (end0 - baseOffset) (length node)
                  let globalEnd := baseOffset + relEnd
                  let globalStart := if baseOffset > overlap then baseOffset - overlap else 0
                  let readLen := globalEnd - globalStart
                  if readLen < pattern.size then
                    (none, cache, order)
                  else
                    let crossesBoundary := globalStart < baseOffset
                    if !crossesBoundary && !bloomMayContain m.bits hashes then
                      (none, cache, order)

      Id.run do
        let mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]
        let mut cacheAcc := cache
        let mut orderAcc := order
        while !stack.isEmpty do
          match stack with
          | [] => pure ()
          | (node, baseOffset) :: rest =>
              stack := rest
              if baseOffset >= end0 then
                pure ()
              else
                match node with
                | ViE.PieceTree.empty => pure ()
                | ViE.PieceTree.leaf _ _ m =>
                    let relEnd := min (end0 - baseOffset) (length node)
                    let globalEnd := baseOffset + relEnd
                    let globalStart := if baseOffset > overlap then baseOffset - overlap else 0
                    let readLen := globalEnd - globalStart
                    if readLen < pattern.size then
                      pure ()
                    else
                      let crossesBoundary := globalStart < baseOffset
                      if !crossesBoundary && !bloomMayContain m.bits hashes then
                        pure ()
                      else
                        let bytes := getBytes t globalStart readLen pt
                        match findLastPatternInBytes bytes pattern with
                        | some idx =>
                            let pos := globalStart + idx
                            if pos < end0 then
                              return (some pos, cacheAcc, orderAcc)
                            pure ()
                        | none => pure ()
                | ViE.PieceTree.internal children _ m =>
                    if !bloomMayContain m.bits hashes then
                      pure ()

                      let bytes := getBytes t globalStart readLen pt
                      match findLastPatternInBytes bytes pattern with
                      | some idx =>
                          let pos := globalStart + idx
                          if pos < end0 then (some pos, cache, order) else (none, cache, order)
                      | none => (none, cache, order)
              | ViE.PieceTree.internal children _ m =>
                  if !bloomMayContain m.bits hashes then
                    (none, cache, order)
                  else
                    let spans : Array (ViE.PieceTree × Nat) := Id.run do
                      let mut acc : Array (ViE.PieceTree × Nat) := #[]
                      let mut offset := baseOffset
                      for child in children do
                        acc := acc.push (child, offset)
                        offset := offset + length child
                      return acc
                    Id.run do

                      let mut cacheAcc := cache
                      let mut orderAcc := order
                      while i < spans.size do
                        let j := spans.size - 1 - i
                        let (child, childOffset) := spans[j]!

                      let mut childOffset := baseOffset
                      while i < children.size do
                        let child := children[i]!

                          let (res, cache', order') := searchNode child childOffset cacheAcc orderAcc fuelN
                          cacheAcc := cache'
                          orderAcc := order'
                          match res with
                          | some v =>
                              if v < end0 then
                                return (some v, cacheAcc, orderAcc)
                              pure ()
                          | none => pure ()

                          stack := (child, childOffset) :: stack
                        childOffset := childOffset + length child

                      return (none, cacheAcc, orderAcc)
      searchNode t 0 cache order fuel

        return (none, cacheAcc, orderAcc)

  let fuel := (height t + 4) * 32 + 64
  searchPrevCore t pt pattern startExclusive chunkSize useBloom cache order cacheMax fuel

  searchPrevCore t pt pattern startExclusive chunkSize useBloom cache order cacheMax

/-- Get byte offset from Row/Col (display column) using per-line index cache if available. -/
def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=

/-- Get byte offset from Row/Col (display column) with configurable tab stop. -/
def getOffsetFromPointInBufferWithTabStop (buffer : FileBuffer) (row col tabStop : Nat) : Option Nat :=

      let byteOff := match buffer.cache.findIndex ⟨row⟩ with
        | some idx => ViE.Unicode.displayColToByteOffsetFromIndex idx col
        | none => ViE.Unicode.displayColToByteOffset line col

      let byteOff := ViE.Unicode.displayColToByteOffsetWithTabStop line tabStop col

/-- Get line length from FileBuffer (delegates to PieceTable) -/
def getLineLengthFromBuffer (buffer : FileBuffer) (n : Row) : Option Nat :=

/-- Get line length from FileBuffer with configurable tab stop. -/
def getLineLengthFromBufferWithTabStop (buffer : FileBuffer) (n : Row) (tabStop : Nat) : Option Nat :=

  | some line => some (ViE.Unicode.stringWidth line)

  | some line => some (ViE.Unicode.stringWidthWithTabStop line tabStop)

/-- Get byte offset from Row/Col (display column) using default tab stop. -/
def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=
  getOffsetFromPointInBufferWithTabStop buffer row col 4
/-- Get line length from FileBuffer (delegates to PieceTable) using default tab stop. -/
def getLineLengthFromBuffer (buffer : FileBuffer) (n : Row) : Option Nat :=
  getLineLengthFromBufferWithTabStop buffer n 4

  let (_, tabKeys) := ViE.parseKey ViE.initialState '\x09' (t0 + 30)
  assertEqual "Tab parses as char tab" [Key.char '\t'] tabKeys

  let s_tab_insert ← runKeys s0 [Key.char 'i', Key.char '\t']
  assertCursor "Tab advances cursor to next tab stop in insert mode" s_tab_insert 0 4
  let s_tab_backspace ← runKeys s0 [Key.char 'i', Key.char '\t', Key.backspace]
  assertBuffer "Tab backspace deletes tab in insert mode" s_tab_backspace ""
  assertCursor "Tab backspace restores cursor column" s_tab_backspace 0 0

  let s_tab ← runKeys s0 [Key.char 'i', Key.char '\t', Key.esc]
  assertBuffer "Tab inserts in insert mode" s_tab "\t"
  assertCursor "Esc after tab returns to tab char in normal mode" s_tab 0 0
  let s0_tab8 := { s0 with config := { s0.config with tabStop := 8 } }
  let s_tab8 ← runKeys s0_tab8 [Key.char 'i', Key.char '\t']
  assertCursor "Tab follows custom tabStop in insert mode" s_tab8 0 8

  tabStop := 4