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.DfsConst (base d : ℕ) (s : WordRAM.Data 32) : Prop

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

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).

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).