Recursive van Emde Boas memory representation

A tree occupies a contiguous five-word header followed by its summary and clusters. An empty record's minimum and maximum cells may contain arbitrary stale words; its presence flag and static split/child-span fields remain specified. Memory outside the recursive footprint is unconstrained by this representation.

This is a memory predicate and its frame/update calculus. It does not by itself provide an initializer, native execution, or an implemented time/space bound. The minimum-excluded algorithm follows [Dem15], whose notes credit Michael Bender; this particular contiguous record layout is an engineering choice.

Main definitions

• Header: the five-word record, allowing stale empty extrema.
• Rep: recursive interpretation of actual memory as a functional tree.
• writeBounds: the concrete presence/extrema writes.

Main results

• rep_frame: changing memory outside a represented interval preserves it.
• rep_writeBounds, rep_replace_cluster, rep_replace_summary: local representation updates.

References

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

def Cslib.Algorithms.WordRAM.VanEmdeBoas.splitSize : ℕ → ℕ

Stored split size: zero marks a leaf.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.childSpan : ℕ → ℕ

Stored size of each recursively allocated child record.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.Header (d : ℕ) (b : Option (ℕ × ℕ)) (p : ℕ) (mem : ℕ → ℕ) : Prop

A record header; absent extrema are deliberately unconstrained.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.Rep {d : ℕ} : Lean.VanEmdeBoas.Tree d → ℕ → (ℕ → ℕ) → Prop

Recursive, interval-local representation of a functional tree in actual memory.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.Rep.header {d p : ℕ} {t : Lean.VanEmdeBoas.Tree d} {mem : ℕ → ℕ} (hr : Rep t p mem) : Header d t.bounds p mem

A represented tree exposes the header of its root, regardless of surrounding memory.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.universeSize_le_span (d : ℕ) : Lean.VanEmdeBoas.universeSize d ≤ Lean.VanEmdeBoas.span d

The recursive record is large enough to store every universe index as a word offset.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.span_le_succ (d : ℕ) : Lean.VanEmdeBoas.span d ≤ Lean.VanEmdeBoas.span (d + 1)

Every smaller record size is bounded by its parent record size.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.splitSize_le_span (d : ℕ) : splitSize d ≤ Lean.VanEmdeBoas.span d

Every split size is bounded by its record span.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.childSpan_le_span (d : ℕ) : childSpan d ≤ Lean.VanEmdeBoas.span d

Every child span is bounded by its parent record span.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.maximum_lt_universe {d p m M : ℕ} {t : Lean.VanEmdeBoas.Tree d} {mem : ℕ → ℕ} (ht : t.Valid) (hr : Rep t p mem) (hb : t.bounds = some (m, M)) : mem (p + 2) = M ∧ M < Lean.VanEmdeBoas.universeSize d

A valid occupied header stores a maximum below its subtree universe.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_descent_safe {d p m M x : ℕ} {s : Lean.VanEmdeBoas.Tree d} {c : Fin (Lean.VanEmdeBoas.universeSize d) → Lean.VanEmdeBoas.Tree d} {mem : ℕ → ℕ} (ht : (Lean.VanEmdeBoas.Tree.node (some (m, M)) s c).Valid) (hr : Rep (Lean.VanEmdeBoas.Tree.node (some (m, M)) s c) p mem) (hx : x < mem (p + 2)) : x / Lean.VanEmdeBoas.universeSize d < Lean.VanEmdeBoas.universeSize d ∧ x % Lean.VanEmdeBoas.universeSize d < Lean.VanEmdeBoas.universeSize d ∧ p + Lean.VanEmdeBoas.clusterOffset d (x / Lean.VanEmdeBoas.universeSize d) + Lean.VanEmdeBoas.span d ≤ p + Lean.VanEmdeBoas.span (d + 1)

The cached-maximum guard makes every computed cluster index valid, even for a query initially outside the universe. No hypothesis constrains memory outside the represented tree.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_descendant_read_safe {d p m M x a : ℕ} {s : Lean.VanEmdeBoas.Tree d} {c : Fin (Lean.VanEmdeBoas.universeSize d) → Lean.VanEmdeBoas.Tree d} {mem : ℕ → ℕ} (ht : (Lean.VanEmdeBoas.Tree.node (some (m, M)) s c).Valid) (hr : Rep (Lean.VanEmdeBoas.Tree.node (some (m, M)) s c) p mem) (hx : x < mem (p + 2)) (ha : a < 5) : p ≤ p + Lean.VanEmdeBoas.clusterOffset d (x / Lean.VanEmdeBoas.universeSize d) + a ∧ p + Lean.VanEmdeBoas.clusterOffset d (x / Lean.VanEmdeBoas.universeSize d) + a < p + Lean.VanEmdeBoas.span (d + 1)

Every header word of a cluster reached through the maximum guard lies in its parent interval. This statement applies before reading that cluster, not only after it is represented.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.header_congr {d p : ℕ} {b : Option (ℕ × ℕ)} {m m' : ℕ → ℕ} (h : ∀ a < 5, m (p + a) = m' (p + a)) : Header d b p m ↔ Header d b p m'

A header depends only on its five words.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.rep_congr {d p : ℕ} {t : Lean.VanEmdeBoas.Tree d} {m m' : ℕ → ℕ} (h : ∀ a < Lean.VanEmdeBoas.span d, m (p + a) = m' (p + a)) : Rep t p m ↔ Rep t p m'

Representation depends only on the allocated recursive interval.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.rep_frame {d p : ℕ} {t : Lean.VanEmdeBoas.Tree d} {m m' : ℕ → ℕ} (hr : Rep t p m) (h : ∀ (a : ℕ), p ≤ a → a < p + Lean.VanEmdeBoas.span d → m' a = m a) : Rep t p m'

Arbitrary changes outside a tree interval preserve its representation.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.writeBounds (mem : ℕ → ℕ) (p : ℕ) : Option (ℕ × ℕ) → ℕ → ℕ

Write presence and, only for a nonempty record, the two extrema.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.writeBounds_away {mem : ℕ → ℕ} {p a : ℕ} (b : Option (ℕ × ℕ)) (ha : a < p ∨ p + 3 ≤ a) : writeBounds mem p b a = mem a

Updating extrema leaves every cell outside the three-word bounds area unchanged.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.header_writeBounds {d p : ℕ} {old : Option (ℕ × ℕ)} {mem : ℕ → ℕ} (hr : Header d old p mem) (b : Option (ℕ × ℕ)) : Header d b p (writeBounds mem p b)

Concrete extrema writes preserve static header fields.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.rep_writeBounds {d p : ℕ} {t : Lean.VanEmdeBoas.Tree d} {mem : ℕ → ℕ} (hr : Rep t p mem) (b : Option (ℕ × ℕ)) : Rep (t.withBounds b) p (writeBounds mem p b)

Concrete extrema writes change precisely the represented root bounds.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.rep_replace_cluster {d p : ℕ} {b : Option (ℕ × ℕ)} {s : Lean.VanEmdeBoas.Tree d} {c : Fin (Lean.VanEmdeBoas.universeSize d) → Lean.VanEmdeBoas.Tree d} {mem mem' : ℕ → ℕ} (hr : Rep (Lean.VanEmdeBoas.Tree.node b s c) p mem) (i : Fin (Lean.VanEmdeBoas.universeSize d)) {t : Lean.VanEmdeBoas.Tree d} (ht : Rep t (p + Lean.VanEmdeBoas.clusterOffset d ↑i) mem') (hf : ∀ (a : ℕ), a < p + Lean.VanEmdeBoas.clusterOffset d ↑i ∨ p + Lean.VanEmdeBoas.clusterOffset d ↑i + Lean.VanEmdeBoas.span d ≤ a → mem' a = mem a) : Rep (Lean.VanEmdeBoas.Tree.node b s (Function.update c i t)) p mem'

Replacing one cluster interval preserves its parent, summary and sibling clusters.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.rep_replace_summary {d p : ℕ} {b : Option (ℕ × ℕ)} {s s' : Lean.VanEmdeBoas.Tree d} {c : Fin (Lean.VanEmdeBoas.universeSize d) → Lean.VanEmdeBoas.Tree d} {mem mem' : ℕ → ℕ} (hr : Rep (Lean.VanEmdeBoas.Tree.node b s c) p mem) (hs : Rep s' (p + Lean.VanEmdeBoas.summaryOffset) mem') (hf : ∀ (a : ℕ), a < p + Lean.VanEmdeBoas.summaryOffset ∨ p + Lean.VanEmdeBoas.summaryOffset + Lean.VanEmdeBoas.span d ≤ a → mem' a = mem a) : Rep (Lean.VanEmdeBoas.Tree.node b s' c) p mem'

Replacing the summary interval preserves the parent header and every cluster.