Native van Emde Boas insertion descent

Insertion updates local extrema in place and recurses at most once per level: either into the summary when the target cluster was empty (after installing the cluster's singleton extrema directly), or into the already-occupied target cluster. Repeated insertion of a local minimum terminates immediately.

Main definitions

• InsertEntry: the insertion-loop register invariant.
• insertNext: a mathematical description of one native insertion iteration.

Main results

• insertBody_exec: an actual insertion iteration takes at most 37 instructions.
• insertLoop_spec: insertion takes at most 39 * (d + 1) + 2 loop instructions, produces a valid memory representation of tree.insert key, and preserves all memory outside [base, base + span d).

References

• E. Demaine, Divide and conquer: van Emde Boas trees, Lecture 4

structure Cslib.Algorithms.WordRAM.VanEmdeBoas.InsertEntry (base key : ℕ) (s : WordRAM.Data 32) : Prop

The constant and traversal registers at entry to an unfinished insertion.

• zero_eq : s.regs zero = 0
• one_eq : s.regs one = 1
• two_eq : s.regs two = 2
• three_eq : s.regs three = 3
• four_eq : s.regs four = 4
• five_eq : s.regs five = 5
• p_eq : s.regs p = base
• x_eq : s.regs x = key
• runFlag_eq : s.regs runFlag = 1

def Cslib.Algorithms.WordRAM.VanEmdeBoas.insertNext (s : WordRAM.Data 32) (base key : ℕ) : WordRAM.Data 32

Mathematical description of one native insertion iteration.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insertBody_exec {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : InsertEntry base key s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hkey : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) : WordRAM.ExecWithin w insertBody s (insertNext s base key) 37

One actual insertion iteration, including all branches and address calculations, executes within 37 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insertLoop_spec {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : InsertEntry base key s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hkey : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w insertLoop s z (39 * (d + 1) + 2) ∧ Rep (tree.insert key) base z.mem ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d ≤ a → z.mem a = s.mem a

The insertion loop is correct for every depth and arbitrary surrounding memory. It executes within 39 * (d + 1) + 2 instructions, establishes Rep (tree.insert key) base z.mem, and leaves all memory outside [base, base + span d) unchanged.