Order Maintenance in Worst-Case Constant Time, Verified

Denis Firsov

cs.LO Oct 28, 2026 · v1 cs.DS

Read PDF arXiv abstract Code

TL;DR

Verifies a worst-case constant-time order-maintenance algorithm in Lean 4. It uses a deeply embedded step-counting RAM, a verified compiler, and a word-size bound, about 78,000 lines in total.

Abstract

Order maintenance asks for a data structure that keeps a sequence of elements under insertions and deletions and tells which of two elements comes first. We give an algorithm, assembled from published components, that performs each operation in worst-case constant time, and verify it in Lean 4. The algorithm is a program for a random-access machine deeply embedded in Lean, whose interpreter counts every instruction. We prove that the program answers every query as a simple reference specification does, that each operation takes at most a fixed number of steps, independent of the number of elements and of the history, and that after $t$ operations no value it has computed has more than $O(\log t)$ bits, so it runs unchanged on a machine with words of that size. A verified translation that preserves step counts exactly connects the high-level proofs to the machine program, so the interpreter is the only cost model to trust. An unverified native implementation shows the algorithm's practical cost.

Problem

Order maintenance in worst-case O(1) time per operation has been known since 1987, but the published algorithms are intricate. None had been implemented, and no order-maintenance algorithm had been verified in a proof assistant.

Approach

An algorithm is assembled from published components (Dietz–Sleator, Bender et al., Kopelowitz) and adapted for proof. Every write is guarded, and top-tree labels are never changed in place. The algorithm is written as a program for a random-access machine deeply embedded in Lean 4, whose interpreter counts every instruction. A verified, step-count-preserving translation through an intermediate language links a functional Level F to the machine program (Level M).

Results

Lean proofs establish three things: answers match a reference list specification, each operation takes a fixed bounded number of steps, and after t operations stored values have O(log t) bits, so the program runs unchanged on a word RAM of that word size. An unverified native Rust implementation stays within a small factor of an AVL tree on insertions, and its cold queries are 2.2–6.3 times faster.

Workload	native (unverified)	AVL	amortized
Random insertion	1.00 / 5.3 / 12.1	0.77 / 5.5 / 7.2	0.54 / 12.3 / 15.3
Clustered insertion	0.085 / 2.9 / 6.3	0.030 / 3.2 / 3.6	0.022 / 3.4 / 5,050
Cold order query	0.93 / – / 1.4	5.9 / – / 8.4	0.50 / – / 0.88
Memory (bytes/element)	112	13	21

Selected measurements in μs (mean / 99.99th percentile / slowest repeatable time)

Papers With

Order Maintenance in Worst-Case Constant Time, Verified