Standalone Word-RAM Indexed Binary Min-Heap

This file proves the full SubroutineDS and PQPackage specifications for the standalone word-RAM indexed binary min-heap (Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pqCode) over Basis.exact, and projects it via Basis.Simulates.exactStandard to standalone .standard-basis DynamicProgram, DynamicCertificate, Stateful.Bound, and adaptive-client theorems.

The heap uses space n = 3 * n + 1 words at any base address base with Fits w (base + space n) and Fits w K_max:

• initFresh runs in O(1) (11 instructions);
• initClear runs in O(n) (12 * n + 21 instructions, derived generically via SubroutineDS);
• isEmpty and getKey run in O(1) worst-case instructions;
• insert, decreaseKey, and extractMin run in O(log n + 1) worst-case instructions with zero potential (potential = 0).

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Rep: concrete representation invariant.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.subroutineDS: exact-basis SubroutineDS certificate.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pkg: PQPackage .exact rBin bundle for black-box algorithm callers such as dijkstra_of_pq_spec.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.dynamicProgram, Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.certificate: standalone .standard-basis machine realization.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.instruction_bound: worst-case per-operation Stateful.Bound over Basis.standard.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.run_client_bound: worst-case total instruction bound for any adaptive Stateful.Client program.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

structure Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Rep (n w base : ℕ) (s : Lean.IndexedMinPQ.State n) (x : WordRAM.Data rBin) : Prop

Concrete representation invariant of the standalone binary heap at base on n handles.

• bounded : WordRAM.Data.Bounded w x

  All registers and memory cells fit in w-bit words.

• reg_base : x.regs Reg.baseReg = base

  Persistent base-address register baseReg = base.

• reg_n : x.regs Reg.nReg = n

  Persistent handle-count register nReg = n.

• reg_hb : x.regs Reg.hb = base + n

  Persistent heap-array base hb = base + n.

• reg_pb : x.regs Reg.pb = base + 2 * n + 1

  Persistent position-array base pb = base + 2 * n + 1.

• heap : HeapInv n base (x.regs Reg.sz) x.mem

  Structural and lexicographic binary-heap invariant on x.mem.

• state_eq : s = stateOfMem n base x.mem

  Abstract state s matches stateOfMem n base x.mem.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.tEmpty : ℕ → ℕ

Worst-case instruction bound for isEmpty.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.tGet : ℕ → ℕ

Worst-case instruction bound for getKey.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.tIns (n : ℕ) : ℕ

Worst-case instruction bound for insert.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.tDec (n : ℕ) : ℕ

Worst-case instruction bound for decreaseKey.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.tExt (n : ℕ) : ℕ

Worst-case instruction bound for extractMin.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.charge (n : ℕ) : Lean.IndexedMinPQ.Op n → ℕ

Per-operation worst-case instruction charge (excluding standalone trailing halt).

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.subroutineDS {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) : WordRAM.SubroutineDS pqCode.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)

Exact-basis SubroutineDS certificate for the standalone binary min-heap.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pkg : PQPackage WordRAM.Basis.exact rBin

Packaged PQPackage .exact rBin for plug-and-play subroutine callers (dijkstra_of_pq_spec).

Standalone .standard-Basis Word-RAM Realization and Worst-Case Bounds

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.dynamicProgram (n K_max : ℕ) : WordRAM.DynamicProgram (Lean.IndexedMinPQ.spec n K_max) rBin

Standalone .standard-basis DynamicProgram serving IndexedMinPQ.spec n K_max.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.certificate {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) : WordRAM.DynamicCertificate (dynamicProgram n K_max) w

Standalone .standard-basis DynamicCertificate for the binary min-heap.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.instruction_bound {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) : Stateful.Bound (certificate hS hK).realization WordRAM.DynamicProgram.OperationTrace.instructions fun (x : (Lean.IndexedMinPQ.spec n K_max).State) (o : (Lean.IndexedMinPQ.spec n K_max).Op) => charge n o + 1

Standalone worst-case per-operation bound for the word-RAM binary min-heap over Basis.standard (charge n o + 1 instructions including the trailing halt).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.run_client_bound {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) {α : Type u_1} (p : (Lean.IndexedMinPQ.spec n K_max).Client α) {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rBin} (hr : Rep n w base s x) (hv : (Lean.IndexedMinPQ.spec n K_max).ValidHistory s ((Lean.IndexedMinPQ.spec n K_max).runClient s p).2.2) : ∃ (y : WordRAM.Data rBin) (traces : List WordRAM.DynamicProgram.OperationTrace), Stateful.Executes ((dynamicProgram n K_max).ExecOp w) p x ((Lean.IndexedMinPQ.spec n K_max).runClient s p).1 y traces ∧ Rep n w base ((Lean.IndexedMinPQ.spec n K_max).runClient s p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ (Lean.IndexedMinPQ.spec n K_max).totalCost (fun (x : (Lean.IndexedMinPQ.spec n K_max).State) (o : (Lean.IndexedMinPQ.spec n K_max).Op) => charge n o + 1) s ((Lean.IndexedMinPQ.spec n K_max).runClient s p).2.2

Standalone adaptive-client bound for the word-RAM binary min-heap over Basis.standard.