Native van Emde Boas membership descent

The proof state records only the registers required by membership; all other registers and all memory outside the represented tree may be arbitrary. Queries need not belong to the tree universe. The maximum guard is checked before any cluster address is calculated.

Main definitions

• MemberEntry: the membership-loop register invariant.
• memberNext: a mathematical description of one native iteration, not a machine instruction.

Main results

• memberBody_exec: an actual iteration takes at most 26 instructions.
• memberLoop_spec: membership takes at most 28 * (d + 1) + 2 loop instructions, gives the functional answer and preserves all memory.

References

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

structure Cslib.Algorithms.WordRAM.VanEmdeBoas.MemberEntry (base query : ℕ) (s : WordRAM.Data 32) : Prop

The constant, traversal and result registers at entry to an unfinished lookup.

• zero_eq : s.regs zero = 0
• one_eq : s.regs one = 1
• two_eq : s.regs two = 2
• three_eq : s.regs three = 3
• four_eq : s.regs four = 4
• five_eq : s.regs five = 5
• p_eq : s.regs p = base
• x_eq : s.regs x = query
• out_eq : s.regs out = 0
• runFlag_eq : s.regs runFlag = 1

def Cslib.Algorithms.WordRAM.VanEmdeBoas.memberNext (s : WordRAM.Data 32) (base query : ℕ) : WordRAM.Data 32

A description of one native iteration. Each update corresponds to an instruction in memberBody; the description itself is used only in proofs.

@[simp]

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.memberNext_mem (s : WordRAM.Data 32) (base query : ℕ) : (memberNext s base query).mem = s.mem

Membership performs no writes, including on unsuccessful or out-of-universe queries.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.memberBody_exec {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : MemberEntry base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) : WordRAM.ExecWithin w memberBody s (memberNext s base query) 26

One real membership iteration, including all branches and address computations. The sole address-fit assumption covers the represented record endpoint.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.memberNext_constants {base query : ℕ} {s : WordRAM.Data 32} (hs : MemberEntry base query s) : (memberNext s base query).regs zero = 0 ∧ (memberNext s base query).regs one = 1 ∧ (memberNext s base query).regs two = 2 ∧ (memberNext s base query).regs three = 3 ∧ (memberNext s base query).regs four = 4 ∧ (memberNext s base query).regs five = 5

Constant registers are preserved by a membership iteration.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_eq_false_of_max_lt {d m M query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} (ht : tree.Valid) (hb : tree.bounds = some (m, M)) (hx : M < query) : tree.member query = false

A query above the cached maximum is absent; this fact uses validity, not outside memory.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_maximum {d m M : ℕ} {tree : Lean.VanEmdeBoas.Tree d} (ht : tree.Valid) (hb : tree.bounds = some (m, M)) : tree.member M = true

The cached maximum is a valid early successful membership result.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.memberLoop_spec {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : MemberEntry base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w memberLoop s z (28 * (d + 1) + 2) ∧ (z.regs out = if tree.member query = true then 1 else 0) ∧ z.mem = s.mem

The membership loop is correct for every depth and arbitrary surrounding memory. Its bound charges each body, loop test and jump; setup, dispatch and halt are separate.