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.insertNext_constants {base key : ℕ} {s : WordRAM.Data 32} (hs : InsertEntry base key s) : (insertNext s base key).regs zero = 0 ∧ (insertNext s base key).regs one = 1 ∧ (insertNext s base key).regs two = 2 ∧ (insertNext s base key).regs three = 3 ∧ (insertNext s base key).regs four = 4 ∧ (insertNext s base key).regs five = 5

Constant registers are preserved by an insertion iteration.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.writeBounds_update_min_max {mem : ℕ → ℕ} {base m M key : ℕ} (hpres : mem base = 1) (hm : mem (base + 1) = m) (hM : mem (base + 2) = M) (hle : m ≤ M) : (have m₁ := if key < m then Function.update mem (base + 1) key else mem; have displaced := if key < m then m else key; if M < displaced then Function.update m₁ (base + 2) displaced else m₁) = writeBounds mem base (some (min m key, max M key))

Updating base + 1 and base + 2 in place on a valid occupied header agrees with writeBounds at every memory cell.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_descent_safe {d base m M key : ℕ} {s : Lean.VanEmdeBoas.Tree d} {c : Fin (Lean.VanEmdeBoas.universeSize d) → Lean.VanEmdeBoas.Tree d} (ht : (Lean.VanEmdeBoas.Tree.node (some (m, M)) s c).Valid) (hkey : key < Lean.VanEmdeBoas.universeSize (d + 1)) : have displaced := max m key; displaced / Lean.VanEmdeBoas.universeSize d < Lean.VanEmdeBoas.universeSize d ∧ displaced % Lean.VanEmdeBoas.universeSize d < Lean.VanEmdeBoas.universeSize d ∧ base + Lean.VanEmdeBoas.clusterOffset d (displaced / Lean.VanEmdeBoas.universeSize d) + Lean.VanEmdeBoas.span d ≤ base + Lean.VanEmdeBoas.span (d + 1)

An occupied node's displaced key max m key has valid cluster coordinates and lies in the parent record interval whenever key < universeSize (d + 1).

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.