Black-Box Dijkstra's Algorithm Parameterized by Any Word-RAM Priority Queue

This file implements the outer graph-traversal layer of Dijkstra's single-source shortest-path algorithm once (Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode) on 15 + r_pq registers over Basis.exact, parameterized only by a Cslib.Algorithms.WordRAM.PriorityQueue.PQCode subroutine, and proves its black-box correctness and amortized instruction-count specification (Cslib.Algorithms.WordRAM.Dijkstra.dijkstra_of_pq_spec) for any Cslib.Algorithms.WordRAM.PriorityQueue.PQPackage (supporting arbitrary concrete potentials potential : Data r_pq → ℕ).

Instantiating dijkstra_of_pq_spec with:

• PriorityQueue.BinaryHeap.pkg (potential = 0) yields LogLinearSpec and LogLinearStatement (O((m + 1) (⌊log₂ n⌋ + 1)));
• any amortized PQPackage with O(1) insert/decreaseKey and O(log n + 1) extractMin (such as a Fibonacci heap) directly yields O(m + min(n, m + 1) (⌊log₂ n⌋ + 1)) and O(m + n (⌊log₂ n⌋ + 1)) with zero duplication of Dijkstra's graph logic.

Main definitions

• Cslib.Algorithms.WordRAM.Dijkstra.pqMap: register relocation Fin.natAdd 15 placing the priority-queue registers at 15 .. 15 + r_pq - 1.
• Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode: structured word-RAM code for Dijkstra's algorithm calling a black-box PQCode .exact r_pq.

Main results

• Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode_exec: structured ExecWithin correctness and amortized running-time bound for dijkstraCode pkg.code.
• Cslib.Algorithms.WordRAM.Dijkstra.dijkstra_of_pq_spec: flat-program Runs + halt theorem for (dijkstraCode pkg.code).program OuterReg.zero.

References

• E. W. Dijkstra, A note on two problems in connexion with graphs
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

def Cslib.Algorithms.WordRAM.Dijkstra.pqMap {r_pq : ℕ} : Fin r_pq → Fin (15 + r_pq)

Relocation map embedding the r_pq priority-queue registers above the 15 outer registers.

theorem Cslib.Algorithms.WordRAM.Dijkstra.pqMap_injective {r_pq : ℕ} : Function.Injective pqMap

Register relocation pqMap is injective.

Outer caller registers (0 .. 14) of dijkstraCode

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.zero {r_pq : ℕ} : Fin (15 + r_pq)

Constant 0.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.one {r_pq : ℕ} : Fin (15 + r_pq)

Constant 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.three {r_pq : ℕ} : Fin (15 + r_pq)

Constant 3.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.nReg {r_pq : ℕ} : Fin (15 + r_pq)

Number of vertices n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.eb {r_pq : ℕ} : Fin (15 + r_pq)

Base address n + 4 of the edge array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.db {r_pq : ℕ} : Fin (15 + r_pq)

Base address G.dbase = n + 2 * m + 4 of the n output distance words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.u {r_pq : ℕ} : Fin (15 + r_pq)

Current vertex u extracted from the priority queue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.best {r_pq : ℕ} : Fin (15 + r_pq)

Distance word best = d[u] of u.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.j {r_pq : ℕ} : Fin (15 + r_pq)

Current edge index j.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.jend {r_pq : ℕ} : Fin (15 + r_pq)

End edge index jend of adj u.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.tv {r_pq : ℕ} : Fin (15 + r_pq)

Target vertex tv of edge j.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.tc {r_pq : ℕ} : Fin (15 + r_pq)

Weight tc of edge j.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.cand {r_pq : ℕ} : Fin (15 + r_pq)

Candidate distance word best + tc.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.dv {r_pq : ℕ} : Fin (15 + r_pq)

Current distance word d[tv] (inside relaxEdges) and emptiness flag (in outer loop).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.OuterReg.t {r_pq : ℕ} : Fin (15 + r_pq)

Scratch address register.

Structured Word-RAM Code of Black-Box Dijkstra

def Cslib.Algorithms.WordRAM.Dijkstra.outerHeader {r_pq : ℕ} : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Straight-line outer header: loads n, source, db = G.dbase, eb = n + 4, sets mem[db + source] := 1, and places pqBase = db + n in t.

def Cslib.Algorithms.WordRAM.Dijkstra.dijkstraSetup {r_pq : ℕ} (P : PriorityQueue.PQCode WordRAM.Basis.exact r_pq) : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Full setup of dijkstraCode: runs outerHeader, initializes the relocated priority queue at pqBase = G.dbase + G.n via initFresh, inserts (source, 1), and sets dv := 0 (non-empty).

def Cslib.Algorithms.WordRAM.Dijkstra.edgePrefix {r_pq : ℕ} : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Straight-line start of one edge relaxation: loads (tv, tc) for edge j, advances j, forms cand := best + tc, and loads dv := mem[db + tv].

def Cslib.Algorithms.WordRAM.Dijkstra.edgeBody {r_pq : ℕ} (P : PriorityQueue.PQCode WordRAM.Basis.exact r_pq) : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Body of relaxEdges for a single outgoing edge.

def Cslib.Algorithms.WordRAM.Dijkstra.relaxEdges {r_pq : ℕ} (P : PriorityQueue.PQCode WordRAM.Basis.exact r_pq) : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Inner loop scanning all outgoing edges [j, jend) of vertex u.

def Cslib.Algorithms.WordRAM.Dijkstra.loadOffsets {r_pq : ℕ} : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Offset-loading block for u: sets j := offset u and jend := offset (u + 1).

def Cslib.Algorithms.WordRAM.Dijkstra.dijkstraRound {r_pq : ℕ} (P : PriorityQueue.PQCode WordRAM.Basis.exact r_pq) : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

One outer round of dijkstraCode: extracts minimum (u, best), loads u's edge range, scans its outgoing edges via relaxEdges, and refreshes the emptiness flag dv via callIsEmpty.

def Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode {r_pq : ℕ} (P : PriorityQueue.PQCode WordRAM.Basis.exact r_pq) : WordRAM.Code WordRAM.Basis.exact (15 + r_pq)

Complete structured word-RAM code for Dijkstra's algorithm calling P : PQCode .exact r_pq.

Input Boundedness and Framing Helpers

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.pqKeyMax (G : ListInstance) : ℕ

Maximum priority-queue key ever inserted or decreased on instance G.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.pqBase (G : ListInstance) : ℕ

Base address G.dbase + G.n of the priority-queue memory block.

Inner Edge-Scan Specification (relaxEdges_spec)

def Cslib.Algorithms.WordRAM.Dijkstra.visitedSet {r_pq : ℕ} (G : ListInstance) (s : Lean.IndexedMinPQ.State G.n) (y : WordRAM.Data (15 + r_pq)) : Finset (Fin G.n)

Discovered vertices (mem[dbase + v] ≠ 0) that are no longer in dom s.

def Cslib.Algorithms.WordRAM.Dijkstra.remEdges (G : ListInstance) (S : Finset (Fin G.n)) : ℕ

Total outgoing edges of vertices outside S.

noncomputable def Cslib.Algorithms.WordRAM.Dijkstra.distWords {r_pq : ℕ} (G : ListInstance) (y : WordRAM.Data (15 + r_pq)) (v : Fin G.n) : ℕ∞

Tentative distances decoded from y.mem (G.dbase + ·).

def Cslib.Algorithms.WordRAM.Dijkstra.PQSync {r_pq : ℕ} (G : ListInstance) (s : Lean.IndexedMinPQ.State G.n) (y : WordRAM.Data (15 + r_pq)) : Prop

Synchronization between abstract PQ state s and distance array y.mem (G.dbase + ·): every handle in dom s has a nonzero distance word equal to its PQ key.

Outer Round Invariant, Setup, Round Step, and Main Black-Box Theorems

theorem Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode_exec {r_pq : ℕ} (pkg : PriorityQueue.PQPackage WordRAM.Basis.exact r_pq) (G : ListInstance) (w : ℕ) (hw_in : WordRAM.Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) (hw_sp : WordRAM.Fits w (G.dbase + G.n + pkg.space G.n)) : ∃ (y : WordRAM.Data (15 + r_pq)), WordRAM.ExecWithin w (dijkstraCode pkg.code) (WordRAM.Data.init G.encode) y (pkg.initTime G.n + pkg.insertTime G.n + 28 + min G.n (G.m + 1) * (pkg.extractTime G.n + pkg.emptyTime G.n + 20) + min G.n G.m * (pkg.insertTime G.n + 20) + G.m * (pkg.decreaseTime G.n + 20)) ∧ ∀ (v : Fin G.n), y.mem (G.outAddr v) = encodeDist (G.dist G.source v)

Black-box structured Dijkstra theorem. For any exact-basis PQPackage, dijkstraCode computes all encoded shortest-path distances within initTime + insertTime + 28 + min(n, m + 1) * (extractTime + emptyTime + 20) + min(n, m) * (insertTime + 20) + m * (decreaseTime + 20) instructions.

theorem Cslib.Algorithms.WordRAM.Dijkstra.dijkstra_of_pq_spec {r_pq : ℕ} (pkg : PriorityQueue.PQPackage WordRAM.Basis.exact r_pq) (G : ListInstance) (w : ℕ) (hw_in : WordRAM.Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) (hw_sp : WordRAM.Fits w (G.dbase + G.n + pkg.space G.n)) : have p := (dijkstraCode pkg.code).program OuterReg.zero; ∃ (t : WordRAM.State (15 + r_pq)) (steps : ℕ), WordRAM.Runs w p (WordRAM.State.init G.encode) t steps ∧ (∃ (v : ℕ), WordRAM.step w p t = WordRAM.Outcome.halt v) ∧ steps ≤ pkg.initTime G.n + pkg.insertTime G.n + 28 + min G.n (G.m + 1) * (pkg.extractTime G.n + pkg.emptyTime G.n + 20) + min G.n G.m * (pkg.insertTime G.n + 20) + G.m * (pkg.decreaseTime G.n + 20) ∧ ∀ (v : Fin G.n), t.data.mem (G.outAddr v) = encodeDist (G.dist G.source v)

Black-box flat-program Dijkstra theorem. Compiling dijkstraCode pkg.code produces a flat word-RAM program over Basis.exact that computes all single-source shortest-path distances and halts within the parameterized priority-queue instruction bound.