Fixed native word-RAM van Emde Boas code

The same thirty-two-register structured program dispatches insertion, membership and strict successor. It uses only standard unsigned integer operations, comparisons, loads and stores. The split size and child span are read from the represented memory; no code is generated from the depth, key or word width.

The minimum is stored outside recursive clusters, following Demaine's exposition. The lecture notes credit Michael Bender. The five-word contiguous records and explicit four-word successor return stack are engineering choices, distinguished from the original stratified representation of van Emde Boas, Kaas and Zijlstra.

These definitions alone establish no operation's correctness, execution bound, initialization or space use. Each certified operation must supply actual execution and representation proofs. In particular, a fitting query word may exceed the tree universe; membership rejects queries above the cached maximum before computing a descendant address.

Main definitions

• program: one fixed dispatch over native instructions.
• memberBody, memberLoop: membership descent with a cached-maximum rejection.
• insertBody, insertLoop: native insertion descent.
• successorDescentBody, successorDescent, successorUnwindBody, successorUnwind: native strict-successor descent and return-stack unwinding.

Main results

• program_size: the fixed dispatch has 212 instructions before halt.
• program_not_readsWidth: no instruction reads the selected word width.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.tag : Fin 32

Caller-supplied operation tag: insertion = 0, membership = 1, successor = 2.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.arg : Fin 32

Caller-supplied key or query word.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.out : Fin 32

Returned key or Boolean membership word.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.found : Fin 32

Presence flag distinguishing a successor from absence.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.root : Fin 32

Persistent base address of the represented tree.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.stackBase : Fin 32

Persistent base address of the reserved return stack.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.depth : Fin 32

Reserved register for initialization depth; the dispatch program does not read it.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.tableBase : Fin 32

Reserved register for initialization metadata; the dispatch program does not read it.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.zero : Fin 32

Register holding zero after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.one : Fin 32

Register holding one after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.two : Fin 32

Register holding two after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.three : Fin 32

Register holding three after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.four : Fin 32

Register holding four after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.five : Fin 32

Register holding the five-word header size after setup.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.p : Fin 32

Current subtree address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.x : Fin 32

Current local query or inserted key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.q : Fin 32

Current node's stored split size.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.t : Fin 32

Current node's stored child span.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.high : Fin 32

High part of the current key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.low : Fin 32

Low part of the current key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.child : Fin 32

Computed child address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.addr : Fin 32

Scratch address for indexed memory operations.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.present : Fin 32

Cached presence flag read from the current record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.mn : Fin 32

Cached minimum read from a record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.mx : Fin 32

Cached maximum read from a record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.tmp : Fin 32

Scratch arithmetic register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.sp : Fin 32

Return-stack cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.runFlag : Fin 32

Whether the descent loop continues.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.kind : Fin 32

Return-frame tag: cluster = 0, summary = 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.payload : Fin 32

Return-frame payload: cluster offset or parent address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.frameQ : Fin 32

Split size loaded from a return frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.VanEmdeBoas.frameT : Fin 32

Child span loaded from a return frame.

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

Initialize constants, traversal, result and stack registers in twelve instructions.

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

Split the key and compute its cluster address using six arithmetic instructions.

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

Return the cached minimum and stop descent.

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

Return the cached maximum and stop descent.

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

Return absence and stop descent.

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

One native insertion iteration. Empty records and empty destination clusters install their first key directly in the three-word bounds area.

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

Native insertion descent.

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

One native membership iteration. The maximum check rejects large queries before descent.

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

Native membership descent, with one depth decrease for each continuing iteration.

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

Push four words: continuation kind, payload, split and child span.

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

Save a cluster-return continuation and descend into the selected cluster.

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

Save a summary-return continuation and descend into the summary.

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

One native successor-descent iteration. The cached maximum chooses between early termination, cluster descent and summary descent.

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

Native successor descent.

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

Pop the four-word return frame.

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

One native successor-unwind iteration.

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

Reconstruct the answer through cluster and summary return frames.

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

One fixed dispatch program, independent of the universe, query, state and word width.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.program_size : program.size = 212

The fixed dispatch has 212 instructions before the final compiled halt.

theorem Cslib.Algorithms.WordRAM.VanEmdeBoas.program_not_readsWidth : ¬program.ReadsWidth

The dispatch never reads the selected word width.