Native van Emde Boas strict-successor certification

This module certifies the native strict-successor operation (successorDescent followed by successorUnwind) in Complexity.Algorithms.WordRAM.VanEmdeBoas.Program.

During descent, each recursive cluster or summary call pushes a four-word continuation frame (kind, payload, q, t) into the scratch stack [stackBase₀, stackBase₀ + 4 * d). Because Tree.successor checks the cached maximum before recursing, every recursive descent is guaranteed to find a key (found = 1), and successorUnwind pops the pushed frames to reconstruct the universe key in out while restoring sp = stackBase₀.

Main definitions

• SuccessorEntry: register invariant at entry to successorDescent.
• successorDescentNext: mathematical description of one successorDescentBody iteration.
• UnwindState: register and memory invariant during successorUnwind.
• successorUnwindNext: mathematical description of one successorUnwindBody iteration.

Main results

• successorDescentBody_exec: one descent iteration executes in at most 42 instructions.
• successorUnwindBody_cluster_exec, successorUnwindBody_summary_exec: one unwind iteration executes in at most 19 instructions.
• successor_loop_spec: successorDescent; successorUnwind executes in at most 65 * (d + 1) + 4 instructions, computes tree.successor query, restores sp = stackBase₀, preserves Rep tree base z.mem, and leaves all memory outside [stackBase₀, stackBase₀ + 4 * d) unchanged.

References

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

structure Cslib.Algorithms.WordRAM.VanEmdeBoas.SuccessorEntry (stackBase₀ sp₀ base query : ℕ) (s : WordRAM.Data 32) : Prop

The constant, stack, and traversal registers at entry to successorDescent.

• 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
• stackBase_eq : s.regs stackBase = stackBase₀
• sp_eq : s.regs sp = sp₀
• p_eq : s.regs p = base
• x_eq : s.regs x = query
• runFlag_eq : s.regs runFlag = 1

def Cslib.Algorithms.WordRAM.VanEmdeBoas.pushFrameData (s : WordRAM.Data 32) (sp₀ k pay qv tv : ℕ) : WordRAM.Data 32

Effect of pushing a four-word continuation frame (k, pay, qv, tv) at sp₀.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.successorDescentNext (s : WordRAM.Data 32) (sp₀ base query : ℕ) : WordRAM.Data 32

Mathematical description of one successorDescentBody iteration.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successorDescentNext_constants {stackBase₀ sp₀ base query : ℕ} {s : WordRAM.Data 32} (hs : SuccessorEntry stackBase₀ sp₀ base query s) : (successorDescentNext s sp₀ base query).regs zero = 0 ∧ (successorDescentNext s sp₀ base query).regs one = 1 ∧ (successorDescentNext s sp₀ base query).regs two = 2 ∧ (successorDescentNext s sp₀ base query).regs three = 3 ∧ (successorDescentNext s sp₀ base query).regs four = 4 ∧ (successorDescentNext s sp₀ base query).regs five = 5 ∧ (successorDescentNext s sp₀ base query).regs stackBase = stackBase₀

Constant and stackBase registers are preserved by successorDescentNext.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.pushFrameData_mem_away (s : WordRAM.Data 32) (sp₀ k pay qv tv a : ℕ) (ha : a < sp₀ ∨ sp₀ + 4 ≤ a) : (pushFrameData s sp₀ k pay qv tv).mem a = s.mem a

Pushing a four-word frame modifies memory only in [sp₀, sp₀ + 4).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successorDescentBody_exec {d w stackBase₀ sp₀ base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : SuccessorEntry stackBase₀ sp₀ base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hsp : WordRAM.Fits w (sp₀ + 4 * d)) : WordRAM.ExecWithin w successorDescentBody s (successorDescentNext s sp₀ base query) 42

One native successor-descent iteration executes in at most 42 instructions.

structure Cslib.Algorithms.WordRAM.VanEmdeBoas.UnwindState (stackBase₀ sp₀ ans : ℕ) (mem : ℕ → ℕ) (s : WordRAM.Data 32) : Prop

Register and memory invariant at the start of an unwind stage at stack pointer sp₀.

• zero_eq : s.regs zero = 0
• one_eq : s.regs one = 1
• five_eq : s.regs five = 5
• stackBase_eq : s.regs stackBase = stackBase₀
• sp_eq : s.regs sp = sp₀
• found_eq : s.regs found = 1
• out_eq : s.regs out = ans
• mem_eq : s.mem = mem

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

Mathematical description of one successorUnwindBody iteration popping at sp₀.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successorUnwindNext_preserved {stackBase₀ sp₀ childAns : ℕ} {mem : ℕ → ℕ} {s : WordRAM.Data 32} (hs : UnwindState stackBase₀ (sp₀ + 4) childAns mem s) : (successorUnwindNext s sp₀).regs zero = 0 ∧ (successorUnwindNext s sp₀).regs one = 1 ∧ (successorUnwindNext s sp₀).regs five = 5 ∧ (successorUnwindNext s sp₀).regs stackBase = stackBase₀ ∧ (successorUnwindNext s sp₀).regs sp = sp₀ ∧ (successorUnwindNext s sp₀).regs found = 1 ∧ (successorUnwindNext s sp₀).mem = mem

Invariant registers and memory preserved across successorUnwindNext.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successorUnwindBody_cluster_exec {w stackBase₀ sp₀ pay qv tv childAns : ℕ} {mem : ℕ → ℕ} {s : WordRAM.Data 32} (hs : UnwindState stackBase₀ (sp₀ + 4) childAns mem s) (hk : mem sp₀ = 0) (hpay : mem (sp₀ + 1) = pay) (hqv : mem (sp₀ + 2) = qv) (htv : mem (sp₀ + 3) = tv) (hsp : WordRAM.Fits w (sp₀ + 4)) (hout : WordRAM.Fits w (pay + childAns)) : WordRAM.ExecWithin w successorUnwindBody s (successorUnwindNext s sp₀) 19

One cluster-return unwind step (kind = 0) executes in at most 19 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successorUnwindBody_summary_exec {d w stackBase₀ sp₀ base j cm : ℕ} {mem : ℕ → ℕ} {s : WordRAM.Data 32} (hs : UnwindState stackBase₀ (sp₀ + 4) j mem s) (hk : mem sp₀ = 1) (hpay : mem (sp₀ + 1) = base) (hqv : mem (sp₀ + 2) = Lean.VanEmdeBoas.universeSize d) (htv : mem (sp₀ + 3) = Lean.VanEmdeBoas.span d) (hj : j < Lean.VanEmdeBoas.universeSize d) (hcm : mem (base + 5 + (j + 1) * Lean.VanEmdeBoas.span d + 1) = cm) (hcm_lt : cm < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span (d + 1))) (hsp : WordRAM.Fits w (sp₀ + 4)) : WordRAM.ExecWithin w successorUnwindBody s (successorUnwindNext s sp₀) 19

One summary-return unwind step (kind = 1) executes in at most 19 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_some_spec {d w stackBase₀ sp₀ base query ans : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : SuccessorEntry stackBase₀ sp₀ base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hans : tree.successor query = some ans) (hsp_le : stackBase₀ ≤ sp₀) (hdisj : base + Lean.VanEmdeBoas.span d ≤ sp₀) (hfit : WordRAM.Fits w (sp₀ + 4 * d)) : ∃ (s₁ : WordRAM.Data 32) (s₃ : WordRAM.Data 32), WordRAM.ExecWithin w successorDescent s s₁ (44 * (d + 1) + 2) ∧ (∀ (a : ℕ), a < sp₀ ∨ sp₀ + 4 * d ≤ a → s₁.mem a = s.mem a) ∧ UnwindState stackBase₀ sp₀ ans s₁.mem s₃ ∧ ∀ (z : WordRAM.Data 32) (T : ℕ), WordRAM.ExecWithin w successorUnwind s₃ z T → WordRAM.ExecWithin w successorUnwind s₁ z (21 * d + T)

Combined inductive certification of successorDescent and CPS successorUnwind whenever tree.successor query = some ans.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_none_spec {d w stackBase₀ sp₀ base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : SuccessorEntry stackBase₀ sp₀ base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hnone : tree.successor query = none) (hdisj : base + Lean.VanEmdeBoas.span d ≤ sp₀) (hfit : WordRAM.Fits w (sp₀ + 4 * d)) : ∃ (s₁ : WordRAM.Data 32), WordRAM.ExecWithin w successorDescent s s₁ 46 ∧ s₁.regs stackBase = stackBase₀ ∧ s₁.regs sp = sp₀ ∧ s₁.regs found = 0 ∧ s₁.regs out = 0 ∧ s₁.mem = s.mem

When tree.successor query = none, successorDescent terminates in one iteration (46 instructions) with found = 0, out = 0, sp = sp₀, and unchanged memory.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_loop_spec {d w stackBase₀ base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : SuccessorEntry stackBase₀ stackBase₀ base query s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hdisj : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hfit : WordRAM.Fits w (stackBase₀ + 4 * d)) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w (successorDescent.seq successorUnwind) s z (65 * (d + 1) + 4) ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ z.regs sp = stackBase₀ ∧ Rep tree base z.mem ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

Complete certification of successorDescent; successorUnwind from sp = stackBase₀: executes in at most 65 * (d + 1) + 4 instructions, computes tree.successor query, restores sp = stackBase₀, preserves Rep tree base z.mem, and frames memory outside [stackBase₀, stackBase₀ + 4 * d).