Degree-indexed root consolidation and extractMin for a Fibonacci heap

This file proves the correctness, memory-safety, and O(log n) amortized instruction bound of scatterRootCode and extractMinCode Fredman and Tarjan Cormen et al., Section 19.2:

• Degree-table invariant (SlotInv): Tracks the subset slotTrees of consolidated root trees currently stored in cons[0..maxDeg], maintaining pairwise-distinct degrees, maxDeg ≤ 2 * Nat.log 2 n + 1, and zeroing of all unoccupied entries cons[d] (d ≤ n).
• Root scattering (scatterRootCode_exec): Repeatedly links equal-degree roots via ValidRoot.link under lexicographic IndexedMinPQ.PrioLT using internal potential 50 * slotTrees.length, executing in t + 50 * slotTrees'.length ≤ 63 + 50 * slotTrees.length steps while framing all other live nodes.
• Minimum extraction (extractMinCode_exec): Removes z = minRoot - 1 (agreeing with IndexedMinPQ.findMin), scatters z's children and the numRoots - 1 remaining roots into cons, and scans only 0 .. maxDeg (≤ 2 * Nat.log 2 n + 2 slots) to rebuild the root circular list and minRootReg while restoring cons = 0 in t + potential y ≤ 410 * (Nat.log 2 n + 1) + potential x instructions.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv: consolidation-table invariant tracking distinct-degree root trees in cons[0..maxDeg].

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.scatterRootCode_exec: amortized root scattering and equal-degree linking specification.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.extractMinCode_exec: O(log n) amortized extractMin specification.

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, Section 19.2

Framing and pure-ℕ degree bounds during consolidation

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot.frame_tree {n : ℕ} {st st' : RawState n} {T : FHTree n} (hT : ValidRoot st none T) (hnode : ∀ u ∈ T.nodes, st'.inHeap u = st.inHeap u ∧ st'.mark u = st.mark u ∧ st'.deg u = st.deg u ∧ st'.child u = st.child u ∧ st'.key u = st.key u ∧ st'.par u = st.par u) (hlr : ∀ u ∈ forestNodes T.children, st'.left u = st.left u ∧ st'.right u = st.right u) : ValidRoot st' none T

Framing ValidRoot st none T across a state transition preserving node fields on T.nodes and pointer fields on strict descendants forestNodes T.children.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot.frame_nodes {n : ℕ} {st st' : RawState n} {T : FHTree n} (hT : ValidRoot st none T) (h : ∀ u ∈ T.nodes, st'.inHeap u = st.inHeap u ∧ st'.mark u = st.mark u ∧ st'.deg u = st.deg u ∧ st'.child u = st.child u ∧ st'.key u = st.key u ∧ st'.par u = st.par u ∧ st'.left u = st.left u ∧ st'.right u = st.right u) : ValidRoot st' none T

Framing ValidRoot st none T when all seven vertex arrays agree on T.nodes.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.deg_bounds_of_extra {n : ℕ} {st : RawState n} {T : FHTree n} {z : Fin n} (hT : ValidSubtree st none T) (hnd : (z :: T.nodes).Nodup) : T.deg ≤ 2 * Nat.log 2 n + 1 ∧ T.deg + 2 ≤ n

Every valid subtree T disjoint from at least one other handle z : Fin n satisfies both T.deg ≤ 2 * Nat.log 2 n + 1 and T.deg + 2 ≤ n.

Consolidation table invariant SlotInv

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv (n : ℕ) (st : RawState n) (slotTrees : List (FHTree n)) (maxDeg : ℕ) : Prop

Invariant for the degree consolidation table st.cons holding slotTrees within 0 .. maxDeg.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.empty {n : ℕ} {st : RawState n} (hcons : ∀ d ≤ n, st.cons d = 0) : SlotInv n st [] 0

Initial empty consolidation table when ∀ d ≤ n, st.cons d = 0.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.frame {n maxDeg : ℕ} {st st' : RawState n} {slotTrees : List (FHTree n)} (hs : SlotInv n st slotTrees maxDeg) (hcons : st'.cons = st.cons) (hvalid : ∀ T ∈ slotTrees, ValidRoot st' none T) : SlotInv n st' slotTrees maxDeg

Framing SlotInv across a transition preserving cons and ValidRoot on slotTrees.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.lookup {n maxDeg : ℕ} {st : RawState n} {slotTrees : List (FHTree n)} (hs : SlotInv n st slotTrees maxDeg) {d : ℕ} (hd : d ≤ n) : (st.cons d = 0 ∧ ∀ T ∈ slotTrees, T.deg ≠ d) ∨ ∃ (i : ℕ) (hi : i < slotTrees.length), slotTrees[i].deg = d ∧ st.cons d = ↑slotTrees[i].root + 1 ∧ (slotTrees.eraseIdx i).length + 1 = slotTrees.length ∧ ∀ R ∈ slotTrees.eraseIdx i, R.deg ≠ d

Lookup in st.cons d (d ≤ n): either st.cons d = 0 and no tree in slotTrees has degree d, or a unique index i < slotTrees.length has (slotTrees[i]).deg = d and st.cons d = (slotTrees[i]).root.val + 1.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.step_collision {n maxDeg : ℕ} {st st' : RawState n} {slotTrees : List (FHTree n)} (hs : SlotInv n st slotTrees maxDeg) {i d : ℕ} (hi : i < slotTrees.length) (hdeg_i : slotTrees[i].deg = d) (_hd : d ≤ n) (hno_other : ∀ R ∈ slotTrees.eraseIdx i, R.deg ≠ d) (hcons' : st'.cons = Function.update st.cons d 0) (hvalid' : ∀ R ∈ slotTrees.eraseIdx i, ValidRoot st' none R) : SlotInv n st' (slotTrees.eraseIdx i) maxDeg

Clearing slot d = (slotTrees[i]).deg (d ≤ n) removes slotTrees[i] from SlotInv.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.insert_empty {n maxDeg : ℕ} {st : RawState n} {slotTrees : List (FHTree n)} (hs : SlotInv n st slotTrees maxDeg) {T_cur : FHTree n} {d : ℕ} (_hd_n : d + 2 ≤ n) (hd_log : d ≤ 2 * Nat.log 2 n + 1) (hT_deg : T_cur.deg = d) (hnone : ∀ R ∈ slotTrees, R.deg ≠ d) (hT_valid : ValidRoot st none T_cur) : SlotInv n { key := st.key, par := st.par, child := st.child, left := st.left, right := st.right, deg := st.deg, mark := st.mark, inHeap := st.inHeap, cons := Function.update st.cons d (↑T_cur.root + 1), minRoot := st.minRoot, numRoots := st.numRoots, numMarked := st.numMarked, sz := st.sz } (T_cur :: slotTrees) (max maxDeg d)

Storing a consolidated tree T_cur of unoccupied degree d into st.cons d and updating maxDeg to max maxDeg d inserts T_cur into SlotInv.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.SlotInv.done_of_cleared {n maxDeg : ℕ} {st : RawState n} {slotTrees : List (FHTree n)} (hs : SlotInv n st slotTrees maxDeg) (hcleared : ∀ d < maxDeg + 1, ∀ T ∈ slotTrees, T.deg ≠ d) : slotTrees = [] ∧ ∀ d ≤ n, st.cons d = 0

Once every degree < maxDeg + 1 has been cleared from SlotInv, slotTrees = [] and all entries st.cons d (d ≤ n) are 0.

Root scattering (scatterBody_exec and scatterRootCode_exec)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.eta {n : ℕ} (T : FHTree n) : node T.root T.children = T

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.scatterRootCode_exec {n base w maxDeg₀ : ℕ} {x : WordRAM.Data rFib} {T₀ : FHTree n} {slotTrees₀ : List (FHTree n)} {otherNodes : List (Fin n)} {z : Fin n} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) (hz_mem : z ∈ otherNodes) (hnd : (T₀.nodes ++ (forestNodes slotTrees₀ ++ otherNodes)).Nodup) (hs : SlotInv n (RawState.ofData n base x) slotTrees₀ maxDeg₀) (hT₀ : ValidRoot (RawState.ofData n base x) none T₀) (hx_ic : x.regs iterCur = ↑T₀.root) (hx_md : x.regs maxDegReg = maxDeg₀) : ∃ (y : WordRAM.Data rFib) (slotTrees' : List (FHTree n)) (maxDeg' : ℕ) (t : ℕ), WordRAM.ExecWithin w scatterRootCode x y t ∧ t + slotCredit * slotTrees'.length ≤ 63 + slotCredit * slotTrees₀.length ∧ WordRAM.Data.Bounded w y ∧ BaseRegs n base y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ (∀ (r : Fin rFib), ↑r < 33 → y.regs r = x.regs r) ∧ y.regs maxDegReg = maxDeg' ∧ (forestNodes slotTrees').Perm (T₀.nodes ++ forestNodes slotTrees₀) ∧ (forestNodes slotTrees' ++ otherNodes).Nodup ∧ SlotInv n (RawState.ofData n base y) slotTrees' maxDeg' ∧ have st := RawState.ofData n base x; have st' := RawState.ofData n base y; st'.key = st.key ∧ st'.mark = st.mark ∧ st'.inHeap = st.inHeap ∧ st'.minRoot = st.minRoot ∧ st'.numRoots = st.numRoots ∧ st'.numMarked = st.numMarked ∧ st'.sz = st.sz ∧ ∀ u ∈ otherNodes, st'.par u = st.par u ∧ st'.child u = st.child u ∧ st'.left u = st.left u ∧ st'.right u = st.right u ∧ st'.deg u = st.deg u

scatterRootCode inserts root T₀ (iterCur = T₀.root.val) into cons, linking equal-degree roots and updating maxDegReg in t + 50 * slotTrees'.length ≤ 63 + 50 * slotTrees₀.length instructions while preserving all registers < 33 and framing otherNodes.

Consolidation scatter loops (childScatterLoop and rootScatterLoop)

Phase B slot gathering (gatherSlotsLoop_exec)

extractMinCode correctness and O(log n) amortized bound

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.extractMinCode_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 extractMinCode x y t ∧ code.decode Lean.IndexedMinPQ.Op.extractMin y.regs = some ((Lean.IndexedMinPQ.spec n K_max).step s Lean.IndexedMinPQ.Op.extractMin).2 ∧ FibInv n K_max w base ((Lean.IndexedMinPQ.spec n K_max).step s Lean.IndexedMinPQ.Op.extractMin).1 y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ t + potential y ≤ 410 * (Nat.log 2 n + 1) + potential x

extractMinCode implements .extractMin on FibInv within 410 * (Nat.log 2 n + 1) amortized instructions (t + potential y ≤ 410 * (Nat.log 2 n + 1) + potential x).