Documentation

Complexity.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Sift

Indexed Binary Min-Heap: Sift-Up, Sift-Down, and Root Extraction Proofs #

This file proves functional correctness, framing, and O(⌊log₂ n⌋ + 1) exact-basis instruction bounds for siftUp, siftDown, and doExtractNonEmpty under the lexicographic priority order IndexedMinPQ.PrioLE.

Main results #

References #

Sift-up #

source
theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftUp_spec {N base S w K : ℕ} {x : WordRAM.Data rBin} (hzero : x.regs Reg.zero = 0) (hone : x.regs Reg.one = 1) (hbase : x.regs Reg.baseReg = base) (hhb : x.regs Reg.hb = base + N) (hpb : x.regs Reg.pb = base + 2 * N + 1) (hk : x.regs Reg.k = K) (hK : 1 ≤ K) (hKS : K ≤ S) (hfit : WordRAM.Fits w (base + space N)) (hshape : HeapShape N base S x.mem) (hord : UpOrdered (heapEntry N base x.mem) S K) :
∃ (y : WordRAM.Data rBin), WordRAM.ExecWithin w siftUp x y (28 * Nat.log 2 K + 2) ∧ (∀ i ∉ [Reg.k, Reg.p, Reg.vk, Reg.vp, Reg.dk, Reg.dp, Reg.t], y.regs i = x.regs i) ∧ HeapInv N base S y.mem ∧ (∀ v < N, y.mem (base + 2 * N + 1 + v) = 0 ↔ x.mem (base + 2 * N + 1 + v) = 0) ∧ ∀ (a : ℕ), a ≤ base + N ∨ base + 3 * N < a → y.mem a = x.mem a

Sift-up repairs a single upward defect at K in 28 ⌊log₂ K⌋ + 2 instructions.

Sift-down and Root Extraction #

source
theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDown_spec {N base S w K : ℕ} {x : WordRAM.Data rBin} (hzero : x.regs Reg.zero = 0) (hone : x.regs Reg.one = 1) (hbase : x.regs Reg.baseReg = base) (hhb : x.regs Reg.hb = base + N) (hpb : x.regs Reg.pb = base + 2 * N + 1) (hsz : x.regs Reg.sz = S) (hk : x.regs Reg.k = K) (hK : 1 ≤ K) (hKS : K ≤ S) (hfit : WordRAM.Fits w (base + space N)) (hshape : HeapShape N base S x.mem) (hord : DownOrdered (heapEntry N base x.mem) S K) :
∃ (y : WordRAM.Data rBin), WordRAM.ExecWithin w siftDown x y (46 * Nat.log 2 (S + 1) + 4) ∧ (∀ i ∉ [Reg.k, Reg.p, Reg.vk, Reg.vp, Reg.dk, Reg.dp, Reg.t, Reg.l, Reg.szp], y.regs i = x.regs i) ∧ HeapInv N base S y.mem ∧ (∀ v < N, y.mem (base + 2 * N + 1 + v) = 0 ↔ x.mem (base + 2 * N + 1 + v) = 0) ∧ ∀ (a : ℕ), a ≤ base + N ∨ base + 3 * N < a → y.mem a = x.mem a

Sift-down repairs a single downward defect at K in 46 ⌊log₂ (S + 1)⌋ + 4 instructions.

source
theorem Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doExtractNonEmpty_spec {N base S w : ℕ} {x : WordRAM.Data rBin} (hzero : x.regs Reg.zero = 0) (hone : x.regs Reg.one = 1) (hbase : x.regs Reg.baseReg = base) (hhb : x.regs Reg.hb = base + N) (hpb : x.regs Reg.pb = base + 2 * N + 1) (hsz : x.regs Reg.sz = S) (hS : 1 ≤ S) (hfit : WordRAM.Fits w (base + space N)) (hheap : HeapInv N base S x.mem) :
∃ (y : WordRAM.Data rBin), WordRAM.ExecWithin w doExtractNonEmpty x y (46 * Nat.log 2 S + 20) ∧ (∀ i ∉ [Reg.outFlag, Reg.outV, Reg.outK, Reg.t, Reg.vk, Reg.sz, Reg.k, Reg.p, Reg.vp, Reg.dk, Reg.dp, Reg.l, Reg.szp], y.regs i = x.regs i) ∧ y.regs Reg.outFlag = 1 ∧ y.regs Reg.outV = x.mem (base + N + 1) ∧ y.regs Reg.outK = x.mem (base + x.mem (base + N + 1)) ∧ y.regs Reg.sz = S - 1 ∧ HeapInv N base (S - 1) y.mem ∧ (∀ v < N, y.mem (base + 2 * N + 1 + v) = 0 ↔ x.mem (base + 2 * N + 1 + v) = 0 ∨ v = x.mem (base + N + 1)) ∧ ∀ (a : ℕ), a ≤ base + N ∨ base + 3 * N < a → y.mem a = x.mem a

Non-empty root extraction runs in 46 ⌊log₂ S⌋ + 20 instructions, sets (outFlag, outV, outK) = (1, U, key[U]), and removes U while preserving HeapInv and all keys.