Van Emde Boas initializer program and Phase 1–2 lookup-table construction

This module defines the fixed 32-register structured initializer program initProgram for recursive van Emde Boas trees and certifies its first two phases:

1. Computing (universeSize d, span d) by d iterations of the layout recurrences (sizeLoop).
2. Populating the (splitSize k, childSpan k) lookup table of 2 * (d + 1) words at [base + span d, base + span d + 2 * (d + 1)) (tableLoop).

Main definitions

• initProgram: the fixed 32-register structured initializer program.
• TableInv: the lookup-table invariant for (splitSize j, childSpan j).

Main results

• sizeLoop_spec: Phase 1 recurrence loop specification.
• tableLoop_spec: Phase 2 lookup-table loop specification.

References

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

Structured initializer program

def Cslib.Algorithms.WordRAM.VanEmdeBoas.initSetup : WordRAM.Code WordRAM.Basis.standard 32

Constant and recurrence-seed setup for Phase 1.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.sizeBody : WordRAM.Code WordRAM.Basis.standard 32

One step of the (universeSize, span) recurrence loop.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.sizeLoop : WordRAM.Code WordRAM.Basis.standard 32

Phase 1 loop computing (universeSize d, span d).

def Cslib.Algorithms.WordRAM.VanEmdeBoas.tableSetup : WordRAM.Code WordRAM.Basis.standard 32

Setup for the Phase 2 (splitSize, childSpan) table construction.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.tableBody : WordRAM.Code WordRAM.Basis.standard 32

One step of the Phase 2 table-population loop.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.tableLoop : WordRAM.Code WordRAM.Basis.standard 32

Phase 2 loop writing (splitSize (k + 1), childSpan (k + 1)) for k < d.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsSetup : WordRAM.Code WordRAM.Basis.standard 32

Setup for the Phase 3 depth-first header initialization.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsEnterBody : WordRAM.Code WordRAM.Basis.standard 32

Downward step of the DFS initializer: write the current node's empty header and either turn around at a leaf or initialize the cluster counter and descend into the summary.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsExitBody : WordRAM.Code WordRAM.Basis.standard 32

Upward/sibling step of the DFS initializer: ascend to the parent level and either finish when above depth, continue ascending when all clusters are done, or decrement the remaining cluster counter and descend into the next cluster.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsBody : WordRAM.Code WordRAM.Basis.standard 32

Full body of the Phase 3 DFS loop.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dfsLoop : WordRAM.Code WordRAM.Basis.standard 32

Phase 3 DFS traversal loop.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.initProgram : WordRAM.Code WordRAM.Basis.standard 32

Fixed 32-register structured program initializing an empty van Emde Boas tree of depth depth at root and placing stackBase at root + span depth.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.initProgram_not_readsWidth : ¬initProgram.ReadsWidth

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.compiled_initProgram_not_readsWidth : ¬(initProgram.program out).ReadsWidth

Phase 1: computing (universeSize d, span d)

def Cslib.Algorithms.WordRAM.VanEmdeBoas.initSetupData (s : WordRAM.Data 32) : WordRAM.Data 32

State after initSetup.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.initSetup_exec {w : ℕ} {s : WordRAM.Data 32} (hw : WordRAM.Fits w 5) : WordRAM.Exec w initSetup s (initSetupData s) 9

def Cslib.Algorithms.WordRAM.VanEmdeBoas.sizeBodyData (s : WordRAM.Data 32) (k : ℕ) : WordRAM.Data 32

State after one iteration of sizeBody at depth k.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.sizeBody_exec {w d k : ℕ} {s : WordRAM.Data 32} (hk : k < d) (hspan : WordRAM.Fits w (Lean.VanEmdeBoas.span d)) (hd : WordRAM.Fits w d) (h1 : s.regs one = 1) (h5 : s.regs five = 5) (hq : s.regs q = Lean.VanEmdeBoas.universeSize k) (ht : s.regs t = Lean.VanEmdeBoas.span k) (hhigh : s.regs high = k) : WordRAM.ExecWithin w sizeBody s (sizeBodyData s k) 6

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.sizeLoop_spec {w d : ℕ} (rem : ℕ) {k : ℕ} {s : WordRAM.Data 32} (hk : k + rem = d) (hspan : WordRAM.Fits w (Lean.VanEmdeBoas.span d)) (hd : WordRAM.Fits w d) (h0 : s.regs zero = 0) (h1 : s.regs one = 1) (h2 : s.regs two = 2) (h3 : s.regs three = 3) (h4 : s.regs four = 4) (h5 : s.regs five = 5) (hdepth : s.regs depth = d) (hq : s.regs q = Lean.VanEmdeBoas.universeSize k) (ht : s.regs t = Lean.VanEmdeBoas.span k) (hhigh : s.regs high = k) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w sizeLoop s z (8 * rem + 2) ∧ z.regs zero = 0 ∧ z.regs one = 1 ∧ z.regs two = 2 ∧ z.regs three = 3 ∧ z.regs four = 4 ∧ z.regs five = 5 ∧ z.regs root = s.regs root ∧ z.regs depth = d ∧ z.regs q = Lean.VanEmdeBoas.universeSize d ∧ z.regs t = Lean.VanEmdeBoas.span d ∧ z.mem = s.mem

sizeLoop advances (q, t, high) from (universeSize k, span k, k) to (universeSize d, span d, d) in 8 * (d - k) + 2 instructions without modifying memory.

Phase 2: populating the (splitSize, childSpan) table

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

State after tableSetup.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.tableSetup_exec {w base d : ℕ} {s : WordRAM.Data 32} (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (h0 : s.regs zero = 0) (h1 : s.regs one = 1) (h2 : s.regs two = 2) (h5 : s.regs five = 5) (hroot : s.regs root = base) (ht : s.regs t = Lean.VanEmdeBoas.span d) : WordRAM.Exec w tableSetup s (tableSetupData s base d) 11

def Cslib.Algorithms.WordRAM.VanEmdeBoas.tableBodyData (s : WordRAM.Data 32) (sp₀ k : ℕ) : WordRAM.Data 32

State after one iteration of tableBody at depth k and pointer sp₀.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.tableBody_exec {w base d k : ℕ} {s : WordRAM.Data 32} (hk : k < d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (h1 : s.regs one = 1) (h5 : s.regs five = 5) (hsp : s.regs sp = base + Lean.VanEmdeBoas.span d + 2 * (k + 1)) (hq : s.regs q = Lean.VanEmdeBoas.universeSize k) (ht : s.regs t = Lean.VanEmdeBoas.span k) (hhigh : s.regs high = k) : WordRAM.ExecWithin w tableBody s (tableBodyData s (base + Lean.VanEmdeBoas.span d + 2 * (k + 1)) k) 10

def Cslib.Algorithms.WordRAM.VanEmdeBoas.TableInv (tbl m : ℕ) (mem : ℕ → ℕ) : Prop

Lookup-table invariant up to depth m: for all j ≤ m, mem (tbl + 2 * j) = splitSize j and mem (tbl + 2 * j + 1) = childSpan j.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.tableLoop_spec {w base d : ℕ} (rem : ℕ) {k : ℕ} {s : WordRAM.Data 32} (hk : k + rem = d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d + 4 * (d + 1))) (h0 : s.regs zero = 0) (h1 : s.regs one = 1) (h2 : s.regs two = 2) (h3 : s.regs three = 3) (h4 : s.regs four = 4) (h5 : s.regs five = 5) (hroot : s.regs root = base) (hdepth : s.regs depth = d) (hpay : s.regs payload = base + Lean.VanEmdeBoas.span d) (htbl : s.regs tableBase = base + Lean.VanEmdeBoas.span d) (hstk : s.regs stackBase = base + Lean.VanEmdeBoas.span d) (hsp : s.regs sp = base + Lean.VanEmdeBoas.span d + 2 * (k + 1)) (hq : s.regs q = Lean.VanEmdeBoas.universeSize k) (ht : s.regs t = Lean.VanEmdeBoas.span k) (hhigh : s.regs high = k) (hinv : TableInv (base + Lean.VanEmdeBoas.span d) k s.mem) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w tableLoop s z (12 * rem + 2) ∧ z.regs zero = 0 ∧ z.regs one = 1 ∧ z.regs two = 2 ∧ z.regs three = 3 ∧ z.regs four = 4 ∧ z.regs five = 5 ∧ z.regs root = base ∧ z.regs depth = d ∧ z.regs payload = base + Lean.VanEmdeBoas.span d ∧ z.regs tableBase = base + Lean.VanEmdeBoas.span d ∧ z.regs stackBase = base + Lean.VanEmdeBoas.span d ∧ z.regs sp = base + Lean.VanEmdeBoas.span d + 2 * (d + 1) ∧ TableInv (base + Lean.VanEmdeBoas.span d) d z.mem ∧ ∀ (a : ℕ), a < base + Lean.VanEmdeBoas.span d + 2 * (k + 1) ∨ base + Lean.VanEmdeBoas.span d + 2 * (d + 1) ≤ a → z.mem a = s.mem a

tableLoop populates the lookup table from depth k up to d in 12 * (d - k) + 2 instructions, advancing sp to base + span d + 2 * (d + 1) and preserving all memory outside [base + span d + 2 * (k + 1), base + span d + 2 * (d + 1)).