Indexed Binary Min-Heap: Memory Model and Invariant

This file defines the flat memory layout and structural/ordering invariants of the standalone word-RAM indexed binary min-heap on N handles 0, …, N - 1 placed at base address base with footprint space N = 3 * N + 1:

• mem (base + v) (v < N): current key of handle v (arbitrary word in 0 .. K_max, including 0).
• mem (base + N + i) (1 ≤ i ≤ sz): handle stored at 1-based heap position i (base + N is unused).
• mem (base + 2 * N + 1 + v) (v < N): 1-based heap position of handle v, or 0 when v is absent from the priority queue.

Heap entries are ordered by Cslib.Algorithms.Lean.IndexedMinPQ.PrioLE on (handle, key), breaking equal-key ties toward smaller handle indices so extractMin deterministically implements Cslib.Algorithms.Lean.IndexedMinPQ.findMin.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.space: footprint size 3 * N + 1.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.stateOfMem: abstract IndexedMinPQ.State N represented in memory.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape, Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv: structural and lexicographic heap invariants.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.UpOrdered, Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.DownOrdered: single-defect invariants during siftUp and siftDown.

References

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

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.space (N : ℕ) : ℕ

Memory footprint size (3 * N + 1 words) of an indexed binary heap over N handles.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.space_lower (N : ℕ) : N + 1 ≤ space N

The binary-heap footprint on N handles is at least N + 1 words.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.entryLE_of_key_le {u k₁ k₂ : ℕ} (h : k₁ ≤ k₂) : Lean.IndexedMinPQ.RawPrioLE (u, k₁) (u, k₂)

Decreasing a handle's key improves its priority under IndexedMinPQ.RawPrioLE.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.heapEntry (N base : ℕ) (mem : ℕ → ℕ) (i : ℕ) : ℕ × ℕ

The (handle, key) pair stored at 1-based heap position i.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.stateOfMem (N base : ℕ) (mem : ℕ → ℕ) : Lean.IndexedMinPQ.State N

Abstract IndexedMinPQ.State N decoded from the key and pos arrays at base.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.stateOfMem_congr {N base : ℕ} {m₁ m₂ : ℕ → ℕ} (h : ∀ a ∈ { base := base, length := space N }.footprint, m₁ a = m₂ a) : stateOfMem N base m₁ = stateOfMem N base m₂

stateOfMem depends only on memory cells inside (Block.mk base (space N)).footprint.

structure Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape (N base sz : ℕ) (mem : ℕ → ℕ) : Prop

Structural binary-heap invariant: positions 1, …, sz store handles < N, and the pos array at base + 2 * N + 1 is the partial inverse of heap at base + N.

• size_le : sz ≤ N

  Heap size never exceeds N.

• vertex_lt (i : ℕ) : 1 ≤ i → i ≤ sz → mem (base + N + i) < N

  Every occupied heap slot holds a valid handle < N.

• pos_vertex (i : ℕ) : 1 ≤ i → i ≤ sz → mem (base + 2 * N + 1 + mem (base + N + i)) = i

  pos[heap[i]] = i for 1 ≤ i ≤ sz.

• pos_le (v : ℕ) : v < N → mem (base + 2 * N + 1 + v) ≤ sz

  Every handle's position is at most sz.

• vertex_pos (v : ℕ) : v < N → mem (base + 2 * N + 1 + v) ≠ 0 → mem (base + N + mem (base + 2 * N + 1 + v)) = v

  Every handle with nonzero position p sits at heap[p].

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Ordered (f : ℕ → ℕ × ℕ) (sz : ℕ) : Prop

Heap order under IndexedMinPQ.RawPrioLE: every child 2 ≤ i ≤ sz has priority at least that of its parent i / 2.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.UpOrdered (f : ℕ → ℕ × ℕ) (sz k : ℕ) : Prop

Heap order except possibly between k and its parent k / 2 (siftUp invariant).

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.DownOrdered (f : ℕ → ℕ × ℕ) (sz k : ℕ) : Prop

Heap order except possibly between k and its children (siftDown invariant).

structure Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv (N base sz : ℕ) (mem : ℕ → ℕ) extends Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape N base sz mem : Prop

Full binary-heap invariant: structural bijection plus lexicographic heap order.

• size_le : sz ≤ N
• vertex_lt (i : ℕ) : 1 ≤ i → i ≤ sz → mem (base + N + i) < N
• pos_vertex (i : ℕ) : 1 ≤ i → i ≤ sz → mem (base + 2 * N + 1 + mem (base + N + i)) = i
• pos_le (v : ℕ) : v < N → mem (base + 2 * N + 1 + v) ≤ sz
• vertex_pos (v : ℕ) : v < N → mem (base + 2 * N + 1 + v) ≠ 0 → mem (base + N + mem (base + 2 * N + 1 + v)) = v
• ordered : Ordered (heapEntry N base mem) sz

  Lexicographic min-heap order on (handle, key).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.congr_mem {N base S : ℕ} {mem m₂ : ℕ → ℕ} (h : HeapInv N base S mem) (hm : ∀ a ∈ { base := base, length := space N }.footprint, m₂ a = mem a) : HeapInv N base S m₂

HeapInv depends only on memory cells inside (Block.mk base (space N)).footprint.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape.size_lt {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapShape N base S mem) {v : ℕ} (hv : v < N) (hp : mem (base + 2 * N + 1 + v) = 0) : S < N

A heap missing handle v < N has size strictly below N.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape.stateOfMem_zero {N base : ℕ} {mem : ℕ → ℕ} (h : HeapShape N base 0 mem) : stateOfMem N base mem = Lean.IndexedMinPQ.empty N

When sz = 0, the represented IndexedMinPQ.State N is empty N.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapShape.size_eq_zero_iff {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapShape N base S mem) : S = 0 ↔ Lean.IndexedMinPQ.dom (stateOfMem N base mem) = ∅

Size S = 0 iff the represented dom is empty.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.findMin_eq_root {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapInv N base S mem) (hS : 1 ≤ S) : Lean.IndexedMinPQ.findMin (stateOfMem N base mem) = some (⟨mem (base + N + 1), ⋯⟩, mem (base + mem (base + N + 1)))

Root optimality: the root at position 1 has lexicographically minimum (handle, key) among all handles present in the heap, so IndexedMinPQ.findMin equals the root entry.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.push {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapInv N base S mem) {v c : ℕ} (hv : v < N) (hp : mem (base + 2 * N + 1 + v) = 0) : have m' := Function.update (Function.update (Function.update mem (base + v) c) (base + N + (S + 1)) v) (base + 2 * N + 1 + v) (S + 1); HeapShape N base (S + 1) m' ∧ UpOrdered (heapEntry N base m') (S + 1) (S + 1)

Insertion: storing key c for an absent handle v < N and appending v at S + 1 produces HeapShape and UpOrdered at S + 1.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.decrease {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapInv N base S mem) {v c : ℕ} (hv : v < N) (_hp : mem (base + 2 * N + 1 + v) ≠ 0) (hle : c ≤ mem (base + v)) : have m' := Function.update mem (base + v) c; HeapShape N base S m' ∧ UpOrdered (heapEntry N base m') S (mem (base + 2 * N + 1 + v))

Decrease-key: lowering the key of a present handle v < N from mem (base + v) to c produces HeapShape and UpOrdered at pos[v].

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.extract {N base S : ℕ} {mem : ℕ → ℕ} (h : HeapInv N base S mem) (hS : 2 ≤ S) : have m' := Function.update (Function.update (Function.update mem (base + 2 * N + 1 + mem (base + N + 1)) 0) (base + N + 1) (mem (base + N + S))) (base + 2 * N + 1 + mem (base + N + S)) 1; HeapShape N base (S - 1) m' ∧ DownOrdered (heapEntry N base m') (S - 1) 1 ∧ ∀ v < N, m' (base + 2 * N + 1 + v) = 0 ↔ mem (base + 2 * N + 1 + v) = 0 ∨ v = mem (base + N + 1)

Root removal (2 ≤ S): clearing the root's position and moving the last entry to 1 produces HeapShape of size S - 1 and DownOrdered at 1.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.HeapInv.extract_one {N base : ℕ} {mem : ℕ → ℕ} (h : HeapInv N base 1 mem) : HeapInv N base 0 (Function.update mem (base + 2 * N + 1 + mem (base + N + 1)) 0)

Singleton root removal: clearing the root's position on a 1-element heap leaves the empty heap invariant.