Repository navigation
refactor(wordram): reuse Block.HoldsList in fusion-tree memory predicates #1509
Description
Follow-up requested in #1465 review. FusionTree.Stores in Complexity/Algorithms/WordRAM/FusionTree/Model.lean duplicates Block.HoldsList from Complexity/Computability/WordRAM/ListArray.lean (up to argument order); private stores_append duplicates Block.HoldsList.append.
Migrate the fusion-tree model and its regression client to the smaller generic list-array API, removing Stores/stores_append and updating every client. Preserve all memory-layout and execution theorem meanings, and check the representative fusion-tree client. No new memory model or 3SUM headline is needed. Available, unclaimed; the complete #1446 native preprocessing objective stays open.
Metadata
Metadata
Assignees
Labels
No labels
Activity
fix(wordram): export sorted radix keys from composed contracts
edemaine commentedon Oct 28, 2026
active — worker codex-chanhe-native-t3-28da2261 claims this available follow-up on actual branch t3/fusion-tree-holds-list, based on the published #1537 repair. I will migrate FusionTree's representation and regression clients to Block.HoldsList, delete Stores/stores_iff/stores_append, and reuse the small list-array API with any directly needed append decomposition there. Native layouts/programs and surviving meanings stay unchanged. #1537 requested changes are pushed; root #1546 owns the audit slot, so this work is source/MCP only until an explicit release. No new agents/reviews.
edemaine commentedon Oct 28, 2026
active — codex-chanhe-native-t3-28da2261: the three-file migration and concrete generic-read client are implemented on t3/fusion-tree-holds-list. ListArray, full Model and the layout/native-interpreter regression have clean targeted diagnostics; duplicate declarations are gone. Final all-six/static validation is queued behind root #1546's sole audit slot. Completed own MCP workers are released; no aggregate or static check is running here. No PR/completion claim until final validation.
edemaine commentedon Oct 28, 2026
awaiting review — codex-chanhe-native-t3-28da2261: #1557 completes the generic list-block migration, removes the superseded predicates/wrappers and updates the concrete layout client. All six gates and final static checks pass; preservation/reuse/abstract assessment and validation are in the PR. Coordinator/outside review routing requested; no new review agent commissioned. Issue remains open for review/integration. Audit slot explicitly released directly back to root for #1556.
feat(wordram): add native radix sorting and multiplicity arrays (csli…
SamuelSchlesinger commentedon Oct 29, 2026
Completed: fusion-tree representation reuses Block.HoldsList, preserving the representation and clients. Landed through #1570; verified on main with accepted source, contributor credit and API follow-ups retained. The broader #1394 objective, concrete fast ET backend and complete ordinary-3SUM/1.9992 endpoint remain open.
feat(3sum): integrate native preprocessing and conditional host (csli…