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

• initSetup, sizeBody, sizeLoop: Phase 1 constant setup and (universeSize, span) recurrence loop.
• tableSetup, tableBody, tableLoop: Phase 2 setup and (splitSize, childSpan) lookup-table loop.
• dfsSetup, dfsEnterBody, dfsExitBody, dfsBody, dfsLoop: Phase 3 setup and iterative depth-first header initialization loop.
• initProgram: the fixed 32-register structured initializer program.
• initSetupData, tableSetupData: register and memory state after initSetup and tableSetup.
• 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

The structured initializer program initProgram does not read the word width.

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

The compiled flat initializer program does not read the word width.

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

initSetup executes in 9 instructions and produces initSetupData s.

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

tableSetup executes in 11 instructions and produces tableSetupData s base d.

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