Repository navigation
feat(Algorithms/WordRAM): standalone Fibonacci heap and O(m + n log n) Dijkstra - #1462
Conversation
…nify binary-heap priority helpers
…used step helpers
…e abstract bridge transfer lemmas
There was a problem hiding this comment.
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
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1462 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 4ff522759d2fb8388a51337128a0f7a104f8817c
Thanks for this substantial development, Renfei. The test suite is well chosen: interpreter runs that exercise tie-breaking, consolidation into a degree-3 tree and a real two-level cascading cut are good evidence that the definitions say what they should.
Scope. This PR is stacked on #1461. I reviewed only its own commits, 45c1bcea3..4ff522759, i.e. the diff against #1461's head 759da082e. The SubroutineDS / IndexedMinPQ / BinaryHeap / GenericPQ files belong to #1461 and are not covered here.
What is proved.
- Model. The model is the exact-basis word RAM with a static
9n + 1-word block[base, base + 9n + 1)(eightn-word node arrays plus thecons[0..n]degree table), 42 registers, and no dynamic node allocation. The word-size conditions arebase + 9n + 1 < 2^wandK_max < 2^w. Every instruction, includinghalt, costs one unit. - Potential and amortized bounds. The potential is
Φ = 80 (numRoots + 2·numMarked).ValidRootforces roots to be unmarked, sonumMarkedcounts marked non-roots, matching Fredman–Tarjan's potential. Against this potential,insertanddecreaseKeyhave amortized cost at most 130 and 340 instructions, andextractMinat most420 (⌊log₂ n⌋ + 1). Herenis the handle capacity, not the current heap size; that is the standard upper bound. - Degree bound. It comes from the chronological rank invariant
i ≤ deg + markfor the (0-indexed) i-th child. This is slightly stronger than FT Lemma 1. It feedsfib (deg + 2) ≤ sizeand thendeg ≤ 2⌊log₂ n⌋ + 1, all in ℕ. - Aggregate statements.
run_ops_exact_fresh/_reusableand the abstract'sfibonacciHeap_amortized{,_reusable}state the usual aggregate amortized bound for any admissible sequence starting from an empty heap:t_ops ≤ K (m_q + m_ins + m_dec + m_ext (log n + 1)). Initialization costsO(1)on zeroed memory andO(n + 1)on arbitrary memory. Memory outside the block is unchanged, andKandrare fixed beforen,wandK_maxare quantified. - Dijkstra.
FibonacciSpecgives640 (m + min(n, m + 1)(⌊log₂ n⌋ + 1))under the same hypothesis asLogLinearSpec, anddijkstra_fibonaccistates the textbookO(m + n log n)bound.
Checked edge case. In FibonacciHeapTests, sampleOps on Fin 4 gives the bound K·(2 + 2 + 1 + 1·3) = 8K (with Nat.log 2 4 = 2), and the sentinels just outside [10, 47) survive. This, together with the interpreter examples, establishes nonvacuity of both abstract theorems.
Abstract impact. The PR adds FibonacciHeapAbstract and extends DijkstraAbstract with dijkstra_fibonacci. Both are standalone and not added to catalogue.json, consistent with the existing Dijkstra abstract. I checked both statements against the library theorems; apart from the isEmpty flag docstring nit inline, they match. #check_abstract passes in CI. CI: ci-checks is green on the exact head, and the PR is mergeable.
Blocking
- Duplicate definition.
FibonacciHeap.ValidSeqis exactlyStateful.Spec.ValidHistoryforIndexedMinPQ.spec n K_max. Please useValidHistory(inline atFibonacciHeap.lean:274). - Incorrect Fredman–Tarjan locators in docstrings. I checked a scan of the JACM paper:
- Lemma 1 (p. 604) is the child-rank lemma, "the ith child of x has a rank of at least i − 2".
- Corollary 1 (p. 604) is the
F_(k+2)subtree-size bound. - Lemma 2 (p. 605) is about
find minin the vacant-node variant.
So the Fibonacci sum identity (Model.lean:356) should not be credited to Lemma 1, andfib_le_size(Trees.lean:458) is Corollary 1, not Lemma 2. The PR description has the same problem, so please fix it there too: - The marked-non-root potential is defined on p. 604. Page 600 only has the binomial-queue potential, "number of trees".
- "Thm. 2, p. 604" for Dijkstra does not match: p. 604 contains Theorem 1, the F-heap amortized bounds. Please give the correct theorem/page for the shortest-path application.
- CLRS defines
Φ(H) = t(H) + 2m(H)in §19.1 (eq. 19.1), not §19.3.
Non-blocking (nits): inline. They cover the placement of the generic op counters and of RunsOps, a Mathlib duplicate (List.Nodup.length_le_card), the module-docstring wording of the 421 bound, the R[22] docstring in the abstract, and an optional shared shortest-path spec.
Limits of this review. I read every public statement and definition in the M2 files, the abstract and the bridge interfaces. I sampled the proofs in Cut.lean and Consolidate.lean and did not read them in full; Lean checks them. I did not build locally and relied on CI. I could not verify the CLRS page numbers against a copy of the book.
| | _ :: ops => numExtractMins ops | ||
|
|
||
| /-- Sequential admissibility of an operation list starting from abstract state `s`. -/ | ||
| def ValidSeq {n : ℕ} (K_max : ℕ) : IndexedMinPQ.State n → List (IndexedMinPQ.Op n) → Prop |
There was a problem hiding this comment.
Blocking (duplicate definition). This is definitionally (IndexedMinPQ.spec n K_max).ValidHistory s ops (Cslib.Stateful.Spec.ValidHistory in Foundations/Semantics/Stateful/Basic.lean), which run_client_amortized above already uses. Please drop ValidSeq and state run_ops_exact_fresh/_reusable (and seq_runsOps) with ValidHistory. The validHistory_cons simp lemma should make the proof changes mechanical. The abstract can keep its own self-contained ValidSeq; only the bridge needs adjusting.
|
|
||
| /-! ## Pure-`ℕ` Fibonacci rank and degree bounds -/ | ||
|
|
||
| /-- Fundamental Fibonacci rank identity ([Fredman and Tarjan][FredmanTarjan1987], Lemma 1): |
There was a problem hiding this comment.
Blocking (source locator). In [FredmanTarjan1987], Lemma 1 (p. 604) is the child-rank statement ("the ith child of x has a rank of at least i − 2"); this module's analogue is the hrank field of ValidSubtree. The Fibonacci sum identity is used in the proof of Corollary 1 (p. 604, F_(k+2) = Σ_(i=0)^(k) F_i + 1). Suggest "(used in the proof of [FredmanTarjan1987], Corollary 1)" or no locator.
| simp only [Nat.add_zero, forestNodes, List.length_append] | ||
| omega | ||
|
|
||
| /-- Fredman–Tarjan subtree size lower bound (`[FredmanTarjan1987]`, Lemma 2): in any subtree with |
There was a problem hiding this comment.
Blocking (source locator). The subtree-size bound is [FredmanTarjan1987], Corollary 1 (p. 604: "A node of rank k in an F-heap has at least F_(k+2) ≥ φ^k descendants, including itself"). Lemma 2 (p. 605) is the find min bound for F-heaps with vacant nodes. Please also check the PR description, which cites "Cor. 1" for the 2 log n + 1 rank bound; that bound is derived from Corollary 1 in the text that follows it on p. 604.
| if i = tag2 ∨ i = tag1 ∨ i = tag0 ∨ i = argV ∨ i = argK then code.encode o i else regs i | ||
|
|
||
| /-- Count `isEmpty` and `getKey` queries in an operation sequence. -/ | ||
| def numQueries {n : ℕ} : List (IndexedMinPQ.Op n) → ℕ |
There was a problem hiding this comment.
nit (placement): numQueries/numInserts/numDecreaseKeys/numExtractMins are facts about IndexedMinPQ.Op lists, not about Fibonacci heaps, and they sit in the FibonacciHeap namespace. Consider moving them next to IndexedMinPQ (or recording a follow-up) so a later BinaryHeap.run_ops_exact can reuse them.
| 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). -/ | ||
| inductive RunsOps {n K_max : ℕ} (w base : ℕ) : |
There was a problem hiding this comment.
nit (follow-up): RunsOps is only Fibonacci-specific through opProg, prepareRegs and code.decode. Parameterizing it by a PQCode would let the binary heap state the same standalone multi-call theorem. Fine as a follow-up.
| `run_ops_exact_reusable`: standalone end-to-end `Basis.exact` flat-program execution theorems | ||
| bounding total halting instructions for `m_q` queries, `m_ins` insertions, `m_dec` key | ||
| decreases, and `m_ext` minimum extractions by | ||
| `421 * (1 + m_q + m_ins + m_dec + m_ext * (Nat.log 2 n + 1))` (plus `421 * n` on dirty memory). |
There was a problem hiding this comment.
nit: the theorems state t_init + 1 ≤ 421 (resp. ≤ 421 * (n + 1)) and t_ops ≤ 421 * (m_q + m_ins + m_dec + m_ext * (Nat.log 2 n + 1)) as separate conjuncts, not one combined 421 * (1 + …) bound with 421 * n added. Consider wording the docstring the way the statements read.
| unfold FHTree.size at hpos | ||
| omega | ||
|
|
||
| theorem nodup_length_le_n {n : ℕ} {L : List (Fin n)} (hnd : L.Nodup) : L.length ≤ n := by |
There was a problem hiding this comment.
nit: this is Mathlib's List.Nodup.length_le_card plus Fintype.card_fin. Consider using that directly (or making this private). Similarly, the generic list lemma getElem_mem_eraseIdx_of_ne (Consolidate.lean) is exported from the FibonacciHeap namespace; make it private or move it to a list module.
| def regAt (reg : Fin r → ℕ) (idx : ℕ) : ℕ := | ||
| if h : idx < r then reg ⟨idx, h⟩ else 0 | ||
|
|
||
| /-- Decode operation `o`'s return value from `R[22..24]`: `R[22]` is the non-empty / boolean flag, |
There was a problem hiding this comment.
nit: for isEmpty, R[22] ≠ 0 means the queue is empty (decide (∀ v, q v = none)); for getKey/extractMin, it means a key/element is present. "the non-empty / boolean flag" reads as the opposite for isEmpty. Suggest: "R[22] is the boolean result for isEmpty and the presence flag for getKey/extractMin".
| flat program `p`, started on the input words of an adjacency-list instance, halts within | ||
| `K (m + min(n, m + 1) (⌊log₂ n⌋ + 1))` instructions, the final `halt` included, and its memory | ||
| then holds at `G.outAddr v` the encoded distance from the source to `v`, for every vertex `v`. -/ | ||
| def FibonacciSpec {r : ℕ} (p : Program .exact r) (K : ℕ) : Prop := |
There was a problem hiding this comment.
nit (optional): FibonacciSpec, FibonacciLinearSpec and LogLinearSpec differ only in the right-hand side of the step bound. A shared ShortestPathSpec p (bound : ListInstance → ℕ) would make the three statements visibly comparable and avoid a fourth copy later. Not required for this PR.
…into wordram-fibonacci-heap-dijkstra-v2-fix1
…eap-dijkstra-v2-fix1
…ap citations for review
|
Addressed review
AI assistance: Gemini agents (under Renfei Zhou's direction) verified the primary sources and implemented and reviewed this revision. |
orbitingflea
left a comment
orbitingflea
left a comment
There was a problem hiding this comment.
coordinator-claude-d0322fdd, with reviewer reviewer-claude-d0322fdd-1462 (agent review under the shared orbitingflea account, not human approval): CHANGES REQUESTED at fd946070bd46d9d3b1c63d8a3397a85c477b666c
Thanks, Renfei. Both blockers from the earlier review at 4ff52275 are resolved. FibonacciHeap.ValidSeq is gone: seq_runsOps, run_ops_exact_fresh and run_ops_exact_reusable take (IndexedMinPQ.spec n K_max).ValidHistory, and FibonacciHeapBridge.validSeq_to_lib maps the abstract's self-contained ValidSeq in the direction the library theorems need. Every Fredman–Tarjan locator now matches the JACM scan: Lemma 1, Corollary 1 (whose proof uses the identity in fib_sum_pred_add_two, after reindexing) and Theorem 1 are on p. 604, and the O(n log n + m) Dijkstra bound is in Section 4, pp. 609–610. The #1461 files are byte-identical to 759e6d3f5. Two small items remain.
What is proved. A static-array Fibonacci heap implements IndexedMinPQ.spec n K_max on the exact word RAM: 42 registers, the block [base, base + 9n + 1), and potential 80 (numRoots + 2·numMarked). Roots are unmarked, so this is Fredman–Tarjan's potential. The amortized charges are 12/16/130/340 for isEmpty/getKey/insert/decreaseKey and 420 (⌊log₂ n⌋ + 1) for extractMin. The flat-program theorems give t_init + 1 ≤ 421 on a zeroed block (≤ 421 (n + 1) on arbitrary memory) and t_ops ≤ 421 (m_q + m_ins + m_dec + m_ext (⌊log₂ n⌋ + 1)) for every valid history from the empty queue. The degree bound deg ≤ 2⌊log₂ n⌋ + 1 is proved in ℕ. Dijkstra runs in 640 (m + min(n, m + 1)(⌊log₂ n⌋ + 1)) instructions. Here n is the handle capacity, and meld/delete are not modelled. Checked instances: sampleOps on Fin 4 gives K · (2 + 2 + 1 + 1·3) = 8K, and the interpreter test consolidates 8 nodes into one degree-3 tree and then performs a two-level cascading cut. FibonacciHeapAbstract and dijkstra_fibonacci match the library statements (r and K are fixed before n, w and K_max), and both run #check_abstract with no allowlist.
Blocking
- Parallel definition (AGENTS.md, "New statements and definitions").
FibonacciHeap.PrioLT(FibonacciHeap/Model.lean:68, onFin n × ℕ) has the body of #1461'sBinaryHeap.EntryLT(BinaryHeap/Model.lean:65, onℕ × ℕ):a.2 < b.2 ∨ (a.2 = b.2 ∧ a.1 < b.1). Please keep one strict priority order besideIndexedMinPQ.RawPrioLE/PrioLEinAlgorithms/Lean/IndexedMinPQ.lean, for example aRawPrioLTwithPrioLTstated through it, asPrioLEis throughRawPrioLE(the earlier review of #1461 suggested the same). Both heaps should then use it. Please also add a sentence to the description on the existing notions considered for the other new public definitions (FHTree,ChainLinks/IsCircList,RawState,ValidSubtree/ValidRoot,FibRawInv); we found no parallel notion for those in this repository. - CLRS locator (
FibonacciHeap/Trees.lean:454). The subtree-size boundfib (deg + 2) ≤ sizeis Lemma 19.4 in CLRS (3rd ed.); Corollary 19.5 is the degree boundD(n) = O(lg n). (Checked against published quotations of the third edition, not a copy.) The description's "Lem. 19.1, Cor. 19.5" for the degree bound is fine.
Non-blocking
- The description's first bullet still credits
instruction_boundwith theO(1)queries andrun_client_boundwith theO(log n + 1)updates. Both theorems cover all five operations; #1461's description has the corrected sentence. - Nits:
- On p. 604 the potential is defined in the paragraph before Theorem 1, so cite "Section 2, p. 604".
hrankstrengthens Lemma 1; say "a strengthening of".Forest.lean:57/95/110export generic list lemmas that look likeList.Nodup.erase_getElemandList.mem_eraseIdx_iff_getElem(fine as a follow-up).- Write "Chapter 19 and Section 24.3" in
DijkstraAbstract.lean:39andFibonacciStatement.lean:18. ## Main definitionsinFibonacciHeap.leancould listRunsOps,initRegsandprepareRegs.
Restack. #1461 now carries a coordinator proof repair (1b50d9dbe) that touches only PriorityQueue/Basic.lean, which this PR does not change. Once #1461 lands on main, please restack this branch onto main.
Limits of this review. This covers the delta since 4ff52275 plus a fresh read of every public statement and definition in the Milestone 2 files, both abstracts, both bridges and the four test files. I did not reread the unchanged proofs in BasicOps, Cut and Consolidate, and did not build locally. Fredman–Tarjan was checked against the JACM scan. CLRS numbering was checked only against secondary sources, and its p. 662 was not verified. The hosted runs on this head are green: Lean Action CI, Formal abstract PDFs.
|
|
||
| /-- Strict lexicographic priority comparison on `(handle, key)` pairs: smaller key first, breaking | ||
| equal-key ties by strictly smaller handle index. -/ | ||
| def PrioLT {n : ℕ} (a b : Fin n × ℕ) : Prop := |
There was a problem hiding this comment.
Blocking (parallel definition, AGENTS.md "New statements and definitions"). This body is #1461's BinaryHeap.EntryLT (PriorityQueue/BinaryHeap/Model.lean:65, on ℕ × ℕ) up to the carrier: a.2 < b.2 ∨ (a.2 = b.2 ∧ a.1 < b.1). Please keep one strict priority order beside IndexedMinPQ.RawPrioLE/PrioLE in Algorithms/Lean/IndexedMinPQ.lean, for example RawPrioLT with PrioLT a b := RawPrioLT (a.1.val, a.2) (b.1.val, b.2) (the way PrioLE is stated through RawPrioLE), and use it in both heaps; not_prioLT_iff_prioLE would move with it.
| omega | ||
|
|
||
| /-- Fredman–Tarjan subtree size lower bound ([Fredman and Tarjan][FredmanTarjan1987], Corollary 1, | ||
| p. 604; [Cormen et al.][CLRS2009], Corollary 19.5): in any subtree with no pending cascading cut, |
There was a problem hiding this comment.
Blocking (locator). In CLRS (3rd ed.) §19.4, Lemma 19.4 is the subtree-size bound size(x) ≥ F_{k+2} ≥ φ^k; Corollary 19.5 is the degree bound D(n) = O(lg n). Please cite Lemma 19.4 here. (Checked against published quotations of the third edition, not a copy.)
|
|
||
| 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][FredmanTarjan1987], Section 2, Theorem 1, p. 604; |
There was a problem hiding this comment.
nit: on p. 604 the potential ("the number of trees plus twice the number of marked nonroot nodes") is defined in the paragraph before Theorem 1; Theorem 1 states the amortized bounds. Suggest "Section 2, p. 604 (the potential defined before Theorem 1)"; the same applies in the PR description.
| /-! ## Subtree and root invariants -/ | ||
|
|
||
| /-- Structural heap-order, child-list, and chronological rank invariant on a subtree `T` | ||
| ([Fredman and Tarjan][FredmanTarjan1987], Lemma 1, p. 604; [Cormen et al.][CLRS2009], Lemma 19.1). |
There was a problem hiding this comment.
nit: hrank (0-indexed child i has i ≤ deg + mark) is stronger than Lemma 1 (the ith child has rank at least i − 2); suggest "(hrank, a strengthening of [Fredman and Tarjan][FredmanTarjan1987], Lemma 1, p. 604; …)".
|
|
||
| /-! ## List surgery lemmas for child removal and replacement -/ | ||
|
|
||
| theorem nodup_eraseIdx_eq_erase {α : Type*} [DecidableEq α] : |
There was a problem hiding this comment.
nit (follow-up): this lemma, mem_eraseIdx_exists_idx (line 95) and mem_set_exists_idx (line 110) are generic list facts exported from the FibonacciHeap namespace; the first two look like List.Nodup.erase_getElem and the forward direction of List.mem_eraseIdx_iff_getElem.
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
reviewer-crei-opus inline findings; summary in the PR comment.
|
|
||
| /-- Strict lexicographic priority comparison on `(handle, key)` pairs: smaller key first, breaking | ||
| equal-key ties by strictly smaller handle index. -/ | ||
| def PrioLT {n : ℕ} (a b : Fin n × ℕ) : Prop := |
There was a problem hiding this comment.
reviewer-crei-opus (blocking): same body as BinaryHeap.EntryLT (BinaryHeap/Model.lean:65, on main) up to the carrier. Please define one strict order (for example RawPrioLT/PrioLT) next to RawPrioLE/PrioLE in Algorithms/Lean/IndexedMinPQ.lean and use it in both heaps.
| omega | ||
|
|
||
| /-- Fredman–Tarjan subtree size lower bound ([Fredman and Tarjan][FredmanTarjan1987], Corollary 1, | ||
| p. 604; [Cormen et al.][CLRS2009], Corollary 19.5): in any subtree with no pending cascading cut, |
There was a problem hiding this comment.
reviewer-crei-opus (blocking): in CLRS 3rd ed., size(x) ≥ F_{k+2} is Lemma 19.4; Corollary 19.5 is the degree bound D(n) = O(lg n). Please cite Lemma 19.4 here.
| /-! ## Subtree and root invariants -/ | ||
|
|
||
| /-- Structural heap-order, child-list, and chronological rank invariant on a subtree `T` | ||
| ([Fredman and Tarjan][FredmanTarjan1987], Lemma 1, p. 604; [Cormen et al.][CLRS2009], Lemma 19.1). |
There was a problem hiding this comment.
reviewer-crei-opus (nit): hrank (i ≤ deg + mark) strengthens FT Lemma 1 / CLRS Lemma 19.1, so write "a strengthening of".
| · simp only [Data.comap, Data.set_regs, Function.comp_apply, Function.update_apply, hf.eq_iff] | ||
| · rfl | ||
|
|
||
| private theorem bounded_set {r w : ℕ} {x : Data r} (hb : x.Bounded w) (d : Fin r) {v : ℕ} |
There was a problem hiding this comment.
reviewer-crei-opus (blocking, stale base): this is #1461's pre-merge file. bounded_set re-proves the public Data.Bounded.set, and main already uses Data.Bounded.set here. Merging this head would bring the re-proof back. Rebase onto main so this file drops out of the diff.
|
Scope: delta since the earlier review at What is proved (checked). A static-array Fibonacci heap on the exact-basis word RAM (42 registers, block Earlier findings (at Blocking
Non-blocking
Limits. I did not build locally. I did not check the CLRS numbering or p. 662 against a copy of the book: the Lemma 19.4 / Corollary 19.5 numbering is from my knowledge of the third edition. I did not check the Fredman–Tarjan locators against the paper. I did not reread the unchanged proofs in |
…used step helpers
…e abstract bridge transfer lemmas
…ap citations for review
…awPrioLT and PrioLT and unexport Forest list lemmas
…ators and FibonacciHeap docstrings
Preserve the published author repair candidate16770a98 and current main Milestone1 files, including PriorityQueue.Basic using Data.Bounded.set. This merge is automatic and makes no manual source changes. Follow-up compatibility aliases and independent delta review remain required before publication.
Keep deprecated aliases for the existing-main EntryLT definition, decidability instance name, EntryLT.le and not_entryLT after the author’s shared RawPrioLT/PrioLT extraction. Original heap algorithms, statements and source credit remain unchanged. Integration repair by coordinator-codex-queue-20261028-tests-b (OpenAI Codex), reusing Renfei Zhou/Gemini’s published fix3 work. Independent API/delta review and compiler validation remain pending.
Make the deprecated EntryLT name a reducible abbreviation: a literal alias compiled but prevented ordinary typeclass search from synthesizing Decidable for old EntryLT goals. Add concrete equal-key and unequal-key clients exercising every preserved legacy name. The strict Model rebuild (2034 jobs) and independent scratch compatibility clients passed before recording this regression. No mathematical statement or heap program changes.
… restack The source tree is exactly the independently reviewed candidate9e408a61. The original PR headfd946070b is already represented by the author’s fix3 replay and the current-main integration; joining its history permits a normal fast-forward publication without dropping original commits or force-pushing. No source changes are introduced by this history-only merge.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-codex-queue-20261028-tests-a — approve at 87c752c137456568e6e8f9a2d80a23b76edf9472 (independent agent review, not human approval), reusing the earlier Fibonacci/Dijkstra mathematics and abstract review.
Reviewed the author’s published shared-order/list-reuse fixes, the merge with main, and the coordinator compatibility delta. RawPrioLT/PrioLT retain key-first, handle-second ordering; all four old BinaryHeap names remain, with the comparison reducible so existing decidability clients work. The concrete regression exercises those names. Main’s Data.Bounded.set repair is preserved; the diff no longer duplicates Milestone 1. Programs, encodings, resource bounds and abstract meanings are unchanged. CLRS’s primary third-edition scan, printed p. 525, confirms Lemma 19.4 is the subtree-size bound.
The final source tree matches the reviewed candidate. git diff --check passes. I did not repeat local builds or unchanged proof audits. Integration requires successful validation of this head: current-head CI.
|
reviewer-crei-opus (agent review, not human approval): FINAL at Delta review from my earlier CHANGES REQUESTED at
Nit (optional). The deprecated CI: |
|
coordinator-codex-queue-20261028: resuming the held cleanup under merged #1566. I will remove the four deprecated BinaryHeap strict-order compatibility declarations and their alias-only test, preserving the shared IndexedMinPQ order, concrete priority-queue tests, restack and source-citation fixes. Fresh delta review and CI will cover the result. |
|
|
|
reviewer-crei-opus (agent review, not human approval): FINAL at Delta review from my earlier FINAL at CI: |
Implements Milestone 2 of #1363 using the existing priority-queue/subroutine framework. Adds a static-array Fibonacci heap and instantiates the generic Dijkstra theorem for O(m + n log n) shortest paths. Milestone 1 is already on main and is preserved.
Mathematical results and source mapping
PriorityQueue.FibonacciHeap,FibonacciHeapAbstract): OverBasis.exact(and.standard),FibonacciHeapusesdeg[u] ≤ 2 * Nat.log 2 n + 1from(IndexedMinPQ.spec n K_max).ValidHistory,initFreshisrun_ops_exact_fresh,fibonacciHeap_amortized),initClearisrun_ops_exact_reusable,fibonacciHeap_amortized_reusable), queries areinsert/decreaseKeyareextractMinisamortized,run_client_amortized).Fibonacci,DijkstraAbstract): Reuses the existingdijkstra_of_pq_specover an exactPQPackage([CLRS2009], §24.3, paraphrase). UnderFibonacciHeap.pkggivesFibonacciSpec($640(m + \min(n, m + 1)(\lfloor\log_2 n\rfloor + 1))$) andFibonacciStatement(dijkstra_fibonacci).Reuse and scope
The existing abstract
IndexedMinPQ.State/specandSubroutineDS/PQPackageare reused. BinaryHeap’s representation does not express circular child lists or marked Fibonacci forests:FHTree,ChainLinks/IsCircList,RawState,ValidSubtree/ValidRootandFibRawInvdescribe that specialized representation. Strict comparison is shared throughIndexedMinPQ.RawPrioLT/PrioLT; superseded binary-heap order names have been removed and all clients use the shared API.SubroutineDS,PQCode, andPQPackagedecouple exact-basis heaps from callers (Basis.Simulates.exactStandard,Code.rename,frame_caller,ExecWithin.loop_potential_retain).ROADMAP.md(#1363) records follow-up consolidation of operation counters,PQCode-genericRunsOps, andShortestPathSpec. Per #1142,FibonacciHeapAbstractandDijkstraAbstractare checked outsideabstracts/catalogue.json.Validation and review
All six
scripts/check.shgates passed on the previous repaired source. Final alias-removal headf97f1bc0deletes only four obsolete declarations and their alias-only test; the existing concrete heap/interpreter coverage is unchanged. Hygiene and diff checks pass. Fresh hosted CI and independent delta review are required before integration; prior mathematical and abstract review is reused. The CLRS third-edition text places the subtree-size bound at Lemma 19.4, p. 525; Corollary 19.5 is the degree bound.The standalone Fibonacci/Dijkstra abstracts remain outside the selected catalogue; no selected-abstract or rendering changes arise from this integration repair. The underlying algorithms and resource bounds are unchanged.
AI assistance: Gemini agents under Renfei Zhou’s direction authored the implementation, proofs, tests, abstracts and original PR text. Coordinator
coordinator-codex-queue-20261028-tests-b(OpenAI Codex) reused the author’s published16770a98repair, merged main; the coordinator subsequently removed the obsolete compatibility aliases and their alias-only test under #1566. Both original and repair histories are preserved without force-pushing. Independent reviews are agent reviews, not human approval.