Fibonacci Heap: Shared Primitives, Initialization, Queries, and Insertion

This file proves the exact-Word-RAM specifications for:

• shared primitives (prioLTFlag, insertIntoNonEmptyList, addRootAndUpdateMin) reused across insert, decreaseKey, and extractMin;
• allocSpan, initSetup, and incCur (O(1) fresh initialization on zeroed memory);
• isEmptyCode, getKeyCode, and insertCode.

Main definitions

• Shared code fragments are defined in Complexity/Algorithms/WordRAM/PriorityQueue/FibonacciHeap/Program.lean and verified here against FibInv.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.prioLTFlag_exec, insertIntoNonEmptyList_exec, addRootAndUpdateMin_exec: shared list and priority primitives.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.allocSpan_exec, initSetup_exec, incCur_eval: initialization specifications for SubroutineDS.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.isEmptyCode_exec, getKeyCode_exec, insertCode_exec: O(1) query and amortized insertion specifications.

References

• M. L. Fredman and R. E. Tarjan, Fibonacci Heaps and Their Uses in Improved Network Optimization Algorithms
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 19

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.owns_arr_addr {n base k idx : ℕ} (hk : k < 8) (hidx : idx < n) : base ≤ base + k * n + idx ∧ base + k * n + idx < base + space n

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.owns_cons_addr {n base d : ℕ} (hd : d ≤ n) : base ≤ base + 8 * n + d ∧ base + 8 * n + d < base + space n

Shared primitives: prioLTFlag, insertIntoNonEmptyList, addRootAndUpdateMin

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.prioLTFlag_exec {n base w : ℕ} {x : WordRAM.Data rFib} (hbr : BaseRegs n base x) (uReg kuReg vReg kvReg flagReg : Fin rFib) : let ltProp := x.regs kuReg < x.regs kvReg ∨ x.regs kuReg = x.regs kvReg ∧ x.regs uReg < x.regs vReg; have bval := if ltProp then 1 else 0; WordRAM.ExecWithin w (prioLTFlag uReg kuReg vReg kvReg flagReg) x (x.set flagReg bval) 6

prioLTFlag uReg kuReg vReg kvReg flagReg sets flagReg ← 1 iff (u, ku) strictly precedes (v, kv) under IndexedMinPQ.PrioLT, and 0 otherwise, within 6 instructions.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.prioLTFlag_preserves {r uReg kuReg vReg kvReg flagReg : Fin rFib} (hf : r ≠ flagReg) : WordRAM.Code.Preserves r (prioLTFlag uReg kuReg vReg kvReg flagReg)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.insertIntoNonEmptyList_preserves {r hReg uReg : Fin rFib} (h0 : r ≠ s0) (h2 : r ≠ s2) : WordRAM.Code.Preserves r (insertIntoNonEmptyList hReg uReg)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.insertIntoNonEmptyList_exec {n base w : ℕ} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) {hReg uReg : Fin rFib} (hh0 : hReg ≠ s0) (hh2 : hReg ≠ s2) (hu0 : uReg ≠ s0) (hu2 : uReg ≠ s2) {h u : Fin n} {tail : List (Fin n)} (hh_val : x.regs hReg = ↑h) (hu_val : x.regs uReg = ↑u) (hcirc : IsCircList (RawState.ofData n base x).left (RawState.ofData n base x).right (h :: tail)) (hu_not : u ∉ h :: tail) : ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w (insertIntoNonEmptyList hReg uReg) x y 10 ∧ BaseRegs n base y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ (∃ (r : Fin n), (RawState.ofData n base x).right h = ↑r ∧ r ∈ h :: tail ∧ RawState.ofData n base y = have __src := RawState.ofData n base x; { key := __src.key, par := __src.par, child := __src.child, left := Function.update (Function.update (RawState.ofData n base x).left u ↑h) r ↑u, right := Function.update (Function.update (RawState.ofData n base x).right u ↑r) h ↑u, deg := __src.deg, mark := __src.mark, inHeap := __src.inHeap, cons := __src.cons, minRoot := __src.minRoot, numRoots := __src.numRoots, numMarked := __src.numMarked, sz := __src.sz }) ∧ IsCircList (RawState.ofData n base y).left (RawState.ofData n base y).right (h :: u :: tail)

insertIntoNonEmptyList hReg uReg splices u immediately after h in a circular list h :: tail (u ∉ h :: tail) in 10 instructions, modifying only left[u], left[r], right[u], right[h] (r = right[h]) and scratch registers s0, s2.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.descendant_ne_root_of_nodup {n : ℕ} {ts : List (FHTree n)} (hnd : (forestNodes ts).Nodup) {T R : FHTree n} (hT : T ∈ ts) (hR : R ∈ ts) {x : Fin n} (hx : x ∈ forestNodes T.children) : x ≠ R.root

In any Nodup forest ts, no strict descendant x ∈ forestNodes T.children (T ∈ ts) can equal the root of any tree R ∈ ts.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.addRootAndUpdateMin_preserves {r uReg : Fin rFib} (h0 : r ≠ s0) (h1 : r ≠ s1) (h2 : r ≠ s2) (h3 : r ≠ s3) (h4 : r ≠ s4) (h5 : r ≠ s5) (hm : r ≠ minRootReg) (hnr : r ≠ numRootsReg) : WordRAM.Code.Preserves r (addRootAndUpdateMin uReg)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.addRootAndUpdateMin_exec {n base w : ℕ} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) {uReg : Fin rFib} (hu_sc : uReg ≠ s0 ∧ uReg ≠ s1 ∧ uReg ≠ s2 ∧ uReg ≠ s3 ∧ uReg ≠ s4 ∧ uReg ≠ s5 ∧ uReg ≠ minRootReg ∧ uReg ≠ numRootsReg) {u : Fin n} (hu_val : x.regs uReg = ↑u) {T_u : FHTree n} {ts : List (FHTree n)} (hu_root : T_u.root = u) (hnd : (forestNodes (T_u :: ts)).Nodup) (hTu : ValidRoot (RawState.ofData n base x) none T_u) (hts : ∀ T ∈ ts, ValidRoot (RawState.ofData n base x) none T) (hnr : (RawState.ofData n base x).numRoots = ts.length) (hrl : ts = [] ∧ (RawState.ofData n base x).minRoot = 0 ∨ ∃ (m : Fin n) (rtail : List (Fin n)), (RawState.ofData n base x).minRoot = ↑m + 1 ∧ IsCircList (RawState.ofData n base x).left (RawState.ofData n base x).right (m :: rtail) ∧ (m :: rtail).Perm (List.map FHTree.root ts) ∧ ∀ T ∈ ts, Lean.IndexedMinPQ.PrioLE (m, (RawState.ofData n base x).key m) (T.root, (RawState.ofData n base x).key T.root)) : have st := RawState.ofData n base x; ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w (addRootAndUpdateMin uReg) x y 28 ∧ BaseRegs n base y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ have st' := RawState.ofData n base y; st'.key = st.key ∧ st'.par = st.par ∧ st'.child = st.child ∧ st'.deg = st.deg ∧ st'.mark = st.mark ∧ st'.inHeap = st.inHeap ∧ st'.cons = st.cons ∧ st'.numMarked = st.numMarked ∧ st'.sz = st.sz ∧ st'.numRoots = (T_u :: ts).length ∧ (∀ T ∈ T_u :: ts, ValidRoot st' none T) ∧ ∃ (m' : Fin n) (rtail' : List (Fin n)), st'.minRoot = ↑m' + 1 ∧ IsCircList st'.left st'.right (m' :: rtail') ∧ (m' :: rtail').Perm (List.map FHTree.root (T_u :: ts)) ∧ ∀ T ∈ T_u :: ts, Lean.IndexedMinPQ.PrioLE (m', st'.key m') (T.root, st'.key T.root)

addRootAndUpdateMin uReg appends a new valid root tree T_u (T_u.root = u) to the root circular list ts, updating minRootReg under IndexedMinPQ.PrioLT and incrementing numRootsReg in ≤ 28 instructions while preserving ValidRoot across T_u :: ts.

allocSpan, initSetup, and incCur

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.incCur_eval {w : ℕ} {x : WordRAM.Data rFib} (hone : x.regs oneReg = 1) (hfit : WordRAM.Fits w (x.regs curReg + 1)) : WordRAM.Op.eval w (WordRAM.Op.exactBin WordRAM.BinOp.add curReg curReg oneReg) x = some (x.set curReg (x.regs curReg + 1))

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.allocSpan_exec {n w base : ℕ} (hS : WordRAM.Fits w (base + space n)) {x : WordRAM.Data rFib} (_hx : WordRAM.Data.Bounded w x) (hfr : x.regs frontierReg = base) (hpar : ∀ (j : Fin 1), x.regs (![nReg] j) = ![n] j) : ∃ (x₁ : WordRAM.Data rFib), WordRAM.ExecWithin w allocSpan x x₁ 12 ∧ x₁.mem = x.mem ∧ x₁.regs baseReg = base ∧ x₁.regs frontierReg = base + space n ∧ ∀ (j : Fin 1), x₁.regs (![nReg] j) = ![n] j

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.initSetup_exec {n K_max w base : ℕ} {x₁ : WordRAM.Data rFib} (hx₁ : WordRAM.Data.Bounded w x₁) (hb₁ : x₁.regs baseReg = base) (hfr₁ : x₁.regs frontierReg = base + space n) (hpar₁ : ∀ (j : Fin 1), x₁.regs (![nReg] j) = ![n] j) (hz : ∀ a ∈ { base := base, length := space n }.footprint, x₁.mem a = 0) : ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w initSetup x₁ y 14 ∧ y.regs frontierReg = base + space n ∧ FibInv n K_max w base (Lean.IndexedMinPQ.empty n) y ∧ potential y ≤ 0 ∧ WordRAM.Modifies { base := base, length := space n }.footprint x₁.mem y.mem

isEmptyCode, getKeyCode, and insertCode

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.isEmptyCode_exec {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (hinv : FibInv n K_max w base s x) : ∃ (y : WordRAM.Data rFib) (t : ℕ), WordRAM.ExecWithin w isEmptyCode x y t ∧ code.decode Lean.IndexedMinPQ.Op.isEmpty y.regs = some (decide (Lean.IndexedMinPQ.dom s = ∅)) ∧ FibInv n K_max w base s y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ t + potential y ≤ 3 + potential x

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.getKeyCode_exec {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (v : Fin n) (hinv : FibInv n K_max w base s x) (hv_reg : x.regs argV = ↑v) : ∃ (y : WordRAM.Data rFib) (t : ℕ), WordRAM.ExecWithin w getKeyCode x y t ∧ code.decode (Lean.IndexedMinPQ.Op.getKey v) y.regs = some (s v) ∧ FibInv n K_max w base s y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ t + potential y ≤ 7 + potential x

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.insertCode_exec {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (v : Fin n) (k : ℕ) (hinv : FibInv n K_max w base s x) (hval : s v = none ∧ k ≤ K_max) (hv_reg : x.regs argV = ↑v) (hk_reg : x.regs argK = k) : ∃ (y : WordRAM.Data rFib) (t : ℕ), WordRAM.ExecWithin w insertCode x y t ∧ FibInv n K_max w base (Function.update s v (some k)) y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ t + potential y ≤ 121 + potential x