Complete native van Emde Boas calls and adaptive dynamic realization

All three operations — insert (tag = 0), member (tag = 1), and strict successor (tag = 2) — execute on the same fixed 32-register dispatcher program, charging constant setup, dispatch branches, every loop instruction, and the final halt.

In addition, this module connects program to the shared Stateful.Spec / DynamicProgram / DynamicCertificate interface on finite sets (Finset ℕ) and combines the uniform native initializer initProgram with arbitrary adaptive client histories (run_initialized).

Main definitions

• setupData: mathematical description of the twelve charged setup instructions.
• Operation, spec, dynamicProgram, SetRep, certificate: the stateful finite-set specification and its fixed-program Word-RAM realization.

Main results

• insert_dispatch_spec, insert_call, insert_executes, insert_executes_generic, insert_executes_log: complete native insertion calls in 39 * (d + 1) + 16 instructions.
• member_dispatch_spec, member_call, member_executes, member_executes_generic, member_executes_log: complete native membership calls in 28 * (d + 1) + 18 instructions.
• successor_dispatch_spec, successor_call, successor_executes, successor_executes_generic, successor_executes_log: complete native strict-successor calls in 65 * (d + 1) + 22 instructions.
• instruction_bound, instruction_bound_log, client_spec, run_initialized: adaptive history execution and combined initialization-plus-client execution certificates.

References

• P. van Emde Boas, R. Kaas and E. Zijlstra, Design and implementation of an efficient priority queue
• E. Demaine, Divide and conquer: van Emde Boas trees, Lecture 4

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

The state after the twelve actual setup instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.setup_exec {w : ℕ} {s : WordRAM.Data 32} (hw : WordRAM.Fits w 5) : WordRAM.Exec w setup s (setupData s) 12

Constant and traversal setup has exactly twelve native instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.setup_insertEntry (s : WordRAM.Data 32) : InsertEntry (s.regs root) (s.regs arg) (setupData s)

Setup establishes insertion's entry registers from the caller's root and argument.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.setup_memberEntry (s : WordRAM.Data 32) : MemberEntry (s.regs root) (s.regs arg) (setupData s)

Setup establishes membership's entry registers from the caller's root and argument.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.setup_successorEntry (s : WordRAM.Data 32) : SuccessorEntry (s.regs stackBase) (s.regs stackBase) (s.regs root) (s.regs arg) (setupData s)

Setup establishes strict successor's entry registers from the caller's root, stack base, and argument.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.compiled_program_length : List.length (program.program out) = 213

The single compiled program contains 212 ordinary instructions and a final halt.

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

Compiling the fixed dispatcher introduces no word-width instruction.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.log_log_universeSize (d : ℕ) : Nat.log 2 (Nat.log 2 (Lean.VanEmdeBoas.universeSize d)) = d

The supported double-exponential universe has exactly d iterated binary logarithms.

Complete native insertion calls

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_dispatch_spec {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (ht : tree.Valid) (hr : Rep tree base s.mem) (hx : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = key) (htag : s.regs tag = 0) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w program s z (39 * (d + 1) + 15) ∧ Rep (tree.insert key) base z.mem ∧ z.regs out = 0 ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d ≤ a → z.mem a = s.mem a

A complete insertion dispatch (tag = 0), including setup and all control flow but not final halt, executes in at most 39 * (d + 1) + 15 instructions, updates the represented tree to tree.insert key, leaves out = 0, and preserves all memory outside [base, base + span d).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_call {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hx : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = key) (htag : s.regs tag = 0) : ∃ (z : WordRAM.Data 32) (n : ℕ), n + 1 ≤ 39 * (d + 1) + 16 ∧ WordRAM.Exec w program s z n ∧ WordRAM.Data.Bounded w z ∧ Rep (tree.insert key) base z.mem ∧ z.regs root = base ∧ z.regs stackBase = s.regs stackBase ∧ z.regs out = 0 ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d ≤ a → z.mem a = s.mem a

A bounded caller invoking insertion (tag = 0) obtains a bounded state representing tree.insert key, with unchanged persistent root and stackBase registers and all memory outside [base, base + span d) preserved.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_executes {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hx : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = key) (htag : s.regs tag = 0) : ∃ n ≤ 39 * (d + 1) + 16, WordRAM.Executes w (program.program out) { pc := 0, data := s } 0 n

Actual flat bounded-word insertion execution, including its final halt, in 39 * (d + 1) + 16 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_executes_generic {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hx : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = key) (htag : s.regs tag = 0) : ∃ n ≤ 39 * (d + 1) + 16, GenericRAM.Executes w (program.program out).toGeneric (WordRAM.State.toGeneric WordRAM.Basis.standard { pc := 0, data := s }) 0 n

Exact transfer of the flat insertion call into the shared generic RAM model.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.insert_executes_log {d w base key : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hx : key < Lean.VanEmdeBoas.universeSize d) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = key) (htag : s.regs tag = 0) : ∃ n ≤ 39 * (Nat.log 2 (Nat.log 2 (Lean.VanEmdeBoas.universeSize d)) + 1) + 16, WordRAM.Executes w (program.program out) { pc := 0, data := s } 0 n

The charged native insertion bound written directly in terms of the universe size.

Complete native membership calls

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_dispatch_spec {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = query) (htag : s.regs tag = 1) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w program s z (28 * (d + 1) + 17) ∧ (z.regs out = if tree.member query = true then 1 else 0) ∧ z.mem = s.mem

A complete membership dispatch, including setup and all control flow but not final halt. No query-universe restriction and no zero-filled outside-memory assumption are imposed.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_call {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = query) (htag : s.regs tag = 1) : ∃ (z : WordRAM.Data 32) (n : ℕ), n + 1 ≤ 28 * (d + 1) + 18 ∧ WordRAM.Exec w program s z n ∧ WordRAM.Data.Bounded w z ∧ Rep tree base z.mem ∧ z.regs root = base ∧ (z.regs out = if tree.member query = true then 1 else 0) ∧ z.mem = s.mem

A bounded caller obtains a bounded result, identical represented memory and an unchanged persistent root. Its query fits the machine word because every caller register does.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_executes {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = query) (htag : s.regs tag = 1) : ∃ n ≤ 28 * (d + 1) + 18, WordRAM.Executes w (program.program out) { pc := 0, data := s } (if tree.member query = true then 1 else 0) n

Actual flat bounded-word execution, including its final halt, in 28 (d+1) + 18 instructions. The selected fixed program has no depth or word-width parameter.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_executes_generic {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = query) (htag : s.regs tag = 1) : ∃ n ≤ 28 * (d + 1) + 18, GenericRAM.Executes w (program.program out).toGeneric (WordRAM.State.toGeneric WordRAM.Basis.standard { pc := 0, data := s }) (if tree.member query = true then 1 else 0) n

Exact transfer of the actual flat call into the shared generic RAM model; this adds no semantic operation or uncharged oracle instruction.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.member_executes_log {d w base query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (ha : WordRAM.Fits w (base + Lean.VanEmdeBoas.span d)) (hroot : s.regs root = base) (harg : s.regs arg = query) (htag : s.regs tag = 1) : ∃ n ≤ 28 * (Nat.log 2 (Nat.log 2 (Lean.VanEmdeBoas.universeSize d)) + 1) + 18, WordRAM.Executes w (program.program out) { pc := 0, data := s } (if tree.member query = true then 1 else 0) n

The charged native membership bound written directly in terms of the universe size.

Complete native strict-successor calls

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_dispatch_spec {d w base stackBase₀ query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (ht : tree.Valid) (hr : Rep tree base s.mem) (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (hroot : s.regs root = base) (hstk : s.regs stackBase = stackBase₀) (harg : s.regs arg = query) (htag : s.regs tag = 2) : ∃ (z : WordRAM.Data 32), WordRAM.ExecWithin w program s z (65 * (d + 1) + 21) ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ Rep tree base z.mem ∧ z.regs sp = stackBase₀ ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

A complete strict-successor dispatch (tag = 2), including setup, descent, and stack unwind but not final halt, executes in at most 65 * (d + 1) + 21 instructions, preserves the represented tree at base, restores sp = stackBase₀, and modifies no memory outside the 4 * d-word stack region [stackBase₀, stackBase₀ + 4 * d).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_call {d w base stackBase₀ query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (hroot : s.regs root = base) (hstk : s.regs stackBase = stackBase₀) (harg : s.regs arg = query) (htag : s.regs tag = 2) : ∃ (z : WordRAM.Data 32) (n : ℕ), n + 1 ≤ 65 * (d + 1) + 22 ∧ WordRAM.Exec w program s z n ∧ WordRAM.Data.Bounded w z ∧ Rep tree base z.mem ∧ z.regs root = base ∧ z.regs stackBase = stackBase₀ ∧ z.regs sp = stackBase₀ ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

A bounded caller invoking strict successor (tag = 2) obtains a bounded state with the exact optional successor encoded by (found, out), unchanged persistent root and stackBase registers, preserved tree representation, and unchanged memory outside [stackBase₀, stackBase₀ + 4 * d).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_executes {d w base stackBase₀ query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (hroot : s.regs root = base) (hstk : s.regs stackBase = stackBase₀) (harg : s.regs arg = query) (htag : s.regs tag = 2) : ∃ (z : WordRAM.Data 32), ∃ n ≤ 65 * (d + 1) + 22, WordRAM.Executes w (program.program out) { pc := 0, data := s } (z.regs out) n ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ Rep tree base z.mem ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

Actual flat bounded-word strict-successor execution, including its final halt, in 65 * (d + 1) + 22 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_executes_generic {d w base stackBase₀ query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (hroot : s.regs root = base) (hstk : s.regs stackBase = stackBase₀) (harg : s.regs arg = query) (htag : s.regs tag = 2) : ∃ (z : WordRAM.Data 32), ∃ n ≤ 65 * (d + 1) + 22, GenericRAM.Executes w (program.program out).toGeneric (WordRAM.State.toGeneric WordRAM.Basis.standard { pc := 0, data := s }) (z.regs out) n ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ Rep tree base z.mem ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

Exact transfer of the flat strict-successor call into the shared generic RAM model.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_executes_log {d w base stackBase₀ query : ℕ} {tree : Lean.VanEmdeBoas.Tree d} {s : WordRAM.Data 32} (hs : WordRAM.Data.Bounded w s) (ht : tree.Valid) (hr : Rep tree base s.mem) (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (hroot : s.regs root = base) (hstk : s.regs stackBase = stackBase₀) (harg : s.regs arg = query) (htag : s.regs tag = 2) : ∃ (z : WordRAM.Data 32), ∃ n ≤ 65 * (Nat.log 2 (Nat.log 2 (Lean.VanEmdeBoas.universeSize d)) + 1) + 22, WordRAM.Executes w (program.program out) { pc := 0, data := s } (z.regs out) n ∧ (if z.regs found = 0 then none else some (z.regs out)) = tree.successor query ∧ Rep tree base z.mem ∧ ∀ (a : ℕ), a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → z.mem a = s.mem a

The charged native strict-successor bound written directly in terms of the universe size.

Finite-set Stateful.Spec and DynamicCertificate realization

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.successor_eq_least {d : ℕ} {t : Lean.VanEmdeBoas.Tree d} (ht : t.Valid) (q : ℕ) : t.successor q = OrderedSet.least ({x ∈ t.elements | q < x})

Tree.successor on a valid tree computes the mathematical OrderedSet.least of the stored elements strictly greater than the query.

inductive Cslib.Algorithms.WordRAM.VanEmdeBoas.Operation : Type

Dynamic ordered-set operations supported by the van Emde Boas dispatcher.

• insert (key : ℕ) : Operation

  Insert a bounded universe key into the set.

• member (query : ℕ) : Operation

  Query whether a fitting word belongs to the set.

• successor (query : ℕ) : Operation

  Return the least stored key strictly greater than a fitting query, if any.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.instDecidableEqOperation.decEq (x✝ x✝¹ : Operation) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.VanEmdeBoas.instDecidableEqOperation : DecidableEq Operation

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.VanEmdeBoas.instReprOperation : Repr Operation

def Cslib.Algorithms.WordRAM.VanEmdeBoas.instReprOperation.repr : Operation → ℕ → Std.Format

def Cslib.Algorithms.WordRAM.VanEmdeBoas.Operation.Result : Operation → Type

Typed observation returned by each van Emde Boas operation.

def Cslib.Algorithms.WordRAM.VanEmdeBoas.spec (d w : ℕ) : Stateful.Spec

Abstract finite-set specification on the universe [0, universeSize d).

def Cslib.Algorithms.WordRAM.VanEmdeBoas.dynamicProgram (d w : ℕ) : WordRAM.DynamicProgram (spec d w) 32

The single fixed dispatcher program packaged as a DynamicProgram with a register-only calling convention (tag and arg).

structure Cslib.Algorithms.WordRAM.VanEmdeBoas.SetRep (d base stackBase₀ w : ℕ) (s : Finset ℕ) (x : WordRAM.Data 32) : Prop

Persistent machine representation of an abstract finite set s : Finset ℕ by a valid tree at base and scratch stack pointer at stackBase₀.

• bounded : WordRAM.Data.Bounded w x
• root_eq : x.regs root = base
• stackBase_eq : x.regs stackBase = stackBase₀
• tree : ∃ (t : Lean.VanEmdeBoas.Tree d), t.Valid ∧ t.elements = s ∧ Rep t base x.mem

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.arguments_fit {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) {s : Finset ℕ} (o : Operation) (ho : (spec d w).valid s o) (j : Fin 32) : WordRAM.Fits w ((dynamicProgram d w).encode o j)

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.dispatch_spec {d w base stackBase₀ : ℕ} {s : Finset ℕ} {x : WordRAM.Data 32} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) (o : Operation) (hx : SetRep d base stackBase₀ w s x) (ho : (spec d w).valid s o) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w program ((dynamicProgram d w).prepare o x) y (65 * (d + 1) + 21) ∧ (dynamicProgram d w).decode o y.regs = some ((spec d w).step s o).2 ∧ SetRep d base stackBase₀ w ((spec d w).step s o).1 y ∧ ∀ (a : ℕ), a < base ∨ base + Lean.VanEmdeBoas.span d ≤ a → a < stackBase₀ ∨ stackBase₀ + 4 * d ≤ a → y.mem a = x.mem a

Unified per-operation dispatch theorem for (dynamicProgram d w): every admissible operation executes in at most 65 * (d + 1) + 21 structured instructions, produces the decoded abstract observation, preserves SetRep, and modifies no memory outside [base, base + span d) ∪ [stackBase₀, stackBase₀ + 4 * d).

def Cslib.Algorithms.WordRAM.VanEmdeBoas.certificate {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) : WordRAM.DynamicCertificate (dynamicProgram d w) w

Semantic correctness and totality certificate for the fixed bounded-word van Emde Boas implementation.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.instruction_bound {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) : Stateful.Bound (certificate hstk_lo hstk_fit).realization WordRAM.DynamicProgram.OperationTrace.instructions fun (x : (spec d w).State) (x_1 : (spec d w).Op) => 65 * (d + 1) + 22

Separate worst-case per-operation instruction certificate, counting the final halt: every admissible insert, member, or successor call executes in at most 65 * (d + 1) + 22 instructions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.instruction_bound_log {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) : Stateful.Bound (certificate hstk_lo hstk_fit).realization WordRAM.DynamicProgram.OperationTrace.instructions fun (x : (spec d w).State) (x_1 : (spec d w).Op) => 65 * (Nat.log 2 (Nat.log 2 (Lean.VanEmdeBoas.universeSize d)) + 1) + 22

The per-operation instruction certificate written in terms of the universe size.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.execOp_frame {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) {s : Finset ℕ} {o : Operation} {x y : WordRAM.Data 32} {a : (spec d w).Result o} {trace : WordRAM.DynamicProgram.OperationTrace} (hx : SetRep d base stackBase₀ w s x) (ho : (spec d w).valid s o) (he : (dynamicProgram d w).ExecOp w x o a y trace) {j : ℕ} (hj_tree : j < base ∨ base + Lean.VanEmdeBoas.span d ≤ j) (hj_stk : j < stackBase₀ ∨ stackBase₀ + 4 * d ≤ j) : y.mem j = x.mem j

Every actual call preserves memory outside the tree region [base, base + span d) and the scratch stack [stackBase₀, stackBase₀ + 4 * d).

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.executes_client_frame {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) {α : Type} {p : (spec d w).Client α} {s : Finset ℕ} {x y : WordRAM.Data 32} {val : α} {traces : List WordRAM.DynamicProgram.OperationTrace} (hx : SetRep d base stackBase₀ w s x) (hv : (spec d w).ValidHistory s ((spec d w).runClient s p).2.2) (he : Stateful.Executes ((dynamicProgram d w).ExecOp w) p x val y traces) {j : ℕ} (hj_tree : j < base ∨ base + Lean.VanEmdeBoas.span d ≤ j) (hj_stk : j < stackBase₀ ∨ stackBase₀ + 4 * d ≤ j) : y.mem j = x.mem j

Every admissible adaptive client execution preserves memory outside the tree and stack regions across the entire interaction history.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.client_spec {d w base stackBase₀ : ℕ} (hstk_lo : base + Lean.VanEmdeBoas.span d ≤ stackBase₀) (hstk_fit : WordRAM.Fits w (stackBase₀ + 4 * d)) {α : Type} (p : (spec d w).Client α) {s : Finset ℕ} {x : WordRAM.Data 32} (hx : SetRep d base stackBase₀ w s x) (hv : (spec d w).ValidHistory s ((spec d w).runClient s p).2.2) : ∃ (y : WordRAM.Data 32) (traces : List WordRAM.DynamicProgram.OperationTrace), Stateful.Executes ((dynamicProgram d w).ExecOp w) p x ((spec d w).runClient s p).1 y traces ∧ SetRep d base stackBase₀ w ((spec d w).runClient s p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ ((spec d w).runClient s p).2.2.length * (65 * (d + 1) + 22) ∧ ∀ (j : ℕ), j < base ∨ base + Lean.VanEmdeBoas.span d ≤ j → j < stackBase₀ ∨ stackBase₀ + 4 * d ≤ j → y.mem j = x.mem j

Every admissible adaptive client has a concrete execution with the specified answers and final finite set, at most 65 * (d + 1) + 22 instructions per operation, and unchanged memory outside the tree and stack regions.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.run_initialized {d w base : ℕ} {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) {α : Type} (p : (spec d w).Client α) (hv : (spec d w).ValidHistory ∅ ((spec d w).runClient ∅ p).2.2) : ∃ (x₀ : WordRAM.Data 32) (n_init : ℕ) (y : WordRAM.Data 32) (traces : List WordRAM.DynamicProgram.OperationTrace), n_init + 1 ≤ 8 * Lean.VanEmdeBoas.span d + 20 * d + 25 ∧ WordRAM.Exec w initProgram s₀ x₀ n_init ∧ SetRep d base (base + Lean.VanEmdeBoas.span d) w ∅ x₀ ∧ Stateful.Executes ((dynamicProgram d w).ExecOp w) p x₀ ((spec d w).runClient ∅ p).1 y traces ∧ SetRep d base (base + Lean.VanEmdeBoas.span d) w ((spec d w).runClient ∅ p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ ((spec d w).runClient ∅ p).2.2.length * (65 * (d + 1) + 22) ∧ ∀ (j : ℕ), j < base ∨ base + Lean.VanEmdeBoas.span d + 4 * (d + 1) ≤ j → y.mem j = s₀.mem j

Combined native initialization and adaptive client execution: starting from any bounded machine state s₀ with s₀.regs root = base, s₀.regs depth = d, and Fits w (base + span d + 4 * (d + 1)) (with arbitrary initial memory), initProgram executes in at most 8 * span d + 20 * d + 25 instructions to produce an empty represented set x₀, from which any admissible adaptive client p executes to y with at most 65 * (d + 1) + 22 instructions per operation and no memory modified outside [base, base + span d + 4 * (d + 1)).