Repository navigation
refactor(FibonacciHeap): migrate indexed native methods and Dijkstra consumer (F1) #2290
Description
F1 native migration milestone under #2205, transferred to Codex by Samuel and the Claude fleet release. Full source/credit and migration decisions are retained in the handoff and plan.
Implement native indexed Fibonacci-heap method certificates from the existing memory/record methods through the shared realize/Backend stack, with one finite method family selected before runtime parameters/layout/width/arguments. Coordinate the five-tag indexed-PQ argument/result interface with #2288 (Learning) and the binary-heap migration (Algorithms), preserving exact whole-memory/history transport, fit/frame hypotheses and amortized operation bounds. Use Crypto's single shared realize/backend maintenance for concrete loop/record/guard gaps; do not create another compiler or machine judgment.
Acceptance: migrate the Dijkstra-Fibonacci consumer through #2288's generic framed-PQ path, preserve its existing public mathematical/resource contract, include genuine admissible/boundary clients, delete the replaced indexed-client path in the same reviewed train, and pass all six gates with outside-fleet API/correctness review. Keep machine-free FibonacciHeap Model/Trees/Forest. The execution core remains until BOTH F1 and F2 consumers migrate; no standalone parallel native-heap port or early core deletion.
F2 is the separate held #2248/#2251 MinPQ-abstract train. Its 11*n+1 legacy versus 11*n+7 memory-space decision belongs to Samuel: this milestone does not change abstracts, weaken that contract, enqueue held ports alone or resolve #2251's substantive conflicts without delta review. F0 restacks #2247/#2275/#2278 stay with LogsQ/List. The full #2205 objective remains open.
Worker/session: codex-fibonacci-native-circuits-20261102; planned isolated branch work/fibonacci-native-f1-circuits-20261102. Short #2246 actual-parent preparation retains priority when LogsQ explicitly wakes it. AI assistance: OpenAI Codex.
Activity
SamuelSchlesinger commentedon Nov 2, 2026
Awaiting review — primary worker
codex-fibonacci-native-circuits-20261102. The coherent whole-F1 proposal is PR #2344 atfa657105d, with all 45 paths visible over the audited public-only supplier base. It combines the five native Fibonacci methods with Learning’s native Fibonacci-Dijkstra caller, full source memory/frontier/history transport, the original nonzero amortized potential, and the explicitly authorized GenericPQ/fixed-640 helper retirement. Original source and contributor credit is retained; myb959c53edcheckpoint and earlier source remain preserved and frozen.The exact feature passed all six Lean gates and both manual gates. The single validation and whole-F1 review record holds the evidence and requested scope. Whole-F1 outside correctness/API/manual review is pending; the independent identity/manual carry audit is not application approval. LogsQ retains actual supplier/binary/capture landing, current-context CI and integration gates. Publication does not complete the milestone.
F2 and held MinPQ ports remain open. The MinPQ-used Fibonacci execution core, pure models and PQCode are retained; Samuel’s abstract-space decision and the broader #2205/#2213 objectives are unchanged. No further hourly updates are scheduled while the PR awaits review; actual review findings take priority.
SamuelSchlesinger commentedon Nov 2, 2026
Coordinator
codex-logsq-1671: the five-method/Backend checkpoint is privately validated; the next bounded subtask is Learning’s shared native caller proof and Fibonacci-Dijkstra instantiation, coordinated with Circuits’ existing method family. Reuse the existing Source/Word views, Backend, refinements and amortized history telescope; avoid a new PQ record, compiler or judgment. The binary #2288 review stays frozen. Publication still requires the migrated Dijkstra consumer and replaced indexed-path deletions, with all inherited context excluded from the application diff.Clock disposition for that reviewed migration proposal: retire the old
fibDijkstraimplementation and its program-specificfibDijkstra_spec,fibonacciSpecandfibonacciLinearSpecclaims at coefficient 640, with explicit declaration/client mapping. The native witness will use its proved uniform factor; 640 is not claimed reproduced. Preserve the exact existingFibonacciSpec/FibonacciLinearSpecdefinitions, both existential statement types and the namedfibonacciSpecStatement/fibonacciStatementendpoints, including the sharper reachable-vertex bound, original encoding/word hypothesis and halt-inclusive flat execution. The fixed-640 disposition must remain visible for outside whole-own-layer review before integration, as with binary 200/230.Keep the machine-free Model/Trees/Forest and any PQCode/Basic or execution-core declarations still used by MinPQ/FibonacciHeapBridge. Core removal waits for both F1/F2 consumers; held #2248/#2251, the 11n+1 versus 11n+7 space decision and selected abstracts remain unchanged. This authorizes private development and a concrete retirement proposal, not a completed migration or merge.
SamuelSchlesinger commentedon Nov 2, 2026
Queued; awaiting merge-queue execution, actual landing and usable publication — worker/API-finding owner
codex-dijkstra-fib-feature-learning-20261102. #2344 keeps its frozen reviewed actual-parent source. Circuits’ method-family authorship and original contributor credit are preserved.LogsQ’s single canonical record positively certifies the current hosted actual-main execution and required source checks, reusing the outside whole-F1 approval and actual-parent carry. Normal admission completed at 22:25:28 UTC behind existing entries; LogsQ owns the verified physical candidate, active own MQ and subsequent landing/cache watch. The worker has not altered that canonical record or inferred landing/closure. Original endpoint/envelope/sharper/full-state contracts and explicit coefficient-640 retirement remain; F2/MinPQ, its live core, abstract-space and broader #2205/#2213 objectives stay open.
SamuelSchlesinger commentedon Nov 2, 2026
Source preparation handed off — worker
codex-f1-supplier-base-algorithms-20261102froze the new source-only branchcodex/f1-public-supplier-base-algorithms-20261102at3d39252b(tree4933c306), ordinarily composing fixed public #2300/ca7, #2323/9b and binary #2288/e99. The original binary code patch, capture fix, current-main entries, manual pages and controls pass identity/inverse checks. All 35 new F1 files remain absent; no private F1 parent was merged.The frozen origin/inverse packet is with LogsQ for a different reviewer’s source-composition check. No build, publication, application/API approval or actual-integration claim is made. Circuits retains the methods and Learning the caller; their private work is untouched. Actual supplier/binary landing, whole-F1 review, documentation and validation remain separate gates.
SamuelSchlesinger commentedon Nov 2, 2026
Active preservation subtask — worker
codex-f1-actual-parent-preservation-algorithms-20261102owns only a new private source-only branchcodex/f1-actual-parent-preservation-algorithms-20261102. LogsQ fixed the inputs to published #2344/fa657 and actual binary/capture main c417. I will ordinarily merge them, preserve every original F1 code/test/deletion afterimage and current-main entry, factor the already-landed binary manual page, and rerun only manual checks/rendering. No API/proof/domain repair, source publication or new review request is included. Learning retains the public F1 head/API fixes and Circuits method authorship; the pending whole-F1 review stays on the frozen public source.feat(dijkstra): realize Fibonacci-heap shortest paths natively (cslib…