Static-array Word-RAM Fibonacci heap

This file assembles the standalone static-array Word-RAM Fibonacci heap Fredman and Tarjan Cormen et al., Chapter 19 over Cslib.WordRAM.Basis.exact (and lifted to Basis.standard) for Cslib.Algorithms.Lean.IndexedMinPQ.spec.

Over n vertex handles in a contiguous memory block [base, base + 9 * n + 1) with concrete integer potential potential x = 80 * (numRoots + 2 * numMarked) (initPotential = 0, Fredman and Tarjan, Section 2, p. 604 (the potential defined before Theorem 1); Cormen et al., Section 19.1, eq. (19.1)):

• initFresh initializes an empty heap on zeroed [base, base + 9 * n + 1) in O(1) (≤ 26) instructions;
• initClear initializes an empty heap on arbitrary dirty [base, base + 9 * n + 1) in O(n) (≤ 36 * n + 36) instructions;
• isEmpty and getKey run in O(1) worst-case time (≤ 12 and ≤ 16 instructions);
• insert and decreaseKey (with cascading cuts) run in O(1) amortized time (≤ 130 and ≤ 340 instructions);
• extractMin (with degree-table consolidation and deterministic lexicographic (key, handle) tie-breaking) runs in O(log n) amortized time (≤ 420 * (Nat.log 2 n + 1) instructions).

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.subroutineDS: SubroutineDS certificate over Basis.exact.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.pkg, pkgStd: PQPackage bundles over Basis.exact and Basis.standard for plug-and-play graph algorithms (such as Dijkstra).
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initFreshProg, initClearProg, opProg, initRegs, prepareRegs, RunsOps: compiled flat Program .exact rFib artifacts, register calling conventions, and sequential execution predicate for standalone multi-operation execution.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.amortized, run_client_amortized: standalone Stateful.Amortized certificate and adaptive-client bound over Basis.standard.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.run_ops_exact_fresh, run_ops_exact_reusable: standalone end-to-end Basis.exact flat-program execution theorems bounding initialization by t_init + 1 ≤ 421 (initFreshProg on zeroed memory) or t_init + 1 ≤ 421 * (n + 1) (initClearProg on arbitrary memory) and total operation instructions for m_q queries, m_ins insertions, m_dec key decreases, and m_ext minimum extractions by t_ops ≤ 421 * (m_q + m_ins + m_dec + m_ext * (Nat.log 2 n + 1)).

References

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, Section 2, Lemma 1, Corollary 1, and Theorem 1 (p. 604).
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Section 19.1, eq. (19.1), and Sections 19.2–19.4.

Unified dispatcher

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.dispatchCode_exec {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (o : Lean.IndexedMinPQ.Op n) (hinv : FibInv n K_max w base s x) (hval : (Lean.IndexedMinPQ.spec n K_max).valid s o) (harg : code.argMatch o x.regs) : ∃ (y : WordRAM.Data rFib) (m : ℕ), WordRAM.Exec w dispatchCode x y m ∧ code.decode o y.regs = some ((Lean.IndexedMinPQ.spec n K_max).step s o).2 ∧ FibInv n K_max w base ((Lean.IndexedMinPQ.spec n K_max).step s o).1 y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ m + potential y ≤ charge n s o + potential x

Unified dispatcher dispatchCode implements all five IndexedMinPQ operations within charge n s o amortized instructions over Basis.exact.

SubroutineDS certificate and PQPackage bundles

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

Unified standalone and inline-subroutine specification/resource certificate for FibonacciHeap over Basis.exact.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.pkg : PQPackage WordRAM.Basis.exact rFib

Parametric PQPackage .exact rFib bundle for plug-and-play graph algorithms over Basis.exact.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.pkgStd : PQPackage WordRAM.Basis.standard rFib

Parametric PQPackage .standard rFib bundle lifted to Basis.standard.

Standalone Basis.standard DynamicProgram and Stateful.Amortized realizations

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.dynamicProgram {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) : WordRAM.DynamicProgram (Lean.IndexedMinPQ.spec n K_max) rFib

Standalone DynamicProgram realization of FibonacciHeap over Basis.standard.

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

Standalone DynamicCertificate for FibonacciHeap over Basis.standard.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.amortized {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) : Stateful.Amortized (certificate hS hK).realization WordRAM.DynamicProgram.OperationTrace.instructions (fun (x : (Lean.IndexedMinPQ.spec n K_max).State) (x_1 : WordRAM.Data rFib) => potential x_1) fun (s : (Lean.IndexedMinPQ.spec n K_max).State) (o : (Lean.IndexedMinPQ.spec n K_max).Op) => charge n s o + 1

Standalone Stateful.Amortized certificate for FibonacciHeap over Basis.standard, charging + 1 per operation for the trailing halt instruction.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.run_client_amortized {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 rFib} (hr : FibInv n K_max 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 rFib) (traces : List WordRAM.DynamicProgram.OperationTrace), Stateful.Executes ((dynamicProgram hS hK).ExecOp w) p x ((Lean.IndexedMinPQ.spec n K_max).runClient s p).1 y traces ∧ FibInv n K_max w base ((Lean.IndexedMinPQ.spec n K_max).runClient s p).2.1 y ∧ Stateful.total WordRAM.DynamicProgram.OperationTrace.instructions traces + potential y ≤ (Lean.IndexedMinPQ.spec n K_max).totalCost (fun (s : (Lean.IndexedMinPQ.spec n K_max).State) (o : (Lean.IndexedMinPQ.spec n K_max).Op) => charge n s o + 1) s ((Lean.IndexedMinPQ.spec n K_max).runClient s p).2.2 + potential x

Adaptive-client amortized execution bound for any admissible IndexedMinPQ client p over Basis.standard.

Standalone end-to-end Basis.exact flat-program operation-sequence theorems

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initFreshProg : WordRAM.Program WordRAM.Basis.exact rFib

Compiled flat Program .exact rFib for O(1) fresh zeroed-memory initialization.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initClearProg : WordRAM.Program WordRAM.Basis.exact rFib

Compiled flat Program .exact rFib for O(n) dirty-memory reusable initialization.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.opProg : WordRAM.Program WordRAM.Basis.exact rFib

Compiled flat Program .exact rFib serving all five priority-queue operations.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initRegs (n base : ℕ) : Fin rFib → ℕ

Initial register assignment supplying n in nReg (R[0]), base in frontierReg (R[1]), and 0 elsewhere.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.prepareRegs {n : ℕ} (o : Lean.IndexedMinPQ.Op n) (regs : Fin rFib → ℕ) : Fin rFib → ℕ

Deliver operation o's 3-bit tag into tag2..tag0 (R[17..19]) and its handle/key arguments into argV, argK (R[20..21]), leaving all other registers unchanged.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numQueries {n : ℕ} : List (Lean.IndexedMinPQ.Op n) → ℕ

Count isEmpty and getKey queries in an operation sequence.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numInserts {n : ℕ} : List (Lean.IndexedMinPQ.Op n) → ℕ

Count insert operations in an operation sequence.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numDecreaseKeys {n : ℕ} : List (Lean.IndexedMinPQ.Op n) → ℕ

Count decreaseKey operations in an operation sequence.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.numExtractMins {n : ℕ} : List (Lean.IndexedMinPQ.Op n) → ℕ

Count extractMin operations in an operation sequence.

inductive Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.RunsOps {n K_max : ℕ} (w base : ℕ) : Lean.IndexedMinPQ.State n → WordRAM.Data rFib → List (Lean.IndexedMinPQ.Op n) → WordRAM.Data rFib → ℕ → Prop

Sequential flat-program execution of ops by repeated calls to opProg: each call prepares input registers via prepareRegs, runs opProg from pc = 0 to halt, decodes the exact IndexedMinPQ result, modifies memory only within [base, base + space n), and accumulates total instructions executed (each final halt included).

• nil {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} : RunsOps w base s x [] x 0
• cons {n K_max w base : ℕ} {s : (Lean.IndexedMinPQ.spec n K_max).State} {x : WordRAM.Data rFib} {o : Lean.IndexedMinPQ.Op n} {ops : List (Lean.IndexedMinPQ.Op n)} {pc : ℕ} {y z : WordRAM.Data rFib} {steps rest : ℕ} : WordRAM.Runs w opProg { pc := 0, data := { regs := prepareRegs o x.regs, mem := x.mem } } { pc := pc, data := y } steps → (∃ (out : ℕ), WordRAM.step w opProg { pc := pc, data := y } = WordRAM.Outcome.halt out) → code.decode o y.regs = some ((Lean.IndexedMinPQ.spec n K_max).step s o).2 → WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem → RunsOps w base ((Lean.IndexedMinPQ.spec n K_max).step s o).1 y ops z rest → RunsOps w base s x (o :: ops) z (steps + 1 + rest)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.run_ops_exact_fresh {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) {mem₀ : ℕ → ℕ} (hmem : ∀ (a : ℕ), WordRAM.Fits w (mem₀ a)) (hzero : ∀ a ∈ { base := base, length := space n }.footprint, mem₀ a = 0) (ops : List (Lean.IndexedMinPQ.Op n)) (hv : (Lean.IndexedMinPQ.spec n K_max).ValidHistory (Lean.IndexedMinPQ.empty n) ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data rFib) (t_init : ℕ) (z : WordRAM.Data rFib) (t_ops : ℕ), WordRAM.Runs w initFreshProg { pc := 0, data := { regs := initRegs n base, mem := mem₀ } } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w initFreshProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := space n }.footprint mem₀ x₀.mem ∧ RunsOps w base (Lean.IndexedMinPQ.empty n) x₀ ops z t_ops ∧ t_init + 1 ≤ 421 ∧ t_ops ≤ 421 * (numQueries ops + numInserts ops + numDecreaseKeys ops + numExtractMins ops * (Nat.log 2 n + 1))

Standalone Basis.exact operation-sequence theorem with O(1) fresh initialization on zeroed [base, base + 9 * n + 1).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.run_ops_exact_reusable {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + space n)) (hK : WordRAM.Fits w K_max) {mem₀ : ℕ → ℕ} (hmem : ∀ (a : ℕ), WordRAM.Fits w (mem₀ a)) (ops : List (Lean.IndexedMinPQ.Op n)) (hv : (Lean.IndexedMinPQ.spec n K_max).ValidHistory (Lean.IndexedMinPQ.empty n) ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data rFib) (t_init : ℕ) (z : WordRAM.Data rFib) (t_ops : ℕ), WordRAM.Runs w initClearProg { pc := 0, data := { regs := initRegs n base, mem := mem₀ } } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w initClearProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := space n }.footprint mem₀ x₀.mem ∧ RunsOps w base (Lean.IndexedMinPQ.empty n) x₀ ops z t_ops ∧ t_init + 1 ≤ 421 * (n + 1) ∧ t_ops ≤ 421 * (numQueries ops + numInserts ops + numDecreaseKeys ops + numExtractMins ops * (Nat.log 2 n + 1))

Standalone Basis.exact operation-sequence theorem with O(n) reusable initialization on arbitrary w-bounded memory mem₀.