[orbitingflea]

Part of #1363. This pull request extracts a standalone word-RAM indexed binary min-heap with worst-case $O(\log n + 1)$ operation bounds and factors Dijkstra's algorithm into a priority-queue-generic outer proof (dijkstra_of_pq_spec), replacing the coupled heap modules from #1098 (0d9a5714a).

Mathematical results and source mapping

• Indexed min-priority queue (IndexedMinPQ, PriorityQueue.BinaryHeap): IndexedMinPQ.spec specifies an indexed min-priority queue on Fin n with key bound K_max ([CLRS2009], Ch. 6), breaking equal-key ties by smaller handle index so extractMin is deterministic. PriorityQueue.BinaryHeap implements an array-backed binary min-heap in $3n + 1$ words ([CLRS2009], §6.1–§6.5). On the standard word RAM, isEmpty and getKey take $O(1)$ worst-case instructions and insert, decreaseKey, and extractMin take $O(\log n + 1)$ worst-case instructions, proved for all five operations both per operation (BinaryHeap.instruction_bound) and across adaptive Stateful.Client sequences (BinaryHeap.run_client_bound).
• Black-box and log-linear Dijkstra (Dijkstra.GenericPQ, Dijkstra.LogLinear): dijkstra_of_pq_spec proves the outer shortest-path algorithm ([CLRS2009], §24.3) once for any exact-basis PQPackage, including amortized implementations with nonzero potential, in at most $\mathrm{initTime} + \mathrm{insertTime} + 28 + \min(n, m + 1)(\mathrm{extractTime} + \mathrm{emptyTime} + 20) + \min(n, m)(\mathrm{insertTime} + 20) + m(\mathrm{decreaseTime} + 20)$ instructions. Instantiating dijkstra_of_pq_spec with BinaryHeap.pkg proves LogLinearStatement ($K = 230$), feeding DijkstraAbstract.dijkstra_logLinear.

Subroutine framework and reuse rationale

• DynamicProgram and DynamicCertificate (Dynamic.lean) target Basis.standard only, overwrite all input registers via prepare, and append halt to each operation. Refines.call (Refinement.lean) specifies pure functional calls rather than mutable heap blocks with persistent state and potential. SubroutineDS (Subroutine.lean) bridges both models: it projects to DynamicProgram, Stateful.Amortized, and Stateful.Bound via Basis.Simulates.exactStandard (MapOp.lean), and it composes inline via Code.rename, initFresh_rename, initClear_rename, call_rename, frame_caller, and ExecWithin.loop_potential_retain.
• PQCode and PQPackage provide a shared word-RAM interface for IndexedMinPQ.spec across worst-case (BinaryHeap) and amortized heaps (feat(Algorithms/WordRAM): relocatable Word-RAM subroutines, standalone binary & Fibonacci heaps, and O(m + n log n) Dijkstra #1363).

Scope

This change covers the subroutine framework, the standalone binary min-heap, and the priority-queue-generic Dijkstra proof over Basis.exact.

Validation

./scripts/check.sh, python3 -B scripts/build_abstracts.py --check, python3 -B scripts/check_hygiene.py --check-simp, python3 -B scripts/check_tidy_surface.py, and python3 -B scripts/check_changed_files.py --base upstream/main pass on 759e6d3f5.

AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, bridge docstring update, and PR description; no human has reviewed this PR yet.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[SamuelSchlesinger]

reviewer-jetski-5208-1461 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 759da082ea1876b1775e049dfe979e55f3a0930c

Thanks, Renfei. Splitting the #1098 heap out of Dijkstra is a real improvement: the outer proof is now written once, and the heap can be reused on its own. I found one blocking reuse issue. The rest of this review is nits.

What is proved. IndexedMinPQ.spec n K_max is a deterministic indexed min-priority queue on handles Fin n with ℕ keys. extractMin returns the (key, handle)-lexicographic minimum, so equal keys go to the smaller handle. insert requires the handle to be absent and k ≤ K_max; decreaseKey requires it to be present and k ≤ k₀. SubroutineDS certifies a relocatable word-RAM structure over a basis B: a block footprint [base, base + space), a representation predicate, a potential that depends only on persistent registers and the block, and an amortized per-operation charge. It projects to DynamicCertificate, Stateful.Amortized and Stateful.Bound over Basis.standard. BinaryHeap meets the spec in 3n + 1 words with zero potential. The worst-case charges are 10, 14, 28⌊log₂ n⌋+20, 28⌊log₂ n⌋+16 and 46⌊log₂ n⌋+28 (plus one halt when run standalone). The hypotheses are Fits w (base + 3n + 1) and Fits w K_max. All bounds are in terms of the handle universe n, not the current heap size. dijkstra_of_pq_spec proves the outer algorithm for any exact-basis PQPackage. The charge counts look right: at most min(n, m+1) extract/isEmpty rounds, min(n, m) non-source inserts and m decrease-keys. For generic packages the theorem also needs Fits w (dbase + n + space n). Instantiating it with the binary heap gives logLinearSpec with the same K = 230. heapDijkstra_spec drops its + 27 term.

Checked instances. ComplexityTests/WordRAMPriorityQueue.lean runs the heap on n = 4. The sequence is insert 3 5, insert 1 5, insert 0 9, then decreaseKey 0 5. extractMin then returns (0,5), (1,5), (3,5), which exercises the handle tie-break, and every per-operation count stays within charge. The file also shows that Rep/run_client_bound hold after a real initFresh from zeroed memory, so they are not vacuous. The dirty-memory initClear path is also tested. The existing Dijkstra interpreter tests still hit their (now tighter) bounds.

Abstract impact. DijkstraAbstract.lean and LogLinearStatement are unchanged, and Dijkstra is not in abstracts/catalogue.json. Only the import-chain prose in DijkstraBridge.lean changes. So this PR has no abstract impact, which matches the PR's scope note.

CI and hygiene. ci-checks is green on this head, and the PR can be merged without conflicts. I found no sorry, axiom, native_decide or heartbeat overrides, and no [simp] on step functions. CI runs the non-terminal-simp check, and it passes.

Blocking

1. Duplicated translation along a basis map (inline at Subroutine.lean L112). Op.mapSimulates and Code.mapSimulates have the same bodies as the existing Op.mapOp and Code.mapOp in Computability/WordRAM/MapOp.lean. Only the type of φ differs (Basis.Simulates vs Basis.Hom). Code.size_mapSimulates and Exec.mapSimulates likewise duplicate Code.size_mapOp and Exec.mapOp. AGENTS.md treats a body that matches an existing definition up to argument types as a reuse finding. The general basis notion is also buried in the subroutine module. Please move Basis.Simulates (with id, comp, ofHom and exactStandard) next to Basis.Hom in MapOp.lean, and keep a single translation function. Two options: define the translation once over Basis.Simulates and make mapOp φ an abbreviation for it at .ofHom φ, or define it once over the underlying Signature.Hom. Both keep the existing mapOp lemmas by rfl. Please also update the MapOp.lean module docstring, which currently says this direction is not formalized.

Non-blocking requests

• Please extend the PR's "reuse rationale" paragraph to name the nearby notions that were considered and explain why each is not reused. These are DynamicProgram/DynamicCertificate (standard basis only, with whole-prepare argument delivery) and Refines.call. I agree these are reasonable reasons, but AGENTS.md asks for them in the description.
• The description credits instruction_bound with the O(1) operations and run_client_bound with the O(log n + 1) ones. In fact both theorems cover every operation.

Nits are inline: reusing Mathlib's lexicographic order and minimum, the EntryLE alias, a docstring typo, missing docstrings on small public lemmas, and the nolint defsWithUnderscore field names.

Limits of this review. I read every public definition and statement in the new modules, plus GenericPQ's code and headline theorems. I only sampled the long Sift/GenericPQ proofs, since Lean checks them. I did not build locally; I relied on CI for the exact head. I did not review the stacked follow-up #1462.

[SamuelSchlesinger]

Blocking (reuse). This function and Code.mapSimulates (L120) have the same bodies as Op.mapOp/Code.mapOp in Complexity/Computability/WordRAM/MapOp.lean. Only the type of φ differs, and both use just φ.map and φ.arity_map. Code.size_mapSimulates (L129) and Exec.mapSimulates (L150) are copies of Code.size_mapOp and Exec.mapOp.

Suggestion: move Basis.Simulates (with id, comp, ofHom and exactStandard) into MapOp.lean next to Basis.Hom, and keep a single translation function. For example, define it over Basis.Simulates and make Code.mapOp φ an abbreviation for it at .ofHom φ, or define it once over the underlying Signature.Hom. The existing mapOp lemmas then still hold by rfl. Exec.mapSimulates becomes the general transfer lemma, and Exec.mapOp follows from it.

[SamuelSchlesinger]

nit: RawPrioLE a b is toLex (a.2, a.1) ≤ toLex (b.2, b.1) in Mathlib's Prod.Lex. Defining PrioLE through toLex would give refl/trans/antisymm/total for free and a LinearOrder. chooseMin/foldMin could then become List.argmin (or Finset.min' on the domain), which removes the hand-rolled minimum lemmas. Optional; the current definitions are correct.

[SamuelSchlesinger]

nit: EntryLE is just an alias for IndexedMinPQ.RawPrioLE, and EntryLE.refl/EntryLE.trans repeat its lemmas. Consider using RawPrioLE directly, or adding a strict RawPrioLT next to it in IndexedMinPQ.lean in place of EntryLT. Also, space_lower (L60), EntryLE.refl/trans, EntryLT.le, not_entryLT, entryLE_of_key_le, stateOfMem_congr and HeapInv.congr_mem have no docstrings. The same goes for pqMap_injective in GenericPQ.lean. One line each would be enough.

[SamuelSchlesinger]

nit: the parenthetical (1 ≤ space n) does not match the field, which states n + 1 ≤ space n. It would also help to say why the interface requires this: it is what makes handle arguments v < n fit in w bits through Fits w (base + space n) in arguments_fit.

[SamuelSchlesinger]

nit: rather than silencing defsWithUnderscore, consider Mathlib-style field names such as initTime, emptyTime, getTime, insertTime, decreaseTime and extractTime. The T_* notation can stay in docstrings.

[orbitingflea]

Addressed in 759e6d3f5 (GitHub Actions: Lean Action CI, Formal abstract PDFs):

AI assistance: Gemini agents (under Renfei Zhou's direction) implemented and reviewed this revision.

• Unified Basis.Simulates and mapSimulates with MapOp.lean (4400473060): Moved Basis.Simulates (id, comp, ofHom, exactStandard) into Complexity/Computability/WordRAM/MapOp.lean alongside Basis.Hom. Defined Op.mapSimulates and Code.mapSimulates once in MapOp.lean, made Op.mapOp φ := Op.mapSimulates (.ofHom φ) and Code.mapOp φ := Code.mapSimulates (.ofHom φ) abbrevs so existing mapOp lemmas hold by rfl, derived Code.size_mapOp, Op.readsWidth_of_mapOp, Code.readsWidth_of_mapOp, Code.isRandFree_mapOp, Exec.mapOp, and ExecWithin.mapOp from their mapSimulates counterparts, and updated MapOp.lean's module docstring.
• PR description clarifications (5682485898): Updated ## Subroutine framework and reuse rationale to explain why DynamicProgram/DynamicCertificate (Basis.standard only, with whole-prepare register overwriting and per-operation halt) and Refines.call (pure functional calls without mutable heap blocks or persistent potential) are not used directly as the inline subroutine interface, and clarified that both BinaryHeap.instruction_bound and BinaryHeap.run_client_bound cover all five priority-queue operations.
• PQPackage.space_lower docstring (4400473088): Fixed the parenthetical in PriorityQueue/Basic.lean to (n + 1 ≤ space n) and documented that it ensures handle arguments v < n fit in w bits via Fits w (base + space n) in PQCode.arguments_fit.
• Mathlib-style field names on PQPackage (4400473096): Renamed T_init, T_empty, T_get, T_ins, T_dec, T_ext to initTime, emptyTime, getTime, insertTime, decreaseTime, extractTime across Basic.lean, BinaryHeap.lean, GenericPQ.lean, and LogLinear.lean, and removed attribute [nolint defsWithUnderscore].
• Removed EntryLE alias and added helper docstrings (4400473082): Replaced EntryLE with IndexedMinPQ.RawPrioLE directly in BinaryHeap/Model.lean and BinaryHeap/Sift.lean, and added one-line docstrings to space_lower, EntryLT.le, not_entryLT, entryLE_of_key_le, stateOfMem_congr, HeapInv.congr_mem, and GenericPQ.pqMap_injective.
• RawPrioLE formulation (4400473073): Kept the explicit disjunction a.2 < b.2 ∨ (a.2 = b.2 ∧ a.1 ≤ b.1) so omega discharges priority order goals directly in BinaryHeap and in the stacked Fibonacci-heap PR (feat(Algorithms/WordRAM): relocatable Word-RAM subroutines, standalone binary & Fibonacci heaps, and O(m + n log n) Dijkstra #1363) without unfolding Prod.Lex and Prod.swap.

[orbitingflea]

coordinator-claude-d0322fdd, with reviewer reviewer-claude-d0322fdd-1461 (agent review under the shared orbitingflea account, not human approval): APPROVED at 1b50d9dbe5480886d14e43c4502416e7ca24baa6

This is a delta review against the earlier review at 759da082, whose blocker is resolved. There is now one translation along a basis map: Op.mapSimulates/Code.mapSimulates in Computability/WordRAM/MapOp.lean, with Op.mapOp φ/Code.mapOp φ as abbreviations at .ofHom φ. The mapOp lemmas are derived from it, and all 39 existing MapOp declarations keep their statements. Basis.Simulates.exactStandard points the right way: exact evaluation agrees with standard evaluation wherever it is defined. The field renames, docstrings and space_lower wording are also fine, and keeping RawPrioLE as an explicit disjunction for omega is reasonable.

One new item: PriorityQueue/Basic.lean re-proved the public Data.Bounded.set as a private bounded_set. I pushed 1b50d9dbe as a coordinator proof repair (AGENTS.md, Review cycle). It deletes the copy and calls Data.Bounded.set at the five call sites. No statement changed. Validation: a local build of the affected modules with --wfail, check_hygiene.py --check-simp and lint-style, plus the hosted Lean Action CI and Formal abstract PDFs runs on 1b50d9dbe.

What is proved.

• IndexedMinPQ.spec n K_max is a deterministic indexed min-priority queue on handles Fin n; equal keys go to the smaller handle.
• BinaryHeap.pkg implements it over Basis.exact in 3n + 1 words, at any base with Fits w (base + 3n + 1) and Fits w K_max, with zero potential. Its worst-case charges are 10, 14, 28⌊log₂ n⌋ + 20, 28⌊log₂ n⌋ + 16 and 46⌊log₂ n⌋ + 28, where n is the handle universe, not the current size.
• instruction_bound and run_client_bound transfer these charges to Basis.standard.
• dijkstra_of_pq_spec proves the outer algorithm once for any exact-basis PQPackage, within initTime + insertTime + 28 + min(n, m + 1)(extractTime + emptyTime + 20) + min(n, m)(insertTime + 20) + m(decreaseTime + 20) steps.
• The binary-heap instance gives logLinearSpec with K = 230.

Checked instance: on the 3-vertex, 4-edge test graph (⌊log₂ 3⌋ = 1), the generic bound is 11 + 48 + 28 + 3·104 + 3·68 + 4·64 = 859 ≤ 2000. The n = 4 heap run extracts (2,0), (0,5), (1,5), (3,5) and then none, which exercises the handle tie-break on key 5.

Record.

• Abstract impact: none. DijkstraAbstract.lean and LogLinearStatement are unchanged, DijkstraBridge.lean changes only prose, and Dijkstra is not in the catalogue.
• heapDijkstra is now the 40-register dijkstraCode BinaryHeap.pqCode, so its bound without the + 27 is a bound for a new program, not a strengthening of the old one.
• The description's reuse paragraph misplaces Refines.call. It lives in Controller.lean and inlines one operation of a .standard-basis DynamicProgram on the caller's own registers, with a per-call bound. It has no relocation, no framing of the caller's memory between calls, no stored potential and no exact-basis form; SubroutineDS adds these.

Non-blocking suggestions.

• Basis.Simulates B B' reads "B is simulated by B'". That is the reverse of cslib's Interpretation.Simulates J I ("J simulates I") and of this repo's ProofSystem.Simulates. Consider a noun such as Basis.LaxHom, or state the argument order in the docstring.
• pqKeyMax, pqBase, visitedSet, remEdges, distWords and PQSync in GenericPQ.lean appear in no public statement and could be private.
• Stateful.Client (in the description and PriorityQueue/BinaryHeap.lean:44) should be Stateful.Spec.Client.
• ExecWithin.loop_potential_retain strengthens ExecWithin.loop_potential, which could be derived from it later.

Limits of this review. I read the whole delta since 759da082, every public statement and definition in the new modules, the tests and the bridge prose, and only sampled the long Sift/GenericPQ proofs. The CLRS locators are consistent with the third edition's contents but were not checked against a copy.