Charged uniform Word-RAM initialization of van Emde Boas trees

This module certifies a single fixed 32-register Word-RAM program (initProgram) that initializes an empty recursive van Emde Boas tree of arbitrary depth d at base address base, together with the scratch stack pointer at base + span d, without depth-dependent code generation, square-root oracle instructions, or uncharged zero-memory assumptions.

The initializer executes in three phases:

1. Compute (universeSize d, span d) by d iterations of the layout recurrences.
2. Set tableBase = stackBase = base + span d and populate a (splitSize k, childSpan k) lookup table of 2 * (d + 1) words at [tableBase, tableBase + 2 * (d + 1)).
3. Traverse the recursive layout in depth-first order using d words of per-depth cluster counters at [tableBase + 2 * (d + 1) + 1, tableBase + 3 * d + 2], writing 0, splitSize k, and childSpan k into every depth-k header while leaving empty minimum/maximum cells untouched.

The program initProgram and its first two phases are developed in Complexity.Algorithms.WordRAM.VanEmdeBoas.Init.Table and re-exported here.

Main definitions

• DfsConst, DfsState: the constant-register and loop invariants of the Phase 3 traversal.

Main results

• init_dispatch_spec: structured execution in at most 8 * span d + 20 * d + 24 instructions, establishing Rep (Tree.empty d) base z.mem, z.regs root = base, and z.regs stackBase = base + span d, while preserving all memory outside [base, base + span d + 4 * (d + 1)).
• init_call, init_executes, init_executes_generic: bounded-state, flat, and generic RAM initialization certificates.
• init_space_le: the total tree-plus-scratch footprint is at most 10 * universeSize d + 4 * (d + 1) words.

References

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

Phase 3: depth-first empty-header initialization

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsSetupData (s : WordRAM.Data 32) (base d : ℕ) : WordRAM.Data 32

State after dfsSetup.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsSetup_exec {w base d : ℕ} {s : WordRAM.Data 32} (h0 : s.regs zero = 0) (h1 : s.regs one = 1) (hroot : s.regs root = base) (hdepth : s.regs depth = d) (hsp : s.regs sp = base + Lean.VanEmdeBoas.span d + 2 * (d + 1)) : WordRAM.Exec w dfsSetup s (dfsSetupData s base d) 5

def Cslib.Algorithms.WordRAM.VanEmdeBoas.DfsConst (base d : ℕ) (s : WordRAM.Data 32) : Prop

Constant registers and lookup-table invariant preserved throughout the Phase 3 DFS loop.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.DfsConst.tableInv {base d : ℕ} {s : WordRAM.Data 32} (hc : DfsConst base d s) : TableInv (base + Lean.VanEmdeBoas.span d) d s.mem

Extract the lookup-table invariant from DfsConst.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.DfsConst.of_regs_eq {base d : ℕ} {s s' : WordRAM.Data 32} (hc : DfsConst base d s) (hregs : ∀ r ∈ [zero, one, two, three, four, five, root, depth, payload, tableBase, stackBase, low], s'.regs r = s.regs r) (hinv : TableInv (base + Lean.VanEmdeBoas.span d) d s'.mem) : DfsConst base d s'

Transfer DfsConst across a state update that preserves the twelve constant registers and establishes the lookup-table invariant on the new memory.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.DfsState (base d ptr k kindVal : ℕ) (s : WordRAM.Data 32) : Prop

Active DFS state at pointer ptr, subtree depth k, and phase kindVal (0 = enter, 1 = exit).

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsLeafData (s : WordRAM.Data 32) (base d ptr : ℕ) : WordRAM.Data 32

State after dfsBody at a leaf (kind = 0, x = 0).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody_leaf_exec {w base d ptr : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d ptr 0 0 s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hptr_end : ptr + 5 ≤ base + Lean.VanEmdeBoas.span d) : WordRAM.ExecWithin w dfsBody s (dfsLeafData s base d ptr) 14

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsEnterSuccData (s : WordRAM.Data 32) (base d ptr k : ℕ) : WordRAM.Data 32

State after dfsBody entering an internal node (kind = 0, x = k + 1).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody_enter_succ_exec {w base d ptr k : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d ptr (k + 1) 0 s) (hk : k + 1 ≤ d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hptr_end : ptr + Lean.VanEmdeBoas.span (k + 1) ≤ base + Lean.VanEmdeBoas.span d) : WordRAM.ExecWithin w dfsBody s (dfsEnterSuccData s base d ptr k) 17

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsNextClusterData (s : WordRAM.Data 32) (base d k cnt : ℕ) : WordRAM.Data 32

State after dfsBody advancing from one child to the next cluster (kind = 1, x = k, mem (low + k + 1) = cnt + 1).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody_next_cluster_exec {w base d ptr k cnt : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d ptr k 1 s) (hk : k + 1 ≤ d) (hcnt : s.mem (base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + (k + 1)) = cnt + 1) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hcnt_fit : WordRAM.Fits w (cnt + 1 - 1)) : WordRAM.ExecWithin w dfsBody s (dfsNextClusterData s base d k cnt) 13

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsExitNodeData (s : WordRAM.Data 32) (base d k : ℕ) : WordRAM.Data 32

State after dfsBody finishing all clusters of a depth-k + 1 node (kind = 1, x = k, mem (low + k + 1) = 0).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody_exit_node_exec {w base d ptr k : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d ptr k 1 s) (hk : k + 1 ≤ d) (hrem : s.mem (base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + (k + 1)) = 0) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) : WordRAM.ExecWithin w dfsBody s (dfsExitNodeData s base d k) 9

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsFinishData (s : WordRAM.Data 32) (d : ℕ) : WordRAM.Data 32

State after dfsBody exiting the root (kind = 1, x = d).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody_finish_exec {w base d ptr : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d ptr d 1 s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) : WordRAM.ExecWithin w dfsBody s (dfsFinishData s d) 5

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfs_clusters_spec {w base d ptr k : ℕ} (hk : k + 1 ≤ d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hptr_end : ptr + Lean.VanEmdeBoas.span (k + 1) ≤ base + Lean.VanEmdeBoas.span d) (ih : ∀ {p₀ : ℕ} {s₀ : WordRAM.Data 32}, DfsState base d p₀ k 0 s₀ → p₀ + Lean.VanEmdeBoas.span k ≤ base + Lean.VanEmdeBoas.span d → ∃ (s₁ : WordRAM.Data 32), DfsState base d (p₀ + Lean.VanEmdeBoas.span k) k 1 s₁ ∧ Rep (Lean.VanEmdeBoas.Tree.empty k) p₀ s₁.mem ∧ (∀ (a : ℕ), a < p₀ ∨ p₀ + Lean.VanEmdeBoas.span k ≤ a → a < base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + 1 ∨ base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + k < a → s₁.mem a = s₀.mem a) ∧ ∀ (z : WordRAM.Data 32) (T_cont : ℕ), WordRAM.ExecWithin w dfsLoop s₁ z T_cont → WordRAM.ExecWithin w dfsLoop s₀ z (8 * Lean.VanEmdeBoas.span k - 15 + T_cont)) (cnt : ℕ) {m : ℕ} {s : WordRAM.Data 32} (hm : m + cnt = Lean.VanEmdeBoas.universeSize k) (hs : DfsState base d (ptr + 5 + (m + 1) * Lean.VanEmdeBoas.span k) k 1 s) (hcnt : s.mem (base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + (k + 1)) = cnt) (hprev : ∀ (i : Fin (Lean.VanEmdeBoas.universeSize k)), ↑i < m → Rep (Lean.VanEmdeBoas.Tree.empty k) (ptr + Lean.VanEmdeBoas.clusterOffset k ↑i) s.mem) : ∃ (s' : WordRAM.Data 32), DfsState base d (ptr + Lean.VanEmdeBoas.span (k + 1)) k 1 s' ∧ s'.mem (base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + (k + 1)) = 0 ∧ (∀ (i : Fin (Lean.VanEmdeBoas.universeSize k)), Rep (Lean.VanEmdeBoas.Tree.empty k) (ptr + Lean.VanEmdeBoas.clusterOffset k ↑i) s'.mem) ∧ (∀ (a : ℕ), a < ptr + 5 + (m + 1) * Lean.VanEmdeBoas.span k ∨ ptr + Lean.VanEmdeBoas.span (k + 1) ≤ a → a < base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + 1 ∨ base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + (k + 1) < a → s'.mem a = s.mem a) ∧ ∀ (z : WordRAM.Data 32) (T_cont : ℕ), WordRAM.ExecWithin w dfsLoop s' z T_cont → WordRAM.ExecWithin w dfsLoop s z (cnt * (8 * Lean.VanEmdeBoas.span k) + T_cont)

Cluster-iteration helper for dfs_subtree_spec at depth k + 1: given the induction hypothesis ih at depth k, initializes the remaining cnt clusters starting at index m (where m + cnt = universeSize k) in cnt * (8 * span k) loop instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfs_subtree_spec {w base d : ℕ} (k : ℕ) (hk : k ≤ d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) {ptr : ℕ} {s : WordRAM.Data 32} : DfsState base d ptr k 0 s → ptr + Lean.VanEmdeBoas.span k ≤ base + Lean.VanEmdeBoas.span d → ∃ (s' : WordRAM.Data 32), DfsState base d (ptr + Lean.VanEmdeBoas.span k) k 1 s' ∧ Rep (Lean.VanEmdeBoas.Tree.empty k) ptr s'.mem ∧ (∀ (a : ℕ), a < ptr ∨ ptr + Lean.VanEmdeBoas.span k ≤ a → a < base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + 1 ∨ base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + k < a → s'.mem a = s.mem a) ∧ ∀ (z : WordRAM.Data 32) (T_cont : ℕ), WordRAM.ExecWithin w dfsLoop s' z T_cont → WordRAM.ExecWithin w dfsLoop s z (8 * Lean.VanEmdeBoas.span k - 15 + T_cont)

Subtree initialization theorem: from DfsState base d ptr k 0 s with k ≤ d and ptr + span k ≤ base + span d, the DFS loop initializes Rep (Tree.empty k) ptr s'.mem and reaches DfsState base d (ptr + span k) k 1 s' in at most 8 * span k - 15 instructions, modifying only [ptr, ptr + span k) and counters [low + 1, low + k].

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsLoop_spec {w base d : ℕ} {s : WordRAM.Data 32} (hs : DfsState base d base d 0 s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w dfsLoop s z (8 * Lean.VanEmdeBoas.span d - 6) ∧ Rep (Lean.VanEmdeBoas.Tree.empty d) base z.mem ∧ z.regs root = base ∧ z.regs payload = base + Lean.VanEmdeBoas.span d ∧ z.regs stackBase = base + Lean.VanEmdeBoas.span d ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d ≤ a → a < base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + 1 ∨ base + Lean.VanEmdeBoas.span d + 2 * (d + 1) + d < a → z.mem a = s.mem a

Complete Phase 3 DFS loop specification: from DfsState base d base d 0 s, dfsLoop terminates in at most 8 * span d - 6 instructions, establishing Rep (Tree.empty d) base z.mem, preserving root, payload, and stackBase, and modifying only [base, base + span d) and [base + span d + 2 * (d + 1) + 1, base + span d + 3 * d + 2].

Complete initializer specifications

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_dispatch_spec {w base d : ℕ} {s : WordRAM.Data 32} (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hroot : s.regs root = base) (hdepth : s.regs depth = d) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w initProgram s z (8 * Lean.VanEmdeBoas.span d + 20 * d + 24) ∧ Rep (Lean.VanEmdeBoas.Tree.empty d) base z.mem ∧ z.regs root = base ∧ z.regs stackBase = base + Lean.VanEmdeBoas.span d ∧ z.regs out = base + Lean.VanEmdeBoas.span d ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d + 4 * (d + 1) ≤ a → z.mem a = s.mem a

Complete structured execution of initProgram (excluding only the final flat halt): from any state with s.regs root = base and s.regs depth = d, initProgram executes in at most 8 * span d + 20 * d + 24 instructions, establishes Rep (Tree.empty d) base z.mem, preserves z.regs root = base, sets z.regs stackBase = base + span d and z.regs out = base + span d, and modifies no memory outside [base, base + span d + 4 * (d + 1)).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_call {w base d : ℕ} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hroot : s.regs root = base) (hdepth : s.regs depth = d) : ∃ (z : WordRAM.Data 32) (n : ℕ), n + 1 ≤ 8 * Lean.VanEmdeBoas.span d + 20 * d + 25 ∧ WordRAM.Exec w initProgram s z n ∧ WordRAM.Data.Bounded w z ∧ Rep (Lean.VanEmdeBoas.Tree.empty d) base z.mem ∧ z.regs root = base ∧ z.regs stackBase = base + Lean.VanEmdeBoas.span d ∧ z.regs out = base + Lean.VanEmdeBoas.span d ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d + 4 * (d + 1) ≤ a → z.mem a = s.mem a

Bounded-caller initialization certificate: from any bounded state with s.regs root = base and s.regs depth = d, initProgram executes in at most 8 * span d + 20 * d + 25 instructions (including the final halt), preserves boundedness, establishes Rep (Tree.empty d) base z.mem, and sets z.regs root = base and z.regs stackBase = base + span d.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_executes {w base d : ℕ} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hroot : s.regs root = base) (hdepth : s.regs depth = d) : ∃ n ≤ 8 * Lean.VanEmdeBoas.span d + 20 * d + 25, WordRAM.Executes w (initProgram.program out) { pc := 0, data := s } (base + Lean.VanEmdeBoas.span d) n

Flat bounded-word execution of initProgram.program out, including the final halt, in at most 8 * span d + 20 * d + 25 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_executes_generic {w base d : ℕ} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hroot : s.regs root = base) (hdepth : s.regs depth = d) : ∃ n ≤ 8 * Lean.VanEmdeBoas.span d + 20 * d + 25, GenericRAM.Executes w (initProgram.program out).toGeneric (WordRAM.State.toGeneric WordRAM.Basis.standard { pc := 0, data := s }) (base + Lean.VanEmdeBoas.span d) n

Exact transfer of the flat initializer execution into the shared generic RAM model.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_executes_universe {w base d : ℕ} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (hroot : s.regs root = base) (hdepth : s.regs depth = d) : ∃ n ≤ 80 * Lean.VanEmdeBoas.universeSize d + 20 * d, WordRAM.Executes w (initProgram.program out) { pc := 0, data := s } (base + Lean.VanEmdeBoas.span d) n

The flat initializer instruction bound written directly in terms of universeSize d.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.init_space_le (d : ℕ) : Lean.VanEmdeBoas.span d + 4 * (d + 1) ≤ 10 * Lean.VanEmdeBoas.universeSize d + 4 * (d + 1)

The combined tree and scratch region of span d + 4 * (d + 1) words is bounded by 10 * universeSize d + 4 * (d + 1).