4kusto/vie - Change LSCUXT3235I5ZZPZM2MMGLECHU2LAX2TKLRHDULONDAS5JEWTB7QC

optimize piece-tree bloom construction for edit-time paths, plumb bloom build-on-edit config through buffer loading, and reduce concat leaf rebuild overhead

Created by 4kusto on February 18, 2026

LSCUXT3235I5ZZPZM2MMGLECHU2LAX2TKLRHDULONDAS5JEWTB7QC

Dependencies

In channels

main

Change contents

Insertion in ViE/Types.lean at line 129 [5.22248]
[3.13109]
[4.72]
```
  searchBloomBuildOnEdit : Bool := false
```
Insertion in ViE/State/Config.lean at line 30 [5.53268]
[3.13661]
[5.53849]
```
  searchBloomBuildOnEdit := false
```

Replacement in ViE/Data/PieceTable.lean at line 41 [5.73967]

∅:D[6.1692] → [5.74189:74217]

B:BD[5.74189] → [5.74189:74217]

B:BD[5.74217] → [3.13737:13833]

/-- Construct from bytes -/
def PieceTable.fromByteArray (bytes : ByteArray) (buildLeafBits : Bool := true) : PieceTable :=

[6.1692]

[5.74282]

/-- Construct from bytes. `buildOnEdit` controls bloom rebuilding during subsequent edits. -/
def PieceTable.fromByteArray (bytes : ByteArray) (buildLeafBits : Bool := true) (buildOnEdit : Bool := false) : PieceTable :=

Insertion in ViE/Data/PieceTable.lean at line 46 [5.73967]
[6.1824]
[2.9522]
```
      bloomBuildOnEdit := buildOnEdit,
```

Replacement in ViE/Data/PieceTable.lean at line 87 [5.73967]

B:BD[3.14052] → [3.14052:14158]

      original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits,

[3.14052]

[3.14158]

      -- Build bloom bits during initial load if enabled, regardless of edit policy.
      original := bytes, addBuffers := #[], tree := PieceTree.empty, bloomBuildLeafBits := buildLeafBits, bloomBuildOnEdit := true,

Replacement in ViE/Data/PieceTable.lean at line 93 [5.73967]

∅:D[2.10759] → [6.1933:2028]

B:BD[6.1933] → [6.1933:2028]

      original := bytes, addBuffers := #[], tree := tree, bloomBuildLeafBits := buildLeafBits,

[2.10759]

[2.10760]

      original := bytes, addBuffers := #[], tree := tree, bloomBuildLeafBits := buildLeafBits, bloomBuildOnEdit := buildOnEdit,

Replacement in ViE/Data/PieceTable.lean at line 97 [5.73967]

B:BD[5.75576] → [5.75576:75613]

B:BD[5.75613] → [3.14459:14595]

/-- Construct from initial string -/
def PieceTable.fromString (s : String) (buildLeafBits : Bool := true) : PieceTable :=
  PieceTable.fromByteArray s.toUTF8 buildLeafBits

[5.75576]

[5.75704]

/-- Construct from initial string. -/
def PieceTable.fromString (s : String) (buildLeafBits : Bool := true) (buildOnEdit : Bool := false) : PieceTable :=
  PieceTable.fromByteArray s.toUTF8 buildLeafBits buildOnEdit

Insertion in ViE/Data/PieceTable/Tree.lean at line 207 [5.77490]

[7.30545]

[2.14195]

/-- Rolling update for 3-byte polynomial hash:
    h' = ((h - out*base^2) * base + in) mod BloomBits. -/
private def rollHash3 (h : Nat) (outB inB : UInt8) (base baseSq : Nat) : Nat :=
  let m := ViE.BloomBits
  let remove := (outB.toNat * baseSq) % m
  let trimmed := if h >= remove then h - remove else h + m - remove
  ((trimmed * base) + inB.toNat) % m

Insertion in ViE/Data/PieceTable/Tree.lean at line 220 [5.77490]

[7.30715]


private def setMaskBit (mask : ByteArray) (idx : Nat) : ByteArray :=
  let byteIdx := idx / 8
  let bitIdx := idx % 8
  if byteIdx < mask.size then
    let cur := mask[byteIdx]!
    let bit : UInt8 := (1 : UInt8) <<< bitIdx.toUInt8
    mask.set! byteIdx (cur ||| bit)
  else
    mask

Insertion in ViE/Data/PieceTable/Tree.lean at line 231 [5.77490]

[7.30716]

private def applyMaskToBloom (bloom : ByteArray) (mask : ByteArray) : ByteArray := Id.run do
  let mut out := bloom
  let size := min out.size mask.size
  for i in [0:size] do
    let m := mask[i]!
    if m != 0 then
      out := out.set! i (out[i]! ||| m)
  return out

Replacement in ViE/Data/PieceTable/Tree.lean at line 241 [5.77490]
B:BD[7.30806] → [7.30806:30829]
```
  if arr.size < 3 then
```
[7.30806]
[7.30829]
```
  if arr.size < 3 || bloom.size == 0 then
```
Replacement in ViE/Data/PieceTable/Tree.lean at line 244 [5.77490]
B:BD[7.30874] → [7.30874:30897]
```
  let mut out := bloom
```
[7.30874]
[7.30897]
```
  let mut mask : ByteArray := ByteArray.mk (Array.replicate bloom.size (0 : UInt8))
```

Replacement in ViE/Data/PieceTable/Tree.lean at line 246 [5.77490]

B:BD[7.30921] → [7.30921:30999]

    out := addTrigramToBloom out arr[i]! arr[i + 1]! arr[i + 2]!
  return out

[7.30921]

[7.30999]

    let b0 := arr[i]!
    let b1 := arr[i + 1]!
    let b2 := arr[i + 2]!
    let h1 := hash1 b0 b1 b2
    let h2 := hash2 b0 b1 b2
    mask := setMaskBit mask h1
    mask := setMaskBit mask h2
  return applyMaskToBloom bloom mask

Replacement in ViE/Data/PieceTable/Tree.lean at line 290 [5.77490]

B:BD[7.32391] → [7.32391:32640]

def addBytesToBloom (bloom : ByteArray) (carry : Array UInt8) (bytes : ByteArray) : (ByteArray × Array UInt8) :=
  let arr := carry ++ bytes.data
  let bloom' := addTrigramsFromArray bloom arr
  let carry' := takeLastBytes arr 2
  (bloom', carry')

[7.32391]

[7.32640]

def addBytesToBloom (bloom : ByteArray) (carry : Array UInt8) (bytes : ByteArray) : (ByteArray × Array UInt8) := Id.run do
  let total := carry.size + bytes.size
  let carry' :=
    if total <= 2 then
      takeLastBytes (carry ++ bytes.data) 2
    else
      let start := total - 2
      let b0 :=
        if start < carry.size then
          carry[start]!
        else
          bytes[start - carry.size]!
      let b1 :=
        if start + 1 < carry.size then
          carry[start + 1]!
        else
          bytes[start + 1 - carry.size]!
      #[b0, b1]
  if total < 3 || bloom.size == 0 then
    return (bloom, carry')
  let limit := total - 2
  let getAt (i : Nat) : UInt8 :=
    if i < carry.size then carry[i]! else bytes[i - carry.size]!
  let mut h1 := hash1 (getAt 0) (getAt 1) (getAt 2)
  let mut h2 := hash2 (getAt 0) (getAt 1) (getAt 2)
  let mut mask : ByteArray := ByteArray.mk (Array.replicate bloom.size (0 : UInt8))
  for i in [0:limit] do
    mask := setMaskBit mask h1
    mask := setMaskBit mask h2
    if i + 3 < total then
      let outB := getAt i
      let inB := getAt (i + 3)
      h1 := rollHash3 h1 outB inB 31 961
      h2 := rollHash3 h2 outB inB 131 17161
  return (applyMaskToBloom bloom mask, carry')

Replacement in ViE/Data/PieceTable/Tree.lean at line 331 [5.77490]
B:BD[7.32926] → [3.14596:14629]
```
  if !pt.bloomBuildLeafBits then
```
[7.32926]
[7.32960]
```
  if !pt.bloomBuildLeafBits || !pt.bloomBuildOnEdit then
```

Insertion in ViE/Data/PieceTable/Tree.lean at line 432 [5.77490]

[5.80130]

[8.7657]

private def mkLeafWithSearchMeta (pieces : Array ViE.Piece) (searchMeta : ViE.SearchBloom) : ViE.PieceTree :=
  if pieces.size == 0 then
    ViE.PieceTree.empty
  else
    let s := pieces.foldl (fun acc p => acc + (ViE.Stats.ofPiece p)) ViE.Stats.empty
    ViE.PieceTree.leaf pieces s searchMeta

Replacement in ViE/Data/PieceTable/Tree.lean at line 573 [5.77490]

B:BD[9.19728] → [9.19728:19790]

  | ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>

[9.19728]

[9.19790]

  | ViE.PieceTree.leaf ps1 _ sm1, ViE.PieceTree.leaf ps2 _ sm2 =>

Insertion in ViE/Data/PieceTable/Tree.lean at line 578 [5.77490]
[10.9673]
[10.9673]
```
        let mergedMeta := combineBloom sm1 sm2
```
Replacement in ViE/Data/PieceTable/Tree.lean at line 587 [5.77490]
B:BD[10.10087] → [10.10087:10112]
```
            mkLeaf ps pt
```
[10.10087]
[10.10112]
```
            mkLeafWithSearchMeta ps mergedMeta
```

Replacement in ViE/Data/PieceTable/Tree.lean at line 593 [5.77490]

B:BD[10.10285] → [10.10285:10402]

          if ps.size <= ViE.NodeCapacity then mkLeaf ps pt
          else mkInternal #[mkLeaf ps1 pt, mkLeaf ps2 pt]

[10.10285]

[9.19864]

          if ps.size <= ViE.NodeCapacity then
            mkLeafWithSearchMeta ps mergedMeta
          else
            mkInternal #[l, r]

Insertion in ViE/Data/PieceTable/Piece.lean at line 110 [5.93514]
[3.18819]
[8.19665]
```
  bloomBuildOnEdit : Bool := false
```

Replacement in ViE/Buffer/LowIO.lean at line 9 [5.119821]

B:BD[5.119948] → [3.19780:19864]

def emptyBuffer (filename : Option String) (buildLeafBits : Bool) : FileBuffer := {

[5.119948]

[3.19864]

def emptyBuffer (filename : Option String) (buildLeafBits : Bool) (buildOnEdit : Bool) : FileBuffer := {

Replacement in ViE/Buffer/LowIO.lean at line 14 [5.119821]
∅:D[11.3656] → [3.19914:19964]
B:BD[3.19914] → [3.19914:19964]
```
  table := PieceTable.fromString "" buildLeafBits
```
[11.3656]
[3.19964]
```
  table := PieceTable.fromString "" buildLeafBits buildOnEdit
```

Replacement in ViE/Buffer/LowIO.lean at line 19 [5.119821]

B:BD[3.20098] → [3.20098:20195]

def bufferFromData (filename : String) (data : ByteArray) (buildLeafBits : Bool) : FileBuffer :=

[3.20098]

[3.20195]

def bufferFromData (filename : String) (data : ByteArray) (buildLeafBits buildOnEdit : Bool) : FileBuffer :=

Replacement in ViE/Buffer/LowIO.lean at line 21 [5.119821]

B:BD[3.20259] → [3.20259:20318]

  let table := PieceTable.fromByteArray data buildLeafBits

[3.20259]

[3.20318]

  let table := PieceTable.fromByteArray data buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 38 [5.119821]

B:BD[5.120167] → [3.20548:20596]

        return emptyBuffer (some filename) true

[5.120167]

[5.120347]

        return emptyBuffer (some filename) true false

Replacement in ViE/Buffer/LowIO.lean at line 42 [5.119821]

B:BD[5.120440] → [3.20597:20646]

        return bufferFromData filename data true

[5.120440]

[5.120792]

        return bufferFromData filename data true false

Replacement in ViE/Buffer/LowIO.lean at line 45 [5.119821]
B:BD[5.120850] → [3.20647:20693]
```
      return emptyBuffer (some filename) true
```
[5.120850]
[5.121016]
```
      return emptyBuffer (some filename) true false
```
Replacement in ViE/Buffer/LowIO.lean at line 48 [5.119821]
B:BD[5.121066] → [3.20694:20738]
```
    return emptyBuffer (some filename) true
```
[5.121066]
[3.20738]
```
    return emptyBuffer (some filename) true false
```
Insertion in ViE/Buffer/LowIO.lean at line 52 [5.119821]
[3.20894]
[3.20894]
```
  let buildOnEdit := config.searchBloomBuildOnEdit
```

Replacement in ViE/Buffer/LowIO.lean at line 57 [5.119821]

B:BD[3.21005] → [3.21005:21062]

        return emptyBuffer (some filename) buildLeafBits

[3.21005]

[3.21062]

        return emptyBuffer (some filename) buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 60 [5.119821]

B:BD[3.21121] → [3.21121:21179]

        return bufferFromData filename data buildLeafBits

[3.21121]

[3.21179]

        return bufferFromData filename data buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 62 [5.119821]

B:BD[3.21188] → [3.21188:21243]

      return emptyBuffer (some filename) buildLeafBits

[3.21188]

[3.21243]

      return emptyBuffer (some filename) buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 64 [5.119821]

B:BD[3.21256] → [3.21256:21309]

    return emptyBuffer (some filename) buildLeafBits

[3.21256]

[5.121218]

    return emptyBuffer (some filename) buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 71 [5.119821]

B:BD[12.32935] → [3.21310:21358]

        return emptyBuffer (some filename) true

[12.32935]

[12.33232]

        return emptyBuffer (some filename) true false

Replacement in ViE/Buffer/LowIO.lean at line 75 [5.119821]

B:BD[12.33363] → [3.21359:21408]

        return bufferFromData filename data true

[12.33363]

[12.33767]

        return bufferFromData filename data true false

Replacement in ViE/Buffer/LowIO.lean at line 77 [5.119821]
B:BD[12.33776] → [3.21409:21455]
```
      return emptyBuffer (some filename) true
```
[12.33776]
[3.21455]
```
      return emptyBuffer (some filename) true false
```
Replacement in ViE/Buffer/LowIO.lean at line 79 [5.119821]
B:BD[3.21468] → [3.21468:21512]
```
    return emptyBuffer (some filename) true
```
[3.21468]
[3.21512]
```
    return emptyBuffer (some filename) true false
```
Insertion in ViE/Buffer/LowIO.lean at line 83 [5.119821]
[3.21692]
[3.21692]
```
  let buildOnEdit := config.searchBloomBuildOnEdit
```

Replacement in ViE/Buffer/LowIO.lean at line 88 [5.119821]

B:BD[3.21803] → [3.21803:21860]

        return emptyBuffer (some filename) buildLeafBits

[3.21803]

[3.21860]

        return emptyBuffer (some filename) buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 92 [5.119821]

B:BD[3.21991] → [3.21991:22049]

        return bufferFromData filename data buildLeafBits

[3.21991]

[3.22049]

        return bufferFromData filename data buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 94 [5.119821]

B:BD[3.22058] → [3.22058:22113]

      return emptyBuffer (some filename) buildLeafBits

[3.22058]

[12.34057]

      return emptyBuffer (some filename) buildLeafBits buildOnEdit

Replacement in ViE/Buffer/LowIO.lean at line 96 [5.119821]

B:BD[12.34070] → [3.22114:22167]

    return emptyBuffer (some filename) buildLeafBits

[12.34070]

[12.34335]

    return emptyBuffer (some filename) buildLeafBits buildOnEdit

optimize piece-tree bloom construction for edit-time paths, plumb bloom build-on-edit config through buffer loading, and reduce concat leaf rebuild overhead

Dependencies

In channels

Change contents

Insertion in ViE/Types.lean at line 129 [5.22248]

Insertion in ViE/State/Config.lean at line 30 [5.53268]

Replacement in ViE/Data/PieceTable.lean at line 41 [5.73967]

Insertion in ViE/Data/PieceTable.lean at line 46 [5.73967]

Replacement in ViE/Data/PieceTable.lean at line 87 [5.73967]

Replacement in ViE/Data/PieceTable.lean at line 93 [5.73967]

Replacement in ViE/Data/PieceTable.lean at line 97 [5.73967]

Insertion in ViE/Data/PieceTable/Tree.lean at line 207 [5.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 220 [5.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 231 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 241 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 244 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 246 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 290 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 331 [5.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 432 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 573 [5.77490]

Insertion in ViE/Data/PieceTable/Tree.lean at line 578 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 587 [5.77490]

Replacement in ViE/Data/PieceTable/Tree.lean at line 593 [5.77490]

Insertion in ViE/Data/PieceTable/Piece.lean at line 110 [5.93514]

Replacement in ViE/Buffer/LowIO.lean at line 9 [5.119821]

Replacement in ViE/Buffer/LowIO.lean at line 14 [5.119821]